theory Retype_R

lemma mdb_chunked_n: "mdb_chunked n" proof - from valid have "mdb_chunked m" .. thus ?thesis apply (clarsimp simp: mdb_chunked_def) apply (simp add: n_Some_eq split: if_split_asm) apply (simp add: n_Some_eq n_trancl_eq n_rtrancl_eq is_chunk_def) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chunked n proof (state)
goal (1 subgoal):
 1. mdb_chunked n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. mdb_chunked m proof (state)
this:
mdb_chunked m

goal (1 subgoal):
 1. mdb_chunked n proof (prove)
using this:
mdb_chunked m

goal (1 subgoal):
 1. mdb_chunked n proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap na cap' n'. \<lbrakk>\<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); n p = Some (CTE cap na); n p' = Some (CTE cap' n'); global.sameRegionAs cap cap'; p \<noteq> p'\<rbrakk> \<Longrightarrow> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n cap p p') \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap na cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)); \<not> P p; m p = Some (CTE cap na); \<not> P p'; m p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<or> n \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (n \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk n cap p p') \<and> (n \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk n cap' p' p) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap n cap' n'. \<lbrakk>global.sameRegionAs cap cap'; p \<noteq> p'; \<forall>p p' cap. (\<exists>n. m p = Some (CTE cap n)) \<longrightarrow> (\<forall>cap'. (\<exists>n'. m p' = Some (CTE cap' n')) \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> p \<noteq> p' \<longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap''))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))); \<not> P p; m p = Some (CTE cap n); \<not> P p'; m p' = Some (CTE cap' n')\<rbrakk> \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> (\<forall>p''. (P p'' \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> p' \<noteq> 0 \<and> p'' \<noteq> p') \<and> (\<not> P p'' \<longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap cap'')))) \<and> (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> (\<forall>p''. (P p'' \<longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> p \<noteq> 0 \<and> p'' \<noteq> p) \<and> (\<not> P p'' \<longrightarrow> m \<turnstile> p' \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p \<longrightarrow> (\<exists>cap''. (\<exists>n''. m p'' = Some (CTE cap'' n'')) \<and> global.sameRegionAs cap' cap'')))) proof (prove)
goal:
No subgoals! proof (state)
this:
mdb_chunked n

goal:
No subgoals!