theory Retype_R

lemma n_next_trancl:
  "n \<turnstile> c \<leadsto>\<^sup>+ c' \<Longrightarrow> (if P c then c' = 0 else m \<turnstile> c \<leadsto>\<^sup>+ c')" apply (insert no_0_n chain) apply (erule trancl_induct) apply (fastforce simp: n_next) apply (simp split: if_split_asm) apply (clarsimp simp: mdb_next_unfold) apply (simp add: n_next split: if_split_asm) apply (simp add: mdb_chain_0_def) apply (drule_tac x=c in bspec) apply (drule tranclD) apply (clarsimp simp: mdb_next_unfold) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> c \<leadsto>\<^sup>+ c' \<Longrightarrow> if P c then c' = 0 else m \<turnstile> c \<leadsto>\<^sup>+ c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> c \<leadsto>\<^sup>+ c'; no_0 n; mdb_chain_0 m\<rbrakk> \<Longrightarrow> if P c then c' = 0 else m \<turnstile> c \<leadsto>\<^sup>+ c' proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>no_0 n; mdb_chain_0 m; n \<turnstile> c \<leadsto> y\<rbrakk> \<Longrightarrow> if P c then y = 0 else m \<turnstile> c \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>no_0 n; mdb_chain_0 m; n \<turnstile> c \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; if P c then y = 0 else m \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if P c then z = 0 else m \<turnstile> c \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>no_0 n; mdb_chain_0 m; n \<turnstile> c \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; if P c then y = 0 else m \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if P c then z = 0 else m \<turnstile> c \<leadsto>\<^sup>+ z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>no_0 n; mdb_chain_0 m; n \<turnstile> c \<leadsto>\<^sup>+ 0; n \<turnstile> 0 \<leadsto> z; P c; y = 0\<rbrakk> \<Longrightarrow> z = 0
 2. \<And>y z. \<lbrakk>no_0 n; mdb_chain_0 m; n \<turnstile> c \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; \<not> P c; m \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>no_0 n; mdb_chain_0 m; n \<turnstile> c \<leadsto>\<^sup>+ y; n \<turnstile> y \<leadsto> z; \<not> P c; m \<turnstile> c \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>\<not> P c; m \<turnstile> c \<leadsto>\<^sup>+ y; no_0 n; mdb_chain_0 m; n \<turnstile> c \<leadsto>\<^sup>+ y; P y; z = 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>\<not> P c; m \<turnstile> c \<leadsto>\<^sup>+ y; no_0 n; \<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0; n \<turnstile> c \<leadsto>\<^sup>+ y; P y; z = 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto>\<^sup>+ 0 proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>\<not> P c; m \<turnstile> c \<leadsto>\<^sup>+ y; no_0 n; n \<turnstile> c \<leadsto>\<^sup>+ y; P y; z = 0\<rbrakk> \<Longrightarrow> c \<in> dom m
 2. \<And>y z. \<lbrakk>\<not> P c; m \<turnstile> c \<leadsto>\<^sup>+ y; no_0 n; n \<turnstile> c \<leadsto>\<^sup>+ y; P y; z = 0; m \<turnstile> c \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto>\<^sup>+ 0 proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>\<not> P c; no_0 n; n \<turnstile> c \<leadsto>\<^sup>+ y; P y; z = 0; \<exists>z. m \<turnstile> c \<leadsto> z \<and> m \<turnstile> z \<leadsto>\<^sup>* y\<rbrakk> \<Longrightarrow> c \<in> dom m
 2. \<And>y z. \<lbrakk>\<not> P c; m \<turnstile> c \<leadsto>\<^sup>+ y; no_0 n; n \<turnstile> c \<leadsto>\<^sup>+ y; P y; z = 0; m \<turnstile> c \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>\<not> P c; m \<turnstile> c \<leadsto>\<^sup>+ y; no_0 n; n \<turnstile> c \<leadsto>\<^sup>+ y; P y; z = 0; m \<turnstile> c \<leadsto>\<^sup>+ 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto>\<^sup>+ 0 proof (prove)
goal:
No subgoals!