Theory TNEMO

theory TNEMO imports FOL

begin

typedecl Ob
typedecl Ti


arities Ob :: "term"
        Ti :: "term"


(* temporal non-extensional mereology of objects *)

consts

O :: "Ob => Ob => Ti => o"
P :: "Ob => Ob => Ti => o"
PP :: "Ob => Ob => Ti => o"
E :: "Ob => Ti => o"
Me :: "Ob => Ob => Ti => o"

pP :: "Ob => Ob => o"
pPP :: "Ob => Ob => o"
pO :: "Ob => Ob => o"
pMe :: "Ob => Ob => o" 

cP :: "Ob => Ob => o"
bP :: "Ob => Ob => o"

axioms

P_exists1: "(ALL x. (EX t. E(x,t)))"
P_exists2: "(ALL x y t. (P(x,y,t) -->(E(x,t) & E(y,t))))"
P_trans: "(ALL x y z t. (P(x,y,t) & P(y,z,t) --> P(x,z,t)))"
P_ssuppl: "(ALL x y t. ((E(x,t) & ~P(x,y,t)) --> (EX z. (P(z,x,t) & ~O(z,y,t)))))"

defs 

E_def: "E(x,t) == P(x,x,t)"
O_def: "O(x,y,t) == (EX z. (P(z,x,t) & P(z,y,t)))"
PP_def: "PP(x,y,t) == P(x,y,t) & ~P(y,x,t)"
Me_def: "Me(x,y,t) == (P(x,y,t) & P(y,x,t))"

pP_def: "pP(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> P(x,y,t)))"
pPP_def: "pPP(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> PP(x,y,t)))"
pO_def: "pO(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> O(x,y,t)))"
pMe_def: "pMe(x,y) == (ALL t. ((E(x,t) | E(y,t)) --> Me(x,y,t)))"

cP_def: "cP(x,y) == (ALL t. (E(y,t) --> P(x,y,t)))"
bP_def: "bP(x,y) == (ALL t. (E(x,t) --> P(x,y,t)))"

(* axioms as rules *)


lemma P_exists2_rule: "P(x,y,t) ==>(E(x,t) & E(y,t))"
apply(insert P_exists2)
apply(auto)
done

lemma P_trans_rule: "[|P(x,y,t); P(y,z,t)|] ==> P(x,z,t)"
apply(insert P_trans)
apply(erule allE,erule allE,erule allE,erule allE)
apply(rule mp)
apply(assumption)
apply(rule conjI)
apply(assumption)
apply(assumption)
done

lemma P_Me_rule: "[|P(x,y,t);P(y,x,t)|] ==> Me(x,y,t)"
apply(drule conjI)
apply(assumption)
apply(fold Me_def)
apply(assumption)
done

lemma P_ssuppl_rule: "[|E(x,t);~P(x,y,t)|] ==> (EX z. (P(z,x,t) & ~O(z,y,t)))"
apply(insert P_ssuppl)
apply(auto)
done

lemma ltb2: "(~(A & ~B) ==> (~A | B))"
apply(auto) 
done

lemma P_ssuppl_rule_transpos: "~(EX z. (P(z,x,t) & ~O(z,y,t))) ==> (~E(x,t) | P(x,y,t))"
apply(insert P_ssuppl)
apply(rule ltb2)
apply(rule notI)
apply(auto)
done


(* theorems of non-extensional temporal mereology *) 


theorem P_refl: "E(x,t) ==> P(x,x,t)"
apply(unfold E_def)
apply(assumption)
done

theorem Me_refl: "E(x,t) ==> Me(x,x,t)"
apply(unfold Me_def)
apply(unfold E_def)
apply(auto)
done

theorem Me_exists2: "Me(x,y,t) ==> (E(x,t) & E(y,t))"
apply(unfold Me_def)
apply(rule conjI)
apply(erule conjE)
apply(drule P_exists2_rule)
apply(auto)
apply(drule P_exists2_rule)
apply(auto)
done

theorem Me_sym: "Me(x,y,t) ==> Me(y,x,t)"
apply(unfold Me_def)
apply(auto)
done

theorem Me_trans: "[|Me(x,y,t); Me(y,z,t)|] ==> Me(x,z,t)"
apply(unfold Me_def)
apply(rule conjI)
apply(erule conjE,erule conjE)
apply(erule P_trans_rule)
apply(assumption)
apply(erule conjE,erule conjE)
apply(erule P_trans_rule)
apply(assumption)
done

theorem O_refl: "(ALL x t. E(x,t) --> O(x,x,t))"
apply(rule allI,rule allI)
apply(unfold E_def)
apply(unfold O_def)
apply(auto)
done

