Theory IsaSAT_VDom

theory IsaSAT_VDom
  imports IsaSAT_Stats IsaSAT_Clauses
begin

paragraph ‹AI-vdom›
text ‹
We keep all the indices. This is a subset of \<^term>‹vdom› but is cleaned more aggressively.
At first we traid to express the relation directly but this was too cumbersome to use, due to having
both sets and multisets.
›
type_synonym vdom = ‹nat list›
type_synonym aivdom = ‹vdom × vdom × vdom × vdom›
type_synonym isasat_aivdom = ‹aivdom code_hider›

abbreviation get_aivdom  :: ‹isasat_aivdom ⇒ aivdom› where
  ‹get_aivdom ≡ get_content›

abbreviation AIvdom :: ‹aivdom ⇒ isasat_aivdom› where
  ‹AIvdom ≡ Constructor›

fun get_vdom_aivdom where
  ‹get_vdom_aivdom (AIvdom (vdom, avdom, ivdom, tvdom)) = vdom›

fun get_avdom_aivdom where
  ‹get_avdom_aivdom (AIvdom (vdom, avdom, ivdom, tvdom)) = avdom›

fun get_ivdom_aivdom where
  ‹get_ivdom_aivdom (AIvdom (vdom, avdom, ivdom, tvdom)) = ivdom›

fun get_tvdom_aivdom where
  ‹get_tvdom_aivdom (AIvdom (vdom, avdom, ivdom, tvdom)) = tvdom›

fun aivdom_inv :: ‹aivdom ⇒ _ ⇒ bool› where
  ‹aivdom_inv (vdom, avdom, ivdom, tvdom) d ⟷
    set avdom ∩ set ivdom = {} ∧
    set_mset d ⊆ set avdom ∪ set ivdom ∧
    mset avdom ⊆# mset vdom ∧
    mset ivdom ⊆# mset vdom ∧
    distinct_mset d ∧
    distinct vdom ∧
    distinct tvdom ∧
    mset tvdom ⊆# mset vdom›

fun aivdom_inv_strong :: ‹aivdom ⇒ _ ⇒ bool› where
  ‹aivdom_inv_strong (vdom, avdom, ivdom, tvdom) d ⟷
    (aivdom_inv (vdom, avdom, ivdom, tvdom) d ∧ tvdom = vdom)›

definition aivdom_inv_dec :: ‹isasat_aivdom ⇒ _ ⇒ bool› where
  ‹aivdom_inv_dec = aivdom_inv o get_aivdom›

definition aivdom_inv_strong_dec :: ‹isasat_aivdom ⇒ _ ⇒ bool› where
  ‹aivdom_inv_strong_dec = aivdom_inv_strong o get_aivdom›

lemma aivdom_inv_strong_dec_def2:
  ‹aivdom_inv_strong_dec x a ⟷ aivdom_inv_dec x a ∧ get_vdom_aivdom x = get_tvdom_aivdom x›
  by (cases x) (auto simp: aivdom_inv_strong_dec_def aivdom_inv_dec_def)

lemma aivdom_inv_alt_def:
  ‹aivdom_inv (vdom, avdom, ivdom, tvdom) d ⟷
   (set avdom ∩ set ivdom = {} ∧
    set_mset d ⊆ set avdom ∪ set ivdom ∧
    set avdom ⊆ set vdom ∧
    set ivdom ⊆ set vdom ∧
    distinct vdom∧
    distinct ivdom∧
    distinct_mset d ∧
    distinct avdom∧
    distinct tvdom ∧
    set tvdom ⊆ set vdom)›
  using distinct_mset_mono[of ‹mset (avdom)› ‹mset (vdom)›]
    distinct_mset_mono[of ‹mset (ivdom)› ‹mset (vdom)›]
    distinct_subseteq_iff[of  ‹mset (avdom)› ‹mset (vdom)›]
    distinct_subseteq_iff[of ‹mset (ivdom)› ‹mset (vdom)›]
    distinct_subseteq_iff[of ‹mset (tvdom)› ‹mset (vdom)›]
  by auto

lemma AIvdom_split:
  ‹aivdom = AIvdom (get_vdom_aivdom aivdom, get_avdom_aivdom aivdom, get_ivdom_aivdom aivdom, get_tvdom_aivdom aivdom)›
  by (cases aivdom) auto


