Theory Propositional_Wff

section ‹Propositional Well-Formed Formulas›

theory Propositional_Wff
  imports
    Syntax
    Boolean_Algebra
begin

subsection ‹Syntax›

inductive_set pwffs :: "form set" where
  T_pwff: "T⇘o⇙ ∈ pwffs"
| F_pwff: "F⇘o⇙ ∈ pwffs"
| var_pwff: "p⇘o⇙ ∈ pwffs"
| neg_pwff: "∼⇧𝒬 A ∈ pwffs" if "A ∈ pwffs"
| conj_pwff: "A ∧⇧𝒬 B ∈ pwffs" if "A ∈ pwffs" and "B ∈ pwffs"
| disj_pwff: "A ∨⇧𝒬 B ∈ pwffs" if "A ∈ pwffs" and "B ∈ pwffs"
| imp_pwff: "A ⊃⇧𝒬 B ∈ pwffs" if "A ∈ pwffs" and "B ∈ pwffs"
| eqv_pwff: "A ≡⇧𝒬 B ∈ pwffs" if "A ∈ pwffs" and "B ∈ pwffs"

lemmas [intro!] = pwffs.intros

lemma pwffs_distinctnesses [induct_simp]:
  shows "T⇘o⇙ ≠ F⇘o⇙"
  and "T⇘o⇙ ≠ p⇘o⇙"
  and "T⇘o⇙ ≠ ∼⇧𝒬 A"
  and "T⇘o⇙ ≠ A ∧⇧𝒬 B"
  and "T⇘o⇙ ≠ A ∨⇧𝒬 B"
  and "T⇘o⇙ ≠ A ⊃⇧𝒬 B"
  and "T⇘o⇙ ≠ A ≡⇧𝒬 B"
  and "F⇘o⇙ ≠ p⇘o⇙"
  and "F⇘o⇙ ≠ ∼⇧𝒬 A"
  and "F⇘o⇙ ≠ A ∧⇧𝒬 B"
  and "F⇘o⇙ ≠ A ∨⇧𝒬 B"
  and "F⇘o⇙ ≠ A ⊃⇧𝒬 B"
  and "F⇘o⇙ ≠ A ≡⇧𝒬 B"
  and "p⇘o⇙ ≠ ∼⇧𝒬 A"
  and "p⇘o⇙ ≠ A ∧⇧𝒬 B"
  and "p⇘o⇙ ≠ A ∨⇧𝒬 B"
  and "p⇘o⇙ ≠ A ⊃⇧𝒬 B"
  and "p⇘o⇙ ≠ A ≡⇧𝒬 B"
  and "∼⇧𝒬 A ≠ B ∧⇧𝒬 C"
  and "∼⇧𝒬 A ≠ B ∨⇧𝒬 C"
  and "∼⇧𝒬 A ≠ B ⊃⇧𝒬 C"
  and "¬ (B = F⇘o⇙ ∧ A = C) ⟹ ∼⇧𝒬 A ≠ B ≡⇧𝒬 C" ― ‹\<^term>‹∼⇧𝒬 A› is the same as \<^term>‹F⇘o⇙ ≡⇧𝒬 A››
  and "A ∧⇧𝒬 B ≠ C ∨⇧𝒬 D"
  and "A ∧⇧𝒬 B ≠ C ⊃⇧𝒬 D"
  and "A ∧⇧𝒬 B ≠ C ≡⇧𝒬 D"
  and "A ∨⇧𝒬 B ≠ C ⊃⇧𝒬 D"
  and "A ∨⇧𝒬 B ≠ C ≡⇧𝒬 D"
  and "A ⊃⇧𝒬 B ≠ C ≡⇧𝒬 D"
  by simp_all

lemma pwffs_injectivities [induct_simp]:
  shows "∼⇧𝒬 A = ∼⇧𝒬 A' ⟹ A = A'"
  and "A ∧⇧𝒬 B = A' ∧⇧𝒬 B' ⟹ A = A' ∧ B = B'"
  and "A ∨⇧𝒬 B = A' ∨⇧𝒬 B' ⟹ A = A' ∧ B = B'"
  and "A ⊃⇧𝒬 B = A' ⊃⇧𝒬 B' ⟹ A = A' ∧ B = B'"
  and "A ≡⇧𝒬 B = A' ≡⇧𝒬 B' ⟹ A = A' ∧ B = B'"
  by simp_all

lemma pwff_from_neg_pwff [elim!]:
  assumes "∼⇧𝒬 A ∈ pwffs"
  shows "A ∈ pwffs"
  using assms by cases simp_all

lemma pwffs_from_conj_pwff [elim!]:
  assumes "A ∧⇧𝒬 B ∈ pwffs"
  shows "{A, B} ⊆ pwffs"
  using assms by cases simp_all

lemma pwffs_from_disj_pwff [elim!]:
  assumes "A ∨⇧𝒬 B ∈ pwffs"
  shows "{A, B} ⊆ pwffs"
  using assms by cases simp_all

lemma pwffs_from_imp_pwff [elim!]:
  assumes "A ⊃⇧𝒬 B ∈ pwffs"
  shows "{A, B} ⊆ pwffs"
  using assms by cases simp_all

lemma pwffs_from_eqv_pwff [elim!]:
  assumes "A ≡⇧𝒬 B ∈ pwffs"
  shows "{A, B} ⊆ pwffs"
  using assms by cases (simp_all, use F_pwff in fastforce)

lemma pwffs_subset_of_wffso:
  shows "pwffs ⊆ wffs⇘o⇙"
proof
  fix A
  assume "A ∈ pwffs"
  then show "A ∈ wffs⇘o⇙"
    by induction auto
qed

lemma pwff_free_vars_simps [simp]:
  shows T_fv: "free_vars T⇘o⇙ = {}"
  and F_fv: "free_vars F⇘o⇙ = {}"
  and var_fv: "free_vars (p⇘o⇙) = {(p, o)}"
  and neg_fv: "free_vars (∼⇧𝒬 A) = free_vars A"
  and conj_fv: "free_vars (A ∧⇧𝒬 B) = free_vars A ∪ free_vars B"
  and disj_fv: "free_vars (A ∨⇧𝒬 B) = free_vars A ∪ free_vars B"
  and imp_fv: "free_vars (A ⊃⇧𝒬 B) = free_vars A ∪ free_vars B"
  and eqv_fv: "free_vars (A ≡⇧𝒬 B) = free_vars A ∪ free_vars B"
  by force+

