theory ADT_H

lemma next_slot_mdb_next:
  notes split_paired_All[simp del]
  shows
 "next_slot slot t m = Some slot2 \<Longrightarrow> m' \<turnstile> (cte_map slot) \<leadsto> (cte_map slot2)" apply (frule cte_at_has_cap[OF next_slot_cte_at]) apply (elim exE) apply (cut_tac s=s and s'=s' in pspace_relation_ctes_ofI) apply (fold m'_def) using rel apply (simp add: state_relation_def) apply simp using assms' apply simp using assms' apply simp apply (subgoal_tac "cdt_list_relation t m m'") apply (simp add: cdt_list_relation_def) apply (elim exE) apply (case_tac cte) apply (simp add: mdb_next_rel_def mdb_next_def) apply force using rel apply (simp add: state_relation_def m_def t_def m'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_slot slot t m = Some slot2 \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_slot slot t m = Some slot2; \<exists>c. cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
goal (5 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?c3 c)) (?slot3 c) s
 3. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 4. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 5. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. ctes_of s' (cte_map (?slot3 c)) = Some cte \<and> cap_relation (?c3 c) (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
goal (5 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?c3 c)) (?slot3 c) s
 3. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 4. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 5. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map (?slot3 c)) = Some cte \<and> cap_relation (?c3 c) (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
using this:
(s, s') \<in> state_relation

goal (5 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_relation (kheap s) (ksPSpace s')
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?c3 c)) (?slot3 c) s
 3. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 4. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 5. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map (?slot3 c)) = Some cte \<and> cap_relation (?c3 c) (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
goal (4 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?c3 c)) (?slot3 c) s
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 3. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 4. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map (?slot3 c)) = Some cte \<and> cap_relation (?c3 c) (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
goal (3 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 3. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
using this:
pspace_aligned s
pspace_distinct s
pspace_aligned' s'
pspace_distinct' s'
valid_objs s
valid_mdb s
valid_list s

goal (3 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_aligned' s'
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 3. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
using this:
pspace_aligned s
pspace_distinct s
pspace_aligned' s'
pspace_distinct' s'
valid_objs s
valid_mdb s
valid_list s

goal (2 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s\<rbrakk> \<Longrightarrow> pspace_distinct' s'
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2 proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte); cdt_list_relation t m m'\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cdt_list_relation t m m' proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte); \<forall>c cap node. m' (cte_map c) = Some (CTE cap node) \<longrightarrow> (case next_slot c t m of None \<Rightarrow> True | Some next \<Rightarrow> mdbNext node = cte_map next)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cdt_list_relation t m m' proof (prove)
goal (2 subgoals):
 1. \<And>c cte. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<forall>c cap node. m' (cte_map c) = Some (CTE cap node) \<longrightarrow> (case next_slot c t m of None \<Rightarrow> True | Some next \<Rightarrow> mdbNext node = cte_map next); m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cdt_list_relation t m m' proof (prove)
goal (2 subgoals):
 1. \<And>c cte x1 x2. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<forall>c cap node. m' (cte_map c) = Some (CTE cap node) \<longrightarrow> (case next_slot c t m of None \<Rightarrow> True | Some next \<Rightarrow> mdbNext node = cte_map next); m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cdt_list_relation t m m' proof (prove)
goal (2 subgoals):
 1. \<And>c cte x1 x2. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<forall>c cap node. m' (cte_map c) = Some (CTE cap node) \<longrightarrow> (case next_slot c t m of None \<Rightarrow> True | Some next \<Rightarrow> mdbNext node = cte_map next); m' (cte_map slot) = Some (CTE x1 x2) \<and> cap_relation c x1; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> mdbNext x2 = cte_map slot2
 2. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cdt_list_relation t m m' proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cdt_list_relation t m m' proof (prove)
using this:
(s, s') \<in> state_relation

goal (1 subgoal):
 1. \<And>c. \<lbrakk>next_slot slot t m = Some slot2; cte_wp_at ((=) c) slot s; \<exists>cte. m' (cte_map slot) = Some cte \<and> cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cdt_list_relation t m m' proof (prove)
goal:
No subgoals!