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 = src then m' \<Turnstile> p \<rightarrow> dest 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) 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) apply clarsimp done qed

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

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

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

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

goal:
No subgoals!