# HG changeset patch
# User nipkow
# Date 1199872595 -3600
# Node ID b213fd2924bef1be87d98b3926541089a13cb700
# Parent  69c32d6a88c72310cd147eb9a59ebb87fdcd5f39
Finally: no more unproven.

diff -r 69c32d6a88c7 -r b213fd2924be src/HOL/ex/NBE.thy
--- a/src/HOL/ex/NBE.thy	Wed Jan 09 08:57:12 2008 +0100
+++ b/src/HOL/ex/NBE.thy	Wed Jan 09 10:56:35 2008 +0100
@@ -5,8 +5,6 @@
 
 theory NBE imports Main Executable_Set begin
 
-axiomatization where unproven: "PROP A"
-
 declare Let_def[simp]
 
 consts_code undefined ("(raise Match)")
@@ -16,9 +14,7 @@
       ml_var_name = nat
       const_name = nat
 
-datatype tm = Ct const_name | Vt lam_var_name | Lam tm | At tm tm
-            | term_of ml (* function 'to_term' *)
-and ml = (* rep of universal datatype *)
+datatype ml = (* rep of universal datatype *)
           C const_name "ml list" | V lam_var_name "ml list"
         | Fun ml "ml list" nat
         | "apply" ml ml (* function 'apply' *)
@@ -26,6 +22,9 @@
         | V_ML ml_var_name | A_ML ml "ml list" | Lam_ML ml
         | CC const_name (* ref to compiled code *)
 
+datatype tm = Ct const_name | Vt lam_var_name | Lam tm | At tm tm
+            | term_of ml (* function 'to_term' *)
+
 lemma [simp]: "x \<in> set vs \<Longrightarrow> size x < Suc (list_size size vs)"
 by (induct vs) auto
 lemma [simp]:"x \<in> set vs \<Longrightarrow> size x < Suc (size v + list_size size vs)"
@@ -212,11 +211,12 @@
 done
 
 inductive_set
-  tRed :: "(tm * tm)set" (* beta + R reduction on pure terms *)
+  tRed :: "(tm * tm)set" (* beta red + eta exp + R reduction on pure terms *)
   and tred :: "[tm, tm] => bool"  (infixl "\<rightarrow>" 50)
 where
   "s \<rightarrow> t == (s, t) \<in> tRed"
 | "At (Lam t) s \<rightarrow> t[s/0]"
+| "t \<rightarrow> Lam (At (lift 0 t) (Vt 0))"
 | "(nm,ts,t) : R ==> foldl At (Ct nm) (map (subst rs) ts) \<rightarrow> subst rs t"
 | "t \<rightarrow> t' ==> Lam t \<rightarrow> Lam t'"
 | "s \<rightarrow> s' ==> At s t \<rightarrow> At s' t"
@@ -330,12 +330,37 @@
 
 lemma listsum_size'[simp]:
  "v \<in> set vs \<Longrightarrow> size' v < Suc(listsum (map size' vs))"
-by (rule unproven)
+by(induct vs)(auto)
 
 corollary cor_listsum_size'[simp]:
  "v \<in> set vs \<Longrightarrow> size' v < Suc(m + listsum (map size' vs))"
 using listsum_size'[of v vs] by arith
 
+lemma size'_lift_ML: "size' (lift\<^bsub>ML\<^esub> k v) = size' v"
+apply(induct v arbitrary:k rule:size'.induct)
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp)
+apply simp
+apply simp
+apply(simp)
+done
+
+(* FIXME needed? *)
 lemma
 size_subst_ML[simp]: includes Vars assumes A: "!i. size(f i) = 0"
   shows "size(subst\<^bsub>ML\<^esub> f v) = size(v)"
@@ -344,12 +369,58 @@
   by (induct f v and f t rule: subst_ml_ML_subst_tm_ML.induct)
     (simp_all add: o_def cons_ML_def split: nat.split)
 
+(* FIXME name and use explicitly *)
 lemma [simp]:
