theory Syscall_S

lemma bisim_caller_cap:
  assumes bs: "bisim R P P' a (f NullCap)"
  shows   "bisim R P (P' and tcb_at p and separate_state) a (get_cap (p, tcb_cnode_index 3) >>= f)" apply (rule bisim_guard_imp) apply (rule bisim_symb_exec_r [where Pe = \<top>]) apply (rule_tac F = "rv = NullCap" in bisim_gen_asm_r) apply simp apply (rule bs) apply (wp get_cap_wp')+ apply fastforce apply wp apply simp apply (clarsimp simp: cte_wp_at_caps_of_state tcb_at_def
    caps_of_state_tcb_cap_cases dom_tcb_cap_cases
    cong: conj_cong) apply (drule (1) separate_state_get_tcbD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim R P (P' and tcb_at p and separate_state) a (get_cap (p, tcb_cnode_index 3) >>= f) proof (prove)
goal (3 subgoals):
 1. bisim R ?Q ?Q' a (get_cap (p, tcb_cnode_index 3) >>= f)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. (P' and tcb_at p and separate_state) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv. bisim R ?Q (?Q'4 rv) a (f rv)
 2. \<lbrace>?P'4\<rbrace> get_cap (p, tcb_cnode_index 3) \<lbrace>?Q'4\<rbrace>
 3. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> get_cap (p, tcb_cnode_index 3) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. not_empty ?Pd4 (get_cap (p, tcb_cnode_index 3))
 5. \<And>s. P s \<Longrightarrow> ?Q s
 6. \<And>s. (P' and tcb_at p and separate_state) s \<Longrightarrow> (?P'4 and (\<lambda>_. True) and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. \<And>rv. rv = NullCap \<Longrightarrow> bisim R ?Q (?P'9 rv) a (f rv)
 2. \<lbrace>?P'4\<rbrace> get_cap (p, tcb_cnode_index 3) \<lbrace>\<lambda>rv. ?P'9 rv and K (rv = NullCap)\<rbrace>
 3. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> get_cap (p, tcb_cnode_index 3) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. not_empty ?Pd4 (get_cap (p, tcb_cnode_index 3))
 5. \<And>s. P s \<Longrightarrow> ?Q s
 6. \<And>s. (P' and tcb_at p and separate_state) s \<Longrightarrow> (?P'4 and (\<lambda>_. True) and ?Pd4) s proof (prove)
goal (6 subgoals):
 1. bisim R ?Q (?P'9 NullCap) a (f NullCap)
 2. \<lbrace>?P'4\<rbrace> get_cap (p, tcb_cnode_index 3) \<lbrace>\<lambda>rv. ?P'9 rv and K (rv = NullCap)\<rbrace>
 3. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> get_cap (p, tcb_cnode_index 3) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. not_empty ?Pd4 (get_cap (p, tcb_cnode_index 3))
 5. \<And>s. P s \<Longrightarrow> ?Q s
 6. \<And>s. (P' and tcb_at p and separate_state) s \<Longrightarrow> (?P'4 and (\<lambda>_. True) and ?Pd4) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'4\<rbrace> get_cap (p, tcb_cnode_index 3) \<lbrace>\<lambda>rv. P' and K (rv = NullCap)\<rbrace>
 2. \<And>s. \<lbrace>(\<lambda>_. True) and (=) s\<rbrace> get_cap (p, tcb_cnode_index 3) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. not_empty ?Pd4 (get_cap (p, tcb_cnode_index 3))
 4. \<And>s. P s \<Longrightarrow> P s
 5. \<And>s. (P' and tcb_at p and separate_state) s \<Longrightarrow> (?P'4 and (\<lambda>_. True) and ?Pd4) s proof (prove)
goal (4 subgoals):
 1. \<And>s sa. ((\<lambda>_. True) and (=) s) sa \<Longrightarrow> \<forall>cap. caps_of_state sa (p, tcb_cnode_index 3) = Some cap \<longrightarrow> s = sa
 2. not_empty ?Pd4 (get_cap (p, tcb_cnode_index 3))
 3. \<And>s. P s \<Longrightarrow> P s
 4. \<And>s. (P' and tcb_at p and separate_state) s \<Longrightarrow> ((\<lambda>s. \<forall>cap. caps_of_state s (p, tcb_cnode_index 3) = Some cap \<longrightarrow> (P' and K (cap = NullCap)) s) and (\<lambda>_. True) and ?Pd4) s proof (prove)
goal (3 subgoals):
 1. not_empty ?Pd4 (get_cap (p, tcb_cnode_index 3))
 2. \<And>s. P s \<Longrightarrow> P s
 3. \<And>s. (P' and tcb_at p and separate_state) s \<Longrightarrow> ((\<lambda>s. \<forall>cap. caps_of_state s (p, tcb_cnode_index 3) = Some cap \<longrightarrow> (P' and K (cap = NullCap)) s) and (\<lambda>_. True) and ?Pd4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> P s
 2. \<And>s. (P' and tcb_at p and separate_state) s \<Longrightarrow> ((\<lambda>s. \<forall>cap. caps_of_state s (p, tcb_cnode_index 3) = Some cap \<longrightarrow> (P' and K (cap = NullCap)) s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) (p, tcb_cnode_index 3)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P' and tcb_at p and separate_state) s \<Longrightarrow> ((\<lambda>s. \<forall>cap. caps_of_state s (p, tcb_cnode_index 3) = Some cap \<longrightarrow> (P' and K (cap = NullCap)) s) and (\<lambda>_. True) and cte_wp_at (\<lambda>_. True) (p, tcb_cnode_index 3)) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>P' s; separate_state s; get_tcb p s = Some tcb\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>P' s; get_tcb p s = Some tcb; separate_cnode_cap (caps_of_state s) (tcb_ctable tcb) \<and> tcb_caller tcb = NullCap\<rbrakk> \<Longrightarrow> tcb_caller tcb = NullCap proof (prove)
goal:
No subgoals!