kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_DR

lemma dcorres_splits:
  "\<lbrakk> T a \<Longrightarrow> dcorres r P (Q a) f (g a);
    \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a)\<rbrakk>\<Longrightarrow>
    dcorres r P ( (\<lambda>s. (T a) \<longrightarrow> (Q a s)) and (\<lambda>s. (\<not> (T a)) \<longrightarrow> (Q' a s)) ) f (g a)" apply (case_tac "T a") apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T a \<Longrightarrow> dcorres r P (Q a) f (g a); \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a)\<rbrakk> \<Longrightarrow> dcorres r P ((\<lambda>s. T a \<longrightarrow> Q a s) and (\<lambda>s. \<not> T a \<longrightarrow> Q' a s)) f (g a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>T a \<Longrightarrow> dcorres r P (Q a) f (g a); \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a); T a\<rbrakk> \<Longrightarrow> dcorres r P ((\<lambda>s. T a \<longrightarrow> Q a s) and (\<lambda>s. \<not> T a \<longrightarrow> Q' a s)) f (g a)
 2. \<lbrakk>T a \<Longrightarrow> dcorres r P (Q a) f (g a); \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a); \<not> T a\<rbrakk> \<Longrightarrow> dcorres r P ((\<lambda>s. T a \<longrightarrow> Q a s) and (\<lambda>s. \<not> T a \<longrightarrow> Q' a s)) f (g a) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma dcorres_alternate_seq1:
  "corres_underlying t nf nf' r P Q (do y \<leftarrow> f; g y od) rh
    \<Longrightarrow> corres_underlying t nf nf' r P Q (do y \<leftarrow> f; g y \<sqinter> h y od) rh" apply (simp add:alternative_distrib2) apply (erule corres_alternate1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying t nf nf' r P Q (f >>= g) rh \<Longrightarrow> corres_underlying t nf nf' r P Q (do y <- f;
g y \<sqinter> h y
od) rh proof (prove)
goal (1 subgoal):
 1. corres_underlying t nf nf' r P Q (f >>= g) rh \<Longrightarrow> corres_underlying t nf nf' r P Q (f >>= g \<sqinter> f >>= h) rh proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma dcorres_alternate_seq2:
  "corres_underlying t nf nf' r P Q (do y \<leftarrow> f; h y od) rh
    \<Longrightarrow> corres_underlying t nf nf' r P Q (do y \<leftarrow> f; g y \<sqinter> h y od) rh" apply (simp add:alternative_distrib2) apply (erule corres_alternate2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying t nf nf' r P Q (f >>= h) rh \<Longrightarrow> corres_underlying t nf nf' r P Q (do y <- f;
g y \<sqinter> h y
od) rh proof (prove)
goal (1 subgoal):
 1. corres_underlying t nf nf' r P Q (f >>= h) rh \<Longrightarrow> corres_underlying t nf nf' r P Q (f >>= g \<sqinter> f >>= h) rh proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma tcb_fault_update_valid_state[wp]:
  "\<lbrace>invs and (\<lambda>_. valid_fault ft')\<rbrace>
   thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread
   \<lbrace>\<lambda>rv. valid_state\<rbrace>" apply (cases "valid_fault ft'"; simp) apply (strengthen invs_valid_stateI, wp thread_set_tcb_fault_set_invs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>_. valid_fault ft')\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>\<lambda>rv. valid_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_fault ft' \<Longrightarrow> \<lbrace>invs\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>\<lambda>rv. valid_state\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma thread_set_fault_obj_at:
 "\<lbrace>tcb_at thread\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread
  \<lbrace>\<lambda>rv s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (False \<or> (\<exists>y. tcb_fault tcb = Some y)) = True) thread s\<rbrace>" apply (simp add: thread_set_def) apply (wpsimp wp: set_object_wp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at thread\<rbrace> thread_set (tcb_fault_update (\<lambda>_. Some ft')) thread \<lbrace>\<lambda>rv. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (False \<or> (\<exists>y. tcb_fault tcb = Some y)) = True) thread\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at thread\<rbrace> do tcb <- gets_the (get_tcb thread);
