Theory TMTL

Up to index of Isabelle/FOL/BFO

theory TMTL
imports TORL RBG
begin

theory TMTL

imports TNEMO TORL RBG

begin

consts

C :: "Ob => Ob => Ti => o"
EC :: "Ob => Ob => Ti => o"
DC :: "Ob => Ob => Ti => o"
pC :: "Ob => Ob => o"
pEC :: "Ob => Ob => o"
pDC :: "Ob => Ob => o"


defs

C_def: "C(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & CGR(a,b)))"
EC_def: "EC(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & ECR(a,b)))"
DC_def: "DC(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & DCR(a,b)))"
pC_def: "pC(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> C(x,y,t)))"
pEC_def: "pEC(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> EC(x,y,t)))"
pDC_def: "pDC(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> DC(x,y,t)))"
 

theorem E_imp_C: "E(x,t) ==> C(x,x,t)"
apply(unfold C_def)
apply(drule L_exists1)
apply(erule exE)
apply(rule_tac x="a" in exI)
apply(rule_tac x="a" in exI)
apply(insert CGR_refl)
apply(auto)
done

 
theorem C_sym: "C(x,y,t) ==> C(y,x,t)"
apply(unfold C_def)
apply(clarify)
apply(rule_tac x="b" in exI)
apply(rule_tac x="a" in exI)
apply(drule CGR_sym)
apply(auto)
done


theorem C_imp_E_and_E: "C(x,y,t) ==> (E(x,t) & E(y,t))"
apply(unfold C_def)
apply(insert L_exists)
apply(auto)
done

theorem P_imp_C_imp_C: "P(x,y,t) ==> (ALL z. (C(z,x,t) --> C(z,y,t)))"
apply(unfold C_def)
apply(safe)
apply(frule P_exists2_rule)
apply(clarify)
apply(drule_tac x="y" and t="t" in L_exists1)
apply(erule exE)
apply(rule_tac x="a" in exI)
apply(rule_tac x="aa" in exI)
apply(auto)
apply(drule_tac x="x" and a="b" and y="y" and b="aa" and t="t" in L_P_PR_rule) 
apply(safe)
apply(drule_tac a="b" and b="aa" in PR_imp_CGR_imp_CGR)
apply(erule_tac x="a" in allE)
apply(auto)
done

theorem L_and_L_and_C_imp_CGR: "[|L(x,a,t);L(y,b,t);CGR(a,b)|] ==> C(x,y,t)"
apply(unfold C_def)
apply(auto)
done


theorem EC_imp_C_and_notO: "EC(x,y,t) ==> (C(x,y,t) & ~O(x,y,t))"
apply(unfold EC_def,unfold C_def,unfold O_def,unfold ECR_def,unfold OR_def)
apply(clarify)
apply(auto)
apply(drule P_imp_L)
apply(drule P_imp_L)
apply(clarify)
apply(drule_tac x="z" and a="aa" and b="ab" and t="t" in L_unique)
apply(clarify)
apply(drule_tac x="y" and a="b" and b="ba" and t="t" in L_unique)
apply(clarify)
apply(drule_tac x="x" and a="a" and b="bb" and t="t" in L_unique)
apply(clarify)
apply(auto)
done


(*
cannot be a theorem: an object in a cavity in another object: c=both are connected and do not ocerlap but need not be externally connected
theorem C_and_not_O_imp_EC: "[|C(x,y,t);~O(x,y,t)|] ==> EC(x,y,t)"
apply(unfold C_def,unfold EC_def,unfold O_def,unfold ECR_def)
apply(auto)
apply(erule_tac x="x" in allE)
apply(rule_tac x="a" in exI)
apply(safe)
apply(rule_tac x="b" in exI)
apply(auto)
apply(insert L_exists)
apply(erule_tac x="x" in allE)
apply(erule_tac x="t" in allE)
apply(frule_tac x="a" in exI)
apply(auto)
apply(unfold E_def)
apply(auto)
apply(rule_tac x="b" in exI)
apply(auto)
*)


