theory CSpace1_R

lemma ut_revocable_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> cteMDBNode cte = cteMDBNode cte'
  \<and> isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte')"
  shows  "ut_revocable' m \<Longrightarrow> ut_revocable' m'" apply (clarsimp simp:ut_revocable'_def Let_def) apply (drule_tac x = p in spec) apply (frule domI[where m = m'],drule iffD2[OF dom],erule domE) apply (case_tac r) apply clarsimp apply (elim allE impE) apply (frule(1) misc) apply (clarsimp) apply (drule(1) misc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ut_revocable' m \<Longrightarrow> ut_revocable' m' proof (prove)
goal (1 subgoal):
 1. \<And>p cap n. \<lbrakk>\<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; m' p = Some (CTE cap n); isUntypedCap cap\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (1 subgoal):
 1. \<And>p cap n. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; \<forall>cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (1 subgoal):
 1. \<And>p cap n r. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; \<forall>cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; m p = Some r\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (1 subgoal):
 1. \<And>p cap n r x1 x2. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; \<forall>cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; m p = Some r; r = CTE x1 x2\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (1 subgoal):
 1. \<And>p cap n x1 x2. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; isUntypedCap x1 \<longrightarrow> mdbRevocable x2; m p = Some (CTE x1 x2)\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (2 subgoals):
 1. \<And>p cap n x1 x2. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; m p = Some (CTE x1 x2)\<rbrakk> \<Longrightarrow> isUntypedCap x1
 2. \<And>p cap n x1 x2. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; m p = Some (CTE x1 x2); mdbRevocable x2\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (2 subgoals):
 1. \<And>p cap n x1 x2. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; m p = Some (CTE x1 x2); cteMDBNode (CTE x1 x2) = cteMDBNode (CTE cap n) \<and> isUntypedCap (cteCap (CTE x1 x2)) = isUntypedCap (cteCap (CTE cap n))\<rbrakk> \<Longrightarrow> isUntypedCap x1
 2. \<And>p cap n x1 x2. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; m p = Some (CTE x1 x2); mdbRevocable x2\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (1 subgoal):
 1. \<And>p cap n x1 x2. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; m p = Some (CTE x1 x2); mdbRevocable x2\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (1 subgoal):
 1. \<And>p cap n x1 x2. \<lbrakk>m' p = Some (CTE cap n); isUntypedCap cap; mdbRevocable x2; cteMDBNode (CTE x1 x2) = cteMDBNode (CTE cap n) \<and> isUntypedCap (cteCap (CTE x1 x2)) = isUntypedCap (cteCap (CTE cap n))\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal:
No subgoals!