Up to index of Isabelle/FOL/BFO
theory SumsPartitionstheory 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)