Theory Prop_Normalisation

theory Prop_Normalisation
imports Entailment_Definition.Prop_Logic Prop_Abstract_Transformation Nested_Multisets_Ordinals.Multiset_More
begin

text ‹Given the previous definition about abstract rewriting and theorem about them, we now have the
  detailed rule making the transformation into CNF/DNF.›

section ‹Rewrite Rules›
text ‹The idea of Christoph Weidenbach's book is to remove gradually the operators: first
  equivalencies, then implication, after that the unused true/false and finally the reorganizing the
  or/and.  We will prove each transformation seperately.›


subsection ‹Elimination of the Equivalences›

text ‹The first transformation consists in removing every equivalence symbol.›
inductive elim_equiv :: "'v propo ⇒ 'v propo ⇒ bool" where
elim_equiv[simp]: "elim_equiv (FEq φ ψ) (FAnd (FImp φ ψ)  (FImp ψ φ))"

lemma elim_equiv_transformation_consistent:
"A ⊨ FEq φ ψ ⟷ A ⊨ FAnd (FImp φ ψ) (FImp ψ φ)"
  by auto

lemma elim_equiv_explicit: "elim_equiv φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ"
  by (induct rule: elim_equiv.induct, auto)

lemma elim_equiv_consistent: "preserve_models elim_equiv"
  unfolding preserve_models_def by (simp add: elim_equiv_explicit)

lemma elimEquv_lifted_consistant:
  "preserve_models (full (propo_rew_step elim_equiv))"
  by (simp add: elim_equiv_consistent)


text ‹This function ensures that there is no equivalencies left in the formula tested by
  @{term no_equiv_symb}.›
fun no_equiv_symb :: "'v propo ⇒ bool" where
"no_equiv_symb (FEq _ _) = False" |
"no_equiv_symb _ = True"


text ‹Given the definition of @{term no_equiv_symb}, it does not depend on the formula, but only on
  the connective used.›
lemma no_equiv_symb_conn_characterization[simp]:
  fixes c :: "'v connective" and l :: "'v propo list"
  assumes wf: "wf_conn c l"
  shows "no_equiv_symb (conn c l) ⟷ c ≠ CEq"
    by (metis connective.distinct(13,25,35,43) wf no_equiv_symb.elims(3) no_equiv_symb.simps(1)
      wf_conn.cases wf_conn_list(6))

definition no_equiv where "no_equiv = all_subformula_st no_equiv_symb"

lemma no_equiv_eq[simp]:
  fixes φ ψ :: "'v propo"
  shows
    "¬no_equiv (FEq φ ψ)"
    "no_equiv FT"
    "no_equiv FF"
  using no_equiv_symb.simps(1) all_subformula_st_test_symb_true_phi unfolding no_equiv_def by auto

text ‹The following lemma helps to reconstruct @{term no_equiv} expressions: this representation is
  easier to use than the set definition.›


lemma all_subformula_st_decomp_explicit_no_equiv[iff]:
fixes φ ψ :: "'v propo"
shows
  "no_equiv (FNot φ) ⟷ no_equiv φ"
  "no_equiv (FAnd φ ψ) ⟷ (no_equiv φ ∧ no_equiv ψ)"
  "no_equiv (FOr φ ψ) ⟷ (no_equiv φ ∧ no_equiv ψ)"
  "no_equiv (FImp φ ψ) ⟷ (no_equiv φ ∧ no_equiv ψ)"
  by (auto simp: no_equiv_def)

text ‹A theorem to show the link between the rewrite relation @{term elim_equiv} and the function
  @{term no_equiv_symb}. This theorem is one of the assumption we need to characterize the
  transformation.›
lemma no_equiv_elim_equiv_step:
  fixes φ :: "'v propo"
  assumes no_equiv: "¬ no_equiv φ"
  shows "∃ψ ψ'. ψ ≼ φ ∧ elim_equiv ψ ψ'"
proof -
  have test_symb_false_nullary:
    "∀x::'v. no_equiv_symb FF ∧ no_equiv_symb FT ∧ no_equiv_symb (FVar x)"
    unfolding no_equiv_def by auto
  moreover {
    fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
      assume a1: "elim_equiv (conn c l) ψ"
      have "⋀p pa. ¬ elim_equiv (p::'v propo) pa ∨ ¬ no_equiv_symb p"
        using elim_equiv.cases no_equiv_symb.simps(1) by blast
      then have "elim_equiv (conn c l) ψ ⟹ ¬no_equiv_symb (conn c l) " using a1 by metis
  }
  moreover have H': "∀ψ. ¬elim_equiv FT ψ" "∀ψ. ¬elim_equiv FF ψ" "∀ψ x. ¬elim_equiv (FVar x) ψ"
    using elim_equiv.cases by auto
  moreover have "⋀φ. ¬ no_equiv_symb φ ⟹ ∃ψ. elim_equiv φ ψ"
    by (case_tac φ, auto simp: elim_equiv.simps)
  then have "⋀φ'. φ' ≼ φ ⟹ ¬no_equiv_symb φ' ⟹  ∃ψ. elim_equiv φ' ψ" by force
  ultimately show ?thesis
    using no_test_symb_step_exists no_equiv test_symb_false_nullary unfolding no_equiv_def by blast
qed

text ‹Given all the previous theorem and the characterization, once we have rewritten everything,
  there is no equivalence symbol any more.›
lemma no_equiv_full_propo_rew_step_elim_equiv:
  "full (propo_rew_step elim_equiv) φ ψ ⟹ no_equiv ψ"
  using full_propo_rew_step_subformula no_equiv_elim_equiv_step by blast


subsection ‹Eliminate Implication›

text ‹After that, we can eliminate the implication symbols.›
inductive elim_imp :: "'v propo ⇒ 'v propo ⇒ bool" where
[simp]: "elim_imp (FImp φ ψ) (FOr (FNot φ) ψ)"

lemma elim_imp_transformation_consistent:
  "A ⊨ FImp φ ψ ⟷ A ⊨ FOr (FNot φ) ψ"
  by auto

lemma elim_imp_explicit: "elim_imp φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ"
  by (induct φ ψ rule: elim_imp.induct, auto)

lemma elim_imp_consistent: "preserve_models elim_imp"
  unfolding preserve_models_def by (simp add: elim_imp_explicit)

lemma elim_imp_lifted_consistant:
  "preserve_models (full (propo_rew_step elim_imp))"
  by (simp add: elim_imp_consistent)

fun no_imp_symb where
"no_imp_symb (FImp _ _) = False" |
"no_imp_symb _ = True"

lemma no_imp_symb_conn_characterization:
  "wf_conn c l ⟹ no_imp_symb (conn c l) ⟷ c ≠ CImp"
  by (induction rule: wf_conn_induct) auto

definition no_imp where "no_imp ≡ all_subformula_st no_imp_symb"
declare no_imp_def[simp]

lemma no_imp_Imp[simp]:
  "¬no_imp (FImp φ ψ)"
  "no_imp FT"
  "no_imp FF"
  unfolding no_imp_def by auto

lemma all_subformula_st_decomp_explicit_imp[simp]:
  fixes φ ψ :: "'v propo"
  shows
    "no_imp (FNot φ) ⟷ no_imp φ"
    "no_imp (FAnd φ ψ) ⟷ (no_imp φ ∧ no_imp ψ)"
    "no_imp (FOr φ ψ) ⟷ (no_imp φ ∧ no_imp ψ)"
  by auto


text ‹Invariant of the @{term elim_imp} transformation›
lemma elim_imp_no_equiv:
  "elim_imp φ ψ ⟹ no_equiv φ ⟹  no_equiv ψ"
  by (induct φ ψ rule: elim_imp.induct, auto)

lemma elim_imp_inv:
  fixes φ ψ :: "'v propo"
  assumes "full (propo_rew_step elim_imp) φ ψ" and "no_equiv φ"
  shows "no_equiv ψ"
  using full_propo_rew_step_inv_stay_conn[of elim_imp no_equiv_symb φ ψ] assms elim_imp_no_equiv
    no_equiv_symb_conn_characterization unfolding no_equiv_def by metis

lemma no_no_imp_elim_imp_step_exists:
  fixes φ :: "'v propo"
  assumes no_equiv: "¬ no_imp φ"
  shows "∃ψ ψ'. ψ ≼ φ ∧ elim_imp ψ ψ'"
proof -
  have test_symb_false_nullary: "∀x. no_imp_symb FF ∧ no_imp_symb FT ∧ no_imp_symb (FVar (x:: 'v))"
    by auto
  moreover {
     fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
     have H: "elim_imp (conn c l) ψ ⟹ ¬no_imp_symb (conn c l)"
       by (auto elim: elim_imp.cases)
    }
  moreover
    have H': "∀ψ. ¬elim_imp FT ψ" "∀ψ. ¬elim_imp FF ψ" "∀ψ x. ¬elim_imp (FVar x) ψ"
      by (auto elim: elim_imp.cases)+
  moreover
    have "⋀φ. ¬ no_imp_symb φ ⟹ ∃ψ. elim_imp φ ψ"
      by (case_tac φ) (force simp: elim_imp.simps)+
    then have "⋀φ'. φ' ≼ φ ⟹ ¬no_imp_symb φ' ⟹  ∃ ψ. elim_imp φ' ψ" by force
  ultimately show ?thesis
    using no_test_symb_step_exists no_equiv test_symb_false_nullary unfolding no_imp_def by blast
qed

lemma no_imp_full_propo_rew_step_elim_imp: "full (propo_rew_step elim_imp) φ ψ ⟹ no_imp ψ"
  using full_propo_rew_step_subformula no_no_imp_elim_imp_step_exists by blast


subsection "Eliminate all the True and False in the formula"
text ‹Contrary to the book, we have to give the transformation and the ``commutative''
  transformation. The latter is implicit in the book.›
inductive elimTB where
ElimTB1: "elimTB (FAnd φ FT) φ" |
ElimTB1': "elimTB (FAnd FT φ) φ" |

ElimTB2: "elimTB (FAnd φ FF) FF" |
ElimTB2': "elimTB (FAnd FF φ) FF" |

ElimTB3: "elimTB (FOr φ FT) FT" |
ElimTB3': "elimTB (FOr FT φ) FT" |

ElimTB4: "elimTB (FOr φ FF) φ" |
ElimTB4': "elimTB (FOr FF φ) φ" |

ElimTB5: "elimTB (FNot FT) FF" |
ElimTB6: "elimTB (FNot FF) FT"


lemma elimTB_consistent: "preserve_models elimTB"
proof -
  {
    fix φ ψ:: "'b propo"
    have "elimTB φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ" by (induction rule: elimTB.inducts) auto
  }
  then show ?thesis using preserve_models_def by auto
qed

inductive no_T_F_symb :: "'v propo ⇒ bool" where
no_T_F_symb_comp: "c ≠ CF ⟹ c ≠ CT ⟹ wf_conn c l ⟹ (∀φ ∈ set l. φ ≠ FT ∧ φ ≠ FF)
  ⟹ no_T_F_symb (conn c l)"


lemma wf_conn_no_T_F_symb_iff[simp]:
  "wf_conn c ψs ⟹
    no_T_F_symb (conn c ψs) ⟷ (c ≠ CF ∧ c ≠ CT ∧ (∀ψ∈set ψs. ψ ≠ FF ∧ ψ ≠ FT))"
  unfolding no_T_F_symb.simps apply (cases c)
          using wf_conn_list(1) apply fastforce
         using wf_conn_list(2) apply fastforce
        using wf_conn_list(3) apply fastforce
       apply (metis (no_types, opaque_lifting) conn_inj connective.distinct(5,17))
      using conn_inj apply blast+
  done

lemma wf_conn_no_T_F_symb_iff_explicit[simp]:
  "no_T_F_symb (FAnd φ ψ) ⟷ (∀χ ∈ set [φ, ψ]. χ ≠ FF ∧ χ ≠ FT)"
  "no_T_F_symb (FOr φ ψ) ⟷ (∀χ ∈ set [φ, ψ]. χ ≠ FF ∧ χ ≠ FT)"
  "no_T_F_symb (FEq φ ψ) ⟷ (∀χ ∈ set [φ, ψ]. χ ≠ FF ∧ χ ≠ FT)"
  "no_T_F_symb (FImp φ ψ) ⟷ (∀χ ∈ set [φ, ψ]. χ ≠ FF ∧ χ ≠ FT)"
     apply (metis conn.simps(36) conn.simps(37) conn.simps(5) propo.distinct(19)
       wf_conn_helper_facts(5)  wf_conn_no_T_F_symb_iff)
    apply (metis conn.simps(36) conn.simps(37) conn.simps(6) propo.distinct(22)
      wf_conn_helper_facts(6) wf_conn_no_T_F_symb_iff)
   using wf_conn_no_T_F_symb_iff apply fastforce
  by (metis conn.simps(36) conn.simps(37) conn.simps(7) propo.distinct(23) wf_conn_helper_facts(7)
    wf_conn_no_T_F_symb_iff)


lemma no_T_F_symb_false[simp]:
  fixes c :: "'v connective"
  shows
    "¬no_T_F_symb (FT :: 'v propo)"
    "¬no_T_F_symb (FF :: 'v propo)"
    by (metis (no_types) conn.simps(1,2) wf_conn_no_T_F_symb_iff wf_conn_nullary)+

lemma no_T_F_symb_bool[simp]:
  fixes x :: "'v"
  shows "no_T_F_symb (FVar x)"
  using no_T_F_symb_comp wf_conn_nullary by (metis connective.distinct(3, 15) conn.simps(3)
    empty_iff list.set(1))


lemma no_T_F_symb_fnot_imp:
  "¬no_T_F_symb (FNot φ) ⟹ φ = FT ∨ φ = FF"
proof (rule ccontr)
  assume n: "¬ no_T_F_symb (FNot φ)"
  assume "¬ (φ = FT ∨ φ = FF)"
  then have "∀φ' ∈ set [φ]. φ'≠FT ∧ φ'≠FF" by auto
  moreover have "wf_conn CNot [φ]" by simp
  ultimately have "no_T_F_symb (FNot φ)"
    using no_T_F_symb.intros by (metis conn.simps(4) connective.distinct(5,17))
  then show "False" using n by blast
qed

lemma no_T_F_symb_fnot[simp]:
  "no_T_F_symb (FNot φ) ⟷ ¬(φ = FT ∨ φ = FF)"
  using no_T_F_symb.simps no_T_F_symb_fnot_imp by (metis conn_inj_not(2) list.set_intros(1))

text ‹Actually it is not possible to remover every @{term FT} and @{term FF}: if the formula is
  equal to true or false, we can not remove it.›
inductive no_T_F_symb_except_toplevel where
no_T_F_symb_except_toplevel_true[simp]: "no_T_F_symb_except_toplevel FT" |
no_T_F_symb_except_toplevel_false[simp]: "no_T_F_symb_except_toplevel FF" |
noTrue_no_T_F_symb_except_toplevel[simp]: "no_T_F_symb φ ⟹ no_T_F_symb_except_toplevel φ"

lemma no_T_F_symb_except_toplevel_bool:
  fixes x :: "'v"
  shows "no_T_F_symb_except_toplevel (FVar x)"
  by simp

lemma no_T_F_symb_except_toplevel_not_decom:
  "φ ≠ FT ⟹ φ ≠ FF ⟹ no_T_F_symb_except_toplevel (FNot φ)"
  by simp

