Theory Destabilization

theory Destabilization
  imports Basics
begin

section ‹The Destabilization Mechanism›

subsection ‹Definition of the Full Destabilization Mechanism›

text‹The destabilization function is called by the solver before continuing iteration because the
  value of an unknown changed. In this case, also the values of unknowns whose last evaluation was
  based on the outdated value, need to be re-evaluated again. This re-evaluation of influenced
  unknowns is enforced by following the entries for directly influenced unknowns in the map
  @{term infl} and removing all transitively influenced unknowns from @{term stabl}. This way,
  influenced unknowns are not re-evaluated immediately, but instead will be re-evaluated whenever
  they are queried again.
  We first define destab_iter as a mutual recursive function and prove its termination.
  Subsequently, we show that a simple definition that uses the fold function on lists may be used
  instead.›

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

definition destab_iter_dom where
  "destab_iter_dom ls infl stabl = destab_iter_destab_dom (Inl (ls, infl, stabl))"
declare destab_iter_dom_def[simp]

definition destab_dom where
  "destab_dom y infl stabl = destab_iter_destab_dom (Inr (y, infl, stabl))"
declare destab_dom_def[simp]

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


subsubsection ‹Termination Proof›

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)
  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 y i (s - {y})"
    by (cases "destab 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)
  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 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 y infl (stabl - {y}) in
    fold f (fmlookup_default infl [] x) (fmdrop x infl, stabl))"
proof -
  have "destab_iter ys infl stabl =
    (let f = λy (infl, stabl). destab y infl (stabl - {y}) in fold f ys (infl, stabl))"
  "destab x infl stabl =
    (let f = λy (infl, stabl). destab y infl (stabl - {y}) 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, 'x list) fmap ⇒ 'x ⇒ '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 y = Some zs ⟹ z ∈ set zs
    ⟹ z ∈ influenced_by infl x"
inductive_set influenced_by_cutoff ::
    "('x, 'x list) fmap ⇒ 'x ⇒ ('x) 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 ⟹ y ∉ c ⟹ fmlookup infl y = Some zs
    ⟹ z ∈ set zs ⟹ z ∈ influenced_by_cutoff infl x c"

lemma influenced_by_aux:
  shows "influenced_by infl x = (⋃y ∈ slookup infl x. insert y (influenced_by (fmdrop x infl) 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 infl x")
      case True
      then show ?thesis
        using step.hyps(2,3) influenced_by.base[of "fmdrop x infl" y]
        by (cases rule: set_fmlookup_default_cases, cases "x = y") auto
    next
      case False
      then show ?thesis
        using step.IH step.hyps(2,3) influenced_by.step[of y "fmdrop x infl"]
        by (cases rule: notin_fmlookup_default_cases, cases "x = y") auto
    qed
  qed auto
next
  case (2 z)
  then show ?case
  proof(cases "fmlookup infl x")
    case (Some xs)
    then obtain y where z_mem: "z ∈ insert y (influenced_by (fmdrop x infl) y)"
      and step: "y ∈ set (case fmlookup infl 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 infl) 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 infl] influenced_by.step[of y]
          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 infl x ⊆ influenced_by infl x"
proof(intro subsetI, goal_cases)
  case (1 y)
  then show ?case using influenced_by.base[of infl x]
  by (cases rule: set_fmlookup_default_cases) simp
qed

lemma influenced_unknowns_fmdrop_set:
  shows "influenced_by (fmdrop_set C infl) x = influenced_by_cutoff infl 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 by (induction rule: influenced_by_cutoff.induct;
        simp add: influenced_by.base influenced_by.step)
qed

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

lemma influenced_cutoff_subset:
  "influenced_by_cutoff infl x C ⊆ influenced_by infl 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 infl x - (⋃y ∈ C. influenced_by infl y) ⊆ influenced_by_cutoff infl 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 fastforce
  next
    case (step y zs z)
    then show ?case
      using influenced_by.base[OF step(2,3)] influenced_by.step[of y infl]
        influenced_by_cutoff.step[of y infl x C zs z]
      by blast
  qed
qed

lemma union_influenced_to_cutoff:
  shows "insert y (influenced_by infl y) ∪ influenced_by infl x =
    insert y (influenced_by infl y) ∪ influenced_by_cutoff infl x (insert y (influenced_by infl y))"
proof -
  have "u ∈ influenced_by infl y"
    if "u ≠ y" and "u ∉ influenced_by_cutoff infl x (insert y (influenced_by infl y))"
      and "u ∈ influenced_by infl x" for u
    using that influenced_cutoff_subset_2[of infl x "insert y (influenced_by infl y)"]
      influenced_by_transitive[of _ infl y] by auto
  moreover have "u ∈ influenced_by infl y"
    if "u ≠ y" and "u ∉ influenced_by infl x"
      and "u ∈ influenced_by_cutoff infl x (insert y (influenced_by infl 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 infl x] by auto
  qed simp
  ultimately show ?thesis by auto