lemma pwffs_free_vars_are_propositional:
  assumes "A ∈ pwffs"
  and "v ∈ free_vars A"
  obtains p where "v = (p, o)"
using assms by (induction A arbitrary: thesis) auto

lemma is_free_for_in_pwff [intro]:
  assumes "A ∈ pwffs"
  and "v ∈ free_vars A"
  shows "is_free_for B v A"
using assms proof (induction A)
  case (neg_pwff C)
  then show ?case
    using is_free_for_in_neg by simp
next
  case (conj_pwff C D)
  from conj_pwff.prems consider
    (a) "v ∈ free_vars C" and "v ∈ free_vars D"
  | (b) "v ∈ free_vars C" and "v ∉ free_vars D"
  | (c) "v ∉ free_vars C" and "v ∈ free_vars D"
    by auto
  then show ?case
  proof cases
    case a
    then show ?thesis
      using conj_pwff.IH by (intro is_free_for_in_conj)
  next
    case b
    have "is_free_for B v C"
      by (fact conj_pwff.IH(1)[OF b(1)])
    moreover from b(2) have "is_free_for B v D"
      using is_free_at_in_free_vars by blast
    ultimately show ?thesis
      by (rule is_free_for_in_conj)
  next
    case c
    from c(1) have "is_free_for B v C"
      using is_free_at_in_free_vars by blast
    moreover have "is_free_for B v D"
      by (fact conj_pwff.IH(2)[OF c(2)])
    ultimately show ?thesis
      by (rule is_free_for_in_conj)
  qed
next
  case (disj_pwff C D)
  from disj_pwff.prems consider
    (a) "v ∈ free_vars C" and "v ∈ free_vars D"
  | (b) "v ∈ free_vars C" and "v ∉ free_vars D"
  | (c) "v ∉ free_vars C" and "v ∈ free_vars D"
    by auto
  then show ?case
  proof cases
    case a
    then show ?thesis
      using disj_pwff.IH by (intro is_free_for_in_disj)
  next
    case b
    have "is_free_for B v C"
      by (fact disj_pwff.IH(1)[OF b(1)])
    moreover from b(2) have "is_free_for B v D"
      using is_free_at_in_free_vars by blast
    ultimately show ?thesis
      by (rule is_free_for_in_disj)
  next
    case c
    from c(1) have "is_free_for B v C"
      using is_free_at_in_free_vars by blast
    moreover have "is_free_for B v D"
      by (fact disj_pwff.IH(2)[OF c(2)])
    ultimately show ?thesis
      by (rule is_free_for_in_disj)
  qed
next
  case (imp_pwff C D)
  from imp_pwff.prems consider
    (a) "v ∈ free_vars C" and "v ∈ free_vars D"
  | (b) "v ∈ free_vars C" and "v ∉ free_vars D"
  | (c) "v ∉ free_vars C" and "v ∈ free_vars D"
    by auto
  then show ?case
  proof cases
    case a
    then show ?thesis
      using imp_pwff.IH by (intro is_free_for_in_imp)
  next
    case b
    have "is_free_for B v C"
      by (fact imp_pwff.IH(1)[OF b(1)])
    moreover from b(2) have "is_free_for B v D"
      using is_free_at_in_free_vars by blast
    ultimately show ?thesis
      by (rule is_free_for_in_imp)
  next
    case c
    from c(1) have "is_free_for B v C"
      using is_free_at_in_free_vars by blast
    moreover have "is_free_for B v D"
      by (fact imp_pwff.IH(2)[OF c(2)])
    ultimately show ?thesis
      by (rule is_free_for_in_imp)
  qed
next
  case (eqv_pwff C D)
  from eqv_pwff.prems consider
    (a) "v ∈ free_vars C" and "v ∈ free_vars D"
  | (b) "v ∈ free_vars C" and "v ∉ free_vars D"
  | (c) "v ∉ free_vars C" and "v ∈ free_vars D"
    by auto
  then show ?case
  proof cases
    case a
    then show ?thesis
      using eqv_pwff.IH by (intro is_free_for_in_equivalence)
  next
    case b
    have "is_free_for B v C"
      by (fact eqv_pwff.IH(1)[OF b(1)])
    moreover from b(2) have "is_free_for B v D"
      using is_free_at_in_free_vars by blast
    ultimately show ?thesis
      by (rule is_free_for_in_equivalence)
  next
    case c
    from c(1) have "is_free_for B v C"
      using is_free_at_in_free_vars by blast
    moreover have "is_free_for B v D"
      by (fact eqv_pwff.IH(2)[OF c(2)])
    ultimately show ?thesis
      by (rule is_free_for_in_equivalence)
  qed
qed auto

subsection ‹Semantics›

text ‹Assignment of truth values to propositional variables:›

definition is_tv_assignment :: "(nat ⇒ V) ⇒ bool" where
  [iff]: "is_tv_assignment φ ⟷ (∀p. φ p ∈ elts 𝔹)"

text ‹Denotation of a pwff:›

definition is_pwff_denotation_function where
  [iff]: "is_pwff_denotation_function 𝒱 ⟷
    (
      ∀φ. is_tv_assignment φ ⟶
      (
        𝒱 φ T⇘o⇙ = ❙T ∧
        𝒱 φ F⇘o⇙ = ❙F ∧
        (∀p. 𝒱 φ (p⇘o⇙) = φ p) ∧
        (∀A. A ∈ pwffs ⟶ 𝒱 φ (∼⇧𝒬 A) = ∼ 𝒱 φ A) ∧
        (∀A B. A ∈ pwffs ∧ B ∈ pwffs ⟶ 𝒱 φ (A ∧⇧𝒬 B) = 𝒱 φ A ❙∧ 𝒱 φ B) ∧
        (∀A B. A ∈ pwffs ∧ B ∈ pwffs ⟶ 𝒱 φ (A ∨⇧𝒬 B) = 𝒱 φ A ❙∨ 𝒱 φ B) ∧
        (∀A B. A ∈ pwffs ∧ B ∈ pwffs ⟶ 𝒱 φ (A ⊃⇧𝒬 B) = 𝒱 φ A ❙⊃ 𝒱 φ B) ∧
        (∀A B. A ∈ pwffs ∧ B ∈ pwffs ⟶ 𝒱 φ (A ≡⇧𝒬 B) = 𝒱 φ A ❙≡ 𝒱 φ B)
      )
    )"

