theory CSpace_AI

lemma parent_m'_m:
  assumes p_neq: "p \<noteq> dest" "p \<noteq> src"
  assumes px: "m' \<Turnstile> p \<rightarrow> x"
  shows "if x = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> x" using px proof induct case (base y) thus ?case using p_neq apply simp apply (rule conjI) apply (fastforce simp add: cdt_parent_defs m'_def m''_def) apply clarsimp apply (rule r_into_trancl) apply (clarsimp simp add: cdt_parent_defs m'_def m''_def split: if_split_asm) done next case (step y z) thus ?case apply simp apply (rule conjI) apply (clarsimp split: if_split_asm) apply (fastforce intro: trancl_trans) apply (clarsimp split: if_split_asm) apply (fastforce intro: trancl_trans) apply (erule trancl_trans) apply (rule r_into_trancl) apply (simp add: cdt_parent_defs m'_def m''_def split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if x = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> x proof (prove)
using this:
m' \<Turnstile> p \<rightarrow> x

goal (1 subgoal):
 1. if x = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> x proof (state)
goal (2 subgoals):
 1. \<And>y. m' \<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>m' \<Turnstile> p \<rightarrow> y; m' \<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 (state)
this:
m' \<Turnstile> p \<leadsto> y

goal (2 subgoals):
 1. \<And>y. m' \<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>m' \<Turnstile> p \<rightarrow> y; m' \<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)
using this:
m' \<Turnstile> p \<leadsto> y

goal (1 subgoal):
 1. if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y proof (prove)
using this:
m' \<Turnstile> p \<leadsto> y
p \<noteq> dest
p \<noteq> src

goal (1 subgoal):
 1. if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<Turnstile> p \<leadsto> y; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> (y = dest \<longrightarrow> m \<Turnstile> p \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m' \<Turnstile> p \<leadsto> y; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> y = dest \<longrightarrow> m \<Turnstile> p \<rightarrow> src
 2. \<lbrakk>m' \<Turnstile> p \<leadsto> y; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> y \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<Turnstile> p \<leadsto> y; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> y \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<Turnstile> p \<leadsto> y; p \<noteq> dest; p \<noteq> src; y \<noteq> dest\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<Turnstile> p \<leadsto> y; p \<noteq> dest; p \<noteq> src; y \<noteq> dest\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<leadsto> y proof (prove)
goal:
No subgoals! proof (state)
this:
if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<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 (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<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 (state)
this:
m' \<Turnstile> p \<rightarrow> y
m' \<Turnstile> y \<leadsto> z
if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<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)
using this:
m' \<Turnstile> p \<rightarrow> y
m' \<Turnstile> y \<leadsto> z
if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y

goal (1 subgoal):
 1. if z = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else 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. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z = dest \<longrightarrow> m \<Turnstile> p \<rightarrow> src
 2. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> src; y \<noteq> dest; m \<Turnstile> p \<rightarrow> y; z = dest\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> src
 2. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<Turnstile> y \<leadsto> z; if y = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> z \<noteq> dest \<longrightarrow> m \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m' \<Turnstile> p \<rightarrow> dest; m \<Turnstile> src \<leadsto> z; y = dest; m \<Turnstile> p \<rightarrow> src; z \<noteq> dest\<rbrakk> \<Longrightarrow> m \<Turnstile> p \<rightarrow> z
 2. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<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. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<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. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<Turnstile> y \<leadsto> z; y \<noteq> dest; z \<noteq> dest\<rbrakk> \<Longrightarrow> m \<Turnstile> y \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<Turnstile> p \<rightarrow> y; m' \<Turnstile> y \<leadsto> z; y \<noteq> dest; z \<noteq> dest\<rbrakk> \<Longrightarrow> m \<Turnstile> y \<leadsto> z proof (prove)
goal:
No subgoals! proof (state)
this:
if z = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> z

goal:
No subgoals!