Up to index of Isabelle/FOL/BFO
theory ExtensionsOfUniversalstheory ExtensionsOfUniversals imports Instantiation Collections begin consts ExtCo :: "Co => Un => Ti => o" ExtOb :: "Ob => Un => Ti => o" DUn :: "Un => o" axioms Inst_impl_ExtOb_or_ExtCo: "Inst(x,c,t) ==> (ExtOb(x,c,t) | (EX p. ExtCo(p,c,t)))" defs ExtCo_def: "ExtCo(p,c,t) == (ALL x. (In(x,p) <-> Inst(x,c,t)))" ExtOb_def: "ExtOb(x,c,t) == (Inst(x,c,t) & (ALL y. (Inst(y,c,t) --> x=y)))" DUn_def: "DUn(c) == (ALL t. (ALL p. ExtCo(p,c,t) --> DCo(p,t)))" (* theorems about extensions of universals *) theorem DistinctInsts_impl_ExtCo: "[|Inst(x,c,t);Inst(y,c,t); (x~=y)|] ==> (EX p. ExtCo(p,c,t))" apply(drule Inst_impl_ExtOb_or_ExtCo [of x c t]) apply(erule disjE) apply(rule_tac x="p" in exI) apply(unfold ExtOb_def) apply(erule conjE) apply(erule_tac x="y" in allE) apply(auto) done theorem ExtOb_unique: "[|ExtOb(x,c,t);ExtOb(y,c,t)|] ==> x=y" apply(unfold ExtOb_def) apply(auto) done theorem ExtCo_unique: "[|ExtCo(p,c,t);ExtCo(q,c,t)|] ==> p = q" apply(rule Co_ext_rule2) apply(auto) apply(unfold ExtCo_def) apply(auto) done theorem ExtCo_Fp: "ExtCo(p,c,t) ==> Fp(p,t)" apply(unfold Fp_def,unfold ExtCo_def) apply(auto) apply(insert Inst_E) apply(auto) done theorem ExtCo_impl_2members: "ExtCo(p,c,t) ==> (EX x y. (In(x,p) & In(y,p) & x ~= y))" apply(insert Co_members) apply(auto) done theorem IsA_impl_Subseteq: "[|IsA(c,d);ExtCo(p,c,t);ExtCo(q,d,t)|] ==> Subseteq(p,q)" apply(unfold ExtCo_def) apply(unfold Subseteq_def) apply(auto) apply(drule Inst_IsA_rule) apply(auto) done theorem ExtOb_impl_notExtCo: "ExtOb(x,c,t) ==> (~(EX p. ExtCo(p,c,t)))" apply(clarify) apply(insert Co_members) apply(erule_tac x="p" in allE) apply(unfold ExtOb_def) apply(unfold ExtCo_def) apply(clarify) apply(frule_tac x="xa" in spec) apply(erule_tac x="y" in allE) apply(frule_tac x="xa" in spec) apply(erule_tac x="y" in allE) apply(auto) done theorem ExtCo_impl_notExtOb: "ExtCo(p,c,t) ==> (~(EX x. ExtOb(x,c,t)))" apply(clarify) apply(insert Co_members) apply(erule_tac x="p" in allE) apply(unfold ExtOb_def) apply(unfold ExtCo_def) apply(clarify) apply(frule_tac x="xa" in spec) apply(erule_tac x="y" in allE) apply(frule_tac x="xa" in spec) apply(erule_tac x="y" in allE) apply(auto) done theorem NoExt_or_ExtOb_or_ExtDCo_impl_DUn: "(ALL t. ((~ (EX x. Inst(x,c,t))) | (EX x. ExtOb(x,c,t)) | (EX p. ExtCo(p,c,t) & DCo(p,t)))) ==> DUn(c)" apply(unfold DUn_def) apply(clarify) apply(erule_tac x="t" in allE) apply(safe) apply(unfold ExtCo_def) apply(insert Co_members) apply(force) apply(fold ExtCo_def) apply(insert ExtCo_impl_notExtOb) apply(force) apply(insert ExtCo_unique) apply(force) done theorem DUn_impl_NoExt_or_ExtOb_or_ExtDCo: "DUn(c) ==> (ALL t. ((~ (EX x. Inst(x,c,t))) | (EX x. ExtOb(x,c,t)) | (EX p. ExtCo(p,c,t) & DCo(p,t))))" apply(clarify) apply(drule_tac x="x" and c="c" and t="t" in Inst_impl_ExtOb_or_ExtCo) apply(auto) apply(unfold DUn_def) apply(erule_tac x="t" in allE) apply(erule_tac x="p" in allE) apply(erule_tac x="x" in allE) apply(erule_tac x="p" in allE) apply(auto) done theorem DUn_iff_NoExt_or_ExtOb_or_ExtDCo: "DUn(c) <-> (ALL t. ((~ (EX x. Inst(x,c,t))) | (EX x. ExtOb(x,c,t)) | (EX p. ExtCo(p,c,t) & DCo(p,t))))" apply(rule iffI) apply(rule DUn_impl_NoExt_or_ExtOb_or_ExtDCo) apply(assumption) apply(rule NoExt_or_ExtOb_or_ExtDCo_impl_DUn) apply(assumption) done theorem DUn_and_O_impl_Id: "[|DUn(c);Inst(x,c,t);Inst(y,c,t);O(x,y,t)|] ==> x = y" apply(frule_tac x="x" and c="c" and t="t" in Inst_impl_ExtOb_or_ExtCo) apply(frule_tac x="y" and c="c" and t="t" in Inst_impl_ExtOb_or_ExtCo) apply(safe) apply(unfold ExtOb_def) apply(clarify) apply(erule_tac x="y" in allE) apply(force) apply(fold ExtOb_def) apply(drule ExtCo_impl_notExtOb) apply(force) apply(drule ExtCo_impl_notExtOb) apply(force) apply(drule_tac p="p" and c="c" and t="t" and q="pa" in ExtCo_unique) apply(assumption) apply(unfold DUn_def) apply(erule_tac x="t" in allE) apply(erule_tac x="pa" in allE) apply(auto) apply(unfold ExtCo_def,unfold DCo_def) apply(frule_tac x="x" in spec) apply(erule_tac x="y" in allE) apply(erule_tac x="x" in allE) apply(erule_tac x="y" in allE) apply(auto) done end
theorem DistinctInsts_impl_ExtCo:
[| Inst(x, c, t); Inst(y, c, t); x ≠ y |] ==> ∃p. ExtCo(p, c, t)
theorem ExtOb_unique:
[| ExtOb(x, c, t); ExtOb(y, c, t) |] ==> x = y
theorem ExtCo_unique:
[| ExtCo(p, c, t); ExtCo(q, c, t) |] ==> p = q
theorem ExtCo_Fp:
ExtCo(p, c, t) ==> Fp(p, t)
theorem ExtCo_impl_2members:
ExtCo(p, c, t) ==> ∃x y. In(x, p) ∧ In(y, p) ∧ x ≠ y
theorem IsA_impl_Subseteq:
[| IsA(c, d); ExtCo(p, c, t); ExtCo(q, d, t) |] ==> Subseteq(p, q)
theorem ExtOb_impl_notExtCo:
ExtOb(x, c, t) ==> ¬ (∃p. ExtCo(p, c, t))
theorem ExtCo_impl_notExtOb:
ExtCo(p, c, t) ==> ¬ (∃x. ExtOb(x, c, t))
theorem NoExt_or_ExtOb_or_ExtDCo_impl_DUn:
∀t. ¬ (∃x. Inst(x, c, t)) ∨
(∃x. ExtOb(x, c, t)) ∨ (∃p. ExtCo(p, c, t) ∧ DCo(p, t))
==> DUn(c)
theorem DUn_impl_NoExt_or_ExtOb_or_ExtDCo:
DUn(c)
==> ∀t. ¬ (∃x. Inst(x, c, t)) ∨
(∃x. ExtOb(x, c, t)) ∨ (∃p. ExtCo(p, c, t) ∧ DCo(p, t))
theorem DUn_iff_NoExt_or_ExtOb_or_ExtDCo:
DUn(c) <->
(∀t. ¬ (∃x. Inst(x, c, t)) ∨
(∃x. ExtOb(x, c, t)) ∨ (∃p. ExtCo(p, c, t) ∧ DCo(p, t)))
theorem DUn_and_O_impl_Id:
[| DUn(c); Inst(x, c, t); Inst(y, c, t); O(x, y, t) |] ==> x = y