kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchBCorres2_AI

lemma  handle_arch_fault_reply_bcorres[wp,BCorres2_AI_assms]:
  "bcorres ( handle_arch_fault_reply a b c d) (handle_arch_fault_reply a b c d)" by (cases a; simp add: handle_arch_fault_reply_def; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (handle_arch_fault_reply a b c d) (handle_arch_fault_reply a b c d)
theory ArchBCorres2_AI

lemma perform_invocation_bcorres[wp]: "bcorres (perform_invocation a b c) (perform_invocation a b c)" apply (cases c) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (perform_invocation a b c) (perform_invocation a b c) proof (prove)
goal (10 subgoals):
 1. \<And>x1. c = InvokeUntyped x1 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c)
 2. \<And>x21 x22 x23 x24. c = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c)
 3. \<And>x31 x32. c = InvokeNotification x31 x32 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c)
 4. \<And>x41 x42 x43. c = InvokeReply x41 x42 x43 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c)
 5. \<And>x5. c = InvokeTCB x5 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c)
 6. \<And>x61 x62. c = InvokeDomain x61 x62 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c)
 7. \<And>x7. c = InvokeCNode x7 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c)
 8. \<And>x8. c = InvokeIRQControl x8 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c)
 9. \<And>x9. c = InvokeIRQHandler x9 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c)
 10. \<And>x10. c = InvokeArchObject x10 \<Longrightarrow> bcorres (perform_invocation a b c) (perform_invocation a b c) proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma decode_tcb_configure_bcorres[wp]: "bcorres (decode_tcb_configure b (cap.ThreadCap c) d e)
     (decode_tcb_configure b (cap.ThreadCap c) d e)" apply (simp add: decode_tcb_configure_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (decode_tcb_configure b (ThreadCap c) d e) (decode_tcb_configure b (ThreadCap c) d e) proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma decode_tcb_invocation_bcorres[wp]:"bcorres (decode_tcb_invocation a b (cap.ThreadCap c) d e) (decode_tcb_invocation a b (cap.ThreadCap c) d e)" apply (simp add: decode_tcb_invocation_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (decode_tcb_invocation a b (ThreadCap c) d e) (decode_tcb_invocation a b (ThreadCap c) d e) proof (prove)
goal (1 subgoal):
 1. bcorres (case gen_invocation_type a of TCBReadRegisters \<Rightarrow> decode_read_registers b (ThreadCap c) | TCBWriteRegisters \<Rightarrow> decode_write_registers b (ThreadCap c) | TCBCopyRegisters \<Rightarrow> decode_copy_registers b (ThreadCap c) $ map fst e | TCBConfigure \<Rightarrow> decode_tcb_configure b (ThreadCap c) d e | TCBSetPriority \<Rightarrow> decode_set_priority b (ThreadCap c) d e | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority b (ThreadCap c) d e | TCBSetSchedParams \<Rightarrow> decode_set_sched_params b (ThreadCap c) d e | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer b (ThreadCap c) d e | TCBSetSpace \<Rightarrow> decode_set_space b (ThreadCap c) d e | TCBSuspend \<Rightarrow> returnOk $ Suspend $ obj_ref_of (ThreadCap c) | TCBResume \<Rightarrow> returnOk $ Resume $ obj_ref_of (ThreadCap c) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap c) e | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap c) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base b (ThreadCap c) | _ \<Rightarrow> throwError IllegalOperation) (case gen_invocation_type a of TCBReadRegisters \<Rightarrow> decode_read_registers b (ThreadCap c) | TCBWriteRegisters \<Rightarrow> decode_write_registers b (ThreadCap c) | TCBCopyRegisters \<Rightarrow> decode_copy_registers b (ThreadCap c) $ map fst e | TCBConfigure \<Rightarrow> decode_tcb_configure b (ThreadCap c) d e | TCBSetPriority \<Rightarrow> decode_set_priority b (ThreadCap c) d e | TCBSetMCPriority \<Rightarrow> decode_set_mcpriority b (ThreadCap c) d e | TCBSetSchedParams \<Rightarrow> decode_set_sched_params b (ThreadCap c) d e | TCBSetIPCBuffer \<Rightarrow> decode_set_ipc_buffer b (ThreadCap c) d e | TCBSetSpace \<Rightarrow> decode_set_space b (ThreadCap c) d e | TCBSuspend \<Rightarrow> returnOk $ Suspend $ obj_ref_of (ThreadCap c) | TCBResume \<Rightarrow> returnOk $ Resume $ obj_ref_of (ThreadCap c) | TCBBindNotification \<Rightarrow> decode_bind_notification (ThreadCap c) e | TCBUnbindNotification \<Rightarrow> decode_unbind_notification (ThreadCap c) | TCBSetTLSBase \<Rightarrow> decode_set_tls_base b (ThreadCap c) | _ \<Rightarrow> throwError IllegalOperation) proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma create_mapping_entries_bcorres[wp]: "bcorres (create_mapping_entries a b c d e f) (create_mapping_entries a b c d e f)" apply (cases c) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (create_mapping_entries a b c d e f) (create_mapping_entries a b c d e f) proof (prove)
