Theory QSizeR

theory QSizeR 

imports EMR

begin

(* same size *)

consts

SSR :: "Rg => Rg => o"
Sym :: "Rg => Rg => Rg => o"
LER :: "Rg => Rg => o"

axioms

SSR_refl: "ALL a. SSR(a,a)"
SSR_sym: "SSR(a,b) ==> SSR(b,a)"
SSR_trans: "[|SSR(a,b);SSR(b,c)|] ==> SSR(a,c)"
PR_and_SSR_imp_PR: "[|PR(a,b);SSR(a,b)|] ==> PR(b,a)"
SSR_plus: "[|Plus(a,c,d1);Plus(b,c,d2);Sym(c,a,b)|] ==> (SSR(a,b) <-> SSR(d1,d2))"
LER_total: "ALL a b. (LER(a,b) | LER(b,a))"
LER_and_LER_imp_SSR: "[|LER(a,b);LER(b,a)|] ==> SSR(a,b)"

lemma SSR_refl_rule: "SSR(a,a)"
apply(insert SSR_refl)
apply(auto)
done

defs

Sym_def: "Sym(c,a,b) == (ALL d. (PR(d,c) --> (PR(d,a) <-> PR(d,b))))"
LER_def: "LER(a,b) == (EX c. (SSR(c,a) & PR(c,b)))"


(* roughly the same size *)

consts

RSSR :: "Rg => Rg => o"
NEGR :: "Rg => Rg => o"
SSCR :: "Rg => Rg => o"
LRSSR ::  "Rg => Rg => o"
LNRSSR :: "Rg => Rg => o"

defs

NEGR_def: "NEGR(a,b) == (EX c1 c2. (SSR(c1,a) & PR(c1,b) & Diff(b,c1,c2) & RSSR(b,c2)))"
SSCR_def: "SSCR(a,b) == (~NEGR(a,b) & ~NEGR(b,a))"
LRSSR_def: "LRSSR(a,b) == (LER(a,b) | RSSR(a,b))"
LNRSSR_def: "LNRSSR(a,b) == (LRSSR(a,b) & ~RSSR(a,b))"

axioms

RSSR_refl: "ALL a. RSSR(a,a)"
RSSR_sym: "RSSR(a,b) ==> RSSR(b,a)"
RSSR_between: "[|RSSR(a,b);LER(a,c);LER(c,b)|] ==> (RSSR(c,a) & RSSR(c,b))"
(* RSSR_exists: "(ALL a. (EX b. (PPR(b,a) & RSSR(b,a))))"  why this axiom?? *)

RSSR_and_NEGR_imp_NEGR: "[|RSSR(a,b);NEGR(b,c)|] ==> NEGR(a,c)"
NEGR_and_RSSR_imp_NEGR: "[|NEGR(a,b);RSSR(b,c)|] ==> NEGR(a,c)"

NEGR_and_LER_imp_NEGR: "[|NEGR(a,b);LER(b,c)|] ==> NEGR(a,c)"

RSSR_sum: "[|Sum(a,c,d1);Sum(b,c,d2);Sym(c,a,b);RSSR(a,b)|] ==> RSSR(d1,d2)"
RSSR_sum2: "[|Sum(a,b,c);NEGR(a,c)|] ==> ~LRSSR(b,a)"


(* theorems for SSR and LER -- same-size and less-or-equal-in-size*)

theorem Id_imp_SSR: "a=b ==> SSR(a,b)"
apply(insert SSR_refl)
apply(auto)
done

theorem PR_and_PR_imp_SSR: "[|PR(a,b);PR(b,a)|] ==> SSR(a,b)"
apply(insert PR_antisym,insert Id_imp_SSR)
apply(auto)
done

theorem PR_and_SSR_imp_Id: "[|PR(a,b);SSR(a,b)|] ==> a = b"
apply(frule_tac a="a" and b="b" in PR_and_SSR_imp_PR)
apply(assumption)
apply(rule PR_antisym_rule)
apply(safe)
done

theorem PR_imp_LER: "PR(a,b) ==> LER(a,b)"
apply(unfold LER_def)
apply(rule_tac x="a" in exI)
apply(insert SSR_refl)
apply(auto)
done

