theory CSpace_AI

lemma dest_src:
  assumes "m \<Turnstile> src \<rightarrow> x"
  shows "m' \<Turnstile> dest \<rightarrow> x" using assms proof induct case (base y) thus ?case by (fastforce simp add: cdt_parent_defs m'_def m''_def) next case (step y z) thus ?case apply - apply (erule trancl_trans) apply (rule r_into_trancl) apply (simp (no_asm) add: cdt_parent_defs m'_def m''_def) apply (rule conjI) apply (clarsimp simp: cdt_parent_defs) apply clarsimp apply (rule conjI) apply clarsimp apply (drule trancl_trans, erule r_into_trancl) apply simp apply clarsimp apply (rule conjI) apply clarsimp apply (subgoal_tac "y = src") apply simp apply (clarsimp simp: cdt_parent_defs) apply (clarsimp simp: cdt_parent_defs) done qed

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

goal (1 subgoal):
 1. m' \<Turnstile> dest \<rightarrow> x proof (state)
goal (2 subgoals):
 1. \<And>y. m \<Turnstile> src \<leadsto> y \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> y
 2. \<And>y z. \<lbrakk>m \<Turnstile> src \<rightarrow> y; m \<Turnstile> y \<leadsto> z; m' \<Turnstile> dest \<rightarrow> y\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> z proof (state)
this:
m \<Turnstile> src \<leadsto> y

goal (2 subgoals):
 1. \<And>y. m \<Turnstile> src \<leadsto> y \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> y
 2. \<And>y z. \<lbrakk>m \<Turnstile> src \<rightarrow> y; m \<Turnstile> y \<leadsto> z; m' \<Turnstile> dest \<rightarrow> y\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> z proof (prove)
using this:
m \<Turnstile> src \<leadsto> y

goal (1 subgoal):
 1. m' \<Turnstile> dest \<rightarrow> y proof (state)
this:
m' \<Turnstile> dest \<rightarrow> y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> src \<rightarrow> y; m \<Turnstile> y \<leadsto> z; m' \<Turnstile> dest \<rightarrow> y\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> z proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> src \<rightarrow> y; m \<Turnstile> y \<leadsto> z; m' \<Turnstile> dest \<rightarrow> y\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> z proof (state)
this:
m \<Turnstile> src \<rightarrow> y
m \<Turnstile> y \<leadsto> z
m' \<Turnstile> dest \<rightarrow> y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> src \<rightarrow> y; m \<Turnstile> y \<leadsto> z; m' \<Turnstile> dest \<rightarrow> y\<rbrakk> \<Longrightarrow> m' \<Turnstile> dest \<rightarrow> z proof (prove)
using this:
m \<Turnstile> src \<rightarrow> y
m \<Turnstile> y \<leadsto> z
m' \<Turnstile> dest \<rightarrow> y

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

goal:
No subgoals!