Theory Destabilization_side

theory Destabilization_side
  imports Basics_side
begin

section ‹The Destabilization Mechanism for TD\_side›

subsection ‹Definition of the Full Destabilization Mechanism›

function (domintros)
  destab_iter :: "'x list ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ ('x + 'g, 'x list) fmap × 'x set"
  and destab :: "'x + 'g ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ ('x + 'g, 'x list) fmap × 'x set"
where
  "destab_iter [] i s = (i, s)"
| "destab_iter (y # ys) i s = (
    let (i, s) = destab (Inl y) i (s - {y}) in
    destab_iter ys i s)"
| "destab x i s = destab_iter (fmlookup_default i [] x) (fmdrop x i) s"
  by pat_completeness auto


subsubsection ‹Termination Proof›

definition destab_iter_dom :: "'x list ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ bool" where
  "destab_iter_dom ls i s = destab_iter_destab_dom (Inl (ls, i, s))"
declare destab_iter_dom_def[simp]

definition destab_dom :: "'x + 'g ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ bool" where
  "destab_dom y i s = destab_iter_destab_dom (Inr (y, i, s))"
declare destab_dom_def[simp]

lemma destab_domintros:
  "destab_dom (Inl y) i (s - {y}) ⟹
    destab (Inl y) i (s - {y}) = (i', s') ⟹
    destab_iter_dom ys i' s' ⟹
    destab_iter_dom (y # ys) i s"
  "destab_iter_dom (fmlookup_default i [] x) (fmdrop x i) s ⟹ destab_dom x i s"
  using destab_iter_destab.domintros by fastforce+

definition count_non_empty :: "('a, 'b list) fmap ⇒ nat" where
  "count_non_empty m = fcard (ffilter ((≠) [] ∘ snd) (fset_of_fmap m))"

lemma count_non_empty_dec_fmdrop:
  assumes "fmlookup_default m [] x ≠ []"
  shows "Suc (count_non_empty (fmdrop x m)) = count_non_empty m"
proof -
  obtain ys where ys_def: "ys = fmlookup_default m [] x" and ys_non_empty: "ys ≠ []"
    using assms by simp
  then have in_map: "(x, ys) |∈| fset_of_fmap m"
    unfolding fmlookup_default_def
    by (cases "fmlookup m x"; auto)
  then have eq: "fset_of_fmap (fmdrop x m) = fset_of_fmap m |-| {|(x, ys)|}"
    by (auto split: if_splits)
  then have "ffilter ((≠) [] ∘ snd) (fset_of_fmap (fmdrop x m))
      = (ffilter ((≠) [] ∘ snd) (fset_of_fmap m)) |-| {|(x, ys)|}" by fastforce
  then show ?thesis
    unfolding count_non_empty_def
    using in_map ys_non_empty fcard_Suc_fminus1[of "(x, ys)"]
    by auto
qed

lemma count_non_empty_eq_fmdrop:
  assumes "fmlookup_default m [] x = []"
  shows "count_non_empty (fmdrop x m) = count_non_empty m"
proof -
  have "ffilter ((≠) [] ∘ snd) (fset_of_fmap (fmdrop x m))
      = (ffilter ((≠) [] ∘ snd) (fset_of_fmap m))"
    using assms
    unfolding fmlookup_default_def
    by (auto split: if_splits)
  thus ?thesis unfolding count_non_empty_def by simp
qed

lemma count_non_empty_fmdrop:
  shows "count_non_empty (fmdrop x m) ≤ count_non_empty m"
  apply (cases "fmlookup_default m [] x = []")
  subgoal using count_non_empty_eq_fmdrop by fastforce
  subgoal using count_non_empty_dec_fmdrop by fastforce
  done

lemma destab_reduces_count_non_empty:
  "destab_iter_dom ys i s ⟹ (i',s') = destab_iter ys i s ⟹
    count_non_empty i' ≤ count_non_empty i"
  "destab_dom x i s ⟹ (i',s') = destab x i s ⟹
    count_non_empty i' ≤ count_non_empty i"
  unfolding destab_iter_dom_def destab_dom_def
proof (induction ys i s and x i s arbitrary: i' s' and i' s'
       rule: destab_iter_destab.pinduct)
  case (1 i s c)
  show ?case using destab_iter.psimps(1)[OF 1(1)] 1(2) by simp
next
  case (2 y ys i s)
  obtain i1 s1 where i1_s1_def: "(i1, s1) = destab (Inl y) i (s - {y})"
    by (cases "destab (Inl y) i (s - {y})") simp
  then have destab_iter_2: "(i', s') = destab_iter ys i1 s1"
    using 2(4) destab_iter.psimps(2)[OF 2(1)] by (simp split: prod.splits)
  show ?case using 2(3)[OF i1_s1_def _ destab_iter_2] 2(2)[OF i1_s1_def] by simp
next
  case (3 x i s c)
  show ?case
    using destab.psimps[OF 3(1)] order.trans[OF 3(2) count_non_empty_fmdrop] 3(3) by simp
qed

abbreviation
  "term_relation_destab ≡
    let extract = (λp. case p of Inl (ys,i,s) ⇒ (count_non_empty i, length ys, 0)
      | Inr (x,i,s) ⇒ (count_non_empty i, 0, 1)) in
    let r = lex_prod less_than (lex_prod less_than less_than) in
    inv_image r extract"

termination
  apply (relation term_relation_destab)
  subgoal using wf_lex_prod wf_less by auto
  subgoal by simp
  subgoal for y ys i s x i' s'
    using destab_reduces_count_non_empty(2)[of "Inl y" i "s - {y}" i' s']
    by (auto split: prod.split)
  subgoal for x i s
    apply (cases "fmlookup_default i [] x = []")
    subgoal using count_non_empty_eq_fmdrop[of i x] by simp
    subgoal using count_non_empty_dec_fmdrop[of i x] by simp
    done
  done


subsubsection ‹Equivalence with definition based on fold›

lemma destab_iter_equals_fold:
  "destab x infl stabl =
    (let f = λy (infl, stabl). destab (Inl y) infl (stabl - {y}) in
    fold f (fmlookup_default infl [] x) (fmdrop x infl, stabl))"
proof -
  let ?f = "λy (infl, stabl). destab (Inl y) infl (stabl - {y})"
  have "destab_iter ys infl stabl =
    (let f = ?f in fold f ys (infl, stabl))"
  "destab x infl stabl =
    (let f = ?f in fold f (fmlookup_default infl [] x) (fmdrop x infl, stabl))" for ys
    by (induction ys infl stabl and x infl stabl rule: destab_iter_destab.induct)
       (auto split: prod.splits)
  then show ?thesis by simp
qed


subsubsection ‹Description of the Effect of Destabilize›

text‹To describe the effect of a call to the function @{term destab}, we define an inductive
  set that, based on some @{term infl} map, collects all unknowns transitively influenced by some
  unknown @{term x}.›

inductive_set influenced_by :: "('x + 'g, 'x list) fmap ⇒ 'x + 'g ⇒ 'x set" for infl x where
  base: "fmlookup infl x = Some ys ⟹ y ∈ set ys ⟹ y ∈ influenced_by infl x"
| step: "y ∈ influenced_by infl x ⟹ fmlookup infl (Inl y) = Some zs ⟹ z ∈ set zs
    ⟹ z ∈ influenced_by infl x"
inductive_set influenced_by_cutoff ::
    "('x + 'g, 'x list) fmap ⇒ 'x + 'g ⇒ ('x + 'g) set ⇒ 'x set" for infl x c where
  base: "x ∉ c ⟹ fmlookup infl x = Some ys ⟹ y ∈ set ys ⟹ y ∈ influenced_by_cutoff infl x c"
| step: "y ∈ influenced_by_cutoff infl x c ⟹ Inl y ∉ c ⟹ fmlookup infl (Inl y) = Some zs
    ⟹ z ∈ set zs ⟹ z ∈ influenced_by_cutoff infl x c"

lemma influenced_by_aux:
  shows "influenced_by i x = (⋃y ∈ slookup i x. insert y (influenced_by (fmdrop x i) (Inl y)))"
unfolding fmlookup_default_def
proof(intro equalityI subsetI, goal_cases)
  case (1 u)
  then show ?case
  proof(induction rule: influenced_by.induct)
    case (step y zs z)
    then show ?case
    proof(cases "y ∈ slookup i x")
      case True
      then show ?thesis
        using step.hyps(2,3) influenced_by.base[of "fmdrop x i" "Inl y"]
        by (cases rule: set_fmlookup_default_cases, cases "x = Inl y") auto
    next
      case False
      then show ?thesis
        using step.IH step.hyps(2,3) influenced_by.step[of y "fmdrop x i"]
        by (cases rule: notin_fmlookup_default_cases, cases "x = Inl y") auto
    qed
  qed auto
next
  case (2 z)
  then show ?case
  proof(cases "fmlookup i x")
    case (Some xs)
    then obtain y where z_mem: "z ∈ insert y (influenced_by (fmdrop x i) (Inl y))"
      and step: "y ∈ set (case fmlookup i x of None ⇒ [] | Some v ⇒ v)" using 2 by blast
    then show ?thesis using Some influenced_by.base
    proof(cases "z = y")
      case False
      then have "z ∈ influenced_by (fmdrop x i) (Inl y)" using z_mem by auto
      then show ?thesis
      proof(induction rule: influenced_by.induct)
        case (base ys' y')
        then show ?case
          using Some step influenced_by.base[of i] influenced_by.step[OF influenced_by.base[of i]]
          by (auto split: if_splits)
      next
        case (step y' zs z)
        then show ?case using influenced_by.step
          by (auto split: if_splits)
      qed
    qed simp
  qed simp
qed

lemma lookup_in_influenced:
  shows "slookup i x ⊆ influenced_by i x"
proof(intro subsetI, goal_cases)
  case (1 y)
  then show ?case using influenced_by.base[of i x]
  by (cases rule: set_fmlookup_default_cases) simp
qed

lemma influenced_unknowns_fmdrop_set:
  shows "influenced_by (fmdrop_set C i) x = influenced_by_cutoff i x C"
proof (intro equalityI subsetI, goal_cases)
  case (1 u)
  then show ?case
    by (induction rule: influenced_by.induct;
           simp add: influenced_by_cutoff.base influenced_by_cutoff.step split: if_splits)
next
  case (2 u)
  then show ?case
    apply (induction rule: influenced_by_cutoff.induct)
    subgoal by (simp add: influenced_by.base image_iff)
    subgoal
      by (metis influenced_by.step[of _ "fmdrop_set C i" x]
          fmlookup_drop_set[of C i "Inl _"])
    done
qed

lemma influenced_by_transitive:
  assumes "y ∈ influenced_by i x"
    and "z ∈ influenced_by i (Inl y)"
  shows "z ∈ influenced_by i x"
  using assms
proof (induction rule: influenced_by.induct)
  case (base ys y)
  show ?case using base(3,1,2) influenced_by.step[of _ i x]
  proof (induction rule: influenced_by.induct)
    case (base us u)
    then show ?case using influenced_by.base[of i x ys y] by simp
  qed simp
next
  case (step u vs v)
  have "z ∈ influenced_by i (Inl u)" using step(5,1-4)
  proof (induction rule: influenced_by.induct)
    case (base ys y)
    then show ?case using influenced_by.base[of i] influenced_by.step[of v i] by auto
  next
    case (step y zs z)
    then show ?case using influenced_by.step[of _ i] by auto
  qed
  then show ?case using step by auto
qed

lemma influenced_cutoff_subset:
  "influenced_by_cutoff i x C ⊆ influenced_by i x"
proof (intro subsetI, goal_cases)
  case (1 y)
  then show ?case
    by (induction rule: influenced_by_cutoff.induct)
      (auto simp add: influenced_by.base influenced_by.step)
qed

lemma influenced_cutoff_subset_2:
  shows "influenced_by i x - (⋃y ∈ C. influenced_by i y) ⊆ influenced_by_cutoff i x C"
proof (intro equalityI subsetI, elim DiffE, goal_cases)
  case (1 y)
  then show ?case
  proof (induction rule: influenced_by.induct)
    case (base ys z)
    then show ?case
      using 1 influenced_by_cutoff.base
      by (smt (verit, ccfv_threshold) UN_iff imageE)
  next
    case (step y zs z)
    then show ?case
      using influenced_by.base[OF step(2,3)] influenced_by.step[of y i]
        influenced_by_cutoff.step[of y i x C zs z]
      by blast
  qed
qed

lemma union_influenced_to_cutoff:
  shows "insert y (influenced_by i (Inl y)) ∪ influenced_by i x =
    insert y (influenced_by i (Inl y)) ∪ influenced_by_cutoff i x
    (Inl ` (insert y (influenced_by i (Inl y))))"
proof -
  have "u ∈ influenced_by i (Inl y)"
    if "u ≠ y" and "u ∉ influenced_by_cutoff i x (Inl ` (insert y (influenced_by i (Inl y))))"
      and "u ∈ influenced_by i x" for u
    using that influenced_cutoff_subset_2[of i x "Inl ` (insert y (influenced_by i (Inl y)))"]
      influenced_by_transitive[of _ i "Inl y"] by auto
  moreover have "u ∈ influenced_by i (Inl y)"
    if "u ≠ y" and "u ∉ influenced_by i x"
      and "u ∈ influenced_by_cutoff i x (Inl ` (insert y (influenced_by i (Inl y))))" for u
    using that(3)
  proof (induction rule: influenced_by_cutoff.induct)
    case (base ys y)
    then show ?case using that(2,3) influenced_cutoff_subset[of i x] by auto
  qed simp
  ultimately show ?thesis by auto
qed

lemma destab_iter_infl_stabl_relation:
  shows
    "(infl', stabl') = destab_iter xs i s
    ⟹ infl' = fmdrop_set (⋃x ∈ set xs. Inl ` (insert x (influenced_by i (Inl x)))) i
    ∧ stabl' = s - (⋃x ∈ set xs. insert x (influenced_by i (Inl x)))"
  and destab_infl_stabl_relation:
    "(infl', stabl') = destab x i s
    ⟹ infl' = fmdrop_set (insert x (Inl ` influenced_by i x)) i
    ∧ stabl' = s - influenced_by i x"
proof (induction xs i s and x i s
    arbitrary: infl' stabl' and infl' stabl' rule: destab_iter_destab.induct)
  case (1 infl stabl)
  then show ?case by simp
next
  case (2 y ys infl stabl)
  then obtain infl'' stabl'' where
    destab_y: "(infl'', stabl'') = destab (Inl y) infl (stabl - {y})"
    and destab_ys: "(infl', stabl') = destab_iter ys infl'' stabl''"
    by (cases "destab (Inl y) infl (stabl - {y})"; auto)
  note IH1 = "2.IH"(1)[OF destab_y]
  note IH2 = "2.IH"(2)[OF destab_y _ destab_ys, simplified]

  define A where "A x ≡ insert x (influenced_by infl (Inl x))" for x
  define B where "B x ≡ insert x (influenced_by_cutoff infl (Inl x)
      (Inl ` (insert y (influenced_by infl (Inl y)))))" for x
  have A_union_B_simp: "A y ∪ (⋃x∈set ys. B x) = (⋃x∈set (y#ys). A x)"
    using union_influenced_to_cutoff[of y] A_def B_def
    by fastforce

  show ?case
  proof(intro conjI, goal_cases)
    case 1
      have "infl' = fmdrop_set (⋃x∈set ys. Inl ` B x) (fmdrop_set (Inl ` A y) infl)"
        using IH1 IH2 influenced_unknowns_fmdrop_set[of "Inl ` A y"] A_def B_def
        by (smt (verit, ccfv_SIG) Sup.SUP_cong
            influenced_unknowns_fmdrop_set image_insert)
      also have "... = fmdrop_set (Inl ` A y ∪ (⋃x∈set ys. Inl ` B x)) infl"
        by (simp add: Un_commute)
      also have "... = fmdrop_set (Inl ` (A y ∪ (⋃x∈set ys. B x))) infl"
        by (simp add: image_Un image_Union)
      also have "... = fmdrop_set (⋃x∈set (y # ys). Inl ` A x) infl"
        by (simp add: A_union_B_simp image_Un image_Union)
      finally show ?case
        using A_def B_def by auto
  next
    case 2
    have "stabl' = stabl - (A y ∪ (⋃x∈set ys. B x))"
      apply (simp add: conjunct2[OF IH1] conjunct2[OF IH2] conjunct1[OF IH1]
            influenced_unknowns_fmdrop_set[of "Inl ` A y"]
            flip: fmdrop_set_insert image_insert A_def B_def[folded A_def])
      using A_def by auto
    also have "... = stabl - (⋃x∈set (y#ys). A x)"
      using A_union_B_simp
      by auto
    finally show ?case
      using A_def B_def by auto
  qed
next
  case (3 y infl stabl)
  then have
    destab_y: "destab_iter (fmlookup_default infl [] y) (fmdrop y infl) stabl = (infl', stabl')"
    by (metis destab.simps)
  note IH = "3.IH"[OF destab_y[symmetric]]
  then show ?case
    by (simp add: influenced_by_aux[of infl, symmetric]
        flip: image_insert fmdrop_set_insert image_UN)
qed


subsection ‹Definition of the Optimized Destabilization Mechanism›

function (domintros)
  destab_iter_opt ::
    "'x list ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x + 'g, 'x list) fmap × 'x set"
  and destab_opt ::
    "'x + 'g ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x + 'g, 'x list) fmap × 'x set"
where
  "destab_iter_opt [] i s c = (i, s)"
| "destab_iter_opt (y # ys) i s c = (
    let (i, s) = (if y ∈ c then (i, s - {y}) else destab_opt (Inl y) i (s - {y}) c) in
    destab_iter_opt ys i s c)"
| "destab_opt x i s c = destab_iter_opt (fmlookup_default i [] x) (fmdrop x i) s c"
  by pat_completeness auto


subsubsection ‹Termination Proof›

definition destab_iter_opt_dom ::
  "'x list ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ bool" where
  "destab_iter_opt_dom ls i s c = destab_iter_opt_destab_opt_dom (Inl (ls, i, s, c))"
declare destab_iter_opt_dom_def[simp]

definition destab_opt_dom :: "'x + 'g ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ bool" where
  "destab_opt_dom y i s c = destab_iter_opt_destab_opt_dom (Inr (y, i, s, c))"
declare destab_opt_dom_def[simp]

lemma destab_opt_reduces_count_non_empty:
  "destab_iter_opt_dom ys i s c ⟹ (i',s') = destab_iter_opt ys i s c ⟹
    count_non_empty i' ≤ count_non_empty i"
  "destab_opt_dom x i s c ⟹ (i',s') = destab_opt x i s c ⟹
    count_non_empty i' ≤ count_non_empty i"
  unfolding destab_iter_opt_dom_def destab_opt_dom_def
proof (induction ys i s c and x i s c arbitrary: i' s' and i' s'
       rule: destab_iter_opt_destab_opt.pinduct)
  case (1 i s c)
  show ?case using destab_iter_opt.psimps(1)[OF 1(1)] 1(2) by simp
next
  case (2 y ys i s c)
  obtain i1 s1 where i1_s1_def: "(i1, s1) = destab_opt (Inl y) i (s - {y}) c"
    by (cases "destab_opt (Inl y) i (s - {y}) c") simp
  then have destab_iter_2: "(i', s') = destab_iter_opt ys i1 s1 c" if "y ∉ c"
    using that 2(4) destab_iter_opt.psimps(2)[OF 2(1)] by (simp split: prod.splits)
  have destab_iter_2': "(i', s') = destab_iter_opt ys i (s - {y}) c" if "y ∈ c"
    using that 2(4) destab_iter_opt.psimps(2)[OF 2(1)] by (simp split: prod.splits)
  show ?case
    apply (cases "y ∈ c")
    subgoal using 2(3)[OF _ _ destab_iter_2'] by simp
    subgoal using 2(3)[OF _ _ destab_iter_2] 2(2)[OF _ i1_s1_def] i1_s1_def by simp
    done
next
  case (3 x i s c)
  show ?case
    using destab_opt.psimps[OF 3(1)] order.trans[OF 3(2) count_non_empty_fmdrop] 3(3) by simp
qed

abbreviation
  "term_relation_destab_opt ≡
    let extract = (λp. case p of Inl (ys,i,s,c) ⇒ (count_non_empty i, length ys, 0)
      | Inr (x,i,s,c) ⇒ (count_non_empty i, 0, 1)) in
    let r = lex_prod less_than (lex_prod less_than less_than) in
    inv_image r extract"

termination
  apply (relation term_relation_destab_opt)
  subgoal using wf_lex_prod wf_less by auto
  subgoal by simp
  subgoal for y ys i s c x i' s'
    apply (cases "y ∈ c")
    subgoal by auto
    subgoal using destab_opt_reduces_count_non_empty(2)[of "Inl y" i "s - {y}" c i' s'] by auto
    done
  subgoal for x i s c
    apply (cases "fmlookup_default i [] x = []")
    subgoal using count_non_empty_eq_fmdrop[of i x] by simp
    subgoal using count_non_empty_dec_fmdrop[of i x] by simp
    done
  done


subsubsection ‹Equivalence with definition based on fold›

lemma destab_iter_opt_equals_fold:
  "destab_opt x infl stabl cutoff =
    (let f = λy (infl, stabl). (
      if y ∈ cutoff then (infl, stabl - {y})
      else destab_opt (Inl y) infl (stabl - {y}) cutoff) in
    fold f (fmlookup_default infl [] x) (fmdrop x infl, stabl))"
proof -
  let ?f = "λy (infl, stabl). (if y ∈ cutoff then (infl, stabl - {y})
    else destab_opt (Inl y) infl (stabl - {y}) cutoff)"
  have "destab_iter_opt ys infl stabl cutoff =
    (let f = ?f in fold f ys (infl, stabl))"
  "destab_opt x infl stabl cutoff =
    (let f = ?f in fold f (fmlookup_default infl [] x) (fmdrop x infl, stabl))" for ys
    by (induction ys infl stabl cutoff and x infl stabl cutoff
        rule: destab_iter_opt_destab_opt.induct)
       (auto split: prod.splits)
  then show ?thesis by simp
qed


subsubsection ‹Description of the Effect of the Optimized Destabilize›

lemma influenced_by_cutoff_aux:
  assumes "x ∉ c"
  shows "influenced_by_cutoff i x c =
    (⋃y ∈ slookup i x. insert y (influenced_by_cutoff (fmdrop x i) (Inl y) c))"
unfolding fmlookup_default_def
proof(intro equalityI subsetI, goal_cases)
  case (1 u)
  then show ?case
  proof(induction rule: influenced_by_cutoff.induct)
    case (step y zs z)
    then show ?case
    proof(cases "y ∈ slookup i x")
      case True
      then show ?thesis
        using step.hyps(2-4) influenced_by_cutoff.base[of "Inl y" _ "fmdrop x i"]
        by (cases rule: set_fmlookup_default_cases, cases "x = Inl y") auto
    next
      case False
      obtain u where "u ∈ slookup i x" "y ∈ influenced_by_cutoff (fmdrop x i) (Inl u) c"
        using step(5) False unfolding fmlookup_default_def by blast
      then show ?thesis
        apply (cases "x = Inl y")
        subgoal using step.hyps(3,4) by auto
        subgoal
          using influenced_by_cutoff.step[of _ "fmdrop x i"] step.hyps(2-4)
          unfolding fmlookup_default_def
          by fastforce
        done
    qed
  qed auto
next
  case (2 z)
  show ?case
  proof(cases "fmlookup i x")
    case None
    then show ?thesis using 2 by simp
  next
    case (Some xs)
    then obtain y where z_mem: "z ∈ insert y (influenced_by_cutoff (fmdrop x i) (Inl y) c)"
      and step: "y ∈ set (case fmlookup i x of None ⇒ [] | Some v ⇒ v)" using 2 by blast
    show ?thesis
    proof(cases "z = y")
      case True
      then show ?thesis using Some assms influenced_by_cutoff.base local.step by fastforce
   next
      case False
      then have "z ∈ influenced_by_cutoff (fmdrop x i) (Inl y) c" using z_mem by auto
      then show ?thesis
      proof(induction rule: influenced_by_cutoff.induct)
        case (base ys' y')
        then show ?case
          using assms Some step influenced_by_cutoff.base[of _ _ i]
            influenced_by_cutoff.step[OF influenced_by_cutoff.base[of _ _ i]]
          by (auto split: if_splits)
      next
        case (step y' zs z)
        then show ?case using influenced_by_cutoff.step by (auto split: if_splits)
      qed
    qed
  qed
qed

lemma lookup_in_influenced_cutoff:
  shows "slookup i x ⊆ influenced_by_cutoff i x (cu - {x})"
proof(intro subsetI, goal_cases)
  case (1 y)
  then show ?case using influenced_by_cutoff.base[of x]
  by (cases rule: set_fmlookup_default_cases) simp
qed

lemma influenced_cutoff_fmdrop_set:
  shows "influenced_by_cutoff (fmdrop_set C1 i) x C2 = influenced_by_cutoff i x (C1 ∪ C2)"
proof (intro equalityI subsetI, goal_cases)
  case (1 u)
  then show ?case
    by (induction rule: influenced_by_cutoff.induct;
           simp add: influenced_by_cutoff.base influenced_by_cutoff.step split: if_splits)
next
  case (2 u)
  then show ?case
    apply (induction rule: influenced_by_cutoff.induct)
    subgoal by (simp add: influenced_by_cutoff.base image_iff)
    subgoal for y zs z
      apply (rule influenced_by_cutoff.step[of y "fmdrop_set C1 i" x C2 zs z])
      by (simp add: fmlookup_drop_set[of C1 i "Inl y"])+
    done
qed

lemma in_cutoff_influenced_by_cutoff_empty:
  assumes "y ∈ c"
  shows "influenced_by_cutoff infl (Inl y) (Inl ` c) = {}"
proof (rule ccontr, goal_cases)
  case 1
  then obtain b where "b ∈ influenced_by_cutoff infl (Inl y) (Inl ` c)" by auto
  then show ?case using assms(1) by (induction rule: influenced_by_cutoff.induct) simp+
qed

lemma influenced_by_cutoff_transitive:
  assumes "y ∈ influenced_by_cutoff i x c"
    and "z ∈ influenced_by_cutoff i (Inl y) c"
  shows "z ∈ influenced_by_cutoff i x c"
  using assms
proof (induction rule: influenced_by_cutoff.induct)
  case (base ys y)
  show ?case using base(4,1-3) influenced_by_cutoff.step[of _ i x]
  proof (induction rule: influenced_by_cutoff.induct)
    case (base us u)
    then show ?case using influenced_by_cutoff.base[of x c i ys y] by simp
  qed simp
next
  case (step u vs v)
  have "z ∈ influenced_by_cutoff i (Inl u) c" using step(6,1-5)
  proof (induction rule: influenced_by_cutoff.induct)
    case (base ys y)
    then show ?case
      using influenced_by_cutoff.base[of _ _ i] influenced_by_cutoff.step[of v i] by auto
  next
    case (step y zs z)
    then show ?case using influenced_by_cutoff.step[of _ i] by blast
  qed
  then show ?case using step by auto
qed

lemma influenced_by_cutoff_union:
  "influenced_by_cutoff infl (Inl x)
    (Inl ` insert y (influenced_by_cutoff infl (Inl y) (Inl ` c)) ∪ Inl ` c)
    ∪ (insert y (influenced_by_cutoff infl (Inl y) (Inl ` c)))
  = influenced_by_cutoff infl (Inl x) (Inl ` c)
    ∪ (insert y (influenced_by_cutoff infl (Inl y) (Inl ` c)))"
