Theory AutoCorres2.Reaches

(*
 * Copyright (c) 2024 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory Reaches
  imports Spec_Monad
begin


text ‹The core notions on spec monads are
▪ Properties of a monad: \<^const>‹runs_to›, \<^const>‹runs_to_partial›
▪ Refinement / Simulation of monads: \<^const>‹refines›, \<^const>‹rel_spec› and \<^const>‹rel_spec_monad›.

It is considered good style to use these more abstract concepts as much as possible.

Next we introduce some notions that are more in a 'pointwise' spirit in the sense that they talk about a 
particular outcome of a monadic computation, e.g. that a particular state is a reachable outcome
of a monadic computation.

There is nothing ∗‹wrong› with these notions but we consider them as less elegant and more
'brute force'. So we encourage to think twice before using them and prefer the more abstract
notions.
›

primrec outcomes :: "'a post_state ⇒ 'a set" where
  "outcomes Failure = {}"
| "outcomes (Success X) = X"

lemma le_post_state_iff:
  "p ≤ q ⟷ (q ≠ Failure ⟶ (p ≠ Failure ∧ outcomes p ⊆ outcomes q))"
  by (cases q; cases p) simp_all

lemma outcomes_map[simp]: "outcomes (map_post_state f x) = f ` outcomes x"
  by (cases x) simp_all

lemma map_post_state_eq_Failure[simp]:
  "map_post_state f x = Failure ⟷ x = Failure"
  by (cases x; simp)

lemma outcomes_Sup[simp]: "Failure ∉ F ⟹ outcomes (Sup F) = (⋃f∈F. outcomes f)"
  by (auto simp: Sup_post_state_def)
    (metis outcomes.simps(2) post_state.exhaust vimage_eq)


(* TODO: remove: *)
lemmas runs_to_holds_def = runs_to.rep_eq
lemmas runs_to_partial_holds_partial_def = runs_to_partial.rep_eq
(* END TODO *)

section ‹‹succeeds› and ‹reaches››

definition succeeds :: "('e::default, 'a, 's) spec_monad ⇒ 's ⇒ bool" where
  "succeeds f s ⟷ run f s ≠ ⊤"

definition reaches :: "('e::default, 'a, 's) spec_monad ⇒ 's ⇒ ('e, 'a) exception_or_result ⇒ 's ⇒ bool" where
  "reaches f s r' s' ⟷ (r', s') ∈ outcomes (run f s)"

text ‹There seems to a similarity between what happens in HOL with the dualism of sets as type vs. the
characterisation as predicate as expressed in \<^const>‹Collect›. Similar \<^typ>‹'a post_state› has a
set in the \<^const>‹Success› case. In particular with \<^const>‹holds_post_state› we switch to the predicate view.
Which is then continued in \<^const>‹runs_to› which is the predicate view and the set view with \<^const>‹reaches›,
which is more the element wise set view similar to \<^term>‹x ∈ X› and finally culminates in
 @{thm spec_monad_eq_iff}. The predicate view seems to be the one we finally
aim for. So maybe we could get completely rid of the set like things and start of with a
predicate already in \<^typ>‹'a post_state›?›

lemma runs_to_partial_def_old:
  "runs_to_partial f s Q ⟷ (succeeds f s ⟶ (∀r t. reaches f s r t ⟶ Q r t))"
  unfolding succeeds_def reaches_def runs_to_partial.rep_eq
  by (cases "run f s") (auto simp: top_post_state_def)

lemma runs_to_def_old: "runs_to f s Q ⟷ succeeds f s ∧ (∀r t. reaches f s r t ⟶ Q r t)"
  unfolding succeeds_def reaches_def runs_to.rep_eq
  by (cases "run f s") (auto simp: top_post_state_def)

lemma runs_to_succeeds_runsto_partial_conv:
  "runs_to f s Q ⟷ (succeeds f s ∧ runs_to_partial f s Q)"
  by (auto simp add: runs_to_def_old runs_to_partial_def_old)

lemma run_Success_succeeds: "run f s = Success x ⟹ succeeds f s"
  by (auto simp add: succeeds_def top_post_state_def)

lemma runs_to_partial_le_outcomes_conv:
  "runs_to_partial f s Q ⟷ (outcomes (run f s)) ≤ {(r,t). Q r t}"
  apply (simp add: runs_to_partial_def_old succeeds_def outcomes_def reaches_def top_post_state_def)
  apply transfer
  apply standard
  subgoal
    by (auto split: post_state.splits)
  subgoal
    by blast
  done

lemma not_succeeds_empty_outcomes: "¬ succeeds f s ⟹ outcomes (run f s) = {}"
  by (simp add: succeeds_def top_post_state_def)

lemma reaches_succeeds: "reaches f s r t ⟹ succeeds f s"
  apply (simp add: reaches_def succeeds_def top_post_state_def)
  apply transfer
  apply auto
  done

lemma always_progress_succeeds_reaches_conv:
  "always_progress f ⟷ (∀s. succeeds f s ⟶ (∃r t. reaches f s r t))"
  apply (simp add: always_progress_def succeeds_def reaches_def)
  apply transfer
  apply (clarsimp simp add: top_post_state_def bot_post_state_def, safe)
   apply (metis ex_in_conv outcomes.simps(2) post_state.exhaust surj_pair)
  by (metis empty_iff post_state.distinct(1) outcomes.simps(2))

lemma le_succeedsD: "g ≤ f ⟹ succeeds f s ⟹ succeeds g s"
  apply (simp add: succeeds_def)
  apply transfer
  by (auto simp add: le_fun_def less_eq_post_state.simps top_post_state_def)

lemma outcomes_succeeds_run_conv: "outcomes (run f s) = X ⟹ succeeds f s ⟹ run f s = Success X"
  by (cases "run f s") (auto simp add: succeeds_def top_post_state_def)

lemma succeeds_outcomes_run_eqI: "succeeds f s ⟷ succeeds g s ⟹
       (succeeds f s ⟹ succeeds g s ⟹ (outcomes (run f s) = outcomes (run g s))) ⟹
       run f s = run g s"
  by (cases "run f s"; cases "run g s") (auto simp add: succeeds_def top_post_state_def)

lemma succeeds_outcomes_spec_monad_eqI:
"(⋀s. succeeds f s ⟷ succeeds g s) ⟹
 (⋀s. succeeds f s ⟹ succeeds g s ⟹ (outcomes (run f s) = outcomes (run g s))) ⟹
 f = g"
  apply (rule spec_monad_ext)
  apply (auto intro: succeeds_outcomes_run_eqI)
  done

lemma succeeds_reaches_spec_monad_eqI:
"(⋀s. succeeds f s ⟷ succeeds g s) ⟹
 (⋀s r t. succeeds f s ⟹ succeeds g s ⟹ (reaches f s r t ⟷ reaches g s r t)) ⟹
 f = g"
  apply (rule succeeds_outcomes_spec_monad_eqI)
   apply simp
  apply (auto simp add: reaches_def)
  done

lemma succeeds_runs_to_iff: "succeeds f s ⟷ runs_to f s (λ_ _. True)"
  by (simp add: runs_to_def_old)

named_theorems outcomes_spec_monad "Simplification rules for outcomes of Spec monad"

subsection ‹Relational rewriting for Monads›

lemma refines_def_old:
  "refines f g s t R ⟷
    (succeeds g t ⟶ succeeds f s ∧
      (∀r s'. reaches f s r s' ⟶ (∃x t'. reaches g t x t' ∧ R (r, s') (x, t'))))"
  by (cases "run g t"; cases "run f s")
     (force simp: refines.rep_eq succeeds_def reaches_def top_post_state_def)+

lemma rel_specI:
  assumes "succeeds f s ⟷ succeeds g t"
  assumes "⋀r s'. reaches f s r s' ⟹ ∃q t'. reaches g t q t' ∧ R (r, s') (q, t')"
  assumes "⋀q t'. reaches g t q t' ⟹ ∃r s'. reaches f s r s' ∧ R (r, s') (q, t')"
  shows "rel_spec f g s t R"
  using assms
  by (cases "run f s"; cases "run g t";
      fastforce simp: rel_spec_def rel_prod.simps rel_set_def
      reaches_def succeeds_def top_post_state_def)

lemma rel_specD_succeeds:
  "rel_spec f g s t R ⟹ succeeds f s ⟷ succeeds g t"
  by (cases "run f s"; cases "run g t";
      simp add: rel_post_state.simps rel_spec_def rel_prod.simps succeeds_def top_post_state_def)

lemma rel_specD_reaches1:
  "rel_spec f g s t R ⟹ reaches f s r s' ⟹ ∃q t'. reaches g t q t' ∧ R (r, s') (q, t')"
  by (cases "run f s"; cases "run g t";
      fastforce simp: rel_post_state.simps rel_spec_def rel_prod.simps rel_set_def
      reaches_def top_post_state_def)

lemma rel_specD_reaches2:
  "rel_spec f g s t R ⟹ reaches g t q t' ⟹ ∃r s'. reaches f s r s' ∧ R (r, s') (q, t')"
  by (cases "run f s"; cases "run g t";
      fastforce simp: rel_post_state.simps rel_spec_def rel_prod.simps rel_set_def
      reaches_def top_post_state_def)

lemma refines_iff:
  "refines f g s t R ⟷
    ((succeeds g t ⟶ succeeds f s) ∧
    (succeeds g t ⟶ succeeds f s ⟶
       (∀r s'. reaches f s r s' ⟶ (∃q t'. reaches g t q t' ∧ R (r, s') (q, t')))))"
  by (simp add: refines_def_old) blast

lemma refinesI:
  assumes "succeeds g t ⟹ succeeds f s"
  assumes "⋀r s'. succeeds g t ⟹ succeeds f s ⟹ reaches f s r s' ⟹
    (∃q t'. reaches g t q t' ∧ R (r, s') (q, t'))"
  shows "refines f g s t R"
  using assms
  by (auto simp add: refines_def_old)

lemma refinesD_succeeds:
  "refines f g s t R ⟹ succeeds g t ⟹ succeeds f s"
  by (auto simp: refines_def_old)

lemma refinesD_reaches:
  "refines f g s t R ⟹ reaches f s r s' ⟹ succeeds g t
    ⟹ ∃q t'. reaches g t q t' ∧ R (r, s') (q, t')"
  by (fastforce simp: refines_def_old )

lemma refines_strengthen':
  assumes "refines f g s t R"
  assumes "⋀r u q v. reaches f s r u ⟹ reaches g t q v ⟹ succeeds f s ⟹ succeeds g t
   ⟹ R (r, u) (q, v) ⟹ Q (r, u) (q, v)"
  shows "refines f g s t Q"
  using assms by (fastforce simp: refines_def_old)

lemma always_progressD: "always_progress f ⟹ succeeds f s ⟹ ∃r t. reaches f s r t"
  by (auto simp:always_progress_succeeds_reaches_conv)

lemma Ex_reaches: "f ∙ s ⦃ P ⦄ ⟹ always_progress f ⟹ ∃r t. reaches f s r t"
  by (auto simp: runs_to_def_old always_progress_succeeds_reaches_conv)

lemma witness_outcomes_succeeds: "x ∈ outcomes (run f s) ⟹ succeeds f s"
  using not_succeeds_empty_outcomes by fastforce

lemma runs_toD2: "f ∙ s ⦃ P ⦄ ⟹ reaches f s r t ⟹ P r t"
  by (simp add: runs_to_def_old)

lemma runs_toD2_res: fixes f:: "('a, 's) res_monad"
  shows "f ∙ s ⦃λRes r. P r ⦄ ⟹ reaches f s (Result r) t ⟹ P r t"
  by (simp add: runs_to_def_old)

lemma rel_post_state_runI:
  assumes "succeeds f s ⟷ succeeds g t"
  assumes "succeeds f s ⟹ succeeds g t ⟹ rel_set R (outcomes (run f s)) (outcomes (run g t))"
  shows "rel_post_state R (run f s) (run g t)"
  using assms
  by (cases "run f s"; cases "run g t") 
     (auto simp add: rel_post_state.simps succeeds_def top_post_state_def)

lemma rel_post_state_runI':
  assumes "succeeds f s ⟷ succeeds g t"
  assumes "succeeds f s ⟹ succeeds g t ⟹ rel_post_state R (run f s) (run g t)"
  shows "rel_post_state R (run f s) (run g t)"
  using assms
  by (auto simp add: rel_post_state.simps succeeds_def top_post_state_def)

lemma rel_post_state_runD:
  assumes "rel_post_state R (run f s) (run g t)"
  shows "(succeeds f s ⟷ succeeds g t) ∧
         (succeeds f s ⟶ succeeds g t ⟶ rel_set R (outcomes (run f s)) (outcomes (run g t)))"
  using assms
  by (auto simp add: rel_post_state.simps succeeds_def top_post_state_def)

lemma rel_post_state_run_iff:
  "rel_post_state R (run f s) (run g t) ⟷
    ((succeeds f s ⟷ succeeds g t) ∧
     (succeeds f s ⟶ succeeds g t ⟶ rel_set R (outcomes (run f s)) (outcomes (run g t))))"
  using rel_post_state_runI rel_post_state_runD by metis

lemma rel_spec_monad_succeeds_iff: "rel_spec_monad R Q f g ⟹ R s t ⟹ succeeds f s ⟷ succeeds g t"
  by (meson rel_specD_succeeds rel_spec_monad_iff_rel_spec)

lemma outcomes_top_ps[simp]: "outcomes ⊤ = {}" "outcomes (pure_post_state x) = {x}"
"outcomes ⊥ = {}"
  by (auto simp: top_post_state_def pure_post_state_def bot_post_state_def)

subsection "\<^const>‹top›"

lemma outcomes_top[outcomes_spec_monad]: "outcomes (run ⊤ s) = {}"
  by transfer (simp add: top_spec_monad_def top_post_state_def)

lemma succeeds_top[simp]: "succeeds ⊤ s ⟷ False"
  unfolding succeeds_def
  by transfer (simp add: top_spec_monad_def top_post_state_def)

lemma reaches_top[simp]: "reaches ⊤ s r t ⟷ False"
  unfolding reaches_def
  by (simp add: outcomes_top top_post_state_def)

subsection ‹\<^const>‹bot››

lemma outcomes_bot[outcomes_spec_monad]: "outcomes (run ⊥ s) = {}"
  by transfer (simp add: bot_spec_monad_def bot_post_state_def)

lemma succeeds_bot[simp]: "succeeds ⊥ s ⟷ True"
  unfolding succeeds_def
  by transfer (simp add: bot_spec_monad_def bot_post_state_def top_post_state_def)

lemma reaches_bot[simp]: "reaches ⊥ s r t ⟷ False"
  unfolding reaches_def
  by (simp add: outcomes_bot bot_post_state_def)

subsection "\<^const>‹fail›"

lemma outcomes_fail[outcomes_spec_monad]: "outcomes (run fail s) = {}"
  by transfer simp

lemma succeeds_fail_iff[iff]: "¬ (succeeds fail f)"
  by (simp add: succeeds_def)

lemma reaches_fail_iff[iff]: "¬ reaches fail s r t"
  by (simp add: reaches_def outcomes_spec_monad top_post_state_def)


subsection "\<^const>‹yield›"

lemma succeeds_yield[simp]: "succeeds (yield r) s"
  unfolding succeeds_def
  apply transfer
  apply (simp add: pure_post_state_def top_post_state_def)
  done

lemma outcomes_yield [outcomes_spec_monad]: "outcomes (run (yield r) s) = {(r, s)}"
  by (simp add: pure_post_state_def)

lemma reaches_yield[simp]: "reaches (yield v) s r t ⟷ (r = v ∧ (t = s))"
  by (simp add: reaches_def outcomes_spec_monad pure_post_state_def)


subsection "\<^const>‹return›"

lemma outcomes_return [outcomes_spec_monad]:
  "outcomes (run (return v) s) = {(Result v, s)}"
  by transfer (simp add: pure_post_state_def)

lemma succeeds_return [iff]: "succeeds (return v) s"
  by (simp add: succeeds_def top_post_state_def)

lemma reaches_return[simp]: "reaches (return v) s r t ⟷ (r = Result v ∧ (t = s))"
  by (simp add: reaches_def outcomes_spec_monad pure_post_state_def)

lemma refines_yield_left:
  "refines (yield x) f s t R"
  if "succeeds f t ⟹ reaches f t x' s' ∧ R (x, s) (x', s')"
  using that
  unfolding refines_def_old
  by (auto simp: succeeds_def top_post_state_def intro!: bexI[where x="(x', s')"])

subsection "\<^const>‹skip›"

lemma outcomes_skip [outcomes_spec_monad]:
  "outcomes (run (skip) s) = {(Result (), s)}"
  by (simp add: outcomes_spec_monad pure_post_state_def)

lemma succeeds_skip: "succeeds skip s"
  by simp

lemma reaches_skip: "reaches (return v) s r t ⟷ (r = Result () ∧ (t = s))"
  by (simp add: reaches_def outcomes_spec_monad pure_post_state_def)

lemma runs_to_skip[runs_to_vcg]: "skip ∙ s ⦃ λ_ t. t = s ⦄"
  by simp

lemma runs_to_partial_skip[runs_to_vcg]: "skip ∙ s ?⦃ λ_ t. t = s ⦄"
  by simp

lemma runs_to_skip_iff[runs_to_iff]: "skip ∙ s ⦃Q⦄ ⟷ Q (Result ()) s"
  by (simp add: runs_to_def_old)


subsection ‹\<^const>‹throw_exception_or_result››

lemma outcomes_throw_exception_or_result [outcomes_spec_monad]:
  "outcomes (run (throw_exception_or_result x) s) = {(Exception x, s)}"
  by transfer (simp add: pure_post_state_def)

lemma succeeds_throw_exception_or_result [iff]: "succeeds (throw_exception_or_result v) s"
  by (simp add: succeeds_def top_post_state_def)

lemma reaches_throw_exception_or_result[simp]:
  "reaches (throw_exception_or_result x) s r t ⟷ (r = Exception x ∧ (t = s))"
  by (simp add: reaches_def outcomes_spec_monad pure_post_state_def)

subsection ‹\<^const>‹throw››

lemma outcomes_throw [outcomes_spec_monad]:
  "outcomes (run (throw e) s) = {(Exn e, s)}"
  by (simp add: pure_post_state_def)

subsection ‹\<^const>‹get_state››

lemma outcomes_get_state [outcomes_spec_monad]:
  "outcomes (run get_state s) = {(Result s, s)}"
  by transfer (simp add: pure_post_state_def)

lemma succeeds_get_state [iff]: "succeeds get_state s"
  by (simp add: succeeds_def)

lemma reaches_get_state[simp]:
  "reaches get_state s r t ⟷ (r = Result s ∧ (t = s))"
  by (simp add: reaches_def outcomes_spec_monad pure_post_state_def)

subsection ‹\<^const>‹set_state››

lemma outcomes_set_state [outcomes_spec_monad]:
  "outcomes (run (set_state t) s) = {(Result (), t)}"
  by transfer (simp add: pure_post_state_def)

lemma succeeds_set_state [iff]: "succeeds (set_state t) s"
  by (simp add: succeeds_def)

lemma reaches_set_state[simp]: "reaches (set_state s') s r t ⟷ (r = Result () ∧ (t = s'))"
  by (simp add: reaches_def outcomes_spec_monad pure_post_state_def)

subsection ‹\<^const>‹select››

lemma succeeds_holds: "succeeds f s ⟷ holds_post_state (λx. True) (run f s)"
  by (cases "run f s") (simp_all add: succeeds_def top_post_state_def)

lemma succeeds_select[simp]: "succeeds (select S) s"
  apply (simp add:  succeeds_holds select_def)
  apply transfer
  apply (auto simp add: pure_post_state_def)
  done

lemma select_outcomes[outcomes_spec_monad]: "outcomes (run (select S) s) = (λv. (Result v, s)) ` S"
  apply (simp add: select_def)
  apply transfer
  apply (force simp add: pure_post_state_def outcomes_def Inf_set_def Sup_post_state_def
      split: post_state.splits prod.splits)
  done

lemma reaches_select [simp]: "reaches (select S) s r t ⟷ (r ∈ Result ` S ∧ t = s)"
  apply (auto simp add: reaches_def outcomes_spec_monad)
  done


subsection ‹\<^const>‹unknown››

lemma succeeds_unknown[simp]: "succeeds unknown s"
  unfolding unknown_def by simp

lemma unknown_outcomes[outcomes_spec_monad]: "outcomes (run unknown s) = (λv. (Result v, s)) ` UNIV"
  by simp

lemma reaches_unknown [simp]: "reaches unknown s r t ⟷ (r ∈ Result ` UNIV ∧ t = s)"
  unfolding unknown_def by simp


subsection ‹\<^const>‹lift_state››

lemma succeeds_lift_state_iff: "succeeds (lift_state R f) s ⟷ (∀s'. R s s' ⟶ succeeds f s')"
  by (simp add: succeeds_holds lift_state_def Spec_inverse)


subsection ‹const‹exec_concrete››

lemma succeeds_exec_concrete_iff: "succeeds (exec_concrete st f) s ⟷ (∀t. s = st t ⟶ succeeds f t)"
  by (simp add: exec_concrete_def succeeds_lift_state_iff)

lemma reaches_exec_concrete:
  assumes succeeds: "succeeds (exec_concrete st f) s"
  shows "reaches (exec_concrete st f) s r s' ⟷ (∃t t'. s = st t ∧ reaches f t r t' ∧ s' = st t')"
  apply (simp add: reaches_def run_exec_concrete)
  apply standard
  subgoal
    by (auto simp add: map_post_state_def Sup_post_state_def image_def vimage_def
        split: prod.splits post_state.splits if_split_asm)
      (metis outcomes.simps(2))
  subgoal
    using succeeds
    apply (simp add: succeeds_def run_exec_concrete)
    by (auto simp add: map_post_state_def Sup_post_state_def image_def vimage_def top_post_state_def
        split: prod.splits post_state.splits if_split_asm)
      (metis apsnd_conv outcomes.simps(2) post_state.exhaust)
  done


subsection ‹const‹exec_abstract››

lemma succeeds_exec_abstract_iff[simp]: "succeeds (exec_abstract st f) s ⟷ succeeds f (st s)"
  by (simp add: exec_abstract_def succeeds_lift_state_iff)

lemma reaches_exec_abstract:
  shows "reaches (exec_abstract st f) s r s' ⟷ (∃t'. reaches f (st s) r t' ∧ t' = st s')"
  by (cases "run f (st s)") (simp_all add: reaches_def run_exec_abstract)

subsection ‹\<^const>‹bind_handle››


lemma succeeds_bind_handle:
  "succeeds (bind_handle f g h) s ⟷
     (succeeds f s ∧
       (∀x s'. reaches f s x s' ⟶
         (case x of Exception e ⇒ succeeds (h e) s' | Result v ⇒ succeeds (g v) s')))"
  apply (cases "run f s")
  apply (simp_all add:
      succeeds_def run_bind_handle bot_post_state_def top_post_state_def
      image_iff eq_commute[of Failure] reaches_def
    split: prod.splits exception_or_result_splits)
  apply auto
  done

lemma succeeds_bind_handle_res:
  "succeeds (bind_handle (f::('s, 'a) res_monad) g h) s ⟷
     (succeeds f s ∧
       (∀v s'. reaches f s (Result v) s' ⟶
          succeeds (g v) s'))"
  by (simp add: succeeds_bind_handle)

lemma outcomes_bind_handle_succeeds: "succeeds (bind_handle f g h) s ⟹
  outcomes (run (bind_handle f g h) s) =
    ⋃ ((λ(r, s'). case r of  Exception e => outcomes (run (h e) s')
  | Result v ⇒ outcomes (run (g v) s'))
       ` (outcomes (run f s)))"
  apply (cases "run f s")
  apply (simp_all add: succeeds_bind_handle succeeds_def run_bind_handle bind_post_state_eq_top)
  apply (simp add: top_post_state_def image_iff split_beta'
              split: exception_or_result_splits)
  apply (intro SUP_cong refl)
  subgoal for X x by (cases "fst x") auto
  done

lemma outcomes_bind_handle_succeeds_res: "succeeds (bind_handle (f::('a, 's) res_monad) g h) s ⟹
  outcomes (run (bind_handle f g h) s) =
    ⋃ ((λ(r, s'). case r of  Exception e => {} | Result v ⇒ outcomes (run (g v) s'))
       ` (outcomes (run f s)))"
  apply (simp add: outcomes_bind_handle_succeeds)
  apply (auto split: exception_or_result_splits)
  done

lemma reaches_bind_handle: "reaches (bind_handle f g h) s r t ⟷
       (succeeds (bind_handle f g h) s ∧
         (∃r' s'. reaches f s r' s' ∧
            (case r' of
               Exception e ⇒ reaches (h e) s' r t
             | Result v ⇒ reaches (g v) s' r t)))"
  apply standard
  subgoal (* FIXME: understand this and make simp / auto proof *)
    apply (frule reaches_succeeds)
    apply (simp add: reaches_def outcomes_bind_handle_succeeds)
    apply (clarsimp split: exception_or_result_splits)
    apply (metis (no_types, opaque_lifting) Exception_eq_Result the_Exception_simp)
    apply (metis (no_types, opaque_lifting) Result_eq_Result the_Exception_simp the_Exception_Result)
    done
  subgoal
    apply (simp add: reaches_def outcomes_bind_handle_succeeds)
    by (auto split: exception_or_result_splits)
      (metis (mono_tags) case_exception_or_result_Exception case_exception_or_result_Result
        case_prod_conv exception_or_result_cases)
  done

lemma reaches_bind_handle_res: "reaches ((bind_handle (f::('a, 's) res_monad) g h)) s r t ⟷
       (succeeds (bind_handle f g h) s ∧
         (∃v s'. reaches f s (Result v) s' ∧ reaches (g v) s' r t))"
  by (simp add: reaches_bind_handle)


subsection ‹\<^const>‹bind››

lemma succeeds_bind:
  "succeeds (bind f g) s ⟷
     (succeeds f s ∧ (∀v s'. reaches f s (Result v) s' ⟶ succeeds (g v) s'))"
  apply (simp add: bind_def succeeds_bind_handle)
  apply (auto split: exception_or_result_splits)
  done

lemma outcomes_bind_succeeds: "succeeds (bind f g) s ⟹ outcomes (run (bind f g) s) =
  ⋃ ((λ(r, s'). case r of Exception e => {(Exception e, s')} | Result v ⇒ outcomes (run (g v) s'))
     ` (outcomes (run f s)))"
  by (simp add: bind_def outcomes_bind_handle_succeeds outcomes_spec_monad pure_post_state_def)

lemma outcomes_bind_succeeds_res: "succeeds (bind  (f::('a, 's) res_monad) g) s ⟹ outcomes (run (bind f g) s) =
  ⋃ ((λ(r, s'). case r of Exception e => {} | Result v ⇒ outcomes (run (g v) s'))
     ` (outcomes (run f s)))"
  by (simp add: bind_def outcomes_bind_handle_succeeds_res outcomes_spec_monad)

lemma reaches_bind: "reaches (bind f g) s r t ⟷
       (succeeds (bind f g) s ∧
         (∃r' s'. reaches f s r' s' ∧
            (case r' of
               Exception e ⇒ r = Exception e ∧ t = s'
             | Result v ⇒ reaches (g v) s' r t)))"
  by (simp add: bind_def reaches_bind_handle)

lemma reaches_bind_res: "reaches ((bind f g)::('a, 's) res_monad) s r t ⟷
       (succeeds (bind f g) s ∧
         (∃v s'. reaches f s (Result v) s' ∧ reaches (g v) s' r t))"
  by (simp add: bind_def reaches_bind_handle_res)

lemma runs_toD_outcomes: "f ∙ s ⦃ P ⦄ ⟹ (x, s) ∈ outcomes (run f s) ⟹ P x s"
  by (cases "run f s") (auto simp: runs_to.rep_eq)

lemma run_bind_reaches_cong:
  assumes f: "run f s = run f' s"
  assumes g: "⋀v s'. succeeds f s ⟹ succeeds f' s ⟹
     reaches f' s (Result v) s' ⟹ run (g v) s' = run (g' v) s'"
  shows "run (bind f g) s = run (bind f' g') s"
  using f g  apply (cases "run f' s") apply (auto simp add: run_bind succeeds_def reaches_def intro!: SUP_cong
split : exception_or_result_splits)
  done

lemma refines_bind_right':
  "succeeds g t ⟹ reaches g t (Result a) t' ⟹
    refines f (h a) s t' R ⟹
    refines f (g >>= h) s t R"
  by (force simp: refines_iff succeeds_bind reaches_bind)

lemma outcomes_empty_bind:
  assumes emp: "outcomes (run f s) = {}"
  shows "outcomes (run (f >>= g) s) = {}"
proof (cases "run f s")
  case Failure
  then show ?thesis  by (auto simp add: run_bind)
next
  case (Success x2)
  then show ?thesis using emp
    by (auto simp add: run_bind bot_post_state_def)
qed

lemma refines_bind_bind_exn: 
  assumes f: "refines f f' s s' Q"
  assumes ll: "⋀e e' t t'.
    Q (Exn e, t) (Exn e', t') ⟹
    R (Exn e, t) (Exn e', t')"
  assumes lr: "⋀e v' t t'.
    Q (Exn e, t) (Result v', t') ⟹
    refines (throw e) (g' v') t t' R" 
   assumes rl: "⋀v e' t t'.
    Q (Result v, t) (Exn e', t') ⟹
    refines (g v) (throw e') t t' R" 
   assumes rr: "⋀v v' t t'.
    Q (Result v, t) (Result v', t') ⟹
    refines (g v) (g' v') t t' R"
   shows "refines (f ⤜ g) (f' ⤜ g') s s' R"
  apply (rule refines_bind')
  apply (rule refines_mono [OF _ f])
  using assms
  apply (auto simp add: default_option_def Exn_def)
  done


subsection ‹\<^const>‹assert››

lemma outcomes_assert[outcomes_spec_monad]:
  "outcomes (run (assert P) s) = (if P then {(Result (), s)} else {})"
  by (simp add: assert_def outcomes_bind_succeeds outcomes_spec_monad)

lemma succeeds_assert[simp]: "succeeds (assert P) s ⟷ P"
  by (simp add: assert_def)

lemma reaches_assert[simp]: "reaches (assert P) s r t ⟷ (P ∧ r = Result () ∧ t = s)"
  by (simp add: assert_def)


subsection "\<^const>‹assume›"

lemma outcomes_assume[outcomes_spec_monad]:
  "outcomes (run (assume P) s) =  (if P then {(Result (), s)} else {})"
  by (simp add: assume_def  outcomes_spec_monad)

lemma succeeds_assume[simp]: "succeeds (assume P) s"
  by (simp add: assume_def)

lemma reaches_assume[simp]: "reaches (assume P) s r t ⟷ (P ∧  r = Result () ∧ t = s)"
  by (simp add: assume_def)


subsection ‹\<^const>‹assume_outcome››

lemma outcomes_assume_outcome[outcomes_spec_monad]:
  "outcomes (run (assume_outcome f) s) = f s"
  by simp

lemma succeeds_assume_outcome[simp]:
  "succeeds (assume_outcome f) s"
  by (simp add: succeeds_def top_post_state_def)

lemma reaches_assume_outcome[simp]:
  "reaches (assume_outcome f) s r t ⟷ (r, t) ∈ f s"
  by (simp add: reaches_def)

subsection ‹\<^const>‹assume_result_and_state››

lemma outcomes_assume_result_and_state[outcomes_spec_monad]:
  "outcomes (run (assume_result_and_state f) s) = ((λ(v, t). (Result v, t)) `  f s)"
  by simp

lemma succeeds_assume_result_and_state[simp]: "succeeds (assume_result_and_state f) s"
  by (simp add: assume_result_and_state_def succeeds_bind)

lemma Union_outcomes_split:
  "(⋃x∈f s.
         (outcomes (run (case x of (v, y) ⇒ g v y) s))) = (⋃(v, y)∈ f s. outcomes (run (g v y) s))"
  using Sup.SUP_cong by auto

lemma reaches_assume_result_and_state [simp]: "reaches (assume_result_and_state f) s r t ⟷ (∃v. r = Result v ∧ (v, t) ∈ f s)"
  by (auto simp add: reaches_def outcomes_spec_monad)

subsection ‹\<^const>‹gets››

lemma succeeds_gets[simp]: "succeeds (gets f) s"
  by (simp add: gets_def succeeds_bind)

lemma outcomes_gets[simp]: "outcomes (run (gets f) s) = {(Result (f s), s)}"
  by simp

lemma reaches_gets[simp]: "reaches (gets f) s r t ⟷ (r = Result (f s) ∧ t = s)"
  by (simp add: reaches_def)

subsection ‹\<^const>‹assert_result_and_state››

lemma succeeds_assert_result_and_state[simp]: "succeeds (assert_result_and_state f) s ⟷ f s ≠ {}"
  by (simp add: assert_result_and_state_def succeeds_bind)

lemma outcomes_assert_result_and_state[outcomes_spec_monad]:
  "outcomes (run (assert_result_and_state f) s) = (if f s = {} then {} else ((λ(v, t). (Result v, t)) `  f s))"
proof (cases "f s = {}")
  case True
  hence "¬ succeeds (assert_result_and_state f) s" by simp
  hence "outcomes (run (assert_result_and_state f) s) = {}"
    by (simp add: not_succeeds_empty_outcomes)
  thus ?thesis by (simp add: True)
next
  case False
  then show ?thesis
    by (auto simp add: assert_result_and_state_def run_bind Sup_Success_pair
        pure_post_state_def)
qed

lemma reaches_assert_result_and_state [simp]: "reaches (assert_result_and_state f) s r t ⟷ (∃v. r = Result v ∧ (v, t) ∈ f s)"
  by (auto simp add: reaches_def outcomes_spec_monad)


subsection "\<^const>‹assuming›"

lemma succeeds_assuming[simp]: "succeeds (assuming g) s"
  by (simp add: assuming_def succeeds_bind)

lemma outcomes_assuming[outcomes_spec_monad]: "outcomes (run (assuming g) s) = (if g s then {(Result (), s)} else {})"
  by (simp add: run_assuming)

lemma reaches_assuming[simp]: "reaches (assuming g) s r t ⟷ (g s ∧ r = Result () ∧ t = s)"
  by (simp add: reaches_def outcomes_assuming)


subsection "\<^const>‹guard›"

lemma succeeds_guard[simp]: "succeeds (guard g) s ⟷ g s"
  by (simp add: guard_def succeeds_bind)

lemma outcomes_guard[outcomes_spec_monad]: "outcomes (run (guard g) s) = (if g s then {(Result (), s)} else {})"
  by (simp add: run_guard)

lemma reaches_guard[simp]: "reaches (guard g) s r t ⟷ (g s ∧ r = Result () ∧ t = s)"
  by (simp add: reaches_def outcomes_guard)


subsection "\<^const>‹assert_opt›"

lemma succeeds_assert_opt[simp]: "succeeds (assert_opt x) s ⟷ (∃v. x = Some v)"
  by (simp add: assert_opt_def split: option.splits)

lemma outcomes_assert_opt[simp]:
  "outcomes (run (assert_opt x) s) = (case x of Some v ⇒ {(Result v, s)} | None ⇒ {})"
  by (simp split: option.splits)

lemma reaches_assert_opt[simp]: "reaches (assert_opt x) s r t ⟷ (∃v. x = Some v ∧ r = Result v ∧ t = s)"
  by (simp add: reaches_def split: option.splits)

subsection "\<^const>‹gets_the›"

lemma succeeds_gets_the[simp]: "succeeds (gets_the f) s ⟷ (∃v. f s = Some v)"
  by (simp add: gets_the_def succeeds_bind)

lemma outcomes_gets_the[simp]:
  "outcomes (run (gets_the f) s) = (case f s of Some v ⇒ {(Result v, s)} | None ⇒ {})"
  by (simp split: option.splits)

lemma reaches_gets_the[simp]: "reaches (gets_the f) s r t ⟷ (∃v. f s = Some v ∧ r = Result v ∧ t = s)"
  by (simp add: reaches_def split: option.splits)

subsection ‹\<^const>‹modify››

lemma outcomes_run_modify[outcomes_spec_monad]: "outcomes (run (modify f) s) = {(Result (), f s)}"
  by simp

lemma succeeds_modify[simp]: "succeeds (modify f) s"
  by (simp add: modify_def succeeds_bind)

lemma reaches_modify[simp]: "reaches (modify f) s r t ⟷ (r = Result () ∧ t = f s)"
  by (auto simp add: modify_def reaches_bind succeeds_bind)


subsection ‹condition›

lemma outcomes_condition:
  "outcomes (run (condition c f g) s) = (if c s then outcomes (run f s) else outcomes (run g s))"
proof (cases "succeeds (condition c f g) s")
  case True
  then show ?thesis by (auto simp add: condition_def outcomes_bind_succeeds outcomes_spec_monad
        split: exception_or_result_splits)
next
  case False
  then show ?thesis
    by (simp add: condition_def run_bind)
  qed

lemma succeeds_condition_iff:
  "succeeds (condition c f g) s ⟷ succeeds (if c s then f else g) s"
  by (simp add: condition_def succeeds_bind)

lemma reaches_condition_iff:
  "reaches (condition c f g) s r' s' ⟷ reaches (if c s then f else g) s r' s'"
  by (simp add:  reaches_def outcomes_condition)

lemma reaches_condition_True[simp]:
  "c s ⟹ reaches (condition c f g) s r' s' ⟷ reaches f s r' s'"
  by (simp add: reaches_condition_iff)

lemma reaches_condition_False[simp]:
  "¬ c s ⟹ reaches (condition c f g) s r' s' ⟷ reaches g s r' s'"
  by (simp add: reaches_condition_iff)

lemma succeeds_condition_True[simp]:
  "c s ⟹ succeeds (condition c f g) s ⟷ succeeds f s"
  by (simp add: succeeds_condition_iff)

lemma succeeds_condition_False[simp]:
  "¬(c s) ⟹ succeeds (condition c f g) s ⟷ succeeds g s"
  by (simp add: succeeds_condition_iff)

subsection "\<^const>‹when›"

lemma succeeds_when: "succeeds (when c f) s ⟷ ¬c ∨ succeeds f s"
  unfolding when_def by (simp add: succeeds_condition_iff)

lemma outcomes_when[outcomes_spec_monad]:
  "outcomes (run (when c f) s) = (if c then outcomes (run f s) else {(Result (), s)})"
  by (simp add: run_when)

lemma reaches_when_iff:
  "reaches (when c f) s r' s' ⟷ (if c then reaches f  s r' s' else (r' = Result () ∧ s' = s))"
  by (simp add:  reaches_def outcomes_when)

subsection ‹While›

lemma reaches_whileLoop_cond_false:
  "reaches (whileLoop C B r) s (Result r') s' ⟹ ¬ C r' s'"
  using runs_to_partial_whileLoop_cond_false[of C B r s]
  by (auto simp: reaches_succeeds runs_to_partial_def_old)

lemma bind_post_state_cong:
  "(⋀r . r ∈ outcomes x ⟹ g r = g' r) ⟹ bind_post_state x g = bind_post_state x g'"
  by (cases x) simp_all

subsection ‹\<^const>‹map_value››

lemma succeeds_map_value[simp]: "succeeds (map_value f g) s ⟷ succeeds g s"
  by (simp add: succeeds_def run_map_value top_post_state_def
      bot_post_state_def split: post_state.splits)

lemma outcomes_map_value[outcomes_spec_monad]:
  "outcomes (run (map_value f g) s) = ((λ(v, s). (f v, s)) ` (outcomes (run g s)))"
  by (auto simp add: always_progress_def run_map_value
      top_post_state_def bot_post_state_def split: post_state.splits)

lemma reaches_map_value: "reaches (map_value f g) s r t ⟷ (∃r'. reaches g s r' t ∧ r = f r')"
  by (auto simp add: reaches_def outcomes_map_value)

subsection ‹\<^const>‹liftE››

lemma succeeds_liftE[simp]: "succeeds (liftE f) s ⟷ succeeds f s"
  by (simp add: liftE_def)

lemma outcomes_liftE[outcomes_spec_monad]:
  "outcomes (run (liftE f) s) =
    ((λ(v, s). (map_exception_or_result (λx. undefined) id v, s)) ` (outcomes (run f s)))"
  by (simp add: liftE_def outcomes_spec_monad)

lemma reaches_liftE: "reaches (liftE f) s r t ⟷ (∃r'. reaches f s (Result r') t ∧ r = Result r')"
  by (auto simp add: liftE_def reaches_map_value)

lemma bind_cong1:
  fixes f::"('a, 's) res_monad"
  shows "⟦ f = f'; ⋀v s s'. reaches f s (Result v) s' ⟹ g v = g' v ⟧ ⟹ f >>= g = f' >>= g'"
  apply (rule spec_monad_ext)
  apply (rule run_bind_reaches_cong)
   apply auto
  done

lemma bind_liftE_cong1:
  fixes f::"('a, 's) res_monad"
  shows "⟦ f = f'; ⋀v s s'. reaches f s (Result v) s' ⟹ g v = g' v ⟧ ⟹
    (liftE f) >>= g = (liftE f') >>= g'"
  apply (rule spec_monad_ext)
  apply (rule run_bind_reaches_cong)
  apply (auto simp add: reaches_liftE)
  done

subsection ‹\<^const>‹try››

lemma succeeds_try[simp]: "succeeds (try f) s ⟷ succeeds f s"
  by (simp add: try_def)

lemma outcomes_try[outcomes_spec_monad]:
  "outcomes (run (try f) s) = ((λ(v, s). (unnest_exn v, s)) ` (outcomes (run f s)))"
  by (simp add: try_def outcomes_spec_monad)

lemma reaches_try: "reaches (try f) s r t ⟷ (∃r'. reaches f s r' t ∧ r = unnest_exn r')"
  by (simp add: try_def reaches_map_value)

subsection ‹\<^const>‹finally››

lemma succeeds_finally[simp]: "succeeds (finally f) s ⟷ succeeds f s"
  by (simp add: finally_def)

lemma outcomes_finally[outcomes_spec_monad]:
  "outcomes (run (finally f) s) = ((λ(v, s). (unite v, s)) ` (outcomes (run f s)))"
  by (simp add: finally_def outcomes_spec_monad)

lemma reaches_finally: "reaches (finally f) s r t ⟷ (∃r'. reaches f s r' t ∧ r = unite r')"
  by (simp add: finally_def reaches_map_value)

subsection ‹\<^const>‹catch››

lemma succeeds_catch: "succeeds (f <catch> h) s ⟷
  (succeeds f s ∧
    (∀x s'. reaches f s x s' ⟶ (case x of Exn e ⇒ succeeds (h e) s' | Result v ⇒ True)))"
  unfolding catch_def
  by (fastforce simp add: succeeds_bind_handle default_option_def Exn_def split: exception_or_result_splits xval_splits)

lemma outcomes_catch_succeeds: "succeeds (f <catch> h) s ⟹
  outcomes (run (f <catch> h) s) =
    ⋃ ((λ(r, s'). case r of  Exn e => outcomes (run (h e) s') | Result v ⇒ {(Result v, s')})
       ` (outcomes (run f s)))"
  unfolding catch_def
  by (auto simp add: outcomes_bind_handle_succeeds default_option_def Exn_def 
      split: prod.splits exception_or_result_splits xval_splits)
    (metis Exn_def Exn_neq_Result the_Exception_simp fst_conv option.sel snd_conv  
      Pair_inject Result_eq_Result)+

lemma reaches_catch: "reaches (f <catch> h) s r t ⟷
       (succeeds (f <catch> h) s ∧
         (∃r' s'. reaches f s r' s' ∧
            (case r' of
               Exn e ⇒ reaches (h e) s' r t
             | Result v ⇒ r = Result v ∧ t = s')))"
  unfolding catch_def
  by (auto simp add: reaches_bind_handle default_option_def Exn_def split: prod.splits exception_or_result_splits xval_splits)
    (metis option.sel)+


subsection ‹\<^const>‹check››

lemma succeeds_check[simp]: "succeeds (check e p) s"
  by (simp add: succeeds_def run_check top_post_state_def)

lemma outcomes_check[outcomes_spec_monad]: "outcomes (run (check e p) s) =
  (if (∃x. p s x) then ((λx. (x, s)) ` (Result ` {x. p s x})) else {(Exn e, s)})"
by (simp add: run_check)

lemma reaches_check: "reaches (check e p) s r t ⟷
  (t = s) ∧
   (if (∃x. p s x) then (∃x. r = Result x ∧ p s x) else r = Exn e)"
  by (auto simp add: reaches_def outcomes_check)

lemma refines_bind_ok:
  "succeeds g t ⟹ reaches g t (Result a) t' ⟹
    refines f (h a) s t' R ⟹
    refines f (g >>= h) s t R"
 by (fastforce simp: refines_iff succeeds_bind reaches_bind)

subsection ‹\<^const>‹ignoreE››

lemma succeeds_ignoreE[simp]:
  "succeeds (ignoreE f) s ⟷ (succeeds f s)"
  unfolding ignoreE_def
  by (auto simp add: succeeds_catch split: xval_splits)

lemma outcomes_ignoreE_succeeds: "succeeds f s ⟹ outcomes (run (ignoreE f) s) =
   ⋃ ((λ(r, s'). case r of  Exn e => {} | Result v ⇒ {(Result v, s')})
       ` (outcomes (run f s)))"
  apply (subst (asm) succeeds_ignoreE [symmetric])
  by (simp add: ignoreE_def outcomes_catch_succeeds)

lemma reaches_ignoreE:
  "reaches (ignoreE f) s r t ⟷ (succeeds f s) ∧ (∃v. r = Result v ∧ reaches f s (Result v) t)"
  apply (simp add:  reaches_catch succeeds_catch ignoreE_def)
  apply (fastforce split: xval_splits)
  done

subsection ‹\<^const>‹bind_exception_or_result››

lemma succeeds_bind_exception_or_result:
  "succeeds (bind_exception_or_result f g) s ⟷
    succeeds f s ∧ (∀v s'. reaches f s v s' ⟶ succeeds (g v) s')"
  by (cases "run f s";
    force simp: succeeds_def bind_exception_or_result.rep_eq
                bind_post_state_eq_top top_post_state_def reaches_def)

lemma reaches_bind_exception_or_result:
  "reaches (bind_exception_or_result f g) s r t ⟷
    (succeeds (bind_exception_or_result f g) s ∧
      (∃r' s'. reaches f s r' s' ∧ reaches (g r') s' r t))"
  apply (cases "run f s")
  apply (simp_all add: reaches_def succeeds_def bind_exception_or_result.rep_eq)
  subgoal for X
    apply (cases "∃x∈X. case x of (v, x) ⇒ run (g v) x = ⊤")
    apply (simp_all add: Sup_post_state_def image_iff split_beta' Bex_def Ball_def eq_commute
                 flip: top_post_state_def)
    by (metis outcomes.simps(2) post_state.exhaust top_post_state_def)
  done

lemma refines_bind_exception_or_result_strong:
  assumes f: "refines f f' s s' Q"
  assumes g: "⋀r t r' t'. Q (r, t) (r', t') ⟹ reaches f s r t ⟹ reaches f' s' r' t' ⟹  refines (g r) (g' r') t t' R"
  shows "refines (bind_exception_or_result f g) (bind_exception_or_result f' g') s s' R"
  using refines_bind_exception_or_result refines_mono f g
  by (smt (verit, ccfv_threshold) case_prod_conv refines_strengthen')

subsection ‹\<^const>‹bind_finally››

lemma succeeds_bind_finally:
  "succeeds (bind_finally f g) s = (succeeds f s ∧ (∀v s'. reaches f s v s' ⟶ succeeds (g v) s'))"
  by (rule succeeds_bind_exception_or_result)

lemma reaches_bind_finally: "reaches (bind_finally f g) s r t ⟷ (succeeds (bind_finally f g) s ∧ (∃r' s'. reaches f s r' s' ∧ reaches (g r') s' r t))"
  by (rule reaches_bind_exception_or_result)

subsection ‹\<^const>‹run_bind››

lemma succeeds_run_bind:
  "succeeds (run_bind f t g) s ⟷ succeeds f t ∧ (∀r t'. reaches f t r t' ⟶ succeeds (g r t') s)"
  by (cases "run f t")
     (force simp: succeeds_def run_run_bind top_post_state_def reaches_def
            split: post_state.splits)+

lemma reaches_run_bind: "reaches (run_bind f t g) s r s' ⟷
         (succeeds (run_bind f t g) s) ∧
         (∃r' t'. reaches f t r' t' ∧ reaches (g r' t') s r s')"
  apply (cases "run f t")
  apply (simp_all add: reaches_def run_run_bind succeeds_run_bind)
  apply (simp add: succeeds_def split_beta')
  subgoal for A
    apply (cases "∀r t'. (r, t') ∈ A ⟶ run (g r t') s ≠ ⊤")
    subgoal by (subst outcomes_Sup; force simp flip: top_post_state_def)
    subgoal
      apply (subst Sup_eq_Failure[THEN iffD2])
      apply (force simp flip: top_post_state_def)
      apply auto
      done
    done
  done


lemma runs_to_partial_reaches: "f ∙ s ?⦃ reaches f s ⦄"
  apply (cases "run f s")
  apply (auto simp add: runs_to_partial_def reaches_def)
  done

lemma refines_strengthen_reaches:
  assumes f_g: "refines f g s t R" 
  assumes reach: "(⋀x s' y t'. R (x, s') (y, t') ⟹ reaches f s x s' ⟹ reaches g t y t'  ⟹ Q (x, s') (y, t'))"
  shows "refines f g s t Q"
  apply (rule refines_strengthen [OF f_g  runs_to_partial_reaches  runs_to_partial_reaches] )
  using reach
  by blast


lemma refines_bind_bind_strong': 
  assumes f: "refines f f' s s' Q"
  assumes Ex_Ex: "(⋀e e' t t'.
    Q (Exception e, t) (Exception e', t') ⟹
    e ≠ default ⟹
    e' ≠ default ⟹
    reaches f s (Exception e) t ⟹
    reaches f' s' (Exception e') t' ⟹
    R (Exception e, t) (Exception e', t'))"
  assumes Res_Ex: "(⋀e v' t t'.
    Q (Exception e, t) (Result v', t') ⟹
    e ≠ default ⟹
    reaches f s (Exception e) t ⟹
    reaches f' s' (Result v') t' ⟹
    refines (yield (Exception e)) (g' v') t t' R)"
  assumes Ex_Ex: "(⋀v e' t t'.
    Q (Result v, t) (Exception e', t') ⟹
    e' ≠ default ⟹
    reaches f s (Result v) t ⟹
    reaches f' s' (Exception e') t' ⟹
    refines (g v) (yield (Exception e')) t t' R)"
  assumes Res_Res: "(⋀v v' t t'.
    Q (Result v, t) (Result v', t') ⟹
    reaches f s (Result v) t ⟹
    reaches f' s' (Result v') t' ⟹
    refines (g v) (g' v') t t' R)"
  shows "refines (f ⤜ g) (f' ⤜ g') s s' R"
  apply (rule refines_bind')
  apply (rule refines_strengthen_reaches [OF f])
  apply (auto intro: assms)
  done


lemma rel_spec_monad_bind_strong:
  assumes f_f': "rel_spec_monad S P f f'"
  assumes Ex_Ex: "⋀e e' s s' t t'. S s s' ⟹ S t t' ⟹ P (Exception e) (Exception e') ⟹ e ≠ default ⟹ e' ≠ default ⟹ 
    reaches f s (Exception e) t ⟹ reaches f' s' (Exception e') t' ⟹
    Q (Exception e) (Exception e')"
  assumes Ex_Res: "⋀e v' s s' t t'. S s s' ⟹ S t t' ⟹ P (Exception e) (Result v') ⟹ e ≠ default ⟹ 
    reaches f s (Exception e) t ⟹ reaches f' s' (Result v') t' ⟹ 
    rel_spec_monad S Q (yield (Exception e)) (g' v')"
  assumes Res_Ex: "⋀v e' s s' t t'. S s s' ⟹ S t t' ⟹ P (Result v) (Exception e') ⟹ e' ≠ default ⟹
     reaches f s (Result v) t ⟹ reaches f' s' (Exception e') t' ⟹ 
     rel_spec_monad S Q (g v) (yield (Exception e'))"
  assumes Res_Res: "⋀v v' s s' t t'. S s s' ⟹ S t t' ⟹ P (Result v) (Result v') ⟹
     reaches f s (Result v) t ⟹ reaches f' s' (Result v') t' ⟹ 
     rel_spec_monad S Q (g v) (g' v')"
  shows "rel_spec_monad S Q (f ⤜ g) (f' ⤜ g')"
  apply (simp add: rel_spec_monad_iff_refines)
  apply (clarify, intro conjI)
  subgoal for s t
    apply (rule refines_bind_bind_strong' [where Q="(rel_prod P S)"])
    subgoal using f_f' by (auto simp add: rel_spec_monad_iff_refines)
    subgoal
      using Ex_Ex by auto
    subgoal
      using Ex_Res by (auto simp add: rel_spec_monad_iff_refines)
    subgoal
      using Res_Ex by (auto simp add: rel_spec_monad_iff_refines)
    subgoal
      using Res_Res by (auto simp add: rel_spec_monad_iff_refines)
    done
  subgoal for s t
    apply (rule refines_bind_bind_strong' [where Q="(rel_prod P¯¯ S¯¯)"])
    subgoal using f_f' by (auto simp add: rel_spec_monad_iff_refines)
    subgoal
      using Ex_Ex by auto
    subgoal
      using Res_Ex by (auto simp add: rel_spec_monad_iff_refines)
    subgoal
      using Ex_Res by (auto simp add: rel_spec_monad_iff_refines)
    subgoal
      using Res_Res by (auto simp add: rel_spec_monad_iff_refines)
    done
  done

lemma rel_spec_monad_bind_strong_exn:
  assumes f_f': "rel_spec_monad S P f f'"
  assumes Ex_Ex: "⋀e e' s s' t t'. S s s' ⟹ S t t' ⟹ P (Exn e) (Exn e') ⟹ 
    reaches f s (Exn e) t ⟹ reaches f' s' (Exn e') t' ⟹
    Q (Exn e) (Exn e')"
  assumes Ex_Res: "⋀e v' s s' t t'. S s s' ⟹ S t t' ⟹ P (Exn e) (Result v') ⟹ 
    reaches f s (Exn e) t ⟹ reaches f' s' (Result v') t' ⟹ 
    rel_spec_monad S Q (throw e) (g' v')"
  assumes Res_Ex: "⋀v e' s s' t t'. S s s' ⟹ S t t' ⟹ P (Result v) (Exn e') ⟹
     reaches f s (Result v) t ⟹ reaches f' s' (Exn e') t' ⟹ 
     rel_spec_monad S Q (g v) (throw e')"
  assumes Res_Res: "⋀v v' s s' t t'. S s s' ⟹ S t t' ⟹ P (Result v) (Result v') ⟹
     reaches f s (Result v) t ⟹ reaches f' s' (Result v') t' ⟹ 
     rel_spec_monad S Q (g v) (g' v')"
  shows "rel_spec_monad S Q (f ⤜ g) (f' ⤜ g')"
  apply (rule rel_spec_monad_bind_strong [OF f_f'])
  subgoal using Ex_Ex by (auto simp add: Exn_def default_option_def)
  subgoal using Ex_Res by (auto simp add: Exn_def default_option_def)
  subgoal using Res_Ex by (auto simp add: Exn_def default_option_def)
  subgoal using Res_Res by (auto)
  done


lemma rel_spec_monad_rel_xval_bind_strong:
  assumes f_f': "rel_spec_monad S (rel_xval L P) f f'"
  assumes Res_Res: "⋀v v' s s' t t'. S s s' ⟹ S t t' ⟹ P v v' ⟹
     reaches f s (Result v) t ⟹ reaches f' s' (Result v') t' ⟹ 
     rel_spec_monad S (rel_xval L R) (g v) (g' v')"
  shows "rel_spec_monad S (rel_xval L R) (f ⤜ g) (f' ⤜ g')"
  apply (rule rel_spec_monad_bind_strong_exn [OF f_f'])
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal using Res_Res by auto
  done

lemma rel_spec_monad_bind_exception_or_result_strong:
  assumes f_f': "rel_spec_monad S P f f'"
  assumes g_g': "⋀r r' s s' t t'. S s s' ⟹ S t t' ⟹ P r r' ⟹
    reaches f s r t ⟹ reaches f' s' r' t' ⟹
    rel_spec_monad S Q (g r) (g' r')"
  shows "rel_spec_monad S Q (bind_exception_or_result f g) (bind_exception_or_result f' g')"
  apply (simp add: rel_spec_monad_iff_refines)
  apply (clarify, intro conjI)
  subgoal for s t
    apply (rule refines_bind_exception_or_result_strong [where Q="rel_prod P S"])
    subgoal
      using f_f' by (auto simp add: rel_spec_monad_iff_refines)
    subgoal
      using g_g' by (auto simp add: rel_spec_monad_iff_refines)
    done
  subgoal for s t
    apply (rule refines_bind_exception_or_result_strong [where Q="rel_prod P¯¯ S¯¯"])
    subgoal
      using f_f' by (auto simp add: rel_spec_monad_iff_refines)
    subgoal
      using g_g' by (auto simp add: rel_spec_monad_iff_refines)
    done
  done

end