theorem PPR_imp_notSSR: "PPR(a,b) ==> ~SSR(a,b)"
apply(rule ccontr)
apply(auto)
apply(frule_tac a="a" and b="b" in PPR_imp_PR)
apply(drule_tac a="a" and b="b" in PR_and_SSR_imp_PR)
apply(assumption)
apply(unfold PPR_def)
apply(auto)
done


theorem LER_refl: "LER(a,a)"
apply(unfold LER_def)
apply(insert SSR_refl,insert PR_refl)
apply(auto)
done


theorem LER_and_SSR_imp_LER: "[|LER(a,b);SSR(b,c)|] ==> LER(a,c)"
apply(insert LER_total) 
apply(erule_tac x="a" in allE)
apply(erule_tac x="c" in allE)
apply(clarify)
apply(unfold LER_def)
apply(frule_tac exE)
apply(assumption)
apply(erule exE)
apply(erule exE)
apply(fold LER_def)
apply(clarify)
apply(drule_tac a="b" and b="c" in SSR_sym)
apply(frule_tac a="caa" and b="c" and c="b" in SSR_trans)
apply(assumption)
apply(frule_tac P="SSR(caa,b)" and Q="PR(caa,a)" in conjI)
apply(assumption)
apply(drule_tac P="% caa. (SSR(caa, b) & PR(caa, a))" in exI)
apply(fold LER_def)
apply(drule_tac a="a" and b="b" in LER_and_LER_imp_SSR)
apply(assumption)
apply(drule_tac a="c" and b="b" in SSR_sym) 
apply(drule_tac a="a" and b="b" and c="c" in SSR_trans)
apply(assumption)
apply(unfold LER_def)
apply(rule_tac x="c" in exI)
apply(drule_tac a="a" and b="c" in SSR_sym)
apply(insert PR_refl)
apply(auto)
done


theorem SSR_and_LER_imp_LER: "[|SSR(c,a);LER(a,b)|] ==> LER(c,b)"
apply(unfold LER_def)
apply(clarify)
apply(drule_tac a="ca" and b="a" in SSR_sym)
apply(drule_tac a="c" and b="a" and c="ca" in SSR_trans)
apply(assumption)
apply(drule_tac a="c" and b="ca" in SSR_sym)
apply(rule_tac x="ca" in exI)
apply(auto)
done


theorem SSR_imp_LER: "SSR(a,b) ==> LER(a,b)"
apply(unfold LER_def)
apply(rule_tac x="b" in exI)
apply(drule SSR_sym)
apply(insert PR_refl)
apply(auto)
done

theorem SSR_imp_LER_and_LER: "SSR(a,b) ==> (LER(a,b) & LER(b,a))"
apply(frule SSR_imp_LER)
apply(drule SSR_sym)
apply(drule SSR_imp_LER)
apply(auto)
done


theorem LER_trans: "[|LER(a,b);LER(b,c)|] ==> LER(a,c)"
apply(insert LER_total) 
apply(erule_tac x="a" in allE)
apply(erule_tac x="c" in allE)
apply(clarify)
apply(unfold LER_def)
thm exE
apply(frule_tac P="% c. (SSR(c, a) & PR(c, b))" and R="(EX (ca::Rg). (SSR(ca, a) & PR(ca, c)))" in exE)
prefer 2
apply(assumption)
apply(frule_tac P="% ca. (SSR(ca, b) & PR(ca, c))"  and R="(EX (ca::Rg). (SSR(ca, a) & PR(ca, c)))" in exE)
prefer 2
apply(assumption)
apply(frule_tac P="% ca. (SSR(ca, c) & PR(ca, a))"  and R="(EX (ca::Rg). (SSR(ca, a) & PR(ca, c)))" in exE)
prefer 2
apply(assumption)
apply(fold LER_def)
apply(clarify)
apply(insert LER_total) 
apply(erule_tac x="xb" in allE)
apply(erule_tac x="b" in allE)
apply(safe)
apply(unfold LER_def)
apply(erule_tac P="% c. (SSR(c, xb) & PR(c, b))" in exE)
apply(fold LER_def)
apply(clarify)
apply(unfold LER_def)
apply(drule_tac a="xc" and b="xb" and c="c" in SSR_trans)
apply(assumption)
apply(drule_tac P="SSR(xc, c)" and Q="PR(xc, b)" in conjI)
apply(assumption)
thm exI
apply(drule_tac P="% xc. (SSR(xc, c) & PR(xc, b))" in exI) 
apply(fold LER_def)
apply(drule_tac a="b" and b="c" in LER_and_LER_imp_SSR)
apply(assumption)
apply(drule_tac a="b" and b="c" in SSR_sym)
apply(drule_tac a="xb" and b="c" and c="b" in SSR_trans)
apply(assumption)
apply(drule_tac P="SSR(xb, b)" and Q="PR(xb, a)" in conjI)
apply(assumption)
apply(drule_tac P="% xb. (SSR(xb, b) & PR(xb, a))" in exI) 
apply(fold LER_def)
apply(drule_tac a="a" and b="b" in LER_and_LER_imp_SSR)
apply(assumption)
apply(drule_tac a="c" and b="b" in SSR_sym)
apply(drule_tac a="a" and b="b" and c="c" in SSR_trans)
apply(assumption)
apply(unfold LER_def)
apply(rule_tac x="c" in exI)
apply(drule_tac a="a" and b="c" in SSR_sym)
apply(insert PR_refl)
apply(force)

