Theory RBG

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