theorem EC_irrefl: "(ALL x t. (~EC(x,x,t)))"
apply(unfold EC_def)
apply(auto)
apply(drule L_unique)
apply(assumption)
apply(insert ECR_irrefl)
apply(auto)
done

theorem EC_sym: "EC(x,y,t) ==> EC(y,x,t)"
apply(unfold EC_def)
apply(insert ECR_sym)
apply(auto)
done


theorem DC_irrefl: "(ALL x t. (~DC(x,x,t)))"
apply(unfold DC_def)
apply(auto)
apply(drule L_unique)
apply(assumption)
apply(insert DCR_irrefl)
apply(auto)
done

theorem DC_sym: "DC(x,y,t) ==> DC(y,x,t)"
apply(unfold DC_def)
apply(insert DCR_sym)
apply(auto)
done

theorem DC_imp_notC: "DC(x,y,t) ==> ~C(x,y,t)"
apply(unfold C_def,unfold DC_def,unfold DCR_def)
apply(clarify)
apply(drule_tac x="x" and a="a" and b="aa" and t="t" in L_unique)
apply(assumption)
apply(drule_tac x="y" and a="b" and b="ba" and t="t" in L_unique)
apply(auto)
done


theorem P_imp_C: "P(x,y,t) ==> C(x,y,t)"
apply(unfold C_def)
apply(drule P_imp_L)
apply(clarify)
apply(rule_tac x="a" in exI)
apply(rule_tac x="b" in exI)
apply(drule PR_imp_CGR)
apply(auto)
done

theorem O_imp_C: "O(x,y,t) ==> C(x,y,t)"
apply(unfold O_def)
apply(clarify)
apply(drule_tac x="z" and y="x" and t="t" in P_imp_L)
apply(drule_tac x="z" and y="y" and t="t" in P_imp_L)
apply(safe)
apply(frule_tac x="z" and a="a" and b="aa" and t="t" in L_unique)
apply(safe)
apply(unfold C_def)
apply(rule_tac x="b" in exI)
apply(rule_tac x="ba" in exI)
apply(safe)
apply(rule_tac a="b" and b="ba" in OR_imp_CGR)
apply(unfold OR_def)
apply(auto)
done

theorem P_and_C_imp_C: "[|P(x,y,t);C(x,z,t)|] ==> C(y,z,t)"
apply(drule_tac x="x" and y="y" and t="t" in P_imp_C_imp_C)
apply(erule_tac x="z" in allE)
apply(insert C_sym)
apply(auto)
done

theorem PCoin_imp_C: "PCoin(x,y,t) ==> C(x,y,t)"
apply(unfold PCoin_def,unfold C_def)
apply(clarify)
apply(rule_tac x="a" in exI)
apply(rule_tac x="b" in exI)
apply(drule OR_imp_CGR)
apply(auto)
done

theorem LocIn_imp_C: "LocIn(x,y,t) ==> C(x,y,t)"
apply(insert LocIn_imp_PCoin,insert PCoin_imp_C)
apply(auto)
done


theorem PCoin_or_EC_or_notC: "(ALL x y t. (PCoin(x,y,t) | EC(x,y,t) | ~C(x,y,t)))"
apply(unfold PCoin_def,unfold EC_def,unfold C_def)
apply(auto)
apply(erule_tac x="a" in allE)
apply(erule_tac x="a" in allE)
apply(auto)
apply(erule_tac x="b" in allE)
apply(auto)
apply(erule_tac x="b" in allE)
apply(auto)
apply(insert ECR_def)
apply(auto)
done

theorem C_and_LocIn_imp_C: "[|C(x,y,t);LocIn(y,z,t)|] ==> C(x,z,t)"
apply(unfold C_def,unfold LocIn_def)
apply(clarify)
apply(rule_tac x="a" in exI)
apply(rule_tac x="ba" in exI)
apply(auto)
apply(frule_tac x="y" and a="aa" and b="b" and t="t" in L_unique)
apply(clarify)
apply(insert CGR_sym)
apply(insert PR_and_CGR_imp_CGR)
apply(auto)
done


