Theory GEM

section ‹ General Extensional Mereology ›

(*<*)
theory GEM
  imports GMM CEM
begin (*>*)

text ‹ The theory of \emph{general extensional mereology}, also known as \emph{classical extensional
mereology} adds general mereology to extensional mereology.\footnote{For this axiomatization see
cite"varzi_parts_1996" p. 265  and cite"casati_parts_1999" p. 46.} ›

locale GEM = GM + EM +
  assumes sum_eq: "x  y = (THE z. v. O v z  O v x  O v y)" 
  assumes product_eq: 
    "x  y = (THE z. v. P v z  P v x  P v y)"
  assumes difference_eq: 
    "x  y = (THE z. w. P w z = (P w x  ¬ O w y))"
  assumes complement_eq: " x = (THE z. w. P w z  ¬ O w x)"
  assumes universe_eq: "u = (THE x. y. P y x)"
  assumes fusion_eq: "x. F x  
    (σ x. F x) = (THE x. y. O y x  (z. F z  O y z))"
  assumes general_product_eq: "(π x. F x) = (σ x. y. F y  P x y)"

sublocale GEM  GMM
proof
qed

subsection ‹ General Sums  ›

context GEM
begin

lemma fusion_intro: 
"(y. O y z  (x. F x  O y x))  (σ x. F x) = z"
proof -
  assume antecedent: "(y. O y z  (x. F x  O y x))"
  hence "(THE x. y. O y x  (z. F z  O y z)) = z"
  proof (rule the_equality)
    fix a
    assume a: "(y. O y a  (x. F x  O y x))"
    have "x. O x a  O x z"
    proof
      fix b     
      from antecedent have "O b z  (x. F x  O b x)"..
      moreover from a have "O b a  (x. F x  O b x)"..
      ultimately show "O b a  O b z" by (rule ssubst)
    qed
    with overlap_extensionality show "a = z"..
  qed
  moreover from antecedent have "O z z  (x. F x  O z x)"..
  hence "x. F x  O z x" using overlap_reflexivity..
  hence "x. F x" by auto
  hence "(σ x. F x) = (THE x. y. O y x  (z. F z  O y z))"
    by (rule fusion_eq)
  ultimately show "(σ v. F v) = z" by (rule subst)
qed

lemma fusion_idempotence: "(σ x. z = x) = z"
proof -
  have "y. O y z  (x. z = x  O y x)"
  proof
    fix y
    show "O y z  (x. z = x  O y x)"
    proof
      assume "O y z"
      with refl have "z = z  O y z"..
      thus "x. z = x  O y x"..
    next
      assume "x. z = x  O y x"
      then obtain x where x: "z = x  O y x"..
      hence "z = x"..
      moreover from x have "O y x"..
      ultimately show "O y z" by (rule ssubst)
    qed
  qed
  thus "(σ x. z = x) = z"
    by (rule fusion_intro)
qed

text ‹ The whole is the sum of its parts. ›

lemma fusion_absorption: "(σ x. P x z) = z"
proof -
  have "(y. O y z  (x. P x z  O y x))"
  proof
    fix y
    show "O y z  (x. P x z  O y x)"
    proof
      assume "O y z"
      with part_reflexivity have "P z z  O y z"..
      thus "x. P x z  O y x"..
    next
      assume "x. P x z  O y x"
      then obtain x where x: "P x z  O y x"..
      hence "P x z"..
      moreover from x have "O y x"..
      ultimately show "O y z" by (rule overlap_monotonicity)
    qed
  qed
  thus "(σ x. P x z) = z"
    by (rule fusion_intro)
qed

lemma part_fusion: "P w (σ v. P v x)  P w x"
proof -
  assume "P w (σ v. P v x)"
  with fusion_absorption show "P w x" by (rule subst)
qed

lemma fusion_character: 
  "x. F x  (y. O y (σ v. F v)  (x. F x  O y x))"
proof -
  assume "x. F x"
  hence "z. y. O y z  (x. F x  O y x)"
    by (rule fusion)
  then obtain z where z: "y. O y z  (x. F x  O y x)"..
  hence "(σ v. F v) = z " by (rule fusion_intro)
  thus "y. O y (σ v. F v)  (x. F x  O y x)" using z by (rule ssubst)
qed

text ‹ The next lemma characterises fusions in terms of parthood.\footnote{See cite"pontow_note_2004" pp. 202-9.} ›

lemma fusion_part_character: "x. F x  
  (y. P y (σ v. F v)  (w. P w y  (v. F v  O w v)))"
proof -
  assume "(x. F x)"
  hence F: "y. O y (σ v. F v)  (x. F x  O y x)"
    by (rule fusion_character)
  show "y. P y (σ v. F v)  (w. P w y  (v. F v  O w v))"
  proof
    fix y
    show "P y (σ v. F v)  (w. P w y  (v. F v  O w v))"
    proof
      assume "P y (σ v. F v)"
      show "w. P w y  (v. F v  O w v)"
      proof
        fix w
        from F have w: "O w (σ v. F v)  (x. F x  O w x)"..
        show "P w y  (v. F v  O w v)"
        proof
          assume "P w y"
          hence "P w (σ v. F v)" using P y (σ v. F v)
            by (rule part_transitivity)
          hence "O w (σ v. F v)" by (rule part_implies_overlap)
          with w show "x. F x  O w x"..
        qed
      qed
    next
      assume right: "w. P w y  (v. F v  O w v)"
      show "P y (σ v. F v)"
      proof (rule ccontr)
        assume "¬ P y (σ v. F v)"
        hence "v. P v y  ¬ O v (σ v. F v)"
          by (rule strong_supplementation)
        then obtain v where v: "P v y  ¬ O v (σ v. F v)"..
        hence "¬ O v (σ v. F v)"..
        from right have "P v y  (w. F w  O v w)"..
        moreover from v have "P v y"..
        ultimately have "w. F w  O v w"..
        from F have "O v (σ v. F v)  (x. F x  O v x)"..
        hence "O v (σ v. F v)" using w. F w  O v w..
        with ¬ O v (σ v. F v) show "False"..
      qed
    qed
  qed
