Theory Formula

theory Formula
imports Trs_Impl Sorted_Algebra
(*
Author:  Sebastiaan Joosten (2016-2017)
Author:  René Thiemann (2016-2017)
Author:  Akihisa Yamada (2016-2017)
License: LGPL (see file COPYING.LESSER)
*)
theory Formula
imports
  "Abstract-Rewriting.Abstract_Rewriting"
  TRS.Trs_Impl
  First_Order_Terms.Option_Monad
  Sorted_Algebra
begin

type_synonym ('v,'t,'d) valuation = "'v × 't ⇒ 'd"

datatype 'a formula =
  Atom "'a"
| NegAtom "'a"
| Conjunction "'a formula list"
| Disjunction "'a formula list"

syntax "_list_all" :: "pttrn ⇒ 'a list ⇒ 'b ⇒ 'b"    ("(3⋀f _←_. _)" [0, 51, 10] 10)
translations "⋀f x←xs. b"  "CONST Conjunction (CONST map (λx. b) xs)"

syntax "_list_exists" :: "pttrn ⇒ 'a list ⇒ 'b ⇒ 'b"    ("(3⋁f _←_. _)" [0, 51, 10] 10)
translations "⋁f x←xs. b"  "CONST Disjunction (CONST map (λx. b) xs)"

instantiation formula :: (showl) showl
begin
fun showsl_formula where 
  "showsl_formula (Atom a) = showsl a" 
| "showsl_formula (NegAtom a) = showsl_lit (STR ''! ('') o showsl a o showsl_lit (STR '')'')" 
| "showsl_formula (Conjunction a) = showsl_list_gen id (STR ''TRUE'') (STR ''('') (STR '' & '') (STR '')'') (map showsl a)"  
| "showsl_formula (Disjunction a) = showsl_list_gen id (STR ''FALSE'') (STR ''('') (STR '' | '') (STR '')'') (map showsl a)"  
definition "showsl_list (xs :: 'a formula list) = default_showsl_list showsl xs"
instance ..
end

fun isLit where "isLit (Atom _) = True" | "isLit (NegAtom _) = True" | "isLit _ = False"

abbreviation disj_atoms :: "'a list ⇒ 'a formula" where
  "disj_atoms as ≡ Disjunction (map Atom as)"
abbreviation conj_atoms :: "'a list ⇒ 'a formula" where
  "conj_atoms as ≡ Conjunction (map Atom as)"

inductive is_conj_lits
where "(⋀φ. φ ∈ set φs ⟹ isLit φ) ⟹ is_conj_lits (Conjunction φs)"

inductive is_clause
  where "(⋀φ. φ ∈ set φs ⟹ isLit φ) ⟹ is_clause (Disjunction φs)"

lemma is_clause_code[code]: "is_clause (Disjunction ls) = (∀ l ∈ set ls. isLit l)" 
  "is_clause (Conjunction xs) = False" 
  "is_clause (Atom a) = False" 
  "is_clause (NegAtom a) = False" 
  by (auto simp: is_clause.simps)

fun is_neg_atom where "is_neg_atom (NegAtom _) = True" | "is_neg_atom _ = False"
  
inductive is_neg_atom_clause
  where "(⋀φ. φ ∈ set φs ⟹ is_neg_atom φ) ⟹ is_neg_atom_clause (Disjunction φs)"

lemma is_neg_atom_clause[code]: "is_neg_atom_clause (Disjunction ls) = (∀ l ∈ set ls. is_neg_atom l)" 
  "is_neg_atom_clause (Conjunction xs) = False" 
  "is_neg_atom_clause (Atom a) = False" 
  "is_neg_atom_clause (NegAtom a) = False" 
  by (auto simp: is_neg_atom_clause.simps)
    
fun is_Atom where "is_Atom (Atom _) = True" | "is_Atom _ = False" 
fun get_Atom where "get_Atom (Atom a) = a" | "get_Atom (NegAtom a) = a" 

inductive is_conj_atoms
where "(⋀φ. φ ∈ set φs ⟹ is_Atom φ) ⟹ is_conj_atoms (Conjunction φs)"

inductive is_cnf
where "(⋀φ. φ ∈ set φs ⟹ is_clause φ) ⟹ is_cnf (Conjunction φs)"

abbreviation form_False :: "'a formula" ("Falsef")
where "form_False ≡ Disjunction []"

abbreviation form_True  :: "'a formula" ("Truef")
where "form_True ≡ Conjunction []"

fun form_not :: "'a formula ⇒ 'a formula" (f _" [43] 43)
where "(¬f Atom a) = NegAtom a"
    | "(¬f NegAtom a) = Atom a"
    | "(¬f Conjunction φs) = Disjunction (map form_not φs)"
    | "(¬f Disjunction φs) = Conjunction (map form_not φs)"

fun form_and :: "'a formula ⇒ 'a formula ⇒ 'a formula" (infixl "∧f" 42)
where "(Trueff ψ) = ψ"
    | "(φ ∧f Truef) = φ"
    | "(Conjunction φs ∧f Conjunction ψs) = Conjunction (φs @ ψs)"
    | "(Conjunction φs ∧f ψ) = Conjunction (φs @ [ψ])"
    | "(φ ∧f Conjunction ψs) = Conjunction (φ # ψs)"
    | "(φ ∧f ψ) = Conjunction [φ,ψ]"

fun form_or :: "'a formula ⇒ 'a formula ⇒ 'a formula" (infixl "∨f" 41)
where "(Falseff ψ) = ψ"
    | "(φ ∨f Falsef) = φ"
    | "(Disjunction φs ∨f Disjunction ψs) = Disjunction (φs @ ψs)"
    | "(Disjunction φs ∨f ψ) = Disjunction (φs @ [ψ])"
    | "(φ ∨f Disjunction ψs) = Disjunction (φ # ψs)"
    | "(φ ∨f ψ) = Disjunction [φ,ψ]"

fun simplify
where "simplify (Disjunction (φ#φs)) = (simplify φ ∨f simplify (Disjunction φs))"
    | "simplify (Conjunction [φ]) = simplify φ"
    | "simplify (Conjunction (φ#φs)) = (simplify φ ∧f simplify (Conjunction φs))"
    | "simplify φ = φ"

lemma is_Atom_neg[simp]: "is_Atom (¬f f) = is_neg_atom f" by (cases f, auto) 
  
lemma is_conj_atoms_neg[simp]: "is_conj_atoms (¬f φ) = is_neg_atom_clause φ" 
  by (cases φ, auto simp: is_conj_atoms.simps is_neg_atom_clause.simps)

fun cnf_form_or :: "'a formula ⇒ 'a formula ⇒ 'a formula" (infixl "∨cf" 41) where 
  "(Conjunction φs ∨cf Conjunction ψs) = Conjunction [φ ∨f ψ . φ ← φs, ψ ← ψs]"
| "(φ ∨cf ψ) = (φ ∨f ψ)"

lemma map_form_and: "map_formula f (φ ∧f ψ) = (map_formula f φ ∧f map_formula f ψ)"
  by (cases "(φ,ψ)" rule:form_and.cases, auto)

lemma map_form_or: "map_formula f (φ ∨f ψ) = (map_formula f φ ∨f map_formula f ψ)"
  by (cases "(φ,ψ)" rule:form_or.cases, auto)

lemma map_form_not: "map_formula f (¬f φ) = (¬f map_formula f φ)"
  by (induct φ, auto)

text ‹The internal constructs are less useful.›

declare form_and.simps[simp del] form_or.simps[simp del]

abbreviation form_imp (infixr "⟶f" 40) where "(φ ⟶f ψ) ≡ ¬f φ ∨f ψ"

fun form_all
where "form_all [] = Truef"
    | "form_all (φ#φs) = (φ ∧f form_all φs)"

fun form_ex
where "form_ex [] = Falsef"
    | "form_ex (φ#φs) = (φ ∨f form_ex φs)"

fun form_cnf_ex
where "form_cnf_ex [] = Conjunction [Falsef]"
    | "form_cnf_ex (φ#φs) = (φ ∨cf form_cnf_ex φs)"

fun flatten where
  "flatten (Conjunction φs) = form_all (map flatten φs)"
| "flatten (Disjunction φs) = form_cnf_ex (map flatten φs)"
| "flatten φ = Conjunction [Disjunction [φ]]"
  
fun conjuncts where "conjuncts (Conjunction φs) = φs" | "conjuncts φ = [φ]"

fun disjuncts where "disjuncts (Disjunction φs) = φs" | "disjuncts φ = [φ]"

fun triv_unsat :: "'a formula ⇒ bool"
where "triv_unsat (Conjunction φs) = (∀φ ∈ set φs. triv_unsat φ)"
    | "triv_unsat _ = False"




locale formula =
  fixes atom :: "'atom ⇒ bool"
    and assignment :: "'assignment ⇒ bool"
    and eval_true :: "'assignment ⇒ 'atom ⇒ bool"
begin

abbreviation "Assignments ≡ Collect assignment"

subsection ‹Well-formedness›

fun formula :: "'atom formula ⇒ bool" where
  "formula (Atom a) = atom a"
| "formula (NegAtom a) = atom a"
| "formula (Conjunction φs) = (∀φ ∈ set φs. formula φ)"
| "formula (Disjunction φs) = (∀φ ∈ set φs. formula φ)"
 
lemma formula_and[simp]: "formula (φ ∧f ψ) ⟷ formula φ ∧ formula ψ"
  by (cases "(φ,ψ)" rule: form_and.cases, auto simp: form_and.simps)

lemma formula_or[simp]: "formula (φ ∨f ψ) ⟷ formula φ ∧ formula ψ"
  by (cases "(φ,ψ)" rule: form_or.cases, auto simp: form_or.simps)

lemma formula_not[simp]: "formula (¬f φ) ⟷ formula φ" by (induct φ; auto)

lemma formula_all[simp]: "formula (form_all φs) ⟷ (∀φ ∈ set φs. formula φ)"
  by (induct φs, auto)

lemma formula_ex[simp]: "formula (form_ex φs) ⟷ (∀φ ∈ set φs. formula φ)"
  by (induct φs, auto)

lemma formula_cnf_or[simp]: "formula φ ⟹ formula ψ ⟹ formula (φ ∨cf ψ)"
  by (cases φ; cases ψ, auto)

lemma formula_cnf_ex[simp]: "(∀φ ∈ set φs. formula φ) ⟹ formula (form_cnf_ex φs)"
  by (induct φs, auto)

lemma formula_flatten[simp]: "formula φ ⟹ formula (flatten φ)"
  by (induct φ rule: flatten.induct, auto simp: Let_def)

lemma formula_simplify[simp]: "formula (simplify φ) ⟷ formula φ"
  by (induct φ rule: simplify.induct, auto)

lemma isLit_negate[simp]: "isLit (¬f f) = isLit f" by (cases f, auto)

lemma is_conj_lits_negate[simp]: "is_conj_lits (¬f f) = is_clause f"
  by (cases f, auto simp: is_clause.simps is_conj_lits.simps)

lemma is_cnf_form_and[simp]: "is_cnf f ⟹ is_cnf g ⟹ is_cnf (f ∧f g)"
  by (cases "(f,g)" rule: form_and.cases; auto simp: is_cnf.simps form_and.simps)

lemma is_clause_form_or[simp]: "is_clause f ⟹ is_clause g ⟹ is_clause (f ∨f g)"
  by (cases "(f,g)" rule: form_or.cases; auto simp: is_clause.simps form_or.simps)

lemma is_cnf_cnf_form_or[simp]: "is_cnf f ⟹ is_cnf g ⟹ is_cnf (f ∨cf g)"
  by (cases f; cases g; auto simp: is_cnf.simps form_and.simps)

lemma is_cnf_form_True[simp]: "is_cnf Truef"
  by (simp add: is_cnf.simps)

lemma is_cnf_form_all[simp]: "(⋀ f. f ∈ set fs ⟹ is_cnf f) ⟹ is_cnf (form_all fs)"
  by(induct fs, auto)

lemma is_cnf_form_cnf_ex[simp]: "(⋀ f. f ∈ set fs ⟹ is_cnf f) ⟹ is_cnf (form_cnf_ex fs)"
  by(induct fs, auto, auto simp: is_cnf.simps is_clause.simps)

lemma is_cnf_Conjunction[simp]: "is_cnf (Conjunction fs) = (∀ f ∈ set fs. is_clause f)"
  by (auto simp: is_cnf.simps)

lemma is_clause_Disjunction[simp]: "is_clause (Disjunction fs) = (∀ f ∈ set fs. isLit f)"
  by (auto simp: is_clause.simps)

lemma is_cnf_flatten[simp]:
  "is_cnf (flatten (φ :: ('f,'v,'t) exp formula))"
  by (induct φ rule: flatten.induct, auto intro!: is_cnf_form_all is_cnf_form_cnf_ex)


subsection ‹Valuation›

context fixes α :: "'assignment" begin

  fun satisfies :: "'atom formula ⇒ bool" where
    "satisfies (Atom a) ⟷ eval_true α a"
  | "satisfies (NegAtom a) ⟷ ¬ eval_true α a"
  | "satisfies (Conjunction φs) ⟷ (∀φ ∈ set φs. satisfies φ)"
  | "satisfies (Disjunction φs) ⟷ (∃φ ∈ set φs. satisfies φ)"

  lemma satisfiesI[intro]:
    "eval_true α a ⟹ satisfies (Atom a)"
    "¬ eval_true α a ⟹ satisfies (NegAtom a)"
    "(⋀φ. φ ∈ set φs ⟹ satisfies φ) ⟹ satisfies (Conjunction φs)"
    "⋀φ. φ ∈ set φs ⟹ satisfies φ ⟹ satisfies (Disjunction φs)" by auto

  lemma form_True[simp]: "satisfies Truef" by auto

  lemma satisfies_NegAtom[simp]: "satisfies (NegAtom a) ⟷ ¬ satisfies (Atom a)" by simp

  lemma satisfies_and[simp]: "satisfies (φ ∧f ψ) ⟷ satisfies φ ∧ satisfies ψ"
    by (cases "(φ,ψ)" rule:form_and.cases, auto simp: form_and.simps)

  lemma satisfies_or[simp]: "satisfies (φ ∨f ψ) ⟷ satisfies φ ∨ satisfies ψ"
    by (cases "(φ,ψ)" rule:form_or.cases, auto simp: form_or.simps)

  lemma satisfies_not[simp]: "satisfies (¬f φ) ⟷ ¬ satisfies φ"
    by (induct φ, auto)

  lemma satisfies_all[simp]:
    "satisfies (form_all φs) ⟷ (∀φ ∈ set φs. satisfies φ)" by (induct φs, auto)

  lemma satisfies_ex[simp]:
    "satisfies (form_ex φs) ⟷ (∃φ ∈ set φs. satisfies φ)" by (induct φs, auto)
end

notation satisfies (infix "⊨" 40)


subsection ‹Language›

definition Language where "Language φ = {α ∈ Assignments. α ⊨ φ}"
notation Language ("ℒ") (* this allows the notation available in sublocales *)

lemma Language_dom [dest]: assumes "α ∈ ℒ φ" shows "assignment α"
  using assms by (auto simp: Language_def)

lemma Language_simps[simp]:
  "ℒ Falsef = {}"
  "ℒ Truef = Assignments"
  "ℒ (φ ∧f ψ) = ℒ φ ∩ ℒ ψ"
  "ℒ (φ ∨f ψ) = ℒ φ ∪ ℒ ψ"
  "ℒ (NegAtom a) = Assignments - ℒ (Atom a)"
  "ℒ (Conjunction (φ#φs)) = ℒ φ ∩ ℒ (Conjunction φs)"
  "ℒ (Disjunction (φ#φs)) = ℒ φ ∪ ℒ (Disjunction φs)" by (auto simp: Language_def)

lemma Language_Conjunction[simp]: "ℒ (Conjunction φs) = Assignments ∩ (⋂φ ∈ set φs. ℒ φ)" by (induct φs, auto)

lemma Language_Disjunction[simp]: "ℒ (Disjunction φs) = (⋃φ ∈ set φs. ℒ φ)" by (induct φs, auto)

lemma Language_not[simp]: "ℒ (¬f φ) = Assignments - ℒ φ" by (induct φ, auto)

lemma Language_all[simp]: "ℒ (form_all φs) = Assignments ∩ (⋂φ ∈ set φs. ℒ φ)" by (induct φs, auto)

lemma Language_ex[simp]: "ℒ (form_ex φs) = (⋃φ ∈ set φs. ℒ φ)" by (induct φs, auto)

lemma all_conjuncts[simplified,simp]: "ℒ (form_all (conjuncts φ)) = ℒ φ" by (cases φ, auto)
lemma formula_conjuncts[simplified,simp]: "(∀φ' ∈ set (conjuncts φ). formula φ') = formula φ" by (cases φ, auto)

lemma ex_disjuncts[simplified,simp]: "ℒ (form_ex (disjuncts φ)) = ℒ φ" by (cases φ, auto) 
lemma formula_disjuncts[simplified,simp]: "(∀φ' ∈ set (disjuncts φ). formula φ') = formula φ" by (cases φ, auto)

lemma Language_cnf_form_or[simp]: "ℒ (φ ∨cf ψ) = ℒ φ ∪ ℒ ψ"
  by (cases φ; cases ψ, auto)

lemma Language_cnf_ex[simp]: "ℒ (form_cnf_ex φs) = (⋃φ ∈ set φs. ℒ φ)" by (induct φs, auto)

lemma Langage_flatten[simp]: "ℒ (flatten φ) = ℒ φ"
  by (induct φ rule: flatten.induct, auto simp: Let_def)

lemma Language_simplify[simp]: "ℒ (simplify φ) = ℒ φ"
  by (induct φ rule: simplify.induct, auto)

lemma satisfies_Language: assumes "assignment α" shows "α ⊨ φ ⟷ α ∈ ℒ φ"
  using assms by (auto simp: Language_def)

definition implies :: "'atom formula ⇒ 'atom formula ⇒ bool" where
  "implies φ ψ ≡ ∀α. assignment α ⟶ α ⊨ φ ⟶ α ⊨ ψ"

notation implies (infix "⟹f" 41)

lemma impliesI[intro]:
  assumes "⋀ α. assignment α ⟹ α ⊨ φ ⟹ α ⊨ ψ"
  shows "φ ⟹f ψ" using assms by (auto simp: implies_def)

lemma impliesD[dest]:
  assumes "φ ⟹f ψ"
  shows "assignment α ⟹ α ⊨ φ ⟹ α ⊨ ψ"
  using assms by (auto simp: implies_def)

lemma impliesE[elim]:
  assumes "φ ⟹f ψ" "(⋀α. assignment α ⟹ α ⊨ φ ⟹ α ⊨ ψ) ⟹ P"
  shows P using assms by (auto simp: implies_def)

lemma implies_Language[simp]: "(φ ⟹f ψ) ⟷ ℒ φ ⊆ ℒ ψ"
  by (auto simp add: implies_def satisfies_Language)

definition equivalent where "equivalent φ ψ ≡ φ ⟹f ψ ∧ ψ ⟹f φ"
notation equivalent (infix "⟺f" 40)

lemma equivalentI[intro]: assumes "φ ⟹f ψ" and "ψ ⟹f φ" shows "φ ⟺f ψ"
  using assms by (auto simp: equivalent_def)

lemma equivalentE[elim]: assumes "φ ⟺f ψ" and "(φ ⟹f ψ) ⟹ (ψ ⟹f φ) ⟹ thesis" shows thesis
  using assms by (auto simp: equivalent_def)

lemma equivalent_Language[simp]: "φ ⟺f ψ ⟷ ℒ φ = ℒ ψ" by auto

definition valid where
  "(valid φ) = (∀ α. assignment α ⟶ α ⊨ φ)"

notation valid ("⊨f _" [40]40)

lemma validI[intro]:
  assumes "⋀ α. assignment α ⟹ α ⊨ φ"
  shows "⊨f φ" using assms by (auto simp: valid_def)

lemma validD[dest]:
  assumes "⊨f φ"
  shows "assignment α ⟹ α ⊨ φ"
  using assms by (auto simp: valid_def)

lemma valid_Language:
  "⊨f φ ⟷ ℒ φ = Assignments" by (auto simp: satisfies_Language)

lemma valid_simplify [simp]: "⊨f simplify φ ⟷ ⊨f φ"
  by (simp add: valid_Language)

lemma valid_flatten [simp]: "⊨f flatten φ ⟷ ⊨f φ"
  by (simp add: valid_Language)

lemma valid_implies_trans [trans]:
  assumes "⊨f φ" and "φ ⟹f ψ" shows "⊨f ψ"
  using assms by (auto simp: valid_Language)

lemma valid_equivalent_trans [trans]:
  assumes "⊨f φ" and "φ ⟺f ψ" shows "⊨f ψ"
  using assms by (auto simp: valid_Language)

lemma implies_trans [trans]:
  assumes "φ ⟹f ψ" and "ψ ⟹f ρ" shows "φ ⟹f ρ"
  using assms by auto

lemma implies_equivalent_trans [trans]:
  assumes "φ ⟹f ψ" and "ψ ⟺f ρ" shows "φ ⟹f ρ"
  using assms by auto

lemma equivalent_implies_trans [trans]:
  assumes "φ ⟺f ψ" and "ψ ⟹f ρ" shows "φ ⟹f ρ"
  using assms by (auto dest: implies_trans)

end

locale showsl_formula =
  fixes showsl_atom :: "'a ⇒ showsl"
begin
fun showsl_formula :: "'a formula ⇒ showsl" where
  "showsl_formula (Atom a) = showsl_atom a"
| "showsl_formula (NegAtom a) = showsl (STR ''! ('') o showsl_atom a o showsl (STR '')'')"
| "showsl_formula (Conjunction fs) = (let ss = map showsl_formula fs in
     showsl_list_gen id (STR ''True'') (STR ''Conj['') (STR '', '') (STR '']'') ss)" 
| "showsl_formula (Disjunction fs) = (let ss = map showsl_formula fs in
     showsl_list_gen id (STR ''False'') (STR ''Disj['') (STR '', '') (STR '']'') ss)" 
