Theory EMR

Up to index of Isabelle/FOL/BFO

theory EMR
imports FOL
begin

theory EMR 

imports FOL

begin
typedecl Rg


arities Rg :: "term"

(* Atemporal extensional mereology of regions*)

consts

OR :: "Rg => Rg => o"
POR :: "Rg => Rg => o"
PR :: "Rg => Rg  => o"
PPR :: "Rg => Rg  => o"
Sum :: "Rg => Rg => Rg => o"
Diff :: "Rg => Rg => Rg => o"
Prod :: "Rg => Rg => Rg => o"
UniR :: "Rg => o"

axioms

PR_refl: "(ALL a. PR(a,a))"
PR_antisym: "(ALL a b. (PR(a,b) & PR(b,a) --> a=b))"
PR_trans: "(ALL a b c. (PR(a,b) & PR(b,c) --> PR(a,c)))"
PR_diff: "(ALL a b. (~PR(a,b)) --> (EX c. Diff(a,b,c)))"
PR_sum: "(ALL a b. (EX c. Sum(a,b,c)))"
PR_prod: "(ALL a b. (OR(a,b) --> (EX c. Prod(a,b,c))))"

defs

OR_def: "OR(a,b) == (EX c. (PR(c,a) & PR(c,b)))"
POR_def: "POR(a,b) == OR(a,b) & ~PR(a,b) & ~PR(b,a)"
PPR_def: "PPR(a,b) == PR(a,b) & ~PR(b,a)"
Sum_def: "Sum(a,b,c) == (ALL d. OR(d,c) <-> (OR(d,a) | OR(d,b)))"
Diff_def: "Diff(a,b,c) == (ALL d. OR(d,c) <-> (EX e. (PR(e,a) & ~OR(e,b) & OR(e,d))))"
Prod_def: "Prod(a,b,c) == (ALL d. OR(d,c) <-> (OR(d,a) & OR(d,b)))"
UniR_def: "UniR(a) == (ALL b. PR(b,a))"

(* axioms as rules *)

lemma PR_refl_rule: "PR(a,a)"
apply(insert PR_refl)
apply(auto)
done


lemma PR_trans_rule: "[|PR(a,b); PR(b,c)|] ==> PR(a,c)"
apply(insert PR_trans)
apply(erule allE,erule allE,erule allE)
apply(rule mp)
apply(assumption)
apply(rule conjI)
apply(assumption)
apply(assumption)
done

lemma PR_antisym_rule: "[|PR(a,b); PR(b,a)|] ==> a=b"
apply(insert PR_antisym)
apply(erule allE,erule allE)
apply(rule mp)
apply(assumption)
apply(rule conjI)
apply(assumption)
apply(assumption)
done

lemma PR_diff_rule: "~PR(a,b)==>(EX c. Diff(a,b,c))"
apply(insert PR_diff)
apply(auto)
done

(* Theorems of extensional atemporal mereology of regions *)

lemma PPR_imp_PR: "PPR(a,b) ==> PR(a,b)"
apply(unfold PPR_def)
apply(auto)
done

theorem PPR_asym: "PPR(a,b) ==> ~PPR(b,a)"
apply(unfold PPR_def)
apply(auto)
done

theorem PPR_trans: "[|PPR(a,b);PPR(b,c)|]==>PPR(a,c)"
apply(unfold PPR_def)
apply(clarify)
apply(rule conjI)
apply(rule PR_trans_rule)
apply(assumption)
apply(assumption)
apply(drule PR_trans_rule)
apply(assumption)
apply(rule notI)
apply(drule PR_trans_rule)
apply(assumption)
apply(erule notE)
apply(assumption)
done

theorem PR_imp_PPR_or_Id: "PR(a,b) ==> (PPR(a,b) | (a=b))"
apply(safe)
apply(unfold PPR_def)
apply(safe)
apply(drule PR_antisym_rule)
apply(auto)
done

theorem PPR_or_Id_imp_PR: "(PPR(a,b) | (a=b)) ==> PR(a,b)"
apply(insert PPR_imp_PR)
apply(insert PR_refl)
apply(auto)
done

theorem PR_and_PPR_imp_PPR: "[|PR(a,b);PPR(b,c)|] ==> PPR(a,c)"
apply(drule PR_imp_PPR_or_Id)
apply(safe)
apply(drule PPR_trans [of a b c])
apply(auto)
done