qed

lemma fusion_part: "F x  P x (σ x. F x)"
proof -
  assume "F x"
  hence "x. F x"..
  hence "y. P y (σ v. F v)  (w. P w y  (v. F v  O w v))"
    by (rule fusion_part_character)
  hence "P x (σ v. F v)  (w. P w x  (v. F v  O w v))"..
  moreover have "w. P w x  (v. F v  O w v)"
  proof
    fix w
    show "P w x  (v. F v  O w v)"
    proof
      assume "P w x"
      hence "O w x" by (rule part_implies_overlap)
      with F x have "F x  O w x"..
      thus "v. F v  O w v"..
    qed
  qed
  ultimately show "P x (σ v. F v)"..
qed

lemma common_part_fusion: 
  "O x y  (w. P w (σ v. (P v x  P v y))  (P w x  P w y))"
proof -
  assume "O x y"
  with overlap_eq have "z. (P z x  P z y)"..
  hence sum: "(w. P w (σ v. (P v x  P v y))  
    (z. P z w  (v. (P v x  P v y)  O z v)))"
    by (rule fusion_part_character)
  show "w. P w (σ v. (P v x  P v y))  (P w x  P w y)"
  proof
    fix w
    from sum have w: "P w (σ v. (P v x  P v y)) 
       (z. P z w  (v. (P v x  P v y)  O z v))"..
    show "P w (σ v. (P v x  P v y))  (P w x  P w y)"
    proof
      assume "P w (σ v. (P v x  P v y))"
      with w have bla: 
        "(z. P z w  (v. (P v x  P v y)  O z v))"..
      show "P w x  P w y" 
      proof
        show "P w x"
        proof (rule ccontr)
          assume "¬ P w x"
          hence "z. P z w  ¬ O z x"
            by (rule strong_supplementation)
          then obtain z where z: "P z w  ¬ O z x"..
          hence "¬ O z x"..
          from bla have "P z w  (v. (P v x  P v y)  O z v)"..
          moreover from z have "P z w"..
          ultimately have "v. (P v x  P v y)  O z v"..
          then obtain v where v: "(P v x  P v y)  O z v"..
          hence "P v x  P v y"..
          hence "P v x"..
          moreover from v have "O z v"..
          ultimately have "O z x"
            by (rule overlap_monotonicity)
          with ¬ O z x show "False"..
        qed
        show "P w y"
        proof (rule ccontr)
          assume "¬ P w y"
          hence "z. P z w  ¬ O z y"
            by (rule strong_supplementation)
          then obtain z where z: "P z w  ¬ O z y"..
          hence "¬ O z y"..
          from bla have "P z w  (v. (P v x  P v y)  O z v)"..
          moreover from z have "P z w"..
          ultimately have "v. (P v x  P v y)  O z v"..
          then obtain v where v: "(P v x  P v y)  O z v"..
          hence "P v x  P v y"..
          hence "P v y"..
          moreover from v have "O z v"..
          ultimately have "O z y"
            by (rule overlap_monotonicity)
          with ¬ O z y show "False"..
        qed
      qed
    next
      assume "P w x  P w y"
      thus "P w (σ v. (P v x  P v y))"
        by (rule fusion_part)
    qed
  qed
qed

theorem product_closure: 
  "O x y  (z. w. P w z  (P w x  P w y))"
proof -
  assume "O x y"
  hence "(w. P w (σ v. (P v x  P v y))  (P w x  P w y))"
    by (rule common_part_fusion)
  thus "z. w. P w z  (P w x  P w y)"..
qed

end

sublocale GEM  CEM
proof
  fix x y
  show "z. w. O w z = (O w x  O w y)" 
    using sum_closure.
  show "x  y = (THE z. v. O v z  O v x  O v y)" 
    using sum_eq.
  show "x  y = (THE z. v. P v z  P v x  P v y)" 
    using product_eq.
  show "O x y  (z. w. P w z = (P w x  P w y))" 
    using product_closure.
qed

context GEM
begin

corollary "O x y  x  y = (σ v. P v x  P v y)"
proof -
  assume "O x y"
  hence "(w. P w (σ v. (P v x  P v y))  (P w x  P w y))"
    by (rule common_part_fusion)
  thus "x  y = (σ v. P v x  P v y)" by (rule product_intro)
qed

lemma disjoint_fusion:
  "w. ¬ O w x  (w. P w (σ z. ¬ O z x)  ¬ O w x)"
proof -
  assume antecedent: "w. ¬ O w x"
  hence "y. O y (σ v. ¬ O v x)  (v. ¬ O v x  O y v)"
    by (rule fusion_character)
  hence x: "O x (σ v. ¬ O v x)  (v. ¬ O v x  O x v)"..
  show "w. P w (σ z. ¬ O z x)  ¬ O w x"
  proof
    fix y
    show "P y (σ z. ¬ O z x)  ¬ O y x"
    proof
      assume "P y (σ z. ¬ O z x)"
      moreover have "¬ O x (σ z. ¬ O z x)"
      proof
        assume "O x (σ z. ¬ O z x)"
        with x have "(v. ¬ O v x  O x v)"..
        then obtain v where v: "¬ O v x  O x v"..
        hence "¬ O v x"..
        from v have "O x v"..
        hence "O v x" by (rule overlap_symmetry)
        with ¬ O v x show "False"..
      qed
      ultimately have "¬ O x y"
        by (rule disjoint_demonotonicity)
      thus "¬ O y x" by (rule disjoint_symmetry)
    next
      assume "¬ O y x"
      thus "P y (σ v. ¬ O v x)"
        by (rule fusion_part)
    qed
  qed
qed

theorem complement_closure: 
  "w. ¬ O w x  (z. w. P w z  ¬ O w x)"
