Theory ExtensionsOfUniversals

Up to index of Isabelle/FOL/BFO

theory ExtensionsOfUniversals
imports Instantiation Collections
begin

theory 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