theory Detype_R

lemma descendants_range_in_lift':
  assumes st: "\<And>P. \<lbrace>\<lambda>s. Q s \<and> P ((swp descendants_of') (null_filter' (ctes_of s)))\<rbrace>
  f \<lbrace>\<lambda>r s. P ((swp descendants_of') (null_filter' (ctes_of s)))\<rbrace>"
  assumes cap_range:
  "\<And>P p. \<lbrace>\<lambda>s. Q' s \<and> cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p s\<rbrace> f \<lbrace>\<lambda>r s. cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p s\<rbrace>"
  shows "\<lbrace>\<lambda>s. Q s \<and> Q' s \<and> descendants_range_in' S slot (ctes_of s)\<rbrace> f \<lbrace>\<lambda>r s. descendants_range_in' S slot (ctes_of s)\<rbrace>" apply (clarsimp simp:descendants_range_in'_def2) apply (subst swp_def[where f = descendants_of', THEN meta_eq_to_obj_eq,
                       THEN fun_cong, THEN fun_cong, symmetric])+ apply (simp only: Ball_def[unfolded imp_conv_disj]) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift st cap_range) apply (rule_tac Q = "\<lambda>r s. cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s"
      in hoare_strengthen_post) apply (wp cap_range) apply (clarsimp simp:cte_wp_at_ctes_of null_filter'_def) apply clarsimp apply (drule spec, drule(1) mp) apply (subst (asm) null_filter_descendants_of') apply simp apply (case_tac "(ctes_of s) x") apply (clarsimp simp:descendants_of'_def null_filter'_def subtree_target_Some) apply (case_tac a) apply (clarsimp simp:cte_wp_at_ctes_of null_filter'_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s \<and> Q' s \<and> descendants_range_in' S slot (ctes_of s)\<rbrace> f \<lbrace>\<lambda>r s. descendants_range_in' S slot (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s \<and> Q' s \<and> (\<forall>p'\<in>descendants_of' slot (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})\<rbrace> f \<lbrace>\<lambda>r s. \<forall>p'\<in>descendants_of' slot (null_filter' (ctes_of s)). \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s \<and> Q' s \<and> (\<forall>p'\<in>swp descendants_of' (null_filter' (ctes_of s)) slot. \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})\<rbrace> f \<lbrace>\<lambda>r s. \<forall>p'\<in>swp descendants_of' (null_filter' (ctes_of s)) slot. \<forall>c. (\<exists>n. null_filter' (ctes_of s) p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s \<and> Q' s \<and> (\<forall>x. x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}))\<rbrace> f \<lbrace>\<lambda>r s. \<forall>x. x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q8\<rbrace> f \<lbrace>\<lambda>r s. \<forall>x. x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})\<rbrace>
 2. \<And>s. Q s \<and> Q' s \<and> (\<forall>x. x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})) \<Longrightarrow> ?Q8 s proof (prove)
goal (2 subgoals):
 1. \<And>x c. \<lbrace>?P16 x c\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}\<rbrace>
 2. \<And>s. Q s \<and> Q' s \<and> (\<forall>x. x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})) \<Longrightarrow> \<forall>x. Q s \<and> x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>xa. ?P16 x xa s) proof (prove)
goal (3 subgoals):
 1. \<And>x c. \<lbrace>?P16 x c\<rbrace> f \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x\<rbrace>
 2. \<And>x c rv s. cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s \<Longrightarrow> (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}
 3. \<And>s. Q s \<and> Q' s \<and> (\<forall>x. x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})) \<Longrightarrow> \<forall>x. Q s \<and> x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>xa. ?P16 x xa s) proof (prove)
goal (2 subgoals):
 1. \<And>x c rv s. cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s \<Longrightarrow> (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}
 2. \<And>s. Q s \<and> Q' s \<and> (\<forall>x. x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})) \<Longrightarrow> \<forall>x. Q s \<and> x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>xa. Q' s \<and> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. Q s \<and> Q' s \<and> (\<forall>x. x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {})) \<Longrightarrow> \<forall>x. Q s \<and> x \<notin> swp descendants_of' (null_filter' (ctes_of s)) slot \<or> (\<forall>xa. Q' s \<and> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>Q s; Q' s; \<forall>x. x \<in> descendants_of' slot (null_filter' (ctes_of s)) \<longrightarrow> (\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}); x \<in> descendants_of' slot (null_filter' (ctes_of s))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>Q s; Q' s; x \<in> descendants_of' slot (null_filter' (ctes_of s)); \<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; Q s; Q' s\<rbrakk> \<Longrightarrow> null_filter' (null_filter' (ctes_of s)) = null_filter' (?ys46 s x)
 2. \<And>s x. \<lbrakk>Q s; Q' s; x \<in> descendants_of' slot (?ys46 s x); \<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>Q s; Q' s; x \<in> descendants_of' slot (ctes_of s); \<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>Q s; Q' s; x \<in> descendants_of' slot (ctes_of s); \<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; ctes_of s x = None\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s
 2. \<And>s x a. \<lbrakk>Q s; Q' s; x \<in> descendants_of' slot (ctes_of s); \<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; ctes_of s x = Some a\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s proof (prove)
goal (1 subgoal):
 1. \<And>s x a. \<lbrakk>Q s; Q' s; x \<in> descendants_of' slot (ctes_of s); \<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; ctes_of s x = Some a\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s proof (prove)
goal (1 subgoal):
 1. \<And>s x a x1 x2. \<lbrakk>Q s; Q' s; x \<in> descendants_of' slot (ctes_of s); \<forall>c. (\<exists>n. null_filter' (ctes_of s) x = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; ctes_of s x = Some a; a = CTE x1 x2\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> S = {}) x s proof (prove)
goal:
No subgoals!