Theory UniversalParthood

Up to index of Isabelle/FOL/BFO

theory UniversalParthood
imports ExtensionsOfUniversals PartonomicInclusion
begin

theory UniversalParthood

imports ExtensionsOfUniversals PartonomicInclusion

begin

consts


UPt1 :: "Un => Un => Ti => o"
UPt2 :: "Un => Un => Ti => o"
UPt12 :: "Un => Un => Ti => o"

UP1 :: "Un => Un => o"
UP2 :: "Un => Un  => o"
UP12 :: "Un => Un  => o"

defs

UPt1_def: "UPt1(c,d,t) == (ALL x. (Inst(x,c,t) --> (EX y. (Inst(y,d,t) & P(x,y,t)))))"
UPt2_def: "UPt2(c,d,t) == (ALL y. (Inst(y,d,t) --> (EX x. (Inst(x,c,t) & P(x,y,t)))))"
UPt12_def: "UPt12(c,d,t) == UPt1(c,d,t) & UPt2(c,d,t)"

UP1_def: "UP1(c,d) == (ALL t. UPt1(c,d,t))"
UP2_def: "UP2(c,d) == (ALL t. UPt2(c,d,t))"
UP12_def: "UP12(c,d) == (ALL t. UPt12(c,d,t))"


(* theorems about universal parthood *)

theorem ExtCo_and_ExtCo: "[|ExtCo(p,c,t);ExtCo(q,d,t)|] ==> (P1(p,q,t) <-> UPt1(c,d,t))"
apply(unfold iff_def)
apply(unfold ExtCo_def)
apply(unfold P1_def)
apply(unfold UPt1_def)
apply(auto)
done


theorem ExtOb_and_ExtOb: "[|ExtOb(x,c,t);ExtOb(y,d,t)|] ==> (P(x,y,t) <-> UPt1(c,d,t))"
apply(unfold iff_def)
apply(unfold ExtOb_def)
apply(unfold UPt1_def)
apply(rule conjI)
apply(rule impI)
apply(rule allI)
apply(rule impI)
apply(erule conjE)
apply(erule conjE)
apply(rule_tac x="y" in exI)
apply(rule conjI)
apply(assumption)
apply(erule_tac x="xa" in allE)
apply(drule mp)
apply(assumption)
apply(erule_tac a="x" and b="xa" in subst)
apply(assumption)
apply(rule impI)
apply(erule_tac x="x" in allE)
apply(erule conjE)
apply(erule conjE)
apply(drule mp)
apply(assumption)
apply(erule exE)
apply(erule conjE)
apply(rotate_tac 3)
apply(erule_tac x="ya" in allE)
apply(drule mp)
apply(assumption)
apply(drule_tac a="y" and b="ya" in sym)
apply(erule_tac a="ya" and b="y" in subst)
apply(assumption)
done


theorem ExtCo_and_ExtOb: "[|ExtCo(p,c,t);ExtOb(x,d,t)|] ==> ((EX y. (Inst(y,c,t) & P(y,x,t)))) <-> UPt2(c,d,t)"
apply(unfold iff_def)
apply(unfold UPt2_def)
apply(unfold ExtCo_def)
apply(unfold ExtOb_def)
apply(auto)
done


theorem ExtOb_and_ExtCo: "[|ExtOb(x,c,t);ExtCo(p,d,t)|] ==> ((EX y. (Inst(y,d,t) & P(x,y,t)))) <-> UPt1(c,d,t)"
apply(unfold iff_def)
apply(unfold UPt1_def)
apply(unfold ExtOb_def)
apply(unfold ExtCo_def)
apply(auto)
done


theorem UPt1_refl: "(ALL c t. UPt1(c,c,t))"
apply(unfold UPt1_def)
apply(auto)
apply(rule_tac x="x" in exI)
apply(auto)
apply(insert Inst_E)
apply(unfold E_def)
apply(auto)
done

theorem UPt2_refl: "(ALL c t. UPt2(c,c,t))"
apply(unfold UPt2_def)
apply(auto)
apply(rule_tac x="y" in exI)
apply(auto)
apply(insert Inst_E)
apply(unfold E_def)
apply(auto)
done

theorem UPt12_refl: "(ALL c t. UPt12(c,c,t))"
apply(unfold UPt12_def)
apply(insert UPt1_refl)
apply(insert UPt2_refl)
apply(auto)
done


theorem UPt1_trans: "[|UPt1(c,d,t);UPt1(d,e,t)|]==> UPt1(c,e,t)"
apply(unfold UPt1_def)
apply(auto)
apply(erule_tac x="x" in allE)
apply(auto)
apply(erule_tac x="y" in allE)
apply(auto)
apply(rule_tac x="ya" in exI)
apply(drule_tac x="x" and y="y" and z="ya" in P_trans_rule)
apply(auto)
done

