theory Finalise_IF

lemma thread_set_tcb_at:
  "\<lbrace>\<lambda>s. Q s\<rbrace> thread_set x ptr \<lbrace>\<lambda>_ s. P s\<rbrace>
   \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at ptr s \<longrightarrow> Q s\<rbrace> thread_set x ptr \<lbrace>\<lambda>_ s. P s\<rbrace>" apply (rule use_spec(1)) apply (case_tac "tcb_at ptr s") apply (clarsimp simp add: spec_valid_def valid_def) apply (simp add: spec_valid_def thread_set_def set_object_def[abs_def]) apply (wp get_object_wp) apply (force simp: get_tcb_def obj_at_def is_tcb_def
              split: option.splits Structures_A.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at ptr s \<longrightarrow> Q s\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>Q\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. tcb_at ptr s \<longrightarrow> Q s\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<lbrace>Q\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace>; tcb_at ptr s\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. tcb_at ptr s \<longrightarrow> Q s\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>Q\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace>; \<not> tcb_at ptr s\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. tcb_at ptr s \<longrightarrow> Q s\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>Q\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace>; \<not> tcb_at ptr s\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. tcb_at ptr s \<longrightarrow> Q s\<rbrace> thread_set x ptr \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>Q\<rbrace> do tcb <- gets_the (get_tcb ptr);
kobj <- get_object ptr;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (x tcb))\<rparr>)
od \<lbrace>\<lambda>_. P\<rbrace>; \<not> tcb_at ptr s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> (tcb_at ptr sa \<longrightarrow> Q sa)\<rbrace> do tcb <- gets_the (get_tcb ptr);
kobj <- get_object ptr;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (x tcb))\<rparr>)
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>\<lbrace>Q\<rbrace> do tcb <- gets_the (get_tcb ptr);
kobj <- get_object ptr;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr \<mapsto> TCB (x tcb))\<rparr>)
od \<lbrace>\<lambda>_. P\<rbrace>; \<not> tcb_at ptr s; sa = s \<and> (tcb_at ptr sa \<longrightarrow> Q sa)\<rbrakk> \<Longrightarrow> get_tcb ptr sa \<noteq> None \<longrightarrow> (\<forall>ko. ko_at ko ptr sa \<longrightarrow> a_type ko = ATCB \<longrightarrow> P (sa\<lparr>kheap := (kheap sa)(ptr \<mapsto> TCB (x (the (get_tcb ptr sa))))\<rparr>)) proof (prove)
goal:
No subgoals!