theory KHeap_AI

lemma valid_obj_same_type:
  "\<lbrakk> valid_obj p' obj s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
   \<Longrightarrow> valid_obj p' obj (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)" apply (cases obj; simp) apply (clarsimp simp add: valid_obj_def valid_cs_def) apply (drule (1) bspec) apply (erule (2) valid_cap_same_type) apply (clarsimp simp: valid_obj_def valid_tcb_def valid_bound_ntfn_def valid_arch_tcb_same_type) apply (fastforce elim: valid_cap_same_type typ_at_same_type
                      simp: valid_tcb_state_def ep_at_typ
                            ntfn_at_typ tcb_at_typ
                     split: Structures_A.thread_state.splits option.splits) apply (clarsimp simp add: valid_obj_def valid_ep_def) apply (fastforce elim: typ_at_same_type
                    simp: tcb_at_typ
                    split: Structures_A.endpoint.splits) apply (clarsimp simp add: valid_obj_def valid_ntfn_def valid_bound_tcb_def) apply (auto elim: typ_at_same_type
                   simp: tcb_at_typ
                  split: Structures_A.ntfn.splits option.splits) apply (clarsimp simp add: valid_obj_def) apply (auto intro: arch_valid_obj_same_type) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_obj p' obj s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> valid_obj p' obj (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>valid_obj p' (CNode x11 x12) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = CNode x11 x12\<rbrakk> \<Longrightarrow> valid_obj p' (CNode x11 x12) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 2. \<And>x2. \<lbrakk>valid_obj p' (TCB x2) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = TCB x2\<rbrakk> \<Longrightarrow> valid_obj p' (TCB x2) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 3. \<And>x3. \<lbrakk>valid_obj p' (Endpoint x3) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Endpoint x3\<rbrakk> \<Longrightarrow> valid_obj p' (Endpoint x3) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 4. \<And>x4. \<lbrakk>valid_obj p' (Notification x4) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Notification x4\<rbrakk> \<Longrightarrow> valid_obj p' (Notification x4) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 5. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 cap. \<lbrakk>case k of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb p 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 p = Some ko; a_type k = a_type ko; obj = CNode x11 x12; cap \<in> ran x12; \<forall>cap\<in>ran x12. s \<turnstile> cap; valid_cs_size x11 x12\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr> \<turnstile> cap
 2. \<And>x2. \<lbrakk>valid_obj p' (TCB x2) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = TCB x2\<rbrakk> \<Longrightarrow> valid_obj p' (TCB x2) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 3. \<And>x3. \<lbrakk>valid_obj p' (Endpoint x3) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Endpoint x3\<rbrakk> \<Longrightarrow> valid_obj p' (Endpoint x3) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 4. \<And>x4. \<lbrakk>valid_obj p' (Notification x4) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Notification x4\<rbrakk> \<Longrightarrow> valid_obj p' (Notification x4) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 5. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 cap. \<lbrakk>case k of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb p 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 p = Some ko; a_type k = a_type ko; obj = CNode x11 x12; cap \<in> ran x12; valid_cs_size x11 x12; s \<turnstile> cap\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr> \<turnstile> cap
 2. \<And>x2. \<lbrakk>valid_obj p' (TCB x2) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = TCB x2\<rbrakk> \<Longrightarrow> valid_obj p' (TCB x2) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 3. \<And>x3. \<lbrakk>valid_obj p' (Endpoint x3) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Endpoint x3\<rbrakk> \<Longrightarrow> valid_obj p' (Endpoint x3) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 4. \<And>x4. \<lbrakk>valid_obj p' (Notification x4) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Notification x4\<rbrakk> \<Longrightarrow> valid_obj p' (Notification x4) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 5. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>valid_obj p' (TCB x2) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = TCB x2\<rbrakk> \<Longrightarrow> valid_obj p' (TCB x2) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 2. \<And>x3. \<lbrakk>valid_obj p' (Endpoint x3) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Endpoint x3\<rbrakk> \<Longrightarrow> valid_obj p' (Endpoint x3) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 3. \<And>x4. \<lbrakk>valid_obj p' (Notification x4) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Notification x4\<rbrakk> \<Longrightarrow> valid_obj p' (Notification x4) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 4. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>case k of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb p 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 p = Some ko; a_type k = a_type ko; obj = TCB x2; \<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p' (tcb_state x2) (getF x2)); valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f; length (tcb_fault_handler x2) = word_bits; case tcb_bound_notification x2 of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>ran tcb_cap_cases. case x of (getF, ab) \<Rightarrow> s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr> \<turnstile> getF x2 \<and> (case ab of (setF, restr) \<Rightarrow> restr p' (tcb_state x2) (getF x2))) \<and> valid_tcb_state (tcb_state x2) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) \<and> (case tcb_bound_notification x2 of None \<Rightarrow> True | Some a \<Rightarrow> ntfn_at a (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>))
 2. \<And>x3. \<lbrakk>valid_obj p' (Endpoint x3) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Endpoint x3\<rbrakk> \<Longrightarrow> valid_obj p' (Endpoint x3) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 3. \<And>x4. \<lbrakk>valid_obj p' (Notification x4) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Notification x4\<rbrakk> \<Longrightarrow> valid_obj p' (Notification x4) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 4. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>valid_obj p' (Endpoint x3) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Endpoint x3\<rbrakk> \<Longrightarrow> valid_obj p' (Endpoint x3) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 2. \<And>x4. \<lbrakk>valid_obj p' (Notification x4) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Notification x4\<rbrakk> \<Longrightarrow> valid_obj p' (Notification x4) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 3. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>case x3 of IdleEP \<Rightarrow> True | SendEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at t s) \<and> distinct ts | RecvEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at t s) \<and> distinct ts; case k of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb p 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 p = Some ko; a_type k = a_type ko; obj = Endpoint x3\<rbrakk> \<Longrightarrow> case x3 of IdleEP \<Rightarrow> True | SendEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at t (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)) \<and> distinct ts | RecvEP ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at t (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)) \<and> distinct ts
 2. \<And>x4. \<lbrakk>valid_obj p' (Notification x4) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Notification x4\<rbrakk> \<Longrightarrow> valid_obj p' (Notification x4) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 3. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>valid_obj p' (Notification x4) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = Notification x4\<rbrakk> \<Longrightarrow> valid_obj p' (Notification x4) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
 2. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x4. \<lbrakk>case k of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb p 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 p = Some ko; a_type k = a_type ko; obj = Notification x4; case ntfn_obj x4 of WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at t s) \<and> distinct ts \<and> (case ntfn_bound_tcb x4 of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True; case ntfn_bound_tcb x4 of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at t s\<rbrakk> \<Longrightarrow> (case ntfn_obj x4 of WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at t (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)) \<and> distinct ts \<and> (case ntfn_bound_tcb x4 of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> (case ntfn_bound_tcb x4 of None \<Rightarrow> True | Some t \<Rightarrow> tcb_at t (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>))
 2. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x5. \<lbrakk>valid_obj p' (ArchObj x5) s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> valid_obj p' (ArchObj x5) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x5. \<lbrakk>arch_valid_obj x5 s; case k of CNode sz cs \<Rightarrow> valid_cs sz cs s | TCB t \<Rightarrow> valid_tcb p 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 p = Some ko; a_type k = a_type ko; obj = ArchObj x5\<rbrakk> \<Longrightarrow> arch_valid_obj x5 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) proof (prove)
goal:
No subgoals!