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