lemma pwff_denotation_is_truth_value:
  assumes "A ∈ pwffs"
  and "is_tv_assignment φ"
  and "is_pwff_denotation_function 𝒱"
  shows "𝒱 φ A ∈ elts 𝔹"
using assms(1) proof induction
  case (neg_pwff A)
  then have "𝒱 φ (∼⇧𝒬 A) = ∼ 𝒱 φ A"
    using assms(2,3) by auto
  then show ?case
    using neg_pwff.IH by auto
next
  case (conj_pwff A B)
  then have "𝒱 φ (A ∧⇧𝒬 B) = 𝒱 φ A ❙∧ 𝒱 φ B"
    using assms(2,3) by auto
  then show ?case
    using conj_pwff.IH by auto
next
  case (disj_pwff A B)
  then have "𝒱 φ (A ∨⇧𝒬 B) = 𝒱 φ A ❙∨ 𝒱 φ B"
    using assms(2,3) by auto
  then show ?case
    using disj_pwff.IH by auto
next
  case (imp_pwff A B)
  then have "𝒱 φ (A ⊃⇧𝒬 B) = 𝒱 φ A ❙⊃ 𝒱 φ B"
    using assms(2,3) by blast
  then show ?case
    using imp_pwff.IH by auto
next
  case (eqv_pwff A B)
  then have "𝒱 φ (A ≡⇧𝒬 B) = 𝒱 φ A ❙≡ 𝒱 φ B"
    using assms(2,3) by blast
  then show ?case
    using eqv_pwff.IH by auto
qed (use assms(2,3) in auto)

lemma closed_pwff_is_meaningful_regardless_of_assignment:
  assumes "A ∈ pwffs"
  and "free_vars A = {}"
  and "is_tv_assignment φ"
  and "is_tv_assignment ψ"
  and "is_pwff_denotation_function 𝒱"
  shows "𝒱 φ A = 𝒱 ψ A"
using assms(1,2) proof induction
  case T_pwff
  have "𝒱 φ T⇘o⇙ = ❙T"
    using assms(3,5) by blast
  also have "… = 𝒱 ψ T⇘o⇙"
    using assms(4,5) by force
  finally show ?case .
next
  case F_pwff
  have "𝒱 φ F⇘o⇙ = ❙F"
    using assms(3,5) by blast
  also have "… = 𝒱 ψ F⇘o⇙"
    using assms(4,5) by force
  finally show ?case .
next
  case (var_pwff p) ― ‹impossible case›
  then show ?case
    by simp
next
  case (neg_pwff A)
  from ‹free_vars (∼⇧𝒬 A) = {}› have "free_vars A = {}"
    by simp
  have "𝒱 φ (∼⇧𝒬 A) = ∼ 𝒱 φ A"
    using assms(3,5) and neg_pwff.hyps by auto
  also from ‹free_vars A = {}› have "… = ∼ 𝒱 ψ A"
    using assms(3-5) and neg_pwff.IH by presburger
  also have "… = 𝒱 ψ (∼⇧𝒬 A)"
    using assms(4,5) and neg_pwff.hyps by simp
  finally show ?case .
next
  case (conj_pwff A B)
  from ‹free_vars (A ∧⇧𝒬 B) = {}› have "free_vars A = {}" and "free_vars B = {}"
    by simp_all
  have "𝒱 φ (A ∧⇧𝒬 B) = 𝒱 φ A ❙∧ 𝒱 φ B"
    using assms(3,5) and conj_pwff.hyps(1,2) by auto
  also from ‹free_vars A = {}› and ‹free_vars B = {}› have "… = 𝒱 ψ A ❙∧ 𝒱 ψ B"
    using conj_pwff.IH(1,2) by presburger
  also have "… = 𝒱 ψ (A ∧⇧𝒬 B)"
    using assms(4,5) and conj_pwff.hyps(1,2) by fastforce
  finally show ?case .
next
  case (disj_pwff A B)
  from ‹free_vars (A ∨⇧𝒬 B) = {}› have "free_vars A = {}" and "free_vars B = {}"
    by simp_all
  have "𝒱 φ (A ∨⇧𝒬 B) = 𝒱 φ A ❙∨ 𝒱 φ B"
    using assms(3,5) and disj_pwff.hyps(1,2) by auto
  also from ‹free_vars A = {}› and ‹free_vars B = {}› have "… = 𝒱 ψ A ❙∨ 𝒱 ψ B"
    using disj_pwff.IH(1,2) by presburger
  also have "… = 𝒱 ψ (A ∨⇧𝒬 B)"
    using assms(4,5) and disj_pwff.hyps(1,2) by fastforce
  finally show ?case .
next
  case (imp_pwff A B)
  from ‹free_vars (A ⊃⇧𝒬 B) = {}› have "free_vars A = {}" and "free_vars B = {}"
    by simp_all
  have "𝒱 φ (A ⊃⇧𝒬 B) = 𝒱 φ A ❙⊃ 𝒱 φ B"
    using assms(3,5) and imp_pwff.hyps(1,2) by auto
  also from ‹free_vars A = {}› and ‹free_vars B = {}› have "… = 𝒱 ψ A ❙⊃ 𝒱 ψ B"
    using imp_pwff.IH(1,2) by presburger
  also have "… = 𝒱 ψ (A ⊃⇧𝒬 B)"
    using assms(4,5) and imp_pwff.hyps(1,2) by fastforce
  finally show ?case .
next
  case (eqv_pwff A B)
  from ‹free_vars (A ≡⇧𝒬 B) = {}› have "free_vars A = {}" and "free_vars B = {}"
    by simp_all
  have "𝒱 φ (A ≡⇧𝒬 B) = 𝒱 φ A ❙≡ 𝒱 φ B"
    using assms(3,5) and eqv_pwff.hyps(1,2) by auto
  also from ‹free_vars A = {}› and ‹free_vars B = {}› have "… = 𝒱 ψ A ❙≡ 𝒱 ψ B"
    using eqv_pwff.IH(1,2) by presburger
  also have "… = 𝒱 ψ (A ≡⇧𝒬 B)"
    using assms(4,5) and eqv_pwff.hyps(1,2) by fastforce
  finally show ?case .
