Theory QSizeO

theory QSizeO 

imports TORL QSizeR 

begin


consts

SS :: "Ob => Ob => Ti => o"
LE :: "Ob => Ob => Ti => o"
RSS :: "Ob => Ob => Ti => o"
NEG :: "Ob => Ob => Ti => o"
SSC :: "Ob => Ob => Ti => o"

pSS :: "Ob => Ob => o"
pLE :: "Ob => Ob => o"
pRSS :: "Ob => Ob => o"
pNEG :: "Ob => Ob => o"
pSSC :: "Ob => Ob => o"


defs

SS_def: "SS(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & SSR(a,b)))"
LE_def: "LE(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & LER(a,b)))"
RSS_def: "RSS(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & RSSR(a,b)))"
NEG_def: "NEG(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & NEGR(a,b)))"
SSC_def: "SSC(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & SSCR(a,b)))"

pSS_def: "pSS(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> SS(x,y,t)))"
pLE_def: "pLE(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> LE(x,y,t)))"
pRSS_def: "pRSS(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> RSS(x,y,t)))"
pNEG_def: "pNEG(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> NEG(x,y,t)))"
pSSC_def: "pSSC(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> SSC(x,y,t)))"


(*theorems for SS and LE *)

theorem SS_imp_E_and_E: "SS(x,y,t) ==> (E(x,t) & E(y,t))"
apply(unfold SS_def)
apply(insert L_exists2)
apply(auto)
done

theorem SS_refl: "ALL x t. (E(x,t) <-> SS(x,x,t))"
apply(unfold SS_def)
apply(insert SSR_refl)
apply(insert L_exists)
apply(auto)
done

theorem SS_sym: "SS(x,y,t) ==> SS(y,x,t)"
apply(unfold SS_def)
apply(insert SSR_sym)
apply(auto)
done

theorem SS_trans: "[|SS(x,y,t);SS(y,z,t)|] ==> SS(x,z,t)"
apply(unfold SS_def)
apply(clarify)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(drule sym)
apply(frule_tac a="aa" and b="b" and P="% aa. SSR(aa,ba)" in ssubst)
apply(assumption)
apply(drule_tac a="a" and b="b" and c="ba" in SSR_trans)
apply(clarify)
apply(auto)
done



theorem P_and_SS_imp_P: "[|P(x,y,t);SS(x,y,t)|] ==> P(y,x,t)"
apply(unfold SS_def)
apply(clarify)
apply(frule_tac x="x" and y="y" and a="a" and b="b" and t="t" in L_P_PR_rule)
apply(safe)
apply(frule_tac a="a" and b="b" in PR_and_SSR_imp_PR)
apply(assumption)
apply(drule_tac a="a" and b="b" in PR_antisym_rule)
apply(safe)
apply(rule_tac x="x" and y="y" and a="b" and t="t" in P_and_L_and_L_imp_P_rule)
apply(auto)
done

theorem P_and_P_imp_SS: "[|P(x,y,t);P(y,x,t)|] ==> SS(x,y,t)"
apply(unfold SS_def)
apply(drule_tac x="x" and y="y" and t="t" in P_imp_L)
apply(drule_tac x="y" and y="x" and t="t" in P_imp_L)
apply(clarify)
apply(drule_tac x="x" and a="a" and b="ba" and t="t" in L_unique)
apply(assumption)
apply(drule_tac x="y" and a="b" and b="aa" and t="t" in L_unique)
apply(safe)
apply(rule_tac x="ba" in exI)
apply(rule_tac x="aa" in exI)
apply(safe)
apply(rule_tac a="ba" and b="aa" in PR_and_PR_imp_SSR)
apply(auto)
done

theorem LE_total: "[|E(x,t);E(y,t)|] ==> (LE(x,y,t) | LE(y,x,t))"
apply(drule_tac x="x" and t="t" in L_exists1)
apply(drule_tac x="y" and t="t" in L_exists1)
apply(clarify)
apply(unfold LE_def)
apply(rule_tac x="a" in exI)
apply(rule_tac x="aa" in exI)
apply(safe)
apply(auto)
apply(erule_tac x="aa" in allE)
apply(clarify)
apply(erule_tac x="a" in allE)
apply(safe)
apply(insert LER_total)
apply(auto)
done

