theory FinalCaps

lemma perform_invocation_silc_inv:
  "\<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv
                    and einvs and simple_sched_action
                    and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace>
   perform_invocation block call iv
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (cases iv) by (wp invoke_untyped_silc_inv send_ipc_silc_inv
         invoke_tcb_silc_inv invoke_cnode_silc_inv
         invoke_irq_control_silc_inv
         invoke_irq_handler_silc_inv
         arch_perform_invocation_silc_inv
      | simp add: authorised_invocation_def invs_valid_objs
                  invs_mdb invs_sym_refs
                  split_def invoke_domain_def
      | fastforce dest:silc_inv_not_subject)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x1. iv = InvokeUntyped x1 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x21 x22 x23 x24. iv = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x31 x32. iv = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>x41 x42 x43. iv = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>x5. iv = InvokeTCB x5 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>x61 x62. iv = InvokeDomain x61 x62 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. \<And>x7. iv = InvokeCNode x7 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. \<And>x8. iv = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 9. \<And>x9. iv = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 10. \<And>x10. iv = InvokeArchObject x10 \<Longrightarrow> \<lbrace>silc_inv aag st and valid_invocation iv and authorised_invocation aag iv and einvs and simple_sched_action and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> perform_invocation block call iv \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>