Theory CNF_DNF_Exp_Blowup

theory CNF_DNF_Exp_Blowup
imports
  Main
  Propositional_Proof_Systems.Formulas
  Propositional_Proof_Systems.Sema
  Propositional_Proof_Systems.CNF_Formulas
begin

section ‹Move to \<^session>‹HOL››

(*TODO: Delete when a new Isabelle version is released. *)
lemma card_Domain_le:
  assumes "finite A"
  shows "card (Domain A) ≤ card A"
  using assms by (metis card_image_le fst_eq_Domain)

(*TODO: Delete when a new Isabelle version is released. *)
lemma card_le_card_if_mem_imp_ex_mem:
  fixes f :: "'a ⇒ 'b ⇒ 'c" and 𝒳 :: "'a set" and 𝒴 :: "'c set"
  defines "XY ≡ {(x, y). x ∈ 𝒳 ∧ f x y ∈ 𝒴}"
  assumes "finite 𝒳" and "finite 𝒴" and
    f_inj: "inj_on (λ(x, y). f x y) XY" and
    ex_in_𝒴: "⋀x. x ∈ 𝒳 ⟹ ∃y. f x y ∈ 𝒴"
  shows "card 𝒳 ≤ card 𝒴"
proof -
  have f_XY_subset: "(λ(x, y). f x y) ` XY ⊆ 𝒴"
    using XY_def by auto

  then have "finite ((λ(x, y). f x y) ` XY)"
    using ‹finite 𝒴› by (rule finite_subset)

  then have "finite XY"
    by (rule finite_image_iff[THEN iffD1, OF f_inj])

  moreover have "Domain XY = 𝒳"
    unfolding XY_def
    using ex_in_𝒴
    by (simp add: equalityI subsetI)

  ultimately have "card 𝒳 ≤ card XY"
    using card_Domain_le by iprover

  also have "… ≤ card 𝒴"
    using inj_on_iff_card_le[OF ‹finite XY› ‹finite 𝒴›]
    using f_XY_subset f_inj by blast

  finally show "card 𝒳 ≤ card 𝒴" .
qed


section ‹Move to \<^session>‹Propositional_Proof_Systems››

lemma is_disj_if_is_lit_plus: "is_lit_plus φ ⟹ is_disj φ"
  by (induction φ rule: is_lit_plus.induct) simp_all

lemma disj_is_cnf: "is_disj φ ⟹ is_cnf φ"
  by (induction φ) auto

lemma cnf_in_nnf: "is_cnf φ ⟹ is_nnf φ"
  by (induction φ) (simp_all add: disj_is_nnf is_disj_if_is_lit_plus)


section ‹Functions, Predicates, and Datatypes›


subsection ‹Formula Equivalence›

definition equiv :: "'a formula ⇒ 'a formula ⇒ bool" where
  "equiv φ ψ ⟷ (∀α. (α ⊨ φ) ⟷ (α ⊨ ψ))"

lemma equiv_reflexive: "⋀φ. equiv φ φ"
  unfolding equiv_def by simp

lemma equiv_symmetric[sym]: "⋀φ ψ. equiv φ ψ ⟹ equiv ψ φ"
  unfolding equiv_def by simp

lemma equiv_transitive[trans]: "⋀ξ φ ψ. equiv ξ φ ⟹ equiv φ ψ ⟹ equiv ξ ψ"
  unfolding equiv_def by simp

lemma equiv_Not_left_Not_right[simp]: "⋀φ ψ. equiv (Not φ) (Not ψ) ⟷ equiv φ ψ"
  unfolding equiv_def by simp_all

lemma equiv_Not_Not_left[simp]: "⋀φ ψ. equiv (Not (Not φ)) ψ ⟷ equiv φ ψ"
  unfolding equiv_def by simp_all

lemma equiv_Not_Not_right[simp]: "⋀φ ψ. equiv φ (Not (Not ψ)) ⟷ equiv φ ψ"
  unfolding equiv_def by simp_all


subsection ‹Conjunctive Normal Form›

fun unconj :: "'a formula ⇒ 'a formula list" where
  "unconj (And φ ψ) = unconj φ @ unconj ψ" |
  "unconj φ = [φ]"

lemma unconj_neq_Nil[simp]: "unconj φ ≠ []"
  by (induction φ) simp_all

fun count_And :: "'a formula ⇒ nat" where
  "count_And (And φ ψ) = count_And φ + count_And ψ + 1" |
  "count_And _ = 0"

lemma length_unconj: "length (unconj φ) = count_And φ + 1"
  by (induction φ) simp_all

lemma ball_unconj_is_disj:
  fixes φ :: "'a formula"
  assumes "is_cnf φ"
  shows "⋀C. C ∈ set (unconj φ) ⟹ is_disj C"
  using assms
  by (induction φ rule: is_cnf.induct) auto


subsection ‹Disjunctive Normal Form›

fun is_conj :: "'a formula ⇒ bool" where
  "is_conj (And φ ψ) ⟷ (is_lit_plus φ ∧ is_conj ψ)" |
  "is_conj φ ⟷ is_lit_plus φ"

fun is_dnf :: "'a formula ⇒ bool" where
  "is_dnf (Or φ ψ) ⟷ (is_dnf φ ∧ is_dnf ψ)" |
  "is_dnf φ ⟷ is_conj φ"

lemma conj_is_dnf: "is_conj φ ⟹ is_dnf φ"
  by (induction φ) auto

fun undisj :: "'a formula ⇒ 'a formula list" where
  "undisj (Or φ ψ) = undisj φ @ undisj ψ" |
  "undisj φ = [φ]"

lemma undisj_neq_Nil[simp]: "undisj φ ≠ []"
  by (induction φ) simp_all

lemma ball_undisj_is_conj:
  fixes φ :: "'a formula"
  assumes "is_dnf φ"
  shows "⋀T. T ∈ set (undisj φ) ⟹ is_conj T"
  using assms
  by (induction φ rule: is_dnf.induct) auto

fun count_Or :: "'a formula ⇒ nat" where
  "count_Or (Or φ ψ) = count_Or φ + count_Or ψ + 1" |
  "count_Or _ = 0"

lemma length_undisj: "length (undisj φ) = count_Or φ + 1"
  by (induction φ) simp_all

subsection ‹Big Conjunction›

fun BigAnd' :: "'a formula list ⇒ 'a formula" where
  "BigAnd' [] = (❙¬⊥)" |
  "BigAnd' [F] = F" |
  "BigAnd' (F # Fs) = F ❙∧ BigAnd' Fs"

