theory StateTranslation_D

lemma transform_intent_isnot_TcbIntent:
      "(\<not> (\<exists> ti. Some (TcbIntent ti) = transform_intent label args))
       = ((label = GenInvocationLabel TCBReadRegisters \<longrightarrow> length args < 2) \<and>
          (label = GenInvocationLabel TCBWriteRegisters \<longrightarrow> length args < 2) \<and>
          (label = GenInvocationLabel TCBCopyRegisters \<longrightarrow> length args < 1) \<and>
          (label = GenInvocationLabel TCBConfigure \<longrightarrow> length args < 4) \<and>
          (label = GenInvocationLabel TCBSetPriority \<longrightarrow> length args < 1) \<and>
          (label = GenInvocationLabel TCBSetMCPriority \<longrightarrow> length args < 1) \<and>
          (label = GenInvocationLabel TCBSetSchedParams \<longrightarrow> length args < 2) \<and>
          (label = GenInvocationLabel TCBSetIPCBuffer \<longrightarrow> length args < 1) \<and>
          (label = GenInvocationLabel TCBSetSpace \<longrightarrow> length args < 3) \<and>
          (label \<noteq> GenInvocationLabel TCBSuspend) \<and>
          (label \<noteq> GenInvocationLabel TCBResume) \<and>
          (label \<noteq> GenInvocationLabel TCBBindNotification) \<and>
          (label \<noteq> GenInvocationLabel TCBUnbindNotification) \<and>
          (label \<noteq> GenInvocationLabel TCBSetTLSBase))" apply(rule iffI) subgoal apply(erule contrapos_np) apply(clarsimp simp: transform_intent_def) apply(case_labels label; simp) apply(fastforce simp: transform_intent_tcb_defs option_map_def
                             split: list.split)+ done apply(unfold transform_intent_def) apply(case_labels label; simp add: option_map_def split: option.split) apply(auto simp: transform_intent_tcb_defs
                      split: list.splits arch_invocation_label.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<nexists>ti. Some (TcbIntent ti) = transform_intent label args) = ((label = GenInvocationLabel TCBReadRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBWriteRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBCopyRegisters \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBConfigure \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel TCBSetPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetMCPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSchedParams \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBSetIPCBuffer \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSpace \<longrightarrow> length args < 3) \<and> label \<noteq> GenInvocationLabel TCBSuspend \<and> label \<noteq> GenInvocationLabel TCBResume \<and> label \<noteq> GenInvocationLabel TCBBindNotification \<and> label \<noteq> GenInvocationLabel TCBUnbindNotification \<and> label \<noteq> GenInvocationLabel TCBSetTLSBase) proof (prove)
goal (2 subgoals):
 1. \<nexists>ti. Some (TcbIntent ti) = transform_intent label args \<Longrightarrow> (label = GenInvocationLabel TCBReadRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBWriteRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBCopyRegisters \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBConfigure \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel TCBSetPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetMCPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSchedParams \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBSetIPCBuffer \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSpace \<longrightarrow> length args < 3) \<and> label \<noteq> GenInvocationLabel TCBSuspend \<and> label \<noteq> GenInvocationLabel TCBResume \<and> label \<noteq> GenInvocationLabel TCBBindNotification \<and> label \<noteq> GenInvocationLabel TCBUnbindNotification \<and> label \<noteq> GenInvocationLabel TCBSetTLSBase
 2. (label = GenInvocationLabel TCBReadRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBWriteRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBCopyRegisters \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBConfigure \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel TCBSetPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetMCPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSchedParams \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBSetIPCBuffer \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSpace \<longrightarrow> length args < 3) \<and> label \<noteq> GenInvocationLabel TCBSuspend \<and> label \<noteq> GenInvocationLabel TCBResume \<and> label \<noteq> GenInvocationLabel TCBBindNotification \<and> label \<noteq> GenInvocationLabel TCBUnbindNotification \<and> label \<noteq> GenInvocationLabel TCBSetTLSBase \<Longrightarrow> \<nexists>ti. Some (TcbIntent ti) = transform_intent label args proof (prove)
