kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_DR

lemma retype_addrs_range_subset_strong:
  notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff
  shows "\<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk>
  \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}" apply (clarsimp simp: retype_addrs_def ptr_add_def) apply (drule_tac p = x in range_cover_subset) apply clarsimp+ apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>range_cover ptr sz (obj_bits_api ty us) n; x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> xa \<in> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> x < n
 2. \<And>x xa. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<And>x xa. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}; {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> xa \<in> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x < n; p = ptr + word_of_nat x * 2 ^ obj_bits_api ty us; xa \<in> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}; {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> xa \<in> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma le_p2_minus_1:
  "a \<le> (2^z - (Suc 0::nat)) \<Longrightarrow> a < 2^z" apply (subgoal_tac "(0 :: nat)< 2^z") apply arith apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> 2 ^ z - Suc 0 \<Longrightarrow> a < 2 ^ z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> 2 ^ z - Suc 0; 0 < 2 ^ z\<rbrakk> \<Longrightarrow> a < 2 ^ z
 2. a \<le> 2 ^ z - Suc 0 \<Longrightarrow> 0 < 2 ^ z proof (prove)
goal (1 subgoal):
 1. a \<le> 2 ^ z - Suc 0 \<Longrightarrow> 0 < 2 ^ z proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma in_empty_setE:
  "\<lbrakk>x\<in> A;x\<in> B; A\<inter> B = {}\<rbrakk> \<Longrightarrow> Q" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; x \<in> B; A \<inter> B = {}\<rbrakk> \<Longrightarrow> Q
theory Untyped_DR

lemma mapME_x_upt_length_ys:
  "mapME_x (\<lambda>_. f) [0 ..< length ys]
    = mapME_x (\<lambda>_. f) ys" by (metis mapME_x_map_simp[where f="\<lambda>_. ()" and m="\<lambda>_. m" for m,
            unfolded o_def] map_replicate_const length_upt minus_nat.diff_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x (\<lambda>_. f) [0..<length ys] = mapME_x (\<lambda>_. f) ys
theory Untyped_DR

