Theory TORL

theory TORL 

imports TNEMO EMR

begin

consts

L :: "Ob => Rg => Ti => o"
LocIn :: "Ob => Ob => Ti => o"
PCoin :: "Ob => Ob => Ti => o"
ContIn :: "Ob => Ob => Ti => o"

pLocIn :: "Ob => Ob => o"
pPCoin :: "Ob => Ob => o"
pContIn :: "Ob => Ob => o"

axioms

L_exists: "(ALL x t. (E(x,t) <-> (EX a. L(x,a,t))))"
L_P_PR: "(ALL x y a b t. (L(x,a,t) & L(y,b,t) & P(x,y,t) --> PR(a,b)))"
P_and_L_and_L_imp_P: "(ALL x y a t. (P(x,y,t) & L(x,a,t) & L(y,a,t) --> P(y,x,t)))"

defs

LocIn_def: "LocIn(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & PR(a,b)))"
PCoin_def: "PCoin(x,y,t) == (EX a b. (L(x,a,t) & L(y,b,t) & OR(a,b)))"
ContIn_def: "ContIn(x,y,t) == LocIn(x,y,t) & ~O(x,y,t)"

pLocIn_def: "pLocIn(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> LocIn(x,y,t)))"
pPCoin_def: "pPCoin(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> PCoin(x,y,t)))"
pContIn_def: "pContIn(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> ContIn(x,y,t)))"


(* axioms as rules *)


lemma L_exists1: "E(x,t) ==> (EX a. L(x,a,t))"
apply(insert L_exists)
apply(auto)
done

lemma L_exists2: "(EX a. L(x,a,t)) ==> E(x,t)"
apply(insert L_exists)
apply(auto)
done


lemma L_P_PR_rule: "[|L(x,a,t); L(y,b,t); P(x,y,t)|] ==> PR(a,b)"
apply(insert L_P_PR)
apply(erule_tac x="x" in allE)
apply(erule_tac x="y" in allE)
apply(erule_tac x="a" in allE)
apply(erule_tac x="b" in allE)
apply(erule_tac x="t" in allE)
apply(auto)
done


lemma P_and_L_and_L_imp_P_rule: "[|P(x,y,t);L(x,a,t);L(y,a,t)|] ==> P(y,x,t)"
apply(insert P_and_L_and_L_imp_P)
apply(auto)
done

(* theorems for location *)

theorem L_unique: "[|L(x,a,t);L(x,b,t)|] ==> a=b"
apply(rule PR_antisym_rule)
apply(insert L_P_PR_rule [of "x" "a" "t" "x" "b"])
apply(insert L_exists)
apply(unfold E_def)
apply(auto)
apply(insert L_P_PR_rule [of "x" "b" "t" "x" "a"])
apply(auto)
done

theorem LocIn_imp_E_and_E: "LocIn(x,y,t) ==> (E(x,t) & E(y,t))"
apply(unfold LocIn_def)
apply(insert L_exists)
apply(auto)
done

theorem P_imp_L: "P(x,y,t) ==> (EX a b. (L(x,a,t) & L(y,b,t) & PR(a,b)))"
apply(frule P_exists2_rule)
apply(erule conjE)
apply(drule L_exists1)
apply(drule L_exists1)
apply(clarify)
apply(frule_tac x="x" and y="y" and a="a" and b="aa" and t="t" in L_P_PR_rule)
apply(auto)
done

theorem L_and_L_and_PR_imp_L: "[|L(x,a,t);L(y,b,t);PR(a,b)|] ==> LocIn(x,y,t)"
apply(unfold LocIn_def)
apply(auto)
done



theorem LocIn_imp_PCoin: "LocIn(x,y,t) ==> PCoin(x,y,t)"
apply(unfold LocIn_def,unfold PCoin_def)
apply(insert PR_imp_OR)
apply(auto)
done

theorem E_imp_LocIn: "E(x,t) ==> LocIn(x,x,t)"
apply(unfold LocIn_def)
apply(drule L_exists1)
apply(erule exE)
apply(rule_tac x="a" in exI)
apply(rule_tac x="a" in exI)
apply(insert PR_refl)
apply(auto)
done

