Theory SumsPartitions

Up to index of Isabelle/FOL/BFO

theory SumsPartitions
imports Collections
begin

theory SumsPartitions

imports TNEMO Collections

begin


consts

SumPp :: "Co => Ob => Ti => o"
PtPp :: "Co => Ob => Ti => o"
SumFp :: "Co => Ob => Ti => o"
PtFp :: "Co => Ob => Ti => o"

cSumFp :: "Co => Ob => o"
bSumFp :: "Co => Ob => o"
pSumFp :: "Co => Ob => o"

defs 

SumPp_def: "SumPp(p,x,t) == (Pp(p,t) & (ALL z. (O(z,x,t) <-> (EX y. (In(y,p) & O(z,y,t))))))"
SumFp_def: "SumFp(p,x,t) == (Fp(p,t) & (ALL z. (O(z,x,t) <-> (EX y. (In(y,p) & O(z,y,t))))))"
PtPp_def: "PtPp(p,x,t) == (SumPp(p,x,t) & DCo(p,t))"
PtFp_def: "PtFp(p,x,t) == (SumFp(p,x,t) & DCo(p,t))"

cSumFp_def: "cSumFp(p,x) == (ALL t. (E(x,t) --> SumFp(p,x,t)))"
bSumFp_def: "bSumFp(p,x) == (ALL t. (Fp(p,t) --> SumFp(p,x,t)))"
pSumFp_def: "pSumFp(p,x) == cSumFp(p,x) & bSumFp(p,x)"

(* Sums and partitions *)

theorem SumPp_and_In_and_E_imp_P: "(ALL p x y t. (SumPp(p,x,t) & In(y,p) & E(y,t) --> P(y,x,t)))"
apply(rule allI,rule allI,rule allI,rule allI,rule impI,erule conjE,erule conjE)
apply(rule_tac x="y" and y="x" and t="t" in O_imp_O_imp_P_rule)
apply(assumption)
apply(unfold SumPp_def)
apply(auto)
done


lemma SumPp_and_In_and_E_imp_P_rule: "[|SumPp(p,x,t); In(y,p);E(y,t)|] ==> P(y,x,t)"
apply(insert SumPp_and_In_and_E_imp_P)
apply(auto)
done


theorem SumFp_and_In_imp_P: "[|SumFp(p,x,t); In(y,p)|] ==> P(y,x,t)"
apply(unfold SumFp_def)
apply(rule_tac x="y" and y="x" and t="t" in O_imp_O_imp_P_rule)
apply(unfold Fp_def)
apply(auto)
done



theorem SumPp_imp_E: "(ALL p x t. (SumPp(p,x,t) --> E(x,t)))"
apply(rule allI,rule allI,rule allI,rule impI)
apply(unfold SumPp_def)
apply(erule conjE)
apply(unfold Pp_def)
apply(erule exE)
apply(erule conjE)
apply(drule O_refl_rule)
apply(erule_tac x="xa" in allE)
apply(drule conjI)
apply(assumption)
apply(auto)
apply(rotate_tac 2)
apply(drule O_imp_E_and_E)
apply(auto)
done

lemma SumPp_imp_E_rule: "SumPp(p,x,t) ==> E(x,t)"
apply(insert SumPp_imp_E)
apply(auto)
done

theorem SumPp_and_SumPp_imp_Me: "(ALL p x y t. (SumPp(p,x,t) & SumPp(p,y,t) --> Me(x,y,t)))"
apply(rule allI,rule allI,rule allI,rule allI)
apply(rule impI)
apply(erule conjE)
apply(unfold Me_def)
apply(frule SumPp_imp_E_rule)
apply(rotate_tac 1)
apply(frule SumPp_imp_E_rule)
apply(rule conjI)
apply(rule O_imp_O_imp_P_rule)
apply(unfold SumPp_def)
apply(auto)
apply(rule O_imp_O_imp_P_rule)
apply(auto)
done

lemma SumPp_and_SumPp_imp_Me_rule: "[|SumPp(p,x,t);SumPp(p,y,t)|] ==> Me(x,y,t)"
apply(insert SumPp_and_SumPp_imp_Me)
apply(auto)
done

theorem SumPp_and_P_impl_Overlap: "[|SumPp(p,y,t);P(x,y,t)|] ==> (EX z. (In(z,p) & O(x,z,t)))"
apply(unfold SumPp_def)
apply(erule conjE)
apply(erule_tac x="x" in allE)
apply(drule P_imp_O)
apply(auto)
done


