Theory QDistR

theory QDistR

imports QSizeR RBG QDiaSizeR

begin

consts

CLR :: "Rg => Rg => o"
SCLR :: "Rg => Rg => o"
NR :: "Rg => Rg => o"
SNR :: "Rg => Rg => o"
AR :: "Rg => Rg => o"
FAR :: "Rg => Rg => o"
MAR :: "Rg => Rg => o"

SpShR :: "Rg => o" 

defs

CLR_def: "CLR(a,b) == (EX c. (SpR(c) & CGR(c,a) & CGR(c,b) & NEGR(c,a)))"
SCLR_def: "SCLR(a,b) == ~CGR(a,b) & CLR(a,b)"
NR_def: "NR(a,b) == (EX c. (SpR(c) & CGR(c,a) & CGR(c,b) & (NEGR(c,a) | RSSR(c,a))))"
SNR_def: "SNR(a,b) == ~CLR(a,b) & NR(a,b)"
AR_def: "AR(a,b) == ~NR(a,b)"
FAR_def: "FAR(a,b) == (ALL c. (SpR(c) & CGR(c,a) & CGR(c,b) --> (NEGR(a,c))))"
MAR_def: "MAR(a,b) == AR(a,b) & ~ FAR(a,b)"

SpShR_def: "SpShR(a) == (EX b. (MinBSpR(b,a) & RSSR(a,b)))"

axioms

PR_imp_NR_imp_NR: "PR(a,b) ==>  (ALL c. (NR(a,c) --> NR(b,c)))"
LRSSR_and_NR_imp_NR: "[|LRSSR(a,b);NR(a,b)|] ==> NR(b,a)"



(* theorems *)

lemma SSR_or_notSSR: "ALL a b. (SSR(a,b) | ~SSR(a,b))"
apply(insert excluded_middle [of "SSR(a,b)"])
apply(auto)
done


theorem CGR_imp_CLR: "CGR(a,b) ==> CLR(a,b)"
apply(unfold CLR_def)
apply(unfold CGR_def)
apply(clarify)
apply(fold CGR_def)
apply(drule_tac a="c" in SpR_CoPPR_NEGR_exists)
apply(clarify)
apply(insert LER_total)
apply(rotate_tac 5)
apply(erule_tac x="a" in allE)
apply(rotate_tac 5)
apply(erule_tac x="c" in allE)
apply(erule disjE)
prefer 2
apply(drule_tac a="ba" and b="c" and c="a" in NEGR_and_LER_imp_NEGR)
apply(assumption)
apply(erule_tac x="ba" in allE)
apply(clarify)
apply(drule_tac a="ba" and b="a" in OR_imp_CGR)
apply(drule_tac a="ba" and b="b" in OR_imp_CGR)
apply(rule_tac x="ba" in exI)
apply(drule_tac a="ba" and b="c" in CoPPR_imp_SpR_and_SpR)
apply(safe)
apply(insert SSR_or_notSSR)
apply(rotate_tac 6)
apply(erule_tac x="a" in allE)
apply(rotate_tac 6)
apply(erule_tac x="c" in allE)
apply(safe)
apply(drule_tac a="a" and b="c" in SSR_sym)
apply(drule_tac a="c" and b="a" in SSR_imp_LER)
apply(drule_tac a="ba" and b="c" and c="a" in NEGR_and_LER_imp_NEGR)
apply(assumption)
apply(erule_tac x="ba" in allE)
apply(clarify)
apply(drule_tac a="ba" and b="a" in OR_imp_CGR)
apply(drule_tac a="ba" and b="b" in OR_imp_CGR)
apply(rule_tac x="ba" in exI)
apply(drule_tac a="ba" and b="c" in CoPPR_imp_SpR_and_SpR)
apply(safe)
apply(drule_tac a="ba" and b="c" in CoPPR_imp_SpR_and_SpR)
apply(clarify)
apply(drule_tac a="c" and b="a" in SpR_and_LER_and_notSSR_imp_CoPPR_and_SSR_exists)
apply(assumption)+
apply(clarify)
apply(frule_tac a="ca" and b="c" in CoPPR_imp_SpR_and_SpR)
apply(clarify)
apply(drule_tac a="ca" in SpR_CoPPR_NEGR_exists)
apply(clarify)
apply(drule_tac a="baa" and b="ca" and c="c" in CoPPR_trans)
apply(assumption)
apply(erule_tac x="baa" in allE)
apply(clarify)
apply(drule_tac a="ca" and b="a" in SSR_imp_LER)
apply(drule_tac a="baa" and b="ca" and c="a" in NEGR_and_LER_imp_NEGR)
apply(assumption)
apply(drule_tac a="baa" and b="a" in OR_imp_CGR)
apply(drule_tac a="baa" and b="b" in OR_imp_CGR)
apply(rule_tac x="baa" in exI)
apply(drule_tac a="baa" and b="c" in CoPPR_imp_SpR_and_SpR)
apply(safe)
done