goal (1 subgoal):
 1. \<nexists>ti. Some (TcbIntent ti) = transform_intent label args \<Longrightarrow> (label = GenInvocationLabel TCBReadRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBWriteRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBCopyRegisters \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBConfigure \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel TCBSetPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetMCPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSchedParams \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBSetIPCBuffer \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSpace \<longrightarrow> length args < 3) \<and> label \<noteq> GenInvocationLabel TCBSuspend \<and> label \<noteq> GenInvocationLabel TCBResume \<and> label \<noteq> GenInvocationLabel TCBBindNotification \<and> label \<noteq> GenInvocationLabel TCBUnbindNotification \<and> label \<noteq> GenInvocationLabel TCBSetTLSBase proof (prove)
goal (1 subgoal):
 1. \<not> ((label = GenInvocationLabel TCBReadRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBWriteRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBCopyRegisters \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBConfigure \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel TCBSetPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetMCPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSchedParams \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBSetIPCBuffer \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSpace \<longrightarrow> length args < 3) \<and> label \<noteq> GenInvocationLabel TCBSuspend \<and> label \<noteq> GenInvocationLabel TCBResume \<and> label \<noteq> GenInvocationLabel TCBBindNotification \<and> label \<noteq> GenInvocationLabel TCBUnbindNotification \<and> label \<noteq> GenInvocationLabel TCBSetTLSBase) \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = transform_intent label args proof (prove)
goal (1 subgoal):
 1. label = GenInvocationLabel TCBReadRegisters \<and> \<not> length args < 2 \<or> label = GenInvocationLabel TCBWriteRegisters \<and> \<not> length args < 2 \<or> label = GenInvocationLabel TCBCopyRegisters \<and> args \<noteq> [] \<or> label = GenInvocationLabel TCBConfigure \<and> \<not> length args < 4 \<or> label = GenInvocationLabel TCBSetPriority \<and> args \<noteq> [] \<or> label = GenInvocationLabel TCBSetMCPriority \<and> args \<noteq> [] \<or> label = GenInvocationLabel TCBSetSchedParams \<and> \<not> length args < 2 \<or> label = GenInvocationLabel TCBSetIPCBuffer \<and> args \<noteq> [] \<or> label = GenInvocationLabel TCBSetSpace \<and> \<not> length args < 3 \<or> label = GenInvocationLabel TCBSuspend \<or> label = GenInvocationLabel TCBResume \<or> label = GenInvocationLabel TCBBindNotification \<or> label = GenInvocationLabel TCBUnbindNotification \<or> label = GenInvocationLabel TCBSetTLSBase \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = (case label of GenInvocationLabel InvalidInvocation \<Rightarrow> None | GenInvocationLabel UntypedRetype \<Rightarrow> map_option UntypedIntent (transform_intent_untyped_retype args) | GenInvocationLabel TCBReadRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_read_registers args) | GenInvocationLabel TCBWriteRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_write_registers args) | GenInvocationLabel TCBCopyRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_copy_registers args) | GenInvocationLabel TCBConfigure \<Rightarrow> map_option TcbIntent (transform_intent_tcb_configure args) | GenInvocationLabel TCBSetPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_priority args) | GenInvocationLabel TCBSetMCPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_mcpriority args) | GenInvocationLabel TCBSetSchedParams \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_sched_params args) | GenInvocationLabel TCBSetIPCBuffer \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_ipc_buffer args) | GenInvocationLabel TCBSetSpace \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_space args) | GenInvocationLabel TCBSuspend \<Rightarrow> Some (TcbIntent TcbSuspendIntent) | GenInvocationLabel TCBResume \<Rightarrow> Some (TcbIntent TcbResumeIntent) | GenInvocationLabel TCBBindNotification \<Rightarrow> Some (TcbIntent TcbBindNTFNIntent) | GenInvocationLabel TCBUnbindNotification \<Rightarrow> Some (TcbIntent TcbUnbindNTFNIntent) | GenInvocationLabel TCBSetTLSBase \<Rightarrow> Some (TcbIntent TcbSetTLSBaseIntent) | GenInvocationLabel CNodeRevoke \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeRevokeIntent args) | GenInvocationLabel CNodeDelete \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeDeleteIntent args) | GenInvocationLabel CNodeCancelBadgedSends \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeCancelBadgedSendsIntent args) | GenInvocationLabel CNodeCopy \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_copy args) | GenInvocationLabel CNodeMint \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mint args) | GenInvocationLabel CNodeMove \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_move args) | GenInvocationLabel CNodeMutate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mutate args) | GenInvocationLabel CNodeRotate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_rotate args) | GenInvocationLabel CNodeSaveCaller \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeSaveCallerIntent args) | GenInvocationLabel IRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (transform_intent_issue_irq_handler args) | GenInvocationLabel IRQAckIRQ \<Rightarrow> Some (IrqHandlerIntent IrqHandlerAckIntent) | GenInvocationLabel IRQSetIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerSetEndpointIntent) | GenInvocationLabel IRQClearIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerClearIntent) | GenInvocationLabel DomainSetSet \<Rightarrow> map_option DomainIntent (transform_intent_domain args) | ArchInvocationLabel ARMPageTableMap \<Rightarrow> map_option PageTableIntent (transform_intent_page_table_map args) | ArchInvocationLabel ARMPageTableUnmap \<Rightarrow> Some (PageTableIntent PageTableUnmapIntent) | ArchInvocationLabel ARMPageMap \<Rightarrow> map_option PageIntent (transform_intent_page_map args) | ArchInvocationLabel ARMPageUnmap \<Rightarrow> Some (PageIntent PageUnmapIntent) | ArchInvocationLabel ARMPageClean_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageCleanInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageGetAddress \<Rightarrow> Some (PageIntent PageGetAddressIntent) | ArchInvocationLabel ARMASIDControlMakePool \<Rightarrow> map_option AsidControlIntent (transform_cnode_index_and_depth AsidControlMakePoolIntent args) | ArchInvocationLabel ARMASIDPoolAssign \<Rightarrow> Some (AsidPoolIntent AsidPoolAssignIntent) | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (arch_transform_intent_issue_irq_handler args) | ArchInvocationLabel _ \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent)) proof (prove)
