Theory Collections

Up to index of Isabelle/FOL/BFO

theory Collections
imports TNEMO
begin

theory Collections 

imports TNEMO

begin

typedecl Co


arities Co :: "term"

consts


In :: "Ob => Co => o"
Union :: "Co => Co => Co => o"
Intersect :: "Co => Co => Co => o"
Subseteq :: "Co => Co => o"
Fp :: "Co => Ti => o"
Pp :: "Co => Ti => o"
Np :: "Co => Ti => o"

DCo :: "Co => Ti => o"

axioms

Co_members: "(ALL p. (EX x y. (In(x,p) & In(y,p) & x ~= y)))"
Co_ext: "(ALL p q. (p=q <-> (ALL x. (In(x,p) <-> In(x,q)))))"
Co_union: "(ALL p q. (EX r. (Union(p,q,r))))"
Co_intersect: "(ALL p q. (EX x y. (x ~= y & In(x,p) & In(x,q) & In(y,p) & In(y,q))) --> (EX r. (Intersect(p,q,r))))"

defs

Subseteq_def: "Subseteq(p,q) == (ALL x. (In(x,p) --> In(x,q)))" 
Union_def: "Union(p,q,r) == (ALL x. (In(x,r) <-> (In(x,p) | In(x,q))))"
Intersect_def: "Intersect(p,q,r) == (ALL x. (In(x,r) <-> (In(x,p) & In(x,q))))"
Fp_def: "Fp(p,t) == (ALL x. (In(x,p) --> E(x,t)))"
Pp_def: "Pp(p,t) == (EX x. (In(x,p) & E(x,t)))"
Np_def: "Np(p,t) == (~Pp(p,t))"

DCo_def: "DCo(p,t) == (ALL x y. (In(x,p) & In(y,p) & O(x,y,t) --> x=y))"

(* axioms as rules *)

lemma Co_ext_rule1: "p=q ==> (ALL x. (In(x,p) <-> In(x,q)))"
apply(insert Co_ext)
apply(auto)
done

lemma Co_ext_rule2: "(ALL x. (In(x,p) <-> In(x,q))) ==> p=q"
apply(insert Co_ext)
apply(auto)
done

(* theorems and lemmata for collections *)

theorem Union_unique: "[|Union(p,q,r1);Union(p,q,r2)|] ==> r1=r2"
apply(unfold Union_def)
apply(insert Co_ext)
apply(blast)
done

theorem Intersect_unique: "[|Intersect(p,q,r1);Intersect(p,q,r2)|] ==> r1=r2"
apply(unfold Intersect_def)
apply(insert Co_ext)
apply(blast)
done




theorem Subseteq_refl: "(ALL p. Subseteq(p,p))"
apply(unfold Subseteq_def)
apply(rule allI,rule allI)
apply(rule impI)
apply(assumption)
done




theorem Subseteq_antisym: "(ALL p q. (Subseteq(p,q) & Subseteq(q,p) --> p=q))"
apply(rule allI,rule allI)
apply(rule impI)
apply(rule Co_ext_rule2)
apply(rule allI)
apply(rule iffI)
apply(erule conjE)
apply(unfold Subseteq_def)
apply(erule_tac x="x" in allE)
apply(drule mp)
apply(assumption)
apply(assumption)
apply(erule conjE)
apply(rotate_tac 2)
apply(erule_tac x="x" in allE)
apply(drule mp)
apply(assumption)
apply(assumption)
done

lemma Subseteq_antisym_rule: "[|Subseteq(p,q);Subseteq(q,p)|]==>p=q"
apply(insert Subseteq_antisym)
apply(auto)
done

theorem Subseteq_trans: "(ALL p q r. (Subseteq(p,q) & Subseteq(q,r) --> Subseteq(p,r)))"
apply(rule allI,rule allI,rule allI)
apply(rule impI)
apply(unfold Subseteq_def)
apply(rule allI)
apply(erule conjE)
apply(erule_tac x="x" in allE)
apply(erule_tac x="x" in allE)
apply(rule impI)
apply(drule mp)
apply(assumption)
apply(drule mp)
apply(assumption)
apply(assumption)
done