theorem PPR_and_PR_imp_PPR: "[|PPR(a,b);PR(b,c)|] ==> PPR(a,c)"
apply(drule PR_imp_PPR_or_Id [of b c])
apply(safe)
apply(drule PPR_trans [of a b c])
apply(auto)
done


theorem OR_refl: "OR(a,a)"
apply(unfold OR_def)
apply(insert PR_refl)
apply(auto)
done


theorem OR_sym: "OR(a,b) ==> OR(b,a)"
apply(unfold OR_def)
apply(auto)
done

theorem POR_sym: "POR(a,b) ==> POR(b,a)"
apply(unfold POR_def)
apply(insert OR_sym)
apply(auto)
done

theorem POR_irrefl: "~POR(a,a)"
apply(unfold POR_def)
apply(insert PR_refl)
apply(auto)
done

theorem PR_imp_OR: "PR(a,b) ==> OR(a,b)"
apply(unfold OR_def)
apply(insert PR_refl)
apply(auto)
done

theorem PR_and_OR: "[|PR(a,b);OR(a,c)|] ==> OR(b,c)" 
apply(unfold OR_def)
apply(insert PR_trans_rule)
apply(auto)
done



theorem PR_and_notOR_imp_notOR: "[|PR(a,b);~OR(b,c)|] ==> ~OR(a,c)"
apply(insert PR_and_OR)
apply(auto)
done

theorem notOR_sym: "~OR(a,b) ==> ~OR(b,a)"
apply(insert OR_sym)
apply(auto)
done



theorem PR_ssuppl: "~PR(a,b) ==> (EX c. (PR(c,a) & ~OR(c,b)))"
apply(drule PR_diff_rule)
apply(unfold Diff_def)
apply(insert OR_refl)
apply(auto)
done

lemma PR_ssuppl_transpos: "~(EX c. (PR(c,a) & ~OR(c,b))) ==> PR(a,b)"
apply(insert PR_ssuppl)
apply(auto)
done

theorem OR_imp_OR_imp_PR: "(ALL c. (OR(c,a) --> OR(c,b))) ==> PR(a,b)"
apply(rule PR_ssuppl_transpos)
apply(insert PR_imp_OR)
apply(auto)
done


theorem OR_ident : "(ALL a b. (ALL c. (OR(c,a) <-> OR(c,b))) <-> a=b)"
apply(rule allI,rule allI)
apply(unfold iff_def)
apply(rule conjI)
apply(rule impI)
apply(rule PR_antisym_rule)
apply(auto)
apply(rule OR_imp_OR_imp_PR)
apply(auto)
apply(rule_tac a="b" and b="a" in OR_imp_OR_imp_PR)
apply(auto)
done

theorem Sum_unique: "[|Sum(a,b,c);Sum(a,b,d)|] ==> c = d"
apply(unfold Sum_def)
apply(rule PR_antisym_rule)
apply(insert OR_imp_OR_imp_PR)
apply(auto)
done


theorem Sum_imp_PR_and_PR: "Sum(a,b,c)  ==> PR(a,c) & PR(b,c)"
apply(safe)
apply(rule_tac a="a" and b="c"  in OR_imp_OR_imp_PR)
apply(unfold Sum_def)
apply(force)
apply(rule_tac a="b" and b="c"  in OR_imp_OR_imp_PR)
apply(auto)
done

theorem Sum_sym: "Sum(a,b,c) ==> Sum(b,a,c)"
apply(unfold Sum_def)
apply(auto)
done

theorem Sum_refl: "Sum(a,a,a)"
apply(unfold Sum_def)
apply(auto)
done

theorem Sum_imp_id: "Sum(a,a,b) ==> a=b"
apply(unfold Sum_def)
apply(rule PR_antisym_rule)
apply(rule OR_imp_OR_imp_PR)
apply(auto)
apply(rule OR_imp_OR_imp_PR)
apply(auto)
done

theorem PR_imp_Sum: "PR(a,b) ==> Sum(a,b,b)"
apply(unfold Sum_def)
apply(safe)
apply(drule_tac a="d" and b="a" in OR_sym)
apply(drule_tac a="a" and b="b" and c="d" in PR_and_OR)
apply(assumption)
apply(rule OR_sym)
apply(assumption)
done