qed

inductive 𝒱⇩B_graph for φ where
  𝒱⇩B_graph_T: "𝒱⇩B_graph φ T⇘o⇙ ❙T"
| 𝒱⇩B_graph_F: "𝒱⇩B_graph φ F⇘o⇙ ❙F"
| 𝒱⇩B_graph_var: "𝒱⇩B_graph φ (p⇘o⇙) (φ p)"
| 𝒱⇩B_graph_neg: "𝒱⇩B_graph φ (∼⇧𝒬 A) (∼ b⇩A)" if "𝒱⇩B_graph φ A b⇩A"
| 𝒱⇩B_graph_conj: "𝒱⇩B_graph φ (A ∧⇧𝒬 B) (b⇩A ❙∧ b⇩B)" if "𝒱⇩B_graph φ A b⇩A" and "𝒱⇩B_graph φ B b⇩B"
| 𝒱⇩B_graph_disj: "𝒱⇩B_graph φ (A ∨⇧𝒬 B) (b⇩A ❙∨ b⇩B)" if "𝒱⇩B_graph φ A b⇩A" and "𝒱⇩B_graph φ B b⇩B"
| 𝒱⇩B_graph_imp: "𝒱⇩B_graph φ (A ⊃⇧𝒬 B) (b⇩A ❙⊃ b⇩B)" if "𝒱⇩B_graph φ A b⇩A" and "𝒱⇩B_graph φ B b⇩B"
| 𝒱⇩B_graph_eqv: "𝒱⇩B_graph φ (A ≡⇧𝒬 B) (b⇩A ❙≡ b⇩B)" if "𝒱⇩B_graph φ A b⇩A" and "𝒱⇩B_graph φ B b⇩B" and "A ≠ F⇘o⇙"

lemmas [intro!] = 𝒱⇩B_graph.intros

lemma 𝒱⇩B_graph_denotation_is_truth_value [elim!]:
  assumes "𝒱⇩B_graph φ A b"
  and "is_tv_assignment φ"
  shows "b ∈ elts 𝔹"
using assms proof induction
  case (𝒱⇩B_graph_neg A b⇩A)
  show ?case
    using 𝒱⇩B_graph_neg.IH[OF assms(2)] by force
next
  case (𝒱⇩B_graph_conj A b⇩A B b⇩B)
  then show ?case
    using 𝒱⇩B_graph_conj.IH and assms(2) by force
next
  case (𝒱⇩B_graph_disj A b⇩A B b⇩B)
  then show ?case
    using 𝒱⇩B_graph_disj.IH and assms(2) by force
next
  case (𝒱⇩B_graph_imp A b⇩A B b⇩B)
  then show ?case
    using 𝒱⇩B_graph_imp.IH and assms(2) by force
next
  case (𝒱⇩B_graph_eqv A b⇩A B b⇩B)
  then show ?case
    using 𝒱⇩B_graph_eqv.IH and assms(2) by force
qed simp_all

lemma 𝒱⇩B_graph_denotation_uniqueness:
  assumes "A ∈ pwffs"
  and "is_tv_assignment φ"
  and "𝒱⇩B_graph φ A b" and "𝒱⇩B_graph φ A b'"
  shows "b = b'"
