theory ADT_H

lemma next_sib_2_reachable: "next_sib_2 slot p s = Some slot2  \<Longrightarrow> m' \<turnstile> (cte_map slot) \<leadsto>\<^sup>* (cte_map slot2)" apply (induct slot rule: next_sib_2_pinduct[where s=s and p=p]) apply (cut_tac slot=slot and s=s and p=p in next_sib_2.psimps[OF next_sib_2_termination], (simp add: assms')+) apply (fold m_def t_def) apply (simp split: if_split_asm) apply (case_tac "next_slot slot t m") apply simp apply (simp split: if_split_asm) apply (rule r_into_rtrancl) apply (erule next_slot_mdb_next) apply (rule trans) apply (rule r_into_rtrancl) apply (rule next_slot_mdb_next) apply (simp add: assms' valid_list_2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_sib_2 slot p s = Some slot2 \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2 proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; next_sib_2 slot p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p (cdt s); next_slot slot (cdt_list s) (cdt s) = Some a; cdt s a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; (if slot \<in> descendants_of p (cdt s) then case next_slot slot (cdt_list s) (cdt s) of None \<Rightarrow> None | Some next \<Rightarrow> if cdt s next = Some p then Some next else next_sib_2 next p s else None) = Some slot2; next_sib_2 slot p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 2. valid_mdb s
 3. valid_list s proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<And>a. \<lbrakk>slot \<in> descendants_of p m; next_slot slot t m = Some a; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; (if slot \<in> descendants_of p m then case next_slot slot t m of None \<Rightarrow> None | Some next \<Rightarrow> if m next = Some p then Some next else next_sib_2 next p s else None) = Some slot2; next_sib_2 slot p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 2. valid_mdb s
 3. valid_list_2 t m proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>next_sib_2 slot p s = Some slot2; \<And>a. \<lbrakk>next_slot slot t m = Some a; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; (case next_slot slot t m of None \<Rightarrow> None | Some next \<Rightarrow> if m next = Some p then Some next else next_sib_2 next p s) = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 2. valid_mdb s
 3. valid_list_2 t m proof (prove)
goal (4 subgoals):
 1. \<And>slot. \<lbrakk>next_sib_2 slot p s = Some slot2; \<And>a. \<lbrakk>next_slot slot t m = Some a; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; (case next_slot slot t m of None \<Rightarrow> None | Some next \<Rightarrow> if m next = Some p then Some next else next_sib_2 next p s) = Some slot2; next_slot slot t m = None\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 2. \<And>slot a. \<lbrakk>next_sib_2 slot p s = Some slot2; \<And>a. \<lbrakk>next_slot slot t m = Some a; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; (case next_slot slot t m of None \<Rightarrow> None | Some next \<Rightarrow> if m next = Some p then Some next else next_sib_2 next p s) = Some slot2; next_slot slot t m = Some a\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 3. valid_mdb s
 4. valid_list_2 t m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>next_sib_2 slot p s = Some slot2; \<And>a. \<lbrakk>next_slot slot t m = Some a; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; (case next_slot slot t m of None \<Rightarrow> None | Some next \<Rightarrow> if m next = Some p then Some next else next_sib_2 next p s) = Some slot2; next_slot slot t m = Some a\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 2. valid_mdb s
 3. valid_list_2 t m proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_slot slot t m = Some slot2; next_sib_2 slot p s = Some slot2; slot \<in> descendants_of p m; m slot2 = Some p; a = slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 2. \<And>slot a. \<lbrakk>next_slot slot t m = Some a; next_sib_2 slot p s = Some slot2; m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 3. valid_mdb s
 4. valid_list_2 t m proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_slot slot t m = Some slot2; next_sib_2 slot p s = Some slot2; slot \<in> descendants_of p m; m slot2 = Some p; a = slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map slot2
 2. \<And>slot a. \<lbrakk>next_slot slot t m = Some a; next_sib_2 slot p s = Some slot2; m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 3. valid_mdb s
 4. valid_list_2 t m proof (prove)
goal (3 subgoals):
 1. \<And>slot a. \<lbrakk>next_slot slot t m = Some a; next_sib_2 slot p s = Some slot2; m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map slot2
 2. valid_mdb s
 3. valid_list_2 t m proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_slot slot t m = Some a; next_sib_2 slot p s = Some slot2; m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto>\<^sup>* cte_map (?y32 slot a)
 2. \<And>slot a. \<lbrakk>next_slot slot t m = Some a; next_sib_2 slot p s = Some slot2; m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map (?y32 slot a) \<leadsto>\<^sup>* cte_map slot2
 3. valid_mdb s
 4. valid_list_2 t m proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_slot slot t m = Some a; next_sib_2 slot p s = Some slot2; m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map slot \<leadsto> cte_map (?y32 slot a)
 2. \<And>slot a. \<lbrakk>next_slot slot t m = Some a; next_sib_2 slot p s = Some slot2; m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map (?y32 slot a) \<leadsto>\<^sup>* cte_map slot2
 3. valid_mdb s
 4. valid_list_2 t m proof (prove)
goal (4 subgoals):
 1. \<And>slot a. \<lbrakk>next_slot slot t m = Some a; next_sib_2 slot p s = Some slot2; m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> next_slot slot t m = Some (?y32 slot a)
 2. \<And>slot a. \<lbrakk>next_slot slot t m = Some a; next_sib_2 slot p s = Some slot2; m' \<turnstile> cte_map a \<leadsto>\<^sup>* cte_map slot2; slot \<in> descendants_of p m; m a \<noteq> Some p; next_sib_2 a p s = Some slot2\<rbrakk> \<Longrightarrow> m' \<turnstile> cte_map (?y32 slot a) \<leadsto>\<^sup>* cte_map slot2
 3. valid_mdb s
 4. valid_list_2 t m proof (prove)
goal:
No subgoals!