theory DomainSepInv

lemma domain_sep_inv_wp:
  assumes nctrl:
    "\<And>slot. \<lbrace>(\<lambda>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s) and P\<rbrace>
             f
             \<lbrace>\<lambda>_ s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) slot s\<rbrace>"
  assumes irq_pres:
    "\<And>P. \<not> irqs \<Longrightarrow> \<lbrace>(\<lambda>s. P (interrupt_states s)) and R\<rbrace>
                     f
                     \<lbrace>\<lambda>_ s. P (interrupt_states s)\<rbrace>"
  shows
    "\<lbrace>domain_sep_inv irqs st and P and (\<lambda>s. irqs \<or> R s)\<rbrace>
     f
     \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>" apply (clarsimp simp: domain_sep_inv_def2 valid_def) apply (subst conj_assoc[symmetric]) apply (rule conjI) apply (rule conjI) apply (intro allI) apply (erule use_valid[OF _ hoare_strengthen_post[OF nctrl]]) apply (fastforce simp: cte_wp_at_not_domain_sep_inv_cap) apply (fastforce simp: cte_wp_at_not_domain_sep_inv_cap) apply (fastforce elim!: use_valid[OF _ hoare_strengthen_post[OF nctrl]]
                     simp: cte_wp_at_not_domain_sep_inv_cap) apply (case_tac "irqs") apply blast apply (rule disjI2) apply simp apply (intro allI conjI) apply (erule_tac P1="\<lambda>x. x irq \<noteq> IRQSignal" in use_valid[OF _ irq_pres], assumption) apply blast apply (erule use_valid[OF _ irq_pres], assumption) apply blast apply (erule use_valid[OF _ irq_pres], assumption) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>domain_sep_inv irqs st and P and (\<lambda>s. irqs \<or> R s)\<rbrace> f \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> (\<forall>a ba. \<not> cte_wp_at ((=) DomainCap) (a, ba) b) \<and> (irqs \<or> (\<forall>irq a ba. \<not> cte_wp_at ((=) IRQControlCap) (a, ba) b \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, ba) b)) \<and> (irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> ((\<forall>a ba. \<not> cte_wp_at ((=) DomainCap) (a, ba) b) \<and> (irqs \<or> (\<forall>irq a ba. \<not> cte_wp_at ((=) IRQControlCap) (a, ba) b \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, ba) b))) \<and> (irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st)) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> (\<forall>a ba. \<not> cte_wp_at ((=) DomainCap) (a, ba) b) \<and> (irqs \<or> (\<forall>irq a ba. \<not> cte_wp_at ((=) IRQControlCap) (a, ba) b \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, ba) b))
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st) proof (prove)
goal (3 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> \<forall>a ba. \<not> cte_wp_at ((=) DomainCap) (a, ba) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq a ba. \<not> cte_wp_at ((=) IRQControlCap) (a, ba) b \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, ba) b)
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st) proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> \<not> cte_wp_at ((=) DomainCap) (aa, ba) b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq a ba. \<not> cte_wp_at ((=) IRQControlCap) (a, ba) b \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, ba) b)
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st) proof (prove)
goal (4 subgoals):
 1. \<And>s a b aa ba rv sa. \<lbrakk>\<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s; \<not> cte_wp_at (not domain_sep_inv_cap irqs) (?slot26 s a b aa ba) sa\<rbrakk> \<Longrightarrow> \<not> cte_wp_at ((=) DomainCap) (aa, ba) sa
 2. \<And>s a b aa ba. \<lbrakk>\<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> ((\<lambda>sa. \<not> cte_wp_at (not domain_sep_inv_cap irqs) (?slot26 s a b aa ba) sa) and P) s
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq a ba. \<not> cte_wp_at ((=) IRQControlCap) (a, ba) b \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, ba) b)
 4. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st) proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba. \<lbrakk>\<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> cte_wp_at (not domain_sep_inv_cap irqs) (aa, ba) s) and P) s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq a ba. \<not> cte_wp_at ((=) IRQControlCap) (a, ba) b \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, ba) b)
 3. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq a ba. \<not> cte_wp_at ((=) IRQControlCap) (a, ba) b \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, ba) b)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s; irqs\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s; \<not> irqs\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s; \<not> irqs\<rbrakk> \<Longrightarrow> irqs \<or> (\<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); \<forall>a b. \<not> cte_wp_at ((=) DomainCap) (a, b) s; irqs \<or> (\<forall>irq a b. \<not> cte_wp_at ((=) IRQControlCap) (a, b) s \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) (a, b) s); irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st); P s; irqs \<or> R s; \<not> irqs\<rbrakk> \<Longrightarrow> \<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> \<forall>irq. interrupt_states b irq \<noteq> IRQSignal \<and> interrupt_states b irq \<noteq> IRQReserved \<and> interrupt_states b = interrupt_states st proof (prove)
goal (3 subgoals):
 1. \<And>s a b irq. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> interrupt_states b irq \<noteq> IRQSignal
 2. \<And>s a b irq. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> interrupt_states b irq \<noteq> IRQReserved
 3. \<And>s a b irq. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> interrupt_states b = interrupt_states st proof (prove)
goal (3 subgoals):
 1. \<And>s a b irq. \<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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> ((\<lambda>s. interrupt_states s irq \<noteq> IRQSignal) and R) s
 2. \<And>s a b irq. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> interrupt_states b irq \<noteq> IRQReserved
 3. \<And>s a b irq. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> interrupt_states b = interrupt_states st proof (prove)
goal (2 subgoals):
 1. \<And>s a b irq. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> interrupt_states b irq \<noteq> IRQReserved
 2. \<And>s a b irq. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> interrupt_states b = interrupt_states st proof (prove)
goal (2 subgoals):
 1. \<And>s a b irq. \<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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> ((\<lambda>s. interrupt_states s irq \<noteq> IRQReserved) and R) s
 2. \<And>s a b irq. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> interrupt_states b = interrupt_states st proof (prove)
goal (1 subgoal):
 1. \<And>s a b irq. \<lbrakk>(a, b) \<in> fst (f 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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> interrupt_states b = interrupt_states st proof (prove)
goal (1 subgoal):
 1. \<And>s a b irq. \<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; \<forall>irq. interrupt_states s irq \<noteq> IRQSignal \<and> interrupt_states s irq \<noteq> IRQReserved \<and> interrupt_states s = interrupt_states st; P s; R s; \<not> irqs\<rbrakk> \<Longrightarrow> ((\<lambda>s. interrupt_states s = interrupt_states st) and R) s proof (prove)
goal:
No subgoals!