- "\<forall>i j. size'(f i) = size'(V_ML j) \<Longrightarrow> size' (subst\<^bsub>ML\<^esub> f v) = size' v"
-by (rule unproven)
+ "\<forall>i j. size'(f i) = 1 \<Longrightarrow> size' (subst\<^bsub>ML\<^esub> f v) = size' v"
+apply(induct v arbitrary:f rule:size'.induct)
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(erule meta_allE)
+apply(erule meta_mp)
+apply(simp add:cons_ML_def size'_lift_ML split:nat.split)
+done
 
 lemma [simp]: "size' (lift i v) = size' v"
-by (rule unproven)
+apply(induct v arbitrary:i rule:size'.induct)
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply(simp add:map_compose[symmetric])
+apply(rule arg_cong[where f = listsum])
+apply(rule map_ext)
+apply simp
+apply simp
+apply simp
+apply simp
+apply simp
+done
 
 (* the kernel function as in Section 4.1 of "Operational aspects\<dots>" *)
 
@@ -534,22 +605,47 @@
 apply simp
 done
 
-(*
-lemma subst_ML_compose:
-  "subst_ml_ML f2 (subst_ml_ML f1 v) = subst_ml_ML (%i. subst_ml_ML f2 (f1 i)) v"
-by (rule unproven)
-*)
-
 lemma map_eq_iff_nth:
  "(map f xs = map g xs) = (!i<size xs. f(xs!i) = g(xs!i))"
-by (rule unproven)
+by(simp add:list_eq_iff_nth_eq)
+
+lemma ML_closed_lift_ML[simp]:
+  includes Vars shows "ML_closed_t k t \<Longrightarrow> lift\<^bsub>ML\<^esub> k t = t"
+  and  "ML_closed k v \<Longrightarrow> lift\<^bsub>ML\<^esub> k v = v"
+apply (induct k t and k v rule: lift_tm_ML_lift_ml_ML.induct)
+apply (simp_all add:list_eq_iff_nth_eq)
+done
 
-lemma [simp]: includes Vars shows "ML_closed k v \<Longrightarrow> lift\<^bsub>ML\<^esub> k v = v"
-by (rule unproven)
-lemma [simp]: includes Vars shows "ML_closed 0 v \<Longrightarrow> subst\<^bsub>ML\<^esub> f v = v"
-by (rule unproven)
-lemma [simp]: includes Vars shows "ML_closed k v \<Longrightarrow> ML_closed k (lift m v)"
-by (rule unproven)
+lemma ML_closed_subst_ML[simp]:
+  includes Vars shows "ML_closed k v \<Longrightarrow> !i<k. f i = V_ML i \<Longrightarrow> subst\<^bsub>ML\<^esub> f v = v"
+  and  "ML_closed_t k t \<Longrightarrow> !i<k. f i = V_ML i \<Longrightarrow> subst\<^bsub>ML\<^esub> f t = t"
+apply (induct f v and f t arbitrary: k and k rule: subst_ml_ML_subst_tm_ML.induct)
+apply    (auto simp add: list_eq_iff_nth_eq)
+apply(simp add:Ball_def)
+apply(erule_tac x="vs!i" in meta_allE)
+apply(erule_tac x="k" in meta_allE)
+apply simp
+apply(erule_tac x="vs!i" in meta_allE)
+apply(erule_tac x="k" in meta_allE)
+apply simp
+apply(erule_tac x="vs!i" in meta_allE)
+apply(erule_tac x="k" in meta_allE)
+apply(erule_tac x="k" in meta_allE)
+apply simp
+apply(erule_tac x="vs!i" in meta_allE)
+apply(erule_tac x="k" in meta_allE)
+apply(erule_tac x="k" in meta_allE)
+apply simp
+apply(erule_tac x="Suc k" in meta_allE)
+apply (simp add:cons_ML_def split:nat.split)
+done
+
+lemma ML_closed_lift[simp]:
+  includes Vars shows "ML_closed_t k t \<Longrightarrow> ML_closed_t k (lift m t)"
+  and "ML_closed k v \<Longrightarrow> ML_closed k (lift m v)"
+apply(induct k t and k v arbitrary: m and m rule: lift_tm_ML_lift_ml_ML.induct)
+apply (simp_all add:list_eq_iff_nth_eq)
+done
 
 lemma red_Lam[simp]: includes Vars shows "t \<rightarrow>* t' ==> Lam t \<rightarrow>* Lam t'"
 apply(induct rule:rtrancl_induct)
@@ -628,7 +724,8 @@
 apply (simp add:cons_def split:nat.split)
 done
 
-lemma [simp]: "lift k (foldl At s ts) = foldl At (lift k s) (map (lift k) ts)"
+lemma lift_foldl_At[simp]:
+  "lift k (foldl At s ts) = foldl At (lift k s) (map (lift k) ts)"
 by(induct ts arbitrary:s) simp_all
 
 subsection "Horrible detour"
@@ -693,10 +790,6 @@
 
 text{* End of horrible detour *}
 
-lemma kernel_subst1:
-"ML_closed 1 u \<Longrightarrow> ML_closed 0 v \<Longrightarrow> kernel( u[v/0]) = (kernel((lift 0 u)[V 0 []/0]))[kernel v/0]"
-by (rule unproven)
-
 lemma includes Vars shows foldl_Pure[simp]:
  "t : Pure_tms \<Longrightarrow> \<forall>t\<in>set ts. t : Pure_tms \<Longrightarrow> 
  (!!s t. s : Pure_tms \<Longrightarrow> t : Pure_tms \<Longrightarrow> f s t : Pure_tms) \<Longrightarrow>
@@ -705,23 +798,381 @@
 
 declare Pure_tms.intros[simp]
 
-lemma includes Vars shows "ML_closed 0 v \<Longrightarrow> kernel v : Pure_tms"
-apply(induct rule:kernel.induct)
+lemma "ML_closed_t n t \<Longrightarrow> ML_closed_t (Suc n) (lift\<^bsub>ML\<^esub> k t)" and
+  ML_closed_Suc: "ML_closed n v \<Longrightarrow> ML_closed (Suc n) (lift\<^bsub>ML\<^esub> k v)"
+by (induct k t and k v arbitrary: n and n rule: lift_tm_ML_lift_ml_ML.induct)
+   simp_all
+
+lemma subst_ML_coincidence:
+  "ML_closed k v \<Longrightarrow> !i<k. f i = g i \<Longrightarrow> subst\<^bsub>ML\<^esub> f v = subst\<^bsub>ML\<^esub> g v" and
+  "ML_closed_t k t \<Longrightarrow> !i<k. f i = g i \<Longrightarrow> subst\<^bsub>ML\<^esub> f t = subst\<^bsub>ML\<^esub> g t"
+apply (induct f v and f t arbitrary: k g and k g rule: subst_ml_ML_subst_tm_ML.induct)
+apply (auto simp:cons_ML_def split:nat.split)
+done
+
+
+lemma ML_closed_subst_ML1:
+  "!i. ML_closed k (f i) \<Longrightarrow> ML_closed k (subst\<^bsub>ML\<^esub> f v)" and
+  "!i. ML_closed k (f i) \<Longrightarrow> ML_closed_t k (subst\<^bsub>ML\<^esub> f t)"
+apply (induct f v and f t arbitrary: k and k rule: subst_ml_ML_subst_tm_ML.induct)
+apply (auto simp:cons_ML_def ML_closed_Suc split:nat.split)
+done
+
+lemma ML_closed_t_foldl_At:
+  "ML_closed_t k (foldl At t ts) \<longleftrightarrow>
+   ML_closed_t k t & (ALL t:set ts. ML_closed_t k t)"
+by(induct ts arbitrary: t) simp_all
+
+lemma subst_Vt: "t : Pure_tms \<Longrightarrow> subst Vt t = t"
+apply(induct set:Pure_tms)
 apply simp_all
-apply(rule Pure_tms.intros);
-(* "ML_closed (Suc k) v \<Longrightarrow> ML_closed k (lift 0 v)" *)
-by (rule unproven)
+apply(subgoal_tac "Vt 0 ## Vt = Vt")
+apply simp
+apply(rule ext)
+apply(simp add:cons_def split:nat.split)
+done
+
+lemma ML_closed_Pure_tms: "ML_closed 0 v \<Longrightarrow> v! : Pure_tms"
+apply(induct v rule:kernel.induct)
+apply auto
+apply(rule Pure_tms.intros)
+apply(erule meta_mp)
+apply(subgoal_tac "ML_closed (Suc 0) (lift 0 v)")
+apply(subgoal_tac "ML_closed 0 (subst\<^bsub>ML\<^esub> (\<lambda>n. V 0 []) (lift 0 v))")
+apply(drule subst_ML_coincidence[of _ _ "\<lambda>n. V 0 []" "\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)"])back
+apply simp
+apply metis
+apply simp
+apply(rule ML_closed_subst_ML1)
+apply simp+
+done
+
+corollary subst_Vt_kernel: "ML_closed 0 v \<Longrightarrow> subst Vt (v!) = v!"
+by (metis ML_closed_Pure_tms subst_Vt)
+
+lemma ML_closed_subst_ML3:
+    "ML_closed k v \<Longrightarrow> !i<k. ML_closed l (f i) \<Longrightarrow> ML_closed l (subst\<^bsub>ML\<^esub> f v)"
+and "ML_closed_t k t \<Longrightarrow> !i<k. ML_closed l (f i) \<Longrightarrow> ML_closed_t l (subst\<^bsub>ML\<^esub> f t)"
+apply (induct f v and f t arbitrary: k l and k l rule: subst_ml_ML_subst_tm_ML.induct)
+apply (auto simp:cons_ML_def ML_closed_Suc split:nat.split)
+done
+
+
+lemma kernel_lift_tm: "ML_closed 0 v \<Longrightarrow> (lift i v)! = lift i (v!)"
+apply(induct v arbitrary: i rule: kernel.induct)
+apply (simp_all add:list_eq_iff_nth_eq)
+apply(erule_tac x="Suc i" in meta_allE)
+apply(erule meta_impE)
+defer
+apply (simp add:lift_subst_ML)
+apply(subgoal_tac "lift (Suc i) \<circ> (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)) = (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1))")
+apply (simp add:lift_lift(2))
+apply(rule ext)
+apply(simp)
+apply(subst ML_closed_subst_ML3[of "1"])
+apply(simp)
+apply(simp)
+apply(simp)
+done
+
+(*
+lemma kernel_subst1_lem:
+assumes cl: "ML_closed 0 v"
+shows "ML_closed (Suc k) u \<Longrightarrow> f k = v \<Longrightarrow> (!i<k. f i = (C nm [])) \<Longrightarrow> 
+       g k = V k [] \<Longrightarrow> (! i<k. g i = (C nm [])) \<Longrightarrow>
+       kernel(subst\<^bsub>ML\<^esub> f u) = (kernel(subst\<^bsub>ML\<^esub> g (lift k u)))[kernel v/k]"
+apply(induct v arbitrary: i rule: kernel.induct)
+*)
+
+lemma subst_ML_comp: includes Vars shows
+  "!i. h i = subst\<^bsub>ML\<^esub> f (g i) \<Longrightarrow> subst\<^bsub>ML\<^esub> f (subst\<^bsub>ML\<^esub> g v) = subst\<^bsub>ML\<^esub> h v"
+and  "!i. h i = subst\<^bsub>ML\<^esub> f (g i) \<Longrightarrow> subst\<^bsub>ML\<^esub> f (subst\<^bsub>ML\<^esub> g t) = subst\<^bsub>ML\<^esub> h t"
+apply (induct h v and h t arbitrary: f g and f g rule: subst_ml_ML_subst_tm_ML.induct)
+apply (simp)
+apply (simp)
+defer
+apply (simp)
+apply (simp)
+apply (simp add: list_eq_iff_nth_eq)
+apply (simp add: list_eq_iff_nth_eq)
+apply (simp add: list_eq_iff_nth_eq)
+apply (simp)
+apply (simp)
+apply (simp add: list_eq_iff_nth_eq)
+defer
+apply (simp)
+apply(simp)
+apply(erule meta_allE)+
+apply(erule meta_mp)
+apply(simp)
+apply (metis lift_subst_ML(2) subst_ml_ML.simps(5))
+apply(simp)
+apply(erule meta_allE)+
+apply(erule meta_mp)
+apply(auto simp:cons_ML_def split:nat.split)
+apply (metis cons_ML_def o_apply subst_cons_lift)
+done
+
+lemma if_cong0: "If x y z = If x y z"
+by simp
+
+corollary [simp]: "ML_closed 0 v \<Longrightarrow> subst\<^bsub>ML\<^esub> f v = v"
+using ML_closed_subst_ML(1)[where k=0] by simp
+
+fun subst_ml :: "(nat \<Rightarrow> nat) \<Rightarrow> ml \<Rightarrow> ml" where
+"subst_ml f (C nm vs) = C nm (map (subst_ml f) vs)" |
+"subst_ml f (V x vs) = V (f x) (map (subst_ml f) vs)" |
+"subst_ml f (Fun v vs n) = Fun (subst_ml f v) (map (subst_ml f) vs) n" |
+"subst_ml f (apply u v) = apply (subst_ml f u) (subst_ml f v)" |
+"subst_ml f (V_ML X) = V_ML X" |
+"subst_ml f (A_ML v vs) = A_ML (subst_ml f v) (map (subst_ml f) vs)" |
+"subst_ml f (Lam_ML v) = Lam_ML (subst_ml f v)" |
+"subst_ml f (CC nm) = CC nm"
+
+lemma lift_ML_subst_ml:
+"lift\<^bsub>ML\<^esub> k (subst_ml f v) = subst_ml f (lift\<^bsub>ML\<^esub> k v)"
+apply (induct f v arbitrary: k rule:subst_ml.induct)
+apply (simp_all add:list_eq_iff_nth_eq)
+done
+
+
+(* FIXME Only ml version needed!!! *)
+lemma subst_ml_subst_ML: includes Vars shows
+  "subst_ml f (subst\<^bsub>ML\<^esub> g v) = subst\<^bsub>ML\<^esub> (subst_ml f o g) (subst_ml f v)"
+and "True"
+apply (induct g v and g "t::tm" arbitrary: f  rule: subst_ml_ML_subst_tm_ML.induct)
+apply(simp_all add:list_eq_iff_nth_eq)
+apply(subgoal_tac "(subst_ml fa \<circ> V_ML 0 ## f) = V_ML 0 ## (subst_ml fa \<circ> f)")
+apply simp
+apply(rule ext)
+apply(simp add:cons_ML_def lift_ML_subst_ml split:nat.split)
+done
+
+lemma lift_Pure_tms[simp]: "t : Pure_tms \<Longrightarrow> lift k t : Pure_tms"
+by(induct arbitrary:k set:Pure_tms) simp_all
+
+lemma lift_subst_aux:
+  "t : Pure_tms \<Longrightarrow> !i<k. g i = lift k (f i) \<Longrightarrow>
+   ALL i>= k. g(Suc i) = lift k (f i) \<Longrightarrow> 
+  g k = Vt k \<Longrightarrow> lift k (subst f t) = subst g (lift k t)"
+apply(induct arbitrary:f g k set:Pure_tms)
+apply (simp_all add: split:nat.split)
+apply(erule meta_allE)+
+apply(erule meta_impE)
+defer
+apply(erule meta_impE)
+defer
+apply(erule meta_mp)
+apply (simp_all add: cons_def lift_lift split:nat.split)
+done
+
+corollary lift_subst:
+  "t : Pure_tms \<Longrightarrow> lift 0 (subst f t) = subst (Vt 0 ## f) (lift 0 t)"
+by (simp add: lift_subst_aux cons_def lift_lift split:nat.split)
 
-lemma subst_Vt: includes Vars shows "subst Vt = id"
-by (rule unproven)
-(*
+lemma subst_comp: includes Vars shows
+  "t : Pure_tms \<Longrightarrow> !i. g i : Pure_tms \<Longrightarrow>
+   h = (%i. subst f (g i)) \<Longrightarrow> subst f (subst g t) = subst h t"
+apply(induct arbitrary:f g h set:Pure_tms)
+apply simp
+apply simp
+defer
+apply simp
+apply (simp (no_asm))
+apply(erule meta_allE)+
+apply(erule meta_impE)
+defer
+apply(erule meta_mp)
+prefer 2 apply (simp add:cons_def split:nat.split)
+apply(rule ext)
+apply(subst (1) cons_def)
+apply(subst (2) cons_def)
+apply(simp split:nat.split)
+apply rule apply (simp add:cons_def)
+apply(simp add:lift_subst)
+done
+
+lemma lift_is_subst_ml:"lift k v = subst_ml (%n. if n<k then n else n+1) v"
+apply(induct v arbitrary: k rule:subst_ml.induct[of "%f v. Q v", standard])
+apply (simp_all add:list_eq_iff_nth_eq)
+done
+
+lemma subst_ml_comp:
+ "subst_ml f (subst_ml g v) = subst_ml (f o g) v"
+apply(induct v rule:subst_ml.induct[of "%f v. Q v", standard])
+apply (simp_all add:list_eq_iff_nth_eq)
+done
+
+
+lemma subst_kernel:
+  "ML_closed 0 v \<Longrightarrow>  subst (%n. Vt (f n)) (v!) = (subst_ml f v)!"
+apply (induct v arbitrary: f rule:kernel.induct)
+apply (simp_all add:list_eq_iff_nth_eq)
+apply(erule_tac x="%n. case n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> Suc(f k)" in meta_allE)
+apply(erule_tac meta_impE)
+defer
+apply(subgoal_tac "(\<lambda>n. Vt (case n of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> Suc (f k))) = (Vt 0 ## (\<lambda>n. Vt (f n)))")
+apply (simp add:subst_ml_subst_ML)
+defer
 apply(rule ext)
-apply(induct_tac x)
-apply simp_all
+apply(simp add:cons_def split:nat.split)
+apply(simp add:cons_def)
+defer
+apply(simp add:lift_is_subst_ml subst_ml_comp)
+apply(rule arg_cong[where f = kernel])
+apply(subgoal_tac "(nat_case 0 (\<lambda>k. Suc (f k)) \<circ> Suc) = Suc o f")
+prefer 2
+apply(rule ext)apply(simp split:nat.split)
+apply simp
+apply(subgoal_tac "(subst_ml (nat_case 0 (\<lambda>k. Suc (f k))) \<circ>
+               (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)))
+             = (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1))")
+apply simp
+apply(rule ext)apply(simp split:nat.split)
+apply(rule ML_closed_subst_ML3[where k="Suc 0"])
+apply (metis ML_closed_lift(2))
+apply simp
+done
 
-done
-*)
-(* klappt noch nicht ganz *)
+lemma kernel_subst1:
+  "ML_closed 0 v \<Longrightarrow> ML_closed (Suc 0) u \<Longrightarrow>
+   kernel(u[v/0]) = (kernel((lift 0 u)[V 0 []/0]))[v!/0]"
+proof(induct u arbitrary:v rule:kernel.induct)
+  case (2 w)
+  show ?case (is "?L = ?R")
+  proof -
+    have "?L = Lam (lift 0 (w[lift\<^bsub>ML\<^esub> 0 v/Suc 0])[V 0 []/0]!)"
+      by (simp cong:if_cong0)
+    also have "\<dots> = Lam ((lift 0 w)[lift\<^bsub>ML\<^esub> 0 (lift 0 v)/Suc 0][V 0 []/0]!)"
+      by (metis kernel.simps(2) lift_lift_ML_comm(2) lift_subst_ML1)
+    also have "\<dots> = Lam (subst\<^bsub>ML\<^esub> (%n. if n=0 then V 0 [] else
+            if n=Suc 0 then lift 0 v else V_ML (n - 2)) (lift 0 w) !)"
+      apply simp
+      apply(rule arg_cong[where f = kernel])
+      apply(rule subst_ML_comp)
+      using 2
+      apply auto
+      done
+    also have "\<dots> = Lam ((lift 0 w)[V 0 []/0][lift 0 v/0]!)"
+      apply simp
+      apply(rule arg_cong[where f = kernel])
+      apply(rule subst_ML_comp[symmetric])
+      using 2
+      apply auto
+      done
+    also have "\<dots> = Lam ((lift_ml 0 ((lift_ml 0 w)[V 0 []/0]))[V 0 []/0]![(lift 0 v)!/0])"
+      apply(rule arg_cong[where f = Lam])
+      apply(rule 2(1))
+      apply (metis ML_closed_lift(2) 2)
+      apply(subgoal_tac "ML_closed (Suc(Suc 0)) w")
+      defer
+      using 2
+      apply force
+      apply(subgoal_tac  "ML_closed (Suc (Suc 0)) (lift 0 w)")
+      defer
+      apply(erule ML_closed_lift)
+      apply(erule ML_closed_subst_ML3)
+      apply simp
+      done
+    also have "\<dots> = Lam ((lift_ml 0 (lift_ml 0 w)[V 1 []/0])[V 0 []/0]![(lift 0 v)!/0])" (is "_ = ?M")
+      apply(subgoal_tac "lift_ml 0 (lift_ml 0 w[V 0 []/0])[V 0 []/0] =
+                         lift_ml 0 (lift_ml 0 w)[V 1 []/0][V 0 []/0]")
+      apply simp
+      apply(subst lift_subst_ML(2))
+      apply(simp add:comp_def if_distrib[where f="lift_ml 0"] cong:if_cong)
+      done
+    finally have "?L = ?M" .
+    have "?R = Lam (subst (Vt 0 ## subst_decr 0 (v!))
+          (lift 0 (lift_ml 0 w[V 0 []/Suc 0])[V 0 []/0]!))"
+      apply(subgoal_tac "(V_ML 0 ## (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - Suc 0))) = subst_decr_ML (Suc 0) (V 0 [])")
+      apply(simp cong:if_cong)
+      apply(simp add:expand_fun_eq cons_ML_def split:nat.splits)
+      done
+    also have "\<dots> = Lam (subst (Vt 0 ## subst_decr 0 (v!))
+          ((lift 0 (lift_ml 0 w))[V 1 []/Suc 0][V 0 []/0]!))"
+      apply(subgoal_tac "lift 0 (lift 0 w[V 0 []/Suc 0]) = lift 0 (lift 0 w)[V 1 []/Suc 0]")
+      apply simp
+      apply(subst lift_subst_ML(2))
+      apply(simp add:comp_def if_distrib[where f="lift_ml 0"] cong:if_cong)
+      done
+    also have "(lift_ml 0 (lift_ml 0 w))[V 1 []/Suc 0][V 0 []/0] =
+               (lift 0 (lift_ml 0 w))[V 0 []/0][V 1 []/ 0]" (is "?l = ?r")
+    proof -
+      have "?l = subst\<^bsub>ML\<^esub> (%n. if n= 0 then V 0 [] else if n = 1 then V 1 [] else
+                      V_ML (n - 2))
+               (lift_ml 0 (lift_ml 0 w))"
+      by(auto intro!:subst_ML_comp)
+    also have "\<dots> = ?r" by(auto intro!:subst_ML_comp[symmetric])
+    finally show ?thesis .
+  qed
+  also have "Lam (subst (Vt 0 ## subst_decr 0 (v!)) (?r !)) = ?M"
+  proof-
+    have "subst (subst_decr (Suc 0) (lift_tm 0 (kernel v))) (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]!) =
+    subst (subst_decr 0 (kernel(lift_ml 0 v))) (lift_ml 0 (lift_ml 0 w)[V 1 []/0][V 0 []/0]!)" (is "?a = ?b")
+    proof-
+      def pi == "%n::nat. if n = 0 then 1 else if n = 1 then 0 else n"
+      have "(\<lambda>i. Vt (pi i)[lift 0 (v!)/0]) = subst_decr (Suc 0) (lift 0 (v!))"
+	by(rule ext)(simp add:pi_def)
+      hence "?a =
+  subst (subst_decr 0 (lift_tm 0 (kernel v))) (subst (% n. Vt (pi n)) (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]!))"
+	apply(subst subst_comp[OF _ _ refl])
+	prefer 3 apply simp
+	using 2(3)
+	apply simp
+	apply(rule ML_closed_Pure_tms)
+	apply(rule ML_closed_subst_ML3[where k="Suc 0"])
+	apply(rule ML_closed_subst_ML3[where k="Suc(Suc 0)"])
+	apply simp
+	apply simp
+	apply simp
+	apply simp
+	done
+      also have "\<dots> =
+ (subst_ml pi (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]))![lift_tm 0 (v!)/0]"
+	apply(subst subst_kernel)
+	using 2 apply auto
+	apply(rule ML_closed_subst_ML3[where k="Suc 0"])
+	apply(rule ML_closed_subst_ML3[where k="Suc(Suc 0)"])
+	apply simp
+	apply simp
+	apply simp
+	done
+      also have "\<dots> = (subst_ml pi (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]))![lift 0 v!/0]"
+      proof -
+	have "lift 0 (v!) = lift 0 v!" by (metis 2(2) kernel_lift_tm)
+	thus ?thesis by (simp cong:if_cong)
+      qed
+      also have "\<dots> = ?b"
+      proof-
+	have 1: "subst_ml pi (lift 0 (lift 0 w)) = lift 0 (lift 0 w)"
+	  apply(simp add:lift_is_subst_ml subst_ml_comp)
+	  apply(subgoal_tac "pi \<circ> (Suc \<circ> Suc) = (Suc \<circ> Suc)")
+	  apply(simp)
+	  apply(simp add:pi_def expand_fun_eq)
+	  done
+	have "subst_ml pi (lift_ml 0 (lift_ml 0 w)[V 0 []/0][V 1 []/0]) =
+             lift_ml 0 (lift_ml 0 w)[V 1 []/0][V 0 []/0]"
+	  apply(subst subst_ml_subst_ML)
+	  apply(subst subst_ml_subst_ML)
+	  apply(subst 1)
+	  apply(subst subst_ML_comp)
+	  apply(rule)
+	  apply(rule)
+	  apply(rule subst_ML_comp[symmetric])
+	  apply(auto simp:pi_def)
+	  done
+	thus ?thesis by simp
+      qed
+      finally show ?thesis .
+    qed
+    thus ?thesis by(simp cong:if_cong0 add:shift_subst_decr)
+  qed
+  finally have "?R = ?M" .
+  then show "?L = ?R" using `?L = ?M` by metis
+qed
+qed (simp_all add:list_eq_iff_nth_eq)
+
+
 theorem Red_sound: includes Vars
  shows "v \<Rightarrow> v' \<Longrightarrow> ML_closed 0 v \<Longrightarrow> v! \<rightarrow>* v'! & ML_closed 0 v'"
     and "t \<Rightarrow> t' \<Longrightarrow> ML_closed_t 0 t \<Longrightarrow> kernelt t \<rightarrow>* kernelt t'  & ML_closed_t 0 t'"
