theory Deterministic_AI

lemma next_not_child_not_self:
notes split_paired_All[simp del] split_paired_Ex[simp del]
shows
"valid_list_2 t m \<Longrightarrow> finite_depth m \<Longrightarrow> no_mloop m \<Longrightarrow> next_not_child src t m \<noteq> Some src" apply (rule notI) apply (drule next_not_childD,simp+) apply (elim disjE) apply (frule next_sib_not_self[where src=src],simp) apply (elim conjE exE) apply (frule_tac me=src and sib=q in next_sib_same_parent,assumption) apply (elim exE conjE) apply (subgoal_tac "src \<notin> descendants_of q m") apply simp apply (rule sib_not_desc,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m\<rbrakk> \<Longrightarrow> next_not_child src t m \<noteq> Some src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_not_child src t m = Some src\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = Some src \<or> next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some src \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = Some src\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some src \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = None \<and> (\<exists>q. next_sib q t m = Some src \<and> src \<in> descendants_of q m \<and> (\<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = None; next_sib q t m = Some src; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = None; next_sib q t m = Some src; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; \<exists>p. m q = Some p \<and> m src = Some p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>q p. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = None; next_sib q t m = Some src; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some p; m src = Some p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>q p. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = None; next_sib q t m = Some src; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some p; m src = Some p; src \<notin> descendants_of q m\<rbrakk> \<Longrightarrow> False
 2. \<And>q p. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = None; next_sib q t m = Some src; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some p; m src = Some p\<rbrakk> \<Longrightarrow> src \<notin> descendants_of q m proof (prove)
goal (1 subgoal):
 1. \<And>q p. \<lbrakk>valid_list_2 t m; finite_depth m; no_mloop m; next_sib src t m = None; next_sib q t m = Some src; src \<in> descendants_of q m; \<forall>q'. q' \<in> descendants_of q m \<and> src \<in> descendants_of q' m \<longrightarrow> next_sib q' t m = None; m q = Some p; m src = Some p\<rbrakk> \<Longrightarrow> src \<notin> descendants_of q m proof (prove)
goal:
No subgoals!