Up to index of Isabelle/FOL/BFO
theory UniversalParthoodtheory UniversalParthood imports ExtensionsOfUniversals PartonomicInclusion begin consts UPt1 :: "Un => Un => Ti => o" UPt2 :: "Un => Un => Ti => o" UPt12 :: "Un => Un => Ti => o" UP1 :: "Un => Un => o" UP2 :: "Un => Un => o" UP12 :: "Un => Un => o" defs UPt1_def: "UPt1(c,d,t) == (ALL x. (Inst(x,c,t) --> (EX y. (Inst(y,d,t) & P(x,y,t)))))" UPt2_def: "UPt2(c,d,t) == (ALL y. (Inst(y,d,t) --> (EX x. (Inst(x,c,t) & P(x,y,t)))))" UPt12_def: "UPt12(c,d,t) == UPt1(c,d,t) & UPt2(c,d,t)" UP1_def: "UP1(c,d) == (ALL t. UPt1(c,d,t))" UP2_def: "UP2(c,d) == (ALL t. UPt2(c,d,t))" UP12_def: "UP12(c,d) == (ALL t. UPt12(c,d,t))" (* theorems about universal parthood *) theorem ExtCo_and_ExtCo: "[|ExtCo(p,c,t);ExtCo(q,d,t)|] ==> (P1(p,q,t) <-> UPt1(c,d,t))" apply(unfold iff_def) apply(unfold ExtCo_def) apply(unfold P1_def) apply(unfold UPt1_def) apply(auto) done theorem ExtOb_and_ExtOb: "[|ExtOb(x,c,t);ExtOb(y,d,t)|] ==> (P(x,y,t) <-> UPt1(c,d,t))" apply(unfold iff_def) apply(unfold ExtOb_def) apply(unfold UPt1_def) apply(rule conjI) apply(rule impI) apply(rule allI) apply(rule impI) apply(erule conjE) apply(erule conjE) apply(rule_tac x="y" in exI) apply(rule conjI) apply(assumption) apply(erule_tac x="xa" in allE) apply(drule mp) apply(assumption) apply(erule_tac a="x" and b="xa" in subst) apply(assumption) apply(rule impI) apply(erule_tac x="x" in allE) apply(erule conjE) apply(erule conjE) apply(drule mp) apply(assumption) apply(erule exE) apply(erule conjE) apply(rotate_tac 3) apply(erule_tac x="ya" in allE) apply(drule mp) apply(assumption) apply(drule_tac a="y" and b="ya" in sym) apply(erule_tac a="ya" and b="y" in subst) apply(assumption) done theorem ExtCo_and_ExtOb: "[|ExtCo(p,c,t);ExtOb(x,d,t)|] ==> ((EX y. (Inst(y,c,t) & P(y,x,t)))) <-> UPt2(c,d,t)" apply(unfold iff_def) apply(unfold UPt2_def) apply(unfold ExtCo_def) apply(unfold ExtOb_def) apply(auto) done theorem ExtOb_and_ExtCo: "[|ExtOb(x,c,t);ExtCo(p,d,t)|] ==> ((EX y. (Inst(y,d,t) & P(x,y,t)))) <-> UPt1(c,d,t)" apply(unfold iff_def) apply(unfold UPt1_def) apply(unfold ExtOb_def) apply(unfold ExtCo_def) apply(auto) done theorem UPt1_refl: "(ALL c t. UPt1(c,c,t))" apply(unfold UPt1_def) apply(auto) apply(rule_tac x="x" in exI) apply(auto) apply(insert Inst_E) apply(unfold E_def) apply(auto) done theorem UPt2_refl: "(ALL c t. UPt2(c,c,t))" apply(unfold UPt2_def) apply(auto) apply(rule_tac x="y" in exI) apply(auto) apply(insert Inst_E) apply(unfold E_def) apply(auto) done theorem UPt12_refl: "(ALL c t. UPt12(c,c,t))" apply(unfold UPt12_def) apply(insert UPt1_refl) apply(insert UPt2_refl) apply(auto) done theorem UPt1_trans: "[|UPt1(c,d,t);UPt1(d,e,t)|]==> UPt1(c,e,t)" apply(unfold UPt1_def) apply(auto) apply(erule_tac x="x" in allE) apply(auto) apply(erule_tac x="y" in allE) apply(auto) apply(rule_tac x="ya" in exI) apply(drule_tac x="x" and y="y" and z="ya" in P_trans_rule) apply(auto) done theorem UPt2_trans: "[|UPt2(c,d,t);UPt2(d,e,t)|]==> UPt2(c,e,t)" apply(unfold UPt2_def) apply(auto) apply(rotate_tac 1) apply(erule_tac x="y" in allE) apply(auto) apply(erule_tac x="x" in allE) apply(auto) apply(rule_tac x="xa" in exI) apply(drule_tac x="xa" and y="x" and z="y" in P_trans_rule) apply(auto) done theorem UPt12_trans: "[|UPt12(c,d,t);UPt12(d,e,t)|]==> UPt12(c,e,t)" apply(unfold UPt12_def) apply(auto) apply(drule UPt1_trans) apply(auto) apply(drule UPt2_trans) apply(auto) done theorem UP1_iff: "(ALL c d. (UP1(c,d) <-> (ALL t x. (Inst(x,c,t) --> (EX y. (Inst(y,d,t) & P(x,y,t)))))))" apply(unfold UP1_def,unfold UPt1_def) apply(auto) done theorem UP2_iff: "(ALL c d. (UP2(c,d) <-> (ALL t y. (Inst(y,d,t) --> (EX x. (Inst(x,c,t) & P(x,y,t)))))))" apply(unfold UP2_def,unfold UPt2_def) apply(auto) done theorem UP1_refl: "(ALL c. UP1(c,c))" apply(unfold UP1_def) apply(insert UPt1_refl) apply(auto) done theorem UP2_refl: "(ALL c. UP2(c,c))" apply(unfold UP2_def) apply(insert UPt2_refl) apply(auto) done theorem UP12_refl: "(ALL c. UP12(c,c))" apply(unfold UP12_def) apply(insert UPt12_refl) apply(auto) done theorem UP1_trans: "[|UP1(c,d);UP1(d,e)|]==> UP1(c,e)" apply(unfold UP1_def) apply(auto) apply(drule_tac x="t" in allE) apply(drule_tac x="t" in allE) apply(drule UPt1_trans) apply(auto) done theorem UP2_trans: "[|UP2(c,d);UP2(d,e)|]==> UP2(c,e)" apply(unfold UP2_def) apply(auto) apply(drule_tac x="t" in allE) apply(drule_tac x="t" in allE) apply(drule UPt2_trans) apply(auto) done theorem UP12_trans: "[|UP12(c,d);UP12(d,e)|]==> UP12(c,e)" apply(unfold UP12_def) apply(auto) apply(drule_tac x="t" in allE) apply(drule_tac x="t" in allE) apply(drule UPt12_trans) apply(auto) done theorem UP12_impl_UP1_and_UP2: "UP12(c,d) ==> (UP1(c,d) & UP2(c,d))" apply(unfold UP12_def,unfold UP1_def,unfold UP2_def) apply(rule conjI) apply(rule allI) apply(erule_tac x="t" in allE) apply(unfold UPt12_def) apply(auto) done theorem IsA_and_UP1_impl_UP1_1: "[|IsA(e,c);UP1(c,d)|] ==> UP1(e,d)" apply(unfold UP1_def,unfold UPt1_def) apply(drule_tac c="e" and d="c" in Inst_IsA_rule) apply(auto) done theorem IsA_and_UP1_impl_UP1_2: "[|IsA(d,e);UP1(c,d)|] ==> UP1(c,e)" apply(unfold UP1_def,unfold UPt1_def) apply(drule_tac c="d" and d="e" in Inst_IsA_rule) apply(auto) apply(erule_tac x="t" in allE) apply(rotate_tac 2) apply(erule_tac x="x" in allE) apply(auto) done theorem IsA_and_UP2_impl_UP2_1: "[|IsA(e,d);UP2(c,d)|] ==> UP2(c,e)" apply(unfold UP2_def,unfold UPt2_def) apply(drule_tac c="e" and d="d" in Inst_IsA_rule) apply(auto) done theorem IsA_and_UP2_impl_UP2_2: "[|IsA(c,e);UP2(c,d)|] ==> UP2(e,d)" apply(unfold UP2_def,unfold UPt2_def) apply(drule_tac c="c" and d="e" in Inst_IsA_rule) apply(auto) apply(erule_tac x="t" in allE) apply(rotate_tac 2) apply(erule_tac x="y" in allE) apply(auto) done theorem IsA_and_UP12_impl_UP1_1: "[|IsA(e,c);UP12(c,d)|] ==> UP1(e,d)" apply(drule UP12_impl_UP1_and_UP2) apply(erule conjE) apply(drule IsA_and_UP1_impl_UP1_1) apply(auto) done theorem IsA_and_UP12_impl_UP2_2: "[|IsA(c,e);UP12(c,d)|] ==> UP2(e,d)" apply(drule UP12_impl_UP1_and_UP2) apply(erule conjE) apply(drule IsA_and_UP2_impl_UP2_2) apply(auto) done theorem IsA_and_UP12_impl_UP2_1: "[|IsA(e,d);UP12(c,d)|] ==> UP2(c,e)" apply(drule UP12_impl_UP1_and_UP2) apply(erule conjE) apply(drule IsA_and_UP2_impl_UP2_1) apply(auto) done theorem IsA_and_UP12_impl_UP1_2: "[|IsA(d,e);UP12(c,d)|] ==> UP1(c,e)" apply(drule UP12_impl_UP1_and_UP2) apply(erule conjE) apply(drule IsA_and_UP1_impl_UP1_2) apply(auto) done theorem IsA_imp_UP1: "IsA(c,d) ==> UP1(c,d)" apply(unfold UP1_def) apply(safe) apply(unfold UPt1_def) apply(safe) apply(drule Inst_IsA_rule [of c d]) apply(erule_tac x="x" in allE) apply(erule_tac x="t" in allE) apply(safe) apply(rule_tac x="x" in exI) apply(insert Inst_E) apply(insert P_refl) apply(auto) done end
theorem ExtCo_and_ExtCo:
[| ExtCo(p, c, t); ExtCo(q, d, t) |] ==> P1(p, q, t) <-> UPt1(c, d, t)
theorem ExtOb_and_ExtOb:
[| ExtOb(x, c, t); ExtOb(y, d, t) |] ==> P(x, y, t) <-> UPt1(c, d, t)
theorem ExtCo_and_ExtOb:
[| ExtCo(p, c, t); ExtOb(x, d, t) |]
==> (∃y. Inst(y, c, t) ∧ P(y, x, t)) <-> UPt2(c, d, t)
theorem ExtOb_and_ExtCo:
[| ExtOb(x, c, t); ExtCo(p, d, t) |]
==> (∃y. Inst(y, d, t) ∧ P(x, y, t)) <-> UPt1(c, d, t)
theorem UPt1_refl:
∀c t. UPt1(c, c, t)
theorem UPt2_refl:
∀c t. UPt2(c, c, t)
theorem UPt12_refl:
∀c t. UPt12(c, c, t)
theorem UPt1_trans:
[| UPt1(c, d, t); UPt1(d, e, t) |] ==> UPt1(c, e, t)
theorem UPt2_trans:
[| UPt2(c, d, t); UPt2(d, e, t) |] ==> UPt2(c, e, t)
theorem UPt12_trans:
[| UPt12(c, d, t); UPt12(d, e, t) |] ==> UPt12(c, e, t)
theorem UP1_iff:
∀c d. UP1(c, d) <-> (∀t x. Inst(x, c, t) --> (∃y. Inst(y, d, t) ∧ P(x, y, t)))
theorem UP2_iff:
∀c d. UP2(c, d) <-> (∀t y. Inst(y, d, t) --> (∃x. Inst(x, c, t) ∧ P(x, y, t)))
theorem UP1_refl:
∀c. UP1(c, c)
theorem UP2_refl:
∀c. UP2(c, c)
theorem UP12_refl:
∀c. UP12(c, c)
theorem UP1_trans:
[| UP1(c, d); UP1(d, e) |] ==> UP1(c, e)
theorem UP2_trans:
[| UP2(c, d); UP2(d, e) |] ==> UP2(c, e)
theorem UP12_trans:
[| UP12(c, d); UP12(d, e) |] ==> UP12(c, e)
theorem UP12_impl_UP1_and_UP2:
UP12(c, d) ==> UP1(c, d) ∧ UP2(c, d)
theorem IsA_and_UP1_impl_UP1_1:
[| IsA(e, c); UP1(c, d) |] ==> UP1(e, d)
theorem IsA_and_UP1_impl_UP1_2:
[| IsA(d, e); UP1(c, d) |] ==> UP1(c, e)
theorem IsA_and_UP2_impl_UP2_1:
[| IsA(e, d); UP2(c, d) |] ==> UP2(c, e)
theorem IsA_and_UP2_impl_UP2_2:
[| IsA(c, e); UP2(c, d) |] ==> UP2(e, d)
theorem IsA_and_UP12_impl_UP1_1:
[| IsA(e, c); UP12(c, d) |] ==> UP1(e, d)
theorem IsA_and_UP12_impl_UP2_2:
[| IsA(c, e); UP12(c, d) |] ==> UP2(e, d)
theorem IsA_and_UP12_impl_UP2_1:
[| IsA(e, d); UP12(c, d) |] ==> UP2(c, e)
theorem IsA_and_UP12_impl_UP1_2:
[| IsA(d, e); UP12(c, d) |] ==> UP1(c, e)
theorem IsA_imp_UP1:
IsA(c, d) ==> UP1(c, d)