Theory PartonomicInclusion

Up to index of Isabelle/FOL/BFO

theory PartonomicInclusion
imports Collections
begin

theory 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)