end


subsection ‹Formulas over terms›

fun vars_formula :: "('f,'v) term formula ⇒ 'v set"
where "vars_formula (Atom a) = vars_term a"
    | "vars_formula (NegAtom a) = vars_term a"
    | "vars_formula (Conjunction φs) = (⋃(vars_formula ` set φs))"
    | "vars_formula (Disjunction φs) = (⋃(vars_formula ` set φs))"

fun vars_formula_list :: "('f,'v) term formula ⇒ 'v list"
where "vars_formula_list (Atom a) = vars_term_list a"
    | "vars_formula_list (NegAtom a) = vars_term_list a"
    | "vars_formula_list (Conjunction φs) = concat (map vars_formula_list φs)"
    | "vars_formula_list (Disjunction φs) = concat (map vars_formula_list φs)"

fun in_vars_formula :: "'v ⇒ ('f,'v) term formula ⇒ bool"
where "in_vars_formula x (Atom a) = (x ∈ set (vars_term_list a))"
    | "in_vars_formula x (NegAtom a) = (x ∈ set (vars_term_list a))"
    | "in_vars_formula x (Conjunction φs) = (∃ φ ∈ set φs. in_vars_formula x φ)" 
    | "in_vars_formula x (Disjunction φs) = (∃ φ ∈ set φs. in_vars_formula x φ)" 