goal (9 subgoals):
 1. \<And>x1. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel TCBReadRegisters; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = map_option TcbIntent (transform_intent_tcb_read_registers args)
 2. \<And>x1. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel TCBWriteRegisters; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = map_option TcbIntent (transform_intent_tcb_write_registers args)
 3. \<And>x1. \<lbrakk>args \<noteq> []; label = GenInvocationLabel TCBCopyRegisters; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = map_option TcbIntent (transform_intent_tcb_copy_registers args)
 4. \<And>x1. \<lbrakk>\<not> length args < 4; label = GenInvocationLabel TCBConfigure; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = map_option TcbIntent (transform_intent_tcb_configure args)
 5. \<And>x1. \<lbrakk>args \<noteq> []; label = GenInvocationLabel TCBSetPriority; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = map_option TcbIntent (transform_intent_tcb_set_priority args)
 6. \<And>x1. \<lbrakk>args \<noteq> []; label = GenInvocationLabel TCBSetMCPriority; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = map_option TcbIntent (transform_intent_tcb_set_mcpriority args)
 7. \<And>x1. \<lbrakk>\<not> length args < 2; label = GenInvocationLabel TCBSetSchedParams; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = map_option TcbIntent (transform_intent_tcb_set_sched_params args)
 8. \<And>x1. \<lbrakk>args \<noteq> []; label = GenInvocationLabel TCBSetIPCBuffer; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = map_option TcbIntent (transform_intent_tcb_set_ipc_buffer args)
 9. \<And>x1. \<lbrakk>\<not> length args < 3; label = GenInvocationLabel TCBSetSpace; x1 = TCBSetSpace\<rbrakk> \<Longrightarrow> \<exists>ti. Some (TcbIntent ti) = map_option TcbIntent (transform_intent_tcb_set_space args) proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. (label = GenInvocationLabel TCBReadRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBWriteRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBCopyRegisters \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBConfigure \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel TCBSetPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetMCPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSchedParams \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBSetIPCBuffer \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSpace \<longrightarrow> length args < 3) \<and> label \<noteq> GenInvocationLabel TCBSuspend \<and> label \<noteq> GenInvocationLabel TCBResume \<and> label \<noteq> GenInvocationLabel TCBBindNotification \<and> label \<noteq> GenInvocationLabel TCBUnbindNotification \<and> label \<noteq> GenInvocationLabel TCBSetTLSBase \<Longrightarrow> \<nexists>ti. Some (TcbIntent ti) = transform_intent label args proof (prove)