theorem pEC_irrefl: "ALL x. ~pEC(x,x)"
apply(unfold pEC_def)
apply(insert ECR_irrefl)
apply(unfold EC_def)
apply(unfold ECR_def)
apply(auto)
apply(insert P_exists1)
apply(erule_tac x="x" in allE)
apply(erule exE)
apply(rule_tac x="t" in exI)
apply(safe)
apply(drule_tac x="x" and a="a" and b="b"  and t="t" in L_unique)
apply(auto)
done

theorem pEC_sym: "pEC(x,y) ==> pEC(y,x)"
apply(unfold pEC_def)
apply(insert EC_sym)
apply(auto)
done


theorem pDC_irrefl: "ALL x. ~pDC(x,x)"
apply(unfold pDC_def)
apply(insert DC_irrefl)
apply(safe)
apply(insert P_exists1)
apply(rotate_tac 2)
apply(erule_tac x="x" in allE)
apply(erule exE)
apply(erule_tac x="x" in allE)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
done

theorem pDC_sym: "pDC(x,y) ==> pDC(y,x)"
apply(unfold pDC_def)
apply(insert DC_sym)
apply(auto)
done

theorem pDC_imp_notC: "pDC(x,y) ==> (ALL t. ~ C(x,y,t))"
apply(unfold pDC_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(frule_tac x="x" and y="y" and t="t" in C_imp_E_and_E)
apply(unfold DC_def)
apply(auto)
apply(unfold C_def,unfold DCR_def)
apply(clarify)
apply(drule_tac x="x" and a="a" and b="aa" and t="t" in L_unique)
apply(assumption)
apply(drule_tac x="y" and a="b" and b="ba" and t="t" in L_unique)
apply(auto)
done


theorem pDC_imp_not_pC: "pDC(x,y) ==>  ~ pC(x,y)"
apply(unfold pDC_def,unfold pC_def)
apply(safe)
apply(insert  P_exists1)
apply(erule_tac x="x" in allE)
apply(clarify)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(insert DC_imp_notC)
apply(auto)
done

theorem pP_imp_pC: "pP(x,y) ==> pC(x,y)"
apply(unfold pP_def,unfold pC_def)
apply(insert P_imp_C)
apply(auto)
done

theorem pPCoin_imp_pC: "pPCoin(x,y) ==> pC(x,y)"
apply(unfold pPCoin_def,unfold pC_def)
apply(insert PCoin_imp_C)
apply(auto)
done

(*
theorem pPCoin_or_pEC_or_notpC: "(ALL x y. (pPCoin(x,y) | pEC(x,y) | ~pC(x,y)))"
apply(unfold pPCoin_def,unfold pEC_def,unfold pC_def)
this is clearly NOT a theorem
*)


theorem pC_and_pLocIn_imp_pC: "[|pC(x,y);pLocIn(y,z)|] ==> pC(x,z)"
apply(unfold pC_def,unfold pLocIn_def)
apply(safe)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in C_and_LocIn_imp_C)
apply(auto)
apply(insert C_imp_E_and_E)
apply(auto)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in C_and_LocIn_imp_C)
apply(insert LocIn_imp_E_and_E)
apply(auto)
done


theorem pEC_imp_pC_and_notpO: "pEC(x,y) ==> (pC(x,y) & ~pO(x,y))"
apply(unfold pEC_def,unfold pC_def,unfold pO_def)
apply(insert EC_imp_C_and_notO)
apply(safe)
apply(erule_tac x="t" in allE)
apply(force)
apply(force)
apply(insert P_exists1)
apply(erule_tac x="x" in allE)
apply(erule exE)
apply(auto)
done



theorem pP_imp_pC_imp_pC: "pP(x,y) ==> (ALL z. (pC(z,x) --> pC(z,y)))"
apply(unfold pP_def,unfold pC_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="z" and y="x" and t="t" in C_imp_E_and_E)
apply(safe)
apply(drule P_imp_C_imp_C)
apply(drule E_imp_C)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule P_exists2_rule)
apply(auto)
apply(drule P_imp_C_imp_C)
apply(drule E_imp_C)
apply(auto)
done


theorem pC_sym: "pC(x,y) ==> pC(y,x)"
apply(unfold pC_def)
apply(safe)
apply(rule_tac x="x" and y="y" in C_sym)
apply(auto)
apply(rule_tac x="x" and y="y" in C_sym)
apply(auto)
done

