theory Deterministic_AI

lemma wf_cdt_parent_rel:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "finite_depth m \<Longrightarrow> wf (cdt_parent_rel m)" apply(subst wf_iff_no_infinite_down_chain) apply(rule notI) apply(clarsimp simp: finite_depth_def descendants_of_def cdt_parent_defs) apply(erule_tac x="f 0" in allE) apply(elim exE conjE) apply(erule disjE) apply(simp add: trancl_power) apply(elim exE conjE) apply(frule cdt_power) apply(assumption) apply(clarsimp) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite_depth m \<Longrightarrow> wf (cdt_parent_rel m) proof (prove)
goal (1 subgoal):
 1. finite_depth m \<Longrightarrow> \<nexists>f. \<forall>i. m \<Turnstile> f (Suc i) \<leadsto> f i proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite_depth m; \<exists>f. \<forall>i. m \<Turnstile> f (Suc i) \<leadsto> f i\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>slot. \<exists>p. ((p, slot) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> p = slot) \<and> m p = None; \<forall>i. m (f i) = Some (f (Suc i))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); \<exists>p. ((p, f 0) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> p = f 0) \<and> m p = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>f p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); (p, f 0) \<in> {(p, c). m c = Some p}\<^sup>+ \<or> p = f 0; m p = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>f p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; (p, f 0) \<in> {(p, c). m c = Some p}\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<And>f p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; p = f 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>f p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; \<exists>n>0. (p, f 0) \<in> {(p, c). m c = Some p} ^^ n\<rbrakk> \<Longrightarrow> False
 2. \<And>f p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; p = f 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>f p n. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; 0 < n; (p, f 0) \<in> {(p, c). m c = Some p} ^^ n\<rbrakk> \<Longrightarrow> False
 2. \<And>f p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; p = f 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>f p n. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; 0 < n; (p, f 0) \<in> {(p, c). m c = Some p} ^^ n\<rbrakk> \<Longrightarrow> (?p11 f p n, f 0) \<in> {(p, c). m c = Some p} ^^ ?n11 f p n
 2. \<And>f p n. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; 0 < n; (p, f 0) \<in> {(p, c). m c = Some p} ^^ n; ?p11 f p n = f (?n11 f p n)\<rbrakk> \<Longrightarrow> False
 3. \<And>f p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; p = f 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>f p n. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; 0 < n; (p, f 0) \<in> {(p, c). m c = Some p} ^^ n; p = f n\<rbrakk> \<Longrightarrow> False
 2. \<And>f p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; p = f 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>f p. \<lbrakk>\<forall>i. m (f i) = Some (f (Suc i)); m p = None; p = f 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!