lemma aivdom_inv_dec_alt_def:
  ‹aivdom_inv_dec aivdom d ⟷
  (set (get_avdom_aivdom aivdom) ∩ set (get_ivdom_aivdom aivdom) = {} ∧
    set_mset d ⊆ set (get_avdom_aivdom aivdom) ∪ set (get_ivdom_aivdom aivdom) ∧
    mset (get_avdom_aivdom aivdom) ⊆# mset (get_vdom_aivdom aivdom) ∧
    mset (get_ivdom_aivdom aivdom) ⊆# mset (get_vdom_aivdom aivdom) ∧
  distinct_mset d ∧ distinct (get_vdom_aivdom aivdom) ∧
  mset (get_tvdom_aivdom aivdom) ⊆# mset (get_vdom_aivdom aivdom)  ∧ distinct (get_tvdom_aivdom aivdom))›
  apply (subst AIvdom_split)
  apply (subst aivdom_inv_dec_def)
  apply (subst comp_def)
  apply (auto simp add: aivdom_inv_alt_def)
  done

lemma aivdom_inv_dec_alt_def2:
  ‹aivdom_inv_dec aivdom d ⟷
  (set (get_avdom_aivdom aivdom) ∩ set (get_ivdom_aivdom aivdom) = {} ∧
    set_mset d ⊆ set (get_avdom_aivdom aivdom) ∪ set (get_ivdom_aivdom aivdom) ∧
    mset (get_avdom_aivdom aivdom) ⊆# mset (get_vdom_aivdom aivdom) ∧
    mset (get_ivdom_aivdom aivdom) ⊆# mset (get_vdom_aivdom aivdom) ∧
  distinct_mset d ∧ distinct (get_vdom_aivdom aivdom) ∧ distinct (get_avdom_aivdom aivdom) ∧
  distinct (get_ivdom_aivdom aivdom)∧
  mset (get_tvdom_aivdom aivdom) ⊆# mset (get_vdom_aivdom aivdom)  ∧ distinct (get_tvdom_aivdom aivdom))›
  apply (subst AIvdom_split)
  apply (subst aivdom_inv_dec_def)
  apply (subst comp_def)
  apply (auto dest: distinct_mset_mono simp add: aivdom_inv_alt_def)
  done

lemmas aivdom_inv_strong_dec_alt_def =
  aivdom_inv_strong_dec_def2[unfolded aivdom_inv_dec_alt_def2]

lemma distinct_butlast_set:
  ‹distinct xs ⟹ set (butlast xs) = set xs - {last xs}›
  by (cases xs rule: rev_cases) auto

lemma distinct_remove_readd_last_set:
  ‹distinct xs ⟹ i < length xs ⟹ set (butlast (xs[i := last xs])) = set xs - {xs!i}›
  by (cases xs rule: rev_cases) (auto simp: list_update_append set_update_distinct nth_append)

definition add_learned_clause_aivdom_int where
  ‹add_learned_clause_aivdom_int = (λ C (vdom, avdom, ivdom). (vdom @ [C], avdom @ [C], ivdom))›

definition add_learned_clause_aivdom :: ‹_ ⇒ isasat_aivdom ⇒ isasat_aivdom› where
  ‹add_learned_clause_aivdom C ≡ AIvdom o add_learned_clause_aivdom_int C o get_aivdom›

lemma aivdom_inv_intro_add_mset:
  ‹C ∉# d ⟹ C ∉ set vdom ⟹ aivdom_inv (vdom, avdom, ivdom, tvdom) d ⟹ aivdom_inv (vdom @ [C], avdom @ [C], ivdom, tvdom) (add_mset C d)›
  unfolding aivdom_inv_alt_def
  by (cases ‹C ∈ (set (avdom) ∪ set (ivdom))›)
   (auto dest: subset_mset_imp_subset_add_mset simp: add_learned_clause_aivdom_int_def split: code_hider.splits)

lemma aivdom_inv_dec_intro_add_mset:
  ‹C ∉# d ⟹ C ∉ set (get_vdom_aivdom aivdom) ⟹ aivdom_inv_dec aivdom d ⟹ aivdom_inv_dec (add_learned_clause_aivdom C aivdom) (add_mset C d)›
  using aivdom_inv_intro_add_mset[of C d ‹get_vdom_aivdom aivdom› ‹get_avdom_aivdom aivdom›
    ‹get_ivdom_aivdom aivdom›]
  by (cases aivdom)
    (auto simp: aivdom_inv_dec_def add_learned_clause_aivdom_int_def add_learned_clause_aivdom_def
    simp del: aivdom_inv.simps)

definition add_init_clause_aivdom_int where
  ‹add_init_clause_aivdom_int = (λ C (vdom, avdom, ivdom, tvdom). (vdom @ [C], avdom, ivdom @ [C], tvdom))›

definition add_init_clause_aivdom :: ‹_ ⇒ isasat_aivdom ⇒ isasat_aivdom› where
  ‹add_init_clause_aivdom C ≡ AIvdom o add_init_clause_aivdom_int C o get_aivdom›

lemma aivdom_inv_intro_init_add_mset:
  ‹C ∉# d ⟹ C ∉ set vdom ⟹ aivdom_inv (vdom, avdom, ivdom, tvdom) d ⟹ aivdom_inv (vdom @ [C], avdom, ivdom @ [C], tvdom) (add_mset C d)›
  unfolding aivdom_inv_alt_def
  by (cases ‹C ∈ (set (avdom) ∪ set (ivdom))›)
   (auto dest: subset_mset_imp_subset_add_mset simp: add_init_clause_aivdom_int_def split: code_hider.splits)

lemma aivdom_inv_dec_intro_init_add_mset:
  ‹C ∉# d ⟹ C ∉ set (get_vdom_aivdom aivdom) ⟹ aivdom_inv_dec aivdom d ⟹ aivdom_inv_dec (add_init_clause_aivdom C aivdom) (add_mset C d)›
  using aivdom_inv_intro_init_add_mset[of C d ‹get_vdom_aivdom aivdom› ‹get_avdom_aivdom aivdom›
    ‹get_ivdom_aivdom aivdom› ‹get_tvdom_aivdom aivdom›]
  by (cases aivdom)
    (auto simp: aivdom_inv_dec_def add_init_clause_aivdom_int_def add_init_clause_aivdom_def
    simp del: aivdom_inv.simps)

definition remove_inactive_aivdom_tvdom_int :: ‹_ ⇒ aivdom ⇒ aivdom› where
  ‹remove_inactive_aivdom_tvdom_int = (λi (vdom, avdom, ivdom, tvdom). (vdom, avdom, ivdom, delete_index_and_swap tvdom i))›

definition remove_inactive_aivdom_tvdom :: ‹_ ⇒ isasat_aivdom ⇒ isasat_aivdom› where
  ‹remove_inactive_aivdom_tvdom C ≡ AIvdom o remove_inactive_aivdom_tvdom_int C o get_aivdom›

definition remove_inactive_aivdom_int :: ‹_ ⇒ aivdom ⇒ aivdom› where
  ‹remove_inactive_aivdom_int = (λi (vdom, avdom, ivdom, tvdom). (vdom, delete_index_and_swap avdom i, ivdom, tvdom))›

definition remove_inactive_aivdom :: ‹_ ⇒ isasat_aivdom ⇒ isasat_aivdom› where
  ‹remove_inactive_aivdom C ≡ AIvdom o remove_inactive_aivdom_int C o get_aivdom›

lemma aivdom_inv_remove_and_swap_inactive_tvdom:
  assumes ‹i < length tv› and ‹aivdom_inv (m, n, s, tv) baa›
  shows ‹aivdom_inv (m, n, s, butlast (tv[i := last tv])) (remove1_mset (tv ! i) baa)›
proof -
  show ?thesis
    using assms distinct_mset_mono[of ‹mset n› ‹mset m›]
    by (auto simp: aivdom_inv_alt_def distinct_remove_readd_last_set mset_le_subtract distinct_butlast_set
       dest: in_set_butlastD in_vdom_m_fmdropD simp del: nth_mem)
qed
lemma aivdom_inv_dec_remove_and_swap_inactive_tvdom:
  assumes ‹i < length (get_tvdom_aivdom ai)› and ‹aivdom_inv_dec ai baa›
  shows ‹aivdom_inv_dec (remove_inactive_aivdom_tvdom i ai)  (remove1_mset (get_tvdom_aivdom ai ! i) baa)›
  using aivdom_inv_remove_and_swap_inactive_tvdom[of i ‹get_tvdom_aivdom ai›
    ‹get_vdom_aivdom ai› ‹get_avdom_aivdom ai› ‹get_ivdom_aivdom ai› baa] assms
  by (cases ai; auto simp: aivdom_inv_dec_def remove_inactive_aivdom_tvdom_int_def remove_inactive_aivdom_tvdom_def
    simp del: aivdom_inv.simps)

lemma aivdom_inv_remove_and_swap_inactive:
  assumes ‹i < length n› and ‹aivdom_inv (m, n, s, tv) baa›
  shows ‹aivdom_inv (m, butlast (n[i := last n]), s, tv) (remove1_mset (n ! i) baa)›
proof -
  have [simp]: ‹set n - {n ! i} ∪ set s = set n ∪ set s - {n ! i}›
    using assms nth_mem[of i n]
    by (auto simp: aivdom_inv_alt_def distinct_remove_readd_last_set
      dest: in_set_butlastD in_vdom_m_fmdropD simp del: nth_mem)
  have [simp]: ‹mset_set (set n ∪ set s - {n ! i}) = remove1_mset (n!i) (mset_set (set n ∪ set s))›
     using assms
     by (auto simp: aivdom_inv_alt_def mset_set_Diff)
  show ?thesis
    using assms distinct_mset_mono[of ‹mset n› ‹mset m›]
    by (auto simp: aivdom_inv_alt_def distinct_remove_readd_last_set mset_le_subtract distinct_butlast_set
       dest: in_set_butlastD in_vdom_m_fmdropD simp del: nth_mem)
qed

lemma aivdom_inv_dec_remove_and_swap_inactive:
  assumes ‹i < length (get_avdom_aivdom ai)› and ‹aivdom_inv_dec ai baa›
  shows ‹aivdom_inv_dec (remove_inactive_aivdom i ai)  (remove1_mset (get_avdom_aivdom ai ! i) baa)›
  using aivdom_inv_remove_and_swap_inactive[of i ‹get_avdom_aivdom ai›
    ‹get_vdom_aivdom ai› ‹get_ivdom_aivdom ai› ‹get_tvdom_aivdom ai› baa] assms
  by (cases ai; auto simp: aivdom_inv_dec_def remove_inactive_aivdom_int_def remove_inactive_aivdom_def
    simp del: aivdom_inv.simps)

lemma aivdom_inv_remove_clause:
  ‹aivdom_inv ai baa ⟹ aivdom_inv ai (remove1_mset C baa)›
  by (cases ai) (auto simp: aivdom_inv_alt_def distinct_remove_readd_last_set
      dest: in_set_butlastD dest: in_diffD)

lemma aivdom_inv_dec_remove_clause:
  ‹aivdom_inv_dec ai baa ⟹ aivdom_inv_dec ai (remove1_mset C baa)›
  using aivdom_inv_remove_clause[of ‹get_content ai› baa]
  by (auto simp: aivdom_inv_dec_def)

lemma aivdom_inv_removed_inactive:
  assumes ‹i < length n› and ‹aivdom_inv (m, n, s, tv) baa› ‹n!i ∉# baa›
  shows ‹aivdom_inv (m, butlast (n[i := last n]), s, tv) baa›
  by (metis aivdom_inv_remove_and_swap_inactive assms(1) assms(2) assms(3) diff_single_trivial)

lemma aivdom_inv_dec_removed_inactive:
  assumes ‹i < length (get_avdom_aivdom ai)› and ‹aivdom_inv_dec ai baa› ‹get_avdom_aivdom ai!i ∉# baa›
  shows ‹aivdom_inv_dec (remove_inactive_aivdom i ai) baa›
  using aivdom_inv_removed_inactive[OF assms(1), of ‹get_vdom_aivdom ai›
    ‹get_ivdom_aivdom ai› ‹get_tvdom_aivdom ai› baa] assms(2-)
  by (cases ai)
    (auto simp: aivdom_inv_dec_def remove_inactive_aivdom_int_def
    remove_inactive_aivdom_def simp del: aivdom_inv.simps)

(*TODO rename all*)
lemmas aivdom_inv_remove_and_swap_removed = aivdom_inv_removed_inactive



lemma aivdom_inv_removed_inactive_tvdom:
  assumes ‹i < length tv› and ‹aivdom_inv (m, n, s, tv) baa› ‹tv!i ∉# baa›
  shows ‹aivdom_inv (m, n, s, butlast (tv[i := last tv])) baa›
  by (metis aivdom_inv_remove_and_swap_inactive_tvdom assms(1) assms(2) assms(3) diff_single_trivial)

lemma aivdom_inv_dec_removed_inactive_tvdom:
  assumes ‹i < length (get_tvdom_aivdom ai)› and ‹aivdom_inv_dec ai baa› ‹get_tvdom_aivdom ai!i ∉# baa›
  shows ‹aivdom_inv_dec (remove_inactive_aivdom_tvdom i ai) baa›
  using aivdom_inv_removed_inactive_tvdom[OF assms(1), of ‹get_vdom_aivdom ai›
    ‹get_avdom_aivdom ai› ‹get_ivdom_aivdom ai› baa] assms(2-)
  by (cases ai)
    (auto simp: aivdom_inv_dec_def remove_inactive_aivdom_tvdom_int_def
    remove_inactive_aivdom_tvdom_def simp del: aivdom_inv.simps)

lemma get_aivdom_remove_inactive_aivdom[simp]:
  ‹get_vdom_aivdom (remove_inactive_aivdom i m) = get_vdom_aivdom m›
  ‹get_avdom_aivdom (remove_inactive_aivdom i m) = (delete_index_and_swap (get_avdom_aivdom m) i)›
  ‹get_ivdom_aivdom (remove_inactive_aivdom i m) = get_ivdom_aivdom m›
  ‹get_tvdom_aivdom (remove_inactive_aivdom i m) = get_tvdom_aivdom m›
  ‹get_vdom_aivdom (remove_inactive_aivdom_tvdom i m) = get_vdom_aivdom m›
  ‹get_tvdom_aivdom (remove_inactive_aivdom_tvdom i m) = (delete_index_and_swap (get_tvdom_aivdom m) i)›
  ‹get_avdom_aivdom (remove_inactive_aivdom_tvdom i m) = get_avdom_aivdom m›
  ‹get_ivdom_aivdom (remove_inactive_aivdom_tvdom i m) = get_ivdom_aivdom m›
  by (cases m; auto simp: remove_inactive_aivdom_def remove_inactive_aivdom_int_def
      remove_inactive_aivdom_tvdom_def remove_inactive_aivdom_tvdom_int_def; fail)+

definition vdom_aivdom_at_int :: ‹aivdom ⇒ nat ⇒ nat› where
  ‹vdom_aivdom_at_int  = (λ(a,b,c) C. a ! C)›

definition vdom_aivdom_at :: ‹isasat_aivdom ⇒ nat ⇒ nat› where
  ‹vdom_aivdom_at ai C = get_vdom_aivdom ai ! C›

lemma vdom_aivdom_at_alt_def:
  ‹vdom_aivdom_at = vdom_aivdom_at_int o get_content›
  by (intro ext, rename_tac x y, case_tac x) (auto simp: vdom_aivdom_at_int_def vdom_aivdom_at_def)


definition avdom_aivdom_at_int :: ‹aivdom ⇒ nat ⇒ nat› where
  ‹avdom_aivdom_at_int = (λ(a,b,c) C. b ! C)›

definition avdom_aivdom_at :: ‹isasat_aivdom ⇒ nat ⇒ nat› where
  ‹avdom_aivdom_at ai C = get_avdom_aivdom ai ! C›

lemma avdom_aivdom_at_alt_def:
  ‹avdom_aivdom_at = avdom_aivdom_at_int o get_content›
  by (intro ext, rename_tac x y, case_tac x) (auto simp: avdom_aivdom_at_int_def avdom_aivdom_at_def)


definition ivdom_aivdom_at_int :: ‹aivdom ⇒ nat ⇒ nat› where
  ‹ivdom_aivdom_at_int = (λ(a,b,c,d) C. c ! C)›

definition ivdom_aivdom_at :: ‹isasat_aivdom ⇒ nat ⇒ nat› where
  ‹ivdom_aivdom_at ai C = get_ivdom_aivdom ai ! C›

lemma ivdom_aivdom_at_alt_def:
  ‹ivdom_aivdom_at = ivdom_aivdom_at_int o get_content›
  by (intro ext, rename_tac x y, case_tac x) (auto simp: ivdom_aivdom_at_int_def ivdom_aivdom_at_def)

definition tvdom_aivdom_at_int :: ‹aivdom ⇒ nat ⇒ nat› where
  ‹tvdom_aivdom_at_int = (λ(a,b,c,d) C. d ! C)›

definition tvdom_aivdom_at :: ‹isasat_aivdom ⇒ nat ⇒ nat› where
  ‹tvdom_aivdom_at ai C = get_tvdom_aivdom ai ! C›

lemma tvdom_aivdom_at_alt_def:
  ‹tvdom_aivdom_at = tvdom_aivdom_at_int o get_content›
  by (intro ext, rename_tac x y, case_tac x) (auto simp: tvdom_aivdom_at_int_def tvdom_aivdom_at_def)

definition length_ivdom_aivdom_int :: ‹aivdom ⇒ nat› where
  ‹length_ivdom_aivdom_int = (λ(a,b,c,d). length c)›

definition length_ivdom_aivdom :: ‹isasat_aivdom ⇒ nat› where
  ‹length_ivdom_aivdom ai = length (get_ivdom_aivdom ai)›

lemma length_ivdom_aivdom_alt_def:
  ‹length_ivdom_aivdom = length_ivdom_aivdom_int o get_content›
  by (intro ext, rename_tac x, case_tac x) (auto simp: length_ivdom_aivdom_def length_ivdom_aivdom_int_def)

definition length_avdom_aivdom_int :: ‹aivdom ⇒ nat› where
  ‹length_avdom_aivdom_int = (λ(a,b,c). length b)›

definition length_avdom_aivdom :: ‹isasat_aivdom ⇒ nat› where
  ‹length_avdom_aivdom ai = length (get_avdom_aivdom ai)›

lemma length_avdom_aivdom_alt_def:
  ‹length_avdom_aivdom = length_avdom_aivdom_int o get_content›
  by (intro ext, rename_tac x, case_tac x) (auto simp: length_avdom_aivdom_def length_avdom_aivdom_int_def)

definition length_vdom_aivdom_int :: ‹aivdom ⇒ nat› where
  ‹length_vdom_aivdom_int = (λ(a,b,c). length a)›

definition length_vdom_aivdom :: ‹isasat_aivdom ⇒ nat› where
  ‹length_vdom_aivdom ai = length (get_vdom_aivdom ai)›

lemma length_vdom_aivdom_alt_def:
  ‹length_vdom_aivdom = length_vdom_aivdom_int o get_content›
  by (intro ext, rename_tac x, case_tac x) (auto simp: length_vdom_aivdom_def length_vdom_aivdom_int_def)

definition length_tvdom_aivdom_int :: ‹aivdom ⇒ nat› where
  ‹length_tvdom_aivdom_int = (λ(a,b,c,d). length d)›

definition length_tvdom_aivdom :: ‹isasat_aivdom ⇒ nat› where
  ‹length_tvdom_aivdom ai = length (get_tvdom_aivdom ai)›

lemma length_tvdom_aivdom_alt_def:
  ‹length_tvdom_aivdom = length_tvdom_aivdom_int o get_content›
  by (intro ext, rename_tac x, case_tac x) (auto simp: length_tvdom_aivdom_def length_tvdom_aivdom_int_def)


definition add_init_clause_aivdom_strong_int where
  ‹add_init_clause_aivdom_strong_int = (λ C (vdom, avdom, ivdom, tvdom). (vdom @ [C], avdom, ivdom @ [C], tvdom @ [C]))›

definition add_init_clause_aivdom_strong :: ‹_ ⇒ isasat_aivdom ⇒ isasat_aivdom› where
  ‹add_init_clause_aivdom_strong C ≡ AIvdom o add_init_clause_aivdom_strong_int C o get_aivdom›

lemma aivdom_inv_intro_init_strong_add_mset:
  ‹C ∉# d ⟹ C ∉ set vdom ⟹ aivdom_inv_strong (vdom, avdom, ivdom, tvdom) d ⟹ aivdom_inv_strong (vdom @ [C], avdom, ivdom @ [C], tvdom @ [C]) (add_mset C d)›
  unfolding aivdom_inv_alt_def
  by (cases ‹C ∈ (set (avdom) ∪ set (ivdom))›)
    (auto dest: subset_mset_imp_subset_add_mset simp: add_init_clause_aivdom_strong_int_def
    split: code_hider.splits)

lemma aivdom_inv_dec_intro_init_strong_add_mset:
  ‹C ∉# d ⟹ C ∉ set (get_vdom_aivdom aivdom) ⟹ aivdom_inv_strong_dec aivdom d ⟹ aivdom_inv_strong_dec (add_init_clause_aivdom_strong C aivdom) (add_mset C d)›
  using aivdom_inv_intro_init_strong_add_mset[of C d ‹get_vdom_aivdom aivdom› ‹get_avdom_aivdom aivdom›
    ‹get_ivdom_aivdom aivdom› ‹get_tvdom_aivdom aivdom›]
  by (cases aivdom)
    (auto simp: aivdom_inv_dec_def add_init_clause_aivdom_strong_int_def add_init_clause_aivdom_strong_def
    aivdom_inv_strong_dec_def
    simp del: aivdom_inv.simps)

definition add_learned_clause_aivdom_strong_int where
  ‹add_learned_clause_aivdom_strong_int = (λ C (vdom, avdom, ivdom, tvdom). (vdom @ [C], avdom @ [C], ivdom, tvdom @ [C]))›

definition add_learned_clause_aivdom_strong :: ‹_ ⇒ isasat_aivdom ⇒ isasat_aivdom› where
  ‹add_learned_clause_aivdom_strong C ≡ AIvdom o add_learned_clause_aivdom_strong_int C o get_aivdom›

lemma aivdom_inv_intro_learned_strong_add_mset:
  ‹C ∉# d ⟹ C ∉ set vdom ⟹ aivdom_inv_strong (vdom, avdom, ivdom, tvdom) d ⟹ aivdom_inv_strong (vdom @ [C], avdom @ [C], ivdom, tvdom @ [C]) (add_mset C d)›
  unfolding aivdom_inv_alt_def
  by (cases ‹C ∈ (set (avdom) ∪ set (ivdom))›)
    (auto dest: subset_mset_imp_subset_add_mset simp: add_learned_clause_aivdom_strong_int_def
    split: code_hider.splits)

lemma aivdom_inv_dec_intro_learned_strong_add_mset:
  ‹C ∉# d ⟹ C ∉ set (get_vdom_aivdom aivdom) ⟹ aivdom_inv_strong_dec aivdom d ⟹ aivdom_inv_strong_dec (add_learned_clause_aivdom_strong C aivdom) (add_mset C d)›
  using aivdom_inv_intro_learned_strong_add_mset[of C d ‹get_vdom_aivdom aivdom› ‹get_avdom_aivdom aivdom›
    ‹get_ivdom_aivdom aivdom› ‹get_tvdom_aivdom aivdom›]
  by (cases aivdom)
    (auto simp: aivdom_inv_dec_def add_learned_clause_aivdom_strong_int_def add_learned_clause_aivdom_strong_def
    aivdom_inv_strong_dec_def
    simp del: aivdom_inv.simps)

lemma [simp]:
  ‹get_vdom_aivdom (add_learned_clause_aivdom C aivdom) = get_vdom_aivdom aivdom @ [C]›
  ‹get_avdom_aivdom (add_learned_clause_aivdom C aivdom) = get_avdom_aivdom aivdom @ [C]›
  ‹get_ivdom_aivdom (add_learned_clause_aivdom C aivdom) = get_ivdom_aivdom aivdom›
  ‹get_tvdom_aivdom (add_learned_clause_aivdom C aivdom) = get_tvdom_aivdom aivdom›
  ‹get_vdom_aivdom (add_init_clause_aivdom C aivdom) = get_vdom_aivdom aivdom @ [C]›
  ‹get_avdom_aivdom (add_init_clause_aivdom C aivdom) = get_avdom_aivdom aivdom›
  ‹get_ivdom_aivdom (add_init_clause_aivdom C aivdom) = get_ivdom_aivdom aivdom  @ [C]›
  ‹get_tvdom_aivdom (add_init_clause_aivdom C aivdom) = get_tvdom_aivdom aivdom›
  ‹get_vdom_aivdom (add_learned_clause_aivdom_strong C aivdom) = get_vdom_aivdom aivdom @ [C]›
  ‹get_avdom_aivdom (add_learned_clause_aivdom_strong C aivdom) = get_avdom_aivdom aivdom @ [C]›
  ‹get_ivdom_aivdom (add_learned_clause_aivdom_strong C aivdom) = get_ivdom_aivdom aivdom›
  ‹get_tvdom_aivdom (add_learned_clause_aivdom_strong C aivdom) = get_tvdom_aivdom aivdom @ [C]›
  ‹get_vdom_aivdom (add_init_clause_aivdom_strong C aivdom) = get_vdom_aivdom aivdom @ [C]›
  ‹get_avdom_aivdom (add_init_clause_aivdom_strong C aivdom) = get_avdom_aivdom aivdom›
  ‹get_ivdom_aivdom (add_init_clause_aivdom_strong C aivdom) = get_ivdom_aivdom aivdom  @ [C]›
  ‹get_tvdom_aivdom (add_init_clause_aivdom_strong C aivdom) = get_tvdom_aivdom aivdom @ [C]›
  by (cases aivdom; auto simp: add_learned_clause_aivdom_def add_learned_clause_aivdom_int_def
    add_learned_clause_aivdom_strong_def add_learned_clause_aivdom_strong_int_def
    add_init_clause_aivdom_strong_def add_init_clause_aivdom_strong_int_def
    add_init_clause_aivdom_def add_init_clause_aivdom_int_def; fail)+

definition empty_aivdom_int where
  ‹empty_aivdom_int = (λ(vdom, avdom, ivdom, tvdom). (take 0 vdom, take 0 avdom, take 0 ivdom, take 0 tvdom))›

definition empty_aivdom :: ‹isasat_aivdom ⇒ isasat_aivdom› where
  ‹empty_aivdom = Constructor o empty_aivdom_int o get_content›

lemma [simp]:
  ‹get_vdom_aivdom (empty_aivdom aivdom) = []›
  ‹get_avdom_aivdom (empty_aivdom aivdom) = []›
  ‹get_ivdom_aivdom (empty_aivdom aivdom) = []›
  ‹get_tvdom_aivdom (empty_aivdom aivdom) = []›
  ‹aivdom_inv_dec (empty_aivdom aivdom) {#}›
  ‹aivdom_inv_strong_dec (empty_aivdom aivdom) {#}›
  by (auto simp: empty_aivdom_def empty_aivdom_int_def aivdom_inv_dec_alt_def
    aivdom_inv_strong_dec_def)

fun swap_avdom_aivdom where
  ‹swap_avdom_aivdom (AIvdom (vdom, avdom, ivdom, tvdom)) i j =
  (AIvdom (vdom, swap avdom i j, ivdom, tvdom))›

lemma [simp]:
  ‹get_avdom_aivdom (swap_avdom_aivdom aivdom i j) = swap (get_avdom_aivdom aivdom) i j›
  ‹get_vdom_aivdom (swap_avdom_aivdom aivdom i j) = (get_vdom_aivdom aivdom)›
  ‹get_ivdom_aivdom (swap_avdom_aivdom aivdom i j) = (get_ivdom_aivdom aivdom)›
  ‹get_tvdom_aivdom (swap_avdom_aivdom aivdom i j) = (get_tvdom_aivdom aivdom)›
  by (cases aivdom; auto simp:)+

fun take_avdom_aivdom where
  ‹take_avdom_aivdom i (AIvdom (vdom, avdom, ivdom, tvdom)) =
  (AIvdom (vdom, take i avdom, ivdom, tvdom))›

lemma [simp]:
  ‹get_avdom_aivdom (take_avdom_aivdom i aivdom) = take i (get_avdom_aivdom aivdom)›
  ‹get_vdom_aivdom (take_avdom_aivdom i aivdom) = get_vdom_aivdom aivdom›
  ‹get_tvdom_aivdom (take_avdom_aivdom i aivdom) = get_tvdom_aivdom aivdom›
  ‹get_ivdom_aivdom (take_avdom_aivdom i aivdom) = get_ivdom_aivdom aivdom›
  by (cases aivdom; auto simp:; fail)+

definition map_vdom_aivdom :: ‹_› where
  ‹map_vdom_aivdom f = (λx. case x of AIvdom (vdom, avdom, ivdom, tvdom) ⇒ do {
    avdom ← f avdom;
    RETURN (AIvdom (vdom, avdom, ivdom, tvdom))
  })›

definition map_tvdom_aivdom :: ‹_› where
  ‹map_tvdom_aivdom f = (λx. case x of AIvdom (vdom, avdom, ivdom, tvdom) ⇒ do {
    tvdom ← f tvdom;
    RETURN (AIvdom (vdom, avdom, ivdom, tvdom))
  })›

definition AIvdom_init :: ‹nat list ⇒ nat list ⇒ nat list ⇒ isasat_aivdom› where
  ‹AIvdom_init vdom avdom ivdom = AIvdom (vdom, avdom, ivdom, vdom)›


definition push_to_tvdom_int where
  ‹push_to_tvdom_int = (λ C (vdom, avdom, ivdom, tvdom). (vdom, avdom, ivdom, tvdom @ [C]))›

definition push_to_tvdom :: ‹_ ⇒ isasat_aivdom ⇒ isasat_aivdom› where
  ‹push_to_tvdom C ≡ AIvdom o push_to_tvdom_int C o get_aivdom›

lemma aivdom_inv_push_to_tvdom_int:
  ‹C ∈ set vdom ⟹ C ∉ set tvdom ⟹ aivdom_inv (vdom, avdom, ivdom, tvdom) d ⟹ aivdom_inv (vdom, avdom, ivdom, tvdom @ [C]) d›
  unfolding aivdom_inv_alt_def
  by (auto dest: subset_mset_imp_subset_add_mset simp: add_learned_clause_aivdom_strong_int_def
    split: code_hider.splits)

lemma aivdom_push_to_tvdom:
  ‹C ∈ set (get_vdom_aivdom aivdom) ⟹ C ∉ set (get_tvdom_aivdom aivdom) ⟹ aivdom_inv_dec aivdom d ⟹ aivdom_inv_dec (push_to_tvdom C aivdom) d›
  using aivdom_inv_push_to_tvdom_int[of C ‹get_vdom_aivdom aivdom› ‹get_tvdom_aivdom aivdom›
    ‹get_avdom_aivdom aivdom› ‹get_ivdom_aivdom aivdom› d]
  by (cases aivdom)
    (auto simp: aivdom_inv_dec_def add_learned_clause_aivdom_strong_int_def add_learned_clause_aivdom_strong_def
    aivdom_inv_strong_dec_def push_to_tvdom_def push_to_tvdom_int_def
    simp del: aivdom_inv.simps)

fun empty_tvdom_int where
  ‹empty_tvdom_int (vdom, avdom, ivdom, tvdom) = (vdom, avdom, ivdom, take 0 tvdom)›

definition empty_tvdom where
  ‹empty_tvdom = AIvdom o empty_tvdom_int o get_content›

lemma get_aivdom_add_learned_clause_aivdom[simp]:
  ‹get_vdom_aivdom (add_learned_clause_aivdom x2 vdom) = get_vdom_aivdom vdom @ [x2]›
  ‹get_avdom_aivdom (add_learned_clause_aivdom x2 vdom) = get_avdom_aivdom vdom @ [x2]›
  ‹get_ivdom_aivdom (add_learned_clause_aivdom x2 vdom) = get_ivdom_aivdom vdom›
  by (cases vdom; auto simp: add_learned_clause_aivdom_def add_learned_clause_aivdom_int_def; fail)+

end