Theory MLSS_Proc_Code

theory MLSS_Proc_Code
  imports MLSS_Proc MLSS_Typing_Urelems "Fresh_Identifiers.Fresh_Nat" "List-Index.List_Index"
begin

section ‹An Executable Specification of the Procedure›

instantiation nat :: default
begin
definition "default_nat = (0::nat)"

instance ..
end

fun subterms_term_list :: "'a pset_term ⇒ 'a pset_term list"  where
  "subterms_term_list (∅ n) = [∅ n]"
| "subterms_term_list (Var i) = [Var i]"
| "subterms_term_list (t1 ⊔⇩s t2) = [t1 ⊔⇩s t2] @ subterms_term_list t1 @ subterms_term_list t2"
| "subterms_term_list (t1 ⊓⇩s t2) = [t1 ⊓⇩s t2] @ subterms_term_list t1 @ subterms_term_list t2"
| "subterms_term_list (t1 -⇩s t2) = [t1 -⇩s t2] @ subterms_term_list t1 @ subterms_term_list t2"
| "subterms_term_list (Single t) = [Single t] @ subterms_term_list t"

fun subterms_atom_list :: "'a pset_atom ⇒ 'a pset_term list"  where
  "subterms_atom_list (t1 ∈⇩s t2) = subterms_term_list t1 @ subterms_term_list t2"
| "subterms_atom_list (t1 =⇩s t2) = subterms_term_list t1 @ subterms_term_list t2"

fun atoms_list :: "'a pset_fm ⇒ 'a pset_atom list" where
  "atoms_list (Atom a) = [a]"
| "atoms_list (And p q) = atoms_list p @ atoms_list q"
| "atoms_list (Or p q) = atoms_list p @ atoms_list q"
| "atoms_list (Neg p) = atoms_list p"

definition subterms_fm_list :: "'a pset_fm ⇒ 'a pset_term list" where
 "subterms_fm_list φ ≡ concat (map subterms_atom_list (atoms_list φ))"

definition subterms_branch_list :: "'a branch ⇒ 'a pset_term list" where
  "subterms_branch_list b ≡ concat (map subterms_fm_list b)"

lemma set_subterms_term_list[simp]:
  "set (subterms_term_list t) = subterms t"
  by (induction t) auto

lemma set_subterms_atom_list[simp]:
  "set (subterms_atom_list t) = subterms t"
  by (cases t) auto

lemma set_atoms_list[simp]:
  "set (atoms_list φ) = atoms φ"
  by (induction φ) auto

lemma set_subterms_fm_list[simp]:
  "set (subterms_fm_list φ) = subterms_fm φ"
  unfolding subterms_fm_list_def subterms_fm_def by simp

lemma set_subterms_branch_list[simp]:
  "set (subterms_branch_list b) = subterms b"
  unfolding subterms_branch_list_def subterms_branch_def by simp

fun lexpand_fm1 :: "'a branch ⇒ 'a pset_fm ⇒ 'a branch list" where
  "lexpand_fm1 b (And p q) = [[p, q]]"
| "lexpand_fm1 b (Neg (Or p q)) = [[Neg p, Neg q]]"
| "lexpand_fm1 b (Or p q) =
    (if Neg p ∈ set b then [[q]] else []) @
    (if Neg q ∈ set b then [[p]] else [])"
| "lexpand_fm1 b (Neg (And p q)) =
    (if p ∈ set b then [[Neg q]] else []) @
    (if q ∈ set b then [[Neg p]] else [])"
| "lexpand_fm1 b (Neg (Neg p)) = [[p]]"
| "lexpand_fm1 b _ = []"

definition "lexpand_fm b ≡ concat (map (lexpand_fm1 b) b)"

lemma lexpand_fm_if_lexpands_fm:
  "lexpands_fm b' b ⟹ b' ∈ set (lexpand_fm b)"
  apply(induction rule: lexpands_fm.induct)
        apply(force simp: lexpand_fm_def)+
  done

lemma lexpands_fm_if_lexpand_fm1: 
  "b' ∈ set (lexpand_fm1 b p) ⟹ p ∈ set b ⟹ lexpands_fm b' b"
  apply(induction b p rule: lexpand_fm1.induct)
        apply(auto simp: lexpands_fm.intros)
  done

lemma lexpands_fm_if_lexpand_fm:
  "b' ∈ set (lexpand_fm b) ⟹ lexpands_fm b' b"
  using lexpands_fm_if_lexpand_fm1 unfolding lexpand_fm_def by auto