proof -
  assume "(w. ¬ O w x)"
  hence "w. P w (σ z. ¬ O z x)  ¬ O w x"
    by (rule disjoint_fusion)
  thus "z. w. P w z  ¬ O w x"..
qed

end

sublocale GEM  CEMC
proof
  fix x y
  show " x = (THE z. w. P w z  ¬ O w x)" 
    using complement_eq.
  show "(w. ¬ O w x)  (z. w. P w z = (¬ O w x))" 
    using complement_closure.
  show "x  y = (THE z. w. P w z = (P w x  ¬ O w y))" 
    using difference_eq.
  show "u = (THE x. y. P y x)"
    using universe_eq.
qed

context GEM
begin

corollary complement_is_disjoint_fusion: 
  "w. ¬ O w x   x = (σ z. ¬ O z x)"
proof -
  assume "w. ¬ O w x"
  hence "w. P w (σ z. ¬ O z x)  ¬ O w x"
    by (rule disjoint_fusion)
  thus " x = (σ z. ¬ O z x)"
    by (rule complement_intro)
qed

theorem strong_fusion: "x. F x 
  x. (y. F y  P y x)  (y. P y x  (z. F z  O y z))"
proof -
  assume "x. F x"
  have "(y. F y  P y (σ v. F v)) 
     (y. P y (σ v. F v)  (z. F z  O y z))"
  proof
    show "y. F y  P y (σ v. F v)"
    proof
      fix y
      show "F y  P y (σ v. F v)"
      proof
        assume "F y"
        thus "P y (σ v. F v)"
          by (rule fusion_part)
      qed
    qed
  next
    have "(y. P y (σ v. F v)  
      (w. P w y  (v. F v  O w v)))"
      using x. F x by (rule fusion_part_character)
    hence "P (σ v. F v) (σ v. F v)  (w. P w (σ v. F v)  
      (v. F v  O w v))"..
    thus "w. P w (σ v. F v)  (v. F v  O w v)" using part_reflexivity..
  qed
  thus ?thesis..
qed

theorem strong_fusion_eq: "x. F x  (σ x. F x) = 
  (THE x. (y. F y  P y x)  (y. P y x  (z. F z  O y z)))"
proof -
  assume "x. F x"
  have "(THE x. (y. F y  P y x)  (y. P y x  (z. F z  O y z))) = (σ x. F x)" 
  proof (rule the_equality)
    show "(y. F y  P y (σ x. F x))  (y. P y (σ x. F x)  (z. F z  O y z))"
    proof
      show "y. F y  P y (σ x. F x)"
      proof
        fix y
        show "F y  P y (σ x. F x)"
        proof
          assume "F y"
          thus "P y (σ x. F x)"
            by (rule fusion_part)
        qed
      qed
    next
      show "(y. P y (σ x. F x)  (z. F z  O y z))"
      proof
        fix y
        show "P y (σ x. F x)  (z. F z  O y z)"
        proof
          have  "y. P y (σ v. F v)  (w. P w y  (v. F v  O w v))"
            using x. F x by (rule fusion_part_character)
          hence "P y (σ v. F v)  (w. P w y  (v. F v  O w v))"..
          moreover assume "P y (σ x. F x)"
          ultimately have "w. P w y  (v. F v  O w v)"..
          hence "P y y  (v. F v  O y v)"..
          thus "v. F v  O y v" using part_reflexivity..
        qed
      qed
    qed
  next
    fix x
    assume x: "(y. F y  P y x)  (y. P y x  (z. F z  O y z))"
    have "y. O y x  (z. F z  O y z)"
    proof
      fix y
      show "O y x  (z. F z  O y z)"
      proof
        assume "O y x"
        with overlap_eq have "v. P v y  P v x"..
        then obtain v where v: "P v y  P v x"..
        from x have "y. P y x  (z. F z  O y z)"..
        hence "P v x  (z. F z  O v z)"..
        moreover from v have "P v x"..
        ultimately have "z. F z  O v z"..
        then obtain z where z: "F z  O v z"..
        hence "F z"..
        from v have "P v y"..
        moreover from z have "O v z"..
        hence "O z v" by (rule overlap_symmetry)
        ultimately have "O z y" by (rule overlap_monotonicity)
        hence "O y z" by (rule overlap_symmetry)
        with F z have "F z  O y z"..
        thus "z. F z  O y z"..
      next
        assume "z. F z  O y z"
        then obtain z where z: "F z  O y z"..
        from x have "y. F y  P y x"..
        hence "F z  P z x"..
        moreover from z have "F z"..
        ultimately have "P z x"..
        moreover from z have "O y z"..
        ultimately show "O y x"
          by (rule overlap_monotonicity)
      qed
    qed
    hence "(σ x. F x) = x"
      by (rule fusion_intro)
    thus "x = (σ x. F x)"..
  qed
  thus ?thesis..
qed