qed

lemma destab_iter_infl_stabl_relation:
    "(infl', stabl') = destab_iter xs infl stabl
    ⟹ infl' = fmdrop_set (⋃x ∈ set xs. insert x (influenced_by infl x)) infl
    ∧ stabl' = stabl - (⋃x ∈ set xs. insert x (influenced_by infl x))"
  and destab_infl_stabl_relation:
    "(infl', stabl') = destab x infl stabl
    ⟹ infl' = fmdrop_set (insert x (influenced_by infl x)) infl
    ∧ stabl' = stabl - influenced_by infl x"
proof (induction xs infl stabl and x infl stabl
    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 y infl (stabl - {y})"
    and destab_ys: "(infl', stabl') = destab_iter ys infl'' stabl''"
    by (cases "destab 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 x)" for x
  define B where "B x ≡ insert x (influenced_by_cutoff infl x (insert y (influenced_by infl 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. B x) (fmdrop_set (A y) infl)"
        using IH1 IH2 influenced_unknowns_fmdrop_set[of "A y"] A_def B_def by auto
      also have "... = fmdrop_set (A y ∪ (⋃x∈set ys. B x)) infl"
        by (simp add: Un_commute)
      also have "... = fmdrop_set (⋃x∈set (y # ys). A x) infl"
        using A_union_B_simp by auto
      finally show ?case
        using A_def B_def by auto
  next
    case 2
    have "stabl' = stabl - (A y ∪ (⋃x∈set ys. B x))"
      using IH1 IH2 A_def B_def influenced_unknowns_fmdrop_set[of "A y"]
      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 simp
  note IH = "3.IH"[OF destab_y[symmetric]]
  then show ?case using influenced_by_aux[of infl] by simp
qed

subsubsection ‹Lemmas about the Full Destabilization›

lemma destab_x_no_dep:
  assumes "(infl', stabl') = destab x infl stabl"
    and "∀y∈stabl - (c - {x}). ∀z∈dep T σ y. y ∈ slookup infl z"
  shows "∀y ∈ stabl' - (c - {x}). x ∉ dep T σ y"
proof (intro ballI, goal_cases)
  case (1 y)
  note stabl'_def = conjunct2[OF destab_infl_stabl_relation[OF assms(1)]]
  show ?case
  proof (rule ccontr, goal_cases)
    case 1
    then have "y ∈ slookup infl x"
      using stabl'_def assms ‹y ∈ stabl' - (c - {x})› by blast
    then have "y ∈ influenced_by infl x"
      using lookup_in_influenced by force
    moreover have "y ∉ influenced_by infl x"
      using stabl'_def assms(1) ‹y ∈ stabl' - (c - {x})› by fastforce
    ultimately show ?case by auto
  qed
qed

lemma destab_preserves_infl_dom_stabl:
  assumes "(infl', stabl') = destab x infl stabl"
    and "fset (fmdom infl) ⊆ stabl"
  shows "fset (fmdom infl') ⊆ stabl'"
proof -
  have "infl' = fmdrop_set (insert x (influenced_by infl x)) infl"
    and A: "stabl' = stabl - influenced_by infl x"
    using assms(1) destab_infl_stabl_relation by metis+
  then show ?thesis
    using assms(2)
    by (metis Diff_mono fmdom'_alt_def fmdom'_drop_set subset_insertI)
qed

lemma destab_and_upd_preserves_dep_closed_in_infl:
  assumes "(infl2, stabl2) = destab x infl1 stabl1"
    and "(∀y∈stabl1 - (c - {x}). ∀z∈dep T σ1 y. y ∈ slookup infl1 z)"
  shows "(∀y∈stabl2 - (c - {x}). ∀z∈dep T (σ1(x ↦ xd')) y. y ∈ slookup infl2 z)"
proof (intro ballI, goal_cases)
  case (1 z y)
  have infl2_def: "infl2 = fmdrop_set (insert x (influenced_by infl1 x)) infl1"
    and stabl2_def: "stabl2 = stabl1 - influenced_by infl1 x"
    using assms(1) destab_infl_stabl_relation by metis+

  have "y ∈ dep T σ1 z"
  proof (goal_cases)
    case 1
    have "∀y∈stabl2 - (c - {x}). x ∉ dep T σ1 y"
      using destab_x_no_dep[OF assms(1,2)] by auto
    then have "x ∉ dep T σ1 z"
        using ‹z ∈ stabl2 - (c - {x})› by blast
    then have "dep T (σ1(x ↦ xd')) z = dep T σ1 z"
      using dep_eq[of T σ1 z "σ1(x ↦ xd')"] mlup_eq_mupd_set[of x "dep T σ1 z" σ1 σ1 xd']
      by metis
    then show ?case using ‹y ∈ dep T (σ1(x ↦ xd')) z› by auto
  qed
  then have z_in_infl1_y: "z ∈ slookup infl1 y"
    using 1(1) stabl2_def assms(2) by fastforce

  have "z ∈ influenced_by infl1 y"
    using lookup_in_influenced[of infl1 y] z_in_infl1_y
    by auto
  then have "y ∉ influenced_by infl1 x" and "y ≠ x"
    using stabl2_def 1(1) influenced_by_transitive[of y _ x z] by auto
  then show ?case
    using z_in_infl1_y fmlookup_drop_set infl2_def
    unfolding fmlookup_default_def
    by fastforce
qed


subsection ‹Definition of the Optimized Destabilization Mechanism›

function (domintros)
  destab_iter_opt ::
    "'x list ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x, 'x list) fmap × 'x set"
  and destab_opt ::
    "'x ⇒ ('x, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x, '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 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, '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 ⇒ ('x, '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 y i (s - {y}) c"
    by (cases "destab_opt 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 destab_opt
  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 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 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 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) y c))"
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 y c "fmdrop x i"]
        by (cases "y ≠ x") auto
    next
      case False
      obtain u where "u ∈ slookup i x" "y ∈ influenced_by_cutoff (fmdrop x i) u c"
        using step(5) False unfolding fmlookup_default_def by blast
      then show ?thesis
        apply (cases "x = y")
        subgoal using step.hyps(3,4) by auto
        subgoal
          using influenced_by_cutoff.step[of y "fmdrop x i" u c] step.hyps(2-4)
          by auto
        done
    qed
  qed auto
next
  case (2 z)
  show ?case
  proof(cases "fmlookup i x")
    case None
    then show ?thesis using 2 unfolding fmlookup_default_def by simp
  next
    case (Some xs)
    then obtain y where z_mem: "z ∈ insert y (influenced_by_cutoff (fmdrop x i) y c)"
      and step: "y ∈ set (case fmlookup i x of None ⇒ [] | Some v ⇒ v)"
      using 2 unfolding fmlookup_default_def 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) 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 y])+
    done
