theory Untyped_R

lemma parent_n_m:
  assumes "n \<turnstile> p \<rightarrow> p'"
  shows "if p' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> p'" proof - from assms have [simp]: "p \<noteq> site" by (clarsimp simp: site_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 parent new_parent_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=parent") apply simp apply (rule subtree.direct_parent, assumption, assumption) apply (clarsimp simp: parentOf_def n parent new_parent_def split: if_split_asm) apply clarsimp apply (erule subtree.trans_parent, assumption, assumption) apply (clarsimp simp: parentOf_def n parent new_parent_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 parent new_parent_def split: if_split_asm) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if p' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> p' proof (state)
goal (1 subgoal):
 1. if p' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent 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> site proof (state)
this:
p \<noteq> site

goal (1 subgoal):
 1. if p' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent 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' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent 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' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; if c' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent 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' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'
 2. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; if c' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent 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 = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent 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 = site \<longrightarrow> p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent) \<and> (c \<noteq> site \<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 = site \<longrightarrow> p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c\<rbrakk> \<Longrightarrow> c \<noteq> site \<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> site \<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> site\<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> site\<rbrakk> \<Longrightarrow> m \<turnstile> p \<leadsto> c
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> site\<rbrakk> \<Longrightarrow> c \<noteq> 0
 3. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> site\<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> site\<rbrakk> \<Longrightarrow> c \<noteq> 0
 2. \<lbrakk>n \<turnstile> p \<leadsto> c; c \<noteq> 0; n \<turnstile> p parentOf c; c \<noteq> site\<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> site\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf c proof (prove)
goal:
No subgoals! proof (state)
this:
if c = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c

goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; if c' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'' proof (state)
goal (1 subgoal):
 1. \<And>c' c''. \<lbrakk>n \<turnstile> p \<rightarrow> c'; if c' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'' proof (state)
this:
n \<turnstile> p \<rightarrow> c
if c = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent 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' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'; n \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; n \<turnstile> p parentOf c''\<rbrakk> \<Longrightarrow> if c'' = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c'' proof (prove)
using this:
n \<turnstile> p \<rightarrow> c
if c = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent 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 = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<rightarrow> c; if c = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c; n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d\<rbrakk> \<Longrightarrow> (d = site \<longrightarrow> p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent) \<and> (d \<noteq> site \<longrightarrow> m \<turnstile> p \<rightarrow> d) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<rightarrow> c; if c = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> c; n \<turnstile> c \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d\<rbrakk> \<Longrightarrow> d \<noteq> site \<longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> site \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> site; c = site; p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent; d \<noteq> site\<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> site; m \<turnstile> p \<rightarrow> c; d \<noteq> site\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> site; c = site; p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent; d \<noteq> site\<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> site; m \<turnstile> p \<rightarrow> c; d \<noteq> site\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> site; c = site; p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent; d \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d
 2. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> site; c = site; p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent; d \<noteq> site; p \<noteq> parent\<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> site; m \<turnstile> p \<rightarrow> c; d \<noteq> site\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> parent parentOf d; n \<turnstile> parent \<rightarrow> site; c = site; d \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<rightarrow> d
 2. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> site; c = site; p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent; d \<noteq> site; p \<noteq> parent\<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> site; m \<turnstile> p \<rightarrow> c; d \<noteq> site\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> parent parentOf d; n \<turnstile> parent \<rightarrow> site; c = site; d \<noteq> site; p = parent\<rbrakk> \<Longrightarrow> m \<turnstile> parent parentOf d
 2. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> site; c = site; p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent; d \<noteq> site; p \<noteq> parent\<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> site; m \<turnstile> p \<rightarrow> c; d \<noteq> site\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> site; c = site; p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent; d \<noteq> site; p \<noteq> parent\<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> site; m \<turnstile> p \<rightarrow> c; d \<noteq> site\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> site; c = site; m \<turnstile> p \<rightarrow> parent; d \<noteq> site; p \<noteq> parent\<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> site; m \<turnstile> p \<rightarrow> c; d \<noteq> site\<rbrakk> \<Longrightarrow> m \<turnstile> p \<rightarrow> d proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> d; d \<noteq> 0; n \<turnstile> p parentOf d; n \<turnstile> p \<rightarrow> site; c = site; d \<noteq> site; p \<noteq> parent\<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> site; m \<turnstile> p \<rightarrow> c; d \<noteq> site\<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> site; m \<turnstile> p \<rightarrow> c; d \<noteq> site\<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> site; d \<noteq> site\<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> site; d \<noteq> site\<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> site; d \<noteq> site\<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> site; d \<noteq> site\<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> site; d \<noteq> site\<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> site; d \<noteq> site\<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf d proof (prove)
goal:
No subgoals! proof (state)
this:
if d = site then p \<noteq> parent \<longrightarrow> m \<turnstile> p \<rightarrow> parent else m \<turnstile> p \<rightarrow> d

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

goal:
No subgoals!