kings-crown/FVELER_Isabelle huggingface dataset:
theory InterruptAcc_R

lemma sch_act_simple_irq_state_independent[intro!, simp]:
  "sch_act_simple (s \<lparr> ksMachineState := ksMachineState s \<lparr> irq_state := f (irq_state (ksMachineState s)) \<rparr> \<rparr>) =
   sch_act_simple s" by (simp add: sch_act_simple_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_simple (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := f (irq_state (ksMachineState s))\<rparr>\<rparr>) = sch_act_simple s
theory InterruptAcc_R

lemma preemptionPoint_invs [wp]:
  "\<lbrace>invs'\<rbrace> preemptionPoint \<lbrace>\<lambda>_. invs'\<rbrace>" by (wp preemptionPoint_inv | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> preemptionPoint \<lbrace>\<lambda>_. invs'\<rbrace>
theory Retype_R

lemma placeNewObject_def2:
 "placeNewObject ptr val gb = createObjects' ptr 1 (injectKO val) gb" apply (clarsimp simp:placeNewObject_def placeNewObject'_def
     createObjects'_def shiftL_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. placeNewObject ptr val gb = createObjects' ptr 1 (injectKO val) gb proof (prove)
goal:
No subgoals!
theory Retype_R

lemma objBitsKO_bounded2[simp]:
  "objBitsKO ko < word_bits" by (simp add: objBits_simps' word_bits_def pageBits_def archObjSize_def pdeBits_def pteBits_def
           split: Structures_H.kernel_object.split arch_kernel_object.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. objBitsKO ko < word_bits
theory Retype_R

lemma NullCap_valid' [iff]: "s \<turnstile>' capability.NullCap" unfolding valid_cap'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' capability.NullCap s proof (prove)
goal (1 subgoal):
 1. capAligned capability.NullCap \<and> (case capability.NullCap of capability.ThreadCap r \<Rightarrow> tcb_at' r s | capability.NotificationCap r badge x y \<Rightarrow> ntfn_at' r s | capability.IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | capability.EndpointCap r badge x y z t \<Rightarrow> ep_at' r s | capability.Zombie r b n \<Rightarrow> n \<le> zombieCTEs b \<and> zBits b < word_bits \<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)) | capability.ArchObjectCap (arch_capability.ASIDPoolCap pool asid) \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> True | capability.ArchObjectCap (arch_capability.PageCap d ref rghts sz mapdata) \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | capability.ArchObjectCap (arch_capability.PageTableCap ref mapdata) \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | capability.ArchObjectCap (arch_capability.PageDirectoryCap ref mapdata) \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | capability.ReplyCap r m x \<Rightarrow> tcb_at' r s | capability.UntypedCap d r n f \<Rightarrow> valid_untyped' d r n f s \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> n \<and> n \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ n \<and> is_aligned (word_of_nat f) minUntypedSizeBits | capability.CNodeCap r bits guard guard_sz \<Rightarrow> bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and> guard && mask guard_sz = guard \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask bits)) s) | _ \<Rightarrow> True)
theory Retype_R

lemma valid_obj_makeObject_tcb [simp]:
  "valid_obj' (KOTCB makeObject) s" unfolding valid_obj'_def valid_tcb'_def  valid_tcb_state'_def by (clarsimp simp: makeObject_tcb makeObject_cte tcb_cte_cases_def minBound_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj' (KOTCB makeObject) s proof (prove)
goal (1 subgoal):
 1. case KOTCB makeObject of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s | KONotification notification \<Rightarrow> valid_ntfn' notification s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. valid_cap' (cteCap (getF tcb)) s) \<and> (case tcbState tcb of Structures_H.thread_state.BlockedOnReceive ref a \<Rightarrow> ep_at' ref s | Structures_H.thread_state.BlockedOnNotification ref \<Rightarrow> ntfn_at' ref s | Structures_H.thread_state.BlockedOnSend ref a b d c \<Rightarrow> ep_at' ref s | _ \<Rightarrow> True) \<and> is_aligned (tcbIPCBuffer tcb) msg_align_bits \<and> valid_bound_ntfn' (tcbBoundNotification tcb) s \<and> tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority \<and> tcbMCP tcb \<le> maxPriority | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True
theory Retype_R

lemma valid_obj_makeObject_endpoint [simp]:
  "valid_obj' (KOEndpoint makeObject) s" unfolding valid_obj'_def valid_ep'_def by (clarsimp simp: makeObject_endpoint)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj' (KOEndpoint makeObject) s proof (prove)
goal (1 subgoal):
 1. case KOEndpoint makeObject of KOEndpoint (Structures_H.endpoint.RecvEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts | KOEndpoint Structures_H.endpoint.IdleEP \<Rightarrow> True | KOEndpoint (Structures_H.endpoint.SendEP ts) \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts | KONotification notification \<Rightarrow> valid_ntfn' notification s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True
theory Retype_R

lemma valid_obj_makeObject_notification [simp]:
  "valid_obj' (KONotification makeObject) s" unfolding valid_obj'_def valid_ntfn'_def by (clarsimp simp: makeObject_notification)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj' (KONotification makeObject) s proof (prove)
goal (1 subgoal):
 1. case KONotification makeObject of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s | KONotification notification \<Rightarrow> (case ntfnObj notification of Structures_H.ntfn.WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at' t s) \<and> distinct ts \<and> (case ntfnBoundTCB notification of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> valid_bound_tcb' (ntfnBoundTCB notification) s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True
theory Retype_R

lemma valid_obj_makeObject_user_data [simp]:
  "valid_obj' (KOUserData) s" unfolding valid_obj'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj' KOUserData s proof (prove)
goal (1 subgoal):
 1. case KOUserData of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s | KONotification notification \<Rightarrow> valid_ntfn' notification s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True
theory Retype_R

lemma valid_obj_makeObject_user_data_device [simp]:
  "valid_obj' (KOUserDataDevice) s" unfolding valid_obj'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj' KOUserDataDevice s proof (prove)
goal (1 subgoal):
 1. case KOUserDataDevice of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s | KONotification notification \<Rightarrow> valid_ntfn' notification s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True
theory Retype_R

lemma valid_obj_makeObject_pte[simp]:
  "valid_obj' (KOArch (KOPTE makeObject)) s" unfolding valid_obj'_def by (simp add: makeObject_pte)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj' (KOArch (KOPTE makeObject)) s proof (prove)
goal (1 subgoal):
 1. case KOArch (KOPTE makeObject) of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s | KONotification notification \<Rightarrow> valid_ntfn' notification s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True
theory Retype_R

lemma valid_obj_makeObject_pde[simp]:
  "valid_obj' (KOArch (KOPDE makeObject)) s" unfolding valid_obj'_def by (simp add: makeObject_pde)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj' (KOArch (KOPDE makeObject)) s proof (prove)
goal (1 subgoal):
 1. case KOArch (KOPDE makeObject) of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s | KONotification notification \<Rightarrow> valid_ntfn' notification s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True
theory Retype_R

lemma valid_obj_makeObject_asid_pool[simp]:
  "valid_obj' (KOArch (KOASIDPool makeObject)) s" unfolding valid_obj'_def by (simp add: makeObject_asidpool Let_def ran_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj' (KOArch (KOASIDPool makeObject)) s proof (prove)
goal (1 subgoal):
 1. case KOArch (KOASIDPool makeObject) of KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s | KONotification notification \<Rightarrow> valid_ntfn' notification s | KOKernelData \<Rightarrow> False | KOTCB tcb \<Rightarrow> valid_tcb' tcb s | KOCTE cte \<Rightarrow> valid_cte' cte s | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s | _ \<Rightarrow> True
theory Retype_R

lemma null_filter_parent_of'':
  "\<lbrakk> null_filter' xs = null_filter' ys; xs \<turnstile> x \<leadsto> c; c \<noteq> 0 \<rbrakk>
     \<Longrightarrow> ys \<turnstile> x \<leadsto> c" apply (clarsimp simp add: mdb_next_unfold) apply (drule arg_cong[where f="\<lambda>xs. xs x"]) apply (simp add: null_filter'_def nullPointer_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>null_filter' xs = null_filter' ys; xs \<turnstile> x \<leadsto> c; c \<noteq> 0\<rbrakk> \<Longrightarrow> ys \<turnstile> x \<leadsto> c proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>null_filter' xs = null_filter' ys; mdbNext (cteMDBNode z) \<noteq> 0; xs x = Some z; c = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> \<exists>za. ys x = Some za \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za) proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>mdbNext (cteMDBNode z) \<noteq> 0; xs x = Some z; c = mdbNext (cteMDBNode z); null_filter' xs x = null_filter' ys x\<rbrakk> \<Longrightarrow> \<exists>za. ys x = Some za \<and> mdbNext (cteMDBNode z) = mdbNext (cteMDBNode za) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma null_filter_descendants_of':
  "null_filter' xs = null_filter' ys
    \<Longrightarrow> descendants_of' x xs = descendants_of' x ys" apply (simp add: descendants_of'_def) apply (rule set_eqI, rule iffI) apply simp apply (erule(1) null_filter_descendant) apply simp apply (erule(1) null_filter_descendant[OF sym]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. null_filter' xs = null_filter' ys \<Longrightarrow> descendants_of' x xs = descendants_of' x ys proof (prove)
goal (1 subgoal):
 1. null_filter' xs = null_filter' ys \<Longrightarrow> {c'. xs \<turnstile> x \<rightarrow> c'} = {c'. ys \<turnstile> x \<rightarrow> c'} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>null_filter' xs = null_filter' ys; xa \<in> {c'. xs \<turnstile> x \<rightarrow> c'}\<rbrakk> \<Longrightarrow> xa \<in> {c'. ys \<turnstile> x \<rightarrow> c'}
 2. \<And>xa. \<lbrakk>null_filter' xs = null_filter' ys; xa \<in> {c'. ys \<turnstile> x \<rightarrow> c'}\<rbrakk> \<Longrightarrow> xa \<in> {c'. xs \<turnstile> x \<rightarrow> c'} proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>null_filter' xs = null_filter' ys; xs \<turnstile> x \<rightarrow> xa\<rbrakk> \<Longrightarrow> ys \<turnstile> x \<rightarrow> xa
 2. \<And>xa. \<lbrakk>null_filter' xs = null_filter' ys; xa \<in> {c'. ys \<turnstile> x \<rightarrow> c'}\<rbrakk> \<Longrightarrow> xa \<in> {c'. xs \<turnstile> x \<rightarrow> c'} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>null_filter' xs = null_filter' ys; xa \<in> {c'. ys \<turnstile> x \<rightarrow> c'}\<rbrakk> \<Longrightarrow> xa \<in> {c'. xs \<turnstile> x \<rightarrow> c'} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>null_filter' xs = null_filter' ys; ys \<turnstile> x \<rightarrow> xa\<rbrakk> \<Longrightarrow> xs \<turnstile> x \<rightarrow> xa proof (prove)
goal:
No subgoals!
theory Retype_R

lemma descendants_of_cte_at':
  "\<lbrakk> p \<in> descendants_of x (cdt s); valid_mdb s \<rbrakk>
  \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) p s" apply (simp add: descendants_of_def) apply (drule tranclD2) apply (clarsimp simp: cdt_parent_defs valid_mdb_def mdb_cte_at_def
                  simp del: split_paired_All) apply (fastforce elim: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> descendants_of x (cdt s); valid_mdb s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt s \<Turnstile> x \<rightarrow> p; valid_mdb s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; \<exists>z. cdt s \<Turnstile> x \<rightarrow>* z \<and> cdt s \<Turnstile> z \<leadsto> p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) p s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>p c. cdt s c = Some p \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cte_wp_at ((\<noteq>) cap.NullCap) c s; (x, a, b) \<in> {(p, c). cdt s c = Some p}\<^sup>*; cdt s p = Some (a, b); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) p s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma descendants_of_cte_at2':
  "\<lbrakk> p \<in> descendants_of x (cdt s); valid_mdb s \<rbrakk>
  \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) x s" apply (simp add: descendants_of_def) apply (drule tranclD) apply (clarsimp simp: cdt_parent_defs valid_mdb_def mdb_cte_at_def
                  simp del: split_paired_All) apply (fastforce elim: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> descendants_of x (cdt s); valid_mdb s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) x s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt s \<Turnstile> x \<rightarrow> p; valid_mdb s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) x s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; \<exists>z. cdt s \<Turnstile> x \<leadsto> z \<and> cdt s \<Turnstile> z \<rightarrow>* p\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) x s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>p c. cdt s c = Some p \<longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) p s \<and> cte_wp_at ((\<noteq>) cap.NullCap) c s; cdt s (a, b) = Some x; ((a, b), p) \<in> {(p, c). cdt s c = Some p}\<^sup>*; untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) x s proof (prove)