lemma O_refl_rule: "E(x,t) ==> O(x,x,t)"
apply(insert O_refl)
apply(auto)
done

theorem O_sym: "(ALL x y t. (O(x,y,t) --> O(y,x,t)))"
apply(unfold O_def)
apply(auto)
done


lemma O_sym_rule: "O(x,y,t) ==> O(y,x,t)"
apply(insert O_sym)
apply(auto)
done


theorem O_imp_E_and_E: "O(x,y,t) ==> (E(x,t) & E(y,t))"
apply(rule conjI)
apply(unfold O_def)
apply(erule exE)
apply(erule conjE)
apply(drule P_exists2_rule)
apply(auto)
apply(rotate_tac 1)
apply(drule P_exists2_rule)
apply(auto)
done


theorem PP_imp_P: "(ALL x y t. (PP(x,y,t) --> P(x,y,t)))"
apply(unfold PP_def)
apply(auto)
done

lemma PP_imp_P_rule: "PP(x,y,t) ==> P(x,y,t)"
apply(unfold PP_def)
apply(auto)
done

theorem P_imp_Me_or_PP: "P(x,y,t) ==> (Me(x,y,t) | PP(x,y,t))"
apply(unfold PP_def,unfold Me_def)
apply(auto)
done

theorem PP_or_Me_imp_P: "(PP(x,y,t) | Me(x,y,t)) ==> P(x,y,t)"
apply(unfold Me_def)
apply(safe)
apply(drule PP_imp_P_rule)
apply(assumption)
done




theorem PP_asym: "(ALL x y t. PP(x,y,t) --> ~PP(y,x,t))"
apply(unfold PP_def)
apply(auto)
done



lemma PP_asym_rule: "PP(x,y,t) ==> ~PP(y,x,t)"
apply(insert PP_asym)
apply(auto)
done

theorem PP_trans: "(ALL x y z t. (PP(x,y,t) & PP(y,z,t)-->PP(x,z,t)))"
apply(rule allI, rule allI, rule allI,rule allI)
apply(rule impI)
apply(unfold PP_def)
apply(rule conjI)
apply(erule conjE,erule conjE,erule conjE)
apply(rule P_trans_rule)
apply(assumption)
apply(assumption)
apply(erule conjE, erule conjE, erule conjE)
apply(drule P_trans_rule)
apply(assumption)
apply(rule notI)
apply(drule P_trans_rule)
apply(assumption)
apply(erule notE)
apply(assumption)
done

lemma PP_trans_rule: assumes p1: "PP(x,y,t)" assumes p2: "PP(y,z,t)" shows "PP(x,z,t)"
apply(insert PP_trans)
apply(erule allE, erule allE,erule allE,erule allE)
apply(rule mp)
apply(assumption)
apply(rule conjI)
apply(insert p1)
apply(assumption)
apply(insert p2)
apply(assumption)
done


theorem P_and_PP_imp_PP: "[|P(x,y,t);PP(y,z,t)|] ==> PP(x,z,t)"
apply(drule P_imp_Me_or_PP)
apply(safe)
apply(unfold Me_def)
apply(clarify)
prefer 2
apply(drule PP_trans_rule [of x y t z])
apply(assumption)
apply(assumption)
apply(unfold PP_def)
apply(safe)
apply(drule P_trans_rule [of x y t z])
apply(assumption)
apply(assumption)
apply(drule P_trans_rule [of z x t y])
apply(auto)
done

theorem PP_and_P_imp_PP: "[|PP(x,y,t);P(y,z,t)|] ==> PP(x,z,t)"
apply(drule P_imp_Me_or_PP)
apply(safe)
apply(unfold Me_def)
apply(clarify)
prefer 2
apply(drule PP_trans_rule [of x y t z])
apply(assumption)
apply(assumption)
apply(unfold PP_def)
apply(safe)
apply(drule P_trans_rule [of x y t z])
apply(assumption)
apply(assumption)
apply(drule P_trans_rule [of y z t x])
apply(auto)
done


(* from now on we only use the rule notation wherever possible *)


theorem P_and_notMe_imp_PP: "[|P(x,y,t);~Me(x,y,t)|] ==> PP(x,y,t)"
apply(unfold Me_def,unfold PP_def)
apply(auto)
done

theorem P_imp_O: "P(x,y,t) ==> O(x,y,t)"
apply(unfold O_def)
apply(rule exI)
apply(rule conjI)
apply(drule P_exists2_rule)
apply(erule conjE)
apply(unfold E_def)
apply(assumption)
apply(assumption)
done

theorem P_and_O: "[|P(x,y,t);O(x,z,t)|] ==> O(y,z,t)" 
apply(unfold O_def)
apply(erule exE)
apply(rule exI)
apply(rule conjI)
apply(erule conjE)
prefer 2
apply(erule conjE)
apply(assumption)
apply(rule P_trans_rule)
apply(assumption)
apply(assumption)
done


