Theory TD_side_upd_rule

section ‹TD side with Widening for Globals and Warrowing for Locals›

theory TD_side_upd_rule
  imports Basics_side TD_side Update_rules
begin

declare fun_upd_apply[simp del]


subsection ‹Definition of the Solver Algorithm›

record ('x,'g,'d) state =
  "('x,'g,'d) TD_side.state" +
  point :: "'x set"

declare TD_side.state.defs(4)[simp]

locale TD_side_upd_rule = update_rule init_ug_state update_global
  for init_ug_state :: "('x,'g,'d::{bounded_semilattice_sup_bot,warrowing},'upd) ug_state_scheme"
  and update_global ::
    "'d ⇒ 'x ⇒ 'g ⇒ 'd ⇒ ('x,'g,'d,'upd) ug_state_scheme
      ⇒ 'd option × ('x,'g,'d,'upd) ug_state_scheme"  +
  fixes T :: "('x,'g,'d::{bounded_semilattice_sup_bot,warrowing}) eqsT"
begin

interpretation TD_side: TD_side_opt False T
  done

function (domintros)
    query :: "'x ⇒ 'x ⇒ ('x,'g,'d) state ⇒ ('x,'g,'d,'upd) ug_state_scheme
              ⇒ 'd × ('x,'g,'d) state × ('x,'g,'d,'upd) ug_state_scheme" and
  iterate :: "'x ⇒ ('x,'g,'d) state ⇒ ('x,'g,'d,'upd) ug_state_scheme
              ⇒ 'd × ('x,'g,'d) state × ('x,'g,'d,'upd) ug_state_scheme" and
   repeat :: "'x ⇒ ('x,'g,'d) state ⇒ ('x,'g,'d,'upd) ug_state_scheme
              ⇒ 'd × ('x,'g,'d) state × ('x,'g,'d,'upd) ug_state_scheme" and
     eval :: "'x ⇒ ('x,'g,'d) strategy_tree ⇒ ('g ⇒ 'd) ⇒ ('x,'g,'d) state
              ⇒ ('x,'g,'d,'upd) ug_state_scheme
              ⇒ 'd × ('x,'g,'d) state × ('x,'g,'d,'upd) ug_state_scheme" where
  "query x y state ug_state = (
    let (xd, state, ug_state) =
      if y ∈ (called state) then
        ((σ state) (Inl y), state⦇point := insert y (point state)⦈, ug_state)
      else
        iterate y (state ⦇called := insert y (called state)⦈) ug_state
    in (xd, state⦇infl := fminsert (infl state) (Inl y) x⦈, ug_state))"
| "iterate x state ug_state = (
    if x ∉ (stabl state) then
      let is_point = x ∈ point state in
      let (d_new, state, ug_state) = repeat x state ug_state in
      let d_new = (if is_point then (σ state) (Inl x) ∇Δ d_new else d_new) in
      if (σ state) (Inl x) = d_new then
        (d_new, state⦇called := called state - {x}, point := point state - {x} ⦈, ug_state)
      else
        let (infl', stabl') = destab_opt (Inl x) (infl state) (stabl state) (called state) in
        iterate x (state ⦇infl := infl', stabl := stabl', σ := (σ state)(Inl x := d_new) ⦈) ug_state
    else
      ((σ state) (Inl x), state⦇called := called state - {x}, point := point state - {x} ⦈, ug_state))"
| "repeat x state ug_state = (
    let (d_new, state, ug_state) =
      eval x (T x) (λ_. ⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state in
    if x ∈ stabl state then (d_new, state, ug_state)
    else repeat x state ug_state)"
| "eval x t sides⇩a⇩c⇩c state ug_state = (case t of
      Answer d ⇒ (d, state, ug_state)
    | QueryL y g ⇒ (
        let (yd, state, ug_state) = query x y state ug_state in
        eval x (g yd) sides⇩a⇩c⇩c state ug_state)
    | QueryG y g ⇒ (
        let yd = (σ state) (Inr y) in
        eval x (g yd) sides⇩a⇩c⇩c (state ⦇infl := fminsert (infl state) (Inr y) x⦈) ug_state)
    | Side y d t ⇒ (
        let d = sides⇩a⇩c⇩c y ⊔ d in
        let sides⇩a⇩c⇩c = sides⇩a⇩c⇩c(y := d) in
        let (upd, ug_state) = update_global (σ state (Inr y)) x y d ug_state in
        case upd of None ⇒ eval x t sides⇩a⇩c⇩c state ug_state
        | Some d ⇒
          let (infl', stabl') = destab_opt (Inr y) (infl state) (stabl state) (called state) in
          eval x t sides⇩a⇩c⇩c (state ⦇infl := infl', stabl := stabl', σ := (σ state)(Inr y := d) ⦈)
            ug_state))"
  by pat_completeness auto

definition init_state :: "('x,'g,'d) state" where
  "init_state = ⦇ called = {}, infl = fmempty, stabl = {}, σ = (λ_. ⊥), point = {} ⦈"

