theory Access_AC

lemma cca_to_transferable_or_subject:
  "\<lbrakk> valid_objs s; valid_mdb s; pas_refined aag s; cdt_change_allowed' aag ptr s \<rbrakk>
     \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable (caps_of_state s ptr)" apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases) apply (rule all_children_parent_of_rtrancl[OF pas_refined_all_children]; blast) apply (simp add:rtrancl_eq_or_trancl,elim disjE conjE) apply (simp add:direct_call_def, elim conjE) apply (drule tcb_states_of_state_kheapD, elim exE conjE) apply (frule(2) tcb_caller_slot_empty_on_recieve ,simp) apply (cases ptr,simp) apply (simp add:caps_of_state_tcb) apply (elim tcb_states_of_state_kheapE) apply (drule(2) descendant_of_caller_slot[OF _ _ tcb_atI]) by (force simp add: descendants_of_def simp del:split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt_change_allowed' aag ptr s\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (2 subgoals):
 1. \<And>pptr. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> pptr \<rightarrow>* ptr; pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> pptr \<rightarrow>* ptr; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (1 subgoal):
 1. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt s \<Turnstile> pptr \<rightarrow>* ptr; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (2 subgoals):
 1. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; pptr = ptr\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; pptr \<noteq> ptr; cdt s \<Turnstile> pptr \<rightarrow> ptr\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (2 subgoals):
 1. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; tcb_states_of_state s (fst ptr) = Some tcbst; snd ptr = tcb_cnode_index 3; pptr = ptr; ep_recv_blocked ep tcbst; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; pptr \<noteq> ptr; cdt s \<Turnstile> pptr \<rightarrow> ptr\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (2 subgoals):
 1. \<And>pptr tcbst ep tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; snd ptr = tcb_cnode_index 3; pptr = ptr; ep_recv_blocked ep tcbst; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s (fst ptr) = Some (TCB tcb); tcb_state tcb = tcbst\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; pptr \<noteq> ptr; cdt s \<Turnstile> pptr \<rightarrow> ptr\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (2 subgoals):
 1. \<And>pptr tcbst ep tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; snd ptr = tcb_cnode_index 3; pptr = ptr; ep_recv_blocked ep tcbst; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s (fst ptr) = Some (TCB tcb); tcb_state tcb = tcbst; tcb_caller tcb = NullCap \<and> cdt s (fst ptr, tcb_cnode_index 3) = None \<and> descendants_of (fst ptr, tcb_cnode_index 3) (cdt s) = {}\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; pptr \<noteq> ptr; cdt s \<Turnstile> pptr \<rightarrow> ptr\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (2 subgoals):
 1. \<And>pptr tcbst ep tcb a b. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; b = tcb_cnode_index 3; pptr = (a, tcb_cnode_index 3); ep_recv_blocked ep tcbst; (pasSubject aag, Call, pasObjectAbs aag ep) \<in> pasPolicy aag; kheap s a = Some (TCB tcb); tcb_state tcb = tcbst; tcb_caller tcb = NullCap \<and> cdt s (a, tcb_cnode_index 3) = None \<and> descendants_of (a, tcb_cnode_index 3) (cdt s) = {}; ptr = (a, tcb_cnode_index 3)\<rbrakk> \<Longrightarrow> is_subject aag a \<or> is_transferable_in (a, tcb_cnode_index 3) s
 2. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; pptr \<noteq> ptr; cdt s \<Turnstile> pptr \<rightarrow> ptr\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (1 subgoal):
 1. \<And>pptr tcbst ep. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; pptr \<noteq> ptr; cdt s \<Turnstile> pptr \<rightarrow> ptr\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (1 subgoal):
 1. \<And>pptr tcbst ep tcb. \<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; pptr \<noteq> ptr; cdt s \<Turnstile> pptr \<rightarrow> ptr; kheap s (fst pptr) = Some (TCB tcb); tcb_state tcb = tcbst\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s proof (prove)
goal (1 subgoal):
 1. \<And>pptr tcbst ep tcb. \<lbrakk>valid_objs s; pas_refined aag s; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3; pptr \<noteq> ptr; cdt s \<Turnstile> pptr \<rightarrow> ptr; kheap s (fst pptr) = Some (TCB tcb); tcb_state tcb = tcbst; descendants_of (fst pptr, tcb_cnode_index 3) (cdt s) = {}\<rbrakk> \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable_in ptr s