proof -
  have "u ∈ influenced_by_cutoff infl (Inl x) (Inl ` c)"
    if "u ∈ influenced_by_cutoff infl (Inl x)
      (Inl ` insert y (influenced_by_cutoff infl (Inl y) (Inl ` c)) ∪ Inl ` c)"
      "u ∉ influenced_by_cutoff infl (Inl y) (Inl ` c)" "u ≠ y"
    for u
    by (metis fmdrop_set_twice influenced_cutoff_fmdrop_set
        influenced_cutoff_subset influenced_unknowns_fmdrop_set subset_eq
        that(1))
  moreover have "u ∈ influenced_by_cutoff infl (Inl x)
    (Inl ` insert y (influenced_by_cutoff infl (Inl y) (Inl ` c)) ∪ Inl ` c)"
    if "u ∈ influenced_by_cutoff infl (Inl x) (Inl ` c)"
      "u ∉ influenced_by_cutoff infl (Inl y) (Inl ` c)" "u ≠ y"
    for u
    using that(1,2)
  proof (induction rule: influenced_by_cutoff.induct)
    case (base zs z)
    show ?case
      apply (rule influenced_by_cutoff.base[where ?ys=zs])
      subgoal using base(1,4) influenced_by_cutoff.base[OF base(1-3)]
          influenced_by_cutoff_transitive[of x infl "Inl y" "Inl ` c" z] by auto
      subgoal using base(2) by simp
      subgoal using base(3) by simp
      done
  next
    case (step u zs z)
    show ?case
      apply (rule influenced_by_cutoff.step[of u _ _ _ zs])
      subgoal
        using step.IH influenced_by_cutoff.step[OF _ step.hyps(2-4)] step.prems by auto
      subgoal
        using step(2,6) influenced_by_cutoff.step[OF _ step.hyps(2-4)]
          influenced_by_cutoff.base[OF _ step.hyps(3,4)] by auto
      subgoal using step(3) by simp
      subgoal using step(4) by simp
      done
  qed
  ultimately show ?thesis using influenced_cutoff_fmdrop_set by auto