theorem LE_and_LE_imp_SS: "[|LE(x,y,t);LE(y,x,t)|] ==> SS(x,y,t)"
apply(unfold LE_def)
apply(clarify)
apply(drule_tac x="x" and a="a" and b="ba" and t="t" in L_unique)
apply(drule_tac x="y" and a="aa" and b="b" and t="t" in L_unique)
apply(safe)
apply(unfold SS_def)
apply(rule_tac x="ba" in exI)
apply(rule_tac x="b" in exI)
apply(safe)
apply(drule_tac x="y" and a="aa" and b="b" and t="t" in L_unique)
apply(safe)
apply(rule_tac a="ba" and b="b" in LER_and_LER_imp_SSR)
apply(auto)
done

theorem LE_imp_E_and_E: "LE(x,y,t) ==> (E(x,t) & E(y,t))"
apply(unfold LE_def)
apply(insert L_exists2)
apply(auto)
done


theorem LE_refl: "ALL x t. E(x,t) <-> LE(x,x,t)"
apply(unfold LE_def)
apply(insert L_exists)
apply(insert LER_refl)
apply(auto)
apply(rule_tac x="a" in exI)
apply(auto)
done

theorem LE_trans: "[|LE(x,y,t);LE(y,z,t)|] ==> LE(x,z,t)"
apply(unfold LE_def)
apply(clarify)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(drule sym)
apply(frule_tac a="aa" and b="b" and P="% aa. LER(aa,ba)" in ssubst)
apply(assumption)
apply(drule_tac a="a" and b="b" and c="ba" in LER_trans)
apply(auto)
done


theorem LE_and_LE_imp_SS: "[|LE(x,y,t);LE(y,x,t)|] ==> SS(x,y,t)"
apply(unfold LE_def)
apply(unfold SS_def)
apply(clarify)
apply(drule_tac x="x" and a="a" and b="ba" in L_unique)
apply(assumption)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(insert LER_and_LER_imp_SSR)
apply(auto)
done

theorem SS_and_LE_imp_LE: "[|SS(x,y,t);LE(y,z,t)|] ==> LE(x,z,t)"
apply(unfold LE_def,unfold SS_def)
apply(clarify)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(drule sym)
apply(frule_tac a="aa" and b="b" and P="% aa. LER(aa,ba)" in ssubst)
apply(assumption)
apply(drule_tac c="a" and a="b" and b="ba" in SSR_and_LER_imp_LER)
apply(auto)
done

theorem LE_and_SS_imp_LE: "[|LE(x,y,t);SS(y,z,t)|] ==> LE(x,z,t)"
apply(unfold LE_def,unfold SS_def)
apply(clarify)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(drule sym)
thm ssubst
apply(drule_tac a="aa" and b="b" and P="% aa. SSR(aa,ba)" in ssubst)
apply(assumption)
apply(drule_tac a="a" and b="b" and c="ba" in LER_and_SSR_imp_LER)
apply(auto)
done


(* ------theorems for RSS and NEG ad SSC --------------------------------------------------*)

theorem RSS_imp_E_and_E: "RSS(x,y,t) ==> (E(x,t) & E(y,t))"
apply(unfold RSS_def)
apply(insert L_exists2)
apply(auto)
done

theorem RSS_refl: "ALL x t. (E(x,t) <-> RSS(x,x,t))"
apply(unfold RSS_def)
apply(insert RSSR_refl)
apply(insert L_exists)
apply(auto)
done

theorem RSS_sym: "RSS(x,y,t) ==> RSS(y,x,t)"
apply(unfold RSS_def)
apply(insert RSSR_sym)
apply(auto)
done

theorem RSS_and_SS_imp_RSS:  "[|RSS(x,y,t);SS(y,z,t)|] ==> RSS(x,z,t)"
apply(unfold RSS_def,unfold SS_def)
apply(clarify)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(drule sym)
apply(frule_tac a="aa" and b="b" and P="% aa. SSR(aa,ba)" in ssubst)
apply(assumption)
apply(drule_tac a="a" and b="b" and c="ba" in RSSR_and_SSR_imp_RSSR)
apply(auto)
done

