Theory Classical_Connectives

chapter ‹ Classical Logic Connectives \label{sec:logical-connectives}›

theory Classical_Connectives
  imports
    Classical_Logic_Completeness
    List_Utilities
begin

text ‹ Here we define the usual connectives for classical logic. ›

no_notation FuncSet.funcset (infixr "→" 60)

section ‹ Verum ›

definition (in classical_logic) verum :: "'a" ("⊤")
  where
    "⊤ = ⊥ → ⊥"

lemma (in classical_logic) verum_tautology [simp]: "⊢ ⊤"
  by (metis list_implication.simps(1) list_implication_axiom_k verum_def)

lemma verum_semantics [simp]:
  "𝔐 ⊨⇩p⇩r⇩o⇩p ⊤"
  unfolding verum_def by simp

lemma (in classical_logic) verum_embedding [simp]:
  "❙⦇ ⊤ ❙⦈ = ⊤"
  by (simp add: classical_logic_class.verum_def verum_def)

section ‹ Conjunction ›

definition (in classical_logic)
  conjunction :: "'a ⇒ 'a ⇒ 'a" (infixr "⊓" 67)
  where
    "φ ⊓ ψ = (φ → ψ → ⊥) → ⊥"

primrec (in classical_logic)
  arbitrary_conjunction :: "'a list ⇒ 'a" ("⨅")
  where
     "⨅ [] = ⊤"
  |  "⨅ (φ # Φ) = φ ⊓ ⨅ Φ"

lemma (in classical_logic) conjunction_introduction:
  "⊢ φ → ψ → (φ ⊓ ψ)"
  by (metis
        modus_ponens
        conjunction_def
        list_flip_implication1
        list_implication.simps(1)
        list_implication.simps(2))

lemma (in classical_logic) conjunction_left_elimination:
  "⊢ (φ ⊓ ψ) → φ"
  by (metis (full_types)
        Peirces_law
        pseudo_scotus
        conjunction_def
        list_deduction_base_theory
        list_deduction_modus_ponens
        list_deduction_theorem
        list_deduction_weaken)

lemma (in classical_logic) conjunction_right_elimination:
  "⊢ (φ ⊓ ψ) → ψ"
  by (metis (full_types)
        axiom_k
        Contraposition
        modus_ponens
        conjunction_def
        flip_hypothetical_syllogism
        flip_implication)

lemma (in classical_logic) conjunction_embedding [simp]:
  "❙⦇ φ ⊓ ψ ❙⦈ = ❙⦇ φ ❙⦈ ⊓ ❙⦇ ψ ❙⦈"
  unfolding conjunction_def classical_logic_class.conjunction_def
  by simp

lemma conjunction_semantics [simp]:
  "𝔐 ⊨⇩p⇩r⇩o⇩p φ ⊓ ψ = (𝔐 ⊨⇩p⇩r⇩o⇩p φ ∧ 𝔐 ⊨⇩p⇩r⇩o⇩p ψ)"
  unfolding conjunction_def by simp

section ‹ Biconditional ›

definition (in classical_logic) biconditional :: "'a ⇒ 'a ⇒ 'a"   (infixr "↔" 75)
  where
    "φ ↔ ψ = (φ → ψ) ⊓ (ψ → φ)"

lemma (in classical_logic) biconditional_introduction:
  "⊢ (φ → ψ) → (ψ → φ) → (φ ↔ ψ)"
  by (simp add: biconditional_def conjunction_introduction)

lemma (in classical_logic) biconditional_left_elimination:
  "⊢ (φ ↔ ψ) → φ → ψ"
  by (simp add: biconditional_def conjunction_left_elimination)

lemma (in classical_logic) biconditional_right_elimination:
  "⊢ (φ ↔ ψ) → ψ → φ"
  by (simp add: biconditional_def conjunction_right_elimination)

lemma (in classical_logic) biconditional_embedding [simp]:
  "❙⦇ φ ↔ ψ ❙⦈ = ❙⦇ φ ❙⦈ ↔ ❙⦇ ψ ❙⦈"
  unfolding biconditional_def classical_logic_class.biconditional_def
  by simp

lemma biconditional_semantics [simp]:
  "𝔐 ⊨⇩p⇩r⇩o⇩p φ ↔ ψ = (𝔐 ⊨⇩p⇩r⇩o⇩p φ ⟷ 𝔐 ⊨⇩p⇩r⇩o⇩p ψ)"
  unfolding biconditional_def
  by (simp, blast)

section ‹ Negation ›

definition (in classical_logic) negation :: "'a ⇒ 'a"  ("∼")
  where
    "∼ φ = φ → ⊥"

lemma (in classical_logic) negation_introduction:
  "⊢ (φ → ⊥) → ∼ φ"
  unfolding negation_def
  by (metis axiom_k modus_ponens implication_absorption)

lemma (in classical_logic) negation_elimination:
  "⊢ ∼ φ → (φ → ⊥)"
  unfolding negation_def
  by (metis axiom_k modus_ponens implication_absorption)

lemma (in classical_logic) negation_embedding [simp]:
  "❙⦇ ∼ φ ❙⦈ = ∼ ❙⦇ φ ❙⦈"
  by (simp add:
        classical_logic_class.negation_def
        negation_def)

lemma negation_semantics [simp]:
  "𝔐 ⊨⇩p⇩r⇩o⇩p ∼ φ = (¬ 𝔐 ⊨⇩p⇩r⇩o⇩p φ)"
  unfolding negation_def
  by simp

section ‹ Disjunction ›

definition (in classical_logic) disjunction :: "'a ⇒ 'a ⇒ 'a"   (infixr "⊔" 67)
  where
    "φ ⊔ ψ = (φ → ⊥) → ψ"

primrec (in classical_logic) arbitrary_disjunction :: "'a list ⇒ 'a" ("⨆")
  where
     "⨆ [] = ⊥"
  |  "⨆ (φ # Φ) = φ ⊔ ⨆ Φ"

lemma (in classical_logic) disjunction_elimination:
  "⊢ (φ → χ) → (ψ → χ) → (φ ⊔ ψ) → χ"
proof -
  let ?Γ = "[φ → χ, ψ → χ, φ ⊔ ψ]"
  have "?Γ :⊢ (φ → ⊥) → χ"
    unfolding disjunction_def
    by (metis hypothetical_syllogism
              list_deduction_def
              list_implication.simps(1)
              list_implication.simps(2)
              set_deduction_base_theory
              set_deduction_theorem
              set_deduction_weaken)
  hence "?Γ :⊢ χ"
    using excluded_middle_elimination
          list_deduction_modus_ponens
          list_deduction_theorem
          list_deduction_weaken
    by blast
  thus ?thesis
    unfolding list_deduction_def
    by simp
qed

lemma (in classical_logic) disjunction_left_introduction:
  "⊢ φ → (φ ⊔ ψ)"
  unfolding disjunction_def
  by (metis modus_ponens
            pseudo_scotus
            flip_implication)

lemma (in classical_logic) disjunction_right_introduction:
  "⊢ ψ → (φ ⊔ ψ)"
  unfolding disjunction_def
  using axiom_k
  by simp

lemma (in classical_logic) disjunction_embedding [simp]:
  "❙⦇ φ ⊔ ψ ❙⦈ = ❙⦇ φ ❙⦈ ⊔ ❙⦇ ψ ❙⦈"
  unfolding disjunction_def classical_logic_class.disjunction_def
  by simp

lemma disjunction_semantics [simp]:
  "𝔐 ⊨⇩p⇩r⇩o⇩p φ ⊔ ψ = (𝔐 ⊨⇩p⇩r⇩o⇩p φ ∨ 𝔐 ⊨⇩p⇩r⇩o⇩p ψ)"
  unfolding disjunction_def
  by (simp, blast)

section ‹ Mutual Exclusion ›

primrec (in classical_logic) exclusive :: "'a list ⇒ 'a" ("∐")
  where
      "∐ [] = ⊤"
    | "∐ (φ # Φ) = ∼ (φ ⊓ ⨆ Φ) ⊓ ∐ Φ"

