theory CSpace1_R

lemma caps_contained'_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>
  isUntypedCap (cteCap cte) = isUntypedCap (cteCap cte')
  \<and> untypedRange (cteCap cte) = untypedRange (cteCap cte')
  \<and> capRange (cteCap cte) = capRange (cteCap cte')
  \<and> cteMDBNode cte = cteMDBNode cte'"
  shows "caps_contained' m \<Longrightarrow> caps_contained' m'" apply (clarsimp simp:caps_contained'_def) apply (frule iffD2[OF dom,OF domI]) apply (frule_tac x1 = p' in iffD2[OF dom,OF domI]) apply clarsimp apply (case_tac y,case_tac ya) apply (drule_tac x= p in spec) apply (drule_tac x= p' in spec) apply (frule_tac x = p in misc) apply assumption apply (frule_tac x = p' in misc) apply assumption apply (elim allE impE) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_contained' m \<Longrightarrow> caps_contained' m' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<in> dom m\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p \<in> dom m; p' \<in> dom m\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x y ya. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; \<forall>p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> m' p = Some (?cte'38 p p' c n c' n' x y ya x1 x2 x1a x2a)
 2. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); isUntypedCap (cteCap y) = isUntypedCap (cteCap (?cte'38 p p' c n c' n' x y ya x1 x2 x1a x2a)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (?cte'38 p p' c n c' n' x y ya x1 x2 x1a x2a)) \<and> capRange (cteCap y) = capRange (cteCap (?cte'38 p p' c n c' n' x y ya x1 x2 x1a x2a)) \<and> cteMDBNode y = cteMDBNode (?cte'38 p p' c n c' n' x y ya x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (2 subgoals):
 1. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n)\<rbrakk> \<Longrightarrow> m' p' = Some (?cte'40 p p' c n c' n' x y ya x1 x2 x1a x2a)
 2. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n); isUntypedCap (cteCap ya) = isUntypedCap (cteCap (?cte'40 p p' c n c' n' x y ya x1 x2 x1a x2a)) \<and> untypedRange (cteCap ya) = untypedRange (cteCap (?cte'40 p p' c n c' n' x y ya x1 x2 x1a x2a)) \<and> capRange (cteCap ya) = capRange (cteCap (?cte'40 p p' c n c' n' x y ya x1 x2 x1a x2a)) \<and> cteMDBNode ya = cteMDBNode (?cte'40 p p' c n c' n' x y ya x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n); isUntypedCap (cteCap ya) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap ya) = untypedRange (cteCap (CTE c' n')) \<and> capRange (cteCap ya) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode ya = cteMDBNode (CTE c' n')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (5 subgoals):
 1. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n); isUntypedCap (cteCap ya) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap ya) = untypedRange (cteCap (CTE c' n')) \<and> capRange (cteCap ya) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode ya = cteMDBNode (CTE c' n')\<rbrakk> \<Longrightarrow> \<exists>na. m p = Some (CTE (?c42 p p' c n c' n' x y ya x1 x2 x1a x2a) na)
 2. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n); isUntypedCap (cteCap ya) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap ya) = untypedRange (cteCap (CTE c' n')) \<and> capRange (cteCap ya) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode ya = cteMDBNode (CTE c' n')\<rbrakk> \<Longrightarrow> \<exists>n'a. m p' = Some (CTE (?c'44 p p' c n c' n' x y ya x1 x2 x1a x2a) n'a)
 3. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n); isUntypedCap (cteCap ya) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap ya) = untypedRange (cteCap (CTE c' n')) \<and> capRange (cteCap ya) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode ya = cteMDBNode (CTE c' n')\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (?c'44 p p' c n c' n' x y ya x1 x2 x1a x2a)
 4. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n); isUntypedCap (cteCap ya) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap ya) = untypedRange (cteCap (CTE c' n')) \<and> capRange (cteCap ya) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode ya = cteMDBNode (CTE c' n')\<rbrakk> \<Longrightarrow> capRange (?c'44 p p' c n c' n' x y ya x1 x2 x1a x2a) \<inter> untypedRange (?c42 p p' c n c' n' x y ya x1 x2 x1a x2a) \<noteq> {}
 5. \<And>p p' c n c' n' x y ya x1 x2 x1a x2a. \<lbrakk>m' p = Some (CTE c n); m' p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; m p = Some y; m p' = Some ya; y = CTE x1 x2; ya = CTE x1a x2a; isUntypedCap (cteCap y) = isUntypedCap (cteCap (CTE c n)) \<and> untypedRange (cteCap y) = untypedRange (cteCap (CTE c n)) \<and> capRange (cteCap y) = capRange (cteCap (CTE c n)) \<and> cteMDBNode y = cteMDBNode (CTE c n); isUntypedCap (cteCap ya) = isUntypedCap (cteCap (CTE c' n')) \<and> untypedRange (cteCap ya) = untypedRange (cteCap (CTE c' n')) \<and> capRange (cteCap ya) = capRange (cteCap (CTE c' n')) \<and> cteMDBNode ya = cteMDBNode (CTE c' n'); capRange (?c'44 p p' c n c' n' x y ya x1 x2 x1a x2a) \<subseteq> untypedRange (?c42 p p' c n c' n' x y ya x1 x2 x1a x2a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal:
No subgoals!