kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DR

lemma transform_tcb_slot_3:
  "transform_cslot_ptr (a,tcb_cnode_index 3) = (a,tcb_caller_slot)" apply (clarsimp simp:transform_cslot_ptr_def) apply (unfold tcb_caller_slot_def) apply (simp add: tcb_cnode_index_def) apply (simp add:bl_to_bin_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cslot_ptr (a, tcb_cnode_index 3) = (a, tcb_caller_slot) proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (tcb_cnode_index 3)) = tcb_caller_slot proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (tcb_cnode_index 3)) = 3 proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin [True, True]) = 3 proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_tcb_slot_4:
  "transform_cslot_ptr (a,tcb_cnode_index 4) = (a,tcb_ipcbuffer_slot)" apply (clarsimp simp:transform_cslot_ptr_def) apply (unfold tcb_ipcbuffer_slot_def) apply (simp add: tcb_cnode_index_def) apply (simp add:bl_to_bin_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cslot_ptr (a, tcb_cnode_index 4) = (a, tcb_ipcbuffer_slot) proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (tcb_cnode_index 4)) = tcb_ipcbuffer_slot proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin (tcb_cnode_index 4)) = 4 proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin [True, False, False]) = 4 proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma descendants_cdl_cdt_lift:
  "(\<And>P. \<lbrace>\<lambda>s. P (cdl_cdt s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cdl_cdt s)\<rbrace>) \<Longrightarrow>
   \<lbrace>\<lambda>s. P (KHeap_D.descendants_of slot s)\<rbrace> f \<lbrace>\<lambda>_ s. P (KHeap_D.descendants_of slot s)\<rbrace>" apply (simp add: KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def
                   KHeap_D.is_cdt_parent_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>\<lambda>s. P (cdl_cdt s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cdl_cdt s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (KHeap_D.descendants_of slot s)\<rbrace> f \<lbrace>\<lambda>_ s. P (KHeap_D.descendants_of slot s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>\<lambda>s. P (cdl_cdt s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cdl_cdt s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P {q. (slot, q) \<in> {(p, c). cdl_cdt s c = Some p}\<^sup>+}\<rbrace> f \<lbrace>\<lambda>_ s. P {q. (slot, q) \<in> {(p, c). cdl_cdt s c = Some p}\<^sup>+}\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma fast_finalise_descendants:
  "\<lbrace>\<lambda>s. P (KHeap_D.descendants_of slot s)\<rbrace>
   PageTableUnmap_D.fast_finalise cap fin
  \<lbrace>\<lambda>_ s. P (KHeap_D.descendants_of slot s) \<rbrace>" apply (cases cap, simp_all) apply (wp descendants_cdl_cdt_lift|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (KHeap_D.descendants_of slot s)\<rbrace> PageTableUnmap_D.fast_finalise cap fin \<lbrace>\<lambda>_ s. P (KHeap_D.descendants_of slot s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. cap = cdl_cap.EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. P (KHeap_D.descendants_of slot s)\<rbrace> when fin (PageTableUnmap_D.cancel_all_ipc x31) \<lbrace>\<lambda>_ s. P (KHeap_D.descendants_of slot s)\<rbrace>
 2. \<And>x41 x42 x43. cap = cdl_cap.NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. P (KHeap_D.descendants_of slot s)\<rbrace> when fin (do y <- PageTableUnmap_D.unbind_maybe_notification x41;
PageTableUnmap_D.cancel_all_ipc x41
od) \<lbrace>\<lambda>_ s. P (KHeap_D.descendants_of slot s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma always_empty_slot_card:
  "\<lbrace>\<lambda>s'. s' = s \<and> slot \<in> KHeap_D.descendants_of x s' \<and>
         finite (KHeap_D.descendants_of x s') \<rbrace>
    always_empty_slot slot
  \<lbrace>\<lambda>_ s'. card (KHeap_D.descendants_of x s') < card (KHeap_D.descendants_of x s)\<rbrace>" apply (clarsimp simp: always_empty_slot_def remove_parent_def) apply (wp set_cap_descendants) apply clarsimp apply (erule psubset_card_mono) apply (erule removed_descendants_subset) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s'. s' = s \<and> slot \<in> KHeap_D.descendants_of x s' \<and> finite (KHeap_D.descendants_of x s')\<rbrace> always_empty_slot slot \<lbrace>\<lambda>_ s'. card (KHeap_D.descendants_of x s') < card (KHeap_D.descendants_of x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s'. s' = s \<and> slot \<in> KHeap_D.descendants_of x s' \<and> finite (KHeap_D.descendants_of x s')\<rbrace> do y <- modify (\<lambda>s. s\<lparr>cdl_cdt := \<lambda>x. if x = slot then None else if cdl_cdt s x = Some slot then cdl_cdt s slot else cdl_cdt s x\<rparr>);
KHeap_D.set_cap slot cdl_cap.NullCap
od \<lbrace>\<lambda>_ s'. card (KHeap_D.descendants_of x s') < card (KHeap_D.descendants_of x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. sa = s \<and> slot \<in> KHeap_D.descendants_of x sa \<and> finite (KHeap_D.descendants_of x sa) \<Longrightarrow> card (KHeap_D.descendants_of x (sa\<lparr>cdl_cdt := \<lambda>x. if x = slot then None else if cdl_cdt sa x = Some slot then cdl_cdt sa slot else cdl_cdt sa x\<rparr>)) < card (KHeap_D.descendants_of x s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot \<in> KHeap_D.descendants_of x s; finite (KHeap_D.descendants_of x s)\<rbrakk> \<Longrightarrow> card (KHeap_D.descendants_of x (s\<lparr>cdl_cdt := \<lambda>x. if x = slot then None else if cdl_cdt s x = Some slot then cdl_cdt s slot else cdl_cdt s x\<rparr>)) < card (KHeap_D.descendants_of x s) proof (prove)
goal (1 subgoal):
 1. slot \<in> KHeap_D.descendants_of x s \<Longrightarrow> KHeap_D.descendants_of x (s\<lparr>cdl_cdt := \<lambda>x. if x = slot then None else if cdl_cdt s x = Some slot then cdl_cdt s slot else cdl_cdt s x\<rparr>) \<subset> KHeap_D.descendants_of x s proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma valid_irq_node_cte_at_irq_slot:
 "valid_irq_node s \<Longrightarrow> cte_at (interrupt_irq_node s x,[]) s" apply (clarsimp simp:valid_irq_node_def) apply (drule_tac x = x in spec) apply (clarsimp simp:obj_at_def is_cap_table_def) apply (clarsimp split: Structures_A.kernel_object.splits
                  simp: cte_wp_at_cases well_formed_cnode_n_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_node s \<Longrightarrow> cte_wp_at (\<lambda>_. True) (interrupt_irq_node s x, []) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (interrupt_irq_node s x, []) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj (interrupt_irq_node s); cap_table_at 0 (interrupt_irq_node s x) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (interrupt_irq_node s x, []) s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>inj (interrupt_irq_node s); kheap s (interrupt_irq_node s x) = Some ko; case ko of kernel_object.CNode sz cs \<Rightarrow> 0 = sz \<and> well_formed_cnode_n 0 cs | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (interrupt_irq_node s x, []) s proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>inj (interrupt_irq_node s); kheap s (interrupt_irq_node s x) = Some (kernel_object.CNode 0 x12); dom x12 = {[]}\<rbrakk> \<Longrightarrow> \<exists>cap. x12 [] = Some cap proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_cslot_ptr_inj:
  "\<lbrakk> cte_at p s; cte_at p' s \<rbrakk> \<Longrightarrow>
   (transform_cslot_ptr p = transform_cslot_ptr p') = (p = p')" apply (clarsimp simp: transform_cslot_ptr_def
                        bl_to_bin_ge0 eq_nat_nat_iff split_def
                        valid_irq_node_def) apply (cases p, cases p') apply (safe, simp_all) apply (drule bl_to_bin_inj) apply (erule(1) cte_at_cref_len) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s\<rbrakk> \<Longrightarrow> (transform_cslot_ptr p = transform_cslot_ptr p') = (p = p') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s\<rbrakk> \<Longrightarrow> (fst p = fst p' \<and> bl_to_bin (snd p) = bl_to_bin (snd p')) = (p = p') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> (fst p = fst p' \<and> bl_to_bin (snd p) = bl_to_bin (snd p')) = (p = p') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) (aa, b) s; cte_wp_at (\<lambda>_. True) (aa, ba) s; p' = (aa, ba); p = (aa, b); a = aa; bl_to_bin b = bl_to_bin ba\<rbrakk> \<Longrightarrow> b = ba proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) (aa, b) s; cte_wp_at (\<lambda>_. True) (aa, ba) s; p' = (aa, ba); p = (aa, b); a = aa\<rbrakk> \<Longrightarrow> length b = length ba
 2. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) (aa, b) s; cte_wp_at (\<lambda>_. True) (aa, ba) s; p' = (aa, ba); p = (aa, b); a = aa; b = ba\<rbrakk> \<Longrightarrow> b = ba proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at (\<lambda>_. True) (aa, b) s; cte_wp_at (\<lambda>_. True) (aa, ba) s; p' = (aa, ba); p = (aa, b); a = aa; b = ba\<rbrakk> \<Longrightarrow> b = ba proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma transform_cdt_slot_inj_on_cte_at:
  "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> cte_wp_at P x s \<rbrakk> \<Longrightarrow>
       inj_on (transform_cslot_ptr) S" apply (rule inj_onI) apply (subst(asm) transform_cslot_ptr_inj, simp_all) apply (fastforce simp: cte_wp_at_caps_of_state)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> S \<Longrightarrow> cte_wp_at P x s) \<Longrightarrow> inj_on transform_cslot_ptr S proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> cte_wp_at P x s; x \<in> S; y \<in> S; transform_cslot_ptr x = transform_cslot_ptr y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> cte_wp_at P x s; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x (?s2 x y)
 2. \<And>x y. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> cte_wp_at P x s; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) y (?s2 x y) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma get_cur_thread_corres:
  "dcorres (\<lambda>rv rv'. rv = rv') \<top>
         (\<lambda>s. not_idle_thread (cur_thread s) s)
     (gets_the cdl_current_thread)
     (gets cur_thread)" apply (simp add:gets_the_def gets_def) apply (rule dcorres_absorb_get_l) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:assert_opt_def transform_def transform_current_thread_def) apply (simp add:corres_underlying_def not_idle_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (=) (\<lambda>_. True) (\<lambda>s. not_idle_thread (cur_thread s) s) (gets_the cdl_current_thread) (gets cur_thread) proof (prove)
goal (1 subgoal):
 1. dcorres (=) (\<lambda>_. True) (\<lambda>s. not_idle_thread (cur_thread s) s) (do s <- get;
assert_opt (cdl_current_thread s)
od) (do s <- get;
return (cur_thread s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; not_idle_thread (cur_thread s') s'\<rbrakk> \<Longrightarrow> dcorres (=) ((=) (transform s')) ((=) s') (assert_opt (cdl_current_thread (transform s'))) (do s <- get;
return (cur_thread s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>True; not_idle_thread (cur_thread s') s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres (=) ((=) (transform s'a)) ((=) s'a) (assert_opt (cdl_current_thread (transform s'))) (return (cur_thread s'a)) proof (prove)
goal (1 subgoal):
 1. \<And>s'a. \<lbrakk>not_idle_thread (idle_thread s'a) s'a; cur_thread s'a = idle_thread s'a\<rbrakk> \<Longrightarrow> corres_underlying {ss'. (cur_thread (snd ss') \<noteq> idle_thread (snd ss') \<longrightarrow> \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects (snd ss'), cdl_cdt = transform_cdt (snd ss'), cdl_current_thread = Some (cur_thread (snd ss')), cdl_irq_node = interrupt_irq_node (snd ss'), cdl_asid_table = transform_asid_table (snd ss'), cdl_current_domain = cur_domain (snd ss')\<rparr> = fst ss') \<and> (cur_thread (snd ss') = idle_thread (snd ss') \<longrightarrow> \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects (snd ss'), cdl_cdt = transform_cdt (snd ss'), cdl_current_thread = None, cdl_irq_node = interrupt_irq_node (snd ss'), cdl_asid_table = transform_asid_table (snd ss'), cdl_current_domain = cur_domain (snd ss')\<rparr> = fst ss')} False False (=) ((=) \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s'a, cdl_cdt = transform_cdt s'a, cdl_current_thread = None, cdl_irq_node = interrupt_irq_node s'a, cdl_asid_table = transform_asid_table s'a, cdl_current_domain = cur_domain s'a\<rparr>) ((=) s'a) fail (return (idle_thread s'a)) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma not_in_dom_dest:
  "\<lbrakk>dom f = P; f x = None\<rbrakk> \<Longrightarrow> x\<notin> P" by (clarsimp simp:dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom f = P; f x = None\<rbrakk> \<Longrightarrow> x \<notin> P
theory KHeap_DR

lemma in_dom_dest:
  "\<lbrakk>dom f = P; f x \<noteq> None\<rbrakk> \<Longrightarrow> x\<in> P" by (clarsimp simp:dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom f = P; f x \<noteq> None\<rbrakk> \<Longrightarrow> x \<in> P
theory KHeap_DR

lemma bl_to_bin_tcb_cnode_index_le0:
  "n < 8 \<Longrightarrow> (bl_to_bin (tcb_cnode_index n) \<le> 0) = (n = 0)" by (simp add: tcb_cnode_index_def uint_nat unat_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 8 \<Longrightarrow> (bl_to_bin (tcb_cnode_index n) \<le> 0) = (n = 0)
theory KHeap_DR

lemma nat_bl_to_bin_lt2p: "nat(bl_to_bin b) < 2 ^ length b" apply (rule iffD2[OF nat_less_iff[OF bl_to_bin_ge0]]) apply (simp add:bl_to_bin_lt2p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nat (bl_to_bin b) < 2 ^ length b proof (prove)
goal (1 subgoal):
 1. bl_to_bin b < int (2 ^ length b) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma cap_slot_cnode_property_lift:
  "\<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; b\<in> dom cs\<rbrakk>
  \<Longrightarrow> (opt_cap (transform_cslot_ptr (a, b)) (transform s')) =
     (case (cs b) of None \<Rightarrow> None | Some y \<Rightarrow> Some (transform_cap y))" apply clarsimp apply (subgoal_tac "cte_wp_at ((=) y) (a, b) s'") apply (subst caps_of_state_transform_opt_cap, simp_all) apply (simp add: cte_wp_at_caps_of_state) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) apply (rule cte_wp_at_cteI, fastforce, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; b \<in> dom cs\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') = (case cs b of None \<Rightarrow> None | Some y \<Rightarrow> Some (transform_cap y)) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; cs b = Some y\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some (transform_cap y) proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; cs b = Some y; cte_wp_at ((=) y) (a, b) s'\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (a, b)) (transform s') = Some (transform_cap y)
 2. \<And>y. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; cs b = Some y\<rbrakk> \<Longrightarrow> cte_wp_at ((=) y) (a, b) s' proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; cs b = Some y; cte_wp_at ((=) y) (a, b) s'\<rbrakk> \<Longrightarrow> caps_of_state s' (a, b) = Some y
 2. \<And>y. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; cs b = Some y; cte_wp_at ((=) y) (a, b) s'\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s'
 3. \<And>y. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; cs b = Some y\<rbrakk> \<Longrightarrow> cte_wp_at ((=) y) (a, b) s' proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; cs b = Some y; cte_wp_at ((=) y) (a, b) s'\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s'
 2. \<And>y. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; cs b = Some y\<rbrakk> \<Longrightarrow> cte_wp_at ((=) y) (a, b) s' proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>valid_etcbs s'; kheap s' a = Some (kernel_object.CNode sz cs); valid_idle s'; well_formed_cnode_n sz cs; cs b = Some y\<rbrakk> \<Longrightarrow> cte_wp_at ((=) y) (a, b) s' proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma get_cap_helper:
  "dcorres r P (P') f (get_cap slot >>= g) \<Longrightarrow> dcorres r P (P' and (cte_wp_at ((=) cap) slot)) f  (g cap)" by (clarsimp simp:bind_def corres_underlying_def cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P P' f (CSpaceAcc_A.get_cap slot >>= g) \<Longrightarrow> dcorres r P (P' and cte_wp_at ((=) cap) slot) f (g cap)
theory KHeap_DR

lemma opt_cap_wp_at_def':
  "opt_cap_wp_at P slot s = (case (opt_cap slot s) of Some a \<Rightarrow> P a | _ \<Rightarrow> False) " apply (clarsimp simp:opt_cap_wp_at_def opt_cap_def gets_the_def gets_def get_def return_def assert_opt_def bind_def) apply (auto simp:fail_def return_def split:option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. opt_cap_wp_at P slot s = (case opt_cap slot s of None \<Rightarrow> False | Some a \<Rightarrow> P a) proof (prove)
goal (1 subgoal):
 1. (\<exists>cap. fst ((case (case slot of (obj_id, slot) \<Rightarrow> \<lambda>s. slots_of obj_id s slot) s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(cap, s)} \<and> P cap) = (case (case slot of (obj_id, slot) \<Rightarrow> \<lambda>s. slots_of obj_id s slot) s of None \<Rightarrow> False | Some a \<Rightarrow> P a) proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma nat2p: "nat (2^(x::nat)) = 2^(x::nat)" by (rule nat_int.Rep_inverse',simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nat (2 ^ x) = 2 ^ x
theory KHeap_DR

lemma nat_to_bl_to_bin:
  "nat_to_bl bits n = Some xs \<Longrightarrow> n = nat (bl_to_bin xs)" by (clarsimp simp:nat_to_bl_def bin_bl_bin' bintrunc_mod2p split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nat_to_bl bits n = Some xs \<Longrightarrow> n = nat (bl_to_bin xs)
theory KHeap_DR

lemma eqset_imp': "A = B \<Longrightarrow> \<forall>x. ((x\<in> A) = (x\<in> B))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A = B \<Longrightarrow> \<forall>x. (x \<in> A) = (x \<in> B)
theory KHeap_DR

lemma eq_singleton_set: "\<lbrakk>A = f` B; \<forall>x\<in>B. \<forall>y\<in> B. x\<noteq> y \<longrightarrow> f x\<noteq> f y \<rbrakk>\<Longrightarrow> (\<exists>a. A = {a}) = (\<exists>b. B = {b})" apply (subgoal_tac "card A = card B") apply (auto simp: trans[OF eq_commute card_Suc_eq])[1] apply (metis card_image inj_onI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A = f ` B; \<forall>x\<in>B. \<forall>y\<in>B. x \<noteq> y \<longrightarrow> f x \<noteq> f y\<rbrakk> \<Longrightarrow> (\<exists>a. A = {a}) = (\<exists>b. B = {b}) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A = f ` B; \<forall>x\<in>B. \<forall>y\<in>B. x \<noteq> y \<longrightarrow> f x \<noteq> f y; card A = card B\<rbrakk> \<Longrightarrow> (\<exists>a. A = {a}) = (\<exists>b. B = {b})
 2. \<lbrakk>A = f ` B; \<forall>x\<in>B. \<forall>y\<in>B. x \<noteq> y \<longrightarrow> f x \<noteq> f y\<rbrakk> \<Longrightarrow> card A = card B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A = f ` B; \<forall>x\<in>B. \<forall>y\<in>B. x \<noteq> y \<longrightarrow> f x \<noteq> f y\<rbrakk> \<Longrightarrow> card A = card B proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma opt_cap_wp_at_ex_opt_cap:
  "opt_cap_wp_at P p s = (\<exists>cap'. opt_cap p s = Some cap' \<and> P cap')" by (simp add: opt_cap_wp_at_def' split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. opt_cap_wp_at P p s = (\<exists>cap'. opt_cap p s = Some cap' \<and> P cap')
theory KHeap_DR

lemma dcorres_exec_is_final_cap:
  assumes c: "\<And>final. dcorres r (P final) P' (f final) f'"
  shows "dcorres r (\<lambda>s. P (PageTableUnmap_D.is_final_cap' cap s) s) P' (PageTableUnmap_D.is_final_cap cap >>= f) f'" unfolding PageTableUnmap_D.is_final_cap_def apply (rule corres_underlying_gets_pre_lhs) apply (rule c) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r (\<lambda>s. P (PageTableUnmap_D.is_final_cap' cap s) s) P' (PageTableUnmap_D.is_final_cap cap >>= f) f' proof (prove)
goal (1 subgoal):
 1. dcorres r (\<lambda>s. P (PageTableUnmap_D.is_final_cap' cap s) s) P' (gets (PageTableUnmap_D.is_final_cap' cap) >>= f) f' proof (prove)
goal (1 subgoal):
 1. \<And>x. dcorres r (P x) P' (f x) f' proof (prove)
goal:
No subgoals!
theory KHeap_DR

lemma set_original_dummy_corres:
  "dcorres dc \<top> \<top> (return a) (set_original slot tag)" apply (clarsimp simp:set_original_def gets_def) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:return_def simpler_modify_def corres_underlying_def) apply (clarsimp simp:transform_def transform_current_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (set_original slot tag) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return a) (do s <- get;
modify (is_original_cap_update (\<lambda>_. (is_original_cap s)(slot := tag)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (return a) (modify (is_original_cap_update (\<lambda>_. (is_original_cap s')(slot := tag)))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. transform (s'\<lparr>is_original_cap := (is_original_cap s')(slot := tag)\<rparr>) = transform s' proof (prove)
goal:
No subgoals!