lemma in_vars_formula[code_unfold]: "(x ∈ vars_formula φ) = in_vars_formula x φ" 
  by (induct φ, auto)

lemma vars_formula_list: "vars_formula φ = set (vars_formula_list φ)"
  by (induct φ, auto)

lemma vars_formula_set_formula: "vars_formula φ = ⋃ (vars_term ` set_formula φ)"
  by (induct φ, auto)

abbreviation rename_vars_formula :: "('v ⇒ 'w) ⇒ ('f,'v,'t) exp formula ⇒ ('f,'w,'t) exp formula"
where "rename_vars_formula r cls ≡ map_formula (rename_vars r) cls"

adhoc_overloading rename_vars rename_vars_formula

lemma rename_vars_formula_comp[simp]:
  "rename_vars f (rename_vars g (φ::('f,'v,'t) exp formula)) = rename_vars (f ∘ g) φ"
   by (cases φ, auto simp: formula.map_comp o_def)

(* record-based locales makes interpretation with rewrites not OK
record ('f,'t,'d) "logic" =
  type_of_fun :: "'f ⇒ 't list × 't"
  Values_of_type :: "'t ⇒ 'd set"
  Bool_types :: "'t set"
  to_bool :: "'d ⇒ bool"
  "interpret" :: "'f ⇒ 'd list ⇒ 'd"
*)


locale prelogic =
  pre_sorted_algebra where type_fixer = type_fixer
  for type_fixer :: "('f×'t×'d) itself"
  and Bool_types :: "'t set"
  and to_bool :: "'d ⇒ bool"
begin

  definition "is_bool e ≡ (∃b ∈ Bool_types. e :f b) ∧ ¬ is_Var e"

  lemma is_bool_simps[simp]: "is_bool (Var x) = False"
   "is_bool (Fun f es) = (∃b ∈ Bool_types. Fun f es :f b)" by (auto simp: is_bool_def)

  abbreviation "BOOL_EXP ≡ Collect is_bool"

  sublocale formula is_bool assignment "λα t. to_bool (⟦t⟧α)".

  lemma Language_atom[simp]: "ℒ (Atom e) = { α ∈ Assignments. to_bool (⟦e⟧α) }" by (auto simp: Language_def)

  lemma is_bool_imp_expression[simp]: "is_bool e ⟹ expression e" unfolding is_bool_def by auto

  lemma formula_rename_vars[simp]: "formula (rename_vars r e) = formula e"
  proof (induct e)
    case (Atom x)
    then show ?case by (cases x, auto)
  next
    case (NegAtom x)
    then show ?case by (cases x, auto)
  qed auto

  lemma formula_rename_vars_map[simp]:
    "list_all formula (map (rename_vars r) l) = list_all formula l"
    using formula_rename_vars unfolding list_all_def by auto

  lemma eval_with_fresh_var[simp]: "xx ∉ vars_term e ⟹ ⟦e⟧ (α(xx:=a)) = ⟦e⟧ α" by auto

  lemma satisfies_with_fresh_var[simp]:
    assumes fv: "xx ∉ vars_formula φ"
    shows "α(xx:=a) ⊨ φ ⟷ α ⊨ φ" by (insert fv, induct φ, auto)

  lemma satisfies_rename_vars:
    assumes r: "⋀ x t. α (x,t) = β (r x, t)"
    shows "β ⊨ (rename_vars r φ) ⟷ α ⊨ φ"
    by (induct φ, auto simp: eval_rename_vars[of α, OF r])

  definition satisfiable where "satisfiable φ = (∃ α. assignment α ∧ α ⊨ φ)" 

end

fun ground_formula where
  "ground_formula (Atom a) = ground a" 
| "ground_formula (NegAtom a) = ground a" 
| "ground_formula (Disjunction fs) = (∀ f ∈ set fs. ground_formula f)" 
| "ground_formula (Conjunction fs) = (∀ f ∈ set fs. ground_formula f)" 

locale logic = prelogic + sorted_algebra


subsection ‹Checking validity›

type_synonym ('h,'f,'v,'t) logic_checker =
  "'h ⇒ ('f,'v,'t) exp formula ⇒ showsl check"

datatype 'h hint =
  Default
| Base 'h
| Distribute nat "('h hint list)"
| Erase nat "('h hint)"
| LexStrict "('h hint list)"
| LexWeak "('h hint list)"

primrec showsl_hint where
  "showsl_hint Default = showsl_lit (STR '' auto'')"
| "showsl_hint (Base raw) = showsl_lit (STR '' '') o showsl raw"
| "showsl_hint (Distribute i hints) = showsl_lit (STR '' Distribute '') o showsl i o 
    showsl_list_gen id (STR '' []'') (STR '' ['') (STR '', '') (STR '']'') (map showsl_hint hints)"
| "showsl_hint (LexStrict hints) = showsl_lit (STR '' LexStrict'') o 
    showsl_list_gen id (STR '' []'') (STR '' ['') (STR '', '') (STR '']'') (map showsl_hint hints)"
| "showsl_hint (LexWeak hints) = showsl_lit (STR '' LexWeak'') o 
    showsl_list_gen id (STR '' []'') (STR '' ['') (STR '', '') (STR '']'') (map showsl_hint hints)"
| "showsl_hint (Erase i hint) = showsl_lit (STR '' Erase '') o showsl i o showsl_lit (STR '' ['') o showsl_hint hint o showsl_lit (STR '' ]'')"


instantiation hint :: (default) default
begin
  definition "default ≡ Default"
  instance ..
end

hide_const(open) Default Base Distribute Erase

definition trivial_checker where
  "trivial_checker lits = (case partition is_Atom lits of
     (as, nas) ⇒ let pos = map get_Atom as; neg = map get_Atom nas
    in (∃ a ∈ set pos. a ∈ set neg))"

