theory CNodeInv_R

lemma in_preempt':
  "(Inr rv, s') \<in> fst (preemptionPoint s) \<Longrightarrow>
   \<exists>f g. s' = ksWorkUnitsCompleted_update f
      (s \<lparr> ksMachineState := ksMachineState s \<lparr> irq_state := g (irq_state (ksMachineState s)) \<rparr>\<rparr>)" apply (simp add: preemptionPoint_def alternative_def in_monad eq_commute
                   getActiveIRQ_def doMachineOp_def split_def
                   select_f_def select_def getWorkUnits_def setWorkUnits_def
                   modifyWorkUnits_def return_def returnOk_def
              split: option.splits if_splits) apply (erule disjE) apply (cases "workUnitsLimit \<le> ksWorkUnitsCompleted s + 1", drule (1) mp,
            rule exI[where x="\<lambda>x. 0"], rule exI[where x=Suc], force,
            rule exI[where x="\<lambda>x. x + 1"], rule exI[where x=id], force)+ apply (rule exI[where x="\<lambda>x. x + 1"], rule exI[where x=id], force) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Inr rv, s') \<in> fst (preemptionPoint s) \<Longrightarrow> \<exists>f g. s' = ksWorkUnitsCompleted_update f (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := g (irq_state (ksMachineState s))\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted s + 1 \<longrightarrow> s' = s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>; irq_masks (ksMachineState s) (irq_oracle (Suc (irq_state (ksMachineState s)))) \<or> irq_oracle (Suc (irq_state (ksMachineState s))) = 0x3FF \<or> irq_oracle (Suc (irq_state (ksMachineState s))) \<in> non_kernel_IRQs; FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted s + 1 \<longrightarrow> s' = s\<lparr>ksWorkUnitsCompleted := 0, ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>\<rparr>\<rbrakk> \<Longrightarrow> \<exists>f g. s' = ksWorkUnitsCompleted_update f (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := g (irq_state (ksMachineState s))\<rparr>\<rparr>)
 2. \<lbrakk>s' = s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>; \<not> irq_masks (ksMachineState s) (irq_oracle (Suc (irq_state (ksMachineState s)))) \<and> irq_oracle (Suc (irq_state (ksMachineState s))) \<noteq> 0x3FF \<and> irq_oracle (Suc (irq_state (ksMachineState s))) \<notin> non_kernel_IRQs; \<not> FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted s + 1\<rbrakk> \<Longrightarrow> \<exists>f g. s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr> = ksWorkUnitsCompleted_update f (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := g (irq_state (ksMachineState s))\<rparr>\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted s + 1 \<longrightarrow> s' = s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>; FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted s + 1 \<longrightarrow> s' = s\<lparr>ksWorkUnitsCompleted := 0, ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>\<rparr>; irq_masks (ksMachineState s) (irq_oracle (Suc (irq_state (ksMachineState s))))\<rbrakk> \<Longrightarrow> \<exists>f g. s' = ksWorkUnitsCompleted_update f (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := g (irq_state (ksMachineState s))\<rparr>\<rparr>)
 2. \<lbrakk>\<not> FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted s + 1 \<longrightarrow> s' = s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>; FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted s + 1 \<longrightarrow> s' = s\<lparr>ksWorkUnitsCompleted := 0, ksMachineState := ksMachineState s\<lparr>irq_state := Suc (irq_state (ksMachineState s))\<rparr>\<rparr>; irq_oracle (Suc (irq_state (ksMachineState s))) = 0x3FF \<or> irq_oracle (Suc (irq_state (ksMachineState s))) \<in> non_kernel_IRQs\<rbrakk> \<Longrightarrow> \<exists>f g. s' = ksWorkUnitsCompleted_update f (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := g (irq_state (ksMachineState s))\<rparr>\<rparr>)
 3. \<lbrakk>s' = s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>; \<not> irq_masks (ksMachineState s) (irq_oracle (Suc (irq_state (ksMachineState s)))) \<and> irq_oracle (Suc (irq_state (ksMachineState s))) \<noteq> 0x3FF \<and> irq_oracle (Suc (irq_state (ksMachineState s))) \<notin> non_kernel_IRQs; \<not> FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted s + 1\<rbrakk> \<Longrightarrow> \<exists>f g. s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr> = ksWorkUnitsCompleted_update f (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := g (irq_state (ksMachineState s))\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' = s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr>; \<not> irq_masks (ksMachineState s) (irq_oracle (Suc (irq_state (ksMachineState s)))) \<and> irq_oracle (Suc (irq_state (ksMachineState s))) \<noteq> 0x3FF \<and> irq_oracle (Suc (irq_state (ksMachineState s))) \<notin> non_kernel_IRQs; \<not> FaultMonad_H.workUnitsLimit \<le> ksWorkUnitsCompleted s + 1\<rbrakk> \<Longrightarrow> \<exists>f g. s\<lparr>ksWorkUnitsCompleted := ksWorkUnitsCompleted s + 1\<rparr> = ksWorkUnitsCompleted_update f (s\<lparr>ksMachineState := ksMachineState s\<lparr>irq_state := g (irq_state (ksMachineState s))\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!