theory Invocation_DP

lemma handle_pending_interrupts_no_ntf_cap:
  "\<lbrace>P and no_pending\<rbrace>
     handle_pending_interrupts
  \<lbrace>\<lambda>r. P\<rbrace>" apply (simp add: handle_pending_interrupts_def) apply (rule hoare_pre) apply (wp send_signal_no_pending
           | wpc
           | simp add: option_select_def handle_interrupt_def split del: if_split)+ apply (wp hoare_drop_imps hoare_vcg_all_lift) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and no_pending\<rbrace> handle_pending_interrupts \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and no_pending\<rbrace> do active <- get_active_irq;
case active of None \<Rightarrow> return () | Some irq \<Rightarrow> handle_interrupt irq
od \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do active <- get_active_irq;
case active of None \<Rightarrow> return () | Some irq \<Rightarrow> handle_interrupt irq
od \<lbrace>\<lambda>r. P\<rbrace>
 2. \<And>s. (P and no_pending) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_active_irq \<lbrace>\<lambda>active s. (active = None \<longrightarrow> P s) \<and> (\<forall>x. active = Some x \<longrightarrow> (maxIRQ < x \<longrightarrow> P s) \<and> (\<not> maxIRQ < x \<longrightarrow> (opt_cap (get_irq_slot x s) s = None \<longrightarrow> P s) \<and> (\<forall>xa. opt_cap (get_irq_slot x s) s = Some xa \<longrightarrow> (xa = NullCap \<longrightarrow> P s) \<and> ((\<exists>x xb xc. xa = UntypedCap x xb xc) \<longrightarrow> P s) \<and> ((\<exists>x xb xc. xa = EndpointCap x xb xc) \<longrightarrow> P s) \<and> (\<forall>x xb xc. xa = NotificationCap x xb xc \<longrightarrow> (AllowWrite \<in> xc \<longrightarrow> P s \<and> no_pending s) \<and> (AllowWrite \<notin> xc \<longrightarrow> P s)) \<and> ((\<exists>x xb. xa = ReplyCap x xb) \<longrightarrow> P s) \<and> ((\<exists>x. xa = MasterReplyCap x) \<longrightarrow> P s) \<and> ((\<exists>x xb xc xd. xa = CNodeCap x xb xc xd) \<longrightarrow> P s) \<and> ((\<exists>x. xa = TcbCap x) \<longrightarrow> P s) \<and> (xa = DomainCap \<longrightarrow> P s) \<and> ((\<exists>x xb xc xd xe xf. xa = PendingSyncSendCap x xb xc xd xe xf) \<longrightarrow> P s) \<and> ((\<exists>x xb xc. xa = PendingSyncRecvCap x xb xc) \<longrightarrow> P s) \<and> ((\<exists>x. xa = PendingNtfnRecvCap x) \<longrightarrow> P s) \<and> (xa = RestartCap \<longrightarrow> P s) \<and> (xa = RunningCap \<longrightarrow> P s) \<and> (xa = IrqControlCap \<longrightarrow> P s) \<and> ((\<exists>x. xa = IrqHandlerCap x) \<longrightarrow> P s) \<and> ((\<exists>x xb xc xd xe xf. xa = FrameCap x xb xc xd xe xf) \<longrightarrow> P s) \<and> ((\<exists>x xb xc. xa = PageTableCap x xb xc) \<longrightarrow> P s) \<and> ((\<exists>x xb xc. xa = PageDirectoryCap x xb xc) \<longrightarrow> P s) \<and> (xa = AsidControlCap \<longrightarrow> P s) \<and> ((\<exists>x xb. xa = AsidPoolCap x xb) \<longrightarrow> P s) \<and> ((\<exists>x xb. xa = IOPortsCap x xb) \<longrightarrow> P s) \<and> (xa = IOSpaceMasterCap \<longrightarrow> P s) \<and> ((\<exists>x. xa = IOSpaceCap x) \<longrightarrow> P s) \<and> ((\<exists>x. xa = IOPageTableCap x) \<longrightarrow> P s) \<and> ((\<exists>x. xa = ZombieCap x) \<longrightarrow> P s) \<and> ((\<exists>x. xa = BoundNotificationCap x) \<longrightarrow> P s))))\<rbrace>
 2. \<And>s. (P and no_pending) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and no_pending) s \<Longrightarrow> P s \<and> (\<forall>x. P s \<and> P s \<and> (\<forall>x. P s \<and> P s \<and> P s \<and> (\<forall>x xa xb. (P s \<and> no_pending s) \<and> P s) \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s \<and> P s)) proof (prove)
goal:
No subgoals!