theory Invariants_AI

lemma valid_obj_pspaceI:
  "\<lbrakk> valid_obj ptr obj s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_obj ptr obj s'" unfolding valid_obj_def apply (cases obj) apply (auto simp add: valid_ntfn_def valid_cs_def valid_tcb_def valid_ep_def
                            valid_tcb_state_def pred_tcb_at_def valid_bound_ntfn_def
                            valid_bound_tcb_def wellformed_arch_pspace
                 intro: obj_at_pspaceI valid_cap_pspaceI valid_arch_tcb_pspaceI
                 split: ntfn.splits endpoint.splits
                        thread_state.splits option.split
          | auto split: kernel_object.split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_obj ptr obj s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> valid_obj ptr obj s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case obj 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; kheap s = kheap s'\<rbrakk> \<Longrightarrow> case obj 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. \<And>x11 x12. \<lbrakk>case obj 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; kheap s = kheap s'; obj = CNode x11 x12\<rbrakk> \<Longrightarrow> case obj 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>x2. \<lbrakk>case obj 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; kheap s = kheap s'; obj = TCB x2\<rbrakk> \<Longrightarrow> case obj 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>x3. \<lbrakk>case obj 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; kheap s = kheap s'; obj = Endpoint x3\<rbrakk> \<Longrightarrow> case obj 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>x4. \<lbrakk>case obj 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; kheap s = kheap s'; obj = Notification x4\<rbrakk> \<Longrightarrow> case obj 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>x5. \<lbrakk>case obj 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; kheap s = kheap s'; obj = ArchObj x5\<rbrakk> \<Longrightarrow> case obj 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!