theory Detype_R

lemma is_chunk[elim!]:
  "is_chunk (ctes_of s) cap x y \<Longrightarrow> is_chunk ctes' cap x y" apply (simp add: is_chunk_def) apply (erule allEI) apply (clarsimp dest!: trancl_next_rev) apply (drule rtranclD, erule disjE) apply (clarsimp simp: tree_to_ctes) apply (cut_tac p=y in non_null_present) apply (clarsimp simp: cte_wp_at_ctes_of) apply simp apply (clarsimp dest!: trancl_next_rev simp: trancl_into_rtrancl) apply (clarsimp simp: tree_to_ctes) apply (cut_tac p=p'' in non_null_present) apply (clarsimp simp add: cte_wp_at_ctes_of) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_chunk (ctes_of s) cap x y \<Longrightarrow> is_chunk ctes' cap x y proof (prove)
goal (1 subgoal):
 1. \<forall>p''. ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p'' \<longrightarrow> ctes_of s \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes_of s p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'') \<Longrightarrow> \<forall>p''. ctes' \<turnstile> x \<leadsto>\<^sup>+ p'' \<longrightarrow> ctes' \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'') proof (prove)
goal (1 subgoal):
 1. \<And>p''. ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p'' \<longrightarrow> ctes_of s \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes_of s p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'') \<Longrightarrow> ctes' \<turnstile> x \<leadsto>\<^sup>+ p'' \<longrightarrow> ctes' \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'') proof (prove)
goal (1 subgoal):
 1. \<And>p''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; ctes' \<turnstile> p'' \<leadsto>\<^sup>* y; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes_of s p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'' proof (prove)
goal (2 subgoals):
 1. \<And>p''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes_of s p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); p'' = y\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''
 2. \<And>p''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes_of s p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); p'' \<noteq> y \<and> ctes' \<turnstile> p'' \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'' proof (prove)
goal (2 subgoals):
 1. \<And>cap'' n''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ y; global.sameRegionAs cap cap''; ctes_of s y = Some (CTE cap'' n''); base \<le> y; y \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False
 2. \<And>p''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes_of s p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); p'' \<noteq> y \<and> ctes' \<turnstile> p'' \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'' proof (prove)
goal (3 subgoals):
 1. \<And>cap'' n''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ y; global.sameRegionAs cap cap''; ctes_of s y = Some (CTE cap'' n''); base \<le> y; y \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) y s
 2. \<And>cap'' n''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ y; global.sameRegionAs cap cap''; ctes_of s y = Some (CTE cap'' n''); base \<le> y; y \<le> base + (2 ^ bits - 1); y \<notin> base_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>p''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes_of s p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); p'' \<noteq> y \<and> ctes' \<turnstile> p'' \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'' proof (prove)
goal (2 subgoals):
 1. \<And>cap'' n''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ y; global.sameRegionAs cap cap''; ctes_of s y = Some (CTE cap'' n''); base \<le> y; y \<le> base + (2 ^ bits - 1); y \<notin> base_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>p''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes_of s p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); p'' \<noteq> y \<and> ctes' \<turnstile> p'' \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'' proof (prove)
goal (1 subgoal):
 1. \<And>p''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>* y \<longrightarrow> (\<exists>cap''. (\<exists>n''. ctes_of s p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''); p'' \<noteq> y \<and> ctes' \<turnstile> p'' \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'' proof (prove)
goal (1 subgoal):
 1. \<And>p'' cap'' n''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; p'' \<noteq> y; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>+ y; global.sameRegionAs cap cap''; ctes_of s p'' = Some (CTE cap'' n'')\<rbrakk> \<Longrightarrow> \<exists>cap''. (\<exists>n''. ctes' p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'' proof (prove)
goal (1 subgoal):
 1. \<And>p'' cap'' n''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; p'' \<noteq> y; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>+ y; global.sameRegionAs cap cap''; ctes_of s p'' = Some (CTE cap'' n''); base \<le> p''; p'' \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p'' cap'' n''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; p'' \<noteq> y; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>+ y; global.sameRegionAs cap cap''; ctes_of s p'' = Some (CTE cap'' n''); base \<le> p''; p'' \<le> base + (2 ^ bits - 1)\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) p'' s
 2. \<And>p'' cap'' n''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; p'' \<noteq> y; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>+ y; global.sameRegionAs cap cap''; ctes_of s p'' = Some (CTE cap'' n''); base \<le> p''; p'' \<le> base + (2 ^ bits - 1); p'' \<notin> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p'' cap'' n''. \<lbrakk>ctes_of s \<turnstile> x \<leadsto>\<^sup>+ p''; p'' \<noteq> y; ctes_of s \<turnstile> p'' \<leadsto>\<^sup>+ y; global.sameRegionAs cap cap''; ctes_of s p'' = Some (CTE cap'' n''); base \<le> p''; p'' \<le> base + (2 ^ bits - 1); p'' \<notin> base_bits\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!