theorem LocIn_trans: "[|LocIn(x,y,t);LocIn(y,z,t)|] ==> LocIn(x,z,t)"
apply(unfold LocIn_def)
apply(clarify)
apply(rotate_tac 1)
apply(drule_tac x="y" and a="aa" and t="t" and b="b" in L_unique)
apply(assumption)
apply(rule_tac x="a" in exI)
apply(rule_tac x="ba" in exI)
apply(rule conjI)
apply(assumption)
apply(rule conjI)
apply(assumption)
apply(rule PR_trans_rule)
apply(assumption)
apply(auto)
done

theorem PCoin_sym: "PCoin(x,y,t) ==> PCoin(y,x,t)"
apply(unfold PCoin_def)
apply(insert OR_sym)
apply(auto)
done

theorem P_imp_LocIn: "P(x,y,t) ==> LocIn(x,y,t)"
apply(unfold LocIn_def)
apply(frule P_exists2_rule)
apply(erule conjE)
apply(drule L_exists1)
apply(drule_tac x="y" in L_exists1)
apply(erule exE)
apply(erule exE)
apply(rule_tac x="a" in  exI)
apply(rule_tac x="aa" in exI)
apply(auto)
apply(rule_tac a="a" and b="aa" in L_P_PR_rule)
apply(auto)
done

theorem P_and_LocIn_imp_P: "[|P(x,y,t);LocIn(y,x,t)|] ==> P(y,x,t)"
apply(unfold LocIn_def)
apply(clarify)
apply(frule_tac x="x" and y="y" and t="t" in P_imp_L)
apply(clarify)
apply(drule_tac x="x" and a="b" and b="aa" and t="t" in L_unique)
apply(drule_tac x="y" and a="a" and b="ba" and t="t" in L_unique)
apply(safe)
apply(drule_tac x="y" and a="a" and b="ba" and t="t" in L_unique)
apply(safe)
apply(drule_tac a="aa" and b="ba" in PR_antisym_rule)
apply(safe)
apply(drule_tac x="x" and y="y" and a="ba" and t="t" in P_and_L_and_L_imp_P_rule)
apply(auto)
done

theorem LocIn_and_P_imp_LocIn: "[|LocIn(x,y,t);P(y,z,t)|] ==> LocIn(x,z,t)"
apply(insert P_imp_LocIn)
apply(insert LocIn_trans)
apply(auto)
done

theorem P_and_LocIn_imp_LocIn: "[|P(x,y,t);LocIn(y,z,t)|] ==> LocIn(x,z,t)"
apply(drule P_imp_LocIn)
apply(rotate_tac 1)
apply(drule LocIn_trans)
apply(auto)
done

theorem O_imp_PCoin: "O(x,y,t) ==> PCoin(x,y,t)"
apply(unfold PCoin_def)
apply(unfold O_def)
apply(erule exE)
apply(erule conjE)
apply(frule P_exists2_rule)
apply(rotate_tac 1)
apply(frule P_exists2_rule)
apply(clarify)
apply(drule L_exists1)
apply(drule L_exists1)
apply(drule L_exists1)
apply(drule L_exists1)
apply(clarify)
apply(rule_tac x="aa" in exI)
apply(rule_tac x="ac" in exI)
apply(auto)
apply(unfold OR_def)
apply(frule_tac x="z" and a="ab" and y="y" and b="ac" and t="t" in L_P_PR_rule)
apply(auto)
apply(drule_tac x="z" and a="ab" and y="x" and b="aa" and t="t" in L_P_PR_rule)
apply auto
done

(*
theorem ContIn_asym: "ContIn(x,y,t) ==> ~ContIn(y,x,t)"
apply(unfold ContIn_def,unfold LocIn_def)
apply(clarify)
at this point it is clear that we cannot prove asymmetry. the axioms allow that non-overlapping regions are located at the same spatial region ...
*)

(*
theorem ContIn_trans: "[|ContIn(x,y,t);ContIn(y,z,t)|] ==> ContIn(x,z,t)"
apply(unfold ContIn_def)
apply(safe)
apply(rule LocIn_trans)
apply(auto)
apply(drule_tac x="x" and y="y" and z="z" and t="t" in LocIn_trans)
apply(assumption)
apply(unfold LocIn_def)
apply(clarify)
apply(drule_tac x="z" and a="b" and b="ba" and t="t" in L_unique)
apply(assumption)
apply(auto)
we cannot prove transitivity since non-overlapping objects can be located at overlapping regions
*)