apply(erule_tac P="% c. (SSR(c, b) & PR(c, xb))" in exE)
apply(fold LER_def)
apply(clarify)
apply(drule_tac a="xc" and b="xb" and c="a" in PR_trans_rule)
apply(assumption)
apply(drule_tac P="SSR(xc, b)" and Q="PR(xc, a)" in conjI)
apply(assumption)
apply(drule_tac P="% xc. (SSR(xc, b) & PR(xc, a))" in exI) 
apply(fold LER_def)
apply(drule_tac a="a" and b="b" in LER_and_LER_imp_SSR)
apply(assumption)
apply(drule_tac a="xa" and b="b" in SSR_sym)
apply(drule_tac a="a" and b="b" and c="xa" in SSR_trans)
apply(assumption)
apply(unfold LER_def)
apply(rule_tac x="xa" in exI)
apply(rule conjI)
apply(rule_tac b="xa" and a="a" in SSR_sym)
apply(auto)
done


(* theorems for RSSR *)


theorem SSR_and_RSSR_imp_RSSR: "[|SSR(a,b);RSSR(b,c)|] ==> RSSR(a,c)"
apply(insert LER_total)
apply(erule_tac x="b" in allE)
apply(erule_tac x="c" in allE)
apply(safe)
thm SSR_and_LER_imp_LER
apply(frule_tac c="a" and a="b" and b="c" in SSR_and_LER_imp_LER) 
apply(assumption)
apply(drule_tac a="a" and b="b" in SSR_sym)
apply(drule_tac a="b" and b="a" in SSR_imp_LER)
thm RSSR_between
apply(drule_tac a="b" and b="c" and c="a" in RSSR_between) 
apply(assumption,assumption)
apply(clarify)

apply(frule_tac a="a" and b="b" in SSR_sym)
apply(frule_tac a="c" and b="b" and c="a" in LER_and_SSR_imp_LER) 
apply(assumption)
apply(drule_tac a="b" and b="c" in RSSR_sym)
apply(drule_tac a="a" and b="b" in SSR_imp_LER)
apply(drule_tac a="c" and b="b" and c="a" in RSSR_between) 
apply(assumption,assumption)
apply(clarify)
done


theorem RSSR_and_SSR_imp_RSSR: "[|RSSR(a,b);SSR(b,c)|] ==> RSSR(a,c)"
apply(drule_tac a="a" and b="b" in RSSR_sym)
apply(drule_tac a="b" and b="c" in SSR_sym)
apply(rule_tac a="c" and b="a" in RSSR_sym)
apply(rule_tac a="c" and b="b" and c="a" in SSR_and_RSSR_imp_RSSR)
apply(auto)
done

theorem SSR_imp_RSSR: "SSR(a,b) ==> RSSR(a,b)"
apply(insert RSSR_refl)
apply(insert RSSR_and_SSR_imp_RSSR)
apply(auto)
done


