Up to index of Isabelle/FOL/BFO
theory PartonomicInclusiontheory PartonomicInclusion imports TNEMO Collections begin consts P1 :: "Co => Co => Ti => o" P2 :: "Co => Co => Ti => o" P12 :: "Co => Co => Ti => o" DP1 :: "Co => Co => Ti => o" DP2 :: "Co => Co => Ti => o" DP12 :: "Co => Co => Ti => o" defs P1_def: "P1(p,q,t) == (ALL x. (In(x,p) --> (EX y. (In(y,q) & P(x,y,t)))))" P2_def: "P2(p,q,t) == (ALL y. (In(y,q) --> (EX x. (In(x,p) & P(x,y,t)))))" P12_def: "P12(p,q,t) == P1(p,q,t) & P2(p,q,t)" DP1_def: "DP1(p,q,t) == P1(p,q,t) & DCo(p,t) & DCo(q,t)" DP2_def: "DP2(p,q,t) == P2(p,q,t) & DCo(p,t) & DCo(q,t)" DP12_def: "DP12(p,q,t) == DP1(p,q,t) & DP2(p,q,t)" (* theorems for partonomic inclusion relations *) theorem P1_imp_Fp_Pp: "P1(p,q,t) ==> (Fp(p,t) & Pp(q,t))" apply(unfold P1_def,unfold Fp_def,unfold Pp_def) apply(rule conjI) apply(rule allI) apply(rule impI) apply(erule_tac x="x" in allE) apply(auto) apply(drule P_exists2_rule) apply(auto) apply(insert Co_members) apply(rotate_tac 1) apply(erule_tac x="p" in allE) apply(erule exE) apply(erule exE) apply(erule_tac x="x" in allE) apply(auto) apply(rule exI) apply(rule conjI) apply(assumption) apply(drule P_exists2_rule) apply(auto) done theorem P2_imp_Pp_Fp: "P2(p,q,t) ==>(Pp(p,t) & Fp(q,t))" apply(unfold P2_def,unfold Fp_def, unfold Pp_def) apply(rule conjI) apply(insert Co_members) apply(rotate_tac 1) apply(erule_tac x="q" in allE) apply(erule exE,erule exE) apply(erule_tac x="y" in allE) apply(erule conjE,erule conjE) apply(drule mp) apply(assumption) apply(erule exE) apply(erule conjE) apply(drule P_exists2_rule) apply(erule conjE) apply(rule_tac x="xa" in exI) apply(rule conjI) apply(assumption,assumption) apply(rule allI) apply(rule impI) apply(erule_tac x="x" in allE) apply(auto) apply(drule P_exists2_rule) apply(auto) done theorem P12_imp_Pp_Fp: "P12(p,q,t) ==> (Fp(p,t) & Fp(q,t))" apply(rule conjI) apply(rule_tac P="Fp(p,t)" and Q="Pp(q,t)" in conjunct1) apply(rule P1_imp_Fp_Pp) apply(unfold P12_def) apply(erule conjE) apply(assumption) apply(rule_tac Q="Fp(q,t)" and P="Pp(p,t)" in conjunct2) apply(rule P2_imp_Pp_Fp) apply(erule conjE) apply(assumption) done theorem Fp_iff_P1: "(ALL p t. (Fp(p,t) <-> P1(p,p,t)))" apply(rule allI,rule allI,rule iffI) apply(unfold P1_def) apply(rule allI) apply(rule impI) apply(rule_tac x="x" in exI) apply(auto) apply(unfold Fp_def) apply(erule_tac x="x" in allE) apply(auto) apply(unfold E_def) apply(auto) apply(erule_tac x="x" in allE) apply(auto) apply(fold E_def) apply(drule P_exists2_rule) apply(auto) done theorem P1_iff_P2: "(ALL p t. (P1(p,p,t) <-> P2(p,p,t)))" apply(auto) apply(unfold P2_def) apply(unfold P1_def) apply(rule allI) apply(rule impI) apply(erule_tac x="y" in allE) apply(drule mp) apply(assumption) apply(erule exE) apply(erule conjE) apply(rule_tac x="y" in exI) apply(rule conjI) apply(assumption) apply(drule P_exists2_rule) apply(erule conjE) apply(unfold E_def) apply(assumption) apply(rule allI) apply(rule impI) apply(erule_tac x="x" in allE) apply(drule mp) apply(assumption) apply(erule exE) apply(erule conjE) apply(rule_tac x="x" in exI) apply(auto) apply(drule P_exists2_rule) apply(unfold E_def) apply(auto) done theorem P2_iff_P12: "(ALL p t. (P2(p,p,t) <-> P12(p,p,t)))" apply(auto) apply(unfold P12_def,unfold P1_def,unfold P2_def) apply(auto) apply(erule_tac x="x" in allE) apply(auto) apply(rule_tac x="x" in exI) apply(auto) apply(drule P_exists2_rule) apply(unfold E_def) apply(auto) done theorem P1_trans: "[|P1(p,q,t);P1(q,r,t)|] ==> P1(p,r,t)" apply(unfold P1_def) apply(rule allI) apply(rule impI) apply(erule_tac x="x" in allE) apply(drule mp) apply(assumption) apply(erule exE) apply(erule conjE) apply(erule_tac x="y" in allE) apply(drule mp) apply(assumption) apply(erule exE) apply(erule conjE) apply(rule_tac x="ya" in exI) apply(rule conjI) apply(assumption) apply(drule_tac x="x" and y="y" and z="ya" in P_trans_rule) apply(auto) done theorem P2_trans: "[|P2(p,q,t);P2(q,r,t)|] ==> P2(p,r,t)" apply(unfold P2_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(auto) apply(drule_tac x="xa" and y="x" and z="y" in P_trans_rule) apply(auto) done theorem P12_trans: "[|P12(p,q,t);P12(q,r,t)|] ==> P12(p,r,t)" apply(unfold P12_def) apply(auto) apply(drule P1_trans) apply(auto) apply(drule P2_trans) apply(auto) done theorem DP1_trans: "[|DP1(p,q,t);DP1(q,r,t)|] ==> DP1(p,r,t)" apply(unfold DP1_def) apply(auto) apply(drule P1_trans) apply(auto) done theorem DP2_trans: "[|DP2(p,q,t);DP2(q,r,t)|] ==> DP2(p,r,t)" apply(unfold DP2_def) apply(auto) apply(drule P2_trans) apply(auto) done theorem DP12_trans: "[|DP12(p,q,t);DP12(q,r,t)|] ==> DP12(p,r,t)" apply(unfold DP12_def) apply(auto) apply(drule DP1_trans) apply(auto) apply(rule DP2_trans) apply(auto) done (* Sub-collections and partonomic inclusion. *) theorem Subseteq_and_P1_imp_P1_1: "[|Subseteq(r,p);P1(p,q,t)|] ==> P1(r,q,t)" apply(unfold Subseteq_def, unfold P1_def) apply(clarify) apply(erule_tac x="x" in allE) apply(clarify) apply(erule_tac x="x" in allE) apply(clarify) done theorem Subseteq_and_P1_imp_P1_2: "[|Subseteq(q,r);P1(p,q,t)|] ==> P1(p,r,t)" apply(unfold Subseteq_def, unfold P1_def) apply(clarify) apply(rotate_tac 1) apply(erule_tac x="x" in allE) apply(clarify) apply(erule_tac x="y" in allE) apply(clarify) apply(rule_tac x="y" in exI) apply(clarify) done theorem Subseteq_and_P2_imp_P2_1: "[|Subseteq(r,q);P2(p,q,t)|] ==> P2(p,r,t)" apply(unfold Subseteq_def, unfold P2_def) apply(clarify) apply(erule_tac x="y" in allE) apply(clarify) apply(erule_tac x="y" in allE) apply(clarify) done theorem Subseteq_and_P2_imp_P2_2: "[|Subseteq(p,r);P2(p,q,t)|] ==> P2(r,q,t)" apply(unfold Subseteq_def, unfold P2_def) apply(clarify) apply(rotate_tac 1) apply(erule_tac x="y" in allE) apply(clarify) apply(erule_tac x="x" in allE) apply(clarify) apply(rule_tac x="x" in exI) apply(clarify) done theorem Subseteq_and_P12_imp_P1_1: "[|Subseteq(r,p);P12(p,q,t)|] ==> P1(r,q,t)" apply(unfold P12_def) apply(clarify) apply(drule Subseteq_and_P1_imp_P1_1) apply(auto) done theorem Subseteq_and_P12_imp_P2_2: "[|Subseteq(p,r);P12(p,q,t)|] ==> P2(r,q,t)" apply(unfold P12_def) apply(clarify) apply(drule Subseteq_and_P2_imp_P2_2) apply(auto) done theorem Subseteq_and_P12_imp_P2_1: "[|Subseteq(r,q);P12(p,q,t)|] ==> P2(p,r,t)" apply(unfold P12_def) apply(clarify) apply(drule Subseteq_and_P2_imp_P2_1) apply(auto) done theorem Subseteq_and_P12_imp_P1_2: "[|Subseteq(q,r);P12(p,q,t)|] ==> P1(p,r,t)" apply(unfold P12_def) apply(clarify) apply(drule Subseteq_and_P1_imp_P1_2) apply(auto) done theorem Subseteq_and_DP1_imp_DP1: "[|Subseteq(r,p);DP1(p,q,t)|] ==> DP1(r,q,t)" apply(unfold DP1_def) apply(clarify) apply(frule Subseteq_and_P1_imp_P1_1) apply(auto) apply(drule_tac p="p" and q="r" in DCo_subseteq_rule) apply(auto) done theorem Subseteq_and_DP1_imp_P1: "[|Subseteq(q,r);DP1(p,q,t)|] ==> P1(p,r,t)" apply(unfold DP1_def) apply(clarify) apply(frule Subseteq_and_P1_imp_P1_2) apply(auto) done theorem Subseteq_and_DP2_imp_DP2: "[|Subseteq(r,q);DP2(p,q,t)|] ==> DP2(p,r,t)" apply(unfold DP2_def) apply(clarify) apply(frule Subseteq_and_P2_imp_P2_1) apply(auto) apply(drule_tac p="q" and q="r" in DCo_subseteq_rule) apply(auto) done theorem Subseteq_and_DP2_imp_P2: "[|Subseteq(p,r);DP2(p,q,t)|] ==> P2(r,q,t)" apply(unfold DP2_def) apply(clarify) apply(frule Subseteq_and_P2_imp_P2_2) apply(auto) done theorem Subseteq_and_DP12_imp_DP1: "[|Subseteq(r,p);DP12(p,q,t)|] ==> DP1(r,q,t)" apply(unfold DP12_def) apply(clarify) apply(rule Subseteq_and_DP1_imp_DP1) apply(auto) done theorem Subseteq_and_DP12_imp_P2: "[|Subseteq(p,r);DP12(p,q,t)|] ==> P2(r,q,t)" apply(unfold DP12_def) apply(clarify) apply(rule Subseteq_and_DP2_imp_P2) apply(auto) done theorem Subseteq_and_DP12_imp_DP2: "[|Subseteq(r,q);DP12(p,q,t)|] ==> DP2(p,r,t)" apply(unfold DP12_def) apply(clarify) apply(rule Subseteq_and_DP2_imp_DP2) apply(auto) done theorem Subseteq_and_DP12_imp_P1: "[|Subseteq(q,r);DP12(p,q,t)|] ==> P1(p,r,t)" apply(unfold DP12_def) apply(clarify) apply(rule Subseteq_and_DP1_imp_P1) apply(auto) done end
theorem P1_imp_Fp_Pp:
P1(p, q, t) ==> Fp(p, t) ∧ Pp(q, t)
theorem P2_imp_Pp_Fp:
P2(p, q, t) ==> Pp(p, t) ∧ Fp(q, t)
theorem P12_imp_Pp_Fp:
P12(p, q, t) ==> Fp(p, t) ∧ Fp(q, t)
theorem Fp_iff_P1:
∀p t. Fp(p, t) <-> P1(p, p, t)
theorem P1_iff_P2:
∀p t. P1(p, p, t) <-> P2(p, p, t)
theorem P2_iff_P12:
∀p t. P2(p, p, t) <-> P12(p, p, t)
theorem P1_trans:
[| P1(p, q, t); P1(q, r, t) |] ==> P1(p, r, t)
theorem P2_trans:
[| P2(p, q, t); P2(q, r, t) |] ==> P2(p, r, t)
theorem P12_trans:
[| P12(p, q, t); P12(q, r, t) |] ==> P12(p, r, t)
theorem DP1_trans:
[| DP1(p, q, t); DP1(q, r, t) |] ==> DP1(p, r, t)
theorem DP2_trans:
[| DP2(p, q, t); DP2(q, r, t) |] ==> DP2(p, r, t)
theorem DP12_trans:
[| DP12(p, q, t); DP12(q, r, t) |] ==> DP12(p, r, t)
theorem Subseteq_and_P1_imp_P1_1:
[| Subseteq(r, p); P1(p, q, t) |] ==> P1(r, q, t)
theorem Subseteq_and_P1_imp_P1_2:
[| Subseteq(q, r); P1(p, q, t) |] ==> P1(p, r, t)
theorem Subseteq_and_P2_imp_P2_1:
[| Subseteq(r, q); P2(p, q, t) |] ==> P2(p, r, t)
theorem Subseteq_and_P2_imp_P2_2:
[| Subseteq(p, r); P2(p, q, t) |] ==> P2(r, q, t)
theorem Subseteq_and_P12_imp_P1_1:
[| Subseteq(r, p); P12(p, q, t) |] ==> P1(r, q, t)
theorem Subseteq_and_P12_imp_P2_2:
[| Subseteq(p, r); P12(p, q, t) |] ==> P2(r, q, t)
theorem Subseteq_and_P12_imp_P2_1:
[| Subseteq(r, q); P12(p, q, t) |] ==> P2(p, r, t)
theorem Subseteq_and_P12_imp_P1_2:
[| Subseteq(q, r); P12(p, q, t) |] ==> P1(p, r, t)
theorem Subseteq_and_DP1_imp_DP1:
[| Subseteq(r, p); DP1(p, q, t) |] ==> DP1(r, q, t)
theorem Subseteq_and_DP1_imp_P1:
[| Subseteq(q, r); DP1(p, q, t) |] ==> P1(p, r, t)
theorem Subseteq_and_DP2_imp_DP2:
[| Subseteq(r, q); DP2(p, q, t) |] ==> DP2(p, r, t)
theorem Subseteq_and_DP2_imp_P2:
[| Subseteq(p, r); DP2(p, q, t) |] ==> P2(r, q, t)
theorem Subseteq_and_DP12_imp_DP1:
[| Subseteq(r, p); DP12(p, q, t) |] ==> DP1(r, q, t)
theorem Subseteq_and_DP12_imp_P2:
[| Subseteq(p, r); DP12(p, q, t) |] ==> P2(r, q, t)
theorem Subseteq_and_DP12_imp_DP2:
[| Subseteq(r, q); DP12(p, q, t) |] ==> DP2(p, r, t)
theorem Subseteq_and_DP12_imp_P1:
[| Subseteq(q, r); DP12(p, q, t) |] ==> P1(p, r, t)