theory ADT_IF

lemma next_irq_state_le:
  "\<lbrakk> irq_is_recurring irq s; masks = (irq_masks (machine_state s)) \<rbrakk>
     \<Longrightarrow> cur \<le> next_irq_state cur masks" apply (clarsimp simp: irq_is_recurring_def) apply (drule_tac x=cur in spec) apply (erule exE) proof - fix m assume i: "is_irq_at s irq (cur + m)" have le: "cur \<le> cur + m" by simp thus "cur \<le> next_irq_state cur (irq_masks (machine_state s))" apply - apply (induct rule: inc_induct) apply (clarsimp simp: is_irq_at_next_irq_state[OF i]) apply (case_tac "is_irq_at s irq n") apply (simp add: is_irq_at_next_irq_state) apply (subst next_irq_state.psimps) apply (rule is_irq_at_next_irq_state_dom[OF _ i]) apply simp apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_is_recurring irq s; masks = irq_masks (machine_state s)\<rbrakk> \<Longrightarrow> cur \<le> next_irq_state cur masks proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. \<exists>m. is_irq_at s irq (n + m); masks = irq_masks (machine_state s)\<rbrakk> \<Longrightarrow> cur \<le> next_irq_state cur (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>masks = irq_masks (machine_state s); \<exists>m. is_irq_at s irq (cur + m)\<rbrakk> \<Longrightarrow> cur \<le> next_irq_state cur (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>masks = irq_masks (machine_state s); is_irq_at s irq (cur + m)\<rbrakk> \<Longrightarrow> cur \<le> next_irq_state cur (irq_masks (machine_state s)) proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>masks = irq_masks (machine_state s); is_irq_at s irq (cur + m)\<rbrakk> \<Longrightarrow> cur \<le> next_irq_state cur (irq_masks (machine_state s)) proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>masks = irq_masks (machine_state s); is_irq_at s irq (cur + m)\<rbrakk> \<Longrightarrow> cur \<le> next_irq_state cur (irq_masks (machine_state s)) proof (state)
this:
is_irq_at s irq (cur + m)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>masks = irq_masks (machine_state s); is_irq_at s irq (cur + m)\<rbrakk> \<Longrightarrow> cur \<le> next_irq_state cur (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. cur \<le> cur + m proof (state)
this:
cur \<le> cur + m

goal (1 subgoal):
 1. \<And>m. \<lbrakk>masks = irq_masks (machine_state s); is_irq_at s irq (cur + m)\<rbrakk> \<Longrightarrow> cur \<le> next_irq_state cur (irq_masks (machine_state s)) proof (prove)
using this:
cur \<le> cur + m

goal (1 subgoal):
 1. cur \<le> next_irq_state cur (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. cur \<le> cur + m \<Longrightarrow> cur \<le> next_irq_state cur (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. cur + m \<le> next_irq_state (cur + m) (irq_masks (machine_state s))
 2. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> n \<le> next_irq_state n (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> n \<le> next_irq_state n (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s)); is_irq_at s irq n\<rbrakk> \<Longrightarrow> n \<le> next_irq_state n (irq_masks (machine_state s))
 2. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> n \<le> next_irq_state n (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> n \<le> next_irq_state n (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> next_irq_state_dom (n, irq_masks (machine_state s))
 2. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> n \<le> (if irq_at n (irq_masks (machine_state s)) = None then next_irq_state (Suc n) (irq_masks (machine_state s)) else n) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> n \<le> cur + m
 2. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> n \<le> (if irq_at n (irq_masks (machine_state s)) = None then next_irq_state (Suc n) (irq_masks (machine_state s)) else n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>cur \<le> n; n < cur + m; Suc n \<le> next_irq_state (Suc n) (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> n \<le> (if irq_at n (irq_masks (machine_state s)) = None then next_irq_state (Suc n) (irq_masks (machine_state s)) else n) proof (prove)
goal:
No subgoals! proof (state)
this:
cur \<le> next_irq_state cur (irq_masks (machine_state s))

goal:
No subgoals!