goal:
No subgoals!
theory Retype_R

lemma foldr_update_obj_at':
  assumes pv: "pspace_aligned' s" "pspace_distinct' s"
     and pv': "pspace_aligned' (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)"
              "pspace_distinct' (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)"
      and al: "\<forall>x \<in> set addrs. is_aligned x (objBitsKO obj)"
   shows
  "obj_at' P p (ksPSpace_update (\<lambda>x xa. if xa \<in> set addrs then Some obj else ksPSpace s xa) s)
         = (if p \<in> set addrs then (\<exists>obj'. projectKO_opt obj = Some obj' \<and> P obj')
                         else obj_at' P p s)" apply (simp only: obj_at'_real_def) apply (rule foldr_update_ko_wp_at' [OF pv pv' al]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) = (if p \<in> set addrs then \<exists>obj'. projectKO_opt obj = Some obj' \<and> P obj' else obj_at' P p s) proof (prove)
goal (1 subgoal):
 1. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p (s\<lparr>ksPSpace := \<lambda>xa. if xa \<in> set addrs then Some obj else ksPSpace s xa\<rparr>) = (if p \<in> set addrs then \<exists>obj'. projectKO_opt obj = Some obj' \<and> P obj' else ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s) proof (prove)
goal:
No subgoals!
theory Retype_R

lemma makeObjectKO_eq:
  assumes x: "makeObjectKO dev tp = Some v"
  shows
  "(v = KOCTE cte) =
       (tp = Inr (APIObjectType ArchTypes_H.CapTableObject) \<and> cte = makeObject)"
  "(v = KOTCB tcb) =
       (tp = Inr (APIObjectType ArchTypes_H.TCBObject) \<and> tcb = makeObject)" using x by (simp add: makeObjectKO_def eq_commute
         split: apiobject_type.split_asm sum.split_asm kernel_object.split_asm
                ARM_H.object_type.split_asm arch_kernel_object.split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (v = KOCTE cte) = (tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> cte = makeObject) &&& (v = KOTCB tcb) = (tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> tcb = makeObject) proof (prove)
using this:
makeObjectKO dev tp = Some v

goal (1 subgoal):
 1. (v = KOCTE cte) = (tp = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject) \<and> cte = makeObject) &&& (v = KOTCB tcb) = (tp = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject) \<and> tcb = makeObject)