lemma strong_sum_eq: "x  y = (THE z. (P x z  P y z)  (w. P w z  O w x  O w y))"
proof -
  have "(THE z. (P x z  P y z)  (w. P w z  O w x  O w y)) = x  y"
  proof (rule the_equality)
    show "(P x (x  y)  P y (x  y))  (w. P w (x  y)  O w x  O w y)"
    proof
      show "P x (x  y)  P y (x  y)"
        proof
          show "P x (x  y)" using first_summand_in_sum.
          show "P y (x  y)" using second_summand_in_sum.
        qed
      show "w. P w (x  y)  O w x  O w y"
      proof
        fix w
        show "P w (x  y)  O w x  O w y"
        proof
          assume "P w (x  y)"
          hence "O w (x  y)" by (rule part_implies_overlap)
          with sum_overlap show "O w x  O w y"..
        qed
      qed
    qed
    fix z
    assume z: "(P x z  P y z)  (w. P w z  O w x  O w y)"
    hence "P x z  P y z"..
    have "w. O w z  (O w x  O w y)"
    proof
      fix w
      show "O w z  (O w x  O w y)"
      proof
        assume "O w z"
        with overlap_eq have "v. P v w  P v z"..
        then obtain v where v: "P v w  P v z"..
        hence "P v w"..
        from z have "w. P w z  O w x  O w y"..
        hence "P v z  O v x  O v y"..
        moreover from v have "P v z"..
        ultimately have "O v x  O v y"..
        thus "O w x  O w y"
        proof
          assume "O v x"
          hence "O x v" by (rule overlap_symmetry)
          with P v w have "O x w" by (rule overlap_monotonicity)
          hence "O w x" by (rule overlap_symmetry)
          thus "O w x  O w y"..
        next
          assume "O v y"
          hence "O y v" by (rule overlap_symmetry)
          with P v w have "O y w" by (rule overlap_monotonicity)
          hence "O w y" by (rule overlap_symmetry)
          thus "O w x  O w y"..
        qed
      next
        assume "O w x  O w y"
        thus "O w z"
        proof
          from P x z  P y z have "P x z"..
          moreover assume "O w x"
          ultimately show "O w z"
            by (rule overlap_monotonicity)
        next
          from P x z  P y z have "P y z"..
          moreover assume "O w y"
          ultimately show "O w z"
            by (rule overlap_monotonicity)
        qed
      qed
    qed
    hence "x  y = z" by (rule sum_intro)
    thus "z = x  y"..
  qed
  thus ?thesis..
qed

subsection ‹ General Products ›

lemma general_product_intro: "(y. O y x  (z. (y. F y  P z y)  O y z))  (π x. F x) = x"
proof -
  assume "y. O y x  (z. (y. F y  P z y)  O y z)"
  hence "(σ x. y. F y  P x y) = x" by (rule fusion_intro)
  with general_product_eq show "(π x. F x) = x" by (rule ssubst)
qed

lemma general_product_idempotence: "(π z. z = x) = x"
proof -
  have "y. O y x  (z. (y. y = x  P z y)  O y z)"
    by (meson overlap_eq part_reflexivity part_transitivity)
  thus "(π z. z = x) = x" by (rule general_product_intro)
qed

lemma general_product_absorption: "(π z. P x z) = x"
proof -
  have "y. O y x  (z. (y. P x y  P z y)  O y z)"
    by (meson overlap_eq part_reflexivity part_transitivity)
  thus "(π z. P x z) = x" by (rule general_product_intro)
qed

lemma general_product_character: "z. y. F y  P z y  
  y. O y (π x. F x)  (z. (y. F y  P z y)  O y z)"
proof -
  assume "(z. y. F y  P z y)"
  hence "(x. y. O y x  (z. (y. F y  P z y)  O y z))"
    by (rule fusion)
  then obtain x where x: 
    "y. O y x  (z. (y. F y  P z y)  O y z)"..
  hence "(π x. F x) = x" by (rule general_product_intro)
  thus "(y. O y (π x. F x)  (z. (y. F y  P z y)  O y z))"
    using x by (rule ssubst)
qed

corollary "¬ (x. F x)  u = (π x. F x)"
proof -
  assume antecedent: "¬ (x. F x)"
  have "y. P y (π x. F x)"
  proof
    fix y
    show "P y (π x. F x)"
    proof (rule ccontr)
      assume "¬ P y (π x. F x)"
     hence "z. P z y  ¬ O z (π x. F x)" by (rule strong_supplementation)
      then obtain z where z: "P z y  ¬ O z (π x. F x)"..
      hence "¬ O z (π x. F x)"..
      from antecedent have bla: " y. F y  P z y" by simp 
      hence " v.  y. F y  P v y"..
      hence "(y. O y (π x. F x)  (z. (y. F y  P z y)  O y z))" by (rule general_product_character)
      hence "O z (π x. F x)  (v. (y. F y  P v y)  O z v)"..
      moreover from bla have  "( y. F y  P z y)  O z z" 
        using overlap_reflexivity..
      hence " v. ( y. F y  P v y)  O z v"..
      ultimately have "O z (π x. F x)"..
      with ¬ O z (π x. F x) show "False"..
    qed
  qed
  thus "u = (π x. F x)"
    by (rule universe_intro)
qed

end

subsection ‹ Strong Fusion ›

text ‹ An alternative axiomatization of general extensional mereology adds a stronger version of the
fusion axiom to minimal mereology, with correspondingly stronger definitions of sums and general
sums.\footnote{See cite"tarski_foundations_1983" p. 25. The proofs in this section are adapted
from cite"hovda_what_2009".} ›

locale GEM1 = MM + 
  assumes strong_fusion: "x. F x  x. (y. F y  P y x)  (y. P y x  (z. F z  O y z))"
  assumes strong_sum_eq: "x  y = (THE z. (P x z  P y z)  (w. P w z  O w x  O w y))"
  assumes product_eq: 
    "x  y = (THE z. v. P v z  P v x  P v y)"
  assumes difference_eq: 
    "x  y = (THE z. w. P w z = (P w x  ¬ O w y))"
  assumes complement_eq: " x = (THE z. w. P w z  ¬ O w x)"
  assumes universe_eq: "u = (THE x. y. P y x)"
  assumes strong_fusion_eq:  "x. F x  (σ x. F x) = (THE x. (y. F y  P y x)  (y. P y x  (z. F z  O y z)))"
  assumes general_product_eq: "(π x. F x) = (σ x. y. F y  P x y)"
begin

theorem fusion: 
  "x. φ x  (z. y. O y z  (x. φ x  O y x))"
