theory RBG imports EMR QSizeR begin consts SpR :: "Rg => o" MxSpR :: "Rg => Rg => Rg => o" CoPPR :: "Rg => Rg => o" CGR :: "Rg => Rg => o" CNGSpR :: "Rg => Rg => o" ECR :: "Rg => Rg => o" DCR :: "Rg => Rg => o" defs MxSpR_def: "MxSpR(a,b,c) == SpR(a) & SpR(b) & SpR(c) & PR(a,c) & PR(b,c) & ~OR(a,b) & (ALL e. (SpR(e) & PR(a,e) --> (a = e | OR(e,b) | ~PR(e,c))))" CoPPR_def: "CoPPR(a,b) == SpR(a) & SpR(b) & PPR(a,b) & (ALL c d. (MxSpR(c,a,b) & MxSpR(d,a,b) --> SSR(c,d)))" CGR_def: "CGR(a,b) == (EX c. (SpR(c) & OR(c,a) & OR(c,b) & (ALL d. (CoPPR(d,c) --> (OR(d,a) & OR(d,b))))))" CNGSpR_def: "CNGSpR(a,b) == SpR(a) & SpR(b) & (EX ca cb. (CoPPR(ca,cb) & MxSpR(a,ca,cb) & MxSpR(b,ca,cb)))" ECR_def: "ECR(a,b) == CGR(a,b) & ~OR(a,b)" DCR_def: "DCR(a,b) == ~CGR(a,b)" axioms SP_nested: "[|Sp(a);Sp(b);Sp(c);MxSpR(u,a,c);MxSpR(v,a,c);(ALL ua va. (((MxSpR(ua,a,b) & MxSpR(va,a,b)) | (MxSpR(ua,b,c) & MxSpR(va,b,c))) --> SSR(ua,va)))|] ==> SSR(u,v)" (* in the paper is only the transitivity axiom for CoPPR and not this version *) SP_PPR_exists: "EX b. (SpR(b) & PPR(b,a))" SSR_imp_CoPPR_and_MxSpR: "[|SpR(a);SpR(b);SSR(a,b)|] ==> (EX ca cb. (CoPPR(ca,cb) & MxSpR(a,ca,cb) & MxSpR(b,ca,cb)))" CGR_imp_CGR_imp_PR: "(ALL c. (CGR(c,a) --> CGR(c,b))) ==> PR(a,b)" SpR_CoPPR_NEGR_exists: "SpR(a) ==> (EX b. CoPPR(b,a) & NEGR(b,a))" SpR_and_LER_and_notSSR_imp_CoPPR_and_SSR_exists: "[|SpR(a);LER(b,a);~SSR(b,a)|] ==> (EX c. (CoPPR(c,a) & SSR(c,b)))" SpR_and_SpR_and_PP_imp_MaxSpR: "[|SpR(a);SpR(b);PPR(a,b)|] ==> (EX c. (MxSpR(c,a,b)))" (* SpR_and_SumR_imp_CGR: "[|SpR(a);SumR(b,c,a)|] ==> CGR(b,c)" self-connectedness-might be usefull? *) (* theorem CGR_imp_CGR_imp_PR: " (ALL c. (CGR(c,a) --> CGR(c,b))) ==> PR(a,b)" apply(rule_tac a="a" and b="b" in OR_imp_OR_imp_PR) apply(clarify) apply(drule_tac a="c" and b="a" in OR_imp_CGR) apply(erule_tac x="c" in allE) apply(clarify) at this point it seems to be clear that this cannot be provable *) (* theorems *) lemma SP_PR_exists: "EX b. (SpR(b) & PR(b,a))" apply(insert SP_PPR_exists [of a]) apply(clarify) apply(drule_tac b="a" and a="b" in PPR_imp_PR) apply(rule_tac x="b" in exI) apply(safe) done lemma CoPPR_imp_PPR: "CoPPR(a,b) ==> PPR(a,b)" apply(unfold CoPPR_def) apply(auto) done lemma CoPPR_imp_SpR_and_SpR: "CoPPR(a,b) ==> (SpR(a) & SpR(b))" apply(unfold CoPPR_def) apply(auto) done theorem CoPPR_asym: "CoPPR(a,b) ==> ~CoPPR(b,a)" apply(unfold CoPPR_def) apply(insert PPR_asym) apply(auto) done theorem CoPPR_trans: "[|CoPPR(a,b);CoPPR(b,c)|] ==> CoPPR(a,c)" apply(unfold CoPPR_def) apply(safe) apply(rule_tac a="a" and b="b" and c="c" in PPR_trans) apply(assumption)+ apply(rule_tac a="a" and b="b" and c="c" and u="ca" and v="d" in SP_nested) apply(auto) done theorem PPR_exists: "(EX b. PPR(b,a))" apply(insert SP_PPR_exists) apply(auto) done theorem Sp_CoPPR_exists: "SpR(a) ==> (EX b. CoPPR(b,a))" apply(insert SP_PPR_exists [of a]) apply(clarify) apply(insert SpR_and_LER_and_notSSR_imp_CoPPR_and_SSR_exists [of a]) apply(frule_tac a="b" and b="a" in PPR_imp_notSSR) apply(drule_tac a="b" and b="a" in PPR_imp_PR) apply(frule_tac a="b" and b="a" in PR_imp_LER) apply(auto) done theorem PR_and_NEGR_exists: "EX b. (PR(b,a) & NEGR(b,a))" apply(insert SP_PPR_exists [of a]) apply(clarify) apply(drule_tac a="b" in SpR_CoPPR_NEGR_exists) apply(clarify) 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(assumption) 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(rule_tac x="ba" in exI) apply(safe) done theorem CGR_refl: "CGR(a,a)" apply(insert SP_PR_exists [of a]) apply(clarify) apply(unfold CGR_def) apply(rule_tac x="b" in exI) apply(safe) apply(rule_tac a="b" and b="a" in PR_imp_OR,assumption)+ apply(unfold CoPPR_def) apply(clarify) apply(drule_tac a="d" and b="b" and c="a" in PPR_and_PR_imp_PPR) apply(assumption) apply(drule_tac a="d" and b="a" in PPR_imp_PR) apply(drule_tac a="d" and b="a" in PR_imp_OR) apply(assumption) apply(clarify) apply(drule_tac a="d" and b="b" and c="a" in PPR_and_PR_imp_PPR) apply(assumption) apply(drule_tac a="d" and b="a" in PPR_imp_PR) apply(drule_tac a="d" and b="a" in PR_imp_OR) apply(assumption) done theorem CGR_sym: "CGR(a,b) ==> CGR(b,a)" apply(unfold CGR_def) apply(clarify) apply(rule_tac x="c" in exI) apply(auto) done theorem PR_imp_CGR_imp_CGR: "PR(a,b) ==> (ALL c. (CGR(c,a) --> CGR(c,b)))" apply(unfold CGR_def) apply(clarify) apply(rule_tac x="ca" in exI) apply(safe) apply(drule_tac a="ca" and b="a" in OR_sym) apply(drule_tac a="a" and b="b" and c="ca" in PR_and_OR) apply(assumption) apply(simp add: OR_sym) apply(erule_tac x="d" in allE) apply(force) apply(erule_tac x="d" in allE) apply(safe) apply(drule_tac a="d" and b="a" in OR_sym) apply(drule_tac a="a" and b="b" and c="d" in PR_and_OR) apply(assumption) apply(simp add:OR_sym) done theorem OR_imp_CGR: "OR(a,b) ==> CGR(a,b)" apply(unfold OR_def) apply(clarify) apply(drule_tac a="c" and b="a" in PR_imp_CGR_imp_CGR) apply(drule_tac a="c" and b="b" in PR_imp_CGR_imp_CGR) apply(erule_tac x="c" in allE) apply(insert CGR_refl) apply(auto) apply(insert CGR_sym) apply(auto) done theorem PR_iff_CGR_imp_CGR: "PR(a,b) <-> (ALL c. (CGR(c,a) --> CGR(c,b)))" apply(rule iffI) apply(drule_tac a="a" and b="b" in PR_imp_CGR_imp_CGR) apply(assumption) apply(drule_tac a="a" and b="b" in CGR_imp_CGR_imp_PR) apply(assumption) done theorem Id_iff_CGR_iff_CGR: "a=b <-> (ALL c. (CGR(c,a) <-> CGR(c,b)))" apply(rule iffI) apply(simp) apply(rule_tac a="a" and b="b" in PR_antisym_rule) apply(simp add: PR_iff_CGR_imp_CGR) apply(simp add: PR_iff_CGR_imp_CGR) done theorem PR_imp_CGR: "PR(a,b) ==> CGR(a,b)" apply(insert PR_imp_CGR_imp_CGR) apply(insert CGR_refl) apply(auto) done theorem PR_and_CGR_imp_CGR: "[|PR(a,b);CGR(a,c)|] ==> CGR(b,c)" apply(drule PR_imp_CGR_imp_CGR) apply(insert CGR_sym) apply(auto) done theorem PR_and_notCGR_imp_notCGR: "[|PR(a,b);~CGR(b,c)|] ==> ~CGR(a,c)" apply(insert PR_and_CGR_imp_CGR) apply(auto) done theorem Sp_sum: "OR(w,a) <-> (EX b. (SpR(b) & PR(b,a) & OR(w,b)))" apply(safe) apply(unfold OR_def) apply(clarify) apply(insert SP_PR_exists) apply(drule allI) apply(erule_tac x="c" in allE) apply(clarify) apply(rule_tac x="b" in exI) apply(safe) apply(rule_tac a="b" and b="c" and c="a" in PR_trans_rule) apply(auto) apply(drule_tac a="b" and b="c" and c="w" in PR_trans_rule) apply(assumption) apply(rule_tac x="b" in exI) apply(safe) apply(rule_tac a="b" in PR_refl_rule) apply(drule_tac a="c" and b="b" and c="a" in PR_trans_rule) apply(assumption) apply(rule_tac x="c" in exI) apply(auto) done theorem Sp_imp_CNGSpR: "SpR(a) ==> CNGSpR(a,a)" apply(unfold CNGSpR_def) apply(clarify) apply(insert SSR_refl_rule [of a]) apply(insert SSR_imp_CoPPR_and_MxSpR [of a a]) apply(auto) done theorem CNGSpR_imp_SSR: "CNGSpR(a,b) ==> SSR(a,b)" apply(unfold CNGSpR_def) apply(clarify) apply(unfold CoPPR_def) apply(clarify) apply(erule_tac x="a" in allE) apply(erule_tac x="b" in allE) apply(auto) done theorem Sp_and_SSR_imp_CNGSpR: "[|SpR(a);SpR(b);SSR(a,b)|] ==> CNGSpR(a,b)" apply(unfold CNGSpR_def) apply(frule_tac a="a" and b="b" in SSR_imp_CoPPR_and_MxSpR) apply(auto) done theorem Sp_imp_SSR_iff_CONSpR: "[|SpR(a);SpR(b)|] ==> (SSR(a,b) <-> CNGSpR(a,b))" apply(insert Sp_and_SSR_imp_CNGSpR) apply(insert CNGSpR_imp_SSR) apply(auto) done theorem CNGSpR_imp_Sp_and_Sp: "CNGSpR(a,b) ==> (SpR(a) & SpR(b))" apply(unfold CNGSpR_def) apply(auto) done theorem CNGSpR_sym: "CNGSpR(a,b) ==> CNGSpR(b,a)" apply(unfold CNGSpR_def) apply(auto) done theorem CNGSpR_trans: "[|CNGSpR(a,b);CNGSpR(b,c)|] ==> CNGSpR(a,c)" apply(frule_tac a="a" and b="b" in CNGSpR_imp_SSR) apply(frule_tac a="b" and b="c" in CNGSpR_imp_SSR) apply(drule_tac a="a" and b="b" in CNGSpR_imp_Sp_and_Sp) apply(drule_tac a="b" and b="c" in CNGSpR_imp_Sp_and_Sp) apply(drule_tac a="a" and b="b" and c="c" in SSR_trans) apply(safe) apply(drule_tac a="a" and b="c" in Sp_and_SSR_imp_CNGSpR) apply(auto) done theorem ECR_sym: "ECR(a,b) ==> ECR(b,a)" apply(unfold ECR_def) apply(insert OR_sym) apply(insert CGR_sym) apply(auto) done theorem ECR_irrefl: "~ECR(a,a)" apply(unfold ECR_def) apply(insert CGR_refl) apply(insert OR_refl) apply(auto) done theorem DCR_sym: "DCR(a,b) ==> DCR(b,a)" apply(unfold DCR_def) apply(insert CGR_sym) apply(auto) done theorem DCR_irrefl: "~DCR(a,a)" apply(unfold DCR_def) apply(insert CGR_refl) apply(auto) done end
lemma SP_PR_exists:
∃b. SpR(b) ∧ PR(b, a)
lemma CoPPR_imp_PPR:
CoPPR(a, b) ==> PPR(a, b)
lemma CoPPR_imp_SpR_and_SpR:
CoPPR(a, b) ==> SpR(a) ∧ SpR(b)
theorem CoPPR_asym:
CoPPR(a, b) ==> ¬ CoPPR(b, a)
theorem CoPPR_trans:
[| CoPPR(a, b); CoPPR(b, c) |] ==> CoPPR(a, c)
theorem PPR_exists:
∃b. PPR(b, a)
theorem Sp_CoPPR_exists:
SpR(a) ==> ∃b. CoPPR(b, a)
theorem PR_and_NEGR_exists:
∃b. PR(b, a) ∧ NEGR(b, a)
theorem CGR_refl:
CGR(a, a)
theorem CGR_sym:
CGR(a, b) ==> CGR(b, a)
theorem PR_imp_CGR_imp_CGR:
PR(a, b) ==> ∀c. CGR(c, a) --> CGR(c, b)
theorem OR_imp_CGR:
OR(a, b) ==> CGR(a, b)
theorem PR_iff_CGR_imp_CGR:
PR(a, b) <-> (∀c. CGR(c, a) --> CGR(c, b))
theorem Id_iff_CGR_iff_CGR:
a = b <-> (∀c. CGR(c, a) <-> CGR(c, b))
theorem PR_imp_CGR:
PR(a, b) ==> CGR(a, b)
theorem PR_and_CGR_imp_CGR:
[| PR(a, b); CGR(a, c) |] ==> CGR(b, c)
theorem PR_and_notCGR_imp_notCGR:
[| PR(a, b); ¬ CGR(b, c) |] ==> ¬ CGR(a, c)
theorem Sp_sum:
OR(w, a) <-> (∃b. SpR(b) ∧ PR(b, a) ∧ OR(w, b))
theorem Sp_imp_CNGSpR:
SpR(a) ==> CNGSpR(a, a)
theorem CNGSpR_imp_SSR:
CNGSpR(a, b) ==> SSR(a, b)
theorem Sp_and_SSR_imp_CNGSpR:
[| SpR(a); SpR(b); SSR(a, b) |] ==> CNGSpR(a, b)
theorem Sp_imp_SSR_iff_CONSpR:
[| SpR(a); SpR(b) |] ==> SSR(a, b) <-> CNGSpR(a, b)
theorem CNGSpR_imp_Sp_and_Sp:
CNGSpR(a, b) ==> SpR(a) ∧ SpR(b)
theorem CNGSpR_sym:
CNGSpR(a, b) ==> CNGSpR(b, a)
theorem CNGSpR_trans:
[| CNGSpR(a, b); CNGSpR(b, c) |] ==> CNGSpR(a, c)
theorem ECR_sym:
ECR(a, b) ==> ECR(b, a)
theorem ECR_irrefl:
¬ ECR(a, a)
theorem DCR_sym:
DCR(a, b) ==> DCR(b, a)
theorem DCR_irrefl:
¬ DCR(a, a)