definition trivial_clause_checker where "trivial_clause_checker f = (case f of Disjunction lits ⇒ trivial_checker lits)" 

lemma trivial_checker:
  assumes "⋀ l. l ∈ set lits ⟹ isLit l" and "trivial_checker lits"
  shows "∃ a. Atom a ∈ set lits ∧ NegAtom a ∈ set lits"
proof -
  obtain as nas where part: "partition is_Atom lits = (as,nas)" by force
  from assms[unfolded trivial_checker_def part split, simplified]
  obtain a where a: "a ∈ set as" "get_Atom a ∈ get_Atom ` set nas" by auto
  from partition_filter_conv[of is_Atom lits, unfolded part]
  have id: "as = filter is_Atom lits" "nas = filter (λ x. ¬ is_Atom x) lits" by (auto simp: o_def)
  from a(1)[unfolded id] have "is_Atom a" and mem: "a ∈ set lits" by auto
  then obtain aa where aa: "a = Atom aa" by (cases a, auto)
  from a(2)[unfolded aa] obtain na where na: "get_Atom na = aa" "na ∈ set nas" by auto
  from na(2)[unfolded id] assms(1) have "¬ is_Atom na" "isLit na" "na ∈ set lits" by auto
  with na have "NegAtom aa ∈ set lits" by (cases na, auto)
  with mem aa show ?thesis by auto