theorem O_imp_O_imp_P: "(ALL x y t. (E(x,t) & (ALL z. (O(z,x,t) --> O(z,y,t))) --> P(x,y,t)))"
apply(rule allI,rule allI,rule allI)
apply(rule impI)
apply(erule conjE)
apply(rule_tac P="~E(x,t)" and Q="P(x,y,t)" in disjE)
apply(rule P_ssuppl_rule_transpos)
apply(rule notI)
apply(erule exE)
apply(erule allE)
apply(erule conjE)
apply(drule P_imp_O)
apply(drule mp)
apply(assumption)
apply(erule notE)
apply(assumption)
apply(erule_tac R="P(x,y,t)" in notE)
apply(assumption)
apply(assumption)
done

lemma O_imp_O_imp_P_rule: "[|E(x,t);(ALL z. (O(z,x,t) --> O(z,y,t)))|] ==> P(x,y,t)"
apply(insert O_imp_O_imp_P)
apply(auto)
done

lemma ltb1: "(ALL z. (A(z,x,t) & B(z,y,t))) ==> (ALL z. A(z,x,t)) & (ALL z. B(z,y,t))"
apply(auto)
done


theorem O_iff_O_iff_Me : "(ALL x y t. ((E(x,t) & E(y,t) & (ALL z. (O(z,x,t) <-> O(z,y,t)))) <-> Me(x,y,t)))"
apply(rule allI,rule allI,rule allI)
apply(unfold iff_def)
apply(rule conjI)
apply(rule impI)
apply(unfold Me_def)
apply(erule conjE,erule conjE)
apply(drule ltb1)
apply(erule conjE)
apply(rule conjI)
apply(drule O_imp_O_imp_P_rule)
prefer 2
apply(assumption)
apply(assumption)
apply(drule_tac x="y" and y="x" in O_imp_O_imp_P_rule)
prefer 2
apply(assumption)
apply(assumption)
apply(auto)
apply(drule P_exists2_rule)
apply(erule conjE)
apply(assumption)
apply(drule P_exists2_rule)
apply(erule conjE)
apply(assumption)
apply(drule P_and_O)
apply(drule O_sym_rule)
apply(assumption)
apply(rule O_sym_rule)
apply(assumption)
apply(drule_tac x="y" and y="x" in P_and_O)
apply(drule O_sym_rule)
apply(assumption)
apply(rule O_sym_rule)
apply(assumption)
done



theorem P_iff_P_iff_Me:  "(ALL x y t. ((E(x,t) & E(y,t) & (ALL z. (P(z,x,t) <-> P(z,y,t)))) <-> Me(x,y,t)))"
apply(rule allI,rule allI,rule allI)
apply(rule iffI)
apply(erule conjE,erule conjE)
apply(unfold Me_def)
apply(unfold E_def)
apply(rule conjI)
apply(erule_tac x="x" in allE)
apply(erule iffE)
apply(drule_tac P="P(x, x, t)" and Q="P(x, y, t)" in mp)
apply(assumption)
apply(assumption)
apply(erule_tac x="y" in allE)
apply(erule iffE)
apply(drule_tac P="P(y, y, t)" and Q="P(y, x, t)" in mp)
apply(assumption)
apply(assumption)
apply(rule conjI)
apply(fold E_def)
apply(fold Me_def)
apply(drule Me_exists2)
apply(erule conjE)
apply(assumption)
apply(rule conjI)
apply(drule Me_exists2)
apply(erule conjE)
apply(assumption)
apply(rule allI)
apply(rule iffI)
apply(unfold Me_def)
apply(erule conjE)
apply(drule_tac x="z" and y="x" and z="y" in P_trans_rule)
apply(assumption)
apply(assumption)
apply(erule conjE)
apply(drule_tac x="z" and y="y" and z="x" in P_trans_rule)
apply(auto)
done


theorem pP_refl: "ALL x. pP(x,x)"
apply(unfold pP_def)
apply(unfold E_def)
apply(auto)
done

theorem pP_trans: "[|pP(x,y);pP(y,z)|] ==> pP(x,z)"
apply(unfold pP_def)
apply(auto)
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(frule P_exists2_rule)
apply(auto)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in P_trans_rule)
apply(assumption, assumption)
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)
apply(frule P_exists2_rule)
apply(auto)
apply(rule_tac x="x" and y="y" and z="z" and t="t" in P_trans_rule)
apply(assumption, assumption)
done

