theory Tcb_R

lemma threadcontrol_corres_helper1:
  "\<lbrace> einvs and simple_sched_action\<rbrace>
     thread_set (tcb_ipc_buffer_update f) a
           \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs\<rbrace>" apply (rule hoare_pre) apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (simp | intro impI | elim exE conjE)+ apply (frule get_tcb_SomeD) apply (erule ssubst) apply (clarsimp simp add: weak_valid_sched_action_def valid_etcbs_2_def st_tcb_at_kh_def
              get_tcb_def obj_at_kh_def obj_at_def is_etcb_at'_def valid_sched_def valid_sched_action_def) apply (erule_tac x=a in allE)+ apply (clarsimp simp: is_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and simple_sched_action\<rbrace> thread_set (tcb_ipc_buffer_update f) a \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> thread_set (tcb_ipc_buffer_update f) a \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs\<rbrace>
 2. \<And>s. (einvs and simple_sched_action) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do tcb <- gets_the (get_tcb a);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh a = Some y);
return (the (kh a))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb_ipc_buffer_update f tcb))\<rparr>)
od \<lbrace>\<lambda>x. weak_valid_sched_action and valid_etcbs\<rbrace>
 2. \<And>s. (einvs and simple_sched_action) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (einvs and simple_sched_action) s \<Longrightarrow> get_tcb a s \<noteq> None \<longrightarrow> (\<exists>y. kheap s a = Some y) \<longrightarrow> a_type (the (kheap s a)) = ATCB \<longrightarrow> (weak_valid_sched_action and valid_etcbs) (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb a s))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y ya. \<lbrakk>a_type ya = ATCB; get_tcb a s = Some y; kheap s a = Some ya; invs s; valid_list s; valid_sched s; simple_sched_action s\<rbrakk> \<Longrightarrow> weak_valid_sched_action_2 (scheduler_action s) (ekheap s) (\<lambda>b. if b = a then Some (TCB (tcb_ipc_buffer_update f y)) else kheap s b) \<and> valid_etcbs_2 (ekheap s) (\<lambda>b. if b = a then Some (TCB (tcb_ipc_buffer_update f y)) else kheap s b) proof (prove)
goal (1 subgoal):
 1. \<And>s y ya. \<lbrakk>a_type ya = ATCB; get_tcb a s = Some y; kheap s a = Some ya; invs s; valid_list s; valid_sched s; simple_sched_action s; kheap s a = Some (TCB y)\<rbrakk> \<Longrightarrow> weak_valid_sched_action_2 (scheduler_action s) (ekheap s) (\<lambda>b. if b = a then Some (TCB (tcb_ipc_buffer_update f y)) else kheap s b) \<and> valid_etcbs_2 (ekheap s) (\<lambda>b. if b = a then Some (TCB (tcb_ipc_buffer_update f y)) else kheap s b) proof (prove)
goal (1 subgoal):
 1. \<And>s y ya. \<lbrakk>get_tcb a s = Some y; kheap s a = Some ya; invs s; valid_list s; valid_sched s; simple_sched_action s; kheap s a = Some (TCB y)\<rbrakk> \<Longrightarrow> weak_valid_sched_action_2 (scheduler_action s) (ekheap s) (\<lambda>b. if b = a then Some (TCB (tcb_ipc_buffer_update f y)) else kheap s b) \<and> valid_etcbs_2 (ekheap s) (\<lambda>b. if b = a then Some (TCB (tcb_ipc_buffer_update f y)) else kheap s b) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>invs s; valid_list s; simple_sched_action s; kheap s a = Some (TCB y); \<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); DetSchedInvs_AI.valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; \<forall>t. scheduler_action s = switch_thread t \<longrightarrow> (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb))); switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s\<rbrakk> \<Longrightarrow> (scheduler_action s = switch_thread a \<longrightarrow> runnable (tcb_state y)) \<and> (\<exists>y. ekheap s a = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>invs s; valid_list s; simple_sched_action s; kheap s a = Some (TCB y); DetSchedInvs_AI.valid_queues s; ct_not_in_q s; is_activatable (cur_thread s) s; switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; (\<exists>ko. kheap s a = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s a = Some y); scheduler_action s = switch_thread a \<longrightarrow> (\<exists>ko. kheap s a = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))\<rbrakk> \<Longrightarrow> (scheduler_action s = switch_thread a \<longrightarrow> runnable (tcb_state y)) \<and> (\<exists>y. ekheap s a = Some y) proof (prove)
goal:
No subgoals!