qed

fun get_disjunctions where
  "get_disjunctions (Disjunction phis) = concat (map get_disjunctions phis)" 
| "get_disjunctions x = [x]"

fun get_conjunctions where
  "get_conjunctions (Conjunction phis) = concat (map get_conjunctions phis)" 
| "get_conjunctions x = [x]"

definition check_trivial_implication where
  "check_trivial_implication φ ψ = 
      (∀ phi ∈ set (get_disjunctions φ). let c_phis = get_conjunctions phi in  
       ∃ psi ∈ set (get_disjunctions ψ). ∀ c_psi ∈ set (get_conjunctions psi). c_psi ∈ set c_phis)" 

fun trivial_formula where
  "trivial_formula (Disjunction φs) = list_ex trivial_formula φs"
| "trivial_formula (Conjunction φs) = list_all trivial_formula φs"
| "trivial_formula _ = False"

context prelogic
begin

lemma get_disjunctions: "(α ⊨ form_ex (get_disjunctions φ)) = (α ⊨ φ)"
  by (induct φ, auto)

lemma get_conjunctions: "(α ⊨ form_all (get_conjunctions φ)) = (α ⊨ φ)"
  by (induct φ, auto)

lemma check_trivial_implication:
  assumes "check_trivial_implication φ ψ" shows "φ ⟹f ψ"
proof
  fix α
  assume "α ⊨ φ" 
  then have "α ⊨ form_ex (get_disjunctions φ)" unfolding get_disjunctions .
  then obtain phi where phi: "phi ∈ set (get_disjunctions φ)" and sat: "α ⊨ phi" by auto
  from assms[unfolded check_trivial_implication_def Let_def, rule_format, OF phi]
  obtain psi where psi: "psi ∈ set (get_disjunctions ψ)"
    and conj: "⋀ c_psi. c_psi∈set (get_conjunctions psi) ⟹ c_psi ∈ set (get_conjunctions phi)" by auto
  {
    fix c_psi
    assume "c_psi ∈ set (get_conjunctions psi)" 
    then have mem: "c_psi ∈ set (get_conjunctions phi)" using conj by auto
    from sat[folded get_conjunctions[of _ phi]] mem have "α ⊨ c_psi" by auto
  }
  then have "α ⊨ psi" using get_conjunctions[of _ psi] by auto
  then show "α ⊨ ψ" using psi get_disjunctions[of _ ψ] by auto
qed

lemma trivial_formula:
  assumes "trivial_formula φ" shows "⊨f φ"
  by (insert assms, induct φ, auto simp: list_all_iff list_ex_iff valid_Language)

lemma trivial_clause_checker:
  assumes "is_clause φ" and "trivial_clause_checker φ" shows "⊨f φ"
proof -
  from assms obtain lits where phi: "φ = Disjunction lits" and lits: "⋀ l. l ∈ set lits ⟹ isLit l"
    using is_clause.cases by blast
  from assms[unfolded trivial_clause_checker_def phi] have triv: "trivial_checker lits" by auto
  from trivial_checker[OF lits this] obtain a where a: "Atom a ∈ set lits" "NegAtom a ∈ set lits" by auto
  from split_list[OF a(1)] obtain l1 l2 where lits: "lits = l1 @ Atom a # l2" by auto
  from a(2) lits have "NegAtom a ∈ set (l1 @ l2)" by auto
  from split_list[OF this] obtain l3 l4 where l12: "l1 @ l2 = l3 @ NegAtom a # l4" by auto
  have "set lits = insert (Atom a) (set (l1 @ l2))" unfolding lits by auto
  also have "… = insert (Atom a) (insert (NegAtom a) (set l3 ∪ set l4))" unfolding l12 by auto
  finally show ?thesis unfolding phi by auto
qed

end

locale pre_logic_checker =
  prelogic where type_fixer = "TYPE('f×'t×'d)" +
  showsl_formula showsl_atom
  for type_fixer :: "('f × 'v :: showl × 't × 'd × 'h :: {default,showl}) itself"
  and showsl_atom :: "('f,'v,'t) exp ⇒ showsl"
  and logic_checker :: "('h,'f,'v,'t) logic_checker"
  and negate_atom :: "('f,'v,'t) exp ⇒ ('f,'v,'t) exp formula"
begin