goal (4 subgoals):
 1. c = ARMSmallPage \<Longrightarrow> bcorres (create_mapping_entries a b c d e f) (create_mapping_entries a b c d e f)
 2. c = ARMLargePage \<Longrightarrow> bcorres (create_mapping_entries a b c d e f) (create_mapping_entries a b c d e f)
 3. c = ARMSection \<Longrightarrow> bcorres (create_mapping_entries a b c d e f) (create_mapping_entries a b c d e f)
 4. c = ARMSuperSection \<Longrightarrow> bcorres (create_mapping_entries a b c d e f) (create_mapping_entries a b c d e f) proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma ensure_safe_mapping_bcorres[wp]: "bcorres (ensure_safe_mapping a) (ensure_safe_mapping a)" apply (induct rule: ensure_safe_mapping.induct) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (ensure_safe_mapping a) (ensure_safe_mapping a) proof (prove)
goal (7 subgoals):
 1. \<And>uu_. bcorres (ensure_safe_mapping (Inl (InvalidPTE, uu_))) (ensure_safe_mapping (Inl (InvalidPTE, uu_)))
 2. \<And>uv_ uw_ ux_ pt_slots. bcorres (ensure_safe_mapping (Inl (SmallPagePTE uv_ uw_ ux_, pt_slots))) (ensure_safe_mapping (Inl (SmallPagePTE uv_ uw_ ux_, pt_slots)))
 3. \<And>uy_ uz_ va_ pt_slots. bcorres (ensure_safe_mapping (Inl (LargePagePTE uy_ uz_ va_, pt_slots))) (ensure_safe_mapping (Inl (LargePagePTE uy_ uz_ va_, pt_slots)))
 4. \<And>vb_. bcorres (ensure_safe_mapping (Inr (InvalidPDE, vb_))) (ensure_safe_mapping (Inr (InvalidPDE, vb_)))
 5. \<And>vc_ vd_ ve_ vf_. bcorres (ensure_safe_mapping (Inr (PageTablePDE vc_ vd_ ve_, vf_))) (ensure_safe_mapping (Inr (PageTablePDE vc_ vd_ ve_, vf_)))
 6. \<And>vg_ vh_ vi_ vj_ pd_slots. bcorres (ensure_safe_mapping (Inr (SectionPDE vg_ vh_ vi_ vj_, pd_slots))) (ensure_safe_mapping (Inr (SectionPDE vg_ vh_ vi_ vj_, pd_slots)))
 7. \<And>vk_ vl_ vm_ pd_slots. bcorres (ensure_safe_mapping (Inr (SuperSectionPDE vk_ vl_ vm_, pd_slots))) (ensure_safe_mapping (Inr (SuperSectionPDE vk_ vl_ vm_, pd_slots))) proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma handle_vm_fault_bcorres[wp]: "bcorres (handle_vm_fault a b) (handle_vm_fault a b)" apply (cases b) apply (simp | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (handle_vm_fault a b) (handle_vm_fault a b) proof (prove)
goal (2 subgoals):
 1. b = ARMDataAbort \<Longrightarrow> bcorres (handle_vm_fault a b) (handle_vm_fault a b)
 2. b = ARMPrefetchAbort \<Longrightarrow> bcorres (handle_vm_fault a b) (handle_vm_fault a b) proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma handle_reserved_irq_bcorres[wp]: "bcorres (handle_reserved_irq a) (handle_reserved_irq a)" by (simp add: handle_reserved_irq_def; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (handle_reserved_irq a) (handle_reserved_irq a)
theory ArchBCorres2_AI

lemma handle_hypervisor_fault_bcorres[wp]: "bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b)" apply (cases b) apply (simp | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b) proof (prove)
goal (1 subgoal):
 1. b = ARMNoHypFaults \<Longrightarrow> bcorres (handle_hypervisor_fault a b) (handle_hypervisor_fault a b) proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma handle_event_bcorres[wp]: "bcorres (handle_event e) (handle_event e)" apply (cases e) apply (simp add: handle_send_def handle_call_def handle_recv_def handle_reply_def handle_yield_def
                   handle_interrupt_def Let_def arch_mask_irq_signal_def
         | intro impI conjI allI | wp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (handle_event e) (handle_event e) proof (prove)
goal (6 subgoals):
 1. \<And>x1. e = SyscallEvent x1 \<Longrightarrow> bcorres (handle_event e) (handle_event e)
 2. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> bcorres (handle_event e) (handle_event e)
 3. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> bcorres (handle_event e) (handle_event e)
 4. e = Interrupt \<Longrightarrow> bcorres (handle_event e) (handle_event e)
 5. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> bcorres (handle_event e) (handle_event e)
 6. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> bcorres (handle_event e) (handle_event e) proof (prove)
goal:
No subgoals!
theory ArchBCorres2_AI

lemma choose_switch_or_idle:
  "((), s') \<in> fst (choose_thread s) \<Longrightarrow>
       (\<exists>word. ((),s') \<in> fst (guarded_switch_to word s)) \<or>
       ((),s') \<in> fst (switch_to_idle_thread s)" apply (simp add: choose_thread_def) apply (clarsimp simp add: switch_to_idle_thread_def bind_def gets_def
                   arch_switch_to_idle_thread_def in_monad
                   return_def get_def modify_def put_def
                    get_thread_state_def
                   thread_get_def
                   split: if_split_asm) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (choose_thread s) \<Longrightarrow> (\<exists>word. ((), s') \<in> fst (guarded_switch_to word s)) \<or> ((), s') \<in> fst (switch_to_idle_thread s) proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst ((do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od) s) \<Longrightarrow> (\<exists>word. ((), s') \<in> fst (guarded_switch_to word s)) \<or> ((), s') \<in> fst (switch_to_idle_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>prio. \<lbrakk>((), s') \<in> fst (guarded_switch_to (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) s); ready_queues s (cur_domain s) prio \<noteq> []; \<forall>x\<in>fst (set_vm_root (idle_thread s) s). ((), s') \<notin> fst (case x of (y, sa) \<Rightarrow> ({((), sa\<lparr>cur_thread := idle_thread s\<rparr>)}, False))\<rbrakk> \<Longrightarrow> \<exists>word. ((), s') \<in> fst (guarded_switch_to word s) proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma obj_at_detype[simp]:
  "obj_at P p (detype S s) = (p \<notin> S \<and> obj_at P p s)" by (clarsimp simp: obj_at_def detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P p (detype S s) = (p \<notin> S \<and> obj_at P p s)
theory Detype_AI

lemma pspace_detype[simp]:
  "(kheap (detype S s) ptr = Some x)
    = (kheap s ptr = Some x \<and> ptr \<notin> S)" by (simp add: detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (kheap (detype S s) ptr = Some x) = (kheap s ptr = Some x \<and> ptr \<notin> S)
theory Detype_AI

lemma cte_wp_at_detype[simp]:
  "(cte_wp_at P p (detype S s))
    = (cte_wp_at P p s \<and> fst p \<notin> S)" apply (case_tac "fst p \<in> S") apply (simp add: cte_wp_at_cases)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P p (detype S s) = (cte_wp_at P p s \<and> fst p \<notin> S) proof (prove)
goal (2 subgoals):
 1. fst p \<in> S \<Longrightarrow> cte_wp_at P p (detype S s) = (cte_wp_at P p s \<and> fst p \<notin> S)
 2. fst p \<notin> S \<Longrightarrow> cte_wp_at P p (detype S s) = (cte_wp_at P p s \<and> fst p \<notin> S) proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma cdt_detype[simp]:
  "cdt (detype S s) = cdt s" by (simp add: detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt (detype S s) = cdt s
theory Detype_AI

lemma caps_of_state_detype[simp]:
  "caps_of_state (detype S s) =
   (\<lambda>p. if fst p \<in> S then None else caps_of_state s p)" by (fastforce simp add: caps_of_state_cte_wp_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state (detype S s) = (\<lambda>p. if fst p \<in> S then None else caps_of_state s p)
theory Detype_AI

lemma state_refs_of_detype:
  "state_refs_of (detype S s) = (\<lambda>x. if x \<in> S then {} else state_refs_of s x)" by (rule ext, simp add: state_refs_of_def detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_refs_of (detype S s) = (\<lambda>x. if x \<in> S then {} else state_refs_of s x)
theory Detype_AI

lemma ex_cte_cap_to_obj_ref_disj:
  "ex_cte_cap_wp_to P ptr s
      \<Longrightarrow> ((\<exists>ptr'. cte_wp_at (\<lambda>cap. fst ptr \<in> obj_refs cap) ptr' s)
               \<or> (\<exists>ptr' irq. cte_wp_at ((=) (cap.IRQHandlerCap irq)) ptr' s
                               \<and> ptr = (interrupt_irq_node s irq, [])))" apply (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state) apply (frule cte_refs_obj_refs_elem, erule disjE) apply fastforce apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to P ptr s \<Longrightarrow> (\<exists>ptr'. cte_wp_at (\<lambda>cap. fst ptr \<in> obj_refs cap) ptr' s) \<or> (\<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> ptr = (interrupt_irq_node s irq, [])) proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>caps_of_state s (a, b) = Some cap; P cap; ptr \<in> cte_refs cap (interrupt_irq_node s); \<forall>a b irq. caps_of_state s (a, b) = Some (IRQHandlerCap irq) \<longrightarrow> ptr \<noteq> (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> fst ptr \<in> obj_refs cap proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>caps_of_state s (a, b) = Some cap; P cap; ptr \<in> cte_refs cap (interrupt_irq_node s); \<forall>a b irq. caps_of_state s (a, b) = Some (IRQHandlerCap irq) \<longrightarrow> ptr \<noteq> (interrupt_irq_node s irq, []); fst ptr \<in> obj_refs cap\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> fst ptr \<in> obj_refs cap
 2. \<And>a b cap. \<lbrakk>caps_of_state s (a, b) = Some cap; P cap; ptr \<in> cte_refs cap (interrupt_irq_node s); \<forall>a b irq. caps_of_state s (a, b) = Some (IRQHandlerCap irq) \<longrightarrow> ptr \<noteq> (interrupt_irq_node s irq, []); \<exists>irq. cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> fst ptr \<in> obj_refs cap proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>caps_of_state s (a, b) = Some cap; P cap; ptr \<in> cte_refs cap (interrupt_irq_node s); \<forall>a b irq. caps_of_state s (a, b) = Some (IRQHandlerCap irq) \<longrightarrow> ptr \<noteq> (interrupt_irq_node s irq, []); \<exists>irq. cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> fst ptr \<in> obj_refs cap proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma descendants_range_in_lift:
  assumes st: "\<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> f \<lbrace>\<lambda>r s. P (cdt s)\<rbrace>"
  assumes untyped_range: "\<And>P p. \<lbrace>\<lambda>s. Q s \<and> cte_wp_at (\<lambda>c. P (cap_range c)) p s\<rbrace> f \<lbrace>\<lambda>r s. cte_wp_at (\<lambda>c. P (cap_range c)) p s\<rbrace>"
  shows "\<lbrace>Q and descendants_range_in S slot\<rbrace> f \<lbrace>\<lambda>r. descendants_range_in S slot\<rbrace>" apply (clarsimp simp:descendants_range_in_def) apply (rule hoare_pre) apply (wps st) apply (rule hoare_vcg_ball_lift) apply (wp untyped_range) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q and descendants_range_in S slot\<rbrace> f \<lbrace>\<lambda>r. descendants_range_in S slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q and (\<lambda>s. \<forall>p'\<in>descendants_of slot (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s)\<rbrace> f \<lbrace>\<lambda>r s. \<forall>p'\<in>descendants_of slot (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>r s. \<forall>p'\<in>descendants_of slot (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s\<rbrace>
 2. \<And>s. (Q and (\<lambda>s. \<forall>p'\<in>descendants_of slot (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. \<forall>p'\<in>descendants_of slot (cdt prev_s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s'\<rbrace>
 2. \<And>s. (Q and (\<lambda>s. \<forall>p'\<in>descendants_of slot (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s)) s \<Longrightarrow> ?P3 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s p'. p' \<in> descendants_of slot (cdt prev_s) \<Longrightarrow> \<lbrace>?P9 prev_s p'\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p'\<rbrace>
 2. \<And>s. (Q and (\<lambda>s. \<forall>p'\<in>descendants_of slot (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s)) s \<Longrightarrow> \<forall>x\<in>descendants_of slot (cdt s). ?P9 s x s proof (prove)
goal (1 subgoal):
 1. \<And>s. (Q and (\<lambda>s. \<forall>p'\<in>descendants_of slot (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s)) s \<Longrightarrow> \<forall>x\<in>descendants_of slot (cdt s). Q s \<and> cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) x s proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma set_cap_descendants_range_in:
  shows "\<lbrace>cte_wp_at (\<lambda>c. cap_range c = cap_range cap) slot and descendants_range_in S slot\<rbrace>
  set_cap cap slot \<lbrace>\<lambda>r. descendants_range_in S slot\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (rule hoare_pre) apply (wp descendants_range_in_lift
     [where Q = "cte_wp_at (\<lambda>c. cap_range c = cap_range cap) slot"] ) apply (wp set_cap_cte_wp_at) apply (clarsimp simp:cte_wp_at_caps_of_state)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>c. cap_range c = cap_range cap) slot and descendants_range_in S slot\<rbrace> set_cap cap slot \<lbrace>\<lambda>r. descendants_range_in S slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at (\<lambda>c. cap_range c = cap_range cap) slot and descendants_range_in S slot) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap cap slot \<lbrace>\<lambda>r. descendants_range_in S slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>descendants_range_in S slot s; caps_of_state s slot = Some capa; cap_range capa = cap_range cap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap cap slot \<lbrace>\<lambda>r. descendants_range_in S slot\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>descendants_range_in S slot s; caps_of_state s slot = Some capa; cap_range capa = cap_range cap\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s capa\<rbrace> set_cap cap slot \<lbrace>\<lambda>r. descendants_range_in S slot\<rbrace>
 2. \<And>s capa sa. \<lbrakk>descendants_range_in S slot s; caps_of_state s slot = Some capa; cap_range capa = cap_range cap; s = sa\<rbrakk> \<Longrightarrow> ?Q5 s capa sa proof (prove)
goal (2 subgoals):
 1. \<And>s capa P p. \<lbrakk>descendants_range_in S slot s; caps_of_state s slot = Some capa; cap_range capa = cap_range cap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. cap_range c = cap_range cap) slot s \<and> cte_wp_at (\<lambda>c. P (cap_range c)) p s\<rbrace> set_cap cap slot \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. P (cap_range c)) p\<rbrace>
 2. \<And>s capa sa. \<lbrakk>descendants_range_in S slot s; caps_of_state s slot = Some capa; cap_range capa = cap_range cap; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. cap_range c = cap_range cap) slot and descendants_range_in S slot) sa proof (prove)
goal (2 subgoals):
 1. \<And>s capa P p sa. \<lbrakk>descendants_range_in S slot s; caps_of_state s slot = Some capa; cap_range capa = cap_range cap; cte_wp_at (\<lambda>c. cap_range c = cap_range cap) slot sa \<and> cte_wp_at (\<lambda>c. P (cap_range c)) p sa\<rbrakk> \<Longrightarrow> ((\<lambda>s. if p = slot then P (cap_range cap) else cte_wp_at (\<lambda>c. P (cap_range c)) p s) and cte_wp_at (\<lambda>_. True) slot) sa
 2. \<And>s capa sa. \<lbrakk>descendants_range_in S slot s; caps_of_state s slot = Some capa; cap_range capa = cap_range cap; s = sa\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>c. cap_range c = cap_range cap) slot and descendants_range_in S slot) sa proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma empty_descendants_range_in:
  "descendants_of p (cdt s) = {} \<Longrightarrow> descendants_range_in S p s" by (clarsimp simp:descendants_range_in_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of p (cdt s) = {} \<Longrightarrow> descendants_range_in S p s
theory Detype_AI

lemma descendants_rangeD:
  "\<lbrakk> descendants_range cap p s; cdt s \<Turnstile> p \<rightarrow> p' \<rbrakk> \<Longrightarrow>
  \<exists>c. caps_of_state s p' = Some c \<and> cap_range c \<inter> cap_range cap = {}" by (simp add: descendants_range_def descendants_of_def cte_wp_at_caps_of_state
           del: split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range cap p s; cdt s \<Turnstile> p \<rightarrow> p'\<rbrakk> \<Longrightarrow> \<exists>c. caps_of_state s p' = Some c \<and> cap_range c \<inter> cap_range cap = {}