theorem SS_and_RSS_imp_RSS:  "[|SS(x,y,t);RSS(y,z,t)|] ==> RSS(x,z,t)"
apply(unfold RSS_def,unfold SS_def)
apply(clarify)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(drule sym)
apply(frule_tac a="aa" and b="b" and P="% aa. RSSR(aa,ba)" in ssubst)
apply(assumption)
apply(drule_tac a="a" and b="b" and c="ba" in SSR_and_RSSR_imp_RSSR)
apply(auto)
done


theorem NEG_imp_LE: "NEG(x,y,t) ==> LE(x,y,t)"
apply(unfold NEG_def,unfold LE_def)
apply(insert NEGR_imp_LER)
apply(auto)
done

theorem NEG_imp_E_and_E: "NEG(x,y,t) ==>(E(x,t) & E(y,t))"
apply(drule NEG_imp_LE)
apply(drule LE_imp_E_and_E)
apply(auto)
done

theorem NEG_irrefl: "ALL x t. ~NEG(x,x,t)"
apply(unfold NEG_def)
apply(auto)
apply(drule_tac x="x" and a="a" and b="b" and t="t" in L_unique)
apply(clarify)
apply(insert NEGR_irrefl)
apply(auto)
done

theorem NEG_assym: "NEG(x,y,t) ==> ~NEG(y,x,t)"
apply(unfold NEG_def)
apply(safe)
apply(drule_tac x="x" and a="a" and b="ba" and t="t" in L_unique)
apply(assumption)
apply(drule_tac x="y" and a="b" and b="aa" and t="t" in L_unique)
apply(assumption)
apply(insert NEGR_assym)
apply(auto)
done


theorem NEG_trans: "[|NEG(x,y,t);NEG(y,z,t)|] ==> NEG(x,z,t)"
apply(unfold NEG_def)
apply(clarify)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(drule sym)
apply(frule_tac a="aa" and b="b" and P="% aa. NEGR(aa,ba)" in ssubst)
apply(assumption)
apply(drule_tac a="a" and b="b" and c="ba" in NEGR_trans)
apply(auto)
done

theorem NEG_and_LE_imp_NEG: "[|NEG(x,y,t);LE(y,z,t)|] ==> NEG(x,z,t)"
apply(unfold NEG_def,unfold LE_def)
apply(clarify)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(drule sym)
apply(frule_tac a="aa" and b="b" and P="% aa. LER(aa,ba)" in ssubst)
apply(assumption)
apply(drule_tac a="a" and b="b" and c="ba" in NEGR_and_LER_imp_NEGR)
apply(auto)
done

theorem LE_and_NEG_imp_NEG: "[|LE(x,y,t);NEG(y,z,t)|] ==> NEG(x,z,t)"
apply(unfold NEG_def,unfold LE_def)
apply(clarify)
apply(drule_tac x="y" and a="aa" and b="b" in L_unique)
apply(assumption)
apply(drule sym)
apply(frule_tac a="aa" and b="b" and P="% aa. NEGR(aa,ba)" in ssubst)
apply(assumption)
apply(drule_tac a="a" and b="b" and c="ba" in LER_and_NEGR_imp_NEGR)
apply(auto)
done

theorem P_imp_LE: "P(x,y,t) ==> LE(x,y,t)"
apply(unfold LE_def)
apply(drule_tac x="x" and y="y" and t="t" in P_imp_L)
apply(safe)
apply(rule_tac x="a" in exI)
apply(rule_tac x="b" in exI)
apply(safe)
apply(rule PR_imp_LER)
apply(auto)
done


theorem NEG_and_P_imp_NEG: "[|NEG(x,y,t);P(y,z,t)|] ==> NEG(x,z,t)"
apply(drule_tac x="y" and y="z" and t="t" in P_imp_LE)
apply(rule_tac x="x" and z="z" and t="t" in NEG_and_LE_imp_NEG)
apply(auto)
done

