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)