theory Retype_R

lemma dlist_n: "valid_dlist n" using dlist no_0 no_0_n apply (simp add: valid_dlist_def2) apply (clarsimp simp: n_prev n_next) apply (rule conjI) apply clarsimp apply (erule allE, erule (1) impE) apply (erule_tac x=c' in allE) apply simp apply (drule P) apply (simp add: mdb_next_unfold) apply clarsimp apply (erule allE, erule (1) impE) apply (erule_tac x=c' in allE) apply simp apply (drule P) apply (simp add: mdb_prev_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist n proof (prove)
using this:
valid_dlist m
no_0 m
no_0 n

goal (1 subgoal):
 1. valid_dlist n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n\<rbrakk> \<Longrightarrow> \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> n \<turnstile> c \<leadsto> c' = n \<turnstile> c \<leftarrow> c') proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0\<rbrakk> \<Longrightarrow> (P c \<longrightarrow> \<not> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c') \<and> (\<not> P c \<longrightarrow> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c') proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0\<rbrakk> \<Longrightarrow> P c \<longrightarrow> \<not> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c'
 2. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> P c \<longrightarrow> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0; P c; \<not> P c'; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> P c \<longrightarrow> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>no_0 m; no_0 n; c \<noteq> 0; P c; \<not> P c'; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'; \<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> P c \<longrightarrow> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>no_0 m; no_0 n; c \<noteq> 0; P c; \<not> P c'; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'; c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> P c \<longrightarrow> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>no_0 m; no_0 n; c \<noteq> 0; P c; \<not> P c'; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'; m \<turnstile> c \<leadsto> c'\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> P c \<longrightarrow> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c' proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>no_0 m; no_0 n; c \<noteq> 0; \<not> P c'; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'; m \<turnstile> c \<leadsto> c'; m c = None\<rbrakk> \<Longrightarrow> False
 2. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> P c \<longrightarrow> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c' proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0\<rbrakk> \<Longrightarrow> \<not> P c \<longrightarrow> P c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> \<not> m \<turnstile> c \<leftarrow> c' proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>\<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'); no_0 m; no_0 n; c \<noteq> 0; \<not> P c; P c'; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>no_0 m; no_0 n; c \<noteq> 0; \<not> P c; P c'; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'; \<forall>c'. c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>no_0 m; no_0 n; c \<noteq> 0; \<not> P c; P c'; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'; c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>no_0 m; no_0 n; c \<noteq> 0; \<not> P c; P c'; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'; m \<turnstile> c \<leadsto> c'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>no_0 m; no_0 n; c \<noteq> 0; \<not> P c; c' \<noteq> 0; m \<turnstile> c \<leftarrow> c'; m \<turnstile> c \<leadsto> c'; m c' = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!