section ‹ Subtraction ›

definition (in classical_logic) subtraction :: "'a ⇒ 'a ⇒ 'a" (infixl "∖" 69)
  where "φ ∖ ψ = φ ⊓ ∼ ψ"

lemma (in classical_logic) subtraction_embedding [simp]:
  "❙⦇ φ ∖ ψ ❙⦈ = ❙⦇ φ ❙⦈ ∖ ❙⦇ ψ ❙⦈"
  unfolding subtraction_def classical_logic_class.subtraction_def
  by simp

section ‹ Negated Lists ›

definition (in classical_logic) map_negation :: "'a list ⇒ 'a list" ("❙∼")
  where [simp]: "❙∼ Φ ≡ map ∼ Φ"

section ‹ Common (\& Uncommon) Identities ›

subsection ‹ Biconditional Equivalence Relation ›

lemma (in classical_logic) biconditional_reflection:
  "⊢ φ ↔ φ"
  by (meson
        axiom_k
        modus_ponens
        biconditional_introduction
        implication_absorption)

lemma (in classical_logic) biconditional_symmetry:
  "⊢ (φ ↔ ψ) ↔ (ψ ↔ φ)"
  by (metis (full_types) modus_ponens
                         biconditional_def
                         conjunction_def
                         flip_hypothetical_syllogism
                         flip_implication)

lemma (in classical_logic) biconditional_symmetry_rule:
  "⊢ φ ↔ ψ ⟹ ⊢ ψ ↔ φ"
  by (meson modus_ponens
            biconditional_introduction
            biconditional_left_elimination
            biconditional_right_elimination)

lemma (in classical_logic) biconditional_transitivity:
    "⊢ (φ ↔ ψ) → (ψ ↔ χ) → (φ ↔ χ)"
proof -
  have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ ↔ ❙⟨ψ❙⟩) → (❙⟨ψ❙⟩ ↔ ❙⟨χ❙⟩) → (❙⟨φ❙⟩ ↔ ❙⟨χ❙⟩)"
    by simp
  hence "⊢ ❙⦇ (❙⟨φ❙⟩ ↔ ❙⟨ψ❙⟩) → (❙⟨ψ❙⟩ ↔ ❙⟨χ❙⟩) → (❙⟨φ❙⟩ ↔ ❙⟨χ❙⟩) ❙⦈"
    using propositional_semantics by blast
 thus ?thesis by simp
qed

lemma (in classical_logic) biconditional_transitivity_rule:
  "⊢ φ ↔ ψ ⟹ ⊢ ψ ↔ χ ⟹ ⊢ φ ↔ χ"
  using modus_ponens biconditional_transitivity by blast

subsection ‹ Biconditional Weakening ›

lemma (in classical_logic) biconditional_weaken:
  assumes "Γ ⊩ φ ↔ ψ"
  shows "Γ ⊩ φ = Γ ⊩ ψ"
  by (metis assms
            biconditional_left_elimination
            biconditional_right_elimination
            set_deduction_modus_ponens
            set_deduction_weaken)

lemma (in classical_logic) list_biconditional_weaken:
  assumes "Γ :⊢ φ ↔ ψ"
  shows "Γ :⊢ φ = Γ :⊢ ψ"
  by (metis assms
            biconditional_left_elimination
            biconditional_right_elimination
            list_deduction_modus_ponens
            list_deduction_weaken)

lemma (in classical_logic) weak_biconditional_weaken:
  assumes "⊢ φ ↔ ψ"
  shows "⊢ φ = ⊢ ψ"
  by (metis assms
            biconditional_left_elimination
            biconditional_right_elimination
            modus_ponens)

subsection ‹ Conjunction Identities ›

lemma (in classical_logic) conjunction_negation_identity:
  "⊢ ∼ (φ ⊓ ψ) ↔ (φ → ψ → ⊥)"
  by (metis Contraposition
            double_negation_converse
            modus_ponens
            biconditional_introduction
            conjunction_def
            negation_def)

lemma (in classical_logic) conjunction_set_deduction_equivalence [simp]:
  "Γ ⊩ φ ⊓ ψ = (Γ ⊩ φ ∧ Γ ⊩ ψ)"
  by (metis set_deduction_weaken [where Γ="Γ"]
            set_deduction_modus_ponens [where Γ="Γ"]
            conjunction_introduction
            conjunction_left_elimination
            conjunction_right_elimination)

lemma (in classical_logic) conjunction_list_deduction_equivalence [simp]:
  "Γ :⊢ φ ⊓ ψ = (Γ :⊢ φ ∧ Γ :⊢ ψ)"
  by (metis list_deduction_weaken [where Γ="Γ"]
            list_deduction_modus_ponens [where Γ="Γ"]
            conjunction_introduction
            conjunction_left_elimination
            conjunction_right_elimination)

lemma (in classical_logic) weak_conjunction_deduction_equivalence [simp]:
  "⊢ φ ⊓ ψ = (⊢ φ ∧ ⊢ ψ)"
  by (metis conjunction_set_deduction_equivalence set_deduction_base_theory)

lemma (in classical_logic) conjunction_set_deduction_arbitrary_equivalence [simp]:
  "Γ ⊩ ⨅ Φ = (∀ φ ∈ set Φ. Γ ⊩ φ)"
  by (induct Φ, simp add: set_deduction_weaken, simp)

lemma (in classical_logic) conjunction_list_deduction_arbitrary_equivalence [simp]:
  "Γ :⊢ ⨅ Φ = (∀ φ ∈ set Φ. Γ :⊢ φ)"
  by (induct Φ, simp add: list_deduction_weaken, simp)

lemma (in classical_logic) weak_conjunction_deduction_arbitrary_equivalence [simp]:
  "⊢ ⨅ Φ = (∀ φ ∈ set Φ. ⊢ φ)"
  by (induct Φ, simp+)

lemma (in classical_logic) conjunction_commutativity:
  "⊢ (ψ ⊓ φ) ↔ (φ ⊓ ψ)"
  by (metis
        (full_types)
        modus_ponens
        biconditional_introduction
        conjunction_def
        flip_hypothetical_syllogism
        flip_implication)

lemma (in classical_logic) conjunction_associativity:
  "⊢ ((φ ⊓ ψ) ⊓ χ) ↔ (φ ⊓ (ψ ⊓ χ))"
proof -
  have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ((❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) ⊓ ❙⟨χ❙⟩) ↔ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩))"
    by simp
  hence "⊢ ❙⦇ ((❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) ⊓ ❙⟨χ❙⟩) ↔ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ❙⦈"
    using propositional_semantics by blast
  thus ?thesis by simp
qed

lemma (in classical_logic) arbitrary_conjunction_antitone:
  "set Φ ⊆ set Ψ ⟹ ⊢ ⨅ Ψ → ⨅ Φ"
