theory CNode_IF

lemma only_timer_irq_inv_determines_irq_masks:
  "\<lbrakk>invs (s :: det_state); only_timer_irq_inv irq st s\<rbrakk> \<Longrightarrow>
   \<not> irq_masks (machine_state s) irq \<and>
   (\<forall>x. x \<noteq> irq \<longrightarrow> irq_masks (machine_state s) x)" apply (rule conjI) apply (clarsimp simp: only_timer_irq_inv_def only_timer_irq_def) apply (blast dest: irq_is_recurring_not_masked) apply (clarsimp simp: only_timer_irq_inv_def domain_sep_inv_def only_timer_irq_def) apply (case_tac "interrupt_states s x") apply (fastforce simp: invs_def valid_state_def valid_irq_states_def valid_irq_masks_def) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; only_timer_irq_inv irq st s\<rbrakk> \<Longrightarrow> \<not> irq_masks (machine_state s) irq \<and> (\<forall>x. x \<noteq> irq \<longrightarrow> irq_masks (machine_state s) x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; only_timer_irq_inv irq st s\<rbrakk> \<Longrightarrow> \<not> irq_masks (machine_state s) irq
 2. \<lbrakk>invs s; only_timer_irq_inv irq st s\<rbrakk> \<Longrightarrow> \<forall>x. x \<noteq> irq \<longrightarrow> irq_masks (machine_state s) x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; domain_sep_inv False st s; \<forall>x. interrupt_states s x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>invs s; only_timer_irq_inv irq st s\<rbrakk> \<Longrightarrow> \<forall>x. x \<noteq> irq \<longrightarrow> irq_masks (machine_state s) x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; only_timer_irq_inv irq st s\<rbrakk> \<Longrightarrow> \<forall>x. x \<noteq> irq \<longrightarrow> irq_masks (machine_state s) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>invs s; \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; \<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; \<forall>x. interrupt_states st x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; x \<noteq> irq\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) x proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>invs s; \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; \<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; \<forall>x. interrupt_states st x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; x \<noteq> irq; interrupt_states s x = IRQInactive\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) x
 2. \<And>x. \<lbrakk>invs s; \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; \<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; \<forall>x. interrupt_states st x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; x \<noteq> irq; interrupt_states s x = IRQSignal\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) x
 3. \<And>x. \<lbrakk>invs s; \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; \<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; \<forall>x. interrupt_states st x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; x \<noteq> irq; interrupt_states s x = IRQTimer\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) x
 4. \<And>x. \<lbrakk>invs s; \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; \<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; \<forall>x. interrupt_states st x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; x \<noteq> irq; interrupt_states s x = IRQReserved\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>invs s; \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; \<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; \<forall>x. interrupt_states st x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; x \<noteq> irq; interrupt_states s x = IRQSignal\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) x
 2. \<And>x. \<lbrakk>invs s; \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; \<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; \<forall>x. interrupt_states st x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; x \<noteq> irq; interrupt_states s x = IRQTimer\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) x
 3. \<And>x. \<lbrakk>invs s; \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; \<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; \<forall>x. interrupt_states st x = IRQTimer \<longrightarrow> x = irq; irq_is_recurring irq s; x \<noteq> irq; interrupt_states s x = IRQReserved\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) x proof (prove)
goal:
No subgoals!