theory DomainSepInv

lemma cte_wp_at_not_domain_sep_inv_cap:
  "cte_wp_at (not domain_sep_inv_cap irqs) slot s \<longleftrightarrow>
   ((irqs \<longrightarrow> False) \<and>
    (\<not> irqs \<longrightarrow> (cte_wp_at ((=) IRQControlCap) slot s \<or>
                 (\<exists> irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s)))) \<or>
   cte_wp_at ((=) DomainCap) slot s" apply (rule iffI) apply (drule cte_wp_at_norm) apply clarsimp apply (case_tac c, simp_all add: domain_sep_inv_cap_def pred_neg_def) apply (auto elim: cte_wp_at_weakenE split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (not domain_sep_inv_cap irqs) slot s = ((irqs \<longrightarrow> False) \<and> (\<not> irqs \<longrightarrow> cte_wp_at ((=) IRQControlCap) slot s \<or> (\<exists>irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<or> cte_wp_at ((=) DomainCap) slot s) proof (prove)
goal (2 subgoals):
 1. cte_wp_at (not domain_sep_inv_cap irqs) slot s \<Longrightarrow> (irqs \<longrightarrow> False) \<and> (\<not> irqs \<longrightarrow> cte_wp_at ((=) IRQControlCap) slot s \<or> (\<exists>irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<or> cte_wp_at ((=) DomainCap) slot s
 2. (irqs \<longrightarrow> False) \<and> (\<not> irqs \<longrightarrow> cte_wp_at ((=) IRQControlCap) slot s \<or> (\<exists>irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<or> cte_wp_at ((=) DomainCap) slot s \<Longrightarrow> cte_wp_at (not domain_sep_inv_cap irqs) slot s proof (prove)
goal (2 subgoals):
 1. \<exists>c. cte_wp_at ((=) c) slot s \<and> (not domain_sep_inv_cap irqs) c \<Longrightarrow> (irqs \<longrightarrow> False) \<and> (\<not> irqs \<longrightarrow> cte_wp_at ((=) IRQControlCap) slot s \<or> (\<exists>irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<or> cte_wp_at ((=) DomainCap) slot s
 2. (irqs \<longrightarrow> False) \<and> (\<not> irqs \<longrightarrow> cte_wp_at ((=) IRQControlCap) slot s \<or> (\<exists>irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<or> cte_wp_at ((=) DomainCap) slot s \<Longrightarrow> cte_wp_at (not domain_sep_inv_cap irqs) slot s proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>cte_wp_at ((=) c) slot s; \<not> domain_sep_inv_cap irqs c; \<not> cte_wp_at ((=) DomainCap) slot s\<rbrakk> \<Longrightarrow> \<not> irqs \<and> (\<not> irqs \<longrightarrow> cte_wp_at ((=) IRQControlCap) slot s \<or> (\<exists>irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s))
 2. (irqs \<longrightarrow> False) \<and> (\<not> irqs \<longrightarrow> cte_wp_at ((=) IRQControlCap) slot s \<or> (\<exists>irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<or> cte_wp_at ((=) DomainCap) slot s \<Longrightarrow> cte_wp_at (not domain_sep_inv_cap irqs) slot s proof (prove)
goal (2 subgoals):
 1. \<And>c x10. \<lbrakk>cte_wp_at ((=) (IRQHandlerCap x10)) slot s; \<not> irqs; \<not> cte_wp_at ((=) DomainCap) slot s; c = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cte_wp_at ((=) IRQControlCap) slot s \<or> (\<exists>irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s)
 2. \<not> irqs \<and> (\<not> irqs \<longrightarrow> cte_wp_at ((=) IRQControlCap) slot s \<or> (\<exists>irq. cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<or> cte_wp_at ((=) DomainCap) slot s \<Longrightarrow> cte_wp_at (\<lambda>x. \<not> (case x of DomainCap \<Rightarrow> False | IRQControlCap \<Rightarrow> irqs | IRQHandlerCap irq \<Rightarrow> irqs | _ \<Rightarrow> True)) slot s proof (prove)
goal:
No subgoals!