Theory QDiaSizeR

Up to index of Isabelle/FOL/BFO

theory QDiaSizeR
imports RBG
begin

theory QDiaSizeR 

imports RBG

begin

(* same bounding-diameter size *)
(* crisp relations *)

consts

SSRdia :: "Rg => Rg => o"
LERdia :: "Rg => Rg => o"
MinBSpR :: "Rg => Rg => o"

BR :: "Rg => Rg => Rg => o"

defs

MinBSpR_def: "MinBSpR(a,b) == SpR(a) & PR(b,a) & (ALL c. (SpR(c) & PR(b,c) --> LER(a,c)))" 
SSRdia_def: "SSRdia(a,b) == (EX ca cb. (MinBSpR(ca,a) & MinBSpR(cb,b) & SSR(ca,cb)))"
LERdia_def: "LERdia(a,b) == (EX ca cb. (MinBSpR(ca,a) & MinBSpR(cb,b) & LER(ca,cb)))"

BR_def: "BR(a,b,c) == SpR(a) & SpR(b) & SpR(c) & (EX sab sbc sac bab bbc bac. (Sum(a,b,sab) & Sum(b,c,sbc) & Sum(a,c,sac) & MinBSpR(bab,sab) & MinBSpR(bbc,sbc) & MinBSpR(bac,sac) & PR(bab,bac) & PR(bbc,bac)))"

axioms

MinBSpR_exists: "(EX b. MinBSpR(b,a))"
PR_and_MinBSpR_and_MinBSpR_imp_PR: "[|PR(a,b);MinBSpR(aa,a);MinBSpR(bb,b)|] ==> PR(aa,bb)"
(*MinBSpR_between: "[|MinBSpR(aa,a);PR(a,b);PR(b,aa)|] ==> MinBSpR(aa,b)"*)

BR_trans: "[|BR(a,b,w);BR(b,c,w)|] ==> BR(a,b,c)"
BR_connect: "[|BR(a,b,w);BR(a,c,w)|] ==> (BR(a,b,c) | BR(a,c,b))"


(* theorems for MonBSpR *)

theorem MinBSpR_imp_PR: "MinBSpR(a,b) ==> PR(b,a)"
apply(unfold MinBSpR_def)
apply(auto)
done


theorem MinBSpR_and_MinBSpR_imp_SSR: "[|MinBSpR(a,c);MinBSpR(b,c)|] ==> SSR(a,b)"
apply(unfold MinBSpR_def)
apply(rule_tac a="a" and b="b" in LER_and_LER_imp_SSR)
apply(auto)
done


theorem MinBSpR_unique: "[|MinBSpR(a,c);MinBSpR(b,c)|] ==> a=b"
apply(rule PR_and_SSR_imp_Id)
apply(rule PR_and_MinBSpR_and_MinBSpR_imp_PR [of c c])
apply(rule PR_refl_rule)
apply(assumption)+
apply(rule  MinBSpR_and_MinBSpR_imp_SSR)
apply(auto)
done

theorem SpR_iff_MinBSpR: "SpR(a) <-> MinBSpR(a,a)"
apply(rule iffI)
apply(unfold MinBSpR_def)
apply(safe)
apply(rule PR_refl_rule [of a])
apply(drule_tac a="a" and b="c" in PR_imp_LER)
apply(assumption)
done