proof -
  have "∀ Φ. set Φ ⊆ set Ψ ⟶ ⊢ ⨅ Ψ → ⨅ Φ"
  proof (induct Ψ)
    case Nil
    then show ?case
      by (simp add: pseudo_scotus verum_def)
  next
    case (Cons ψ Ψ)
    {
      fix Φ
      assume "set Φ ⊆ set (ψ # Ψ)"
      have "⊢ ⨅ (ψ # Ψ) → ⨅ Φ"
      proof (cases "ψ ∈ set Φ")
        assume "ψ ∈ set Φ"
                have "∀ φ ∈ set Φ. ⊢ ⨅ Φ ↔ (φ ⊓ ⨅ (removeAll φ Φ))"
        proof (induct Φ)
          case Nil
          then show ?case by simp
        next
          case (Cons χ Φ)
          {
            fix φ
            assume "φ ∈ set (χ # Φ)"
            have "⊢ ⨅ (χ # Φ) ↔ (φ ⊓ ⨅ (removeAll φ (χ # Φ)))"
            proof cases
              assume "φ ∈ set Φ"
              hence "⊢ ⨅ Φ ↔ (φ ⊓ ⨅ (removeAll φ Φ))"
                using Cons.hyps ‹φ ∈ set Φ›
                by auto
              moreover
              have "⊢ (⨅ Φ ↔ (φ ⊓ ⨅ (removeAll φ Φ))) →
                      (χ ⊓ ⨅ Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))"
              proof -
                have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p
                        (❙⟨⨅ Φ❙⟩ ↔ (❙⟨φ❙⟩ ⊓ ❙⟨⨅ (removeAll φ Φ)❙⟩))
                            → (❙⟨χ❙⟩ ⊓ ❙⟨⨅ Φ❙⟩)
                                   ↔ (❙⟨φ❙⟩ ⊓ ❙⟨χ❙⟩ ⊓ ❙⟨⨅ (removeAll φ Φ)❙⟩)"
                    by auto
                hence "⊢ ❙⦇ (❙⟨⨅ Φ❙⟩ ↔ (❙⟨φ❙⟩ ⊓ ❙⟨⨅ (removeAll φ Φ)❙⟩))
                               → (❙⟨χ❙⟩ ⊓ ❙⟨⨅ Φ❙⟩)
                                      ↔ (❙⟨φ❙⟩ ⊓ ❙⟨χ❙⟩ ⊓ ❙⟨⨅ (removeAll φ Φ)❙⟩) ❙⦈"
                  using propositional_semantics by blast
                thus ?thesis by simp
              qed
              ultimately have "⊢ ⨅ (χ # Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))"
                using modus_ponens by auto
              show ?thesis
              proof cases
                assume "φ = χ"
                moreover
                {
                  fix φ
                  have "⊢ (χ ⊓ φ) → (χ ⊓ χ ⊓ φ)"
                    unfolding conjunction_def
                    by (meson
                          axiom_s
                          double_negation
                          modus_ponens
                          flip_hypothetical_syllogism
                          flip_implication)
                } note tautology = this
                from ‹⊢ ⨅ (χ # Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))›
                     ‹φ = χ›
                have "⊢ (χ ⊓ ⨅ (removeAll χ Φ)) → (χ ⊓ ⨅ Φ)"
                  unfolding biconditional_def
                  by (simp, metis tautology hypothetical_syllogism modus_ponens)
                moreover
                from ‹⊢ ⨅ (χ # Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))›
                     ‹φ = χ›
                have "⊢ (χ ⊓ ⨅ Φ) → (χ ⊓ ⨅ (removeAll χ Φ))"
                  unfolding biconditional_def
                  by (simp,
                      metis conjunction_right_elimination
                            hypothetical_syllogism
                            modus_ponens)
                ultimately show ?thesis
                  unfolding biconditional_def
                  by simp
              next
                assume "φ ≠ χ"
                then show ?thesis
                  using ‹⊢ ⨅ (χ # Φ) ↔ (φ ⊓ χ ⊓ ⨅ (removeAll φ Φ))›
                  by simp
              qed
            next
              assume "φ ∉ set Φ"
              hence "φ = χ" "χ ∉ set Φ"
                using ‹φ ∈ set (χ # Φ)› by auto
              then show ?thesis
                using biconditional_reflection
                by simp
            qed
          }
          thus ?case by blast
        qed
        hence "⊢ (ψ ⊓ ⨅ (removeAll ψ Φ)) → ⨅ Φ"
          using modus_ponens biconditional_right_elimination ‹ψ ∈ set Φ›
          by blast
        moreover
        from ‹ψ ∈ set Φ› ‹set Φ ⊆ set (ψ # Ψ)› Cons.hyps
        have "⊢ ⨅ Ψ → ⨅ (removeAll ψ Φ)"
          by (simp add: subset_insert_iff insert_absorb)
        hence "⊢ (ψ ⊓ ⨅ Ψ) → (ψ ⊓ ⨅ (removeAll ψ Φ))"
          unfolding conjunction_def
          using
            modus_ponens
            hypothetical_syllogism
            flip_hypothetical_syllogism
          by meson
        ultimately have "⊢ (ψ ⊓ ⨅ Ψ) → ⨅ Φ"
          using modus_ponens hypothetical_syllogism
          by blast
        thus ?thesis
          by simp
      next
        assume "ψ ∉ set Φ"
        hence "⊢ ⨅ Ψ → ⨅ Φ"
          using Cons.hyps ‹set Φ ⊆ set (ψ # Ψ)›
          by auto
        hence "⊢ (ψ ⊓ ⨅ Ψ) → ⨅ Φ"
          unfolding conjunction_def
          by (metis
                modus_ponens
                conjunction_def
                conjunction_right_elimination
                hypothetical_syllogism)
        thus ?thesis
          by simp
      qed
    }
    thus ?case by blast
  qed
  thus "set Φ ⊆ set Ψ ⟹ ⊢ ⨅ Ψ → ⨅ Φ" by blast
qed

lemma (in classical_logic) arbitrary_conjunction_remdups:
  "⊢ (⨅ Φ) ↔ ⨅ (remdups Φ)"
  by (simp add: arbitrary_conjunction_antitone biconditional_def)

lemma (in classical_logic) curry_uncurry:
  "⊢ (φ → ψ → χ) ↔ ((φ ⊓ ψ) → χ)"
proof -
  have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ → ❙⟨ψ❙⟩ → ❙⟨χ❙⟩) ↔ ((❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) → ❙⟨χ❙⟩)"
      by auto
  hence "⊢ ❙⦇ (❙⟨φ❙⟩ → ❙⟨ψ❙⟩ → ❙⟨χ❙⟩) ↔ ((❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) → ❙⟨χ❙⟩) ❙⦈"
    using propositional_semantics by blast
  thus ?thesis by simp
qed

lemma (in classical_logic) list_curry_uncurry:
  "⊢ (Φ :→ χ) ↔ (⨅ Φ → χ)"
proof (induct Φ)
  case Nil
  have "⊢ χ ↔ (⊤ → χ)"
    unfolding biconditional_def
              conjunction_def
              verum_def
    using
      axiom_k
      ex_falso_quodlibet
      modus_ponens
      conjunction_def
      excluded_middle_elimination
      set_deduction_base_theory
      conjunction_set_deduction_equivalence
    by metis
  with Nil show ?case
    by simp
next
  case (Cons φ Φ)
  have "⊢ ((φ # Φ) :→ χ) ↔ (φ → (Φ :→ χ))"
    by (simp add: biconditional_reflection)
  with Cons have "⊢ ((φ # Φ) :→ χ) ↔ (φ → ⨅ Φ → χ)"
    by (metis modus_ponens
              biconditional_def
              hypothetical_syllogism
              list_implication.simps(2)
              weak_conjunction_deduction_equivalence)
  with curry_uncurry [where ?φ="φ"  and ?ψ="⨅ Φ" and ?χ="χ"]
  show ?case
    unfolding biconditional_def
    by (simp, metis modus_ponens hypothetical_syllogism)
qed

subsection ‹ Disjunction Identities ›

lemma (in classical_logic) bivalence:
  "⊢ ∼ φ ⊔ φ"
  by (simp add: double_negation disjunction_def negation_def)

lemma (in classical_logic) implication_equivalence:
  "⊢ (∼ φ ⊔ ψ) ↔ (φ → ψ)"
  by (metis double_negation_converse
            modus_ponens
            biconditional_introduction
            bivalence
            disjunction_def
            flip_hypothetical_syllogism
            negation_def)

lemma (in classical_logic) disjunction_commutativity:
  "⊢ (ψ ⊔ φ) ↔ (φ ⊔ ψ)"
  by (meson modus_ponens
            biconditional_introduction
            disjunction_elimination
            disjunction_left_introduction
            disjunction_right_introduction)

lemma (in classical_logic) disjunction_associativity:
  "⊢ ((φ ⊔ ψ) ⊔ χ) ↔ (φ ⊔ (ψ ⊔ χ))"
proof -
  have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ((❙⟨φ❙⟩ ⊔ ❙⟨ψ❙⟩) ⊔ ❙⟨χ❙⟩) ↔ (❙⟨φ❙⟩ ⊔ (❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩))"
    by simp
  hence "⊢ ❙⦇ ((❙⟨φ❙⟩ ⊔ ❙⟨ψ❙⟩) ⊔ ❙⟨χ❙⟩) ↔ (❙⟨φ❙⟩ ⊔ (❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩)) ❙⦈"
    using propositional_semantics by blast
  thus ?thesis by simp
qed

lemma (in classical_logic) arbitrary_disjunction_monotone:
  "set Φ ⊆ set Ψ ⟹ ⊢ ⨆ Φ → ⨆ Ψ"
proof -
  have "∀ Φ. set Φ ⊆ set Ψ ⟶ ⊢ ⨆ Φ → ⨆ Ψ"
  proof (induct Ψ)
    case Nil
    then show ?case using verum_def verum_tautology by auto
  next
    case (Cons ψ Ψ)
    {
      fix Φ
      assume "set Φ ⊆ set (ψ # Ψ)"
      have "⊢ ⨆ Φ → ⨆ (ψ # Ψ)"
      proof cases
        assume "ψ ∈ set Φ"
        have "∀ φ ∈ set Φ. ⊢ ⨆ Φ ↔ (φ ⊔ ⨆ (removeAll φ Φ))"
        proof (induct Φ)
          case Nil
          then show ?case by simp
        next
          case (Cons χ Φ)
          {
            fix φ
            assume "φ ∈ set (χ # Φ)"
            have "⊢ ⨆ (χ # Φ) ↔ (φ ⊔ ⨆ (removeAll φ (χ # Φ)))"
            proof cases
              assume "φ ∈ set Φ"
              hence "⊢ ⨆ Φ ↔ (φ ⊔ ⨆ (removeAll φ Φ))"
                using Cons.hyps ‹φ ∈ set Φ›
                by auto
              moreover
              have "⊢ (⨆ Φ ↔ (φ ⊔ ⨆ (removeAll φ Φ))) →
                      (χ ⊔ ⨆ Φ) ↔ (φ ⊔ χ ⊔ ⨆ (removeAll φ Φ))"
              proof -
                have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p
                        (❙⟨⨆ Φ❙⟩ ↔ (❙⟨φ❙⟩ ⊔ ❙⟨⨆ (removeAll φ Φ)❙⟩))
                         → (❙⟨χ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)
                              ↔ (❙⟨φ❙⟩ ⊔ ❙⟨χ❙⟩ ⊔ ❙⟨⨆ (removeAll φ Φ)❙⟩)"
                    by auto
                  hence "⊢ ❙⦇ (❙⟨⨆ Φ❙⟩ ↔ (❙⟨φ❙⟩ ⊔ ❙⟨⨆ (removeAll φ Φ)❙⟩))
                             → (❙⟨χ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)
                                 ↔ (❙⟨φ❙⟩ ⊔ ❙⟨χ❙⟩ ⊔ ❙⟨⨆ (removeAll φ Φ)❙⟩) ❙⦈"
                    using propositional_semantics by blast
                  thus ?thesis by simp
              qed
              ultimately have "⊢ ⨆ (χ # Φ) ↔ (φ ⊔ χ ⊔ ⨆ (removeAll φ Φ))"
                using modus_ponens by auto
              show ?thesis
              proof cases
                assume "φ = χ"
                then show ?thesis
                  using ‹⊢ ⨆ (χ # Φ) ↔ (φ ⊔ χ ⊔ ⨆ (removeAll φ Φ))›
                  unfolding biconditional_def
                  by (simp add: disjunction_def,
                      meson
                        axiom_k
                        modus_ponens
                        flip_hypothetical_syllogism
                        implication_absorption)
              next
                assume "φ ≠ χ"
                then show ?thesis
                  using ‹⊢ ⨆ (χ # Φ) ↔ (φ ⊔ χ ⊔ ⨆ (removeAll φ Φ))›
                  by simp
              qed
            next
              assume "φ ∉ set Φ"
              hence "φ = χ" "χ ∉ set Φ"
                using ‹φ ∈ set (χ # Φ)› by auto
              then show ?thesis
                using biconditional_reflection
                by simp
            qed
          }
          thus ?case by blast
        qed
        hence "⊢ ⨆ Φ → (ψ ⊔ ⨆ (removeAll ψ Φ))"
          using modus_ponens biconditional_left_elimination ‹ψ ∈ set Φ›
          by blast
        moreover
        from ‹ψ ∈ set Φ› ‹set Φ ⊆ set (ψ # Ψ)› Cons.hyps
        have "⊢ ⨆ (removeAll ψ Φ) → ⨆ Ψ"
          by (simp add: subset_insert_iff insert_absorb)
        hence "⊢ (ψ ⊔ ⨆ (removeAll ψ Φ)) → ⨆ (ψ # Ψ)"
          using
            modus_ponens
            disjunction_def
            hypothetical_syllogism
          by fastforce
        ultimately show ?thesis
          by (simp, metis modus_ponens hypothetical_syllogism)
      next
        assume "ψ ∉ set Φ"
        hence "⊢ ⨆ Φ → ⨆ Ψ"
          using Cons.hyps ‹set Φ ⊆ set (ψ # Ψ)›
          by auto
        then show ?thesis
          by (metis
                arbitrary_disjunction.simps(2)
                disjunction_def
                list_deduction_def
                list_deduction_theorem
                list_deduction_weaken
                list_implication.simps(1)
                list_implication.simps(2))
      qed
    }
    then show ?case by blast
  qed
  thus "set Φ ⊆ set Ψ ⟹ ⊢ ⨆ Φ → ⨆ Ψ" by blast
qed

lemma (in classical_logic) arbitrary_disjunction_remdups:
  "⊢ (⨆ Φ) ↔ ⨆ (remdups Φ)"
  by (simp add: arbitrary_disjunction_monotone biconditional_def)

lemma (in classical_logic) arbitrary_disjunction_exclusion_MCS:
  assumes "MCS Ω"
  shows "⨆ Ψ ∉ Ω ≡ ∀ ψ ∈ set Ψ. ψ ∉ Ω"
proof (induct Ψ)
  case Nil
  then show ?case
    using
      assms
      formula_consistent_def
      formula_maximally_consistent_set_def_def
      maximally_consistent_set_def
      set_deduction_reflection
    by (simp, blast)
next
  case (Cons ψ Ψ)
  have "⨆ (ψ # Ψ) ∉ Ω = (ψ ∉ Ω ∧ ⨆ Ψ ∉ Ω)"
    by (simp add: disjunction_def,
        meson
          assms
          formula_consistent_def
          formula_maximally_consistent_set_def_def
          formula_maximally_consistent_set_def_implication
          maximally_consistent_set_def
          set_deduction_reflection)
  thus ?case using Cons.hyps by simp
qed

lemma (in classical_logic) contra_list_curry_uncurry:
  "⊢ (Φ :→ χ) ↔ (∼ χ → ⨆ (❙∼ Φ))"
proof (induct Φ)
  case Nil
  then show ?case
    by (simp,
          metis
            biconditional_introduction
            bivalence
            disjunction_def
            double_negation_converse
            modus_ponens
            negation_def)
next
  case (Cons φ Φ)
  hence "⊢ (⨅ Φ → χ) ↔ (∼ χ → ⨆ (❙∼ Φ))"
    by (metis
          biconditional_symmetry_rule
          biconditional_transitivity_rule
          list_curry_uncurry)
  have "⊢ (⨅ (φ # Φ) → χ) ↔ (∼ χ → ⨆ (❙∼ (φ # Φ)))"
  proof -
    have "⊢ (⨅ Φ → χ) ↔ (∼ χ → ⨆ (❙∼ Φ))
             → ((φ ⊓ ⨅ Φ) → χ) ↔ (∼ χ → (∼ φ ⊔ ⨆ (❙∼ Φ)))"
    proof -
      have
       "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p
         (❙⟨⨅ Φ❙⟩ → ❙⟨χ❙⟩) ↔ (∼ ❙⟨χ❙⟩ → ❙⟨⨆ (❙∼ Φ)❙⟩)
             → ((❙⟨φ❙⟩ ⊓ ❙⟨⨅ Φ❙⟩) → ❙⟨χ❙⟩) ↔ (∼ ❙⟨χ❙⟩ → (∼ ❙⟨φ❙⟩ ⊔ ❙⟨⨆ (❙∼ Φ)❙⟩))"
        by auto
      hence
        "⊢ ❙⦇ (❙⟨⨅ Φ❙⟩ → ❙⟨χ❙⟩) ↔ (∼ ❙⟨χ❙⟩ → ❙⟨⨆ (❙∼ Φ)❙⟩)
             → ((❙⟨φ❙⟩ ⊓ ❙⟨⨅ Φ❙⟩) → ❙⟨χ❙⟩) ↔ (∼ ❙⟨χ❙⟩ → (∼ ❙⟨φ❙⟩ ⊔ ❙⟨⨆ (❙∼ Φ)❙⟩)) ❙⦈"
        using propositional_semantics by blast
      thus ?thesis by simp
    qed
    thus ?thesis
      using ‹⊢ (⨅ Φ → χ) ↔ (∼ χ → ⨆ (❙∼ Φ))› modus_ponens by auto
  qed
  then show ?case
    using biconditional_transitivity_rule list_curry_uncurry by blast
qed

subsection ‹ Monotony of Conjunction and Disjunction ›

lemma (in classical_logic) conjunction_monotonic_identity:
  "⊢ (φ → ψ) → (φ ⊓ χ) → (ψ ⊓ χ)"
  unfolding conjunction_def
  using modus_ponens
        flip_hypothetical_syllogism
  by blast

lemma (in classical_logic) conjunction_monotonic:
  assumes "⊢ φ → ψ"
  shows "⊢ (φ ⊓ χ) → (ψ ⊓ χ)"
  using assms
        modus_ponens
        conjunction_monotonic_identity
  by blast

lemma (in classical_logic) disjunction_monotonic_identity:
  "⊢ (φ → ψ) → (φ ⊔ χ) → (ψ ⊔ χ)"
  unfolding disjunction_def
  using modus_ponens
        flip_hypothetical_syllogism
  by blast

lemma (in classical_logic) disjunction_monotonic:
  assumes "⊢ φ → ψ"
  shows "⊢ (φ ⊔ χ) → (ψ ⊔ χ)"
  using assms
        modus_ponens
        disjunction_monotonic_identity
  by blast

subsection ‹ Distribution Identities ›

lemma (in classical_logic) conjunction_distribution:
  "⊢ ((ψ ⊔ χ) ⊓ φ) ↔ ((ψ ⊓ φ) ⊔ (χ ⊓ φ))"
proof -
  have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ((❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩) ⊓ ❙⟨φ❙⟩) ↔ ((❙⟨ψ❙⟩ ⊓ ❙⟨φ❙⟩) ⊔ (❙⟨χ❙⟩ ⊓ ❙⟨φ❙⟩))"
      by auto
  hence "⊢ ❙⦇ ((❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩) ⊓ ❙⟨φ❙⟩) ↔ ((❙⟨ψ❙⟩ ⊓ ❙⟨φ❙⟩) ⊔ (❙⟨χ❙⟩ ⊓ ❙⟨φ❙⟩)) ❙⦈"
    using propositional_semantics by blast
  thus ?thesis by simp
qed

lemma (in classical_logic) subtraction_distribution:
  "⊢ ((ψ ⊔ χ) ∖ φ) ↔ ((ψ ∖ φ) ⊔ (χ ∖ φ))"
  by (simp add: conjunction_distribution subtraction_def)

lemma (in classical_logic) conjunction_arbitrary_distribution:
  "⊢ (⨆ Ψ ⊓ φ) ↔ ⨆ [ψ ⊓ φ. ψ ← Ψ]"
proof (induct Ψ)
  case Nil
  then show ?case
    by (simp add: ex_falso_quodlibet
                  biconditional_def
                  conjunction_left_elimination)
next
  case (Cons ψ Ψ)
  have "⊢ (⨆ (ψ # Ψ) ⊓ φ) ↔ ((ψ ⊓ φ) ⊔ ((⨆ Ψ) ⊓ φ))"
    using conjunction_distribution by auto
  moreover
  from Cons have
    "⊢ ((ψ ⊓ φ) ⊔ ((⨆ Ψ) ⊓ φ)) ↔ ((ψ ⊓ φ) ⊔ (⨆ [ψ ⊓ φ. ψ ← Ψ]))"
    unfolding disjunction_def biconditional_def
    by (simp, meson modus_ponens hypothetical_syllogism)
  ultimately show ?case
    by (simp, metis biconditional_transitivity_rule)
qed

lemma (in classical_logic) subtraction_arbitrary_distribution:
  "⊢ (⨆ Ψ ∖ φ) ↔ ⨆ [ψ ∖ φ. ψ ← Ψ]"
  by (simp add: conjunction_arbitrary_distribution subtraction_def)

lemma (in classical_logic) disjunction_distribution:
  "⊢ (φ ⊔ (ψ ⊓ χ)) ↔ ((φ ⊔ ψ) ⊓ (φ ⊔ χ))"
proof -
  have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ ⊔ (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ↔ ((❙⟨φ❙⟩ ⊔ ❙⟨ψ❙⟩) ⊓ (❙⟨φ❙⟩ ⊔ ❙⟨χ❙⟩))"
      by auto
  hence "⊢ ❙⦇ (❙⟨φ❙⟩ ⊔ (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ↔ ((❙⟨φ❙⟩ ⊔ ❙⟨ψ❙⟩) ⊓ (❙⟨φ❙⟩ ⊔ ❙⟨χ❙⟩)) ❙⦈"
    using propositional_semantics by blast
  thus ?thesis by simp
qed

lemma (in classical_logic) implication_distribution:
  "⊢ (φ → (ψ ⊓ χ)) ↔ ((φ → ψ) ⊓ (φ → χ))"
proof -
  have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ → (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ↔ ((❙⟨φ❙⟩ → ❙⟨ψ❙⟩) ⊓ (❙⟨φ❙⟩ → ❙⟨χ❙⟩))"
      by auto
  hence "⊢ ❙⦇ (❙⟨φ❙⟩ → (❙⟨ψ❙⟩ ⊓ ❙⟨χ❙⟩)) ↔ ((❙⟨φ❙⟩ → ❙⟨ψ❙⟩) ⊓ (❙⟨φ❙⟩ → ❙⟨χ❙⟩)) ❙⦈"
    using propositional_semantics by blast
  thus ?thesis by simp
qed

lemma (in classical_logic) list_implication_distribution:
  "⊢ (Φ :→ (ψ ⊓ χ)) ↔ ((Φ :→ ψ) ⊓ (Φ :→ χ))"
proof (induct Φ)
  case Nil
  then show ?case
    by (simp add: biconditional_reflection)
next
  case (Cons φ Φ)
  hence " ⊢ (φ # Φ) :→ (ψ ⊓ χ) ↔ (φ → (Φ :→ ψ ⊓ Φ :→ χ))"
    by (metis
          modus_ponens
          biconditional_def
          hypothetical_syllogism
          list_implication.simps(2)
          weak_conjunction_deduction_equivalence)
  moreover
  have "⊢ (φ → (Φ :→ ψ ⊓ Φ :→ χ)) ↔ (((φ # Φ) :→ ψ) ⊓ ((φ # Φ) :→ χ))"
    using implication_distribution by auto
  ultimately show ?case
    by (simp, metis biconditional_transitivity_rule)
qed

lemma (in classical_logic) biconditional_conjunction_weaken:
  "⊢ (α ↔ β) → ((γ ⊓ α) ↔ (γ ⊓ β))"
proof -
  have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨α❙⟩ ↔ ❙⟨β❙⟩) → ((❙⟨γ❙⟩ ⊓ ❙⟨α❙⟩) ↔ (❙⟨γ❙⟩ ⊓ ❙⟨β❙⟩))"
      by auto
  hence "⊢ ❙⦇ (❙⟨α❙⟩ ↔ ❙⟨β❙⟩) → ((❙⟨γ❙⟩ ⊓ ❙⟨α❙⟩) ↔ (❙⟨γ❙⟩ ⊓ ❙⟨β❙⟩)) ❙⦈"
    using propositional_semantics by blast
  thus ?thesis by simp
qed

lemma (in classical_logic) biconditional_conjunction_weaken_rule:
  "⊢ (α ↔ β) ⟹ ⊢ (γ ⊓ α) ↔ (γ ⊓ β)"
  using modus_ponens biconditional_conjunction_weaken by blast

lemma (in classical_logic) disjunction_arbitrary_distribution:
  "⊢ (φ ⊔ ⨅ Ψ) ↔ ⨅ [φ ⊔ ψ. ψ ← Ψ]"
proof (induct Ψ)
  case Nil
  then show ?case
    unfolding disjunction_def biconditional_def
    using axiom_k modus_ponens verum_tautology
    by (simp, blast)
next
  case (Cons ψ Ψ)
  have "⊢ (φ ⊔ ⨅ (ψ # Ψ)) ↔ ((φ ⊔ ψ) ⊓ (φ ⊔ ⨅ Ψ))"
    by (simp add: disjunction_distribution)
  moreover
  from biconditional_conjunction_weaken_rule
       Cons
  have " ⊢ ((φ ⊔ ψ) ⊓ φ ⊔ ⨅ Ψ) ↔ ⨅ (map (λ χ . φ ⊔ χ) (ψ # Ψ))"
    by simp
  ultimately show ?case
    by (metis biconditional_transitivity_rule)
qed

lemma (in classical_logic) list_implication_arbitrary_distribution:
  "⊢ (Φ :→ ⨅ Ψ) ↔ ⨅ [Φ :→ ψ. ψ ← Ψ]"
proof (induct Ψ)
  case Nil
  then show ?case
    by (simp add: biconditional_def,
        meson
          axiom_k
          modus_ponens
          list_implication_axiom_k
          verum_tautology)
next
  case (Cons ψ Ψ)
  have "⊢ Φ :→ ⨅ (ψ # Ψ) ↔ (Φ :→ ψ ⊓ Φ :→ ⨅ Ψ)"
    using list_implication_distribution
    by fastforce
  moreover
  from biconditional_conjunction_weaken_rule
       Cons
  have "⊢ (Φ :→ ψ ⊓ Φ :→ ⨅ Ψ) ↔ ⨅ [Φ :→ ψ. ψ ← (ψ # Ψ)]"
    by simp
  ultimately show ?case
    by (metis biconditional_transitivity_rule)
qed

lemma (in classical_logic) implication_arbitrary_distribution:
  "⊢ (φ → ⨅ Ψ) ↔ ⨅ [φ → ψ. ψ ← Ψ]"
  using list_implication_arbitrary_distribution [where ?Φ="[φ]"]
  by simp

subsection ‹ Negation ›

lemma (in classical_logic) double_negation_biconditional:
  "⊢ ∼ (∼ φ) ↔ φ"
  unfolding biconditional_def negation_def
  by (simp add: double_negation double_negation_converse)

lemma (in classical_logic) double_negation_elimination [simp]:
  "Γ ⊩ ∼ (∼ φ) = Γ ⊩ φ"
  using
    set_deduction_weaken
    biconditional_weaken
    double_negation_biconditional
  by metis

lemma (in classical_logic) alt_double_negation_elimination [simp]:
  "Γ ⊩ (φ → ⊥) → ⊥ ≡ Γ ⊩ φ"
  using double_negation_elimination
  unfolding negation_def
  by auto

lemma (in classical_logic) base_double_negation_elimination [simp]:
  "⊢ ∼ (∼ φ) = ⊢ φ"
  by (metis double_negation_elimination set_deduction_base_theory)

lemma (in classical_logic) alt_base_double_negation_elimination [simp]:
  "⊢ (φ → ⊥) → ⊥ ≡ ⊢ φ"
  using base_double_negation_elimination
  unfolding negation_def
  by auto

subsection ‹ Mutual Exclusion Identities ›

lemma (in classical_logic) exclusion_contrapositive_equivalence:
  "⊢ (φ → γ) ↔ ∼ (φ ⊓ ∼ γ)"
proof -
  have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨φ❙⟩ → ❙⟨γ❙⟩) ↔ ∼ (❙⟨φ❙⟩ ⊓ ∼ ❙⟨γ❙⟩)"
    by auto
  hence "⊢ ❙⦇ (❙⟨φ❙⟩ → ❙⟨γ❙⟩) ↔ ∼ (❙⟨φ❙⟩ ⊓ ∼ ❙⟨γ❙⟩) ❙⦈"
    using propositional_semantics by blast
  thus ?thesis by simp
qed

lemma (in classical_logic) disjuction_exclusion_equivalence:
  "Γ ⊩ ∼ (ψ ⊓ ⨆ Φ) ≡ ∀ φ ∈ set Φ. Γ ⊩ ∼ (ψ ⊓ φ)"
proof (induct Φ)
  case Nil
  then show ?case
    by (simp add:
          conjunction_right_elimination
          negation_def
          set_deduction_weaken)
next
  case (Cons φ Φ)
  have "⊢ ∼ (ψ ⊓ ⨆ (φ # Φ)) ↔ ∼ (ψ ⊓ (φ ⊔ ⨆ Φ))"
    by (simp add: biconditional_reflection)
  moreover have "⊢ ∼ (ψ ⊓ (φ ⊔ ⨆ Φ)) ↔ (∼ (ψ ⊓ φ) ⊓ ∼ (ψ ⊓ ⨆ Φ))"
  proof -
    have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ∼ (❙⟨ψ❙⟩ ⊓ (❙⟨φ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))
                         ↔ (∼ (❙⟨ψ❙⟩ ⊓ ❙⟨φ❙⟩) ⊓ ∼ (❙⟨ψ❙⟩ ⊓ ❙⟨⨆ Φ❙⟩))"
      by auto
    hence "⊢ ❙⦇ ∼ (❙⟨ψ❙⟩ ⊓ (❙⟨φ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))
               ↔ (∼ (❙⟨ψ❙⟩ ⊓ ❙⟨φ❙⟩) ⊓ ∼ (❙⟨ψ❙⟩ ⊓ ❙⟨⨆ Φ❙⟩)) ❙⦈"
      using propositional_semantics by blast
    thus ?thesis by simp
  qed
  ultimately
  have "⊢ ∼ (ψ ⊓ ⨆ (φ # Φ)) ↔ (∼ (ψ ⊓ φ) ⊓ ∼ (ψ ⊓ ⨆ Φ))"
    by simp
  hence "Γ ⊩ ∼ (ψ ⊓ ⨆ (φ # Φ)) = (Γ ⊩ ∼ (ψ ⊓ φ)
           ∧ (∀φ∈set Φ. Γ ⊩ ∼ (ψ ⊓ φ)))"
    using set_deduction_weaken [where Γ="Γ"]
          conjunction_set_deduction_equivalence [where Γ="Γ"]
          Cons.hyps
          biconditional_def
          set_deduction_modus_ponens
    by metis
  thus "Γ ⊩ ∼ (ψ ⊓ ⨆ (φ # Φ)) = (∀φ∈set (φ # Φ). Γ ⊩ ∼ (ψ ⊓ φ))"
    by simp
qed

lemma (in classical_logic) exclusive_elimination1:
  assumes "Γ ⊩ ∐ Φ"
  shows "∀ φ ∈ set Φ. ∀ ψ ∈ set Φ. (φ ≠ ψ) ⟶ Γ ⊩ ∼ (φ ⊓ ψ)"
  using assms
proof (induct Φ)
  case Nil
  thus ?case by auto
next
  case (Cons χ Φ)
  assume "Γ ⊩ ∐ (χ # Φ)"
  hence "Γ ⊩ ∐ Φ" by simp
  hence "∀φ∈set Φ. ∀ψ∈set Φ. φ ≠ ψ ⟶ Γ ⊩ ∼ (φ ⊓ ψ)"
    using Cons.hyps by blast
  moreover have "Γ ⊩ ∼ (χ ⊓ ⨆ Φ)"
    using ‹Γ ⊩ ∐ (χ # Φ)› conjunction_set_deduction_equivalence by auto
  hence "∀ φ ∈ set Φ. Γ ⊩ ∼ (χ ⊓ φ)"
    using disjuction_exclusion_equivalence by auto
  moreover {
    fix φ
    have "⊢ ∼ (χ ⊓ φ) → ∼ (φ ⊓ χ)"
      unfolding negation_def
                conjunction_def
      using modus_ponens flip_hypothetical_syllogism flip_implication by blast
  }
  with ‹∀ φ ∈ set Φ. Γ ⊩ ∼ (χ ⊓ φ)› have "∀ φ ∈ set Φ. Γ ⊩ ∼ (φ ⊓ χ)"
    using set_deduction_weaken [where Γ="Γ"]
          set_deduction_modus_ponens [where Γ="Γ"]
    by blast
  ultimately
  show "∀φ ∈ set (χ # Φ). ∀ψ ∈ set (χ # Φ). φ ≠ ψ ⟶ Γ ⊩ ∼ (φ ⊓ ψ)"
    by simp
qed

lemma (in classical_logic) exclusive_elimination2:
  assumes "Γ ⊩ ∐ Φ"
  shows "∀ φ ∈ duplicates Φ. Γ ⊩ ∼ φ"
  using assms
proof (induct Φ)
  case Nil
  then show ?case by simp
next
  case (Cons φ Φ)
  assume "Γ ⊩ ∐ (φ # Φ)"
  hence "Γ ⊩ ∐ Φ" by simp
  hence "∀φ∈duplicates Φ. Γ ⊩ ∼ φ" using Cons.hyps by auto
  show ?case
  proof cases
    assume "φ ∈ set Φ"
    moreover {
      fix φ ψ χ
      have "⊢ ∼ (φ ⊓ (ψ ⊔ χ)) ↔ (∼ (φ ⊓ ψ) ⊓ ∼ (φ ⊓ χ))"
      proof -
        have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩))
                       ↔ (∼ (❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) ⊓ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨χ❙⟩))"
          by auto
        hence "⊢ ❙⦇ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨χ❙⟩)) ↔ (∼ (❙⟨φ❙⟩ ⊓ ❙⟨ψ❙⟩) ⊓ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨χ❙⟩)) ❙⦈"
          using propositional_semantics by blast
        thus ?thesis by simp
      qed
      hence "Γ ⊩ ∼ (φ ⊓ (ψ ⊔ χ)) ≡ Γ ⊩ ∼ (φ ⊓ ψ) ⊓ ∼ (φ ⊓ χ)"
        using set_deduction_weaken
              biconditional_weaken by presburger
    }
    moreover
    have "⊢ ∼ (φ ⊓ φ) ↔ ∼ φ"
    proof -
      have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ∼ (❙⟨φ❙⟩ ⊓ ❙⟨φ❙⟩) ↔ ∼ ❙⟨φ❙⟩"
        by auto
      hence "⊢ ❙⦇ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨φ❙⟩) ↔ ∼ ❙⟨φ❙⟩ ❙⦈"
        using propositional_semantics by blast
      thus ?thesis by simp
    qed
    hence "Γ ⊩ ∼ (φ ⊓ φ) ≡ Γ ⊩ ∼ φ"
      using set_deduction_weaken
            biconditional_weaken by presburger
    moreover have "Γ ⊩ ∼ (φ ⊓ ⨆ Φ)" using ‹Γ ⊩ ∐ (φ # Φ)› by simp
    ultimately have "Γ ⊩ ∼ φ" by (induct Φ, simp, simp, blast)
    thus ?thesis using ‹φ ∈ set Φ› ‹∀φ∈duplicates Φ. Γ ⊩ ∼ φ› by simp
  next
    assume "φ ∉ set Φ"
    hence "duplicates (φ # Φ) = duplicates Φ" by simp
    then show ?thesis using ‹∀φ∈duplicates Φ. Γ ⊩ ∼ φ›
      by auto
  qed
qed

lemma (in classical_logic) exclusive_equivalence:
   "Γ ⊩ ∐ Φ =
      ((∀φ∈duplicates Φ. Γ ⊩ ∼ φ) ∧
         (∀ φ ∈ set Φ. ∀ ψ ∈ set Φ. (φ ≠ ψ) ⟶ Γ ⊩ ∼ (φ ⊓ ψ)))"
proof -
  {
    assume "∀φ∈duplicates Φ. Γ ⊩ ∼ φ"
           "∀ φ ∈ set Φ. ∀ ψ ∈ set Φ. (φ ≠ ψ) ⟶ Γ ⊩ ∼ (φ ⊓ ψ)"
    hence "Γ ⊩ ∐ Φ"
    proof (induct Φ)
      case Nil
      then show ?case
        by (simp add: set_deduction_weaken)
    next
      case (Cons φ Φ)
      assume A: "∀φ∈duplicates (φ # Φ). Γ ⊩ ∼ φ"
         and B: "∀χ∈set (φ # Φ). ∀ψ∈set (φ # Φ). χ ≠ ψ ⟶ Γ ⊩ ∼ (χ ⊓ ψ)"
      hence C: "Γ ⊩ ∐ Φ" using Cons.hyps by simp
      then show ?case
      proof cases
        assume "φ ∈ duplicates (φ # Φ)"
        moreover from this have "Γ ⊩ ∼ φ" using A by auto
        moreover have "duplicates Φ ⊆ set Φ" by (induct Φ, simp, auto)
        ultimately have "φ ∈ set Φ" by (metis duplicates.simps(2) subsetCE)
        hence "⊢ ∼ φ ↔ ∼(φ ⊓ ⨆ Φ)"
        proof (induct Φ)
          case Nil
          then show ?case by simp
        next
          case (Cons ψ Φ)
          assume "φ ∈ set (ψ # Φ)"
          then show "⊢ ∼ φ ↔ ∼ (φ ⊓ ⨆ (ψ # Φ))"
          proof -
            {
              assume "φ = ψ"
              hence ?thesis
              proof -
                have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))"
                  using ‹φ = ψ› by auto
                hence "⊢ ❙⦇ ∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)) ❙⦈"
                  using propositional_semantics by blast
                thus ?thesis by simp
              qed
            }
            moreover
            {
              assume "φ ≠ ψ"
              hence "φ ∈ set Φ" using ‹φ ∈ set (ψ # Φ)› by auto
              hence "⊢ ∼ φ ↔ ∼ (φ ⊓ ⨆ Φ)" using Cons.hyps by auto
              moreover have "⊢ (∼ φ ↔ ∼ (φ ⊓ ⨆ Φ))
                                   → (∼ φ ↔ ∼ (φ ⊓ (ψ ⊔ ⨆ Φ)))"
              proof -
                have "∀ 𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨⨆ Φ❙⟩)) →
                                     (∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)))"
                  by auto
                hence "⊢ ❙⦇ (∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ ❙⟨⨆ Φ❙⟩))
                           → (∼ ❙⟨φ❙⟩ ↔ ∼ (❙⟨φ❙⟩ ⊓ (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))) ❙⦈"
                  using propositional_semantics by blast
                thus ?thesis by simp
              qed
              ultimately have ?thesis using modus_ponens by simp
            }
            ultimately show ?thesis by auto
          qed
        qed
        with ‹Γ ⊩ ∼ φ› have "Γ ⊩ ∼(φ ⊓ ⨆ Φ)"
          using biconditional_weaken set_deduction_weaken by blast
        with ‹Γ ⊩ ∐ Φ› show ?thesis by simp
      next
        assume "φ ∉ duplicates (φ # Φ)"
        hence "φ ∉ set Φ" by auto
        with B have "∀ψ∈set Φ. Γ ⊩ ∼ (φ ⊓ ψ)" by (simp, metis)
        hence "Γ ⊩ ∼ (φ ⊓ ⨆ Φ)"
          by (simp add: disjuction_exclusion_equivalence)
        with ‹Γ ⊩ ∐ Φ› show ?thesis by simp
      qed
    qed
  }
  thus ?thesis
    by (metis exclusive_elimination1 exclusive_elimination2)
qed

subsection ‹ Miscellaneous Disjunctive Normal Form Identities ›

lemma (in classical_logic) map_negation_list_implication:
  "⊢ ((❙∼ Φ) :→ (∼ φ)) ↔ (φ → ⨆ Φ)"
proof (induct Φ)
  case Nil
  then show ?case
    unfolding
      biconditional_def
      map_negation_def
      negation_def
    using
      conjunction_introduction
      modus_ponens
      trivial_implication
    by simp
next
  case (Cons ψ Φ)
  have "⊢ (❙∼ Φ :→ ∼ φ ↔ (φ → ⨆ Φ))
          → (∼ ψ → ❙∼ Φ :→ ∼ φ) ↔ (φ → (ψ ⊔ ⨆ Φ))"
  proof -
    have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p (❙⟨❙∼ Φ :→ ∼ φ❙⟩ ↔ (❙⟨φ❙⟩ → ❙⟨⨆ Φ❙⟩)) →
                        (∼ ❙⟨ψ❙⟩ → ❙⟨❙∼ Φ :→ ∼ φ❙⟩) ↔ (❙⟨φ❙⟩ → (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩))"
      by fastforce
    hence "⊢ ❙⦇ (❙⟨❙∼ Φ :→ ∼ φ❙⟩ ↔ (❙⟨φ❙⟩ → ❙⟨⨆ Φ❙⟩)) →
               (∼ ❙⟨ψ❙⟩ → ❙⟨❙∼ Φ :→ ∼ φ❙⟩) ↔ (❙⟨φ❙⟩ → (❙⟨ψ❙⟩ ⊔ ❙⟨⨆ Φ❙⟩)) ❙⦈"
      using propositional_semantics by blast
    thus ?thesis
      by simp
  qed
  with Cons show ?case
    by (metis
          map_negation_def
          list.simps(9)
          arbitrary_disjunction.simps(2)
          modus_ponens
          list_implication.simps(2))
qed


lemma (in classical_logic) conj_dnf_distribute:
  "⊢ ⨆ (map (⨅ ∘ (λ φs. φ # φs)) Λ) ↔ (φ ⊓ ⨆ (map ⨅ Λ))"
proof(induct Λ)
  case Nil
  have "⊢ ⊥ ↔ (φ ⊓ ⊥)"
  proof -
    let ?φ = "⊥ ↔ (❙⟨φ❙⟩ ⊓ ⊥)"
    have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ?φ" by fastforce
    hence "⊢ ❙⦇ ?φ ❙⦈" using propositional_semantics by blast
    thus ?thesis by simp
  qed
  then show ?case by simp
next
  case (Cons Ψ Λ)
  assume "⊢ ⨆ (map (⨅ ∘ (λ φs. φ # φs)) Λ) ↔ (φ ⊓ ⨆ (map ⨅ Λ))"
    (is "⊢ ?A ↔ (φ ⊓ ?B)")
  moreover
  have "⊢ (?A ↔ (φ ⊓ ?B)) → (((φ ⊓ ⨅ Ψ) ⊔ ?A) ↔ (φ ⊓ ⨅ Ψ ⊔ ?B))"
  proof -
    let ?φ = "(❙⟨?A❙⟩ ↔ (❙⟨φ❙⟩ ⊓ ❙⟨?B❙⟩)) →
               (((❙⟨φ❙⟩ ⊓ ❙⟨⨅ Ψ❙⟩) ⊔ ❙⟨?A❙⟩) ↔ (❙⟨φ❙⟩ ⊓ ❙⟨⨅ Ψ❙⟩ ⊔ ❙⟨?B❙⟩))"
    have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ?φ" by fastforce
    hence "⊢ ❙⦇ ?φ ❙⦈" using propositional_semantics by blast
    thus ?thesis
      by simp
  qed
  ultimately have "⊢ ((φ ⊓ ⨅ Ψ) ⊔ ?A) ↔ (φ ⊓ ⨅ Ψ ⊔ ?B)"
    using modus_ponens
    by blast
  moreover
  have "map (⨅ ∘ (λ φs. φ # φs)) Λ = map (λΨ. φ ⊓ ⨅ Ψ) Λ" by simp
  ultimately show ?case by simp
qed

lemma (in classical_logic) append_dnf_distribute:
  "⊢ ⨆ (map (⨅ ∘ (λ Ψ. Φ @ Ψ)) Λ) ↔ (⨅ Φ ⊓ ⨆ (map ⨅ Λ))"
proof(induct Φ)
  case Nil
  have "⊢ ⨆ (map ⨅ Λ) ↔ (⊤ ⊓ ⨆ (map ⨅ Λ))"
    (is "⊢ ?A ↔ (⊤ ⊓ ?A)")
  proof -
    let ?φ = "❙⟨?A❙⟩ ↔ ((⊥ → ⊥) ⊓ ❙⟨?A❙⟩)"
    have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ?φ" by simp
    hence "⊢ ❙⦇ ?φ ❙⦈" using propositional_semantics by blast
    thus ?thesis
      unfolding verum_def
      by simp
  qed
  then show ?case by simp
next
  case (Cons φ Φ)
  have "⊢ ⨆ (map (⨅ ∘ (@) Φ) Λ) ↔ (⨅ Φ ⊓ ⨆ (map ⨅ Λ))
       = ⊢ ⨆ (map ⨅ (map ((@) Φ) Λ)) ↔ (⨅ Φ ⊓ ⨆ (map ⨅ Λ))"
    by simp
  with Cons have
    "⊢ ⨆ (map ⨅ (map (λ Ψ. Φ @ Ψ) Λ)) ↔ (⨅ Φ ⊓ ⨆ (map ⨅ Λ))"
    (is "⊢ ⨆ (map ⨅ ?A) ↔ (?B ⊓ ?C)")
    by meson
  moreover have "⊢ ⨆ (map ⨅ ?A) ↔ (?B ⊓ ?C)
                → (⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A) ↔ (φ ⊓ ⨆ (map ⨅ ?A)))
                → ⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A) ↔ ((φ ⊓ ?B) ⊓ ?C)"
  proof -
    let ?φ = "❙⟨⨆ (map ⨅ ?A)❙⟩ ↔ (❙⟨?B❙⟩ ⊓ ❙⟨?C❙⟩)
           → (❙⟨⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A)❙⟩ ↔ (❙⟨φ❙⟩ ⊓ ❙⟨⨆ (map ⨅ ?A)❙⟩))
           → ❙⟨⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A)❙⟩ ↔ ((❙⟨φ❙⟩ ⊓ ❙⟨?B❙⟩) ⊓ ❙⟨?C❙⟩)"
    have "∀𝔐. 𝔐 ⊨⇩p⇩r⇩o⇩p ?φ" by simp
    hence "⊢ ❙⦇ ?φ ❙⦈" using propositional_semantics by blast
    thus ?thesis
      by simp
  qed
  ultimately have "⊢ ⨆ (map (⨅ ∘ (λ φs. φ # φs)) ?A) ↔ ((φ ⊓ ?B) ⊓ ?C)"
    using modus_ponens conj_dnf_distribute
    by blast
  moreover
  have "⨅ ∘ (@) (φ # Φ) = ⨅ ∘ (#) φ ∘ (@) Φ" by auto
  hence
    "⊢ ⨆ (map (⨅ ∘ (@) (φ # Φ)) Λ) ↔ (⨅ (φ # Φ) ⊓ ?C)
   = ⊢ ⨆ (map (⨅ ∘ (#) φ) ?A) ↔ ((φ ⊓ ?B) ⊓ ?C)"
    by simp
  ultimately show ?case by meson
qed

notation FuncSet.funcset (infixr "→" 60)

end