theory Finalise_R

lemma (in vmdb) isFinal_untypedParent:
  assumes x: "m slot = Some cte" "isFinal (cteCap cte) slot (option_map cteCap o m)"
             "final_matters' (cteCap cte) \<and> \<not> isIRQHandlerCap (cteCap cte)"
  shows
  "m \<turnstile> x \<rightarrow> slot \<Longrightarrow>
  (\<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> RetypeDecls_H.sameRegionAs (cteCap cte') (cteCap cte))" apply (cases "x=slot", simp) apply (insert x) apply (frule subtree_mdb_next) apply (drule subtree_parent) apply (drule tranclD) apply clarsimp apply (clarsimp simp: mdb_next_unfold parentOf_def isFinal_def) apply (case_tac cte') apply (rename_tac c' n') apply (cases cte) apply (rename_tac c n) apply simp apply (erule_tac x=x in allE) apply clarsimp apply (drule isMDBParent_sameRegion) apply simp apply (rule classical, simp) apply (simp add: final_matters_sameRegion_sameObject2
                   sameObjectAs_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<rightarrow> slot \<Longrightarrow> \<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> x \<rightarrow> slot; x \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; m slot = Some cte; isFinal (cteCap cte) slot (map_option cteCap \<circ> m); final_matters' (cteCap cte) \<and> \<not> isIRQHandlerCap (cteCap cte)\<rbrakk> \<Longrightarrow> \<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> x \<rightarrow> slot; x \<noteq> slot; m slot = Some cte; isFinal (cteCap cte) slot (map_option cteCap \<circ> m); final_matters' (cteCap cte) \<and> \<not> isIRQHandlerCap (cteCap cte); m \<turnstile> x \<leadsto>\<^sup>+ slot\<rbrakk> \<Longrightarrow> \<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> slot; m slot = Some cte; isFinal (cteCap cte) slot (map_option cteCap \<circ> m); final_matters' (cteCap cte) \<and> \<not> isIRQHandlerCap (cteCap cte); m \<turnstile> x \<leadsto>\<^sup>+ slot; m \<turnstile> x parentOf slot\<rbrakk> \<Longrightarrow> \<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> slot; m slot = Some cte; isFinal (cteCap cte) slot (map_option cteCap \<circ> m); final_matters' (cteCap cte) \<and> \<not> isIRQHandlerCap (cteCap cte); m \<turnstile> x parentOf slot; \<exists>z. m \<turnstile> x \<leadsto> z \<and> m \<turnstile> z \<leadsto>\<^sup>* slot\<rbrakk> \<Longrightarrow> \<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>x \<noteq> slot; m slot = Some cte; isFinal (cteCap cte) slot (map_option cteCap \<circ> m); m \<turnstile> x parentOf slot; final_matters' (cteCap cte); \<not> isIRQHandlerCap (cteCap cte); m \<turnstile> x \<leadsto> z; m \<turnstile> z \<leadsto>\<^sup>* slot\<rbrakk> \<Longrightarrow> \<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>x \<noteq> slot; m slot = Some cte; final_matters' (cteCap cte); \<not> isIRQHandlerCap (cteCap cte); m \<turnstile> mdbNext (cteMDBNode cte') \<leadsto>\<^sup>* slot; \<not> isUntypedCap (cteCap cte); \<forall>p' c. (\<exists>z. m p' = Some z \<and> cteCap z = c) \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs (cteCap cte) c; isMDBParentOf cte' cte; m x = Some cte'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte' x1 x2. \<lbrakk>x \<noteq> slot; m slot = Some cte; final_matters' (cteCap cte); \<not> isIRQHandlerCap (cteCap cte); m \<turnstile> mdbNext (cteMDBNode cte') \<leadsto>\<^sup>* slot; \<not> isUntypedCap (cteCap cte); \<forall>p' c. (\<exists>z. m p' = Some z \<and> cteCap z = c) \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs (cteCap cte) c; isMDBParentOf cte' cte; m x = Some cte'; cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte' c' n'. \<lbrakk>x \<noteq> slot; m slot = Some cte; final_matters' (cteCap cte); \<not> isIRQHandlerCap (cteCap cte); m \<turnstile> mdbNext (cteMDBNode cte') \<leadsto>\<^sup>* slot; \<not> isUntypedCap (cteCap cte); \<forall>p' c. (\<exists>z. m p' = Some z \<and> cteCap z = c) \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs (cteCap cte) c; isMDBParentOf cte' cte; m x = Some cte'; cte' = CTE c' n'\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte' c' n' x1 x2. \<lbrakk>x \<noteq> slot; m slot = Some cte; final_matters' (cteCap cte); \<not> isIRQHandlerCap (cteCap cte); m \<turnstile> mdbNext (cteMDBNode cte') \<leadsto>\<^sup>* slot; \<not> isUntypedCap (cteCap cte); \<forall>p' c. (\<exists>z. m p' = Some z \<and> cteCap z = c) \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs (cteCap cte) c; isMDBParentOf cte' cte; m x = Some cte'; cte' = CTE c' n'; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte' c' n' c n. \<lbrakk>x \<noteq> slot; m slot = Some cte; final_matters' (cteCap cte); \<not> isIRQHandlerCap (cteCap cte); m \<turnstile> mdbNext (cteMDBNode cte') \<leadsto>\<^sup>* slot; \<not> isUntypedCap (cteCap cte); \<forall>p' c. (\<exists>z. m p' = Some z \<and> cteCap z = c) \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap c \<longrightarrow> \<not> global.sameObjectAs (cteCap cte) c; isMDBParentOf cte' cte; m x = Some cte'; cte' = CTE c' n'; cte = CTE c n\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte') \<and> global.sameRegionAs (cteCap cte') (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>cte' c' n' c n. \<lbrakk>x \<noteq> slot; m slot = Some (CTE c n); final_matters' c; \<not> isIRQHandlerCap c; m \<turnstile> mdbNext n' \<leadsto>\<^sup>* slot; \<not> isUntypedCap c; \<forall>p' ca. (\<exists>z. m p' = Some z \<and> cteCap z = ca) \<longrightarrow> slot \<noteq> p' \<longrightarrow> \<not> isUntypedCap ca \<longrightarrow> \<not> global.sameObjectAs c ca; isMDBParentOf (CTE c' n') (CTE c n); m x = Some (CTE c' n'); cte' = CTE c' n'; cte = CTE c n\<rbrakk> \<Longrightarrow> isUntypedCap c' \<and> global.sameRegionAs c' c proof (prove)
goal (1 subgoal):
 1. \<And>cte' c' n' c n. \<lbrakk>x \<noteq> slot; m slot = Some (CTE c n); final_matters' c; \<not> isIRQHandlerCap c; m \<turnstile> mdbNext n' \<leadsto>\<^sup>* slot; \<not> isUntypedCap c; isMDBParentOf (CTE c' n') (CTE c n); m x = Some (CTE c' n'); cte' = CTE c' n'; cte = CTE c n; \<forall>ca. (\<exists>z. m x = Some z \<and> cteCap z = ca) \<longrightarrow> slot \<noteq> x \<longrightarrow> \<not> isUntypedCap ca \<longrightarrow> \<not> global.sameObjectAs c ca\<rbrakk> \<Longrightarrow> isUntypedCap c' \<and> global.sameRegionAs c' c proof (prove)
goal (1 subgoal):
 1. \<And>c' n' c n. \<lbrakk>x \<noteq> slot; m slot = Some (CTE c n); final_matters' c; \<not> isIRQHandlerCap c; m \<turnstile> mdbNext n' \<leadsto>\<^sup>* slot; \<not> isUntypedCap c; isMDBParentOf (CTE c' n') (CTE c n); m x = Some (CTE c' n'); cte = CTE c n; \<not> isUntypedCap c' \<longrightarrow> \<not> global.sameObjectAs c c'\<rbrakk> \<Longrightarrow> isUntypedCap c' \<and> global.sameRegionAs c' c proof (prove)
goal (1 subgoal):
 1. \<And>c' n' c n. \<lbrakk>x \<noteq> slot; m slot = Some (CTE c n); final_matters' c; \<not> isIRQHandlerCap c; m \<turnstile> mdbNext n' \<leadsto>\<^sup>* slot; \<not> isUntypedCap c; m x = Some (CTE c' n'); cte = CTE c n; \<not> isUntypedCap c' \<longrightarrow> \<not> global.sameObjectAs c c'; global.sameRegionAs (cteCap (CTE c' n')) (cteCap (CTE c n))\<rbrakk> \<Longrightarrow> isUntypedCap c' \<and> global.sameRegionAs c' c proof (prove)
goal (1 subgoal):
 1. \<And>c' n' c n. \<lbrakk>x \<noteq> slot; m slot = Some (CTE c n); final_matters' c; \<not> isIRQHandlerCap c; m \<turnstile> mdbNext n' \<leadsto>\<^sup>* slot; \<not> isUntypedCap c; m x = Some (CTE c' n'); cte = CTE c n; \<not> isUntypedCap c' \<longrightarrow> \<not> global.sameObjectAs c c'; global.sameRegionAs c' c\<rbrakk> \<Longrightarrow> isUntypedCap c' proof (prove)
goal (1 subgoal):
 1. \<And>c' n' c n. \<lbrakk>x \<noteq> slot; m slot = Some (CTE c n); final_matters' c; \<not> isIRQHandlerCap c; m \<turnstile> mdbNext n' \<leadsto>\<^sup>* slot; \<not> isUntypedCap c; m x = Some (CTE c' n'); cte = CTE c n; \<not> global.sameObjectAs c c'; global.sameRegionAs c' c; \<not> isUntypedCap c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!