theorem EX_SpR_CGR_and_CGR: "(EX c. (SpR(c) & CGR(c,a) & CGR(c,b)))"
apply(insert PR_sum)
apply(erule_tac x="a" in allE)
apply(erule_tac x="b" in allE)
apply(clarify)
apply(insert MinBSpR_exists)
apply(drule allI)
apply(erule_tac x="c" in allE)
apply(clarify)
apply(rule_tac x="ba" in exI)
apply(safe)
apply(unfold MinBSpR_def)
apply(clarify)
apply(fold MinBSpR_def)
apply(drule_tac a="a" and b="b" and c="c" in Sum_imp_PR_and_PR)
apply(clarify)
apply(drule_tac a="ba" and b="c" in MinBSpR_imp_PR)
apply(drule_tac a="a" and b="c" and c="ba" in PR_trans_rule)
apply(assumption)
apply(drule_tac a="a" and b="ba" in PR_imp_CGR)
apply(rule CGR_sym)
apply(clarify)
apply(drule_tac a="a" and b="b" and c="c" in Sum_imp_PR_and_PR)
apply(clarify)
apply(drule_tac a="ba" and b="c" in MinBSpR_imp_PR)
apply(drule_tac a="b" and b="c" and c="ba" in PR_trans_rule)
apply(assumption)
apply(drule_tac a="b" and b="ba" in PR_imp_CGR)
apply(rule CGR_sym)
apply(clarify)
done

(* theorems for between *)

theorem BR_imp_PR: "BR(a,b,a) ==> PR(b,a)"
apply(unfold BR_def)
apply(clarify)
apply(frule_tac a="a" and b="sac" in Sum_imp_id)
apply(clarify)
apply(frule_tac a="a" and b="b" in Sum_sym)
apply(frule_tac a="b" and b="a" and c="sbc" and d="sab" in Sum_unique)
apply(clarify)
apply(frule_tac a="bab" and c="sab" and b="bbc" in MinBSpR_unique)
apply(clarify)
apply(frule_tac a="b" and b="a" and c="sab" in Sum_imp_PR_and_PR)
apply(clarify)
apply(frule_tac a="bbc" and b="sab" in MinBSpR_imp_PR)
apply(frule_tac a="b" and b="sab" and c="bbc" in PR_trans_rule)
apply(assumption)
apply(frule_tac a="b" and b="bbc" and c="bac" in PR_trans_rule)
apply(clarify)
apply(simp add: SpR_iff_MinBSpR)
apply(frule_tac a="a" and b="bac" and c="a" in MinBSpR_unique)
apply(safe)
done

theorem BR_refl: "[|SpR(a);SpR(b)|] ==> BR(a,a,b)"
apply(unfold BR_def)
apply(safe)
apply(rule_tac x="a" in exI)
apply(insert Sum_refl [of a])
apply(insert PR_sum)
apply(erule_tac x="a" in allE)
apply(erule_tac x="b" in allE)
apply(clarify)
apply(rule_tac x="c" in exI)
apply(rule_tac x="c" in exI)
apply(insert MinBSpR_exists [of a])
apply(insert MinBSpR_exists)
apply(drule allI)
apply(erule_tac x="c" in allE)
apply(clarify)
apply(rule_tac x="ba" in exI)
apply(rule_tac x="baa" in exI)
apply(rule_tac x="baa" in exI)
apply(safe)
apply(drule_tac a="a" and b="b" and c="c" in Sum_imp_PR_and_PR)
apply(clarify)
apply(drule_tac a="a" and b="c" and aa="ba" and bb="baa" in PR_and_MinBSpR_and_MinBSpR_imp_PR) 
apply(safe)
apply(insert PR_refl)
apply(auto)
done

theorem BR_sym: "BR(a,b,c) ==> BR(c,b,a)"
apply(unfold BR_def)
apply(clarify)
apply(rule_tac x="sbc" in exI)
apply(rule_tac x="sab" in exI)
apply(rule_tac x="sac" in exI)
apply(rule_tac x="bbc" in exI)
apply(rule_tac x="bab" in exI)
apply(rule_tac x="bac" in exI)
apply(safe)
apply(insert Sum_sym)
apply(auto)
done



(* theorems for SSRdia and LERdia *)


theorem SSRdia_refl: "SSRdia(a,a)"
apply(rule ccontr)
apply(unfold SSRdia_def)
apply(auto)
apply(insert MinBSpR_exists [of a])
apply(clarify)
apply(erule_tac x="b" in allE)
apply(clarify)
apply(erule_tac x="b" in allE)
apply(safe)
apply(insert SSR_refl)
apply(erule_tac x="b" in allE)
apply(auto)
done


