Theory Logic

theory Logic
  imports Main
begin

chapter ‹Propositional formulae›
text ‹
  This theory contains syntax and semantics of propositional formulae.
  Furthermore, it contains a function that converts a formula into
  disjunctive normal form. This conversion is justified
  with a proof term. 
›

datatype (atoms: 'a) fm =
  is_Atom: Atom 'a | And "'a fm" "'a fm" | Or "'a fm" "'a fm" |
  Neg "'a fm"

fun amap_fm :: "('a ⇒ 'b fm) ⇒ 'a fm ⇒ 'b fm" ("amap⇩f⇩m") where
  "amap⇩f⇩m h (Atom a) = h a" |
  "amap⇩f⇩m h (And φ⇩1 φ⇩2) = And (amap⇩f⇩m h φ⇩1) (amap⇩f⇩m h φ⇩2)" |
  "amap⇩f⇩m h (Or φ⇩1 φ⇩2) = Or (amap⇩f⇩m h φ⇩1) (amap⇩f⇩m h φ⇩2)" |
  "amap⇩f⇩m h (Neg φ) = Neg (amap⇩f⇩m h φ)"

fun dnf_and_fm :: "'a fm ⇒ 'a fm ⇒ 'a fm" where
  "dnf_and_fm (Or φ⇩1 φ⇩2) ψ = Or (dnf_and_fm φ⇩1 ψ) (dnf_and_fm φ⇩2 ψ)" |
  "dnf_and_fm ψ (Or φ⇩1 φ⇩2) = Or (dnf_and_fm ψ φ⇩1) (dnf_and_fm ψ φ⇩2)" |
  "dnf_and_fm φ⇩1 φ⇩2 = And φ⇩1 φ⇩2"

fun dnf_fm :: "'a fm ⇒ 'a fm" where
  "dnf_fm (And φ⇩1 φ⇩2) = dnf_and_fm (dnf_fm φ⇩1) (dnf_fm φ⇩2)" |
  "dnf_fm (Or φ⇩1 φ⇩2) = Or (dnf_fm φ⇩1) (dnf_fm φ⇩2)" |
  "dnf_fm x = x"

fun conj_list :: "'a fm ⇒ 'a list" where
  "conj_list (And φ⇩1 φ⇩2) = conj_list φ⇩1 @ conj_list φ⇩2" |
  "conj_list (Atom a) = [a]"

fun disj_conj_list :: "'a fm ⇒ 'a list list" where
  "disj_conj_list (Or φ⇩1 φ⇩2) = disj_conj_list φ⇩1 @ disj_conj_list φ⇩2" |
  "disj_conj_list (And φ⇩1 φ⇩2) = [conj_list (And φ⇩1 φ⇩2)]" |
  "disj_conj_list (Atom a) = [[a]]"

definition "dnf ≡ disj_conj_list o dnf_fm"

lemma dnf_and_fm_induct[case_names DistribR DistribL NoDistrib]:
  fixes φ⇩1 φ⇩2 :: "'a fm"
  assumes "⋀φ⇩1 φ⇩2 ψ. ⟦P φ⇩1 ψ; P φ⇩2 ψ⟧ ⟹ P (Or φ⇩1 φ⇩2) ψ"
  assumes "⋀ψ φ⇩1 φ⇩2. ⟦P ψ φ⇩1; P ψ φ⇩2; ∄x y. ψ = Or x y⟧ ⟹ P ψ (Or φ⇩1 φ⇩2)"
  assumes "⋀φ⇩1 φ⇩2. ⟦∄x y. φ⇩1 = Or x y; ∄x y. φ⇩2 = Or x y⟧ ⟹ P φ⇩1 φ⇩2"
  shows "P φ⇩1 φ⇩2"
  apply(induction φ⇩1 φ⇩2 rule: dnf_and_fm.induct)
  using assms by simp_all

fun is_conj :: "'a fm ⇒ bool" where
  "is_conj (And φ⇩1 φ⇩2) ⟷ is_conj φ⇩1 ∧ is_conj φ⇩2" |
  "is_conj (Or _ _) ⟷ False" |
  "is_conj (Neg _) ⟷ False" |
  "is_conj (Atom _) ⟷ True"

fun dnormal :: "'a fm ⇒ bool" where
  "dnormal (Or φ⇩1 φ⇩2) ⟷ dnormal φ⇩1 ∧ dnormal φ⇩2" |
  "dnormal (And φ⇩1 φ⇩2) ⟷ is_conj (And φ⇩1 φ⇩2)" |
  "dnormal (Neg _) ⟷ False" |
  "dnormal _ ⟷ True"

fun nfree :: "'a fm ⇒ bool" where
  "nfree (Atom φ) ⟷ True" |
  "nfree (And φ⇩1 φ⇩2) ⟷ nfree φ⇩1 ∧ nfree φ⇩2" |
  "nfree (Or φ⇩1 φ⇩2) ⟷ nfree φ⇩1 ∧ nfree φ⇩2" |
  "nfree (Neg _) ⟷ False"

lemma atoms_amap⇩f⇩m: "atoms (amap⇩f⇩m f φ) = (⋃a ∈ atoms φ. atoms (f a))"
  by (induction φ) auto

lemma atoms_dnf_and_fm[simp]: "atoms (dnf_and_fm φ⇩1 φ⇩2) = atoms (And φ⇩1 φ⇩2)"
  by (induction φ⇩1 φ⇩2 rule: dnf_and_fm.induct) auto

lemma atoms_dnf_fm[simp]: "atoms (dnf_fm φ) = atoms φ"
  using atoms_dnf_and_fm
  by (induction φ) auto

lemma atoms_conj_list: "is_conj φ ⟹ set (conj_list φ) = atoms φ"
  by (induction φ) auto

lemma atoms_disj_conj_list: "dnormal φ ⟹ (⋃A ∈ set (disj_conj_list φ). set A) = atoms φ"
  by (induction φ) (auto simp: atoms_conj_list)

lemma nfree_amap⇩f⇩m: "(⋀x. nfree (f x)) ⟹ nfree (amap⇩f⇩m f φ) = nfree φ"
  by (induction φ) auto

lemma nfree_amap⇩f⇩mI: "(⋀x. nfree (f x)) ⟹ nfree φ ⟹ nfree (amap⇩f⇩m f φ)"
  using nfree_amap⇩f⇩m by blast

lemma nfree_dnf_and_fm[simp]: "nfree (dnf_and_fm φ⇩1 φ⇩2) = nfree (And φ⇩1 φ⇩2)"
  apply(induction "φ⇩1" "φ⇩2" rule: dnf_and_fm.induct)
  by auto

lemma nfree_dnf_fm[simp]: "nfree (dnf_fm φ) = nfree φ"
  apply(induction φ)
  by auto

lemma dnormal_conj: "is_conj φ ⟹ dnormal φ"
  apply(induction φ)
  by auto

lemma dnormal_dnf_and_fm:
  assumes "nfree φ⇩1" "nfree φ⇩2"
    and "dnormal φ⇩1" "dnormal φ⇩2"
  shows "dnormal (dnf_and_fm φ⇩1 φ⇩2)"
  using assms
proof(induction φ⇩1 φ⇩2 rule: dnf_and_fm_induct)
  case (DistribL ψ φ⇩1 φ⇩2)
  then show ?case
    apply(cases ψ) by auto
next
  case (NoDistrib φ⇩1 φ⇩2)
  then show ?case
    apply(cases φ⇩1; cases φ⇩2) by auto
qed simp

lemma dnormal_dnf_fm[intro]: "nfree φ ⟹ dnormal (dnf_fm φ)"
  apply(induction φ) by (auto simp: dnormal_dnf_and_fm)

fun "interp" :: "('model ⇒ 'a ⇒ bool) ⇒ 'model ⇒ 'a fm ⇒ bool" where
  "interp I⇩a M (Atom a) = I⇩a M a" |
  "interp I⇩a M (And φ⇩1 φ⇩2) = (interp I⇩a M φ⇩1 ∧ interp I⇩a M φ⇩2)" |
  "interp I⇩a M (Or φ⇩1 φ⇩2) = (interp I⇩a M φ⇩1 ∨ interp I⇩a M φ⇩2)" |
  "interp I⇩a M (Neg φ) = (¬ interp I⇩a M φ)"

locale ATOM =
  fixes I⇩a :: "'model ⇒ 'a ⇒ bool"
begin

abbreviation I where "I ≡ interp I⇩a"

lemma I_amap⇩f⇩m: "∀x. I M (h x) = I⇩a M x ⟹ I M (amap⇩f⇩m h φ) = I M φ"
  by (induction φ) auto

lemma I_dnf_and_fm: "nfree φ⇩1 ⟹ nfree φ⇩2 ⟹ I M (dnf_and_fm φ⇩1 φ⇩2) = I M (And φ⇩1 φ⇩2)"
  apply(induction φ⇩1 φ⇩2 rule: dnf_and_fm.induct)
  by auto

lemma I_dnf_fm: "nfree φ ⟹ I M (dnf_fm φ) = I M φ"
  apply(induction φ)
  by (auto simp: I_dnf_and_fm)

lemma I_conj_list: "is_conj φ ⟹ (∀a ∈ set (conj_list φ). I⇩a M a) = I M φ"
  apply(induction φ)
  by auto

lemma I_disj_conj_list: "dnormal φ ⟹
  (∃as ∈ set (disj_conj_list φ). ∀a ∈ set as. I⇩a M a) = I M φ"
proof(induction φ)
  case (And φ1 φ2)
  hence "is_conj (And φ1 φ2)" by simp
  from I_conj_list[OF this] show ?case by simp
qed auto

lemma I_dnf: "nfree φ ⟹ (∃as ∈ set (dnf φ). ∀a ∈ set as. I⇩a M a) = I M φ"
  unfolding dnf_def
  using I_disj_conj_list[OF dnormal_dnf_fm] I_dnf_fm by simp

end

locale nnf = ATOM I⇩a for I⇩a :: "'model ⇒ 'a ⇒ bool" +
  fixes aneg :: "'a ⇒ 'a fm"
  assumes nfree_aneg: "nfree (aneg a)"
  assumes I⇩a_aneg: "interp I⇩a M (aneg a) = (¬ I⇩a M a)"
begin

fun nnf :: "'a fm ⇒ 'a fm" where
  "nnf (And φ⇩1 φ⇩2) = And (nnf φ⇩1) (nnf φ⇩2)" |
  "nnf (Or φ⇩1 φ⇩2) = Or (nnf φ⇩1) (nnf φ⇩2)" |
  "nnf (Neg (Neg φ)) = (nnf φ)" |
  "nnf (Neg (And φ⇩1 φ⇩2)) = (Or (nnf (Neg φ⇩1)) (nnf (Neg φ⇩2)))" |
  "nnf (Neg (Or φ⇩1 φ⇩2)) = (And (nnf (Neg φ⇩1)) (nnf (Neg φ⇩2)))" |
  "nnf (Neg (Atom a)) = aneg a" |
  "nnf φ = φ"

lemma nfree_nnf: "nfree (nnf φ)"
  apply(induction φ rule: nnf.induct)
  using nfree_aneg by auto

lemma I_nnf: "I M (nnf φ) = I M φ"
  by (induction rule: nnf.induct) (simp_all add: I⇩a_aneg)

end

type_synonym var = int

datatype trm = Const String.literal | App trm trm | Var var

datatype prf_trm =
  PThm String.literal |
  Appt prf_trm trm |
  AppP prf_trm prf_trm |
  AbsP trm prf_trm |
  Bound trm |
  Conv trm prf_trm prf_trm

abbreviation "AppPs p ps ≡ foldl AppP p ps"
abbreviation "AppPThm s ≡ AppP (PThm s)"
abbreviation "ApptThm s ≡ Appt (PThm s)"
abbreviation "AppPThms s ps ≡ AppPs (PThm s) ps"

abbreviation "AtomConv ≡ AppPThm (STR ''atom_conv'')"
abbreviation "NegAtomConv ≡ AppPThm (STR ''neg_atom_conv'')"
abbreviation "BinopConv c1 c2 ≡
  AppPThms (STR ''combination_conv'') [AppPThm (STR ''arg_conv'') c1, c2]"
abbreviation "ArgConv ≡ AppPThm (STR ''arg_conv'')"
abbreviation "NegNegConv ≡ PThm (STR ''not_not_conv'')"
abbreviation "NegAndConv ≡ PThm (STR ''de_Morgan_conj_conv'')"
abbreviation "NegOrConv ≡ PThm (STR ''de_Morgan_disj_conv'')"
abbreviation "ConjDisjDistribRConv ≡ PThm (STR ''conj_disj_distribR_conv'')"
abbreviation "ConjDisjDistribLConv ≡ PThm (STR ''conj_disj_distribL_conv'')"
abbreviation "ThenConv c1 c2 ≡ AppPThms (STR ''then_conv'') [c1, c2]"
abbreviation "AllConv ≡ PThm (STR ''all_conv'')"

fun trm_of_fm :: "('a ⇒ trm) ⇒ 'a fm ⇒ trm" where
"trm_of_fm f (Atom a) = f a" |
"trm_of_fm f (And φ⇩1 φ⇩2) = App (App (Const (STR ''conj'')) (trm_of_fm f φ⇩1)) (trm_of_fm f φ⇩2)" |
"trm_of_fm f (Or φ⇩1 φ⇩2) = App (App (Const (STR ''disj'')) (trm_of_fm f φ⇩1)) (trm_of_fm f φ⇩2)" |
"trm_of_fm f (Neg φ) = App (Const (STR ''Not'')) (trm_of_fm f φ)"

fun thm_free :: "String.literal ⇒ prf_trm ⇒ bool" where
"thm_free a (PThm n) ⟷ a ≠ n" |
"thm_free a (AppP p1 p2) ⟷ thm_free a p1 ∧ thm_free a p2" |
"thm_free a (Appt p _) ⟷ thm_free a p"

abbreviation "a_conv_free ≡ thm_free (STR ''atom_conv'')"
abbreviation "aneg_conv_free ≡ thm_free (STR ''neg_atom_conv'')"

locale fm_conv_system = ATOM I⇩a for I⇩a :: "'model ⇒ 'a ⇒ bool" +
  fixes M :: 'model
  fixes a_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool"
  fixes aneg_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool"
begin

inductive convs :: "prf_trm ⇒ 'a fm ⇒ 'a fm ⇒ bool"
  ("_ : _ ≡⇩f⇩m _" [] 60) where
  andC[simplified]: "p1 : A ≡⇩f⇩m C ⟹ p2 : B ≡⇩f⇩m D ⟹ BinopConv p1 p2 : And A B ≡⇩f⇩m And C D" |
  orC[simplified]: "p1 : A ≡⇩f⇩m C ⟹ p2 : B ≡⇩f⇩m D  ⟹ BinopConv p1 p2 : Or A B ≡⇩f⇩m Or C D" |
  negC: "p : A ≡⇩f⇩m B  ⟹ ArgConv p : Neg A ≡⇩f⇩m Neg B" |
  negNegC: "NegNegConv : Neg (Neg A) ≡⇩f⇩m A" |
  negAndC: "NegAndConv : Neg (And A B) ≡⇩f⇩m Or (Neg A) (Neg B)" |
  negOrC: "NegOrConv : Neg (Or A B) ≡⇩f⇩m And (Neg A) (Neg B)" |
  AtomC: "a_convs p a B⟹ AtomConv p : Atom a ≡⇩f⇩m B" |
  negAtomC: "aneg_convs p a B ⟹ NegAtomConv p : Neg (Atom a) ≡⇩f⇩m B" |
  conjDisjDistribRC: "ConjDisjDistribRConv : And (Or A B) C ≡⇩f⇩m Or (And A C) (And B C)" |
  conjDisjDistribLC: "ConjDisjDistribLConv : And A (Or B C) ≡⇩f⇩m Or (And A B) (And A C)" |
  thenC[simplified]: "p1 : A ≡⇩f⇩m B ⟹ p2 : B ≡⇩f⇩m C ⟹ ThenConv p1 p2 : A ≡⇩f⇩m C" |
  allC: "AllConv : A ≡⇩f⇩m A"

lemma convs_sound:
  assumes "p : φ ≡⇩f⇩m ψ"
  assumes "⋀ap a φ⇩a. a_convs ap a φ⇩a ⟹ I⇩a M a = I M φ⇩a"
  assumes "⋀ap a φ⇩a. aneg_convs ap a φ⇩a ⟹ ¬ (I⇩a M a) = I M φ⇩a"
  shows "I M φ = I M ψ"
  using assms
  apply(induction p φ ψ rule: convs.induct) by auto

lemma convs_aneg_conv_free_sound:
  assumes "p : φ ≡⇩f⇩m ψ"
  assumes "aneg_conv_free p" "⋀ap a φ⇩a. a_convs ap a φ⇩a ⟹ I⇩a M a = I M φ⇩a"
  shows "I M φ = I M ψ"
  using assms
  apply (induction p φ ψ rule: convs.induct) by auto

lemma convs_a_conv_free_sound:
  assumes "p : φ ≡⇩f⇩m ψ"
  assumes "a_conv_free p" "⋀ap a φ⇩a. aneg_convs ap a φ⇩a ⟹ ¬ (I⇩a M a) = I M φ⇩a"
  shows "I M φ = I M ψ"
  using assms
  apply(induction p φ ψ rule: convs.induct) by auto

lemma convs_atom_conv_free_sound:
  assumes "p : φ ≡⇩f⇩m ψ"
  assumes "a_conv_free p" "aneg_conv_free p"
  shows "I M φ = I M ψ"
  using assms
  apply(induction p φ ψ rule: convs.induct) by auto

end

locale fm_conv = fm_conv_system I⇩a M a_convs aneg_convs for
  I⇩a :: "'model ⇒ 'a ⇒ bool" and
  M :: 'model and
  a_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" and
  aneg_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" +

  fixes conv :: "'a fm ⇒ 'a fm"
  fixes conv_prf :: "'a fm ⇒ prf_trm"
  assumes conv_convs: "conv_prf φ : φ ≡⇩f⇩m (conv φ) ⟹ I M φ = I M (conv φ)"
begin
end

fun amap⇩f⇩m_prf :: "('a ⇒ prf_trm) ⇒ 'a fm ⇒ prf_trm" where
"amap⇩f⇩m_prf ap (Atom a) = AtomConv (ap a)" |
"amap⇩f⇩m_prf ap (And φ⇩1 φ⇩2) = BinopConv (amap⇩f⇩m_prf ap φ⇩1) (amap⇩f⇩m_prf ap φ⇩2)" |
"amap⇩f⇩m_prf ap (Or φ⇩1 φ⇩2) = BinopConv (amap⇩f⇩m_prf ap φ⇩1) (amap⇩f⇩m_prf ap φ⇩2)" |
"amap⇩f⇩m_prf ap (Neg φ) = ArgConv (amap⇩f⇩m_prf ap φ)"

locale amap⇩f⇩m_conv = fm_conv_system I⇩a M a_convs aneg_convs for
  I⇩a :: "'model ⇒ 'a ⇒ bool" and
  M :: 'model and
  a_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" and
  aneg_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" +
  
  fixes atom_conv :: "'a ⇒ 'a fm"
  fixes atom_conv_prf :: "'a ⇒ prf_trm"
  assumes atom_conv_sound: "I M (atom_conv a) = I⇩a M a"
  assumes aneg_conv_free_atom_conv_prf: "aneg_conv_free (atom_conv_prf a)"
  assumes atom_conv_prf_convs: "a_convs (atom_conv_prf a) a (atom_conv a)"
begin

lemma aneg_conv_free_amap⇩f⇩m_prf: "aneg_conv_free (amap⇩f⇩m_prf atom_conv_prf φ)"
  using aneg_conv_free_atom_conv_prf by (induction φ) auto

lemma amap⇩f⇩m_conv_convs: "amap⇩f⇩m_prf atom_conv_prf A : A ≡⇩f⇩m amap⇩f⇩m atom_conv A"
  apply (induction A)
  using atom_conv_prf_convs AtomC andC orC negC by fastforce+

lemma I_amap⇩f⇩m_conv: "I M (amap⇩f⇩m atom_conv A) = I M A"
  by (simp add: ATOM.I_amap⇩f⇩m atom_conv_sound)

sublocale fm_conv: fm_conv I⇩a M a_convs aneg_convs "amap⇩f⇩m atom_conv" "amap⇩f⇩m_prf atom_conv_prf"
  using I_amap⇩f⇩m_conv by unfold_locales blast

end
  

fun dnf_and_fm_prf :: "'a fm ⇒ 'a fm ⇒ prf_trm" where
  "dnf_and_fm_prf (Or φ⇩1 φ⇩2) ψ = ThenConv ConjDisjDistribRConv
    (BinopConv (dnf_and_fm_prf φ⇩1 ψ) (dnf_and_fm_prf φ⇩2 ψ))" |
  "dnf_and_fm_prf ψ (Or φ⇩1 φ⇩2) = ThenConv ConjDisjDistribLConv
    (BinopConv (dnf_and_fm_prf ψ φ⇩1) (dnf_and_fm_prf ψ φ⇩2))" |
  "dnf_and_fm_prf φ⇩1 φ⇩2 = AllConv"

fun dnf_fm_prf :: "'a fm ⇒ prf_trm" where
  "dnf_fm_prf (And φ⇩1 φ⇩2) = ThenConv (BinopConv (dnf_fm_prf φ⇩1) (dnf_fm_prf φ⇩2))
    (dnf_and_fm_prf (dnf_fm φ⇩1) (dnf_fm φ⇩2))" |
  "dnf_fm_prf (Or φ⇩1 φ⇩2) = BinopConv (dnf_fm_prf φ⇩1) (dnf_fm_prf φ⇩2)" |
  "dnf_fm_prf _ = AllConv"


locale dnf_fm_conv = fm_conv_system
begin

lemma dnf_and_fm_convs: "dnf_and_fm_prf φ⇩1 φ⇩2 : And φ⇩1 φ⇩2 ≡⇩f⇩m dnf_and_fm φ⇩1 φ⇩2"
proof (induction φ⇩1 φ⇩2 rule: dnf_and_fm_induct)
  case (DistribR φ⇩1 φ⇩2 ψ)
  then show ?case
    using thenC[OF conjDisjDistribRC orC[OF DistribR.IH]] by simp
next
  case (DistribL ψ φ⇩1 φ⇩2)
  then show ?case
    using thenC[OF conjDisjDistribLC orC[OF DistribL.IH]] by (cases ψ) simp_all
next
  case (NoDistrib φ⇩1 φ⇩2)
  then show ?case
    apply(cases φ⇩1; cases φ⇩2) by (simp_all add: allC)
qed

lemma a_conv_free_dnf_and_fm_prf: "a_conv_free (dnf_and_fm_prf φ⇩1 φ⇩2)"
  by (induction φ⇩1 φ⇩2 rule: dnf_and_fm_prf.induct) auto

lemma aneg_conv_free_dnf_and_fm_prf: "aneg_conv_free (dnf_and_fm_prf φ⇩1 φ⇩2)"
  by (induction φ⇩1 φ⇩2 rule: dnf_and_fm_prf.induct) auto

lemma dnf_fm_convs: "dnf_fm_prf φ : φ ≡⇩f⇩m dnf_fm φ"
proof(induction φ)
  case (And φ1 φ2)
  then show ?case
    using thenC[where ?B="And (dnf_fm φ1) (dnf_fm φ2)", OF andC]
    by (simp add: dnf_and_fm_convs)
qed (auto simp: convs.intros)

lemma a_conv_free_dnf_fm_prf: "a_conv_free (dnf_fm_prf φ)"
  using a_conv_free_dnf_and_fm_prf
  by (induction φ rule: dnf_fm_prf.induct) auto

lemma aneg_conv_free_dnf_fm_prf: "aneg_conv_free (dnf_fm_prf φ)"
  using aneg_conv_free_dnf_and_fm_prf
  by (induction φ rule: dnf_fm_prf.induct) auto

sublocale fm_conv: fm_conv I⇩a M a_convs aneg_convs dnf_fm dnf_fm_prf
  apply(unfold_locales)
  using convs_atom_conv_free_sound[OF _ a_conv_free_dnf_fm_prf aneg_conv_free_dnf_fm_prf] .

end


locale nnf_conv = nnf I⇩a aneg + fm_conv_system I⇩a M a_convs aneg_convs for
  I⇩a :: "'model ⇒ 'a ⇒ bool" and aneg :: "'a ⇒ 'a fm" and
  M :: 'model and
  a_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" and
  aneg_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" +

  fixes aneg_prf :: "'a ⇒ prf_trm"
  assumes a_conv_free_aneg_prf: "a_conv_free (aneg_prf a)"
  assumes aneg_convs: "aneg_convs (aneg_prf a) a (aneg a)"
  assumes a_convs_sound: "aneg_convs p a A ⟹ (¬ I⇩a M a) = I M A"
begin

fun nnf_prf :: "'a fm ⇒ prf_trm" where
  "nnf_prf (And φ⇩1 φ⇩2) = BinopConv (nnf_prf φ⇩1) (nnf_prf φ⇩2)" |
  "nnf_prf (Or φ⇩1 φ⇩2) = BinopConv (nnf_prf φ⇩1) (nnf_prf φ⇩2)" |
  "nnf_prf (Neg (Neg φ)) = ThenConv NegNegConv (nnf_prf φ)" |
  "nnf_prf (Neg (And φ⇩1 φ⇩2)) = ThenConv NegAndConv
    (BinopConv (nnf_prf (Neg φ⇩1)) (nnf_prf (Neg φ⇩2)))" |
  "nnf_prf (Neg (Or φ⇩1 φ⇩2)) = ThenConv NegOrConv
    (BinopConv (nnf_prf (Neg φ⇩1)) (nnf_prf (Neg φ⇩2)))" |
  "nnf_prf (Neg (Atom a)) = NegAtomConv (aneg_prf a)" |
  "nnf_prf φ = AllConv"

lemma a_conv_free_nnf_prf: "a_conv_free (nnf_prf φ)"
  using a_conv_free_aneg_prf
  apply(induction φ rule: nnf_prf.induct) by auto

sublocale fm_conv: fm_conv I⇩a M a_convs aneg_convs nnf nnf_prf
  using a_convs_sound a_conv_free_nnf_prf
  apply(unfold_locales)
  by (simp add: I_nnf)

lemma nnf_convs: "nnf_prf φ : φ ≡⇩f⇩m nnf φ"
proof(induction φ rule: nnf.induct)
  case (3 φ)
  then show ?case 
    by (auto simp: convs.intros intro: thenC[where ?B=φ])
next
  case (4 φ⇩1 φ⇩2)
  then show ?case
    by (auto simp: convs.intros intro: thenC[where ?B="Or (Neg φ⇩1) (Neg φ⇩2)"])
next
  case (5 φ⇩1 φ⇩2)
  then show ?case
    by (auto simp: convs.intros intro: thenC[where ?B="And (Neg φ⇩1) (Neg φ⇩2)"])
qed (auto simp: aneg_convs convs.intros)

end

definition "Atoms A ≡ {a |a. Atom a ∈ A}"

lemma Atoms_Un[simp]: "Atoms (A ∪ B) = Atoms A ∪ Atoms B"
  unfolding Atoms_def by auto

lemma Atoms_mono: "A ⊆ B ⟹ Atoms A ⊆ Atoms B"
  unfolding Atoms_def by auto

abbreviation "ConjE trm_of c d p ≡
  AppPThms (STR ''conjE'') [Bound (trm_of (And c d)), AbsP (trm_of c) (AbsP (trm_of d) p)]"
abbreviation "DisjE trm_of c d p1 p2 ≡
  AppPThms (STR ''disjE'') [Bound (trm_of (Or c d)), AbsP (trm_of c) p1, AbsP (trm_of d) p2]"

locale prop_fm_system = fm_conv_system I⇩a M a_convs aneg_convs for 
    I⇩a :: "'model ⇒ 'a ⇒ bool" and
    M :: 'model and
    a_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" and
    aneg_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" +

  fixes atom_proves :: "'a set ⇒ prf_trm ⇒ 'a fm ⇒ bool"
  fixes trm_of_atom :: "'a ⇒ trm"
  assumes atom_proves_sound: "atom_proves A ap φ ⟹ ∀a ∈ A. I⇩a M a ⟹ I M φ"
  assumes atom_proves_weaken: "atom_proves A ap φ ⟹ A ⊆ B ⟹ atom_proves B ap φ"
  assumes convs_sound: "convs cp φ ψ ⟹ I M φ = I M ψ"
begin

abbreviation "trm_of ≡ trm_of_fm trm_of_atom"

inductive proves :: "'a fm set ⇒ prf_trm ⇒ 'a fm ⇒ bool"
  ("_ ⊢ _ : _" [] 50) where
  conjE[simplified]: "And c d ∈ A ⟹ insert c (insert d A) ⊢ p : φ
    ⟹ A ⊢ ConjE trm_of c d p : φ" |
  disjE[simplified]: "Or c d ∈ A ⟹ insert c A ⊢ p1 : φ ⟹ insert d A ⊢ p2 : φ
    ⟹ A ⊢ DisjE trm_of c d p1 p2 : φ" |
  conv[simplified]: "c ∈ A ⟹ cp : c ≡⇩f⇩m d ⟹ insert d A ⊢ p : φ
    ⟹ A ⊢ Conv (trm_of c) cp p : φ" |
  lift: "atom_proves (Atoms A) p φ ⟹ A ⊢ p : φ"

lemma lift2: "atom_proves A p φ ⟹ Atom ` A ⊢ p : φ"
  using proves.lift unfolding Atoms_def
  by (simp add: atom_proves_weaken subsetI)

lemma proves_sound: "A ⊢ p : φ ⟹ ∀α ∈ A. I M α ⟹ I M φ"
proof(induction A p φ rule: proves.induct)
  case (conv c A d cp p φ)
  then show ?case using convs_sound by fastforce
next
  case (lift A p a)
  then show ?case using atom_proves_sound unfolding Atoms_def by fastforce
qed fastforce+

lemma proves_contr:
  assumes "A ⊢ p : φ"
  assumes "¬ I M φ"
  obtains ψ where "ψ ∈ A" "¬ I M ψ"
  using assms proves_sound by blast

lemma proves_weaken_Un: "A ⊢ p : φ ⟹ A ∪ B ⊢ p : φ"
proof(induction A p φ arbitrary: B rule: proves.induct)
  case (lift A p φ)
  then have "atom_proves (Atoms (A ∪ B)) p φ"
    unfolding Atoms_def
    using atom_proves_weaken[where ?B="{a |a. Atom a ∈ A ∪ B}"] by auto
  then show ?case by (auto simp: proves.lift)
qed (fastforce intro: proves.intros)+

lemma proves_weaken: "A ⊢ p : φ ⟹ A ⊆ B ⟹ B ⊢ p : φ"
  using proves_weaken_Un unfolding subset_Un_eq by metis

end

context
  fixes trm_of_atom :: "'a ⇒ trm"
begin

fun from_conj_prf :: "prf_trm ⇒ 'a fm ⇒ prf_trm" where
"from_conj_prf p (And a b) = ConjE (trm_of_fm trm_of_atom) a b (from_conj_prf (from_conj_prf p b) a)" |
"from_conj_prf p (Atom a) = p"

end

context
  fixes trm_of_atom :: "'a ⇒ trm"
  fixes contr_atom_prf :: "'a list ⇒ prf_trm option"
begin

fun contr_fm_prf :: "'a fm ⇒ prf_trm option" where
"contr_fm_prf (Or c d) =
  (case contr_fm_prf c of
    Some p1 ⇒ map_option (DisjE (trm_of_fm trm_of_atom) c d p1) (contr_fm_prf d)
  | _ ⇒ None)" |
"contr_fm_prf (And a b) =
  (case contr_atom_prf (conj_list (And a b)) of
    None ⇒ None
  | Some p ⇒ Some (from_conj_prf trm_of_atom p (And a b)))" |
"contr_fm_prf (Atom a) = contr_atom_prf [a]"

end

lemma (in prop_fm_system) from_conj_prf_proves:
  assumes "is_conj φ"
  assumes proves_conj_list: "Atom ` set (conj_list φ) ∪ A ⊢ p : ψ"
  shows "insert φ A ⊢ from_conj_prf trm_of_atom p φ : ψ"
  using assms
proof(induction p φ arbitrary: A rule: from_conj_prf.induct[of _ trm_of_atom])
  case (1 p a b)
  from "1.IH"[where ?A="Atom ` set (conj_list a) ∪ A"] "1.prems"
  have "Atom ` set (conj_list a) ∪ insert b A ⊢ from_conj_prf trm_of_atom p b : ψ"
    by (simp add: image_Un Un_commute sup_left_commute)
  from "1.IH"(2)[OF _ this] "1.prems"
  have "insert a (insert b (insert (And a b) A))
    ⊢ from_conj_prf trm_of_atom (from_conj_prf trm_of_atom p b) a : ψ"
    using proves_weaken[where ?B="insert a (insert b (insert (And a b) A))"]
    by auto
  with "1.prems" show ?case using proves.conjE by simp
next
  case (2 p a)
  then show ?case
    using proves_weaken_Un[where ?B="A" and ?A="{Atom a}"] by simp
qed simp_all


locale contr_fm = prop_fm_system I⇩a M a_convs aneg_convs atom_proves for 
    I⇩a :: "'model ⇒ 'a ⇒ bool" and
    M :: 'model and
    a_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" and
    aneg_convs :: "prf_trm ⇒ 'a ⇒ 'a fm ⇒ bool" and
    atom_proves :: "'a set ⇒ prf_trm ⇒ 'a fm ⇒ bool" +
    
  fixes contr_atom_prf :: "'a list ⇒ prf_trm option"
  fixes Fls :: 'a
  assumes I⇩a_Fls: "¬ I⇩a M Fls"
  assumes contr_atom_prf_proves: "contr_atom_prf A = Some p ⟹ atom_proves (set A) p (Atom Fls)"
begin

lemma contr_fm_prf_proves:
  assumes "dnormal φ"
  assumes "contr_fm_prf trm_of_atom contr_atom_prf φ = Some p"
  shows "insert φ A ⊢ p : Atom Fls"
  using assms
proof(induction φ arbitrary: p)
  case (Atom x)
  then show ?case
    using contr_atom_prf_proves[THEN lift2] proves_weaken_Un by fastforce
next
  case (And φ1 φ2)
  then obtain pa where
    p: "p = from_conj_prf trm_of_atom pa (And φ1 φ2)" and
    pa: "contr_atom_prf (conj_list (And φ1 φ2)) = Some pa"
    by (auto split: option.splits)
  with contr_atom_prf_proves[OF pa]
  have "Atom ` set (conj_list (And φ1 φ2)) ∪ A ⊢ pa : (Atom Fls)"
    using lift2 proves_weaken_Un by blast
  from from_conj_prf_proves[OF _ this] ‹dnormal (And φ1 φ2)› show ?case
    unfolding p by simp
next
  case (Or φ1 φ2)
  then obtain p1 p2 where
    p: "p = DisjE trm_of φ1 φ2 p1 p2" and
    "insert φ1 A ⊢ p1 : Atom Fls" "insert φ2 A ⊢ p2 : Atom Fls"
    by (auto split: option.splits)
  then have
    "insert φ1 (insert (Or φ1 φ2) A) ⊢ p1 : Atom Fls"
    "insert φ2 (insert (Or φ1 φ2) A) ⊢ p2 : Atom Fls"
    by (metis insert_commute proves_weaken subset_insertI)+
  from proves.disjE[OF insertI1 this] p show ?case by simp
qed simp

lemma contr_fm_prf_sound:
  assumes "dnormal φ"
  assumes "contr_fm_prf trm_of_atom contr_atom_prf φ = Some p"
  shows "¬ I M φ"
  using contr_fm_prf_proves[OF assms] I⇩a_Fls proves_sound by fastforce

lemma contr_dnf_fm_prf_proves:
  assumes "nfree φ"
  assumes "map_option (Conv (trm_of_fm trm_of_atom φ) (dnf_fm_prf φ)) 
    (contr_fm_prf trm_of_atom contr_atom_prf (dnf_fm φ)) = Some p"
  shows "insert φ A ⊢ p: Atom Fls"
  using assms
  using contr_fm_prf_proves conv[OF _ dnf_fm_conv.dnf_fm_convs]
  by blast

end

lemma (in ATOM) Ex_conj_contr_atom_prf_None:
  assumes "dnormal φ"
  assumes "contr_fm_prf trm_of_atom contr_atom_prf φ = None"
  shows "∃A ∈ set (disj_conj_list φ). contr_atom_prf A = None"
  using assms
  by (induction φ) (auto split: option.splits)

lemma (in ATOM) I_fm_if_I_conj:
  assumes "dnormal φ"
  assumes "A ∈ set (disj_conj_list φ)" "∀a ∈ set A. I⇩a M a"
  shows "I M φ"
  using assms
proof(induction φ)
  case (And φ1 φ2)
  then show ?case using I_disj_conj_list by blast
qed auto

end