theorem SumPp_and_SumPp_and_Subseteq_impl_P: "[|SumPp(p,x,t);SumPp(q,y,t);Subseteq(p,q)|] ==> P(x,y,t)"
apply(rule O_imp_O_imp_P_rule)
apply(drule SumPp_imp_E_rule)
apply(assumption)
apply(unfold SumPp_def)
apply(erule conjE,erule conjE)
apply(rule allI)
apply(rule impI)
apply(erule_tac x="z" in allE)
apply(erule iffE)
apply(drule mp)
apply(assumption)
apply(erule exE)
apply(unfold Subseteq_def)
apply(erule_tac x="ya" in allE)
apply(erule conjE)
apply(drule_tac P="In(ya,p)" and Q="In(ya,q)" in mp)
apply(assumption)
apply(drule_tac P="In(ya, p)" and  Q="O(z, ya, t)" in conjI)
apply(assumption)
apply(rotate_tac 7)
apply(drule_tac x="ya" in exI)
apply(auto)
done


theorem SumFp_imp_SumPp: "SumFp(p,x,t) ==> SumPp(p,x,t)"
apply(unfold SumFp_def,unfold SumPp_def)
apply(insert Fp_imp_Pp)
apply(auto)
done

theorem PtFp_imp_PtPp: "PtFp(p,x,t) ==> PtPp(p,x,t)"
apply(unfold PtFp_def,unfold PtPp_def)
apply(insert SumFp_imp_SumPp)
apply(auto)
done


theorem cSumFp_imp_E_imp_Fp: "cSumFp(p,x) ==> (ALL t. (E(x,t) --> Fp(p,t)))"
apply(unfold cSumFp_def,unfold SumFp_def)
apply(auto)
done

theorem cSumFp_and_In_imp_cP: "[|cSumFp(p,x);In(y,p)|] ==> cP(y,x)"
apply(unfold cSumFp_def,unfold cP_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(clarify)
apply(rule SumFp_and_In_imp_P)
apply(auto)
done

theorem bSumFp_and_Fp_imp_E: "bSumFp(p,x) --> (ALL t. (Fp(p,t) --> E(x,t)))"
apply(unfold bSumFp_def)
apply(safe) 
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule SumFp_imp_SumPp)
apply(drule SumPp_imp_E_rule)
apply(assumption)
done

theorem bSumFp_and_bSumFp_and_Fp_imp_Me: "[|bSumFp(p,x);bSumFp(p,y);Fp(p,t)|] ==> Me(x,y,t)"
apply(unfold bSumFp_def)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule SumFp_imp_SumPp)
apply(drule SumFp_imp_SumPp)
apply(insert SumPp_and_SumPp_imp_Me)
apply(auto)
done