@@ -734,44 +1185,58 @@
   have "?v! = At (Lam ((?u')!)) (v !)" by simp
   also have "\<dots> \<rightarrow> (?u' !)[v!/0]" (is "_ \<rightarrow> ?R") by(rule tRed.intros)
   also have "?R = u[v/0]!" using cl
-apply(cut_tac u = "u" and v = "v" in kernel_subst1)
-apply(simp_all)
-done
+    apply(cut_tac u = "u" and v = "v" in kernel_subst1)
+    apply(simp_all)
+    done
   finally have "kernel(A_ML (Lam_ML u) [v]) \<rightarrow>* kernel(u[v/0])" (is ?A) by(rule r_into_rtrancl)
-  moreover have "ML_closed 0 (u[v/0])" (is "?C") using cl apply simp by (rule unproven)
+  moreover have "ML_closed 0 (u[v/0])" (is "?C")
+  proof -
+    let ?f = "\<lambda>n. if n = 0 then v else V_ML (n - 1)"
+    let ?g = "\<lambda>n. v"
+    have clu: "ML_closed (Suc 0) u" and clv: "ML_closed 0 v" using cl by simp+
+    have "ML_closed 0 (subst\<^bsub>ML\<^esub> ?g u)"
+      by (metis COMBK_def ML_closed_subst_ML1 clv)
+    hence "ML_closed 0 (subst\<^bsub>ML\<^esub> ?f u)"
+      using subst_ML_coincidence[OF clu, of ?f ?g] by auto
+    thus ?thesis by simp
+  qed
   ultimately show "?A & ?C" ..
 next
