theory Detype_R

lemma (in delete_locale) null_filter':
  assumes  descs: "Q (null_filter' (ctes_of s))"
  shows    "Q (null_filter' (ctes_of state'))" using descs ifunsafe apply (clarsimp elim!: rsubst[where P=Q]) apply (rule ext) apply (clarsimp simp:null_filter'_def tree_to_ctes) apply (rule ccontr) apply (clarsimp) apply (cut_tac p = x in non_null_present) apply (simp add:cte_wp_at_ctes_of) apply (rule ccontr) apply simp apply (erule(1) not_nullMDBNode) apply (case_tac y,simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q (null_filter' (ctes_of state')) proof (prove)
using this:
Q (null_filter' (ctes_of s))
if_unsafe_then_cap' s

goal (1 subgoal):
 1. Q (null_filter' (ctes_of state')) proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap' s \<Longrightarrow> null_filter' (ctes_of s) = null_filter' ctes' proof (prove)
goal (1 subgoal):
 1. \<And>x. if_unsafe_then_cap' s \<Longrightarrow> null_filter' (ctes_of s) x = null_filter' ctes' x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>if_unsafe_then_cap' s; ctes_of s x \<noteq> Some (CTE capability.NullCap nullMDBNode); base \<le> x; x \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> ctes_of s x = None proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>if_unsafe_then_cap' s; ctes_of s x \<noteq> Some (CTE capability.NullCap nullMDBNode); base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) x s
 2. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y; x \<notin> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y\<rbrakk> \<Longrightarrow> cteCap y \<noteq> capability.NullCap
 2. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y; x \<notin> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y; \<not> cteCap y \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y; x \<notin> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y; cteCap y = capability.NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y; x \<notin> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); cteCap y = capability.NullCap; cteMDBNode y = nullMDBNode\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y; x \<notin> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>if_unsafe_then_cap' s; y \<noteq> CTE capability.NullCap nullMDBNode; base \<le> x; x \<le> base + (2 ^ bits - 1); ctes_of s x = Some y; x \<notin> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!