section ‹ Introduction ›

(*<*)
theory PM
  imports Main
begin
(*>*)

text ‹ In this paper, we use Isabelle/HOL to verify some elementary theorems and alternative axiomatizations
  classical extensional mereology, as well as some of its weaker subtheories.\footnote{For similar
  see cite‹"sen_computational_2017"› and cite‹"bittner_formal_2018"›.} We mostly follow the
  from cite‹"simons_parts:_1987"›, cite‹"varzi_parts_1996"› and cite‹"casati_parts_1999"›,
  some important corrections from cite‹"pontow_note_2004"› and cite‹"hovda_what_2009"› as well as
  detailed proofs adapted from cite‹"pietruszczak_metamereology_2018"›.\footnote{For help with
  project I am grateful to Zach Barnett, Sam Baron, Bob Beddor, Olivier Danvy, Mark Goh,
  Joven Joaquin, Wang-Yen Lee, Kee Wei Loo, Bruno Woltzenlogel Paleo, Michael Pelczar, Hsueh Qu,
  Podgorski, Divyanshu Sharma, Manikaran Singh, Neil Sinhababu, Weng-Hong Tang and Zhang Jiang.} ›

text ‹ We will use the following notation throughout.\footnote{See cite‹"simons_parts:_1987"› pp. 99-100
  a helpful comparison of alternative notations.} ›

typedecl i
consts part :: "i → i → bool" (‹P›)
consts overlap :: "i → i → bool" (‹O›)
consts proper_part :: "i → i → bool" (‹PP›)
consts sum :: "i → i → i" (infix ‹⊕› 52)
consts product :: "i → i → i" (infix ‹⊗› 53)
consts difference :: "i → i → i" (infix ‹⊖› 51)
consts complement:: "i → i" (‹←-›)
consts universe :: "i" (‹u›)
consts general_sum :: "(i → bool) → i" (binder ‹σ› 9)
consts general_product :: "(i → bool) → i" (binder ‹π› [8] 9)

section ‹ Premereology ›

text ‹ The theory of \emph{premereology} assumes parthood is reflexive and transitive.\footnote{
  discussion of reflexivity see cite‹"kearns_can_2011"›. For transitivity see cite‹"varzi_note_2006"›.}
  other words, parthood is assumed to be a partial ordering relation.\footnote{Hence the name \emph{premereology},
  cite‹"parsons_many_2014"› p. 6.} Overlap is defined as common parthood.\footnote{See
 cite‹"simons_parts:_1987"› p. 28, cite‹"varzi_parts_1996"› p. 261 and cite‹"casati_parts_1999"› p. 36. } ›

locale PM =
  assumes part_reflexivity: "P x x"
  assumes part_transitivity : "P x y ==> P y z ==> P x z"
  assumes overlap_eq: "O x y ⟷ (∃ z. P z x ∧ P z y)"
begin

subsection ‹ Parthood ›

lemma identity_implies_part : "x = y ==> P x y"
proof -
  assume "x = y"
  moreover have "P x x" by (rule part_reflexivity)
  ultimately show "P x y" by (rule subst)
qed

subsection ‹ Overlap ›

lemma overlap_intro: "P z x ==> P z y ==> O x y"
proof-
  assume "P z x"
  moreover assume "P z y"
  ultimately have "P z x ∧ P z y"..
  hence "∃ z. P z x ∧ P z y"..
  with overlap_eq show "O x y"..
qed

lemma part_implies_overlap: "P x y ==> O x y"
proof -
  assume "P x y"
  with part_reflexivity have "P x x ∧ P x y"..
  hence "∃ z. P z x ∧ P z y"..
  with overlap_eq show "O x y"..
qed

lemma overlap_reflexivity: "O x x"
proof -
  have "P x x ∧ P x x" using part_reflexivity part_reflexivity..
  hence "∃ z. P z x ∧ P z x"..
  with overlap_eq show "O x x"..
qed

lemma overlap_symmetry: "O x y ==> O y x"
proof-
  assume "O x y"
  with overlap_eq have "∃ z. P z x ∧ P z y"..
  hence "∃ z. P z y ∧ P z x" by auto
  with overlap_eq show "O y x"..
qed

lemma overlap_monotonicity: "P x y ==> O z x ==> O z y"
proof -
  assume "P x y"
  assume "O z x"
  with overlap_eq have "∃ v. P v z ∧ P v x"..
  then obtain v where v: "P v z ∧ P v x"..
  hence "P v z"..
  moreover from v have "P v x"..
  hence "P v y" using ‹P x y› by (rule part_transitivity)
  ultimately have "P v z ∧ P v y"..
  hence "∃ v. P v z ∧ P v y"..
  with overlap_eq show "O z y"..
qed

text ‹ The next lemma is from cite‹"hovda_what_2009"› p. 66. ›

lemma overlap_lemma: "∃x. (P x y ∧ O z x) ⟶ O y z"
proof -
  fix x
  have "P x y ∧ O z x ⟶ O y z"
  proof
    assume antecedent: "P x y ∧ O z x"
    hence "O z x"..
    with overlap_eq have "∃v. P v z ∧ P v x"..
    then obtain v where v: "P v z ∧ P v x"..
    hence "P v x"..
    moreover from antecedent have "P x y"..
    ultimately have "P v y" by (rule part_transitivity)
    moreover from v have "P v z"..
    ultimately have "P v y ∧ P v z"..
    hence "∃v. P v y ∧ P v z"..
    with overlap_eq show "O y z"..
  qed
  thus "∃x. (P x y ∧ O z x) ⟶ O y z"..
qed

subsection ‹ Disjointness ›

lemma disjoint_implies_distinct: "¬ O x y ==> x ≠ y"
proof -
  assume "¬ O x y"
  show "x ≠ y"
  proof
    assume "x = y"
    hence "¬ O y y" using ‹¬ O x y› by (rule subst)
    thus "False" using overlap_reflexivity..
  qed
qed

lemma disjoint_implies_not_part: "¬ O x y ==> ¬ P x y"
proof -
  assume "¬ O x y"
  show "¬ P x y"
  proof
    assume "P x y"
    hence "O x y" by (rule part_implies_overlap)
    with ‹¬ O x y› show "False"..
  qed
qed

lemma disjoint_symmetry: "¬ O x y ==> ¬ O y x"
proof -
  assume "¬ O x y"
  show "¬ O y x"
  proof
    assume "O y x"
    hence "O x y" by (rule overlap_symmetry)
    with ‹¬ O x y› show "False"..
  qed
qed

lemma disjoint_demonotonicity: "P x y ==> ¬ O z y ==> ¬ O z x"
proof -
  assume "P x y"
  assume "¬ O z y"
  show "¬ O z x"
  proof
    assume "O z x"
    with ‹P x y› have "O z y"
      by (rule overlap_monotonicity)
    with ‹¬ O z y› show "False"..
  qed
qed

end

(*<*)end(*>*)