theory Syscall_S

lemma handle_reply_bisim:
  "bisim (=) \<top> (separate_state and cur_tcb) (return ()) Syscall_A.handle_reply" unfolding Syscall_A.handle_reply_def apply (rule bisim_guard_imp_both) apply (rule bisim_symb_exec_r [where Pe = \<top>]) apply (rule bisim_caller_cap) apply simp apply (rule bisim_return) apply simp apply (wp | simp add: cur_tcb_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (separate_state and cur_tcb) (return ()) Syscall_A.handle_reply proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (separate_state and cur_tcb) (return ()) (do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od) proof (prove)
goal (2 subgoals):
 1. bisim (=) ?P ?P' (return ()) (do thread <- gets cur_thread;
caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od)
 2. \<And>s. (separate_state and cur_tcb) s \<Longrightarrow> ?P s \<and> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>thread. bisim (=) ?P (?Q'3 thread) (return ()) (do caller_cap <- get_cap (thread, tcb_cnode_index 3);
case caller_cap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail
od)
 2. \<lbrace>?P'3\<rbrace> gets cur_thread \<lbrace>?Q'3\<rbrace>
 3. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. not_empty ?Pd3 (gets cur_thread)
 5. \<And>s. (separate_state and cur_tcb) s \<Longrightarrow> ?P s \<and> (?P'3 and (\<lambda>_. True) and ?Pd3) s proof (prove)
goal (5 subgoals):
 1. \<And>thread. bisim (=) ?P (?P'8 thread) (return ()) (case NullCap of NullCap \<Rightarrow> return () | ReplyCap caller True R \<Rightarrow> fail | ReplyCap caller False R \<Rightarrow> do_reply_transfer thread caller (thread, tcb_cnode_index 3) (AllowGrant \<in> R) | _ \<Rightarrow> fail)
 2. \<lbrace>?P'3\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. ?P'8 thread and tcb_at thread and separate_state\<rbrace>
 3. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. not_empty ?Pd3 (gets cur_thread)
 5. \<And>s. (separate_state and cur_tcb) s \<Longrightarrow> ?P s \<and> (?P'3 and (\<lambda>_. True) and ?Pd3) s proof (prove)
goal (5 subgoals):
 1. \<And>thread. bisim (=) ?P (?P'8 thread) (return ()) (return ())
 2. \<lbrace>?P'3\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. ?P'8 thread and tcb_at thread and separate_state\<rbrace>
 3. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. not_empty ?Pd3 (gets cur_thread)
 5. \<And>s. (separate_state and cur_tcb) s \<Longrightarrow> ?P s \<and> (?P'3 and (\<lambda>_. True) and ?Pd3) s proof (prove)
goal (5 subgoals):
 1. \<And>thread. () = ()
 2. \<lbrace>?P'3\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and tcb_at thread and separate_state\<rbrace>
 3. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. not_empty ?Pd3 (gets cur_thread)
 5. \<And>s. (separate_state and cur_tcb) s \<Longrightarrow> True \<and> (?P'3 and (\<lambda>_. True) and ?Pd3) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'3\<rbrace> gets cur_thread \<lbrace>\<lambda>thread. (\<lambda>_. True) and tcb_at thread and separate_state\<rbrace>
 2. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. not_empty ?Pd3 (gets cur_thread)
 4. \<And>s. (separate_state and cur_tcb) s \<Longrightarrow> True \<and> (?P'3 and (\<lambda>_. True) and ?Pd3) s proof (prove)
goal:
No subgoals!