definition solve :: "'x ⇒ 'x set × ('x + 'g => 'd)" where
  "solve x = (let (d, state, ug_state) =
    iterate x (init_state ⦇ called := insert x (called (init_state :: ('x,'g,'d) state)) ⦈) init_ug_state in
  (stabl state, σ state))"

definition query_dom where
  "query_dom y x state ug_state =
    query_iterate_repeat_eval_dom (Inl (Inl (y, x, state, ug_state)))"
declare query_dom_def [simp]
definition iterate_dom where
  "iterate_dom x state ug_state = query_iterate_repeat_eval_dom (Inl (Inr (x, state, ug_state)))"
declare iterate_dom_def [simp]
definition repeat_dom where
  "repeat_dom x state ug_state = query_iterate_repeat_eval_dom (Inr (Inl (x, state, ug_state)))"
declare repeat_dom_def [simp]
definition eval_dom where
  "eval_dom x t sides⇩a⇩c⇩c state ug_state =
    query_iterate_repeat_eval_dom (Inr (Inr (x, t, sides⇩a⇩c⇩c, state, ug_state)))"
declare eval_dom_def [simp]

definition solve_dom where
  "solve_dom x = iterate_dom x (init_state ⦇ called := insert x (called init_state) ⦈) init_ug_state"

lemmas dom_defs = query_dom_def iterate_dom_def repeat_dom_def eval_dom_def


subsection ‹Refinement of auto-generated rules›

text ‹The auto-generated \texttt{pinduct} rule contains a redundant assumption. This lemma removes
this redundant assumption such that the rule is easier to instantiate and gives comprehensible
names to the cases.›

lemmas query_iterate_repeat_eval_pinduct[consumes 1, case_names Query Iterate Repeat Eval]
  = query_iterate_repeat_eval.pinduct(1)[
      folded dom_defs,
      of x y state ug_state for x y state ug_state
    ]
    query_iterate_repeat_eval.pinduct(2)[
      folded dom_defs,
      of x state ug_state for x state ug_state
    ]
    query_iterate_repeat_eval.pinduct(3)[
      folded dom_defs,
      of x state ug_state for x state ug_state
    ]
    query_iterate_repeat_eval.pinduct(4)[
      folded dom_defs,
      of x t sides⇩a⇩c⇩c state ug_state for x t sides⇩a⇩c⇩c state ug_state
    ]

lemmas iterate_pinduct[consumes 1, case_names Iterate]
  = query_iterate_repeat_eval_pinduct(2)[where ?P="λy x state ug_state. True"
    and ?R="λx state ug_state. True"
    and ?S="λx t sides⇩a⇩c⇩c state ug_state. True", simplified (no_asm_use),
    folded dom_defs]

declare query.psimps[simp] iterate.psimps[simp] eval.psimps[simp]


subsection ‹Domain Lemmas›

lemma dom_backwards_pinduct:
  shows "query_dom x y state ug_state
    ⟹ y ∉ called state ⟹ iterate_dom y (state ⦇called := insert y (called state)⦈) ug_state"
  and "iterate_dom x state ug_state
    ⟹ x ∉ (stabl state) ⟹
         repeat_dom x state ug_state
          ∧ (in_point = (x ∈ point state)
          ⟶ (xd_new1, state1, ug_state1) = repeat x state ug_state
          ⟶ xd_new2 = (if in_point then (σ state1) (Inl x) ∇Δ xd_new1 else xd_new1)
          ⟶ (σ state1) (Inl x) ≠ xd_new2
          ⟶ (infl2, stabl2) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1)
          ⟶ iterate_dom x (state1 ⦇infl := infl2, stabl := stabl2,
              σ := (σ state1)(Inl x := xd_new2)⦈) ug_state1)"
  and "repeat_dom x state ug_state ⟹
        eval_dom x (T x) (λ_. ⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state ∧
        ((d', state', ug_state') =
          eval x (T x) (λ_. ⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state
        ⟶ x ∉ stabl state' ⟶ repeat_dom x state' ug_state')"
  and "eval_dom x t sides⇩a⇩c⇩c state ug_state
    ⟹ (t = QueryL y g ⟶ query_dom x y state ug_state ∧
          ((yd, state', ug_state') = query x y state ug_state
          ⟶ eval_dom x (g yd) sides⇩a⇩c⇩c state' ug_state')) ∧
        (t = QueryG z h ⟶ zd = (σ state) (Inr z) ⟶
          eval_dom x (h zd) sides⇩a⇩c⇩c (state⦇infl := fminsert (infl state) (Inr z) x⦈) ug_state) ∧
        (t = Side u d t' ⟶
          d' = (sides⇩a⇩c⇩c u) ⊔ d ⟶
          sides⇩a⇩c⇩c' = sides⇩a⇩c⇩c(u := d') ⟶
          (upd,ug_state') = update_global (σ state (Inr u)) x u d' ug_state ⟶
          ((upd = None ⟶ eval_dom x t' sides⇩a⇩c⇩c' state ug_state')
          ∧ (upd = Some d'' ⟶
            (infl1, stabl1) = destab_opt (Inr u) (infl state) (stabl state) (called state) ⟶
            eval_dom x t' sides⇩a⇩c⇩c' (state⦇infl := infl1, stabl := stabl1,
              σ := (σ state)(Inr u := d'')⦈) ug_state')))"
proof (induction x y state ug_state and x state ug_state and x state ug_state
               and x t sides⇩a⇩c⇩c state ug_state
    arbitrary: and in_point xd_new1 xd_new2 state1 ug_state1 infl2 stabl2 and d' state' ug_state'
               and y g yd d z h zd u t' d' sides⇩a⇩c⇩c' upd ug_state' d'' state' infl1 stabl1
    rule: query_iterate_repeat_eval_pinduct)
  case (Query y x state ug_state)
  show ?case
    apply (rule query_iterate_repeat_eval.domintros(2)[folded dom_defs])
    using Query.IH(2)[OF Query.prems]
    by simp+
next
  case (Iterate x state ug_state)
  show ?case
    apply (intro impI conjI)
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(3)[folded dom_defs])
      using Iterate.IH(2)[OF Iterate.prems] by fastforce+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(2)[folded dom_defs destab.simps])
      using Iterate.IH(3)[OF Iterate.prems, folded dom_defs, of _ _ _ _ state1 ug_state1] by auto
    done
next
  case (Repeat x state ug_state)
  show ?case
    apply (intro impI conjI)
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Repeat.IH(2)[OF Repeat.prems] by fastforce+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(3)[folded dom_defs])
      using Repeat.IH(3)[OF Repeat.prems] by fastforce+
    done
next
  case (Eval x t sides⇩a⇩c⇩c state ug_state)
  show ?case
    apply (intro impI conjI)
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(1)[folded dom_defs])
      using Eval.IH(2) by simp
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Eval.IH(3) by metis+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Eval.IH(4) by metis+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Eval.IH(5) by metis+
    subgoal
      apply (rule query_iterate_repeat_eval.domintros(4)[folded dom_defs])
      using Eval.IH(6) by metis+
    done
qed


subsection ‹Case Rules›

lemma iterate_continue_fixpoint_cases[consumes 3]:
  assumes "iterate_dom x state ug_state"
    and "(xd, state', ug_state') = iterate x state ug_state"
  obtains (Stable) "state' = state⦇called := called state - {x}, point := point state - {x} ⦈"
    and "(σ state) (Inl x) = xd"
    and "x ∈ stabl state"
    and "ug_state' = ug_state"
  | (Fixpoint) state1 xd_new ug_state1
  where "repeat_dom x state ug_state"
    and "(xd_new, state1, ug_state1) = repeat x state ug_state"
    and "xd = (if x ∈ point state then (σ state1) (Inl x) ∇Δ xd_new else xd_new)"
    and "(σ state1) (Inl x) = xd"
    and "x ∉ stabl state"
    and "state' = state1⦇called := called state1 - {x}, point := point state1 - {x} ⦈"
    and "ug_state' = ug_state1"
  | (Continue) state1 xd_new xd_new' infl2 stabl2 ug_state1
  where "repeat_dom x state ug_state"
    and "(xd_new, state1, ug_state1) = repeat x state ug_state"
    and "xd_new' = (if x ∈ point state then (σ state1) (Inl x) ∇Δ xd_new else xd_new)"
    and "(σ state1) (Inl x) ≠ xd_new'"
    and "(infl2, stabl2) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1)"
    and "iterate_dom x
          (state1 ⦇infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := xd_new')⦈) ug_state1"
    and "(xd, state', ug_state') = iterate x
          (state1 ⦇infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := xd_new')⦈) ug_state1"
    and "x ∉ stabl state"
proof(cases "x ∈ stabl state" rule: case_split[case_names Stable Unstable])
  case Stable
  then show ?thesis using that(1) assms by auto
next
  case Unstable
  have repeat_dom: "repeat_dom x state ug_state"
    using dom_backwards_pinduct(2)[OF assms(1) Unstable]
    by simp
  then obtain xd_new state1 ug_state1 xd_new' where
      repeat: "(xd_new, state1, ug_state1) = repeat x state ug_state" and
      xd_new': "xd_new' = (if x ∈ point state then (σ state1) (Inl x) ∇Δ xd_new else xd_new)"
    by (cases "repeat x state ug_state") auto
  show ?thesis
  proof (cases "(σ state1) (Inl x) = xd_new'")
    case True
    then have xd: "xd = xd_new'"
        and state': "state' = state1⦇called := called state1 - {x}, point := point state1 - {x} ⦈"
        and ug_state': "ug_state' = ug_state1"
      using assms(1) Unstable repeat assms(2) xd_new'
      by (cases "repeat x state ug_state", simp split: if_splits)+
    then show ?thesis
      using that(2)[OF repeat_dom repeat _ _ Unstable] True xd_new' by simp
  next
    case False
    then obtain infl2 stabl2 where destab:
        "(infl2, stabl2) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1)"
      by (cases "destab_opt (Inl x) (infl state1) (stabl state1) (called state1)") simp
    then have iterate_dom: "iterate_dom x (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new')⦈) ug_state1"
      using Unstable False repeat assms dom_backwards_pinduct(2) xd_new'
      by simp
    have iterate: "(xd, state', ug_state') = iterate x (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new')⦈) ug_state1"
      using iterate.psimps[folded dom_defs, OF assms(1)] Unstable repeat False
        destab assms(2) xd_new' by (auto split: prod.split)
    show ?thesis
      using that(3)[OF repeat_dom repeat xd_new' False destab iterate_dom iterate
          Unstable]
      by simp
  qed
qed

lemma repeat_unstable_stable_cases [consumes 2]:
  assumes "repeat_dom x state ug_state"
    and "(d', state', ug_state') = repeat x state ug_state"
  obtains (Unstable) state1 d1 ug_state1
  where "eval_dom x (T x) (λ_.⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state"
    and "(d1, state1, ug_state1) =
          eval x (T x) (λ_.⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state"
    and "x ∉ stabl state1"
    and "repeat_dom x state1 ug_state1"
    and "(d', state', ug_state') = repeat x state1 ug_state1"
  | (Stable) "eval_dom x (T x) (λ_.⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state"
    and "(d', state', ug_state') =
          eval x (T x) (λ_.⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state"
    and "x ∈ stabl state'"
proof -
  have eval_dom: "eval_dom x (T x) (λ_.⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state"
    using dom_backwards_pinduct(3)[OF assms(1)] by simp
  obtain d1 state1 ug_state1 where eval:
    "(d1, state1, ug_state1) =
      eval x (T x) (λ_.⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state"
    by (cases "eval x (T x) (λ_.⊥) (state ⦇stabl := insert x (stabl state)⦈) ug_state") auto
  show ?thesis
  proof (cases "x ∈ stabl state1" rule: case_split[case_names Stable Unstable])
    case Stable
    show ?thesis
      apply (rule that(2)[OF eval_dom])
      using Stable eval assms(2) repeat.psimps[folded dom_defs, OF assms(1)]
      by (cases "eval x (T x) (λ_.⊥) (state⦇stabl := insert x (stabl state)⦈) ug_state", simp)+
  next
    case Unstable
    show ?thesis
      apply (rule that(1)[OF eval_dom eval])
      subgoal using Unstable by simp
      subgoal using dom_backwards_pinduct(3)[OF assms(1)] eval Unstable by simp
      subgoal
        using repeat.psimps[folded dom_defs, OF assms(1)] eval Unstable assms(2)
        by (cases "eval x (T x) (λ_.⊥) (state⦇stabl := insert x (stabl state)⦈) ug_state") simp
      done
  qed
qed

lemma query_iterate_lookup_cases_basic [consumes 2]:
  assumes "query_dom y x state ug_state"
    and "(xd, state', ug_state') = query y x state ug_state"
  obtains (Iterate) state1 xd ug_state1
  where "iterate_dom x (state⦇called := insert x (called state) ⦈) ug_state"
    and "(xd, state1, ug_state1) = iterate x (state⦇called := insert x (called state) ⦈) ug_state"
    and "state' = state1 ⦇infl := fminsert (infl state1) (Inl x) y⦈"
    and "x ∉ called state"
    and "ug_state' = ug_state1"
  | (Lookup) "(σ state) (Inl x) = xd"
    and "state' = state ⦇infl := fminsert (infl state) (Inl x) y, point := insert x (point state)⦈"
    and "x ∈ called state"
    and "ug_state' = ug_state"
proof (cases "x ∈ called state")
  case True
  show ?thesis using assms True by (auto intro: that(2))
next
  case False
  obtain xd state1 ug_state1 where
    iterate: "(xd, state1, ug_state1) = iterate x (state⦇called := insert x (called state)⦈) ug_state"
    by (cases "iterate x (state⦇called := insert x (called state)⦈) ug_state") simp
  show ?thesis
    apply (rule that(1)[of xd state1])
    using dom_backwards_pinduct(1)[OF assms(1) False] assms(1,2) iterate False
    by (simp split: if_splits prod.splits)+
qed

lemma eval_query_answer_cases_basic [consumes 2]:
  assumes "eval_dom x t sides⇩a⇩c⇩c state ug_state"
    and "(xd, state', ug_state') = eval x t sides⇩a⇩c⇩c state ug_state"
  obtains (QueryL) y g yd state1 ug_state1
  where "t = QueryL y g"
    and "query_dom x y state ug_state"
    and "(yd, state1, ug_state1) = query x y state ug_state"
    and "eval_dom x (g yd) sides⇩a⇩c⇩c state1 ug_state1"
    and "(xd, state', ug_state') = eval x (g yd) sides⇩a⇩c⇩c state1 ug_state1"
  | (QueryG) y g yd
  where "t = QueryG y g"
    and "yd = (σ state) (Inr y)"
    and "eval_dom x (g yd) sides⇩a⇩c⇩c (state⦇infl := fminsert (infl state) (Inr y) x⦈) ug_state"
    and "(xd, state', ug_state') =
          eval x (g yd) sides⇩a⇩c⇩c (state⦇infl := fminsert (infl state) (Inr y) x⦈) ug_state"
  | (Side_Subsumed) y yd t1 sides⇩a⇩c⇩c' d' ug_state1
  where "t = Side y yd t1"
    and "d' = sides⇩a⇩c⇩c y ⊔ yd"
    and "sides⇩a⇩c⇩c' = sides⇩a⇩c⇩c(y := d')"
    and "(None, ug_state1) = update_global (σ state (Inr y)) x y d' ug_state"
    and "eval_dom x t1 sides⇩a⇩c⇩c' state ug_state1"
    and "(xd, state', ug_state') = eval x t1 sides⇩a⇩c⇩c' state ug_state1"
  | (Side_Effect) y yd t1 d' sides⇩a⇩c⇩c' d'' ug_state1 infl1 stabl1
  where "t = Side y yd t1"
    and "d' = sides⇩a⇩c⇩c y ⊔ yd"
    and "sides⇩a⇩c⇩c' = sides⇩a⇩c⇩c(y := d')"
    and "(Some d'', ug_state1) = update_global (σ state (Inr y)) x y d' ug_state"
    and "(infl1, stabl1) = destab_opt (Inr y) (infl state) (stabl state) (called state)"
    and "eval_dom x t1 sides⇩a⇩c⇩c' (state ⦇infl := infl1, stabl := stabl1,
          σ := (σ state)(Inr y := d'')⦈) ug_state1"
    and "(xd, state', ug_state') = eval x t1 sides⇩a⇩c⇩c' (state ⦇infl := infl1, stabl := stabl1,
          σ := (σ state)(Inr y := d'')⦈) ug_state1"
  | (Answer) "t = Answer xd"
    and "state' = state"
    and "ug_state' = ug_state"
proof (cases t)
  case (Answer d)
  then show ?thesis using that eval.psimps[folded dom_defs, OF assms(1)] assms(2) by auto
next
  case (QueryL y g)
  obtain yd1 state1 ug_state1 where
    query_y: "(yd1, state1, ug_state1) = query x y state ug_state"
    by (cases "query x y state ug_state", simp)
  have query_y_dom: "query_dom x y state ug_state"
    using dom_backwards_pinduct(4)[OF assms(1), THEN conjunct1, folded
          atomize_imp, OF QueryL, of yd1 state1] by simp
  have "(xd, state', ug_state') = eval x (g yd1) sides⇩a⇩c⇩c state1 ug_state1"
    using eval.psimps[folded dom_defs, OF assms(1)] QueryL query_y assms(2)
    by (auto split: prod.splits)
  then show ?thesis
    using that(1) QueryL query_y_dom query_y dom_backwards_pinduct(4) assms by fast
next
  case (QueryG y g)
  obtain yd1 where query_y: "yd1 = (σ state) (Inr y)" by simp
  have "(xd, state', ug_state') =
      eval x (g yd1) sides⇩a⇩c⇩c (state⦇infl := fminsert (infl state) (Inr y) x⦈) ug_state"
    using eval.psimps[folded dom_defs, OF assms(1)] QueryG query_y assms(2)
    by (auto split: prod.splits)
  then show ?thesis
    using QueryG query_y dom_backwards_pinduct(4)[OF assms(1)] that(2)
    by (auto intro: that(2))
next
  case (Side y d t1)
  define d' where "d' = sides⇩a⇩c⇩c y ⊔ d"
  define sides⇩a⇩c⇩c' where "sides⇩a⇩c⇩c' = sides⇩a⇩c⇩c(y := d')"
  obtain do ug_state1 where
    upd_global: "(do, ug_state1) = update_global (σ state (Inr y)) x y d' ug_state"
    by (cases "update_global (σ state (Inr y)) x y d' ug_state") auto
  show ?thesis
  proof (cases do)
    case None
    then have eval: "(xd, state', ug_state') = eval x t1 sides⇩a⇩c⇩c' state ug_state1"
      using eval.psimps[folded dom_defs, OF assms(1)] Side d'_def sides⇩a⇩c⇩c'_def assms(2)
        upd_global
      by (auto simp add: Let_def split: prod.splits)
    then show ?thesis
      using None Side sides⇩a⇩c⇩c'_def d'_def dom_backwards_pinduct(4)[OF assms(1)] upd_global
      by (auto intro: that(3)[OF Side d'_def sides⇩a⇩c⇩c'_def])
  next
    case (Some d'')
    obtain infl1 stabl1 where
      destab: "(infl1, stabl1) = destab_opt (Inr y) (infl state) (stabl state) (called state)"
      by (cases "destab_opt (Inr y) (infl state) (stabl state) (called state)") simp
    then have eval: "(xd, state', ug_state') = eval x t1 sides⇩a⇩c⇩c' (state ⦇infl := infl1,
        stabl := stabl1, σ := (σ state)(Inr y := d'')⦈) ug_state1"
      using eval.psimps[folded dom_defs, OF assms(1)] Side d'_def sides⇩a⇩c⇩c'_def assms(2) Some
        upd_global
      by (auto simp add: Let_def split: prod.splits)
    then show ?thesis
      using Some destab Side d'_def sides⇩a⇩c⇩c'_def dom_backwards_pinduct(4)[OF assms(1)]
        upd_global
      by (auto intro: that(4)[OF Side d'_def sides⇩a⇩c⇩c'_def])
  qed
qed

lemma called_same:
  shows
    "query_dom x y state ug_state ⟹ (xd, state', ug_state') = query x y state ug_state
      ⟹ called state' = called state"
    "iterate_dom x state ug_state ⟹ (xd, state', ug_state') = iterate x state ug_state
      ⟹ x ∈ called state ⟹ called state' = called state - {x}"
    "repeat_dom x state ug_state ⟹ (xd, state', ug_state') = repeat x state ug_state
      ⟹ called state' = called state"
    "eval_dom x t sides⇩a⇩c⇩c state ug_state
      ⟹ (xd, state', ug_state') = eval x t sides⇩a⇩c⇩c state ug_state
      ⟹ called state' = called state"
proof (induction x y state ug_state and x state ug_state and x state ug_state
        and x t sides⇩a⇩c⇩c state ug_state
       arbitrary: xd state' ug_state' and xd state' ug_state' and xd state' ug_state'
        and xd state' ug_state'
       rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state ug_state)
  show ?case using Query(1,3)
  proof (cases rule: query_iterate_lookup_cases_basic)
    case (Iterate state1 xd)
    then show ?thesis using Query(2)[of xd state1] by simp
  next
    case Lookup
    then show ?thesis by fastforce
  qed
next
  case (Iterate x state ug_state)
  show ?case using Iterate(1,4)
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis by simp
  next
    case (Fixpoint state1 xd_new)
    then show ?thesis using Iterate.IH(1) Iterate.IH(2)[OF Fixpoint(5) _ Fixpoint(2)] by simp
  next
    case (Continue state1 xd_new infl⇩L2 stabl2)
    then show ?thesis
      using Iterate(5) Iterate.IH(2)[OF Continue(8) _ Continue(2)]
        Iterate.IH(3)[OF Continue(8) _ Continue(2)_ _ _ Continue(4) _ _ Continue(7)]
      by simp
  qed
next
  case (Repeat x state)
  show ?case using Repeat(1,4)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    show ?thesis
      using Repeat.IH(2)[OF Unstable(2)] Repeat.IH(3)[OF Unstable(2) _ _ Unstable(3,5)] by simp
  next
    case Stable
    then show ?thesis using Repeat.IH(2)[OF Stable(2)] by simp
  qed
next
  case (Eval x t sides⇩a⇩c⇩c state ug_state)
  show ?case using Eval(1,7)
  proof (cases rule: eval_query_answer_cases_basic)
    case (QueryL y g yd state1 ug_state1)
    show ?thesis
      using Eval.IH(2)[OF QueryL(1,3)] Eval.IH(3)[OF QueryL(1,3) _ _ QueryL(5)] by simp
  next
    case (QueryG y g yd)
    then show ?thesis using Eval.IH(4)[OF QueryG(1,2,4)] by simp
  next
    case (Side_Subsumed y yd t1 sides⇩a⇩c⇩c' d' ug_state1)
    then show ?thesis
      using Eval.IH(5)[OF Side_Subsumed(1-4) _ _ Side_Subsumed(6)]
      by auto
  next
    case (Side_Effect y yd t1 d' sides⇩a⇩c⇩c' d'' ug_state1 infl1 stabl1)
    then show ?thesis
      using Eval.IH(6)[OF Side_Effect(1-4) _ _ Side_Effect(5) _ Side_Effect(7)] Side_Effect(3)
      by auto
  next
    case Answer
    then show ?thesis by simp
  qed
qed

lemma iterate_fmlookup:
  assumes "iterate_dom x state ug_state"
    and "(xd, state', ug_state') = iterate x state ug_state"
  shows "(σ state') (Inl x) = xd"
  using assms
proof(induction x state ug_state rule: iterate_pinduct)
  case (Iterate x state ug_state)
  show ?case
    using Iterate.hyps Iterate.prems
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis by simp
  next
    case Fixpoint
    then show ?thesis by simp
  next
    case (Continue state1 xd_new infl⇩L2 stabl2)
    then show ?thesis
      using Iterate.IH(1) called_same(3)[OF Continue(1,2)] Iterate(3) by fastforce
  qed
qed

corollary query_fmlookup:
  assumes "query_dom y x state ug_state"
    and "(xd, state', ug_state') = query y x state ug_state"
  shows "(σ state') (Inl x) = xd"
  using assms iterate_fmlookup[OF dom_backwards_pinduct(1)[OF assms(1)]]
  by (auto split: prod.splits if_splits)

lemma eval_query_answer_cases [consumes 2]:
  assumes "eval_dom x t sides⇩a⇩c⇩c state ug_state"
    and "(xd, state', ug_state') = eval x t sides⇩a⇩c⇩c state ug_state"
  obtains (QueryL) y g yd state1 ug_state1
  where "t = QueryL y g"
    and "query_dom x y state ug_state"
    and "(yd, state1, ug_state1) = query x y state ug_state"
    and "eval_dom x (g yd) sides⇩a⇩c⇩c state1 ug_state1"
    and "(xd, state', ug_state') = eval x (g yd) sides⇩a⇩c⇩c state1 ug_state1"
    and "(σ state1) (Inl y) = yd"
  | (QueryG) y g yd
  where "t = QueryG y g"
    and "yd = (σ state) (Inr y)"
    and "eval_dom x (g yd) sides⇩a⇩c⇩c (state⦇infl := fminsert (infl state) (Inr y) x⦈) ug_state"
    and "(xd, state', ug_state') =
          eval x (g yd) sides⇩a⇩c⇩c (state⦇infl := fminsert (infl state) (Inr y) x⦈) ug_state"
  | (Side_Subsumed) y yd t1 sides⇩a⇩c⇩c' d' ug_state1
  where "t = Side y yd t1"
    and "d' = sides⇩a⇩c⇩c y ⊔ yd"
    and "sides⇩a⇩c⇩c' = sides⇩a⇩c⇩c(y := d')"
    and "(None, ug_state1) = update_global (σ state (Inr y)) x y d' ug_state"
    and "eval_dom x t1 sides⇩a⇩c⇩c' state ug_state1"
    and "(xd, state', ug_state') = eval x t1 sides⇩a⇩c⇩c' state ug_state1"
  | (Side_Effect) y yd t1 d' sides⇩a⇩c⇩c' d'' ug_state1 infl1 stabl1
  where "t = Side y yd t1"
    and "d' = sides⇩a⇩c⇩c y ⊔ yd"
    and "sides⇩a⇩c⇩c' = sides⇩a⇩c⇩c(y := d')"
    and "(Some d'', ug_state1) = update_global (σ state (Inr y)) x y d' ug_state"
    and "(infl1, stabl1) = destab_opt (Inr y) (infl state) (stabl state) (called state)"
    and "eval_dom x t1 sides⇩a⇩c⇩c' (state ⦇infl := infl1, stabl := stabl1,
          σ := (σ state)(Inr y := d'')⦈) ug_state1"
    and "(xd, state',ug_state') = eval x t1 sides⇩a⇩c⇩c' (state ⦇infl := infl1, stabl := stabl1,
          σ := (σ state)(Inr y := d'')⦈) ug_state1"
  | (Answer) "t = Answer xd"
    and "state' = state"
    and "ug_state' = ug_state"
  using query_fmlookup[of x _ state]
  by (auto intro: eval_query_answer_cases_basic[OF assms])

lemma query_iterate_lookup_cases [consumes 2]:
  assumes "query_dom y x state ug_state"
    and "(xd, state', ug_state') = query y x state ug_state"
  obtains (Iterate) state1 xd
  where "iterate_dom x (state⦇called := insert x (called state) ⦈) ug_state"
    and "(xd, state1, ug_state') = iterate x (state⦇called := insert x (called state) ⦈) ug_state"
    and "state' = state1 ⦇infl := fminsert (infl state1) (Inl x) y⦈"
    and "(σ state') (Inl x) = xd"
    and "x ∉ called state"
  | (Lookup) "(σ state) (Inl x) = xd"
    and "state' = state ⦇infl := fminsert (infl state) (Inl x) y, point := insert x (point state)⦈"
    and "x ∈ called state"
    and "ug_state' = ug_state"
  apply (rule query_iterate_lookup_cases_basic[OF assms])
  using iterate_fmlookup[of x "state⦇called := insert x (called state)⦈"]
  by (simp_all split: if_splits del: dom_defs)


subsection ‹Basic Properties of the Solver State›

lemma called_non_stabl_increasing:
  shows "query_dom x y state ug_state
    ⟹ (xd, state', ug_state') = query x y state ug_state
    ⟹ called state - stabl state ⊆ called state' - stabl state'"
    and "iterate_dom x state ug_state
    ⟹ (xd, state', ug_state') = iterate x state ug_state
    ⟹ x ∈ called state
    ⟹ x ∈ stabl state'
      ∧ (called state - {x}) - stabl state ⊆ called state' - stabl state'"
    and "repeat_dom x state ug_state
    ⟹ (xd, state', ug_state') = repeat x state ug_state
    ⟹ x ∈ called state
    ⟹ x ∈ stabl state'
      ∧ (called state - {x}) - stabl state ⊆ (called state' - {x}) - stabl state'"
    and "eval_dom x t sides⇩a⇩c⇩c state ug_state
    ⟹ (xd, state', ug_state') = eval x t sides⇩a⇩c⇩c state ug_state
    ⟹ called state - stabl state ⊆ called state' - stabl state'"
proof(induction x y state ug_state and x state ug_state and x state ug_state
        and x t sides⇩a⇩c⇩c state ug_state
      arbitrary: xd state' ug_state' and xd state' ug_state' and xd state' ug_state'
        and xd state' ug_state'
      rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state ug_state)
  show ?case using Query(1,3)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1 xd)
    note IH = Query.IH(2)[OF Iterate(5,2)]
    then show ?thesis using Iterate(3) called_same(2)[OF Iterate(1,2), simplified] Iterate(5) by auto
  next
    case Lookup
    then show ?thesis by simp
  qed
next
  case (Iterate x state ug_state)
  show ?case using Iterate(1,4)
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate(5) by auto
  next
    case (Fixpoint state1 xd_new)
    note IH = Iterate.IH(2)[OF Fixpoint(5) _ Fixpoint(2) Iterate.prems(2)]
    then show ?thesis using Iterate(5) Fixpoint(6) by simp
  next
    case (Continue state1 xd_new xd_new' infl2 stabl2 ug_state1)
    note IH = Iterate.IH(2)[OF Continue(8) _ Continue(2) Iterate.prems(2)]
    have "x ∈ called state1" using called_same(3)[OF Continue(1,2)] Iterate.prems(2) by simp
    note ih = Iterate.IH(3)[OF Continue(8) _ Continue(2) _ _ Continue(3,4,5) _ Continue(7),
        simplified, OF _ _ ‹x ∈ called state1›]
    then show ?thesis
      using Iterate(5) IH destab_opt_infl_stabl_relation[OF Continue(5)]
      by auto
  qed
next
  case (Repeat x state)
  show ?case using Repeat(1,4)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2)]
    have "x ∈ called state1" using called_same(4)[OF Unstable(1,2)] Repeat.prems(2) by simp
    note ih = Repeat.IH(3)[OF Unstable(2) _ _ Unstable(3,5) ‹x ∈ called state1›, of d1, simplified]
    then show ?thesis using IH by auto
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2)]
    then show ?thesis using Stable(3) by auto
  qed
next
  case (Eval x t sides⇩a⇩c⇩c state)
  show ?case using Eval(1,7)
  proof (cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,3)]
    note ih = Eval.IH(3)[OF QueryL(1,3) _ _ QueryL(5), simplified]
    then show ?thesis using IH by auto
  next
    case (QueryG y g yd)
    note IH = Eval.IH(4)[OF QueryG(1,2,4)]
    then show ?thesis by simp
  next
    case (Side_Subsumed y yd t1 sides⇩a⇩c⇩c' d' ug_state1)
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4) _ _ Side_Subsumed(6), simplified]
    then show ?thesis using Side_Subsumed(5) by auto
  next
    case (Side_Effect y yd t1 d' sides⇩a⇩c⇩c' d'' ug_state1 infl1 stabl1)
    note IH = Eval.IH(6)[OF Side_Effect(1-4) _ _ Side_Effect(5) refl Side_Effect(7),
        simplified]
    then show ?thesis
      using destab_opt_infl_stabl_relation[OF Side_Effect(5)] by auto
  next
    case Answer
    then show ?thesis by simp
  qed
qed

lemma called_value_unchanged:
  shows "query_dom x y state ug_state
    ⟹ (xd, state', ug_state') = query x y state ug_state
    ⟹ ∀x ∈ called state. (σ state) (Inl x) = (σ state') (Inl x)"
    and "iterate_dom x state ug_state
    ⟹ (xd, state', ug_state') = iterate x state ug_state
    ⟹ x ∈ called state
    ⟹ ∀x ∈ called state - {x}. (σ state) (Inl x) = (σ state') (Inl x)"
    and "repeat_dom x state ug_state
    ⟹ (xd, state', ug_state') = repeat x state ug_state
    ⟹ x ∈ called state
    ⟹ ∀x ∈ called state. (σ state) (Inl x) = (σ state') (Inl x)"
    and "eval_dom x t sides⇩a⇩c⇩c state ug_state
    ⟹ (xd, state', ug_state') = eval x t sides⇩a⇩c⇩c state ug_state
    ⟹ ∀x ∈ called state. (σ state) (Inl x) = (σ state') (Inl x)"
proof(induction x y state ug_state and x state ug_state and x state ug_state
        and y t sides⇩a⇩c⇩c state ug_state
      arbitrary: xd state' ug_state' and xd state' ug_state' and xd state' ug_state'
        and xd state' ug_state'
      rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state ug_state)
  show ?case using Query(1,3)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1 xd)
    note IH = Query.IH(2)[OF Iterate(5,2)]
    then show ?thesis using Iterate(3) called_same(2)[OF Iterate(1,2), simplified] Iterate(5) by auto
  next
    case Lookup
    then show ?thesis by simp
  qed
next
  case (Iterate x state ug_state)
  show ?case using Iterate(1,4)
  proof (cases rule: iterate_continue_fixpoint_cases)
    case Stable
    then show ?thesis using Iterate(5) by auto
  next
    case (Fixpoint state1)
    note IH = Iterate.IH(2)[OF Fixpoint(5) _ Fixpoint(2) Iterate.prems(2)]
    then show ?thesis
      using Iterate(5) Fixpoint(6) by (simp add: image_Int Diff_eq flip: restrict_restrict)
  next
    case (Continue state1 xd_new infl2 stabl2)
    note IH = Iterate.IH(2)[OF Continue(8) _ Continue(2) Iterate.prems(2)]
    have called_same: "called state1 = called state" using called_same(3)[OF Continue(1,2)] by simp
    then have "x ∈ called state1" using Iterate.prems(2) by simp
    note ih = Iterate.IH(3)[OF Continue(8) _ _ Continue(2) _ Continue(3,4,5) _ Continue(7),
        simplified, OF ‹x ∈ called state1›]
    then show ?thesis
      using Iterate(5) IH
      by (auto simp add: image_Int Diff_eq called_same fun_upd_other simp flip: restrict_restrict
          split: if_splits)
  qed
next
  case (Repeat x state)
  show ?case using Repeat(1,4)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2)]
    have called_same: "called state1 = called state" using called_same(4)[OF Unstable(1,2)] by simp
    then have "x ∈ called state1" using Repeat.prems(2) by simp
    note ih = Repeat.IH(3)[OF Unstable(2) _ _ Unstable(3,5) ‹x ∈ called state1›, of d1, simplified]
    then show ?thesis using IH by (simp add: called_same)
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2)]
    then show ?thesis by simp
  qed