using assms(3,1,4) proof (induction arbitrary: b')
  case 𝒱⇩B_graph_T
  from ‹𝒱⇩B_graph φ T⇘o⇙ b'› show ?case
    by (cases rule: 𝒱⇩B_graph.cases) simp_all
next
  case 𝒱⇩B_graph_F
  from ‹𝒱⇩B_graph φ F⇘o⇙ b'› show ?case
    by (cases rule: 𝒱⇩B_graph.cases) simp_all
next
  case (𝒱⇩B_graph_var p)
  from ‹𝒱⇩B_graph φ (p⇘o⇙) b'› show ?case
    by (cases rule: 𝒱⇩B_graph.cases) simp_all
next
  case (𝒱⇩B_graph_neg A b⇩A)
  with ‹𝒱⇩B_graph φ (∼⇧𝒬 A) b'› have "𝒱⇩B_graph φ A (∼ b')"
  proof (cases rule: 𝒱⇩B_graph.cases)
    case (𝒱⇩B_graph_neg A' b⇩A)
    from ‹∼⇧𝒬 A = ∼⇧𝒬 A'› have "A = A'"
      by simp
    with ‹𝒱⇩B_graph φ A' b⇩A› have "𝒱⇩B_graph φ A b⇩A"
      by simp
    moreover have "b⇩A = ∼ b'"
    proof -
      have "b⇩A ∈ elts 𝔹"
        by (fact 𝒱⇩B_graph_denotation_is_truth_value[OF 𝒱⇩B_graph_neg(3) assms(2)])
      moreover from ‹b⇩A ∈ elts 𝔹› and 𝒱⇩B_graph_neg(2) have "∼ b' ∈ elts 𝔹"
        by fastforce
      ultimately show ?thesis
        using 𝒱⇩B_graph_neg(2) by fastforce
    qed
    ultimately show ?thesis
      by blast
  qed simp_all
  moreover from 𝒱⇩B_graph_neg.prems(1) have "A ∈ pwffs"
    by (force elim: pwffs.cases)
  moreover have "b⇩A ∈ elts 𝔹" and "b' ∈ elts 𝔹" and "b⇩A = ∼ b'"
  proof -
    show "b⇩A ∈ elts 𝔹"
      by (fact 𝒱⇩B_graph_denotation_is_truth_value[OF ‹𝒱⇩B_graph φ A b⇩A› assms(2)])
    show "b' ∈ elts 𝔹"
      by (fact 𝒱⇩B_graph_denotation_is_truth_value[OF ‹𝒱⇩B_graph φ (∼⇧𝒬 A) b'› assms(2)])
    show "b⇩A = ∼ b'"
      by (fact 𝒱⇩B_graph_neg(2)[OF ‹A ∈ pwffs› ‹𝒱⇩B_graph φ A (∼ b')›])
  qed
  ultimately show ?case
    by force
next
  case (𝒱⇩B_graph_conj A b⇩A B b⇩B)
  with ‹𝒱⇩B_graph φ (A ∧⇧𝒬 B) b'› obtain b⇩A' and b⇩B'
    where "b' = b⇩A' ❙∧ b⇩B'" and "𝒱⇩B_graph φ A b⇩A'" and "𝒱⇩B_graph φ B b⇩B'"
    by (cases rule: 𝒱⇩B_graph.cases) simp_all
  moreover have "A ∈ pwffs" and "B ∈ pwffs"
    using pwffs_from_conj_pwff[OF 𝒱⇩B_graph_conj.prems(1)] by blast+
  ultimately show ?case
    using 𝒱⇩B_graph_conj.IH and 𝒱⇩B_graph_conj.prems(2) by blast
next
  case (𝒱⇩B_graph_disj A b⇩A B b⇩B)
  from ‹𝒱⇩B_graph φ (A ∨⇧𝒬 B) b'› obtain b⇩A' and b⇩B'
    where "b' = b⇩A' ❙∨ b⇩B'" and "𝒱⇩B_graph φ A b⇩A'" and "𝒱⇩B_graph φ B b⇩B'"
    by (cases rule: 𝒱⇩B_graph.cases) simp_all
  moreover have "A ∈ pwffs" and "B ∈ pwffs"
    using pwffs_from_disj_pwff[OF 𝒱⇩B_graph_disj.prems(1)] by blast+
  ultimately show ?case
    using 𝒱⇩B_graph_disj.IH and 𝒱⇩B_graph_disj.prems(2) by blast
next
  case (𝒱⇩B_graph_imp A b⇩A B b⇩B)
  from ‹𝒱⇩B_graph φ (A ⊃⇧𝒬 B) b'› obtain b⇩A' and b⇩B'
    where "b' = b⇩A' ❙⊃ b⇩B'" and "𝒱⇩B_graph φ A b⇩A'" and "𝒱⇩B_graph φ B b⇩B'"
    by (cases rule: 𝒱⇩B_graph.cases) simp_all
  moreover have "A ∈ pwffs" and "B ∈ pwffs"
    using pwffs_from_imp_pwff[OF 𝒱⇩B_graph_imp.prems(1)] by blast+
  ultimately show ?case
    using 𝒱⇩B_graph_imp.IH and 𝒱⇩B_graph_imp.prems(2) by blast
next
  case (𝒱⇩B_graph_eqv A b⇩A B b⇩B)
  with ‹𝒱⇩B_graph φ (A ≡⇧𝒬 B) b'› obtain b⇩A' and b⇩B'
    where "b' = b⇩A' ❙≡ b⇩B'" and "𝒱⇩B_graph φ A b⇩A'" and "𝒱⇩B_graph φ B b⇩B'"
    by (cases rule: 𝒱⇩B_graph.cases) simp_all
  moreover have "A ∈ pwffs" and "B ∈ pwffs"
    using pwffs_from_eqv_pwff[OF 𝒱⇩B_graph_eqv.prems(1)] by blast+
  ultimately show ?case
    using 𝒱⇩B_graph_eqv.IH and 𝒱⇩B_graph_eqv.prems(2) by blast
qed

lemma 𝒱⇩B_graph_denotation_existence:
  assumes "A ∈ pwffs"
  and "is_tv_assignment φ"
  shows "∃b. 𝒱⇩B_graph φ A b"
using assms proof induction
  case (eqv_pwff A B)
  then obtain b⇩A and b⇩B where "𝒱⇩B_graph φ A b⇩A" and "𝒱⇩B_graph φ B b⇩B"
    by blast
  then show ?case
  proof (cases "A ≠ F⇘o⇙")
    case True
    then show ?thesis
      using eqv_pwff.IH and eqv_pwff.prems by blast
  next
    case False
    then have "A = F⇘o⇙"
      by blast
    then show ?thesis
      using 𝒱⇩B_graph_neg[OF ‹𝒱⇩B_graph φ B b⇩B›] by auto
  qed
qed blast+

lemma 𝒱⇩B_graph_is_functional:
  assumes "A ∈ pwffs"
  and "is_tv_assignment φ"
  shows "∃!b. 𝒱⇩B_graph φ A b"
  using assms and 𝒱⇩B_graph_denotation_existence and 𝒱⇩B_graph_denotation_uniqueness by blast

definition 𝒱⇩B :: "(nat ⇒ V) ⇒ form ⇒ V" where
  [simp]: "𝒱⇩B φ A = (THE b. 𝒱⇩B_graph φ A b)"

lemma 𝒱⇩B_equality:
  assumes "A ∈ pwffs"
  and "is_tv_assignment φ"
  and "𝒱⇩B_graph φ A b"
  shows "𝒱⇩B φ A = b"
  unfolding 𝒱⇩B_def using assms using 𝒱⇩B_graph_denotation_uniqueness by blast

lemma 𝒱⇩B_graph_𝒱⇩B:
  assumes "A ∈ pwffs"
  and "is_tv_assignment φ"
  shows "𝒱⇩B_graph φ A (𝒱⇩B φ A)"
  using 𝒱⇩B_equality[OF assms] and 𝒱⇩B_graph_is_functional[OF assms] by blast

named_theorems 𝒱⇩B_simps

lemma 𝒱⇩B_T [𝒱⇩B_simps]:
  assumes "is_tv_assignment φ"
  shows "𝒱⇩B φ T⇘o⇙ = ❙T"
  by (rule 𝒱⇩B_equality[OF T_pwff assms], intro 𝒱⇩B_graph_T)

lemma 𝒱⇩B_F [𝒱⇩B_simps]:
  assumes "is_tv_assignment φ"
  shows "𝒱⇩B φ F⇘o⇙ = ❙F"
  by (rule 𝒱⇩B_equality[OF F_pwff assms], intro 𝒱⇩B_graph_F)

lemma 𝒱⇩B_var [𝒱⇩B_simps]:
  assumes "is_tv_assignment φ"
  shows "𝒱⇩B φ (p⇘o⇙) = φ p"
  by (rule 𝒱⇩B_equality[OF var_pwff assms], intro 𝒱⇩B_graph_var)

lemma 𝒱⇩B_neg [𝒱⇩B_simps]:
  assumes "A ∈ pwffs"
  and "is_tv_assignment φ"
  shows "𝒱⇩B φ (∼⇧𝒬 A) = ∼ 𝒱⇩B φ A"
  by (rule 𝒱⇩B_equality[OF neg_pwff[OF assms(1)] assms(2)], intro 𝒱⇩B_graph_neg 𝒱⇩B_graph_𝒱⇩B[OF assms])

lemma 𝒱⇩B_disj [𝒱⇩B_simps]:
  assumes "A ∈ pwffs" and "B ∈ pwffs"
  and "is_tv_assignment φ"
  shows "𝒱⇩B φ (A ∨⇧𝒬 B) = 𝒱⇩B φ A ❙∨ 𝒱⇩B φ B"
proof -
  from assms(1,3) have "𝒱⇩B_graph φ A (𝒱⇩B φ A)"
    by (intro 𝒱⇩B_graph_𝒱⇩B)
  moreover from assms(2,3) have "𝒱⇩B_graph φ B (𝒱⇩B φ B)"
    by (intro 𝒱⇩B_graph_𝒱⇩B)
  ultimately have "𝒱⇩B_graph φ (A ∨⇧𝒬 B) (𝒱⇩B φ A ❙∨ 𝒱⇩B φ B)"
    by (intro 𝒱⇩B_graph_disj)
  with assms show ?thesis
    using disj_pwff by (intro 𝒱⇩B_equality)
qed

lemma 𝒱⇩B_conj [𝒱⇩B_simps]:
  assumes "A ∈ pwffs" and "B ∈ pwffs"
  and "is_tv_assignment φ"
  shows "𝒱⇩B φ (A ∧⇧𝒬 B) = 𝒱⇩B φ A ❙∧ 𝒱⇩B φ B"
proof -
  from assms(1,3) have "𝒱⇩B_graph φ A (𝒱⇩B φ A)"
    by (intro 𝒱⇩B_graph_𝒱⇩B)
  moreover from assms(2,3) have "𝒱⇩B_graph φ B (𝒱⇩B φ B)"
    by (intro 𝒱⇩B_graph_𝒱⇩B)
  ultimately have "𝒱⇩B_graph φ (A ∧⇧𝒬 B) (𝒱⇩B φ A ❙∧ 𝒱⇩B φ B)"
    by (intro 𝒱⇩B_graph_conj)
  with assms show ?thesis
    using conj_pwff by (intro 𝒱⇩B_equality)
qed

lemma 𝒱⇩B_imp [𝒱⇩B_simps]:
  assumes "A ∈ pwffs" and "B ∈ pwffs"
  and "is_tv_assignment φ"
  shows "𝒱⇩B φ (A ⊃⇧𝒬 B) = 𝒱⇩B φ A ❙⊃ 𝒱⇩B φ B"
proof -
  from assms(1,3) have "𝒱⇩B_graph φ A (𝒱⇩B φ A)"
    by (intro 𝒱⇩B_graph_𝒱⇩B)
  moreover from assms(2,3) have "𝒱⇩B_graph φ B (𝒱⇩B φ B)"
    by (intro 𝒱⇩B_graph_𝒱⇩B)
  ultimately have "𝒱⇩B_graph φ (A ⊃⇧𝒬 B) (𝒱⇩B φ A ❙⊃ 𝒱⇩B φ B)"
    by (intro 𝒱⇩B_graph_imp)
  with assms show ?thesis
    using imp_pwff by (intro 𝒱⇩B_equality)
qed

lemma 𝒱⇩B_eqv [𝒱⇩B_simps]:
  assumes "A ∈ pwffs" and "B ∈ pwffs"
  and "is_tv_assignment φ"
  shows "𝒱⇩B φ (A ≡⇧𝒬 B) = 𝒱⇩B φ A ❙≡ 𝒱⇩B φ B"
proof (cases "A = F⇘o⇙")
  case True
  then show ?thesis
    using 𝒱⇩B_F[OF assms(3)] and 𝒱⇩B_neg[OF assms(2,3)] by force
next
  case False
  from assms(1,3) have "𝒱⇩B_graph φ A (𝒱⇩B φ A)"
    by (intro 𝒱⇩B_graph_𝒱⇩B)
  moreover from assms(2,3) have "𝒱⇩B_graph φ B (𝒱⇩B φ B)"
    by (intro 𝒱⇩B_graph_𝒱⇩B)
  ultimately have "𝒱⇩B_graph φ (A ≡⇧𝒬 B) (𝒱⇩B φ A ❙≡ 𝒱⇩B φ B)"
    using False by (intro 𝒱⇩B_graph_eqv)
  with assms show ?thesis
    using eqv_pwff by (intro 𝒱⇩B_equality)
qed

declare pwffs.intros [𝒱⇩B_simps]

lemma pwff_denotation_function_existence:
  shows "is_pwff_denotation_function 𝒱⇩B"
  using 𝒱⇩B_simps by simp

text ‹Tautologies:›

definition is_tautology :: "form ⇒ bool" where
  [iff]: "is_tautology A ⟷ A ∈ pwffs ∧ (∀φ. is_tv_assignment φ ⟶ 𝒱⇩B φ A = ❙T)"

lemma tautology_is_wffo:
  assumes "is_tautology A"
  shows "A ∈ wffs⇘o⇙"
  using assms and pwffs_subset_of_wffso by blast

lemma propositional_implication_reflexivity_is_tautology:
  shows "is_tautology (p⇘o⇙ ⊃⇧𝒬 p⇘o⇙)"
  using 𝒱⇩B_simps by simp

lemma propositional_principle_of_simplification_is_tautology:
  shows "is_tautology (p⇘o⇙ ⊃⇧𝒬 (r⇘o⇙ ⊃⇧𝒬 p⇘o⇙))"
  using 𝒱⇩B_simps by simp

lemma closed_pwff_denotation_uniqueness:
  assumes "A ∈ pwffs" and "free_vars A = {}"
  obtains b where "∀φ. is_tv_assignment φ ⟶ 𝒱⇩B φ A = b"
  using assms
  by (meson closed_pwff_is_meaningful_regardless_of_assignment pwff_denotation_function_existence)

lemma pwff_substitution_simps:
  shows "❙S {(p, o) ↣ A} T⇘o⇙ = T⇘o⇙"
  and "❙S {(p, o) ↣ A} F⇘o⇙ = F⇘o⇙"
  and "❙S {(p, o) ↣ A} (p'⇘o⇙) = (if p = p' then A else (p'⇘o⇙))"
  and "❙S {(p, o) ↣ A} (∼⇧𝒬 B) = ∼⇧𝒬 (❙S {(p, o) ↣ A} B)"
  and "❙S {(p, o) ↣ A} (B ∧⇧𝒬 C) = (❙S {(p, o) ↣ A} B) ∧⇧𝒬 (❙S {(p, o) ↣ A} C)"
  and "❙S {(p, o) ↣ A} (B ∨⇧𝒬 C) = (❙S {(p, o) ↣ A} B) ∨⇧𝒬 (❙S {(p, o) ↣ A} C)"
  and "❙S {(p, o) ↣ A} (B ⊃⇧𝒬 C) = (❙S {(p, o) ↣ A} B) ⊃⇧𝒬 (❙S {(p, o) ↣ A} C)"
  and "❙S {(p, o) ↣ A} (B ≡⇧𝒬 C) = (❙S {(p, o) ↣ A} B) ≡⇧𝒬 (❙S {(p, o) ↣ A} C)"
  by simp_all

lemma pwff_substitution_in_pwffs:
  assumes "A ∈ pwffs" and "B ∈ pwffs"
  shows "❙S {(p, o) ↣ A} B ∈ pwffs"
using assms(2) proof induction
  case T_pwff
  then show ?case
    using pwffs.T_pwff by simp
next
  case F_pwff
  then show ?case
    using pwffs.F_pwff by simp
next
  case (var_pwff p)
  from assms(1) show ?case
    using pwffs.var_pwff by simp
next
  case (neg_pwff A)
  then show ?case
    using pwff_substitution_simps(4) and pwffs.neg_pwff by simp
next
  case (conj_pwff A B)
  then show ?case
    using pwff_substitution_simps(5) and pwffs.conj_pwff by simp
next
  case (disj_pwff A B)
  then show ?case
    using pwff_substitution_simps(6) and pwffs.disj_pwff by simp
next
  case (imp_pwff A B)
  then show ?case
    using pwff_substitution_simps(7) and pwffs.imp_pwff by simp
next
  case (eqv_pwff A B)
  then show ?case
    using pwff_substitution_simps(8) and pwffs.eqv_pwff by simp
qed

lemma pwff_substitution_denotation:
  assumes "A ∈ pwffs" and "B ∈ pwffs"
  and "is_tv_assignment φ"
  shows "𝒱⇩B φ (❙S {(p, o) ↣ A} B) = 𝒱⇩B (φ(p := 𝒱⇩B φ A)) B"
proof -
  from assms(1,3) have "is_tv_assignment (φ(p := 𝒱⇩B φ A))"
    using 𝒱⇩B_graph_denotation_is_truth_value[OF 𝒱⇩B_graph_𝒱⇩B] by simp
  with assms(2,1,3) show ?thesis
    using 𝒱⇩B_simps and pwff_substitution_in_pwffs by induction auto
qed

lemma pwff_substitution_tautology_preservation:
  assumes "is_tautology B" and "A ∈ pwffs"
  and "(p, o) ∈ free_vars B"
  shows "is_tautology (❙S {(p, o) ↣ A} B)"
proof (safe, fold is_tv_assignment_def)
  from assms(1,2) show "❙S {(p, o) ↣ A} B ∈ pwffs"
    using pwff_substitution_in_pwffs by blast
next
  fix φ
  assume "is_tv_assignment φ"
  with assms(1,2) have "𝒱⇩B φ (❙S {(p, o) ↣ A} B) = 𝒱⇩B (φ(p := 𝒱⇩B φ A)) B"
    using pwff_substitution_denotation by blast
  moreover from ‹is_tv_assignment φ› and assms(2) have "is_tv_assignment (φ(p := 𝒱⇩B φ A))"
    using 𝒱⇩B_graph_denotation_is_truth_value[OF 𝒱⇩B_graph_𝒱⇩B] by simp
  with assms(1) have "𝒱⇩B (φ(p := 𝒱⇩B φ A)) B = ❙T"
    by fastforce
  ultimately show "𝒱⇩B φ ❙S {(p, o) ↣ A} B = ❙T"
    by (simp only:)
qed

lemma closed_pwff_substitution_free_vars:
  assumes "A ∈ pwffs" and "B ∈ pwffs"
  and "free_vars A = {}"
  and "(p, o) ∈ free_vars B"
  shows "free_vars (❙S {(p, o) ↣ A} B) = free_vars B - {(p, o)}" (is ‹free_vars (❙S ?θ B) = _›)
using assms(2,4) proof induction
  case (conj_pwff C D)
  have "free_vars (❙S ?θ (C ∧⇧𝒬 D)) = free_vars ((❙S ?θ C) ∧⇧𝒬 (❙S ?θ D))"
    by simp
  also have "… = free_vars (❙S ?θ C) ∪ free_vars (❙S ?θ D)"
    by (fact conj_fv)
  finally have *: "free_vars (❙S ?θ (C ∧⇧𝒬 D)) = free_vars (❙S ?θ C) ∪ free_vars (❙S ?θ D)" .
  from conj_pwff.prems consider
    (a) "(p, o) ∈ free_vars C" and "(p, o) ∈ free_vars D"
  | (b) "(p, o) ∈ free_vars C" and "(p, o) ∉ free_vars D"
  | (c) "(p, o) ∉ free_vars C" and "(p, o) ∈ free_vars D"
    by auto
  from this and * and conj_pwff.IH show ?case
    using free_var_singleton_substitution_neutrality by cases auto
next
  case (disj_pwff C D)
  have "free_vars (❙S ?θ (C ∨⇧𝒬 D)) = free_vars ((❙S ?θ C) ∨⇧𝒬 (❙S ?θ D))"
    by simp
  also have "… = free_vars (❙S ?θ C) ∪ free_vars (❙S ?θ D)"
    by (fact disj_fv)
  finally have *: "free_vars (❙S ?θ (C ∨⇧𝒬 D)) = free_vars (❙S ?θ C) ∪ free_vars (❙S ?θ D)" .
  from disj_pwff.prems consider
    (a) "(p, o) ∈ free_vars C" and "(p, o) ∈ free_vars D"
  | (b) "(p, o) ∈ free_vars C" and "(p, o) ∉ free_vars D"
  | (c) "(p, o) ∉ free_vars C" and "(p, o) ∈ free_vars D"
    by auto
  from this and * and disj_pwff.IH show ?case
    using free_var_singleton_substitution_neutrality by cases auto
next
  case (imp_pwff C D)
  have "free_vars (❙S ?θ (C ⊃⇧𝒬 D)) = free_vars ((❙S ?θ C) ⊃⇧𝒬 (❙S ?θ D))"
    by simp
  also have "… = free_vars (❙S ?θ C) ∪ free_vars (❙S ?θ D)"
    by (fact imp_fv)
  finally have *: "free_vars (❙S ?θ (C ⊃⇧𝒬 D)) = free_vars (❙S ?θ C) ∪ free_vars (❙S ?θ D)" .
  from imp_pwff.prems consider
    (a) "(p, o) ∈ free_vars C" and "(p, o) ∈ free_vars D"
  | (b) "(p, o) ∈ free_vars C" and "(p, o) ∉ free_vars D"
  | (c) "(p, o) ∉ free_vars C" and "(p, o) ∈ free_vars D"
    by auto
  from this and * and imp_pwff.IH show ?case
    using free_var_singleton_substitution_neutrality by cases auto
next
  case (eqv_pwff C D)
  have "free_vars (❙S ?θ (C ≡⇧𝒬 D)) = free_vars ((❙S ?θ C) ≡⇧𝒬 (❙S ?θ D))"
    by simp
  also have "… = free_vars (❙S ?θ C) ∪ free_vars (❙S ?θ D)"
    by (fact eqv_fv)
  finally have *: "free_vars (❙S ?θ (C ≡⇧𝒬 D)) = free_vars (❙S ?θ C) ∪ free_vars (❙S ?θ D)" .
  from eqv_pwff.prems consider
    (a) "(p, o) ∈ free_vars C" and "(p, o) ∈ free_vars D"
  | (b) "(p, o) ∈ free_vars C" and "(p, o) ∉ free_vars D"
  | (c) "(p, o) ∉ free_vars C" and "(p, o) ∈ free_vars D"
    by auto
  from this and * and eqv_pwff.IH show ?case
    using free_var_singleton_substitution_neutrality by cases auto
qed (use assms(3) in ‹force+›)

text ‹Substitution in a pwff:›

definition is_pwff_substitution where
  [iff]: "is_pwff_substitution θ ⟷ is_substitution θ ∧ (∀(x, α) ∈ fmdom' θ. α = o)"

text ‹Tautologous pwff:›

definition is_tautologous :: "form ⇒ bool" where
  [iff]: "is_tautologous B ⟷ (∃θ A. is_tautology A ∧ is_pwff_substitution θ ∧ B = ❙S θ A)"

lemma tautologous_is_wffo:
  assumes "is_tautologous A"
  shows "A ∈ wffs⇘o⇙"
  using assms and substitution_preserves_typing and tautology_is_wffo by blast

lemma implication_reflexivity_is_tautologous:
  assumes "A ∈ wffs⇘o⇙"
  shows "is_tautologous (A ⊃⇧𝒬 A)"
proof -
  let ?θ = "{(𝔵, o) ↣ A}"
  have "is_tautology (𝔵⇘o⇙ ⊃⇧𝒬 𝔵⇘o⇙)"
    by (fact propositional_implication_reflexivity_is_tautology)
  moreover have "is_pwff_substitution ?θ"
    using assms by auto
  moreover have "A ⊃⇧𝒬 A = ❙S ?θ (𝔵⇘o⇙ ⊃⇧𝒬 𝔵⇘o⇙)"
    by simp
  ultimately show ?thesis
    by blast
qed

lemma principle_of_simplification_is_tautologous:
  assumes "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  shows "is_tautologous (A ⊃⇧𝒬 (B ⊃⇧𝒬 A))"
proof -
  let ?θ = "{(𝔵, o) ↣ A, (𝔶, o) ↣ B}"
  have "is_tautology (𝔵⇘o⇙ ⊃⇧𝒬 (𝔶⇘o⇙ ⊃⇧𝒬 𝔵⇘o⇙))"
    by (fact propositional_principle_of_simplification_is_tautology)
  moreover have "is_pwff_substitution ?θ"
    using assms by auto
  moreover have "A ⊃⇧𝒬 (B ⊃⇧𝒬 A) = ❙S ?θ (𝔵⇘o⇙ ⊃⇧𝒬 (𝔶⇘o⇙ ⊃⇧𝒬 𝔵⇘o⇙))"
    by simp
  ultimately show ?thesis
    by blast
qed

lemma pseudo_modus_tollens_is_tautologous:
  assumes "A ∈ wffs⇘o⇙" and "B ∈ wffs⇘o⇙"
  shows "is_tautologous ((A ⊃⇧𝒬 ∼⇧𝒬 B) ⊃⇧𝒬 (B ⊃⇧𝒬 ∼⇧𝒬 A))"
proof -
  let ?θ = "{(𝔵, o) ↣ A, (𝔶, o) ↣ B}"
  have "is_tautology ((𝔵⇘o⇙ ⊃⇧𝒬 ∼⇧𝒬 𝔶⇘o⇙) ⊃⇧𝒬 (𝔶⇘o⇙ ⊃⇧𝒬 ∼⇧𝒬 𝔵⇘o⇙))"
    using 𝒱⇩B_simps by (safe, fold is_tv_assignment_def, simp only:) simp
  moreover have "is_pwff_substitution ?θ"
    using assms by auto
  moreover have "(A ⊃⇧𝒬 ∼⇧𝒬 B) ⊃⇧𝒬 (B ⊃⇧𝒬 ∼⇧𝒬 A) = ❙S ?θ ((𝔵⇘o⇙ ⊃⇧𝒬 ∼⇧𝒬 𝔶⇘o⇙) ⊃⇧𝒬 (𝔶⇘o⇙ ⊃⇧𝒬 ∼⇧𝒬 𝔵⇘o⇙))"
    by simp
  ultimately show ?thesis
    by blast
qed

end