theory Retype_AI

lemma valid_obj_default_object:
  assumes tyunt: "ty \<noteq> Untyped"
  and      tyct: "ty = CapTableObject \<Longrightarrow> us < word_bits - cte_level_bits \<and> 0 < us"
  and      arch: "valid_arch_tcb default_arch_tcb s"
  shows "valid_obj ptr (default_object ty dev us) s" unfolding valid_obj_def default_object_def apply (cases ty) apply (simp add: tyunt) apply (simp add: valid_tcb_def default_tcb_def valid_tcb_state_def
                       tcb_cap_cases_def valid_ipc_buffer_cap_def
                       word_bits_def arch) apply (simp add: valid_ep_def default_ep_def) apply (simp add: valid_ntfn_def default_notification_def default_ntfn_def valid_bound_tcb_def) apply (frule tyct) apply (clarsimp simp: valid_cs_def empty_cnode_def well_formed_cnode_n_def) apply safe apply (erule ranE) apply (simp split: if_split_asm) apply (simp add: valid_cs_size_def well_formed_cnode_n_def) apply safe apply (simp split: if_split_asm) apply (clarsimp split: if_split_asm) apply (clarsimp simp add: wellformed_arch_default) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj ptr (default_object ty dev us) s proof (prove)
goal (1 subgoal):
 1. case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (6 subgoals):
 1. ty = Untyped \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 2. ty = TCBObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 3. ty = EndpointObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 4. ty = NotificationObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 5. ty = CapTableObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 6. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (5 subgoals):
 1. ty = TCBObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 2. ty = EndpointObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 3. ty = NotificationObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 4. ty = CapTableObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 5. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (4 subgoals):
 1. ty = EndpointObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 2. ty = NotificationObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 3. ty = CapTableObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 4. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (3 subgoals):
 1. ty = NotificationObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 2. ty = CapTableObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 3. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (2 subgoals):
 1. ty = CapTableObject \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 2. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty = CapTableObject; us < word_bits - cte_level_bits \<and> 0 < us\<rbrakk> \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s
 2. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty = CapTableObject; us < word_bits - cte_level_bits; 0 < us\<rbrakk> \<Longrightarrow> (\<forall>cap\<in>ran (\<lambda>x. if length x = us then Some NullCap else None). s \<turnstile> cap) \<and> valid_cs_size us (\<lambda>x. if length x = us then Some NullCap else None)
 2. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ty of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (3 subgoals):
 1. \<And>cap. \<lbrakk>ty = CapTableObject; us < word_bits - cte_level_bits; 0 < us; cap \<in> ran (\<lambda>x. if length x = us then Some NullCap else None)\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 2. \<lbrakk>ty = CapTableObject; us < word_bits - cte_level_bits; 0 < us\<rbrakk> \<Longrightarrow> valid_cs_size us (\<lambda>x. if length x = us then Some NullCap else None)
 3. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ArchObject x6 of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (3 subgoals):
 1. \<And>cap x. \<lbrakk>ty = CapTableObject; us < word_bits - cte_level_bits; 0 < us; (if length x = us then Some NullCap else None) = Some cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap
 2. \<lbrakk>ty = CapTableObject; us < word_bits - cte_level_bits; 0 < us\<rbrakk> \<Longrightarrow> valid_cs_size us (\<lambda>x. if length x = us then Some NullCap else None)
 3. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ArchObject x6 of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty = CapTableObject; us < word_bits - cte_level_bits; 0 < us\<rbrakk> \<Longrightarrow> valid_cs_size us (\<lambda>x. if length x = us then Some NullCap else None)
 2. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ArchObject x6 of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ty = CapTableObject; us < word_bits - cte_level_bits; 0 < us\<rbrakk> \<Longrightarrow> dom (\<lambda>x. if length x = us then Some NullCap else None) = {x. length x = us}
 2. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ArchObject x6 of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>ty = CapTableObject; us < word_bits - cte_level_bits; 0 < us; (if length x = us then Some NullCap else None) = Some y\<rbrakk> \<Longrightarrow> length x = us
 2. \<And>x. \<lbrakk>ty = CapTableObject; length x < word_bits - cte_level_bits; us = length x; x \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>y. (if length x = length x then Some NullCap else None) = Some y
 3. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ArchObject x6 of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>ty = CapTableObject; length x < word_bits - cte_level_bits; us = length x; x \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>y. (if length x = length x then Some NullCap else None) = Some y
 2. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ArchObject x6 of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>x6. ty = ArchObject x6 \<Longrightarrow> case case ArchObject x6 of TCBObject \<Rightarrow> TCB default_tcb | EndpointObject \<Rightarrow> Endpoint default_ep | NotificationObject \<Rightarrow> Notification default_notification | CapTableObject \<Rightarrow> CNode us (empty_cnode us) | ArchObject aobj \<Rightarrow> ArchObj (default_arch_object aobj dev us) of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb ptr t s | Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s proof (prove)
goal:
No subgoals!