lemma Subseteq_trans_rule: "[|Subseteq(p,q); Subseteq(q,r)|] ==> Subseteq(p,r)"
apply(insert Subseteq_trans)
apply(erule_tac x="p" in allE)
apply(erule_tac x="q" in allE)
apply(erule_tac x="r" in allE)
apply(drule_tac P=" Subseteq(p, q)" and Q="Subseteq(q, r)" in conjI)
apply(assumption)
apply(drule mp)
apply(auto)
done


theorem Fp_imp_Pp: "Fp(p,t) ==> Pp(p,t)"
apply(unfold Pp_def)
apply(unfold Fp_def)
apply(insert Co_members)
apply(rotate_tac 1)
apply(erule_tac x="p" in allE)
apply(erule exE,erule exE)
apply(erule conjE,erule conjE)
apply(rule_tac x="x" in exI)
apply(erule_tac x="x" in allE)
apply(auto)
done

theorem Subseteq_and_Fp_imp_Fp: "[|Subseteq(p,q);Fp(q,t)|] ==> Fp(p,t)"
apply(unfold Subseteq_def)
apply(unfold Fp_def)
apply(auto)
done


theorem Subseteq_and_Np_imp_Np: "[|Subseteq(p,q);Np(q,t)|] ==> Np(p,t)"
apply(unfold Subseteq_def)
apply(unfold Np_def)
apply(unfold Pp_def)
apply(auto)
done

theorem Subseteq_and_Pp_imp_Pp: "[|Subseteq(p,q);Pp(p,t)|] ==> Pp(q,t)"
apply(unfold Subseteq_def)
apply(unfold Pp_def)
apply(auto)
done

theorem Np_imp_Do: "Np(p,t) ==> DCo(p,t)"
apply(unfold Np_def)
apply(unfold Pp_def)
apply(unfold DCo_def)
apply(unfold O_def)
apply(auto)
apply(erule_tac x="x" in allE)
apply(auto)
apply(drule P_exists2_rule)
apply(auto)
done

theorem DCo_subseteq: "(ALL p q t. (DCo(p,t) & Subseteq(q,p) --> DCo(q,t)))"
apply(rule allI,rule allI,rule allI)
apply(rule impI)
apply(unfold DCo_def)
apply(rule allI,rule allI)
apply(erule conjE)
apply(erule_tac x="x" in allE)
apply(erule_tac x="y" in allE)
apply(unfold Subseteq_def)
apply(auto)
done

lemma DCo_subseteq_rule: "[|DCo(p,t); Subseteq(q,p)|] ==> DCo(q,t)"
apply(insert DCo_subseteq)
apply(auto)
done



end

lemma Co_ext_rule1:

  p = q ==> ∀x. In(x, p) <-> In(x, q)

lemma Co_ext_rule2:

  x. In(x, p) <-> In(x, q) ==> p = q

theorem Union_unique:

  [| Union(p, q, r1.0); Union(p, q, r2.0) |] ==> r1.0 = r2.0

theorem Intersect_unique:

  [| Intersect(p, q, r1.0); Intersect(p, q, r2.0) |] ==> r1.0 = r2.0

theorem Subseteq_refl:

  p. Subseteq(p, p)

theorem Subseteq_antisym:

  p q. Subseteq(p, q) ∧ Subseteq(q, p) --> p = q

lemma Subseteq_antisym_rule:

  [| Subseteq(p, q); Subseteq(q, p) |] ==> p = q

theorem Subseteq_trans:

  p q r. Subseteq(p, q) ∧ Subseteq(q, r) --> Subseteq(p, r)

lemma Subseteq_trans_rule:

  [| Subseteq(p, q); Subseteq(q, r) |] ==> Subseteq(p, r)

theorem Fp_imp_Pp:

  Fp(p, t) ==> Pp(p, t)

theorem Subseteq_and_Fp_imp_Fp:

  [| Subseteq(p, q); Fp(q, t) |] ==> Fp(p, t)

theorem Subseteq_and_Np_imp_Np:

  [| Subseteq(p, q); Np(q, t) |] ==> Np(p, t)

theorem Subseteq_and_Pp_imp_Pp:

  [| Subseteq(p, q); Pp(p, t) |] ==> Pp(q, t)

theorem Np_imp_Do:

  Np(p, t) ==> DCo(p, t)

theorem DCo_subseteq:

  p q t. DCo(p, t) ∧ Subseteq(q, p) --> DCo(q, t)

lemma DCo_subseteq_rule:

  [| DCo(p, t); Subseteq(q, p) |] ==> DCo(q, t)