theorem Diff_unique: "[|Diff(a,b,c);Diff(a,b,d)|] ==> c = d"
apply(unfold Diff_def)
apply(rule PR_antisym_rule)
apply(rule_tac a="c" and b="d" in OR_imp_OR_imp_PR)
apply(clarify)
apply(erule_tac x="ca" in allE)
apply(clarify)
apply(frule_tac x="ca" in spec)
apply(insert OR_refl)
apply(erule iffE)
apply(auto)
apply(rule_tac a="d" and b="c" in OR_imp_OR_imp_PR)
apply(clarify)
apply(rotate_tac 1)
apply(erule_tac x="ca" in allE)
apply(clarify)
apply(frule_tac x="c" in spec)
apply(erule iffE)
apply(auto)
done

theorem Prod_unique: "[|Prod(a,b,c);Prod(a,b,d)|] ==> c = d"
apply(unfold Prod_def)
apply(rule PR_antisym_rule)
apply(insert OR_imp_OR_imp_PR)
apply(auto)
done



theorem Diff_imp_notPR: "Diff(a,b,c) ==> ~PR(a,b)"
apply(unfold Diff_def)
apply(safe)
apply(erule_tac x="c" in allE)
apply(insert OR_refl)
apply(auto)
apply(drule_tac a="e" and b="b" in notOR_sym)
apply(drule_tac a="a" and b="b" and c="e" in PR_and_notOR_imp_notOR)
apply(assumption)
apply(drule_tac a="e" and b="a" in PR_imp_OR)
apply(drule_tac a="e" and b="a" in OR_sym)
apply(clarify) 
done

theorem notOR_imp_Diff: "~OR(a,b) ==> Diff(a,b,a)"
apply(unfold Diff_def)
apply(safe)
apply(rule_tac x="a" in exI)
apply(auto)
apply(insert PR_refl)
apply(force)
apply(insert OR_sym)
apply(force)
apply(drule_tac a="e" and b="a" and c="d" in PR_and_OR)
apply(auto)
done

theorem Diff_imp_PR: "Diff(a,b,c) ==> PR(c,a)"
apply(unfold Diff_def)
apply(rule_tac a="c" and b="a" in OR_imp_OR_imp_PR)
apply(rule allI)
apply(clarify)
apply(erule_tac x="ca" in allE)
apply(safe)
apply(drule_tac a="e" and  b="a" and c="ca" in PR_and_OR)
apply(assumption)
apply(rule OR_sym)
apply(assumption)
done


theorem PR_and_notPR_imp_notPR: "[|PR(a,b);~PR(c,b)|] ==> ~PR(c,a)"
apply(safe)
apply(drule PR_trans_rule [of c a b])
apply(auto)
done

theorem PR_and_Diff_impl_Diff_PR: "[|PR(a,b);Diff(c,b,d)|] ==> (EX e. (Diff(c,a,e) & PR(d,e)))"
apply(frule Diff_imp_notPR [of c b d])
apply(frule Diff_imp_PR [of c b d])
apply(frule PR_and_notPR_imp_notPR [of a b c])
apply(assumption)
apply(frule PR_diff_rule [of c a])
apply(safe)
apply(rule_tac x="ca" in exI)
apply(safe)
apply(insert excluded_middle [of "OR(c,a)"])
apply(safe)
apply(drule_tac a="c" and b="a" in notOR_imp_Diff)
apply(rotate_tac 6)
apply(drule Diff_unique)
apply(assumption)
apply(force)
apply(rule_tac a="d" and b="ca" in OR_imp_OR_imp_PR)
apply(safe)
apply(drule_tac a="caa" and b="d" in OR_sym)
apply(frule_tac a="d" and b="c" and c="caa" in PR_and_OR)
apply(assumption)
apply(unfold Diff_def)
apply(rotate_tac 5)
apply(erule_tac x="caa" in allE)
apply(erule_tac x="caa" in allE)
apply(drule_tac a="d" and b="caa" in OR_sym)
apply(rotate_tac 7)
apply(erule iffE)
apply(drule_tac P="OR(caa, d)" and Q="(EX (e::Rg). (PR(e, c) & ((~ OR(e, b)) & OR(e, caa))))" in mp)
apply(assumption)
apply(erule exE)
apply(erule conjE)
apply(erule conjE)
apply(drule_tac a="e" and b="b" in notOR_sym)
apply(frule_tac a="a" and b="b" and c="e" in PR_and_notOR_imp_notOR)
apply(assumption)
thm conjI
apply(drule_tac a="a" and b="e" in notOR_sym)
apply(drule_tac P="PR(e, c)" and Q="~ OR(e, a)" in conjI)
apply(assumption)
apply(drule_tac P="(PR(e, c) & (~ OR(e, a)))" and Q="OR(e, caa)" in conjI)
apply(assumption)
apply(drule_tac P="% e. ((PR(e, c) & (~ OR(e, a))) & OR(e, caa))" in exI)
apply(erule iffE)
apply(auto)
done

