theory BCorres2_AI

lemma guarded_switch_bcorres: "s_bcorres (guarded_switch_to t :: 'a state \<Rightarrow> _) schedule s" using switch_thread_bcorreses(2)[where t=t] apply (clarsimp simp: schedule_unfold_all s_bcorres_underlying_def
                        in_monad in_select
            split del: if_split) apply (drule guarded_sub_switch) apply (rule_tac x=t in exI, clarsimp split del: if_split) apply (drule_tac s=s in drop_sbcorres_underlying) apply (clarsimp simp: s_bcorres_underlying_def) apply (auto intro!: alternative_second) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s_bcorres (guarded_switch_to t) schedule s proof (prove)
using this:
bcorres (switch_to_thread t) (switch_to_thread t)

goal (1 subgoal):
 1. s_bcorres (guarded_switch_to t) schedule s proof (prove)
goal (1 subgoal):
 1. \<And>ba. \<lbrakk>bcorres (switch_to_thread t) (switch_to_thread t); ((), ba) \<in> fst (guarded_switch_to t s); ((), truncate_state ba) \<notin> fst ((if idle_thread s = cur_thread s then return () \<sqinter> switch_to_idle_thread else switch_to_idle_thread) (truncate_state s))\<rbrakk> \<Longrightarrow> \<exists>thread. (\<exists>y. (case get_tcb thread s of None \<Rightarrow> None | Some tcb \<Rightarrow> if runnable (tcb_state tcb) then Some tcb else None) = Some y) \<and> ((), truncate_state ba) \<in> fst ((if thread = cur_thread s then return () \<sqinter> switch_to_thread (cur_thread s) else switch_to_thread thread) (truncate_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ba. \<lbrakk>bcorres (switch_to_thread t) (switch_to_thread t); ((), truncate_state ba) \<notin> fst ((if idle_thread s = cur_thread s then return () \<sqinter> switch_to_idle_thread else switch_to_idle_thread) (truncate_state s)); ((), ba) \<in> fst (switch_to_thread t s) \<and> (\<exists>y. get_tcb t s = Some y \<and> runnable (tcb_state y))\<rbrakk> \<Longrightarrow> \<exists>thread. (\<exists>y. (case get_tcb thread s of None \<Rightarrow> None | Some tcb \<Rightarrow> if runnable (tcb_state tcb) then Some tcb else None) = Some y) \<and> ((), truncate_state ba) \<in> fst ((if thread = cur_thread s then return () \<sqinter> switch_to_thread (cur_thread s) else switch_to_thread thread) (truncate_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ba y. \<lbrakk>bcorres (switch_to_thread t) (switch_to_thread t); ((), truncate_state ba) \<notin> fst ((if idle_thread s = cur_thread s then return () \<sqinter> switch_to_idle_thread else switch_to_idle_thread) (truncate_state s)); ((), ba) \<in> fst (switch_to_thread t s); get_tcb t s = Some y; runnable (tcb_state y)\<rbrakk> \<Longrightarrow> ((), truncate_state ba) \<in> fst ((if t = cur_thread s then return () \<sqinter> switch_to_thread (cur_thread s) else switch_to_thread t) (truncate_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ba y. \<lbrakk>((), truncate_state ba) \<notin> fst ((if idle_thread s = cur_thread s then return () \<sqinter> switch_to_idle_thread else switch_to_idle_thread) (truncate_state s)); ((), ba) \<in> fst (switch_to_thread t s); get_tcb t s = Some y; runnable (tcb_state y); s_bcorres (switch_to_thread t) (switch_to_thread t) s\<rbrakk> \<Longrightarrow> ((), truncate_state ba) \<in> fst ((if t = cur_thread s then return () \<sqinter> switch_to_thread (cur_thread s) else switch_to_thread t) (truncate_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>ba y. \<lbrakk>((), truncate_state ba) \<notin> fst ((if idle_thread s = cur_thread s then return () \<sqinter> switch_to_idle_thread else switch_to_idle_thread) (truncate_state s)); ((), ba) \<in> fst (switch_to_thread t s); get_tcb t s = Some y; runnable (tcb_state y); (\<lambda>x. case x of (x, y) \<Rightarrow> ((), truncate_state y)) ` fst (switch_to_thread t s) \<subseteq> fst (switch_to_thread t (truncate_state s))\<rbrakk> \<Longrightarrow> (t = cur_thread s \<longrightarrow> ((), truncate_state ba) \<in> fst ((return () \<sqinter> switch_to_thread (cur_thread s)) (truncate_state s))) \<and> (t \<noteq> cur_thread s \<longrightarrow> ((), truncate_state ba) \<in> fst (switch_to_thread t (truncate_state s))) proof (prove)
goal:
No subgoals!