theory CSpace1_R

lemma irq_control_preserve_oneway:
  assumes dom: "\<And>x. (x \<in> dom m) = (x \<in> dom m')"
  assumes misc:
  "\<And>x cte cte'. \<lbrakk>m x =Some cte;m' x = Some cte'\<rbrakk> \<Longrightarrow>
      isIRQControlCap (cteCap cte) = isIRQControlCap (cteCap cte') \<and>
      cteMDBNode cte = cteMDBNode cte'"
  shows "irq_control m \<Longrightarrow> irq_control m'" apply (clarsimp simp:irq_control_def) apply (frule iffD2[OF dom,OF domI]) apply clarsimp apply (frule(1) misc) apply (clarsimp simp:isCap_simps) apply (case_tac y) apply (elim allE impE) apply fastforce apply clarsimp apply (drule_tac x = p' in spec) apply (erule impE) apply (frule_tac x1 = p' in iffD2[OF dom,OF domI]) apply clarsimp apply (drule(1) misc)+ apply (case_tac y) apply (simp add:isCap_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_control m \<Longrightarrow> irq_control m' proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); m' p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m' p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); m' p = Some (CTE capability.IRQControlCap n); p \<in> dom m\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m' p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n y. \<lbrakk>\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); m' p = Some (CTE capability.IRQControlCap n); m p = Some y\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m' p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n y. \<lbrakk>\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); m' p = Some (CTE capability.IRQControlCap n); m p = Some y; isIRQControlCap (cteCap y) = isIRQControlCap (cteCap (CTE capability.IRQControlCap n)) \<and> cteMDBNode y = cteMDBNode (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m' p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p y. \<lbrakk>\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); m' p = Some (CTE capability.IRQControlCap (cteMDBNode y)); m p = Some y; cteCap y = capability.IRQControlCap\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode y) \<and> (\<forall>p'. (\<exists>n'. m' p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p y x1 x2. \<lbrakk>\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); m' p = Some (CTE capability.IRQControlCap (cteMDBNode y)); m p = Some y; cteCap y = capability.IRQControlCap; y = CTE x1 x2\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode y) \<and> (\<forall>p'. (\<exists>n'. m' p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (2 subgoals):
 1. \<And>p y x1 x2. \<lbrakk>m' p = Some (CTE capability.IRQControlCap (cteMDBNode y)); m p = Some y; cteCap y = capability.IRQControlCap; y = CTE x1 x2\<rbrakk> \<Longrightarrow> m (?p17 p y x1 x2) = Some (CTE capability.IRQControlCap (?n18 p y x1 x2))
 2. \<And>p y x1 x2. \<lbrakk>m' p = Some (CTE capability.IRQControlCap (cteMDBNode y)); m p = Some y; cteCap y = capability.IRQControlCap; y = CTE x1 x2; mdbRevocable (?n18 p y x1 x2) \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = ?p17 p y x1 x2)\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode y) \<and> (\<forall>p'. (\<exists>n'. m' p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p y x1 x2. \<lbrakk>m' p = Some (CTE capability.IRQControlCap (cteMDBNode y)); m p = Some y; cteCap y = capability.IRQControlCap; y = CTE x1 x2; mdbRevocable x2 \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> mdbRevocable (cteMDBNode y) \<and> (\<forall>p'. (\<exists>n'. m' p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p x2 p' n'. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; \<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p; m' p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<And>p x2 p' n'. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>p x2 p' n'. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> \<exists>n'. m p' = Some (CTE capability.IRQControlCap n')
 2. \<And>p x2 p' n'. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); p' = p\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>p x2 p' n'. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); p' \<in> dom m\<rbrakk> \<Longrightarrow> \<exists>n'. m p' = Some (CTE capability.IRQControlCap n')
 2. \<And>p x2 p' n'. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); p' = p\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>p x2 p' n' y. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); m p' = Some y\<rbrakk> \<Longrightarrow> \<exists>n'. y = CTE capability.IRQControlCap n'
 2. \<And>p x2 p' n'. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); p' = p\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>p x2 p' n' y. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); isIRQControlCap (cteCap (CTE capability.IRQControlCap x2)) = isIRQControlCap (cteCap (CTE capability.IRQControlCap x2)) \<and> cteMDBNode (CTE capability.IRQControlCap x2) = cteMDBNode (CTE capability.IRQControlCap x2); isIRQControlCap (cteCap y) = isIRQControlCap (cteCap (CTE capability.IRQControlCap n')) \<and> cteMDBNode y = cteMDBNode (CTE capability.IRQControlCap n')\<rbrakk> \<Longrightarrow> \<exists>n'. y = CTE capability.IRQControlCap n'
 2. \<And>p x2 p' n'. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); p' = p\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (2 subgoals):
 1. \<And>p x2 p' n' y x1 x2a. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); isIRQControlCap (cteCap (CTE capability.IRQControlCap x2)) = isIRQControlCap (cteCap (CTE capability.IRQControlCap x2)) \<and> cteMDBNode (CTE capability.IRQControlCap x2) = cteMDBNode (CTE capability.IRQControlCap x2); isIRQControlCap (cteCap y) = isIRQControlCap (cteCap (CTE capability.IRQControlCap n')) \<and> cteMDBNode y = cteMDBNode (CTE capability.IRQControlCap n'); y = CTE x1 x2a\<rbrakk> \<Longrightarrow> \<exists>n'. y = CTE capability.IRQControlCap n'
 2. \<And>p x2 p' n'. \<lbrakk>m' p = Some (CTE capability.IRQControlCap x2); m p = Some (CTE capability.IRQControlCap x2); mdbRevocable x2; m' p' = Some (CTE capability.IRQControlCap n'); p' = p\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal:
No subgoals!