KHeap_A.set_object thread (TCB (tcb\<lparr>tcb_fault := Some ft'\<rparr>))
od \<lbrace>\<lambda>rv. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>y. tcb_fault tcb = Some y)) thread\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma send_fault_ipc_corres_conj_helper:
  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_. E \<rbrace>; \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_ s. A s \<and> B s \<and> C s \<and> D s \<rbrace>   \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_ s. A s \<and> B s \<and> C s \<and> D s \<and> E s \<rbrace>" apply (subst conj_assoc[symmetric]) apply (subst conj_assoc[symmetric]) apply (subst conj_assoc[symmetric]) apply (rule hoare_conjI[rotated]) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. A s \<and> B s \<and> C s \<and> D s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. A s \<and> B s \<and> C s \<and> D s \<and> E s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. A s \<and> B s \<and> C s \<and> D s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. (A s \<and> B s) \<and> C s \<and> D s \<and> E s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. A s \<and> B s \<and> C s \<and> D s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. ((A s \<and> B s) \<and> C s) \<and> D s \<and> E s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. A s \<and> B s \<and> C s \<and> D s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. (((A s \<and> B s) \<and> C s) \<and> D s) \<and> E s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. A s \<and> B s \<and> C s \<and> D s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. E\<rbrace>
 2. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. A s \<and> B s \<and> C s \<and> D s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. ((A s \<and> B s) \<and> C s) \<and> D s\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma set_object_valid_etcbs_2:
  "\<lbrace>\<lambda>s. valid_etcbs_2 a (kheap s) \<and>  kheap s ptr = Some (TCB tcba)\<rbrace> KHeap_A.set_object ptr (TCB tcbb) \<lbrace>\<lambda>rv s. valid_etcbs_2 a (kheap s)\<rbrace>" apply (wpsimp wp: set_object_wp) apply (fastforce simp: valid_etcbs_def st_tcb_at_def obj_at_def is_etcb_at_def st_tcb_at_kh_def obj_at_kh_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_etcbs_2 a (kheap s) \<and> kheap s ptr = Some (TCB tcba)\<rbrace> KHeap_A.set_object ptr (TCB tcbb) \<lbrace>\<lambda>rv s. valid_etcbs_2 a (kheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_etcbs_2 a (kheap s); kheap s ptr = Some (TCB tcba)\<rbrakk> \<Longrightarrow> valid_etcbs_2 a (\<lambda>a. if a = ptr then Some (TCB tcbb) else kheap s a) proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma valid_etcbs_2_lift:
  assumes a: "\<And>P T t. \<lbrace>\<lambda>s. P (typ_at T t s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T t s)\<rbrace>"
    shows "\<lbrace>\<lambda>s. valid_etcbs_2 ekh (kheap s)\<rbrace> f \<lbrace>\<lambda>rv s. valid_etcbs_2 ekh (kheap s)\<rbrace>" apply (simp add: valid_etcbs_def) apply (simp add: tcb_at_st_tcb_at[symmetric] tcb_at_typ) apply (wp hoare_vcg_all_lift a) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_etcbs_2 ekh (kheap s)\<rbrace> f \<lbrace>\<lambda>rv s. valid_etcbs_2 ekh (kheap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ptr. st_tcb_at (\<lambda>_. True) ptr s = is_etcb_at' ptr ekh\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>ptr. st_tcb_at (\<lambda>_. True) ptr s = is_etcb_at' ptr ekh\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ptr. typ_at ATCB ptr s = is_etcb_at' ptr ekh\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>ptr. typ_at ATCB ptr s = is_etcb_at' ptr ekh\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_DR

lemma thread_set_valid_etcbs_2:
  "\<lbrace>\<lambda>s. valid_etcbs_2 a (kheap s)\<rbrace> thread_set ref ts \<lbrace>\<lambda>_ s. valid_etcbs_2 a (kheap s) \<rbrace>" by (wp hoare_drop_imps valid_etcbs_2_lift | simp add: thread_set_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_etcbs_2 a (kheap s)\<rbrace> thread_set ref ts \<lbrace>\<lambda>_ s. valid_etcbs_2 a (kheap s)\<rbrace>
theory Untyped_DR

lemma is_arch_page_cap_def2:
  "is_arch_page_cap cap \<longleftrightarrow>
   (\<exists>dev buf rights sz mapdata.
      cap = cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz mapdata))" by (simp add: is_arch_page_cap_def  split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_arch_page_cap cap = (\<exists>dev buf rights sz mapdata. cap = ArchObjectCap (PageCap dev buf rights sz mapdata))
theory Untyped_DR

lemma valid_page_cap_imp_valid_buf:
  "s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False buf rights sz mapdata) \<Longrightarrow>
   is_aligned buf (pageBitsForSize sz) \<and> typ_at (AArch (AUserData sz)) buf s" by (clarsimp simp add: valid_cap_simps cap_aligned_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> ArchObjectCap (PageCap False buf rights sz mapdata) \<Longrightarrow> is_aligned buf (pageBitsForSize sz) \<and> typ_at (AArch (AUserData sz)) buf s
theory Untyped_DR

lemma unat_ptr_range_end:
  "\<lbrakk> is_aligned (ptr :: 'a :: len word) sz; sz < len_of TYPE('a)\<rbrakk>
       \<Longrightarrow> unat (ptr + 2 ^ sz - 1) = unat ptr + 2 ^ sz - 1" apply (simp only: add_diff_eq[symmetric]) apply (subst unat_plus_simple[THEN iffD1]) apply (simp add: add_diff_eq) apply (subst unat_minus_one) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (ptr + 2 ^ sz - 1) = unat ptr + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> unat (ptr + (2 ^ sz - 1)) = unat ptr + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ sz - 1)
 2. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + unat (2 ^ sz - 1) = unat ptr + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + unat (2 ^ sz - 1) = unat ptr + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ sz \<noteq> 0
 2. \<lbrakk>is_aligned ptr sz; sz < LENGTH('a)\<rbrakk> \<Longrightarrow> unat ptr + (unat (2 ^ sz) - 1) = unat ptr + 2 ^ sz - 1 proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma transform_empty_cnode:
  "transform_cnode_contents o_bits (empty_cnode o_bits) = empty_cap_map o_bits" apply (simp add: transform_cnode_contents_def dom_empty_cnode) apply (rule ext, simp add: option_map_join_def empty_cap_map_def
                             nat_to_bl_def len_bin_to_bl_aux empty_cnode_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cnode_contents o_bits (Retype_A.empty_cnode o_bits) = empty_cap_map o_bits proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. map_option transform_cap (option_map_join (Retype_A.empty_cnode o_bits) (nat_to_bl o_bits n))) = empty_cap_map o_bits proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma transform_unat_map_empty:
  "unat_map (\<lambda>_ :: ('a :: len) word. Some cdl_cap.NullCap)
      = empty_cap_map (len_of TYPE('a))" by (rule ext, simp add: unat_map_def empty_cap_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat_map (\<lambda>_. Some cdl_cap.NullCap) = empty_cap_map LENGTH('a)
theory Untyped_DR

lemma obj_bits_bound4:
  "\<lbrakk>type = Structures_A.Untyped \<longrightarrow> untyped_min_bits \<le> us\<rbrakk> \<Longrightarrow>
    untyped_min_bits \<le> obj_bits_api type us" apply (case_tac type; simp add: obj_bits_api_def word_bits_def slot_bits_def untyped_min_bits_def) apply (rename_tac aobject_type) apply (case_tac aobject_type; simp add:arch_kobj_size_def default_arch_object_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us \<Longrightarrow> untyped_min_bits \<le> obj_bits_api type us proof (prove)
goal (1 subgoal):
 1. \<And>x6. type = ArchObject x6 \<Longrightarrow> 4 \<le> arch_kobj_size (default_arch_object x6 False us) proof (prove)
goal (1 subgoal):
 1. \<And>aobject_type. type = ArchObject aobject_type \<Longrightarrow> 4 \<le> arch_kobj_size (default_arch_object aobject_type False us) proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma length_retype_addrs[simp]:
  "length (retype_addrs ptr type n us) = n" by (simp add:retype_addrs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (retype_addrs ptr type n us) = n
theory Untyped_DR

lemma retype_transform_obj_ref_ut:
 "(p \<in> (retype_transform_obj_ref Structures_A.Untyped sz ptr)) = (p \<in> {ptr .. ptr + 2^sz - 1})" by (clarsimp simp:retype_transform_obj_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p \<in> retype_transform_obj_ref apiobject_type.Untyped sz ptr) = (p \<in> {ptr..ptr + (2::'a) ^ sz - (1::'a)})
theory Untyped_DR

lemma transform_none_to_untyped:
  "\<lbrakk>valid_idle s'; kheap s' obj_id = None\<rbrakk>
   \<Longrightarrow> cdl_objects (transform s') obj_id = Some Types_D.Untyped" apply (clarsimp simp: transform_def restrict_map_def map_add_def transform_objects_def) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' obj_id = None\<rbrakk> \<Longrightarrow> cdl_objects (transform s') obj_id = Some cdl_object.Untyped proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (idle_thread s') = None; obj_id = idle_thread s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma retype_transform_obj_ref_pick_id:
  "type \<noteq> Structures_A.Untyped
   \<Longrightarrow> map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref type us) xs)
   = map (retype_transform_obj_ref type us) xs" by (simp add:retype_transform_obj_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. type \<noteq> apiobject_type.Untyped \<Longrightarrow> map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref type us) xs) = map (retype_transform_obj_ref type us) xs
theory Untyped_DR

lemma translate_object_type_not_untyped:
  "type \<noteq> Structures_A.Untyped
   \<Longrightarrow>  Some (the (Types_D.default_object (translate_object_type type) us current_domain))
    = Types_D.default_object (translate_object_type type) us current_domain" by (clarsimp simp:translate_object_type_def Types_D.default_object_def
    split:Structures_A.apiobject_type.splits aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. type \<noteq> apiobject_type.Untyped \<Longrightarrow> Some (the (Types_D.default_object (translate_object_type type) us current_domain)) = Types_D.default_object (translate_object_type type) us current_domain
theory Untyped_DR

lemma retype_transform_obj_ref_not_untyped:
  "\<lbrakk>type \<noteq> Structures_A.Untyped\<rbrakk>
   \<Longrightarrow>
    {x} \<in> retype_transform_obj_ref type us ` set xs = (x \<in> set xs)" apply (rule iffI) apply (clarsimp simp:retype_transform_obj_ref_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. type \<noteq> apiobject_type.Untyped \<Longrightarrow> ({x} \<in> retype_transform_obj_ref type us ` set xs) = (x \<in> set xs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>type \<noteq> apiobject_type.Untyped; {x} \<in> retype_transform_obj_ref type us ` set xs\<rbrakk> \<Longrightarrow> x \<in> set xs
 2. \<lbrakk>type \<noteq> apiobject_type.Untyped; x \<in> set xs\<rbrakk> \<Longrightarrow> {x} \<in> retype_transform_obj_ref type us ` set xs proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma page_objects_default_object:
  "ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj}
     \<Longrightarrow> \<exists>vmsz. (default_object ty dev us = ArchObj (DataPage dev vmsz) \<and> pageBitsForSize vmsz = obj_bits_api ty us)" by (auto simp: default_object_def default_arch_object_def obj_bits_api_def pageBitsForSize_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj} \<Longrightarrow> \<exists>vmsz. Retype_A.default_object ty dev us = ArchObj (DataPage dev vmsz) \<and> pageBitsForSize vmsz = obj_bits_api ty us
theory Untyped_DR

lemma monad_commute_set_cap_assert:
  "monad_commute \<top> (KHeap_D.set_cap ptr cap) (assert F)" apply (simp add: monad_commute_def
     assert_def fail_def bind_def return_def) apply (subgoal_tac "empty_fail (KHeap_D.set_cap ptr cap)") apply (clarsimp simp:empty_fail_def) apply fastforce apply (simp add:KHeap_D.set_cap_def split_def) apply (wp|wpc|clarsimp split:cdl_object.splits)+ apply (simp add:KHeap_D.set_object_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (KHeap_D.set_cap ptr cap) (assert F) proof (prove)
goal (1 subgoal):
 1. \<not> F \<longrightarrow> (\<forall>s. (\<exists>b. ((), b) \<in> fst (KHeap_D.set_cap ptr cap s)) \<or> snd (KHeap_D.set_cap ptr cap s)) proof (prove)
goal (2 subgoals):
 1. empty_fail (KHeap_D.set_cap ptr cap) \<Longrightarrow> \<not> F \<longrightarrow> (\<forall>s. (\<exists>b. ((), b) \<in> fst (KHeap_D.set_cap ptr cap s)) \<or> snd (KHeap_D.set_cap ptr cap s))
 2. empty_fail (KHeap_D.set_cap ptr cap) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. fst (KHeap_D.set_cap ptr cap s) = {} \<longrightarrow> snd (KHeap_D.set_cap ptr cap s); \<not> F; \<not> snd (KHeap_D.set_cap ptr cap s)\<rbrakk> \<Longrightarrow> \<exists>b. ((), b) \<in> fst (KHeap_D.set_cap ptr cap s)
 2. empty_fail (KHeap_D.set_cap ptr cap) proof (prove)
goal (1 subgoal):
 1. empty_fail (KHeap_D.set_cap ptr cap) proof (prove)
goal (1 subgoal):
 1. empty_fail (do obj <- KHeap_D.get_object (fst ptr);
y <- assert (has_slots obj);
(case update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj of Tcb t \<Rightarrow> if snd ptr = tcb_ipcbuffer_slot \<and> object_slots obj (snd ptr) \<noteq> Some cap then do intent' <- select UNIV;
return $ Tcb (dupdate_tcb_intent intent' t)
od else return (update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj) | _ \<Rightarrow> return (update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj)) >>= KHeap_D.set_object (fst ptr)
od) proof (prove)
goal (1 subgoal):
 1. \<And>xb. empty_fail (KHeap_D.set_object (fst ptr) xb) proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma transform_default_cap:
  "transform_cap (default_cap type ptr sz dev)
       = Types_D.default_cap (translate_object_type type)
             (retype_transform_obj_ref type sz ptr) sz dev" by (cases type,
      simp_all add: translate_object_type_def Types_D.default_cap_def
                    free_range_of_untyped_def
                    transform_cap_def arch_default_cap_def transform_mapping_def
                    retype_transform_obj_ref_def vm_read_write_def Nitpick.The_psimp
                    transform_asid_def asid_high_bits_of_def asid_low_bits_def
             split: aobject_type.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cap (Retype_A.default_cap type ptr sz dev) = Types_D.default_cap (translate_object_type type) (retype_transform_obj_ref type sz ptr) sz dev
theory Untyped_DR

lemma set_cap_default_not_none:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>x. slot \<noteq> ptr \<longrightarrow> x \<noteq> cap.NullCap) slot s\<rbrace> CSpaceAcc_A.set_cap (Retype_A.default_cap type a b dev) ptr
  \<lbrace>\<lambda>rv s. cte_wp_at ((\<noteq>) cap.NullCap) slot s\<rbrace>" apply (clarsimp simp:cte_wp_at_caps_of_state valid_def) apply (drule set_cap_caps_of_state_monad) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>x. slot \<noteq> ptr \<longrightarrow> x \<noteq> cap.NullCap) slot\<rbrace> CSpaceAcc_A.set_cap (Retype_A.default_cap type a b dev) ptr \<lbrace>\<lambda>rv. cte_wp_at ((\<noteq>) cap.NullCap) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ba cap. \<lbrakk>((), ba) \<in> fst (CSpaceAcc_A.set_cap (Retype_A.default_cap type a b dev) ptr s); caps_of_state s slot = Some cap; slot \<noteq> ptr \<longrightarrow> cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state ba slot = Some cap \<and> cap.NullCap \<noteq> cap proof (prove)
goal (1 subgoal):
 1. \<And>s ba cap. \<lbrakk>caps_of_state s slot = Some cap; slot \<noteq> ptr \<longrightarrow> cap \<noteq> cap.NullCap; caps_of_state ba = (caps_of_state s)(ptr \<mapsto> Retype_A.default_cap type a b dev)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state ba slot = Some cap \<and> cap.NullCap \<noteq> cap proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma neg_mask_add_2p_helper:
  "\<lbrakk>is_aligned (b::word32) us;us < 32\<rbrakk> \<Longrightarrow> b + 2 ^ us - 1 && ~~ mask us = b" apply (simp add:p_assoc_help) apply (rule is_aligned_add_helper[THEN conjunct2]; simp add:less_1_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned b us; us < 32\<rbrakk> \<Longrightarrow> b + 2 ^ us - 1 && ~~ mask us = b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned b us; us < 32\<rbrakk> \<Longrightarrow> b + (2 ^ us - 1) && ~~ mask us = b proof (prove)
goal:
No subgoals!
theory Untyped_DR

lemma subseteq_set_minus:
  "\<lbrakk>A \<subseteq> B; A\<inter> C = {}\<rbrakk> \<Longrightarrow> A \<subseteq> B - C" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; A \<inter> C = {}\<rbrakk> \<Longrightarrow> A \<subseteq> B - C