theorem NEGR_imp_LER: "NEGR(a,b) ==> LER(a,b)"
apply(unfold NEGR_def)
apply(erule exE,erule exE)
apply(unfold LER_def)
apply(rule_tac x="c1" in exI)
apply(auto)
done

theorem NEGR_imp_LER_and_notSSR: "NEGR(a,b) ==> (LER(a,b) & ~SSR(a,b))"
apply(unfold NEGR_def)
apply(unfold LER_def)
apply(safe)
apply(rule_tac x="c1" in exI)
apply(safe)
apply(drule_tac a="c1" and b="a" and c="b" in SSR_trans)
apply(assumption)
apply(drule_tac a="b" and b="c1" and c="c2" in Diff_imp_notPR)
apply(drule_tac a="c1" and b="b" in PR_and_SSR_imp_PR)
apply(auto)
done

theorem NEGR_irrefl: "ALL a. (~NEGR(a,a))"
apply(rule allI)
apply(rule notI)
apply(drule NEGR_imp_LER_and_notSSR)
apply(insert SSR_refl)
apply(auto)
done

theorem NEGR_assym: "NEGR(a,b) ==> ~NEGR(b,a)"
apply(drule NEGR_imp_LER_and_notSSR)
apply(safe)
apply(drule_tac a="b" and b="a" in NEGR_imp_LER_and_notSSR)
apply(drule LER_and_LER_imp_SSR)
apply(auto)
done

theorem LER_and_NEGR_imp_NEGR: "[|LER(a,b);NEGR(b,c)|] ==> NEGR(a,c)"
apply(unfold NEGR_def)
apply(clarify)
apply(drule_tac a="c1" and b="b" in SSR_sym)
apply(drule_tac a="a" and b="b" and c="c1" in LER_and_SSR_imp_LER)
apply(assumption)
apply(unfold LER_def)
apply(clarify)
apply(frule_tac a="ca" and b="c1" and c="c" and d="c2" in PR_and_Diff_impl_Diff_PR)
apply(assumption)
apply(clarify)
apply(frule_tac a="c" and b="ca" and c="e" in Diff_imp_PR)
apply(drule_tac a="c" and b="c2" in RSSR_sym)
apply(frule_tac a="c2" and b="e" in PR_imp_LER)
apply(frule_tac a="e" and b="c" in PR_imp_LER)
apply(drule_tac a="c2" and b="c" and c="e" in RSSR_between)
apply(assumption,assumption)
apply(rule_tac x="ca" in exI)
apply(rule_tac x="e" in exI)
apply(safe)
apply(drule_tac a="ca" and b="c1" and c="c" in PR_trans_rule)
apply(safe)
apply(rule RSSR_sym)
apply(assumption)
done


theorem SSR_and_NEGR_imp_NEGR: "[|SSR(a,b);NEGR(b,c)|] ==> NEGR(a,c)"
apply(drule SSR_imp_LER)
apply(drule LER_and_NEGR_imp_NEGR)
apply(auto)
done 

theorem NEGR_and_SSR_imp_NEGR: "[|NEGR(a,b);SSR(b,c)|] ==> NEGR(a,c)"
apply(drule SSR_imp_LER [of b c])
apply(drule NEGR_and_LER_imp_NEGR)
apply(auto)
done 

theorem NEGR_trans: "[|NEGR(a,b);NEGR(b,c)|] ==> NEGR(a,c)"
apply(drule NEGR_imp_LER)
apply(drule LER_and_NEGR_imp_NEGR)
apply(auto)
done 

theorem PR_and_NEGR_imp_NEGR: "[|PR(a,b);NEGR(b,c)|] ==> NEGR(a,c)"
apply(drule PR_imp_LER)
apply(drule LER_and_NEGR_imp_NEGR)
apply(auto)
done 

theorem NEGR_and_PR_imp_NEGR: "[|NEGR(a,b);PR(b,c)|] ==> NEGR(a,c)"
apply(drule PR_imp_LER [of b c])
apply(drule NEGR_and_LER_imp_NEGR)
apply(auto)
done 