goal (1 subgoal):
 1. (label = GenInvocationLabel TCBReadRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBWriteRegisters \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBCopyRegisters \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBConfigure \<longrightarrow> length args < 4) \<and> (label = GenInvocationLabel TCBSetPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetMCPriority \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSchedParams \<longrightarrow> length args < 2) \<and> (label = GenInvocationLabel TCBSetIPCBuffer \<longrightarrow> length args < 1) \<and> (label = GenInvocationLabel TCBSetSpace \<longrightarrow> length args < 3) \<and> label \<noteq> GenInvocationLabel TCBSuspend \<and> label \<noteq> GenInvocationLabel TCBResume \<and> label \<noteq> GenInvocationLabel TCBBindNotification \<and> label \<noteq> GenInvocationLabel TCBUnbindNotification \<and> label \<noteq> GenInvocationLabel TCBSetTLSBase \<Longrightarrow> \<nexists>ti. Some (TcbIntent ti) = (case label of GenInvocationLabel InvalidInvocation \<Rightarrow> None | GenInvocationLabel UntypedRetype \<Rightarrow> map_option UntypedIntent (transform_intent_untyped_retype args) | GenInvocationLabel TCBReadRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_read_registers args) | GenInvocationLabel TCBWriteRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_write_registers args) | GenInvocationLabel TCBCopyRegisters \<Rightarrow> map_option TcbIntent (transform_intent_tcb_copy_registers args) | GenInvocationLabel TCBConfigure \<Rightarrow> map_option TcbIntent (transform_intent_tcb_configure args) | GenInvocationLabel TCBSetPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_priority args) | GenInvocationLabel TCBSetMCPriority \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_mcpriority args) | GenInvocationLabel TCBSetSchedParams \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_sched_params args) | GenInvocationLabel TCBSetIPCBuffer \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_ipc_buffer args) | GenInvocationLabel TCBSetSpace \<Rightarrow> map_option TcbIntent (transform_intent_tcb_set_space args) | GenInvocationLabel TCBSuspend \<Rightarrow> Some (TcbIntent TcbSuspendIntent) | GenInvocationLabel TCBResume \<Rightarrow> Some (TcbIntent TcbResumeIntent) | GenInvocationLabel TCBBindNotification \<Rightarrow> Some (TcbIntent TcbBindNTFNIntent) | GenInvocationLabel TCBUnbindNotification \<Rightarrow> Some (TcbIntent TcbUnbindNTFNIntent) | GenInvocationLabel TCBSetTLSBase \<Rightarrow> Some (TcbIntent TcbSetTLSBaseIntent) | GenInvocationLabel CNodeRevoke \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeRevokeIntent args) | GenInvocationLabel CNodeDelete \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeDeleteIntent args) | GenInvocationLabel CNodeCancelBadgedSends \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeCancelBadgedSendsIntent args) | GenInvocationLabel CNodeCopy \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_copy args) | GenInvocationLabel CNodeMint \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mint args) | GenInvocationLabel CNodeMove \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_move args) | GenInvocationLabel CNodeMutate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_mutate args) | GenInvocationLabel CNodeRotate \<Rightarrow> map_option CNodeIntent (transform_intent_cnode_rotate args) | GenInvocationLabel CNodeSaveCaller \<Rightarrow> map_option CNodeIntent (transform_cnode_index_and_depth CNodeSaveCallerIntent args) | GenInvocationLabel IRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (transform_intent_issue_irq_handler args) | GenInvocationLabel IRQAckIRQ \<Rightarrow> Some (IrqHandlerIntent IrqHandlerAckIntent) | GenInvocationLabel IRQSetIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerSetEndpointIntent) | GenInvocationLabel IRQClearIRQHandler \<Rightarrow> Some (IrqHandlerIntent IrqHandlerClearIntent) | GenInvocationLabel DomainSetSet \<Rightarrow> map_option DomainIntent (transform_intent_domain args) | ArchInvocationLabel ARMPageTableMap \<Rightarrow> map_option PageTableIntent (transform_intent_page_table_map args) | ArchInvocationLabel ARMPageTableUnmap \<Rightarrow> Some (PageTableIntent PageTableUnmapIntent) | ArchInvocationLabel ARMPageMap \<Rightarrow> map_option PageIntent (transform_intent_page_map args) | ArchInvocationLabel ARMPageUnmap \<Rightarrow> Some (PageIntent PageUnmapIntent) | ArchInvocationLabel ARMPageClean_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageCleanInvalidate_Data \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow> Some (PageIntent PageFlushCachesIntent) | ArchInvocationLabel ARMPageGetAddress \<Rightarrow> Some (PageIntent PageGetAddressIntent) | ArchInvocationLabel ARMASIDControlMakePool \<Rightarrow> map_option AsidControlIntent (transform_cnode_index_and_depth AsidControlMakePoolIntent args) | ArchInvocationLabel ARMASIDPoolAssign \<Rightarrow> Some (AsidPoolIntent AsidPoolAssignIntent) | ArchInvocationLabel ARMIRQIssueIRQHandler \<Rightarrow> map_option IrqControlIntent (arch_transform_intent_issue_irq_handler args) | ArchInvocationLabel _ \<Rightarrow> Some (PageDirectoryIntent PageDirectoryFlushIntent)) proof (prove)
