theory Detype_R

lemma map_to_ctes_delete:
  assumes vc: "s \<turnstile>' UntypedCap d base magnitude idx"
      and vs: "pspace_distinct' s"
  shows
  "map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x)
    = (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ctes_of s x)" using cte_wp_at_delete' [where P="(=) cte" for cte, OF vc vs]
        arg_cong [where f=Not, OF cte_wp_at_delete' [OF vc vs, where P="\<top>"]] apply (simp (no_asm_use) add: cte_wp_at_ctes_of) apply (rule ext) apply (case_tac "map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) x") apply (fastforce split: if_split_asm) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) = (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ctes_of s x) proof (prove)
using this:
cte_wp_at' ((=) ?cte3) ?p (s\<lparr>ksPSpace := \<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x\<rparr>) = (\<not> (base \<le> ?p \<and> ?p \<le> base + (2 ^ magnitude - 1)) \<and> cte_wp_at' ((=) ?cte3) ?p s)
(\<not> cte_wp_at' (\<lambda>_. True) ?p1 (s\<lparr>ksPSpace := \<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x\<rparr>)) = (\<not> (\<not> (base \<le> ?p1 \<and> ?p1 \<le> base + (2 ^ magnitude - 1)) \<and> cte_wp_at' (\<lambda>_. True) ?p1 s))

goal (1 subgoal):
 1. map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) = (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = Some cte) = ((base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<and> ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = None) = (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1) \<or> ctes_of s p = None)\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) = (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = Some cte) = ((base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<and> ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = None) = (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1) \<or> ctes_of s p = None)\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) x = (if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ctes_of s x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = Some cte) = ((base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<and> ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = None) = (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1) \<or> ctes_of s p = None); map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) x = None\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) x = (if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ctes_of s x)
 2. \<And>x a. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = Some cte) = ((base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<and> ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = None) = (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1) \<or> ctes_of s p = None); map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) x = Some a\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) x = (if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ctes_of s x) proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>\<And>cte p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = Some cte) = ((base \<le> p \<longrightarrow> \<not> p \<le> base + (2 ^ magnitude - 1)) \<and> ctes_of s p = Some cte); \<And>p. (map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) p = None) = (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1) \<or> ctes_of s p = None); map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) x = Some a\<rbrakk> \<Longrightarrow> map_to_ctes (\<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x) x = (if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ctes_of s x) proof (prove)
goal:
No subgoals!