theory ADT_IF

lemma preemption_point_irq_state_inv'[wp]:
  "\<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace>
   preemption_point
   \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" apply (simp add: preemption_point_def) apply (wpsimp wp: OR_choiceE_wp[where P'="irq_state_inv st and K(irq_is_recurring irq st)"
                                    and P''="irq_state_inv st and K(irq_is_recurring irq st)"]
              simp: reset_work_units_def)+ apply simp apply (wpsimp wp: OR_choiceE_wp dmo_getActiveIRQ_wp simp: reset_work_units_def)+ apply (clarsimp simp: irq_state_inv_def) apply (simp add: next_irq_state_Suc[OF _ recurring_next_irq_state_dom]) apply (clarsimp simp: irq_state_next_def) apply (simp add: next_irq_state_Suc'[OF _ recurring_next_irq_state_dom]) apply (wp | simp add: update_work_units_def irq_state_inv_def | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> preemption_point \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)\<rbrace> doE y <- liftE update_work_units;
OR_choiceE work_units_limit_reached (doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE) (returnOk ())
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s. ?B3 () s \<Longrightarrow> irq_state_inv st s \<and> irq_is_recurring irq st
 2. \<And>y. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>y. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> returnOk () \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<lbrace>?Q2\<rbrace> liftE update_work_units \<lbrace>?B3\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 5. \<And>s. (irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)) s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> doE y <- liftE reset_work_units;
liftE (do_machine_op (getActiveIRQ True)) >>=E case_option (returnOk ()) (\<lambda>y. throwError ())
odE \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<And>y. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> returnOk () \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<lbrace>?Q2\<rbrace> liftE update_work_units \<lbrace>\<lambda>a b. irq_state_inv st b \<and> irq_is_recurring irq st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>s. (irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)) s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>irq_state_inv st s; irq_is_recurring irq st\<rbrakk> \<Longrightarrow> (irq_at (Suc (irq_state_of_state s)) (irq_masks_of_state s) = None \<longrightarrow> irq_state_inv st (s\<lparr>work_units_completed := 0, machine_state := machine_state s\<lparr>irq_state := Suc (irq_state_of_state s)\<rparr>\<rparr>)) \<and> ((\<exists>x. irq_at (Suc (irq_state_of_state s)) (irq_masks_of_state s) = Some x) \<longrightarrow> irq_state_next st (s\<lparr>work_units_completed := 0, machine_state := machine_state s\<lparr>irq_state := Suc (irq_state_of_state s)\<rparr>\<rparr>))
 2. \<And>y. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> returnOk () \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<lbrace>?Q2\<rbrace> liftE update_work_units \<lbrace>\<lambda>a b. irq_state_inv st b \<and> irq_is_recurring irq st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>s. (irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)) s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>irq_is_recurring irq st; irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st)\<rbrakk> \<Longrightarrow> (irq_at (Suc (irq_state_of_state s)) (irq_masks_of_state st) = None \<longrightarrow> next_irq_state (Suc (Suc (irq_state_of_state s))) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st)) \<and> ((\<exists>x. irq_at (Suc (irq_state_of_state s)) (irq_masks_of_state st) = Some x) \<longrightarrow> irq_state_next st (s\<lparr>work_units_completed := 0, machine_state := machine_state s\<lparr>irq_state := Suc (irq_state_of_state s)\<rparr>\<rparr>))
 2. \<And>y. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> returnOk () \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<lbrace>?Q2\<rbrace> liftE update_work_units \<lbrace>\<lambda>a b. irq_state_inv st b \<and> irq_is_recurring irq st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>s. (irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)) s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>irq_is_recurring irq st; irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st)\<rbrakk> \<Longrightarrow> (\<exists>x. irq_at (Suc (irq_state_of_state s)) (irq_masks_of_state st) = Some x) \<longrightarrow> irq_state_next st (s\<lparr>work_units_completed := 0, machine_state := machine_state s\<lparr>irq_state := Suc (irq_state_of_state s)\<rparr>\<rparr>)
 2. \<And>y. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> returnOk () \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<lbrace>?Q2\<rbrace> liftE update_work_units \<lbrace>\<lambda>a b. irq_state_inv st b \<and> irq_is_recurring irq st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>s. (irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)) s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>irq_is_recurring irq st; irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st); irq_at (Suc (irq_state_of_state s)) (irq_masks_of_state st) = Some x\<rbrakk> \<Longrightarrow> Suc (irq_state_of_state s) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st)
 2. \<And>y. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> returnOk () \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<lbrace>?Q2\<rbrace> liftE update_work_units \<lbrace>\<lambda>a b. irq_state_inv st b \<and> irq_is_recurring irq st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 4. \<And>s. (irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)) s \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>irq_state_inv st and K (irq_is_recurring irq st)\<rbrace> returnOk () \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 2. \<lbrace>?Q2\<rbrace> liftE update_work_units \<lbrace>\<lambda>a b. irq_state_inv st b \<and> irq_is_recurring irq st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>
 3. \<And>s. (irq_state_inv st and (\<lambda>y. irq_is_recurring irq st)) s \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!