theorem bSumFp_and_cSumFp_and_Subseteq_imp_cP: "[|bSumFp(p,x);cSumFp(q,y);Subseteq(p,q)|] ==> cP(x,y)"
apply(unfold bSumFp_def,unfold cSumFp_def,unfold cP_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(unfold SumFp_def)
apply(drule Subseteq_and_Fp_imp_Fp)
apply(force)
apply(force)
apply(fold SumFp_def)
apply(drule SumFp_imp_SumPp)
apply(drule SumFp_imp_SumPp)
apply(drule_tac p="p" and x="x" and q="q" and y="y" and t="t" in SumPp_and_SumPp_and_Subseteq_impl_P)
apply(auto)
done

theorem cSumFp_and_In_imp_pSumFp: "[|cSumFp(p,x);In(x,p)|] ==> pSumFp(p,x)"
apply(unfold pSumFp_def)
apply(safe)
apply(unfold bSumFp_def)
apply(unfold cSumFp_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(auto)
apply(unfold Fp_def)
apply(auto)
done


theorem pSumFp_imp_Fp_iff_SumFp: "pSumFp(p,x) ==> (ALL t. (Fp(p,t) <-> SumFp(p,x,t)))" 
apply(unfold pSumFp_def,unfold cSumFp_def,unfold bSumFp_def)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(drule SumFp_imp_SumPp)
apply(drule SumPp_imp_E_rule)
apply(auto)
apply(unfold SumFp_def)
apply(auto)
done

theorem pSumFp_imp_E_iff_SumFp: "pSumFp(p,x) ==> (ALL t. (E(x,t) <-> SumFp(p,x,t)))" 
apply(unfold pSumFp_def,unfold cSumFp_def,unfold bSumFp_def)
apply(auto)
apply(drule SumFp_imp_SumPp)
apply(drule SumPp_imp_E_rule)
apply(auto)
done

theorem pSumFp_and_pSumFp_imp_E_iff_E: "[|pSumFp(p,x);pSumFp(p,y)|] ==> (ALL t. (E(x,t) <-> E(y,t)))"
apply(unfold pSumFp_def,unfold cSumFp_def,unfold bSumFp_def)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(unfold SumFp_def)
apply(erule conjE)
apply(fold SumFp_def)
apply(clarify)
apply(drule SumFp_imp_SumPp)
apply(drule SumPp_imp_E_rule)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(clarify)
apply(unfold SumFp_def)
apply(erule conjE)
apply(fold SumFp_def)
apply(clarify)
apply(drule_tac x="x" in SumFp_imp_SumPp)
apply(drule SumPp_imp_E_rule)
apply(assumption)
done

theorem pSumFp_and_pSumFp_imp_E_iff_ME: "[|pSumFp(p,x);pSumFp(p,y)|] ==> (ALL t. (E(x,t) <-> Me(x,y,t)))"
apply(unfold pSumFp_def,unfold cSumFp_def,unfold bSumFp_def)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(clarify)
apply(unfold SumFp_def)
apply(erule conjE)
apply(fold SumFp_def)
apply(clarify)
apply(drule SumFp_imp_SumPp)
apply(drule SumFp_imp_SumPp)
apply(drule SumPp_and_SumPp_imp_Me_rule)
apply(auto)
apply(drule Me_exists2)
apply(auto)
done

end

theorem SumPp_and_In_and_E_imp_P:

  p x y t. SumPp(p, x, t) ∧ In(y, p) ∧ E(y, t) --> P(y, x, t)

lemma SumPp_and_In_and_E_imp_P_rule:

  [| SumPp(p, x, t); In(y, p); E(y, t) |] ==> P(y, x, t)

theorem SumFp_and_In_imp_P:

  [| SumFp(p, x, t); In(y, p) |] ==> P(y, x, t)

theorem SumPp_imp_E:

  p x t. SumPp(p, x, t) --> E(x, t)

lemma SumPp_imp_E_rule:

  SumPp(p, x, t) ==> E(x, t)

theorem SumPp_and_SumPp_imp_Me:

  p x y t. SumPp(p, x, t) ∧ SumPp(p, y, t) --> Me(x, y, t)

lemma SumPp_and_SumPp_imp_Me_rule:

  [| SumPp(p, x, t); SumPp(p, y, t) |] ==> Me(x, y, t)

theorem SumPp_and_P_impl_Overlap:

  [| SumPp(p, y, t); P(x, y, t) |] ==> ∃z. In(z, p) ∧ O(x, z, t)

theorem SumPp_and_SumPp_and_Subseteq_impl_P:

  [| SumPp(p, x, t); SumPp(q, y, t); Subseteq(p, q) |] ==> P(x, y, t)

theorem SumFp_imp_SumPp:

  SumFp(p, x, t) ==> SumPp(p, x, t)

theorem PtFp_imp_PtPp:

  PtFp(p, x, t) ==> PtPp(p, x, t)

theorem cSumFp_imp_E_imp_Fp:

  cSumFp(p, x) ==> ∀t. E(x, t) --> Fp(p, t)

theorem cSumFp_and_In_imp_cP:

  [| cSumFp(p, x); In(y, p) |] ==> cP(y, x)

theorem bSumFp_and_Fp_imp_E:

  bSumFp(p, x) --> (∀t. Fp(p, t) --> E(x, t))

theorem bSumFp_and_bSumFp_and_Fp_imp_Me:

  [| bSumFp(p, x); bSumFp(p, y); Fp(p, t) |] ==> Me(x, y, t)

theorem bSumFp_and_cSumFp_and_Subseteq_imp_cP:

  [| bSumFp(p, x); cSumFp(q, y); Subseteq(p, q) |] ==> cP(x, y)

theorem cSumFp_and_In_imp_pSumFp:

  [| cSumFp(p, x); In(x, p) |] ==> pSumFp(p, x)

theorem pSumFp_imp_Fp_iff_SumFp:

  pSumFp(p, x) ==> ∀t. Fp(p, t) <-> SumFp(p, x, t)

theorem pSumFp_imp_E_iff_SumFp:

  pSumFp(p, x) ==> ∀t. E(x, t) <-> SumFp(p, x, t)

theorem pSumFp_and_pSumFp_imp_E_iff_E:

  [| pSumFp(p, x); pSumFp(p, y) |] ==> ∀t. E(x, t) <-> E(y, t)

theorem pSumFp_and_pSumFp_imp_E_iff_ME:

  [| pSumFp(p, x); pSumFp(p, y) |] ==> ∀t. E(x, t) <-> Me(x, y, t)