theorem UPt2_trans: "[|UPt2(c,d,t);UPt2(d,e,t)|]==> UPt2(c,e,t)"
apply(unfold UPt2_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(drule_tac x="xa" and y="x" and z="y" in P_trans_rule)
apply(auto)
done


theorem UPt12_trans: "[|UPt12(c,d,t);UPt12(d,e,t)|]==> UPt12(c,e,t)"
apply(unfold UPt12_def)
apply(auto)
apply(drule UPt1_trans)
apply(auto)
apply(drule UPt2_trans)
apply(auto)
done


theorem UP1_iff: "(ALL c d. (UP1(c,d) <-> (ALL t x. (Inst(x,c,t) --> (EX y. (Inst(y,d,t) & P(x,y,t)))))))" 
apply(unfold UP1_def,unfold UPt1_def)
apply(auto)
done

theorem UP2_iff: "(ALL c d. (UP2(c,d) <-> (ALL t y. (Inst(y,d,t) --> (EX x. (Inst(x,c,t) & P(x,y,t)))))))" 
apply(unfold UP2_def,unfold UPt2_def)
apply(auto)
done

theorem UP1_refl: "(ALL c. UP1(c,c))"
apply(unfold UP1_def)
apply(insert UPt1_refl)
apply(auto)
done

theorem UP2_refl: "(ALL c. UP2(c,c))"
apply(unfold UP2_def)
apply(insert UPt2_refl)
apply(auto)
done

theorem UP12_refl: "(ALL c. UP12(c,c))"
apply(unfold UP12_def)
apply(insert UPt12_refl)
apply(auto)
done

theorem UP1_trans: "[|UP1(c,d);UP1(d,e)|]==> UP1(c,e)"
apply(unfold UP1_def)
apply(auto)
apply(drule_tac x="t" in allE)
apply(drule_tac x="t" in allE)
apply(drule UPt1_trans)
apply(auto)
done

theorem UP2_trans: "[|UP2(c,d);UP2(d,e)|]==> UP2(c,e)"
apply(unfold UP2_def)
apply(auto)
apply(drule_tac x="t" in allE)
apply(drule_tac x="t" in allE)
apply(drule UPt2_trans)
apply(auto)
done

theorem UP12_trans: "[|UP12(c,d);UP12(d,e)|]==> UP12(c,e)"
apply(unfold UP12_def)
apply(auto)
apply(drule_tac x="t" in allE)
apply(drule_tac x="t" in allE)
apply(drule UPt12_trans)
apply(auto)
done



theorem UP12_impl_UP1_and_UP2: "UP12(c,d) ==> (UP1(c,d) & UP2(c,d))"
apply(unfold UP12_def,unfold UP1_def,unfold UP2_def)
apply(rule conjI)
apply(rule allI)
apply(erule_tac x="t" in allE)
apply(unfold UPt12_def)
apply(auto)
done


theorem IsA_and_UP1_impl_UP1_1: "[|IsA(e,c);UP1(c,d)|] ==> UP1(e,d)"
apply(unfold UP1_def,unfold UPt1_def)
apply(drule_tac c="e" and d="c" in Inst_IsA_rule)
apply(auto)
done

theorem IsA_and_UP1_impl_UP1_2: "[|IsA(d,e);UP1(c,d)|] ==> UP1(c,e)"
apply(unfold UP1_def,unfold UPt1_def)
apply(drule_tac c="d" and d="e" in Inst_IsA_rule)
apply(auto)
apply(erule_tac x="t" in allE)
apply(rotate_tac 2)
apply(erule_tac x="x" in allE)
apply(auto)
done

theorem IsA_and_UP2_impl_UP2_1: "[|IsA(e,d);UP2(c,d)|] ==> UP2(c,e)"
apply(unfold UP2_def,unfold UPt2_def)
apply(drule_tac c="e" and d="d" in Inst_IsA_rule)
apply(auto)
done

theorem IsA_and_UP2_impl_UP2_2: "[|IsA(c,e);UP2(c,d)|] ==> UP2(e,d)"
apply(unfold UP2_def,unfold UPt2_def)
apply(drule_tac c="c" and d="e" in Inst_IsA_rule)
apply(auto)
apply(erule_tac x="t" in allE)
apply(rotate_tac 2)
apply(erule_tac x="y" in allE)
apply(auto)
done



theorem IsA_and_UP12_impl_UP1_1: "[|IsA(e,c);UP12(c,d)|] ==> UP1(e,d)"
apply(drule UP12_impl_UP1_and_UP2)
apply(erule conjE)
apply(drule IsA_and_UP1_impl_UP1_1)
apply(auto)
done

theorem IsA_and_UP12_impl_UP2_2: "[|IsA(c,e);UP12(c,d)|] ==> UP2(e,d)"
apply(drule UP12_impl_UP1_and_UP2)
apply(erule conjE)
apply(drule IsA_and_UP2_impl_UP2_2)
apply(auto)
done

theorem IsA_and_UP12_impl_UP2_1: "[|IsA(e,d);UP12(c,d)|] ==> UP2(c,e)"
apply(drule UP12_impl_UP1_and_UP2)
apply(erule conjE)
apply(drule IsA_and_UP2_impl_UP2_1)
apply(auto)
done


theorem IsA_and_UP12_impl_UP1_2: "[|IsA(d,e);UP12(c,d)|] ==> UP1(c,e)"
apply(drule UP12_impl_UP1_and_UP2)
apply(erule conjE)
apply(drule IsA_and_UP1_impl_UP1_2)
apply(auto)
done

theorem IsA_imp_UP1: "IsA(c,d) ==> UP1(c,d)"
apply(unfold UP1_def)
apply(safe)
apply(unfold UPt1_def)
apply(safe)
apply(drule Inst_IsA_rule [of c d])
apply(erule_tac x="x" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(rule_tac x="x" in exI)
apply(insert Inst_E)
apply(insert P_refl)
apply(auto)
done

end

theorem ExtCo_and_ExtCo:

  [| ExtCo(p, c, t); ExtCo(q, d, t) |] ==> P1(p, q, t) <-> UPt1(c, d, t)

theorem ExtOb_and_ExtOb:

  [| ExtOb(x, c, t); ExtOb(y, d, t) |] ==> P(x, y, t) <-> UPt1(c, d, t)

theorem ExtCo_and_ExtOb:

  [| ExtCo(p, c, t); ExtOb(x, d, t) |]
  ==> (∃y. Inst(y, c, t) ∧ P(y, x, t)) <-> UPt2(c, d, t)

theorem ExtOb_and_ExtCo:

  [| ExtOb(x, c, t); ExtCo(p, d, t) |]
  ==> (∃y. Inst(y, d, t) ∧ P(x, y, t)) <-> UPt1(c, d, t)

theorem UPt1_refl:

  c t. UPt1(c, c, t)

theorem UPt2_refl:

  c t. UPt2(c, c, t)

theorem UPt12_refl:

  c t. UPt12(c, c, t)

theorem UPt1_trans:

  [| UPt1(c, d, t); UPt1(d, e, t) |] ==> UPt1(c, e, t)

theorem UPt2_trans:

  [| UPt2(c, d, t); UPt2(d, e, t) |] ==> UPt2(c, e, t)

theorem UPt12_trans:

  [| UPt12(c, d, t); UPt12(d, e, t) |] ==> UPt12(c, e, t)

theorem UP1_iff:

  c d. UP1(c, d) <-> (∀t x. Inst(x, c, t) --> (∃y. Inst(y, d, t) ∧ P(x, y, t)))

theorem UP2_iff:

  c d. UP2(c, d) <-> (∀t y. Inst(y, d, t) --> (∃x. Inst(x, c, t) ∧ P(x, y, t)))

theorem UP1_refl:

  c. UP1(c, c)

theorem UP2_refl:

  c. UP2(c, c)

theorem UP12_refl:

  c. UP12(c, c)

theorem UP1_trans:

  [| UP1(c, d); UP1(d, e) |] ==> UP1(c, e)

theorem UP2_trans:

  [| UP2(c, d); UP2(d, e) |] ==> UP2(c, e)

theorem UP12_trans:

  [| UP12(c, d); UP12(d, e) |] ==> UP12(c, e)

theorem UP12_impl_UP1_and_UP2:

  UP12(c, d) ==> UP1(c, d) ∧ UP2(c, d)

theorem IsA_and_UP1_impl_UP1_1:

  [| IsA(e, c); UP1(c, d) |] ==> UP1(e, d)

theorem IsA_and_UP1_impl_UP1_2:

  [| IsA(d, e); UP1(c, d) |] ==> UP1(c, e)

theorem IsA_and_UP2_impl_UP2_1:

  [| IsA(e, d); UP2(c, d) |] ==> UP2(c, e)

theorem IsA_and_UP2_impl_UP2_2:

  [| IsA(c, e); UP2(c, d) |] ==> UP2(e, d)

theorem IsA_and_UP12_impl_UP1_1:

  [| IsA(e, c); UP12(c, d) |] ==> UP1(e, d)

theorem IsA_and_UP12_impl_UP2_2:

  [| IsA(c, e); UP12(c, d) |] ==> UP2(e, d)

theorem IsA_and_UP12_impl_UP2_1:

  [| IsA(e, d); UP12(c, d) |] ==> UP2(c, e)

theorem IsA_and_UP12_impl_UP1_2:

  [| IsA(d, e); UP12(c, d) |] ==> UP1(c, e)

theorem IsA_imp_UP1:

  IsA(c, d) ==> UP1(c, d)