theory CNodeInv_AI

lemma valid_cte_wp_at_prop:
  assumes x: "\<And>P p. \<lbrace>cte_wp_at P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>"
  assumes y: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P' (cte_wp_at P p s)\<rbrace> f \<lbrace>\<lambda>rv s. P' (cte_wp_at P p s)\<rbrace>" proof - have cte_wp_at_neg2:
    "\<And>P p s. (\<not> cte_wp_at P p s) = (\<not> cte_at p s \<or> cte_wp_at (\<lambda>c. \<not> P c) p s)" by (fastforce simp: cte_wp_at_def) have rev_iffI:
    "\<And>P Q. \<lbrakk> P \<Longrightarrow> Q; \<not> P \<Longrightarrow> \<not> Q \<rbrakk> \<Longrightarrow> P = Q" by fastforce show ?thesis apply (clarsimp simp: valid_def elim!: rsubst[where P=P']) apply (rule rev_iffI) apply (erule(1) use_valid [OF _ x]) apply (subst cte_wp_at_neg2) apply (erule use_valid) apply (wp hoare_vcg_disj_lift x y valid_cte_at_neg_typ) apply (simp only: cte_wp_at_neg2[symmetric] simp_thms) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (cte_wp_at P p s)\<rbrace> f \<lbrace>\<lambda>rv s. P' (cte_wp_at P p s)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (cte_wp_at P p s)\<rbrace> f \<lbrace>\<lambda>rv s. P' (cte_wp_at P p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P p s. (\<not> cte_wp_at P p s) = (\<not> cte_wp_at (\<lambda>_. True) p s \<or> cte_wp_at (\<lambda>c. \<not> P c) p s) proof (state)
this:
(\<not> cte_wp_at ?P ?p ?s) = (\<not> cte_wp_at (\<lambda>_. True) ?p ?s \<or> cte_wp_at (\<lambda>c. \<not> ?P c) ?p ?s)

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (cte_wp_at P p s)\<rbrace> f \<lbrace>\<lambda>rv s. P' (cte_wp_at P p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>P \<Longrightarrow> Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P = Q proof (state)
this:
\<lbrakk>?P1 \<Longrightarrow> ?Q1; \<not> ?P1 \<Longrightarrow> \<not> ?Q1\<rbrakk> \<Longrightarrow> ?P1 = ?Q1

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (cte_wp_at P p s)\<rbrace> f \<lbrace>\<lambda>rv s. P' (cte_wp_at P p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (cte_wp_at P p s)\<rbrace> f \<lbrace>\<lambda>rv s. P' (cte_wp_at P p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> cte_wp_at P p s = cte_wp_at P p b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); cte_wp_at P p s\<rbrakk> \<Longrightarrow> cte_wp_at P p b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<not> cte_wp_at P p s\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P p b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<not> cte_wp_at P p s\<rbrakk> \<Longrightarrow> \<not> cte_wp_at P p b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<not> cte_wp_at P p s\<rbrakk> \<Longrightarrow> \<not> cte_wp_at (\<lambda>_. True) p b \<or> cte_wp_at (\<lambda>c. \<not> P c) p b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<not> cte_wp_at P p s \<Longrightarrow> \<lbrace>?P19 s a b\<rbrace> f \<lbrace>\<lambda>a b. \<not> cte_wp_at (\<lambda>_. True) p b \<or> cte_wp_at (\<lambda>c. \<not> P c) p b\<rbrace>
 2. \<And>s a b. \<not> cte_wp_at P p s \<Longrightarrow> ?P19 s a b s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<not> cte_wp_at P p s \<Longrightarrow> \<not> cte_wp_at (\<lambda>_. True) p s \<or> cte_wp_at (\<lambda>c. \<not> P c) p s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. P' (cte_wp_at P p s)\<rbrace> f \<lbrace>\<lambda>rv s. P' (cte_wp_at P p s)\<rbrace>

goal:
No subgoals!