theorem SCLR_imp_CLR: "SCLR(a,b) ==> CLR(a,b)"
apply(unfold SCLR_def)
apply(auto)
done

theorem CLR_imp_CGR_or_SCLR: "CLR(a,b) ==> (CGR(a,b) | SCLR(a,b))"
apply(unfold SCLR_def,unfold CLR_def)
apply(auto)
done

theorem CGR_imp_notSCLR: "CGR(a,b) ==> ~SCLR(a,b)"
apply(unfold SCLR_def)
apply(auto)
done

theorem CLR_imp_NR: "CLR(a,b) ==> NR(a,b)"
apply(unfold CLR_def,unfold NR_def)
apply(clarify)
apply(rule_tac x="c" in exI)
apply(safe)
done

theorem SNR_imp_NR: "SNR(a,b) ==> NR(a,b)"
apply(unfold SNR_def)
apply(auto)
done



theorem NR_imp_CLR_or_SNR: "NR(a,b) ==> (CLR(a,b) | SNR(a,b))"
apply(unfold SNR_def,unfold CLR_def)
apply(clarify)
done

theorem CLR_imp_notSNR: "CLR(a,b) ==> ~SNR(a,b)"
apply(unfold SNR_def)
apply(auto)
done


theorem FAR_imp_AR: "FAR(a,b) ==> AR(a,b)"
apply(rule ccontr)
apply(unfold AR_def)
apply(auto)
apply(unfold FAR_def,unfold NR_def)
apply(safe)
apply(erule_tac x="c" in allE)
apply(safe)
apply(drule_tac a="c" and b="a" in NEGR_assym)
apply(safe)
apply(erule_tac x="c" in allE)
apply(safe)
apply(drule_tac a="c" and b="a" in RSSR_sym)
apply(drule_tac a="a" and b="c" in RSSR_imp_notNEGR)
apply(safe)
done

theorem MAR_imp_AR: "MAR(a,b) ==> AR(a,b)"
apply(unfold MAR_def)
apply(auto)
done

theorem AR_imp_MAR_or_FAR: "AR(a,b) ==> (MAR(a,b) | FAR(a,b))"
apply(unfold MAR_def,unfold FAR_def)
apply(clarify)
apply(erule_tac x="c" in allE)
apply(auto)
done

theorem MAR_imp_notFAR: "MAR(a,b) ==> ~FAR(a,b)"
apply(unfold MAR_def)
apply(auto)
done


theorem NR_or_AR: "NR(a,b) | AR(a,b)"
apply(unfold AR_def)
apply(auto)
done