theorem pO_imp_pC: "pO(x,y) ==> pC(x,y)"
apply(unfold pO_def,unfold pC_def)
apply(insert O_imp_C)
apply(auto)
done

theorem pP_and_pC_imp_pC: "[|pP(x,y);pC(x,z)|] ==> pC(y,z)"
apply(unfold pP_def,unfold pC_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="y" and t="t" in P_exists2_rule)
apply(safe)
apply(rule_tac y="y" and z="z" and t="t" in P_and_C_imp_C)
apply(auto)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule_tac x="x" and y="z" and t="t" in C_imp_E_and_E)
apply(safe)
apply(rule_tac y="y" and z="z" and t="t" in P_and_C_imp_C)
apply(auto)
done

end

theorem E_imp_C:

  E(x, t) ==> C(x, x, t)

theorem C_sym:

  C(x, y, t) ==> C(y, x, t)

theorem C_imp_E_and_E:

  C(x, y, t) ==> E(x, t) ∧ E(y, t)

theorem P_imp_C_imp_C:

  P(x, y, t) ==> ∀z. C(z, x, t) --> C(z, y, t)

theorem L_and_L_and_C_imp_CGR:

  [| L(x, a, t); L(y, b, t); CGR(a, b) |] ==> C(x, y, t)

theorem EC_imp_C_and_notO:

  EC(x, y, t) ==> C(x, y, t) ∧ ¬ O(x, y, t)

theorem EC_irrefl:

  x t. ¬ EC(x, x, t)

theorem EC_sym:

  EC(x, y, t) ==> EC(y, x, t)

theorem DC_irrefl:

  x t. ¬ DC(x, x, t)

theorem DC_sym:

  DC(x, y, t) ==> DC(y, x, t)

theorem DC_imp_notC:

  DC(x, y, t) ==> ¬ C(x, y, t)

theorem P_imp_C:

  P(x, y, t) ==> C(x, y, t)

theorem O_imp_C:

  O(x, y, t) ==> C(x, y, t)

theorem P_and_C_imp_C:

  [| P(x, y, t); C(x, z, t) |] ==> C(y, z, t)

theorem PCoin_imp_C:

  PCoin(x, y, t) ==> C(x, y, t)

theorem LocIn_imp_C:

  LocIn(x, y, t) ==> C(x, y, t)

theorem PCoin_or_EC_or_notC:

  x y t. PCoin(x, y, t) ∨ EC(x, y, t) ∨ ¬ C(x, y, t)

theorem C_and_LocIn_imp_C:

  [| C(x, y, t); LocIn(y, z, t) |] ==> C(x, z, t)

theorem pEC_irrefl:

  x. ¬ pEC(x, x)

theorem pEC_sym:

  pEC(x, y) ==> pEC(y, x)

theorem pDC_irrefl:

  x. ¬ pDC(x, x)

theorem pDC_sym:

  pDC(x, y) ==> pDC(y, x)

theorem pDC_imp_notC:

  pDC(x, y) ==> ∀t. ¬ C(x, y, t)

theorem pDC_imp_not_pC:

  pDC(x, y) ==> ¬ pC(x, y)

theorem pP_imp_pC:

  pP(x, y) ==> pC(x, y)

theorem pPCoin_imp_pC:

  pPCoin(x, y) ==> pC(x, y)

theorem pC_and_pLocIn_imp_pC:

  [| pC(x, y); pLocIn(y, z) |] ==> pC(x, z)

theorem pEC_imp_pC_and_notpO:

  pEC(x, y) ==> pC(x, y) ∧ ¬ pO(x, y)

theorem pP_imp_pC_imp_pC:

  pP(x, y) ==> ∀z. pC(z, x) --> pC(z, y)

theorem pC_sym:

  pC(x, y) ==> pC(y, x)

theorem pO_imp_pC:

  pO(x, y) ==> pC(x, y)

theorem pP_and_pC_imp_pC:

  [| pP(x, y); pC(x, z) |] ==> pC(y, z)