theory Finalise_R

lemma irq_control_n [simp]: "irq_control n" using slot apply (clarsimp simp: irq_control_def) apply (frule n_revokable) apply (drule n_cap) apply (clarsimp split: if_split_asm) apply (frule irq_revocable, rule irq_control) apply clarsimp apply (drule n_cap) apply (clarsimp simp: if_split_asm) apply (erule (1) irq_controlD, rule irq_control) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_control n proof (prove)
using this:
m slot = Some (CTE s_cap s_node)

goal (1 subgoal):
 1. irq_control n proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>m slot = Some (CTE s_cap s_node); n p = Some (CTE capability.IRQControlCap na)\<rbrakk> \<Longrightarrow> mdbRevocable na \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>m slot = Some (CTE s_cap s_node); n p = Some (CTE capability.IRQControlCap na); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable na else mdbRevocable na = mdbRevocable node')\<rbrakk> \<Longrightarrow> mdbRevocable na \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>m slot = Some (CTE s_cap s_node); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then \<not> mdbRevocable na else mdbRevocable na = mdbRevocable node'); \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then capability.IRQControlCap = capability.NullCap else cap' = capability.IRQControlCap)\<rbrakk> \<Longrightarrow> mdbRevocable na \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na node'. \<lbrakk>m p = Some (CTE capability.IRQControlCap node'); m slot = Some (CTE s_cap s_node); p \<noteq> slot; mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na node'. \<lbrakk>m p = Some (CTE capability.IRQControlCap node'); m slot = Some (CTE s_cap s_node); p \<noteq> slot; mdbRevocable na = mdbRevocable node'; mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p na node' p' n'. \<lbrakk>m p = Some (CTE capability.IRQControlCap node'); m slot = Some (CTE s_cap s_node); p \<noteq> slot; mdbRevocable na; mdbRevocable node'; n p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n node' p' n'. \<lbrakk>m p = Some (CTE capability.IRQControlCap node'); m slot = Some (CTE s_cap s_node); p \<noteq> slot; mdbRevocable n; mdbRevocable node'; \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then capability.IRQControlCap = capability.NullCap else cap' = capability.IRQControlCap)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n node' p' node'a. \<lbrakk>m p = Some (CTE capability.IRQControlCap node'); m slot = Some (CTE s_cap s_node); p \<noteq> slot; mdbRevocable n; mdbRevocable node'; p' \<noteq> slot; m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal:
No subgoals!