theorem pLocIn_imp_pPCoin: "pLocIn(x,y) ==> pPCoin(x,y)"
apply(unfold pLocIn_def,unfold pPCoin_def)
apply(insert LocIn_imp_PCoin)
apply(auto)
done

theorem pLocIn_refl: "(ALL x. pLocIn(x,x))"
apply(unfold pLocIn_def)
apply(insert E_imp_LocIn)
apply(auto)
done


theorem pLocIn_trans: "[|pLocIn(x,y);pLocIn(y,z)|] ==> pLocIn(x,z)"
apply(unfold pLocIn_def)
apply(rule allI)
apply(safe)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in LocIn_trans)
apply(erule_tac x="t" in allE)
apply(drule_tac P="E(x,t)" and Q="E(y,t)" in disjI1)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(drule_tac P="E(x,t)" and Q="E(y,t)" in disjI1)
apply(clarify)
apply(drule LocIn_imp_E_and_E)
apply(force)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in LocIn_trans)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(drule_tac P="E(y,t)" and Q="E(z,t)" in disjI2)
apply(safe)
apply(drule LocIn_imp_E_and_E)
apply(force)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(drule_tac P="E(y,t)" and Q="E(z,t)" in disjI2)
apply(clarify)
done 

theorem pPCoin_sym: "pPCoin(x,y) ==> pPCoin(y,x)"
apply(unfold pPCoin_def)
apply(insert PCoin_sym)
apply(auto)
done


theorem pP_imp_pLocIn: "pP(x,y) ==> pLocIn(x,y)"
apply(unfold pP_def,unfold pLocIn_def)
apply(insert P_imp_LocIn)
apply(auto)
done

theorem pLocIn_and_pP_imp_pLocIn: "[|pLocIn(x,y);pP(y,z)|] ==> pLocIn(x,z)"
apply(unfold pLocIn_def,unfold pP_def)
apply(safe)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in LocIn_and_P_imp_LocIn)
apply(auto)
apply(insert LocIn_imp_E_and_E)
apply(auto)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in LocIn_and_P_imp_LocIn)
apply(auto)
apply(insert P_exists2_rule)
apply(auto)
done

theorem pP_and_pLocIn_imp_pLocIn: "[|pP(x,y);pLocIn(y,z)|] ==> pLocIn(x,z)"
apply(unfold pLocIn_def,unfold pP_def)
apply(safe)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in P_and_LocIn_imp_LocIn)
apply(auto)
apply(insert P_exists2_rule)
apply(auto)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in P_and_LocIn_imp_LocIn)
apply(insert LocIn_imp_E_and_E)
apply(auto)
done

theorem pP_and_pLocIn_imp_pP: "[|pP(x,y);pLocIn(y,x)|] ==> pP(y,x)"
apply(unfold pP_def,unfold pLocIn_def)
apply(insert P_and_LocIn_imp_P)
apply(auto)
done

theorem pO_imp_pPCoin: "pO(x,y) ==> pPCoin(x,y)"
apply(unfold pO_def,unfold pPCoin_def)
apply(insert O_imp_PCoin)
apply(auto)
done 


theorem pContIn_imp_pLocIn_and_notpO: "pContIn(x,y) ==> pLocIn(x,y) & ~pO(x,y)"
apply(unfold pContIn_def,unfold pLocIn_def,unfold pO_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(safe)
apply(unfold ContIn_def)
apply(safe)
apply(erule_tac x="t" in allE)
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(safe)
done

theorem pContIn_imp_pLocIn_and_notO: "pContIn(x,y) ==> (pLocIn(x,y) & (ALL t. ~O(x,y,t)))"
apply(unfold pContIn_def,unfold pLocIn_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(safe)
apply(unfold ContIn_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(safe)
apply(insert P_exists1)
apply(erule_tac x="x" in allE)
apply(clarify)
apply(frule_tac x="x" and y="y" and t="t" in O_imp_E_and_E)
apply(clarify)
apply(erule_tac x="t" in allE)
apply(safe)
done

theorem pLocIn_and_notO_imp_pContIn: "[|pLocIn(x,y);(ALL t. ~O(x,y,t))|] ==> pContIn(x,y)"
apply(unfold pContIn_def,unfold pLocIn_def)
apply(unfold ContIn_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(safe)
apply(erule_tac x="t" in allE)
apply(safe)
apply(erule_tac x="t" in allE)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
done

end