theory CSpace_AI

lemma parent_n:
  "n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> if p' = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> p'" apply (erule trancl_induct) apply simp apply (rule conjI) apply (rule impI) apply simp apply (clarsimp simp: n_def cdt_parent_defs) apply fastforce apply (simp split: if_split_asm) apply (rule conjI) apply (rule impI) apply simp apply (rule impI) apply (erule trancl_into_trancl) apply (clarsimp simp: n_def cdt_parent_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> if p' = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> (y = dest \<longrightarrow> m \<Turnstile> p \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> y)
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> z proof (prove)
goal (3 subgoals):
 1. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> y = dest \<longrightarrow> m \<Turnstile> p \<rightarrow> src
 2. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> y \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> y
 3. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> z proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>n \<Turnstile> p \<leadsto> y; y = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> src
 2. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> y \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> y
 3. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>y. n \<Turnstile> p \<leadsto> y \<Longrightarrow> y \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> y
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>m (a, b) = Some p; (a, b) \<noteq> dest\<rbrakk> \<Longrightarrow> (p, a, b) \<in> {(p, c). m c = Some p}\<^sup>+
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> if z = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; y \<noteq> dest; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> (z = dest \<longrightarrow> m \<Turnstile> p \<rightarrow> src) \<and> (z \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> z) proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; y \<noteq> dest; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z = dest \<longrightarrow> m \<Turnstile> p \<rightarrow> src
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; y \<noteq> dest; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; y \<noteq> dest; m \<Turnstile> p \<rightarrow> y; z = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> src
 2. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; y \<noteq> dest; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; y \<noteq> dest; m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; y \<noteq> dest; m \<Turnstile> p \<rightarrow> y; z \<noteq> dest\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n \<Turnstile> p \<rightarrow> y; n \<Turnstile> y \<leadsto> z; y \<noteq> dest; z \<noteq> dest\<rbrakk> \<Longrightarrow> m \<Turnstile> y \<leadsto> z proof (prove)
goal:
No subgoals!