theory ADT_H

lemma has_next_not_child_is_descendant:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "next_not_child slot t m = Some slot2 \<Longrightarrow> (\<exists>p. slot \<in> descendants_of p m)" apply (drule next_not_childD) apply (simp add: m_def finite_depth assms')+ using assms' apply (simp add: valid_mdb_def) apply (elim disjE) apply (drule next_sib_same_parent[OF valid_list_2]) apply (elim exE) apply (rule_tac x=p in exI) apply (rule child_descendant) apply simp apply (elim conjE exE) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_not_child slot t m = Some slot2 \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (3 subgoals):
 1. finite_depth m
 2. no_mloop m
 3. next_sib slot t m = Some slot2 \<or> next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (2 subgoals):
 1. no_mloop (cdt s)
 2. next_sib slot t m = Some slot2 \<or> next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m 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. no_mloop (cdt s)
 2. next_sib slot t m = Some slot2 \<or> next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (1 subgoal):
 1. next_sib slot t m = Some slot2 \<or> next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (2 subgoals):
 1. next_sib slot t m = Some slot2 \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m
 2. next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (2 subgoals):
 1. \<exists>p. m slot = Some p \<and> m slot2 = Some p \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m
 2. next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (2 subgoals):
 1. \<And>p. m slot = Some p \<and> m slot2 = Some p \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m
 2. next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (2 subgoals):
 1. \<And>p. m slot = Some p \<and> m slot2 = Some p \<Longrightarrow> slot \<in> descendants_of p m
 2. next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (2 subgoals):
 1. \<And>p. m slot = Some p \<and> m slot2 = Some p \<Longrightarrow> m slot = Some p
 2. next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (1 subgoal):
 1. next_sib slot t m = None \<and> (\<exists>q. next_sib q t m = Some slot2 \<and> slot \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None)) \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>next_sib slot t m = None; next_sib q t m = Some slot2; slot \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> slot \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> \<exists>p. slot \<in> descendants_of p m proof (prove)
goal:
No subgoals!