qed

lemma in_cutoff_influenced_by_cutoff_empty:
  assumes "y ∈ c"
  shows "influenced_by_cutoff infl y c = {}"
proof (rule ccontr, goal_cases)
  case 1
  then obtain b where "b ∈ influenced_by_cutoff infl y 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 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 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 x
    (insert y (influenced_by_cutoff infl y c) ∪ c)
    ∪ (insert y (influenced_by_cutoff infl y c))
  = influenced_by_cutoff infl x c
    ∪ (insert y (influenced_by_cutoff infl y c))"
proof -
  have "u ∈ influenced_by_cutoff infl x c"
    if "u ∈ influenced_by_cutoff infl x
      (insert y (influenced_by_cutoff infl y c) ∪ c)" 
      "u ∉ influenced_by_cutoff infl y 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 x
    (insert y (influenced_by_cutoff infl y c) ∪ c)"
    if "u ∈ influenced_by_cutoff infl x c"
      "u ∉ influenced_by_cutoff infl y 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 y 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. insert x (influenced_by_cutoff i x c) - c) i
    ∧ stabl' = s - (⋃x ∈ set xs. insert x (influenced_by_cutoff i x c))"
  and destab_opt_infl_stabl_relation:
    "(infl', stabl') = destab_opt x i s c ⟹ infl' = fmdrop_set (insert x
    (influenced_by_cutoff i x (c - {x}) - (c - {x}))) i
    ∧ stabl' = s - influenced_by_cutoff i x (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 y infl (stabl - {y}) c)"
    and destab_ys: "(infl', stabl') = destab_iter_opt ys infl'' stabl'' c"
    using 2 by (cases "destab_opt 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 "{y} - c ∪ influenced_by_cutoff infl y 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 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 x c)" for x
    define B where "B x ≡ insert x (influenced_by_cutoff infl x (A y ∪ c))"
      for x
  
    show ?thesis
    proof(intro conjI, goal_cases)
      case 1
      have "infl' = fmdrop_set ((⋃x∈set ys.
          insert x (influenced_by_cutoff (fmdrop_set (A y - c) infl) x c) - c) ∪ (A y - c)) infl"
        using IH1 IH2 False unfolding A_def
        by (simp add: insert_Diff_if[of y _ c] image_set_diff)
      also have "... = fmdrop_set ((⋃x∈set ys. B x - c) ∪ (A y - c)) infl"
        unfolding B_def
        by (simp add: influenced_cutoff_fmdrop_set flip: image_Un)
      also have "... = fmdrop_set ((⋃x∈set ys. (B x ∪ A y - c)) ∪ (A y - c)) infl"
        by (simp add: image_Un Un_Diff)
      also have "... = fmdrop_set ((⋃x∈set ys. (A x ∪ A y - c)) ∪ (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). 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 x (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) x (c - {y}) =
    influenced_by_cutoff infl x (insert y c)" for x
    by (simp add: influenced_cutoff_fmdrop_set[of "{_}", simplified])
  have 2: "insert y (S - (c - {y})) = insert y (S - 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

subsection ‹Adapt simp rule set›

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

end