proof -
  assume "x. φ x"
  hence "x. (y. φ y  P y x)  (y. P y x  (z. φ z  O y z))" by (rule strong_fusion)
  then obtain x where x: 
    "(y. φ y  P y x)  (y. P y x  (z. φ z  O y z))"..
  have "y. O y x  (v. φ v  O y v)"
  proof
    fix y
    show "O y x  (v. φ v  O y v)"
    proof
      assume "O y x"
      with overlap_eq have "z. P z y  P z x"..
      then obtain z where z: "P z y  P z x"..
      hence "P z x"..
      from x have "y. P y x  (v. φ v  O y v)"..
      hence "P z x  (v. φ v  O z v)"..
      hence "v. φ v  O z v" using P z x..
      then obtain v where v: "φ v  O z v"..
      hence "O z v"..
      with overlap_eq have "w. P w z  P w v"..
      then obtain w where w: "P w z  P w v"..
      hence "P w z"..
      moreover from z have "P z y"..
      ultimately have "P w y"
        by (rule part_transitivity)
      moreover from w have "P w v"..
      ultimately have "P w y  P w v"..
      hence "w. P w y  P w v"..
      with overlap_eq have "O y v"..
      from v have "φ v"..
      hence "φ v  O y v" using O y v..
      thus "v. φ v  O y v"..
    next
      assume "v. φ v  O y v"
      then obtain v where v: "φ v  O y v"..
      hence "O y v"..
      with overlap_eq have "z. P z y  P z v"..
      then obtain z where z: "P z y  P z v"..
      hence "P z v"..
      from x have "y. φ y  P y x"..
      hence "φ v  P v x"..
      moreover from v have "φ v"..
      ultimately have "P v x"..
      with P z v have "P z x"
        by (rule part_transitivity)
      from z have "P z y"..
      thus "O y x" using P z x
        by (rule overlap_intro)
    qed
  qed
  thus "(z. y. O y z  (x. φ x  O y x))"..
qed

lemma pair: "v. (w. (w = x  w = y)  P w v)  (w. P w v  (z. (z = x  z = y)  O w z))"
proof -
  have "x = x"..
  hence "x = x  x = y"..
  hence "v. v = x  v = y"..
  thus ?thesis
    by (rule strong_fusion)
qed

lemma or_id: "(v = x  v = y)  O w v  O w x  O w y"
proof -
  assume v: "(v = x  v = y)  O w v"
  hence "O w v"..
  from v have "v = x  v = y"..
  thus "O w x  O w y"
  proof
    assume "v = x"
    hence "O w x" using O w v by (rule subst)
    thus "O w x  O w y"..
  next
    assume "v = y"
    hence "O w y" using O w v by (rule subst)
    thus "O w x  O w y"..
  qed
qed

lemma strong_sum_closure: 
  "z. (P x z  P y z)  (w. P w z  O w x  O w y)"
proof -
  from pair obtain z where z: "(w. (w = x  w = y)  P w z)  (w. P w z  (v. (v = x  v = y)  O w v))"..
  have "(P x z  P y z)  (w. P w z  O w x  O w y)"
  proof
    from z have allw: "w. (w = x  w = y)  P w z"..
    hence "x = x  x = y  P x z"..
    moreover have "x = x  x = y" using refl..
    ultimately have "P x z"..
    from allw have "y = x  y = y  P y z"..
    moreover have "y = x  y = y" using refl..
    ultimately have "P y z"..
    with P x z show "P x z  P y z"..
  next
    show "w. P w z  O w x  O w y"
    proof
      fix w
      show "P w z  O w x  O w y"
      proof
        assume "P w z"
        from z have "w. P w z  (v. (v = x  v = y)  O w v)"..
        hence "P w z  (v. (v = x  v = y)  O w v)"..
        hence "v. (v = x  v = y)  O w v" using P w z..
        then obtain v where v: "(v = x  v = y)  O w v"..
        thus "O w x  O w y" by (rule or_id)
      qed
    qed
  qed
  thus ?thesis..
qed

end 

sublocale GEM1  GMM
proof
  fix x y φ
  show "(x. φ x)  (z. y. O y z  (x. φ x  O y x))" using fusion.
qed

context GEM1
begin

lemma least_upper_bound:
  assumes sf: 
    "((y. F y  P y x)  (y. P y x  (z. F z  O y z)))"
  shows lub: 
      "(y. F y  P y x)  (z. (y. F y  P y z)  P x z)"
proof
 from sf show "y. F y  P y x"..
next
 show "(z. (y. F y  P y z)  P x z)"
 proof
  fix z
  show "(y. F y  P y z)  P x z"
  proof
   assume z: "y. F y  P y z"
   from pair obtain v where v: "(w. (w = x  w = z)  P w v)  (w. P w v  (y. (y = x  y = z)  O w y))"..
   hence left: "(w. (w = x  w = z)  P w v)"..
   hence "(x = x  x = z)  P x v"..
   moreover have "x = x  x = z" using refl..
   ultimately have "P x v"..
   have "z = v"
   proof (rule ccontr)
    assume "z  v"
    from left have "z = x  z = z  P z v"..
    moreover have "z = x  z = z" using refl..
    ultimately have "P z v"..
    hence "P z v  z  v" using z  v..
    with nip_eq have "PP z v"..
    hence "w. P w v  ¬ O w z" by (rule weak_supplementation)
    then obtain w where w: "P w v  ¬ O w z"..
    hence "P w v"..
    from v have right: 
      "w. P w v  (y. (y = x  y = z)  O w y)"..
    hence "P w v  (y. (y = x  y = z)  O w y)"..
    hence "y. (y = x  y = z)  O w y" using P w v..
    then obtain s where s: "(s = x  s = z)  O w s"..
    hence "s = x  s = z"..
    thus "False"
    proof
     assume "s = x"
     moreover from s have "O w s"..
     ultimately have "O w x" by (rule subst)
     with overlap_eq have "t. P t w  P t x"..
     then obtain t where t: "P t w  P t x"..
     hence "P t x"..
     from sf have "(y. P y x  (z. F z  O y z))"..
     hence "P t x  (z. F z  O t z)"..
     hence "z. F z  O t z" using P t x..
     then obtain a where a: "F a  O t a"..
     hence "F a"..
     from sf have ub: "y. F y  P y x"..
     hence "F a  P a x"..
     hence "P a x" using F a..
     moreover from a have "O t a"..
     ultimately have "O t x"
      by (rule overlap_monotonicity)
     from t have "P t w"..
     moreover have "O z t"
     proof -
      from z have "F a  P a z"..
      moreover from a have "F a"..
      ultimately have "P a z"..
      moreover from a have "O t a"..
      ultimately have "O t z"
       by (rule overlap_monotonicity)
      thus "O z t" by (rule overlap_symmetry)
     qed
     ultimately have "O z w"
      by (rule overlap_monotonicity)
     hence "O w z" by (rule overlap_symmetry)
     from w have "¬ O w z"..
     thus "False" using O w z..
    next
     assume "s = z"
     moreover from s have "O w s"..
     ultimately have "O w z" by (rule subst)
     from w have "¬ O w z"..
     thus "False" using O w z..
    qed
   qed
   thus "P x z" using P x v by (rule ssubst)
  qed
 qed