fun lexpand_un1 :: "'a branch ⇒ 'a pset_fm ⇒ 'a branch list" where
  "lexpand_un1 b (AF (s ∈⇩s t)) =
    [[AF (s ∈⇩s t ⊔⇩s t1)]. AF (s' ∈⇩s t1) ← b, s' = s, t ⊔⇩s t1 ∈ subterms (last b)] @
    [[AF (s ∈⇩s t1 ⊔⇩s t)]. AF (s' ∈⇩s t1) ← b, s' = s, t1 ⊔⇩s t ∈ subterms (last b)] @ 
    (case t of
      t1 ⊔⇩s t2 ⇒ [[AF (s ∈⇩s t1), AF (s ∈⇩s t2)]]
    | _ ⇒ [])"
| "lexpand_un1 b (AT (s ∈⇩s t)) =
    [[AT (s ∈⇩s t ⊔⇩s t2)]. t1 ⊔⇩s t2 ← subterms_fm_list (last b), t1 = t] @
    [[AT (s ∈⇩s t1 ⊔⇩s t)]. t1 ⊔⇩s t2 ← subterms_fm_list (last b), t2 = t] @
    (case t of
      t1 ⊔⇩s t2 ⇒ (if AF (s ∈⇩s t1) ∈ set b then [[AT (s ∈⇩s t2)]] else []) @
                  (if AF (s ∈⇩s t2) ∈ set b then [[AT (s ∈⇩s t1)]] else [])
    | _ ⇒ [])"
| "lexpand_un1 _ _ = []"

definition "lexpand_un b ≡ concat (map (lexpand_un1 b) b)"

lemma lexpand_un_if_lexpands_un:
  "lexpands_un b' b ⟹ b' ∈ set (lexpand_un b)"
  apply(induction rule: lexpands_un.induct)
       apply(force simp: lexpand_un_def)+
  done

lemma lexpands_un_if_lexpand_un1:
  "b' ∈ set (lexpand_un1 b l) ⟹ l ∈ set b ⟹ lexpands_un b' b"
  apply(induction b l rule: lexpand_un1.induct)
          apply(auto simp: lexpands_un.intros)
  done

lemma lexpands_un_if_lexpand_un:
  "b' ∈ set (lexpand_un b) ⟹ lexpands_un b' b"
  unfolding lexpand_un_def using lexpands_un_if_lexpand_un1 by auto

fun lexpand_int1 :: "'a branch ⇒ 'a pset_fm ⇒ 'a branch list" where
  "lexpand_int1 b (AT (s ∈⇩s t)) =
    [[AT (s ∈⇩s t1 ⊓⇩s t)]. AT (s' ∈⇩s t1) ← b, s' = s, t1 ⊓⇩s t ∈ subterms (last b)] @
    [[AT (s ∈⇩s t ⊓⇩s t2)]. AT (s' ∈⇩s t2) ← b, s' = s, t ⊓⇩s t2 ∈ subterms (last b)] @
    (case t of t1 ⊓⇩s t2 ⇒ [[AT (s ∈⇩s t1), AT (s ∈⇩s t2)]] | _ ⇒ [])"
| "lexpand_int1 b (AF (s ∈⇩s t)) =
    [[AF (s ∈⇩s t ⊓⇩s t2)]. t1 ⊓⇩s t2 ← subterms_fm_list (last b), t1 = t] @
    [[AF (s ∈⇩s t1 ⊓⇩s t)]. t1 ⊓⇩s t2 ← subterms_fm_list (last b), t2 = t] @
    (case t of
      t1 ⊓⇩s t2 ⇒ (if AT (s ∈⇩s t1) ∈ set b then [[AF (s ∈⇩s t2)]] else []) @
                  (if AT (s ∈⇩s t2) ∈ set b then [[AF (s ∈⇩s t1)]] else [])
    | _ ⇒ [])"
| "lexpand_int1 _ _ = []"

definition "lexpand_int b ≡ concat (map (lexpand_int1 b) b)"

lemma lexpand_int_if_lexpands_int:
  "lexpands_int b' b ⟹ b' ∈ set (lexpand_int b)"
  apply(induction rule: lexpands_int.induct)
       apply(force simp: lexpand_int_def)+
  done

lemma lexpands_int_if_lexpand_int1:
  "b' ∈ set (lexpand_int1 b l) ⟹ l ∈ set b ⟹ lexpands_int b' b"
  apply(induction b l rule: lexpand_int1.induct)
          apply(auto simp: lexpands_int.intros)
  done

lemma lexpands_int_if_lexpand_int:
  "b' ∈ set (lexpand_int b) ⟹ lexpands_int b' b"
  unfolding lexpand_int_def using lexpands_int_if_lexpand_int1 by auto

fun lexpand_diff1 :: "'a branch ⇒ 'a pset_fm ⇒ 'a branch list" where
  "lexpand_diff1 b (AT (s ∈⇩s t)) =
    [[AT (s ∈⇩s t -⇩s t2)]. AF (s' ∈⇩s t2) ← b, s' = s, t -⇩s t2 ∈ subterms (last b)] @
    [[AF (s ∈⇩s t1 -⇩s t)]. AF (s' ∈⇩s t1) ← b, s' = s, t1 -⇩s t ∈ subterms (last b)] @
    [[AF (s ∈⇩s t1 -⇩s t)]. t1 -⇩s t2 ← subterms_fm_list (last b), t2 = t] @
    (case t of t1 -⇩s t2 ⇒ [[AT (s ∈⇩s t1), AF (s ∈⇩s t2)]] | _ ⇒ [])"
| "lexpand_diff1 b (AF (s ∈⇩s t)) =
    [[AF (s ∈⇩s t -⇩s t2)]. t1 -⇩s t2 ← subterms_fm_list (last b), t1 = t] @
    (case t of
      t1 -⇩s t2 ⇒ (if AT (s ∈⇩s t1) ∈ set b then [[AT (s ∈⇩s t2)]] else []) @
                  (if AF (s ∈⇩s t2) ∈ set b then [[AF (s ∈⇩s t1)]] else [])
    | _ ⇒ [])"
| "lexpand_diff1 _ _ = []"

definition "lexpand_diff b ≡ concat (map (lexpand_diff1 b) b)"

lemma lexpand_diff_if_lexpands_diff:
  "lexpands_diff b' b ⟹ b' ∈ set (lexpand_diff b)"
  apply(induction rule: lexpands_diff.induct)
       apply(force simp: lexpand_diff_def)+
  done

lemma lexpands_diff_if_lexpand_diff1:
  "b' ∈ set (lexpand_diff1 b l) ⟹ l ∈ set b ⟹ lexpands_diff b' b"
  apply(induction b l rule: lexpand_diff1.induct)
          apply(auto simp: lexpands_diff.intros)
  done

lemma lexpands_diff_if_lexpand_diff:
  "b' ∈ set (lexpand_diff b) ⟹ lexpands_diff b' b"
  unfolding lexpand_diff_def using lexpands_diff_if_lexpand_diff1 by auto

fun lexpand_single1 :: "'a branch ⇒ 'a pset_fm ⇒ 'a branch list" where
  "lexpand_single1 b (AT (s ∈⇩s Single t)) = [[AT (s =⇩s t)]]"
| "lexpand_single1 b (AF (s ∈⇩s Single t)) = [[AF (s =⇩s t)]]"
| "lexpand_single1 _ _ = []"

definition "lexpand_single b ≡
  [[AT (t1 ∈⇩s Single t1)]. Single t1 ← subterms_fm_list (last b)] @
  concat (map (lexpand_single1 b) b)"

lemma lexpand_single_if_lexpands_single:
  "lexpands_single b' b ⟹ b' ∈ set (lexpand_single b)"
  apply(induction rule: lexpands_single.induct)
       apply(force simp: lexpand_single_def)+
  done

lemma lexpands_single_if_lexpand_single1:
  "b' ∈ set (lexpand_single1 b l) ⟹ l ∈ set b ⟹ lexpands_single b' b"
  apply(induction b l rule: lexpand_single1.induct)
          apply(auto simp: lexpands_single.intros)
  done

lemma lexpands_single_if_lexpand_single:
  "b' ∈ set (lexpand_single b) ⟹ lexpands_single b' b"
  unfolding lexpand_single_def using lexpands_single_if_lexpand_single1
  by (auto simp: lexpands_single.intros)

fun lexpand_eq1 :: "'a branch ⇒ 'a pset_fm ⇒ 'a branch list" where
  "lexpand_eq1 b (AT (t1 =⇩s t2)) =
    [[AT (subst_tlvl t1 t2 a)]. AT a ← b, t1 ∈ tlvl_terms a] @
    [[AF (subst_tlvl t1 t2 a)]. AF a ← b, t1 ∈ tlvl_terms a] @
    [[AT (subst_tlvl t2 t1 a)]. AT a ← b, t2 ∈ tlvl_terms a] @
    [[AF (subst_tlvl t2 t1 a)]. AF a ← b, t2 ∈ tlvl_terms a]"
| "lexpand_eq1 b _ = []"

definition "lexpand_eq b ≡
  [[AF (s =⇩s s')]. AT (s ∈⇩s t) ← b, AF (s' ∈⇩s t') ← b, t' = t] @
  concat (map (lexpand_eq1 b) b)"

lemma lexpand_eq_if_lexpands_eq:
  "lexpands_eq b' b ⟹ b' ∈ set (lexpand_eq b)"
  apply(induction rule: lexpands_eq.induct)
       apply(force simp: lexpand_eq_def)+
  done

lemma lexpands_eq_if_lexpand_eq1:
  "b' ∈ set (lexpand_eq1 b l) ⟹ l ∈ set b ⟹ lexpands_eq b' b"
  apply(induction b l rule: lexpand_eq1.induct)
          apply(auto simp: lexpands_eq.intros)
  done

lemma lexpands_eq_if_lexpand_eq:
  "b' ∈ set (lexpand_eq b) ⟹ lexpands_eq b' b"
  unfolding lexpand_eq_def using lexpands_eq_if_lexpand_eq1
  by (auto simp: lexpands_eq.intros)

definition "lexpand b ≡
  lexpand_fm b @
  lexpand_un b @ lexpand_int b @ lexpand_diff b @ 
  lexpand_single b @ lexpand_eq b"

lemma lexpand_if_lexpands:
  "lexpands b' b ⟹ b' ∈ set (lexpand b)"
  apply(induction rule: lexpands.induct)
  unfolding lexpand_def
  using lexpand_fm_if_lexpands_fm
  using lexpand_un_if_lexpands_un lexpand_int_if_lexpands_int lexpand_diff_if_lexpands_diff
  using lexpand_single_if_lexpands_single lexpand_eq_if_lexpands_eq
  by fastforce+

lemma lexpands_if_lexpand:
  "b' ∈ set (lexpand b) ⟹ lexpands b' b"
  unfolding lexpand_def
  using lexpands_fm_if_lexpand_fm
  using lexpands_un_if_lexpand_un lexpands_int_if_lexpand_int lexpands_diff_if_lexpand_diff
  using lexpands_single_if_lexpand_single lexpands_eq_if_lexpand_eq
  using lexpands.intros by fastforce

fun bexpand_nowit1 :: "'a branch ⇒ 'a pset_fm ⇒ 'a branch list list" where
  "bexpand_nowit1 b (Or p q) =
    (if p ∉ set b ∧ Neg p ∉ set b then [[[p], [Neg p]]] else [])"
| "bexpand_nowit1 b (Neg (And p q)) =
    (if Neg p ∉ set b ∧ p ∉ set b then [[[Neg p], [p]]] else [])"
| "bexpand_nowit1 b (AT (s ∈⇩s t)) =
    [[[AT (s ∈⇩s t2)], [AF (s ∈⇩s t2)]]. t' ⊓⇩s t2 ← subterms_fm_list (last b), t' = t,
                                       AT (s ∈⇩s t2) ∉ set b, AF (s ∈⇩s t2) ∉ set b] @
    [[[AT (s ∈⇩s t2)], [AF (s ∈⇩s t2)]]. t' -⇩s t2 ← subterms_fm_list (last b), t' = t,
                                       AT (s ∈⇩s t2) ∉ set b, AF (s ∈⇩s t2) ∉ set b] @
    (case t of
      t1 ⊔⇩s t2 ⇒
        (if t1 ⊔⇩s t2 ∈ subterms (last b) ∧ AT (s ∈⇩s t1) ∉ set b ∧ AF (s ∈⇩s t1) ∉ set b
          then [[[AT (s ∈⇩s t1)], [AF (s ∈⇩s t1)]]] else [])
    | _ ⇒ [])"
| "bexpand_nowit1 b _ = []"

definition "bexpand_nowit b ≡ concat (map (bexpand_nowit1 b) b)"

lemma bexpand_nowit_if_bexpands_nowit:
  "bexpands_nowit bs' b ⟹ bs' ∈ set ` set (bexpand_nowit b)"
  apply(induction rule: bexpands_nowit.induct)
       apply(force simp: bexpand_nowit_def)+
  done

lemma bexpands_nowit_if_bexpand_nowit1:
  "bs' ∈ set ` set (bexpand_nowit1 b l) ⟹ l ∈ set b ⟹ bexpands_nowit bs' b"
  apply(induction b l rule: bexpand_nowit1.induct)
          apply(auto simp: bexpands_nowit.intros)
  done

lemma bexpands_nowit_if_bexpand_nowit:
  "bs' ∈ set ` set (bexpand_nowit b) ⟹ bexpands_nowit bs' b"
  unfolding bexpand_nowit_def using bexpands_nowit_if_bexpand_nowit1
  by (auto simp: bexpands_nowit.intros)

definition "name_subterm φ ≡ index (subterms_fm_list φ)"

lemma inj_on_name_subterm_subterms:
  "inj_on (name_subterm φ) (subterms φ)"
  unfolding name_subterm_def
  by (intro inj_on_index2) simp

abbreviation "solve_constraints φ ≡
  MLSS_Suc_Theory.solve (MLSS_Suc_Theory.elim_NEq_Zero (constrs_fm (name_subterm φ) φ))"

definition "urelem_code φ t ≡
  (case solve_constraints φ of
    Some ss ⇒ MLSS_Suc_Theory.assign ss (name_subterm φ t) = 0
  | None ⇒ False)"

lemma urelem_code_if_mem_subterms:
  assumes "t ∈ subterms φ"
  shows "urelem φ t ⟷ urelem_code φ t"
proof -
  note urelem_iff_assign_eq_0[OF _ assms] not_types_fm_if_solve_eq_None
  note solve_correct = this[OF inj_on_name_subterm_subterms]
  then show ?thesis
    unfolding urelem_def urelem_code_def
    by (auto split: option.splits)
qed

fun bexpand_wit1 :: "('a::{fresh,default}) branch ⇒ 'a pset_fm ⇒ 'a branch list list" where
  "bexpand_wit1 b (AF (t1 =⇩s t2)) =
    (if t1 ∈ subterms (last b) ∧ t2 ∈ subterms (last b) ∧
        (∀t ∈ set b. case t of AT (x ∈⇩s t1') ⇒ t1' = t1 ⟶ AF (x ∈⇩s t2) ∉ set b | _ ⇒ True) ∧
        (∀t ∈ set b. case t of AT (x ∈⇩s t2') ⇒ t2' = t2 ⟶ AF (x ∈⇩s t1) ∉ set b | _ ⇒ True) ∧
        ¬ urelem_code (last b) t1 ∧ ¬ urelem_code (last b) t2
      then
        (let x = fresh (vars b) default
         in [[[AT (Var x ∈⇩s t1), AF (Var x ∈⇩s t2)],
              [AT (Var x ∈⇩s t2), AF (Var x ∈⇩s t1)]]])
      else [])"
| "bexpand_wit1 b _ = []"

definition "bexpand_wit b ≡ concat (map (bexpand_wit1 b) b)"

lemma Not_Ex_wit_code:
  "(∄x. AT (x ∈⇩s t1) ∈ set b ∧ AF (x ∈⇩s t2) ∈ set b)
    ⟷ (∀fm ∈ set b. case fm of
                        AT (x ∈⇩s t') ⇒ t' = t1 ⟶ AF (x ∈⇩s t2) ∉ set b
                      | _ ⇒ True)"
  by (auto split: fm.splits pset_atom.splits)

lemma bexpand_wit1_if_bexpands_wit:
  assumes "bexpands_wit t1 t2 (fresh (vars b) default) bs' b"
  shows "bs' ∈ set ` set (bexpand_wit1 b (AF (t1 =⇩s t2)))"
proof -
  from bexpands_witD[OF assms] show ?thesis
    by (simp add: Let_def urelem_code_if_mem_subterms Not_Ex_wit_code[symmetric])
qed

lemma bexpand_wit_if_bexpands_wit:
  assumes "bexpands_wit t1 t2 (fresh (vars b) default) bs' b"
  shows "bs' ∈ set ` set (bexpand_wit b)"
  using assms(1)[THEN bexpand_wit1_if_bexpands_wit] bexpands_witD(2)[OF assms(1)]
  unfolding bexpand_wit_def 
  by (auto simp del: bexpand_wit1.simps(1))
  
lemma bexpands_wit_if_bexpand_wit1:
  "b' ∈ set ` set (bexpand_wit1 b l) ⟹ l ∈ set b ⟹ (∃t1 t2 x. bexpands_wit t1 t2 x b' b)"
proof(induction b l rule: bexpand_wit1.induct)
  case (1 b t1 t2)
  show ?case
    apply(rule exI[where ?x=t1], rule exI[where ?x=t2],
          rule exI[where ?x="fresh (vars b) default"])
    using 1
    by (auto simp: Let_def bexpands_wit.simps finite_vars_branch[THEN fresh_notIn]
                   Not_Ex_wit_code[symmetric] urelem_code_if_mem_subterms)
qed auto
    
lemma bexpands_wit_if_bexpand_wit:
  "bs' ∈ set ` set (bexpand_wit b) ⟹ (∃t1 t2 x. bexpands_wit t1 t2 x bs' b)"
proof -
  assume "bs' ∈ set ` set (bexpand_wit b)"
  then obtain l where "bs' ∈ set ` set (bexpand_wit1 b l)" "l ∈ set b" 
    unfolding bexpand_wit_def by auto
  from bexpands_wit_if_bexpand_wit1[OF this] show ?thesis .
qed
                                
definition "bexpand b ≡ bexpand_nowit b @ bexpand_wit b"

lemma bexpands_if_bexpand:
  "bs' ∈ set ` set (bexpand b) ⟹ bexpands bs' b"
  unfolding bexpand_def
  using bexpands_nowit_if_bexpand_nowit bexpands_wit_if_bexpand_wit
  by (metis bexpands.intros UnE image_Un set_append)

lemma Not_bexpands_if_bexpand_empty:
  assumes "bexpand b = []"
  shows "¬ bexpands bs' b"
proof
  assume "bexpands bs' b"
  then show False
    using assms
  proof (induction rule: bexpands.induct)
    case (1 bs' b)
    with bexpand_nowit_if_bexpands_nowit[OF this(1)] show ?case
      unfolding bexpand_def by simp
  next
    case (2 t1 t2 x bs' b)
    note fresh_notIn[OF finite_vars_branch, of b]
    with 2 obtain bs'' where "bexpands_wit t1 t2 (fresh (vars b) default) bs'' b"
      by (auto simp: bexpands_wit.simps)
    from 2 bexpand_wit_if_bexpands_wit[OF this] show ?case
      by (simp add: bexpand_def)
  qed
qed

lemma lin_sat_code:
  "lin_sat b ⟷ filter (λb'. ¬ set b' ⊆ set b) (lexpand b) = []"
  unfolding lin_sat_def
  using lexpand_if_lexpands lexpands_if_lexpand
  by (force simp: filter_empty_conv)

lemma sat_code:
  "sat b ⟷ lin_sat b ∧ bexpand b = []"
  using Not_bexpands_if_bexpand_empty bexpands_if_bexpand
  unfolding sat_def
  by (metis imageI list.set_intros(1) list_exhaust2)

fun bclosed_code1 :: "'a branch ⇒ 'a pset_fm ⇒ bool" where
  "bclosed_code1 b (Neg φ) ⟷
    φ ∈ set b ∨
    (case φ of Atom (t1 =⇩s t2) ⇒ t1 = t2 | _ ⇒ False)"
| "bclosed_code1 b (AT (_ ∈⇩s ∅ _)) ⟷ True"
| "bclosed_code1 _ _ ⟷ False"

definition "bclosed_code b ≡ (∃t ∈ set b. bclosed_code1 b t)"

lemma bclosed_code_if_bclosed:
  assumes "bclosed b" "wf_branch b" "v ⊢ last b"
  shows "bclosed_code b"
  using assms
proof(induction rule: bclosed.induct)
  case (contr φ b)
  then have "bclosed_code1 b (Neg φ)"
    by auto
  with contr show ?case
    unfolding bclosed_code_def by blast
next
  case (memEmpty t n b)
  then have "bclosed_code1 b (AT (t ∈⇩s ∅ n))"
    by auto
  with memEmpty show ?case
    unfolding bclosed_code_def by blast
next
  case (neqSelf t b)
  then have "bclosed_code1 b (AF (t =⇩s t))"
    by auto
  with neqSelf show ?case
    unfolding bclosed_code_def by blast
next
  case (memberCycle cs b)
  then show ?case
    by (auto simp: bclosed_code_def dest: no_member_cycle_if_types_last)
qed

lemma bclosed_if_bclosed_code1:
  "bclosed_code1 b l ⟹ l ∈ set b ⟹ bclosed b"
  by (induction rule: bclosed_code1.induct)
     (auto simp: bclosed.intros split: fm.splits pset_atom.splits)

lemma bclosed_if_bclosed_code:
  "bclosed_code b ⟹ bclosed b"
  unfolding bclosed_code_def using bclosed_if_bclosed_code1 by blast

lemma bclosed_code:
  assumes "wf_branch b" "v ⊢ last b"
  shows "bclosed b ⟷ bclosed_code b"
  using assms bclosed_if_bclosed_code bclosed_code_if_bclosed 
  by blast

definition "lexpand_safe b ≡
  case filter (λb'. ¬ set b' ⊆ set b) (lexpand b) of
    b' # bs' ⇒ b'
  | [] ⇒ []"

lemma lexpands_lexpand_safe:
  "¬ lin_sat b ⟹ lexpands (lexpand_safe b) b ∧ set b ⊂ set (lexpand_safe b @ b)"
  unfolding lexpand_safe_def
  by (auto simp: lin_sat_code intro!: lexpands_if_lexpand dest: filter_eq_ConsD split: list.splits)

lemma wf_branch_lexpand_safe:
  assumes "wf_branch b"
  shows "wf_branch (lexpand_safe b @ b)"
proof -
  from assms have "wf_branch (lexpand_safe b @ b)" if "¬ lin_sat b"
    using that lexpands_lexpand_safe wf_branch_lexpands by metis
  moreover have "wf_branch (lexpand_safe b @ b)" if "lin_sat b"
    using assms that[unfolded lin_sat_code]
    unfolding lexpand_safe_def by simp
  ultimately show ?thesis
    by blast
qed

definition "bexpand_safe b ≡
  case bexpand b of
    bs' # bss' ⇒ bs'
  | [] ⇒ [[]]"

lemma bexpands_bexpand_safe:
  "¬ sat b ⟹ lin_sat b ⟹ bexpands (set (bexpand_safe b)) b"
  unfolding bexpand_safe_def
  by (auto simp: sat_code bexpands_if_bexpand split: list.splits)

lemma wf_branch_bexpand_safe:
  assumes "wf_branch b"
  shows "∀b' ∈ set (bexpand_safe b). wf_branch (b' @ b)"
proof -
  note wf_branch_expandss[OF assms expandss.intros(3), OF bexpands_if_bexpand]
  with assms show ?thesis
    unfolding bexpand_safe_def
    by (simp split: list.splits) (metis expandss.intros(1) image_iff list.set_intros(1))
qed

interpretation mlss_naive: mlss_proc lexpand_safe "set o bexpand_safe"
  apply(unfold_locales)
  using lexpands_lexpand_safe bexpands_bexpand_safe by auto

lemma types_pset_fm_code:
  "(∃v. v ⊢ φ) ⟷ solve_constraints φ ≠ None"
  using not_types_fm_if_solve_eq_None types_pset_fm_assign_solve
  by (meson inj_on_name_subterm_subterms not_Some_eq)

fun foldl_option where
  "foldl_option f a [] = Some a"
| "foldl_option f _ (None # _) = None"
| "foldl_option f a (Some x # xs) = foldl_option f (f a x) xs"

lemma monotone_fold_option_conj[partial_function_mono]:
  "monotone (list_all2 option_ord) option_ord (foldl_option f a)"
proof
  fix xs ys :: "'a option list"
  assume "list_all2 option_ord xs ys"
  then show "option_ord (foldl_option f a xs) (foldl_option f a ys)"
  proof(induction xs ys arbitrary: a rule: list_all2_induct)
    case Nil
    then show ?case by (simp add: option.leq_refl)
  next
    case (Cons xo xos yo yos)
    then consider
        "xo = None" "yo = None"
      | y where "xo = None" "yo = Some y"
      | x y where "xo = Some x" "yo = Some y"
      by (metis flat_ord_def option.exhaust)
    then show ?case
      using Cons
      by cases (simp_all add: option.leq_refl flat_ord_def)
  qed
qed

lemma monotone_map[partial_function_mono]:
  assumes "monotone (list_all2 option_ord) ordb B"
  shows "monotone option.le_fun ordb (λh. B (map h xs))"
  using assms
  by (simp add: fun_ord_def list_all2_conv_all_nth monotone_on_def)

partial_function (option) mlss_proc_branch_partial
  :: "('a::{fresh,default}) branch ⇒ bool option" where
  "mlss_proc_branch_partial b =
    (if ¬ lin_sat b then mlss_proc_branch_partial (lexpand_safe b @ b)
     else if bclosed_code b then Some True
     else if ¬ sat b then
        foldl_option (∧) True (map mlss_proc_branch_partial (map (λb'. b' @ b) (bexpand_safe b)))
     else Some (bclosed_code b))"

lemma mlss_proc_branch_partial_eq:
  assumes "wf_branch b" "v ⊢ last b"
  shows "mlss_proc_branch_partial b = Some (mlss_naive.mlss_proc_branch b)"
    (is "?mlss_part b = Some (?mlss b)")
  using mlss_naive.mlss_proc_branch_dom_if_wf_branch[OF assms(1)] assms
proof(induction rule: mlss_naive.mlss_proc_branch.pinduct)
  case (1 b)
  then have "?mlss_part (lexpand_safe b @ b)
    = Some (mlss_naive.mlss_proc_branch (lexpand_safe b @ b))"
    using wf_branch_lexpand_safe[OF ‹wf_branch b›] by fastforce
  with 1 show ?case
    by (subst mlss_proc_branch_partial.simps)
       (auto simp: mlss_naive.mlss_proc_branch.psimps)
next
  case (2 b)
  then show ?case
    by (subst mlss_proc_branch_partial.simps)
       (auto simp: mlss_naive.mlss_proc_branch.psimps bclosed_code)
next
  case (3 b)
  then have "?mlss_part (b' @ b) = Some (?mlss (b' @ b))"
    if "b' ∈ set (bexpand_safe b)" for b'
    using that wf_branch_bexpand_safe[OF ‹wf_branch b›] by fastforce
  then have "map ?mlss_part (map (λb'. b' @ b) (bexpand_safe b))
    = map Some (map (λb'. (?mlss (b' @ b))) (bexpand_safe b))"
    by simp
  moreover have "foldl_option (∧) a (map Some xs) = Some (a ∧ (∀x ∈ set xs. x))" for a xs
    by (induction xs arbitrary: a) auto
  moreover have foldl_option_eq:
    "foldl_option (∧) True (map ?mlss_part (map (λb'. b' @ b) (bexpand_safe b)))
    = Some (∀b' ∈ set (bexpand_safe b). ?mlss (b' @ b))"
    unfolding calculation by (auto simp: comp_def)
  from 3 show ?case
    by (subst mlss_proc_branch_partial.simps, subst foldl_option_eq)
       (simp add: bclosed_code mlss_naive.mlss_proc_branch.psimps(3))
next
  case (4 b)
  then show ?case
    by (subst mlss_proc_branch_partial.simps)
       (auto simp: mlss_naive.mlss_proc_branch.psimps bclosed_code)
qed

definition "mlss_proc_partial (φ :: nat pset_fm) ≡
  if solve_constraints φ = None then None else mlss_proc_branch_partial [φ]"

lemma mlss_proc_partial_eq_None:
  "mlss_proc_partial φ = None ⟹ (∄v. v ⊢ φ)"
  unfolding mlss_proc_partial_def
  using types_pset_fm_code mlss_proc_branch_partial_eq wf_branch_singleton
  by (metis last.simps option.discI)

lemma mlss_proc_partial_complete:
  assumes "mlss_proc_partial φ = Some False"
  shows "∃M. interp I⇩s⇩a M φ"
proof -
  from assms have "∃v. v ⊢ φ"
    unfolding mlss_proc_partial_def using types_pset_fm_code by force
  moreover have "¬ mlss_naive.mlss_proc φ"
    using assms ‹∃v. v ⊢ φ› mlss_proc_branch_partial_eq calculation wf_branch_singleton
    unfolding mlss_naive.mlss_proc_def mlss_proc_partial_def
    by (metis last.simps option.discI option.inject)
  ultimately show ?thesis
    using mlss_naive.mlss_proc_complete by blast
qed

lemma mlss_proc_partial_sound:
  assumes "mlss_proc_partial φ = Some True"
  shows "¬ interp I⇩s⇩a M φ"
proof -
  from assms have "∃v. v ⊢ φ"
    unfolding mlss_proc_partial_def using types_pset_fm_code by force
  moreover have "mlss_naive.mlss_proc φ"
    using assms ‹∃v. v ⊢ φ› mlss_proc_branch_partial_eq calculation wf_branch_singleton
    unfolding mlss_naive.mlss_proc_def mlss_proc_partial_def
    by (metis last.simps option.discI option.inject)
  ultimately show ?thesis
    using mlss_naive.mlss_proc_sound by blast
qed

declare lin_sat_code[code] sat_code[code]
declare mlss_proc_branch_partial.simps[code]
code_identifier
    code_module MLSS_Calculus ⇀ (SML) MLSS_Proc_Code
  | code_module MLSS_Proc ⇀ (SML) MLSS_Proc_Code
export_code mlss_proc_partial in SML

end