theory DetWP

lemma det_wp_asUser [wp]:
  "det f \<Longrightarrow> det_wp (tcb_at' t) (asUser t f)" apply (simp add: asUser_def split_def) apply (rule det_wp_pre) apply wp apply (drule det_wp_det) apply (erule det_wp_select_f) apply wp+ apply (rule_tac Q="\<lambda>_. tcb_at' t" in hoare_post_imp) apply simp apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> det_wp (tcb_at' t) (asUser t f) proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> det_wp (tcb_at' t) (do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od) proof (prove)
goal (2 subgoals):
 1. det f \<Longrightarrow> det_wp ?P' (do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od)
 2. \<And>s. \<lbrakk>det f; tcb_at' t s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>uc. det f \<Longrightarrow> det_wp (?P6 uc) (select_f (f uc))
 2. \<And>uc p. det f \<Longrightarrow> det_wp (?Q6 uc p) (do y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od)
 3. \<And>uc. det f \<Longrightarrow> \<lbrace>?P'6 uc\<rbrace> select_f (f uc) \<lbrace>?Q6 uc\<rbrace>
 4. det f \<Longrightarrow> \<lbrace>?P'4\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>uc. ?P6 uc and ?P'6 uc\<rbrace>
 5. \<And>s. \<lbrakk>det f; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?P'4) s proof (prove)
goal (5 subgoals):
 1. \<And>uc. det_wp (\<lambda>_. True) f \<Longrightarrow> det_wp (?P6 uc) (select_f (f uc))
 2. \<And>uc p. det f \<Longrightarrow> det_wp (?Q6 uc p) (do y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od)
 3. \<And>uc. det f \<Longrightarrow> \<lbrace>?P'6 uc\<rbrace> select_f (f uc) \<lbrace>?Q6 uc\<rbrace>
 4. det f \<Longrightarrow> \<lbrace>?P'4\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>uc. ?P6 uc and ?P'6 uc\<rbrace>
 5. \<And>s. \<lbrakk>det f; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?P'4) s proof (prove)
goal (4 subgoals):
 1. \<And>uc p. det f \<Longrightarrow> det_wp (?Q6 uc p) (do y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od)
 2. \<And>uc. det f \<Longrightarrow> \<lbrace>?P'6 uc\<rbrace> select_f (f uc) \<lbrace>?Q6 uc\<rbrace>
 3. det f \<Longrightarrow> \<lbrace>?P'4\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>uc. (\<lambda>_. True) and ?P'6 uc\<rbrace>
 4. \<And>s. \<lbrakk>det f; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and ?P'4) s proof (prove)
goal (2 subgoals):
 1. det f \<Longrightarrow> \<lbrace>?P'23\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>rv s. \<forall>x\<in>fst (f rv). (tcb_at' t and (\<lambda>s. True)) s\<rbrace>
 2. \<And>s. \<lbrakk>det f; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>s. True \<and> ?P'23 s)) s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>det f; tcb_at' t s\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f rv). (tcb_at' t and (\<lambda>s. True)) s
 2. det f \<Longrightarrow> \<lbrace>?P'23\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>
 3. \<And>s. \<lbrakk>det f; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>s. True \<and> ?P'23 s)) s proof (prove)
goal (2 subgoals):
 1. det f \<Longrightarrow> \<lbrace>?P'23\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>
 2. \<And>s. \<lbrakk>det f; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>s. True \<and> ?P'23 s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>det f; tcb_at' t s\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>s. True \<and> tcb_at' t s)) s proof (prove)
goal:
No subgoals!