-  case term_of_C thus ?case apply (auto simp:map_compose[symmetric])by (rule unproven)
+  case term_of_C thus ?case
+    by (auto simp:ML_closed_t_foldl_At map_compose[symmetric])
 next
   fix f :: "nat \<Rightarrow> ml" and nm vs v
   assume f: "\<forall>i. ML_closed 0 (f i)"  and compR: "(nm, vs, v) \<in> compR"
-  note tRed.intros(2)[OF compiler_correct[OF compR f], of Vt,simplified map_compose[symmetric]]
-  hence red: "foldl At (Ct nm) (map (kernel o subst\<^bsub>ML\<^esub> f) vs) \<rightarrow>
-         (subst\<^bsub>ML\<^esub> f v)!" (is "_ \<rightarrow> ?R") apply(simp add:map_compose) by (rule unproven)
-  have "A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)! =
-       foldl At (Ct nm) (map (kernel o subst\<^bsub>ML\<^esub> f) vs)" by (simp add:map_compose)
-  also(* have "map (kernel o subst\<^bsub>ML\<^esub> f) vs = map (subst (kernel o f)) (vs!)"
-    using closed_subst_kernel(2)[OF compiled_V_free1[OF compR]]
-    by (simp add:map_compose[symmetric])
-  also*) note red
-  (*also have "?R = subst\<^bsub>ML\<^esub> f v!"
-    using closed_subst_kernel(2)[OF compiled_V_free2[OF compR]] by simp*)
-  finally have "A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)! \<rightarrow>* subst\<^bsub>ML\<^esub> f v!" (is "?A")
-    by(rule r_into_rtrancl) (*
-  also have "?l = (subst\<^bsub>ML\<^esub> fa (A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)))!" (is "_ = ?l'") by (rule unproven)
-  also have "?r = subst\<^bsub>ML\<^esub> fa (subst\<^bsub>ML\<^esub> f v)!"  (is "_ = ?r'") by (rule unproven) 
-  finally have "?l' \<rightarrow>* ?r'" (is ?A) . *)
-  moreover have "ML_closed 0 (subst\<^bsub>ML\<^esub> f v)" (is "?C") by (rule unproven)
+  have "map (subst Vt) (map (subst\<^bsub>ML\<^esub> f) vs!) = map (subst\<^bsub>ML\<^esub> f) vs!"
+    by(simp add:list_eq_iff_nth_eq subst_Vt_kernel ML_closed_subst_ML1[OF f])
+  with tRed.intros(3)[OF compiler_correct[OF compR f], of Vt,simplified map_compose]
+  have red: "foldl At (Ct nm) ((map (subst\<^bsub>ML\<^esub> f) vs) !) \<rightarrow>
+        (subst\<^bsub>ML\<^esub> f v)!" (is "_ \<rightarrow> ?R")
+    by(simp add:subst_Vt_kernel ML_closed_subst_ML1[OF f])
+  hence "A_ML (CC nm) (map (subst\<^bsub>ML\<^esub> f) vs)! \<rightarrow>* subst\<^bsub>ML\<^esub> f v!" (is ?A) by simp
+  moreover
+  have "ML_closed 0 (subst\<^bsub>ML\<^esub> f v)" (is ?C) by(metis ML_closed_subst_ML1 f)
   ultimately show "?A & ?C" ..
 next