fun remove_Atom where
  "remove_Atom (Conjunction φs) = Conjunction (map remove_Atom φs)"
| "remove_Atom (Disjunction φs) = Disjunction (map remove_Atom φs)"
| "remove_Atom (NegAtom φ) = NegAtom φ"
| "remove_Atom (Atom φ) = (¬f (negate_atom φ))"

definition "check_valid_formula φ ≡
  (case flatten φ of Conjunction φs ⇒ check_allm (
     λ φ. try (check (trivial_clause_checker φ) (STR ''trivial clause checker failed'')) catch (λ _. 
       case flatten (remove_Atom φ) of Conjunction φs ⇒ check_allm (logic_checker default) φs)) φs)
  <+? (λs. showsl_lit (STR ''problem in checking validity of formula '') o showsl_formula φ o showsl_nl o s)"

fun is_or_and_shape where
  "is_or_and_shape (Disjunction [φ1,Conjunction [φ2,φ3]]) = True"
| "is_or_and_shape _ = False"

fun is_conj_shape where
  "is_conj_shape [hint1,hint2] (Conjunction [φ1,φ2]) = True"
| "is_conj_shape _ _ = False"

fun is_disj_shape where
  "is_disj_shape (hint1#hints) (Disjunction [Conjunction [φ1,φ2], Conjunction [φ3,φ4]]) = True"
| "is_disj_shape _ _ = False"

function(sequential) check_formula and check_formula_dist and check_formula_lex_weak and check_formula_lex
where
  "check_formula hint.Default φ = check_valid_formula φ"
| "check_formula (hint.Base h) φ = do {
    let ψ = remove_Atom (simplify φ);
    check (is_neg_atom_clause ψ) (showsl (STR ''base hint given to '') o showsl_formula ψ);
    logic_checker h ψ <+? (λ s. showsl (STR ''problem in checking '') o showsl_formula φ o showsl_nl o s)}"
