theory Deterministic_AI

lemma finite_depth_insert_child:
  notes split_paired_All[simp del] split_paired_Ex[simp del]
  shows
  "finite_depth m \<Longrightarrow> finite_depth (m(dest \<mapsto> src))" apply(simp add: finite_depth_def descendants_child split del: if_split) apply(rule allI) apply(case_tac "slot=dest") apply(case_tac "m src") apply(rule_tac x=src in exI) apply(simp add: neq) apply(erule_tac x=src in allE) apply(elim exE conjE) apply(rule_tac x=p in exI) apply(simp) apply(rule notI) apply(simp add: desc neq) apply(erule_tac x=slot in allE) apply(elim conjE exE) apply(rule_tac x=p in exI) apply(simp add: neq) apply(intro conjI impI notI) apply(simp add: desc) apply(simp add: desc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite_depth m \<Longrightarrow> finite_depth (m(dest \<mapsto> src)) proof (prove)
goal (1 subgoal):
 1. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<forall>slot. \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot = dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot = dest; m src = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None
 2. \<And>slot a. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot = dest; m src = Some a\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (3 subgoals):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot = dest; m src = None\<rbrakk> \<Longrightarrow> (slot \<in> (if src \<in> descendants_of src m \<or> src = src then insert dest (descendants_of src m) else descendants_of src m) \<or> src = slot) \<and> (if src = dest then Some src else m src) = None
 2. \<And>slot a. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot = dest; m src = Some a\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None
 3. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot = dest; m src = Some a\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot a. \<lbrakk>slot = dest; m src = Some a; \<exists>p. (src \<in> descendants_of p m \<or> p = src) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot a p. \<lbrakk>slot = dest; m src = Some a; src \<in> descendants_of p m \<or> p = src; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot a p. \<lbrakk>slot = dest; m src = Some a; src \<in> descendants_of p m \<or> p = src; m p = None\<rbrakk> \<Longrightarrow> (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot a p. \<lbrakk>slot = dest; m src = Some a; src \<in> descendants_of p m \<or> p = src; m p = None\<rbrakk> \<Longrightarrow> p \<noteq> dest
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (2 subgoals):
 1. \<And>slot a p. \<lbrakk>slot = dest; m src = Some a; src \<in> descendants_of p m \<or> p = src; m p = None; p = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>\<forall>slot. \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None; slot \<noteq> dest\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot. \<lbrakk>slot \<noteq> dest; \<exists>p. (slot \<in> descendants_of p m \<or> p = slot) \<and> m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None\<rbrakk> \<Longrightarrow> \<exists>p. (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None\<rbrakk> \<Longrightarrow> (slot \<in> (if src \<in> descendants_of p m \<or> p = src then insert dest (descendants_of p m) else descendants_of p m) \<or> p = slot) \<and> (if p = dest then Some src else m p) = None proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None\<rbrakk> \<Longrightarrow> (src \<in> descendants_of p m \<longrightarrow> p \<noteq> dest) \<and> (src \<notin> descendants_of p m \<and> p \<noteq> src \<longrightarrow> p \<noteq> dest) proof (prove)
goal (2 subgoals):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; src \<in> descendants_of p m; p = dest\<rbrakk> \<Longrightarrow> False
 2. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; src \<notin> descendants_of p m \<and> p \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>slot p. \<lbrakk>slot \<noteq> dest; slot \<in> descendants_of p m \<or> p = slot; m p = None; src \<notin> descendants_of p m \<and> p \<noteq> src; p = dest\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!