theory Schedule_R

lemma guarded_switch_to_chooseThread_fragment_corres:
  "corres dc
    (P and st_tcb_at runnable t and invs and valid_sched)
    (P' and st_tcb_at' runnable' t and invs_no_cicd')
          (guarded_switch_to t)
          (do runnable \<leftarrow> isRunnable t;
              y \<leftarrow> assert runnable;
              ThreadDecls_H.switchToThread t
           od)" unfolding guarded_switch_to_def isRunnable_def apply simp apply (rule corres_guard_imp) apply (rule corres_split[OF getThreadState_corres]) apply (rule corres_assert_assume_l) apply (rule corres_assert_assume_r) apply (rule switchToThread_corres) apply (wp gts_st_tcb_at)+ apply (clarsimp simp: st_tcb_at_tcb_at invs_def valid_state_def valid_pspace_def valid_sched_def
                          invs_valid_vs_lookup invs_unique_refs) apply (auto elim!: pred_tcb'_weakenE split: thread_state.splits
              simp: pred_tcb_at' runnable'_def all_invs_but_ct_idle_or_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (P and st_tcb_at runnable t and invs and valid_sched) (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') (guarded_switch_to t) (do runnable <- isRunnable t;
y <- assert runnable;
global.switchToThread t
od) proof (prove)
goal (1 subgoal):
 1. corres dc (P and st_tcb_at runnable t and invs and valid_sched) (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') (do ts <- get_thread_state t;
assert (runnable ts);
switch_to_thread t
od) (do runnable <- do state <- getThreadState t;
return $ case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False
od;
y <- assert runnable;
global.switchToThread t
od) proof (prove)
goal (1 subgoal):
 1. corres dc (P and st_tcb_at runnable t and invs and valid_sched) (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') (do ts <- get_thread_state t;
y <- assert (runnable ts);
switch_to_thread t
od) (do state <- getThreadState t;
y <- assert (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False);
global.switchToThread t
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do ts <- get_thread_state t;
y <- assert (runnable ts);
switch_to_thread t
od) (do state <- getThreadState t;
y <- assert (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False);
global.switchToThread t
od)
 2. \<And>s. (P and st_tcb_at runnable t and invs and valid_sched) s \<Longrightarrow> ?Q s
 3. \<And>s. (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>ts state. thread_state_relation ts state \<Longrightarrow> corres dc (?R4 ts) (?R'4 state) (do y <- assert (runnable ts);
switch_to_thread t
od) (do y <- assert (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False);
global.switchToThread t
od)
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (P and st_tcb_at runnable t and invs and valid_sched) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>ts state. thread_state_relation ts state \<Longrightarrow> corres dc (?P10 ts) (?R'4 state) (switch_to_thread t) (do y <- assert (case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False);
global.switchToThread t
od)
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>ts. ?P10 ts and (\<lambda>s. runnable ts)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (P and st_tcb_at runnable t and invs and valid_sched) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>ts state. thread_state_relation ts state \<Longrightarrow> corres dc (?P10 ts) (?Q14 state) (switch_to_thread t) (global.switchToThread t)
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>ts. ?P10 ts and (\<lambda>s. runnable ts)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>state. ?Q14 state and (\<lambda>s. case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)\<rbrace>
 4. \<And>s. (P and st_tcb_at runnable t and invs and valid_sched) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>ts. valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs and (\<lambda>s. runnable ts)\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>state. valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb' and (\<lambda>s. case state of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False)\<rbrace>
 3. \<And>s. (P and st_tcb_at runnable t and invs and valid_sched) s \<Longrightarrow> (tcb_at t and ?Q4) s
 4. \<And>s. (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (P and st_tcb_at runnable t and invs and valid_sched) s \<Longrightarrow> (tcb_at t and (\<lambda>s. (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) s \<and> st_tcb_at runnable t s)) s
 2. \<And>s. (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') s \<Longrightarrow> (tcb_at' t and (\<lambda>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<and> st_tcb_at' (\<lambda>rv. case rv of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) t s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P' and st_tcb_at' runnable' t and all_invs_but_ct_idle_or_in_cur_domain') s \<Longrightarrow> (tcb_at' t and (\<lambda>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<and> st_tcb_at' (\<lambda>rv. case rv of Structures_H.thread_state.Running \<Rightarrow> True | Structures_H.thread_state.Restart \<Rightarrow> True | _ \<Rightarrow> False) t s)) s proof (prove)
goal:
No subgoals!