kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_R

lemma ct_running_not_idle'[simp]:
  "\<lbrakk>invs' s; ct_running' s\<rbrakk> \<Longrightarrow> ksCurThread s \<noteq> ksIdleThread s" apply (rule ct_not_idle') apply (fastforce simp: invs'_def valid_state'_def ct_in_state'_def
                   elim: pred_tcb'_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; ct_running' s\<rbrakk> \<Longrightarrow> ksCurThread s \<noteq> ksIdleThread s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' s; ct_running' s\<rbrakk> \<Longrightarrow> valid_idle' s
 2. \<lbrakk>invs' s; ct_running' s\<rbrakk> \<Longrightarrow> ct_in_state' (\<lambda>tcb. tcb \<noteq> Structures_H.thread_state.IdleThreadState) s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma ct_active_not_idle'[simp]:
  "\<lbrakk>invs' s; ct_active' s\<rbrakk> \<Longrightarrow> ksCurThread s \<noteq> ksIdleThread s" apply (rule ct_not_idle') apply (fastforce simp: invs'_def valid_state'_def ct_in_state'_def
                   elim: pred_tcb'_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; ct_active' s\<rbrakk> \<Longrightarrow> ksCurThread s \<noteq> ksIdleThread s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' s; ct_active' s\<rbrakk> \<Longrightarrow> valid_idle' s
 2. \<lbrakk>invs' s; ct_active' s\<rbrakk> \<Longrightarrow> ct_in_state' (\<lambda>tcb. tcb \<noteq> Structures_H.thread_state.IdleThreadState) s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma inv_irq_IRQInactive:
  "\<lbrace>\<top>\<rbrace> performIRQControl irqcontrol_invocation
  -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" apply (simp add: performIRQControl_def) apply (rule hoare_pre) apply (wpc|wp|simp add: ARM_H.performIRQControl_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> global.performIRQControl irqcontrol_invocation -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> case irqcontrol_invocation of irqcontrol_invocation.ArchIRQControl invok \<Rightarrow> Arch.performIRQControl invok | Invocations_H.irqcontrol_invocation.IssueIRQHandler irq handlerSlot controlSlot \<Rightarrow> withoutPreemption $ do setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) controlSlot handlerSlot
od -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case irqcontrol_invocation of irqcontrol_invocation.ArchIRQControl invok \<Rightarrow> Arch.performIRQControl invok | Invocations_H.irqcontrol_invocation.IssueIRQHandler irq handlerSlot controlSlot \<Rightarrow> withoutPreemption $ do setIRQState irqstate.IRQSignal irq;
cteInsert (capability.IRQHandlerCap irq) controlSlot handlerSlot
od -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma inv_arch_IRQInactive:
  "\<lbrace>\<top>\<rbrace> Arch.performInvocation invocation
  -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" apply (simp add: ARM_H.performInvocation_def performARMMMUInvocation_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> Arch.performInvocation invocation -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> liftE (case invocation of invocation.InvokePageTable oper \<Rightarrow> do performPageTableInvocation oper;
return []
od | invocation.InvokePageDirectory oper \<Rightarrow> do performPageDirectoryInvocation oper;
return []
od | invocation.InvokePage x \<Rightarrow> performPageInvocation x | invocation.InvokeASIDControl oper \<Rightarrow> do performASIDControlInvocation oper;
return []
od | invocation.InvokeASIDPool oper \<Rightarrow> do performASIDPoolInvocation oper;
return []
od) -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_H

lemma vm_rights_of_vmrights_map_id[simp]:
  "rs \<in> valid_vm_rights \<Longrightarrow> vm_rights_of (vmrights_map rs)= rs" by (auto simp: vm_rights_of_def vmrights_map_def valid_vm_rights_def
                 vm_read_write_def vm_read_only_def vm_kernel_only_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rs \<in> valid_vm_rights \<Longrightarrow> vm_rights_of (vmrights_map rs) = rs
theory ADT_H

lemma thread_state_relation_imp_ThStateMap:
  "thread_state_relation ts ts' \<Longrightarrow> ThStateMap ts' = ts" by (cases ts) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_state_relation ts ts' \<Longrightarrow> ThStateMap ts' = ts
theory ADT_H

lemma LookupFailureMap_lookup_failure_map:
  "(\<forall>n g. lf = ExceptionTypes_A.GuardMismatch n g \<longrightarrow> length g \<le> 32)
   \<Longrightarrow> LookupFailureMap (lookup_failure_map lf) = lf" by (clarsimp simp add: LookupFailureMap_def lookup_failure_map_def
                         uint_of_bl_is_bl_to_bin
               simp del: bin_to_bl_def
               split: ExceptionTypes_A.lookup_failure.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>n g. lf = ExceptionTypes_A.lookup_failure.GuardMismatch n g \<longrightarrow> length g \<le> 32 \<Longrightarrow> LookupFailureMap (lookup_failure_map lf) = lf
theory ADT_H

lemma ArchFaultMap_arch_fault_map: "ArchFaultMap (arch_fault_map f) = f" by (cases f, simp add: ArchFaultMap_def arch_fault_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ArchFaultMap (arch_fault_map f) = f
theory ADT_H

lemma arch_tcb_relation_imp_ArchTcnMap:
  "\<lbrakk> arch_tcb_relation atcb atcb'\<rbrakk> \<Longrightarrow> ArchTcbMap atcb' = atcb" by (clarsimp simp: arch_tcb_relation_def ArchTcbMap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_tcb_relation atcb atcb' \<Longrightarrow> ArchTcbMap atcb' = atcb
theory ADT_H

lemma unaligned_helper:
  "\<lbrakk>is_aligned x n; y\<noteq>0; y < 2 ^ n\<rbrakk> \<Longrightarrow> \<not> is_aligned (x + y) n" apply (simp (no_asm_simp) add: is_aligned_mask) apply (simp add: mask_add_aligned) apply (cut_tac mask_eq_iff_w2p[of n y], simp_all add: word_size) apply (rule ccontr) apply (simp add: not_less power_overflow word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n\<rbrakk> \<Longrightarrow> \<not> is_aligned (x + y) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n\<rbrakk> \<Longrightarrow> x + y && mask n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n\<rbrakk> \<Longrightarrow> y && mask n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n\<rbrakk> \<Longrightarrow> n < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ADT_H

lemma pspace_aligned_distinct_None':
  assumes pspace_aligned: "pspace_aligned s"
  assumes pspace_distinct: "pspace_distinct s"
  shows
  "\<lbrakk>kheap s x = Some ko; y \<in> {0<..<2^(obj_bits ko)}\<rbrakk> \<Longrightarrow> kheap s (x+y) = None" apply (rule pspace_aligned_distinct_None) apply (rule pspace_aligned[simplified pspace_aligned_def]) apply (rule pspace_distinct[simplified pspace_distinct_def]) apply assumption+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> kheap s (x + y) = None proof (prove)
goal (4 subgoals):
 1. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x)))
 2. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> \<forall>x y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}
 3. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> kheap s x = Some ?ko
 4. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> y \<in> {0<..<2 ^ obj_bits ?ko} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> \<forall>x y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> {y..y + (2 ^ obj_bits ko' - 1)} = {}
 2. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> kheap s x = Some ?ko
 3. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> y \<in> {0<..<2 ^ obj_bits ?ko} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> kheap s x = Some ?ko
 2. \<lbrakk>kheap s x = Some ko; y \<in> {0<..<2 ^ obj_bits ko}\<rbrakk> \<Longrightarrow> y \<in> {0<..<2 ^ obj_bits ?ko} proof (prove)
goal:
No subgoals!
theory ADT_H

lemma tcb_cap_cases_length:
  "tcb_cap_cases b = Some x \<Longrightarrow> length b = 3" by (simp add: tcb_cap_cases_def tcb_cnode_index_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_cases b = Some x \<Longrightarrow> length b = 3
theory ADT_H

lemma of_bl_mult_and_not_mask_eq:
  "\<lbrakk>is_aligned (a :: word32) n; length b + m \<le> n\<rbrakk>
   \<Longrightarrow> a + of_bl b * (2^m) && ~~ mask n = a" apply (simp add: shiftl_t2n[simplified mult.commute, symmetric]) apply (simp add: mask_out_add_aligned[where q="of_bl b << m", symmetric]) apply (case_tac "n<32") prefer 2 apply (simp add: not_less power_overflow mask_def) apply (simp add: mask_eq_x_eq_0[symmetric]) apply (rule less_mask_eq) apply (rule shiftl_less_t2n, simp_all) apply (cut_tac 'a=32 and xs=b in of_bl_length, simp) apply (drule nat_move_sub_le) apply (drule two_power_increasing[where 'a=32], simp) apply (drule (2) less_le_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> a + of_bl b * 2 ^ m && ~~ mask n = a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> a + (of_bl b << m) && ~~ mask n = a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n\<rbrakk> \<Longrightarrow> (of_bl b << m) && ~~ mask n = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n; n < 32\<rbrakk> \<Longrightarrow> (of_bl b << m) && ~~ mask n = 0
 2. \<lbrakk>is_aligned a n; length b + m \<le> n; \<not> n < 32\<rbrakk> \<Longrightarrow> (of_bl b << m) && ~~ mask n = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n; \<not> n < 32\<rbrakk> \<Longrightarrow> (of_bl b << m) && ~~ mask n = 0
 2. \<lbrakk>is_aligned a n; length b + m \<le> n; n < 32\<rbrakk> \<Longrightarrow> (of_bl b << m) && ~~ mask n = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n; n < 32\<rbrakk> \<Longrightarrow> (of_bl b << m) && ~~ mask n = 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n; n < 32\<rbrakk> \<Longrightarrow> (of_bl b << m) && mask n = of_bl b << m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n; n < 32\<rbrakk> \<Longrightarrow> of_bl b << m < 2 ^ n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n; n < 32\<rbrakk> \<Longrightarrow> of_bl b < 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; length b + m \<le> n; n < 32; of_bl b < 2 ^ length b\<rbrakk> \<Longrightarrow> of_bl b < 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; n < 32; of_bl b < 2 ^ length b; length b \<le> n - m\<rbrakk> \<Longrightarrow> of_bl b < 2 ^ (n - m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a n; n < 32; of_bl b < 2 ^ length b; 2 ^ length b \<le> 2 ^ (n - m)\<rbrakk> \<Longrightarrow> of_bl b < 2 ^ (n - m) proof (prove)
goal:
No subgoals!
theory ADT_H

lemma TCB_implies_KOTCB:
  "\<lbrakk>pspace_relation (kheap s) (ksPSpace s'); kheap s a = Some (TCB tcb)\<rbrakk>
   \<Longrightarrow> \<exists>tcb'. ksPSpace s' a = Some (KOTCB tcb') \<and> tcb_relation tcb tcb'" apply (clarsimp simp add: pspace_relation_def pspace_dom_def
                            dom_def UNION_eq Collect_eq) apply (erule_tac x=a in allE)+ apply (clarsimp simp add: other_obj_relation_def
                  split: Structures_H.kernel_object.splits) apply (drule iffD1) apply (fastforce simp add: dom_def image_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); kheap s a = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' a = Some (KOTCB tcb') \<and> tcb_relation tcb tcb' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s a = Some (TCB tcb); \<forall>y. (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> y \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>ya. ksPSpace s' y = Some ya); \<forall>x. (\<exists>y. kheap s x = Some y) \<longrightarrow> (\<forall>xa\<in>obj_relation_cuts (the (kheap s x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap s x)) (the (ksPSpace s' y)))\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' a = Some (KOTCB tcb') \<and> tcb_relation tcb tcb' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s a = Some (TCB tcb); (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> a \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>y. ksPSpace s' a = Some y); (\<exists>y. kheap s a = Some y) \<longrightarrow> (\<forall>x\<in>obj_relation_cuts (the (kheap s a)) a. case x of (y, P) \<Rightarrow> P (the (kheap s a)) (the (ksPSpace s' y)))\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' a = Some (KOTCB tcb') \<and> tcb_relation tcb tcb' proof (prove)
goal (1 subgoal):
 1. \<And>x6. \<lbrakk>kheap s a = Some (TCB tcb); (\<exists>x. (\<exists>y. kheap s x = Some y) \<and> a \<in> fst ` obj_relation_cuts (the (kheap s x)) x) = (\<exists>y. ksPSpace s' a = Some y); the (ksPSpace s' a) = KOTCB x6; tcb_relation tcb x6\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' a = Some (KOTCB tcb') \<and> tcb_relation tcb tcb' proof (prove)
goal (2 subgoals):
 1. \<And>x6. \<lbrakk>kheap s a = Some (TCB tcb); the (ksPSpace s' a) = KOTCB x6; tcb_relation tcb x6\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>y. kheap s x = Some y) \<and> a \<in> fst ` obj_relation_cuts (the (kheap s x)) x
 2. \<And>x6. \<lbrakk>kheap s a = Some (TCB tcb); the (ksPSpace s' a) = KOTCB x6; tcb_relation tcb x6; \<exists>y. ksPSpace s' a = Some y\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' a = Some (KOTCB tcb') \<and> tcb_relation tcb tcb' proof (prove)
goal (1 subgoal):
 1. \<And>x6. \<lbrakk>kheap s a = Some (TCB tcb); the (ksPSpace s' a) = KOTCB x6; tcb_relation tcb x6; \<exists>y. ksPSpace s' a = Some y\<rbrakk> \<Longrightarrow> \<exists>tcb'. ksPSpace s' a = Some (KOTCB tcb') \<and> tcb_relation tcb tcb' proof (prove)
goal:
No subgoals!
theory ADT_H

lemma cte_at_CNodeI:
  "\<lbrakk>kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs\<rbrakk>
   \<Longrightarrow> cte_at (a,b) s" apply (subgoal_tac "\<exists>y. cs b = Some y") apply clarsimp apply (rule_tac cte=y in cte_wp_at_cteI[of s _ "length b" cs],
        simp_all) apply (simp add: well_formed_cnode_n_def dom_def Collect_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs; \<exists>y. cs b = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s
 2. \<lbrakk>kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs\<rbrakk> \<Longrightarrow> \<exists>y. cs b = Some y proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs; cs b = Some y\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s
 2. \<lbrakk>kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs\<rbrakk> \<Longrightarrow> \<exists>y. cs b = Some y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s a = Some (CNode (length b) cs); well_formed_cnode_n (length b) cs\<rbrakk> \<Longrightarrow> \<exists>y. cs b = Some y proof (prove)
goal:
No subgoals!
theory ADT_H

lemma valid_mdb_mdb_cte_at:
  "valid_mdb s
   \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c)
      (cdt s)" by (simp add: valid_mdb_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) (cdt s)
theory ADT_H

lemma ctes_of_cte_wp_atD:
  "ctes_of s p = Some cte \<Longrightarrow> cte_wp_at' ((=) cte) p s" by (simp add: KHeap_R.cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s p = Some cte \<Longrightarrow> cte_wp_at' ((=) cte) p s
theory ADT_H

lemma valid_list_2 : "valid_list_2 t m" apply (insert assms') apply (simp add: t_def m_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list_2 t m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; pspace_distinct s; pspace_aligned' s'; pspace_distinct' s'; valid_objs s; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> valid_list_2 t m proof (prove)
goal:
No subgoals!
theory ADT_H

lemma has_next_slot_is_descendant :
    notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
    "next_slot slot t m = Some slot2 \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m)" apply (insert valid_list_2) apply (simp add: next_slot_def next_child_def split: if_split_asm) apply (case_tac "t slot",simp+) apply (simp add: valid_list_2_def) apply (rule disjI1) apply force apply (rule disjI2) apply (erule has_next_not_child_is_descendant) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_slot slot t m = Some slot2 \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_slot slot t m = Some slot2; valid_list_2 t m\<rbrakk> \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; t slot \<noteq> []; (case t slot of [] \<Rightarrow> None | x # xs \<Rightarrow> Some x) = Some slot2\<rbrakk> \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m)
 2. \<lbrakk>valid_list_2 t m; t slot = []; next_not_child slot t m = Some slot2\<rbrakk> \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>valid_list_2 t m; a = slot2; t slot = slot2 # list\<rbrakk> \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m)
 2. \<lbrakk>valid_list_2 t m; t slot = []; next_not_child slot t m = Some slot2\<rbrakk> \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); a = slot2; t slot = slot2 # list\<rbrakk> \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m)
 2. \<lbrakk>valid_list_2 t m; t slot = []; next_not_child slot t m = Some slot2\<rbrakk> \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m) proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>(\<forall>p. set (t p) = {c. m c = Some p}) \<and> (\<forall>p. distinct (t p)); a = slot2; t slot = slot2 # list\<rbrakk> \<Longrightarrow> m slot2 = Some slot
 2. \<lbrakk>valid_list_2 t m; t slot = []; next_not_child slot t m = Some slot2\<rbrakk> \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; t slot = []; next_not_child slot t m = Some slot2\<rbrakk> \<Longrightarrow> m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; t slot = []; next_not_child slot t m = Some slot2\<rbrakk> \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal:
No subgoals!
theory ADT_H

lemma descendant_has_parent:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
    shows
  "slot \<in> descendants_of p m \<Longrightarrow> \<exists>q. m slot = Some q" apply (simp add: descendants_of_def) apply (drule tranclD2) apply (simp add: cdt_parent_of_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot \<in> descendants_of p m \<Longrightarrow> \<exists>q. m slot = Some q proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> slot \<Longrightarrow> \<exists>q. m slot = Some q proof (prove)
goal (1 subgoal):
 1. \<exists>z. m \<Turnstile> p \<rightarrow>* z \<and> m \<Turnstile> z \<leadsto> slot \<Longrightarrow> \<exists>q. m slot = Some q proof (prove)
goal (1 subgoal):
 1. \<exists>z. m \<Turnstile> p \<rightarrow>* z \<and> m slot = Some z \<Longrightarrow> \<exists>q. m slot = Some q proof (prove)
goal:
No subgoals!
theory ADT_H

lemma cte_at_has_cap: "cte_at slot s \<Longrightarrow> \<exists>c. cte_wp_at ((=) c) slot s" apply (drule cte_at_get_cap_wp) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) slot s \<Longrightarrow> \<exists>c. cte_wp_at ((=) c) slot s proof (prove)
goal (1 subgoal):
 1. \<exists>c. (c, s) \<in> fst (get_cap slot s) \<and> cte_wp_at ((=) c) slot s \<Longrightarrow> \<exists>c. cte_wp_at ((=) c) slot s proof (prove)
goal:
No subgoals!
theory ADT_H

lemma next_sib_reachable: "next_sib slot t m = Some slot2 \<Longrightarrow> m slot = Some p \<Longrightarrow>
                             m' \<turnstile> (cte_map slot) \<leadsto>\<^sup>* (cte_map slot2)" apply (rule next_sib_2_reachable) apply (insert assms') apply (simp add: t_def m_def) apply (subst next_sib_def2,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot t m = Some slot2; m slot = Some p\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot t m = Some slot2; m slot = Some p\<rbrakk> \<Longrightarrow> next_sib_2 slot ?p s = Some slot2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot t m = Some slot2; m slot = Some p; pspace_aligned s; pspace_distinct s; pspace_aligned' s'; pspace_distinct' s'; valid_objs s; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> next_sib_2 slot ?p s = Some slot2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_sib slot (cdt_list s) (cdt s) = Some slot2; cdt s slot = Some p; pspace_aligned s; pspace_distinct s; pspace_aligned' s'; pspace_distinct' s'; valid_objs s; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> next_sib_2 slot ?p s = Some slot2 proof (prove)
goal:
No subgoals!