theorem P_and_NEG_imp_NEG: "[|P(x,y,t);NEG(y,z,t)|] ==> NEG(x,z,t)"
apply(drule_tac x="x" and y="y" and t="t" in P_imp_LE)
thm LE_and_NEG_imp_NEG
apply(rule_tac x="x" and z="z" and t="t" in LE_and_NEG_imp_NEG)
apply(auto)
done

theorem SSC_refl: "ALL x t. (E(x,t) <-> SSC(x,x,t))"
apply(unfold SSC_def)
apply(insert SSCR_refl)
apply(insert L_exists)
apply(auto)
done

theorem SSC_sym: "SSC(x,y,t) ==> SSC(y,x,t)"
apply(unfold SSC_def)
apply(insert SSCR_sym)
apply(auto)
done

(* ------theorems for pSS and pLE --------------------------------------------------*)


theorem pSS_refl: "ALL x. pSS(x,x)"
apply(unfold pSS_def)
apply(insert SS_refl)
apply(auto)
done

theorem pSS_sym: "pSS(x,y) ==> pSS(y,x)"
apply(unfold pSS_def)
apply(insert SS_sym)
apply(auto)
done

theorem pSS_trans: "[|pSS(x,y);pSS(y,z)|] ==> pSS(x,z)"
apply(unfold pSS_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" in SS_imp_E_and_E)
apply(safe)
apply(drule SS_trans)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="y" and y="z" in SS_imp_E_and_E)
apply(auto)
apply(drule SS_trans)
apply(auto)
done