theorem SSRdia_sym: "SSRdia(a,b) ==> SSRdia(b,a)"
apply(unfold SSRdia_def)
apply(clarify)
apply(rule_tac x="cb" in exI)
apply(rule_tac x="ca" in exI)
apply(safe)
apply(rule_tac a="ca" and b="cb" in SSR_sym)
apply(assumption)
done

theorem SSRdia_trans: "[|SSRdia(a,b);SSRdia(b,c)|] ==> SSRdia(a,c)"
apply(unfold SSRdia_def)
apply(clarify)
apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) 
apply(assumption)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cba" in exI)
apply(safe)
apply(drule_tac a="ca" and b="cb" and c="cba" in SSR_trans)
apply(auto)
done

theorem LERdia_refl: "LERdia(a,a)"
apply(rule ccontr)
apply(unfold LERdia_def)
apply(auto)
apply(insert MinBSpR_exists [of a])
apply(clarify)
apply(erule_tac x="b" in allE)
apply(clarify)
apply(erule_tac x="b" in allE)
apply(safe)
apply(insert LER_refl)
apply(drule allI)
apply(erule_tac x="b" in allE)
apply(auto)
done

theorem LERdia_trans: "[|LERdia(a,b);LERdia(b,c)|] ==> LERdia(a,c)"
apply(unfold LERdia_def)
apply(clarify)
apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique) 
apply(assumption)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cba" in exI)
apply(safe)
apply(drule_tac a="ca" and b="cb" and c="cba" in LER_trans)
apply(auto)
done

theorem LERdia_and_LERdia_imp_SSRdia: "[|LERdia(a,b);LERdia(b,a)|] ==> SSRdia(a,b)"
apply(unfold LERdia_def,unfold SSRdia_def)
apply(clarify)
apply(drule_tac a="ca" and b="cba" and c="a" in MinBSpR_unique) 
apply(assumption)
apply(drule_tac a="cb" and b="caa" and c="b" in MinBSpR_unique) 
apply(assumption)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cb" in exI)
apply(safe)
apply(drule_tac a="cba" and b="caa" in LER_and_LER_imp_SSR)
apply(auto)
done

theorem SSRdia_imp_LERdia_and_LERdia: "SSRdia(a,b) ==> (LERdia(a,b) & LERdia(b,a))"
apply(unfold SSRdia_def,unfold LERdia_def)
apply(safe)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cb" in exI)
apply(drule_tac a="ca" and b="cb" in SSR_imp_LER)
apply(safe)
apply(rule_tac x="cb" in exI)
apply(rule_tac x="ca" in exI)
apply(drule_tac a="ca" and b="cb" in SSR_sym)
apply(drule_tac a="cb" and b="ca" in SSR_imp_LER)
apply(safe)
done

theorem SSRdia_iff_LERdia_and_LERdia: "SSRdia(a,b) <-> (LERdia(a,b) & LERdia(b,a))"
apply(rule iffI)
apply(drule SSRdia_imp_LERdia_and_LERdia)
apply(auto)
apply(rule LERdia_and_LERdia_imp_SSRdia)
apply(auto)
done

theorem LERdia_or_LERdia: "(LERdia(a,b) | LERdia(b,a))"
apply(insert LER_total)
apply(insert MinBSpR_exists [of a])
apply(insert MinBSpR_exists [of b])
apply(clarify)
apply(erule_tac x="ba" in allE)
apply(erule_tac x="baa" in allE)
apply(safe)
apply(unfold LERdia_def)
apply(auto)
done

theorem Id_imp_SSRdia: "a=b ==> SSRdia(a,b)"
apply(insert SSRdia_refl [of a])
apply(simp)
done