qed

corollary strong_fusion_intro:  "(y. F y  P y x)  (y. P y x  (z. F z  O y z))  (σ x. F x) = x"
proof -
  assume antecedent: "(y. F y  P y x)  (y. P y x  (z. F z  O y z))"
  with least_upper_bound have lubx: 
    "(y. F y  P y x)  (z. (y. F y  P y z)  P x z)".
  from antecedent have "y. P y x  (z. F z  O y z)"..
  hence "P x x  (z. F z  O x z)"..
  hence "z. F z  O x z" using part_reflexivity..
  then obtain z where z: "F z  O x z"..
  hence "F z"..
  hence "z. F z"..
  hence "(σ x. F x) = (THE x. (y. F y  P y x)  (y. P y x  (z. F z  O y z)))" by (rule strong_fusion_eq)
  moreover have "(THE x. (y. F y  P y x)  (y. P y x  (z. F z  O y z))) = x"
  proof (rule the_equality)
    show "(y. F y  P y x)  (y. P y x  (z. F z  O y z))"
      using antecedent.
  next
    fix w
    assume w: 
      "(y. F y  P y w)  (y. P y w  (z. F z  O y z))"
    with least_upper_bound have lubw:
      "(y. F y  P y w)  (z. (y. F y  P y z)  P w z)".
    hence "(z. (y. F y  P y z)  P w z)"..
    hence "(y. F y  P y x)  P w x"..
    moreover from antecedent have "y. F y  P y x"..
    ultimately have "P w x"..
    from lubx have "(z. (y. F y  P y z)  P x z)"..
    hence "(y. F y  P y w)  P x w"..
    moreover from lubw have "(y. F y  P y w)"..
    ultimately have "P x w"..
    with P w x show "w = x"
      by (rule part_antisymmetry)
  qed
  ultimately show "(σ x. F x) = x" by (rule ssubst)
qed

lemma strong_fusion_character: "x. F x  ((y. F y  P y (σ x. F x))  (y. P y (σ x. F x)  (z. F z  O y z)))"
proof -
  assume "x. F x"
  hence "(x. (y. F y  P y x)  (y. P y x  (z. F z  O y z)))" by (rule strong_fusion)
  then obtain x where x: 
    "(y. F y  P y x)  (y. P y x  (z. F z  O y z))"..
  hence "(σ x. F x) = x" by (rule strong_fusion_intro)
  thus ?thesis using x by (rule ssubst)
qed

lemma F_in: "x. F x  (y. F y  P y (σ x. F x))"
proof -
  assume "x. F x"
  hence "((y. F y  P y (σ x. F x))  (y. P y (σ x. F x)  (z. F z  O y z)))" by (rule strong_fusion_character)
 thus "y. F y  P y (σ x. F x)"..
qed

lemma parts_overlap_Fs:
  "x. F x  (y. P y (σ x. F x)  (z. F z  O y z))"
proof -
  assume "x. F x"
  hence "((y. F y  P y (σ x. F x))  (y. P y (σ x. F x)  (z. F z  O y z)))" by (rule strong_fusion_character)
  thus "(y. P y (σ x. F x)  (z. F z  O y z))"..
qed

lemma in_strong_fusion: "P z (σ x. z = x)"
proof -
  have "y. z = y" using refl..
  hence "y. z = y  P y (σ x. z = x)"
    by (rule F_in)
  hence "z = z  P z (σ x. z = x)"..
  thus "P z (σ x. z = x)" using refl..
qed

lemma strong_fusion_in: "P (σ x. z = x) z"
proof -
  have "y. z = y" using refl..
  hence sf:
    "(y. z = y  P y (σ x. z = x))  (y. P y (σ x. z = x)  (v. z = v  O y v))"
    by (rule strong_fusion_character)
  with least_upper_bound have lub: "(y. z = y  P y (σ x. z = x))  (v. (y. z = y  P y v)  P (σ x. z = x) v)".
  hence "(v. (y. z = y  P y v)  P (σ x. z = x) v)"..
  hence "(y. z = y  P y z)  P (σ x. z = x) z"..
  moreover have "(y. z = y  P y z)"
  proof
    fix y
    show "z = y  P y z"
    proof
      assume "z = y"
      thus "P y z" using part_reflexivity by (rule subst)
    qed
  qed
  ultimately show "P (σ x. z = x) z"..
qed

lemma strong_fusion_idempotence: "(σ x. z = x) = z"
 using strong_fusion_in in_strong_fusion by (rule part_antisymmetry)

subsection ‹ Strong Sums ›