next
  case (Eval x t sides⇩a⇩c⇩c state)
  show ?case using Eval(1,7)
  proof (cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,3)]
    have called_same: "called state1 = called state" using called_same(1)[OF QueryL(2,3)] by simp
    note ih = Eval.IH(3)[OF QueryL(1,3) _ _ QueryL(5), simplified]
    then show ?thesis using IH by (simp add: called_same)
  next
    case (QueryG y g yd)
    note IH = Eval.IH(4)[OF QueryG(1,2,4)]
    then show ?thesis by simp
  next
    case (Side_Subsumed y yd t1 sides⇩a⇩c⇩c' d' ug_state1)
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4) _ _ Side_Subsumed(6), simplified]
    then show ?thesis using Side_Subsumed(5) by auto
  next
    case (Side_Effect y yd t1 d' sides⇩a⇩c⇩c' d'' ug_state1 infl1 stabl1)
    note IH = Eval.IH(6)[OF Side_Effect(1-4) _ _ Side_Effect(5) refl Side_Effect(7), simplified]
    then show ?thesis
      using Side_Effect(5)
      by (auto simp add: image_Int Diff_eq called_same fun_upd_other simp flip: restrict_restrict
          split: if_splits)
  next
    case Answer
    then show ?thesis by simp
  qed
qed


subsection ‹Well-formedness of the Stable Set and Infl Map›

subsubsection ‹Induction Proof›

lemma well_infl_stabl_ind:
  shows "query_dom x y state ug_state
    ⟹ (xd, state', ug_state') = query x y state ug_state
    ⟹ TD_side.well_infl_stabl state
    ⟹ TD_side.well_infl_stabl state'
      ∧ x ∈ slookup (infl state') (Inl y)
      ∧ TD_side.update_rel_opt state state'"
    and "iterate_dom x state ug_state
    ⟹ (xd, state', ug_state') = iterate x state ug_state
    ⟹ x ∈ called state
    ⟹ TD_side.well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ TD_side.well_infl_stabl (state'⦇called := called state' - {x}⦈)
      ∧ x ∈ stabl state'
      ∧ TD_side.update_rel_opt (state⦇called := called state - {x}⦈) (state'⦇called := called state' - {x}⦈)"
    and "repeat_dom x state ug_state
    ⟹ (xd, state', ug_state') = repeat x state ug_state
    ⟹ x ∈ called state
    ⟹ TD_side.well_infl_stabl state
    ⟹ TD_side.well_infl_stabl (state'⦇called := called state' - {x}⦈)
      ∧ x ∈ stabl state'
      ∧ TD_side.update_rel_opt (state⦇called := called state - {x}⦈) (state'⦇called := called state' - {x}⦈)"
    and "eval_dom x t sides⇩a⇩c⇩c state ug_state
    ⟹ (xd, state', ug_state') = eval x t sides⇩a⇩c⇩c state ug_state
    ⟹ TD_side.well_infl_stabl state
    ⟹ x ∈ called state
    ⟹ x ∈ stabl state ⟶ (subt_for_prefix (T x) pre (σ state) = Some t
        ∧ (∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p))
    ⟹ TD_side.well_infl_stabl state'
      ∧ (x ∈ stabl state' ⟶ (∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y))
      ∧ TD_side.update_rel_opt state state'"
proof(induction x y state ug_state and x state ug_state and x state ug_state
        and y t sides⇩a⇩c⇩c state ug_state
      arbitrary: xd state' ug_state' and xd state' ug_state' and xd state' ug_state'
        and pre xd state' ug_state'
      rule: query_iterate_repeat_eval_pinduct)
  case (Query y x state ug_state)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1)
    moreover note IH = Query.IH(2)[simplified, OF Iterate(5,2) Query.prems(2)]
    ultimately show ?thesis
    proof(intro conjI, goal_cases)
      case 1
      have "slookup (infl state1) u ⊆ slookup (fminsert (infl state1) (Inl x) y) u" for u
        by (cases "Inl x = u") (auto simp add: slookup_fminsert_same slookup_fminsert_other)
      then show ?case using 1(5,6)
        unfolding TD_side.well_infl_stabl_def
        apply (simp add: 1(3) fminsert_def)
        by (auto simp add: fmlookup_default_def split: option.splits if_splits)
    next
      case 2
      show ?case by (simp add: Iterate(3) slookup_fminsert_same)
    next
      case 3
      show ?case
        using IH Iterate(3)
        by (auto simp add: slookup_fminsert)
    qed
  next
    case Lookup
    show ?thesis
      using Query.prems(2) Lookup(3)
      unfolding TD_side.well_infl_stabl_def
      by (auto simp add: Lookup(2) slookup_fminsert)
  qed
next
  case (Iterate x state ug_state)
  have inv: "TD_side.well_infl_stabl state"
    using TD_side.well_infl_stabl_simp_add_to_c[OF Iterate.prems(3)] by simp
  note IH' = Iterate.IH(2)[rotated 2, OF _ Iterate.prems(2) inv]

  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Stable Iterate.prems(3) unfolding TD_side.well_infl_stabl_def by auto
  next
    case (Fixpoint state1)
    note IH = IH'[OF Fixpoint(2,5), folded dep_def]
    then show ?thesis
      unfolding TD_side.well_infl_stabl_def
      by (auto simp add: Fixpoint(6))
  next
    case (Continue state1 xd_new xd_new' infl2 stabl2 ug_state1)
    note IH = IH'[OF Continue(2,8) refl]

    have c_state1_same_state: "called state1 = called state"
      using called_same(3)[OF Continue(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Iterate.prems(2) by simp

    have inv: "TD_side.well_infl_stabl (state1⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new'), called := called state1 - {x}⦈)"
      apply (rule TD_side.destab_upd_locale_preserves_well_infl_stabl[OF Continue(5)])
      using IH
      by auto

    note ih = Iterate.IH(3)[OF Continue(8) refl  Continue(2) refl _ Continue(3,4,5) _ Continue(7),
        simplified, OF x_in_c1 inv]

    have "called state' = called state1 - {x}"
      using called_same(2)[OF Continue(6,7)] x_in_c1 by simp

    with IH show ?thesis
    proof(elim conjE, intro conjI, goal_cases)
      case 1
      show ?case using ih by blast
    next
      case 2
      show ?case using ih by blast
    next
      case 3
      have upd_rel_destab:
        "TD_side.update_rel_opt (state1⦇called := called state1 - {x}⦈) (state1⦇infl := infl2,
          stabl := stabl2, σ := (σ state1)(Inl x := xd_new'), called := called state1 - {x}⦈)"
        using destab_opt_infl_stabl_relation[OF Continue(5)]
          TD_side.influencing_stabl_after_destab'[OF Continue(5)]
        by (auto simp add: fmlookup_default_drop_set fun_upd_other simp del: fmdrop_set_insert
            split: if_split)
      have upd_rel_begin_destab:
        "TD_side.update_rel_opt (state⦇called := called state - {x}⦈) (state1⦇infl := infl2, stabl := stabl2,
          σ := (σ state1)(Inl x := xd_new'), called := called state1 - {x}⦈)"
        apply (intro TD_side.update_rel_transitive[OF 3(4) upd_rel_destab])
        using called_non_stabl_increasing(3)[OF Continue(1,2)] ‹called state1 = called state›
          destab_opt_infl_stabl_relation[OF Continue(5)]
        by auto
      show ?case
        apply (intro TD_side.update_rel_transitive[OF upd_rel_begin_destab])
        subgoal using ih by simp
        subgoal
          using called_non_stabl_increasing(2)[OF Continue(6,7)] ‹called state' = called state1 - {x}›
            x_in_c1
          by auto
        subgoal using c_state1_same_state by simp
        subgoal using ‹called state' = called state1 - {x}› by simp
        done
    qed
  qed
next
  case (Repeat x state ug_state)
  have inv: "TD_side.well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: TD_side.well_infl_stabl_simp_c_stabl)
  have prefix: "x ∈ stabl (state⦇stabl := insert x (stabl state)⦈) ⟶ (
      subt_for_prefix (T x) [] (σ (state⦇stabl := insert x (stabl state)⦈)) = Some (T x)
      ∧ (∀p ∈ {p. Inl p ∈ set []}. x ∈ slookup (infl (state⦇stabl := insert x (stabl state)⦈)) p))"
    by simp+

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1)
    note IH = Repeat.IH(2)[OF Unstable(2) inv _ prefix, simplified, OF Repeat.prems(2)]

    have "called state1 = called state"
      using called_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have inv1: "TD_side.well_infl_stabl state1"
      using IH by simp

    note ih = Repeat.IH(3)[OF Unstable(2) _ _ Unstable(3,5) x_in_c1 inv1, of d1, simplified]

    have "called state' = called state1" using called_same(3)[OF Unstable(4,5)] by simp
    have "(called state - {x}) ∩ stabl state1 = called state ∩ stabl state1" using Unstable(3) by blast

    show ?thesis
      apply (intro conjI)
      subgoal using ih by simp
      subgoal using ih by simp
      subgoal
        apply (rule TD_side.update_rel_transitive[of _
          "state1⦇called := called state1 - {x}, stabl := insert x (stabl state1)⦈"])
        subgoal using IH Unstable(3) Repeat.prems(2)
          by (auto simp add: ‹called state1 = called state› ‹called state' = called state1›
              ‹(called state - {x}) ∩ stabl state1 = called state ∩ stabl state1› Let_def)
        subgoal using ih Unstable(3) by auto
        subgoal
          using called_non_stabl_increasing(3)[OF Unstable(4,5)] ‹called state' = called state1› x_in_c1
          by auto
        subgoal using ‹called state1 = called state› by simp
        subgoal using ‹called state' = called state1› by simp
        done
      done
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) inv _ prefix, simplified, OF Repeat.prems(2)]
    show ?thesis
      using IH Stable(3)
      unfolding TD_side.well_infl_stabl_def dep_def
      by auto
  qed
next
  case (Eval x t sides⇩a⇩c⇩c state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1)
    note IH = Eval.IH(2)[OF QueryL(1,3) Eval.prems(2)]

    have "called state1 = called state" using called_same(1)[OF QueryL(2,3)] by simp
    then have "x ∈ called state1" using Eval.prems(3) by simp
    have "called state' = called state1" using called_same(4)[OF QueryL(4,5)] by simp

    have prefix_no_indirect_side: "{p. Inl p ∈ set pre}
        ⊆ {u. ∃x ∈ called state ∩ stabl state1. x ∈ slookup (infl state) u}"
        if "x ∈ stabl state1"
      using that called_non_stabl_increasing(1)[OF QueryL(2,3)] ‹x ∈ called state1› Eval.prems(3,4) IH
      by fastforce

    have prefix: "x ∈ stabl state1 ⟶
      (subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state1) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state"
        using called_non_stabl_increasing(1)[OF QueryL(2,3)] Eval.prems(3) by blast
      show ?case using Eval.prems(4)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            subgoal using prefix_no_indirect_side ‹x ∈ stabl state1› IH by fastforce
            subgoal by simp
            done
          subgoal using QueryL(1,6) by simp
          done
      next
        case 2
        then show ?case
          using conjunct2[OF IH] prefix_no_indirect_side[OF 1] by fastforce
      qed
    qed

    note ih = Eval.IH(3)[OF QueryL(1,3) _ _ QueryL(5) conjunct1[OF IH] ‹x ∈ called state1› prefix,
        simplified]

    have y_unaffected:
      "Inl y ∈ {u. ∃x ∈ called state1 ∩ stabl state'. x ∈ slookup (infl state1) u}"
        if "x ∈ stabl state'"
      using lookup_in_influenced that called_non_stabl_increasing(4)[OF QueryL(4,5)]
        prefix called_same(4)[OF QueryL(4,5)] ‹x ∈ called state1›
      by fastforce
    have y_value_unchanged: "(σ state') (Inl y) = yd" if "x ∈ stabl state'"
      using y_unaffected[OF that] ih QueryL(6) by fastforce
    have y_infl_incr: "slookup (infl state1) (Inl y) ⊆ slookup (infl state') (Inl y)"
      if "x ∈ stabl state'"
      using y_unaffected[OF that] ih by auto

    show ?thesis
      apply (intro conjI)
      subgoal using ih by simp
      subgoal using ih IH y_infl_incr by (auto simp add: QueryL(1) y_value_unchanged)
      subgoal
        apply (rule TD_side.update_rel_transitive[of _ state1])
        using IH ih called_non_stabl_increasing(4)[OF QueryL(4,5)] ‹called state' = called state1›
          ‹called state1 = called state›
        by auto
      done
  next
    case (QueryG y g yd)
    have inv: "TD_side.well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2)
      unfolding TD_side.well_infl_stabl_def fmlookup_default_def fminsert_def by auto
    have prefix: "x ∈ stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈) ⟶ (
        subt_for_prefix (T x) (pre @ [Inl (Inr y)])
        (σ (state⦇infl := fminsert (infl state) (Inr y) x⦈)) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inr y)])}. x ∈ slookup
        (infl (state⦇infl := fminsert (infl state) (Inr y) x⦈)) p))"
      using Eval.prems(4) QueryG(1,2) subt_for_prefix_transitive[of "T x" pre _ t "[Inl (Inr y)]"]
      by (simp add: fminsert_def fmlookup_default_def)
    note IH = Eval.IH(4)[OF QueryG(1-2,4) inv _ prefix, simplified, OF Eval.prems(3)]

    have y_unaffected: "Inr y ∈ {u. ∃z ∈ called state ∩ stabl state'.
        z ∈ slookup (fminsert (infl state) (Inr y) x) u}"
        if "x ∈ stabl state'"
      using lookup_in_influenced that called_non_stabl_increasing(4)[OF QueryG(3,4)]
        called_same(4)[OF QueryG(3,4)] ‹x ∈ called state›
      by (auto simp add: slookup_fminsert_same)
    have y_value_unchanged: "(σ state') (Inr y) = yd" if "x ∈ stabl state'"
      using y_unaffected IH QueryG(2) that by fastforce
    have y_infl_incr: "slookup (infl (state⦇infl := fminsert (infl state) (Inr y) x⦈)) (Inr y)
        ⊆ slookup (infl state') (Inr y)" if "x ∈ stabl state'"
      using y_unaffected IH that by fastforce

    show ?thesis
      apply (intro conjI)
      subgoal using IH by simp
      subgoal
        using IH y_infl_incr by (auto simp add: QueryG(1) y_value_unchanged slookup_fminsert_same)
      subgoal using IH by (auto simp add: slookup_fminsert split: if_splits)
      done
  next
    case (Side_Subsumed y yd t1 sides⇩a⇩c⇩c' d' ug_state1)
    have prefix: "x ∈ stabl state ⟶
      (subt_for_prefix (T x) (pre @ [Inr (y, yd)]) (σ state) = Some t1
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inr (y, yd)])}. x ∈ slookup (infl state) p))"
      using Eval.prems(4) subt_for_prefix_transitive[of "T x" pre _ t "[Inr (y, yd)]" t1]
        Side_Subsumed(1,5)
      by simp
    have well_infl_stabl_1: "TD_side.well_infl_stabl state"
      using Eval.prems(2) Side_Subsumed(5) unfolding TD_side.well_infl_stabl_def by simp
    have x_in_c1: "x ∈ called state" using Eval.prems(3) by simp
    note IH = Eval.IH(5)[OF Side_Subsumed(1-4) _ _ Side_Subsumed(6)
        well_infl_stabl_1 x_in_c1 prefix, simplified]

    have "x ∈ stabl state' ⟶ (∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y)"
      using IH Side_Subsumed(5)
      by (simp add: Side_Subsumed(1) dep_aux⇩L_def)

    then show ?thesis using IH Side_Subsumed(5) by simp
  next
    case (Side_Effect y yd t1 d' sides⇩a⇩c⇩c' d'' ug_state1 infl1 stabl1)
    have inv: "TD_side.well_infl_stabl (state ⦇infl := infl1, stabl := stabl1,
        σ := (σ state)(Inr y := d'')⦈)"
      using TD_side.destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5)] Eval.prems(2)
      unfolding TD_side.well_infl_stabl_def
      by simp
    have x_stabl_if_stabl1: "x ∈ stabl state" if "x ∈ stabl1"
      using destab_opt_infl_stabl_relation[OF Side_Effect(5)] that by simp

    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(4) that by simp

    have y_not_in_prefix: "Inl (Inr y) ∉ set pre" if "x ∈ stabl1"
    proof (rule ccontr, goal_cases)
      case 1
      then have "x ∈ slookup (infl state) (Inr y)"
        using prefix_recorded_in_infl that x_stabl_if_stabl1 by simp
      then have "x ∈ influenced_by_cutoff (infl state) (Inr y) (Inl ` called state - {Inr y})"
        by (auto intro!: influenced_by_cutoff.base simp add: fmlookup_default_def)
      then show ?case
        using destab_opt_infl_stabl_relation[OF Side_Effect(5)] that by simp
    qed

    have prefix: "x ∈ stabl1 ⟶
      subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d'')) = Some t1 ∧
      (∀p. Inl p ∈ set (pre @ [Inr (y, yd)]) ⟶ x ∈ slookup infl1 p)"
    proof
      assume A: "x ∈ stabl1"
      then have "x ∈ stabl state" using x_stabl_if_stabl1 by auto
      have P: "subt_for_prefix (T x) pre ((σ state)(Inr y := d'')) = Some t"
        apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
        subgoal using y_not_in_prefix A by (simp add: fun_upd_apply)
        subgoal using Eval.prems(4) x_stabl_if_stabl1 A by simp
        done
      show "subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d'')) = Some t1 ∧
        (∀p. Inl p ∈ set (pre @ [Inr (y, yd)]) ⟶ x ∈ slookup infl1 p)"
        apply (intro conjI)
        using subt_for_prefix_transitive[OF P(1), of "[Inr (y, yd)]" t1]
        apply (subst subt_for_prefix_transitive[OF P(1), of "[Inr (y, yd)]" t1])
        subgoal using Side_Effect(1) by simp
        subgoal by simp
        subgoal
          using Eval.prems(4) ‹x ∈ stabl state›
            TD_side.influencing_stabl_after_destab'[OF Side_Effect(5) _ A]
          by auto
        done
    qed
    have x_in_c1: "x ∈ called state" using Eval.prems(3) Side_Effect(5) by simp

    note IH = Eval.IH(6)[OF Side_Effect(1-4) refl refl Side_Effect(5) refl Side_Effect(7),
        simplified, OF inv x_in_c1 prefix]

    have upd_rel_destab:
      "TD_side.update_rel_opt state (state⦇infl := infl1, stabl := stabl1,
        σ := (σ state)(Inr y := d'')⦈)"
      using destab_opt_infl_stabl_relation[OF Side_Effect(5)] Side_Effect(5)
        TD_side.influencing_stabl_after_destab'[OF Side_Effect(5)]
      by (auto simp add: fmlookup_default_drop_set fun_upd_other simp del: fmdrop_set_insert
          split: if_split)

    have "called state' = called state"
      using called_same(4)[OF Side_Effect(6,7)] by simp

    have "x ∈ stabl state' ⟶ (∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y)"
      using IH by (simp add: Side_Effect(1) dep_aux⇩L_def)

    then show ?thesis
      apply (intro conjI)
      subgoal using IH by simp
      subgoal using IH by simp
      subgoal
        apply (rule TD_side.update_rel_transitive[OF upd_rel_destab])
        subgoal using IH by auto
        subgoal
          using called_non_stabl_increasing(4)[OF Side_Effect(6,7)] ‹called state' = called state› by auto
        subgoal by simp
        subgoal using ‹called state' = called state› by simp
        done
      done
  next
    case Answer
    have "∀y∈dep_aux (σ state') t. x ∈ slookup (infl state') y"
      by (simp add: Answer(1) dep_aux_def)
    moreover have "dep_aux⇩L (σ state) t ⊆ stabl state ∪ called state"
      by (simp add: Answer(1) dep_aux⇩L_def)
    ultimately show ?thesis using Eval.prems(2) Answer(2) by fastforce
  qed