theorem PR_and_PR_imp_SSRdia: "[|PR(a,b);PR(b,a)|] ==> SSRdia(a,b)"
apply(rule Id_imp_SSRdia [of a b])
apply(rule PR_antisym_rule [of a b])
apply(safe)
done

theorem PR_imp_LERdia: "PR(a,b) ==> LERdia(a,b)"
apply(unfold LERdia_def)
apply(insert MinBSpR_exists [of a])
apply(insert MinBSpR_exists [of b])
apply(clarify)
apply(rule_tac x="ba" in exI)
apply(rule_tac x="baa" in exI)
apply(safe)
apply(drule_tac a="a" and b="b" and aa="ba" and bb="baa" in PR_and_MinBSpR_and_MinBSpR_imp_PR)
apply(safe)
apply(drule_tac a="ba" and b="baa" in PR_imp_LER)
apply(assumption)
done

theorem LERdia_and_SSRdia_imp_LERdia: "[|LERdia(a,b);SSRdia(b,c)|] ==> LERdia(a,c)"
apply(unfold LERdia_def,unfold SSRdia_def)
apply(clarify)
apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique)
apply(safe)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cba" in exI)
apply(safe)
apply(drule_tac a="ca" and b="cb" and c="cba" in LER_and_SSR_imp_LER)
apply(safe)
done

theorem SSRdia_and_LERdia_imp_LERdia: "[|SSRdia(a,b);LERdia(b,c)|] ==> LERdia(a,c)"
apply(unfold LERdia_def,unfold SSRdia_def)
apply(clarify)
apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique)
apply(safe)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cba" in exI)
apply(safe)
apply(drule_tac c="ca" and a="cb" and b="cba" in SSR_and_LER_imp_LER)
apply(safe)
done

theorem SpR_and_SpR_and_SSR_imp_SSRdia: "[|SpR(a);SpR(b);SSR(a,b)|] ==> SSRdia(a,b)"
apply(unfold SSRdia_def)
apply(rule_tac x="a" in exI)
apply(rule_tac x="b" in exI)
apply(safe)
apply(simp add:  SpR_iff_MinBSpR)
apply(simp add:  SpR_iff_MinBSpR)
done

theorem SpR_and_SpR_and_SSRdia_imp_SSR: "[|SpR(a);SpR(b);SSRdia(a,b)|] ==> SSR(a,b)"
apply(unfold SSRdia_def)
apply(clarify)
apply(simp add:  SpR_iff_MinBSpR)
apply(drule_tac a="a" and b="ca" and c="a" in  MinBSpR_unique)
apply(assumption)
apply(drule_tac a="b" and b="cb" and c="b" in  MinBSpR_unique)
apply(assumption)
apply(simp)
done

theorem SpR_and_SpR_imp_SSR_iff_SSRdia: "[|SpR(a);SpR(b)|] ==> (SSR(a,b) <-> SSRdia(a,b))"
apply(safe)
apply(rule  SpR_and_SpR_and_SSR_imp_SSRdia)
apply(auto)
apply(rule SpR_and_SpR_and_SSRdia_imp_SSR)
apply(auto)
done

theorem SSRdia_imp_LERdia: "SSRdia(a,b) ==> LERdia(a,b)"
apply(unfold LERdia_def)
apply(unfold SSRdia_def)
apply(clarify)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cb" in exI)
apply(safe)
apply(drule SSR_imp_LER)
apply(auto)
done


(* same bounding-diameter size *)
(* vague relations *)

consts

RSSRdia :: "Rg => Rg => o"
NEGRdia :: "Rg => Rg => o"

defs

RSSRdia_def: "RSSRdia(a,b) == (EX ca cb. (MinBSpR(ca,a) & MinBSpR(cb,b) & RSSR(ca,cb)))"
NEGRdia_def: "NEGRdia(a,b) == (EX ca cb. (MinBSpR(ca,a) & MinBSpR(cb,b) & NEGR(ca,cb)))"


(* theorems for RSSRdia and NEGdia *)