lemma mapME_x_append:
  "mapME_x f (xs @ ys) = (doE mapME_x f xs; mapME_x f ys odE)" apply (induct xs) apply (simp add: mapME_x_Nil) apply (simp add: mapME_x_Cons bindE_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x f (xs @ ys) = doE mapME_x f xs;
mapME_x f ys
odE proof (prove)
goal (2 subgoals):
 1. mapME_x f ([] @ ys) = doE mapME_x f [];
mapME_x f ys
odE
 2. \<And>a xs. mapME_x f (xs @ ys) = doE mapME_x f xs;
mapME_x f ys
odE \<Longrightarrow> mapME_x f ((a # xs) @ ys) = doE mapME_x f (a # xs);
mapME_x f ys
odE proof (prove)
goal (1 subgoal):
 1. \<And>a xs. mapME_x f (xs @ ys) = doE mapME_x f xs;
mapME_x f ys
odE \<Longrightarrow> mapME_x f ((a # xs) @ ys) = doE mapME_x f (a # xs);
mapME_x f ys
odE proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma hd_filter_eq:
  "P (hd xs) \<Longrightarrow> hd (filter P xs) = hd xs" by (cases xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (hd xs) \<Longrightarrow> hd (filter P xs) = hd xs
theory Untyped_DR

lemma corres_whenE_throwError_split_rhs:
  "corres_underlying sr nf nf' r P Q a (whenE G (throwError e) >>=E (\<lambda>_. b))
     = ((G \<longrightarrow> corres_underlying sr nf nf' r P Q a (throwError e))
           \<and> (\<not> G \<longrightarrow> corres_underlying sr nf nf' r P Q a b))" by (simp add: whenE_bindE_throwError_to_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P Q a (doE _ <- whenE G (throwError e);
b
odE) = ((G \<longrightarrow> corres_underlying sr nf nf' r P Q a (throwError e)) \<and> (\<not> G \<longrightarrow> corres_underlying sr nf nf' r P Q a b))
theory Untyped_DR

lemma nat_bl_to_bin_nat_to_cref:
  assumes asms: "x < 2 ^ bits" "bits < word_bits"
  shows "nat (bl_to_bin (nat_to_cref bits x)) = x" proof - note of_bl = of_bl_nat_to_cref[OF asms] have lt_bl: "bl_to_bin (nat_to_cref bits x) < 2 ^ 32" apply (rule order_less_le_trans, rule bl_to_bin_lt2p) apply (rule power_increasing) apply (simp add: nat_to_cref_def) apply simp done have lt_x: "x < 2 ^ 32" apply (rule order_less_le_trans, rule asms) apply (rule power_increasing, simp_all) apply (insert asms word_bits_conv, simp) done show ?thesis using of_bl lt_bl lt_x apply (simp add: of_bl_def) apply (erule word_of_int_word_of_nat_eqD; simp add: bl_to_bin_ge0) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (nat_to_cref bits x)) = x proof (state)
goal (1 subgoal):
 1. nat (bl_to_bin (nat_to_cref bits x)) = x proof (state)
this:
of_bl (nat_to_cref bits x) = word_of_nat x

goal (1 subgoal):
 1. nat (bl_to_bin (nat_to_cref bits x)) = x proof (prove)
goal (1 subgoal):
 1. bl_to_bin (nat_to_cref bits x) < 2 ^ 32 proof (prove)
goal (1 subgoal):
 1. 2 ^ length (nat_to_cref bits x) \<le> 2 ^ 32 proof (prove)
goal (2 subgoals):
 1. length (nat_to_cref bits x) \<le> 32
 2. 1 \<le> 2 proof (prove)
goal (1 subgoal):
 1. 1 \<le> 2 proof (prove)
goal:
No subgoals! proof (state)
this:
bl_to_bin (nat_to_cref bits x) < 2 ^ 32

goal (1 subgoal):
 1. nat (bl_to_bin (nat_to_cref bits x)) = x proof (prove)
goal (1 subgoal):
 1. x < 2 ^ 32 proof (prove)
goal (1 subgoal):
 1. 2 ^ bits \<le> 2 ^ 32 proof (prove)
goal (1 subgoal):
 1. bits \<le> 32 proof (prove)
goal:
No subgoals! proof (state)
this:
x < 2 ^ 32

goal (1 subgoal):
 1. nat (bl_to_bin (nat_to_cref bits x)) = x proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (nat_to_cref bits x)) = x proof (prove)
using this:
of_bl (nat_to_cref bits x) = word_of_nat x
bl_to_bin (nat_to_cref bits x) < 2 ^ 32
x < 2 ^ 32

goal (1 subgoal):
 1. nat (bl_to_bin (nat_to_cref bits x)) = x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_of_int (bl_to_bin (nat_to_cref bits x)) = word_of_nat x; bl_to_bin (nat_to_cref bits x) < 4294967296; x < 4294967296\<rbrakk> \<Longrightarrow> nat (bl_to_bin (nat_to_cref bits x)) = x proof (prove)
goal:
No subgoals! proof (state)
this:
nat (bl_to_bin (nat_to_cref bits x)) = x

goal:
No subgoals!
theory Untyped_DR

lemma mapME_x_inv_wp2:
  "(\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>,\<lbrace>\<lambda>rv. E\<rbrace>)
      \<Longrightarrow> \<lbrace>P and E\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>\<lambda>rv. E\<rbrace>" apply (rule hoare_post_impErr) apply (rule mapME_x_inv_wp[where E="\<lambda>_. E"]) apply (rule hoare_post_impErr, assumption) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>) \<Longrightarrow> \<lbrace>P and E\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace> proof (prove)
goal (3 subgoals):
 1. (\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>) \<Longrightarrow> \<lbrace>P and E\<rbrace> mapME_x f xs \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>; ?Q rv s\<rbrakk> \<Longrightarrow> P s
 3. \<And>e s. \<lbrakk>\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>; ?E e s\<rbrakk> \<Longrightarrow> E s proof (prove)
goal (3 subgoals):
 1. \<And>x. (\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>) \<Longrightarrow> \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>
 2. \<And>rv s. \<lbrakk>\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>; (P and E) s\<rbrakk> \<Longrightarrow> P s
 3. \<And>e s. \<lbrakk>\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>; E s\<rbrakk> \<Longrightarrow> E s proof (prove)
goal (4 subgoals):
 1. \<And>x rv s. \<lbrakk>\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>; (P and E) s\<rbrakk> \<Longrightarrow> (P and E) s
 2. \<And>x e s. \<lbrakk>\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>; E s\<rbrakk> \<Longrightarrow> E s
 3. \<And>rv s. \<lbrakk>\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>; (P and E) s\<rbrakk> \<Longrightarrow> P s
 4. \<And>e s. \<lbrakk>\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>, \<lbrace>\<lambda>rv. E\<rbrace>; E s\<rbrakk> \<Longrightarrow> E s proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma gets_get:
  "get = gets id " by (simp add:gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get = gets id
theory Untyped_DR

lemma transform_cdt_dom_standard:
  "transform_cdt s' slot' = Some (transform_cslot_ptr b)
   \<Longrightarrow> \<exists>slot. slot' = transform_cslot_ptr slot" apply (case_tac b) apply (fastforce simp:transform_cdt_def map_lift_over_def split:if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cdt s' slot' = Some (transform_cslot_ptr b) \<Longrightarrow> \<exists>slot. slot' = transform_cslot_ptr slot proof (prove)
goal (1 subgoal):
 1. \<And>a ba. \<lbrakk>transform_cdt s' slot' = Some (transform_cslot_ptr b); b = (a, ba)\<rbrakk> \<Longrightarrow> \<exists>slot. slot' = transform_cslot_ptr slot proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma alignUp_gt_0:
  "\<lbrakk>is_aligned (x :: 'a :: len word) n; n < len_of TYPE('a); x \<noteq> 0 ; a \<le> x\<rbrakk> \<Longrightarrow> (0 < alignUp a n) = (a \<noteq> 0)" apply (rule iffI) apply (rule ccontr) apply (clarsimp simp:not_less alignUp_def2 mask_def) apply (frule(1) alignUp_is_aligned_nz[where a = a]) apply (simp add:unat_1_0) apply simp apply (simp add:word_neq_0_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x\<rbrakk> \<Longrightarrow> (0 < alignUp a n) = (a \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; 0 < alignUp a n\<rbrakk> \<Longrightarrow> a \<noteq> 0
 2. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; a \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < alignUp a n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; 0 < alignUp a n; \<not> a \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; a \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < alignUp a n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; a \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < alignUp a n proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; a \<noteq> 0\<rbrakk> \<Longrightarrow> a \<le> x
 2. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; a \<noteq> 0\<rbrakk> \<Longrightarrow> a \<noteq> 0
 3. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; a \<noteq> 0; alignUp a n \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < alignUp a n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; a \<noteq> 0\<rbrakk> \<Longrightarrow> a \<noteq> 0
 2. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; a \<noteq> 0; alignUp a n \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < alignUp a n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; n < LENGTH('a); x \<noteq> 0; a \<le> x; a \<noteq> 0; alignUp a n \<noteq> 0\<rbrakk> \<Longrightarrow> 0 < alignUp a n proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma corres_symb_exec_in_gets:
  "corres_underlying sr nf nf' r P P' f (gets g >>= j)
    = (\<forall>v. corres_underlying sr nf nf' r P (P' and (\<lambda>s. g s = v)) f (j v))"
  "corres_underlying sr nf nf' r P P' (gets g' >>= j') f'
    = (\<forall>v. corres_underlying sr nf nf' r (P and (\<lambda>s. g' s = v)) P' (j' v) f')" by (auto simp add: corres_underlying_def exec_gets split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' f (gets g >>= j) = (\<forall>v. corres_underlying sr nf nf' r P (P' and (\<lambda>s. g s = v)) f (j v)) &&& corres_underlying sr nf nf' r P P' (gets g' >>= j') f' = (\<forall>v. corres_underlying sr nf nf' r (P and (\<lambda>s. g' s = v)) P' (j' v) f')
theory Arch_DR

lemma select_ignored:
  "select S >>= (\<lambda>_. f) = (if S = {} then select {} else f)" apply (intro ext) apply (simp add: select_def bind_def cart_singleton_image
                   image_image image_constant_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- select S;
f
od = (if S = {} then select {} else f) proof (prove)
goal (1 subgoal):
 1. \<And>x. (do _ <- select S;
f
od) x = (if S = {} then select {} else f) x proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma liftM_select:
  "liftM f (select S) = select (f ` S)" apply (rule ext) apply (auto simp add: select_def bind_def liftM_def return_def split_def
                        cart_singleton_image image_image) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftM f (select S) = select (f ` S) proof (prove)
goal (1 subgoal):
 1. \<And>x. liftM f (select S) x = select (f ` S) x proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma gets_bind_alternative:
  "((gets f >>= g) \<sqinter> h) = gets f >>= (\<lambda>x. g x \<sqinter> h)" by (rule ext, simp add: alternative_def exec_gets)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (gets f >>= g \<sqinter> h) = do x <- gets f;
g x \<sqinter> h
od
theory Arch_DR

lemma corres_from_rdonly:
  assumes rdonly: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>" "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. P\<rbrace>"
  assumes rv: "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk>
                     \<Longrightarrow> \<lbrace>(=) s'\<rbrace> g \<lbrace>\<lambda>rv s''. \<exists>rv' s'''. (rv', s''') \<in> fst (f s) \<and> r rv' rv\<rbrace>"
  assumes nfl: "fl' \<Longrightarrow> no_fail P' g"
  shows "corres_underlying sr fl fl' r P P' f g" apply (clarsimp simp: corres_underlying_def no_failD[OF nfl]) apply (frule in_inv_by_hoareD[OF rdonly(2)], simp) apply (frule(3) use_valid[OF _ rv], simp) apply clarsimp apply (frule in_inv_by_hoareD[OF rdonly(1)], simp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr fl fl' r P P' f g proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; fl \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> sr \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; fl \<longrightarrow> \<not> snd (f a); (aa, b) \<in> fst (g b); ba = b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, b) \<in> sr \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; fl \<longrightarrow> \<not> snd (f a); (aa, b) \<in> fst (g b); ba = b; \<exists>rv' s'''. (rv', s''') \<in> fst (f a) \<and> r rv' aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, b) \<in> sr \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa rv' s'''. \<lbrakk>(a, b) \<in> sr; P a; P' b; fl \<longrightarrow> \<not> snd (f a); (aa, b) \<in> fst (g b); r rv' aa; (rv', s''') \<in> fst (f a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, b) \<in> sr \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa rv' s'''. \<lbrakk>(a, b) \<in> sr; P a; P' b; fl \<longrightarrow> \<not> snd (f a); (aa, b) \<in> fst (g b); r rv' aa; (rv', a) \<in> fst (f a); s''' = a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, b) \<in> sr \<and> r ra aa proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma get_pde_sp:
  "\<lbrace>P\<rbrace> get_pde p \<lbrace>\<lambda>pde s. \<exists>pd. ko_at (ArchObj (arch_kernel_obj.PageDirectory pd)) (p && ~~ mask pd_bits) s
                                   \<and> pde = (pd (ucast (p && mask pd_bits >> 2))) \<and> P s\<rbrace>" apply (wp get_pde_wp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_pde p \<lbrace>\<lambda>pde s. \<exists>pd. ako_at (arch_kernel_obj.PageDirectory pd) (p && ~~ mask pd_bits) s \<and> pde = pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<and> P s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> \<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (\<exists>pda. ako_at (arch_kernel_obj.PageDirectory pda) (p && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) = pda (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) \<and> P s) proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma shiftl_mod:
  "\<lbrakk> n < 32; (x :: word32) < 2 ^ (32 - n) \<rbrakk> \<Longrightarrow> unat (x << n) mod 2 ^ n = 0" apply (subst shiftl_t2n) apply (clarsimp simp:unat_word_ariths) apply (subgoal_tac "2 ^ n * unat x < 2 ^ 32") apply (clarsimp) apply (subst (asm) word_unat_power) apply (drule unat_less_helper) apply (rule_tac y="2^n * 2 ^(32-n)" in less_le_trans) apply simp apply (simp add:power_add[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 32; x < 2 ^ (32 - n)\<rbrakk> \<Longrightarrow> unat (x << n) mod 2 ^ n = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 32; x < 2 ^ (32 - n)\<rbrakk> \<Longrightarrow> unat (2 ^ n * x) mod 2 ^ n = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 32; x < 2 ^ (32 - n)\<rbrakk> \<Longrightarrow> 2 ^ n * unat x mod 4294967296 mod 2 ^ n = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 32; x < 2 ^ (32 - n); 2 ^ n * unat x < 2 ^ 32\<rbrakk> \<Longrightarrow> 2 ^ n * unat x mod 4294967296 mod 2 ^ n = 0
 2. \<lbrakk>n < 32; x < 2 ^ (32 - n)\<rbrakk> \<Longrightarrow> 2 ^ n * unat x < 2 ^ 32 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 32; x < 2 ^ (32 - n)\<rbrakk> \<Longrightarrow> 2 ^ n * unat x < 2 ^ 32 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 32; x < word_of_nat (2 ^ (32 - n))\<rbrakk> \<Longrightarrow> 2 ^ n * unat x < 2 ^ 32 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 32; unat x < 2 ^ (32 - n)\<rbrakk> \<Longrightarrow> 2 ^ n * unat x < 2 ^ 32 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 32; unat x < 2 ^ (32 - n)\<rbrakk> \<Longrightarrow> 2 ^ n * unat x < 2 ^ n * 2 ^ (32 - n)
 2. \<lbrakk>n < 32; unat x < 2 ^ (32 - n)\<rbrakk> \<Longrightarrow> 2 ^ n * 2 ^ (32 - n) \<le> 2 ^ 32 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 32; unat x < 2 ^ (32 - n)\<rbrakk> \<Longrightarrow> 2 ^ n * 2 ^ (32 - n) \<le> 2 ^ 32 proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma to_select_ret_or_throw:
  "returnOk x = select_ret_or_throw {x} {}"
  "throwError e = select_ret_or_throw {} {e}"
  "alternative (select_ret_or_throw S X) (select_ret_or_throw S' X')
    = select_ret_or_throw (S \<union> S') (X \<union> X')" apply (simp_all add: select_ret_or_throw_def alternative_def returnOk_def return_def
                       select_def bind_def throwError_def) apply (simp add: Sigma_def return_def Un_ac) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. returnOk x = select_ret_or_throw {x} {} &&& throwError e = select_ret_or_throw {} {e} &&& (select_ret_or_throw S X \<sqinter> select_ret_or_throw S' X') = select_ret_or_throw (S \<union> S') (X \<union> X') proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ((\<Union>a\<in>S \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (return \<circ> Inr) x xa)) \<union> (\<Union>a\<in>X \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (return \<circ> Inl) x xa)) \<union> ((\<Union>a\<in>S' \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (return \<circ> Inr) x xa)) \<union> (\<Union>a\<in>X' \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (return \<circ> Inl) x xa))), False)) = (\<lambda>s. ((\<Union>a\<in>(S \<union> S') \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (return \<circ> Inr) x xa)) \<union> (\<Union>a\<in>(X \<union> X') \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (return \<circ> Inl) x xa)), False)) proof (prove)
goal:
No subgoals!
theory Arch_DR

lemma select_ret_or_throw_twice:
  "(do _ \<leftarrow> select_ret_or_throw S X; select_ret_or_throw S X od)
    = select_ret_or_throw S X" apply (simp add: select_ret_or_throw_def alternative_def returnOk_def return_def
                       select_def bind_def throwError_def Sigma_def) apply (rule ext, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- select_ret_or_throw S X;
select_ret_or_throw S X
od = select_ret_or_throw S X proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ((if S = {} then {} else (\<Union>x\<in>S. {(Inr x, s)}) \<union> (\<Union>x\<in>S. \<Union>x\<in>X. {(Inl x, s)})) \<union> (if X = {} then {} else (\<Union>x\<in>S. {(Inr x, s)}) \<union> (\<Union>x\<in>X. \<Union>x\<in>X. {(Inl x, s)})), \<exists>x\<in>(\<Union>x\<in>S. {(Inr x, s)}) \<union> (\<Union>x\<in>X. {(Inl x, s)}). snd (case x of (uu_, s) \<Rightarrow> ((\<Union>x\<in>S. {(Inr x, s)}) \<union> (\<Union>x\<in>X. {(Inl x, s)}), False)))) = (\<lambda>s. ((\<Union>x\<in>S. {(Inr x, s)}) \<union> (\<Union>x\<in>X. {(Inl x, s)}), False)) proof (prove)
goal:
No subgoals!