theory Retype_R

lemma the_ctes_makeObject:
  "fst (the (tcb_cte_cases n)) makeObject
     = (if tcb_cte_cases n = None
           then fst (the None :: (Structures_H.tcb \<Rightarrow> cte) \<times> ((cte \<Rightarrow> cte) \<Rightarrow> Structures_H.tcb \<Rightarrow> Structures_H.tcb))
                     (makeObject :: tcb)
           else makeObject)" apply (simp add: makeObject_tcb) apply (clarsimp simp: tcb_cte_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (the (tcb_cte_cases n)) makeObject = (if tcb_cte_cases n = None then fst (the None) makeObject else makeObject) proof (prove)
goal (1 subgoal):
 1. (\<exists>a b. tcb_cte_cases n = Some (a, b)) \<longrightarrow> fst (the (tcb_cte_cases n)) (Thread makeObject makeObject makeObject makeObject makeObject minBound Structures_H.thread_state.Inactive minBound minBound False None timeSlice 0 0 None newArchTCB) = makeObject proof (prove)
goal:
No subgoals!
theory Retype_R

lemma ps_clearD:
  "\<lbrakk> ps_clear x n s; ksPSpace s y = Some v; x < y; y \<le> x + 2 ^ n - 1 \<rbrakk> \<Longrightarrow> False" apply (clarsimp simp: ps_clear_def) apply (drule_tac a=y in equals0D) apply (simp add: dom_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps_clear x n s; ksPSpace s y = Some v; x < y; y \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>({x..x + 2 ^ n - 1} - {x}) \<inter> dom (ksPSpace s) = {}; ksPSpace s y = Some v; x < y; y \<le> x + 2 ^ n - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s y = Some v; x < y; y \<le> x + 2 ^ n - 1; y \<notin> ({x..x + 2 ^ n - 1} - {x}) \<inter> dom (ksPSpace s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s y = Some v; x < y; y \<le> x + 2 ^ n - 1; x \<le> y \<longrightarrow> y = x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_R

lemma new_cap_addrs_aligned:
  "\<lbrakk> is_aligned ptr (objBitsKO ko) \<rbrakk>
    \<Longrightarrow> \<forall>x \<in> set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko)" apply (clarsimp simp: new_cap_addrs_def) apply (erule aligned_add_aligned[OF _ is_aligned_shift]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr (objBitsKO ko) \<Longrightarrow> \<forall>x\<in>set (new_cap_addrs n ptr ko). is_aligned x (objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned ptr (objBitsKO ko); x < n\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat x << objBitsKO ko)) (objBitsKO ko) proof (prove)
goal (1 subgoal):
 1. \<And>x. x < n \<Longrightarrow> objBitsKO ko \<le> objBitsKO ko proof (prove)
goal:
No subgoals!
theory Retype_R

lemma APIType_map2_Untyped[simp]:
  "(APIType_map2 tp = Structures_A.Untyped)
        = (tp = Inr (APIObjectType ArchTypes_H.Untyped))" by (simp add: APIType_map2_def
         split: sum.split object_type.split kernel_object.split arch_kernel_object.splits
                apiobject_type.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (APIType_map2 tp = Structures_A.apiobject_type.Untyped) = (tp = Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped))