theorem UniR_unique: "[|UniR(a);UniR(b)|] ==> a=b"
apply(unfold UniR_def)
apply(rule_tac a="a" and b="b" in PR_antisym_rule)
apply(auto)
done

end

lemma PR_refl_rule:

  PR(a, a)

lemma PR_trans_rule:

  [| PR(a, b); PR(b, c) |] ==> PR(a, c)

lemma PR_antisym_rule:

  [| PR(a, b); PR(b, a) |] ==> a = b

lemma PR_diff_rule:

  ¬ PR(a, b) ==> ∃c. Diff(a, b, c)

lemma PPR_imp_PR:

  PPR(a, b) ==> PR(a, b)

theorem PPR_asym:

  PPR(a, b) ==> ¬ PPR(b, a)

theorem PPR_trans:

  [| PPR(a, b); PPR(b, c) |] ==> PPR(a, c)

theorem PR_imp_PPR_or_Id:

  PR(a, b) ==> PPR(a, b) ∨ a = b

theorem PPR_or_Id_imp_PR:

  PPR(a, b) ∨ a = b ==> PR(a, b)

theorem PR_and_PPR_imp_PPR:

  [| PR(a, b); PPR(b, c) |] ==> PPR(a, c)

theorem PPR_and_PR_imp_PPR:

  [| PPR(a, b); PR(b, c) |] ==> PPR(a, c)

theorem OR_refl:

  OR(a, a)

theorem OR_sym:

  OR(a, b) ==> OR(b, a)

theorem POR_sym:

  POR(a, b) ==> POR(b, a)

theorem POR_irrefl:

  ¬ POR(a, a)

theorem PR_imp_OR:

  PR(a, b) ==> OR(a, b)

theorem PR_and_OR:

  [| PR(a, b); OR(a, c) |] ==> OR(b, c)

theorem PR_and_notOR_imp_notOR:

  [| PR(a, b); ¬ OR(b, c) |] ==> ¬ OR(a, c)

theorem notOR_sym:

  ¬ OR(a, b) ==> ¬ OR(b, a)

theorem PR_ssuppl:

  ¬ PR(a, b) ==> ∃c. PR(c, a) ∧ ¬ OR(c, b)

lemma PR_ssuppl_transpos:

  ¬ (∃c. PR(c, a) ∧ ¬ OR(c, b)) ==> PR(a, b)

theorem OR_imp_OR_imp_PR:

  c. OR(c, a) --> OR(c, b) ==> PR(a, b)

theorem OR_ident:

  a b. (∀c. OR(c, a) <-> OR(c, b)) <-> a = b

theorem Sum_unique:

  [| Sum(a, b, c); Sum(a, b, d) |] ==> c = d

theorem Sum_imp_PR_and_PR:

  Sum(a, b, c) ==> PR(a, c) ∧ PR(b, c)

theorem Sum_sym:

  Sum(a, b, c) ==> Sum(b, a, c)

theorem Sum_refl:

  Sum(a, a, a)

theorem Sum_imp_id:

  Sum(a, a, b) ==> a = b

theorem PR_imp_Sum:

  PR(a, b) ==> Sum(a, b, b)

theorem Diff_unique:

  [| Diff(a, b, c); Diff(a, b, d) |] ==> c = d

theorem Prod_unique:

  [| Prod(a, b, c); Prod(a, b, d) |] ==> c = d

theorem Diff_imp_notPR:

  Diff(a, b, c) ==> ¬ PR(a, b)

theorem notOR_imp_Diff:

  ¬ OR(a, b) ==> Diff(a, b, a)

theorem Diff_imp_PR:

  Diff(a, b, c) ==> PR(c, a)

theorem PR_and_notPR_imp_notPR:

  [| PR(a, b); ¬ PR(c, b) |] ==> ¬ PR(c, a)

theorem PR_and_Diff_impl_Diff_PR:

  [| PR(a, b); Diff(c, b, d) |] ==> ∃e. Diff(c, a, e) ∧ PR(d, e)

theorem UniR_unique:

  [| UniR(a); UniR(b) |] ==> a = b