theory CSpace_R

lemma irq' [simp]:
  "irq_control n'" using simple apply (clarsimp simp: irq_control_def) apply (frule n'_cap) apply (drule n'_rev) apply (clarsimp split: if_split_asm) apply (simp add: is_simple_cap'_def) apply (frule irq_revocable, rule irq_control) apply clarsimp apply (drule n'_cap) apply (clarsimp split: if_split_asm) apply (erule disjE) apply (clarsimp simp: is_simple_cap'_def) 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:
is_simple_cap' c'

goal (1 subgoal):
 1. irq_control n' proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>is_simple_cap' c'; n' p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'a. n' p' = Some (CTE capability.IRQControlCap n'a)) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>is_simple_cap' c'; n' p = Some (CTE capability.IRQControlCap n); \<exists>node'. if p = dest then capability.IRQControlCap = c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'a. n' p' = Some (CTE capability.IRQControlCap n'a)) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>is_simple_cap' c'; \<exists>node'. if p = dest then capability.IRQControlCap = c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE capability.IRQControlCap node'); \<exists>node'. if p = dest then mdbRevocable n = revokable' src_cap c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE capability.IRQControlCap node') \<and> mdbRevocable n = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'a. n' p' = Some (CTE capability.IRQControlCap n'a)) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>n node'. \<lbrakk>is_simple_cap' capability.IRQControlCap; c' = capability.IRQControlCap; mdbRevocable n = revokable' src_cap capability.IRQControlCap; m dest = Some (CTE dest_cap node')\<rbrakk> \<Longrightarrow> revokable' src_cap capability.IRQControlCap \<and> (\<forall>p'. (\<exists>n'a. n' p' = Some (CTE capability.IRQControlCap n'a)) \<longrightarrow> p' = dest)
 2. \<And>p n node'. \<lbrakk>is_simple_cap' c'; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'a. n' p' = Some (CTE capability.IRQControlCap n'a)) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n node'. \<lbrakk>is_simple_cap' c'; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n = mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'a. n' p' = Some (CTE capability.IRQControlCap n'a)) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n node'. \<lbrakk>is_simple_cap' c'; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n = mdbRevocable node'; mdbRevocable node'\<rbrakk> \<Longrightarrow> mdbRevocable node' \<and> (\<forall>p'. (\<exists>n'a. n' p' = Some (CTE capability.IRQControlCap n'a)) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n node' p' n'a. \<lbrakk>is_simple_cap' c'; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; mdbRevocable node'; n' p' = Some (CTE capability.IRQControlCap n'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n node' p' n'. \<lbrakk>is_simple_cap' c'; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; mdbRevocable node'; \<exists>node'. if p' = dest then capability.IRQControlCap = c' \<and> m p' = Some (CTE dest_cap node') else m p' = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n node' p' node'a. \<lbrakk>is_simple_cap' c'; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; mdbRevocable node'; p' = dest \<longrightarrow> capability.IRQControlCap = c' \<and> m dest = Some (CTE dest_cap node'a); p' = dest \<or> m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>p n node' p' node'a. \<lbrakk>is_simple_cap' c'; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; mdbRevocable node'; p' = dest \<longrightarrow> capability.IRQControlCap = c' \<and> m dest = Some (CTE dest_cap node'a); p' = dest\<rbrakk> \<Longrightarrow> p' = p
 2. \<And>p n node' p' node'a. \<lbrakk>is_simple_cap' c'; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; mdbRevocable node'; p' = dest \<longrightarrow> capability.IRQControlCap = c' \<and> m dest = Some (CTE dest_cap node'a); m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p n node' p' node'a. \<lbrakk>is_simple_cap' c'; p \<noteq> dest; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable n; mdbRevocable node'; p' = dest \<longrightarrow> capability.IRQControlCap = c' \<and> m dest = Some (CTE dest_cap node'a); m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal:
No subgoals!