theory CSpace_AI

lemma src_dest:
  assumes d: "m' \<Turnstile> dest \<rightarrow> x"
  shows "m \<Turnstile> src \<rightarrow> x" using d proof induct case (base y) thus ?case by (fastforce simp add: cdt_parent_defs m'_def m''_def split: if_split_asm) next fix y z assume dest: "m' \<Turnstile> dest \<rightarrow> y" assume y: "m' \<Turnstile> y \<leadsto> z" assume src: "m \<Turnstile> src \<rightarrow> y" from src have "y \<noteq> src" by clarsimp moreover { assume "m z = Some src" with src have "m \<Turnstile> src \<rightarrow> z" by (fastforce simp add: cdt_parent_defs) } moreover { assume "m src = Some y" hence "m \<Turnstile> y \<rightarrow> src" by (fastforce simp add: cdt_parent_defs) with src have "m \<Turnstile> src \<rightarrow> src" by (rule trancl_trans) hence False .. hence "m \<Turnstile> src \<rightarrow> z" .. } moreover { assume "m z = Some y" hence "m \<Turnstile> y \<rightarrow> z" by (fastforce simp add: cdt_parent_defs) with src have "m \<Turnstile> src \<rightarrow> z" by (rule trancl_trans) } ultimately show "m \<Turnstile> src \<rightarrow> z" using y by (simp add: cdt_parent_defs m'_def m''_def split: if_split_asm) qed

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. y \<noteq> src proof (state)
this:
y \<noteq> src

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

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

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

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

goal (1 subgoal):
 1. m \<Turnstile> src \<rightarrow> z proof (state)
this:
m \<Turnstile> src \<rightarrow> z

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. False proof (state)
this:
False

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

goal (1 subgoal):
 1. m \<Turnstile> src \<rightarrow> z proof (state)
this:
m \<Turnstile> src \<rightarrow> z

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

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

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

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

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

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

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

goal (1 subgoal):
 1. m \<Turnstile> src \<rightarrow> z proof (state)
this:
m \<Turnstile> src \<rightarrow> z

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

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

goal (1 subgoal):
 1. m \<Turnstile> src \<rightarrow> z proof (prove)
using this:
y \<noteq> src
m z = Some src \<Longrightarrow> m \<Turnstile> src \<rightarrow> z
m src = Some y \<Longrightarrow> m \<Turnstile> src \<rightarrow> z
m z = Some y \<Longrightarrow> m \<Turnstile> src \<rightarrow> z
m' \<Turnstile> y \<leadsto> z

goal (1 subgoal):
 1. m \<Turnstile> src \<rightarrow> z proof (state)
this:
m \<Turnstile> src \<rightarrow> z

goal:
No subgoals!