theorem CLR_refl: "(ALL a. CLR(a,a))"
apply(unfold CLR_def)
apply(clarify)
apply(insert SP_PPR_exists)
apply(drule allI)
apply(erule_tac x="a"in allE)
apply(clarify)
apply(frule_tac a="b" in SpR_CoPPR_NEGR_exists)
apply(clarify)
apply(frule_tac a="ba" and b="b" in CoPPR_imp_SpR_and_SpR)
apply(drule_tac a="b" and b="a" in PPR_imp_PR)
apply(drule_tac a="ba" and b="b" and c="a" in NEGR_and_PR_imp_NEGR)
apply(safe)
apply(rule_tac x="ba" in exI)
apply(drule_tac a="ba" and b="b" in CoPPR_imp_PPR)
apply(drule_tac a="ba" and b="b" in PPR_imp_PR)
apply(drule_tac a="ba" and b="b" and c="a" in PR_trans_rule)
apply(assumption)
apply(drule_tac a="ba" and b="a" in PR_imp_CGR)
apply(auto)
done

theorem NR_refl: "(ALL a. NR(a,a))"
apply(clarify)
apply(rule_tac a="a" in CLR_imp_NR)
apply(insert CLR_refl)
apply(auto)
done

theorem SCLR_irrefl: "(ALL a. ~SCLR(a,a))"
apply(unfold SCLR_def)
apply(insert CGR_refl)
apply(insert CLR_refl)
apply(auto)
done

theorem SNR_irrefl: "(ALL a. ~SNR(a,a))"
apply(unfold SNR_def)
apply(insert CLR_refl)
apply(insert NR_refl)
apply(auto)
done

theorem AR_irrefl: "(ALL a. ~AR(a,a))"
apply(unfold AR_def)
apply(insert NR_refl)
apply(auto)
done


theorem FAR_irrefl: "(ALL a. ~FAR(a,a))"
apply(insert FAR_imp_AR,insert AR_irrefl)
apply(auto)
done


theorem CLR_and_PR_imp_CLR: "[|CLR(a,b);PR(b,c)|] ==> CLR(a,c)"
apply(unfold CLR_def)
apply(clarify)
apply(rule_tac x="ca" in exI)
apply(clarify)
apply(drule_tac a="ca" and b="b" in CGR_sym)
apply(drule_tac a="b" and b="c" and c="ca" in PR_and_CGR_imp_CGR)
apply(assumption)
apply(drule_tac a="c" and b="ca" in CGR_sym)
apply(assumption)
done


theorem NR_and_PR_imp_NR: "[|NR(a,b);PR(b,c)|] ==> NR(a,c)"
apply(unfold NR_def)
apply(clarify)
apply(rule_tac x="ca" in exI)
apply(safe)
apply(drule_tac a="ca" and b="b" in CGR_sym)
apply(drule_tac a="b" and b="c" and c="ca" in PR_and_CGR_imp_CGR)
apply(assumption)
apply(drule_tac a="c" and b="ca" in CGR_sym)
apply(assumption)
apply(drule_tac a="ca" and b="b" in CGR_sym)
apply(drule_tac a="b" and b="c" and c="ca" in PR_and_CGR_imp_CGR)
apply(assumption)
apply(drule_tac a="c" and b="ca" in CGR_sym)
apply(assumption)
done


theorem PR_and_notNR_imp_notNR: "[|PR(a,b);~NR(b,c)|] ==> ~NR(a,c)"
apply(rule ccontr)
apply(auto)
apply(drule PR_imp_NR_imp_NR [of a b])
apply(auto)
done

theorem PR_imp_NR: "PR(a,b) ==> (NR(a,b) & NR(b,a))"
apply(safe)
apply(drule PR_imp_CGR [of a b])
apply(drule CGR_imp_CLR [of a b])
apply(drule CLR_imp_NR [of a b])
apply(assumption)
apply(drule PR_imp_NR_imp_NR [of a b])
apply(erule_tac x="a" in allE)
apply(insert NR_refl)
apply(erule_tac x="a" in allE)
apply(auto)
done

theorem PR_and_AR_imp_AR: "[|PR(a,b);AR(b,c)|] ==> AR(a,c)"
apply(unfold AR_def)
apply(rule ccontr)
apply(auto)
apply(drule PR_and_notNR_imp_notNR [of a b c])
apply(auto)
done

(* theorems about when the distance relations are symmetric *)