lemma no_T_F_symb_except_toplevel_bin_decom:
  fixes φ ψ :: "'v propo"
  assumes "φ ≠ FT" and "φ ≠ FF" and "ψ ≠ FT" and "ψ ≠ FF"
  and c: "c∈ binary_connectives"
  shows "no_T_F_symb_except_toplevel (conn c [φ, ψ])"
  by (metis (no_types, lifting) assms c conn.simps(4) list.discI noTrue_no_T_F_symb_except_toplevel
    wf_conn_no_T_F_symb_iff no_T_F_symb_fnot set_ConsD wf_conn_binary wf_conn_helper_facts(1)
    wf_conn_list_decomp(1,2))

lemma no_T_F_symb_except_toplevel_if_is_a_true_false:
  fixes l :: "'v propo list" and c :: "'v connective"
  assumes corr: "wf_conn c l"
  and "FT ∈ set l ∨ FF ∈ set l"
  shows "¬no_T_F_symb_except_toplevel (conn c l)"
  by (metis assms empty_iff no_T_F_symb_except_toplevel.simps wf_conn_no_T_F_symb_iff set_empty
    wf_conn_list(1,2))


lemma no_T_F_symb_except_top_level_false_example[simp]:
  fixes φ ψ :: "'v propo"
  assumes "φ = FT ∨ ψ = FT ∨ φ = FF ∨ ψ = FF"
  shows
    "¬ no_T_F_symb_except_toplevel (FAnd φ ψ)"
    "¬ no_T_F_symb_except_toplevel (FOr φ ψ)"
    "¬ no_T_F_symb_except_toplevel (FImp φ ψ)"
    "¬ no_T_F_symb_except_toplevel (FEq φ ψ)"
  using assms no_T_F_symb_except_toplevel_if_is_a_true_false unfolding binary_connectives_def
    by (metis (no_types) conn.simps(5-8) insert_iff list.simps(14-15) wf_conn_helper_facts(5-8))+

lemma no_T_F_symb_except_top_level_false_not[simp]:
  fixes φ ψ :: "'v propo"
  assumes "φ = FT ∨ φ = FF"
  shows
    "¬ no_T_F_symb_except_toplevel (FNot φ)"
  by (simp add: assms no_T_F_symb_except_toplevel.simps)

text ‹This is the local extension of @{const no_T_F_symb_except_toplevel}.›
definition no_T_F_except_top_level where
"no_T_F_except_top_level ≡ all_subformula_st no_T_F_symb_except_toplevel"

text ‹This is another property we will use. While this version might seem to be the one we want to
  prove, it is not since @{term FT} can not be reduced.›
definition no_T_F where
"no_T_F ≡ all_subformula_st no_T_F_symb"

lemma no_T_F_except_top_level_false:
  fixes l :: "'v propo list" and c :: "'v connective"
  assumes "wf_conn c l"
  and "FT ∈ set l ∨ FF ∈ set l"
  shows "¬no_T_F_except_top_level (conn c l)"
  by (simp add: all_subformula_st_decomp assms no_T_F_except_top_level_def
    no_T_F_symb_except_toplevel_if_is_a_true_false)

lemma no_T_F_except_top_level_false_example[simp]:
  fixes φ ψ :: "'v propo"
  assumes "φ = FT ∨ ψ = FT ∨ φ = FF ∨ ψ = FF"
  shows
    "¬no_T_F_except_top_level (FAnd φ ψ)"
    "¬no_T_F_except_top_level (FOr φ ψ)"
    "¬no_T_F_except_top_level (FEq φ ψ)"
    "¬no_T_F_except_top_level (FImp φ ψ)"
  by (metis all_subformula_st_test_symb_true_phi assms no_T_F_except_top_level_def
    no_T_F_symb_except_top_level_false_example)+


lemma no_T_F_symb_except_toplevel_no_T_F_symb:
  "no_T_F_symb_except_toplevel φ ⟹ φ ≠ FF ⟹ φ ≠ FT ⟹ no_T_F_symb φ"
  by (induct rule: no_T_F_symb_except_toplevel.induct, auto)

text ‹The two following lemmas give the precise link between the two definitions.›
lemma no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb:
  "no_T_F_except_top_level φ ⟹ φ ≠ FF ⟹ φ ≠ FT ⟹ no_T_F φ"
  unfolding no_T_F_except_top_level_def no_T_F_def apply (induct φ)
  using no_T_F_symb_fnot by fastforce+

lemma no_T_F_no_T_F_except_top_level:
  "no_T_F φ ⟹ no_T_F_except_top_level φ"
  unfolding no_T_F_except_top_level_def no_T_F_def
  unfolding all_subformula_st_def by auto

lemma no_T_F_except_top_level_simp[simp]:  "no_T_F_except_top_level FF" "no_T_F_except_top_level FT"
  unfolding no_T_F_except_top_level_def by auto

lemma no_T_F_no_T_F_except_top_level'[simp]:
  "no_T_F_except_top_level φ ⟷ (φ = FF ∨ φ = FT ∨ no_T_F φ)"
  using no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb no_T_F_no_T_F_except_top_level
  by auto

lemma no_T_F_bin_decomp[simp]:
  assumes c: "c ∈ binary_connectives"
  shows "no_T_F (conn c [φ, ψ]) ⟷ (no_T_F φ ∧ no_T_F ψ)"
proof -
  have wf: "wf_conn c [φ, ψ]" using c by auto
  then have "no_T_F (conn c [φ, ψ]) ⟷ (no_T_F_symb (conn c [φ, ψ]) ∧ no_T_F φ ∧ no_T_F ψ)"
    by (simp add: all_subformula_st_decomp no_T_F_def)
  then show "no_T_F (conn c [φ, ψ]) ⟷ (no_T_F φ ∧ no_T_F ψ)"
    using c wf all_subformula_st_decomp list.discI no_T_F_def no_T_F_symb_except_toplevel_bin_decom
      no_T_F_symb_except_toplevel_no_T_F_symb no_T_F_symb_false(1,2) wf_conn_helper_facts(2,3)
      wf_conn_list(1,2) by metis
qed

lemma no_T_F_bin_decomp_expanded[simp]:
  assumes c: "c = CAnd ∨ c = COr ∨ c = CEq ∨ c = CImp"
  shows "no_T_F (conn c [φ, ψ]) ⟷ (no_T_F φ ∧ no_T_F ψ)"
  using no_T_F_bin_decomp assms unfolding binary_connectives_def by blast

lemma no_T_F_comp_expanded_explicit[simp]:
  fixes φ ψ :: "'v propo"
  shows
    "no_T_F (FAnd φ ψ) ⟷ (no_T_F φ ∧ no_T_F ψ)"
    "no_T_F (FOr φ ψ)  ⟷ (no_T_F φ ∧ no_T_F ψ)"
    "no_T_F (FEq φ ψ)  ⟷ (no_T_F φ ∧ no_T_F ψ)"
    "no_T_F (FImp φ ψ) ⟷ (no_T_F φ ∧ no_T_F ψ)"
  using conn.simps(5-8) no_T_F_bin_decomp_expanded by (metis (no_types))+

lemma no_T_F_comp_not[simp]:
  fixes φ ψ :: "'v propo"
  shows "no_T_F (FNot φ) ⟷ no_T_F φ"
  by (metis all_subformula_st_decomp_explicit(3) all_subformula_st_test_symb_true_phi no_T_F_def
    no_T_F_symb_false(1,2) no_T_F_symb_fnot_imp)

lemma no_T_F_decomp:
  fixes φ ψ :: "'v propo"
  assumes φ: "no_T_F (FAnd φ ψ) ∨ no_T_F (FOr φ ψ) ∨ no_T_F (FEq φ ψ) ∨ no_T_F (FImp φ ψ)"
  shows "no_T_F ψ" and "no_T_F φ"
  using assms by auto

lemma no_T_F_decomp_not:
  fixes φ :: "'v propo"
  assumes φ: "no_T_F (FNot φ)"
  shows "no_T_F φ"
  using assms by auto

lemma no_T_F_symb_except_toplevel_step_exists:
  fixes φ ψ :: "'v propo"
  assumes "no_equiv φ" and "no_imp φ"
  shows "ψ ≼ φ ⟹ ¬ no_T_F_symb_except_toplevel ψ ⟹ ∃ψ'. elimTB ψ ψ'"