theorem RSSRdia_refl: "RSSRdia(a,a)"
apply(unfold RSSRdia_def)
apply(insert MinBSpR_exists [of a])
apply(insert MinBSpR_exists [of a])
apply(clarify)
apply(rule_tac x="b" in exI)
apply(rule_tac x="ba" in exI)
apply(safe)
apply(drule_tac a="b" and b="ba" and c="a" in  MinBSpR_unique)
apply(insert RSSR_refl)
apply(auto)
done

theorem RSSRdia_sym: "RSSRdia(a,b) ==> RSSRdia(b,a)"
apply(unfold RSSRdia_def)
apply(clarify)
apply(rule_tac x="cb" in exI)
apply(rule_tac x="ca" in exI)
apply(safe)
apply(rule_tac b="cb" and a="ca" in RSSR_sym) 
apply(assumption)
done

(*
this cannot be a theorem for the same reason why RSSR_plus is not a theorem for RSSR  
theorem RSSRdia_plus: "[|Plus(a,c,d1);Plus(b,c,d2);Sym(c,a,b);RSSRdia(a,b)|] ==> RSSRdia(d1,d2)"
*)

theorem RSSRdia_between: "[|RSSRdia(a,b);LERdia(a,c);LERdia(c,b)|] ==> (RSSRdia(c,a) & RSSRdia(c,b))"
apply(unfold RSSRdia_def,unfold LERdia_def)
apply(clarify)
apply(drule_tac a="ca" and b="caa" and c="a" in MinBSpR_unique)
apply(assumption)
apply(drule_tac a="cb" and b="cbb" and c="b" in MinBSpR_unique)
apply(assumption)
apply(drule_tac a="cab" and b="cba" and c="c" in MinBSpR_unique)
apply(assumption)
apply(safe)
apply(rule_tac x="cba" in exI)
apply(rule_tac x="caa" in exI)
apply(safe)
apply(drule_tac a="caa" and b="cbb" and c="cba" in RSSR_between)
apply(safe)
apply(rule_tac x="cba" in exI)
apply(rule_tac x="cbb" in exI)
apply(safe)
apply(drule_tac a="caa" and b="cbb" and c="cba" in RSSR_between)
apply(safe)
done


theorem SSRdia_and_RSSRdia_imp_RSSRdia: "[|SSRdia(a,b);RSSRdia(b,c)|] ==> RSSRdia(a,c)"
apply(unfold SSRdia_def,unfold RSSRdia_def)
apply(clarify)
apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique)
apply(assumption)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cba" in exI)
apply(simp)
apply(rule_tac a="ca" and b="cb" and c="cba" in  SSR_and_RSSR_imp_RSSR)
apply(auto)
done

theorem RSSRdia_and_SSRdia_imp_RSSRdia: "[|RSSRdia(a,b);SSRdia(b,c)|] ==> RSSRdia(a,c)"
apply(unfold SSRdia_def,unfold RSSRdia_def)
apply(clarify)
apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique)
apply(assumption)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cba" in exI)
apply(simp)
apply(rule_tac a="ca" and b="cb" and c="cba" in   RSSR_and_SSR_imp_RSSR)
apply(auto)
done

theorem SSRdia_imp_RSSRdia: "SSRdia(a,b) ==> RSSRdia(a,b)"
apply(insert RSSRdia_refl)
apply(insert RSSRdia_and_SSRdia_imp_RSSRdia)
apply(auto)
done

theorem NEGRdia_imp_LERdia: "NEGRdia(a,b) ==> LERdia(a,b)"
apply(unfold NEGRdia_def)
apply(unfold LERdia_def)
apply(clarify)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cb" in exI)
apply(safe)
apply(drule_tac a="ca" and b="cb" in NEGR_imp_LER)
apply(safe)
done

