theory Retype_R

lemma lookupAround2_pspace_no:
  "is_aligned ptr sz \<Longrightarrow>
   (case fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) of None \<Rightarrow> return ()
             | Some (x, y) \<Rightarrow> haskell_assert (x < fromPPtr ptr) [])
      = assert ({ptr..ptr + 2 ^ sz - 1} \<inter> dom ps = {})" apply (simp add: assert_def split: option.split) apply safe apply (clarsimp simp: lookupAround2_None1) apply (clarsimp simp: lookupAround2_char1) apply (clarsimp simp: lookupAround2_char1) apply (drule_tac a=a in equals0D) apply (simp add: linorder_not_less) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz \<Longrightarrow> (case fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) of None \<Rightarrow> return () | Some (x, y) \<Rightarrow> haskell_assert (x < fromPPtr ptr) []) = assert ({ptr..ptr + 2 ^ sz - 1} \<inter> dom ps = {}) proof (prove)
goal (1 subgoal):
 1. is_aligned ptr sz \<Longrightarrow> (fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) = None \<longrightarrow> {ptr..ptr + 2 ^ sz - 1} \<inter> dom ps \<noteq> {} \<longrightarrow> return () = fail) \<and> (\<forall>a. (a < ptr \<longrightarrow> (\<exists>b. fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) = Some (a, b)) \<longrightarrow> {ptr..ptr + 2 ^ sz - 1} \<inter> dom ps \<noteq> {} \<longrightarrow> return () = fail) \<and> (\<not> a < ptr \<longrightarrow> (\<exists>b. fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) = Some (a, b)) \<longrightarrow> {ptr..ptr + 2 ^ sz - 1} \<inter> dom ps = {} \<longrightarrow> fail = return ())) proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr sz; fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) = None; return () \<noteq> fail; x \<in> {ptr..ptr + 2 ^ sz - 1}; ps x = Some y\<rbrakk> \<Longrightarrow> x \<in> {}
 2. \<And>a b x y. \<lbrakk>is_aligned ptr sz; a < ptr; fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) = Some (a, b); return () \<noteq> fail; x \<in> {ptr..ptr + 2 ^ sz - 1}; ps x = Some y\<rbrakk> \<Longrightarrow> x \<in> {}
 3. \<And>a b. \<lbrakk>is_aligned ptr sz; \<not> a < ptr; fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) = Some (a, b); {ptr..ptr + 2 ^ sz - 1} \<inter> dom ps = {}\<rbrakk> \<Longrightarrow> fail = return () proof (prove)
goal (2 subgoals):
 1. \<And>a b x y. \<lbrakk>is_aligned ptr sz; a < ptr; fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) = Some (a, b); return () \<noteq> fail; x \<in> {ptr..ptr + 2 ^ sz - 1}; ps x = Some y\<rbrakk> \<Longrightarrow> x \<in> {}
 2. \<And>a b. \<lbrakk>is_aligned ptr sz; \<not> a < ptr; fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) = Some (a, b); {ptr..ptr + 2 ^ sz - 1} \<inter> dom ps = {}\<rbrakk> \<Longrightarrow> fail = return () proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_aligned ptr sz; \<not> a < ptr; fst (lookupAround2 (ptr + 2 ^ sz - 1) ps) = Some (a, b); {ptr..ptr + 2 ^ sz - 1} \<inter> dom ps = {}\<rbrakk> \<Longrightarrow> fail = return () proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_aligned ptr sz; \<not> a < ptr; {ptr..ptr + 2 ^ sz - 1} \<inter> dom ps = {}; a \<le> ptr + 2 ^ sz - 1; ps a = Some b; \<forall>z. a < z \<and> z \<le> ptr + 2 ^ sz - 1 \<longrightarrow> ps z = None\<rbrakk> \<Longrightarrow> fail = return () proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_aligned ptr sz; \<not> a < ptr; a \<le> ptr + 2 ^ sz - 1; ps a = Some b; \<forall>z. a < z \<and> z \<le> ptr + 2 ^ sz - 1 \<longrightarrow> ps z = None; a \<notin> {ptr..ptr + 2 ^ sz - 1} \<inter> dom ps\<rbrakk> \<Longrightarrow> fail = return () proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_aligned ptr sz; ptr \<le> a; a \<le> ptr + 2 ^ sz - 1; ps a = Some b; \<forall>z. a < z \<and> z \<le> ptr + 2 ^ sz - 1 \<longrightarrow> ps z = None; a \<notin> dom ps\<rbrakk> \<Longrightarrow> fail = return () proof (prove)
goal:
No subgoals!