kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_AI

lemma no_overflow_n:"n * 2^sbit < 2^len_of TYPE('a)" using aligned sz apply (clarsimp dest!:add_leD1) apply (rule le_less_trans) apply (drule Nat.mult_le_mono[where i = n and k = "2^sbit",OF _ le_refl]) apply (clarsimp simp: power_add[symmetric]) apply (assumption) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n * 2 ^ sbit < 2 ^ LENGTH('a) proof (prove)
using this:
is_aligned ptr sbit
sz < LENGTH('a)
sbit \<le> sz
n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)

goal (1 subgoal):
 1. n * 2 ^ sbit < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> n * 2 ^ sbit < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> n * 2 ^ sbit \<le> ?y5
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> ?y5 < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit \<le> 2 ^ (sz - sbit) * 2 ^ sbit\<rbrakk> \<Longrightarrow> n * 2 ^ sbit \<le> ?y5
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> ?y5 < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit \<le> ?y5
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> ?y5 < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma range_cover_n_le:
  "n \<le> 2 ^ (len_of TYPE('a) - sbit)"
  "n \<le> 2 ^ (sz - sbit)" using aligned sz by (auto elim: le_trans[OF add_leD1])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> 2 ^ (LENGTH('a) - sbit) &&& n \<le> 2 ^ (sz - sbit) proof (prove)
using this:
is_aligned ptr sbit
sz < LENGTH('a)
sbit \<le> sz
n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)

goal (1 subgoal):
 1. n \<le> 2 ^ (LENGTH('a) - sbit) &&& n \<le> 2 ^ (sz - sbit)
theory Retype_AI

lemma range_cover_n_less:
  shows weak: "n < 2 ^ len_of TYPE('a)"
  and string: "n < 2 ^ (len_of TYPE('a) - sbit)" proof - show str: "n < 2 ^ (len_of TYPE('a) - sbit)" using aligned sz by (auto intro: le_less_trans range_cover_n_le(2)) show "n<2^len_of TYPE('a)" using str by (rule less_le_trans) simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 2 ^ LENGTH('a) &&& n < 2 ^ (LENGTH('a) - sbit) proof (state)
goal (2 subgoals):
 1. n < 2 ^ LENGTH('a)
 2. n < 2 ^ (LENGTH('a) - sbit) proof (prove)
goal (1 subgoal):
 1. n < 2 ^ (LENGTH('a) - sbit) proof (prove)
using this:
is_aligned ptr sbit
sz < LENGTH('a)
sbit \<le> sz
n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)

goal (1 subgoal):
 1. n < 2 ^ (LENGTH('a) - sbit) proof (state)
this:
n < 2 ^ (LENGTH('a) - sbit)

goal (1 subgoal):
 1. n < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. n < 2 ^ LENGTH('a) proof (prove)
using this:
n < 2 ^ (LENGTH('a) - sbit)

goal (1 subgoal):
 1. n < 2 ^ LENGTH('a) proof (state)
this:
n < 2 ^ LENGTH('a)

goal:
No subgoals!
theory Retype_AI

lemma range_cover_le_n_less:
  "p \<le> n \<Longrightarrow> p < 2^ len_of TYPE('a)"
  "p \<le> n \<Longrightarrow> p < 2^ (len_of TYPE('a) - sbit)" apply (erule le_less_trans[OF _ range_cover_n_less(1)]) apply (erule le_less_trans[OF _ range_cover_n_less(2)]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p \<le> n \<Longrightarrow> p < 2 ^ LENGTH('a)) &&& (p \<le> n \<Longrightarrow> p < 2 ^ (LENGTH('a) - sbit)) proof (prove)
goal (1 subgoal):
 1. p \<le> n \<Longrightarrow> p < 2 ^ (LENGTH('a) - sbit) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma unat_of_nat_n :"unat ((of_nat n):: 'a :: len word) = n" using range_cover_n_less by (simp add:unat_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat n) = n proof (prove)
using this:
n < 2 ^ LENGTH('a)
n < 2 ^ (LENGTH('a) - sbit)

goal (1 subgoal):
 1. unat (word_of_nat n) = n
theory Retype_AI

lemma range_cover_base_le:
  "(ptr && mask sz) \<le> (ptr && mask sz) + (of_nat n << sbit)" apply (clarsimp simp:no_olen_add_nat shiftl_t2n unat_of_nat_shift field_simps) apply (subst add.commute) apply (rule le_less_trans[OF range_cover_compare_bound]) apply (rule less_le_trans[OF power_strict_increasing]) using sz apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat n << sbit) proof (prove)
goal (1 subgoal):
 1. unat (ptr && mask sz) + n * 2 ^ sbit < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. n * 2 ^ sbit + unat (ptr && mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. 2 ^ sz < 2 ^ LENGTH('a) proof (prove)
goal (3 subgoals):
 1. sz < ?N3
 2. 1 < 2
 3. 2 ^ ?N3 \<le> 2 ^ LENGTH('a) proof (prove)
using this:
sz < LENGTH('a)
sbit \<le> sz
n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)

goal (3 subgoals):
 1. sz < ?N3
 2. 1 < 2
 3. 2 ^ ?N3 \<le> 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma pspace_no_overlapE:
  "\<lbrakk> pspace_no_overlap S s; kheap s x = Some ko;
  {x..x + (2 ^ obj_bits ko - 1)} \<inter> S = {} \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" unfolding pspace_no_overlap_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap S s; kheap s x = Some ko; {x..x + (2 ^ obj_bits ko - 1)} \<inter> S = {} \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x ko. kheap s x = Some ko \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> S = {}; kheap s x = Some ko; {x..x + (2 ^ obj_bits ko - 1)} \<inter> S = {} \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Retype_AI

lemma base_member_set:
  fixes x :: "'a :: len word"
  assumes al: "is_aligned x sz"
  and    szv: "sz < len_of TYPE('a)"
  shows "x \<in> {x .. x + (2 ^ sz - 1)}" proof (simp, rule is_aligned_no_wrap') show "(2 :: 'a :: len word) ^ sz - 1 < 2 ^ sz" using szv by (simp add: word_less_nat_alt word_neq_0_conv unat_minus_one) qed fact+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {x..x + (2 ^ sz - 1)} proof (state)
goal (2 subgoals):
 1. is_aligned x ?sz
 2. 2 ^ sz - 1 < 2 ^ ?sz proof (prove)
goal (1 subgoal):
 1. 2 ^ sz - 1 < 2 ^ sz proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. 2 ^ sz - 1 < 2 ^ sz proof (state)
this:
2 ^ sz - 1 < 2 ^ sz

goal (1 subgoal):
 1. is_aligned x sz
theory Retype_AI

lemma pspace_no_overlapD1:
  "\<lbrakk> pspace_no_overlap_range_cover ptr sz s; kheap s x = Some ko;
  range_cover ptr sz (obj_bits_api ty us) n;
  valid_pspace s\<rbrakk> \<Longrightarrow>
  x \<notin> set (retype_addrs ptr ty n us)" apply (drule(2) pspace_no_overlap_into_Int_none) apply (simp add:range_cover_def) apply (erule orthD2) apply (erule domI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; kheap s x = Some ko; range_cover ptr sz (obj_bits_api ty us) n; valid_pspace s\<rbrakk> \<Longrightarrow> x \<notin> set (retype_addrs ptr ty n us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some ko; range_cover ptr sz (obj_bits_api ty us) n; valid_pspace s; set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {}\<rbrakk> \<Longrightarrow> x \<notin> set (retype_addrs ptr ty n us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some ko; is_aligned ptr (obj_bits_api ty us) \<and> sz < 32 \<and> obj_bits_api ty us \<le> sz \<and> n + unat (ptr && mask sz >> obj_bits_api ty us) \<le> 2 ^ (sz - obj_bits_api ty us); valid_pspace s; set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {}\<rbrakk> \<Longrightarrow> x \<notin> set (retype_addrs ptr ty n us) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some ko; is_aligned ptr (obj_bits_api ty us) \<and> sz < 32 \<and> obj_bits_api ty us \<le> sz \<and> n + unat (ptr && mask sz >> obj_bits_api ty us) \<le> 2 ^ (sz - obj_bits_api ty us); valid_pspace s\<rbrakk> \<Longrightarrow> x \<in> dom (kheap s) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma pspace_no_overlapD2:
  "\<lbrakk> pspace_no_overlap_range_cover ptr sz s; x \<in> set (retype_addrs ptr ty n us);
  range_cover ptr sz (obj_bits_api ty us) n;
   valid_pspace s \<rbrakk> \<Longrightarrow> x \<notin> dom (kheap s)" apply (drule(2) pspace_no_overlap_into_Int_none) apply (simp add:range_cover_def) apply (erule(1) orthD1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; x \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; valid_pspace s\<rbrakk> \<Longrightarrow> x \<notin> dom (kheap s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n; valid_pspace s; set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {}\<rbrakk> \<Longrightarrow> x \<notin> dom (kheap s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set (retype_addrs ptr ty n us); is_aligned ptr (obj_bits_api ty us) \<and> sz < 32 \<and> obj_bits_api ty us \<le> sz \<and> n + unat (ptr && mask sz >> obj_bits_api ty us) \<le> 2 ^ (sz - obj_bits_api ty us); valid_pspace s; set (retype_addrs ptr ty n us) \<inter> dom (kheap s) = {}\<rbrakk> \<Longrightarrow> x \<notin> dom (kheap s) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma pspace_no_overlapC:
  "\<lbrakk> pspace_no_overlap_range_cover ptr sz s; x \<in> set (retype_addrs ptr ty n us); kheap s x = Some ko;
  range_cover ptr sz (obj_bits_api ty us) n;valid_pspace s \<rbrakk> \<Longrightarrow> P" by (auto dest: pspace_no_overlapD1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; x \<in> set (retype_addrs ptr ty n us); kheap s x = Some ko; range_cover ptr sz (obj_bits_api ty us) n; valid_pspace s\<rbrakk> \<Longrightarrow> P
theory Retype_AI

lemma null_filterE:
  "\<lbrakk> null_filter cps x = Some cap;
      \<lbrakk> cps x = Some cap; cap \<noteq> cap.NullCap \<rbrakk> \<Longrightarrow> R \<rbrakk>
     \<Longrightarrow> R" by (simp add: null_filter_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>null_filter cps x = Some cap; \<lbrakk>cps x = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Retype_AI

lemma mdb_cte_at_no_descendants:
  "\<lbrakk> mdb_cte_at f m; \<not> f x \<rbrakk> \<Longrightarrow> descendants_of x m = {}" apply (clarsimp simp add: descendants_of_def) apply (erule tranclE2) apply (simp add: cdt_parent_of_def) apply (drule(1) mdb_cte_atD) apply simp apply (simp add: cdt_parent_of_def) apply (drule(1) mdb_cte_atD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at f m; \<not> f x\<rbrakk> \<Longrightarrow> descendants_of x m = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>mdb_cte_at f m; \<not> f x; m \<Turnstile> x \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>mdb_cte_at f m; \<not> f x; m \<Turnstile> x \<leadsto> (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b c. \<lbrakk>mdb_cte_at f m; \<not> f x; m \<Turnstile> x \<leadsto> c; m \<Turnstile> c \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>mdb_cte_at f m; \<not> f x; m (a, b) = Some x\<rbrakk> \<Longrightarrow> False
 2. \<And>a b c. \<lbrakk>mdb_cte_at f m; \<not> f x; m \<Turnstile> x \<leadsto> c; m \<Turnstile> c \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>mdb_cte_at f m; \<not> f x; f x \<and> f (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b c. \<lbrakk>mdb_cte_at f m; \<not> f x; m \<Turnstile> x \<leadsto> c; m \<Turnstile> c \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>mdb_cte_at f m; \<not> f x; m \<Turnstile> x \<leadsto> c; m \<Turnstile> c \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>mdb_cte_at f m; \<not> f x; m c = Some x; m \<Turnstile> c \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>mdb_cte_at f m; \<not> f x; m \<Turnstile> c \<rightarrow> (a, b); f x \<and> f c\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma retype_addrs_fold:
  " map (\<lambda>p. ptr_add ptr' (p * 2 ^ obj_bits_api ty us)) [0..< n ]
  = retype_addrs ptr' ty n us" by (simp add: retype_addrs_def power_sub)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>p. ptr_add ptr' (p * 2 ^ obj_bits_api ty us)) [0..<n] = retype_addrs ptr' ty n us
theory Retype_AI

lemma mult_div_rearrange:
  "(b::nat) \<le> a \<Longrightarrow> (2::nat) ^ a * (p div 2 ^ b) =
   2 ^ (a - b) * (2 ^ b * (p div 2 ^ b))" by (auto simp:field_simps power_add[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<le> a \<Longrightarrow> 2 ^ a * (p div 2 ^ b) = 2 ^ (a - b) * (2 ^ b * (p div 2 ^ b))
theory Retype_AI

lemma shiftr_mask_cmp:
  "\<lbrakk>c \<le> n; n \<le> len_of TYPE('a)\<rbrakk>
   \<Longrightarrow> ((a::('a::len) word) \<le> mask n) = ((a >> c) \<le> mask (n - c))" apply (rule iffI) apply (drule le_shiftr[where n = c]) apply (simp add:mask_2pm1[symmetric] shiftr_mask2)+ apply (simp add:le_mask_iff shiftr_shiftr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<le> n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> (a \<le> mask n) = (a >> c \<le> mask (n - c)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<le> n; n \<le> LENGTH('a); a \<le> mask n\<rbrakk> \<Longrightarrow> a >> c \<le> mask (n - c)
 2. \<lbrakk>c \<le> n; n \<le> LENGTH('a); a >> c \<le> mask (n - c)\<rbrakk> \<Longrightarrow> a \<le> mask n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<le> n; n \<le> LENGTH('a); a >> c \<le> mask n >> c\<rbrakk> \<Longrightarrow> a >> c \<le> mask (n - c)
 2. \<lbrakk>c \<le> n; n \<le> LENGTH('a); a >> c \<le> mask (n - c)\<rbrakk> \<Longrightarrow> a \<le> mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<le> n; n \<le> LENGTH('a); a >> c \<le> mask (n - c)\<rbrakk> \<Longrightarrow> a \<le> mask n proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma  measure_unat': "p \<noteq> 0 \<Longrightarrow> unat (p - 1) \<le>  unat p - 1" apply (insert measure_unat[where p = p]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> unat (p - 1) \<le> unat p - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> 0; p \<noteq> 0 \<Longrightarrow> unat (p - 1) < unat p\<rbrakk> \<Longrightarrow> unat (p - 1) \<le> unat p - 1 proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma range_cover_not_zero:
  "\<lbrakk>n \<noteq> 0; range_cover (ptr :: 'a :: len word) sz bits n\<rbrakk> \<Longrightarrow> ((of_nat n) :: 'a :: len word) \<noteq> 0" apply (rule of_nat_neq_0) apply simp apply (drule range_cover.range_cover_n_less) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n\<rbrakk> \<Longrightarrow> 0 < n
 2. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; n < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma mult_plus_1: "(a::nat) + b * a = a * (b + 1)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + b * a = a * (b + 1)
theory Retype_AI

lemma is_aligned_ptr_add_helper:
  "\<lbrakk> is_aligned ptr d; d < word_bits; c \<le> d; c \<le> a + b;
     a + b < word_bits \<rbrakk> \<Longrightarrow> is_aligned (ptr_add ptr (x * 2 ^ a * 2 ^ b)) c" apply (simp add: ptr_add_def) apply (erule aligned_add_aligned) apply (rule is_aligned_weaken) apply (simp add: field_simps
                      power_add[symmetric]) apply (rule is_aligned_mult_triv2) apply assumption+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr d; d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> is_aligned (ptr_add ptr (x * 2 ^ a * 2 ^ b)) c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr d; d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat x * 2 ^ a * 2 ^ b) c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat x * 2 ^ a * 2 ^ b) c
 2. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> c \<le> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat x * 2 ^ a * 2 ^ b) ?x3
 2. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> c \<le> ?x3
 3. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> c \<le> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> is_aligned (word_of_nat x * 2 ^ (a + b)) ?x3
 2. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> c \<le> ?x3
 3. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> c \<le> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> c \<le> a + b
 2. \<lbrakk>d < word_bits; c \<le> d; c \<le> a + b; a + b < word_bits\<rbrakk> \<Longrightarrow> c \<le> d proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma range_cover_mem':
  "\<lbrakk>x < of_nat n; range_cover ptr sz us n\<rbrakk>
   \<Longrightarrow> ptr + x * 2 ^ us \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}" apply (drule range_cover_mem[where x = "unat x",rotated]) apply (erule unat_less_helper) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < word_of_nat n; range_cover ptr sz us n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. x < word_of_nat n \<Longrightarrow> unat x < n
 2. \<lbrakk>x < word_of_nat n; ptr + word_of_nat (unat x) * 2 ^ us \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < word_of_nat n; ptr + word_of_nat (unat x) * 2 ^ us \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma range_cover_subset_not_empty:
  "\<lbrakk>x < of_nat n; range_cover ptr sz us n\<rbrakk>
   \<Longrightarrow> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}" apply (clarsimp simp:p_assoc_help) apply (rule is_aligned_no_overflow') apply (rule is_aligned_add_multI) apply (fastforce simp:range_cover_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < word_of_nat n; range_cover ptr sz us n\<rbrakk> \<Longrightarrow> {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < word_of_nat n; range_cover ptr sz us n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us \<le> ptr + x * 2 ^ us + (2 ^ us - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < word_of_nat n; range_cover ptr sz us n\<rbrakk> \<Longrightarrow> is_aligned (ptr + x * 2 ^ us) us proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x < word_of_nat n; range_cover ptr sz us n\<rbrakk> \<Longrightarrow> is_aligned ptr ?m2
 2. \<lbrakk>x < word_of_nat n; range_cover ptr sz us n\<rbrakk> \<Longrightarrow> us \<le> ?m2
 3. \<lbrakk>x < word_of_nat n; range_cover ptr sz us n\<rbrakk> \<Longrightarrow> us = us proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma do_machine_op_return_foo:
  "do_machine_op (do x\<leftarrow>a;return () od) = (do (do_machine_op a); return () od)" apply (clarsimp simp:do_machine_op_def bind_def' gets_def
    get_def return_def select_f_def split_def simpler_modify_def) apply (rule ext)+ apply (clarsimp simp:image_def) apply (rule set_eqI) apply clarsimp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do_machine_op (do x <- a;
return ()
od) = do do_machine_op a;
return ()
od proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ({p. \<exists>b. (\<exists>x\<in>fst (a (machine_state s)). b = snd x) \<and> snd p = s\<lparr>machine_state := b\<rparr>}, snd (a (machine_state s)))) = (\<lambda>s. ({p. \<exists>aa. \<exists>x\<in>fst (a (machine_state s)). aa = fst x \<and> snd p = s\<lparr>machine_state := snd x\<rparr>}, snd (a (machine_state s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s. ({p. \<exists>b. (\<exists>x\<in>fst (a (machine_state s)). b = snd x) \<and> snd p = s\<lparr>machine_state := b\<rparr>}, snd (a (machine_state s))) = ({p. \<exists>aa. \<exists>x\<in>fst (a (machine_state s)). aa = fst x \<and> snd p = s\<lparr>machine_state := snd x\<rparr>}, snd (a (machine_state s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. {p. \<exists>b. (\<exists>x\<in>fst (a (machine_state s)). b = snd x) \<and> snd p = s\<lparr>machine_state := b\<rparr>} = {p. \<exists>aa. \<exists>x\<in>fst (a (machine_state s)). aa = fst x \<and> snd p = s\<lparr>machine_state := snd x\<rparr>} proof (prove)
goal (1 subgoal):
 1. \<And>s x. (x \<in> {p. \<exists>b. (\<exists>x\<in>fst (a (machine_state s)). b = snd x) \<and> snd p = s\<lparr>machine_state := b\<rparr>}) = (x \<in> {p. \<exists>aa. \<exists>x\<in>fst (a (machine_state s)). aa = fst x \<and> snd p = s\<lparr>machine_state := snd x\<rparr>}) proof (prove)
goal (1 subgoal):
 1. \<And>s b. (\<exists>ba. (\<exists>x\<in>fst (a (machine_state s)). ba = snd x) \<and> b = s\<lparr>machine_state := ba\<rparr>) = (\<exists>aa. \<exists>x\<in>fst (a (machine_state s)). aa = fst x \<and> b = s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory Retype_AI

lemma all_invs_but_equal_kernel_mappings_restricted_eq:
  "all_invs_but_equal_kernel_mappings_restricted {}
        = invs" by (rule ext, simp add: invs_def valid_state_def conj_comms restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- {})\<rparr>)) and valid_pspace and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_irq_states and valid_global_objs and valid_arch_caps and valid_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and valid_ioc and valid_machine_state and valid_ioports) = invs