lemma pair_fusion: "(P x z  P y z)  (w. P w z  O w x  O w y)  (σ z. z = x  z = y) = z"
proof
 assume z: "(P x z  P y z)  (w. P w z  O w x  O w y)"
  have "(v. v = x  v = y  P v z)  (v. P v z  (z. (z = x  z = y)  O v z))"
 proof
  show "v. v = x  v = y  P v z"
  proof
   fix w
   from z have "P x z  P y z"..
   show "w = x  w = y  P w z"
   proof
    assume "w = x  w = y"
    thus "P w z"
    proof
     assume "w = x"
     moreover from P x z  P y z have "P x z"..
     ultimately show "P w z" by (rule ssubst)
    next
     assume "w = y"
     moreover from P x z  P y z have "P y z"..
     ultimately show "P w z" by (rule ssubst)
    qed
   qed
  qed
  show "v. P v z  (z. (z = x  z = y)  O v z)"
  proof
   fix v
   show "P v z  (z. (z = x  z = y)  O v z)"
   proof
    assume "P v z"
    from z have "w. P w z  O w x  O w y"..
    hence "P v z  O v x  O v y"..
    hence "O v x  O v y" using P v z..
    thus "z. (z = x  z = y)  O v z"
    proof
     assume "O v x"
     have "x = x  x = y" using refl.. 
     hence "(x = x  x = y)  O v x" using O v x..
     thus "z. (z = x  z = y)  O v z"..
    next
     assume "O v y"
     have "y = x  y = y" using refl..
     hence "(y = x  y = y)  O v y" using O v y..
     thus "z. (z = x  z = y)  O v z"..
    qed
   qed
  qed
 qed
  thus "(σ z. z = x  z = y) = z"
    by (rule strong_fusion_intro)
qed

corollary strong_sum_fusion: "x  y = (σ z. z = x  z = y)"
proof -
  have "(THE z. (P x z  P y z)  
    (w. P w z  O w x  O w y)) = (σ z. z = x  z = y)"
  proof (rule the_equality)
    have "x = x  x = y" using refl..
    hence exz: "z. z = x  z = y"..
    hence allw: "(w. w = x  w = y  P w (σ z. z = x  z = y))"
      by (rule F_in)
    show "(P x (σ z. z = x  z = y)  P y (σ z. z = x  z = y))  
      (w. P w (σ z. z = x  z = y)  O w x  O w y)"
    proof
      show "(P x (σ z. z = x  z = y)  P y (σ z. z = x  z = y))"
      proof
        from allw have "x = x  x = y  P x (σ z. z = x  z = y)"..
        thus "P x (σ z. z = x  z = y)" 
          using x = x  x = y..
      next
        from allw have "y = x  y = y  P y (σ z. z = x  z = y)"..
        moreover have "y = x  y = y" 
          using refl..
        ultimately show "P y (σ z. z = x  z = y)"..
      qed
    next
      show "w. P w (σ z. z = x  z = y)  O w x  O w y"
      proof
        fix w
        show "P w (σ z. z = x  z = y)  O w x  O w y"
        proof
          have "v. P v (σ z. z = x  z = y)  (z. (z = x  z = y)  O v z)" using exz by (rule parts_overlap_Fs)
          hence "P w (σ z. z = x  z = y)  (z. (z = x  z = y)  O w z)"..
          moreover assume "P w (σ z. z = x  z = y)"
          ultimately have "(z. (z = x  z = y)  O w z)"..
          then obtain z where z: "(z = x  z = y)  O w z"..
          thus "O w x  O w y" by (rule or_id)
        qed
      qed
    qed
  next
    fix z
    assume z: "(P x z  P y z)  (w. P w z  O w x  O w y)"
    with pair_fusion have "(σ z. z = x  z = y) = z"..
    thus "z = (σ z. z = x  z = y)"..
  qed
  with strong_sum_eq show "x  y = (σ z. z = x  z = y)" 
    by (rule ssubst)
qed

corollary strong_sum_intro: 
  "(P x z  P y z)  (w. P w z  O w x  O w y)  x  y = z"
proof
  assume z: "(P x z  P y z)  (w. P w z  O w x  O w y)"
  with pair_fusion have "(σ z. z = x  z = y) = z"..
  with strong_sum_fusion show "(x  y) = z" 
    by (rule ssubst)
qed

corollary strong_sum_character: "(P x (x  y)  P y (x  y))  (w. P w (x  y)  O w x  O w y)"
proof -
  from strong_sum_closure obtain z where z: 
    "(P x z  P y z)  (w. P w z  O w x  O w y)"..
 with strong_sum_intro have "x  y = z"..
 thus ?thesis using z by (rule ssubst)
qed

corollary summands_in: "(P x (x  y)  P y (x  y))"
  using strong_sum_character..

corollary first_summand_in: "P x (x  y)" using summands_in..

corollary second_summand_in: "P y (x  y)" using summands_in..

corollary sum_part_overlap: "(w. P w (x  y)  O w x  O w y)" using strong_sum_character..

lemma strong_sum_absorption: "y = (x  y)  P x y"
proof -
 assume "y = (x  y)"
 thus "P x y" using first_summand_in by (rule ssubst)
qed

theorem strong_supplementation: "¬ P x y  (z. P z x  ¬ O z y)"
proof -
 assume "¬ P x y"
 have "¬ (z. P z x  O z y)"
 proof
  assume z: "z. P z x  O z y"
  have "(v. y = v  P v (x  y))  
    (v. P v (x  y)  (z. y = z  O v z))"
  proof
   show "v. y = v  P v (x  y)"
   proof
    fix v
    show "y = v  P v (x  y)"
    proof
     assume "y = v"
     thus "P v (x  y)" 
       using second_summand_in by (rule subst)
    qed
   qed
   show "v. P v (x  y)  (z. y = z  O v z)"
   proof
    fix v
    show "P v (x  y)  (z. y = z  O v z)"
    proof
     assume "P v (x  y)"
     moreover from sum_part_overlap have
       "P v (x  y)  O v x  O v y"..
     ultimately have "O v x  O v y" by (rule rev_mp)
     hence "O v y"
     proof
      assume "O v x"
      with overlap_eq have "w. P w v  P w x"..
      then obtain w where w: "P w v  P w x"..
      from z have "P w x  O w y"..
      moreover from w have "P w x"..
      ultimately have "O w y"..
      with overlap_eq have "t. P t w  P t y"..
      then obtain t where t: "P t w  P t y"..
      hence "P t w"..
      moreover from w have "P w v"..
      ultimately have "P t v"
        by (rule part_transitivity)
      moreover from t have "P t y"..
      ultimately show "O v y"
        by (rule overlap_intro)
     next
      assume "O v y"
      thus "O v y".
     qed
     with refl have "y = y  O v y"..
     thus "z. y = z  O v z"..
    qed
   qed
  qed
  hence  "(σ z. y = z) = (x  y)" by (rule strong_fusion_intro)
  with strong_fusion_idempotence have "y = x  y" by (rule subst)
  hence "P x y" by (rule strong_sum_absorption)
  with ¬ P x y show "False"..
 qed
 thus "z. P z x  ¬ O z y" by simp
