section ‹ Closed Extensional Mereology › (*<*) theory CEM imports CM EM begin (*>*) text ‹ Closed extensional mereology combines closed mereology with extensional mereology.\footnote{ See \<^cite>‹"varzi_parts_1996"› p. 263 and \<^cite>‹"casati_parts_1999"› p. 43.} › locale CEM = CM + EM text ‹ Likewise, closed minimal mereology combines closed mereology with minimal mereology.\footnote{ See \<^cite>‹"casati_parts_1999"› p. 43.} › locale CMM = CM + MM text ‹ But famously closed minimal mereology and closed extensional mereology are the same theory, because in closed minimal mereology product closure and weak supplementation entail strong supplementation.\footnote{See \<^cite>‹"simons_parts:_1987"› p. 31 and \<^cite>‹"casati_parts_1999"› p. 44.} › sublocale CMM ⊆ CEM proof fix x y show strong_supplementation: "¬ P x y ⟹ (∃ z. P z x ∧ ¬ O z y)" proof - assume "¬ P x y" show "∃ z. P z x ∧ ¬ O z y" proof cases assume "O x y" with ‹¬ P x y› have "¬ P x y ∧ O x y".. hence "PP (x ⊗ y) x" by (rule nonpart_implies_proper_product) hence "∃ z. P z x ∧ ¬ O z (x ⊗ y)" by (rule weak_supplementation) then obtain z where z: "P z x ∧ ¬ O z (x ⊗ y)".. hence "¬ O z y" by (rule disjoint_from_second_factor) moreover from z have "P z x".. hence "P z x ∧ ¬ O z y" using ‹¬ O z y›.. thus "∃ z. P z x ∧ ¬ O z y".. next assume "¬ O x y" with part_reflexivity have "P x x ∧ ¬ O x y".. thus "(∃ z. P z x ∧ ¬ O z y)".. qed qed qed sublocale CEM ⊆ CMM.. subsection ‹ Sums › context CEM begin lemma sum_intro: "(∀ w. O w z ⟷ (O w x ∨ O w y)) ⟹ x ⊕ y = z" proof - assume sum: "∀ w. O w z ⟷ (O w x ∨ O w y)" hence "(THE v. ∀ w. O w v ⟷ (O w x ∨ O w y)) = z" proof (rule the_equality) fix a assume a: "∀ w. O w a ⟷ (O w x ∨ O w y)" have "∀ w. O w a ⟷ O w z" proof fix w from sum have "O w z ⟷ (O w x ∨ O w y)".. moreover from a have "O w a ⟷ (O w x ∨ O w y)".. ultimately show "O w a ⟷ O w z" by (rule ssubst) qed with overlap_extensionality show "a = z".. qed thus "x ⊕ y = z" using sum_eq by (rule subst) qed lemma sum_idempotence: "x ⊕ x = x" proof - have "∀ w. O w x ⟷ (O w x ∨ O w x)" proof fix w show "O w x ⟷ (O w x ∨ O w x)" proof (rule iffI) assume "O w x" thus "O w x ∨ O w x".. next assume "O w x ∨ O w x" thus "O w x" by (rule disjE) qed qed thus "x ⊕ x = x" by (rule sum_intro) qed lemma part_sum_identity: "P y x ⟹ x ⊕ y = x" proof - assume "P y x" have "∀ w. O w x ⟷ (O w x ∨ O w y)" proof fix w show "O w x ⟷ (O w x ∨ O w y)" proof assume "O w x" thus "O w x ∨ O w y".. next assume "O w x ∨ O w y" thus "O w x" proof assume "O w x" thus "O w x". next assume "O w y" with ‹P y x› show "O w x" by (rule overlap_monotonicity) qed qed qed thus "x ⊕ y = x" by (rule sum_intro) qed lemma sum_character: "∀ w. O w (x ⊕ y) ⟷ (O w x ∨ O w y)" proof - from sum_closure have "(∃ z. ∀ w. O w z ⟷ (O w x ∨ O w y))". then obtain a where a: "∀ w. O w a ⟷ (O w x ∨ O w y)".. hence "x ⊕ y = a" by (rule sum_intro) thus "∀ w. O w (x ⊕ y) ⟷ (O w x ∨ O w y)" using a by (rule ssubst) qed lemma sum_overlap: "O w (x ⊕ y) ⟷ (O w x ∨ O w y)" using sum_character.. lemma sum_part_character: "P w (x ⊕ y) ⟷ (∀ v. O v w ⟶ O v x ∨ O v y)" proof assume "P w (x ⊕ y)" show "∀ v. O v w ⟶ O v x ∨ O v y" proof fix v show "O v w ⟶ O v x ∨ O v y" proof assume "O v w" with ‹P w (x ⊕ y)› have "O v (x ⊕ y)" by (rule overlap_monotonicity) with sum_overlap show "O v x ∨ O v y".. qed qed next assume right: "∀ v. O v w ⟶ O v x ∨ O v y" have "∀ v. O v w ⟶ O v (x ⊕ y)" proof fix v from right have "O v w ⟶ O v x ∨ O v y".. with sum_overlap show "O v w ⟶ O v (x ⊕ y)" by (rule ssubst) qed with part_overlap_eq show "P w (x ⊕ y)".. qed lemma sum_commutativity: "x ⊕ y = y ⊕ x" proof - from sum_character have "∀ w. O w (y ⊕ x) ⟷ O w y ∨ O w x". hence "∀ w. O w (y ⊕ x) ⟷ O w x ∨ O w y" by metis thus "x ⊕ y = y ⊕ x" by (rule sum_intro) qed lemma first_summand_overlap: "O z x ⟹ O z (x ⊕ y)" proof - assume "O z x" hence "O z x ∨ O z y".. with sum_overlap show "O z (x ⊕ y)".. qed lemma first_summand_disjointness: "¬ O z (x ⊕ y) ⟹ ¬ O z x" proof - assume "¬ O z (x ⊕ y)" show "¬ O z x" proof assume "O z x" hence "O z (x ⊕ y)" by (rule first_summand_overlap) with ‹¬ O z (x ⊕ y)› show "False".. qed qed lemma first_summand_in_sum: "P x (x ⊕ y)" proof - have "∀ w. O w x ⟶ O w (x ⊕ y)" proof fix w show "O w x ⟶ O w (x ⊕ y)" proof assume "O w x" thus "O w (x ⊕ y)" by (rule first_summand_overlap) qed qed with part_overlap_eq show "P x (x ⊕ y)".. qed lemma common_first_summand: "P x (x ⊕ y) ∧ P x (x ⊕ z)" proof from first_summand_in_sum show "P x (x ⊕ y)". from first_summand_in_sum show "P x (x ⊕ z)". qed lemma common_first_summand_overlap: "O (x ⊕ y) (x ⊕ z)" proof - from first_summand_in_sum have "P x (x ⊕ y)". moreover from first_summand_in_sum have "P x (x ⊕ z)". ultimately have "P x (x ⊕ y) ∧ P x (x ⊕ z)".. hence "∃ v. P v (x ⊕ y) ∧ P v (x ⊕ z)".. with overlap_eq show ?thesis.. qed lemma second_summand_overlap: "O z y ⟹ O z (x ⊕ y)" proof - assume "O z y" from sum_character have "O z (x ⊕ y) ⟷ (O z x ∨ O z y)".. moreover from ‹O z y› have "O z x ∨ O z y".. ultimately show "O z (x ⊕ y)".. qed lemma second_summand_disjointness: "¬ O z (x ⊕ y) ⟹ ¬ O z y" proof - assume "¬ O z (x ⊕ y)" show "¬ O z y" proof assume "O z y" hence "O z (x ⊕ y)" by (rule second_summand_overlap) with ‹¬ O z (x ⊕ y)› show False.. qed qed lemma second_summand_in_sum: "P y (x ⊕ y)" proof - have "∀ w. O w y ⟶ O w (x ⊕ y)" proof fix w show "O w y ⟶ O w (x ⊕ y)" proof assume "O w y" thus "O w (x ⊕ y)" by (rule second_summand_overlap) qed qed with part_overlap_eq show "P y (x ⊕ y)".. qed lemma second_summands_in_sums: "P y (x ⊕ y) ∧ P v (z ⊕ v)" proof show "P y (x ⊕ y)" using second_summand_in_sum. show "P v (z ⊕ v)" using second_summand_in_sum. qed lemma disjoint_from_sum: "¬ O z (x ⊕ y) ⟷ ¬ O z x ∧ ¬ O z y" proof - from sum_character have "O z (x ⊕ y) ⟷ (O z x ∨ O z y)".. thus ?thesis by simp qed lemma summands_part_implies_sum_part: "P x z ∧ P y z ⟹ P (x ⊕ y) z" proof - assume antecedent: "P x z ∧ P y z" have "∀ w. O w (x ⊕ y) ⟶ O w z" proof fix w have w: "O w (x ⊕ y) ⟷ (O w x ∨ O w y)" using sum_character.. show "O w (x ⊕ y) ⟶ O w z" proof assume "O w (x ⊕ y)" with w have "O w x ∨ O w y".. thus "O w z" proof from antecedent have "P x z".. moreover assume "O w x" ultimately show "O w z" by (rule overlap_monotonicity) next from antecedent have "P y z".. moreover assume "O w y" ultimately show "O w z" by (rule overlap_monotonicity) qed qed qed with part_overlap_eq show "P (x ⊕ y) z".. qed lemma sum_part_implies_summands_part: "P (x ⊕ y) z ⟹ P x z ∧ P y z" proof - assume antecedent: "P (x ⊕ y) z" show "P x z ∧ P y z" proof from first_summand_in_sum show "P x z" using antecedent by (rule part_transitivity) next from second_summand_in_sum show "P y z" using antecedent by (rule part_transitivity) qed qed lemma in_second_summand: "P z (x ⊕ y) ∧ ¬ O z x ⟹ P z y" proof - assume antecedent: "P z (x ⊕ y) ∧ ¬ O z x" hence "P z (x ⊕ y)".. show "P z y" proof (rule ccontr) assume "¬ P z y" hence "∃ v. P v z ∧ ¬ O v y" by (rule strong_supplementation) then obtain v where v: "P v z ∧ ¬ O v y".. hence "¬ O v y".. from v have "P v z".. hence "P v (x ⊕ y)" using ‹P z (x ⊕ y)› by (rule part_transitivity) hence "O v (x ⊕ y)" by (rule part_implies_overlap) from sum_character have "O v (x ⊕ y) ⟷ O v x ∨ O v y".. hence "O v x ∨ O v y" using ‹O v (x ⊕ y)›.. thus "False" proof (rule disjE) from antecedent have "¬ O z x".. moreover assume "O v x" hence "O x v" by (rule overlap_symmetry) with ‹P v z› have "O x z" by (rule overlap_monotonicity) hence "O z x" by (rule overlap_symmetry) ultimately show "False".. next assume "O v y" with ‹¬ O v y› show "False".. qed qed qed lemma disjoint_second_summands: "P v (x ⊕ y) ∧ P v (x ⊕ z) ⟹ ¬ O y z ⟹ P v x" proof - assume antecedent: "P v (x ⊕ y) ∧ P v (x ⊕ z)" hence "P v (x ⊕ z)".. assume "¬ O y z" show "P v x" proof (rule ccontr) assume "¬ P v x" hence "∃ w. P w v ∧ ¬ O w x" by (rule strong_supplementation) then obtain w where w: "P w v ∧ ¬ O w x".. hence "¬ O w x".. from w have "P w v".. moreover from antecedent have "P v (x ⊕ z)".. ultimately have "P w (x ⊕ z)" by (rule part_transitivity) hence "P w (x ⊕ z) ∧ ¬ O w x" using ‹¬ O w x›.. hence "P w z" by (rule in_second_summand) from antecedent have "P v (x ⊕ y)".. with ‹P w v› have "P w (x ⊕ y)" by (rule part_transitivity) hence "P w (x ⊕ y) ∧ ¬ O w x" using ‹¬ O w x›.. hence "P w y" by (rule in_second_summand) hence "P w y ∧ P w z" using ‹P w z›.. hence "∃ w. P w y ∧ P w z".. with overlap_eq have "O y z".. with ‹¬ O y z› show "False".. qed qed lemma right_associated_sum: "O w (x ⊕ (y ⊕ z)) ⟷ O w x ∨ (O w y ∨ O w z)" proof - from sum_character have "O w (y ⊕ z) ⟷ O w y ∨ O w z".. moreover from sum_character have "O w (x ⊕ (y ⊕ z)) ⟷ (O w x ∨ O w (y ⊕ z))".. ultimately show ?thesis by (rule subst) qed lemma left_associated_sum: "O w ((x ⊕ y) ⊕ z) ⟷ (O w x ∨ O w y) ∨ O w z" proof - from sum_character have "O w (x ⊕ y) ⟷ (O w x ∨ O w y)".. moreover from sum_character have "O w ((x ⊕ y) ⊕ z) ⟷ O w (x ⊕ y) ∨ O w z".. ultimately show ?thesis by (rule subst) qed theorem sum_associativity: "x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z" proof - have "∀ w. O w (x ⊕ (y ⊕ z)) ⟷ O w ((x ⊕ y) ⊕ z)" proof fix w have "O w (x ⊕ (y ⊕ z)) ⟷ (O w x ∨ O w y) ∨ O w z" using right_associated_sum by simp with left_associated_sum show "O w (x ⊕ (y ⊕ z)) ⟷ O w ((x ⊕ y) ⊕ z)" by (rule ssubst) qed with overlap_extensionality show "x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z".. qed subsection ‹ Distributivity › text ‹ The proofs in this section are adapted from \<^cite>‹"pietruszczak_metamereology_2018"› pp. 102-4. › lemma common_summand_in_product: "P x ((x ⊕ y) ⊗ (x ⊕ z))" using common_first_summand by (rule common_part_in_product) lemma product_in_first_summand: "¬ O y z ⟹ P ((x ⊕ y) ⊗ (x ⊕ z)) x" proof - assume "¬ O y z" have "∀ v. P v ((x ⊕ y) ⊗ (x ⊕ z)) ⟶ P v x" proof fix v show "P v ((x ⊕ y) ⊗ (x ⊕ z)) ⟶ P v x" proof assume "P v ((x ⊕ y) ⊗ (x ⊕ z))" with common_first_summand_overlap have "P v (x ⊕ y) ∧ P v (x ⊕ z)" by (rule product_part_in_factors) thus "P v x" using ‹¬ O y z› by (rule disjoint_second_summands) qed qed hence "P ((x ⊕ y) ⊗ (x ⊕ z)) ((x ⊕ y) ⊗ (x ⊕ z)) ⟶ P ((x ⊕ y) ⊗ (x ⊕ z)) x".. thus "P ((x ⊕ y) ⊗ (x ⊕ z)) x" using part_reflexivity.. qed lemma product_is_first_summand: "¬ O y z ⟹ (x ⊕ y) ⊗ (x ⊕ z) = x" proof - assume "¬ O y z" hence "P ((x ⊕ y) ⊗ (x ⊕ z)) x" by (rule product_in_first_summand) thus "(x ⊕ y) ⊗ (x ⊕ z) = x" using common_summand_in_product by (rule part_antisymmetry) qed lemma sum_over_product_left: "O y z ⟹ P (x ⊕ (y ⊗ z)) ((x ⊕ y) ⊗ (x ⊕ z))" proof - assume "O y z" hence "P (y ⊗ z) ((x ⊕ y) ⊗ (x ⊕ z))" using second_summands_in_sums by (rule part_product_in_whole_product) with common_summand_in_product have "P x ((x ⊕ y) ⊗ (x ⊕ z)) ∧ P (y ⊗ z) ((x ⊕ y) ⊗ (x ⊕ z))".. thus "P (x ⊕ (y ⊗ z)) ((x ⊕ y) ⊗ (x ⊕ z))" by (rule summands_part_implies_sum_part) qed lemma sum_over_product_right: "O y z ⟹ P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))" proof - assume "O y z" show "P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))" proof (rule ccontr) assume "¬ P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))" hence "∃ v. P v ((x ⊕ y) ⊗ (x ⊕ z)) ∧ ¬ O v (x ⊕ (y ⊗ z))" by (rule strong_supplementation) then obtain v where v: "P v ((x ⊕ y) ⊗ (x ⊕ z)) ∧ ¬ O v (x ⊕ (y ⊗ z))".. hence " ¬ O v (x ⊕ (y ⊗ z))".. with disjoint_from_sum have vd: "¬ O v x ∧ ¬ O v (y ⊗ z)".. hence "¬ O v (y ⊗ z)".. from vd have "¬ O v x".. from v have "P v ((x ⊕ y) ⊗ (x ⊕ z))".. with common_first_summand_overlap have vs: "P v (x ⊕ y) ∧ P v (x ⊕ z)" by (rule product_part_in_factors) hence "P v (x ⊕ y)".. hence "P v (x ⊕ y) ∧ ¬ O v x" using ‹¬ O v x›.. hence "P v y" by (rule in_second_summand) moreover from vs have "P v (x ⊕ z)".. hence "P v (x ⊕ z) ∧ ¬ O v x" using ‹¬ O v x›.. hence "P v z" by (rule in_second_summand) ultimately have "P v y ∧ P v z".. hence "P v (y ⊗ z)" by (rule common_part_in_product) hence "O v (y ⊗ z)" by (rule part_implies_overlap) with ‹¬ O v (y ⊗ z)› show "False".. qed qed text ‹ Sums distribute over products. › theorem sum_over_product: "O y z ⟹ x ⊕ (y ⊗ z) = (x ⊕ y) ⊗ (x ⊕ z)" proof - assume "O y z" hence "P (x ⊕ (y ⊗ z)) ((x ⊕ y) ⊗ (x ⊕ z))" by (rule sum_over_product_left) moreover have "P ((x ⊕ y) ⊗ (x ⊕ z)) (x ⊕ (y ⊗ z))" using ‹O y z› by (rule sum_over_product_right) ultimately show "x ⊕ (y ⊗ z) = (x ⊕ y) ⊗ (x ⊕ z)" by (rule part_antisymmetry) qed lemma product_in_factor_by_sum: "O x y ⟹ P (x ⊗ y) (x ⊗ (y ⊕ z))" proof - assume "O x y" hence "P (x ⊗ y) x" by (rule product_in_first_factor) moreover have "P (x ⊗ y) y" using ‹O x y› by (rule product_in_second_factor) hence "P (x ⊗ y) (y ⊕ z)" using first_summand_in_sum by (rule part_transitivity) with ‹P (x ⊗ y) x› have "P (x ⊗ y) x ∧ P (x ⊗ y) (y ⊕ z)".. thus "P (x ⊗ y) (x ⊗ (y ⊕ z))" by (rule common_part_in_product) qed lemma product_of_first_summand: "O x y ⟹ ¬ O x z ⟹ P (x ⊗ (y ⊕ z)) (x ⊗ y)" proof - assume "O x y" hence "O x (y ⊕ z)" by (rule first_summand_overlap) assume "¬ O x z" show "P (x ⊗ (y ⊕ z)) (x ⊗ y)" proof (rule ccontr) assume "¬ P (x ⊗ (y ⊕ z)) (x ⊗ y)" hence "∃ v. P v (x ⊗ (y ⊕ z)) ∧ ¬ O v (x ⊗ y)" by (rule strong_supplementation) then obtain v where v: "P v (x ⊗ (y ⊕ z)) ∧ ¬ O v (x ⊗ y)".. hence "P v (x ⊗ (y ⊕ z))".. with ‹O x (y ⊕ z)› have "P v x ∧ P v (y ⊕ z)" by (rule product_part_in_factors) hence "P v x".. moreover from v have "¬ O v (x ⊗ y)".. ultimately have "P v x ∧ ¬ O v (x ⊗ y)".. hence "¬ O v y" by (rule disjoint_from_second_factor) from ‹P v x ∧ P v (y ⊕ z)› have "P v (y ⊕ z)".. hence "P v (y ⊕ z) ∧ ¬ O v y" using ‹¬ O v y›.. hence "P v z" by (rule in_second_summand) with ‹P v x› have "P v x ∧ P v z".. hence "∃ v. P v x ∧ P v z".. with overlap_eq have "O x z".. with ‹¬ O x z› show "False".. qed qed theorem disjoint_product_over_sum: "O x y ⟹ ¬ O x z ⟹ x ⊗ (y ⊕ z) = x ⊗ y" proof - assume "O x y" moreover assume "¬ O x z" ultimately have "P (x ⊗ (y ⊕ z)) (x ⊗ y)" by (rule product_of_first_summand) moreover have "P (x ⊗ y)(x ⊗ (y ⊕ z))" using ‹O x y› by (rule product_in_factor_by_sum) ultimately show "x ⊗ (y ⊕ z) = x ⊗ y" by (rule part_antisymmetry) qed lemma product_over_sum_left: "O x y ∧ O x z ⟹ P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))" proof - assume "O x y ∧ O x z" hence "O x y".. hence "O x (y ⊕ z)" by (rule first_summand_overlap) show "P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))" proof (rule ccontr) assume "¬ P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))" hence "∃ v. P v (x ⊗ (y ⊕ z)) ∧ ¬ O v ((x ⊗ y) ⊕ (x ⊗ z))" by (rule strong_supplementation) then obtain v where v: "P v (x ⊗ (y ⊕ z)) ∧ ¬ O v ((x ⊗ y) ⊕ (x ⊗ z))".. hence "¬ O v ((x ⊗ y) ⊕ (x ⊗ z))".. with disjoint_from_sum have oxyz: "¬ O v (x ⊗ y) ∧ ¬ O v (x ⊗ z)".. from v have "P v (x ⊗ (y ⊕ z))".. with ‹O x (y ⊕ z)› have pxyz: "P v x ∧ P v (y ⊕ z)" by (rule product_part_in_factors) hence "P v x".. moreover from oxyz have "¬ O v (x ⊗ y)".. ultimately have "P v x ∧ ¬ O v (x ⊗ y)".. hence "¬ O v y" by (rule disjoint_from_second_factor) from oxyz have "¬ O v (x ⊗ z)".. with ‹P v x› have "P v x ∧ ¬ O v (x ⊗ z)".. hence "¬ O v z" by (rule disjoint_from_second_factor) with ‹¬ O v y› have "¬ O v y ∧ ¬ O v z".. with disjoint_from_sum have "¬ O v (y ⊕ z)".. from pxyz have "P v (y ⊕ z)".. hence "O v (y ⊕ z)" by (rule part_implies_overlap) with ‹¬ O v (y ⊕ z)› show "False".. qed qed lemma product_over_sum_right: "O x y ∧ O x z ⟹ P((x ⊗ y) ⊕ (x ⊗ z))(x ⊗ (y ⊕ z))" proof - assume antecedent: "O x y ∧ O x z" have "P (x ⊗ y) (x ⊗ (y ⊕ z)) ∧ P (x ⊗ z) (x ⊗ (y ⊕ z))" proof from antecedent have "O x y".. thus "P (x ⊗ y) (x ⊗ (y ⊕ z))" by (rule product_in_factor_by_sum) next from antecedent have "O x z".. hence "P (x ⊗ z) (x ⊗ (z ⊕ y))" by (rule product_in_factor_by_sum) with sum_commutativity show "P (x ⊗ z) (x ⊗ (y ⊕ z))" by (rule subst) qed thus "P((x ⊗ y) ⊕ (x ⊗ z))(x ⊗ (y ⊕ z))" by (rule summands_part_implies_sum_part) qed theorem product_over_sum: "O x y ∧ O x z ⟹ x ⊗ (y ⊕ z) = (x ⊗ y) ⊕ (x ⊗ z)" proof - assume antecedent: "O x y ∧ O x z" hence "P (x ⊗ (y ⊕ z))((x ⊗ y) ⊕ (x ⊗ z))" by (rule product_over_sum_left) moreover have "P((x ⊗ y) ⊕ (x ⊗ z))(x ⊗ (y ⊕ z))" using antecedent by (rule product_over_sum_right) ultimately show "x ⊗ (y ⊕ z) = (x ⊗ y) ⊕ (x ⊗ z)" by (rule part_antisymmetry) qed lemma joint_identical_sums: "v ⊕ w = x ⊕ y ⟹ O x v ∧ O x w ⟹ ((x ⊗ v) ⊕ (x ⊗ w)) = x" proof - assume "v ⊕ w = x ⊕ y" moreover assume "O x v ∧ O x w" hence "x ⊗ (v ⊕ w) = x ⊗ v ⊕ x ⊗ w" by (rule product_over_sum) ultimately have "x ⊗ (x ⊕ y) = x ⊗ v ⊕ x ⊗ w" by (rule subst) moreover have "(x ⊗ (x ⊕ y)) = x" using first_summand_in_sum by (rule part_product_identity) ultimately show "((x ⊗ v) ⊕ (x ⊗ w)) = x" by (rule subst) qed lemma disjoint_identical_sums: "v ⊕ w = x ⊕ y ⟹ ¬ O y v ∧ ¬ O w x ⟹ x = v ∧ y = w" proof - assume identical: "v ⊕ w = x ⊕ y" assume disjoint: "¬ O y v ∧ ¬ O w x" show "x = v ∧ y = w" proof from disjoint have "¬ O y v".. hence "(x ⊕ y) ⊗ (x ⊕ v) = x" by (rule product_is_first_summand) with identical have "(v ⊕ w) ⊗ (x ⊕ v) = x" by (rule ssubst) moreover from disjoint have "¬ O w x".. hence "(v ⊕ w) ⊗ (v ⊕ x) = v" by (rule product_is_first_summand) with sum_commutativity have "(v ⊕ w) ⊗ (x ⊕ v) = v" by (rule subst) ultimately show "x = v" by (rule subst) next from disjoint have "¬ O w x".. hence "(y ⊕ w) ⊗ (y ⊕ x) = y" by (rule product_is_first_summand) moreover from disjoint have "¬ O y v".. hence "(w ⊕ y) ⊗ (w ⊕ v) = w" by (rule product_is_first_summand) with sum_commutativity have "(w ⊕ y) ⊗ (v ⊕ w) = w" by (rule subst) with identical have "(w ⊕ y) ⊗ (x ⊕ y) = w" by (rule subst) with sum_commutativity have "(w ⊕ y) ⊗ (y ⊕ x) = w" by (rule subst) with sum_commutativity have "(y ⊕ w) ⊗ (y ⊕ x) = w" by (rule subst) ultimately show "y = w" by (rule subst) qed qed end subsection ‹ Differences › locale CEMD = CEM + CMD begin lemma plus_minus: "PP y x ⟹ y ⊕ (x ⊖ y) = x" proof - assume "PP y x" hence "∃ z. P z x ∧ ¬ O z y" by (rule weak_supplementation) hence xmy:"∀ w. P w (x ⊖ y) ⟷ (P w x ∧ ¬ O w y)" by (rule difference_character) have "∀ w. O w x ⟷ (O w y ∨ O w (x ⊖ y))" proof fix w from xmy have w: "P w (x ⊖ y) ⟷ (P w x ∧ ¬ O w y)".. show "O w x ⟷ (O w y ∨ O w (x ⊖ y))" proof assume "O w x" with overlap_eq have "∃ v. P v w ∧ P v x".. then obtain v where v: "P v w ∧ P v x".. hence "P v w".. from v have "P v x".. show "O w y ∨ O w (x ⊖ y)" proof cases 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 y ∨ O w (x ⊖ y)".. next from xmy have "P v (x ⊖ y) ⟷ (P v x ∧ ¬ O v y)".. moreover assume "¬ O v y" with ‹P v x› have "P v x ∧ ¬ O v y".. ultimately have "P v (x ⊖ y)".. with ‹P v w› have "P v w ∧ P v (x ⊖ y)".. hence "∃ v. P v w ∧ P v (x ⊖ y)".. with overlap_eq have "O w (x ⊖ y)".. thus "O w y ∨ O w (x ⊖ y)".. qed next assume "O w y ∨ O w (x ⊖ y)" thus "O w x" proof from ‹PP y x› have "P y x" by (rule proper_implies_part) moreover assume "O w y" ultimately show "O w x" by (rule overlap_monotonicity) next assume "O w (x ⊖ y)" with overlap_eq have "∃ v. P v w ∧ P v (x ⊖ y)".. then obtain v where v: "P v w ∧ P v (x ⊖ y)".. hence "P v w".. from xmy have "P v (x ⊖ y) ⟷ (P v x ∧ ¬ O v y)".. moreover from v have "P v (x ⊖ y)".. ultimately have "P v x ∧ ¬ O v y".. hence "P v x".. with ‹P v w› have "P v w ∧ P v x".. hence "∃ v. P v w ∧ P v x".. with overlap_eq show "O w x".. qed qed qed thus "y ⊕ (x ⊖ y) = x" by (rule sum_intro) qed end subsection ‹ The Universe › locale CEMU = CEM + CMU begin lemma something_disjoint: "x ≠ u ⟹ (∃ v. ¬ O v x)" proof - assume "x ≠ u" with universe_character have "P x u ∧ x ≠ u".. with nip_eq have "PP x u".. hence "∃ v. P v u ∧ ¬ O v x" by (rule weak_supplementation) then obtain v where "P v u ∧ ¬ O v x".. hence "¬ O v x".. thus "∃ v. ¬ O v x".. qed lemma overlaps_universe: "O x u" proof - from universe_character have "P x u". thus "O x u" by (rule part_implies_overlap) qed lemma universe_absorbing: "x ⊕ u = u" proof - from universe_character have "P (x ⊕ u) u". thus "x ⊕ u = u" using second_summand_in_sum by (rule part_antisymmetry) qed lemma second_summand_not_universe: "x ⊕ y ≠ u ⟹ y ≠ u" proof - assume antecedent: "x ⊕ y ≠ u" show "y ≠ u" proof assume "y = u" hence "x ⊕ u ≠ u" using antecedent by (rule subst) thus "False" using universe_absorbing.. qed qed lemma first_summand_not_universe: "x ⊕ y ≠ u ⟹ x ≠ u" proof - assume "x ⊕ y ≠ u" with sum_commutativity have "y ⊕ x ≠ u" by (rule subst) thus "x ≠ u" by (rule second_summand_not_universe) qed end subsection ‹ Complements › locale CEMC = CEM + CMC + assumes universe_eq: "u = (THE x. ∀ y. P y x)" begin lemma complement_sum_character: "∀ y. P y (x ⊕ (─x))" proof fix y have "∀ v. O v y ⟶ O v x ∨ O v (─x)" proof fix v show "O v y ⟶ O v x ∨ O v (─x)" proof assume "O v y" show "O v x ∨ O v (─x)" using or_complement_overlap.. qed qed with sum_part_character show "P y (x ⊕ (─x))".. qed lemma universe_closure: "∃ x. ∀ y. P y x" using complement_sum_character by (rule exI) end sublocale CEMC ⊆ CEMU proof show "u = (THE z. ∀w. P w z)" using universe_eq. show "∃ x. ∀ y. P y x" using universe_closure. qed sublocale CEMC ⊆ CEMD proof qed context CEMC begin corollary universe_is_complement_sum: "u = x ⊕ (─x)" using complement_sum_character by (rule universe_intro) lemma strong_complement_character: "x ≠ u ⟹ (∀ v. P v (─x) ⟷ ¬ O v x)" proof - assume "x ≠ u" hence "∃ v. ¬ O v x" by (rule something_disjoint) thus "∀ v. P v (─x) ⟷ ¬ O v x" by (rule complement_character) qed lemma complement_part_not_part: "x ≠ u ⟹ P y (─x) ⟹ ¬ P y x" proof - assume "x ≠ u" hence "∀ w. P w (─x) ⟷ ¬ O w x" by (rule strong_complement_character) hence y: "P y (─x) ⟷ ¬ O y x".. moreover assume "P y (─x)" ultimately have "¬ O y x".. thus "¬ P y x" by (rule disjoint_implies_not_part) qed lemma complement_involution: "x ≠ u ⟹ x = ─(─x)" proof - assume "x ≠ u" have "¬ P u x" proof assume "P u x" with universe_character have "x = u" by (rule part_antisymmetry) with ‹x ≠ u› show "False".. qed hence "∃ v. P v u ∧ ¬ O v x" by (rule strong_supplementation) then obtain v where v: "P v u ∧ ¬ O v x".. hence "¬ O v x".. hence "∃ v. ¬ O v x".. hence notx: "∀ w. P w (─x) ⟷ ¬ O w x" by (rule complement_character) have "─x ≠ u" proof assume "─x = u" hence "∀ w. P w u ⟷ ¬ O w x" using notx by (rule subst) hence "P x u ⟷ ¬ O x x".. hence "¬ O x x" using universe_character.. thus "False" using overlap_reflexivity.. qed have "¬ P u (─x)" proof assume "P u (─x)" with universe_character have "─x = u" by (rule part_antisymmetry) with ‹─x ≠ u› show "False".. qed hence "∃ v. P v u ∧ ¬ O v (─x)" by (rule strong_supplementation) then obtain w where w: "P w u ∧ ¬ O w (─x)".. hence "¬ O w (─x)".. hence "∃ v. ¬ O v (─x)".. hence notnotx: "∀ w. P w (─(─x)) ⟷ ¬ O w (─x)" by (rule complement_character) hence "P x (─(─x)) ⟷ ¬ O x (─x)".. moreover have "¬ O x (─x)" proof assume "O x (─x)" with overlap_eq have "∃ s. P s x ∧ P s (─x)".. then obtain s where s: "P s x ∧ P s (─x)".. hence "P s x".. hence "O s x" by (rule part_implies_overlap) from notx have "P s (─x) ⟷ ¬ O s x".. moreover from s have "P s (─x)".. ultimately have "¬ O s x".. thus "False" using ‹O s x›.. qed ultimately have "P x (─(─x))".. moreover have "P (─(─x)) x" proof (rule ccontr) assume "¬ P (─(─x)) x" hence "∃ s. P s (─(─x)) ∧ ¬ O s x" by (rule strong_supplementation) then obtain s where s: "P s (─(─x)) ∧ ¬ O s x".. hence "¬ O s x".. from notnotx have "P s (─(─x)) ⟷ (¬ O s (─x))".. moreover from s have "P s (─(─x))".. ultimately have "¬ O s (─x)".. from or_complement_overlap have "O s x ∨ O s (─x)".. thus "False" proof assume "O s x" with ‹¬ O s x› show "False".. next assume "O s (─x)" with ‹¬ O s (─x )› show "False".. qed qed ultimately show "x = ─(─x)" by (rule part_antisymmetry) qed lemma part_complement_reversal: "y ≠ u ⟹ P x y ⟹ P (─y) (─x)" proof - assume "y ≠ u" hence ny: "∀ w. P w (─y) ⟷ ¬ O w y" by (rule strong_complement_character) assume "P x y" have "x ≠ u" proof assume "x = u" hence "P u y" using ‹P x y› by (rule subst) with universe_character have "y = u" by (rule part_antisymmetry) with ‹y ≠ u› show "False".. qed hence "∀ w. P w (─x) ⟷ ¬ O w x" by (rule strong_complement_character) hence "P (─y) (─x) ⟷ ¬ O (─y) x".. moreover have "¬ O (─y) x" 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".. hence "P v (─y)".. from ny have "P v (─y) ⟷ ¬ O v y".. hence "¬ O v y" using ‹P v (─y)›.. moreover from v have "P v x".. hence "P v y" using ‹P x y› by (rule part_transitivity) hence "O v y" by (rule part_implies_overlap) ultimately show "False".. qed ultimately show "P (─y) (─x)".. qed lemma complements_overlap: "x ⊕ y ≠ u ⟹ O(─x)(─y)" proof - assume "x ⊕ y ≠ u" hence "∃ z. ¬ O z (x ⊕ y)" by (rule something_disjoint) then obtain z where z:"¬ O z (x ⊕ y)".. hence "¬ O z x" by (rule first_summand_disjointness) hence "P z (─x)" by (rule complement_part) moreover from z have "¬ O z y" by (rule second_summand_disjointness) hence "P z (─y)" by (rule complement_part) ultimately show "O(─x)(─y)" by (rule overlap_intro) qed lemma sum_complement_in_complement_product: "x ⊕ y ≠ u ⟹ P(─(x ⊕ y))(─x ⊗ ─y)" proof - assume "x ⊕ y ≠ u" hence "O (─x) (─y)" by (rule complements_overlap) hence "∀ w. P w (─x ⊗ ─y) ⟷ (P w (─x) ∧ P w (─y))" by (rule product_character) hence "P(─(x ⊕ y))(─x ⊗ ─y)⟷(P(─(x ⊕ y))(─x) ∧ P(─(x ⊕ y))(─y))".. moreover have "P (─(x ⊕ y))(─x) ∧ P (─(x ⊕ y))(─y)" proof show "P (─(x ⊕ y))(─x)" using ‹x ⊕ y ≠ u› first_summand_in_sum by (rule part_complement_reversal) next show "P (─(x ⊕ y))(─y)" using ‹x ⊕ y ≠ u› second_summand_in_sum by (rule part_complement_reversal) qed ultimately show "P (─(x ⊕ y))(─x ⊗ ─y)".. qed lemma complement_product_in_sum_complement: "x ⊕ y ≠ u ⟹ P(─x ⊗ ─y)(─(x ⊕ y))" proof - assume "x ⊕ y ≠ u" hence "∀w. P w (─(x ⊕ y)) ⟷ ¬ O w (x ⊕ y)" by (rule strong_complement_character) hence "P (─x ⊗ ─y) (─(x ⊕ y)) ⟷ (¬ O (─x ⊗ ─y) (x ⊕ y))".. moreover have "¬ O (─x ⊗ ─y) (x ⊕ y)" proof have "O(─x)(─y)" using ‹x ⊕ y ≠ u› by (rule complements_overlap) hence p: "∀ v. P v ((─x) ⊗ (─y)) ⟷ (P v (─x) ∧ P v (─y))" by (rule product_character) have "O(─x ⊗ ─y)(x ⊕ y) ⟷ (O(─x ⊗ ─y) x ∨ O(─x ⊗ ─y)y)" using sum_character.. moreover assume "O (─x ⊗ ─y)(x ⊕ y)" ultimately have "O (─x ⊗ ─y) x ∨ O (─x ⊗ ─y) y".. thus "False" proof assume "O (─x ⊗ ─y) x" with overlap_eq have "∃ v. P v (─x ⊗ ─y) ∧ P v x".. then obtain v where v: "P v (─x ⊗ ─y) ∧ P v x".. hence "P v (─x ⊗ ─y)".. from p have "P v ((─x) ⊗ (─y)) ⟷ (P v (─x) ∧ P v (─y))".. hence "P v (─x) ∧ P v (─y)" using ‹P v (─x ⊗ ─y)›.. hence "P v (─x)".. have "x ≠ u" using ‹x ⊕ y ≠ u› by (rule first_summand_not_universe) hence "∀w. P w (─x) ⟷ ¬ O w x" by (rule strong_complement_character) hence "P v (─x) ⟷ ¬ O v x".. hence "¬ O v x" using ‹P v (─x)›.. moreover from v have "P v x".. hence "O v x" by (rule part_implies_overlap) ultimately show "False".. next assume "O (─x ⊗ ─y) y" with overlap_eq have "∃ v. P v (─x ⊗ ─y) ∧ P v y".. then obtain v where v: "P v (─x ⊗ ─y) ∧ P v y".. hence "P v (─x ⊗ ─y)".. from p have "P v ((─x) ⊗ (─y)) ⟷ (P v (─x) ∧ P v (─y))".. hence "P v (─x) ∧ P v (─y)" using ‹P v (─x ⊗ ─y)›.. hence "P v (─y)".. have "y ≠ u" using ‹x ⊕ y ≠ u› by (rule second_summand_not_universe) hence "∀w. P w (─y) ⟷ ¬ O w y" by (rule strong_complement_character) hence "P v (─y) ⟷ ¬ O v y".. hence "¬ O v y" using ‹P v (─y)›.. moreover from v have "P v y".. hence "O v y" by (rule part_implies_overlap) ultimately show "False".. qed qed ultimately show "P (─x ⊗ ─y) (─(x ⊕ y))".. qed theorem sum_complement_is_complements_product: "x ⊕ y ≠ u ⟹ ─(x ⊕ y) = (─x ⊗ ─y)" proof - assume "x ⊕ y ≠ u" show "─(x ⊕ y) = (─x ⊗ ─y)" proof (rule part_antisymmetry) show "P (─ (x ⊕ y)) (─ x ⊗ ─ y)" using ‹x ⊕ y ≠ u› by (rule sum_complement_in_complement_product) show "P (─ x ⊗ ─ y) (─ (x ⊕ y))" using ‹x ⊕ y ≠ u› by (rule complement_product_in_sum_complement) qed qed lemma complement_sum_in_product_complement: "O x y ⟹ x ≠ u ⟹ y ≠ u ⟹ P ((─x) ⊕ (─y))(─(x ⊗ y))" proof - assume "O x y" assume "x ≠ u" assume "y ≠ u" have "x ⊗ y ≠ u" proof assume "x ⊗ y = u" with ‹O x y› have "x = u" by (rule product_universe_implies_factor_universe) with ‹x ≠ u› show "False".. qed hence notxty: "∀ w. P w (─(x ⊗ y)) ⟷ ¬ O w (x ⊗ y)" by (rule strong_complement_character) hence "P((─x)⊕(─y))(─(x ⊗ y)) ⟷ ¬O((─x)⊕(─y))(x ⊗ y)".. moreover have "¬ O ((─x) ⊕ (─y)) (x ⊗ y)" proof from sum_character have "∀ w. O w ((─x) ⊕ (─y)) ⟷ (O w (─x) ∨ O w (─y))". hence "O(x ⊗ y)((─x)⊕(─y)) ⟷ (O(x ⊗ y)(─x) ∨ O(x ⊗ y)(─y))".. moreover assume "O ((─x) ⊕ (─y)) (x ⊗ y)" hence "O (x ⊗ y) ((─x) ⊕ (─y))" by (rule overlap_symmetry) ultimately have "O (x ⊗ y) (─x) ∨ O (x ⊗ y) (─y)".. thus False proof assume "O (x ⊗ y)(─x)" with overlap_eq have "∃ v. P v (x ⊗ y) ∧ P v (─x)".. then obtain v where v: "P v (x ⊗ y) ∧ P v (─x)".. hence "P v (─x)".. with ‹x ≠ u› have "¬ P v x" by (rule complement_part_not_part) moreover from v have "P v (x ⊗ y)".. with ‹O x y› have "P v x" by (rule product_part_in_first_factor) ultimately show "False".. next assume "O (x ⊗ y) (─y)" with overlap_eq have "∃ v. P v (x ⊗ y) ∧ P v (─y)".. then obtain v where v: "P v (x ⊗ y) ∧ P v (─y)".. hence "P v (─y)".. with ‹y ≠ u› have "¬ P v y" by (rule complement_part_not_part) moreover from v have "P v (x ⊗ y)".. with ‹O x y› have "P v y" by (rule product_part_in_second_factor) ultimately show "False".. qed qed ultimately show "P ((─x) ⊕ (─y))(─(x ⊗ y))".. qed lemma product_complement_in_complements_sum: "x ≠ u ⟹ y ≠ u ⟹ P(─(x ⊗ y))((─x) ⊕ (─y))" proof - assume "x ≠ u" hence "x = ─(─x)" by (rule complement_involution) assume "y ≠ u" hence "y = ─(─y)" by (rule complement_involution) show "P (─(x ⊗ y))((─x) ⊕ (─y))" proof cases assume "─x ⊕ ─y = u" thus "P (─(x ⊗ y))((─x) ⊕ (─y))" using universe_character by (rule ssubst) next assume "─x ⊕ ─y ≠ u" hence "─x ⊕ ─y = ─(─(─x ⊕ ─ y))" by (rule complement_involution) moreover have "─(─x ⊕ ─y) = ─(─x) ⊗ ─(─y)" using ‹─x ⊕ ─y ≠ u› by (rule sum_complement_is_complements_product) with ‹x = ─(─x)› have "─(─x ⊕ ─y) = x ⊗ ─(─y)" by (rule ssubst) with ‹y = ─(─y)› have "─(─x ⊕ ─y) = x ⊗ y" by (rule ssubst) hence "P (─(x ⊗ y))(─(─(─x ⊕ ─y)))" using part_reflexivity by (rule subst) ultimately show "P (─(x ⊗ y))(─x ⊕ ─y)" by (rule ssubst) qed qed theorem complement_of_product_is_sum_of_complements: "O x y ⟹ x ⊕ y ≠ u ⟹ ─(x ⊗ y) = (─x) ⊕ (─y)" proof - assume "O x y" assume "x ⊕ y ≠ u" show "─(x ⊗ y) = (─x) ⊕ (─y)" proof (rule part_antisymmetry) have "x ≠ u" using ‹x ⊕ y ≠ u› by (rule first_summand_not_universe) have "y ≠ u" using ‹x ⊕ y ≠ u› by (rule second_summand_not_universe) show "P (─ (x ⊗ y)) (─ x ⊕ ─ y)" using ‹x ≠ u› ‹y ≠ u› by (rule product_complement_in_complements_sum) show " P (─ x ⊕ ─ y) (─ (x ⊗ y))" using ‹O x y› ‹x ≠ u› ‹y ≠ u› by (rule complement_sum_in_product_complement) qed qed end (*<*) end (*>*)