theorem NEGRdia_imp_LERdia_and_notSSRdia: "NEGRdia(a,b) ==> (LERdia(a,b) & ~SSRdia(a,b))"
apply(unfold NEGRdia_def)
apply(unfold LERdia_def)
apply(unfold SSRdia_def)
apply(safe)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cb" in exI)
apply(safe)
apply(drule_tac a="ca" and b="cb" in NEGR_imp_LER_and_notSSR)
apply(safe)
apply(drule_tac a="ca" and b="caa" and c="a" in MinBSpR_unique)
apply(assumption)
apply(drule_tac a="cb" and b="cba" and c="b" in MinBSpR_unique)
apply(assumption)
apply(drule_tac a="ca" and b="cb" in NEGR_imp_LER_and_notSSR)
apply(safe)
done

theorem NEGRdia_irrefl: "~NEGRdia(a,a)"
apply(unfold NEGRdia_def)
apply(safe)
apply(drule_tac a="ca" and b="cb" and c="a" in MinBSpR_unique)
apply(safe)
apply(insert NEGR_irrefl)
apply(erule_tac x="cb" in allE)
apply(safe)
done

theorem NEGRdia_assym: "NEGRdia(a,b) ==> ~NEGRdia(b,a)"
apply(unfold NEGRdia_def)
apply(safe)
apply(drule_tac a="ca" and b="cba" and c="a" in MinBSpR_unique)
apply(assumption)
apply(drule_tac a="cb" and b="caa" and c="b" in MinBSpR_unique)
apply(safe)
apply(drule_tac a="cba" and b="caa" in NEGR_assym)
apply(safe)
done

theorem LERdia_and_NEGRdia_imp_NEGRdia: "[|LERdia(a,b);NEGRdia(b,c)|] ==> NEGRdia(a,c)"
apply(unfold NEGRdia_def)
apply(unfold LERdia_def)
apply(clarify)
apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique)
apply(safe)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cba" in exI)
apply(safe)
apply(drule_tac a="ca" and b="cb" and c="cba" in LER_and_NEGR_imp_NEGR)
apply(safe)
done

theorem NEGRdia_and_LERdia_imp_NEGRdia: "[|NEGRdia(a,b);LERdia(b,c)|] ==> NEGRdia(a,c)"
apply(unfold NEGRdia_def)
apply(unfold LERdia_def)
apply(clarify)
apply(drule_tac a="caa" and b="cb" and c="b" in MinBSpR_unique)
apply(safe)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="cba" in exI)
apply(safe)
apply(drule_tac a="ca" and b="cb" and c="cba" in NEGR_and_LER_imp_NEGR)
apply(safe)
done

theorem SSRdia_and_NEGRdia_imp_NEGRdia: "[|SSRdia(a,b);NEGRdia(b,c)|] ==> NEGRdia(a,c)"
apply(drule SSRdia_imp_LERdia)
apply(drule LERdia_and_NEGRdia_imp_NEGRdia)
apply(auto)
done 

theorem NEGRdia_SSRdia_imp_NEGRdia: "[|NEGRdia(a,b);SSRdia(b,c)|] ==> NEGRdia(a,c)"
apply(drule SSRdia_imp_LERdia [of b c])
apply(drule NEGRdia_and_LERdia_imp_NEGRdia)
apply(auto)
done 

theorem NEGRdia_trans: "[|NEGRdia(a,b);NEGRdia(b,c)|] ==> NEGRdia(a,c)"
apply(drule NEGRdia_imp_LERdia)
apply(drule LERdia_and_NEGRdia_imp_NEGRdia)
apply(auto)
done 

theorem PR_and_NEGRdia_imp_NEGRdia: "[|PR(a,b);NEGRdia(b,c)|] ==> NEGRdia(a,c)"
apply(drule PR_imp_LERdia)
apply(drule LERdia_and_NEGRdia_imp_NEGRdia)
apply(auto)
done 