qed

lemma sum_character: "v. O v (x  y)  (O v x  O v y)"
proof
  fix v
  show "O v (x  y)  (O v x  O v y)"
  proof
    assume "O v (x  y)"
    with overlap_eq have "w. P w v  P w (x  y)"..
    then obtain w where w: "P w v  P w (x  y)"..
    hence "P w v"..
    have "P w (x  y)  O w x  O w y" using sum_part_overlap..
    moreover from w have "P w (x  y)"..
    ultimately have "O w x  O w y"..
    thus "O v x  O v y"
    proof
      assume "O w x"
      hence "O x w"
        by (rule overlap_symmetry)
      with P w v have "O x v"
        by (rule overlap_monotonicity)
      hence "O v x"
        by (rule overlap_symmetry)
      thus "O v x  O v y"..
    next
      assume "O w y"
      hence "O y w"
        by (rule overlap_symmetry)
      with P w v have "O y v"
        by (rule overlap_monotonicity)
      hence "O v y" by (rule overlap_symmetry)
      thus "O v x  O v y"..
    qed
  next
    assume "O v x  O v y"
    thus "O v (x  y)"
    proof
      assume "O v x"
      with overlap_eq have "w. P w v  P w x"..
      then obtain w where w: "P w v  P w x"..
      hence "P w v"..
      moreover from w have "P w x"..
      hence "P w (x  y)" using first_summand_in
        by (rule part_transitivity)
      ultimately show "O v (x  y)"
        by (rule overlap_intro)
    next
      assume "O v y"
      with overlap_eq have "w. P w v  P w y"..
      then obtain w where w: "P w v  P w y"..
      hence "P w v"..
      moreover from w have "P w y"..
      hence "P w (x  y)" using second_summand_in
        by (rule part_transitivity)
      ultimately show "O v (x  y)"
        by (rule overlap_intro)
    qed
  qed
qed

lemma sum_eq: "x  y = (THE z. v. O v z = (O v x  O v y))"
proof -
  have "(THE z. v. O v z  (O v x  O v y)) = x  y"
  proof (rule the_equality)
    show "v. O v (x  y)  (O v x  O v y)" using sum_character.
  next
    fix z
    assume z: "v. O v z  (O v x  O v y)"
    have "(P x z  P y z)  (w. P w z  O w x  O w y)"
    proof
      show "P x z  P y z"
      proof
        show "P x z"
        proof (rule ccontr)
          assume "¬ P x z"
          hence "v. P v x  ¬ O v z"
            by (rule strong_supplementation)
          then obtain v where v: "P v x  ¬ O v z"..
          hence "¬ O v z"..
          from z have "O v z  (O v x  O v y)"..
          moreover from v have "P v x"..
          hence "O v x" by (rule part_implies_overlap)
          hence "O v x  O v y"..
          ultimately have "O v z"..
          with ¬ O v z show "False"..
        qed
      next
        show "P y z"
        proof (rule ccontr)
          assume "¬ P y z"
          hence "v. P v y  ¬ O v z"
            by (rule strong_supplementation)
          then obtain v where v: "P v y  ¬ O v z"..
          hence "¬ O v z"..
          from z have "O v z  (O v x  O v y)"..
          moreover from v have "P v y"..
          hence "O v y" by (rule part_implies_overlap)
          hence "O v x  O v y"..
          ultimately have "O v z"..
          with ¬ O v z show "False"..
        qed
      qed
      show "w. P w z  (O w x  O w y)"
      proof
        fix w
        show "P w z  (O w x  O w y)"
        proof
          from z have "O w z  O w x  O w y"..
          moreover assume "P w z"
          hence "O w z" by (rule part_implies_overlap)
          ultimately show "O w x  O w y"..
        qed
      qed
    qed
    with strong_sum_intro have "x  y = z"..
    thus "z = x  y"..
  qed
  thus ?thesis..
qed

theorem fusion_eq: "x. F x 
  (σ x. F x) = (THE x. y. O y x  (z. F z  O y z))"
proof -
  assume "x. F x"
  hence bla: "y. P y (σ x. F x)  (z. F z  O y z)"
    by (rule parts_overlap_Fs)
  have "(THE x. y. O y x  (z. F z  O y z)) = (σ x. F x)"
  proof (rule the_equality)
    show "y. O y (σ x. F x)  (z. F z  O y z)"
    proof
      fix y
      show "O y (σ x. F x)  (z. F z  O y z)"
      proof
        assume "O y (σ x. F x)"
        with overlap_eq have "v. P v y  P v (σ x. F x)"..
        then obtain v where v: "P v y  P v (σ x. F x)"..
        hence "P v y"..
        from bla have "P v (σ x. F x)  (z. F z  O v z)"..
        moreover from v have "P v (σ x. F x)"..
        ultimately have "(z. F z  O v z)"..
        then obtain z where z: "F z  O v z"..
        hence "F z"..
        moreover from z have "O v z"..
        hence "O z v" by (rule overlap_symmetry)
        with P v y have "O z y" by