theorem pP_and_pSS_imp_pP: "[|pP(x,y);pSS(x,y)|] ==> pP(y,x)"
apply(unfold pP_def, unfold pSS_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(rule_tac y="y" and x="x" and t="t" in P_and_SS_imp_P)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(rule_tac y="y" and x="x" and t="t" in P_and_SS_imp_P)
apply(safe)
done




theorem pLE_refl: "ALL x. pLE(x,x)"
apply(unfold pLE_def)
apply(insert LE_refl)
apply(auto)
done


theorem pLE_trans: "[|pLE(x,y);pLE(y,z)|] ==> pLE(x,z)"
apply(unfold pLE_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" in LE_imp_E_and_E)
apply(safe)
apply(drule LE_trans)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="y" and y="z" in LE_imp_E_and_E)
apply(auto)
apply(drule LE_trans)
apply(auto)
done

theorem pLE_and_pLE_imp_pSS: "[|pLE(x,y);pLE(y,x)|] ==> pSS(x,y)"
apply(unfold pLE_def,unfold pSS_def)
apply(rule allI)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(insert LE_and_LE_imp_SS)
apply(auto)
done

theorem pSS_and_pLE_imp_pLE: "[|pSS(x,y);pLE(y,z)|] ==> pLE(x,z)"
apply(unfold pLE_def,unfold pSS_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" in SS_imp_E_and_E)
apply(safe)
apply(drule SS_and_LE_imp_LE)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="y" and y="z" in LE_imp_E_and_E)
apply(auto)
apply(drule SS_and_LE_imp_LE)
apply(auto)
done

theorem pLE_and_pSS_imp_pLE: "[|pLE(x,y);pSS(y,z)|] ==> pLE(x,z)"
apply(unfold pLE_def,unfold pSS_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" in LE_imp_E_and_E)
apply(safe)
apply(drule LE_and_SS_imp_LE)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="y" and y="z" in SS_imp_E_and_E)
apply(auto)
apply(drule LE_and_SS_imp_LE)
apply(auto)
done


(* ------theorems for pRSS and pNEG pSSC --------------------------------------------------*)

theorem pRSS_refl: "ALL x. pRSS(x,x)"
apply(unfold pRSS_def)
apply(insert RSS_refl)
apply(auto)
done

theorem pRSS_sym: "pRSS(x,y) ==> pRSS(y,x)"
apply(unfold pRSS_def)
apply(insert RSS_sym)
apply(auto)
done


theorem pRSS_and_pSS_imp_pRSS: "[|pRSS(x,y);pSS(y,z)|] ==> pRSS(x,z)"
apply(unfold pSS_def,unfold pRSS_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" in RSS_imp_E_and_E)
apply(safe)
apply(drule RSS_and_SS_imp_RSS)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="y" and y="z" in SS_imp_E_and_E)
apply(auto)
apply(drule RSS_and_SS_imp_RSS)
apply(auto)
done


theorem pSS_and_pRSS_imp_pRSS: "[|pSS(x,y);pRSS(y,z)|] ==> pRSS(x,z)"
apply(unfold pSS_def,unfold pRSS_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" in SS_imp_E_and_E)
apply(safe)
apply(drule SS_and_RSS_imp_RSS)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="y" and y="z" in RSS_imp_E_and_E)
apply(auto)
apply(drule SS_and_RSS_imp_RSS)
apply(auto)
done

theorem pNEG_irrefl: "ALL x. ~pNEG(x,x)"
apply(insert P_exists1) 
apply(unfold pNEG_def)
apply(auto)
apply(erule_tac x="x" in allE)
apply(erule exE)
apply(rule_tac x="t" in exI)
apply(safe)
apply(insert NEG_irrefl)
apply(erule_tac x="x" in allE)
apply(erule_tac x="t" in allE)
apply(auto)
done

theorem pNEG_assym: "pNEG(x,y) ==> ~pNEG(y,x)"
apply(unfold pNEG_def)
apply(safe)
apply(insert P_exists1)
apply(erule_tac x="x" in allE)
apply(erule exE)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(insert NEG_assym)
apply(auto)
done


theorem pNEG_trans: "[|pNEG(x,y);pNEG(y,z)|] ==> pNEG(x,z)"
apply(unfold pNEG_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" in NEG_imp_E_and_E)
apply(safe)
apply(drule NEG_trans)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="y" and y="z" in NEG_imp_E_and_E)
apply(auto)
apply(drule NEG_trans)
apply(auto)
done

theorem pNEG_and_pLE_imp_pNEG: "[|pNEG(x,y);pLE(y,z)|] ==> pNEG(x,z)"
apply(unfold pNEG_def,unfold pLE_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" in NEG_imp_E_and_E)
apply(safe)
apply(drule NEG_and_LE_imp_NEG)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="y" and y="z" in LE_imp_E_and_E)
apply(auto)
apply(drule NEG_and_LE_imp_NEG)
apply(auto)
done

theorem pLE_and_pNEG_imp_pNEG: "[|pLE(x,y);pNEG(y,z)|] ==> pNEG(x,z)"
apply(unfold pNEG_def,unfold pLE_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" in LE_imp_E_and_E)
apply(safe)
apply(drule LE_and_NEG_imp_NEG)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="y" and y="z" in NEG_imp_E_and_E)
apply(auto)
apply(drule LE_and_NEG_imp_NEG)
apply(auto)
done

theorem pP_imp_pLE: "pP(x,y) ==> pLE(x,y)"
apply(unfold pP_def,unfold pLE_def)
apply(insert P_imp_LE)
apply(auto)
done

theorem pNEG_and_pP_imp_pNEG: "[|pNEG(x,y);pP(y,z)|] ==> pNEG(x,z)"
apply(drule_tac x="y" and y="z"  in pP_imp_pLE)
apply(rule_tac x="x" and z="z"  in pNEG_and_pLE_imp_pNEG)
apply(auto)
done

theorem pP_and_pNEG_imp_pNEG: "[|pP(x,y);pNEG(y,z)|] ==> pNEG(x,z)"
apply(drule_tac x="x" and y="y" in pP_imp_pLE)
apply(rule_tac x="x" and z="z" in pLE_and_pNEG_imp_pNEG)
apply(auto)
done


theorem pSSC_refl: "ALL x. pSSC(x,x)"
apply(unfold pSSC_def)
apply(insert SSC_refl)
apply(auto)
done

theorem pSSC_sym: "pSSC(x,y) ==> pSSC(y,x)"
apply(unfold pSSC_def)
apply(insert SSC_sym)
apply(auto)
done


end