theory Scheduler_IF

lemma irq_inactive_or_timer:
  "\<lbrace>domain_sep_inv False st and Q IRQTimer and Q IRQInactive\<rbrace>
   get_irq_state irq
   \<lbrace>Q\<rbrace>" apply (simp add:get_irq_state_def) apply wp apply (clarsimp simp add: domain_sep_inv_def) apply (drule_tac x=irq in spec) apply (drule_tac x=a in spec)  (*makes yellow variables*)
   apply (drule_tac x=b in spec) apply (drule_tac x=aa in spec, drule_tac x=ba in spec) apply clarsimp apply (case_tac "interrupt_states st irq") apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and Q IRQTimer and Q IRQInactive\<rbrace> get_irq_state irq \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv False st and Q IRQTimer and Q IRQInactive\<rbrace> gets (\<lambda>s. interrupt_states s irq) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (domain_sep_inv False st and Q IRQTimer and Q IRQInactive) s \<Longrightarrow> Q (interrupt_states s irq) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<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; Q IRQTimer s; Q IRQInactive s\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; Q IRQTimer s; Q IRQInactive s; \<forall>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\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Q IRQTimer s; Q IRQInactive s; \<forall>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>b. \<not> cte_wp_at ((=) DomainCap) (a, b) s\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Q IRQTimer s; Q IRQInactive s; \<forall>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>b. \<not> cte_wp_at ((=) DomainCap) (a, b) s\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Q IRQTimer s; Q IRQInactive s; \<forall>b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; \<forall>ba. \<not> cte_wp_at ((=) IRQControlCap) (b, ba) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (b, ba) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Q IRQTimer s; Q IRQInactive s; \<not> cte_wp_at ((=) DomainCap) (a, aa) s; \<not> cte_wp_at ((=) IRQControlCap) (b, ba) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (b, ba) s \<and> interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Q IRQTimer s; Q IRQInactive s; \<not> cte_wp_at ((=) DomainCap) (a, aa) s; \<not> cte_wp_at ((=) IRQControlCap) (b, ba) s; \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (b, ba) s; interrupt_states st irq \<noteq> IRQSignal; interrupt_states st irq \<noteq> IRQReserved; interrupt_states s = interrupt_states st\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>Q IRQTimer s; Q IRQInactive s; \<not> cte_wp_at ((=) DomainCap) (a, aa) s; \<not> cte_wp_at ((=) IRQControlCap) (b, ba) s; \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (b, ba) s; interrupt_states st irq \<noteq> IRQSignal; interrupt_states st irq \<noteq> IRQReserved; interrupt_states s = interrupt_states st; interrupt_states st irq = IRQInactive\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s
 2. \<And>s. \<lbrakk>Q IRQTimer s; Q IRQInactive s; \<not> cte_wp_at ((=) DomainCap) (a, aa) s; \<not> cte_wp_at ((=) IRQControlCap) (b, ba) s; \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (b, ba) s; interrupt_states st irq \<noteq> IRQSignal; interrupt_states st irq \<noteq> IRQReserved; interrupt_states s = interrupt_states st; interrupt_states st irq = IRQSignal\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s
 3. \<And>s. \<lbrakk>Q IRQTimer s; Q IRQInactive s; \<not> cte_wp_at ((=) DomainCap) (a, aa) s; \<not> cte_wp_at ((=) IRQControlCap) (b, ba) s; \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (b, ba) s; interrupt_states st irq \<noteq> IRQSignal; interrupt_states st irq \<noteq> IRQReserved; interrupt_states s = interrupt_states st; interrupt_states st irq = IRQTimer\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s
 4. \<And>s. \<lbrakk>Q IRQTimer s; Q IRQInactive s; \<not> cte_wp_at ((=) DomainCap) (a, aa) s; \<not> cte_wp_at ((=) IRQControlCap) (b, ba) s; \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (b, ba) s; interrupt_states st irq \<noteq> IRQSignal; interrupt_states st irq \<noteq> IRQReserved; interrupt_states s = interrupt_states st; interrupt_states st irq = IRQReserved\<rbrakk> \<Longrightarrow> Q (interrupt_states st irq) s proof (prove)
goal:
No subgoals!