theorem LRSSR_and_CLR_imp_CLR: "[|LRSSR(a,b);CLR(a,b)|] ==> CLR(b,a)"
apply(unfold LRSSR_def)
apply(safe)
apply(unfold CLR_def)
apply(clarify)
apply(rule_tac x="c" in exI)
apply(clarify)
apply(drule_tac a="c" and b="a" and c="b" in NEGR_and_LER_imp_NEGR)
apply(assumption,assumption)
apply(clarify)
apply(rule_tac x="c" in exI)
apply(clarify)
apply(drule_tac a="c" and b="a" and c="b" in NEGR_and_RSSR_imp_NEGR)
apply(safe)
done

theorem LRSSR_and_SCLR_imp_SCLR: "[|LRSSR(a,b);SCLR(a,b)|] ==> SCLR(b,a)"
apply(unfold SCLR_def)
apply(safe)
apply(drule CGR_sym)
apply(safe)
apply(rule LRSSR_and_CLR_imp_CLR)
apply(auto)
done



theorem RSSR_and_SNR_imp_SNR: "[|RSSR(a,b);SNR(a,b)|] ==> SNR(b,a)"
apply(unfold SNR_def)
apply(drule RSSR_imp_LRSSR_and_LRSSR)
apply(safe)
apply(drule_tac a="b" and b="a" in LRSSR_and_CLR_imp_CLR)
apply(auto)
apply(rule LRSSR_and_NR_imp_NR)
apply(auto)
done

theorem LRSSR_and_SNR_imp_NR: "[|LRSSR(a,b);SNR(a,b)|] ==> NR(b,a)"
apply(unfold SNR_def)
apply(clarify)
apply(rule LRSSR_and_NR_imp_NR)
apply(auto)
done


theorem LRSSR_and_AR_imp_AR: "[|LRSSR(b,a);AR(a,b)|] ==> AR(b,a)"
apply(unfold AR_def)
apply(insert LRSSR_and_NR_imp_NR)
apply(auto)
done


theorem LRSSR_and_FAR_imp_FAR: "[|LRSSR(b,a);FAR(a,b)|] ==> FAR(b,a)"
apply(unfold LRSSR_def)
apply(safe)
apply(unfold FAR_def)
apply(safe)
apply(erule_tac x="c" in allE)
apply(safe)
apply(drule_tac a="b" and b="a" and c="c" in LER_and_NEGR_imp_NEGR)
apply(auto)
apply(erule_tac x="c" in allE)
apply(safe)
apply(rule RSSR_and_NEGR_imp_NEGR)
apply(auto)
done


theorem LRSSR_and_MAR_imp_AR: "[|LRSSR(b,a);MAR(a,b)|] ==> AR(b,a)"
apply(unfold MAR_def)
apply(insert LRSSR_and_AR_imp_AR)
apply(auto)
done

theorem RSSR_and_MAR_imp_MAR: "[|RSSR(a,b);MAR(a,b)|] ==> MAR(b,a)"
apply(unfold MAR_def)
apply(drule RSSR_imp_LRSSR_and_LRSSR)
apply(safe)
apply(rule LRSSR_and_AR_imp_AR)
apply(auto)
apply(drule_tac a="b" and b="a" in LRSSR_and_FAR_imp_FAR)
apply(auto)
done

(* composition tables *)

