theory CSpace_I

lemma irq_control_init:
  assumes no_irq: "cap = IRQControlCap \<longrightarrow> no_irq' m"
  assumes ctrl: "irq_control m"
  shows "irq_control (m(p \<mapsto> CTE cap initMDBNode))" using no_irq apply (clarsimp simp: irq_control_def) apply (rule conjI) apply (clarsimp simp: initMDBNode_def) apply (erule (1) no_irqD') apply clarsimp apply (frule irq_revocable, rule ctrl) apply clarsimp apply (rule conjI) apply clarsimp apply (erule (1) no_irqD') apply clarsimp apply (erule (1) irq_controlD, rule ctrl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_control (m(p \<mapsto> CTE cap initMDBNode)) proof (prove)
using this:
cap = capability.IRQControlCap \<longrightarrow> no_irq' m

goal (1 subgoal):
 1. irq_control (m(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<And>pa. cap = capability.IRQControlCap \<longrightarrow> no_irq' m \<Longrightarrow> (pa = p \<longrightarrow> cap = capability.IRQControlCap \<longrightarrow> mdbRevocable initMDBNode \<and> (\<forall>p'. p' \<noteq> p \<longrightarrow> (\<forall>n'. m p' \<noteq> Some (CTE capability.IRQControlCap n')))) \<and> (pa \<noteq> p \<longrightarrow> (\<forall>n. m pa = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (p' = p \<longrightarrow> cap \<noteq> capability.IRQControlCap) \<and> (p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa)))) proof (prove)
goal (2 subgoals):
 1. \<And>pa. cap = capability.IRQControlCap \<longrightarrow> no_irq' m \<Longrightarrow> pa = p \<longrightarrow> cap = capability.IRQControlCap \<longrightarrow> mdbRevocable initMDBNode \<and> (\<forall>p'. p' \<noteq> p \<longrightarrow> (\<forall>n'. m p' \<noteq> Some (CTE capability.IRQControlCap n')))
 2. \<And>pa. cap = capability.IRQControlCap \<longrightarrow> no_irq' m \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>n. m pa = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (p' = p \<longrightarrow> cap \<noteq> capability.IRQControlCap) \<and> (p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa))) proof (prove)
goal (2 subgoals):
 1. \<And>p' n'. \<lbrakk>no_irq' m; cap = capability.IRQControlCap; p' \<noteq> p; m p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> False
 2. \<And>pa. cap = capability.IRQControlCap \<longrightarrow> no_irq' m \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>n. m pa = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (p' = p \<longrightarrow> cap \<noteq> capability.IRQControlCap) \<and> (p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa))) proof (prove)
goal (1 subgoal):
 1. \<And>pa. cap = capability.IRQControlCap \<longrightarrow> no_irq' m \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>n. m pa = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (p' = p \<longrightarrow> cap \<noteq> capability.IRQControlCap) \<and> (p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa))) proof (prove)
goal (1 subgoal):
 1. \<And>pa n. \<lbrakk>cap = capability.IRQControlCap \<longrightarrow> no_irq' m; pa \<noteq> p; m pa = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (p' = p \<longrightarrow> cap \<noteq> capability.IRQControlCap) \<and> (p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa)) proof (prove)
goal (1 subgoal):
 1. \<And>pa n. \<lbrakk>cap = capability.IRQControlCap \<longrightarrow> no_irq' m; pa \<noteq> p; m pa = Some (CTE capability.IRQControlCap n); mdbRevocable n\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (p' = p \<longrightarrow> cap \<noteq> capability.IRQControlCap) \<and> (p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa)) proof (prove)
goal (1 subgoal):
 1. \<And>pa n p'. \<lbrakk>cap = capability.IRQControlCap \<longrightarrow> no_irq' m; pa \<noteq> p; m pa = Some (CTE capability.IRQControlCap n); mdbRevocable n\<rbrakk> \<Longrightarrow> (p' = p \<longrightarrow> cap \<noteq> capability.IRQControlCap) \<and> (p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa) proof (prove)
goal (2 subgoals):
 1. \<And>pa n p'. \<lbrakk>cap = capability.IRQControlCap \<longrightarrow> no_irq' m; pa \<noteq> p; m pa = Some (CTE capability.IRQControlCap n); mdbRevocable n\<rbrakk> \<Longrightarrow> p' = p \<longrightarrow> cap \<noteq> capability.IRQControlCap
 2. \<And>pa n p'. \<lbrakk>cap = capability.IRQControlCap \<longrightarrow> no_irq' m; pa \<noteq> p; m pa = Some (CTE capability.IRQControlCap n); mdbRevocable n\<rbrakk> \<Longrightarrow> p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa proof (prove)
goal (2 subgoals):
 1. \<And>pa n. \<lbrakk>no_irq' m; pa \<noteq> p; m pa = Some (CTE capability.IRQControlCap n); mdbRevocable n; cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> False
 2. \<And>pa n p'. \<lbrakk>cap = capability.IRQControlCap \<longrightarrow> no_irq' m; pa \<noteq> p; m pa = Some (CTE capability.IRQControlCap n); mdbRevocable n\<rbrakk> \<Longrightarrow> p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa proof (prove)
goal (1 subgoal):
 1. \<And>pa n p'. \<lbrakk>cap = capability.IRQControlCap \<longrightarrow> no_irq' m; pa \<noteq> p; m pa = Some (CTE capability.IRQControlCap n); mdbRevocable n\<rbrakk> \<Longrightarrow> p' \<noteq> p \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = pa proof (prove)
goal (1 subgoal):
 1. \<And>pa n p' n'. \<lbrakk>cap = capability.IRQControlCap \<longrightarrow> no_irq' m; pa \<noteq> p; m pa = Some (CTE capability.IRQControlCap n); mdbRevocable n; p' \<noteq> p; m p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = pa proof (prove)
goal:
No subgoals!