theory Finalise_R

lemma interrupt_cap_null_or_ntfn:
  "invs s
    \<Longrightarrow> cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) (interrupt_irq_node s irq, []) s" apply (frule invs_valid_irq_node) apply (clarsimp simp: valid_irq_node_def) apply (drule_tac x=irq in spec) apply (drule cte_at_0) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule caps_of_state_cteD) apply (frule if_unsafe_then_capD, clarsimp+) apply (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state) apply (frule cte_refs_obj_refs_elem, erule disjE) apply (clarsimp | drule caps_of_state_cteD valid_global_refsD[rotated]
     | rule irq_node_global_refs[where irq=irq])+ apply (simp add: cap_range_def) apply (clarsimp simp: appropriate_cte_cap_def
                 split: cap.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) (interrupt_irq_node s irq, []) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; valid_irq_node s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) (interrupt_irq_node s irq, []) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) (interrupt_irq_node s irq, []) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; inj (interrupt_irq_node s); cap_table_at 0 (interrupt_irq_node s irq) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) (interrupt_irq_node s irq, []) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; inj (interrupt_irq_node s); cte_wp_at (\<lambda>_. True) (interrupt_irq_node s irq, replicate 0 False) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) (interrupt_irq_node s irq, []) s proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; inj (interrupt_irq_node s); caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> is_ntfn_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; inj (interrupt_irq_node s); cap \<noteq> cap.NullCap; cte_wp_at ((=) cap) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> is_ntfn_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>invs s; inj (interrupt_irq_node s); cap \<noteq> cap.NullCap; cte_wp_at ((=) cap) (interrupt_irq_node s irq, []) s; ex_cte_cap_wp_to (appropriate_cte_cap cap) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> is_ntfn_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>cap a b capa. \<lbrakk>invs s; inj (interrupt_irq_node s); cap \<noteq> cap.NullCap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; caps_of_state s (a, b) = Some capa; appropriate_cte_cap cap capa; (interrupt_irq_node s irq, []) \<in> cte_refs capa (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> is_ntfn_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>cap a b capa. \<lbrakk>invs s; inj (interrupt_irq_node s); cap \<noteq> cap.NullCap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; caps_of_state s (a, b) = Some capa; appropriate_cte_cap cap capa; (interrupt_irq_node s irq, []) \<in> cte_refs capa (interrupt_irq_node s); fst (interrupt_irq_node s irq, []) \<in> obj_refs capa\<rbrakk> \<Longrightarrow> is_ntfn_cap cap
 2. \<And>cap a b capa. \<lbrakk>invs s; inj (interrupt_irq_node s); cap \<noteq> cap.NullCap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; caps_of_state s (a, b) = Some capa; appropriate_cte_cap cap capa; (interrupt_irq_node s irq, []) \<in> cte_refs capa (interrupt_irq_node s); \<exists>irq. capa = cap.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> is_ntfn_cap cap proof (prove)
goal (2 subgoals):
 1. \<And>cap capa. \<lbrakk>invs s; inj (interrupt_irq_node s); cap \<noteq> cap.NullCap; appropriate_cte_cap cap capa; (interrupt_irq_node s irq, []) \<in> cte_refs capa (interrupt_irq_node s); interrupt_irq_node s irq \<in> obj_refs capa; interrupt_irq_node s irq \<notin> cap_range cap; interrupt_irq_node s irq \<notin> cap_range capa\<rbrakk> \<Longrightarrow> is_ntfn_cap cap
 2. \<And>cap a b capa. \<lbrakk>invs s; inj (interrupt_irq_node s); cap \<noteq> cap.NullCap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; caps_of_state s (a, b) = Some capa; appropriate_cte_cap cap capa; (interrupt_irq_node s irq, []) \<in> cte_refs capa (interrupt_irq_node s); \<exists>irq. capa = cap.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> is_ntfn_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>cap a b capa. \<lbrakk>invs s; inj (interrupt_irq_node s); cap \<noteq> cap.NullCap; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; caps_of_state s (a, b) = Some capa; appropriate_cte_cap cap capa; (interrupt_irq_node s irq, []) \<in> cte_refs capa (interrupt_irq_node s); \<exists>irq. capa = cap.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> is_ntfn_cap cap proof (prove)
goal:
No subgoals!