(* we leave this for later ...

theorem SpR_imp_SpShR: "SpR(a) ==> SpShR(a)"
apply(unfold SpShR_def)
apply(simp add: SpR_iff_MinBSpR)
apply(rule_tac x="a" in exI)
apply(insert RSSR_refl)
apply(auto)
done

theorem C_and_C_and_MinNSpR_and_RSSR_imp_NR: "[|CGR(a,b);CGR(b,c);MinBSpR(sb,b);RSSR(a,sb)|] ==> NR(a,c)"
apply(unfold NR_def)
apply(unfold MinBSpR_def)
apply(clarify)
apply(drule_tac a="a" and b="b" in CGR_sym)
apply(frule_tac a="b" and b="sb" and c="a" in PR_and_CGR_imp_CGR) 
apply(assumption)
apply(drule_tac a="b" and b="sb" and c="c" in PR_and_CGR_imp_CGR) 
apply(assumption)
apply(rule_tac x="sb" in exI)
apply(rule conjI)
apply(assumption)
apply(rule conjI)
apply(assumption)
apply(rule conjI)
apply(assumption)
apply(rule disjI2)
apply(rule RSSR_sym)
apply(assumption)
done

theorem C_and_C_and_MinNSpR_and_NEGR_imp_ClR: "[|CGR(a,b);CGR(b,c);MinBSpR(sb,b);NEGR(sb,a)|] ==> CLR(a,c)"
apply(unfold CLR_def)
apply(unfold MinBSpR_def)
apply(clarify)
apply(drule_tac a="a" and b="b" in CGR_sym)
apply(frule_tac a="b" and b="sb" and c="a" in PR_and_CGR_imp_CGR) 
apply(assumption)
apply(frule_tac a="b" and b="sb" and c="c" in PR_and_CGR_imp_CGR) 
apply(assumption)
apply(rule_tac x="sb" in exI)
apply(auto)
done


theorem CGR_and_SCLR_and_RSSR_imp_notFAR: "[|CGR(a,b);SCLR(b,c);RSSR(a,b)|] ==> ~FAR(a,c)"
apply(rule ccontr)
apply(auto)
apply(unfold FAR_def,unfold SCLR_def)
apply(unfold CLR_def)
apply(clarify)
apply(insert PR_sum)
apply(rotate_tac 8)
apply(erule_tac x="ca" in allE)
apply(rotate_tac 8)
apply(erule_tac x="b" in allE)
apply(clarify)
apply(insert MinBSpR_exists)
apply(drule allI)
apply(rotate_tac 9)
apply(erule_tac x="caa" in allE)
apply(clarify)
apply(erule_tac x="ba" in allE)
apply(unfold MinBSpR_def)
apply(clarify)
apply(frule_tac a="ca" and b="b" and c="caa" in Sum_imp_PR_and_PR)
apply(clarify)
apply(frule_tac a="b" and b="caa" and c="ba" in PR_trans_rule)
apply(clarify)
apply(drule_tac a="a" and b="b" in CGR_sym)
apply(frule_tac a="b" and b="ba" and c="a" in PR_and_CGR_imp_CGR)
apply(clarify)

apply(frule_tac a="ca" and b="caa" and c="ba" in PR_trans_rule)
apply(clarify)
apply(frule_tac a="ca" and b="ba" and c="c" in PR_and_CGR_imp_CGR)
apply(clarify)
apply(safe)
apply(drule_tac a="a" and b="b" in RSSR_sym)
apply(drule_tac a="b" and b="a" and c="ba" in RSSR_and_NEGR_imp_NEGR)
apply(clarify)
apply(frule_tac a="b" and b="ba" in PR_imp_Sum)

done

theorem CGR_and_SCLR_and_MinNSpR_and_RSSR_imp_NR: "[|CGR(a,b);SCLR(b,c);MinBSpR(sb,b);MinBSpR(sa,a);MinBSpR(sc,c);RSSR(a,sb);BR(sa,sb,sc)|] ==> NR(a,c)"
apply(unfold NR_def)
apply(unfold SCLR_def)
apply(unfold CLR_def)
apply(unfold BR_def)
apply(clarify)
apply(drule_tac a="a" and b="b" in CGR_sym)
apply(frule_tac a="b" and b="sb" and c="a" in PR_and_CGR_imp_CGR) 
apply(assumption)
apply(drule_tac a="b" and b="sb" and c="c" in PR_and_CGR_imp_CGR) 
apply(assumption)
apply(rule_tac x="sb" in exI)
apply(rule conjI)
apply(assumption)
apply(rule conjI)
apply(assumption)
apply(rule conjI)
apply(assumption)
apply(rule disjI2)
apply(rule RSSR_sym)
apply(assumption)
done

*)

end