theorem RSSR_imp_notNEGR: "RSSR(a,b) ==> ~NEGR(a,b)" 
apply(rule ccontr)
apply(auto)
apply(insert PR_sum)
apply(erule_tac x="a" in allE)
apply(erule_tac x="b" in allE)
apply(clarify)
apply(frule_tac a="a" and b="b" and c="c" in Sum_imp_PR_and_PR)
apply(clarify)
apply(drule_tac a="a" and b="b" and c="c" in  NEGR_and_PR_imp_NEGR)
apply(assumption)
apply(drule_tac a="a" and b="b" and c="c" in RSSR_sum2)
apply(assumption)
apply(unfold LRSSR_def)
apply(drule_tac a="a" and b="b" in RSSR_sym)
apply(clarify)
done


(* theorems for same-scale *)

theorem SSCR_refl: "ALL a. SSCR(a,a)"
apply(unfold SSCR_def)
apply(rule allI)
apply(insert NEGR_irrefl)
apply(auto)
done

theorem SSCR_sym: "SSCR(a,b) ==> SSCR(b,a)"
apply(unfold SSCR_def)
apply(auto)
done

(* theorems for LRSSR *)

theorem LRSSR_refl: "LRSSR(a,a)"
apply(unfold LRSSR_def)
apply(insert LER_refl [of a])
apply(insert RSSR_refl)
apply(auto)
done

theorem LRSSR_and_LRSSR_imp_RSSR: "[|LRSSR(a,b);LRSSR(b,a)|] ==> RSSR(a,b)"
apply(unfold LRSSR_def)
apply(safe)
apply(drule_tac a="a" and b="b" in LER_and_LER_imp_SSR)
apply(assumption)
apply(drule_tac a="a" and b="b" in SSR_imp_RSSR)
apply(safe)
apply(rule RSSR_sym)
apply(assumption)
done

theorem RSSR_imp_LRSSR_and_LRSSR: "RSSR(a,b) ==> (LRSSR(a,b) & LRSSR(b,a))"
apply(safe)
apply(unfold LRSSR_def)
apply(rule disjI2)
apply(clarify)
apply(rule disjI2)
apply(rule RSSR_sym)
apply(assumption)
done

theorem RSSR_iff_LRSSR_and_LRSSR: "RSSR(a,b) <-> (LRSSR(a,b) & LRSSR(b,a))"
apply(insert LRSSR_and_LRSSR_imp_RSSR [of a b])
apply(insert RSSR_imp_LRSSR_and_LRSSR [of a b])
apply(auto)
done

theorem LRSSR_and_NEGR_imp_NEGR: "[|LRSSR(a,b);NEGR(b,c)|] ==> NEGR(a,c)"
apply(unfold LRSSR_def)
apply(safe)
apply(rule LER_and_NEGR_imp_NEGR [of a b c])
apply(safe)
apply(rule RSSR_and_NEGR_imp_NEGR [of a b c])
apply(safe)
done

theorem NEGR_and_LRSSR_imp_NEGR: "[|NEGR(a,b);LRSSR(b,c)|] ==> NEGR(a,c)"
apply(unfold LRSSR_def)
apply(safe)
apply(rule NEGR_and_LER_imp_NEGR [of a b c])
apply(safe)
apply(rule NEGR_and_RSSR_imp_NEGR [of a b c])
apply(safe)
done

theorem LRSSR_total: "LRSSR(a,b) | LRSSR(b,a)"
apply(unfold LRSSR_def)
apply(safe)
apply(insert LER_total)
apply(erule_tac x="a" in allE)
apply(erule_tac x="b" in allE)
apply(safe)
done

theorem LNRSSR_asym: "LNRSSR(a,b) ==> ~LNRSSR(b,a)"
apply(rule ccontr)
apply(auto)
apply(unfold LNRSSR_def)
apply(unfold LRSSR_def)
apply(safe)
apply(drule LER_and_LER_imp_SSR [of a b])
apply(clarify)
apply(drule SSR_imp_RSSR [of a b])
apply(clarify)
done

theorem LNRSSR_trans: "[|LNRSSR(a,b);LNRSSR(b,c)|] ==> LNRSSR(a,c)"
apply(unfold LNRSSR_def)
apply(safe)
apply(unfold LRSSR_def)
apply(safe)
apply(rule LER_trans [of a b c])
apply(safe)
apply(drule_tac a="a" and b="c" and c="b" in RSSR_between)
apply(auto)
done

end