theory Finalise_AI

lemma tcb_cap_valid_NullCapD:
  "\<And>cap sl. \<lbrakk> tcb_cap_valid cap sl s; \<not> is_master_reply_cap cap \<rbrakk> \<Longrightarrow>
   tcb_cap_valid cap.NullCap sl s" apply (clarsimp simp: tcb_cap_valid_def valid_ipc_buffer_cap_def
                 elim!: pred_tcb_weakenE split: option.splits) apply (rename_tac get set restr) apply (subgoal_tac "(get, set, restr) \<in> ran tcb_cap_cases") apply (fastforce simp: ran_tcb_cap_cases is_cap_simps
                  split: Structures_A.thread_state.split) apply (simp add: ranI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap sl. \<lbrakk>tcb_cap_valid cap sl s; \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> tcb_cap_valid NullCap sl s proof (prove)
goal (1 subgoal):
 1. \<And>cap a b tcb aa ab ba. \<lbrakk>\<not> is_master_reply_cap cap; tcb_at a s; b = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) a s \<longrightarrow> (case cap of NullCap \<Rightarrow> True | ArchObjectCap acap \<Rightarrow> ARM.valid_ipc_buffer_cap_arch acap (tcb_ipc_buffer tcb) | _ \<Rightarrow> False)); ba a (itcb_state tcb) cap; tcb_cap_cases b = Some (aa, ab, ba)\<rbrakk> \<Longrightarrow> ba a (itcb_state tcb) NullCap proof (prove)
goal (1 subgoal):
 1. \<And>cap a b tcb get set restr. \<lbrakk>\<not> is_master_reply_cap cap; tcb_at a s; b = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) a s \<longrightarrow> (case cap of NullCap \<Rightarrow> True | ArchObjectCap acap \<Rightarrow> ARM.valid_ipc_buffer_cap_arch acap (tcb_ipc_buffer tcb) | _ \<Rightarrow> False)); restr a (itcb_state tcb) cap; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> restr a (itcb_state tcb) NullCap proof (prove)
goal (2 subgoals):
 1. \<And>cap a b tcb get set restr. \<lbrakk>\<not> is_master_reply_cap cap; tcb_at a s; b = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) a s \<longrightarrow> (case cap of NullCap \<Rightarrow> True | ArchObjectCap acap \<Rightarrow> ARM.valid_ipc_buffer_cap_arch acap (tcb_ipc_buffer tcb) | _ \<Rightarrow> False)); restr a (itcb_state tcb) cap; tcb_cap_cases b = Some (get, set, restr); (get, set, restr) \<in> ran tcb_cap_cases\<rbrakk> \<Longrightarrow> restr a (itcb_state tcb) NullCap
 2. \<And>cap a b tcb get set restr. \<lbrakk>\<not> is_master_reply_cap cap; tcb_at a s; b = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) a s \<longrightarrow> (case cap of NullCap \<Rightarrow> True | ArchObjectCap acap \<Rightarrow> ARM.valid_ipc_buffer_cap_arch acap (tcb_ipc_buffer tcb) | _ \<Rightarrow> False)); restr a (itcb_state tcb) cap; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> (get, set, restr) \<in> ran tcb_cap_cases proof (prove)
goal (1 subgoal):
 1. \<And>cap a b tcb get set restr. \<lbrakk>\<not> is_master_reply_cap cap; tcb_at a s; b = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) a s \<longrightarrow> (case cap of NullCap \<Rightarrow> True | ArchObjectCap acap \<Rightarrow> ARM.valid_ipc_buffer_cap_arch acap (tcb_ipc_buffer tcb) | _ \<Rightarrow> False)); restr a (itcb_state tcb) cap; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> (get, set, restr) \<in> ran tcb_cap_cases proof (prove)
goal:
No subgoals!