lemma atoms_BigAnd'[simp]: "atoms (BigAnd' Fs) = ⋃(atoms ` set Fs)"
  by (induction Fs rule: BigAnd'.induct) simp_all

lemma BigAnd'_semantics[simp]: "A ⊨ BigAnd' Ts ⟷ (∀f ∈ set Ts. A ⊨ f)"
  by (induction Ts rule: BigAnd'.induct) simp_all

lemma is_cnf_BigAnd':  "(∀C ∈ set Cs. is_disj C ∧ ¬(∀ α. α ⊨ C)) ⟹ is_cnf (BigAnd' Cs)"
  by (induction Cs rule: BigAnd'.induct) (simp_all add: disj_is_cnf)

lemma equiv_BigAnd'_append: "equiv (BigAnd' (xs @ ys)) (And (BigAnd' xs) (BigAnd' ys))"
  by (induction xs) (simp_all add: equiv_def)


subsection ‹Big Disjunction›

fun BigOr' :: "'a formula list ⇒ 'a formula" where
  "BigOr' Nil = ⊥" |
  "BigOr' [F] = F" |
  "BigOr' (F#Fs) = F ❙∨ BigOr' Fs"

lemma atoms_BigOr'[simp]: "atoms (BigOr' Fs) = ⋃(atoms ` set Fs)"
  by (induction Fs rule: BigOr'.induct) simp_all

lemma BigOr'_semantics[simp]: "A ⊨ BigOr' Ts ⟷ (∃f ∈ set Ts. A ⊨ f)"
  by (induction Ts rule: BigOr'.induct) simp_all

lemma is_dnf_BigOr':  "(∀T ∈ set Ts. is_conj T ∧ (∃ α. α ⊨ T)) ⟹ is_dnf (BigOr' Ts)"
proof (induction Ts)
  case Nil
  then show ?case by simp
next
  case (Cons T Ts)
  then show ?case
    by (metis conj_is_dnf list.set_intros(1) BigOr'.simps(2) BigOr'.simps(3) list.set_intros(2)
        is_dnf.simps(1) neq_Nil_conv)
qed

lemma equiv_BigOr'_append: "equiv (BigOr' (xs @ ys)) (Or (BigOr' xs) (BigOr' ys))"
  by (induction xs) (simp_all add: equiv_def)

lemma equiv_BigOr'_undisj_if_dnf:
  fixes φ :: "'a formula"
  shows "equiv (BigOr' (undisj φ)) φ"
  using equiv_BigOr'_append
  by (induction φ rule: is_dnf.induct) (auto simp add: equiv_def)

lemma equiv_BigAnd'_unconj_if_cnf:
  fixes φ :: "'a formula"
  shows "equiv (BigAnd' (unconj φ)) φ"
proof (induction φ rule: unconj.induct)
  case (1 φ ψ)
  then show ?case
    using equiv_BigAnd'_append
    by (auto simp add: equiv_def)
qed (simp_all add: equiv_def)


subsection ‹Formula Size›

text ‹Similar to @{const size}, but ignores @{term "❙¬"} when calculating the size.›

fun sizef :: "'a formula ⇒ nat" where
  "sizef Bot = 1" |
  "sizef (Atom a) = 1" |
  "sizef (Not φ) = sizef φ" |
  "sizef (And φ ψ) = sizef φ + sizef ψ + 1" |
  "sizef (Or φ ψ) = sizef φ + sizef ψ + 1" |
  "sizef (Imp φ ψ) = sizef φ + sizef ψ + 1"

lemma Suc_0_le_sizef[simp]: "Suc 0 ≤ sizef φ"
  by (induction φ) simp_all

lemma Suc_0_le_size[simp]:
  fixes φ :: "'a formula"
  shows "Suc 0 ≤ size φ"
  by (induction φ) simp_all

lemma sizef_le_size: "sizef φ ≤ size φ"
  by (induction φ) simp_all

lemma card_atoms_le_sizef: "card (atoms φ) ≤ sizef φ"
proof (induction φ)
  case (And F1 F2)
  have "card (atoms (F1 ❙∧ F2)) = card (atoms F1 ∪ atoms F2)"
    by simp
  also have "… ≤ card (atoms F1) + card (atoms F2)"
    using card_Un_le by metis
  also have "… < Suc (card (atoms F1) + card (atoms F2))"
    by presburger
  also have "… ≤ Suc (sizef F1 + sizef F2)"
    using And.IH by presburger
  also have "… = sizef (F1 ❙∧ F2)"
    by simp
  finally show ?case
    by presburger
next
  case (Or F1 F2)
  have "card (atoms (F1 ❙∨ F2)) = card (atoms F1 ∪ atoms F2)"
    by simp
  also have "… ≤ card (atoms F1) + card (atoms F2)"
    using card_Un_le by metis
  also have "… < Suc (card (atoms F1) + card (atoms F2))"
    by presburger
  also have "… ≤ Suc (sizef F1 + sizef F2)"
    using Or.IH by presburger
  also have "… = sizef (F1 ❙∨ F2)"
    by simp
  finally show ?case
    by presburger
next
  case (Imp F1 F2)
  have "card (atoms (F1 ❙→ F2)) = card (atoms F1 ∪ atoms F2)"
    by simp
  also have "… ≤ card (atoms F1) + card (atoms F2)"
    using card_Un_le by metis
  also have "… < Suc (card (atoms F1) + card (atoms F2))"
    by presburger
  also have "… ≤ Suc (sizef F1 + sizef F2)"
    using Imp.IH by presburger
  also have "… = sizef (F1 ❙→ F2)"
    by simp
  finally show ?case
    by presburger
qed simp_all

lemma card_atoms_le_size: "card (atoms φ) ≤ size φ"
  by (metis card_atoms_le_sizef le_trans sizef_le_size)

