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
lemma SSR_or_notSSR:
∀a b. SSR(a, b) ∨ ¬ SSR(a, b)
theorem CGR_imp_CLR:
CGR(a, b) ==> CLR(a, b)
theorem SCLR_imp_CLR:
SCLR(a, b) ==> CLR(a, b)
theorem CLR_imp_CGR_or_SCLR:
CLR(a, b) ==> CGR(a, b) ∨ SCLR(a, b)
theorem CGR_imp_notSCLR:
CGR(a, b) ==> ¬ SCLR(a, b)
theorem CLR_imp_NR:
CLR(a, b) ==> NR(a, b)
theorem SNR_imp_NR:
SNR(a, b) ==> NR(a, b)
theorem NR_imp_CLR_or_SNR:
NR(a, b) ==> CLR(a, b) ∨ SNR(a, b)
theorem CLR_imp_notSNR:
CLR(a, b) ==> ¬ SNR(a, b)
theorem FAR_imp_AR:
FAR(a, b) ==> AR(a, b)
theorem MAR_imp_AR:
MAR(a, b) ==> AR(a, b)
theorem AR_imp_MAR_or_FAR:
AR(a, b) ==> MAR(a, b) ∨ FAR(a, b)
theorem MAR_imp_notFAR:
MAR(a, b) ==> ¬ FAR(a, b)
theorem NR_or_AR:
NR(a, b) ∨ AR(a, b)
theorem CLR_refl:
∀a. CLR(a, a)
theorem NR_refl:
∀a. NR(a, a)
theorem SCLR_irrefl:
∀a. ¬ SCLR(a, a)
theorem SNR_irrefl:
∀a. ¬ SNR(a, a)
theorem AR_irrefl:
∀a. ¬ AR(a, a)
theorem FAR_irrefl:
∀a. ¬ FAR(a, a)
theorem CLR_and_PR_imp_CLR:
[| CLR(a, b); PR(b, c) |] ==> CLR(a, c)
theorem NR_and_PR_imp_NR:
[| NR(a, b); PR(b, c) |] ==> NR(a, c)
theorem PR_and_notNR_imp_notNR:
[| PR(a, b); ¬ NR(b, c) |] ==> ¬ NR(a, c)
theorem PR_imp_NR:
PR(a, b) ==> NR(a, b) ∧ NR(b, a)
theorem PR_and_AR_imp_AR:
[| PR(a, b); AR(b, c) |] ==> AR(a, c)
theorem LRSSR_and_CLR_imp_CLR:
[| LRSSR(a, b); CLR(a, b) |] ==> CLR(b, a)
theorem LRSSR_and_SCLR_imp_SCLR:
[| LRSSR(a, b); SCLR(a, b) |] ==> SCLR(b, a)
theorem RSSR_and_SNR_imp_SNR:
[| RSSR(a, b); SNR(a, b) |] ==> SNR(b, a)
theorem LRSSR_and_SNR_imp_NR:
[| LRSSR(a, b); SNR(a, b) |] ==> NR(b, a)
theorem LRSSR_and_AR_imp_AR:
[| LRSSR(b, a); AR(a, b) |] ==> AR(b, a)
theorem LRSSR_and_FAR_imp_FAR:
[| LRSSR(b, a); FAR(a, b) |] ==> FAR(b, a)
theorem LRSSR_and_MAR_imp_AR:
[| LRSSR(b, a); MAR(a, b) |] ==> AR(b, a)
theorem RSSR_and_MAR_imp_MAR:
[| RSSR(a, b); MAR(a, b) |] ==> MAR(b, a)