theory Retype_R

lemma obj_relation_retype_leD:
  "\<lbrakk> obj_relation_retype ko ko' \<rbrakk>
      \<Longrightarrow> objBitsKO ko' \<le> obj_bits ko" by (simp add: obj_relation_retype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_relation_retype ko ko' \<Longrightarrow> objBitsKO ko' \<le> obj_bits ko
theory Retype_R

lemma obj_relation_retype_default_leD:
  "\<lbrakk> obj_relation_retype (default_object (APIType_map2 ty) dev us) ko;
       ty \<noteq> Inr (APIObjectType ArchTypes_H.Untyped) \<rbrakk>
      \<Longrightarrow> objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us" by (simp add: obj_relation_retype_def objBits_def obj_bits_dev_irr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_relation_retype (default_object (APIType_map2 ty) dev us) ko; ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped)\<rbrakk> \<Longrightarrow> objBitsKO ko \<le> obj_bits_api (APIType_map2 ty) us
theory Retype_R

lemma makeObjectKO_Untyped:
  "makeObjectKO dev ty = Some v \<Longrightarrow> ty \<noteq> Inr (APIObjectType ArchTypes_H.Untyped)" by (clarsimp simp: makeObjectKO_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. makeObjectKO dev ty = Some v \<Longrightarrow> ty \<noteq> Inr (APIObjectType ArchTypes_H.apiobject_type.Untyped)