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)