qed

lemma destab_iter_opt_infl_stabl_relation:
  shows
    "(infl', stabl') = destab_iter_opt xs i s c
    ⟹ infl' = fmdrop_set (⋃x ∈ set xs. Inl ` (insert x (influenced_by_cutoff i (Inl x) (Inl ` c)) - c)) i
    ∧ stabl' = s - (⋃x ∈ set xs. insert x (influenced_by_cutoff i (Inl x) (Inl ` c)))"
  and destab_opt_infl_stabl_relation:
    "(infl', stabl') = destab_opt x i s c ⟹ infl' = fmdrop_set (insert x
    (Inl ` (influenced_by_cutoff i x (Inl ` c - {x})) - (Inl ` c - {x}))) i
    ∧ stabl' = s - influenced_by_cutoff i x (Inl ` c - {x})"
proof (induction xs i s c and x i s c
    arbitrary: infl' stabl' and infl' stabl' rule: destab_iter_opt_destab_opt.induct)
  case (1 infl stabl c)
  then show ?case by simp
next
  case (2 y ys infl stabl c)
  obtain infl'' stabl'' where
    destab_y: "(infl'', stabl'') = (if y ∈ c then (infl, stabl - {y})
      else destab_opt (Inl y) infl (stabl - {y}) c)"
    and destab_ys: "(infl', stabl') = destab_iter_opt ys infl'' stabl'' c"
    using 2 by (cases "destab_opt (Inl y) infl (stabl - {y}) c"; auto split: if_splits)
  show ?case
  proof (cases "y ∈ c")
    case True
    then have same'': "infl'' = infl" "stabl'' = stabl - {y}"
      using destab_y by auto
    note IH = "2.IH"(2)[OF destab_y _ destab_ys, simplified]
    have "Inl ` ({y} - c ∪ influenced_by_cutoff infl (Inl y) (Inl ` c)) = {}"
      using True in_cutoff_influenced_by_cutoff_empty by fast
    then show ?thesis using IH same'' by auto
  next
    case False
    then have destab_y': "(infl'', stabl'') = destab_opt (Inl y) infl (stabl - {y}) c"
      using destab_y by auto
    note IH1 = "2.IH"(1)[OF False destab_y']
    note IH2 = "2.IH"(2)[OF destab_y _ destab_ys, simplified]

    define A where "A x ≡ insert x (influenced_by_cutoff infl (Inl x) (Inl ` c))" for x
    define B where "B x ≡ insert x (influenced_by_cutoff infl (Inl x) (Inl ` A y ∪ Inl ` c))"
      for x

    show ?thesis
    proof(intro conjI, goal_cases)
      case 1
      have "infl' = fmdrop_set ((⋃x∈set ys.
          Inl ` (insert x (
          influenced_by_cutoff (fmdrop_set (Inl ` (A y - c)) infl) (Inl x) (Inl ` c)) - c))
          ∪ Inl ` (A y - c))
        infl"
        using IH1 IH2 False unfolding A_def
        by (simp add: insert_Diff_if[of y _ c]
            flip: image_set_diff[of Inl _ "{y}", simplified] image_set_diff)
      also have "... = fmdrop_set ((⋃x∈set ys. Inl ` (B x - c)) ∪ Inl ` (A y - c)) infl"
        unfolding B_def
        by (simp add: influenced_cutoff_fmdrop_set flip: image_Un)
      also have "... = fmdrop_set ((⋃x∈set ys. Inl ` (B x ∪ A y - c)) ∪ Inl ` (A y - c)) infl"
        by (simp add: image_Un Un_Diff)
      also have "... = fmdrop_set ((⋃x∈set ys. Inl ` (A x ∪ A y - c)) ∪ Inl ` (A y - c)) infl"
        unfolding B_def
        apply (subst Un_insert_left)
        apply (subst influenced_by_cutoff_union[of infl _ y c, folded A_def])
        by (simp add: A_def flip: Un_insert_left del: Un_insert_right)
      also have "... = fmdrop_set (⋃x∈set (y#ys). Inl ` (A x - c)) infl"
        by (simp add: Un_Diff image_Un Un_commute)
      finally show ?case unfolding A_def by blast
    next
      case 2
      have "stabl' = stabl - A y -
        (⋃x∈set ys. insert x (influenced_by_cutoff infl (Inl x) (Inl ` (A y ∪ c))))"
        unfolding A_def
        using False
        by (fastforce simp add: IH1 IH2 influenced_cutoff_fmdrop_set
            simp flip: image_set_diff[of Inl _ "{y}", simplified] image_set_diff image_Un
            simp del: fmdrop_set_insert)
      also have "... = stabl - (A y ∪ (⋃x∈set ys. B x ∪ A y))"
        unfolding B_def
        by (fastforce simp add: image_Un)
      also have "... = stabl - (A y ∪ (⋃x∈set ys. A x ∪ A y))"
        unfolding B_def
        using influenced_by_cutoff_union[of infl _ y c, folded A_def]
        apply (subst Un_insert_left)
        apply (subst influenced_by_cutoff_union[of infl _ y c, folded A_def])
        by (simp add: A_def del: Un_insert_right)
      also have "... = stabl - (⋃x∈set (y#ys). A x)"
        by force
      finally show ?case unfolding A_def by simp
    qed
  qed
next
  case (3 y infl stabl c)
  then have
    destab_y: "destab_iter_opt (fmlookup_default infl [] y) (fmdrop y infl) stabl c = (infl', stabl')"
    by (metis destab_opt.simps)
  note IH = "3.IH"[OF destab_y[symmetric]]
  have 1: "influenced_by_cutoff (fmdrop y infl) (Inl x) (Inl ` c - {y}) =
    influenced_by_cutoff infl (Inl x) (insert y (Inl ` c))" for x
    by (simp add: influenced_cutoff_fmdrop_set[of "{_}", simplified])
  have 2: "insert y (S - (Inl ` c - {y})) = insert y (S - (Inl ` c))" for S
    by blast
  show ?case using IH
    apply (intro conjI)
    subgoal
      by (simp add: influenced_cutoff_fmdrop_set[of "{_}", simplified] influenced_by_cutoff_aux 1 2
          flip: image_UN image_set_diff)
    subgoal
      by (auto simp add: influenced_by_cutoff_aux influenced_cutoff_fmdrop_set[of "{_}",
            simplified])
    done
qed


text ‹Destabilization only removes unknowns from the stable set, so it preserves finiteness.
  Stated with the pair equation oriented as ‹prod.splits› produces it, for use as a
  ‹dest› rule.›

lemma destab_opt_stabl_finite:
  assumes "destab_opt x i s cs = (i', s')" and "finite s"
  shows "finite s'"
  using destab_opt_infl_stabl_relation[OF assms(1)[symmetric]] assms(2) by simp

subsection ‹Adapt simp rule set›

declare destab_opt.simps[simp del] destab.simps[simp del]

end