theory Syscall_R

lemma doIPCTransfer_non_null_cte_wp_at2':
  fixes P
  assumes PNN: "\<And>cte. P (cteCap cte) \<Longrightarrow> cteCap cte \<noteq> capability.NullCap"
   and    PUC: "\<And>cap. P cap \<Longrightarrow> \<not> isUntypedCap cap"
  shows "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace>
         doIPCTransfer sender endpoint badge grant receiver
         \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace>" proof - have PimpQ: "\<And>P Q ptr s. \<lbrakk> cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr s;
                               \<And>cte. P (cteCap cte) \<Longrightarrow> Q (cteCap cte) \<rbrakk>
                             \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> Q (cteCap cte)) ptr s" by (erule cte_wp_at_weakenE', clarsimp) show ?thesis apply (rule hoare_chain [OF doIPCTransfer_non_null_cte_wp_at']) apply (erule PUC) apply (erule PimpQ) apply (drule PNN, clarsimp) apply (erule cte_wp_at_weakenE') apply (clarsimp) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace> doIPCTransfer sender endpoint badge grant receiver \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace> doIPCTransfer sender endpoint badge grant receiver \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P Q ptr s. \<lbrakk>cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr s; \<And>cte. P (cteCap cte) \<Longrightarrow> Q (cteCap cte)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> Q (cteCap cte)) ptr s proof (state)
this:
\<lbrakk>cte_wp_at' (\<lambda>cte. ?P (cteCap cte)) ?ptr ?s; \<And>cte. ?P (cteCap cte) \<Longrightarrow> ?Q (cteCap cte)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. ?P (cteCap cte) \<and> ?Q (cteCap cte)) ?ptr ?s

goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace> doIPCTransfer sender endpoint badge grant receiver \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace> doIPCTransfer sender endpoint badge grant receiver \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap. ?P1 cap \<Longrightarrow> \<not> isUntypedCap cap
 2. \<And>s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr s \<Longrightarrow> cte_wp_at' (\<lambda>cte. ?P1 (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ?ptr1 s
 3. \<And>rv s. cte_wp_at' (\<lambda>cte. ?P1 (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ?ptr1 s \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr s proof (prove)
goal (2 subgoals):
 1. \<And>s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr s \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ?ptr1 s
 2. \<And>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ?ptr1 s \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr s proof (prove)
goal (2 subgoals):
 1. \<And>s cte. P (cteCap cte) \<Longrightarrow> cteCap cte \<noteq> capability.NullCap
 2. \<And>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr s \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>rv s c. P (cteCap c) \<and> cteCap c \<noteq> capability.NullCap \<Longrightarrow> P (cteCap c) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace> doIPCTransfer sender endpoint badge grant receiver \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte)) ptr\<rbrace>

goal:
No subgoals!