theory BCorres_AI

lemma OR_choiceE_bcorres[wp]:
  "bcorres f f' \<Longrightarrow> bcorres g g' \<Longrightarrow> bcorres (OR_choiceE b f g) (OR_choiceE b f' g')" apply (simp add: OR_choiceE_def wrap_ext_bool_unit_def) apply wp apply (simp add: bind_def select_f_def mk_ef_def modify_def return_def get_def put_def gets_def
                   select_def) apply (simp add: bcorres_underlying_def s_bcorres_underlying_def) apply (clarsimp simp: if_split_asm) apply (rule_tac x=ab in exI) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcorres f f'; bcorres g g'\<rbrakk> \<Longrightarrow> bcorres (OR_choiceE b f g) (OR_choiceE b f' g') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcorres f f'; bcorres g g'\<rbrakk> \<Longrightarrow> bcorres (doE ex <- liftE get;
(rv, uu_) <- liftE (select_f (mk_ef (wrap_ext_bool b ex)));
if rv then f else g
odE) (doE ex <- liftE get;
(rv, uu_) <- liftE (select_f (mk_ef (select UNIV ex)));
if rv then f' else g'
odE) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>bcorres f f'; bcorres g g'\<rbrakk> \<Longrightarrow> bcorres (do (rv, uu_) <- select_f (mk_ef (wrap_ext_bool b x));
if rv then f else g
od) (do (rv, uu_) <- select_f (mk_ef (select UNIV (truncate_state x)));
if rv then f' else g'
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>bcorres f f'; bcorres g g'\<rbrakk> \<Longrightarrow> bcorres (\<lambda>s. (\<Union>a\<in>fst (wrap_ext_bool b x) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, uu_) \<Rightarrow> if rv then f else g) xa), (\<exists>x\<in>fst (wrap_ext_bool b x). snd ((case x of (rv, uu_) \<Rightarrow> if rv then f else g) s)) \<or> fst (wrap_ext_bool b x) = {} \<or> snd (wrap_ext_bool b x))) (\<lambda>s. (\<Union>a\<in>(UNIV \<times> {truncate_state x}) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, uu_) \<Rightarrow> if rv then f' else g') xa), \<exists>x. (x \<longrightarrow> snd (f' s)) \<and> (\<not> x \<longrightarrow> snd (g' s)))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (f' (truncate_state s)); \<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (g s) \<subseteq> fst (g' (truncate_state s))\<rbrakk> \<Longrightarrow> \<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` (\<Union>a\<in>fst (wrap_ext_bool b x) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, uu_) \<Rightarrow> if rv then f else g) xa)) \<subseteq> (\<Union>a\<in>(UNIV \<times> {truncate_state x}) \<times> {truncate_state s}. fst (case a of (x, xa) \<Rightarrow> (case x of (rv, uu_) \<Rightarrow> if rv then f' else g') xa)) proof (prove)
goal (1 subgoal):
 1. \<And>x s aa ba ab bb. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (f' (truncate_state s)); \<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (g s) \<subseteq> fst (g' (truncate_state s)); (aa, ba) \<in> fst ((if ab then f else g) s); (ab, bb) \<in> fst (wrap_ext_bool b x)\<rbrakk> \<Longrightarrow> \<exists>x. (x \<longrightarrow> (aa, truncate_state ba) \<in> fst (f' (truncate_state s))) \<and> (\<not> x \<longrightarrow> (aa, truncate_state ba) \<in> fst (g' (truncate_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>x s aa ba ab bb. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (f' (truncate_state s)); \<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (g s) \<subseteq> fst (g' (truncate_state s)); (aa, ba) \<in> fst ((if ab then f else g) s); (ab, bb) \<in> fst (wrap_ext_bool b x)\<rbrakk> \<Longrightarrow> (ab \<longrightarrow> (aa, truncate_state ba) \<in> fst (f' (truncate_state s))) \<and> (\<not> ab \<longrightarrow> (aa, truncate_state ba) \<in> fst (g' (truncate_state s))) proof (prove)
goal:
No subgoals!