theory CSpace_AI

lemma parency_m_n:
  assumes "m \<Turnstile> p \<rightarrow> p'"
  shows "n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp p'" using assms proof induct case (base y) thus ?case apply (simp add: s_d_swap_def) apply safe apply (rule r_into_trancl,
                 simp add: n_def n'_def cdt_parent_defs)+ done next case (step x y) thus ?case apply - apply (erule trancl_trans) apply (simp add: s_d_swap_def split: if_split_asm) apply safe apply (rule r_into_trancl,
                 simp add: n_def n'_def cdt_parent_defs)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp p' proof (prove)
using this:
m \<Turnstile> p \<rightarrow> p'

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

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

goal (1 subgoal):
 1. n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> p \<leadsto> y \<Longrightarrow> (p = dest \<longrightarrow> (y = dest \<longrightarrow> n \<Turnstile> src \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> n \<Turnstile> src \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> n \<Turnstile> src \<rightarrow> y))) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> (y = dest \<longrightarrow> n \<Turnstile> dest \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> n \<Turnstile> dest \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> n \<Turnstile> dest \<rightarrow> y))) \<and> (p \<noteq> src \<longrightarrow> (y = dest \<longrightarrow> n \<Turnstile> p \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> n \<Turnstile> p \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> n \<Turnstile> p \<rightarrow> y)))) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>m \<Turnstile> dest \<leadsto> src; p = dest; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> n \<Turnstile> src \<rightarrow> dest
 2. \<lbrakk>m \<Turnstile> dest \<leadsto> y; p = dest; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> n \<Turnstile> src \<rightarrow> y
 3. \<lbrakk>m \<Turnstile> src \<leadsto> dest; src \<noteq> dest; p = src; y = dest\<rbrakk> \<Longrightarrow> n \<Turnstile> dest \<rightarrow> src
 4. \<lbrakk>m \<Turnstile> src \<leadsto> y; src \<noteq> dest; p = src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> n \<Turnstile> dest \<rightarrow> y
 5. \<lbrakk>m \<Turnstile> p \<leadsto> dest; p \<noteq> dest; p \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> src
 6. \<lbrakk>m \<Turnstile> p \<leadsto> src; p \<noteq> dest; p \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> dest
 7. \<lbrakk>m \<Turnstile> p \<leadsto> y; p \<noteq> dest; p \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> y proof (prove)
goal:
No subgoals! proof (state)
this:
n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y\<rbrakk> \<Longrightarrow> n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp z proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y\<rbrakk> \<Longrightarrow> n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp z proof (state)
this:
m \<Turnstile> p \<rightarrow> x
m \<Turnstile> x \<leadsto> y
n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y\<rbrakk> \<Longrightarrow> n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp z proof (prove)
using this:
m \<Turnstile> p \<rightarrow> x
m \<Turnstile> x \<leadsto> y
n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp x

goal (1 subgoal):
 1. n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> x; m \<Turnstile> x \<leadsto> y; n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp x\<rbrakk> \<Longrightarrow> n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> x; m \<Turnstile> x \<leadsto> y\<rbrakk> \<Longrightarrow> n \<Turnstile> s_d_swp x \<rightarrow> s_d_swp y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> x; m \<Turnstile> x \<leadsto> y\<rbrakk> \<Longrightarrow> (x = dest \<longrightarrow> (y = dest \<longrightarrow> n \<Turnstile> src \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> n \<Turnstile> src \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> n \<Turnstile> src \<rightarrow> y))) \<and> (x \<noteq> dest \<longrightarrow> (x = src \<longrightarrow> (y = dest \<longrightarrow> n \<Turnstile> dest \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> n \<Turnstile> dest \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> n \<Turnstile> dest \<rightarrow> y))) \<and> (x \<noteq> src \<longrightarrow> (y = dest \<longrightarrow> n \<Turnstile> x \<rightarrow> src) \<and> (y \<noteq> dest \<longrightarrow> (y = src \<longrightarrow> n \<Turnstile> x \<rightarrow> dest) \<and> (y \<noteq> src \<longrightarrow> n \<Turnstile> x \<rightarrow> y)))) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>m \<Turnstile> p \<rightarrow> dest; m \<Turnstile> dest \<leadsto> src; x = dest; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> n \<Turnstile> src \<rightarrow> dest
 2. \<lbrakk>m \<Turnstile> p \<rightarrow> dest; m \<Turnstile> dest \<leadsto> y; x = dest; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> n \<Turnstile> src \<rightarrow> y
 3. \<lbrakk>m \<Turnstile> p \<rightarrow> src; m \<Turnstile> src \<leadsto> dest; src \<noteq> dest; x = src; y = dest\<rbrakk> \<Longrightarrow> n \<Turnstile> dest \<rightarrow> src
 4. \<lbrakk>m \<Turnstile> p \<rightarrow> src; m \<Turnstile> src \<leadsto> y; src \<noteq> dest; x = src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> n \<Turnstile> dest \<rightarrow> y
 5. \<lbrakk>m \<Turnstile> p \<rightarrow> x; m \<Turnstile> x \<leadsto> dest; x \<noteq> dest; x \<noteq> src; y = dest\<rbrakk> \<Longrightarrow> n \<Turnstile> x \<rightarrow> src
 6. \<lbrakk>m \<Turnstile> p \<rightarrow> x; m \<Turnstile> x \<leadsto> src; x \<noteq> dest; x \<noteq> src; src \<noteq> dest; y = src\<rbrakk> \<Longrightarrow> n \<Turnstile> x \<rightarrow> dest
 7. \<lbrakk>m \<Turnstile> p \<rightarrow> x; m \<Turnstile> x \<leadsto> y; x \<noteq> dest; x \<noteq> src; y \<noteq> dest; y \<noteq> src\<rbrakk> \<Longrightarrow> n \<Turnstile> x \<rightarrow> y proof (prove)
goal:
No subgoals! proof (state)
this:
n \<Turnstile> s_d_swp p \<rightarrow> s_d_swp y

goal:
No subgoals!