theorem pPP_asym: "pPP(x,y) ==> ~pPP(y,x)"
apply(unfold pPP_def)
apply(clarify)
apply(insert P_exists1)
apply(erule_tac x="x" in allE)
apply(erule exE)
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(frule PP_imp_P_rule)
apply(drule P_exists2_rule)
apply(drule PP_asym_rule)
apply(auto)
done

theorem pPP_trans: "[|pPP(x,y);pPP(y,z)|] ==> pPP(x,z)"
apply(unfold pPP_def)
apply(safe)
apply(rule_tac x="x" and y="y" and t="t" in PP_trans_rule)
apply(auto)
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(drule mp, assumption)
apply(frule PP_imp_P_rule)
apply(drule P_exists2_rule)
apply(auto)
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(drule mp, assumption)
apply(frule PP_imp_P_rule)
apply(drule P_exists2_rule)
apply(auto)
apply(rule_tac x="x" and y="y" and t="t" in PP_trans_rule)
apply(auto)
done


theorem pPP_imp_pP_and_notpP: "pPP(x,y) ==> (pP(x,y) & ~pP(y,x))"
apply(unfold pPP_def,unfold pP_def)
apply(unfold PP_def)
apply(rule conjI)
apply(safe)
apply(erule_tac x="t" in allE)
apply(force)
apply(erule_tac x="t" in allE)
apply(force)
apply(insert P_exists1)
apply(erule_tac x="x" in allE)
apply(erule exE)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(auto)
done



(* theorem pP_and_notpP_imp_pPP: "[|pP(x,y);~pP(y,x)|] ==> pPP(x,y)"
apply(unfold pP_def,unfold pPP_def)
apply(clarify)
apply(erule_tac x="ta" in allE)
apply(safe)
apply(unfold PP_def)
apply(safe)
at this point it is clear that this is not provable *)


theorem pO_refl: "(ALL x. pO(x,x))"
apply(unfold pO_def)
apply(insert O_refl)
apply(auto)
done

theorem pO_sym: "pO(x,y) ==> pO(y,x)"
apply(unfold pO_def)
apply(insert O_sym)
apply(auto)
done



(* theorem pO_shared_pP: "[|pO(x,y)|] ==> (EX z. (pP(z,x) & pP(z,y)))"
apply(unfold pO_def,unfold pP_def,unfold O_def)
apply(erule_tac x="t" in allE)
apply(insert excluded_middle [of "(E(x, t) | E(y, t))"])
apply(erule disjE)
prefer 2
apply(auto)
apply(rule_tac x="z" in exI)
apply(auto)
at this point it is clear that we cannot prove this
*)

theorem SharedpP_imp_pO: "(EX z. (pP(z,x) & pP(z,y))) ==> pO(x,y)"
apply(unfold pP_def,unfold pO_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(drule_tac P="E(z,t)" and Q="E(x,t)" in disjI2)
apply(clarify)
apply(unfold O_def)
apply(rule_tac x="z" in exI)
apply(frule_tac x="z" and y="x" and t="t" in P_exists2_rule)
apply(safe)
apply(rule_tac x="z" in exI)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(drule_tac P="E(z,t)" and Q="E(y,t)" in disjI2)
apply(clarify)
apply(drule_tac x="z" and y="y" and t="t" in P_exists2_rule)
apply(auto)
done


theorem cP_refl: "(ALL x. (cP(x,x)))"
apply(unfold cP_def)
apply(insert P_exists1)
apply(unfold E_def)
apply(auto)
done

theorem cP_trans: "[|cP(x,y);cP(y,z)|] ==> cP(x,z)"
apply(unfold cP_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule P_exists2_rule)
apply(safe)
apply(drule_tac x="x" and y="y" and z="z" and t="t" in P_trans_rule)
apply(auto)
done

theorem bP_refl: "(ALL x. (bP(x,x)))"
apply(unfold bP_def)
apply(insert P_exists1)
apply(unfold E_def)
apply(auto)
done

theorem bP_trans: "[|bP(x,y);bP(y,z)|] ==> bP(x,z)"
apply(unfold bP_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(safe)
apply(drule P_exists2_rule)
apply(safe)
apply(drule_tac x="x" and y="y" and z="z" and t="t" in P_trans_rule)
apply(auto)
done


theorem pP_imp_cP_and_bP: "pP(x,y) ==> (cP(x,y) & bP(x,y))"
apply(unfold pP_def,unfold cP_def,unfold bP_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(auto)
done

theorem cP_and_bP_imp_pP: "[|cP(x,y);bP(x,y)|] ==> pP(x,y)"
apply(unfold pP_def,unfold cP_def,unfold bP_def)
apply(safe)
apply(erule_tac x="t" in allE)
apply(erule_tac x="t" in allE)
apply(auto)
done



end