theory Schedule_R

lemma guarded_switch_to_corres:
  "corres dc (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 o caps_of_state
                and st_tcb_at runnable t and valid_etcbs)
             (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues
                and st_tcb_at' runnable' t and cur_tcb')
             (guarded_switch_to t) (switchToThread t)" apply (simp add: guarded_switch_to_def) apply (rule corres_guard_imp) apply (rule corres_symb_exec_l'[OF _ gts_exs_valid]) apply (rule corres_assert_assume_l) apply (rule switchToThread_corres) apply (force simp: st_tcb_at_tcb_at) apply (wp gts_st_tcb_at) apply (force simp: st_tcb_at_tcb_at)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (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) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (guarded_switch_to t) (global.switchToThread t) proof (prove)
goal (1 subgoal):
 1. corres dc (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) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (do ts <- get_thread_state t;
y <- assert (runnable ts);
switch_to_thread t
od) (global.switchToThread t) 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) (global.switchToThread t)
 2. \<And>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 \<Longrightarrow> ?Q s
 3. \<And>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>ts. corres dc (?Q'4 ts) ?Q' (do y <- assert (runnable ts);
switch_to_thread t
od) (global.switchToThread t)
 2. \<And>s. ?P4 s \<Longrightarrow> tcb_at t s
 3. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?Q'4\<rbrace>
 4. \<And>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 \<Longrightarrow> (?P4 and ?Q4) s
 5. \<And>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>ts. corres dc (?P11 ts) ?Q' (switch_to_thread t) (global.switchToThread t)
 2. \<And>s. ?P4 s \<Longrightarrow> tcb_at t s
 3. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>ts. ?P11 ts and (\<lambda>s. runnable ts)\<rbrace>
 4. \<And>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 \<Longrightarrow> (?P4 and ?Q4) s
 5. \<And>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<Longrightarrow> ?Q' s proof (prove)
goal (4 subgoals):
 1. \<And>s. ?P4 s \<Longrightarrow> tcb_at t s
 2. \<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>
 3. \<And>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 \<Longrightarrow> (?P4 and ?Q4) s
 4. \<And>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<Longrightarrow> (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s proof (prove)
goal (3 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. \<And>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 \<Longrightarrow> (tcb_at t and ?Q4) s
 3. \<And>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<Longrightarrow> (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s proof (prove)
goal (2 subgoals):
 1. \<And>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 \<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. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<Longrightarrow> (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s proof (prove)
goal:
No subgoals!