lemma aux_exp_sizef: "length Ts = n ⟹ ∀ T ∈ set Ts. sizef T ≥ m ⟹ sizef (BigOr' Ts) ≥ n * m"
  by (induction Ts arbitrary: m n rule: BigOr'.induct; fastforce)

lemma aux_exp_size: "length Ts = n ⟹ ∀ T ∈ set Ts. size T ≥ m ⟹ size (BigOr' Ts) ≥ n * m"
  by (induction Ts arbitrary: m n rule: BigOr'.induct; fastforce)

lemma exp_sizef:
  assumes "n > 0" and "length Ts ≥ 2^n" and "∀T ∈ set Ts. sizef T ≥ m"
  shows "sizef (BigOr' Ts) ≥ 2^n * m"
  using assms
proof (induction Ts arbitrary: n m rule: BigOr'.induct)
  case 1
  then show ?case
    by simp
next
  case (2 φ)
  then have False
    by (metis list.size(3) One_nat_def length_Cons leD one_less_power less_2_cases_iff)
  then show ?case ..
next
  case (3 T T' Ts')
  define Ts where
    "Ts = T' # Ts'"
  have "2 ^ n ≤ length Ts ∨ 2 ^ n = Suc (length Ts)"
    unfolding Ts_def using "3.prems" by auto
  then have "2 ^ n * m ≤ Suc (sizef T + sizef (BigOr' Ts))"
  proof (elim disjE)
    assume asm1: "2 ^ n ≤ length Ts"

    have "2 ^ n * m ≤ sizef (BigOr' (T' # Ts'))"
    proof (rule "3.IH")
      show "0 < n"
        by (metis "3.prems"(1))
    next
      show "2 ^ n ≤ length (T' # Ts')"
        using Ts_def asm1 by blast
    next
      show "(∀T∈set (T' # Ts'). m ≤ sizef T)"
        by (simp add: "3.prems"(3) Ts_def)
    qed

    also have "… ≤ Suc (sizef T + sizef (BigOr' Ts))"
      by (simp add: Ts_def)

    finally show ?thesis .
  next
    assume "2 ^ n = Suc (length Ts)"

    then have "2 ^ n = length (T # Ts)"
      by simp

    moreover have "∀ T ∈ set (T # Ts). sizef T ≥ m"
      by (metis "3.prems"(3) Ts_def)

    ultimately show ?thesis
      using aux_exp_sizef by fastforce
  qed
  then show ?case
    by (simp add: Ts_def)
qed

lemma exp_size:
  assumes "n > 0" and "length Ts ≥ 2^n" and "∀T ∈ set Ts. size T ≥ m"
  shows "size (BigOr' Ts) ≥ 2^n * m"
  using assms
proof (induction Ts arbitrary: n m rule: BigOr'.induct)
  case 1
  then show ?case
    by simp
next
  case (2 φ)
  then have False
    by (metis list.size(3) One_nat_def length_Cons leD one_less_power less_2_cases_iff)
  then show ?case ..
next
  case (3 T T' Ts')
  define Ts where
    "Ts = T' # Ts'"
  have "2 ^ n ≤ length Ts ∨ 2 ^ n = Suc (length Ts)"
    unfolding Ts_def using "3.prems" by auto
  then have "2 ^ n * m ≤ Suc (size T + size (BigOr' Ts))"
  proof (elim disjE)
    assume asm1: "2 ^ n ≤ length Ts"

    have "2 ^ n * m ≤ size (BigOr' (T' # Ts'))"
    proof (rule "3.IH")
      show "0 < n"
        by (metis "3.prems"(1))
    next
      show "2 ^ n ≤ length (T' # Ts')"
        using Ts_def asm1 by blast
    next
      show "(∀T∈set (T' # Ts'). m ≤ size T)"
        by (simp add: "3.prems"(3) Ts_def)
    qed

    also have "… ≤ Suc (size T + size (BigOr' Ts))"
      by (simp add: Ts_def)

    finally show ?thesis .
  next
    assume "2 ^ n = Suc (length Ts)"

    then have "2 ^ n = length (T # Ts)"
      by simp

    moreover have "∀ T ∈ set (T # Ts). size T ≥ m"
      by (metis "3.prems"(3) Ts_def)

    ultimately show ?thesis
      using aux_exp_size by fastforce
  qed
  then show ?case
    by (simp add: Ts_def)
qed

lemma sizef_BigOr': "xs ≠ [] ⟹ sizef (BigOr' xs) + 1 = sum_list (map sizef xs) + length xs"
  by (induction xs rule: BigOr'.induct) simp_all

lemma size_BigOr': "xs ≠ [] ⟹ size (BigOr' xs) + 1 = sum_list (map size xs) + length xs"
  by (induction xs rule: BigOr'.induct) simp_all

lemma sizef_BigAnd': "xs ≠ [] ⟹ sizef (BigAnd' xs) + 1 = sum_list (map sizef xs) + length xs"
  by (induction xs rule: BigAnd'.induct) simp_all

lemma size_BigAnd': "xs ≠ [] ⟹ size (BigAnd' xs) + 1 = sum_list (map size xs) + length xs"
  by (induction xs rule: BigAnd'.induct) simp_all

lemma sizef_conv_sum_list_undisj: "sizef φ = sum_list (map sizef (undisj φ)) + count_Or φ"
  by (induction φ) simp_all

lemma size_conv_sum_list_undisj: "size φ = sum_list (map size (undisj φ)) + count_Or φ"
  by (induction φ) simp_all

lemma sizef_conv_sum_list_unconj: "sizef φ = sum_list (map sizef (unconj φ)) + count_And φ"
  by (induction φ) simp_all

lemma size_conv_sum_list_unconj: "size φ = sum_list (map size (unconj φ)) + count_And φ"
  by (induction φ) simp_all

lemma sizef_BigOr'_undisj:
  fixes φ :: "'a formula"
  shows "sizef (BigOr' (undisj φ)) = sizef φ"
proof -
  have "sizef φ + 1 = sum_list (map sizef (undisj φ)) + count_Or φ + 1"
    using sizef_conv_sum_list_undisj[of φ] by presburger

  also have "… = sum_list (map sizef (undisj φ)) + length (undisj φ)"
    using length_undisj[of φ] by presburger

  also have "… = sizef (BigOr' (undisj φ)) + 1"
    using sizef_BigOr'[of "undisj φ", simplified] by presburger

  finally show ?thesis
    by presburger
qed

lemma size_BigOr'_undisj:
  fixes φ :: "'a formula"
  shows "size (BigOr' (undisj φ)) = size φ"
proof -
  have "size φ + 1 = sum_list (map size (undisj φ)) + count_Or φ + 1"
    using size_conv_sum_list_undisj[of φ] by presburger

  also have "… = sum_list (map size (undisj φ)) + length (undisj φ)"
    using length_undisj[of φ] by presburger

  also have "… = size (BigOr' (undisj φ)) + 1"
    using size_BigOr'[of "undisj φ", simplified] by presburger

  finally show ?thesis
    by presburger
qed

lemma sizef_BigAnd'_unconj:
  fixes φ :: "'a formula"
  shows "sizef (BigAnd' (unconj φ)) = sizef φ"
proof -
  have "sizef φ + 1 = sum_list (map sizef (unconj φ)) + count_And φ + 1"
    using sizef_conv_sum_list_unconj[of φ] by presburger

  also have "… = sum_list (map sizef (unconj φ)) + length (unconj φ)"
    using length_unconj[of φ] by presburger

  also have "… = sizef (BigAnd' (unconj φ)) + 1"
    using sizef_BigAnd'[of "unconj φ", simplified] by presburger

  finally show ?thesis
    by presburger
qed

lemma size_BigAnd'_unconj:
  fixes φ :: "'a formula"
  shows "size (BigAnd' (unconj φ)) = size φ"
proof -
  have "size φ + 1 = sum_list (map size (unconj φ)) + count_And φ + 1"
    using size_conv_sum_list_unconj[of φ] by presburger

  also have "… = sum_list (map size (unconj φ)) + length (unconj φ)"
    using length_unconj[of φ] by presburger

  also have "… = size (BigAnd' (unconj φ)) + 1"
    using size_BigAnd'[of "unconj φ", simplified] by presburger

  finally show ?thesis
    by presburger
qed

lemma sizef_BigOr'_filter_le: "sizef (BigOr' (filter P xs)) ≤ sizef (BigOr' xs)"
proof (induction xs rule: BigOr'.induct)
  case 1
  then show ?case
    by simp
next
  case (2 φ)
  then show ?case
    by simp
next
  case (3 F v va)

  have "sizef (BigOr' (filter P (F # v # va))) ≤ sizef (BigOr' (F # filter P (v # va)))"
  proof (cases "P F")
    case True
    then show ?thesis
      by simp
  next
    case False
    then show ?thesis
      by (cases "filter P (v # va)") simp_all
  qed

  also have "… ≤ sizef (BigOr' (F # v # va))"
  proof (cases "filter P (v # va)")
    case Nil
    then show ?thesis
      by simp
  next
    case (Cons G Gs)
    then have "sizef (BigOr' (F # filter P (v # va))) =
      sizef F + sizef (BigOr' (filter P (v # va))) + 1"
      by simp
    also have "… ≤ sizef (BigOr' (F # v # va))"
      using 3 by simp
    finally show ?thesis .
  qed

  finally show ?case .
qed

lemma size_BigOr'_filter_le_if:
  assumes "∃x ∈ set xs. P x"
  shows "size (BigOr' (filter P xs)) ≤ size (BigOr' xs)"
  using assms
proof (induction xs rule: BigOr'.induct)
  case 1
  then show ?case
    by simp
next
  case (2 F)
  then show ?case
    by simp
next
  case (3 F v va)

  then have IH: "size (BigOr' (filter P (v # va))) ≤ size (BigOr' (v # va))"
    by (metis BigOr'.simps(1) One_nat_def empty_filter_conv formula.size(8) formula.size_neq
        leI less_one)

  have "size (BigOr' (filter P (F # v # va))) ≤ size (BigOr' (F # filter P (v # va)))"
  proof (cases "P F")
    case True
    then show ?thesis
      by simp
  next
    case False
    then show ?thesis
      by (cases "filter P (v # va)") simp_all
  qed

  also have "… ≤ size (BigOr' (F # v # va))"
  proof (cases "filter P (v # va)")
    case Nil
    then show ?thesis
      by simp
  next
    case (Cons G Gs)
    then have "size (BigOr' (F # filter P (v # va))) =
      size F + size (BigOr' (filter P (v # va))) + 1"
      by simp
    also have "… ≤ size (BigOr' (F # v # va))"
      using IH by auto
    finally show ?thesis .
  qed

  finally show ?case .
qed

lemma sizef_BigAnd'_filter_le: "sizef (BigAnd' (filter P xs)) ≤ sizef (BigAnd' xs)"
proof (induction xs rule: BigAnd'.induct)
  case 1
  then show ?case
    by simp
next
  case (2 F)
  then show ?case
    by simp
next
  case (3 F v va)
  then show ?case
    by (metis BigAnd'.simps(1) BigOr'.simps(1) add_diff_cancel_right diff_is_0_eq sizef.simps(3)
        sizef_BigAnd' sizef_BigOr' sizef_BigOr'_filter_le)
qed


subsection ‹Fn function›

datatype var = Var nat bool

lemma inj_on_Var[simp]: "inj_on (λ(x, y). Var x y) A" for A
  by (rule inj_onI) (simp add: case_prod_beta prod_eq_iff)

fun Fn :: "nat ⇒ var formula" where
  "Fn 0 = (❙¬⊥)"|
  "Fn (Suc n) =
    And
      (And
        (Or
          (Atom (Var (Suc n) False))
          (Atom (Var (Suc n) True)))
        (Or
          (Not (Atom (Var (Suc n) False)))
          (Not (Atom (Var (Suc n) True)))))
    (Fn n)"

lemma sizef_Fn: "sizef (Fn n) = 8 * n + 1"
  by (induction n) auto

lemma size_Fn: "size (Fn n) = 10 * n + 2"
  by (induction n) auto

lemma is_cnf_Fn: "is_cnf (Fn n)"
  by (induction n; auto)

lemma is_nnf_Fn: "is_nnf (Fn n)"
  using is_cnf_Fn[THEN cnf_in_nnf] .

lemma Fn_sat: "∃α. α ⊨ Fn n"
proof -
  define α where "α = (λx. case x of (Var i b) ⇒ b)"
  then have "α ⊨ Fn n"
    by (induction n; simp)
  then show ?thesis
    by auto
qed

lemma semantics_Fn_iff: "α ⊨ Fn n ⟷ (∀i ∈ {1..n}. α (Var i False) ≠ α (Var i True))"
proof (induction n)
  case 0
  show ?case
    by simp
next
  case (Suc n)

  let ?F = "
    And
      (Or
        (Atom (Var (Suc n) False))
        (Atom (Var (Suc n) True)))
      (Or
        (Not (Atom (Var (Suc n) False)))
        (Not (Atom (Var (Suc n) True))))"

  have "α ⊨ Fn (Suc n) ⟷ α ⊨ And ?F (Fn n)"
    by simp
  also have "… ⟷ α ⊨ ?F ∧ α ⊨ (Fn n)"
    by simp
  also have "… ⟷ (α (Var (Suc n) False) ≠ α (Var (Suc n) True)) ∧ α ⊨ (Fn n)"
    by force
  also have "… ⟷ (α (Var (Suc n) False) ≠ α (Var (Suc n) True)) ∧
    (∀i∈{1..n}. α (Var i False) ≠ α (Var i True))"
    unfolding Suc.IH ..
  also have "… ⟷ (∀i∈insert (Suc n) {1..n}. α (Var i False) ≠ α (Var i True))"
    by simp
  also have "… ⟷ (∀i∈{1..Suc n}. α (Var i False) ≠ α (Var i True))"
    by (simp add: atLeastAtMostSuc_conv)
  finally show ?case .
qed


subsection ‹Dual Function›

primrec dual :: "'a formula ⇒ 'a formula" where
  "dual Bot = Not Bot" |
  "dual (Atom v) = Not (Atom v)" |
  "dual (Not v) = v" |
  "dual (And φ ψ) = Or (dual φ) (dual ψ)" |
  "dual (Or φ ψ) = And (dual φ) (dual ψ)" |
  "dual (Imp φ ψ) = And φ (dual ψ)"

lemma sizef_dual_Fn: "sizef (dual (Fn n)) = 8 * n + 1"
  by (induction n) simp_all

lemma size_dual_Fn: "size (dual (Fn n)) = 10 * n + 1"
  by (induction n) simp_all

lemma is_dnf_dual_Fn: "is_dnf (dual (Fn n))"
  by (induction n) simp_all

lemma sizef_dual: "sizef (dual φ) = sizef φ"
  by (induction φ) simp_all

lemma size_dual_le: "size (dual φ) ≤ 2 * size φ"
  by (induction φ) simp_all

lemma equiv_dual: "equiv (dual φ) (Not φ)"
  by (induction φ) (simp_all add: equiv_def)

lemma is_disj_dual_if_is_conj: "is_conj φ ⟹ is_disj (dual φ)"
proof (induction φ)
  case (Not φ)
  then show ?case
    by (metis is_conj.simps(4) is_disj.simps(2,3) is_lit_plus.simps(1,3)
        is_nnf.simps(6) is_nnf_NotD dual.simps(3))
next
  case (And F1 F2)
  then show ?case
    unfolding dual.simps is_conj.simps is_disj.simps
    by (metis dual.simps(1,2,3) is_lit_plus.elims(2) is_lit_plus.simps(1,2,3,4))
qed simp_all

lemma is_conj_dual_if_is_disj: "is_disj φ ⟹ is_conj (dual φ)"
proof (induction φ)
  case (Not φ)
  then show ?case
    using is_nnf_NotD by force
next
  case (Or F1 F2)
  then show ?case
    unfolding dual.simps is_conj.simps is_disj.simps
    by (metis dual.simps(1,2,3) is_lit_plus.elims(2) is_lit_plus.simps(1,2,3,4))
qed simp_all

lemma is_dnf_dual_if_is_cnf: "is_cnf φ ⟹ is_dnf (dual φ)"
proof (induction φ)
  case (Not φ)
  then show ?case
    using conj_is_dnf is_cnf.simps(4) is_conj_dual_if_is_disj by blast
next
  case (Or F1 F2)
  then show ?case
    using conj_is_dnf is_cnf.simps(5) is_conj_dual_if_is_disj by blast
qed simp_all

lemma is_cnf_dual_if_is_dnf: "is_dnf φ ⟹ is_cnf (dual φ)"
proof (induction φ)
  case (Not φ)
  then show ?case
    using disj_is_cnf is_disj_dual_if_is_conj is_dnf.simps(4) by blast
next
  case (And F1 F2)
  then show ?case
    using disj_is_cnf is_disj_dual_if_is_conj is_dnf.simps(5) by blast
qed auto

lemma dual_disj_not_taut_impl_sat: "is_disj φ ⟹ ∃α. ¬ α ⊨ φ ⟹ ∃α. α ⊨ dual φ"
proof (induction φ)
  case (Or F1 F2)
  have F_is_nnf: "is_nnf (F1 ❙∨ F2)"
    using Or.prems(1) disj_is_nnf by blast
  then have equiv: "equiv (Not (F1 ❙∨ F2))(dual (F1 ❙∨ F2))"
    using equiv_dual equiv_def by blast
  obtain α where α_def: "¬ α ⊨ F1 ❙∨ F2"
    using Or.prems(2) by auto
  then have "α ⊨ Not (F1 ❙∨ F2)"
    by auto
  then have "α ⊨ dual (F1 ❙∨ F2)"
    using equiv by (simp add: equiv_def)
  then show ?case
    by auto
qed auto

lemma dual_conj_of_disjs_is_disj_of_conjs:
  fixes Cs
  assumes "∀ C ∈ set Cs. is_disj C ∧ (∃ α. ¬(α ⊨ C))"
  defines "Ts ≡ map dual Cs"
  shows "dual (BigAnd' Cs) = BigOr' Ts" "∀T∈set Ts. is_conj T ∧ (∃ α. α ⊨ T)"
  unfolding atomize_conj Ts_def
  using assms(1)
proof (induction Cs)
  case Nil
  then show ?case
    by simp
next
  case (Cons C Cs)

  then have IH:
      "dual (BigAnd' Cs) = BigOr' (map dual Cs)"
      "(∀T∈set (map dual Cs). is_conj T ∧ (∃α. α ⊨ T))"
    by (auto simp add: Cons.IH Cons.prems)

  show ?case
  proof (intro conjI ballI)
    show "dual (BigAnd' (C # Cs)) = BigOr' (map dual (C # Cs))"
      by (cases Cs) (use IH(1) in simp_all)
  next
    have "is_disj C"
      using Cons.prems by simp
    then have "is_conj (dual C)"
      by (rule is_conj_dual_if_is_disj)
    then show "⋀T. T ∈ set (map dual (C # Cs)) ⟹ is_conj T"
      using IH(2) by auto
  next
    have "∃α. ¬ α ⊨ C"
      using Cons.prems by simp
    then have "∃α. α ⊨ dual C"
      using equiv_dual[of C, unfolded equiv_def] by simp
    then show "⋀T. T ∈ set (map dual (C # Cs)) ⟹ ∃α. α ⊨ T"
      using IH(2) by auto
  qed
qed


subsection ‹Formula Contains Atom›

text ‹Should only be applied to a formula for which @{const is_nnf} holds.›

fun cont_pos :: "'a formula ⇒ 'a ⇒ bool" where
  "cont_pos Bot l = False" |
  "cont_pos (Atom v) l = (v = l)" |
  "cont_pos (Not (Atom v)) l = False" |
  "cont_pos (Not φ) l = False" |
  "cont_pos (And φ ψ) l = (cont_pos φ l ∨ cont_pos ψ l)" |
  "cont_pos (Or φ ψ) l = (cont_pos φ l ∨ cont_pos ψ l)" |
  "cont_pos (Imp φ ψ) l = False"

text ‹Should only be applied to a formula for which @{const is_nnf} holds.›

fun cont_neg :: "'a formula ⇒ 'a ⇒ bool" where
  "cont_neg Bot l = False" |
  "cont_neg (Atom v) l = False" |
  "cont_neg (Not (Atom v)) l = (v = l)" |
  "cont_neg (Not φ) l = False" |
  "cont_neg (And φ ψ) l = (cont_neg φ l ∨ cont_neg ψ l)" |
  "cont_neg (Or φ ψ) l = (cont_neg φ l ∨ cont_neg ψ l)" |
  "cont_neg (Imp φ ψ) l = False"

text ‹Should only be applied to a formula for which @{const is_nnf} holds.›

fun cont :: "'a formula ⇒ 'a ⇒ bool" where
  "cont Bot l = False" |
  "cont (Atom v) l = (v = l)" |
  "cont (Not (Atom v)) l = (v = l)" |
  "cont (Not φ) l = False" |
  "cont (And φ ψ) l = (cont φ l ∨ cont ψ l)" |
  "cont (Or φ ψ) l = (cont φ l ∨ cont ψ l)" |
  "cont (Imp φ ψ) l = False"

lemma impl_not_cont_pos: "¬ cont_pos φ v ⟹ cont_neg φ v ∨ ¬ (cont φ v)"
  by (induction φ) (auto elim: cont.elims)

lemma impl_not_cont: "¬ cont φ v ⟹ ¬ cont_pos φ v ∧ ¬ cont_neg φ v"
  by (induction φ) (auto elim: cont.elims)

lemma mem_atoms_if_cont_pos:
  assumes "cont_pos T v"
  shows "v ∈ atoms T"
  using assms by (induction T v rule: cont_pos.induct) auto

lemma
  assumes "is_conj φ"
  shows
    not_sat_conj_neg_true: "∃v. cont_neg φ v ∧ α v ⟹ ¬(α ⊨ φ)" and
    not_sat_conj_pos_false: "∃v. cont_pos φ v ∧ ¬(α v) ⟹ ¬(α ⊨ φ)"
  using assms
  by (induction φ) (auto elim: cont_pos.elims is_lit_plus.elims)

lemma sat_conj_val_cont_ident:
  assumes "Val1 ⊨ φ" and "∀ v ∈ {v. cont φ v}. Val1 v = Val2 v" and "is_conj φ"
  shows "Val2 ⊨ φ"
  using assms
  by (induction φ) (auto elim: cont_neg.elims is_lit_plus.elims)


section ‹CNF to DNF›

proposition exp_blowup_from_Fn_to_BigOr':
  fixes n :: nat and Ts :: "var formula list"
  defines "φ ≡ Fn n" and "ψ ≡ BigOr' Ts"
  assumes
    n_greater_0: "n > 0" and
    Ts_spec: "(∀T∈set Ts. is_conj T ∧ (∃α. α ⊨ T))" and
    "equiv φ ψ"
  shows "sizef ψ ≥ n*2^n"
proof -
  have occ_var_bool_diff: "cont_pos T (Var i False) ≠ cont_pos T (Var i True)"
    if "T ∈ set Ts" and "i ∈ {1..n}"
    for T :: "var formula" and i :: nat
  proof (rule notI)
    assume "cont_pos T (Var i False) = cont_pos T (Var i True)"

    then consider
      (both_absent) "¬(cont_pos T (Var i False))" "¬(cont_pos T (Var i True))" |
      (both_present) "cont_pos T (Var i False)" "cont_pos T (Var i True)"
      by satx

    then show False
    proof cases
      case both_absent
      then have "∃ α. α ⊨ T"
        by (simp add: ‹T ∈ set Ts› Ts_spec)
      then obtain ValsatT where Valsat: "ValsatT ⊨ T"
        by auto

      define α where
        "α = (λ v. (if v = Var i False ∨ v = Var i True then False else ValsatT v))"

      have "∀ v ∈ {v. cont_pos T v}. ValsatT v = α v"
        by (simp add: α_def both_absent)
      then have "α ⊨ T"
        using not_sat_conj_neg_true impl_not_cont_pos sat_conj_val_cont_ident
        by (metis ‹T ∈ set Ts› α_def Ts_spec mem_Collect_eq Valsat)
      then have "∃ α. α ⊨ T ∧ α (Var i False) = False ∧ α (Var i True) = False"
        unfolding α_def by auto
      then have "∃ α. α ⊨ ψ ∧ ¬(α ⊨ φ)"
        unfolding ψ_def φ_def
        using BigOr'_semantics ‹T ∈ set Ts› ‹i ∈ {1..n}› semantics_Fn_iff by metis
      then have "¬ equiv φ ψ"
        unfolding equiv_def by auto
      then show False
        using ‹equiv φ ψ› by contradiction
    next
      case both_present
      then have "∃ α. α ⊨ T"
        by (simp add: ‹T ∈ set Ts› Ts_spec)
      then have "∃ α. α ⊨ T ∧ α (Var i False) = True ∧ α (Var i True) = True"
        using ‹T ∈ set Ts› both_present not_sat_conj_pos_false Ts_spec by blast
      then have "∃ α. α ⊨ ψ ∧ ¬(α ⊨ φ)"
        unfolding ψ_def φ_def
        using BigOr'_semantics ‹T ∈ set Ts› ‹i ∈ {1..n}› semantics_Fn_iff by metis
      then have "¬ equiv φ ψ"
        unfolding equiv_def by auto
      then show False
        using ‹equiv φ ψ› by contradiction
    qed
  qed

  have ex_T_cont_pos_var_eps: "∃T ∈ set Ts. ∀i ∈ {1..n}. cont_pos T (Var i (nth eps (i-1)))"
    if "length eps = n" for eps :: "bool list"
  proof (rule ccontr)
    assume assm: "¬ (∃T ∈ set Ts. ∀i ∈ {1..n}. cont_pos T (Var i (nth eps (i-1))))"

    define α where
      "α = (λx. case x of (Var i b) ⇒ b = nth eps (i-1))"

    have "α ⊨ φ"
    proof -
      have "α ⊨ Fn n"
        using α_def by (induction n) simp_all
      then show ?thesis
        by (simp add: φ_def)
    qed

    moreover have "¬(α ⊨ ψ)"
    proof -
      have "∀T ∈ set Ts. ∃ i ∈ {1..n}. cont_pos T (Var i (¬(nth eps (i-1))))"
        using assm occ_var_bool_diff by (metis (full_types))
      then have "∀ T ∈ set Ts. ¬(α ⊨ T)"
        by (metis (mono_tags, lifting) Ts_spec α_def not_sat_conj_pos_false var.case)
      then show ?thesis
        unfolding ψ_def by auto
    qed

    ultimately have "¬ equiv φ ψ"
      by (auto simp add: equiv_def)

    then show False
      using ‹equiv φ ψ› by contradiction
  qed

  have n_le_card_atoms: "n ≤ card (atoms T)" if T_in: "T ∈ set Ts" for T
    using card_le_card_if_mem_imp_ex_mem[of "{1..n}" "atoms T" Var, simplified]
    using occ_var_bool_diff[rule_format, OF T_in]
    by (metis One_nat_def atLeastAtMost_iff mem_atoms_if_cont_pos)

  define conj_of_eps :: "bool list ⇒ var formula" where
    "conj_of_eps = (λeps.
      (SOME T. T ∈ set Ts ∧ (∀i ∈ {1..(length eps)}. cont_pos T (Var i (nth eps (i - 1))))))"

  have T_of_conj_of_eps_in_Ts: "conj_of_eps eps ∈ set Ts" if "length eps = n" for eps
    unfolding conj_of_eps_def
    by (smt (verit, best) ex_T_cont_pos_var_eps that verit_sko_ex')

  have "2^n = card {eps :: bool list. length eps = n}"
    using card_lists_length_eq[of "UNIV :: bool set" n, simplified, symmetric] .

  also have "… ≤ card (set Ts)"
  proof (rule card_inj_on_le[of conj_of_eps])
    show "inj_on conj_of_eps {eps. length eps = n}"
    proof (rule inj_onI)
      fix xs ys :: "bool list"
      assume
        xs_in: "xs ∈ {eps. length eps = n}" and
        ys_in: "ys ∈ {eps. length eps = n}"

      have "length xs = n"
        using xs_in by simp

      moreover have "length ys = n"
        using ys_in by simp

      ultimately have "length xs = length ys"
        by simp

      show "conj_of_eps xs = conj_of_eps ys ⟹ xs = ys"
      proof (erule contrapos_pp)
        assume "xs ≠ ys"
        then obtain i where "i < n" and "nth xs i ≠ nth ys i"
          using ‹length xs = length ys›
          using ‹length xs = n› nth_equalityI by blast

        have "cont_pos (conj_of_eps xs) (Var (Suc i) (xs ! i))"
        proof -
          have "conj_of_eps xs ∈ set Ts ∧
                (∀i∈{1..n}. cont_pos (conj_of_eps xs) (Var i (xs ! (i - 1))))"
            by (smt (verit, ccfv_SIG) ‹length xs = n› conj_of_eps_def
                ex_T_cont_pos_var_eps someI_ex)
          then show ?thesis
            using ‹i < n› by force
        qed

        moreover have "cont_pos (conj_of_eps ys) (Var (Suc i) (ys ! i))"
        proof -
          have "conj_of_eps ys ∈ set Ts ∧
                (∀i∈{1..n}. cont_pos (conj_of_eps ys) (Var i (ys ! (i - 1))))"
            by (smt (verit, ccfv_SIG) ‹length ys = n› conj_of_eps_def
                ex_T_cont_pos_var_eps someI_ex)
          then show ?thesis
            using ‹i < n› by force
        qed

        moreover have "
          cont_pos (conj_of_eps ys) (Var (Suc i) False) ≠
          cont_pos (conj_of_eps ys) (Var (Suc i) True)"
          using ‹i < n› occ_var_bool_diff[OF T_of_conj_of_eps_in_Ts[OF ‹length ys = n›], of "Suc i"]
          by simp

        ultimately show "conj_of_eps xs ≠ conj_of_eps ys"
          using ‹xs ! i ≠ ys ! i›
          by (metis (mono_tags))
      qed
    qed
  next
    show "conj_of_eps ` {eps. length eps = n} ⊆ set Ts"
      using T_of_conj_of_eps_in_Ts by auto
  next
    show "finite (set Ts)"
      by simp
  qed

  also have "… ≤ length Ts"
    using card_length[of Ts] .

  finally have "length Ts ≥ 2^n" .

  moreover have "∀T ∈ set Ts. sizef T ≥ n"
    using n_le_card_atoms card_atoms_le_sizef
    using le_trans by blast

  ultimately show ?thesis
    unfolding ψ_def
    using exp_sizef[OF n_greater_0]
    by (metis mult.commute)
qed

lemma ex_equiv_disj_list_if_is_dnf:
  fixes φ :: "'a formula"
  assumes dnf: "is_dnf φ" and sat: "∃α. α ⊨ φ"
  shows "∃(Ts :: 'a formula list). equiv φ (BigOr' Ts) ∧
    size (BigOr' Ts) ≤ size φ ∧
    (∀T ∈ set Ts. is_conj T) ∧
    (∀T ∈ set Ts. ∃α. α ⊨ T)"
proof -
  have bex_sat: "∃T ∈ set (undisj φ). ∃α. α ⊨ T"
    using sat
    by (metis equiv_def BigOr'_semantics equiv_BigOr'_undisj_if_dnf)

  define Ts :: "'a formula list" where
    "Ts = filter (λT. ∃α. α ⊨ T) (undisj φ)"

  show ?thesis
  proof (intro exI[of _ Ts] conjI ballI)
    have "equiv φ (BigOr' (undisj φ))"
      using equiv_BigOr'_undisj_if_dnf[symmetric] .
    then show "equiv φ (BigOr' Ts)"
      unfolding Ts_def
      by (auto simp add: equiv_def)
  next
    have "size (BigOr' (undisj φ)) = size φ"
      using size_BigOr'_undisj .
    then show "size (BigOr' Ts) ≤ size φ"
      unfolding Ts_def
      using size_BigOr'_filter_le_if[OF bex_sat]
      by presburger
  next
    show "⋀T. T ∈ set Ts ⟹ is_conj T"
      using ball_undisj_is_conj[OF dnf]
      by (simp add: Ts_def)
  next
    show "⋀T. T ∈ set Ts ⟹ ∃α. α ⊨ T"
      by (simp add: Ts_def)
  qed
qed

theorem exp_blowup_from_CNF_to_DNF:
  fixes n :: nat
  shows "∃(φ :: var formula).
    is_cnf φ ∧
    size φ = 10 * n + 2 ∧
    (∀(ψ :: var formula). equiv φ ψ ⟶ is_dnf ψ ⟶ size ψ ≥ n * 2 ^ n)"
proof (cases n)
  case 0
  then show ?thesis
    using is_cnf_Fn size_Fn by fastforce
next
  case (Suc n')

  then have "0 < n"
    by presburger

  show ?thesis
  proof (intro exI conjI allI impI)
    show "is_cnf (Fn n)"
      using is_cnf_Fn .
  next
    show "size (Fn n) = 10 * n + 2"
      using size_Fn .
  next
    fix ψ :: "var formula"
    assume "equiv (Fn n) ψ"
    then have sat_G⇩n: "∃α. α ⊨ ψ"
      unfolding equiv_def
      using Fn_sat[of n] by metis

    assume "is_dnf ψ"
    then obtain Ts :: "var formula list" where
      "∀T ∈ set Ts. is_conj T" and
      "∀T ∈ set Ts. ∃α. α ⊨ T" and
      "equiv ψ (BigOr' Ts)" and
      size: "size (BigOr' Ts) ≤ size ψ"
      using ex_equiv_disj_list_if_is_dnf[OF _ sat_G⇩n] by metis

    moreover have "equiv (Fn n) (BigOr' Ts)"
      using equiv_transitive[OF ‹equiv (Fn n) ψ› ‹equiv ψ (BigOr' Ts)›] .

    ultimately have "n * 2 ^ n ≤ sizef (BigOr' Ts)"
      using exp_blowup_from_Fn_to_BigOr'[OF ‹0 < n›, of Ts] by metis

    then show "n * 2 ^ n ≤ size ψ"
      using size sizef_le_size[of "BigOr' Ts"] by presburger
  qed
qed


section ‹DNF to CNF›

proposition exp_blowup_from_dual_Fn_to_BigAnd':
  fixes n :: nat and Cs :: "var formula list"
  defines "φ ≡ dual (Fn n)" and "ψ ≡ BigAnd' Cs"
  assumes
    n_greater_0: "n > 0" and
    Cs_spec: "(∀ C ∈ set Cs. is_disj C ∧ ¬(∀ α. α ⊨ C))" and
    "equiv φ ψ"
  shows "sizef ψ ≥ n*2^n"
proof -
  have G_in_cnf: "is_cnf ψ"
    using ψ_def Cs_spec is_cnf_BigAnd' by auto
  have G_in_nnf: "is_nnf ψ"
    using G_in_cnf cnf_in_nnf by auto

  show ?thesis
  proof (rule ccontr)
    assume "¬ n*2^n ≤ sizef ψ"
    then have "sizef ψ < n*2^n"
      by presburger
    then have "sizef (dual ψ) < n*2^n"
      using sizef_dual[of ψ] by presburger

    obtain Ts where
      "dual ψ = BigOr' Ts" "∀T∈set Ts. is_conj T ∧ (∃ α. α ⊨ T)"
      using ψ_def Cs_spec dual_conj_of_disjs_is_disj_of_conjs by metis

    moreover have "equiv (Fn n) (dual ψ)"
    proof -
      have "equiv (dual ψ) (Not ψ)"
        using equiv_dual .
      also have "equiv … (Not (dual (Fn n)))"
        unfolding equiv_Not_left_Not_right
        using ‹equiv φ ψ›[symmetric, unfolded φ_def] .
      also have "equiv … (Not (Not (Fn n)))"
        unfolding equiv_Not_left_Not_right
        using equiv_dual .
      also have "equiv … (Fn n)"
        unfolding equiv_Not_Not_left
        using equiv_reflexive .
      finally show ?thesis
        by (rule equiv_symmetric)
    qed

    ultimately have "n * 2 ^ n ≤ sizef (dual ψ)"
      using exp_blowup_from_Fn_to_BigOr'[of n Ts] by force
    then show False
      using ‹sizef (dual ψ) < n*2^n› by presburger
  qed
qed

lemma ex_equiv_conj_list_if_is_cnf:
  fixes φ :: "'a formula"
  assumes cnf: "is_cnf φ"
  shows "∃(Cs :: 'a formula list). equiv φ (BigAnd' Cs) ∧
    sizef (BigAnd' Cs) ≤ sizef φ ∧
    (∀C ∈ set Cs. is_disj C) ∧
    (∀C ∈ set Cs. ¬ ⊨ C)"
proof -
  define Cs :: "'a formula list" where
    "Cs = filter (λC. ¬ ⊨ C) (unconj φ)"

  show ?thesis
  proof (intro exI[of _ Cs] conjI ballI)
    have "equiv φ (BigAnd' (unconj φ))"
      using equiv_BigAnd'_unconj_if_cnf[symmetric] .
    then show "equiv φ (BigAnd' Cs)"
      unfolding Cs_def
      by (auto simp add: equiv_def)
  next
    have "sizef (BigAnd' (unconj φ)) = sizef φ"
      using sizef_BigAnd'_unconj .
    then show "sizef (BigAnd' Cs) ≤ sizef φ"
      unfolding Cs_def
      using sizef_BigAnd'_filter_le[of "λC. ¬ ⊨ C" "unconj φ"]
      by presburger
  next
    show "⋀C. C ∈ set Cs ⟹ is_disj C"
      using ball_unconj_is_disj[OF cnf]
      by (simp add: Cs_def)
  next
    show "⋀C. C ∈ set Cs ⟹ ¬ ⊨ C"
      by (simp add: Cs_def)
  qed
qed

theorem exp_blowup_from_DNF_to_CNF:
  fixes n :: nat
  shows "∃(φ :: var formula).
    is_dnf φ ∧
    size φ = 10 * n + 1 ∧
    (∀(ψ :: var formula). equiv φ ψ ⟶ is_cnf ψ ⟶ size ψ ≥ n * 2 ^ n)"
proof (cases n)
  case 0
  then show ?thesis
    using is_dnf_dual_Fn size_dual_Fn
    by fastforce
next
  case (Suc n')

  then have "n > 0"
    by presburger

  show ?thesis
  proof (intro exI conjI allI impI)
    show "is_dnf (dual (Fn n))"
      using is_dnf_dual_Fn .
  next
    show "size (dual (Fn n)) = 10 * n + 1"
      using size_dual_Fn .
  next
    fix ψ :: "var formula"
    assume "equiv (dual (Fn n)) ψ"
    assume "is_cnf ψ"

    then obtain Cs :: "var formula list" where
      "∀C ∈ set Cs. is_disj C" and
      "∀C ∈ set Cs. ¬ ⊨ C" and
      "equiv ψ (BigAnd' Cs)" and
      sizef: "sizef (BigAnd' Cs) ≤ sizef ψ"
      using ex_equiv_conj_list_if_is_cnf[of ψ] by metis

    moreover have "equiv (dual (Fn n)) (BigAnd' Cs)"
      using equiv_transitive[OF ‹equiv (dual (Fn n)) ψ› ‹equiv ψ (BigAnd' Cs)›] .

    ultimately have "n * 2 ^ n ≤ sizef (BigAnd' Cs)"
      using exp_blowup_from_dual_Fn_to_BigAnd'[OF ‹0 < n›, of Cs] by metis

    then show "n * 2 ^ n ≤ size ψ"
      using sizef sizef_le_size[of ψ] by presburger
  qed
qed

end