theory CNodeInv_AI

lemma cap_swap_irq_handlers[wp]:
  "\<lbrace>valid_irq_handlers and
    cte_wp_at (weak_derived c) a and
    cte_wp_at (weak_derived c') b\<rbrace>
     cap_swap c a c' b \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>" apply (simp add: valid_irq_handlers_def irq_issued_def) apply (rule hoare_pre) apply (wp hoare_use_eq [where f=interrupt_states,
                           OF cap_swap_interrupt_states cap_swap_caps_of_state]) apply (clarsimp simp: cte_wp_at_caps_of_state
                 elim!: ranE split: if_split_asm
                 dest!: weak_derived_cap_irqs) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q11\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> ?Q11 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal) and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b) s \<Longrightarrow> \<forall>cap\<in>ran ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal proof (prove)
goal (3 subgoals):
 1. \<And>s aa ba irq capa capb. \<lbrakk>irq \<in> cap_irqs capa; \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal; caps_of_state s a = Some capa; cap_irqs c = cap_irqs capa; caps_of_state s (aa, ba) = Some capb; cap_irqs c' = cap_irqs capb; b = (aa, ba)\<rbrakk> \<Longrightarrow> interrupt_states s irq = IRQSignal
 2. \<And>s cap aa ba irq capa capb. \<lbrakk>irq \<in> cap_irqs capb; \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal; caps_of_state s a = Some capa; cap_irqs c = cap_irqs capa; caps_of_state s b = Some capb; cap_irqs cap = cap_irqs capb; a \<noteq> b; (aa, ba) = a; c' = cap\<rbrakk> \<Longrightarrow> interrupt_states s irq = IRQSignal
 3. \<And>s cap aa ba irq capa capb. \<lbrakk>irq \<in> cap_irqs cap; \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal; caps_of_state s a = Some capa; cap_irqs c = cap_irqs capa; caps_of_state s b = Some capb; cap_irqs c' = cap_irqs capb; (aa, ba) \<noteq> b; (aa, ba) \<noteq> a; caps_of_state s (aa, ba) = Some cap\<rbrakk> \<Longrightarrow> interrupt_states s irq = IRQSignal proof (prove)
goal:
No subgoals!