theory CSpace_R

lemma parent_n_m:
  assumes "n \<turnstile> p \<rightarrow> p'"
  shows "if p' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p'" proof - from assms have [simp]: "p \<noteq> dest" by (clarsimp simp: dest_no_parent_n) from assms show ?thesis proof induct case (direct_parent c) thus ?case apply simp apply (rule conjI) apply clarsimp apply clarsimp apply (rule subtree.direct_parent) apply (simp add: n_direct_eq split: if_split_asm) apply simp apply (clarsimp simp: parentOf_def n src new_src_def split: if_split_asm) done next case (trans_parent c d) thus ?case apply clarsimp apply (rule conjI, clarsimp) apply (clarsimp split: if_split_asm) apply (simp add: n_direct_eq) apply (cases "p=src") apply simp apply (rule subtree.direct_parent, assumption, assumption) apply (clarsimp simp: parentOf_def n src new_src_def split: if_split_asm) apply clarsimp apply (erule subtree.trans_parent, assumption, assumption) apply (clarsimp simp: parentOf_def n src new_src_def split: if_split_asm) apply (erule subtree.trans_parent) apply (simp add: n_direct_eq split: if_split_asm) apply assumption apply (clarsimp simp: parentOf_def n src new_src_def split: if_split_asm) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if p' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p' proof (state)
goal (1 subgoal):
 1. if p' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p' proof (chain)
picking this:
n \<turnstile> p \<rightarrow> p' proof (prove)
using this:
n \<turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. p \<noteq> dest proof (state)
this:
p \<noteq> dest

goal (1 subgoal):
 1. if p' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p' proof (chain)
picking this:
n \<turnstile> p \<rightarrow> p' proof (prove)
using this:
n \<turnstile> p \<rightarrow> p'

goal (1 subgoal):
 1. if p' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p' proof (state)
goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> if c' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; if c' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'' proof (state)
this:
n \<turnstile> p \<leadsto> c
c \<noteq> 0
n \<turnstile> p parentOf c

goal (2 subgoals):
 1. \<And>c'. \<lbrakk>n \<turnstile> p \<leadsto> c'; c' \<noteq> 0; n \<turnstile> p parentOf c'\<rbrakk> \<Longrightarrow> if c' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; if c' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
n \<turnstile> p \<leadsto> c
c \<noteq> 0
n \<turnstile> p parentOf c

goal (1 subgoal):
 1. if c = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> (c = dest \<longrightarrow> p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c = dest \<longrightarrow> p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> c proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> dest\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal:
No subgoals! proof (state)
this:
if c = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; if c' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; if c' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'' proof (state)
this:
n \<turnstile> p \<rightarrow> c
if c = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c
n \<turnstile> c \<leadsto> d
d \<noteq> 0
n \<turnstile> p parentOf d

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; if c' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
n \<turnstile> p \<rightarrow> c
if c = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c
n \<turnstile> c \<leadsto> d
d \<noteq> 0
n \<turnstile> p parentOf d

goal (1 subgoal):
 1. if d = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<rightarrow> c; if c = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c; n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d\<rbrakk> \<Longrightarrow> (d = dest \<longrightarrow> p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src) \<and> (d \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> d) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<rightarrow> c; if c = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> c; n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d\<rbrakk> \<Longrightarrow> d \<noteq> dest \<longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> dest \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> dest; c = dest; p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d
 2. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> dest; c = dest; p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d
 2. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> dest; c = dest; p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src; d \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d
 2. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> dest; c = dest; p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src; d \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d
 3. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> src parentOf d; n \<turnstile> src \<rightarrow> dest; c = dest; d \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> m \<turnstile> src \<rightarrow> d
 2. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> dest; c = dest; p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src; d \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d
 3. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> src parentOf d; n \<turnstile> src \<rightarrow> dest; c = dest; d \<noteq> dest; p = src\<rbrakk> \<Longrightarrow> m \<turnstile> src parentOf d
 2. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> dest; c = dest; p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src; d \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d
 3. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> dest; c = dest; p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src; d \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d
 2. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> dest; c = dest; m \<turnstile> p \<rightarrow> src; d \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d
 2. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> src \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> dest; c = dest; d \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf d
 2. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; m \<turnstile> p \<rightarrow> c; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> d
 2. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; d \<noteq> dest\<rbrakk> \<Longrightarrow> d \<noteq> 0
 3. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; d \<noteq> dest\<rbrakk> \<Longrightarrow> d \<noteq> 0
 2. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> c; c \<noteq> dest; d \<noteq> dest\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf d proof (prove)
goal:
No subgoals! proof (state)
this:
if d = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> d

goal:
No subgoals! proof (state)
this:
if p' = dest then p \<noteq> src \<longrightarrow> m \<turnstile> p \<rightarrow> src else m \<turnstile> p \<rightarrow> p'

goal:
No subgoals!