theory CNode_IF

lemma only_timer_irq_pres:
  assumes a: "\<And>P. \<lbrace>(\<lambda>s. P (irq_masks (machine_state s))) and Q\<rbrace>
                   f
                   \<lbrace>\<lambda>rv s. P (irq_masks (machine_state s))\<rbrace>"
  assumes b:
    "\<And>st :: 's state. \<lbrace>domain_sep_inv False st and P\<rbrace> f \<lbrace>\<lambda>_. domain_sep_inv False st\<rbrace>"
  shows
    "\<lbrace>only_timer_irq irq and Q and P and (\<lambda>s. domain_sep_inv False (st :: 's state) s)\<rbrace>
     f
     \<lbrace>\<lambda>_. only_timer_irq irq\<rbrace>" apply (clarsimp simp: only_timer_irq_def valid_def) apply (rule conjI) apply (clarsimp) apply (drule spec) apply (erule mp) apply (erule contrapos_pp, erule use_valid, rule domain_sep_inv_to_interrupt_states_pres, rule b, fastforce) apply (erule use_valid[OF _ irq_is_recurring_triv[OF a]]) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_timer_irq irq and Q and P and domain_sep_inv False st\<rbrace> f \<lbrace>\<lambda>_. only_timer_irq irq\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> (\<forall>x. interrupt_states b x = IRQTimer \<longrightarrow> x = irq) \<and> irq_is_recurring irq b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> \<forall>x. interrupt_states b x = IRQTimer \<longrightarrow> x = irq
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> irq_is_recurring irq b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); \<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s; interrupt_states b x = IRQTimer\<rbrakk> \<Longrightarrow> x = irq
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> irq_is_recurring irq b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s; interrupt_states b x = IRQTimer; interrupt_states s (?x22 s a b x) = IRQTimer \<longrightarrow> ?x22 s a b x = irq\<rbrakk> \<Longrightarrow> x = irq
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> irq_is_recurring irq b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s; interrupt_states b x = IRQTimer\<rbrakk> \<Longrightarrow> interrupt_states s x = IRQTimer
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> irq_is_recurring irq b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> irq_is_recurring irq b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; Q s; P s; domain_sep_inv False st s\<rbrakk> \<Longrightarrow> (irq_is_recurring irq and Q) s