proof (induct ψ rule: propo_induct_arity)
  case (nullary φ' x)
  then have "False" using no_T_F_symb_except_toplevel_true no_T_F_symb_except_toplevel_false by auto
  then show ?case by blast
next
  case (unary ψ)
  then have "ψ = FF ∨ ψ = FT" using no_T_F_symb_except_toplevel_not_decom by blast
  then show ?case using ElimTB5 ElimTB6 by blast
next
  case (binary φ' ψ1 ψ2)
  note IH1 = this(1) and IH2 = this(2) and φ' = this(3) and Fφ = this(4) and n = this(5)
  {
    assume "φ' = FImp ψ1 ψ2 ∨ φ' = FEq ψ1 ψ2"
    then have "False" using n Fφ subformula_all_subformula_st assms
      by (metis (no_types) no_equiv_eq(1) no_equiv_def no_imp_Imp(1) no_imp_def)
    then have ?case by blast
  }
  moreover {
    assume φ': "φ' = FAnd ψ1 ψ2 ∨ φ' = FOr ψ1 ψ2"
    then have "ψ1 = FT ∨ ψ2 = FT ∨ ψ1 = FF ∨ ψ2 = FF"
      using no_T_F_symb_except_toplevel_bin_decom conn.simps(5,6) n unfolding binary_connectives_def
      by fastforce+
    then have ?case using elimTB.intros φ' by blast
  }
  ultimately show ?case using φ' by blast
qed

lemma no_T_F_except_top_level_rew:
  fixes φ :: "'v propo"
  assumes noTB: "¬ no_T_F_except_top_level φ" and no_equiv: "no_equiv φ" and no_imp: "no_imp φ"
  shows "∃ψ ψ'. ψ ≼ φ ∧ elimTB ψ ψ' "
proof -
  have test_symb_false_nullary: "∀x. no_T_F_symb_except_toplevel (FF:: 'v propo)
    ∧ no_T_F_symb_except_toplevel FT ∧ no_T_F_symb_except_toplevel (FVar (x:: 'v))" by auto
  moreover {
     fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
     have H: "elimTB (conn c l) ψ ⟹ ¬no_T_F_symb_except_toplevel (conn c l) "
       by (cases "conn c l" rule: elimTB.cases, auto)
  }
  moreover {
     fix x :: "'v"
     have H': "no_T_F_except_top_level FT" " no_T_F_except_top_level FF"
       "no_T_F_except_top_level (FVar x)"
       by (auto simp: no_T_F_except_top_level_def test_symb_false_nullary)
  }
  moreover {
     fix ψ
     have "ψ ≼ φ ⟹ ¬ no_T_F_symb_except_toplevel ψ ⟹ ∃ψ'. elimTB ψ ψ'"
       using no_T_F_symb_except_toplevel_step_exists no_equiv no_imp by auto
  }
  ultimately show ?thesis
    using no_test_symb_step_exists noTB unfolding no_T_F_except_top_level_def by blast
qed

lemma elimTB_inv:
  fixes φ ψ :: "'v propo"
  assumes "full (propo_rew_step elimTB) φ ψ "
  and "no_equiv φ" and "no_imp φ"
  shows "no_equiv ψ" and "no_imp ψ"
proof -
  {
     fix φ ψ :: "'v propo"
     have H: "elimTB φ ψ ⟹ no_equiv φ ⟹  no_equiv ψ"
       by (induct φ ψ rule: elimTB.induct, auto)
  }
  then show "no_equiv ψ"
    using full_propo_rew_step_inv_stay_conn[of elimTB no_equiv_symb φ ψ]
      no_equiv_symb_conn_characterization assms unfolding no_equiv_def by metis
next
  {
     fix φ ψ :: "'v propo"
     have H: "elimTB φ ψ ⟹ no_imp φ ⟹ no_imp ψ"
       by (induct φ ψ rule: elimTB.induct, auto)
  }
  then show "no_imp ψ"
    using full_propo_rew_step_inv_stay_conn[of elimTB no_imp_symb φ ψ] assms
      no_imp_symb_conn_characterization unfolding no_imp_def by metis
qed

lemma elimTB_full_propo_rew_step:
  fixes φ ψ :: "'v propo"
  assumes "no_equiv φ" and "no_imp φ" and "full (propo_rew_step elimTB) φ ψ"
  shows "no_T_F_except_top_level ψ"
  using full_propo_rew_step_subformula no_T_F_except_top_level_rew assms elimTB_inv by fastforce


subsection "PushNeg"
text ‹Push the negation inside the formula, until the litteral.›
inductive pushNeg where
PushNeg1[simp]: "pushNeg (FNot (FAnd φ ψ)) (FOr (FNot φ) (FNot ψ))" |
PushNeg2[simp]: "pushNeg (FNot (FOr φ ψ)) (FAnd (FNot φ) (FNot ψ))" |
PushNeg3[simp]: "pushNeg (FNot (FNot φ)) φ"


lemma pushNeg_transformation_consistent:
"A ⊨ FNot (FAnd φ ψ) ⟷ A ⊨ (FOr (FNot φ) (FNot ψ))"
"A ⊨ FNot (FOr φ ψ)  ⟷ A ⊨ (FAnd (FNot φ) (FNot ψ))"
"A ⊨ FNot (FNot φ)   ⟷ A ⊨ φ"
  by auto


lemma pushNeg_explicit: "pushNeg φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ"
  by (induct φ ψ rule: pushNeg.induct, auto)

lemma pushNeg_consistent: "preserve_models pushNeg"
  unfolding preserve_models_def by (simp add: pushNeg_explicit)


lemma pushNeg_lifted_consistant:
"preserve_models (full (propo_rew_step pushNeg))"
  by (simp add: pushNeg_consistent)

fun simple where
"simple FT = True" |
"simple FF = True" |
"simple (FVar _) = True" |
"simple _ = False"

lemma simple_decomp:
  "simple φ ⟷ (φ = FT ∨ φ = FF ∨ (∃x. φ = FVar x))"
  by (cases φ) auto

lemma subformula_conn_decomp_simple:
  fixes φ ψ :: "'v propo"
  assumes s: "simple ψ"
  shows "φ ≼ FNot ψ ⟷ (φ = FNot ψ ∨ φ = ψ)"
proof -
  have "φ ≼ conn CNot [ψ] ⟷ (φ = conn CNot [ψ] ∨ (∃ ψ∈ set [ψ]. φ ≼ ψ))"
    using subformula_conn_decomp wf_conn_helper_facts(1) by metis
  then show "φ ≼ FNot ψ ⟷ (φ = FNot ψ ∨ φ = ψ)" using s by (auto simp: simple_decomp)
qed

lemma subformula_conn_decomp_explicit[simp]:
  fixes φ :: "'v propo" and x :: "'v"
  shows
    "φ ≼ FNot FT ⟷ (φ = FNot FT ∨ φ = FT)"
    "φ ≼ FNot FF ⟷ (φ = FNot FF ∨ φ = FF)"
    "φ ≼ FNot (FVar x) ⟷ (φ = FNot (FVar x) ∨ φ = FVar x)"
  by (auto simp: subformula_conn_decomp_simple)


fun simple_not_symb where
"simple_not_symb (FNot φ) = (simple φ)" |
"simple_not_symb _ = True"

definition simple_not where
"simple_not = all_subformula_st simple_not_symb"
declare simple_not_def[simp]

lemma simple_not_Not[simp]:
  "¬ simple_not (FNot (FAnd φ ψ))"
  "¬ simple_not (FNot (FOr φ ψ))"
  by auto

lemma simple_not_step_exists:
  fixes φ ψ :: "'v propo"
  assumes "no_equiv φ" and "no_imp φ"
  shows "ψ ≼ φ ⟹ ¬ simple_not_symb ψ ⟹ ∃ψ'. pushNeg ψ ψ'"
  apply (induct ψ, auto)
  apply (rename_tac ψ, case_tac ψ, auto intro: pushNeg.intros)
  by (metis assms(1,2) no_imp_Imp(1) no_equiv_eq(1) no_imp_def no_equiv_def
    subformula_in_subformula_not subformula_all_subformula_st)+

lemma simple_not_rew:
  fixes φ :: "'v propo"
  assumes noTB: "¬ simple_not φ" and no_equiv: "no_equiv φ" and no_imp: "no_imp φ"
  shows "∃ψ ψ'. ψ ≼ φ ∧ pushNeg ψ ψ'"
proof -
  have "∀x. simple_not_symb (FF:: 'v propo) ∧ simple_not_symb FT ∧ simple_not_symb (FVar (x:: 'v))"
    by auto
  moreover {
     fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
     have H: "pushNeg (conn c l) ψ ⟹ ¬simple_not_symb (conn c l)"
       by (cases "conn c l" rule: pushNeg.cases) auto
  }
  moreover {
     fix x :: "'v"
     have H': "simple_not FT" "simple_not FF" "simple_not (FVar x)"
       by simp_all
  }
  moreover {
     fix ψ :: "'v propo"
     have "ψ ≼ φ ⟹ ¬ simple_not_symb ψ ⟹ ∃ψ'. pushNeg ψ ψ'"
       using simple_not_step_exists no_equiv no_imp by blast
  }
  ultimately show ?thesis using no_test_symb_step_exists noTB unfolding simple_not_def by blast
qed

lemma no_T_F_except_top_level_pushNeg1:
  "no_T_F_except_top_level (FNot (FAnd φ ψ)) ⟹ no_T_F_except_top_level (FOr (FNot φ) (FNot ψ))"
  using no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb no_T_F_comp_not no_T_F_decomp(1)
    no_T_F_decomp(2) no_T_F_no_T_F_except_top_level by (metis no_T_F_comp_expanded_explicit(2)
      propo.distinct(5,17))

lemma no_T_F_except_top_level_pushNeg2:
  "no_T_F_except_top_level (FNot (FOr φ ψ)) ⟹ no_T_F_except_top_level (FAnd (FNot φ) (FNot ψ))"
  by auto

lemma no_T_F_symb_pushNeg:
  "no_T_F_symb (FOr (FNot φ') (FNot ψ'))"
  "no_T_F_symb (FAnd (FNot φ') (FNot ψ'))"
  "no_T_F_symb (FNot (FNot φ'))"
  by auto

lemma propo_rew_step_pushNeg_no_T_F_symb:
  "propo_rew_step pushNeg φ ψ ⟹ no_T_F_except_top_level φ ⟹ no_T_F_symb φ ⟹ no_T_F_symb ψ"
  apply (induct rule: propo_rew_step.induct)
  apply (cases rule: pushNeg.cases)
  apply simp_all
  apply (metis no_T_F_symb_pushNeg(1))
  apply (metis no_T_F_symb_pushNeg(2))
  apply (simp, metis all_subformula_st_test_symb_true_phi no_T_F_def)
proof -
  fix φ φ':: "'a propo" and c:: "'a connective" and ξ ξ':: "'a propo list"
  assume rel: "propo_rew_step pushNeg φ φ'"
  and IH: "no_T_F φ ⟹ no_T_F_symb φ ⟹ no_T_F_symb φ'"
  and wf: "wf_conn c (ξ @ φ # ξ')"
  and n: "conn c (ξ @ φ # ξ') = FF ∨ conn c (ξ @ φ # ξ') = FT ∨ no_T_F (conn c (ξ @ φ # ξ'))"
  and x: "c ≠ CF ∧ c ≠ CT ∧ φ ≠ FF ∧ φ ≠ FT ∧ (∀ψ ∈ set ξ ∪ set ξ'. ψ ≠ FF ∧ ψ ≠ FT)"
  then have "c ≠ CF ∧ c ≠ CF ∧ wf_conn c (ξ @ φ' # ξ')"
    using wf_conn_no_arity_change_helper wf_conn_no_arity_change by metis
  moreover have n': "no_T_F (conn c (ξ @ φ # ξ'))" using n by (simp add: wf wf_conn_list(1,2))
  moreover
  {
    have "no_T_F φ"
      by (metis Un_iff all_subformula_st_decomp list.set_intros(1)  n' wf no_T_F_def set_append)
    moreover then have "no_T_F_symb φ"
      by (simp add: all_subformula_st_test_symb_true_phi no_T_F_def)
    ultimately have "φ' ≠ FF ∧ φ' ≠ FT"
      using IH no_T_F_symb_false(1) no_T_F_symb_false(2) by blast
    then have "∀ψ∈ set (ξ @ φ' # ξ'). ψ ≠ FF ∧ ψ ≠ FT" using x by auto
  }
  ultimately show "no_T_F_symb (conn c (ξ @ φ' # ξ'))" by (simp add: x)
qed

lemma propo_rew_step_pushNeg_no_T_F:
  "propo_rew_step pushNeg φ ψ ⟹ no_T_F φ ⟹ no_T_F ψ"
proof (induct rule: propo_rew_step.induct)
  case global_rel
  then show ?case
    by (metis (no_types, lifting) no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb
      no_T_F_def no_T_F_except_top_level_pushNeg1 no_T_F_except_top_level_pushNeg2
      no_T_F_no_T_F_except_top_level all_subformula_st_decomp_explicit(3) pushNeg.simps
      simple.simps(1,2,5,6))
next
  case (propo_rew_one_step_lift φ φ' c ξ ξ')
  note rel = this(1) and IH = this(2) and wf = this(3) and no_T_F = this(4)
  moreover have wf': "wf_conn c (ξ @ φ' # ξ')"
    using wf_conn_no_arity_change wf_conn_no_arity_change_helper wf by metis
  ultimately show "no_T_F (conn c (ξ @ φ' # ξ'))"
    using all_subformula_st_test_symb_true_phi
    by (fastforce simp: no_T_F_def all_subformula_st_decomp wf wf')
qed


lemma pushNeg_inv:
  fixes φ ψ :: "'v propo"
  assumes "full (propo_rew_step pushNeg) φ ψ"
  and "no_equiv φ" and "no_imp φ" and "no_T_F_except_top_level φ"
  shows "no_equiv ψ" and "no_imp ψ" and "no_T_F_except_top_level ψ"
proof -
  {
    fix φ ψ :: "'v propo"
    assume rel: "propo_rew_step pushNeg φ ψ"
    and no: "no_T_F_except_top_level φ"
    then have " no_T_F_except_top_level ψ"
      proof -
        {
          assume "φ = FT ∨ φ = FF"
          from rel this have False
            apply (induct rule: propo_rew_step.induct)
              using pushNeg.cases apply blast
            using wf_conn_list(1) wf_conn_list(2) by auto
          then have "no_T_F_except_top_level ψ" by blast
        }
        moreover {
          assume "φ ≠ FT ∧ φ ≠ FF"
          then have "no_T_F φ"
            by (metis no no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb)
          then have "no_T_F ψ"
            using propo_rew_step_pushNeg_no_T_F rel by auto
          then have "no_T_F_except_top_level ψ" by (simp add: no_T_F_no_T_F_except_top_level)
        }
        ultimately show "no_T_F_except_top_level ψ" by metis
      qed
  }
  moreover {
     fix c :: "'v connective" and ξ ξ' :: "'v propo list" and ζ ζ' :: "'v propo"
     assume rel: "propo_rew_step pushNeg ζ ζ'"
     and incl: "ζ ≼ φ"
     and corr: "wf_conn c (ξ @ ζ # ξ')"
     and no_T_F: "no_T_F_symb_except_toplevel (conn c (ξ @ ζ # ξ'))"
     and n: "no_T_F_symb_except_toplevel ζ'"
     have "no_T_F_symb_except_toplevel (conn c (ξ @ ζ' # ξ'))"
     proof
       have p: "no_T_F_symb (conn c (ξ @ ζ # ξ'))"
         using corr wf_conn_list(1) wf_conn_list(2) no_T_F_symb_except_toplevel_no_T_F_symb no_T_F
         by blast
       have l: "∀φ∈set (ξ @ ζ # ξ'). φ ≠ FT ∧ φ ≠ FF"
         using corr wf_conn_no_T_F_symb_iff p by blast
       from rel incl have "ζ'≠FT ∧ζ'≠FF"
         apply (induction ζ ζ' rule: propo_rew_step.induct)
         apply (cases rule: pushNeg.cases, auto)
         by (metis assms(4) no_T_F_symb_except_top_level_false_not no_T_F_except_top_level_def
           all_subformula_st_test_symb_true_phi subformula_in_subformula_not
           subformula_all_subformula_st append_is_Nil_conv list.distinct(1)
           wf_conn_no_arity_change_helper wf_conn_list(1,2) wf_conn_no_arity_change)+
       then have "∀φ ∈ set (ξ @ ζ' # ξ'). φ ≠ FT ∧ φ ≠ FF" using l by auto
       moreover have "c ≠ CT ∧ c ≠ CF" using corr by auto
       ultimately show "no_T_F_symb (conn c (ξ @ ζ' # ξ'))"
         by (metis corr no_T_F_symb_comp wf_conn_no_arity_change wf_conn_no_arity_change_helper)
     qed
  }
  ultimately show "no_T_F_except_top_level ψ"
    using full_propo_rew_step_inv_stay_with_inc[of pushNeg no_T_F_symb_except_toplevel φ] assms
      subformula_refl unfolding no_T_F_except_top_level_def full_unfold by metis
next
  {
    fix φ ψ :: "'v propo"
    have H: "pushNeg φ ψ ⟹ no_equiv φ ⟹ no_equiv ψ"
      by (induct φ ψ rule: pushNeg.induct, auto)
  }
  then show "no_equiv ψ"
    using full_propo_rew_step_inv_stay_conn[of pushNeg no_equiv_symb φ ψ]
    no_equiv_symb_conn_characterization assms unfolding no_equiv_def full_unfold by metis
next
  {
    fix φ ψ :: "'v propo"
    have H: "pushNeg φ ψ ⟹ no_imp φ ⟹  no_imp ψ"
      by (induct φ ψ rule: pushNeg.induct, auto)
  }
  then show "no_imp ψ"
    using full_propo_rew_step_inv_stay_conn[of pushNeg no_imp_symb φ ψ] assms
      no_imp_symb_conn_characterization unfolding no_imp_def full_unfold by metis
qed


lemma pushNeg_full_propo_rew_step:
  fixes φ ψ :: "'v propo"
  assumes
    "no_equiv φ" and
    "no_imp φ" and
    "full (propo_rew_step pushNeg) φ ψ" and
    "no_T_F_except_top_level φ"
  shows "simple_not ψ"
  using assms full_propo_rew_step_subformula pushNeg_inv(1,2) simple_not_rew by blast


subsection ‹Push Inside›

inductive push_conn_inside :: "'v connective ⇒ 'v connective ⇒ 'v propo ⇒ 'v propo ⇒ bool"
  for c c':: "'v connective" where
push_conn_inside_l[simp]: "c = CAnd ∨ c = COr ⟹ c' = CAnd ∨ c' = COr
  ⟹ push_conn_inside c c' (conn c [conn c' [φ1, φ2], ψ])
        (conn c' [conn c [φ1, ψ], conn c [φ2, ψ]])" |
push_conn_inside_r[simp]: "c = CAnd ∨ c = COr ⟹ c' = CAnd ∨ c' = COr
  ⟹ push_conn_inside c c' (conn c [ψ, conn c' [φ1, φ2]])
    (conn c' [conn c [ψ, φ1], conn c [ψ, φ2]])"


lemma push_conn_inside_explicit: "push_conn_inside c c' φ ψ ⟹ ∀A. A⊨φ ⟷ A⊨ψ"
  by (induct φ ψ rule: push_conn_inside.induct, auto)

lemma push_conn_inside_consistent: "preserve_models (push_conn_inside c c')"
  unfolding preserve_models_def by (simp add: push_conn_inside_explicit)

lemma propo_rew_step_push_conn_inside[simp]:
 "¬propo_rew_step (push_conn_inside c c') FT ψ" "¬propo_rew_step (push_conn_inside c c') FF ψ"
 proof -
  {
    {
      fix φ ψ
      have "push_conn_inside c c' φ ψ ⟹ φ = FT ∨ φ = FF ⟹ False"
        by (induct rule: push_conn_inside.induct, auto)
    } note H = this
    fix φ
    have "propo_rew_step (push_conn_inside c c') φ ψ ⟹ φ = FT ∨ φ = FF ⟹ False"
      apply (induct rule: propo_rew_step.induct, auto simp: wf_conn_list(1) wf_conn_list(2))
      using H by blast+
  }
  then show
    "¬propo_rew_step (push_conn_inside c c') FT ψ"
    "¬propo_rew_step (push_conn_inside c c') FF ψ" by blast+
qed


inductive not_c_in_c'_symb:: "'v connective ⇒ 'v connective ⇒ 'v propo ⇒ bool" for c c' where
not_c_in_c'_symb_l[simp]: "wf_conn c [conn c' [φ, φ'], ψ] ⟹ wf_conn c' [φ, φ']
  ⟹ not_c_in_c'_symb c c' (conn c [conn c' [φ, φ'], ψ])" |
not_c_in_c'_symb_r[simp]: "wf_conn c [ψ, conn c' [φ, φ']] ⟹ wf_conn c' [φ, φ']
  ⟹ not_c_in_c'_symb c c' (conn c [ψ, conn c' [φ, φ']])"

abbreviation "c_in_c'_symb c c' φ ≡ ¬not_c_in_c'_symb c c' φ"


lemma c_in_c'_symb_simp:
  "not_c_in_c'_symb c c' ξ ⟹ ξ = FF ∨ ξ = FT ∨ ξ = FVar x ∨ ξ = FNot FF ∨ ξ = FNot FT
    ∨ ξ = FNot (FVar x)⟹ False"
  apply (induct rule: not_c_in_c'_symb.induct, auto simp: wf_conn.simps wf_conn_list(1-3))
  using conn_inj_not(2) wf_conn_binary unfolding binary_connectives_def by fastforce+

lemma c_in_c'_symb_simp'[simp]:
  "¬not_c_in_c'_symb c c' FF"
  "¬not_c_in_c'_symb c c' FT"
  "¬not_c_in_c'_symb c c' (FVar x)"
  "¬not_c_in_c'_symb c c' (FNot FF)"
  "¬not_c_in_c'_symb c c' (FNot FT)"
  "¬not_c_in_c'_symb c c' (FNot (FVar x))"
  using c_in_c'_symb_simp by metis+

definition c_in_c'_only where
"c_in_c'_only c c' ≡ all_subformula_st (c_in_c'_symb c c')"

lemma c_in_c'_only_simp[simp]:
  "c_in_c'_only c c' FF"
  "c_in_c'_only c c' FT"
  "c_in_c'_only c c' (FVar x)"
  "c_in_c'_only c c' (FNot FF)"
  "c_in_c'_only c c' (FNot FT)"
  "c_in_c'_only c c' (FNot (FVar x))"
  unfolding c_in_c'_only_def by auto


lemma not_c_in_c'_symb_commute:
  "not_c_in_c'_symb c c' ξ ⟹ wf_conn c [φ, ψ] ⟹ ξ = conn c [φ, ψ]
    ⟹ not_c_in_c'_symb c c' (conn c [ψ, φ])"
proof (induct rule: not_c_in_c'_symb.induct)
  case (not_c_in_c'_symb_r φ' φ'' ψ') note H = this
  then have ψ: "ψ = conn c' [φ'', ψ']" using conn_inj by auto
  have "wf_conn c [conn c' [φ'', ψ'], φ]"
    using H(1) wf_conn_no_arity_change length_Cons by metis
  then show "not_c_in_c'_symb c c' (conn c [ψ, φ])"
    unfolding ψ using not_c_in_c'_symb.intros(1) H by auto
next
  case (not_c_in_c'_symb_l φ' φ'' ψ') note H = this
  then have "φ = conn c' [φ', φ'']" using conn_inj by auto
  moreover have "wf_conn c [ψ', conn c' [φ', φ'']]"
    using H(1) wf_conn_no_arity_change length_Cons by metis
  ultimately show "not_c_in_c'_symb c c' (conn c [ψ, φ])"
    using not_c_in_c'_symb.intros(2) conn_inj not_c_in_c'_symb_l.hyps
      not_c_in_c'_symb_l.prems(1,2) by blast
qed

lemma not_c_in_c'_symb_commute':
  "wf_conn c [φ, ψ] ⟹ c_in_c'_symb c c' (conn c [φ, ψ])  ⟷ c_in_c'_symb c c' (conn c [ψ, φ])"
  using not_c_in_c'_symb_commute wf_conn_no_arity_change by (metis length_Cons)

lemma not_c_in_c'_comm:
  assumes wf: "wf_conn c [φ, ψ]"
  shows "c_in_c'_only c c' (conn c [φ, ψ]) ⟷ c_in_c'_only c c' (conn c [ψ, φ])" (is "?A ⟷ ?B")
proof -
  have "?A ⟷ (c_in_c'_symb c c' (conn c [φ, ψ])
               ∧ (∀ξ ∈ set [φ, ψ]. all_subformula_st (c_in_c'_symb c c') ξ))"
    using all_subformula_st_decomp wf unfolding c_in_c'_only_def by fastforce
  also have "… ⟷ (c_in_c'_symb c c' (conn c [ψ, φ])
                    ∧ (∀ξ ∈ set [ψ, φ]. all_subformula_st (c_in_c'_symb c c') ξ))"
    using not_c_in_c'_symb_commute' wf by auto
  also
    have "wf_conn c [ψ, φ]" using wf_conn_no_arity_change wf by (metis length_Cons)
    then have "(c_in_c'_symb c c' (conn c [ψ, φ])
             ∧ (∀ξ ∈ set [ψ, φ]. all_subformula_st (c_in_c'_symb c c') ξ))
           ⟷ ?B"
      using all_subformula_st_decomp unfolding c_in_c'_only_def by fastforce
  finally show ?thesis .
qed

lemma not_c_in_c'_simp[simp]:
  fixes φ1 φ2 ψ :: "'v propo" and x :: "'v"
  shows
  "c_in_c'_symb c c' FT"
  "c_in_c'_symb c c' FF"
  "c_in_c'_symb c c' (FVar x)"
  "wf_conn c [conn c' [φ1, φ2], ψ] ⟹ wf_conn c' [φ1, φ2]
    ⟹ ¬ c_in_c'_only c c' (conn c [conn c' [φ1, φ2], ψ])"
  apply (simp_all add: c_in_c'_only_def)
  using all_subformula_st_test_symb_true_phi not_c_in_c'_symb_l by blast

lemma c_in_c'_symb_not[simp]:
  fixes c c' :: "'v connective" and ψ :: "'v propo"
  shows "c_in_c'_symb c c' (FNot ψ)"
proof -
  {
    fix ξ :: "'v propo"
    have "not_c_in_c'_symb c c' (FNot ψ) ⟹ False"
      apply (induct "FNot ψ" rule: not_c_in_c'_symb.induct)
      using conn_inj_not(2) by blast+
  }
 then show ?thesis by auto
qed

lemma c_in_c'_symb_step_exists:
  fixes φ :: "'v propo"
  assumes c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
  shows "ψ ≼ φ ⟹ ¬ c_in_c'_symb c c' ψ ⟹ ∃ψ'. push_conn_inside c c' ψ ψ'"
  apply (induct ψ rule: propo_induct_arity)
  apply auto[2]
proof -
  fix ψ1 ψ2 φ':: "'v propo"
  assume IHψ1: "ψ1 ≼ φ ⟹ ¬ c_in_c'_symb c c' ψ1 ⟹ Ex (push_conn_inside c c' ψ1)"
  and IHψ2: "ψ1 ≼ φ ⟹ ¬ c_in_c'_symb c c' ψ1 ⟹ Ex (push_conn_inside c c' ψ1)"
  and φ': "φ' = FAnd ψ1 ψ2 ∨ φ' = FOr ψ1 ψ2 ∨ φ' = FImp ψ1 ψ2 ∨ φ' = FEq ψ1 ψ2"
  and inφ: "φ' ≼ φ" and n0: "¬c_in_c'_symb c c' φ'"
  then have n: "not_c_in_c'_symb c c' φ'" by auto
  {
    assume φ': "φ' = conn c [ψ1, ψ2]"
    obtain a b where "ψ1 = conn c' [a, b] ∨ ψ2 = conn c' [a, b]"
      using n φ' apply (induct rule: not_c_in_c'_symb.induct)
      using c by force+
    then have "Ex (push_conn_inside c c' φ')"
      unfolding φ' apply auto
      using push_conn_inside.intros(1) c c' apply blast
      using push_conn_inside.intros(2) c c' by blast
  }
  moreover {
     assume φ': "φ' ≠ conn c [ψ1, ψ2]"
     have "∀φ c ca. ∃φ1 ψ1 ψ2 ψ1' ψ2' φ2'. conn (c::'v connective) [φ1, conn ca [ψ1, ψ2]] = φ
             ∨ conn c [conn ca [ψ1', ψ2'], φ2'] = φ ∨ c_in_c'_symb c ca φ"
       by (metis not_c_in_c'_symb.cases)
     then have "Ex (push_conn_inside c c' φ')"
       by (metis (no_types) c c' n push_conn_inside_l push_conn_inside_r)
  }
  ultimately show "Ex (push_conn_inside c c' φ')" by blast
qed


lemma c_in_c'_symb_rew:
  fixes φ :: "'v propo"
  assumes noTB: "¬c_in_c'_only c c' φ"
  and c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
  shows "∃ψ ψ'. ψ ≼ φ ∧ push_conn_inside c c' ψ ψ' "
proof -
  have test_symb_false_nullary:
    "∀x. c_in_c'_symb c c' (FF:: 'v propo) ∧ c_in_c'_symb c c' FT
      ∧ c_in_c'_symb c c' (FVar (x:: 'v))"
    by auto
  moreover {
    fix x :: "'v"
    have H': "c_in_c'_symb c c' FT" "c_in_c'_symb c c' FF" "c_in_c'_symb c c' (FVar x)"
      by simp+
  }
  moreover {
    fix ψ :: "'v propo"
    have "ψ ≼ φ ⟹ ¬ c_in_c'_symb c c' ψ ⟹ ∃ψ'. push_conn_inside c c' ψ ψ'"
      by (auto simp: assms(2) c' c_in_c'_symb_step_exists)
  }
  ultimately show ?thesis using noTB no_test_symb_step_exists[of "c_in_c'_symb c c'"]
    unfolding c_in_c'_only_def by metis
qed

lemma push_conn_insidec_in_c'_symb_no_T_F:
  fixes φ ψ :: "'v propo"
  shows "propo_rew_step (push_conn_inside c c') φ ψ ⟹ no_T_F φ ⟹ no_T_F ψ"
proof (induct rule: propo_rew_step.induct)
  case (global_rel φ ψ)
  then show "no_T_F ψ"
    by (cases rule: push_conn_inside.cases, auto)
next
  case (propo_rew_one_step_lift φ φ' c ξ ξ')
  note rel = this(1) and IH = this(2) and wf = this(3) and no_T_F = this(4)
  have "no_T_F φ"
    using wf no_T_F no_T_F_def subformula_into_subformula subformula_all_subformula_st
    subformula_refl by (metis (no_types) in_set_conv_decomp)
  then have φ': "no_T_F φ'" using IH by blast

  have "∀ζ ∈ set (ξ @ φ # ξ'). no_T_F ζ" by (metis wf no_T_F no_T_F_def all_subformula_st_decomp)
  then have n: "∀ζ ∈ set (ξ @ φ' # ξ'). no_T_F ζ" using φ' by auto
  then have n': "∀ζ ∈ set (ξ @ φ' # ξ'). ζ ≠  FF ∧ ζ ≠ FT"
    using φ' by (metis no_T_F_symb_false(1) no_T_F_symb_false(2) no_T_F_def
      all_subformula_st_test_symb_true_phi)

  have wf': "wf_conn c (ξ @ φ' # ξ')"
    using wf wf_conn_no_arity_change by (metis wf_conn_no_arity_change_helper)
  {
    fix x :: "'v"
    assume "c = CT ∨ c = CF ∨ c = CVar x"
    then have "False" using wf by auto
    then have "no_T_F (conn c (ξ @ φ' # ξ'))" by blast
  }
  moreover {
    assume c: "c = CNot"
    then have "ξ = []" "ξ' = []" using wf by auto
    then have "no_T_F (conn c (ξ @ φ' # ξ'))"
      using c by (metis φ' conn.simps(4) no_T_F_symb_false(1,2) no_T_F_symb_fnot no_T_F_def
        all_subformula_st_decomp_explicit(3) all_subformula_st_test_symb_true_phi self_append_conv2)
  }
  moreover {
    assume c: "c ∈ binary_connectives"
    then have "no_T_F_symb (conn c (ξ @ φ' # ξ'))" using wf' n' no_T_F_symb.simps by fastforce
    then have "no_T_F (conn c (ξ @ φ' # ξ'))"
      by (metis all_subformula_st_decomp_imp wf' n no_T_F_def)
  }
  ultimately show "no_T_F (conn c (ξ @ φ' # ξ'))" using connective_cases_arity by auto
qed


lemma simple_propo_rew_step_push_conn_inside_inv:
"propo_rew_step (push_conn_inside c c') φ ψ ⟹ simple φ ⟹ simple ψ"
  apply (induct rule: propo_rew_step.induct)
  apply (rename_tac φ, case_tac φ, auto simp: push_conn_inside.simps)[]
  by (metis append_is_Nil_conv list.distinct(1) simple.elims(2) wf_conn_list(1-3))


lemma simple_propo_rew_step_inv_push_conn_inside_simple_not:
  fixes c c' :: "'v connective" and φ ψ :: "'v propo"
  shows "propo_rew_step (push_conn_inside c c') φ ψ ⟹ simple_not φ ⟹ simple_not ψ"
proof (induct rule: propo_rew_step.induct)
  case (global_rel φ ψ)
  then show ?case by (cases φ, auto simp: push_conn_inside.simps)
next
  case (propo_rew_one_step_lift φ φ' ca ξ ξ') note rew = this(1) and IH = this(2) and wf = this(3)
   and simple = this(4)
  show ?case
    proof (cases ca rule: connective_cases_arity)
      case nullary
      then show ?thesis using propo_rew_one_step_lift by auto
    next
      case binary note ca = this
      obtain a b where ab: "ξ @ φ' # ξ' = [a, b]"
        using wf ca list_length2_decomp wf_conn_bin_list_length
        by (metis (no_types) wf_conn_no_arity_change_helper)
      have "∀ζ ∈ set (ξ @ φ # ξ'). simple_not ζ"
        by (metis wf all_subformula_st_decomp simple simple_not_def)
      then have "∀ζ ∈ set (ξ @ φ' # ξ'). simple_not ζ" using IH by simp
      moreover have "simple_not_symb (conn ca (ξ @ φ' # ξ'))" using ca
      by (metis ab conn.simps(5-8) helper_fact simple_not_symb.simps(5) simple_not_symb.simps(6)
          simple_not_symb.simps(7) simple_not_symb.simps(8))
      ultimately show ?thesis
        by (simp add: ab all_subformula_st_decomp ca)
    next
      case unary
      then show ?thesis
         using rew simple_propo_rew_step_push_conn_inside_inv[OF rew] IH local.wf simple by auto
    qed
qed

lemma propo_rew_step_push_conn_inside_simple_not:
  fixes φ φ' :: "'v propo" and ξ ξ' :: "'v propo list" and c :: "'v connective"
  assumes
    "propo_rew_step (push_conn_inside c c') φ φ'" and
    "wf_conn c (ξ @ φ # ξ')" and
    "simple_not_symb (conn c (ξ @ φ # ξ'))" and
    "simple_not_symb φ'"
  shows "simple_not_symb (conn c (ξ @ φ' # ξ'))"
  using assms
proof (induction rule: propo_rew_step.induct)
print_cases
  case (global_rel)
  then show ?case
    by (metis conn.simps(12,17) list.discI push_conn_inside.cases simple_not_symb.elims(3)
      wf_conn_helper_facts(5) wf_conn_list(2) wf_conn_list(8) wf_conn_no_arity_change
      wf_conn_no_arity_change_helper)
next
  case (propo_rew_one_step_lift φ φ' c' χs χs') note tel = this(1) and wf = this(2) and
    IH = this(3) and wf' = this(4) and simple' = this(5) and simple = this(6)
  then show ?case
    proof (cases c' rule: connective_cases_arity)
      case nullary
      then show ?thesis using wf simple simple' by auto
    next
      case binary note c = this(1)
      have corr': "wf_conn c (ξ @ conn c' (χs @ φ' # χs') # ξ')"
        using wf wf_conn_no_arity_change
        by (metis wf' wf_conn_no_arity_change_helper)
      then show ?thesis
        using c propo_rew_one_step_lift wf
        by (metis conn.simps(17) connective.distinct(37) propo_rew_step_subformula_imp
          push_conn_inside.cases simple_not_symb.elims(3) wf_conn.simps wf_conn_list(2,8))
    next
      case unary
      then have empty: "χs = []" "χs' = []" using wf by auto
      then show ?thesis using simple unary simple' wf wf'
        by (metis connective.distinct(37) connective.distinct(39) propo_rew_step_subformula_imp
          push_conn_inside.cases simple_not_symb.elims(3) tel wf_conn_list(8)
          wf_conn_no_arity_change wf_conn_no_arity_change_helper)
    qed
qed

lemma push_conn_inside_not_true_false:
  "push_conn_inside c c' φ ψ ⟹ ψ ≠ FT ∧ ψ ≠ FF"
  by (induct rule: push_conn_inside.induct, auto)

lemma push_conn_inside_inv:
  fixes φ ψ :: "'v propo"
  assumes "full (propo_rew_step (push_conn_inside c c')) φ ψ"
  and "no_equiv φ" and "no_imp φ" and "no_T_F_except_top_level φ" and "simple_not φ"
  shows "no_equiv ψ" and "no_imp ψ" and "no_T_F_except_top_level ψ" and "simple_not ψ"
proof -
  {
     {
        fix φ ψ :: "'v propo"
        have H: "push_conn_inside c c' φ ψ ⟹ all_subformula_st simple_not_symb φ
          ⟹ all_subformula_st simple_not_symb ψ"
          by (induct φ ψ rule: push_conn_inside.induct, auto)
     } note H = this

    fix φ ψ :: "'v propo"
    have H: "propo_rew_step (push_conn_inside c c') φ ψ ⟹ all_subformula_st simple_not_symb φ
      ⟹ all_subformula_st simple_not_symb ψ"
      apply (induct φ ψ rule: propo_rew_step.induct)
      using H apply simp
      proof (rename_tac φ φ' ca ψs ψs', case_tac ca rule: connective_cases_arity)
        fix φ φ' :: "'v propo" and c:: "'v connective" and ξ ξ':: "'v propo list"
        and x:: "'v"
        assume "wf_conn c (ξ @ φ # ξ')"
        and " c = CT ∨ c = CF ∨ c = CVar x"
        then have "ξ @ φ # ξ' = []" by auto
        then have False by auto
        then show "all_subformula_st simple_not_symb (conn c (ξ @ φ' # ξ'))" by blast
      next
        fix φ φ' :: "'v propo" and ca:: "'v connective" and ξ ξ':: "'v propo list"
        and x :: "'v"
        assume rel: "propo_rew_step (push_conn_inside c c') φ φ'"
        and φ_φ': "all_subformula_st simple_not_symb φ ⟹ all_subformula_st simple_not_symb φ'"
        and corr: "wf_conn ca (ξ @ φ # ξ')"
        and n: "all_subformula_st simple_not_symb (conn ca (ξ @ φ # ξ'))"
        and c: "ca = CNot"

        have empty: "ξ = []" "ξ' = []" using c corr by auto
        then have simple_not:"all_subformula_st simple_not_symb (FNot φ)" using corr c n by auto
        then have "simple φ"
          using all_subformula_st_test_symb_true_phi simple_not_symb.simps(1) by blast
        then have "simple φ'"
          using rel simple_propo_rew_step_push_conn_inside_inv by blast
        then show "all_subformula_st simple_not_symb (conn ca (ξ @ φ' # ξ'))" using c empty
          by (metis simple_not φ_φ' append_Nil conn.simps(4) all_subformula_st_decomp_explicit(3)
            simple_not_symb.simps(1))
      next
        fix φ φ' :: "'v propo" and ca :: "'v connective" and ξ ξ' :: "'v propo list"
        and x :: "'v"
        assume rel: "propo_rew_step (push_conn_inside c c') φ φ'"
        and nφ: "all_subformula_st simple_not_symb φ ⟹  all_subformula_st simple_not_symb φ'"
        and corr: "wf_conn ca (ξ @ φ # ξ')"
        and n: "all_subformula_st simple_not_symb (conn ca (ξ @ φ # ξ'))"
        and c: "ca ∈ binary_connectives"

        have "all_subformula_st simple_not_symb φ"
          using n c corr all_subformula_st_decomp by fastforce
        then have φ': " all_subformula_st simple_not_symb φ'" using nφ by blast
        obtain a b where ab: "[a, b] = (ξ @ φ # ξ')"
          using corr c list_length2_decomp wf_conn_bin_list_length by metis
        then have "ξ @ φ' # ξ' = [a, φ'] ∨ (ξ @ φ' # ξ') = [φ', b]"
          using ab by (metis (no_types, opaque_lifting) append_Cons append_Nil append_Nil2
            append_is_Nil_conv butlast.simps(2) butlast_append list.sel(3) tl_append2)
        moreover
        {
           fix χ :: "'v propo"
           have wf': "wf_conn ca [a, b]"
             using ab corr by presburger
           have "all_subformula_st simple_not_symb (conn ca [a, b])"
             using ab n by presburger
           then have "all_subformula_st simple_not_symb χ ∨ χ ∉ set (ξ @ φ' # ξ')"
             using wf' by (metis (no_types) φ' all_subformula_st_decomp calculation insert_iff
               list.set(2))
        }
        then have "∀φ. φ ∈ set (ξ @ φ' # ξ') ⟶ all_subformula_st simple_not_symb φ"
            by (metis (no_types))

        moreover have "simple_not_symb (conn ca (ξ @ φ' # ξ'))"
          using ab conn_inj_not(1) corr wf_conn_list_decomp(4) wf_conn_no_arity_change
            not_Cons_self2 self_append_conv2 simple_not_symb.elims(3) by (metis (no_types) c
            calculation(1) wf_conn_binary)
        moreover have "wf_conn ca (ξ @ φ' # ξ')" using c calculation(1) by auto
        ultimately show "all_subformula_st simple_not_symb (conn ca (ξ @ φ' # ξ'))"
          by (metis all_subformula_st_decomp_imp)
      qed
  }
  moreover {
     fix ca :: "'v connective" and ξ ξ' :: "'v propo list" and φ φ' :: "'v propo"
     have "propo_rew_step (push_conn_inside c c') φ φ' ⟹ wf_conn ca (ξ @ φ # ξ')
       ⟹ simple_not_symb (conn ca (ξ @ φ # ξ')) ⟹ simple_not_symb φ'
       ⟹ simple_not_symb (conn ca (ξ @ φ' # ξ'))"
       by (metis append_self_conv2 conn.simps(4) conn_inj_not(1) simple_not_symb.elims(3)
         simple_not_symb.simps(1) simple_propo_rew_step_push_conn_inside_inv
         wf_conn_no_arity_change_helper wf_conn_list_decomp(4) wf_conn_no_arity_change)
  }
  ultimately show "simple_not ψ"
    using full_propo_rew_step_inv_stay'[of "push_conn_inside c c'" "simple_not_symb"] assms
    unfolding no_T_F_except_top_level_def simple_not_def full_unfold by metis
next
  {
    fix φ ψ :: "'v propo"
    have H: "propo_rew_step (push_conn_inside c c') φ ψ ⟹ no_T_F_except_top_level φ
      ⟹  no_T_F_except_top_level ψ"
      proof -
        assume rel: "propo_rew_step (push_conn_inside c c') φ ψ"
        and "no_T_F_except_top_level φ"
        then have "no_T_F φ ∨ φ = FF ∨ φ = FT"
          by (metis no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb)
        moreover {
          assume "φ = FF ∨ φ = FT"
          then have False using rel propo_rew_step_push_conn_inside by blast
          then have "no_T_F_except_top_level ψ" by blast
        }
        moreover {
          assume "no_T_F φ ∧ φ ≠ FF ∧ φ ≠ FT"
          then have "no_T_F ψ" using rel push_conn_insidec_in_c'_symb_no_T_F by blast
          then have "no_T_F_except_top_level ψ" using no_T_F_no_T_F_except_top_level by blast
        }
        ultimately show "no_T_F_except_top_level ψ" by blast
      qed
  }
  moreover {
     fix ca :: "'v connective" and ξ ξ' :: "'v propo list" and φ φ' :: "'v propo"
     assume rel: "propo_rew_step (push_conn_inside c c') φ φ'"
     assume corr: "wf_conn ca (ξ @ φ # ξ')"
     then have c: "ca ≠ CT ∧ ca ≠ CF" by auto
     assume no_T_F: "no_T_F_symb_except_toplevel (conn ca (ξ @ φ # ξ'))"
     have "no_T_F_symb_except_toplevel (conn ca (ξ @ φ' # ξ'))"
     proof
       have c: "ca ≠ CT ∧ ca ≠ CF" using corr by auto
       have ζ: "∀ζ∈ set (ξ @ φ # ξ'). ζ≠FT ∧ ζ ≠ FF"
         using corr no_T_F no_T_F_symb_except_toplevel_if_is_a_true_false by blast
       then have "φ ≠ FT ∧ φ ≠ FF" by auto
       from rel this have "φ' ≠ FT ∧ φ' ≠ FF"
         apply (induct rule: propo_rew_step.induct)
         by (metis append_is_Nil_conv conn.simps(2) conn_inj list.distinct(1)
           wf_conn_helper_facts(3) wf_conn_list(1) wf_conn_no_arity_change
           wf_conn_no_arity_change_helper push_conn_inside_not_true_false)+
       then have "∀ζ ∈ set (ξ @ φ' # ξ'). ζ ≠ FT ∧ ζ ≠ FF" using ζ by auto
       moreover have "wf_conn ca (ξ @ φ' # ξ')"
         using corr wf_conn_no_arity_change by (metis wf_conn_no_arity_change_helper)
       ultimately show "no_T_F_symb (conn ca (ξ @ φ' # ξ'))" using no_T_F_symb.intros c by metis
     qed
  }
  ultimately show "no_T_F_except_top_level ψ"
    using full_propo_rew_step_inv_stay'[of "push_conn_inside c c'" "no_T_F_symb_except_toplevel"]
    assms unfolding no_T_F_except_top_level_def full_unfold by metis

next
  {
    fix φ ψ :: "'v propo"
    have H: "push_conn_inside c c' φ ψ ⟹ no_equiv φ ⟹ no_equiv ψ"
      by (induct φ ψ rule: push_conn_inside.induct, auto)
  }
  then show "no_equiv ψ"
    using full_propo_rew_step_inv_stay_conn[of "push_conn_inside c c'" no_equiv_symb] assms
    no_equiv_symb_conn_characterization unfolding no_equiv_def by metis

next
  {
    fix φ ψ :: "'v propo"
    have H: "push_conn_inside c c' φ ψ ⟹ no_imp φ ⟹  no_imp ψ"
      by (induct φ ψ rule: push_conn_inside.induct, auto)
  }
  then show "no_imp ψ"
    using full_propo_rew_step_inv_stay_conn[of "push_conn_inside c c'" no_imp_symb] assms
    no_imp_symb_conn_characterization unfolding no_imp_def by metis
qed


lemma push_conn_inside_full_propo_rew_step:
  fixes φ ψ :: "'v propo"
  assumes
    "no_equiv φ" and
    "no_imp φ" and
    "full (propo_rew_step (push_conn_inside c c')) φ ψ" and
    "no_T_F_except_top_level φ" and
    "simple_not φ" and
    "c = CAnd ∨ c = COr" and
    "c' = CAnd ∨ c' = COr"
  shows "c_in_c'_only c c' ψ"
  using c_in_c'_symb_rew assms full_propo_rew_step_subformula by blast


subsubsection ‹Only one type of connective in the formula (+ not)›
inductive only_c_inside_symb :: "'v connective ⇒ 'v propo ⇒ bool" for c :: "'v connective" where
simple_only_c_inside[simp]: "simple φ ⟹  only_c_inside_symb c φ" |
simple_cnot_only_c_inside[simp]: "simple φ ⟹  only_c_inside_symb c (FNot φ)" |
only_c_inside_into_only_c_inside: "wf_conn c l ⟹ only_c_inside_symb c (conn c l)"


lemma only_c_inside_symb_simp[simp]:
  "only_c_inside_symb c FF" "only_c_inside_symb c FT" "only_c_inside_symb c (FVar x)" by auto


definition only_c_inside where "only_c_inside c = all_subformula_st (only_c_inside_symb c)"

lemma only_c_inside_symb_decomp:
  "only_c_inside_symb c ψ ⟷ (simple ψ
                                ∨ (∃ φ'. ψ = FNot φ' ∧ simple φ')
                                ∨ (∃l. ψ = conn c l ∧ wf_conn c l))"
  by (auto simp: only_c_inside_symb.intros(3)) (induct rule: only_c_inside_symb.induct, auto)

lemma only_c_inside_symb_decomp_not[simp]:
  fixes c :: "'v connective"
  assumes c: "c ≠ CNot"
  shows "only_c_inside_symb c (FNot ψ) ⟷ simple ψ"
  apply (auto simp: only_c_inside_symb.intros(3))
  by (induct "FNot ψ" rule: only_c_inside_symb.induct, auto simp: wf_conn_list(8) c)

lemma only_c_inside_decomp_not[simp]:
  assumes c: "c ≠ CNot"
  shows "only_c_inside c (FNot ψ) ⟷ simple ψ"
  by (metis (no_types, opaque_lifting) all_subformula_st_def all_subformula_st_test_symb_true_phi c
    only_c_inside_def only_c_inside_symb_decomp_not simple_only_c_inside
    subformula_conn_decomp_simple)


lemma only_c_inside_decomp:
  "only_c_inside c φ ⟷
    (∀ψ. ψ ≼ φ ⟶ (simple ψ ∨ (∃ φ'. ψ = FNot φ' ∧ simple φ')
                    ∨ (∃l. ψ = conn c l ∧ wf_conn c l)))"
  unfolding only_c_inside_def by (auto simp: all_subformula_st_def only_c_inside_symb_decomp)

lemma only_c_inside_c_c'_false:
  fixes c c' :: "'v connective" and l :: "'v propo list" and φ :: "'v propo"
  assumes cc': "c ≠ c'" and c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
  and only: "only_c_inside c φ" and incl: "conn c' l ≼ φ" and wf: "wf_conn c' l"
  shows False
proof -
  let ?ψ = "conn c' l"
  have "simple ?ψ ∨ (∃ φ'. ?ψ = FNot φ' ∧ simple φ') ∨ (∃l. ?ψ = conn c l ∧ wf_conn c l)"
    using only_c_inside_decomp only incl by blast
  moreover have "¬ simple ?ψ"
    using wf simple_decomp by (metis c' connective.distinct(19) connective.distinct(7,9,21,29,31)
      wf_conn_list(1-3))
  moreover
    {
      fix φ'
      have "?ψ ≠ FNot φ'" using c' conn_inj_not(1) wf by blast
    }
  ultimately obtain l :: "'v propo list" where "?ψ = conn c l ∧ wf_conn c l" by metis
  then have "c = c'" using conn_inj wf by metis
  then show False using cc' by auto
qed

lemma only_c_inside_implies_c_in_c'_symb:
  assumes δ: "c ≠ c'" and c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
  shows "only_c_inside c φ ⟹ c_in_c'_symb c c' φ"
  apply (rule ccontr)
  apply (cases rule: not_c_in_c'_symb.cases, auto)
  by (metis δ c c' connective.distinct(37,39) list.distinct(1) only_c_inside_c_c'_false
    subformula_in_binary_conn(1,2) wf_conn.simps)+

lemma c_in_c'_symb_decomp_level1:
  fixes l :: "'v propo list" and c c' ca :: "'v connective"
  shows "wf_conn ca l ⟹ ca ≠ c ⟹ c_in_c'_symb c c' (conn ca l)"
proof -
  have "not_c_in_c'_symb c c' (conn ca l) ⟹  wf_conn ca l ⟹ ca = c"
    by (induct "conn ca l" rule: not_c_in_c'_symb.induct, auto simp: conn_inj)
  then show "wf_conn ca l ⟹ ca ≠ c ⟹ c_in_c'_symb c c' (conn ca l)" by blast
qed


lemma only_c_inside_implies_c_in_c'_only:
  assumes δ: "c ≠ c'" and c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr"
  shows "only_c_inside c φ ⟹ c_in_c'_only c c' φ"
  unfolding c_in_c'_only_def all_subformula_st_def
  using only_c_inside_implies_c_in_c'_symb
    by (metis all_subformula_st_def assms(1) c c' only_c_inside_def subformula_trans)


lemma c_in_c'_symb_c_implies_only_c_inside:
  assumes δ: "c = CAnd ∨ c = COr" "c' = CAnd ∨ c' = COr" "c ≠ c'" and wf: "wf_conn c [φ, ψ]"
  and inv: "no_equiv (conn c l)" "no_imp (conn c l)" "simple_not (conn c l)"
  shows "wf_conn c l ⟹ c_in_c'_only c c' (conn c l) ⟹ (∀ψ∈ set l. only_c_inside c ψ)"
using inv
proof (induct "conn c l" arbitrary: l rule: propo_induct_arity)
  case (nullary x)
  then show ?case by (auto simp: wf_conn_list assms)
next
  case (unary φ la)
  then have "c = CNot ∧ la = [φ]" by (metis (no_types) wf_conn_list(8))
  then show ?case using assms(2) assms(1) by blast
next
  case (binary φ1 φ2)
  note IHφ1 = this(1) and IHφ2 = this(2) and φ = this(3) and only = this(5) and wf = this(4)
    and no_equiv = this(6) and no_imp = this(7) and simple_not = this(8)
  then have l: "l = [φ1, φ2]" by (meson wf_conn_list(4-7))
  let ?φ = "conn c l"

  obtain c1 l1 c2 l2 where φ1: "φ1 = conn c1 l1" and wfφ1: "wf_conn c1 l1"
    and φ2: "φ2 = conn c2 l2" and wfφ2: "wf_conn c2 l2" using exists_c_conn by metis
  then have c_in_onlyφ1: "c_in_c'_only c c' (conn c1 l1)" and "c_in_c'_only c c' (conn c2 l2)"
    using only l unfolding c_in_c'_only_def using assms(1) by auto
  have incφ1: "φ1 ≼ ?φ" and incφ2: "φ2 ≼ ?φ"
    using φ1 φ2 φ local.wf by (metis conn.simps(5-8) helper_fact subformula_in_binary_conn(1,2))+

  have c1_eq: "c1 ≠ CEq" and c2_eq: "c2 ≠ CEq"
    unfolding no_equiv_def using incφ1 incφ2 by (metis φ1 φ2 wfφ1 wfφ2 assms(1) no_equiv
      no_equiv_eq(1) no_equiv_symb.elims(3) no_equiv_symb_conn_characterization wf_conn_list(4,5)
      no_equiv_def subformula_all_subformula_st)+
  have c1_imp: "c1 ≠ CImp" and c2_imp: "c2 ≠ CImp"
    using no_imp by (metis φ1 φ2 all_subformula_st_decomp_explicit_imp(2,3) assms(1)
      conn.simps(5,6) l no_imp_Imp(1) no_imp_symb.elims(3) no_imp_symb_conn_characterization
      wfφ1 wfφ2 all_subformula_st_decomp no_imp_symb_conn_characterization)+
  have c1c: "c1 ≠ c'"
    proof
      assume c1c: "c1 = c'"
      then obtain ξ1 ξ2 where l1: "l1 = [ξ1, ξ2]"
        by (metis assms(2) connective.distinct(37,39) helper_fact wfφ1 wf_conn.simps
          wf_conn_list_decomp(1-3))
      have "c_in_c'_only c c' (conn c [conn c' l1, φ2])" using c1c l only φ1 by auto
      moreover have "not_c_in_c'_symb c c' (conn c [conn c' l1, φ2])"
        using l1 φ1 c1c l local.wf not_c_in_c'_symb_l wfφ1 by blast
      ultimately show False using φ1 c1c l l1 local.wf not_c_in_c'_simp(4) wfφ1 by blast
   qed
  then have "(φ1 = conn c l1 ∧ wf_conn c l1) ∨ (∃ψ1. φ1 = FNot ψ1) ∨ simple φ1"
    by (metis φ1 assms(1-3) c1_eq c1_imp simple.elims(3) wfφ1 wf_conn_list(4) wf_conn_list(5-7))
  moreover {
    assume "φ1 = conn c l1 ∧ wf_conn c l1"
    then have "only_c_inside c φ1"
      by (metis IHφ1 φ1 all_subformula_st_decomp_imp incφ1 no_equiv no_equiv_def no_imp no_imp_def
        c_in_onlyφ1 only_c_inside_def only_c_inside_into_only_c_inside simple_not simple_not_def
        subformula_all_subformula_st)
  }
  moreover {
    assume "∃ψ1. φ1 = FNot ψ1"
    then obtain ψ1 where "φ1 = FNot ψ1" by metis
    then have "only_c_inside c φ1"
      by (metis all_subformula_st_def assms(1) connective.distinct(37,39) incφ1
        only_c_inside_decomp_not simple_not simple_not_def simple_not_symb.simps(1))
  }
  moreover {
    assume "simple φ1"
    then have "only_c_inside c φ1"
      by (metis all_subformula_st_decomp_explicit(3) assms(1) connective.distinct(37,39)
        only_c_inside_decomp_not only_c_inside_def)
  }
  ultimately have only_c_insideφ1: "only_c_inside c φ1" by metis

  have c_in_onlyφ2: "c_in_c'_only c c' (conn c2 l2)"
    using only l φ2 wfφ2 assms unfolding c_in_c'_only_def by auto
  have c2c: "c2 ≠ c'"
    proof
      assume c2c: "c2 = c'"
      then obtain ξ1 ξ2 where l2: "l2 = [ξ1, ξ2]"
       by (metis assms(2) wfφ2 wf_conn.simps connective.distinct(7,9,19,21,29,31,37,39))
      then have "c_in_c'_symb c c' (conn c [φ1, conn c' l2])"
        using c2c l only φ2 all_subformula_st_test_symb_true_phi unfolding c_in_c'_only_def by auto
      moreover have "not_c_in_c'_symb c c' (conn c [φ1, conn c' l2])"
        using assms(1) c2c l2 not_c_in_c'_symb_r wfφ2 wf_conn_helper_facts(5,6) by metis
      ultimately show False by auto
    qed
  then have "(φ2 = conn c l2 ∧ wf_conn c l2) ∨ (∃ψ2. φ2 = FNot ψ2) ∨ simple φ2"
    using c2_eq by (metis φ2 assms(1-3) c2_eq c2_imp simple.elims(3) wfφ2 wf_conn_list(4-7))
  moreover {
    assume "φ2 = conn c l2 ∧ wf_conn c l2"
    then have "only_c_inside c φ2"
      by (metis IHφ2 φ2 all_subformula_st_decomp incφ2 no_equiv no_equiv_def no_imp no_imp_def
        c_in_onlyφ2 only_c_inside_def only_c_inside_into_only_c_inside simple_not simple_not_def
        subformula_all_subformula_st)
  }
  moreover {
    assume "∃ψ2. φ2 = FNot ψ2"
    then obtain ψ2 where "φ2 = FNot ψ2" by metis
    then have "only_c_inside c φ2"
      by (metis all_subformula_st_def assms(1-3) connective.distinct(38,40) incφ2
        only_c_inside_decomp_not simple_not simple_not_def simple_not_symb.simps(1))
  }
  moreover {
    assume "simple φ2"
    then have "only_c_inside c φ2"
      by (metis all_subformula_st_decomp_explicit(3) assms(1) connective.distinct(37,39)
        only_c_inside_decomp_not only_c_inside_def)
  }
  ultimately have only_c_insideφ2: "only_c_inside c φ2" by metis
  show ?case using l only_c_insideφ1 only_c_insideφ2 by auto
qed



subsubsection ‹Push Conjunction›

definition pushConj where "pushConj = push_conn_inside CAnd COr"

lemma pushConj_consistent: "preserve_models pushConj"
  unfolding pushConj_def by (simp add: push_conn_inside_consistent)

definition and_in_or_symb where "and_in_or_symb = c_in_c'_symb CAnd COr"

definition and_in_or_only where
"and_in_or_only = all_subformula_st (c_in_c'_symb CAnd COr)"

lemma pushConj_inv:
  fixes φ ψ :: "'v propo"
  assumes "full (propo_rew_step pushConj) φ ψ"
  and "no_equiv φ" and "no_imp φ" and "no_T_F_except_top_level φ" and "simple_not φ"
  shows "no_equiv ψ" and "no_imp ψ" and "no_T_F_except_top_level ψ" and "simple_not ψ"
  using push_conn_inside_inv assms unfolding pushConj_def by metis+


lemma pushConj_full_propo_rew_step:
  fixes φ ψ :: "'v propo"
  assumes
    "no_equiv φ" and
    "no_imp φ" and
    "full (propo_rew_step pushConj) φ ψ" and
    "no_T_F_except_top_level φ" and
    "simple_not φ"
  shows "and_in_or_only ψ"
  using assms push_conn_inside_full_propo_rew_step
  unfolding pushConj_def and_in_or_only_def c_in_c'_only_def by (metis (no_types))



subsubsection ‹Push Disjunction›
definition pushDisj where "pushDisj = push_conn_inside COr CAnd"

lemma pushDisj_consistent: "preserve_models pushDisj"
  unfolding pushDisj_def by (simp add: push_conn_inside_consistent)

definition or_in_and_symb where "or_in_and_symb = c_in_c'_symb COr CAnd"

definition or_in_and_only where
"or_in_and_only = all_subformula_st (c_in_c'_symb COr CAnd)"


lemma not_or_in_and_only_or_and[simp]:
  "~or_in_and_only (FOr (FAnd ψ1 ψ2) φ')"
  unfolding or_in_and_only_def
  by (metis all_subformula_st_test_symb_true_phi conn.simps(5-6) not_c_in_c'_symb_l
    wf_conn_helper_facts(5) wf_conn_helper_facts(6))

lemma pushDisj_inv:
  fixes φ ψ :: "'v propo"
  assumes "full (propo_rew_step pushDisj) φ ψ"
  and "no_equiv φ" and "no_imp φ" and "no_T_F_except_top_level φ" and "simple_not φ"
  shows "no_equiv ψ" and "no_imp ψ" and "no_T_F_except_top_level ψ" and "simple_not ψ"
  using push_conn_inside_inv assms unfolding pushDisj_def by metis+

lemma pushDisj_full_propo_rew_step:
  fixes φ ψ :: "'v propo"
  assumes
    "no_equiv φ" and
    "no_imp φ" and
    "full (propo_rew_step pushDisj) φ ψ" and
    "no_T_F_except_top_level φ" and
    "simple_not φ"
  shows "or_in_and_only ψ"
  using assms push_conn_inside_full_propo_rew_step
  unfolding pushDisj_def or_in_and_only_def c_in_c'_only_def by (metis (no_types))


section ‹The Full Transformations›

subsection ‹Abstract Definition›

text ‹The normal form is a super group of groups›

inductive grouped_by :: "'a connective ⇒ 'a propo ⇒ bool" for c where
simple_is_grouped[simp]: "simple φ ⟹ grouped_by c φ" |
simple_not_is_grouped[simp]: "simple φ ⟹ grouped_by c (FNot φ)" |
connected_is_group[simp]: "grouped_by c φ ⟹  grouped_by c ψ ⟹ wf_conn c [φ, ψ]
  ⟹ grouped_by c (conn c [φ, ψ])"

lemma simple_clause[simp]:
  "grouped_by c FT"
  "grouped_by c FF"
  "grouped_by c (FVar x)"
  "grouped_by c (FNot FT)"
  "grouped_by c (FNot FF)"
  "grouped_by c (FNot (FVar x))"
  by simp+

lemma only_c_inside_symb_c_eq_c':
  "only_c_inside_symb c (conn c' [φ1, φ2]) ⟹ c' = CAnd ∨ c' = COr ⟹ wf_conn c' [φ1, φ2]
    ⟹ c' = c"
  by (induct "conn c' [φ1, φ2]" rule: only_c_inside_symb.induct, auto simp: conn_inj)


lemma only_c_inside_c_eq_c':
  "only_c_inside c (conn c' [φ1, φ2]) ⟹  c' = CAnd ∨ c' = COr ⟹ wf_conn c' [φ1, φ2] ⟹ c = c'"
  unfolding only_c_inside_def all_subformula_st_def using only_c_inside_symb_c_eq_c' subformula_refl
  by blast

lemma only_c_inside_imp_grouped_by:
  assumes c: "c ≠ CNot" and c': "c' = CAnd ∨ c' = COr"
  shows "only_c_inside c φ ⟹ grouped_by c φ" (is "?O φ ⟹ ?G φ")
proof (induct φ rule: propo_induct_arity)
  case (nullary φ x)
  then show "?G φ" by auto
next
  case (unary ψ)
  then show "?G (FNot ψ)" by (auto simp: c)
next
  case (binary φ φ1 φ2)
  note IHφ1 = this(1) and IHφ2 = this(2) and φ = this(3) and only = this(4)
  have φ_conn: "φ = conn c [φ1, φ2]" and wf: "wf_conn c [φ1, φ2]"
    proof -
      obtain c'' l'' where φ_c'': "φ = conn c'' l''" and wf: "wf_conn c'' l''"
        using exists_c_conn by metis
      then have l'': "l'' = [φ1, φ2]" using φ by (metis wf_conn_list(4-7))
      have "only_c_inside_symb c (conn c'' [φ1, φ2])"
        using only all_subformula_st_test_symb_true_phi
        unfolding only_c_inside_def φ_c'' l'' by metis
      then have "c = c''"
        by (metis φ φ_c'' conn_inj conn_inj_not(2) l'' list.distinct(1) list.inject wf
          only_c_inside_symb.cases simple.simps(5-8))
      then show "φ = conn c [φ1, φ2]" and "wf_conn c [φ1, φ2]" using φ_c'' wf l'' by auto
    qed
  have "grouped_by c φ1" using wf IHφ1 IHφ2 φ_conn only φ unfolding only_c_inside_def by auto
  moreover have "grouped_by c φ2"
    using wf φ IHφ1 IHφ2 φ_conn only unfolding only_c_inside_def by auto
  ultimately show "?G φ" using φ_conn connected_is_group local.wf by blast
qed


lemma grouped_by_false:
  "grouped_by c (conn c' [φ, ψ]) ⟹ c ≠ c' ⟹ wf_conn c' [φ, ψ] ⟹ False"
  apply (induct "conn c' [φ, ψ]" rule: grouped_by.induct)
  apply (auto simp: simple_decomp wf_conn_list, auto simp: conn_inj)
  by (metis list.distinct(1) list.sel(3) wf_conn_list(8))+

text ‹Then the CNF form is a conjunction of clauses: every clause is in CNF form and two formulas in
  CNF form can be related by an and.›
inductive super_grouped_by:: "'a connective ⇒ 'a connective ⇒ 'a propo ⇒ bool" for c c' where
grouped_is_super_grouped[simp]: "grouped_by c φ ⟹ super_grouped_by c c' φ" |
connected_is_super_group: "super_grouped_by c c' φ ⟹ super_grouped_by c c' ψ ⟹ wf_conn c [φ, ψ]
  ⟹ super_grouped_by c c' (conn c' [φ, ψ])"

lemma simple_cnf[simp]:
  "super_grouped_by c c' FT"
  "super_grouped_by c c' FF"
  "super_grouped_by c c' (FVar x)"
  "super_grouped_by c c' (FNot FT)"
  "super_grouped_by c c' (FNot FF)"
  "super_grouped_by c c' (FNot (FVar x))"
  by auto

lemma c_in_c'_only_super_grouped_by:
  assumes c: "c = CAnd ∨ c = COr" and c': "c' = CAnd ∨ c' = COr" and cc': "c ≠ c'"
  shows "no_equiv φ ⟹ no_imp φ ⟹ simple_not φ ⟹ c_in_c'_only c c' φ
    ⟹ super_grouped_by c c' φ"
    (is "?NE φ ⟹ ?NI φ ⟹ ?SN φ ⟹ ?C φ ⟹ ?S φ")
proof (induct φ rule: propo_induct_arity)
  case (nullary φ x)
  then show "?S φ" by auto
next
  case (unary φ)
  then have "simple_not_symb (FNot φ)"
    using all_subformula_st_test_symb_true_phi unfolding simple_not_def by blast
  then have "φ = FT ∨ φ = FF ∨ (∃ x. φ = FVar x)" by (cases φ, auto)
  then show "?S (FNot φ)" by auto
next
  case (binary φ φ1 φ2)
  note IHφ1 = this(1) and IHφ2 = this(2) and no_equiv = this(4) and no_imp = this(5)
    and simpleN = this(6) and c_in_c'_only = this(7) and φ' = this(3)
  {
    assume "φ = FImp φ1 φ2 ∨ φ = FEq φ1 φ2"
    then have False using no_equiv no_imp by auto
    then have "?S φ" by auto
  }
  moreover {
    assume φ: "φ = conn c' [φ1, φ2] ∧ wf_conn c' [φ1, φ2]"
    have c_in_c'_only: "c_in_c'_only c c' φ1 ∧ c_in_c'_only c c' φ2 ∧ c_in_c'_symb c c' φ"
      using c_in_c'_only φ' unfolding c_in_c'_only_def by auto
    have "super_grouped_by c c' φ1" using φ c' no_equiv no_imp simpleN IHφ1 c_in_c'_only by auto
    moreover have "super_grouped_by c c' φ2"
      using φ c' no_equiv no_imp simpleN IHφ2 c_in_c'_only by auto
    ultimately have "?S φ"
      using super_grouped_by.intros(2) φ by (metis c wf_conn_helper_facts(5,6))
  }
  moreover {
    assume φ: "φ = conn c [φ1, φ2] ∧ wf_conn c [φ1, φ2]"
    then have "only_c_inside c φ1 ∧ only_c_inside c φ2"
      using c_in_c'_symb_c_implies_only_c_inside c c' c_in_c'_only list.set_intros(1)
        wf_conn_helper_facts(5,6)  no_equiv no_imp simpleN last_ConsL last_ConsR last_in_set
        list.distinct(1) by (metis (no_types, opaque_lifting) cc')
    then have "only_c_inside c (conn c [φ1, φ2])"
      unfolding only_c_inside_def using φ
      by (simp add: only_c_inside_into_only_c_inside all_subformula_st_decomp)
    then have "grouped_by c φ" using φ only_c_inside_imp_grouped_by c by blast
    then have "?S φ" using super_grouped_by.intros(1) by metis
  }
  ultimately show "?S φ" by (metis φ' c c' cc' conn.simps(5,6) wf_conn_helper_facts(5,6))
qed


subsection ‹Conjunctive Normal Form›

subsubsection ‹Definition›

definition is_conj_with_TF where "is_conj_with_TF == super_grouped_by COr CAnd"

lemma or_in_and_only_conjunction_in_disj:
  shows "no_equiv φ ⟹ no_imp φ ⟹ simple_not φ ⟹ or_in_and_only φ ⟹ is_conj_with_TF φ"
  using c_in_c'_only_super_grouped_by
  unfolding is_conj_with_TF_def or_in_and_only_def c_in_c'_only_def
  by (simp add: c_in_c'_only_def c_in_c'_only_super_grouped_by)

definition is_cnf where
"is_cnf φ ≡ is_conj_with_TF φ ∧ no_T_F_except_top_level φ"

subsubsection ‹Full CNF transformation›

text ‹The full1 CNF transformation consists simply in chaining all the transformation defined
  before.›
definition cnf_rew where "cnf_rew =
  (full (propo_rew_step elim_equiv)) OO
  (full (propo_rew_step elim_imp)) OO
  (full (propo_rew_step elimTB)) OO
  (full (propo_rew_step pushNeg)) OO
  (full (propo_rew_step pushDisj))"

lemma cnf_rew_equivalent: "preserve_models cnf_rew"
  by (simp add: cnf_rew_def elimEquv_lifted_consistant elim_imp_lifted_consistant elimTB_consistent
    preserve_models_OO pushDisj_consistent pushNeg_lifted_consistant)

(*TODO Redo proof*)
lemma cnf_rew_is_cnf: "cnf_rew φ φ' ⟹ is_cnf φ'"
  apply (unfold cnf_rew_def OO_def)
  apply auto
proof -
  fix φ φEq φImp φTB φNeg φDisj :: "'v propo"
  assume Eq: "full (propo_rew_step elim_equiv) φ φEq"
  then have no_equiv: "no_equiv φEq" using no_equiv_full_propo_rew_step_elim_equiv by blast

  assume Imp: "full (propo_rew_step elim_imp) φEq φImp"
  then have no_imp: "no_imp φImp" using no_imp_full_propo_rew_step_elim_imp by blast
  have no_imp_inv: "no_equiv φImp" using no_equiv Imp elim_imp_inv by blast

  assume TB: "full (propo_rew_step elimTB) φImp φTB"
  then have noTB: "no_T_F_except_top_level φTB"
    using no_imp_inv no_imp elimTB_full_propo_rew_step by blast
  have noTB_inv: "no_equiv φTB" "no_imp φTB" using elimTB_inv TB no_imp no_imp_inv by blast+

  assume Neg: "full (propo_rew_step pushNeg) φTB φNeg"
  then have noNeg: "simple_not φNeg"
    using noTB_inv noTB pushNeg_full_propo_rew_step by blast
  have noNeg_inv: "no_equiv φNeg" "no_imp φNeg" "no_T_F_except_top_level φNeg"
    using pushNeg_inv Neg noTB noTB_inv by blast+

  assume Disj: "full (propo_rew_step pushDisj) φNeg φDisj"
  then have no_Disj: "or_in_and_only φDisj"
    using noNeg_inv noNeg pushDisj_full_propo_rew_step by blast
  have noDisj_inv: "no_equiv φDisj" "no_imp φDisj" "no_T_F_except_top_level φDisj"
    "simple_not φDisj"
  using pushDisj_inv Disj noNeg noNeg_inv by blast+

  moreover have "is_conj_with_TF φDisj"
    using or_in_and_only_conjunction_in_disj noDisj_inv no_Disj by blast
  ultimately show "is_cnf φDisj" unfolding is_cnf_def by blast
qed

subsection ‹Disjunctive Normal Form›

subsubsection ‹Definition›

definition is_disj_with_TF where "is_disj_with_TF ≡ super_grouped_by CAnd COr"

lemma and_in_or_only_conjunction_in_disj:
  shows "no_equiv φ ⟹ no_imp φ ⟹ simple_not φ ⟹ and_in_or_only φ ⟹ is_disj_with_TF φ"
  using c_in_c'_only_super_grouped_by
  unfolding is_disj_with_TF_def and_in_or_only_def c_in_c'_only_def
  by (simp add: c_in_c'_only_def c_in_c'_only_super_grouped_by)

definition is_dnf :: "'a propo ⇒ bool" where
"is_dnf φ ⟷ is_disj_with_TF φ ∧ no_T_F_except_top_level φ"


subsubsection ‹Full DNF transform›

text ‹The full1 DNF transformation consists simply in chaining all the transformation defined
  before.›
definition dnf_rew where "dnf_rew ≡
  (full (propo_rew_step elim_equiv)) OO
  (full (propo_rew_step elim_imp)) OO
  (full (propo_rew_step elimTB)) OO
  (full (propo_rew_step pushNeg)) OO
  (full (propo_rew_step pushConj))"

lemma dnf_rew_consistent: "preserve_models dnf_rew"
  by (simp add: dnf_rew_def elimEquv_lifted_consistant elim_imp_lifted_consistant elimTB_consistent
    preserve_models_OO pushConj_consistent pushNeg_lifted_consistant)

theorem dnf_transformation_correction:
    "dnf_rew φ φ' ⟹ is_dnf φ'"
  apply (unfold dnf_rew_def OO_def)
  by (meson and_in_or_only_conjunction_in_disj elimTB_full_propo_rew_step elimTB_inv(1,2)
    elim_imp_inv is_dnf_def no_equiv_full_propo_rew_step_elim_equiv
    no_imp_full_propo_rew_step_elim_imp pushConj_full_propo_rew_step pushConj_inv(1-4)
    pushNeg_full_propo_rew_step pushNeg_inv(1-3))

section ‹More aggressive simplifications: Removing true and false at the beginning›

subsection ‹Transformation›
text ‹We should remove @{term FT} and @{term FF} at the beginning and not in the middle of the
  algorithm. To do this, we have to use more rules (one for each connective):›
inductive elimTBFull where
ElimTBFull1[simp]: "elimTBFull (FAnd φ FT) φ" |
ElimTBFull1'[simp]: "elimTBFull (FAnd FT φ) φ" |

ElimTBFull2[simp]: "elimTBFull (FAnd φ FF) FF" |
ElimTBFull2'[simp]: "elimTBFull (FAnd FF φ) FF" |

ElimTBFull3[simp]: "elimTBFull (FOr φ FT) FT" |
ElimTBFull3'[simp]: "elimTBFull (FOr FT φ) FT" |

ElimTBFull4[simp]: "elimTBFull (FOr φ FF) φ" |
ElimTBFull4'[simp]: "elimTBFull (FOr FF φ) φ" |

ElimTBFull5[simp]: "elimTBFull (FNot FT) FF" |
ElimTBFull5'[simp]: "elimTBFull (FNot FF) FT" |

ElimTBFull6_l[simp]: "elimTBFull (FImp FT φ) φ" |
ElimTBFull6_l'[simp]: "elimTBFull (FImp FF φ) FT" |
ElimTBFull6_r[simp]: "elimTBFull (FImp φ FT) FT" |
ElimTBFull6_r'[simp]: "elimTBFull (FImp φ FF) (FNot φ)" |

ElimTBFull7_l[simp]: "elimTBFull (FEq FT φ) φ" |
ElimTBFull7_l'[simp]: "elimTBFull (FEq FF φ) (FNot φ)" |
ElimTBFull7_r[simp]: "elimTBFull (FEq φ FT) φ" |
ElimTBFull7_r'[simp]: "elimTBFull (FEq φ FF) (FNot φ)"

text ‹The transformation is still consistent.›
lemma elimTBFull_consistent: "preserve_models elimTBFull"
proof -
  {
    fix φ ψ:: "'b propo"
    have "elimTBFull φ ψ ⟹ ∀A. A ⊨ φ ⟷ A ⊨ ψ"
      by (induct_tac rule: elimTBFull.inducts, auto)
  }
  then show ?thesis using preserve_models_def by auto
qed

text ‹Contrary to the theorem @{thm [source] no_T_F_symb_except_toplevel_step_exists}, we do not
  need the assumption @{term "no_equiv φ"} and @{term "no_imp φ"}, since our transformation is
  more general.›
lemma no_T_F_symb_except_toplevel_step_exists':
  fixes φ :: "'v propo"
  shows "ψ ≼ φ ⟹ ¬ no_T_F_symb_except_toplevel ψ ⟹ ∃ψ'. elimTBFull ψ ψ'"
proof (induct ψ rule: propo_induct_arity)
  case (nullary φ')
  then have False using no_T_F_symb_except_toplevel_true no_T_F_symb_except_toplevel_false by auto
  then show "Ex (elimTBFull φ')" by blast
next
  case (unary ψ)
  then have "ψ = FF ∨ ψ = FT" using no_T_F_symb_except_toplevel_not_decom by blast
  then show "Ex (elimTBFull (FNot ψ))" using ElimTBFull5 ElimTBFull5' by blast
next
  case (binary φ' ψ1 ψ2)
  then have "ψ1 = FT ∨ ψ2 = FT ∨ ψ1 = FF ∨ ψ2 = FF"
    by (metis binary_connectives_def conn.simps(5-8) insertI1 insert_commute
      no_T_F_symb_except_toplevel_bin_decom binary.hyps(3))
  then show "Ex (elimTBFull φ')" using elimTBFull.intros binary.hyps(3)  by blast
qed

text ‹The same applies here. We do not need the assumption, but the deep link between
  @{term "¬ no_T_F_except_top_level φ"} and the existence of a rewriting step, still exists.›
lemma no_T_F_except_top_level_rew':
  fixes φ :: "'v propo"
  assumes noTB: "¬ no_T_F_except_top_level φ"
  shows "∃ψ ψ'. ψ ≼ φ ∧ elimTBFull ψ ψ'"
proof -
  have test_symb_false_nullary:
    "∀x. no_T_F_symb_except_toplevel (FF:: 'v propo) ∧ no_T_F_symb_except_toplevel FT
      ∧ no_T_F_symb_except_toplevel (FVar (x:: 'v))"
    by auto
  moreover {
    fix c:: "'v connective" and l :: "'v propo list" and ψ :: "'v propo"
    have H: "elimTBFull (conn c l) ψ ⟹ ¬no_T_F_symb_except_toplevel (conn c l)"
      by (cases "conn c l" rule: elimTBFull.cases) auto
  }
  ultimately show ?thesis
    using no_test_symb_step_exists[of no_T_F_symb_except_toplevel φ elimTBFull] noTB
    no_T_F_symb_except_toplevel_step_exists' unfolding no_T_F_except_top_level_def by metis
qed



lemma elimTBFull_full_propo_rew_step:
  fixes φ ψ :: "'v propo"
  assumes "full (propo_rew_step elimTBFull) φ ψ"
  shows "no_T_F_except_top_level ψ"
  using full_propo_rew_step_subformula no_T_F_except_top_level_rew' assms by fastforce

subsection ‹More invariants›
text ‹As the aim is to use the transformation as the first transformation, we have to show some more
  invariants for @{term elim_equiv} and @{term elim_imp}. For the other transformation, we have
  already proven it.›
lemma propo_rew_step_ElimEquiv_no_T_F: "propo_rew_step elim_equiv φ ψ ⟹ no_T_F φ ⟹  no_T_F ψ"
proof (induct rule: propo_rew_step.induct)
  fix φ' :: "'v propo" and ψ' :: "'v propo"
  assume a1: "no_T_F φ'"
  assume a2: "elim_equiv φ' ψ'"
  have "∀x0 x1. (¬ elim_equiv (x1 :: 'v propo) x0 ∨ (∃v2 v3 v4 v5 v6 v7. x1 = FEq v2 v3
    ∧ x0 = FAnd (FImp v4 v5) (FImp v6 v7) ∧ v2 = v4 ∧ v4 = v7 ∧ v3 = v5 ∧ v3 = v6))
 = (¬ elim_equiv x1 x0 ∨ (∃v2 v3 v4 v5 v6 v7. x1 = FEq v2 v3
    ∧ x0 = FAnd (FImp v4 v5) (FImp v6 v7) ∧ v2 = v4 ∧ v4 = v7 ∧ v3 = v5 ∧ v3 = v6))"
    by meson
  then have "∀p pa. ¬ elim_equiv (p :: 'v propo) pa ∨ (∃pb pc pd pe pf pg. p = FEq pb pc
    ∧ pa = FAnd (FImp pd pe) (FImp pf pg) ∧ pb = pd ∧ pd = pg ∧ pc = pe ∧ pc = pf)"
    using elim_equiv.cases by force
  then show "no_T_F ψ'" using a1 a2 by fastforce
next
  fix φ φ' :: "'v propo" and ξ ξ' :: "'v propo list" and c :: "'v connective"
  assume rel: "propo_rew_step elim_equiv φ φ'"
  and IH: "no_T_F φ ⟹ no_T_F φ'"
  and corr: "wf_conn c (ξ @ φ # ξ')"
  and no_T_F: "no_T_F (conn c (ξ @ φ # ξ'))"
  {
    assume c: "c = CNot"
    then have empty: "ξ = []" "ξ' = []" using corr by auto
    then have "no_T_F φ" using no_T_F c no_T_F_decomp_not by auto
    then have "no_T_F (conn c (ξ @ φ' # ξ'))" using c empty no_T_F_comp_not IH by auto
  }
  moreover {
    assume c: "c ∈ binary_connectives"
    obtain a b where ab: "ξ @ φ # ξ' = [a, b]"
      using corr c list_length2_decomp wf_conn_bin_list_length by metis
    then have φ: "φ = a ∨ φ = b"
      by (metis append.simps(1) append_is_Nil_conv list.distinct(1) list.sel(3) nth_Cons_0
        tl_append2)
    have ζ: "∀ζ∈ set (ξ @ φ # ξ'). no_T_F ζ"
      using no_T_F unfolding no_T_F_def using corr all_subformula_st_decomp by blast

    then have φ': "no_T_F φ'" using ab IH φ by auto
    have l': "ξ @ φ' # ξ' = [φ', b] ∨ ξ @ φ' # ξ' = [a, φ']"
      by (metis (no_types, opaque_lifting) ab append_Cons append_Nil append_Nil2 butlast.simps(2)
        butlast_append list.distinct(1) list.sel(3))
    then have "∀ζ ∈ set (ξ @ φ' # ξ'). no_T_F ζ" using ζ φ' ab by fastforce
    moreover
      have "∀ζ ∈ set (ξ @ φ # ξ'). ζ ≠ FT ∧ ζ ≠ FF"
        using ζ corr no_T_F no_T_F_except_top_level_false no_T_F_no_T_F_except_top_level by blast
      then have "no_T_F_symb (conn c (ξ @ φ' # ξ'))"
        by (metis φ' l' ab all_subformula_st_test_symb_true_phi c list.distinct(1)
          list.set_intros(1,2) no_T_F_symb_except_toplevel_bin_decom
          no_T_F_symb_except_toplevel_no_T_F_symb no_T_F_symb_false(1,2) no_T_F_def wf_conn_binary
          wf_conn_list(1,2))
    ultimately have "no_T_F (conn c (ξ @ φ' # ξ'))"
      by (metis l' all_subformula_st_decomp_imp c no_T_F_def wf_conn_binary)
  }
  moreover {
     fix x
     assume "c = CVar x ∨ c = CF ∨ c = CT"
     then have False using corr by auto
     then have "no_T_F (conn c (ξ @ φ' # ξ'))" by auto
  }
  ultimately show "no_T_F (conn c (ξ @ φ' # ξ'))" using corr wf_conn.cases by metis
qed

lemma elim_equiv_inv':
  fixes φ ψ :: "'v propo"
  assumes "full (propo_rew_step elim_equiv) φ ψ" and "no_T_F_except_top_level φ"
  shows "no_T_F_except_top_level ψ"
proof -
  {
    fix φ ψ :: "'v propo"
    have "propo_rew_step elim_equiv φ ψ ⟹ no_T_F_except_top_level φ
      ⟹ no_T_F_except_top_level ψ"
      proof -
        assume rel: "propo_rew_step elim_equiv φ ψ"
        and no: "no_T_F_except_top_level φ"
        {
          assume "φ = FT ∨ φ = FF"
          from rel this have False
            apply (induct rule: propo_rew_step.induct, auto simp: wf_conn_list(1,2))
            using elim_equiv.simps by blast+
          then have "no_T_F_except_top_level ψ" by blast
        }
        moreover {
          assume "φ ≠ FT ∧ φ ≠ FF"
          then have "no_T_F φ"
            by (metis no no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb)
          then have "no_T_F ψ" using propo_rew_step_ElimEquiv_no_T_F rel by blast
          then have "no_T_F_except_top_level ψ" by (simp add: no_T_F_no_T_F_except_top_level)
        }
        ultimately show "no_T_F_except_top_level ψ" by metis
      qed
  }
  moreover {
     fix c :: "'v connective" and ξ ξ' :: "'v propo list" and ζ ζ' :: "'v propo"
     assume rel: "propo_rew_step elim_equiv ζ ζ'"
     and incl: "ζ ≼ φ"
     and corr: "wf_conn c (ξ @ ζ # ξ')"
     and no_T_F: "no_T_F_symb_except_toplevel (conn c (ξ @ ζ # ξ'))"
     and n: "no_T_F_symb_except_toplevel ζ'"
     have "no_T_F_symb_except_toplevel (conn c (ξ @ ζ' # ξ'))"
     proof
       have p: "no_T_F_symb (conn c (ξ @ ζ # ξ'))"
         using corr wf_conn_list(1) wf_conn_list(2) no_T_F_symb_except_toplevel_no_T_F_symb no_T_F
         by blast
       have l: "∀φ∈set (ξ @ ζ # ξ'). φ ≠ FT ∧ φ ≠ FF"
         using corr wf_conn_no_T_F_symb_iff p by blast
       from rel incl have "ζ'≠FT ∧ζ'≠FF"
         apply (induction ζ ζ' rule: propo_rew_step.induct)
         apply (cases rule: elim_equiv.cases, auto simp: elim_equiv.simps)
         by (metis append_is_Nil_conv list.distinct wf_conn_list(1,2) wf_conn_no_arity_change
           wf_conn_no_arity_change_helper)+
       then have "∀φ ∈ set (ξ @ ζ' # ξ'). φ ≠ FT ∧ φ ≠ FF" using l by auto
       moreover have "c ≠ CT ∧ c ≠ CF" using corr by auto
       ultimately show "no_T_F_symb (conn c (ξ @ ζ' # ξ'))"
         by (metis corr wf_conn_no_arity_change wf_conn_no_arity_change_helper no_T_F_symb_comp)
     qed
  }
  ultimately show "no_T_F_except_top_level ψ"
    using full_propo_rew_step_inv_stay_with_inc[of "elim_equiv" "no_T_F_symb_except_toplevel" "φ"]
      assms subformula_refl unfolding no_T_F_except_top_level_def by metis
qed


lemma propo_rew_step_ElimImp_no_T_F: "propo_rew_step elim_imp φ ψ ⟹ no_T_F φ ⟹  no_T_F ψ"
proof (induct rule: propo_rew_step.induct)
  case (global_rel φ' ψ')
  then show "no_T_F ψ'"
    using elim_imp.cases no_T_F_comp_not no_T_F_decomp(1,2)
    by (metis no_T_F_comp_expanded_explicit(2))
next
  case (propo_rew_one_step_lift φ φ' c ξ ξ')
  note rel = this(1) and IH = this(2) and corr = this(3) and no_T_F = this(4)
  {
    assume c: "c = CNot"
    then have empty: "ξ = []" "ξ' = []" using corr by auto
    then have "no_T_F φ" using no_T_F c no_T_F_decomp_not by auto
    then have "no_T_F (conn c (ξ @ φ' # ξ'))" using c empty no_T_F_comp_not IH by auto
  }
  moreover {
    assume c: "c ∈ binary_connectives"
    then obtain a b where ab: "ξ @ φ # ξ' = [a, b]"
      using corr list_length2_decomp wf_conn_bin_list_length by metis
    then have φ: "φ = a ∨ φ = b"
      by (metis append_self_conv2 wf_conn_list_decomp(4) wf_conn_unary list.discI list.sel(3)
        nth_Cons_0 tl_append2)
    have ζ: "∀ζ ∈ set (ξ @ φ # ξ'). no_T_F ζ" using ab c propo_rew_one_step_lift.prems by auto

    then have φ': "no_T_F φ'"
      using ab IH φ corr no_T_F no_T_F_def all_subformula_st_decomp_explicit by auto
    have χ: "ξ @ φ' # ξ' = [φ', b] ∨ ξ @ φ' # ξ' = [a, φ']"
      by (metis (no_types, opaque_lifting) ab append_Cons append_Nil append_Nil2 butlast.simps(2)
        butlast_append list.distinct(1) list.sel(3))
    then have "∀ζ∈ set (ξ @ φ' # ξ'). no_T_F ζ" using ζ φ' ab by fastforce
    moreover
      have "no_T_F (last (ξ @ φ' # ξ'))" by (simp add: calculation)
      then have "no_T_F_symb (conn c (ξ @ φ' # ξ'))"
        by (metis χ φ' ζ ab all_subformula_st_test_symb_true_phi c last.simps list.distinct(1)
          list.set_intros(1) no_T_F_bin_decomp no_T_F_def)
    ultimately have "no_T_F (conn c (ξ @ φ' # ξ'))" using c χ by fastforce
  }
  moreover {
    fix x
    assume "c = CVar x ∨ c = CF ∨ c = CT"
    then have False using corr by auto
    then have "no_T_F (conn c (ξ @ φ' # ξ'))" by auto
  }
  ultimately show "no_T_F (conn c (ξ @ φ' # ξ'))" using corr wf_conn.cases by blast
qed


lemma elim_imp_inv':
  fixes φ ψ :: "'v propo"
  assumes "full (propo_rew_step elim_imp) φ ψ" and "no_T_F_except_top_level φ"
  shows"no_T_F_except_top_level ψ"
proof -
  {
    {
      fix φ ψ :: "'v propo"
      have H: "elim_imp φ ψ ⟹ no_T_F_except_top_level φ ⟹  no_T_F_except_top_level ψ"
        by (induct φ ψ rule: elim_imp.induct, auto)
    } note H = this
    fix φ ψ :: "'v propo"
    have "propo_rew_step elim_imp φ ψ ⟹ no_T_F_except_top_level φ ⟹  no_T_F_except_top_level ψ"
      proof -
        assume rel: "propo_rew_step elim_imp φ ψ"
        and no: "no_T_F_except_top_level φ"
        {
          assume "φ = FT ∨ φ = FF"
          from rel this have False
            apply (induct rule: propo_rew_step.induct)
            by (cases rule: elim_imp.cases, auto simp: wf_conn_list(1,2))
          then have "no_T_F_except_top_level ψ" by blast
        }
        moreover {
          assume "φ ≠ FT ∧ φ ≠ FF"
          then have "no_T_F φ"
            by (metis no no_T_F_symb_except_toplevel_all_subformula_st_no_T_F_symb)
          then have "no_T_F ψ"
            using rel propo_rew_step_ElimImp_no_T_F by blast
          then have "no_T_F_except_top_level ψ" by (simp add: no_T_F_no_T_F_except_top_level)
        }
        ultimately show "no_T_F_except_top_level ψ" by metis
      qed
  }
  moreover {
     fix c :: "'v connective" and ξ ξ' :: "'v propo list" and ζ ζ' :: "'v propo"
     assume rel: "propo_rew_step elim_imp ζ ζ'"
     and incl: "ζ ≼ φ"
     and corr: "wf_conn c (ξ @ ζ # ξ')"
     and no_T_F: "no_T_F_symb_except_toplevel (conn c (ξ @ ζ # ξ'))"
     and n: "no_T_F_symb_except_toplevel ζ'"
     have "no_T_F_symb_except_toplevel (conn c (ξ @ ζ' # ξ'))"
     proof
       have p: "no_T_F_symb (conn c (ξ @ ζ # ξ'))"
         by (simp add: corr no_T_F no_T_F_symb_except_toplevel_no_T_F_symb wf_conn_list(1,2))

       have l: "∀φ∈set (ξ @ ζ # ξ'). φ ≠ FT ∧ φ ≠ FF"
         using corr wf_conn_no_T_F_symb_iff p by blast
       from rel incl have "ζ'≠FT ∧ζ'≠FF"
         apply (induction ζ ζ' rule: propo_rew_step.induct)
         apply (cases rule: elim_imp.cases, auto)
         using wf_conn_list(1,2) wf_conn_no_arity_change wf_conn_no_arity_change_helper
         by (metis append_is_Nil_conv list.distinct(1))+
       then have "∀φ∈set (ξ @ ζ' # ξ'). φ ≠ FT ∧ φ ≠ FF" using l by auto
       moreover have "c ≠ CT ∧ c ≠ CF" using corr by auto
       ultimately show "no_T_F_symb (conn c (ξ @ ζ' # ξ'))"
         using corr wf_conn_no_arity_change no_T_F_symb_comp
         by (metis wf_conn_no_arity_change_helper)
     qed
  }
  ultimately show "no_T_F_except_top_level ψ"
    using full_propo_rew_step_inv_stay_with_inc[of "elim_imp" "no_T_F_symb_except_toplevel" "φ"]
    assms subformula_refl unfolding no_T_F_except_top_level_def by metis
qed


subsection ‹The new CNF and DNF transformation›

text ‹The transformation is the same as before, but the order is not the same.›
definition dnf_rew' :: "'a propo ⇒ 'a propo ⇒ bool" where
"dnf_rew' =
  (full (propo_rew_step elimTBFull)) OO
  (full (propo_rew_step elim_equiv)) OO
  (full (propo_rew_step elim_imp)) OO
  (full (propo_rew_step pushNeg)) OO
  (full (propo_rew_step pushConj))"

lemma dnf_rew'_consistent: "preserve_models dnf_rew'"
  by (simp add: dnf_rew'_def elimEquv_lifted_consistant elim_imp_lifted_consistant
    elimTBFull_consistent preserve_models_OO pushConj_consistent pushNeg_lifted_consistant)

theorem cnf_transformation_correction:
    "dnf_rew' φ φ' ⟹ is_dnf φ'"
  unfolding dnf_rew'_def OO_def
  by (meson and_in_or_only_conjunction_in_disj elimTBFull_full_propo_rew_step elim_equiv_inv'
    elim_imp_inv elim_imp_inv' is_dnf_def no_equiv_full_propo_rew_step_elim_equiv
    no_imp_full_propo_rew_step_elim_imp pushConj_full_propo_rew_step pushConj_inv(1-4)
    pushNeg_full_propo_rew_step pushNeg_inv(1-3))

text ‹Given all the lemmas before the CNF transformation is easy to prove:›
definition cnf_rew' :: "'a propo ⇒ 'a propo ⇒ bool" where
"cnf_rew' =
  (full (propo_rew_step elimTBFull)) OO
  (full (propo_rew_step elim_equiv)) OO
  (full (propo_rew_step elim_imp)) OO
  (full (propo_rew_step pushNeg)) OO
  (full (propo_rew_step pushDisj))"

lemma cnf_rew'_consistent: "preserve_models cnf_rew'"
  by (simp add: cnf_rew'_def elimEquv_lifted_consistant elim_imp_lifted_consistant
    elimTBFull_consistent preserve_models_OO pushDisj_consistent pushNeg_lifted_consistant)

theorem cnf'_transformation_correction:
  "cnf_rew' φ φ' ⟹ is_cnf φ'"
  unfolding cnf_rew'_def OO_def
  by (meson elimTBFull_full_propo_rew_step elim_equiv_inv' elim_imp_inv elim_imp_inv' is_cnf_def
    no_equiv_full_propo_rew_step_elim_equiv no_imp_full_propo_rew_step_elim_imp
    or_in_and_only_conjunction_in_disj pushDisj_full_propo_rew_step pushDisj_inv(1-4)
    pushNeg_full_propo_rew_step pushNeg_inv(1) pushNeg_inv(2) pushNeg_inv(3))

end