theory ADT_H

lemma next_slot_cte_at:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "next_slot slot t m = Some slot2 \<Longrightarrow> cte_at slot s" apply (cut_tac valid_mdb_mdb_cte_at) prefer 2 apply (cut_tac assms') apply simp apply (fold m_def) apply (simp add: mdb_cte_at_def) apply (simp add: cte_wp_at_caps_of_state) apply (drule has_next_slot_is_descendant) apply (elim disjE) apply force apply (elim exE) apply (drule descendant_has_parent) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_slot slot t m = Some slot2 \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_slot slot t m = Some slot2; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state ?s1 p = Some c \<and> cap.NullCap \<noteq> c) (cdt ?s1)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s
 2. next_slot slot t m = Some slot2 \<Longrightarrow> valid_mdb ?s1 proof (prove)
goal (2 subgoals):
 1. next_slot slot t m = Some slot2 \<Longrightarrow> valid_mdb ?s1
 2. \<lbrakk>next_slot slot t m = Some slot2; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state ?s1 p = Some c \<and> cap.NullCap \<noteq> c) (cdt ?s1)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>next_slot slot t m = Some slot2; pspace_aligned s; pspace_distinct s; pspace_aligned' s'; pspace_distinct' s'; valid_objs s; valid_mdb s; valid_list s\<rbrakk> \<Longrightarrow> valid_mdb ?s1
 2. \<lbrakk>next_slot slot t m = Some slot2; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state ?s1 p = Some c \<and> cap.NullCap \<noteq> c) (cdt ?s1)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_slot slot t m = Some slot2; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_slot slot t m = Some slot2; mdb_cte_at (\<lambda>p. \<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) m\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_slot slot t m = Some slot2; \<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>ca. caps_of_state s c = Some ca \<and> cap.NullCap \<noteq> ca)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_slot slot t m = Some slot2; \<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>ca. caps_of_state s c = Some ca \<and> cap.NullCap \<noteq> ca)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s slot = Some cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>ca. caps_of_state s c = Some ca \<and> cap.NullCap \<noteq> ca); m slot2 = Some slot \<or> (\<exists>p. slot \<in> descendants_of p m)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s slot = Some cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>ca. caps_of_state s c = Some ca \<and> cap.NullCap \<noteq> ca); m slot2 = Some slot\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s slot = Some cap
 2. \<lbrakk>\<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>ca. caps_of_state s c = Some ca \<and> cap.NullCap \<noteq> ca); \<exists>p. slot \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s slot = Some cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>ca. caps_of_state s c = Some ca \<and> cap.NullCap \<noteq> ca); \<exists>p. slot \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s slot = Some cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>ca. caps_of_state s c = Some ca \<and> cap.NullCap \<noteq> ca); slot \<in> descendants_of p m\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s slot = Some cap proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. caps_of_state s p = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>ca. caps_of_state s c = Some ca \<and> cap.NullCap \<noteq> ca); \<exists>q. m slot = Some q\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s slot = Some cap proof (prove)
goal:
No subgoals!