qed

corollary solve_returns_stabl_closed_under_dep:
  assumes "solve_dom x"
    and "solve x = (st, sigma)"
  shows "∀x∈st. dep⇩L T sigma x ⊆ st"
proof -
  obtain xd state' ug_state' where iterate: "(xd, state', ug_state') =
        iterate x (init_state⦇ called := insert x (called init_state) ⦈) init_ug_state"
      and "st = stabl state'" and "sigma = σ state'"
    using assms unfolding solve_dom_def solve_def
    by (cases "iterate x (init_state⦇called := insert x (called init_state)⦈) init_ug_state") auto
  then have "TD_side.well_infl_stabl (state'⦇called := called state' - {x}⦈)"
    using well_infl_stabl_ind(2)[OF assms(1)[unfolded solve_dom_def]]
    unfolding TD_side.well_infl_stabl_def init_state_def fmlookup_default_def
    by auto
  show ?thesis
    using TD_side.well_infl_stabl_implies_stabl_c_closed[OF
        ‹TD_side.well_infl_stabl (state'⦇called := called state' - {x}⦈)›] ‹st = stabl state'›
        ‹sigma = σ state'› called_same(2)[OF assms(1)[unfolded solve_dom_def] iterate]
    unfolding TD_side.TD_side.well_infl_stabl_def init_state_def
    by simp
qed


subsection ‹Partial Correctness›

abbreviation rho_invariant :: "('x + 'g ⇒ 'd) ⇒ ('g ⇒ ('x, 'd) fmap) ⇒ bool" where
  "rho_invariant sigma rho ≡ ∀g orig. rho_lookup rho g orig ≤ sigma (Inr g)"

abbreviation part_post_solution_inv :: "('x,'g,'d) state ⇒ ('g ⇒ ('x, 'd) fmap) ⇒ bool" where
  "part_post_solution_inv state rho ≡ (∀x ∈ stabl state - called state.
    traverse_rhs (T x) (σ state) ≤ (σ state) (Inl x)
    ∧ sides_of_rhs (T x) (σ state) ≤
      (λu. case u of Inl _ ⇒ ⊥ | Inr g ⇒ rho_lookup rho g x))
    ∧ rho_invariant (σ state) rho"

lemma subt_for_prefix_Answer_rho_subsumes:
  "subt_for_prefix t pre sigma = Some (Answer d)
   ⟹ ∀(u, ud) ∈ {s. Inr s ∈ set pre}. ud ≤ rho_lookup rho u x
   ⟹ sides_of_rhs t sigma ≤ case_sum (λ_. ⊥) (λg. rho_lookup rho g x)"
  apply (induction t pre sigma rule: subt_for_prefix.induct)
  apply (auto simp add: Let_def le_fun_def fun_upd_def split: if_splits)
  by (metis old.sum.simps(6))

lemma subsumes_se_eq':
  assumes "∀u ∈ dep_aux sigma t. sigma u = sigma' u"
    and "sides_of_rhs t sigma ≤ rho"
  shows "sides_of_rhs t sigma' ≤ rho"
  using assms(2,1)
  apply (induction t)
  by (auto simp add: dep_aux_def Let_def le_fun_def fun_upd_def split: if_splits)

lemma sides_of_rhs_local: "sides_of_rhs t (σ state) (Inl x) = ⊥"
  by (induction t) (auto simp add: Let_def fun_upd_def)

subsubsection ‹Preservation of the Partial Solution when Destabilizing›

lemma destab_upd_locale_preserves_part_post_solution:
  assumes destab: "(infl2, stabl2) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1)"
      and IH: "part_post_solution_inv state1 rho1"
          "eq T x (σ state1) ≤ xd_new"
          "sides_of_rhs (T x) (σ state1) ≤ case_sum (λx. ⊥) (λg. rho_lookup rho1 g x)"
      and x_in_c1: "x ∈ called state1"
      and well_infl_stabl_1: "TD_side.well_infl_stabl (state1⦇called := called state1 - {x}⦈)"
    shows "part_post_solution_inv (state1⦇σ := (σ state1)(Inl x := xd_new), stabl := stabl2,
            infl := infl2, called := called state1 - {x}⦈) rho1"