-  case term_of_V thus ?case apply (auto simp:map_compose[symmetric]) by (rule unproven)
+  case term_of_V thus ?case
+    by (auto simp:map_compose[symmetric]ML_closed_t_foldl_At)
 next
   case (term_of_Fun vf vs n)
+  hence "foldl At (lift 0 vf!)
+              (map (subst\<^bsub>ML\<^esub> (\<lambda>n. if n = 0 then V 0 [] else V_ML (n - 1)))
+                (map (lift 0) vs)!)
+         = lift 0 (foldl At (vf!) (map kernel vs))"
+    by (simp add:kernel_lift_tm list_eq_iff_nth_eq)
   hence "term_of (Fun vf vs n)! \<rightarrow>*
-       Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0]))!" by - (rule unproven)
+       Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0]))!"
+    using term_of_Fun
+    apply (simp del:lift_foldl_At)
+    apply (metis kernel.simps r_into_rtrancl tRed.intros(2))
+    done
   moreover
   have "ML_closed_t 0
-        (Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0])))" by (rule unproven)
+        (Lam (term_of (apply (lift 0 (Fun vf vs n)) (V_ML 0)[V 0 []/0])))"
+    using term_of_Fun by simp
   ultimately show ?case ..
 next
   case apply_Fun1 thus ?case by simp