theorem NEGRdia_PR_imp_NEGRdia: "[|NEGRdia(a,b);PR(b,c)|] ==> NEGRdia(a,c)"
apply(drule PR_imp_LERdia [of b c])
apply(drule NEGRdia_and_LERdia_imp_NEGRdia)
apply(auto)
done 


theorem SpR_and_SpR_and_RSSR_imp_RSSRdia: "[|SpR(a);SpR(b);RSSR(a,b)|] ==> RSSRdia(a,b)"
apply(unfold RSSRdia_def)
apply(rule_tac x="a" in exI)
apply(rule_tac x="b" in exI)
apply(safe)
apply(simp add:  SpR_iff_MinBSpR)
apply(simp add:  SpR_iff_MinBSpR)
done

theorem SpR_and_SpR_and_RSSRdia_imp_RSSR: "[|SpR(a);SpR(b);RSSRdia(a,b)|] ==> RSSR(a,b)"
apply(unfold RSSRdia_def)
apply(clarify)
apply(simp add:  SpR_iff_MinBSpR)
apply(drule_tac a="a" and b="ca" and c="a" in  MinBSpR_unique)
apply(assumption)
apply(drule_tac a="b" and b="cb" and c="b" in  MinBSpR_unique)
apply(assumption)
apply(simp)
done

theorem SpR_and_SpR_imp_RSSR_iff_RSSRdia: "[|SpR(a);SpR(b)|] ==> (RSSR(a,b) <-> RSSRdia(a,b))"
apply(safe)
apply(rule  SpR_and_SpR_and_RSSR_imp_RSSRdia)
apply(auto)
apply(rule SpR_and_SpR_and_RSSRdia_imp_RSSR)
apply(auto)
done




end

theorem MinBSpR_imp_PR:

  MinBSpR(a, b) ==> PR(b, a)

theorem MinBSpR_and_MinBSpR_imp_SSR:

  [| MinBSpR(a, c); MinBSpR(b, c) |] ==> SSR(a, b)

theorem MinBSpR_unique:

  [| MinBSpR(a, c); MinBSpR(b, c) |] ==> a = b

theorem SpR_iff_MinBSpR:

  SpR(a) <-> MinBSpR(a, a)

theorem EX_SpR_CGR_and_CGR:

  c. SpR(c) ∧ CGR(c, a) ∧ CGR(c, b)

theorem BR_imp_PR:

  BR(a, b, a) ==> PR(b, a)

theorem BR_refl:

  [| SpR(a); SpR(b) |] ==> BR(a, a, b)

theorem BR_sym:

  BR(a, b, c) ==> BR(c, b, a)

theorem SSRdia_refl:

  SSRdia(a, a)

theorem SSRdia_sym:

  SSRdia(a, b) ==> SSRdia(b, a)

theorem SSRdia_trans:

  [| SSRdia(a, b); SSRdia(b, c) |] ==> SSRdia(a, c)

theorem LERdia_refl:

  LERdia(a, a)

theorem LERdia_trans:

  [| LERdia(a, b); LERdia(b, c) |] ==> LERdia(a, c)

theorem LERdia_and_LERdia_imp_SSRdia:

  [| LERdia(a, b); LERdia(b, a) |] ==> SSRdia(a, b)

theorem SSRdia_imp_LERdia_and_LERdia:

  SSRdia(a, b) ==> LERdia(a, b) ∧ LERdia(b, a)

theorem SSRdia_iff_LERdia_and_LERdia:

  SSRdia(a, b) <-> LERdia(a, b) ∧ LERdia(b, a)

theorem LERdia_or_LERdia:

  LERdia(a, b) ∨ LERdia(b, a)

theorem Id_imp_SSRdia:

  a = b ==> SSRdia(a, b)

theorem PR_and_PR_imp_SSRdia:

  [| PR(a, b); PR(b, a) |] ==> SSRdia(a, b)

theorem PR_imp_LERdia:

  PR(a, b) ==> LERdia(a, b)