goal (9 subgoals):
 1. \<And>x1. \<lbrakk>length args < 2; label = GenInvocationLabel TCBReadRegisters; x1 = TCBReadRegisters\<rbrakk> \<Longrightarrow> transform_intent_tcb_read_registers args = None
 2. \<And>x1. \<lbrakk>length args < 2; label = GenInvocationLabel TCBWriteRegisters; x1 = TCBWriteRegisters\<rbrakk> \<Longrightarrow> transform_intent_tcb_write_registers args = None
 3. \<And>x1. \<lbrakk>args = []; label = GenInvocationLabel TCBCopyRegisters; x1 = TCBCopyRegisters\<rbrakk> \<Longrightarrow> transform_intent_tcb_copy_registers [] = None
 4. \<And>x1. \<lbrakk>length args < 4; label = GenInvocationLabel TCBConfigure; x1 = TCBConfigure\<rbrakk> \<Longrightarrow> transform_intent_tcb_configure args = None
 5. \<And>x1. \<lbrakk>args = []; label = GenInvocationLabel TCBSetPriority; x1 = TCBSetPriority\<rbrakk> \<Longrightarrow> transform_intent_tcb_set_priority [] = None
 6. \<And>x1. \<lbrakk>args = []; label = GenInvocationLabel TCBSetMCPriority; x1 = TCBSetMCPriority\<rbrakk> \<Longrightarrow> transform_intent_tcb_set_mcpriority [] = None
 7. \<And>x1. \<lbrakk>length args < 2; label = GenInvocationLabel TCBSetSchedParams; x1 = TCBSetSchedParams\<rbrakk> \<Longrightarrow> transform_intent_tcb_set_sched_params args = None
 8. \<And>x1. \<lbrakk>args = []; label = GenInvocationLabel TCBSetIPCBuffer; x1 = TCBSetIPCBuffer\<rbrakk> \<Longrightarrow> transform_intent_tcb_set_ipc_buffer [] = None
 9. \<And>x1. \<lbrakk>length args < 3; label = GenInvocationLabel TCBSetSpace; x1 = TCBSetSpace\<rbrakk> \<Longrightarrow> transform_intent_tcb_set_space args = None proof (prove)
goal:
No subgoals!