theory ADT_IF

lemma next_irq_state_mono:
  assumes lep: "pos \<le> pos'"
  assumes recur: "irq_is_recurring irq s"
  assumes m: "masks = irq_masks (machine_state s)"
  shows "next_irq_state pos masks \<le> next_irq_state pos' masks" apply (insert recur m) apply (clarsimp simp: irq_is_recurring_def) apply (drule_tac x=pos' in spec) apply (erule exE) proof - fix m assume i: "is_irq_at s irq (pos' + m)" from lep have le: "pos \<le> pos' + m" by fastforce from lep show "next_irq_state pos (irq_masks (machine_state s)) \<le>
                      next_irq_state pos' (irq_masks (machine_state s))" apply - apply (induct rule: inc_induct) apply simp apply (case_tac "is_irq_at s irq n") apply (simp add: is_irq_at_next_irq_state) apply (rule less_imp_le_nat) apply (erule less_le_trans) apply (blast intro: next_irq_state_le[OF recur]) apply (subst next_irq_state.psimps) apply (rule is_irq_at_next_irq_state_dom[OF _ i]) apply simp apply (clarsimp simp: is_irq_at_def Let_def) apply (rule less_imp_le_nat) apply (erule less_le_trans) apply (blast intro: next_irq_state_le[OF recur]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_irq_state pos masks \<le> next_irq_state pos' masks proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_is_recurring irq s; masks = irq_masks (machine_state s)\<rbrakk> \<Longrightarrow> next_irq_state pos masks \<le> next_irq_state pos' 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> next_irq_state pos (irq_masks (machine_state s)) \<le> next_irq_state pos' (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 (pos' + m)\<rbrakk> \<Longrightarrow> next_irq_state pos (irq_masks (machine_state s)) \<le> next_irq_state pos' (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 (pos' + m)\<rbrakk> \<Longrightarrow> next_irq_state pos (irq_masks (machine_state s)) \<le> next_irq_state pos' (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 (pos' + m)\<rbrakk> \<Longrightarrow> next_irq_state pos (irq_masks (machine_state s)) \<le> next_irq_state pos' (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 (pos' + m)\<rbrakk> \<Longrightarrow> next_irq_state pos (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (state)
this:
is_irq_at s irq (pos' + m)

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

goal (1 subgoal):
 1. pos \<le> pos' + m proof (state)
this:
pos \<le> pos' + m

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

goal (1 subgoal):
 1. next_irq_state pos (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. pos \<le> pos' \<Longrightarrow> next_irq_state pos (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. next_irq_state pos' (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s))
 2. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> next_irq_state n (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> next_irq_state n (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); is_irq_at s irq n\<rbrakk> \<Longrightarrow> next_irq_state n (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s))
 2. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> next_irq_state n (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); is_irq_at s irq n\<rbrakk> \<Longrightarrow> n \<le> next_irq_state pos' (irq_masks (machine_state s))
 2. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> next_irq_state n (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); is_irq_at s irq n\<rbrakk> \<Longrightarrow> n < next_irq_state pos' (irq_masks (machine_state s))
 2. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> next_irq_state n (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>pos \<le> n; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); is_irq_at s irq n\<rbrakk> \<Longrightarrow> pos' \<le> next_irq_state pos' (irq_masks (machine_state s))
 2. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> next_irq_state n (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> next_irq_state n (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (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>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> (if irq_at n (irq_masks (machine_state s)) = None then next_irq_state (Suc n) (irq_masks (machine_state s)) else n) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> n \<le> pos' + m
 2. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> (if irq_at n (irq_masks (machine_state s)) = None then next_irq_state (Suc n) (irq_masks (machine_state s)) else n) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); \<not> is_irq_at s irq n\<rbrakk> \<Longrightarrow> (if irq_at n (irq_masks (machine_state s)) = None then next_irq_state (Suc n) (irq_masks (machine_state s)) else n) \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n y. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); y \<noteq> irq; irq_at n (irq_masks (machine_state s)) = Some y\<rbrakk> \<Longrightarrow> n \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n y. \<lbrakk>pos \<le> n; n < pos'; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); y \<noteq> irq; irq_at n (irq_masks (machine_state s)) = Some y\<rbrakk> \<Longrightarrow> n < next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n y. \<lbrakk>pos \<le> n; next_irq_state (Suc n) (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s)); y \<noteq> irq; irq_at n (irq_masks (machine_state s)) = Some y\<rbrakk> \<Longrightarrow> pos' \<le> next_irq_state pos' (irq_masks (machine_state s)) proof (prove)
goal:
No subgoals! proof (state)
this:
next_irq_state pos (irq_masks (machine_state s)) \<le> next_irq_state pos' (irq_masks (machine_state s))

goal:
No subgoals!