theorem LERdia_and_SSRdia_imp_LERdia:

  [| LERdia(a, b); SSRdia(b, c) |] ==> LERdia(a, c)

theorem SSRdia_and_LERdia_imp_LERdia:

  [| SSRdia(a, b); LERdia(b, c) |] ==> LERdia(a, c)

theorem SpR_and_SpR_and_SSR_imp_SSRdia:

  [| SpR(a); SpR(b); SSR(a, b) |] ==> SSRdia(a, b)

theorem SpR_and_SpR_and_SSRdia_imp_SSR:

  [| SpR(a); SpR(b); SSRdia(a, b) |] ==> SSR(a, b)

theorem SpR_and_SpR_imp_SSR_iff_SSRdia:

  [| SpR(a); SpR(b) |] ==> SSR(a, b) <-> SSRdia(a, b)

theorem SSRdia_imp_LERdia:

  SSRdia(a, b) ==> LERdia(a, b)

theorem RSSRdia_refl:

  RSSRdia(a, a)

theorem RSSRdia_sym:

  RSSRdia(a, b) ==> RSSRdia(b, a)

theorem RSSRdia_between:

  [| RSSRdia(a, b); LERdia(a, c); LERdia(c, b) |]
  ==> RSSRdia(c, a) ∧ RSSRdia(c, b)

theorem SSRdia_and_RSSRdia_imp_RSSRdia:

  [| SSRdia(a, b); RSSRdia(b, c) |] ==> RSSRdia(a, c)

theorem RSSRdia_and_SSRdia_imp_RSSRdia:

  [| RSSRdia(a, b); SSRdia(b, c) |] ==> RSSRdia(a, c)

theorem SSRdia_imp_RSSRdia:

  SSRdia(a, b) ==> RSSRdia(a, b)

theorem NEGRdia_imp_LERdia:

  NEGRdia(a, b) ==> LERdia(a, b)

theorem NEGRdia_imp_LERdia_and_notSSRdia:

  NEGRdia(a, b) ==> LERdia(a, b) ∧ ¬ SSRdia(a, b)

theorem NEGRdia_irrefl:

  ¬ NEGRdia(a, a)

theorem NEGRdia_assym:

  NEGRdia(a, b) ==> ¬ NEGRdia(b, a)

theorem LERdia_and_NEGRdia_imp_NEGRdia:

  [| LERdia(a, b); NEGRdia(b, c) |] ==> NEGRdia(a, c)

theorem NEGRdia_and_LERdia_imp_NEGRdia:

  [| NEGRdia(a, b); LERdia(b, c) |] ==> NEGRdia(a, c)

theorem SSRdia_and_NEGRdia_imp_NEGRdia:

  [| SSRdia(a, b); NEGRdia(b, c) |] ==> NEGRdia(a, c)

theorem NEGRdia_SSRdia_imp_NEGRdia:

  [| NEGRdia(a, b); SSRdia(b, c) |] ==> NEGRdia(a, c)

theorem NEGRdia_trans:

  [| NEGRdia(a, b); NEGRdia(b, c) |] ==> NEGRdia(a, c)

theorem PR_and_NEGRdia_imp_NEGRdia:

  [| PR(a, b); NEGRdia(b, c) |] ==> NEGRdia(a, c)

theorem NEGRdia_PR_imp_NEGRdia:

  [| NEGRdia(a, b); PR(b, c) |] ==> NEGRdia(a, c)

theorem SpR_and_SpR_and_RSSR_imp_RSSRdia:

  [| SpR(a); SpR(b); RSSR(a, b) |] ==> RSSRdia(a, b)

theorem SpR_and_SpR_and_RSSRdia_imp_RSSR:

  [| SpR(a); SpR(b); RSSRdia(a, b) |] ==> RSSR(a, b)

theorem SpR_and_SpR_imp_RSSR_iff_RSSRdia:

  [| SpR(a); SpR(b) |] ==> RSSR(a, b) <-> RSSRdia(a, b)