theory ADT_IF_Refine_C

lemma handleEvent_Interrupt_no_fail: "no_fail (invs' and ex_abs einvs) (handleEvent Interrupt)" apply (simp add: handleEvent_def) apply wp apply (rule handleInterrupt_no_fail) apply (simp add: crunch_simps) apply (rule_tac Q="\<lambda>r s. ex_abs (einvs) s \<and> invs' s \<and>
                             (\<forall>irq. r = Some irq
                                    \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)"
                 in hoare_strengthen_post) apply (rule hoare_vcg_conj_lift) apply (rule corres_ex_abs_lift) apply (rule dmo_getActiveIRQ_corres) apply wpsimp apply (wpsimp wp: doMachineOp_getActiveIRQ_IRQ_active) apply clarsimp apply wpsimp apply (clarsimp simp: invs'_def valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (invs' and ex_abs einvs) (handleEvent Interrupt) proof (prove)
goal (1 subgoal):
 1. no_fail (invs' and ex_abs einvs) (liftE (doMachineOp (getActiveIRQ False) >>= case_option (return ()) handleInterrupt)) proof (prove)
goal (4 subgoals):
 1. \<And>rv x. no_fail (?Q3 rv x) (handleInterrupt x)
 2. \<lbrace>?Q2\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. if rv = None then \<lambda>_. True else ?Q3 rv (the rv)\<rbrace>
 3. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 4. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and ?Q2) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q2\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. if rv = None then \<lambda>_. True else ex_abs einvs and invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) (the rv) \<noteq> irqstate.IRQInactive)\<rbrace>
 2. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 3. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and ?Q2) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q2\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv x. (\<exists>y. rv = Some y) \<longrightarrow> ex_abs einvs x \<and> invs' x \<and> intStateIRQTable (ksInterruptState x) (the rv) \<noteq> irqstate.IRQInactive\<rbrace>
 2. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 3. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and ?Q2) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q2\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>r s. ex_abs einvs s \<and> invs' s \<and> (\<forall>irq. r = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)\<rbrace>
 2. \<And>rv s. ex_abs einvs s \<and> invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive) \<Longrightarrow> (\<exists>y. rv = Some y) \<longrightarrow> ex_abs einvs s \<and> invs' s \<and> intStateIRQTable (ksInterruptState s) (the rv) \<noteq> irqstate.IRQInactive
 3. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 4. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and ?Q2) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv. ex_abs einvs\<rbrace>
 2. \<lbrace>?P'7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)\<rbrace>
 3. \<And>rv s. ex_abs einvs s \<and> invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive) \<Longrightarrow> (\<exists>y. rv = Some y) \<longrightarrow> ex_abs einvs s \<and> invs' s \<and> intStateIRQTable (ksInterruptState s) (the rv) \<noteq> irqstate.IRQInactive
 4. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 5. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and (\<lambda>s. ?P7 s \<and> ?P'7 s)) s proof (prove)
goal (6 subgoals):
 1. corres ?r10 ?S10 ?P'10 ?f10 (doMachineOp (getActiveIRQ False))
 2. \<lbrace>?P10\<rbrace> ?f10 \<lbrace>\<lambda>rv. einvs\<rbrace>
 3. \<lbrace>?P'7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)\<rbrace>
 4. \<And>rv s. ex_abs einvs s \<and> invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive) \<Longrightarrow> (\<exists>y. rv = Some y) \<longrightarrow> ex_abs einvs s \<and> invs' s \<and> intStateIRQTable (ksInterruptState s) (the rv) \<noteq> irqstate.IRQInactive
 5. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 6. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and (\<lambda>s. (ex_abs (?P10 and ?S10) and ?P'10) s \<and> ?P'7 s)) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P10\<rbrace> do_machine_op (getActiveIRQ ?in_kernel13) \<lbrace>\<lambda>rv. einvs\<rbrace>
 2. \<lbrace>?P'7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)\<rbrace>
 3. \<And>rv s. ex_abs einvs s \<and> invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive) \<Longrightarrow> (\<exists>y. rv = Some y) \<longrightarrow> ex_abs einvs s \<and> invs' s \<and> intStateIRQTable (ksInterruptState s) (the rv) \<noteq> irqstate.IRQInactive
 4. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 5. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and (\<lambda>s. (ex_abs (?P10 and (\<lambda>_. True)) and (\<lambda>_. True)) s \<and> ?P'7 s)) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'7\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>rv s. invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)\<rbrace>
 2. \<And>rv s. ex_abs einvs s \<and> invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive) \<Longrightarrow> (\<exists>y. rv = Some y) \<longrightarrow> ex_abs einvs s \<and> invs' s \<and> intStateIRQTable (ksInterruptState s) (the rv) \<noteq> irqstate.IRQInactive
 3. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 4. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and (\<lambda>s. (ex_abs (einvs and (\<lambda>_. True)) and (\<lambda>_. True)) s \<and> ?P'7 s)) s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. ex_abs einvs s \<and> invs' s \<and> (\<forall>irq. rv = Some irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive) \<Longrightarrow> (\<exists>y. rv = Some y) \<longrightarrow> ex_abs einvs s \<and> invs' s \<and> intStateIRQTable (ksInterruptState s) (the rv) \<noteq> irqstate.IRQInactive
 2. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 3. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and (\<lambda>s. (ex_abs (einvs and (\<lambda>_. True)) and (\<lambda>_. True)) s \<and> invs' s \<and> valid_irq_states' s)) s proof (prove)
goal (2 subgoals):
 1. no_fail ?P2 (doMachineOp (getActiveIRQ False))
 2. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> (?P2 and (\<lambda>s. (ex_abs (einvs and (\<lambda>_. True)) and (\<lambda>_. True)) s \<and> invs' s \<and> valid_irq_states' s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ex_abs einvs) s \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and (\<lambda>s. (ex_abs (einvs and (\<lambda>_. True)) and (\<lambda>_. True)) s \<and> invs' s \<and> valid_irq_states' s)) s proof (prove)
goal:
No subgoals!