proof -
  have "part_post_solution_inv (state1⦇σ := (σ state1)(Inl x := xd_new), stabl := stabl2⦈) rho1"
  proof (intro conjI, intro ballI, goal_cases)
    case (1 y)
    then have "y ∈ stabl2 - called state1" by simp
    then have "y ∈ stabl state1 - called state1" "x ≠ y"
      using destab x_in_c1 destab_opt_infl_stabl_relation[OF destab] by auto
    then have "eq T y (σ state1) ≤ (σ state1) (Inl y)"
      "sides_of_rhs (T y) (σ state1) ≤ (λu. case u of Inl x ⇒ ⊥ | Inr g ⇒ rho_lookup rho1 g y)"
      using IH by simp+
    have "Inl x ∉ dep T (σ state1) y"
    proof (rule ccontr, goal_cases)
      case 1
      then have "Inl x ∈ dep T (σ state1) y" by simp
      then have "y ∈ slookup (infl state1) (Inl x)"
        using well_infl_stabl_1 ‹y ∈ stabl state1 - called state1›
        unfolding TD_side.well_infl_stabl_def
        by simp
      then have "y ∈ influenced_by_cutoff (infl state1) (Inl x) (Inl ` called state1 - {Inl x})"
        using lookup_in_influenced_cutoff
        by fast
      then have "y ∉ stabl2" using destab_opt_infl_stabl_relation[OF destab] by simp
      then show ?case using ‹y ∈ stabl2 - called state1› by simp
    qed
    then have "eq T y (σ state1) = eq T y ((σ state1)(Inl x := xd_new))"
      using eq_mupd_no_dep
      unfolding dep_def by fast
    moreover have "(σ state1) (Inl y) = ((σ state1)(Inl x := xd_new)) (Inl y)"
      using ‹x ≠ y› by (simp add: fun_upd_other)
    moreover have "sides_of_rhs (T y) ((σ state1)(Inl x := xd_new))
        ≤ (λu. case u of Inl x ⇒ ⊥ | Inr g ⇒ rho_lookup rho1 g y)"
      apply (rule subsumes_se_eq'[of "σ state1"])
      subgoal
      proof -
        have "Inl x ∉ dep_aux (σ state1) (T y)"
          using ‹Inl x ∉ dep T (σ state1) y› unfolding dep_aux_def dep_def by simp
        then show ?thesis by (metis fun_upd_other)
      qed
      subgoal
        using IH ‹y ∈ stabl state1 - called state1› by blast
      done
    ultimately show ?case apply (simp cong: sum.case_cong)
      using ‹eq T y (σ state1) ≤ (σ state1) (Inl y)› by simp
  next
    case 2
    then show ?case using IH by (simp add: le_fun_def fun_upd_def)
  qed
  moreover have "eq T x ((σ state1)(Inl x := xd_new)) ≤ xd_new"
    "sides_of_rhs (T x) ((σ state1)(Inl x := xd_new))
      ≤ (λu. case u of Inl x ⇒ ⊥ | Inr g ⇒ rho_lookup rho1 g x)"
    if "x ∈ stabl2"
  proof -
    have "x ∈ stabl state1"
      using that destab_opt_infl_stabl_relation[OF destab] by simp
    have "x ∉ influenced_by_cutoff (infl state1) (Inl x) (Inl ` called state1 - {Inl x})"
      using that destab_opt_infl_stabl_relation[OF destab] by simp
    then have "x ∉ slookup (infl state1) (Inl x)"
      using lookup_in_influenced_cutoff by fast
    then have "Inl x ∉ dep T (σ state1) x"
      using conjunct1[OF well_infl_stabl_1[unfolded TD_side.well_infl_stabl_def]]
        ‹x ∈ stabl state1›
      by auto
    then show "eq T x ((σ state1)(Inl x := xd_new)) ≤ xd_new"
      using eq_mupd_no_dep IH
      unfolding dep_def by fastforce
    show "sides_of_rhs (T x) ((σ state1)(Inl x := xd_new))
        ≤ (λu. case u of Inl x ⇒ ⊥ | Inr g ⇒ rho_lookup rho1 g x)"
      apply (rule subsumes_se_eq'[of "σ state1"])
      subgoal
      proof -
        have "Inl x ∉ dep_aux (σ state1) (T x)"
          using ‹Inl x ∉ dep T (σ state1) x› unfolding dep_aux_def dep_def by simp
        then show ?thesis
          using ‹Inl x ∉ dep T (σ state1) x›
          by (metis fun_upd_other)
      qed
      subgoal
        using IH by blast
      done
  qed
  ultimately show ?thesis by (auto simp add: fun_upd_same cong: sum.case_cong)
qed

lemma destab_upd_globale_preserves_part_post_solution:
  assumes destab: "(infl1, stabl1) = destab_opt (Inr y) (infl state) (stabl state) (called state)"
      and part_sol_inv: "(∀x ∈ stabl state - called state.
        traverse_rhs (T x) (σ state) ≤ (σ state) (Inl x)
        ∧ sides_of_rhs (T x) (σ state) ≤ (λu. case u of Inl _ ⇒ ⊥ | Inr g ⇒ rho_lookup rho g x))"
      and rho_inv: "rho_invariant ((σ state)(Inr y := d')) rho"
      and well_infl_stabl: "TD_side.well_infl_stabl state"
    shows "part_post_solution_inv (state⦇infl := infl1, stabl := stabl1,
        σ := (σ state)(Inr y := d')⦈) rho"
proof (intro conjI, intro ballI, goal_cases)
  case (1 x)
  then have "x ∈ stabl1 - called state" by simp
  then have "x ∈ stabl state - called state"
    using destab_opt_infl_stabl_relation[OF destab] by auto
  then have "eq T x (σ state) ≤ (σ state) (Inl x)"
    "sides_of_rhs (T x) (σ state) ≤ (λu. case u of Inl x ⇒ ⊥ | Inr g ⇒ rho_lookup rho g x)"
    using part_sol_inv by simp+
  have "Inr y ∉ dep T (σ state) x"
  proof (rule ccontr, goal_cases)
    case 1
    then have "Inr y ∈ dep T (σ state) x" by simp
    then have "x ∈ slookup (infl state) (Inr y)"
      using well_infl_stabl ‹x ∈ stabl state - called state›
      unfolding TD_side.well_infl_stabl_def by simp
    then have "x ∈ influenced_by_cutoff (infl state) (Inr y) (Inl ` called state - {Inr y})"
      using lookup_in_influenced_cutoff by fast
    then have "x ∉ stabl1" using destab_opt_infl_stabl_relation[OF destab] by simp
    then show ?case using ‹x ∈ stabl1 - called state› by simp
  qed
  then have "eq T x (σ state) = eq T x ((σ state)(Inr y := d'))"
    using eq_mupd_no_dep
    unfolding dep_def by fast
  moreover have "(σ state) (Inl x) = ((σ state)(Inr y := d')) (Inl x)"
    by (simp add: fun_upd_other)
  moreover have "sides_of_rhs (T x) ((σ state)(Inr y := d'))
      ≤ (λu. case u of Inl x ⇒ ⊥ | Inr g ⇒ rho_lookup rho g x)"
    apply (rule subsumes_se_eq'[of "σ state"])
    subgoal
    proof -
      have "Inr y ∉ dep_aux (σ state) (T x)"
        using ‹Inr y ∉ dep T (σ state) x› unfolding dep_aux_def dep_def by simp
      then show ?thesis
        using ‹Inr y ∉ dep T (σ state) x›
        by (metis fun_upd_other)
    qed
    subgoal
      using part_sol_inv ‹x ∈ stabl state - called state› by blast
    done
  ultimately show ?case
    using ‹eq T x (σ state) ≤ (σ state) (Inl x)› 1 by (auto cong: sum.case_cong)
next
  case 2
  show ?case using rho_inv by simp
qed

subsubsection ‹Induction Proof›

lemma partial_solution_ind:
  shows "query_dom x y state ug_state
    ⟹ (xd, state', ug_state') = query x y state ug_state
    ⟹ TD_side.well_infl_stabl state
    ⟹ part_post_solution_inv state (ρ ug_state)
    ⟹ part_post_solution_inv state' (ρ ug_state')
        ∧ (∀x ∈ called state. (λg. rho_lookup (ρ ug_state) g x) = (λg. rho_lookup (ρ ug_state') g x))"
    and "iterate_dom x state ug_state
    ⟹ (xd, state', ug_state') = iterate x state ug_state
    ⟹ x ∈ called state
    ⟹ TD_side.well_infl_stabl (state⦇called := called state - {x}⦈)
    ⟹ part_post_solution_inv (state⦇called := called state - {x}⦈) (ρ ug_state)
    ⟹ part_post_solution_inv (state'⦇called := called state' - {x}⦈) (ρ ug_state') ∧ (∀x ∈ called state - {x}.
          (λg. rho_lookup (ρ ug_state) g x) = (λg. rho_lookup (ρ ug_state') g x))"
    and "repeat_dom x state ug_state
    ⟹ (xd, state', ug_state') = repeat x state ug_state
    ⟹ x ∈ called state
    ⟹ TD_side.well_infl_stabl state
    ⟹ part_post_solution_inv state (ρ ug_state)
    ⟹ part_post_solution_inv state' (ρ ug_state')
        ∧ (∀x ∈ called state - {x}. (λg. rho_lookup (ρ ug_state) g x)
          = (λg. rho_lookup (ρ ug_state') g x))
        ∧ traverse_rhs (T x) (σ state') = xd
        ∧ sides_of_rhs (T x) (σ state') ≤ case_sum (λx. ⊥) (λg. rho_lookup (ρ ug_state') g x)"
    and "eval_dom x t sides⇩a⇩c⇩c state ug_state
    ⟹ (xd, state', ug_state') = eval x t sides⇩a⇩c⇩c state ug_state
    ⟹ TD_side.well_infl_stabl state
    ⟹ part_post_solution_inv state (ρ ug_state)
    ⟹ x ∈ called state
    ⟹ x ∈ stabl state ⟶ (subt_for_prefix (T x) pre (σ state) = Some t
        ∧ (∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p)
        ∧ (∀(u, ud) ∈ {s. Inr s ∈ set pre}. ud ≤ sides⇩a⇩c⇩c u
           ∧ sides⇩a⇩c⇩c u ≤ rho_lookup (ρ ug_state) u x))
    ⟹ part_post_solution_inv state' (ρ ug_state')
        ∧ (∀x ∈ called state - {x}. (λg. rho_lookup (ρ ug_state) g x)
          = (λg. rho_lookup (ρ ug_state') g x))
        ∧ (x ∈ stabl state' ⟶ traverse_rhs (T x) (σ state') = xd
                                ∧ sides_of_rhs (T x) (σ state')
                                    ≤ case_sum (λx. ⊥) (λg. rho_lookup (ρ ug_state') g x))"
proof(induction x y state ug_state and x state ug_state and x state ug_state
        and y t sides⇩a⇩c⇩c state ug_state
      arbitrary: xd state' ug_state' and xd state' ug_state' and xd state' ug_state'
        and pre xd state' ug_state'
      rule: query_iterate_repeat_eval_pinduct)
  case (Query y x state ug_state)
  show ?case using Query.IH(1) Query.prems(1)
  proof(cases rule: query_iterate_lookup_cases)
    case (Iterate state1 xd)
    note IH = Query.IH(2)[simplified, OF Iterate(5,2) Query.prems(2-3)]
    then show ?thesis by (simp add: Iterate(3) cong: sum.case_cong)
  next
    case Lookup
    show ?thesis using Query.prems(3) by (simp add: Lookup(2,4) cong: sum.case_cong)
  qed
next
  case (Iterate x state ug_state)
  have inv: "TD_side.well_infl_stabl state"
    using Iterate.prems(3) unfolding TD_side.well_infl_stabl_def
    by auto
  have part_post_solution: "part_post_solution_inv state (ρ ug_state)"
    using Iterate.prems(4) by (simp cong: sum.case_cong)
  note IH' = Iterate.IH(2)[rotated 3, OF Iterate.prems(2) inv part_post_solution]

  show ?case using Iterate.IH(1) Iterate.prems(1)
  proof(cases rule: iterate_continue_fixpoint_cases)
    case Stable
    show ?thesis using Stable(2,3) Iterate.prems(4) by (simp add: Stable(1,4) cong: sum.case_cong)
  next
    case (Fixpoint state1 xd_new ug_state1)
    have inv: "TD_side.well_infl_stabl state"
      using Iterate.prems(2,3)
      unfolding TD_side.well_infl_stabl_def
      by auto
    note IH = IH'[OF Fixpoint(5) _ Fixpoint(2), folded dep_def, of "x ∈ point state", simplified]

    have "xd_new ≤ (σ state1) (Inl x)"
      using Fixpoint(3,4) warrowing_properties(2) by (simp split: if_splits)
    then show ?thesis using IH by (auto simp add: Fixpoint(3,6,7) cong: sum.case_cong)
  next
    case (Continue state1 xd_new xd_new' infl2 stabl2 ug_state1)
    have inv: "TD_side.well_infl_stabl state"
      using Iterate.prems(2,3)
      unfolding TD_side.well_infl_stabl_def
      by auto
    note IH = IH'[OF Continue(8) _ Continue(2), of "x ∈ point state", simplified]
    note well_infl_stabl_1 = well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) inv]

    have x_in_c1: "x ∈ called state1" using called_same(3)[OF Continue(1,2)] Iterate.prems(2) by simp

    have inv: "TD_side.well_infl_stabl (state1 ⦇infl := infl2, stabl := stabl2,
        σ := (σ state1)(Inl x := xd_new'), called := called state1 - {x}⦈)"
      apply (rule TD_side.destab_upd_locale_preserves_well_infl_stabl[OF Continue(5)])
      using conjunct1[OF well_infl_stabl_ind(3)[OF Continue(1,2) Iterate.prems(2) inv]]
      unfolding TD_side.well_infl_stabl_def
      by auto
    have part_post_solution_2: "(∀u∈stabl2 - (called state1 - {x}).
        eq T u ((σ state1)(Inl x := xd_new'))
          ≤ ((σ state1)(Inl x := xd_new')) (Inl u) ∧
        sides_of_rhs (T u) ((σ state1)(Inl x := xd_new'))
          ≤ case_sum (λx. ⊥) (λg. rho_lookup (ρ ug_state1) g u)) ∧
        rho_invariant ((σ state1)(Inl x := xd_new')) (ρ ug_state1)"
      using destab_upd_locale_preserves_part_post_solution[OF Continue(5) _ _ _
          x_in_c1 conjunct1[OF well_infl_stabl_1], of "ρ ug_state1" xd_new'] IH Continue(3)
          warrowing_properties(1)
      by (auto split: if_splits)

    note ih = Iterate.IH(3)[OF Continue(8) _ Continue(2) refl _ Continue(3-5) _ Continue(7),
        simplified, OF x_in_c1 inv, OF part_post_solution_2]

    then show ?thesis using IH called_same(3)[OF Continue(1,2)] by (simp cong: sum.case_cong)
  qed
next
  case (Repeat x state ug_state)
  have inv: "TD_side.well_infl_stabl (state⦇stabl := insert x (stabl state)⦈)"
    using Repeat.prems(2,3) by (simp add: TD_side.well_infl_stabl_simp_c_stabl)
  have part_post: "part_post_solution_inv (state⦇stabl := insert x (stabl state)⦈) (ρ ug_state)"
    using Repeat.prems(2,4) by (simp cong: sum.case_cong)

  show ?case using Repeat.IH(1) Repeat.prems(1)
  proof (cases rule: repeat_unstable_stable_cases)
    case (Unstable state1 d1 ug_state1)
    note IH = Repeat.IH(2)[OF Unstable(2) inv part_post, of "[]", simplified, OF Repeat.prems(2)]

    have "called state1 = called state"
      using called_same(4)[OF Unstable(1,2)] by simp
    then have x_in_c1: "x ∈ called state1"
      using Repeat.prems(2) by simp
    have inv1: "TD_side.well_infl_stabl state1"
      using well_infl_stabl_ind(4)[OF Unstable(1,2) inv, of "[]", simplified, OF Repeat.prems(2)]
      by simp
    have part_post_inv: "part_post_solution_inv state1 (ρ ug_state1)"
      using IH by simp

    note ih = Repeat.IH(3)[OF Unstable(2) _ _ Unstable(3,5) x_in_c1 inv1 part_post_inv, simplified]

    then show ?thesis using IH ‹called state1 = called state› by simp
  next
    case Stable
    note IH = Repeat.IH(2)[OF Stable(2) inv part_post, of "[]", simplified, OF Repeat.prems(2)]
    then show ?thesis using Stable(3) by simp
  qed
next
  case (Eval x t sides⇩a⇩c⇩c state ug_state)
  show ?case using Eval.IH(1) Eval.prems(1)
  proof(cases rule: eval_query_answer_cases)
    case (QueryL y g yd state1 ug_state1)
    note IH = Eval.IH(2)[OF QueryL(1,3) Eval.prems(2-3)]
    note well_infl_stabl_1 = well_infl_stabl_ind(1)[OF QueryL(2,3) Eval.prems(2)]

    have "called state1 = called state" using called_same(1)[OF QueryL(2,3)] by simp
    then have "x ∈ called state1" using Eval.prems(4) by simp

    have prefix_no_indirect_side: "{p. Inl p ∈ set pre}
        ⊆ {u. ∃x ∈ called state ∩ stabl state1. x ∈ slookup (infl state) u}"
        if "x ∈ stabl state1"
      using that called_non_stabl_increasing(1)[OF QueryL(2,3)] ‹x ∈ called state1› Eval.prems(4,5) IH
      by fastforce

    have prefix: "x ∈ stabl state1 ⟶
      (subt_for_prefix (T x) (pre @ [Inl (Inl y)]) (σ state1) = Some (g yd)
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inl (Inl y)])}. x ∈ slookup (infl state1) p)
      ∧ (∀(u,ud) ∈ {s. Inr s ∈ set (pre @ [Inl (Inl y)])}.
        ud ≤ sides⇩a⇩c⇩c u ∧ sides⇩a⇩c⇩c u ≤ rho_lookup (ρ ug_state1) u x))"
    proof (intro impI, goal_cases)
      case 1
      then have "x ∈ stabl state"
        using called_non_stabl_increasing(1)[OF QueryL(2,3)] Eval.prems(4) by blast
      show ?case using Eval.prems(5)[rule_format, OF ‹x ∈ stabl state›]
      proof (intro conjI impI, goal_cases)
        case 1
        then show ?case
          apply (intro subt_for_prefix_transitive[where ?t2.0=t])
          subgoal
            apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
            subgoal using prefix_no_indirect_side ‹x ∈ stabl state1› well_infl_stabl_1 by fastforce
            subgoal by simp
            done
          subgoal using QueryL(1,6) by simp
          done
      next
        case 2
        then show ?case
          using conjunct2[OF well_infl_stabl_1] prefix_no_indirect_side[OF 1] by fastforce
      next
        case 3
        have "rho_lookup (ρ ug_state1) u x = rho_lookup (ρ ug_state) u x" for u
          using conjunct2[OF IH, rule_format, OF Eval.prems(4)] by metis
        then show ?case using 3 Eval.prems(4) by auto
      qed
    qed

    note ih = Eval.IH(3)[OF QueryL(1,3) _ _ QueryL(5) conjunct1[OF well_infl_stabl_1]
        conjunct1[OF IH] ‹x ∈ called state1› prefix, simplified]

    then show ?thesis using conjunct2[OF IH] ‹called state1 = called state› by simp
  next
    case (QueryG y g yd)
    have inv: "TD_side.well_infl_stabl (state⦇infl := fminsert (infl state) (Inr y) x⦈)"
      using Eval.prems(2) unfolding TD_side.well_infl_stabl_def fmlookup_default_def fminsert_def
      by auto
    have part_post_inv:
        "part_post_solution_inv (state⦇infl := fminsert (infl state) (Inr y) x⦈) (ρ ug_state)"
      using Eval.prems(3) unfolding fmlookup_default_def fminsert_def
      by (simp cong: sum.case_cong)
    have prefix: "x ∈ stabl state ⟶
        subt_for_prefix (T x) (pre @ [Inl (Inr y)]) (σ state) = Some (g yd) ∧
        (∀p. Inl p ∈ set (pre @ [Inl (Inr y)]) ⟶
            x ∈ slookup (fminsert (infl state) (Inr y) x) p) ∧
        (∀a b. Inr (a, b) ∈ set (pre @ [Inl (Inr y)]) ⟶
          b ≤ sides⇩a⇩c⇩c a ∧ sides⇩a⇩c⇩c a ≤ rho_lookup (ρ ug_state) a x)"
      using Eval.prems(5) QueryG(1,2) subt_for_prefix_transitive[of "T x" pre _ t "[Inl (Inr y)]"]
      by (simp add: fminsert_def fmlookup_default_def)

    note IH = Eval.IH(4)[OF QueryG(1,2,4) inv part_post_inv, simplified, OF Eval.prems(4) prefix]

    then show ?thesis using IH by simp
  next
    case (Side_Subsumed y yd t1 sides⇩a⇩c⇩c' d' ug_state1)
    have inv: "TD_side.well_infl_stabl state" and x_in_c_state1: "x ∈ called state"
      using Eval.prems(2,4) Side_Subsumed(5)
      unfolding TD_side.well_infl_stabl_def
      by auto
    have part_post: "part_post_solution_inv state (ρ ug_state1)"
      using Eval.prems(3,4) update_global_untouched(1,2)[OF Side_Subsumed(4)] Side_Subsumed(5)
        update_global_preserves_rho_invariant(1)[OF Side_Subsumed(4)]
      by (fastforce simp add: le_fun_def sides_of_rhs_local split: sum.splits)
    have prefix: "x ∈ stabl state ⟶
      (subt_for_prefix (T x) (pre @ [Inr (y, yd)]) (σ state) = Some t1
      ∧ (∀p ∈ {p. Inl p ∈ set (pre @ [Inr (y, yd)])}. x ∈ slookup (infl state) p)
      ∧ (∀(u, ud) ∈ {s. Inr s ∈ set (pre @ [Inr (y, yd)])}.
        ud ≤ sides⇩a⇩c⇩c' u ∧ sides⇩a⇩c⇩c' u ≤ rho_lookup (ρ ug_state1) u x))"
      using Eval.prems(5) subt_for_prefix_transitive[of "T x" pre _ t "[Inr (y, yd)]" t1]
        Side_Subsumed(1-5) update_global_recorded_in_rho[OF Side_Subsumed(4)]
        update_global_untouched(1)[OF Side_Subsumed(4)]
      by (auto intro: le_supI1 simp add: fun_upd_def)

    note IH = Eval.IH(5)[OF Side_Subsumed(1-4) _ _ Side_Subsumed(6) inv
        part_post x_in_c_state1 prefix, simplified]

    show ?thesis
      using IH update_global_untouched(2)[OF Side_Subsumed(4)] Side_Subsumed(5)
      by auto
  next
    case (Side_Effect y yd t1 d' sides⇩a⇩c⇩c' d'' ug_state1 infl1 stabl1)
    have inv: "TD_side.well_infl_stabl (state ⦇infl := infl1, stabl := stabl1,
      σ := (σ state)(Inr y := d'')⦈)"
      using TD_side.destab_upd_globale_preserves_well_infl_stabl[OF Side_Effect(5)] Eval.prems(2)
        Side_Effect(5)
      unfolding TD_side.well_infl_stabl_def
      by simp
    have x_stabl_if_stabl1: "x ∈ stabl state" if "x ∈ stabl1"
      using destab_opt_infl_stabl_relation[OF Side_Effect(5)] that Side_Effect(5) by simp

    have prefix_recorded_in_infl:
      "∀p ∈ {p. Inl p ∈ set pre}. x ∈ slookup (infl state) p" if "x ∈ stabl state"
      using Eval.prems(5) that by simp

    have y_not_in_prefix: "Inl (Inr y) ∉ set pre" if "x ∈ stabl1"
    proof (rule ccontr, goal_cases)
      case 1
      then have "x ∈ slookup (infl state) (Inr y)"
        using prefix_recorded_in_infl that x_stabl_if_stabl1 by simp
      then have "x ∈ influenced_by_cutoff (infl state) (Inr y) (Inl ` called state - {Inr y})"
        using lookup_in_influenced_cutoff by fastforce
      then show ?case
        using destab_opt_infl_stabl_relation[OF Side_Effect(5)] that Side_Effect(5) by simp
    qed

    have prefix: "x ∈ stabl1 ⟶
      subt_for_prefix (T x) (pre @ [Inr (y, yd)]) ((σ state)(Inr y := d'')) = Some t1 ∧
      (∀p. Inl p ∈ set (pre @ [Inr (y, yd)]) ⟶ x ∈ slookup infl1 p) ∧
      (∀a b. Inr (a, b) ∈ set (pre @ [Inr (y, yd)]) ⟶
        b ≤ sides⇩a⇩c⇩c' a ∧ sides⇩a⇩c⇩c' a ≤ rho_lookup (ρ ug_state1) a x)"
    proof (intro impI conjI, goal_cases)
      case 1
      have P: "subt_for_prefix (T x) pre ((σ state)(Inr y := d'')) = Some t"
        apply (subst subt_for_prefix_same[where ?sigma'="(σ state)"])
        subgoal using y_not_in_prefix 1 by (simp add: fun_upd_apply mlup_def)
        subgoal using Eval.prems(5) x_stabl_if_stabl1 1 by simp
        done
      then show ?case using Side_Effect(1) by (auto intro: subt_for_prefix_transitive[OF P])
    next
      case 2
      then show ?case
        using TD_side.influencing_stabl_after_destab'[OF Side_Effect(5)] x_stabl_if_stabl1
            prefix_recorded_in_infl
          by simp
    next
      case 3
      then show ?case
        using Side_Effect(2,3,5) Eval.prems(5) x_stabl_if_stabl1
          update_global_recorded_in_rho[OF Side_Effect(4)]
          update_global_untouched(1)[OF Side_Effect(4)]
        by (auto simp add: fun_upd_def le_supI1)
    qed

    have part_post_solution1: "part_post_solution_inv (state
         ⦇infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d'')⦈) (ρ ug_state1)"
      apply (intro destab_upd_globale_preserves_part_post_solution[OF Side_Effect(5)])
      subgoal
        apply (intro ballI)
        subgoal for u
          using Eval.prems(3,4) update_global_untouched(2)[OF Side_Effect(4), of u]
          by force
        done
      subgoal
        using Eval.prems(3) Side_Effect(4,5) update_global_preserves_rho_invariant(2)
          update_global_untouched(1)[OF Side_Effect(4)]
        by (auto simp add: le_fun_def fun_upd_def split: sum.splits)
      subgoal
        using Eval.prems(2) by simp
      done
    have x_in_c_state1: "x ∈ called state" using Eval.prems(4) Side_Effect(5) by simp

    note IH = Eval.IH(6)[OF Side_Effect(1-4) _ _ Side_Effect(5) _ Side_Effect(7) inv
        part_post_solution1, simplified, OF _ _ x_in_c_state1 prefix]

    have "∀x∈called state - {x}. (λg. rho_lookup (ρ ug_state) g x) = (λg. rho_lookup (ρ ug_state') g x)"
    proof -
      have "(λg. rho_lookup ((ρ ug_state)(y := fmupd x (rho_lookup (ρ ug_state) y x ∇Δ d')
        (ρ ug_state y))) g u) = (λg. rho_lookup (ρ ug_state) g u)" if "u ≠ x" for u
        using that by (auto simp add: fun_upd_apply fun_eq_iff fmlookup_default_def)
      then show ?thesis
        using IH update_global_untouched(2)[OF Side_Effect(4)] Side_Effect(5) by auto
    qed

    then show ?thesis using IH by auto
  next
    case Answer
    have "traverse_rhs (T x) (σ state') = xd" if "x ∈ stabl state'"
    proof -
      have "subt_for_prefix (T x) pre (σ state) = Some t"
        using Eval.prems(5) Answer(2) that by simp
      then have "traverse_rhs (T x) (σ state) = xd"
        using subt_for_prefix_Answer_eq_traverse Answer(1) by blast
      then show ?thesis using Answer(2) by simp
    qed
    moreover have "sides_of_rhs (T x) (σ state') ≤ case_sum (λx. ⊥)
      (λg. rho_lookup (ρ ug_state') g x)" if "x ∈ stabl state'"
    proof -
      have "subt_for_prefix (T x) pre (σ state) = Some (Answer xd)"
        using Eval.prems(5) Answer that by simp
      moreover have "∀(u, ud)∈{s. Inr s ∈ set pre}. ud ≤ rho_lookup (ρ ug_state') u x"
        using Eval.prems(3,5) that Answer(2,3) order.trans[of _ "sides⇩a⇩c⇩c _"]
        by blast
      ultimately show ?thesis
        using subt_for_prefix_Answer_rho_subsumes[where ?rho="ρ ug_state'"] Answer(2) by blast
    qed
    ultimately show ?thesis using Eval.prems(3,4) Answer(2,3) by (simp cong: sum.case_cong)
  qed
qed

theorem partial_post_solution:
  assumes "solve_dom x"
      and "solve x = (st, sigma)"
    shows "part_post_solution T x sigma st"
proof -
  obtain d state ug_state where iterate: "(d, state, ug_state) =
      iterate x (init_state ⦇ called := insert x (called init_state) ⦈) init_ug_state"
    and st: "st = stabl state" and sigma: "sigma = σ state"
    using assms(2) unfolding solve_def by (auto split: prod.splits)
  have c_empty: "called state = {}"
    using called_same(2)[OF assms(1)[unfolded solve_dom_def] iterate]
    unfolding init_state_def
    by simp
  have well_init: "TD_side.well_infl_stabl (init_state⦇called := called init_state - {x}⦈)"
    unfolding init_state_def TD_side.well_infl_stabl_def fmlookup_default_def
    by simp
  then have well_result_state: "TD_side.well_infl_stabl (state⦇called := called state - {x}⦈)"
    and x_stabl: "x ∈ stabl state"
    using well_infl_stabl_ind(2)[OF assms(1)[unfolded solve_dom_def] iterate]
    by auto
  moreover have "(∀x ∈ stabl state. eq T x (σ state) ≤ (σ state) (Inl x)
      ∧ sides_of_rhs (T x) (σ state) ≤ σ state)"
  proof -
    have "∀x∈stabl state. eq T x (σ state) ≤ σ state (Inl x) ∧
          sides_of_rhs (T x) (σ state) ≤ case_sum (λx. ⊥) (λg. rho_lookup (ρ ug_state) g x)"
        "case_sum (λx. ⊥) (λg. rho_lookup (ρ ug_state) g u) ≤ σ state" for u
      using partial_solution_ind(2)[OF assms(1)[unfolded solve_dom_def] iterate] c_empty well_init
        init_rho_leq_bot
      unfolding init_state_def
      by (auto simp add: le_fun_def split: sum.splits)
    then show ?thesis
      by (auto intro: order.trans[of _ "case_sum (λx. ⊥) (λg. rho_lookup (ρ ug_state) g _)"])
  qed
  moreover have "∀u ∈ stabl state. dep⇩L T (σ state) u ⊆ stabl state"
    using TD_side.well_infl_stabl_implies_stabl_c_closed[OF well_result_state] c_empty
    unfolding TD_side.well_infl_stabl_def dep⇩L_def
    by simp
  ultimately show ?thesis using x_stabl st sigma by simp
qed


subsection ‹Program Refinement for Code Generation›

text‹To derive executable code for the TD, we do a program refinement and define an
  equivalent solve function based on partial\_function with options that can be used for the code
  generation.›

datatype ('a,'b,'c :: "{bounded_semilattice_sup_bot,warrowing}",'u) func_state =
    Q "'a × 'a × ('a,'b,'c) state × ('a,'b,'c,'u) ug_state_scheme"
  | I "'a × ('a,'b,'c) state × ('a,'b,'c,'u) ug_state_scheme"
  | R "'a × ('a,'b,'c) state × ('a,'b,'c,'u) ug_state_scheme"
  | E "'a × ('a,'b,'c) strategy_tree × ('b ⇒ 'c) × ('a,'b,'c) state ×
      ('a,'b,'c,'u) ug_state_scheme"

partial_function (option) solve_rec_c ::
  "('x,'g,'d,'upd) func_state ⇒ ('d × ('x,'g,'d) state × ('x,'g,'d,'upd) ug_state_scheme) option"
  where
  "solve_rec_c s = (case s of Q (y,x,state,ug_state) ⇒ Option.bind (
      if x ∈ called state then
        Some ((σ state) (Inl x), state⦇ point := insert x (point state) ⦈, ug_state)
      else
        solve_rec_c (I (x, state⦇ called := insert x (called state) ⦈, ug_state)))
      (λ (xd, state, ug_state). Some (xd, state⦇infl := fminsert (infl state) (Inl x) y⦈, ug_state))
  | I (x,state,ug_state) ⇒
      if x ∉ stabl state then Option.bind (
        solve_rec_c (R (x, state, ug_state)))
        (λ(d_new, state1, ug_state1).
          let d_new = (if x ∈ point state then (σ state1) (Inl x) ∇Δ d_new else d_new) in
          if (σ state1) (Inl x) = d_new then
            Some (d_new, state1⦇ called := called state1 - {x}, point := (point state1) - {x}⦈, ug_state1)
          else
            let (infl1, stabl1) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1) in
            solve_rec_c (I (x, state1⦇ infl := infl1, stabl := stabl1,
              σ := (σ state1)(Inl x := d_new) ⦈, ug_state1)))
      else
        Some ((σ state) (Inl x), state⦇ called := called state - {x}, point := (point state) - {x}⦈, ug_state)
  | R (x, state, ug_state) ⇒ Option.bind (
      solve_rec_c (E (x, T x, (λ_. ⊥), state ⦇stabl := insert x (stabl state)⦈, ug_state)))
      (λ (xd, state, ug_state). if x ∈ stabl state then Some (xd, state, ug_state)
        else solve_rec_c (R (x, state, ug_state)))
  | E (x,t,sides⇩a⇩c⇩c,state,ug_state) ⇒ (case t of
        Answer d ⇒ Some (d, state, ug_state)
      | QueryL y g ⇒ (
          Option.bind (solve_rec_c (Q (x, y, state, ug_state))) (λ(yd, state, ug_state).
          solve_rec_c (E (x, g yd, sides⇩a⇩c⇩c, state, ug_state))))
      | QueryG y g ⇒ (
          solve_rec_c (E (x, g ((σ state) (Inr y)), sides⇩a⇩c⇩c,
            state⦇ infl := fminsert (infl state) (Inr y) x⦈, ug_state)))
      | Side y d t ⇒ (
          let d = sides⇩a⇩c⇩c y ⊔ d in
          let sides⇩a⇩c⇩c = sides⇩a⇩c⇩c(y := d) in
          let (upd,ug_state) = update_global (σ state (Inr y)) x y d ug_state in
          case upd of None ⇒ solve_rec_c (E (x, t, sides⇩a⇩c⇩c, state, ug_state))
          | Some d ⇒
            let (infl', stabl') = destab_opt (Inr y) (infl state) (stabl state) (called state) in
            solve_rec_c (E (x, t, sides⇩a⇩c⇩c, state⦇ infl := infl', stabl := stabl',
              σ := (σ state)(Inr y := d)⦈, ug_state)))
      ))"

definition solve_rec_c_dom where "solve_rec_c_dom p ≡ ∃σ. solve_rec_c p = Some σ"

declare solve_rec_c.simps[simp,code]

definition solve_c :: "'x ⇒ ('x set × (('x + 'g => 'd))) option" where
  "solve_c x = Option.bind (solve_rec_c
    (I (x, init_state⦇ called := insert x (called (init_state :: ('x,'g,'d) state)) ⦈, init_ug_state)))
    (λ(_, state, _). Some (stabl state, σ state))"

definition solve_c_dom :: "'x ⇒ bool" where
  "solve_c_dom x ≡ ∃r. solve_c x = Some r"

text‹We prove the equivalence of the refined solver function for code generation and the initial
  version used for the partial correctness proof.›

lemma query_iterate_eval_solve_rec_c_equiv:
  shows "query_dom x y state ug_state ⟹ solve_rec_c_dom (Q (x,y,state,ug_state))
    ∧ query x y state ug_state = the (solve_rec_c (Q (x,y,state,ug_state)))"
  and "iterate_dom x state ug_state ⟹ solve_rec_c_dom (I (x,state,ug_state))
    ∧ iterate x state ug_state = the (solve_rec_c (I (x,state,ug_state)))"
  and "repeat_dom x state ug_state ⟹ solve_rec_c_dom (R (x,state,ug_state))
    ∧ repeat x state ug_state = the (solve_rec_c (R (x,state,ug_state)))"
  and "eval_dom x t sides⇩a⇩c⇩c state ug_state ⟹ solve_rec_c_dom (E (x,t,sides⇩a⇩c⇩c,state,ug_state))
    ∧ eval x t sides⇩a⇩c⇩c state ug_state = the (solve_rec_c (E (x,t,sides⇩a⇩c⇩c,state,ug_state)))"
proof (induction x y state ug_state and x state ug_state and x state ug_state
      and x t sides⇩a⇩c⇩c state ug_state
    rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state ug_state)
  show ?case
  proof (cases "y ∈ called state")
    case True
    then have "solve_rec_c (Q (x, y, state, ug_state))
        = Some ((σ state) (Inl y), state⦇ point := insert y (point state),
          infl := fminsert (infl state) (Inl y) x ⦈, ug_state)"
      by simp
    moreover have "query x y state ug_state = ((σ state) (Inl y),
        state⦇ point := insert y (point state),
          infl := fminsert (infl state) (Inl y) x ⦈, ug_state)"
      using query.psimps[folded dom_defs] Query(1) True by force
    ultimately show ?thesis unfolding solve_rec_c_dom_def by auto
  next
    case False
    obtain d1 state1 ug_state1 where
        I: "iterate y (state⦇ called := insert y (called state) ⦈) ug_state = (d1, state1, ug_state1)"
      by (cases "iterate y (state⦇ called := insert y (called state) ⦈) ug_state") simp
    then have J: "query x y state ug_state =
        (d1, state1⦇ infl := fminsert (infl state1) (Inl y) x ⦈, ug_state1)"
      using False Query.IH(1) query.pelims[folded dom_defs] by fastforce
    then have "solve_rec_c (I (y, state⦇ called := insert y (called state) ⦈, ug_state)) =
        Some (d1, state1, ug_state1)"
      using Query(2) False I by (simp add: solve_rec_c_dom_def)
    then have "solve_rec_c (Q (x, y, state, ug_state)) =
        Some (d1, state1⦇ infl := fminsert (infl state1) (Inl y) x ⦈, ug_state1)"
      using False by simp
    moreover have "solve_rec_c_dom (Q (x, y, state, ug_state))"
      using Query(2) False unfolding solve_rec_c_dom_def by fastforce
    ultimately show ?thesis using Query J unfolding solve_rec_c_dom_def by auto
  qed
next
  case (Iterate x state ug_state)
  show ?case
  proof (cases "x ∈ stabl state")
    case True
    have "iterate_dom x state ug_state ∧ iterate x state ug_state = ((σ state) (Inl x),
        state⦇ called := called state - {x}, point := (point state) - {x}⦈, ug_state)"
      using True iterate.psimps query_iterate_repeat_eval.domintros(2)
      unfolding iterate_dom_def
      by fastforce
    then show ?thesis using True unfolding solve_rec_c_dom_def by simp
  next
    case False
    obtain d1 state1 ug_state1 where
        repeat: "repeat x state ug_state = (d1, state1, ug_state1)"
        "solve_rec_c (R (x, state, ug_state)) = Some (d1, state1, ug_state1)"
      using Iterate(2)[OF False, of "x ∈ point state"] unfolding solve_rec_c_dom_def by auto
    define d' where "d' = (if x ∈ point state then (σ state1) (Inl x) ∇Δ d1 else d1)"
    show ?thesis
    proof (cases "(σ state1) (Inl x) = d'")
      case True
      have "iterate x state ug_state =
          (d', state1⦇called := called state1 - {x}, point := point state1 - {x}⦈, ug_state1)"
        using repeat iterate.psimps[folded dom_defs, OF Iterate(1)] True False d'_def by simp
      moreover have "solve_rec_c (I (x, state, ug_state)) =
          Some (d', state1⦇called := called state1 - {x}, point := point state1 - {x}⦈, ug_state1)"
        using repeat False True d'_def
        apply (subst solve_rec_c.simps)
        by (simp del: solve_rec_c.simps)
      ultimately show ?thesis unfolding solve_rec_c_dom_def by simp
    next
      case False
      obtain infl2 stabl2 where
        destab: "(infl2, stabl2) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1)"
        by (cases "destab_opt (Inl x) (infl state1) (stabl state1) (called state1)") auto
      have "solve_rec_c_dom (I (x, state1⦇ infl := infl2, stabl := stabl2,
          σ := (σ state1)(Inl x := d') ⦈, ug_state1))"
        and "iterate x (state1⦇ infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := d') ⦈)
          ug_state1 =
          the (solve_rec_c (I (x, state1⦇ infl := infl2, stabl := stabl2,
          σ := (σ state1)(Inl x := d') ⦈, ug_state1)))"
        using Iterate(3)[OF ‹x ∉ stabl state› _ _ repeat(1)[symmetric] _ d'_def False destab]
        by blast+
      moreover have "iterate x state ug_state = iterate x (state1⦇ infl := infl2, stabl := stabl2,
          σ := (σ state1)(Inl x := d') ⦈) ug_state1"
        using repeat iterate.psimps[folded dom_defs, OF Iterate(1)] False ‹x ∉ stabl state› destab
          d'_def
        by (cases "destab_opt (Inl x) (infl state1) (stabl state1) (called state1)") simp
      moreover have "solve_rec_c (I (x, state, ug_state)) =
          solve_rec_c (I (x, state1⦇infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := d')⦈,
          ug_state1))"
        using ‹x ∉ stabl state› False repeat(2) destab[symmetric] d'_def
        apply (subst solve_rec_c.simps)
        by (auto simp del: solve_rec_c.simps split: prod.splits)
      ultimately show ?thesis unfolding solve_rec_c_dom_def by auto
    qed
  qed
next
  case (Repeat x state ug_state)
  obtain d1 state1 ug_state1 where
      eval: "eval x (T x) (λ_.⊥) (state ⦇ stabl := insert x (stabl state) ⦈) ug_state
        = (d1, state1, ug_state1)"
      "solve_rec_c (E (x, T x, λ_.⊥, state ⦇ stabl := insert x (stabl state) ⦈, ug_state))
        = Some (d1, state1, ug_state1)"
    using Repeat(2) unfolding solve_rec_c_dom_def by auto
  show ?case
  proof (cases "x ∈ stabl state1")
    case True
    then show ?thesis
      using True repeat.psimps[folded dom_defs, OF Repeat(1)] eval
      unfolding solve_rec_c_dom_def by simp
  next
    case False
    have "solve_rec_c_dom (R (x, state1, ug_state1))"
        "repeat x state1 ug_state1 = the (local.solve_rec_c (R (x, state1, ug_state1)))"
      using Repeat.IH(3)[OF eval(1)[symmetric] refl refl False] by auto
    then show ?thesis
      using False repeat.psimps[folded dom_defs, OF Repeat(1)] eval
      unfolding solve_rec_c_dom_def
      by simp
  qed
next
  case (Eval x t sides⇩a⇩c⇩c state ug_state)
  show ?case
  proof (cases t)
    case (Answer d)
    then have "eval x t sides⇩a⇩c⇩c state ug_state = (d, state, ug_state)"
      using eval.psimps query_iterate_repeat_eval.domintros(4) dom_defs(4) by fastforce
    then show ?thesis using Eval Answer unfolding solve_rec_c_dom_def by simp
  next
    case (QueryL y g)
    then obtain d1 state1 ug_state1 where
        query: "solve_rec_c (Q (x, y, state, ug_state)) = Some (d1, state1, ug_state1)"
          "query x y state ug_state = (d1, state1, ug_state1)"
      using QueryL Eval(2) unfolding solve_rec_c_dom_def by auto
    then have "solve_rec_c_dom (E (x, g d1, sides⇩a⇩c⇩c, state1, ug_state1))"
        "eval x (g d1) sides⇩a⇩c⇩c state1 ug_state1
          = the (solve_rec_c (E (x, g d1, sides⇩a⇩c⇩c, state1, ug_state1)))"
      using Eval(3)[OF QueryL] by auto
    moreover have "eval x t sides⇩a⇩c⇩c state ug_state = eval x (g d1) sides⇩a⇩c⇩c state1 ug_state1"
      using Eval.IH(1) QueryL eval.psimps query unfolding eval_dom_def
      by fastforce
    moreover have "solve_rec_c (E (x, t, sides⇩a⇩c⇩c, state, ug_state))
        = solve_rec_c (E (x, g d1, sides⇩a⇩c⇩c, state1, ug_state1))"
      using QueryL query solve_rec_c.simps[of "E (x,t,sides⇩a⇩c⇩c,state,ug_state)"]
      by (simp del: solve_rec_c.simps)
    ultimately show ?thesis unfolding solve_rec_c_dom_def by force
  next
    case (QueryG y g)
    have "solve_rec_c_dom (E (x, g ((σ state) (Inr y)), sides⇩a⇩c⇩c,
          state⦇infl := fminsert (infl state) (Inr y) x⦈, ug_state))"
        "eval x (g ((σ state) (Inr y))) sides⇩a⇩c⇩c (state⦇infl := fminsert (infl state) (Inr y) x⦈)
          ug_state = the (solve_rec_c (E (x, g ((σ state) (Inr y)), sides⇩a⇩c⇩c,
          state⦇infl := fminsert (infl state) (Inr y) x⦈, ug_state)))"
      using Eval(4)[OF QueryG] by auto
    moreover have "eval x t sides⇩a⇩c⇩c state ug_state = eval x (g ((σ state) (Inr y))) sides⇩a⇩c⇩c
        (state⦇infl := fminsert (infl state) (Inr y) x⦈) ug_state"
      using Eval.IH(1) QueryG eval.psimps unfolding eval_dom_def
      by fastforce
    moreover have "solve_rec_c (E (x, t, sides⇩a⇩c⇩c, state, ug_state)) = solve_rec_c (E (x,
        g ((σ state) (Inr y)), sides⇩a⇩c⇩c, state⦇infl := fminsert (infl state) (Inr y) x⦈, ug_state))"
      using QueryG solve_rec_c.simps[of "E (x,t,sides⇩a⇩c⇩c,state,ug_state)"]
      by (simp del: solve_rec_c.simps)
    ultimately show ?thesis unfolding solve_rec_c_dom_def by simp
  next
    case (Side y d t')
    let ?d = "sides⇩a⇩c⇩c y ⊔ d"
    let ?sides⇩a⇩c⇩c = "sides⇩a⇩c⇩c(y := ?d)"
    obtain upd ug_state1 where
      upd_global: "(upd, ug_state1) = update_global (σ state (Inr y)) x y ?d ug_state"
      by (cases "update_global (σ state (Inr y)) x y ?d ug_state") auto
    show ?thesis
    proof (cases upd)
      case None
      have "solve_rec_c_dom (E (x, t', ?sides⇩a⇩c⇩c, state, ug_state1))"
          "eval x t' ?sides⇩a⇩c⇩c state ug_state1
            = the (solve_rec_c (E (x, t', ?sides⇩a⇩c⇩c, state, ug_state1)))"
        using Eval(5)[OF Side _ _ upd_global _ None] by auto
      moreover have "eval x t sides⇩a⇩c⇩c state ug_state = eval x t' ?sides⇩a⇩c⇩c state ug_state1"
        using Eval.IH(1) Side None eval.psimps upd_global unfolding eval_dom_def
        by (auto simp add: Let_def split: prod.splits)
      moreover have "solve_rec_c (E (x, t, sides⇩a⇩c⇩c, state, ug_state)) =
          solve_rec_c (E (x, t', ?sides⇩a⇩c⇩c, state, ug_state1))"
        using Side solve_rec_c.simps[of "E (x,t,sides⇩a⇩c⇩c,state,ug_state)"] None upd_global
        by (auto simp add: Let_def simp del: solve_rec_c.simps split: option.splits prod.splits)
      ultimately show ?thesis using Side unfolding solve_rec_c_dom_def by simp
    next
      case (Some d')
      obtain infl1 stabl1 where
          destab: "(infl1, stabl1) = destab_opt (Inr y) (infl state) (stabl state) (called state)"
        by (cases "destab_opt (Inr y) (infl state) (stabl state) (called state)") simp
      let ?state' = "state ⦇ infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d') ⦈"
      have "solve_rec_c_dom (E (x, t', ?sides⇩a⇩c⇩c, ?state', ug_state1))"
          "eval x t' ?sides⇩a⇩c⇩c ?state' ug_state1 =
            the (solve_rec_c (E (x, t', ?sides⇩a⇩c⇩c, ?state', ug_state1)))"
        using Eval(6)[OF Side refl refl upd_global _ Some destab]
        by (auto simp del: solve_rec_c.simps)
      moreover have "eval x t sides⇩a⇩c⇩c state ug_state = eval x t' ?sides⇩a⇩c⇩c ?state' ug_state1"
        using Eval.IH(1) Side Some eval.psimps destab upd_global unfolding eval_dom_def
        by (auto simp add: Let_def split: option.splits prod.splits)
      moreover have
        "solve_rec_c (E (x, t, sides⇩a⇩c⇩c, state, ug_state)) =
          solve_rec_c (E (x, t', ?sides⇩a⇩c⇩c, ?state', ug_state1))"
        using Side solve_rec_c.simps[of "E (x,t,sides⇩a⇩c⇩c,state,ug_state)"] Some destab upd_global
        by (auto simp add: Let_def split: prod.split)
      ultimately show ?thesis using Side unfolding solve_rec_c_dom_def by simp
    qed
  qed
qed

lemma solve_rec_c_query_iterate_eval_equiv:
  shows "solve_rec_c s = Some r ⟹ (case s of
        Q (x,y,state,ug_state) ⇒ query_dom x y state ug_state ∧ query x y state ug_state = r
      | I (x,state,ug_state) ⇒ iterate_dom x state ug_state ∧ iterate x state ug_state = r
      | R (x,state,ug_state) ⇒ repeat_dom x state ug_state ∧ repeat x state ug_state = r
      | E (x,t,sides⇩a⇩c⇩c,state,ug_state) ⇒ eval_dom x t sides⇩a⇩c⇩c state ug_state ∧
          eval x t sides⇩a⇩c⇩c state ug_state = r)"
proof (induction arbitrary: s r rule: solve_rec_c.fixp_induct)
  case 1
  then show ?case
    by (smt (verit) ccpo.admissibleI chain_fun curry_def flat_lub_in_chain fun_lub_def
        mem_Collect_eq option.simps(3))
next
  case 2
  then show ?case by simp
next
  case (3 S)
  show ?case
  proof (cases s)
    case (Q a)
    obtain x y state ug_state where "a = (x, y, state, ug_state)" using prod_cases4 by blast
    have "query_dom x y state ug_state ∧ query x y state ug_state = r"
    proof (cases "y ∈ called state")
      case True
      then have "Some ((σ state) (Inl y), state ⦇ point := insert y (point state),
          infl := fminsert (infl state) (Inl y) x ⦈, ug_state) = Some r"
        using 3(2) Q ‹a = (x, y, state, ug_state)› by simp
      then show ?thesis using query.psimps[folded query_dom_def, of x y state]
            query_iterate_repeat_eval.domintros(1)[folded query_dom_def, of y state] True by simp
    next
      case False
      then have "Option.bind (S (I (y, state ⦇ called := insert y (called state) ⦈, ug_state)))
          (λ(d,state, ug_state). Some (d, state ⦇ infl := fminsert (infl state) (Inl y) x ⦈,
          ug_state)) = Some r"
        using 3(2) Q ‹a = (x, y, state, ug_state)› by simp
      then obtain d1 state1 ug_state1 where
        "S (I (y, state ⦇ called := insert y (called state) ⦈, ug_state)) = Some (d1, state1, ug_state1)"
        and "(d1, state1 ⦇ infl := fminsert (infl state1) (Inl y) x ⦈, ug_state1) = r"
        by (cases "S (I (y, state ⦇ called := insert y (called state) ⦈, ug_state))") auto
      then have "iterate_dom y (state ⦇ called := insert y (called state) ⦈) ug_state
          ∧ iterate y (state ⦇ called := insert y (called state) ⦈) ug_state = (d1, state1, ug_state1)"
        using 3(1) unfolding iterate_dom_def by fastforce
      then show ?thesis
        using False ‹(d1, state1 ⦇ infl := fminsert (infl state1) (Inl y) x ⦈, ug_state1) = r›
        by (simp add: query_iterate_repeat_eval.domintros(1) False)
    qed
    then show ?thesis using Q ‹a = (x, y, state, ug_state)› by simp
  next
    case (I a)
    obtain x state ug_state where "a = (x, state, ug_state)"
      using repeat.cases by blast
    show ?thesis
    proof(cases "x ∈ stabl state")
      case True
      then have "((σ state) (Inl x),
          state⦇called := called state - {x}, point := point state - {x}⦈, ug_state) = r"
        using I ‹a = (x, state, ug_state)› 3(2) by simp
      moreover have "iterate_dom x state ug_state ∧ iterate x state ug_state = ((σ state) (Inl x),
          state⦇called := called state - {x}, point := point state - {x}⦈, ug_state)"
        using True query_iterate_repeat_eval.domintros(2) iterate.psimps dom_defs by fastforce
      ultimately show ?thesis using I ‹a = (x, state, ug_state)› by simp
    next
      case False
      then have IH1: "Option.bind (S (R (x, state, ug_state)))
         (λ(d_new, state1, ug_state1).
           let d_new = if x ∈ point state then (σ state1) (Inl x) ∇Δ d_new else d_new in
           if (σ state1) (Inl x) = d_new then
            Some (d_new, state1⦇called := called state1 - {x}, point := point state1 - {x}⦈, ug_state1)
           else let (infl1, stabl1) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1) in
            S (I (x, state1⦇ infl := infl1, stabl := stabl1,
            σ := (σ state1)(Inl x := d_new) ⦈, ug_state1))) = Some r"
        using 3(2) I ‹a = (x, state, ug_state)› by simp
      then obtain d_new state1 ug_state1
        where repeat_some: "S (R (x, state, ug_state)) = Some (d_new, state1, ug_state1)"
        using 3(2) I
        by (cases "S (R (x, state, ug_state))") auto
      then have repeat: "repeat_dom x state ug_state
          ∧ repeat x state ug_state = (d_new, state1, ug_state1)"
        using 3(1) unfolding repeat_dom_def by force
      let ?d_new = "if x ∈ point state then (σ state1) (Inl x) ∇Δ d_new else d_new"
      have "iterate_dom x state ug_state ∧ iterate x state ug_state = r"
      proof (cases "(σ state1) (Inl x) = ?d_new")
        case True
        then have
          "(?d_new, state1⦇called := called state1 - {x}, point := point state1 - {x}⦈, ug_state1) = r"
          using IH1 repeat_some by simp
        moreover have "iterate_dom x state ug_state"
          using query_iterate_repeat_eval.domintros(2)[folded dom_defs] False True repeat
          by fastforce
        ultimately show ?thesis
          using iterate.psimps[folded dom_defs] False True repeat by fastforce
      next
        case False
        obtain infl2 stabl2 where
            destab: "(infl2, stabl2) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1)"
          by (cases "destab_opt (Inl x) (infl state1) (stabl state1) (called state1)") auto
        let ?state = "state1⦇ infl := infl2, stabl := stabl2, σ := (σ state1)(Inl x := ?d_new) ⦈"
        have "S (I (x, ?state, ug_state1)) = Some r"
          using IH1 False repeat_some destab
          by (cases "destab_opt (Inl x) (infl state1) (stabl state1) (called state1)") simp
        then have iter_cont: "iterate_dom x ?state ug_state1 ∧ iterate x ?state ug_state1 = r"
          using 3(1) unfolding iterate_dom_def by fastforce
        then have "iterate_dom x state ug_state"
          using query_iterate_repeat_eval.domintros(2)[folded dom_defs destab.simps, of x state]
            repeat ‹x ∉ stabl state› False destab
          by (cases "destab_opt (Inl x) (infl state1) (stabl state1) (called state1)") fastforce
        then show ?thesis
          using iterate.psimps[folded dom_defs, of x state] ‹x ∉ stabl state› destab repeat
            False iter_cont
          by (cases "destab_opt (Inl x) (infl state1) (stabl state1) (called state1)") auto
      qed
      then show ?thesis
        using I ‹a = (x, state, ug_state)› by simp
    qed
  next
    case (R a)
    obtain x state ug_state where "a = (x, state, ug_state)"
      using repeat.cases by blast
    then have IH1: "Option.bind
        (S (E (x, T x, λ_. ⊥, state⦇stabl := insert x (stabl state)⦈, ug_state)))
        (λa. case a of
             (xd, state, ug_state) ⇒
               if x ∈ stabl state then Some (xd, state, ug_state)
               else S (R (x, state, ug_state))) = Some r"
      using 3(2) R by simp
    then obtain d_new state1 ug_state1 where eval_some:
      "S (E (x, T x, λ_. ⊥, state⦇stabl := insert x (stabl state)⦈, ug_state)) =
        Some (d_new, state1, ug_state1)"
      using 3(2) R
      by (cases "S (E (x, T x, λ_. ⊥, state⦇stabl := insert x (stabl state)⦈, ug_state))") auto
    then have eval: "eval_dom x (T x) (λ_. ⊥) (state⦇stabl := insert x (stabl state)⦈) ug_state ∧
        eval x (T x) (λ_. ⊥) (state⦇stabl := insert x (stabl state)⦈) ug_state =
          (d_new, state1, ug_state1)"
      using 3(1) unfolding repeat_dom_def by force
    show ?thesis
    proof(cases "x ∈ stabl state1")
      case True
      then have "(d_new, state1, ug_state1) = r"
        using R ‹a = (x, state, ug_state)› 3(2) eval_some by simp
      moreover have "repeat_dom x state ug_state ∧
        repeat x state ug_state = (d_new, state1, ug_state1)"
        using True query_iterate_repeat_eval.domintros(3) repeat.psimps dom_defs eval
        by fastforce
      ultimately show ?thesis using R ‹a = (x, state, ug_state)› by simp
    next
      case False
      have "S (R (x, state1, ug_state1)) = Some r"
        using IH1 False eval_some by simp
      then have repeat_cont: "repeat_dom x state1 ug_state1 ∧ repeat x state1 ug_state1 = r"
        using 3(1) unfolding repeat_dom_def by fastforce
      then have "repeat_dom x state ug_state"
        apply (intro query_iterate_repeat_eval.domintros(3)[folded dom_defs, of x state])
        using eval False by simp+
      then show ?thesis
        using repeat.psimps[folded dom_defs, of x state] ‹x ∉ stabl state1› eval
          False repeat_cont R ‹a = (x, state, ug_state)›
        by simp
    qed
  next
    case (E a)
    obtain x t sides⇩a⇩c⇩c state ug_state where "a = (x, t, sides⇩a⇩c⇩c, state, ug_state)"
      using prod_cases5 by blast
    then have "s = E (x, t, sides⇩a⇩c⇩c, state, ug_state)" using E by auto
    have "eval_dom x t sides⇩a⇩c⇩c state ug_state ∧ eval x t sides⇩a⇩c⇩c state ug_state = r"
    proof (cases t)
      case (Answer d)
      then have "eval_dom x t sides⇩a⇩c⇩c state ug_state"
        unfolding eval_dom_def
        using query_iterate_repeat_eval.domintros(4)
        by fastforce
      moreover have "eval x t sides⇩a⇩c⇩c state ug_state = (d, state, ug_state)"
        using Answer eval.psimps[folded dom_defs, OF calculation] by auto
      moreover have "(d, state, ug_state) = r"
        using 3(2) ‹s = E (x, t, sides⇩a⇩c⇩c, state, ug_state)› Answer by simp
      ultimately show ?thesis by simp
    next
      case (QueryL y g)
      then have "Option.bind (S (Q (x, y, state, ug_state))) (λ(yd, state, ug_state).
          S (E (x, g yd, sides⇩a⇩c⇩c, state, ug_state))) = Some r"
        using ‹s = E (x, t, sides⇩a⇩c⇩c, state, ug_state)› 3(2) by simp
      then obtain yd state1 ug_state1
          where S1: "S (Q (x, y, state, ug_state)) = Some (yd, state1, ug_state1)"
          and S2: "S (E (x, g yd, sides⇩a⇩c⇩c, state1, ug_state1)) = Some r"
        by (cases "S (Q (x, y, state, ug_state))") auto
      then have "query_dom x y state ug_state
            ∧ query x y state ug_state = (yd, state1, ug_state1)"
          and "eval_dom x (g yd) sides⇩a⇩c⇩c state1 ug_state1
            ∧ eval x (g yd) sides⇩a⇩c⇩c state1 ug_state1 = r"
        using 3(1)[OF S1] 3(1)[OF S2] by force+
      then show ?thesis
        using query_iterate_repeat_eval.domintros(4)[of t x state] QueryL eval.psimps[of x t]
        unfolding dom_defs by fastforce
    next
      case (QueryG y g)
      then have E_cont: "S (E (x, g ((σ state) (Inr y)), sides⇩a⇩c⇩c,
          state⦇ infl := fminsert (infl state) (Inr y) x ⦈, ug_state)) = Some r"
        using ‹s = E (x, t, sides⇩a⇩c⇩c, state, ug_state)› 3(2) by simp
      have "eval_dom x (g ((σ state) (Inr y))) sides⇩a⇩c⇩c
          (state⦇ infl := fminsert (infl state) (Inr y) x ⦈) ug_state ∧
          eval x (g ((σ state) (Inr y))) sides⇩a⇩c⇩c
          (state⦇ infl := fminsert (infl state) (Inr y) x ⦈) ug_state = r"
        using 3(1)[OF E_cont] by simp
      then show ?thesis
        using query_iterate_repeat_eval.domintros(4)[of t x state] QueryG eval.psimps[of x t]
        unfolding dom_defs by fastforce
    next
      case (Side y d t')
      let ?d = "sides⇩a⇩c⇩c y ⊔ d"
      let ?sides⇩a⇩c⇩c = "sides⇩a⇩c⇩c(y := ?d)"
      obtain upd ug_state1 where
        upd_global: "(upd, ug_state1) = update_global (σ state (Inr y)) x y ?d ug_state"
        by (cases "update_global (σ state (Inr y)) x y ?d ug_state") fastforce
      show ?thesis
      proof (cases upd)
        case None
        then have E_cont: "S (E (x, t', ?sides⇩a⇩c⇩c, state, ug_state1)) = Some r"
          using ‹s = E (x, t, sides⇩a⇩c⇩c, state, ug_state)› 3(2) Side upd_global
          by (auto simp add: Let_def split: prod.splits option.splits)
        have "eval_dom x t' ?sides⇩a⇩c⇩c state ug_state1 ∧ eval x t' ?sides⇩a⇩c⇩c state ug_state1 = r"
          using 3(1)[OF E_cont] by simp
        then show ?thesis
          using query_iterate_repeat_eval.domintros(4)[of t x state ug_state sides⇩a⇩c⇩c] Side
            eval.psimps[of x t sides⇩a⇩c⇩c state] upd_global[simplified None]
          unfolding dom_defs
          by (cases "update_global (σ state (Inr y)) x y ?d ug_state") fastforce
      next
        case (Some d')
        obtain infl1 stabl1 where
          destab: "(infl1, stabl1) = destab_opt (Inr y) (infl state) (stabl state) (called state)"
          by (cases "destab_opt (Inr y) (infl state) (stabl state) (called state)") simp
        let ?state = "state⦇ infl := infl1, stabl := stabl1, σ := (σ state)(Inr y := d') ⦈"
        have E_cont: "S (E (x, t', ?sides⇩a⇩c⇩c, ?state, ug_state1)) = Some r"
          using ‹s = E (x, t, sides⇩a⇩c⇩c, state, ug_state)› 3(2) Side Some destab upd_global
          by (auto simp add: Let_def split: option.splits prod.splits)
        have "eval_dom x t' ?sides⇩a⇩c⇩c ?state ug_state1 ∧ eval x t' ?sides⇩a⇩c⇩c ?state ug_state1 = r"
          using 3(1)[OF E_cont] by simp
        then show ?thesis
          using query_iterate_repeat_eval.domintros(4)[of t x state ug_state sides⇩a⇩c⇩c] Side Some
            destab eval.psimps[of x _ sides⇩a⇩c⇩c state] upd_global
          unfolding dom_defs
          by (cases "update_global (σ state (Inr y)) x y ?d ug_state";
              cases "destab_opt (Inr y) (infl state) (stabl state) (called state)") fastforce
      qed
    qed
    then show ?thesis using E ‹a = (x, t, sides⇩a⇩c⇩c, state, ug_state)› by simp
  qed
qed

theorem term_equivalence: "solve_dom x ⟷ solve_c_dom x"
  using solve_rec_c_query_iterate_eval_equiv[of "I (x, init_state⦇ called :=
    insert x (called init_state) ⦈, init_ug_state)"] query_iterate_eval_solve_rec_c_equiv(2)[of x
    "init_state⦇ called := insert x (called init_state) ⦈" init_ug_state]
  unfolding solve_dom_def solve_c_dom_def solve_rec_c_dom_def solve_c_def init_state_def
  apply (cases "solve_rec_c (I (x, init_state⦇ called := insert x (called init_state) ⦈, init_ug_state))")
  by (auto simp add: init_state_def init_rho_leq_bot)

theorem value_equivalence:
  "solve_dom x ⟹ ∃stabl σ. solve_c x = Some (stabl, σ) ∧ solve x = (stabl, σ)"
proof goal_cases
  case 1
  then obtain r where "solve_rec_c (I
    (x, init_state ⦇ called := insert x (called init_state) ⦈, init_ug_state)) = Some r
    ∧ iterate x (init_state ⦇ called := insert x (called init_state) ⦈) init_ug_state = r"
    using query_iterate_eval_solve_rec_c_equiv(2)[OF 1[unfolded solve_dom_def]]
    unfolding solve_rec_c_dom_def solve_dom_def init_state_def
    by fastforce
  then show ?case
    unfolding solve_c_def solve_def init_state_def by (auto split: prod.split)
qed

text‹With the equivalence of the refined version and the initial version proven, we can specify a
  code equation.›

lemma solve_code_equation [code]:
  "solve x = (case solve_c x of Some r ⇒ r
  | None ⇒ Code.abort (STR ''Input not in domain'') (λ_. solve x))"
proof (cases "solve_dom x")
  case True
  then show ?thesis
    using value_equivalence unfolding solve_c_def solve_def by fastforce
next
  case False
  then have "solve_c x = None" using term_equivalence
    unfolding solve_c_dom_def by (simp split: option.splits) fast
  then show ?thesis by auto
qed

subsection ‹Consequences of Termination›

text ‹An executable run that returns a result lies in the solver domain, so the partial
  correctness theorem applies to it.›

lemma solve_dom_of_solve_c:
  assumes "solve_c x ≠ None"
  shows "solve_dom x"
  unfolding term_equivalence solve_c_dom_def using assms by (cases "solve_c x") auto

lemma part_post_solution_of_solve_c:
  assumes "solve_c x ≠ None"
  shows "part_post_solution T x (snd (solve x)) (fst (solve x))"
proof -
  from partial_post_solution[OF solve_dom_of_solve_c[OF assms], of "fst (solve x)" "snd (solve x)"]
  show ?thesis by simp
qed

text ‹A terminating solve returns a finite stable set. The stable set changes in three places:
  ‹repeat› inserts one unknown, and ‹iterate› and the side-effect case of ‹eval› replace
  it by a \<^const>‹destab_opt› result, which is a subset of its input.›

lemma finite_stabl_ind:
  shows "query_dom x y state ug_state
    ⟹ (xd, state', ug_state') = query x y state ug_state
    ⟹ finite (stabl state) ⟹ finite (stabl state')"
    and "iterate_dom x state ug_state
    ⟹ (xd, state', ug_state') = iterate x state ug_state
    ⟹ finite (stabl state) ⟹ finite (stabl state')"
    and "repeat_dom x state ug_state
    ⟹ (xd, state', ug_state') = repeat x state ug_state
    ⟹ finite (stabl state) ⟹ finite (stabl state')"
    and "eval_dom x t sides⇩a⇩c⇩c state ug_state
    ⟹ (xd, state', ug_state') = eval x t sides⇩a⇩c⇩c state ug_state
    ⟹ finite (stabl state) ⟹ finite (stabl state')"
proof (induction x y state ug_state and x state ug_state and x state ug_state
        and x t sides⇩a⇩c⇩c state ug_state
      arbitrary: xd state' ug_state' and xd state' ug_state' and xd state' ug_state'
        and xd state' ug_state'
      rule: query_iterate_repeat_eval_pinduct)
  case (Query x y state ug_state)
  then show ?case
    by (auto simp: query.psimps[OF Query(1)[unfolded query_dom_def]]
        split: if_splits prod.splits)
next
  case (Iterate x state ug_state)
  then show ?case
    by (auto simp: iterate.psimps[OF Iterate(1)[unfolded iterate_dom_def]] Let_def
        split: if_splits prod.splits dest: destab_opt_stabl_finite)
next
  case (Repeat x state ug_state)
  then show ?case
    by (auto simp: repeat.psimps[OF Repeat(1)[unfolded repeat_dom_def]] Let_def
        split: if_splits prod.splits)
next
  case (Eval x t sides⇩a⇩c⇩c state ug_state)
  text ‹‹Side› is the one shape whose recursive call moves to a destabilized
    state, so its induction hypothesis wants finiteness of a set ‹auto› has not
    yet related to ‹stabl state›. Supplying that link with this case's own
    finiteness already discharged keeps it a one-premise ‹dest› rule, which
    leaves the ‹destab_opt› equation in place for the hypothesis itself.›
  from Eval have fin: "finite (stabl state)" by blast
  have fin_destab: "⋀y i' s'.
      destab_opt y (infl state) (stabl state) (called state) = (i', s') ⟹ finite s'"
    using fin destab_opt_stabl_finite by blast
  from Eval fin_destab show ?case
    by (auto simp: eval.psimps[OF Eval(1)[unfolded eval_dom_def]] Let_def
        split: if_splits prod.splits option.splits strategy_tree.splits)
qed

lemma finite_stabl_solve:
  assumes "solve_dom x"
  shows "finite (fst (solve x))"
proof -
  obtain d state ug_state where iterate: "(d, state, ug_state) =
      iterate x (init_state ⦇ called := insert x (called init_state) ⦈) init_ug_state"
    by (cases "iterate x (init_state ⦇ called := insert x (called init_state) ⦈) init_ug_state")
      auto
  have "fst (solve x) = stabl state"
    using iterate unfolding solve_def by (auto split: prod.splits)
  moreover have "finite (stabl state)"
    using finite_stabl_ind(2)[OF assms[unfolded solve_dom_def] iterate]
    unfolding init_state_def by simp
  ultimately show ?thesis by simp
qed


end ―‹end of locale TD_side_upd_rule›

text‹Finally, we interpret the locale TD_side_upd_rule with each of the five update rules presented.
  The resulting instantiated definitions are then passed to the code generator and thus exported to
  Standard ML.›

global_interpretation TD_side_always_join_Interp:
  TD_side_upd_rule init_basic_ug_state update_global_always_join T for T
  defines TD_side_always_join_Interp_solve = TD_side_always_join_Interp.solve
  and TD_side_always_join_Interp_solve_c = TD_side_always_join_Interp.solve_c
  and TD_side_always_join_Interp_solve_rec_c = TD_side_always_join_Interp.solve_rec_c
  by (simp add: TD_side_upd_rule.intro always_join.update_rule_axioms)

global_interpretation TD_side_per_origin_Interp:
  TD_side_upd_rule init_basic_ug_state update_global_per_origin T for T
  defines TD_side_per_origin_Interp_solve = TD_side_per_origin_Interp.solve
  and TD_side_per_origin_Interp_solve_c = TD_side_per_origin_Interp.solve_c
  and TD_side_per_origin_Interp_solve_rec_c = TD_side_per_origin_Interp.solve_rec_c
  by (simp add: TD_side_upd_rule.intro per_origin.update_rule_axioms)

global_interpretation TD_side_warrowing_apinis_Interp:
  TD_side_upd_rule init_basic_ug_state update_global_warrowing_apinis T for T
  defines TD_side_warrowing_apinis_Interp_solve = TD_side_warrowing_apinis_Interp.solve
  and TD_side_warrowing_apinis_Interp_solve_c = TD_side_warrowing_apinis_Interp.solve_c
  and TD_side_warrowing_apinis_Interp_solve_rec_c = TD_side_warrowing_apinis_Interp.solve_rec_c
  by (simp add: TD_side_upd_rule.intro warrowing_apinis.update_rule_axioms)

global_interpretation TD_side_warrowing_per_origin_Interp:
  TD_side_upd_rule init_basic_ug_state update_global_warrowing_per_origin T for T
  defines TD_side_warrowing_per_origin_Interp_solve = TD_side_warrowing_per_origin_Interp.solve
  and TD_side_warrowing_per_origin_Interp_solve_c = TD_side_warrowing_per_origin_Interp.solve_c
  and TD_side_warrowing_per_origin_Interp_solve_rec_c =
    TD_side_warrowing_per_origin_Interp.solve_rec_c
  by (simp add: TD_side_upd_rule.intro warrowing_per_origin.update_rule_axioms)

global_interpretation TD_side_bounded_narrowing_Interp:
  TD_side_upd_rule init_ug_state_with_gas "update_global_bounded_narrowing x" T for x T
  defines TD_side_bounded_narrowing_Interp_solve = TD_side_bounded_narrowing_Interp.solve
  and TD_side_bounded_narrowing_Interp_solve_c = TD_side_bounded_narrowing_Interp.solve_c
  and TD_side_bounded_narrowing_Interp_solve_rec_c = TD_side_bounded_narrowing_Interp.solve_rec_c
  by (simp add: TD_side_upd_rule.intro bounded_narrowing.update_rule_axioms)

end ―‹end of theory TD_side_upd_rule›