theory CSpace_R

lemma (in mdb_insert_der) irq_control_n:
  "irq_control n" using src dest partial_is_derived' apply (clarsimp simp: irq_control_def) apply (frule n_cap) apply (drule n_revocable) apply (clarsimp split: if_split_asm) apply (simp add: is_derived'_def isCap_simps) 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_derived'_def isCap_simps) 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 src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)
is_derived' m src c' src_cap

goal (1 subgoal):
 1. irq_control n proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; 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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; n p = Some (CTE capability.IRQControlCap na); \<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 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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; \<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 na = revokable' src_cap c' else mdbRevocable na = mdbRevocable node' \<and> m p = Some (CTE capability.IRQControlCap node')\<rbrakk> \<Longrightarrow> mdbRevocable na \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src capability.IRQControlCap src_cap; mdbRevocable na = revokable' src_cap capability.IRQControlCap; c' = capability.IRQControlCap\<rbrakk> \<Longrightarrow> revokable' src_cap capability.IRQControlCap \<and> (\<forall>p'. (\<exists>n'. n p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = dest)
 2. \<And>p na node'. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; p \<noteq> dest; mdbRevocable na = mdbRevocable node'; m p = Some (CTE capability.IRQControlCap 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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; p \<noteq> dest; mdbRevocable na = mdbRevocable node'; m p = Some (CTE capability.IRQControlCap 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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; p \<noteq> dest; mdbRevocable na = mdbRevocable node'; m p = Some (CTE capability.IRQControlCap 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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; p \<noteq> dest; mdbRevocable na; m p = Some (CTE capability.IRQControlCap node'); 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 src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; p \<noteq> dest; mdbRevocable n; m p = Some (CTE capability.IRQControlCap node'); 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>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; p \<noteq> dest; mdbRevocable n; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable node'; p' = dest \<longrightarrow> capability.IRQControlCap = c' \<and> dest_node = 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>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; p \<noteq> dest; mdbRevocable n; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable node'; p' = dest \<longrightarrow> capability.IRQControlCap = c' \<and> dest_node = node'a; p' = dest\<rbrakk> \<Longrightarrow> p' = p
 2. \<And>p n node' p' node'a. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; p \<noteq> dest; mdbRevocable n; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable node'; p' = dest \<longrightarrow> capability.IRQControlCap = c' \<and> dest_node = 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>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); is_derived' m src c' src_cap; p \<noteq> dest; mdbRevocable n; m p = Some (CTE capability.IRQControlCap node'); mdbRevocable node'; p' = dest \<longrightarrow> capability.IRQControlCap = c' \<and> dest_node = node'a; m p' = Some (CTE capability.IRQControlCap node'a)\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal:
No subgoals!