@@ -812,22 +1277,44 @@
 qed
 
 
-inductive_cases tRedE: "Ct n \<rightarrow> u"
-thm tRedE
-
 lemma [simp]: "Ct n = foldl At t ts \<longleftrightarrow> t = Ct n & ts = []"
 by (induct ts arbitrary:t) auto
 
 corollary kernel_inv: includes Vars shows
- "(t :: tm) \<Rightarrow>* t' ==> ML_closed_t 0 t ==> t! \<rightarrow>* t'!"
-by (rule unproven)
+ "(t :: tm) \<Rightarrow>* t' ==> ML_closed_t 0 t ==> t! \<rightarrow>* t'! \<and> ML_closed_t 0 t' "
+apply(induct rule: rtrancl.induct)
+apply (metis rtrancl_eq_or_trancl)
+apply (metis Red_sound rtrancl_trans)
+done
+
+lemma  ML_closed_t_term_of_eval:
+ "t : Pure_tms \<Longrightarrow> ALL i : free_vars t. i < size e \<Longrightarrow>
+ !i<length e. ML_closed n (e!i) \<Longrightarrow> ML_closed_t n (term_of (eval t e))"
+apply(induct arbitrary:n e rule: Pure_tms.induct)
+apply simp
+apply simp
+apply simp
+prefer 2 apply simp
+apply(erule_tac x="Suc n" in meta_allE)
+apply(erule_tac x="V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e" in meta_allE)
+apply(subgoal_tac "\<forall>i\<in>free_vars t. i < length (V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e)")
+prefer 2
+apply simp
+apply (metis Nat.less_trans gr0_implies_Suc gr_implies_not0 linorder_neq_iff not_less_eq)
+apply(subgoal_tac " \<forall>i<length (V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e).
+            ML_closed (Suc n) ((V_ML 0 # map (lift\<^bsub>ML\<^esub> 0) e) ! i)")
+apply (auto simp:nth_Cons')
+apply (metis ML_closed_Suc Nat.less_trans Suc_eq_add_numeral_1 Suc_pred' add_0_left less_add_Suc2 less_antisym)
+done
 
 theorem includes Vars
 assumes t: "t : Pure_tms" and t': "t' : Pure_tms" and
- closed: "free_vars t = {}" and reds: "term_of (eval t []) \<Rightarrow>* t'"
- shows "t \<rightarrow>* t' "
+closed: "free_vars t = {}" and reds: "term_of (eval t []) \<Rightarrow>* t'"
+shows "t \<rightarrow>* t'"
 proof -
-  have ML_cl: "ML_closed_t 0 (term_of (eval t []))" by (rule unproven)
+  have ML_cl: "ML_closed_t 0 (term_of (eval t []))"
+    apply(rule ML_closed_t_term_of_eval[OF t])
+    using closed apply auto done
   have "(eval t [])! = t!"
     using kernel_eval[OF t, where e="[]"] closed by simp
   hence "(term_of (eval t []))! = t!" by simp