| "check_formula (hint.Erase n hint) φ =
    ( case φ of formula.Disjunction φs ⇒ do {
        let l = length φs;
        check (n < l) (showsl (STR ''erase hint at position '') o showsl n o showsl (STR '' while goal is length '') o showsl l);
        let pre = take n φs;
        let post = drop (Suc n) φs;
        check_formula hint (formula.Disjunction (pre @ Falsef # post))
      }
      | _ ⇒ error (showsl (STR ''Erase hint to non-Disjunction''))
    )"
| "check_formula (hint.Distribute n hints) φ =
    ( case φ of formula.Disjunction φs ⇒ do {
        let l = length φs;
        check (n < l) (showsl (STR ''distribute hint at position '') o showsl n o showsl (STR '' while goal is length '') o showsl l);
        let pre = take n φs;
        let post = drop (Suc n) φs;
        case φs ! n of
          Conjunction ψs ⇒ check_formula_dist hints pre post ψs
        | _ ⇒ error (showsl (STR ''Distribute hint in: ⏎'') o showsl_formula φ o showsl (STR ''⏎ at non-Conjunction position:⏎'') o showsl_formula (φs ! n))
      }
      | _ ⇒ error (showsl (STR ''Distribute hint for non Disjunction '') o showsl_formula φ)
    )"
| "check_formula (hint.LexWeak hints) ψ = (case ψ of 
     Disjunction (φ#φs) ⇒ check_formula_lex_weak hints φ φs
   | _ ⇒ error (showsl (STR ''LexWeak hint applied on '') o showsl_formula ψ))"
| "check_formula (hint.LexStrict hints) ψ = (case ψ of 
     Disjunction (φ#φs) ⇒ check_formula_lex hints φ φs
   | _ ⇒ error (showsl (STR ''LexStrict hint applied on '') o showsl_formula ψ))"
| "check_formula_dist [] pre post [] = succeed"
| "check_formula_dist (h#hs) pre post (φ#φs) =
   check_formula h (formula.Disjunction (pre @ φ # post)) ⪢ check_formula_dist hs pre post φs"
| "check_formula_dist _ _ _ _ = error (showsl (STR ''Length mismatch in Distribute hints''))"
| "check_formula_lex_weak [] φ φs =
   check (trivial_formula φ) (showsl (STR ''LexWeak base case error: '') o showsl_formula φ)"
| "check_formula_lex_weak (hint#hints) φ φs = (if is_or_and_shape φ then (case φ of
    Disjunction [φ1,Conjunction [φ2,φ3]] ⇒ do {
      check_formula hint (Disjunction (φ2#φs));
      check_formula_lex_weak hints φ3 φs
    })
    else (case hints of 
      Nil ⇒ check_formula hint (Disjunction (φ#φs))
    | _ ⇒ error (showsl (STR ''LexWeak hint application error''))))"
| "check_formula_lex hints φ φs = (if is_conj_shape hints φ then
      (case hints of [hint1,hint2] ⇒ case φ of Conjunction [φ1,φ2] ⇒ do {
      check_formula hint1 (Disjunction (φ1#φs));
      check_formula hint2 (Disjunction (φ2#φs))
    }) else (if is_disj_shape hints φ then
      (case hints of hint1#hints2 ⇒ case φ of Disjunction [Conjunction [φ1,φ2], Conjunction [φ3,φ4]] ⇒ 
        (case hints2 of 
          [hint2] ⇒ do {
            check_formula hint1 (Disjunction (φ1#φs));
            check_formula hint2 (Disjunction (φ2#φs))
          }
        | _ ⇒ do {
            check_formula hint1 (Disjunction (φ3#φs));
            check_formula_lex hints2 φ4 φs
          })) 
      else error (showsl (STR ''LexStrict hint application error: '') o
        showsl_hint (LexStrict hints) o showsl (STR ''⏎applied on '') o showsl_formula φ)))" 
  by (pat_completeness,auto)

termination by (relation "measure (λx.
  case x of Inl (Inl (x,_)) ⇒ size x
  | Inl (Inr (xs,_)) ⇒ size_list size xs
  | Inr (Inl (xs,_)) ⇒ size_list size xs
  | Inr (Inr (xs,_)) ⇒ size_list size xs)", auto)

lemma isOK_check_formula_dist:
  assumes "isOK (check_formula_dist hs pre post φs)" and "φ ∈ set φs"
  shows "∃h ∈ set hs. isOK (check_formula h (Disjunction (pre @ φ # post)))"
proof (insert assms, induct φs arbitrary: hs)
  case IH: (Cons a φs) then show ?case by(cases hs, auto)
qed auto

end

fun mono_formula where
  "mono_formula b (Conjunction fs) = (∀ f ∈ set fs. mono_formula b f)"
| "mono_formula b (Disjunction fs) = (∀ f ∈ set fs. mono_formula b f)"
| "mono_formula b (Atom a) = b"
| "mono_formula b (NegAtom a) = (¬ b)"

lemma mono_formula_negate: "mono_formula (¬ b) f ⟹ mono_formula b (¬f f)"
  by (induct f, auto)

lemma mono_formula_and: "mono_formula b f ⟹ mono_formula b g ⟹ mono_formula b (f ∧f g)"
  by (induct f g rule: form_and.induct, auto simp: form_and.simps)

lemma mono_formula_form_all: "(⋀ f. f ∈ set fs ⟹ mono_formula b f) ⟹ mono_formula b (form_all fs)"
  by (induct fs, auto simp: mono_formula_and)

lemma mono_formula_or: "mono_formula b f ⟹ mono_formula b g ⟹ mono_formula b (f ∨f g)"
  by (induct f g rule: form_or.induct, auto simp: form_or.simps)

lemma mono_formula_cnf_form_or: "mono_formula b f ⟹ mono_formula b g ⟹ mono_formula b (f ∨cf g)"
  by (induct f g rule: cnf_form_or.induct, auto intro: mono_formula_or)

lemma mono_formula_form_cnf_ex: "(⋀ f. f ∈ set fs ⟹ mono_formula b f) ⟹ mono_formula b (form_cnf_ex fs)"
  by (induct fs, auto simp: mono_formula_cnf_form_or)

lemma mono_formula_flatten: "mono_formula b f ⟹ mono_formula b (flatten f)"
  by (induct f, auto intro!: mono_formula_form_all mono_formula_form_cnf_ex)

locale logic_checker =
  logic where type_fixer = "TYPE(_)" + pre_logic_checker +
  assumes logic_checker:
    "⋀h φ. isOK(logic_checker h φ) ⟹ formula φ ⟹ is_neg_atom_clause φ ⟹ ⊨f φ"
    and negate_atom_formula: "is_bool e ⟹ formula (negate_atom e)"
    and negate_atom_mono: "mono_formula True (negate_atom e)" 
    and negate_atom_negates: "is_bool e ⟹ assignment α ⟹ α ⊨ negate_atom e ⟷ ¬ α ⊨ Atom e"
begin

lemma mono_formula_remove_Atom: "mono_formula False (remove_Atom f)"
  by (induct f, auto intro!: mono_formula_negate negate_atom_mono)

lemma formula_remove_Atom: "formula f ⟹ formula (remove_Atom f)"
  by (induct f, auto simp: negate_atom_formula)

lemma Language_remove_Atom: "formula f ⟹ ℒ (remove_Atom f) = ℒ f"
  by (induct f, auto, auto simp: negate_atom_negates Language_def)

lemma check_valid_formula:
  assumes ok: "isOK(check_valid_formula φ)" and φ: "formula φ"
  shows "⊨f φ"
proof-
  from φ have form: "formula (flatten φ)" by auto
  from is_cnf_flatten[of φ] have "is_cnf (flatten φ)" .
  then obtain φs where *: "flatten φ = Conjunction φs" "⋀ φi. φi ∈ set φs ⟹ is_clause φi" by (cases, auto)
  from form have form: "⋀ψ. ψ ∈ set φs ⟹ formula ψ" by (auto simp: *)
  {
    fix ψ
    assume **: "ψ ∈ set φs" 
    note form = form[OF **]
    note clause = *(2)[OF **]
    let  = "remove_Atom ψ" 
    from is_cnf_flatten[of ] have "is_cnf (flatten ?ψ)" .
    then obtain χs where 1: "flatten ?ψ = Conjunction χs" "⋀ φi. φi ∈ set χs ⟹ is_clause φi" by (cases, auto)
    from formula_remove_Atom[OF form] have form': "⋀ψ. ψ ∈ set χs ⟹ formula ψ" 
      using 1 formula_flatten by force
    from ok[unfolded check_valid_formula_def *, simplified, rule_format, OF **, unfolded 1, simplified]
    consider (Triv) "trivial_clause_checker ψ" | (lc) "∀x∈set χs. isOK (logic_checker default x)" by auto
    then have "⊨f ψ" 
    proof (cases)
      case lc
      {
        fix χ
        assume chi: "χ ∈ set χs" 
        with lc have ok: "isOK(logic_checker default χ)" by auto
        from 1(2)[OF chi] have "is_clause χ" .
        moreover have "mono_formula False χ" 
          using mono_formula_flatten[OF mono_formula_remove_Atom[of ψ], unfolded 1] chi by auto
        ultimately
        have "is_neg_atom_clause χ" 
        proof (induct χ, simp add: is_neg_atom_clause.simps, intro allI impI, goal_cases)
          case (1 fs f)
          then show ?case by (cases f, force+)
        qed
        from logic_checker[OF ok form'[OF chi] this] 
        have "⊨f χ" .
      } 
      then have "⊨f flatten ?ψ" unfolding 1 by (simp add: valid_def)
      also have "… ⟺f ψ" by (simp add: Language_remove_Atom form)
      finally show ?thesis by simp
    next
      case Triv
      from trivial_clause_checker[OF clause this] show ?thesis . 
    qed
  }
  then have "⊨f form_all φs" by (auto simp: valid_Language)
  also have "... ⟺f flatten φ" by (auto simp add: *)
  finally show ?thesis by simp
qed

lemma isOK_simp: "isOK x = (x = Inr ())" by auto

lemma check_formula:
  assumes "isOK(check_formula h φ)" and "formula φ"
  shows "⊨f φ"
proof-
  have "isOK (check_formula h φ) ⟹ formula φ ⟹ ⊨f φ"
   and "isOK (check_formula_dist hs pre post φs) ⟹
        (∀φ ∈ set pre. formula φ) ⟹
        (∀φ ∈ set post. formula φ) ⟹
        (∀φ ∈ set φs. formula φ) ⟹ ∀ φ ∈ set φs. ⊨f Disjunction (pre @ φ # post)"
   and "isOK (check_formula_lex_weak hs φ φs) ⟹ formula φ ⟹ ∀φ ∈ set φs. formula φ ⟹ ⊨f Disjunction (φ#φs)"
   and "isOK (check_formula_lex hs φ φs) ⟹ formula φ ⟹ ∀φ ∈ set φs. formula φ ⟹ ⊨f Disjunction (φ#φs)"
   for h φ hs φs pre post
  proof (induct h φ and hs pre post φs and hs φ φs and hs φ φs rule:check_formula_check_formula_dist_check_formula_lex_weak_check_formula_lex.induct)
    case (1 φ) with check_valid_formula show ?case by auto
  next
    case (2 h φ)
    then have "formula (remove_Atom (simplify φ))" by (intro formula_remove_Atom, auto) 
    with 2 have "⊨f remove_Atom (simplify φ)" by (auto dest: logic_checker)
    also have "… ⟺f φ" using 2(2) by (simp add: Language_remove_Atom)
    finally show ?case .
  next
    case (3 n h φ)
    show ?case
    proof (cases φ)
      case φ: (Disjunction φs)
      show ?thesis
      proof (cases "n < length φs")
        case True
        moreover define pre where "pre = take n φs"
        moreover define post where "post = drop (Suc n) φs"
        moreover define ψ where "ψ = φs ! n"
        ultimately have split: "φs = pre @ ψ # post"
          by (simp add: id_take_nth_drop)
        from 3(3) have form: "∀φ ∈ set pre. formula φ" "∀φ ∈ set post. formula φ"
          by (auto simp: φ pre_def post_def dest: in_set_takeD in_set_dropD)
        with 3(2)[unfolded φ, simplified, folded pre_def post_def]
        have "⊨f Disjunction (pre @ Falsef # post)"
          by (intro 3(1)[OF φ refl _] pre_def post_def, auto simp: check_def)
        then show ?thesis
          by (auto simp: φ split valid_Language)
      next
        case False with 3 φ show ?thesis by auto
      qed
    qed (insert 3, auto simp: check_def)
  next
    case *: (4 n hints φ)
    show ?case
    proof (cases φ)
      case φ: (Disjunction φs)
      with *(3) have form: "∀ψ ∈ set φs. formula ψ" by auto
      show ?thesis
      proof (cases "n < length φs")
        case [simp]: True
        moreover define pre where "pre = take n φs"
        moreover define post where "post = drop (Suc n) φs"
        moreover define ψ where "ψ = φs ! n"
        ultimately have split: "φs = pre @ ψ # post"
          by (simp add: id_take_nth_drop)
        from True form have form: "formula ψ" "∀ φ ∈ set pre. formula φ" "∀ φ ∈ set post. formula φ"
          unfolding ψ_def pre_def post_def by (auto dest:in_set_takeD in_set_dropD)
        note [symmetric,simp] = pre_def post_def ψ_def
        show ?thesis
        proof (cases "ψ")
          case [simp]: (Conjunction ψs)
          note ψ_def[symmetric,unfolded split this,simp]
          from form have form2: "∀ρ ∈ set ψs. formula ρ" by auto
          from *(1)[OF φ refl _ pre_def post_def, unfolded check_def, simplified, OF refl] form *(2)
          show ?thesis apply (simp add: φ satisfies_Language) apply (unfold split) apply (auto simp: valid_Language) done
        qed (insert * φ, auto)
      qed (insert * φ, auto)
    qed (insert *, auto)
  next
    case *: (5 h ψ)
    from *(2) obtain φ φs where ψ: "ψ = Disjunction (φ#φs)" 
      by (cases ψ; cases "disjuncts ψ", auto)
    with * show ?case by auto
  next 
    case *: (6 h ψ) 
    from *(2) obtain φ φs where ψ: "ψ = Disjunction (φ#φs)" 
      by (cases ψ; cases "disjuncts ψ", auto)
    with * show ?case by auto
  next
    case (10 φ φs) then show ?case by (auto dest!: trivial_formula simp: valid_Language)
  next
    case *: (11 hint hints φ φs)
    have ok: "isOK (check_formula_lex_weak (hint # hints) φ φs)" by fact
    show ?case
    proof (cases "is_or_and_shape φ")
      case False
      then have "hints = []" "isOK(check_formula hint (Disjunction (φ#φs)))" using ok by (cases hints, auto)+
      from *(3)[OF False this] show ?thesis using * by auto
    next
      case True
      from True obtain φ1 x where φ: "φ = Disjunction [φ1, x]" 
        by (cases φ; cases "disjuncts φ" rule: list_4_cases, auto)
      from True φ obtain φ2 φ3 where φ: "φ = Disjunction [φ1,Conjunction [φ2,φ3]]" 
        by (cases x; cases "conjuncts x" rule: list_4_cases, auto)
      note IH = *(1-2)[OF True φ refl refl refl refl refl refl refl]
      from ok φ True IH *(5,6) 
      have "⊨f Disjunction (φ2 # φs)" and "⊨f Disjunction (φ3 # φs)" by auto
      then show ?thesis unfolding φ by (auto simp: valid_Language)
    qed
  next
    case *: (12 hints φ φs)
    note prems = *(9-)
    show ?case
    proof (cases "is_conj_shape hints φ")
      case True
      then obtain h1 h2 where hints: "hints = [h1,h2]" 
        by (cases hints rule: list_4_cases, auto)      
      from True hints obtain φ1 φ2 where φ: "φ = Conjunction [φ1, φ2]" 
        by (cases φ; cases "conjuncts φ" rule: list_4_cases, auto)
      note IH = *(1-2)[OF True hints refl refl φ refl refl refl]
      from IH prems φ hints show ?thesis by (auto simp:isOK_simp valid_Language) 
    next
      case False
      with prems have disj: "is_disj_shape hints φ" by (auto split: if_splits)
      then obtain h1 hints2 where hints: "hints = h1 # hints2" 
        by (cases hints, auto)      
      from disj obtain x y where φ: "φ = Disjunction [x, y]" 
        by (cases φ; cases "disjuncts φ" rule: list_4_cases, auto)
      from disj φ obtain φ1 φ2 where φ: "φ = Disjunction [Conjunction [φ1,φ2], y]" 
        by (cases x; cases "conjuncts x" rule: list_4_cases, auto)  
      from disj φ obtain φ3 φ4 where φ: "φ = Disjunction [Conjunction [φ1,φ2], Conjunction [φ3,φ4]]" 
        by (cases y; cases "conjuncts y" rule: list_4_cases, auto)  
      note IH = *(3-8)[OF False disj hints φ refl refl refl refl refl refl refl refl refl refl refl]
      note prems = prems[unfolded φ hints]
      show ?thesis
      proof (cases hints2 rule:list_3_cases)
        case Nil
        from IH(1-2)[OF Nil] prems
        show ?thesis by (auto simp: Nil)
      next
        case (1 h2)
        from IH(3-4)[OF 1 refl] prems φ hints
        show ?thesis by (auto simp: 1 isOK_simp valid_Language)
      next
        case (2 h2 h3 hints3)
        from IH(5-6)[OF 2 refl] prems φ hints
        show ?thesis by (auto simp: 2 isOK_simp valid_Language)
      qed
    qed
  qed auto
  from this(1) assms show ?thesis by auto
qed
end

type_synonym ('f,'v,'t) definability_checker = "'v ⇒ 't ⇒ ('f,'v,'t) exp formula ⇒ showsl check"

locale pre_definability_checker =
  prelogic where type_fixer = "TYPE('f×'t×'d)"
  for type_fixer :: "('f×'v×'t×'d) itself"
  and definability_checker :: "('f,'v,'t) definability_checker"

locale definability_checker = pre_definability_checker +
  assumes definability_checker:
    "⋀x ty φ. isOK (definability_checker x ty φ) ⟹ assignment α ⟹ ∃a ∈ Values_of_type ty. α((x,ty):=a) ⊨ φ"

lemmas [code] =
  prelogic.is_bool_def
  pre_sorted_algebra.has_type.simps
  formula.formula.simps
  showsl_formula.showsl_formula.simps
  pre_logic_checker.check_valid_formula_def
  pre_logic_checker.check_formula.simps
  pre_logic_checker.check_formula_dist.simps
  pre_logic_checker.check_formula_lex_weak.simps
  pre_logic_checker.check_formula_lex.simps
  pre_logic_checker.remove_Atom.simps
  pre_logic_checker.is_or_and_shape.simps
  pre_logic_checker.is_disj_shape.simps
  pre_logic_checker.is_conj_shape.simps

end