theory Finalise_DR

lemma OR_choiceE_det:
  "\<lbrakk>det c; \<And>P. \<lbrace>P\<rbrace> c \<lbrace>\<lambda>rv. P\<rbrace>\<rbrakk> \<Longrightarrow> (OR_choiceE c (f :: ('a + 'b) det_ext_monad) g)
     = (doE rv \<leftarrow> liftE c; if rv then f else g odE)" apply (rule ext) apply (clarsimp simp: OR_choiceE_def select_f_def bind_def det_def valid_def
               wrap_ext_bool_det_ext_ext_def get_def bindE_def ethread_get_def split_def
               gets_the_def assert_opt_def return_def gets_def fail_def mk_ef_def liftE_def no_fail_def
               split: option.splits prod.splits) apply atomize apply (erule_tac x="(=) x" in allE) apply (erule_tac x=x in allE)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det c; \<And>P. \<lbrace>P\<rbrace> c \<lbrace>\<lambda>rv. P\<rbrace>\<rbrakk> \<Longrightarrow> OR_choiceE c f g = doE rv <- liftE c;
if rv then f else g
odE proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>det c; \<And>P. \<lbrace>P\<rbrace> c \<lbrace>\<lambda>rv. P\<rbrace>\<rbrakk> \<Longrightarrow> OR_choiceE c f g x = (doE rv <- liftE c;
if rv then f else g
odE) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. \<exists>a b. c s = ({(a, b)}, False); \<And>P. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (c s). P (snd x))\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (c x) \<times> {x}. fst ((if fst (fst x) then f else g) (snd x))) = (\<Union>x\<in>fst (c x). fst ((if fst x then f else g) (snd x))) \<and> ((\<exists>xa\<in>fst (c x). (fst xa \<longrightarrow> snd (f x)) \<and> (\<not> fst xa \<longrightarrow> snd (g x))) \<or> fst (c x) = {} \<or> snd (c x)) = ((\<exists>y\<in>fst (c x). (fst y \<longrightarrow> snd (f (snd y))) \<and> (\<not> fst y \<longrightarrow> snd (g (snd y)))) \<or> snd (c x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. \<exists>a b. c s = ({(a, b)}, False); \<forall>P s. P s \<longrightarrow> (\<forall>x\<in>fst (c s). P (snd x))\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (c x) \<times> {x}. fst ((if fst (fst x) then f else g) (snd x))) = (\<Union>x\<in>fst (c x). fst ((if fst x then f else g) (snd x))) \<and> ((\<exists>xa\<in>fst (c x). (fst xa \<longrightarrow> snd (f x)) \<and> (\<not> fst xa \<longrightarrow> snd (g x))) \<or> fst (c x) = {} \<or> snd (c x)) = ((\<exists>y\<in>fst (c x). (fst y \<longrightarrow> snd (f (snd y))) \<and> (\<not> fst y \<longrightarrow> snd (g (snd y)))) \<or> snd (c x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. \<exists>a b. c s = ({(a, b)}, False); \<forall>s. x = s \<longrightarrow> (\<forall>xa\<in>fst (c s). x = snd xa)\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (c x) \<times> {x}. fst ((if fst (fst x) then f else g) (snd x))) = (\<Union>x\<in>fst (c x). fst ((if fst x then f else g) (snd x))) \<and> ((\<exists>xa\<in>fst (c x). (fst xa \<longrightarrow> snd (f x)) \<and> (\<not> fst xa \<longrightarrow> snd (g x))) \<or> fst (c x) = {} \<or> snd (c x)) = ((\<exists>y\<in>fst (c x). (fst y \<longrightarrow> snd (f (snd y))) \<and> (\<not> fst y \<longrightarrow> snd (g (snd y)))) \<or> snd (c x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<exists>a b. c x = ({(a, b)}, False); x = x \<longrightarrow> (\<forall>xa\<in>fst (c x). x = snd xa)\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (c x) \<times> {x}. fst ((if fst (fst x) then f else g) (snd x))) = (\<Union>x\<in>fst (c x). fst ((if fst x then f else g) (snd x))) \<and> ((\<exists>xa\<in>fst (c x). (fst xa \<longrightarrow> snd (f x)) \<and> (\<not> fst xa \<longrightarrow> snd (g x))) \<or> fst (c x) = {} \<or> snd (c x)) = ((\<exists>y\<in>fst (c x). (fst y \<longrightarrow> snd (f (snd y))) \<and> (\<not> fst y \<longrightarrow> snd (g (snd y)))) \<or> snd (c x)) proof (prove)
goal:
No subgoals!