theory Syscall_AI

lemma do_ipc_transfer_non_null_cte_wp_at2:
  fixes P
  assumes PNN: "\<And>cap. P cap \<Longrightarrow> cap \<noteq> cap.NullCap"
  assumes PUC: "\<And>cap. P cap \<Longrightarrow> \<not> is_untyped_cap cap"
  shows "\<lbrace>valid_objs and cte_wp_at P ptr\<rbrace> do_ipc_transfer st ep b gr rt \<lbrace>\<lambda>_. cte_wp_at P ptr\<rbrace>" proof - have PimpQ: "\<And>P Q ptr s. \<lbrakk> cte_wp_at P ptr s; \<And>cap. P cap \<Longrightarrow> Q cap \<rbrakk> \<Longrightarrow> cte_wp_at (P and Q) ptr s" by (erule cte_wp_at_weakenE, clarsimp) show ?thesis apply (rule hoare_chain [OF do_ipc_transfer_non_null_cte_wp_at]) apply (erule PUC) apply (clarsimp ) 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>valid_objs and cte_wp_at P ptr\<rbrace> do_ipc_transfer st ep b gr rt \<lbrace>\<lambda>_. cte_wp_at P ptr\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at P ptr\<rbrace> do_ipc_transfer st ep b gr rt \<lbrace>\<lambda>_. cte_wp_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P Q ptr s. \<lbrakk>cte_wp_at P ptr s; \<And>cap. P cap \<Longrightarrow> Q cap\<rbrakk> \<Longrightarrow> cte_wp_at (P and Q) ptr s proof (state)
this:
\<lbrakk>cte_wp_at ?P ?ptr ?s; \<And>cap. ?P cap \<Longrightarrow> ?Q cap\<rbrakk> \<Longrightarrow> cte_wp_at (?P and ?Q) ?ptr ?s

goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at P ptr\<rbrace> do_ipc_transfer st ep b gr rt \<lbrace>\<lambda>_. cte_wp_at P ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at P ptr\<rbrace> do_ipc_transfer st ep b gr rt \<lbrace>\<lambda>_. cte_wp_at P ptr\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>c. ?P1 c \<Longrightarrow> \<not> is_untyped_cap c
 2. \<And>s. (valid_objs and cte_wp_at P ptr) s \<Longrightarrow> (valid_objs and cte_wp_at (?P1 and (\<noteq>) NullCap) ?ptr1) s
 3. \<And>rv s. cte_wp_at (?P1 and (\<noteq>) NullCap) ?ptr1 s \<Longrightarrow> cte_wp_at P ptr s proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_objs and cte_wp_at P ptr) s \<Longrightarrow> (valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ?ptr1) s
 2. \<And>rv s. cte_wp_at (P and (\<noteq>) NullCap) ?ptr1 s \<Longrightarrow> cte_wp_at P ptr s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_objs s; cte_wp_at P ptr s\<rbrakk> \<Longrightarrow> cte_wp_at (P and (\<noteq>) NullCap) ?ptr1 s
 2. \<And>rv s. cte_wp_at (P and (\<noteq>) NullCap) ?ptr1 s \<Longrightarrow> cte_wp_at P ptr s proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>valid_objs s; P cap\<rbrakk> \<Longrightarrow> NullCap \<noteq> cap
 2. \<And>rv s. cte_wp_at (P and (\<noteq>) NullCap) ptr s \<Longrightarrow> cte_wp_at P ptr s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. cte_wp_at (P and (\<noteq>) NullCap) ptr s \<Longrightarrow> cte_wp_at P ptr s proof (prove)
goal (1 subgoal):
 1. \<And>rv s c. (P and (\<noteq>) NullCap) c \<Longrightarrow> P c proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>valid_objs and cte_wp_at P ptr\<rbrace> do_ipc_transfer st ep b gr rt \<lbrace>\<lambda>_. cte_wp_at P ptr\<rbrace>

goal:
No subgoals!