Theory Refines_Spec
chapter ‹TS phase: Type Strengthening (find suitable target monad)›
theory Refines_Spec
imports
Option_MonadND
L2ExceptionRewrite
begin
lemma gets_the_ocondition:
"Spec_Monad.gets_the (ocondition C T F) =
Spec_Monad.condition C (Spec_Monad.gets_the T) (Spec_Monad.gets_the F)"
by (simp add: spec_monad_ext_iff ocondition_def run_condition)
lemma gets_the_oreturn:
"Spec_Monad.gets_the (oreturn x) = Spec_Monad.return x"
by (simp add: spec_monad_ext_iff)
lemma gets_the_obind:
"Spec_Monad.gets_the (obind f g) =
Spec_Monad.bind (Spec_Monad.gets_the f) (λx. Spec_Monad.gets_the (g x))"
by (simp add: spec_monad_ext_iff run_bind obind_def split: option.splits)
setup ‹
let open Mutual_CCPO_Rec in
add_ccpo "spec_monad_gfp" (fn ctxt => fn (T as \<^Type>‹spec_monad E A S›) =>
let
in
synth_gfp ctxt T
end)
|> Context.theory_map
end
›
lemma rel_map_the_Result[simp]: "rel_map the_Result (Result v) b ⟷ v = b"
by (auto simp add: rel_map_def)
lemma holds_partial_post_state_Inf:
assumes X: "⋀x. x ∈ X ⟹ holds_partial_post_state P x"
shows "holds_partial_post_state P (⨅ X)"
apply (clarsimp simp add: Inf_post_state_def vimage_def)
subgoal premises prems for p x
using X[of "Success x"] prems by auto
done
lemma holds_post_state_Inf:
assumes X: "⋀x. x ∈ X ⟹ holds_post_state P x"
shows "X ≠ {} ⟹ holds_post_state P (⨅ X)"
apply (clarsimp simp add: Inf_post_state_def vimage_def, safe)
subgoal for x using X[of x] by (cases x) auto
subgoal using assms by force
done
lemma admissible_runs_to[corres_admissible]:
"ccpo.admissible Inf (λx y. y ≤ x) (λx. x ∙ s ⦃ Q ⦄)"
apply (simp add: ccpo.admissible_def chain_def)
apply transfer
apply (auto intro: holds_post_state_Inf)
done
lemma spec_monad_Inf_run: "(run (⨅A) s) = ⨅ ((λf. (run f s)) ` A)"
by (metis INF_apply Inf_spec_monad.rep_eq)
lemma outcomes_Inf_run_succeeds_conv:
"outcomes (⨅f∈A. run f t) = outcomes (⨅f ∈ {f. f ∈ A ∧ succeeds f t}. run f t)"
apply (clarsimp simp add: Inf_post_state_def succeeds_def top_post_state_def)
apply fastforce
done
lemma succeeds_outcomes_Inf_Inter_conv:
"g ∈ A ⟹ succeeds g t ⟹ outcomes (⨅f ∈ {f ∈ A. succeeds f t}. run f t) =
(⋂f∈{f ∈ A. succeeds f t}. outcomes (run f t))"
apply (clarsimp simp add: Inf_post_state_def succeeds_def top_post_state_def, intro impI conjI set_eqI iffI)
subgoal by (auto simp add: vimage_def image_def split: post_state.splits)
subgoal by (smt (verit, ccfv_SIG) INF_top_conv(2) Inf_post_state_def mem_Collect_eq top_post_state_def)
subgoal by (smt (verit) Success_vimage_image_cancel image_cong mem_Collect_eq outcomes_succeeds_run_conv succeeds_def top_post_state_def)
subgoal by (smt (verit, best) Success_vimage_image_cancel image_cong mem_Collect_eq outcomes_succeeds_run_conv succeeds_def top_post_state_def)
done
lemma admissible_refines_spec_fun_of_rel:
assumes prj: "fun_of_rel R prj"
shows "ccpo.admissible Inf (≥)
(λ(A::('e::default, 'a, 's) spec_monad) . refines C A s t (rel_prod R (=)))"
proof (rule ccpo.admissibleI)
fix A::"('e, 'a, 's) spec_monad set"
assume A_prop: "∀g∈A. refines C g s t (rel_prod R (=))"
assume chain: "Complete_Partial_Order.chain (≥) A"
assume non_empty: "A ≠ {}"
have Inf_lower: "⋀g. g ∈ A ⟹ ⨅ A ≤ g"
by (simp add: Inf_lower)
hence run_Inf_lower: "⋀g s. g ∈ A ⟹ run ( ⨅ A) s ≤ run g s"
by (simp add: le_funD less_eq_spec_monad.rep_eq)
have "(⋀s. (⋀g. g ∈ A ⟹ run g s = Failure) ⟹ run (⨅A) s = Failure)"
apply (simp add: spec_monad_Inf_run)
by (simp add: non_empty)
hence succeeds: "⋀s. succeeds (⨅A) s ⟹ (∃g ∈ A. succeeds g s)"
by (auto simp add: succeeds_def top_post_state_def)
show "refines C (⨅ A) s t (rel_prod R (=))"
apply (clarsimp simp add: refines_def_old reaches_def)
apply (intro conjI allI impI)
proof -
assume "succeeds (⨅ A) t" then
show "succeeds C s"
using succeeds A_prop non_empty
by (auto simp add: refines_def_old)
next
fix r s'
assume succeeds_Inf: "succeeds (⨅ A) t"
then obtain g where g: "g ∈ A" and succeeds_g: "succeeds g t"
using succeeds by blast
assume res: "(r, s') ∈ outcomes (run C s)"
show "∃r'. (r', s') ∈ outcomes (run (⨅ A) t) ∧ R r r'"
proof -
from A_prop res prj
have prj_prop: "⋀g. g ∈ A ⟹ succeeds g t ⟹ (prj r, s') ∈ outcomes (run g t) ∧ R r (prj r)"
apply (clarsimp simp add: refines_def_old )
using fun_of_rel_def
by (smt (verit) reaches_def)
hence "(prj r, s') ∈ outcomes (run (⨅ A) t)"
apply (simp add: spec_monad_Inf_run)
apply (subst outcomes_Inf_run_succeeds_conv)
apply (subst succeeds_outcomes_Inf_Inter_conv [OF g succeeds_g])
apply auto
done
moreover from prj_prop g succeeds_g have "R r (prj r)" by blast
ultimately show ?thesis by blast
qed
qed
qed
lemma admissible_refines_spec_funp:
assumes "funp R"
shows "ccpo.admissible Inf (≥)
(λ(A::('e::default, 'a, 's) spec_monad) . refines C A s t (rel_prod R (=)))"
proof -
from assms obtain prj where "fun_of_rel R prj"
by (auto simp add: funp_def)
then show ?thesis
by (rule admissible_refines_spec_fun_of_rel)
qed
lemma admissible_refines_spec_res[corres_admissible]:
shows "ccpo.admissible Inf (≥)
(λ(A::('a, 's) res_monad) . refines C A s t (rel_prod (rel_liftE ) (=)))"
by (rule admissible_refines_spec_funp) (intro funp_intros)
lemma admissible_refines_spec_exit_eq[corres_admissible]:
shows "ccpo.admissible Inf (≥)
(λ(A::('e, 'a, 's) exn_monad) . refines C A s t (rel_prod (rel_xval (=) (=)) (=)))"
by (rule admissible_refines_spec_funp) (intro funp_intros)
lemma admissible_refines_spec_exit_the_Nonlocal[corres_admissible]:
shows "ccpo.admissible Inf (≥)
(λ(A::('e, 'a, 's) exn_monad) . refines C A s t (rel_prod ((rel_xval (rel_Nonlocal) (=))) (=)))"
by (rule admissible_refines_spec_funp) (intro funp_intros)
lemma gen_admissible_refines_gets_the[corres_admissible]:
shows "ccpo.admissible option.lub_fun option.le_fun (λA. refines C (gets_the A) s t (rel_prod (rel_liftE) (=)))"
apply (clarsimp simp add: refines_def_old relcompp.simps rel_liftE_def rel_map_def
split: option.splits)
by (smt (verit) ccpo.admissibleI chain_fun flat_lub_in_chain fun_lub_def mem_Collect_eq option.discI)
theorem refines_option_top [corres_top]: "refines f (gets_the Map.empty) s t R"
by (auto simp add: refines_def_old)
section ‹Synthesize Rules Setup›
text ‹Canonical format for the currently supported monads:
\<^term>‹refines C (lift_to_spec A) s t (rel_prod rel_res (=))›
where \<^term>‹lift_spec›, \<^term>‹rel_res› is
▪ pure (Pure function): \<^term>‹return›, \<^term>‹rel_liftE›
▪ gets (Reader monad): \<^term>‹gets›,\<^term>‹rel_liftE›
▪ option (Option monad): \<^term>‹gets_the›,\<^term>‹rel_liftE›
▪ nondet: \<^term>‹id› (ommitted),\<^term>‹rel_liftE›
▪ exit:
▪ \<^term>‹id› (ommitted),\<^term>‹rel_xval rel_Nonlocal (=)›
▪ \<^term>‹id› (ommitted),\<^term>‹rel_xval (=) (=)› for those function that were
lifted by the IO phase.
›
synthesize_rules pure and reader and option and nondet and exit
add_synthesize_pattern pure and reader and option and nondet and exit where
refines_pure_synth = ‹Trueprop (refines ?f ((return ?f')::(?'a, ?'s) res_monad) _ _ ?R)› (f')
add_synthesize_pattern reader and option and nondet and exit where
refines_reader_synth = ‹Trueprop (refines ?f (gets ?f') _ _ ?R)› (f')
add_synthesize_pattern option where
refines_option_synth = ‹Trueprop (refines ?f (gets_the ?f') _ _ ?R)› (f')
add_synthesize_pattern nondet and exit where
refines_nondet_synth = ‹Trueprop (refines ?f ?f' _ _ ?R)› (f') and
rel_liftE_nondet_synth = ‹Trueprop (rel_liftE ?x ?x')› (x') and
rel_sum_nondet_synth = ‹Trueprop (rel_sum _ _ ?x ?x')› (x') and
rel_sum_nondet_synth = ‹Trueprop (rel_xval _ _ ?x ?x')› (x') and
rel_compp_nondet_synth = ‹Trueprop ((_ OO _) ?x ?x')› (x') and
rel_map_synth = ‹Trueprop (rel_map ?f ?x ?x')› (x') and
rel_eq_nondet_synth = ‹Trueprop (?x = ?x')› (x')
add_synthesize_pattern exit where
rel_Nondet_exit_synth = ‹Trueprop (rel_Nonlocal ?x ?x')› (x')
text ‹
Recursive functions are defined using @{command fixed_point}.
The option, nondet and exit monad are setup to handle these definitions. Hence the minimal
monad for recursive functions is the option monad.
›
section ‹Pure Monad›
lemma refines_L2_call_embed_pure:
assumes f: "refines f (return f') s s (rel_prod rel_liftE (=))"
shows "refines (L2_call f emb ns) (return (L2_VARS f' ns)::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
unfolding L2_VARS_def L2_call_def
using f
apply (clarsimp simp add: refines_def_old reaches_map_value map_exn_def rel_liftE_def split: xval_splits)
apply (metis Exn_def default_option_def exception_or_result_cases not_Some_eq)+
done
lemma refines_L2_gets_pure:
"refines (L2_gets (λ_. v) ns) (return (L2_VARS v ns)::('a,'s) res_monad) s s (rel_prod (rel_liftE) (=))"
unfolding L2_VARS_def L2_defs gets_return
by (auto intro: refines_yield)
lemma refines_L2_seq_pure:
assumes g [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (g v) (return (g' v)::('a,'s) res_monad) t t (rel_prod rel_liftE (=)))"
assumes f [unfolded THIN_def, rule_format]: "PROP THIN (Trueprop (refines f ((return f')::('b,'s) res_monad) s s (rel_prod rel_liftE (=))))"
shows "refines (L2_seq f g) (return (let v = f' in (g' v))::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
using g f unfolding L2_defs
apply (clarsimp simp add: refines_def_old reaches_bind succeeds_bind rel_liftE_def default_option_def split: exception_or_result_splits)
apply (metis default_option_def exception_or_result_cases option.exhaust_sel)+
done
lemma refines_L2_condition_pure:
assumes g: "refines g (return g'::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
assumes f: "refines f (return f'::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
shows "refines (L2_condition (λ_. c) f g) (return (if c then f' else g')::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
using g f unfolding L2_defs
by (auto intro: refines_condition)
lemma refines_L2_try_L2_throw_pure:
shows "refines (L2_try (L2_throw (Inr r) ns)) (return (L2_VARS r ns)::('a,'s)res_monad) s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_VARS_def
by (auto simp add: refines_def_old reaches_try rel_liftE_def unnest_exn_def)
lemma refines_L2_try_L2_seq_pure:
assumes g: "⋀v t. refines (L2_try (g v)) (return (g' v)::('a,'s) res_monad) t t (rel_prod rel_liftE (=))"
assumes f: "refines f (return f'::('b,'s) res_monad) s s (rel_prod rel_liftE (=))"
shows "refines (L2_try (L2_seq f g)) (return (let v = f' in (g' v))::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
unfolding L2_defs try_def refines_map_value_left_iff return_let_bind
apply (rule refines_bind [OF f])
subgoal by auto
subgoal by (auto simp add: default_option_def Exn_def[symmetric] rel_liftE_def)
subgoal by auto
subgoal using g [simplified L2_defs try_def refines_map_value_left_iff] by auto
done
lemma refines_L2_try_L2_condition_pure:
assumes f: "refines (L2_try f) (return f'::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
assumes g: "refines (L2_try g) (return g'::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
shows "refines (L2_try (L2_condition (λ_. c) f g)) (return (if c then f' else g')::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
using f g unfolding L2_defs
apply (auto simp add: refines_def_old reaches_try reaches_bind succeeds_bind rel_liftE_def unnest_exn_def
default_option_def Exn_def [symmetric]
split: xval_split exception_or_result_splits sum.splits)
done
lemma refines_L2_try_pure:
assumes f: "refines f (return f'::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
shows "refines (L2_try f) (return f'::('a,'s) res_monad) s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_guarded_def try_def using f
apply (clarsimp simp add: refines_def_old reaches_try reaches_map_value rel_liftE_def unnest_exn_def
default_option_def Exn_def [symmetric]
split: xval_split exception_or_result_splits sum.splits)
by (metis Exn_def default_option_def exception_or_result_cases option.exhaust_sel sum_all_ex(2))
print_synthesize_rules pure
lemmas refines_monad_pure =
refines_L2_call_embed_pure [synthesize_rule pure and reader and option and nondet and exit priority:510]
refines_L2_gets_pure [synthesize_rule pure and reader and option and nondet and exit priority:510]
refines_L2_seq_pure [synthesize_rule pure and reader and option and nondet and exit priority:510 split: g and g']
refines_L2_condition_pure [synthesize_rule pure and reader and option and nondet and exit priority:510]
refines_L2_try_L2_throw_pure [synthesize_rule pure and reader and option and nondet and exit priority:520]
refines_L2_try_L2_seq_pure [synthesize_rule pure and reader and option and nondet and exit priority:520 split: g and g']
refines_L2_try_L2_condition_pure [synthesize_rule pure and reader and option and nondet and exit priority:520]
refines_L2_try_pure [synthesize_rule pure and reader and option and nondet and exit priority:510]
print_synthesize_rules pure
section ‹Reader Monad (Gets)›
lemma refines_L2_call_embed_reader:
assumes f: "refines f (gets f') s s (rel_prod rel_liftE (=))"
shows "refines (L2_call f emb ns) (gets (L2_VARS f' ns)) s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_call_def liftE_def L2_VARS_def using f
apply (clarsimp simp add: refines_def_old reaches_try reaches_map_value rel_liftE_def map_exn_def
default_option_def Exn_def [symmetric]
split: xval_split exception_or_result_splits sum.splits)
by (metis Exn_def default_option_def exception_or_result_cases option.exhaust_sel)
lemma refines_L2_gets_reader:
"refines (L2_gets f ns) (gets (L2_VARS f ns)) s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_VARS_def liftE_def
by (auto intro: refines_gets)
lemma refines_lift_pure_reader:
assumes f: "refines f (return f') s s (rel_prod rel_liftE (=))"
shows "refines f (gets (λ_. f')) s s (rel_prod rel_liftE (=))"
using f unfolding liftE_def
by (simp add: gets_return)
lemma refines_L2_seq_reader:
assumes g: "⋀v t. refines (g v) (gets (g' v)) t t (rel_prod rel_liftE (=))"
assumes f: "refines f (gets f') s s (rel_prod rel_liftE (=))"
shows "refines (L2_seq f g) (gets (λs. let v = f' s in (g' v s))) s s (rel_prod rel_liftE (=))"
using g f unfolding L2_defs liftE_def
apply (clarsimp simp add: refines_def_old reaches_bind succeeds_bind rel_liftE_def
default_option_def Exn_def [symmetric]
split: xval_split exception_or_result_splits sum.splits)
apply (metis Exn_def default_option_def exception_or_result_cases option.exhaust_sel)+
done
lemma refines_L2_condition_reader:
assumes g [unfolded THIN_def]: "PROP THIN (Trueprop (refines g (gets g') s s (rel_prod rel_liftE (=))))"
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f (gets f') s s (rel_prod rel_liftE (=))))"
shows "refines (L2_condition c f g) (gets (λs. if c s then f' s else g' s)) s s (rel_prod rel_liftE (=))"
using g f unfolding L2_defs liftE_def
apply (auto simp add: refines_def_old reaches_bind succeeds_bind rel_liftE_def
default_option_def Exn_def [symmetric]
split: xval_split exception_or_result_splits sum.splits)
done
lemma refines_L2_try_L2_throw_reader:
shows "refines (L2_try (L2_throw (Inr r) ns)) (gets (L2_VARS (λ_. r) ns)) s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_VARS_def liftE_def
apply (auto simp add: refines_def_old reaches_try reaches_map_value rel_liftE_def map_exn_def
default_option_def Exn_def [symmetric]
split: xval_split exception_or_result_splits sum.splits)
done
lemma refines_L2_try_L2_seq_reader:
assumes g [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (L2_try (g v)) (gets (g' v)) t t (rel_prod rel_liftE (=)))"
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f (gets f') s s (rel_prod rel_liftE (=))))"
shows "refines (L2_try (L2_seq f g)) (gets (λs. let v = f' s in (g' v s))) s s (rel_prod rel_liftE (=))"
unfolding L2_defs try_def refines_map_value_left_iff gets_let_bind
apply (rule refines_bind [OF f])
subgoal by auto
subgoal by (auto simp add: default_option_def Exn_def [symmetric] rel_liftE_def)
subgoal by auto
subgoal using g [unfolded L2_defs try_def refines_map_value_left_iff ] by auto
done
lemma refines_L2_try_L2_condition_reader:
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines (L2_try f) (gets f') s s (rel_prod rel_liftE (=))))"
assumes g [unfolded THIN_def]: "PROP THIN (Trueprop (refines (L2_try g) (gets g') s s (rel_prod rel_liftE (=))))"
shows "refines (L2_try (L2_condition (c) f g)) (gets (λs. if c s then f' s else g' s)) s s (rel_prod rel_liftE (=))"
using f g unfolding L2_defs liftE_def
apply (auto simp add: refines_def_old reaches_try)
done
lemma refines_L2_try_reader:
assumes f: "refines f (gets f') s s (rel_prod rel_liftE (=))"
shows "refines (L2_try f) (gets f') s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_guarded_def try_def liftE_def using f
by (auto simp add: refines_def_old reaches_map_value rel_liftE_def unnest_exn_def split: xval_splits)
(metis Exn_def default_option_def exception_or_result_cases option.exhaust_sel)+
lemmas refines_monad_reader =
refines_L2_call_embed_reader [synthesize_rule reader and option and nondet and exit priority:410]
refines_L2_gets_reader [synthesize_rule reader and option and nondet and exit priority:410]
refines_lift_pure_reader [synthesize_rule reader and option and nondet and exit priority:440]
refines_L2_seq_reader [synthesize_rule reader and option and nondet and exit priority:410 split: g and g']
refines_L2_condition_reader [synthesize_rule reader and option and nondet and exit priority:410]
refines_L2_try_L2_throw_reader [synthesize_rule reader and option and nondet and exit priority:420]
refines_L2_try_L2_seq_reader [synthesize_rule reader and option and nondet and exit priority:420 split: g and g']
refines_L2_try_L2_condition_reader [synthesize_rule reader and option and nondet and exit priority:420]
refines_L2_try_reader [synthesize_rule reader and option and nondet and exit priority:410]
section ‹Option (Reader) Monad ›
lemma refines_lift_reader_option:
assumes f: "refines f (gets f') s s (rel_prod rel_liftE (=))"
shows "refines f (gets_the (ogets f')) s s (rel_prod rel_liftE (=))"
using f
apply (auto simp add: refines_def_old rel_liftE_def ogets_def)
done
lemma refines_L2_call_embed_option:
assumes f: "refines f (gets_the f') s s (rel_prod rel_liftE (=))"
shows "refines (L2_call f emb ns) (gets_the (L2_VARS f' ns)) s s (rel_prod rel_liftE (=))"
unfolding L2_VARS_def L2_call_def L2_defs using f
apply (clarsimp simp add: refines_def_old reaches_map_value map_exn_def rel_liftE_def split: xval_splits)
apply (metis Exn_def default_option_def exception_or_result_cases option.exhaust_sel)+
done
lemma refines_L2_gets_option:
"refines (L2_gets v ns) (gets_the (L2_VARS (ogets v) ns)) s s (rel_prod rel_liftE (=))"
unfolding L2_VARS_def L2_defs liftE_def
apply (auto simp add: refines_def_old rel_liftE_def ogets_def)
done
lemma refines_L2_seq_option:
assumes g [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (g v) (gets_the (g' v)) t t (rel_prod rel_liftE (=)))"
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f (gets_the f') s s (rel_prod rel_liftE (=))))"
shows "refines (L2_seq f g) (gets_the (f' |>> g')) s s (rel_prod rel_liftE (=))"
using g f unfolding L2_defs obind_def [abs_def]
by (fastforce simp add: refines_def_old reaches_bind succeeds_bind rel_liftE_def split: xval_splits option.splits)
lemma refines_L2_condition_option:
assumes g [unfolded THIN_def]: "PROP THIN (Trueprop (refines g (gets_the g') s s (rel_prod rel_liftE (=))))"
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f (gets_the f') s s (rel_prod rel_liftE (=))))"
shows "refines (L2_condition c f g) (gets_the (ocondition c f' g')) s s (rel_prod rel_liftE (=))"
using g f unfolding L2_defs ocondition_def
by (auto simp add: refines_def_old rel_liftE_def split: xval_splits option.splits)
lemma refines_L2_try_L2_throw_option:
shows "refines (L2_try (L2_throw (Inr r) ns)) (gets_the (L2_VARS (oreturn r) ns)) s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_VARS_def oreturn_def K_def
by (auto simp add: refines_def_old reaches_try unnest_exn_def rel_liftE_def split: xval_splits)
lemma refines_L2_try_L2_seq_option:
assumes g [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (L2_try (g v)) (gets_the (g' v)) t t (rel_prod rel_liftE (=)))"
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f (gets_the f') s s (rel_prod rel_liftE (=))))"
shows "refines (L2_try (L2_seq f g)) (gets_the (f' |>> g')) s s (rel_prod rel_liftE (=))"
unfolding L2_defs try_def refines_map_value_left_iff
apply (simp add: gets_the_obind)
apply (rule refines_bind [OF f])
subgoal by auto
subgoal by (auto simp add: default_option_def Exn_def [symmetric] rel_liftE_def)
subgoal by auto
subgoal using g [simplified L2_defs try_def refines_map_value_left_iff] by auto
done
lemma refines_L2_try_L2_condition_option:
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines (L2_try f) (gets_the f') s s (rel_prod rel_liftE (=))))"
assumes g [unfolded THIN_def]: "PROP THIN (Trueprop (refines (L2_try g) (gets_the g') s s (rel_prod rel_liftE (=))))"
shows "refines (L2_try (L2_condition c f g)) (gets_the (ocondition c f' g')) s s (rel_prod rel_liftE (=))"
using f g unfolding L2_defs ocondition_def
apply (auto simp add: refines_def_old reaches_try)
done
lemma refines_L2_try_option:
assumes f: "refines f (gets_the f') s s (rel_prod rel_liftE (=))"
shows "refines (L2_try f) (gets_the f') s s (rel_prod rel_liftE (=))"
unfolding L2_defs using f
apply (clarsimp simp add: refines_def_old reaches_try unnest_exn_def rel_liftE_def split: xval_splits)
apply (metis Exn_def default_option_def exception_or_result_cases not_None_eq)+
done
lemma le_whileLoop_succeeds_terminatesI:
assumes "⋀s. run (whileLoop C B r) s ≠ ⊤ ⟹ run f s ≤ run (whileLoop C B r) s"
shows "f ≤ whileLoop C B r"
proof (rule le_spec_monad_runI)
fix s
show "run f s ≤ run (whileLoop C B r) s"
proof (cases "run (whileLoop C B r) s = ⊤")
case False then show ?thesis by (rule assms)
qed simp
qed
lemma gets_the_whileLoop:
fixes C :: "'a ⇒ 's ⇒ bool"
shows "whileLoop C (λa. gets_the (B a)) r =
((gets_the (owhile C B r))::('e::default, 'a, 's) spec_monad)"
proof (rule antisym)
show "(whileLoop C (λa. Spec_Monad.gets_the (B a)) r::('e, 'a, 's) spec_monad) ≤
Spec_Monad.gets_the (owhile C B r)"
proof -
{
fix s v
assume "(Some r, Some v) ∈ option_while' (λa. C a s) (λa. B a s)"
then have "run ((whileLoop C (λa. Spec_Monad.gets_the (B a)) r)::('e, 'a, 's) spec_monad) s ≤ Success {(Result v, s)}"
proof (induct "Some r" "Some v" arbitrary: r )
assume "¬ C v s"
then
show "run (whileLoop C (λa. Spec_Monad.gets_the (B a)) v) s ≤ Success {(Result v, s)}"
by (subst whileLoop_unroll) simp
next
fix r r'
assume "C r s"
and "B r s = Some r'"
and "(Some r', Some v) ∈ option_while' (λa. C a s) (λa. B a s)"
and "run ((whileLoop C (λa. Spec_Monad.gets_the (B a)) r')::('e, 'a, 's) spec_monad) s ≤ Success {(Result v, s)}"
thus "run ((whileLoop C (λa. Spec_Monad.gets_the (B a)) r)::('e, 'a, 's) spec_monad) s ≤ Success {(Result v, s)}"
by (subst whileLoop_unroll) (simp add: run_bind)
qed
} note * = this
show ?thesis
apply (rule le_spec_monad_runI)
apply simp
apply (clarsimp simp add: owhile_def option_while_def option_while'_THE pure_post_state_def
split: option.splits)
by (rule *)
qed
next
show "Spec_Monad.gets_the (owhile C B r) ≤ ((whileLoop C (λa. Spec_Monad.gets_the (B a)) r)::('e, 'a, 's) spec_monad)"
proof (rule le_whileLoop_succeeds_terminatesI)
fix s
assume "run (whileLoop C (λa. Spec_Monad.gets_the (B a)) r) s ≠ ⊤"
then show "run (Spec_Monad.gets_the (owhile C B r)) s
≤ run ((whileLoop C (λa. Spec_Monad.gets_the (B a)) r)::('e, 'a, 's) spec_monad) s"
proof (induction rule: whileLoop_ne_top_induct)
case (step a s) then show ?case
apply (subst owhile_unroll)
apply (subst whileLoop_unroll)
apply (auto simp add: gets_the_obind gets_the_ocondition gets_the_oreturn run_condition
run_bind runs_to_holds_def
split: option.split)
done
qed
qed
qed
lemma refines_L2_while_option:
assumes f [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (b v) (gets_the (b' v)) t t (rel_prod rel_liftE (=)))"
shows "refines (L2_while c b i ns) (gets_the (L2_VARS (owhile c b' i) ns)) s s (rel_prod rel_liftE (=))"
unfolding L2_while_def L2_VARS_def gets_the_whileLoop[symmetric]
apply (rule refines_whileLoop)
using f
apply (simp_all add: rel_liftE_def)
done
lemma refines_L2_fail_option:
shows "refines L2_fail (gets_the ofail) s s (rel_prod rel_liftE (=))"
unfolding L2_defs
by (auto simp add: refines_def_old)
lemma refines_L2_guard_option:
shows "refines (L2_guard g) (gets_the (oguard g)) s s (rel_prod rel_liftE (=))"
unfolding L2_defs
by (auto simp add: refines_def_old oguard_def)
lemma refines_L2_guarded:
assumes f: "g s ⟹ refines f (gets_the f') s s (rel_prod rel_liftE (=))"
shows "refines (L2_guarded g f) (gets_the (oguard g |>> (λ_. f'))) s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_guarded_def using f
by (auto simp add: refines_def_old reaches_bind succeeds_bind obind_def oguard_def split: option.splits)
lemmas refines_monad_option =
refines_lift_reader_option [synthesize_rule option priority:350]
refines_L2_call_embed_option [synthesize_rule option priority:310]
refines_L2_gets_option [synthesize_rule option priority:310]
refines_L2_seq_option [synthesize_rule option priority:310 split: g and g']
refines_L2_condition_option [synthesize_rule option priority:310]
refines_L2_try_L2_throw_option [synthesize_rule option priority:320]
refines_L2_try_L2_seq_option [synthesize_rule option priority:320 split: g and g']
refines_L2_try_L2_condition_option [synthesize_rule option priority:320]
refines_L2_try_option [synthesize_rule option priority:310]
refines_L2_while_option [synthesize_rule option priority:310 split: b and b']
refines_L2_fail_option [synthesize_rule option priority:310]
refines_L2_guard_option [synthesize_rule option priority:310]
refines_L2_guarded [synthesize_rule option priority:310]
section ‹Nondet Monad›
text ‹Note that \<^const>‹L2_catch› is already replaced by \<^const>‹L2_try› during exception rewriting in phase L2.›
lemma refines_L2_call_embed_nondet:
assumes f: "refines f f' s s (rel_prod rel_liftE (=))"
shows "refines (L2_call f emb ns) (L2_VARS f' ns) s s (rel_prod rel_liftE (=))"
using f unfolding L2_call_def L2_VARS_def
apply (clarsimp simp add: refines_def_old reaches_map_value map_exn_def rel_liftE_def split: xval_splits)
by (metis Exn_def default_option_def exception_or_result_cases option.exhaust_sel)
lemma refines_L2_call_embed_exn:
assumes f: "refines f f' s s (rel_prod rel_liftE (=))"
shows "refines (L2_call f emb ns) (liftE (L2_VARS f' ns)) s s (rel_prod (rel_xval L (=)) (=))"
using f unfolding L2_call_def L2_VARS_def
apply (clarsimp simp add: refines_def_old reaches_map_value map_exn_def reaches_liftE
rel_liftE_def rel_xval.simps split: xval_splits)
by (metis Exn_def default_option_def exception_or_result_cases option.exhaust_sel)
lemma refines_liftE_exn:
assumes f: "refines f f' s s (rel_prod rel_liftE (=))"
shows "refines f (liftE f') s s (rel_prod (rel_xval L (=)) (=))"
using f
by (fastforce simp add: refines_def_old reaches_map_value map_exn_def reaches_liftE
rel_liftE_def rel_xval.simps split: xval_splits)
lemma refines_L2_seq_nondet_polymorphic:
assumes r [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (g v) (g' v) t t (rel_prod rel_liftE (=)))"
assumes f [unfolded THIN_def, rule_format]: "PROP THIN (Trueprop (refines f f' s s (rel_prod rel_liftE (=))))"
shows "refines (L2_seq f g) (bind f' g') s s (rel_prod rel_liftE (=))"
unfolding L2_seq_def
apply (rule refines_bind [OF f])
apply (auto simp add: r rel_liftE_def)
done
lemma refines_L2_seq_nondet:
fixes f':: "('a, 's) res_monad"
assumes r [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (g v) (g' v) t t (rel_prod rel_liftE (=)))"
assumes f [unfolded THIN_def, rule_format]: "PROP THIN (Trueprop (refines f f' s s (rel_prod rel_liftE (=))))"
shows "refines (L2_seq f g) ((bind f' g')::('b, 's) res_monad) s s (rel_prod rel_liftE (=))"
using assms
by (rule refines_L2_seq_nondet_polymorphic)
lemma refines_L2_seq_exn:
assumes g [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (g v) (g' v) t t (rel_prod (rel_xval L (=)) (=)))"
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f f' s s (rel_prod (rel_xval L (=)) (=))))"
shows "refines (L2_seq f g) (bind f' g') s s (rel_prod (rel_xval L (=)) (=))"
unfolding L2_seq_def
apply (rule refines_bind [OF f])
apply (auto simp add: g rel_xval.simps default_option_def Exn_def)
done
lemma refines_try_bind_rel_liftE':
assumes g : "⋀v s t. S s t ⟹ refines (try (g v)) (g' v) s t (rel_prod rel_liftE S)"
assumes f: "refines f f' s t (rel_prod rel_liftE S)"
shows "refines (try (bind f g)) (bind f' g') s t (rel_prod rel_liftE S)"
unfolding try_def refines_map_value_left_iff
apply (rule refines_bind [OF f])
subgoal by auto
subgoal by (auto simp add: default_option_def Exn_def [symmetric] rel_liftE_def)
subgoal by auto
subgoal
using g [simplified L2_defs try_def refines_map_value_left_iff]
by auto
done
lemma refines_try_bind_rel_liftE:
assumes g : "⋀v t. refines (try (g v)) (g' v) t t (rel_prod rel_liftE (=))"
assumes f: "refines f f' s s (rel_prod rel_liftE (=))"
shows "refines (try (bind f g)) (bind f' g') s s (rel_prod rel_liftE (=))"
apply (rule refines_try_bind_rel_liftE' [OF _ f])
using g by simp
lemma refines_L2_try_L2_seq_nondet:
assumes g [unfolded THIN_def L2_defs, rule_format]: "PROP THIN (⋀v t. refines (L2_try (g v)) (g' v) t t (rel_prod rel_liftE (=)))"
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f f' s s (rel_prod rel_liftE (=))))"
shows "refines (L2_try (L2_seq f g)) (bind f' g') s s (rel_prod rel_liftE (=))"
unfolding L2_defs using g f
by (rule refines_try_bind_rel_liftE)
lemma refines_L2_try_L2_condition_nondet:
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines (L2_try f) f' s s (rel_prod rel_liftE (=))))"
assumes g [unfolded THIN_def]: "PROP THIN (Trueprop (refines (L2_try g) g' s s (rel_prod rel_liftE (=))))"
shows "refines (L2_try (L2_condition c f g)) (condition c f' g') s s (rel_prod rel_liftE (=))"
using f g unfolding L2_defs
apply (auto simp add: refines_def_old succeeds_condition_iff reaches_condition_iff reaches_try)
done
lemma refines_L2_try_rel_LiftE_nondet:
assumes f: "refines f f' s s (rel_prod rel_liftE (=))"
shows "refines (L2_try f) f' s s (rel_prod rel_liftE (=))"
using f unfolding L2_defs
apply (clarsimp simp add: refines_def_old reaches_try rel_liftE_def unnest_exn_def split: xval_splits)
by (metis Exn_def default_option_def exception_or_result_cases option.exhaust_sel)
lemma refines_try_finally_rel_liftE:
assumes f: "refines f f' s s (rel_prod (rel_xval rel_liftE' (=)) (=))"
shows "refines (try f) (finally f') s s (rel_prod rel_liftE (=))"
using f unfolding try_def finally_def
apply (rule refines_map_value)
apply (auto simp add: unnest_exn_def unite_def rel_liftE'_def split: xval_splits sum.splits)
done
lemma refines_L2_try_finally_nondet:
assumes f: "refines f f' s s (rel_prod (rel_xval rel_liftE' (=)) (=))"
shows "refines (L2_try f) (finally f') s s (rel_prod rel_liftE (=))"
using f unfolding L2_defs
by (rule refines_try_finally_rel_liftE)
lemma refines_L2_try_exn:
assumes f: "refines f f' s s (rel_prod (rel_xval (rel_sum L (=)) (=)) (=))"
shows "refines (L2_try f) (try f') s s (rel_prod (rel_xval L (=)) (=))"
using f unfolding L2_defs try_def
apply (rule refines_map_value)
apply (auto simp add: unnest_exn_def split: xval_splits sum.splits)
done
lemma refines_L2_condition_nondet:
assumes g [unfolded THIN_def]: "PROP THIN (Trueprop (refines g g' s s (rel_prod V (=))))"
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines f f' s s (rel_prod V (=))))"
shows "refines (L2_condition c f g) (condition c f' g') s s (rel_prod V (=))"
unfolding L2_condition_def using g f
apply (auto intro: refines_condition)
done
lemma refines_L2_while_nondet:
assumes b [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (b v) (b' v) t t (rel_prod rel_liftE (=)))"
shows "refines (L2_while c b i ns) (L2_VARS (whileLoop c b' i) ns) s s (rel_prod rel_liftE (=))"
unfolding L2_while_def L2_VARS_def
apply (rule refines_whileLoop'')
subgoal
by (auto)
subgoal
by (auto intro: b)
subgoal
by auto
subgoal
by (auto simp add: rel_liftE_def rel_exception_or_result.simps)
done
lemma refines_L2_while_exn:
assumes b [unfolded THIN_def, rule_format]: "PROP THIN (⋀v t. refines (b v) (b' v) t t (rel_prod (rel_xval L (=)) (=)))"
shows "refines (L2_while c b i ns) (L2_VARS (whileLoop c b' i) ns) s s (rel_prod ((rel_xval L (=))) (=))"
unfolding L2_while_def L2_VARS_def
apply (rule refines_whileLoop_exn)
apply (auto simp add: b)
done
lemma refines_L2_unknown_nondet:
shows "refines (L2_unknown ns) (L2_VARS (select UNIV) ns) s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_VARS_def
apply (auto intro: refines_select)
done
lemma refines_L2_unknown_exn:
shows "refines (L2_unknown ns) (L2_VARS (select UNIV) ns) s s (rel_prod (rel_xval L (=)) (=))"
unfolding L2_defs L2_VARS_def
apply (auto intro: refines_select)
done
lemma refines_L2_modify_nondet:
shows "refines (L2_modify f) (modify f) s s (rel_prod rel_liftE (=))"
unfolding L2_defs
apply (auto intro: refines_modify)
done
lemma refines_L2_gets_nondet:
shows "refines (L2_gets f ns) (L2_VARS (gets f) ns) s s (rel_prod rel_liftE (=))"
unfolding L2_defs L2_VARS_def
apply (auto intro: refines_gets)
done
lemma refines_L2_throw_exn:
"L x x' ⟹
refines (L2_throw x ns) (L2_VARS (throw x') ns) s s (rel_prod (rel_xval L (=)) (=))"
unfolding L2_throw_def L2_VARS_def
apply (auto simp add: refines_def_old rel_xval.simps Exn_def)
done
lemma refines_L2_spec_nondet:
shows "refines (L2_spec r) (assert_result_and_state (λs. {(v, t). (s, t) ∈ r})) s s (rel_prod rel_liftE (=))"
unfolding L2_defs
apply (auto simp add: refines_def_old reaches_bind succeeds_bind)
done
lemma refines_L2_assume_nondet:
shows "refines (L2_assume r) (assume_result_and_state r) s s (rel_prod rel_liftE (=))"
unfolding L2_defs
apply (auto simp add: refines_def_old reaches_bind succeeds_bind)
done
lemma refines_L2_guard_nondet:
shows "refines (L2_guard c) (guard c) s s (rel_prod rel_liftE (=))"
unfolding L2_defs
by (auto intro: refines_guard)
lemma refines_L2_guarded_nondet:
assumes f: "c s ⟹ refines f f' s s (rel_prod rel_liftE (=))"
shows "refines (L2_guarded c f) (bind (guard c) (λ_. f')) s s (rel_prod rel_liftE (=))"
unfolding L2_guarded_def L2_seq_def L2_guard_def using f
apply (auto simp add: refines_def_old succeeds_bind reaches_bind)
done
lemma refines_L2_guarded_exn:
assumes f: "c s ⟹ refines f f' s s (rel_prod (rel_xval L (=)) (=))"
shows "refines (L2_guarded c f) (bind (guard c) (λ_. f')) s s (rel_prod (rel_xval L (=)) (=))"
unfolding L2_guarded_def L2_seq_def L2_guard_def using f
apply (auto simp add: refines_def_old succeeds_bind reaches_bind)
done
lemma refines_L2_fail_nondet:
shows "refines L2_fail fail s s (rel_prod R (=))"
by simp
lemma refines_exec_concrete_gen_nondet:
assumes f: "⋀s. refines f f' s s (rel_prod R (=))"
shows "refines (exec_concrete st f) (exec_concrete st f') s s (rel_prod R (=))"
using f
by (fastforce simp add: refines_def_old reaches_exec_concrete succeeds_exec_concrete_iff)
lemmas refines_exec_concrete_nondet = refines_exec_concrete_gen_nondet [where R="rel_liftE"]
lemmas refines_exec_concrete_exit = refines_exec_concrete_gen_nondet [where R="rel_xval L (=)"] for L
lemma refines_exec_abstract_gen_nondet:
assumes f: "⋀s. refines f f' s s (rel_prod R (=))"
shows "refines (exec_abstract st f) (exec_abstract st f') s s (rel_prod R (=))"
using f
by (fastforce simp add: refines_def_old reaches_exec_abstract)
lemmas refines_exec_abstract_nondet = refines_exec_abstract_gen_nondet [where R="rel_liftE"]
lemmas refines_exec_abstract_exit = refines_exec_abstract_gen_nondet [where R="rel_xval L (=)"] for L
lemma rel_map_ResultI:
"rel_map Result x (Result x)"
by (simp add: rel_map_def)
lemma rel_map_to_xval_InlI:
"rel_map to_xval (Inl l) (Exn l)"
by (simp add: rel_map_def)
lemma rel_map_to_xval_InrI:
"rel_map to_xval (Inr r) (Result r)"
by (simp add: rel_map_def)
lemma refines_rel_prod_eq_guard_on_exit:
assumes f: "refines f⇩c f⇩a s s (rel_prod Q (=))"
shows "refines
(guard_on_exit f⇩c grd cleanup)
(guard_on_exit f⇩a grd cleanup) s s
(rel_prod Q (=))"
unfolding guard_on_exit_bind_exception_or_result_conv
apply (rule refines_bind_exception_or_result_strong [OF f])
apply clarsimp
apply (rule refines_bind_no_throw [where Q="rel_prod ⊤ (=)"] )
apply simp
apply simp
apply (rule refines_guard)
apply simp
apply simp
apply (rule refines_bind_no_throw )
apply simp
apply simp
apply (clarsimp)
apply (rule refines_state_select_same)
apply clarsimp
done
lemma refines_rel_prod_eq_assume_on_exit:
assumes f: "refines f⇩c f⇩a s s (rel_prod Q (=))"
shows "refines
(assume_on_exit f⇩c grd cleanup)
(assume_on_exit f⇩a grd cleanup) s s
(rel_prod Q (=))"
unfolding assume_on_exit_bind_exception_or_result_conv
apply (rule refines_bind_exception_or_result_strong [OF f])
apply clarsimp
apply (rule refines_bind_no_throw [where Q="rel_prod ⊤ (=)"] )
apply simp
apply simp
subgoal
by (auto simp add: refines_def_old)
apply (rule refines_bind_no_throw )
apply simp
apply simp
apply (clarsimp)
apply (rule refines_state_select_same)
apply clarsimp
done
context stack_heap_state
begin
thm refines_rel_prod_with_fresh_stack_ptr
lemma refines_rel_prod_L2_try_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (L2_try (f⇩c p)) (f⇩a p) s s (rel_prod Q (=))"
shows
"refines
(L2_try (with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm)))
(with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod Q (=))"
apply (simp add: L2_try_with_fresh_stack_ptr L2_VARS_def)
apply (rule refines_rel_prod_with_fresh_stack_ptr [unfolded L2_VARS_def])
apply (rule init_eq)
apply (rule f)
done
end
context typ_heap_typing
begin
lemma refines_rel_prod_guard_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (f⇩c p) (f⇩a p) s s (rel_prod L (=))"
shows
"refines
(guard_with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))
(guard_with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod L (=))"
apply (simp add: guard_with_fresh_stack_ptr_def L2_VARS_def assume_stack_alloc_def)
apply (rule refines_bind')
apply (subst refines_assume_result_and_state_iff)
apply (subst init_eq)
apply (intro sim_set_refl)
apply clarsimp
apply (rule refines_on_exit')
apply (rule refines_weaken[OF f])
apply simp
apply (rule refines_bind'[OF refines_guard])
apply simp_all
apply (rule refines_assert_result_and_state)
apply auto
done
lemma refines_rel_prod_assume_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (f⇩c p) (f⇩a p) s s (rel_prod L (=))"
shows
"refines
(assume_with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))
(assume_with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod L (=))"
apply (simp add: assume_with_fresh_stack_ptr_def L2_VARS_def assume_stack_alloc_def)
apply (rule refines_bind')
apply (subst refines_assume_result_and_state_iff)
apply (subst init_eq)
apply (intro sim_set_refl)
apply clarsimp
apply (rule refines_on_exit')
apply (rule refines_weaken[OF f])
apply simp
apply (rule refines_bind'[OF refines_assuming])
apply simp_all
apply (rule refines_assert_result_and_state)
apply auto
done
lemma refines_rel_prod_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (f⇩c p) (f⇩a p) s s (rel_prod L (=))"
shows
"refines
(with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm))
(with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod L (=))"
apply (simp add: with_fresh_stack_ptr_def L2_VARS_def assume_stack_alloc_def)
apply (rule refines_bind_no_throw )
apply simp
apply simp
apply (rule refines_assume_result_and_state_same')
apply (simp only: init_eq)
apply clarsimp
apply (rule refines_rel_prod_eq_on_exit)
apply (rule f)
done
lemma refines_rel_prod_L2_try_guard_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (L2_try (f⇩c p)) (f⇩a p) s s (rel_prod L (=))"
shows
"refines
(L2_try (guard_with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm)))
(guard_with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod L (=))"
apply (simp add: L2_try_guard_with_fresh_stack_ptr L2_VARS_def)
apply (rule refines_rel_prod_guard_with_fresh_stack_ptr [unfolded L2_VARS_def])
apply (rule init_eq)
apply (rule f)
done
lemma refines_rel_prod_L2_try_assume_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (L2_try (f⇩c p)) (f⇩a p) s s (rel_prod L (=))"
shows
"refines
(L2_try (assume_with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm)))
(assume_with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod L (=))"
apply (simp add: L2_try_assume_with_fresh_stack_ptr L2_VARS_def)
apply (rule refines_rel_prod_assume_with_fresh_stack_ptr [unfolded L2_VARS_def])
apply (rule init_eq)
apply (rule f)
done
lemma refines_rel_prod_L2_try_with_fresh_stack_ptr:
assumes init_eq: "init⇩c s = init⇩a s"
assumes f: "⋀s p. refines (L2_try (f⇩c p)) (f⇩a p) s s (rel_prod L (=))"
shows
"refines
(L2_try (with_fresh_stack_ptr n init⇩c (L2_VARS f⇩c nm)))
(with_fresh_stack_ptr n init⇩a (L2_VARS f⇩a nm)) s s
(rel_prod L (=))"
apply (simp add: L2_try_with_fresh_stack_ptr L2_VARS_def)
apply (rule refines_rel_prod_with_fresh_stack_ptr [unfolded L2_VARS_def])
apply (rule init_eq)
apply (rule f)
done
end
lemma relcomppI_swapped: "s b c ⟹ r a b ⟹ (r OO s) a c"
by (rule relcomppI)
lemmas refines_monad_nondet =
refines_L2_call_embed_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_call_embed_exn [synthesize_rule nondet and exit priority:210]
refines_liftE_exn [synthesize_rule nondet and exit priority:250]
refines_L2_seq_nondet [synthesize_rule nondet and exit priority:210 split: g and g']
refines_L2_seq_exn [synthesize_rule nondet and exit priority:210 split: g and g']
refines_L2_try_L2_seq_nondet [synthesize_rule nondet and exit priority:230 split: g and g']
refines_L2_try_L2_condition_nondet [synthesize_rule nondet and exit priority:230]
refines_L2_try_rel_LiftE_nondet [synthesize_rule nondet and exit priority:220]
refines_L2_try_finally_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_try_exn [synthesize_rule nondet and exit priority:210]
refines_L2_condition_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_while_nondet [synthesize_rule nondet and exit priority:210 split: b and b']
refines_L2_while_exn [synthesize_rule nondet and exit priority:210 split: b and b']
refines_L2_unknown_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_unknown_exn [synthesize_rule nondet and exit priority:210]
refines_L2_modify_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_gets_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_throw_exn [synthesize_rule nondet and exit priority:210]
refines_L2_spec_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_assume_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_guard_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_guarded_nondet [synthesize_rule nondet and exit priority:210]
refines_L2_guarded_exn [synthesize_rule nondet and exit priority:210]
refines_L2_fail_nondet [synthesize_rule nondet and exit priority:210]
refines_exec_concrete_nondet [synthesize_rule nondet and exit priority:210]
refines_exec_concrete_exit [synthesize_rule nondet and exit priority:210]
refines_exec_abstract_nondet [synthesize_rule nondet and exit priority:210]
refines_exec_abstract_exit [synthesize_rule nondet and exit priority:210]
rel_liftE_trivial [synthesize_rule nondet and exit priority:210]
rel_liftE'_Inr [synthesize_rule nondet and exit priority:210]
rel_sum_Inl [synthesize_rule nondet and exit priority:210]
rel_sum_Inr [synthesize_rule nondet and exit priority:210]
rel_xval_Exn [synthesize_rule nondet and exit priority:210]
rel_xval_Result [synthesize_rule nondet and exit priority:210]
relcomppI_swapped [synthesize_rule nondet and exit priority:210]
rel_map_ResultI [synthesize_rule nondet and exit priority:210]
rel_map_to_xval_InlI [synthesize_rule nondet and exit priority:210]
rel_map_to_xval_InrI [synthesize_rule nondet and exit priority:210]
refl [synthesize_rule nondet and exit priority: 210]
context typ_heap_typing
begin
lemmas refines_monad_nondet =
refines_rel_prod_L2_try_guard_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:232]
refines_rel_prod_L2_try_assume_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:232]
refines_rel_prod_L2_try_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:232]
refines_rel_prod_guard_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:210]
refines_rel_prod_assume_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:210]
refines_rel_prod_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:210]
refines_rel_xval_guard_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:210]
refines_rel_xval_assume_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:210]
refines_rel_xval_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:210]
end
context stack_heap_state
begin
lemmas refines_nondet_monad =
refines_rel_prod_L2_try_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:232]
refines_rel_prod_with_fresh_stack_ptr [synthesize_rule nondet and exit priority:210]
end
add_synthesize_pattern nondet and exit where
rel_throwE_nondet_synth = ‹Trueprop (rel_throwE _ ?x ?x')› (x')
subsection ‹Elimination of ‹L2_try› in the Error Monad›
subsubsection ‹Eliminate Inner Exception›
text ‹rules for elimination of ‹L2_try› when the inner exception layer is not needed, i.e.,
‹rel_sum (rel_throwE L) (=)››
lemma bind_bind_exception_or_result_conv:
"(f ⤜ g) = (bind_exception_or_result f (λException e ⇒ yield (Exception e) | Result v ⇒ g v))"
apply (rule spec_monad_eqI)
apply (clarsimp simp add: runs_to_iff)
apply (auto simp add: runs_to_def_old split: exception_or_result_splits)
done
lemma rel_throwE'_rel_throwE_conv: "rel_throwE' L = (rel_map to_xval OO rel_throwE L)"
apply (rule ext)+
apply (auto simp add: rel_throwE_def rel_throwE'_def rel_xval.simps relcompp.simps
rel_map_def to_xval_def split: sum.splits)
done
lemma "rel_throwE (rel_throwE' L) = (rel_throwE (rel_map to_xval OO rel_throwE L))"
apply (rule ext)+
apply (auto simp add: rel_throwE_def rel_throwE'_def rel_xval.simps relcompp.simps
rel_map_def to_xval_def split: sum.splits)
done
lemma refines_L2_try_L2_seq_exn:
fixes f::" (('b + 'c), 'f, 'a) exn_monad"
and g::"'f ⇒ ( ('b + 'c), 'c, 'a) exn_monad"
assumes g [unfolded THIN_def L2_defs, rule_format]:
"PROP THIN (⋀v t. refines (L2_try (g v)) (g' v) t t (rel_prod ((rel_xval L R)) (=)))"
assumes f [unfolded THIN_def]:
"PROP THIN (Trueprop (refines f f' s s (rel_prod (rel_xval (rel_throwE' L) (=)) (=))))"
shows "refines (L2_try (L2_seq f g)) (bind f' g') s s (rel_prod (rel_xval L R) (=))"
unfolding L2_try_def L2_seq_def try_nested_bind_exception_or_result_conv
apply (simp add: bind_bind_exception_or_result_conv)
apply (rule refines_bind_exception_or_result)
apply (rule refines_weaken [OF f])
apply (auto split: xval_splits sum.splits simp: rel_xval.simps rel_prod.simps g)
done
lemma refines_L2_try_L2_condition_exit:
assumes f [unfolded THIN_def]: "PROP THIN (Trueprop (refines (L2_try f) f' s s (rel_prod R (=))))"
assumes g [unfolded THIN_def]: "PROP THIN (Trueprop (refines (L2_try g) g' s s (rel_prod R (=))))"
shows "refines (L2_try (L2_condition c f g)) (condition c f' g') s s (rel_prod R (=))"
using f g unfolding L2_defs L2_try_def
apply (auto simp add: refines_def_old succeeds_condition_iff reaches_condition_iff reaches_try)
done
lemma refines_try_rel_xval_rel_throwE':
assumes "refines f f' s s (rel_prod (rel_xval (rel_throwE' A) B) S)"
shows "refines (try f) f' s s (rel_prod (rel_xval A B) S)"
unfolding try_def refines_map_value_left_iff
apply (rule refines_weaken [OF assms])
apply (auto simp add: unnest_exn_def rel_xval.simps split: xval_splits sum.splits )
done
lemma refines_L2_try_rel_sum_rel_throwE_nondet:
assumes "refines f f' s s (rel_prod (rel_xval (rel_throwE' A) B) (=))"
shows "refines (L2_try f) f' s s (rel_prod (rel_xval A B) (=))"
using assms unfolding L2_defs
by (rule refines_try_rel_xval_rel_throwE')
lemma refines_try_rel_throwE:
assumes "refines f f' s s (rel_prod (rel_throwE (rel_throwE' L)) S)"
shows "refines (try f) f' s s (rel_prod (rel_throwE L) S)"
unfolding try_def
apply (simp add: refines_map_value_left_iff)
apply (rule refines_weaken [OF assms])
apply (auto simp add: unnest_exn_def split: xval_splits sum.splits)
done
lemma refines_L2_try_rel_throwE_nondet:
assumes "refines f f' s s (rel_prod (rel_throwE (rel_throwE' L)) (=))"
shows "refines (L2_try f) f' s s (rel_prod (rel_throwE L) (=))"
using assms unfolding L2_defs
by (rule refines_try_rel_throwE)
lemmas ts_L2_try_inner_exception =
rel_throwE'_Inl[synthesize_rule nondet and exit]
rel_throwE_Exn[synthesize_rule nondet and exit]
refines_L2_try_L2_seq_exn [synthesize_rule nondet and exit priority: 218 split: g and g']
refines_L2_try_L2_condition_exit [synthesize_rule nondet and exit priority: 218]
refines_L2_try_rel_throwE_nondet [synthesize_rule nondet and exit priority: 216]
refines_L2_try_rel_sum_rel_throwE_nondet [synthesize_rule nondet and exit priority: 215]
bundle del_ts_L2_try_inner_exception =
rel_throwE'_Inl[synthesize_rule nondet and exit del]
rel_throwE_Exn[synthesize_rule nondet and exit del]
refines_L2_try_L2_seq_exn [synthesize_rule nondet and exit priority: 218 split: g and g' del]
refines_L2_try_L2_condition_exit [synthesize_rule nondet and exit priority: 218 del]
refines_L2_try_rel_throwE_nondet [synthesize_rule nondet and exit priority: 216 del]
refines_L2_try_rel_sum_rel_throwE_nondet [synthesize_rule nondet and exit priority: 215 del]
print_synthesize_rules exit ‹Trueprop (refines (L2_seq _ _) _ _ _ (rel_prod rel_liftE (=))) ›
subsubsection ‹Eliminate ‹L2_try› over exiting branches›
text ‹
Eliminate ‹L2_try› over a condition, when one branch always exits (‹rel_throwE (rel_sum L R)›)
›
lemma rel_map_to_xval_rel_xval_rel_sum_conv:
"rel_map to_xval OO rel_xval L R = rel_sum L R OO rel_map to_xval"
apply (rule ext)+
apply (auto simp add: rel_sum.simps rel_xval.simps relcompp.simps
rel_map_def to_xval_def split: sum.splits)
done
lemma refines_L2_try_L2_seq_L2_condition_exit1:
assumes g [unfolded THIN_def]:
"PROP THIN (Trueprop (refines (L2_try (L2_seq g h)) gh' s s (rel_prod LR (=))))"
assumes f [unfolded THIN_def]:
"PROP THIN (Trueprop (refines f f' s s (rel_prod (rel_throwE (rel_map to_xval OO LR)) (=))))"
shows "refines (L2_try (L2_seq (L2_condition c f g) h)) (condition c f' gh') s s (rel_prod LR (=))"
using g f
apply (simp add: L2_defs try_def refines_map_value_left_iff refines_condition_bind_left
refines_condition_false)
apply (intro impI refines_condition_true)
apply assumption
subgoal premises prems
proof -
have "refines (f >>= h) (f' ⤜ return) s s (λ(x, s) (y, t). LR (unnest_exn x) y ∧ s = t)"
apply (intro refines_bind[OF prems(2)])
apply (auto simp: rel_throwE_def rel_map_def unnest_exn_def
split: xval_splits sum.splits)
done
then show ?thesis by simp
qed
done
lemma refines_L2_try_L2_seq_L2_condition_exit2:
assumes f [unfolded THIN_def]:
"PROP THIN (Trueprop (refines (L2_try (L2_seq f h)) fh' s s (rel_prod LR (=))))"
assumes g [unfolded THIN_def]:
"PROP THIN (Trueprop (refines g g' s s (rel_prod (rel_throwE (rel_map to_xval OO LR)) (=))))"
shows "refines (L2_try (L2_seq (L2_condition c f g) h)) (condition c fh' g') s s (rel_prod LR (=))"
using assms
unfolding L2_defs
apply (subst (1 2) condition_swap)
apply (erule (1) refines_L2_try_L2_seq_L2_condition_exit1[unfolded L2_defs])
done
lemma refines_L2_seq_L2_condition_rel_throwE1:
assumes g [unfolded THIN_def]:
"PROP THIN (Trueprop (refines (L2_seq g h) gh' s s (rel_prod (rel_throwE LR)(=))))"
assumes f [unfolded THIN_def]:
"PROP THIN (Trueprop (refines f f' s s (rel_prod (rel_throwE LR) (=))))"
shows "refines (L2_seq (L2_condition c f g) h) (condition c f' gh') s s (rel_prod (rel_throwE LR) (=))"
proof cases
assume "c s"
from this f
show ?thesis
unfolding L2_defs
by (auto simp add: refines_def_old reaches_condition_iff succeeds_condition_iff succeeds_bind reaches_bind rel_throwE_def
default_option_def Exn_def
split: xval_splits exception_or_result_splits)
(metis default_option_def the_Exception_simp exception_or_result_cases option.exhaust_sel)+
next
assume "¬c s"
then have *:
"run ((condition c f g) >>= h) s = run (g >>= h) s"
"run (condition c f' gh') s = run gh' s"
by (auto simp add: run_condition run_bind)
from g show ?thesis
unfolding refines_def_old succeeds_def reaches_def
L2_defs * .
qed
lemma refines_L2_seq_L2_condition_rel_throwE2:
assumes f [unfolded THIN_def]:
"PROP THIN (Trueprop (refines (L2_seq f h) fh' s s (rel_prod (rel_throwE LR) (=))))"
assumes g [unfolded THIN_def]:
"PROP THIN (Trueprop (refines g g' s s (rel_prod (rel_throwE LR) (=))))"
shows "refines (L2_seq (L2_condition c f g) h) (condition c fh' g') s s (rel_prod (rel_throwE LR) (=))"
using assms
unfolding L2_defs
by (subst (1 2) condition_swap)
(erule (1) refines_L2_seq_L2_condition_rel_throwE1[unfolded L2_defs])
lemma refines_bind_rel_throwE_first:
assumes f: "refines f f' s s (rel_prod (rel_throwE LR) S)"
shows "refines (f >>= g) f' s s (rel_prod (rel_throwE LR) S)"
using f unfolding L2_defs
by (auto simp add: refines_def_old succeeds_bind reaches_bind rel_throwE_def
default_option_def Exn_def
split: xval_splits exception_or_result_splits)
(metis default_option_def the_Exception_simp exception_or_result_cases option.exhaust_sel)+
lemma refines_L2_seq_rel_throwE_throwE:
assumes f [unfolded THIN_def]:
"PROP THIN (Trueprop (refines f f' s s (rel_prod (rel_throwE LR) (=))))"
shows "refines (L2_seq f g) f' s s (rel_prod (rel_throwE LR) (=))"
unfolding L2_defs using f
by (rule refines_bind_rel_throwE_first)
lemma refines_L2_seq_rel_throwE_throwE1:
assumes g[unfolded THIN_def, rule_format] :
"PROP THIN (⋀v t. refines (g v) (g' v) t t (rel_prod (rel_throwE (rel_map to_xval OO rel_xval L R)) (=)))"
assumes f [unfolded THIN_def, rule_format]:
"PROP THIN (Trueprop (refines f f' s s (rel_prod (rel_xval (rel_throwE' L) (=)) (=))))"
shows "refines (L2_seq f g) (bind f' g') s s (rel_prod (rel_throwE (rel_map to_xval OO rel_xval L R)) (=))"
unfolding L2_defs
apply (rule refines_bind_bind_exn [OF f])
apply (auto simp: g rel_throwE'_iff)
done
lemma refines_L2_seq_rel_throwE_liftE:
assumes g [unfolded THIN_def, rule_format]:
"PROP THIN (⋀v t. refines (g v) (g' v) t t (rel_prod (rel_throwE LR) (=)))"
assumes f [unfolded THIN_def]:
"PROP THIN (Trueprop (refines f f' s s (rel_prod rel_liftE (=))))"
shows "refines (L2_seq f g) (bind f' g') s s (rel_prod (rel_throwE LR) (=))"
using g f unfolding L2_defs
apply (clarsimp simp add: refines_def_old succeeds_bind reaches_bind reaches_try succeeds_condition_iff reaches_condition_iff
rel_throwE_def rel_throwE'_def relcompp.simps rel_liftE_def rel_xval.simps
split: xval_splits sum.splits, safe )
apply (metis the_Result_simp )
apply (smt (verit) case_exception_or_result_Result case_xval_simps(1))
by (metis (no_types, lifting) case_exception_or_result_Result case_xval_simps(2))
lemma refines_L2_throw_rel_throwE_Inl:
assumes "L l l'"
shows "refines (L2_throw (Inl l) ns) (throw (L2_VARS l' ns)) s s (rel_prod (rel_throwE (rel_map to_xval OO rel_xval L R)) (=))"
using assms unfolding L2_defs L2_VARS_def
by (auto simp add: refines_def_old rel_throwE_def rel_xval.simps relcompp.simps rel_map_def to_xval_def Exn_def
split: sum.splits)
lemma refines_L2_throw_rel_throwE_Inr:
assumes "R r r'"
shows "refines (L2_throw (Inr r) ns) (return (L2_VARS r' ns)) s s (rel_prod (rel_throwE ((rel_map to_xval OO rel_xval L R))) (=))"
using assms unfolding L2_defs L2_VARS_def
by (auto simp add: refines_def_old rel_throwE_def rel_xval.simps relcompp.simps rel_map_def to_xval_def Exn_def
split: sum.splits)
lemma refines_L2_throw_rel_throwE:
assumes "R r (Result r')"
shows "refines (L2_throw r ns) (L2_VARS (return r') ns) s s (rel_prod (rel_throwE R) (=))"
using assms unfolding L2_defs L2_VARS_def
by (auto simp add: refines_def_old rel_throwE_def rel_sum.simps relcompp.simps rel_map_def to_xval_def Exn_def
split: sum.splits)
lemmas ts_L2_try_condition_exit =
refines_L2_try_L2_seq_L2_condition_exit1[synthesize_rule nondet and exit priority:217]
refines_L2_try_L2_seq_L2_condition_exit2[synthesize_rule nondet and exit priority:217]
refines_L2_seq_L2_condition_rel_throwE1[synthesize_rule nondet and exit priority:216]
refines_L2_seq_L2_condition_rel_throwE2[synthesize_rule nondet and exit priority:216]
refines_L2_seq_rel_throwE_throwE [synthesize_rule nondet and exit priority:213]
refines_L2_seq_rel_throwE_throwE1[synthesize_rule nondet and exit priority:212 split: g and g']
refines_L2_seq_rel_throwE_liftE [synthesize_rule nondet and exit priority:212 split: g and g']
refines_L2_throw_rel_throwE_Inl [synthesize_rule nondet and exit priority:212]
refines_L2_throw_rel_throwE_Inr [synthesize_rule nondet and exit priority:212]
refines_L2_throw_rel_throwE [synthesize_rule nondet and exit priority:212]
bundle del_ts_L2_try_condition_exit =
refines_L2_try_L2_seq_L2_condition_exit1[synthesize_rule nondet and exit priority:217 del]
refines_L2_try_L2_seq_L2_condition_exit2[synthesize_rule nondet and exit priority:217 del]
refines_L2_seq_L2_condition_rel_throwE1[synthesize_rule nondet and exit priority:216 del]
refines_L2_seq_L2_condition_rel_throwE2[synthesize_rule nondet and exit priority:216 del]
refines_L2_seq_rel_throwE_throwE [synthesize_rule nondet and exit priority:213 del]
refines_L2_seq_rel_throwE_throwE1[synthesize_rule nondet and exit priority:212 split: g and g' del]
refines_L2_seq_rel_throwE_liftE [synthesize_rule nondet and exit priority:212 split: g and g' del]
refines_L2_throw_rel_throwE_Inl [synthesize_rule nondet and exit priority:212 del]
refines_L2_throw_rel_throwE_Inr [synthesize_rule nondet and exit priority:212 del]
refines_L2_throw_rel_throwE [synthesize_rule nondet and exit priority:212 del]
section ‹Error Monad (exit)›
lemma refines_L2_call_embed_exit:
assumes f: "refines f f' s s (rel_prod (rel_xval rel_Nonlocal (=)) (=))"
assumes emb: "⋀e'. L (emb (Nonlocal e')) (emb' e')"
shows "refines (L2_call f emb ns) (L2_VARS (map_value (map_exn emb') f') ns) s s (rel_prod (rel_xval L (=)) (=))"
unfolding L2_defs L2_VARS_def L2_call_def
apply (rule refines_map_value [OF f] )
using emb
by (auto simp add: rel_xval.simps map_exn_def rel_Nonlocal_conv)
lemma refines_L2_call_embed_exit_in_out:
assumes emb: "⋀e'. L (emb e') (emb' e')"
assumes f: "refines f f' s s (rel_prod (rel_xval (=) (=)) (=))"
shows "refines (L2_call f emb ns) (L2_VARS (map_value (map_exn emb') f') ns) s s (rel_prod (rel_xval L (=)) (=))"
unfolding L2_defs L2_VARS_def L2_call_def
apply (rule refines_map_value [OF f] )
using emb
by (auto simp add: rel_xval.simps map_exn_def rel_Nonlocal_conv)
lemma refines_L2_catch_exit:
assumes f: "refines f f' s s (rel_prod (rel_xval (=) R) (=))"
assumes h: "⋀s' v. refines (h v) (h' v) s' s' (rel_prod (rel_xval L R) (=))"
shows "refines (L2_catch f h) (catch f' h') s s (rel_prod (rel_xval L R) (=))"
unfolding L2_catch_def
using f h
apply (auto intro!: refines_catch)
done
lemma rel_xval_eq_refl: "rel_xval (=) (=) x x"
by (auto simp add: rel_xval_eq)
lemmas refines_monad_exit =
refines_L2_call_embed_exit [synthesize_rule exit priority:110]
refines_L2_call_embed_exit_in_out [synthesize_rule exit priority:109 split: emb and emb']
refines_L2_catch_exit [synthesize_rule exit priority:110 split: h and h']
rel_Nonlocal_Nonlocal [synthesize_rule exit priority:110]
rel_sum_eq [synthesize_rule exit priority:210]
rel_xval_eq_refl [synthesize_rule exit priority:210]
print_synthesize_rules exit
end