theory TCB_DP

lemma decode_tcb_invocation_simps:
  "is_tcb_cap cap \<Longrightarrow>
  decode_invocation cap cap_ref caps (TcbIntent intent) = liftME InvokeTcb (decode_tcb_invocation cap cap_ref caps intent)" apply (clarsimp simp: decode_invocation_def) apply (clarsimp simp: decode_invocation_def
     get_tcb_intent_def throw_opt_def cap_type_def
     split:cdl_cap.splits ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb_cap cap \<Longrightarrow> decode_invocation cap cap_ref caps (TcbIntent intent) = liftME InvokeTcb (decode_tcb_invocation cap cap_ref caps intent) proof (prove)
goal (1 subgoal):
 1. is_tcb_cap cap \<Longrightarrow> (case cap of UntypedCap x xa xb \<Rightarrow> doE untyped_intent <- throw_opt undefined $ get_untyped_intent (TcbIntent intent);
liftME InvokeUntyped $ decode_untyped_invocation cap cap_ref caps untyped_intent
odE | EndpointCap o_id badge rights \<Rightarrow> if AllowWrite \<in> rights then returnOk $ InvokeEndpoint (SyncMessage badge (AllowGrant \<in> rights) (AllowGrantReply \<in> rights) o_id) else throw | NotificationCap o_id badge rights \<Rightarrow> if AllowWrite \<in> rights then returnOk $ InvokeNotification (Signal badge o_id) else throw | ReplyCap o_id rights \<Rightarrow> returnOk $ InvokeReply (ReplyMessage o_id cap_ref (AllowGrant \<in> rights)) | CNodeCap x xa xb xc \<Rightarrow> doE cnode_intent <- throw_opt undefined $ get_cnode_intent (TcbIntent intent);
liftME InvokeCNode $ decode_cnode_invocation cap cap_ref caps cnode_intent
odE | TcbCap x \<Rightarrow> doE tcb_intent <- throw_opt undefined $ get_tcb_intent (TcbIntent intent);
liftME InvokeTcb $ decode_tcb_invocation cap cap_ref caps tcb_intent
odE | DomainCap \<Rightarrow> doE domain_intent <- throw_opt undefined $ get_domain_intent (TcbIntent intent);
liftME InvokeDomain $ decode_domain_invocation caps domain_intent
odE | IrqControlCap \<Rightarrow> doE irq_control_intent <- throw_opt undefined $ get_irq_control_intent (TcbIntent intent);
liftME InvokeIrqControl $ decode_irq_control_invocation cap cap_ref caps irq_control_intent
odE | IrqHandlerCap x \<Rightarrow> doE irq_handler_intent <- throw_opt undefined $ get_irq_handler_intent (TcbIntent intent);
liftME InvokeIrqHandler $ decode_irq_handler_invocation cap cap_ref caps irq_handler_intent
odE | FrameCap x xa xb xc xd xe \<Rightarrow> doE page_intent <- throw_opt undefined $ get_page_intent (TcbIntent intent);
liftME InvokePage $ decode_page_invocation cap cap_ref caps page_intent
odE | PageTableCap x xa xb \<Rightarrow> doE page_table_intent <- throw_opt undefined $ get_page_table_intent (TcbIntent intent);
liftME InvokePageTable $ decode_page_table_invocation cap cap_ref caps page_table_intent
odE | PageDirectoryCap x xa xb \<Rightarrow> doE page_directory_intent <- throw_opt undefined $ get_page_directory_intent (TcbIntent intent);
liftME InvokePageDirectory $ decode_page_directory_invocation cap cap_ref caps page_directory_intent
odE | AsidControlCap \<Rightarrow> doE asid_control_intent <- throw_opt undefined $ get_asid_control_intent (TcbIntent intent);
liftME InvokeAsidControl $ decode_asid_control_invocation cap cap_ref caps asid_control_intent
odE | AsidPoolCap x xa \<Rightarrow> doE asid_pool_intent <- throw_opt undefined $ get_asid_pool_intent (TcbIntent intent);
liftME InvokeAsidPool $ decode_asid_pool_invocation cap cap_ref caps asid_pool_intent
odE | _ \<Rightarrow> throw) = liftME InvokeTcb (decode_tcb_invocation cap cap_ref caps intent) proof (prove)
goal:
No subgoals!