Theory NBE

(*  Author:     Klaus Aehlig, Tobias Nipkow

Normalization by Evaluation.
*)
(*<*)
theory NBE imports Main begin

declare [[syntax_ambiguity_warning = false]]

declare Let_def[simp]
(*>*)
section "Terms"

type_synonym vname = nat
type_synonym ml_vname = nat

(* FIXME only for codegen*)
type_synonym cname = int

text‹ML terms:›

datatype ml =
 ― ‹ML›
  C_ML cname (CML) (* ref to compiled code *)
| V_ML ml_vname (VML)
| A_ML ml "(ml list)" (AML)
| Lam_ML ml (LamML)
 ― ‹the universal datatype›
| CU cname "(ml list)"
| VU vname "(ml list)"
| Clo ml "(ml list)" nat
 ― ‹ML function \emph{apply}›
| "apply" ml ml

text‹Lambda-terms:›

datatype tm = C cname | V vname | Λ tm | At tm tm (infix  100)
            | "term" ml   ― ‹ML function \texttt{term}›

text ‹The following locale captures type conventions for variables.
  It is not actually used, merely a formal comment.›

locale Vars =
 fixes r s t:: tm
 and rs ss ts :: "tm list"
 and u v w :: ml
 and us vs ws :: "ml list"
 and nm :: cname
 and x :: vname
 and X :: ml_vname

text‹The subset of pure terms:›

inductive pure :: "tm  bool" where
"pure(C nm)" |
"pure(V x)" |
Lam: "pure t  pure(Λ t)" |
"pure s  pure t  pure(st)"

declare pure.intros[simp]
declare Lam[simp del]

lemma pure_Lam[simp]: "pure(Λ t) = pure t"
proof
  assume "pure(Λ t)" thus "pure t"
  proof cases qed auto
next
  assume "pure t" thus "pure(Λ t)" by(rule Lam)
qed

text‹Closed terms w.r.t.\ ML variables:›

fun closed_ML :: "nat  ml  bool" (closedML) where
"closedML i (CML nm) = True" |
"closedML i (VML X) = (X<i)"  |
"closedML i (AML v vs) = (closedML i v  (v  set vs. closedML i v))" |
"closedML i (LamML v) = closedML (i+1) v" |
"closedML i (CU nm vs) = (v  set vs. closedML i v)" |
"closedML i (VU nm vs) = (v  set vs. closedML i v)" |
"closedML i (Clo f vs n) = (closedML i f  (v  set vs. closedML i v))" |
"closedML i (apply v w) = (closedML i v  closedML i w)"

fun closed_tm_ML :: "nat  tm  bool" (closedML) where
"closed_tm_ML i (rs) = (closed_tm_ML i r  closed_tm_ML i s)" |
"closed_tm_ML i (Λ t) = (closed_tm_ML i t)" |
"closed_tm_ML i (term v) = closed_ML i v" |
"closed_tm_ML i v = True"

text‹Free variables:›

fun fv_ML :: "ml  ml_vname set" (fvML) where
"fvML (CML nm) = {}" |
"fvML (VML X) = {X}"  |
"fvML (AML v vs) = fvML v  (v  set vs. fvML v)" |
"fvML (LamML v) = {X. Suc X : fvML v}" |
"fvML (CU nm vs) = (v  set vs. fvML v)" |
"fvML (VU nm vs) = (v  set vs. fvML v)" |
"fvML (Clo f vs n) = fvML f  (v  set vs. fvML v)" |
"fvML (apply v w) = fvML v  fvML w"

primrec fv :: "tm  vname set" where
"fv (C nm) = {}" |
"fv (V X) = {X}"  |
"fv (s  t) = fv s  fv t" |
"fv (Λ t) = {X. Suc X : fv t}"


subsection "Iterated Term Application"

abbreviation foldl_At (infix ∙∙ 90) where
"t ∙∙ ts  foldl (∙) t ts"

text‹Auxiliary measure function:›
primrec depth_At :: "tm  nat"
where
  "depth_At(C nm) = 0"
| "depth_At(V x) = 0"
| "depth_At(s  t) = depth_At s + 1"
| "depth_At(Λ t) = 0"
| "depth_At(term v) = 0"

lemma depth_At_foldl:
 "depth_At(s ∙∙ ts) = depth_At s + size ts"
by (induct ts arbitrary: s) simp_all

lemma foldl_At_eq_lemma: "size ts = size ts' 
 s ∙∙ ts = s' ∙∙ ts'  s = s'  ts = ts'"
by (induct arbitrary: s s' rule:list_induct2) simp_all

lemma foldl_At_eq_length:
 "s ∙∙ ts = s ∙∙ ts'  length ts = length ts'"
apply(subgoal_tac "depth_At(s ∙∙ ts) = depth_At(s ∙∙ ts')")
apply(erule thin_rl)
 apply (simp add:depth_At_foldl)
apply simp
done

lemma foldl_At_eq[simp]: "s ∙∙ ts = s ∙∙ ts'  ts = ts'"
apply(rule)
 prefer 2 apply simp
apply(blast dest:foldl_At_eq_lemma foldl_At_eq_length)
done

lemma term_eq_foldl_At[simp]:
  "term v = t ∙∙ ts  t = term v  ts = []"
by (induct ts arbitrary:t) auto

lemma At_eq_foldl_At[simp]:
  "r  s = t ∙∙ ts 
  (if ts=[] then t = r  s else s = last ts  r = t ∙∙ butlast ts)"
apply (induct ts arbitrary:t)
 apply fastforce
apply rule
 apply clarsimp
 apply rule
  apply clarsimp
 apply clarsimp
 apply(subgoal_tac "ts' t'. ts = ts' @ [t']")
  apply clarsimp
 defer
 apply (clarsimp split:list.split)
apply (metis append_butlast_last_id)
done

lemma foldl_At_eq_At[simp]:
  "t ∙∙ ts = r  s 
  (if ts=[] then t = r  s else s = last ts  r = t ∙∙ butlast ts)"
by(metis At_eq_foldl_At)

lemma Lam_eq_foldl_At[simp]:
  "Λ s = t ∙∙ ts  t = Λ s  ts = []"
by (induct ts arbitrary:t) auto

lemma foldl_At_eq_Lam[simp]:
  "t ∙∙ ts = Λ s  t = Λ s  ts = []"
by (induct ts arbitrary:t) auto

lemma [simp]: "s  t  s"
apply(subgoal_tac "size(s  t)  size s")
apply metis
apply simp
done

(* Better: a simproc for disproving "s = t"
   if s is a subterm of t or vice versa, by proving "size s ~= size t"
*)

fun atomic_tm :: "tm  bool" where
"atomic_tm(s  t) = False" |
"atomic_tm(_) = True"

fun head_tm where
"head_tm(s  t) = head_tm s" |
"head_tm(s) = s"

fun args_tm where
"args_tm(s  t) = args_tm s @ [t]" |
"args_tm(_) = []"

lemma head_tm_foldl_At[simp]: "head_tm(s ∙∙ ts) = head_tm s"
by(induct ts arbitrary: s) auto

lemma args_tm_foldl_At[simp]: "args_tm(s ∙∙ ts) = args_tm s @ ts"
by(induct ts arbitrary: s) auto

lemma tm_eq_iff:
  "atomic_tm(head_tm s)  atomic_tm(head_tm t)
    s = t  head_tm s = head_tm t  args_tm s = args_tm t"
apply(induct s arbitrary: t)
apply(case_tac t, simp+)+
done

declare
  tm_eq_iff[of "h ∙∙ ts", simp]
  tm_eq_iff[of _ "h ∙∙ ts", simp]
  for h ts

lemma atomic_tm_head_tm: "atomic_tm(head_tm t)"
by(induct t) auto

lemma head_tm_idem: "head_tm(head_tm t) = head_tm t"
by(induct t) auto

lemma args_tm_head_tm: "args_tm(head_tm t) = []"
by(induct t) auto

lemma eta_head_args: "t = head_tm t ∙∙ args_tm t"
by (subst tm_eq_iff) (auto simp: atomic_tm_head_tm head_tm_idem args_tm_head_tm)


lemma tm_vector_cases:
  "(n ts. t = V n ∙∙ ts) 
   (nm ts. t = C nm ∙∙ ts) 
   (t' ts. t = Λ t' ∙∙ ts) 
   (v ts. t = term v ∙∙ ts)"
apply(induct t)
apply simp_all
by (metis snoc_eq_iff_butlast)

lemma fv_head_C[simp]: "fv (t ∙∙ ts) = fv t  (tset ts. fv t)"
by(induct ts arbitrary:t) auto


subsection "Lifting and Substitution"

fun lift_ml :: "nat  ml  ml" (lift) where
"lift i (CML nm) = CML nm" |
"lift i (VML X) = VML X" |
"lift i (AML v vs) = AML (lift i v) (map (lift i) vs)" |
"lift i (LamML v) = LamML (lift i v)" |
"lift i (CU nm vs) = CU nm (map (lift i) vs)" |
"lift i (VU x vs) = VU (if x < i then x else x+1) (map (lift i) vs)" |
"lift i (Clo v vs n) = Clo (lift i v) (map (lift i) vs) n" |
"lift i (apply u v) = apply (lift i u) (lift i v)"

lemmas ml_induct = lift_ml.induct[of "λi v. P v"] for P

fun lift_tm :: "nat  tm  tm" (lift) where
"lift i (C nm) = C nm" |
"lift i (V x) = V(if x < i then x else x+1)" |
"lift i (st) = (lift i s)(lift i t)" |
"lift i (Λ t) = Λ(lift (i+1) t)" |
"lift i (term v) = term (lift i v)"

fun lift_ML :: "nat  ml  ml" (liftML) where
"liftML i (CML nm) = CML nm" |
"liftML i (VML X) = VML (if X < i then X else X+1)" |
"liftML i (AML v vs) = AML (liftML i v) (map (liftML i) vs)" |
"liftML i (LamML v) = LamML (liftML (i+1) v)" |
"liftML i (CU nm vs) = CU nm (map (liftML i) vs)" |
"liftML i (VU x vs) = VU x (map (liftML i) vs)" |
"liftML i (Clo v vs n) = Clo (liftML i v) (map (liftML i) vs) n" |
"liftML i (apply u v) = apply (liftML i u) (liftML i v)"

definition
 cons :: "tm  (nat  tm)  (nat  tm)" (infix ## 65) where
"t##σ  λi. case i of 0  t | Suc j  lift 0 (σ j)"

definition
 cons_ML :: "ml  (nat  ml)  (nat  ml)" (infix ## 65) where
"v##σ  λi. case i of 0  v::ml | Suc j  liftML 0 (σ j)"

text‹Only for pure terms!›
primrec subst :: "(nat  tm)  tm  tm"
where
  "subst σ (C nm) = C nm"
| "subst σ (V x) = σ x"
| "subst σ (Λ t) = Λ(subst (V 0 ## σ) t)"
| "subst σ (st) = (subst σ s)  (subst σ t)"

fun subst_ML :: "(nat  ml)  ml  ml" (substML) where
"substML σ (CML nm) = CML nm" |
"substML σ (VML X) = σ X" |
"substML σ (AML v vs) = AML (substML σ v) (map (substML σ) vs)" |
"substML σ (LamML v) = LamML (substML (VML 0 ## σ) v)" |
"substML σ (CU nm vs) = CU nm (map (substML σ) vs)" |
"substML σ (VU x vs) = VU x (map (substML σ) vs)" |
"substML σ (Clo v vs n) = Clo (substML σ v) (map (substML σ) vs) n" |
"substML σ (apply u v) = apply (substML σ u) (substML σ v)"
(* FIXME currrently needed for code generator
lemmas [code] = lift_tm.simps lift_ml.simps
lemmas [code] = subst_ML.simps *)

abbreviation
  subst_decr :: "nat  tm  nat  tm" where
  "subst_decr k t  λn. if n<k then V n else if n=k then t else V(n - 1)"
abbreviation
  subst_decr_ML :: "nat  ml  nat  ml" where
"subst_decr_ML k v  λn. if n<k then VML n else if n=k then v else VML(n - 1)"
abbreviation
  subst1 :: "tm  tm  nat  tm" ((_/[_'/_]) [300, 0, 0] 300) where
 "s[t/k]  subst (subst_decr k t) s"
abbreviation
  subst1_ML :: "ml  ml  nat  ml" ((_/[_'/_]) [300, 0, 0] 300) where
 "u[v/k]  substML (subst_decr_ML k v) u"

lemma apply_cons[simp]:
  "(t##σ) i = (if i=0 then t::tm else lift 0 (σ(i - 1)))"
by(simp add: cons_def split:nat.split)

lemma apply_cons_ML[simp]:
  "(v##σ) i = (if i=0 then v::ml else liftML 0 (σ(i - 1)))"
by(simp add: cons_ML_def split:nat.split)

lemma lift_foldl_At[simp]:
  "lift k (s ∙∙ ts) = (lift k s) ∙∙ (map (lift k) ts)"
by(induct ts arbitrary:s) simp_all

lemma lift_lift_ml: fixes v :: ml shows
  "i < k+1  lift (Suc k) (lift i v) = lift i (lift k v)"
by(induct i v rule:lift_ml.induct)
  simp_all
lemma lift_lift_tm: fixes t :: tm shows
    "i < k+1  lift (Suc k) (lift i t) = lift i (lift k t)"
by(induct t arbitrary: i rule:lift_tm.induct)(simp_all add:lift_lift_ml)

lemma lift_lift_ML:
  "i < k+1  liftML (Suc k) (liftML i v) = liftML i (liftML k v)"
by(induct v arbitrary: i rule:lift_ML.induct)
  simp_all

lemma lift_lift_ML_comm:
  "lift j (liftML i v) = liftML i (lift j v)"
by(induct v arbitrary: i j rule:lift_ML.induct)
  simp_all

lemma V_ML_cons_ML_subst_decr[simp]:
  "VML 0 ## subst_decr_ML k v = subst_decr_ML (Suc k) (liftML 0 v)"
by(rule ext)(simp add:cons_ML_def split:nat.split)

lemma shift_subst_decr[simp]:
 "V 0 ## subst_decr k t = subst_decr (Suc k) (lift 0 t)"
by(rule ext)(simp add:cons_def split:nat.split)

lemma lift_comp_subst_decr[simp]:
  "lift 0 o subst_decr_ML k v = subst_decr_ML k (lift 0 v)"
by(rule ext) simp

lemma subst_ML_ext: "i. σ i = σ' i  substML σ v = substML σ' v"
by(metis ext)

lemma subst_ext: "i. σ i = σ' i  subst σ v = subst σ' v"
by(metis ext)

lemma lift_Pure_tms[simp]: "pure t  pure(lift k t)"
by(induct arbitrary:k pred:pure) simp_all

lemma cons_ML_V_ML[simp]: "(VML 0 ## VML) = VML"
by(rule ext) simp

lemma cons_V[simp]: "(V 0 ## V) = V"
by(rule ext) simp

lemma lift_o_shift: "lift k  (VML 0 ## σ) = (VML 0 ## (lift k  σ))"
by(rule ext)(simp add: lift_lift_ML_comm)

lemma lift_subst_ML:
 "lift k (substML σ v) = substML (lift k  σ) (lift k v)"
apply(induct σ v rule:subst_ML.induct)
apply(simp_all add: o_assoc lift_o_shift del:apply_cons_ML)
apply(simp add:o_def)
done

corollary lift_subst_ML1:
  "v k. lift_ml 0 (u[v/k]) = (lift_ml 0 u)[lift 0 v/k]"
apply(induct u rule:ml_induct)
apply(simp_all add:lift_lift_ml lift_subst_ML)
apply(subst lift_lift_ML_comm)apply simp
done

lemma lift_ML_subst_ML:
 "liftML k (substML σ v) =
  substML (λi. if i<k then liftML k (σ i) else if i=k then VML k else liftML k (σ(i - 1))) (liftML k v)"
  (is "_ = substML (?insrt k σ) (liftML k v)")
apply (induct k v arbitrary: σ k rule: lift_ML.induct)
apply (simp_all add: o_assoc lift_o_shift)
apply(subgoal_tac "VML 0 ## ?insrt k σ = ?insrt (Suc k) (VML 0 ## σ)")
 apply simp
apply (simp add:fun_eq_iff lift_lift_ML cons_ML_def split:nat.split)
done

corollary subst_cons_lift:
 "substML (VML 0 ## σ) o (liftML 0) = liftML 0 o (substML σ)"
apply(rule ext)
apply(simp add: lift_ML_subst_ML)
apply(subgoal_tac "(VML 0 ## σ) = (λi. if i = 0 then VML 0 else liftML 0 (σ (i - 1)))")
 apply simp
apply(rule ext, simp)
done

lemma lift_ML_id[simp]: "closedML k v  liftML k v = v"
by(induct k v rule: lift_ML.induct)(simp_all add:list_eq_iff_nth_eq)

lemma subst_ML_id:
  "closedML k v  i<k. σ i = VML i  substML σ v = v"
apply (induct σ v arbitrary: k rule: subst_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(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 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
done

corollary subst_ML_id2[simp]: "closedML 0 v  substML σ v = v"
using subst_ML_id[where k=0] by simp

lemma subst_ML_coincidence:
  "closedML k v  i<k. σ i = σ' i  substML σ v = substML σ' v"
by (induct σ v arbitrary: k σ' rule: subst_ML.induct) auto

lemma subst_ML_comp:
  "substML σ (substML σ' v) = substML (substML σ   σ') v"
apply (induct σ' v arbitrary: σ rule: subst_ML.induct)
apply (simp_all add: list_eq_iff_nth_eq)
apply(rule subst_ML_ext)
apply simp
apply (metis o_apply subst_cons_lift)
done

lemma subst_ML_comp2:
  "i. σ'' i = substML σ (σ' i)  substML σ (substML σ' v) = substML σ'' v"
by(simp add:subst_ML_comp subst_ML_ext)

lemma closed_tm_ML_foldl_At:
  "closedML k (t ∙∙ ts)  closedML k t  (t  set ts. closedML k t)"
by(induct ts arbitrary: t) simp_all

lemma closed_ML_lift[simp]:
  fixes v :: ml shows "closedML k v  closedML k (lift m v)"
by(induct k v arbitrary: m rule: lift_ML.induct)
  (simp_all add:list_eq_iff_nth_eq)

lemma closed_ML_Suc: "closedML n v  closedML (Suc n) (liftML k v)"
by (induct k v arbitrary: n rule: lift_ML.induct) simp_all

lemma closed_ML_subst_ML:
  "i. closedML k (σ i)  closedML k (substML σ v)"
by(induct σ v arbitrary: k rule: subst_ML.induct) (auto simp: closed_ML_Suc)

lemma closed_ML_subst_ML2:
  "closedML k v  i<k. closedML l (σ i)  closedML l (substML σ v)"
by(induct σ v arbitrary: k l rule: subst_ML.induct)(auto simp: closed_ML_Suc)


lemma subst_foldl[simp]:
 "subst σ (s ∙∙ ts) = (subst σ s) ∙∙ (map (subst σ) ts)"
by (induct ts arbitrary: s) auto

lemma subst_V: "pure t  subst V t = t"
by(induct pred:pure) simp_all

lemma lift_subst_aux:
  "pure t  i<k. σ' i = lift k (σ i) 
   ik. σ'(Suc i) = lift k (σ i)  
  σ' k = V k  lift k (subst σ t) = subst σ' (lift k t)"
apply(induct arbitrary:σ σ' k pred:pure)
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_ml lift_lift_tm split:nat.split)
done

corollary lift_subst:
  "pure t  lift 0 (subst σ t) = subst (V 0 ## σ) (lift 0 t)"
by (simp add: lift_subst_aux lift_lift_ml)

lemma subst_comp:
  "pure t  i. pure(σ' i) 
   σ'' = (λi. subst σ (σ' i))  subst σ (subst σ' t) = subst σ'' t"
apply(induct arbitrary:σ σ' σ'' pred:pure)
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
apply(rule ext)
apply(simp add:lift_subst)
done


section "Reduction"

subsection "Patterns"

inductive pattern :: "tm  bool"
      and patterns :: "tm list  bool" where
       "patterns ts  tset ts. pattern t" |
pat_V: "pattern(V X)" |
pat_C: "patterns ts  pattern(C nm ∙∙ ts)"

lemma pattern_Lam[simp]: "¬ pattern(Λ t)"
by(auto elim!: pattern.cases)

lemma pattern_At'D12: "pattern r  r = (s  t)  pattern s  pattern t"
proof(induct arbitrary: s t pred:pattern)
  case pat_V thus ?case by simp
next
  case pat_C thus ?case
    by (simp add: atomic_tm_head_tm split:if_split_asm)
       (metis eta_head_args in_set_butlastD pattern.pat_C)
qed

lemma pattern_AtD12: "pattern(s  t)  pattern s  pattern t"
by(metis pattern_At'D12)

lemma pattern_At_vecD: "pattern(s ∙∙ ts)  patterns ts"
apply(induct ts rule:rev_induct)
 apply simp
apply (fastforce dest!:pattern_AtD12)
done

lemma pattern_At_decomp: "pattern(s  t)  nm ss. s = C nm ∙∙ ss"
proof(induct s arbitrary: t)
  case (At s1 s2) show ?case
    using At by (metis foldl_Cons foldl_Nil foldl_append pattern_AtD12)
qed (auto elim!: pattern.cases split:if_split_asm)


subsection "Reduction of λ›-terms"

text‹The source program:›

axiomatization R :: "(cname * tm list * tm)set" where
pure_R: "(nm,ts,t) : R  (t  set ts. pure t)  pure t" and
fv_R:   "(nm,ts,t) : R  X : fv t  t'  set ts. X : fv t'" and
pattern_R: "(nm,ts,t') : R  patterns ts"

inductive_set
  Red_tm :: "(tm * tm)set"
  and red_tm :: "[tm, tm] => bool"  (infixl  50)
where
  "s  t  (s, t)  Red_tm"
 ― ‹$\beta$-reduction›
| "(Λ t)  s  t[s/0]"
 ― ‹$\eta$-expansion›
| "t  Λ ((lift 0 t)  (V 0))"
 ― ‹Rewriting›
| "(nm,ts,t) : R  (C nm) ∙∙ (map (subst σ) ts)  subst σ t"
| "t  t'  Λ t  Λ t'"
| "s  s'  s  t  s'  t"
| "t  t'  s  t  s  t'"

abbreviation
  reds_tm :: "[tm, tm] => bool"  (infixl →* 50) where
  "s →* t  (s, t)  Red_tm^*"

inductive_set
  Reds_tm_list :: "(tm list * tm list) set"
  and reds_tm_list :: "[tm list, tm list]  bool" (infixl →* 50)
where
  "ss →* ts  (ss, ts)  Reds_tm_list"
| "[] →* []"
| "ts →* ts'  t →* t'  t#ts →* t'#ts'"


declare Reds_tm_list.intros[simp]

lemma Reds_tm_list_refl[simp]: fixes ts :: "tm list" shows "ts →* ts"
by(induct ts) auto

lemma Red_tm_append: "rs →* rs'  ts →* ts'  rs @ ts →* rs' @ ts'"
by(induct set: Reds_tm_list) auto

lemma Red_tm_rev: "ts →* ts'  rev ts →* rev ts'"
by(induct set: Reds_tm_list) (auto simp:Red_tm_append)

lemma red_Lam[simp]: "t →* t'  Λ t →* Λ t'"
apply(induct rule:rtrancl_induct)
apply(simp_all)
apply(blast intro: rtrancl_into_rtrancl Red_tm.intros)
done

lemma red_At1[simp]: "t →* t'  t  s →* t'  s"
apply(induct rule:rtrancl_induct)
apply(simp_all)
apply(blast intro: rtrancl_into_rtrancl Red_tm.intros)
done

lemma red_At2[simp]: "t →* t'  s  t →* s  t'"
apply(induct rule:rtrancl_induct)
apply(simp_all)
apply(blast intro:rtrancl_into_rtrancl Red_tm.intros)
done

lemma Reds_tm_list_foldl_At:
 "ts →* ts'  s →* s'  s ∙∙ ts →* s' ∙∙ ts'"
apply(induct arbitrary:s s' rule:Reds_tm_list.induct)
apply simp
apply simp
apply(blast dest: red_At1 red_At2 intro:rtrancl_trans)
done


subsection "Reduction of ML-terms"

text‹The compiled rule set:›

consts compR :: "(cname * ml list * ml)set"

text‹\noindent
The actual definition is given in \S\ref{sec:Compiler} below.›

text‹Now we characterize ML values that cannot possibly be rewritten by a
rule in @{const compR}.›

lemma termination_no_match_ML:
  "i < length ps  rev ps ! i = CU nm vs
    sum_list (map size vs) < sum_list (map size ps)"
apply(subgoal_tac "CU nm vs : set ps")
 apply(drule sum_list_map_remove1[of _ _ size])
 apply (simp add:size_list_conv_sum_list)
apply (metis in_set_conv_nth length_rev set_rev)
done

declare conj_cong[fundef_cong]

function no_match_ML (no'_matchML) where
"no_matchML ps os =
  (i < min (size os) (size ps).
   nm nm' vs vs'. (rev ps)!i = CU nm vs  (rev os)!i = CU nm' vs' 
      (nm=nm'  no_matchML vs vs'))"
by pat_completeness auto
termination
apply(relation "measure(%(vs::ml list,_). vvs. size v)")
apply (auto simp:termination_no_match_ML)
done


abbreviation
"no_match_compR nm os 
  (nm',ps,v) compR. nm=nm'  no_matchML ps os"

declare no_match_ML.simps[simp del]

inductive_set
  Red_ml :: "(ml * ml)set"
  and Red_ml_list :: "(ml list * ml list)set"
  and red_ml :: "[ml, ml] => bool"  (infixl  50)
  and red_ml_list :: "[ml list, ml list] => bool"  (infixl  50)
  and reds_ml :: "[ml, ml] => bool"  (infixl ⇒* 50)
where
  "s  t  (s, t)  Red_ml"
| "ss  ts  (ss, ts)  Red_ml_list"
| "s ⇒* t  (s, t)  Red_ml^*"
 ― ‹ML $\beta$-reduction›
| "AML (LamML u) [v]  u[v/0]"
 ― ‹Execution of a compiled rewrite rule›
| "(nm,vs,v) : compR   i. closedML 0 (σ i) 
   AML (CML nm) (map (substML σ) vs)  substML σ v"
― ‹default rule:›
| "i. closedML 0 (σ i)
    vs = map VML [0..<arity nm]  vs' = map (substML σ) vs
    no_match_compR nm vs'
    AML (CML nm) vs'  substML σ (CU nm vs)"
 ― ‹Equations for function \texttt{apply}›
| apply_Clo1: "apply (Clo f vs (Suc 0)) v  AML f (v # vs)"
| apply_Clo2: "n > 0 
 apply (Clo f vs (Suc n)) v  Clo f (v # vs) n"
| apply_C: "apply (CU nm vs) v  CU nm (v # vs)"
| apply_V: "apply (VU x vs) v  VU x (v # vs)"
 ― ‹Context rules›
| ctxt_C: "vs  vs'  CU nm vs  CU nm vs'"
| ctxt_V: "vs  vs'  VU x vs  VU x vs'"
| ctxt_Clo1: "f  f'    Clo f vs n  Clo f' vs n"
| ctxt_Clo3: "vs  vs'  Clo f vs n  Clo f vs' n"
| ctxt_apply1: "s  s'    apply s t  apply s' t"
| ctxt_apply2: "t  t'    apply s t  apply s t'"
| ctxt_A_ML1: "f  f'    AML f vs  AML f' vs"
| ctxt_A_ML2: "vs  vs'  AML f vs  AML f vs'"
| ctxt_list1: "v  v'    v#vs  v'#vs"
| ctxt_list2: "vs  vs'  v#vs  v#vs'"

inductive_set
  Red_term :: "(tm * tm)set"
  and red_term :: "[tm, tm] => bool"  (infixl  50)
  and reds_term :: "[tm, tm] => bool"  (infixl ⇒* 50)
where
  "s  t  (s, t)  Red_term"
| "s ⇒* t  (s, t)  Red_term^*"
 ― ‹function \texttt{term}›
| term_C: "term (CU nm vs)  (C nm) ∙∙ (map term (rev vs))"
| term_V: "term (VU x vs)  (V x) ∙∙ (map term (rev vs))"
| term_Clo: "term(Clo vf vs n)  Λ (term (apply (lift 0 (Clo vf vs n)) (VU 0 [])))"
 ― ‹context rules›
| ctxt_Lam: "t  t'  Λ t  Λ t'"
| ctxt_At1: "s  s'  s  t  s'  t"
| ctxt_At2: "t  t'  s  t  s  t'"
| ctxt_term: "v  v'  term v  term v'"


section "Kernel"

text‹First a special size function and some lemmas for the
termination proof of the kernel function.›

fun size' :: "ml  nat" where
"size' (CML nm) = 1" |
"size' (VML X) = 1"  |
"size' (AML v vs) = (size' v + (vvs. size' v))+1" |
"size' (LamML v) = size' v + 1" |
"size' (CU nm vs) = (vvs. size' v)+1" |
"size' (VU nm vs) = (vvs. size' v)+1" |
"size' (Clo f vs n) = (size' f + (vvs. size' v))+1" |
"size' (apply v w) = (size' v + size' w)+1"

lemma sum_list_size'[simp]:
 "v  set vs  size' v < Suc(sum_list (map size' vs))"
by(induct vs)(auto)

corollary cor_sum_list_size'[simp]:
 "v  set vs  size' v < Suc(m + sum_list (map size' vs))"
using sum_list_size'[of v vs] by arith

lemma size'_lift_ML: "size' (liftML k v) = size' v"
apply(induct v arbitrary:k rule:size'.induct)
apply simp_all
   apply(rule arg_cong[where f = sum_list])
   apply(rule map_ext)
   apply simp
  apply(rule arg_cong[where f = sum_list])
  apply(rule map_ext)
  apply simp
 apply(rule arg_cong[where f = sum_list])
 apply(rule map_ext)
 apply simp
apply(rule arg_cong[where f = sum_list])
apply(rule map_ext)
apply simp
done

lemma size'_subst_ML[simp]:
 "i j. size'(σ i) = 1  size' (substML σ v) = size' v"
apply(induct v arbitrary:σ rule:size'.induct)
apply simp_all
    apply(rule arg_cong[where f = sum_list])
    apply(rule map_ext)
    apply simp
   apply(erule meta_allE)
   apply(erule meta_mp)
   apply(simp add: size'_lift_ML split:nat.split)
  apply(rule arg_cong[where f = sum_list])
  apply(rule map_ext)
  apply simp
 apply(rule arg_cong[where f = sum_list])
 apply(rule map_ext)
 apply simp
apply(rule arg_cong[where f = sum_list])
apply(rule map_ext)
apply simp
done

lemma size'_lift[simp]: "size' (lift i v) = size' v"
apply(induct v arbitrary:i rule:size'.induct)
apply simp_all
   apply(rule arg_cong[where f = sum_list])
   apply(rule map_ext)
   apply simp
  apply(rule arg_cong[where f = sum_list])
  apply(rule map_ext)
  apply simp
 apply(rule arg_cong[where f = sum_list])
 apply(rule map_ext)
 apply simp
apply(rule arg_cong[where f = sum_list])
apply(rule map_ext)
apply simp
done

function kernel  :: "ml  tm"  (‹_! 300) where
"(CML nm)! = C nm" |
"(AML v vs)! = v! ∙∙ (map kernel (rev vs))" |
"(LamML v)! = Λ (((lift 0 v)[VU 0 []/0])!)" |
"(CU nm vs)! = (C nm) ∙∙ (map kernel (rev vs))" |
"(VU x vs)! = (V x) ∙∙ (map kernel (rev vs))" |
"(Clo f vs n)! = f! ∙∙ (map kernel (rev vs))" |
"(apply v w)! = v!  (w!)" |
"(VML X)! = undefined"
by pat_completeness auto
termination by(relation "measure size'") auto

primrec kernelt :: "tm  tm" (‹_! 300)
where
  "(C nm)! = C nm"
| "(V x)! = V x"
| "(s  t)! = (s!)  (t!)"
| "(Λ t)! = Λ(t!)"
| "(term v)! = v!"

abbreviation
  kernels :: "ml list  tm list" (‹_! 300) where
  "vs!  map kernel vs"

lemma kernel_pure: assumes "pure t" shows "t! = t"
using assms by (induct) simp_all

lemma kernel_foldl_At[simp]: "(s ∙∙ ts)! = (s!) ∙∙ (map kernelt ts)"
by (induct ts arbitrary: s) simp_all

lemma kernelt_o_term[simp]: "(kernelt  term) = kernel"
by(rule ext) simp

lemma pure_foldl:
 "pure t  tset ts. pure t  
 (!!s t. pure s  pure t  pure(f s t)) 
 pure(foldl f t ts)"
by(induct ts arbitrary: t) simp_all

lemma pure_kernel: fixes v :: ml shows "closedML 0 v  pure(v!)"
proof(induct v rule:kernel.induct)
  case (3 v)
  hence "closedML (Suc 0) (lift 0 v)" by simp
  then have "substML (λn. VU 0 []) (lift 0 v) = lift 0 v[VU 0 []/0]"
    by(rule subst_ML_coincidence) simp
  moreover have "closedML 0 (substML (λn. VU 0 []) (lift 0 v))"
    by(simp add: closed_ML_subst_ML)
  ultimately have "closedML 0 (lift 0 v[VU 0 []/0])" by simp
  thus ?case using 3(1) by (simp add:pure_foldl)
qed (simp_all add:pure_foldl)

corollary subst_V_kernel: fixes v :: ml shows
  "closedML 0 v  subst V (v!) = v!"
by (metis pure_kernel subst_V)

lemma kernel_lift_tm: fixes v :: ml shows
  "closedML 0 v  (lift i v)! = lift i (v!)"
apply(induct v arbitrary: i rule: kernel.induct)
apply (simp_all add:list_eq_iff_nth_eq)
 apply(simp add: rev_nth)
defer
 apply(simp add: rev_nth)
 apply(simp add: rev_nth)
 apply(simp add: rev_nth)
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)  (λn. if n = 0 then VU 0 [] else VML (n - 1)) = (λn. if n = 0 then VU 0 [] else VML (n - 1))")
apply (simp add:lift_lift_ml)
apply(rule ext)
apply(simp)
apply(subst closed_ML_subst_ML2[of "1"])
apply(simp)
apply(simp)
apply(simp)
done

subsection "An auxiliary substitution"

text‹This function is only introduced to prove the involved susbtitution
lemma kernel_subst1› below.›

fun subst_ml :: "(nat  nat)  ml  ml" where
"subst_ml σ (CML nm) = CML nm" |
"subst_ml σ (VML X) = VML X" |
"subst_ml σ (AML v vs) = AML (subst_ml σ v) (map (subst_ml σ) vs)" |
"subst_ml σ (LamML v) = LamML (subst_ml σ v)" |
"subst_ml σ (CU nm vs) = CU nm (map (subst_ml σ) vs)" |
"subst_ml σ (VU x vs) = VU (σ x) (map (subst_ml σ) vs)" |
"subst_ml σ (Clo v vs n) = Clo (subst_ml σ v) (map (subst_ml σ) vs) n" |
"subst_ml σ (apply u v) = apply (subst_ml σ u) (subst_ml σ v)"

lemma lift_ML_subst_ml:
  "liftML k (subst_ml σ v) = subst_ml σ (liftML k v)"
apply (induct σ v arbitrary: k rule:subst_ml.induct)
apply (simp_all add:list_eq_iff_nth_eq)
done

lemma subst_ml_subst_ML:
  "subst_ml σ (substML σ' v) = substML (subst_ml σ o σ') (subst_ml σ v)"
apply (induct σ' v arbitrary: σ rule: subst_ML.induct)
apply(simp_all add:list_eq_iff_nth_eq)
apply(subgoal_tac "(subst_ml σ'  VML 0 ## σ) = VML 0 ## (subst_ml σ'  σ)")
apply simp
apply(rule ext)
apply(simp add: lift_ML_subst_ml)
done


text‹Maybe this should be the def of lift:›
lemma lift_is_subst_ml: "lift k v = subst_ml (λn. if n<k then n else n+1) v"
by(induct k v rule:lift_ml.induct)(simp_all add:list_eq_iff_nth_eq)

lemma subst_ml_comp:  "subst_ml σ (subst_ml σ' v) = subst_ml (σ o σ') v"
by(induct σ' v rule:subst_ml.induct)(simp_all add:list_eq_iff_nth_eq)

lemma subst_kernel:
  "closedML 0 v   subst (λn. V(σ n)) (v!) = (subst_ml σ v)!"
apply (induct v arbitrary: σ rule:kernel.induct)
apply (simp_all add:list_eq_iff_nth_eq)
 apply(simp add: rev_nth)
defer
 apply(simp add: rev_nth)
 apply(simp add: rev_nth)
 apply(simp add: rev_nth)
apply(erule_tac x="λn. case n of 0  0 | Suc k  Suc(σ k)" in meta_allE)
apply(erule_tac meta_impE)
apply(rule closed_ML_subst_ML2[where k="Suc 0"])
apply (metis closed_ML_lift)
apply simp
apply(subgoal_tac "(λn. V(case n of 0  0 | Suc k  Suc (σ k))) = (V 0 ## (λn. V(σ n)))")
apply (simp add:subst_ml_subst_ML)
defer
apply(simp add:fun_eq_iff split:nat.split)
apply(simp add:lift_is_subst_ml subst_ml_comp)
apply(rule arg_cong[where f = kernel])
apply(subgoal_tac "(case_nat 0 (λk. Suc (σ k))  Suc) = Suc o σ")
prefer 2 apply(simp add:fun_eq_iff split:nat.split)
apply(subgoal_tac "(subst_ml (case_nat 0 (λk. Suc (σ k))) 
               (λn. if n = 0 then VU 0 [] else VML (n - 1)))
             = (λn. if n = 0 then VU 0 [] else VML (n - 1))")
apply simp
apply(simp add: fun_eq_iff)
done

lemma if_cong0: "If x y z = If x y z"
by simp

lemma kernel_subst1:
  "closedML 0 v  closedML (Suc 0) u 
   kernel(u[v/0]) = (kernel((lift 0 u)[VU 0 []/0]))[v!/0]"
proof(induct u arbitrary:v rule:kernel.induct)
  case (3 w)
  show ?case (is "?L = ?R")
  proof -
    have "?L = Λ(lift 0 (w[liftML 0 v/Suc 0])[VU 0 []/0] !)"
      by (simp cong:if_cong0)
    also have " = Λ((lift 0 w)[liftML 0 (lift 0 v)/Suc 0][VU 0 []/0]!)"
      by(simp only: lift_subst_ML1 lift_lift_ML_comm)
    also have " = Λ(substML (λn. if n=0 then VU 0 [] else
            if n=Suc 0 then lift 0 v else VML (n - 2)) (lift 0 w) !)"
      apply simp
      apply(rule arg_cong[where f = kernel])
      apply(rule subst_ML_comp2)
      using 3
      apply auto
      done
    also have " = Λ((lift 0 w)[VU 0 []/0][lift 0 v/0]!)"
      apply simp
      apply(rule arg_cong[where f = kernel])
      apply(rule subst_ML_comp2[symmetric])
      using 3
      apply auto
      done
    also have " = Λ((lift_ml 0 ((lift_ml 0 w)[VU 0 []/0]))[VU 0 []/0]![(lift 0 v)!/0])"
      apply(rule arg_cong[where f = Λ])
      apply(rule 3(1))
      apply (metis closed_ML_lift 3(2))
      apply(subgoal_tac "closedML (Suc(Suc 0)) w")
      defer
      using 3
      apply force
      apply(subgoal_tac  "closedML (Suc (Suc 0)) (lift 0 w)")
      defer
      apply(erule closed_ML_lift)
      apply(erule closed_ML_subst_ML2)
      apply simp
      done
    also have " = Λ((lift_ml 0 (lift_ml 0 w)[VU 1 []/0])[VU 0 []/0]![(lift 0 v)!/0])" (is "_ = ?M")
      apply(subgoal_tac "lift_ml 0 (lift_ml 0 w[VU 0 []/0])[VU 0 []/0] =
                         lift_ml 0 (lift_ml 0 w)[VU 1 []/0][VU 0 []/0]")
      apply simp
      apply(subst lift_subst_ML)
      apply(simp add:comp_def if_distrib[where f="lift_ml 0"] cong:if_cong)
      done
    finally have "?L = ?M" .
    have "?R = Λ (subst (V 0 ## subst_decr 0 (v!))
          (lift 0 (lift_ml 0 w[VU 0 []/Suc 0])[VU 0 []/0]!))"
      apply(subgoal_tac "(VML 0 ## (λn. if n = 0 then VU 0 [] else VML (n - Suc 0))) = subst_decr_ML (Suc 0) (VU 0 [])")
      apply(simp cong:if_cong)
      apply(simp add:fun_eq_iff cons_ML_def split:nat.splits)
      done
    also have " = Λ (subst (V 0 ## subst_decr 0 (v!))
          ((lift 0 (lift_ml 0 w))[VU 1 []/Suc 0][VU 0 []/0]!))"
      apply(subgoal_tac "lift 0 (lift 0 w[VU 0 []/Suc 0]) = lift 0 (lift 0 w)[VU 1 []/Suc 0]")
      apply simp
      apply(subst lift_subst_ML)
      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))[VU 1 []/Suc 0][VU 0 []/0] =
               (lift 0 (lift_ml 0 w))[VU 0 []/0][VU 1 []/ 0]" (is "?l = ?r")
    proof -
      have "?l = substML (λn. if n= 0 then VU 0 [] else if n = 1 then VU 1 [] else
                      VML (n - 2))
               (lift_ml 0 (lift_ml 0 w))"
      by(auto intro!:subst_ML_comp2)
    also have " = ?r" by(auto intro!:subst_ML_comp2[symmetric])
    finally show ?thesis .
  qed
  also have "Λ (subst (V 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)[VU 0 []/0][VU 1 []/0]!) =
    subst (subst_decr 0 (kernel(lift_ml 0 v))) (lift_ml 0 (lift_ml 0 w)[VU 1 []/0][VU 0 []/0]!)" (is "?a = ?b")
    proof-
      define pi where "pi n = (if n = 0 then 1 else if n = 1 then 0 else n)" for n :: nat
      have "(λi. V (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. V(pi n)) (lift_ml 0 (lift_ml 0 w)[VU 0 []/0][VU 1 []/0]!))"
        apply(subst subst_comp[OF _ _ refl])
        prefer 3 apply simp
        using 3(3)
        apply simp
        apply(rule pure_kernel)
        apply(rule closed_ML_subst_ML2[where k="Suc 0"])
        apply(rule closed_ML_subst_ML2[where k="Suc(Suc 0)"])
        apply simp
        apply simp
        apply simp
        apply simp
        done
      also have " =
 (subst_ml pi (lift_ml 0 (lift_ml 0 w)[VU 0 []/0][VU 1 []/0]))![lift_tm 0 (v!)/0]"
        apply(subst subst_kernel)
        using 3 apply auto
        apply(rule closed_ML_subst_ML2[where k="Suc 0"])
        apply(rule closed_ML_subst_ML2[where k="Suc(Suc 0)"])
        apply simp
        apply simp
        apply simp
        done
      also have " = (subst_ml pi (lift_ml 0 (lift_ml 0 w)[VU 0 []/0][VU 1 []/0]))![lift 0 v!/0]"
      proof -
        have "lift 0 (v!) = lift 0 v!" by (metis 3(2) kernel_lift_tm)
        thus ?thesis by (simp cong:if_cong)
      qed
      also have " = ?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  (Suc  Suc) = (Suc  Suc)")
          apply(simp)
          apply(simp add:pi_def fun_eq_iff)
          done
        have "subst_ml pi (lift_ml 0 (lift_ml 0 w)[VU 0 []/0][VU 1 []/0]) =
             lift_ml 0 (lift_ml 0 w)[VU 1 []/0][VU 0 []/0]"
          apply(subst subst_ml_subst_ML)
          apply(subst subst_ml_subst_ML)
          apply(subst 1)
          apply(subst subst_ML_comp)
          apply(rule subst_ML_comp2[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, (simp_all add:rev_nth)?)


section ‹Compiler \label{sec:Compiler}›

axiomatization arity :: "cname  nat"

primrec compile :: "tm  (nat  ml)  ml"
where
  "compile (V x) σ = σ x"
| "compile (C nm) σ =
    (if arity nm > 0 then Clo (CML nm) [] (arity nm) else AML (CML nm) [])"
| "compile (s  t) σ = apply (compile s σ) (compile t σ)"
| "compile (Λ t) σ = Clo (LamML (compile t (VML 0 ## σ))) [] 1"

text‹Compiler for open terms and for terms with fixed free variables:›

definition "comp_open t = compile t VML"
abbreviation "comp_fixed t  compile t (λi. VU i [])"

text‹Compiled rules:›

lemma size_args_less_size_tm[simp]: "s  set (args_tm t)  size s < size t"
by(induct t) auto

fun comp_pat where
"comp_pat t =
   (case head_tm t of
     C nm  CU nm (map comp_pat (rev (args_tm t)))
   | V X  VML X)"

declare comp_pat.simps[simp del] size_args_less_size_tm[simp del]

lemma comp_pat_V[simp]: "comp_pat(V X) = VML X"
by(simp add:comp_pat.simps)

lemma comp_pat_C[simp]:
  "comp_pat(C nm ∙∙ ts) = CU nm (map comp_pat (rev ts))"
by(simp add:comp_pat.simps)

lemma comp_pat_C_Nil[simp]: "comp_pat(C nm) = CU nm []"
by(simp add:comp_pat.simps)


overloading compR  compR
begin
  definition "compR  (λ(nm,ts,t). (nm, map comp_pat (rev ts), comp_open t)) ` R"
end


lemma fv_ML_comp_open: "pure t  fvML(comp_open t) = fv t"
by(induct t pred:pure) (simp_all add:comp_open_def)

lemma fv_ML_comp_pat: "pattern t  fvML(comp_pat t) = fv t"
by(induct t pred:pattern)(simp_all add:comp_open_def)

lemma fv_compR_aux:
  "(nm,ts,t') : R  x  fvML (comp_open t')
    tset ts. x  fvML(comp_pat t)"
apply(frule pure_R)
apply(simp add:fv_ML_comp_open)
apply(frule (1) fv_R)
apply clarsimp
apply(rule bexI) prefer 2 apply assumption
apply(drule pattern_R)
apply(simp add:fv_ML_comp_pat)
done

lemma fv_compR:
  "(nm,vs,v) : compR  x  fvML v  uset vs. x  fvML u"
by(fastforce simp add:compR_def image_def dest: fv_compR_aux)

lemma lift_compile:
  "pure t  σ k. lift k (compile t σ) = compile t (lift k  σ)"
apply(induct pred:pure)
apply simp_all
apply clarsimp
apply(rule_tac f = "compile t" in arg_cong)
apply(rule ext)
apply (clarsimp simp: lift_lift_ML_comm)
done

lemma subst_ML_compile:
  "pure t  substML σ' (compile t σ) = compile t (substML σ' o σ)"
apply(induct arbitrary: σ σ' pred:pure)
apply simp_all
apply(erule_tac x="VML 0 ## σ'" in meta_allE)
apply(erule_tac x= "VML 0 ## (liftML 0  σ)" in meta_allE)
apply(rule_tac f = "compile t" in arg_cong)
apply(rule ext)
apply (auto simp add:subst_ML_ext lift_ML_subst_ML)
done

theorem kernel_compile:
  "pure t  i. σ i = VU i []  (compile t σ)! = t"
apply(induct arbitrary: σ pred:pure)
apply simp_all
apply(subst lift_compile) apply simp
apply(subst subst_ML_compile) apply simp
apply(subgoal_tac "(substML (λn. if n = 0 then VU 0 [] else VML (n - 1)) 
               (lift 0  VML 0 ## σ)) = (λa. VU a [])")
apply(simp)
apply(rule ext)
apply(simp)
done

lemma kernel_subst_ML_pat:
  "pure t  pattern t  i. closedML 0 (σ i) 
   (substML σ (comp_pat t))! = subst (kernel  σ) t"
apply(induct arbitrary: σ pred:pure)
apply simp_all
apply(frule pattern_At_decomp)
apply(frule pattern_AtD12)
apply clarsimp
apply(subst comp_pat.simps)
apply(simp add: rev_map)
done

lemma kernel_subst_ML:
  "pure t  i. closedML 0 (σ i) 
   (substML σ (comp_open t))! = subst (kernel  σ) t"
proof(induct arbitrary: σ pred:pure)
  case (Lam t)
  have "lift 0 o VML = VML" by (simp add:fun_eq_iff)
  hence "(substML σ (comp_open (Λ t)))! =
    Λ (substML (lift 0  VML 0 ## σ) (comp_open t)[VU 0 []/0]!)"
    using Lam by(simp add: lift_subst_ML comp_open_def lift_compile)
  also have " = Λ (subst (V 0 ## (kernel  σ)) t)" using Lam
    by(simp add: subst_ML_comp subst_ext kernel_lift_tm)
  also have " = subst (kernel o σ) (Λ t)" by simp
  finally show ?case .
qed (simp_all add:comp_open_def)

lemma kernel_subst_ML_pat_map:
  "t  set ts. pure t  patterns ts  i. closedML 0 (σ i) 
   map kernel (map (substML σ) (map comp_pat ts)) =
   map (subst (kernel  σ)) ts"
by(simp add:list_eq_iff_nth_eq kernel_subst_ML_pat)

lemma compR_Red_tm: "(nm, vs, v) : compR   i. closedML 0 (σ i)
   C nm ∙∙ (map (substML σ) (rev vs))! →* (substML σ v)!"
apply(auto simp add:compR_def rev_map simp del: map_map)
apply(frule pure_R)
apply(subst kernel_subst_ML) apply fast+
apply(subst kernel_subst_ML_pat_map)
 apply fast
 apply(fast dest:pattern_R)
 apply assumption
apply(rule r_into_rtrancl)
apply(erule Red_tm.intros)
done


section "Correctness"

(* Without this special rule one "also" in the next proof *diverges*,
   probably because of HOU. *)
lemma eq_Red_tm_trans: "s = t  t  t'  s  t'"
by simp

text‹Soundness of reduction:›
theorem fixes v :: ml shows Red_ml_sound:
  "v  v'  closedML 0 v  v! →* v'!  closedML 0 v'" and
  "vs  vs'  vset vs. closedML 0 v 
   vs! →* vs'!  (v'set vs'. closedML 0 v')"
proof(induct rule:Red_ml_Red_ml_list.inducts)
  fix u v
  let ?v = "AML (LamML u) [v]"
  assume cl: "closedML 0 (AML (LamML u) [v])"
  let ?u' = "(lift_ml 0 u)[VU 0 []/0]"
  have "?v! = (Λ((?u')!))  (v !)" by simp
  also have "  (?u' !)[v!/0]" (is "_  ?R") by(rule Red_tm.intros)
  also(eq_Red_tm_trans) have "?R = u[v/0]!" using cl
    apply(cut_tac u = "u" and v = "v" in kernel_subst1)
    apply(simp_all)
    done
  finally have "kernel(AML (LamML u) [v]) →* kernel(u[v/0])" (is ?A)
    by(rule r_into_rtrancl)
  moreover have "closedML 0 (u[v/0])" (is "?C")
  proof -
    let  = "λn. if n = 0 then v else VML (n - 1)"
    let ?σ' = "λn. v"
    have clu: "closedML (Suc 0) u" and clv: "closedML 0 v" using cl by simp+
    have "closedML 0 (substML ?σ' u)"
      by (metis closed_ML_subst_ML clv)
    hence "closedML 0 (substML  u)"
      using subst_ML_coincidence[OF clu, of  ?σ'] by auto
    thus ?thesis by simp
  qed
  ultimately show "?A  ?C" ..
next
  fix σ :: "nat  ml" and nm vs v
  assume σ: "i. closedML 0 (σ i)"  and compR: "(nm, vs, v)  compR"
  have "map (subst V) (map (substML σ) (rev vs)!) = map (substML σ) (rev vs)!"
    by(simp add:list_eq_iff_nth_eq subst_V_kernel closed_ML_subst_ML[OF σ])
  with compR_Red_tm[OF compR σ]
  have "(C nm) ∙∙ ((map (substML σ) (rev vs)) !) →* (substML σ v)!"
    by(simp add:subst_V_kernel closed_ML_subst_ML[OF σ])
  hence "AML (CML nm) (map (substML σ) vs)! →* substML σ v!" (is ?A)
    by(simp add:rev_map)
  moreover
  have "closedML 0 (substML σ v)" (is ?C) by(metis closed_ML_subst_ML σ)
  ultimately show "?A  ?C" ..
qed (auto simp:Reds_tm_list_foldl_At Red_tm_rev rev_map[symmetric])

theorem Red_term_sound:
  "t  t'  closedML 0 t  kernelt t →* kernelt t'   closedML 0 t'"
proof(induct rule:Red_term.inducts)
  case term_C thus ?case
    by (auto simp:closed_tm_ML_foldl_At)
next
  case term_V thus ?case
    by (auto simp:closed_tm_ML_foldl_At)
next
  case (term_Clo vf vs n)
  hence "(lift 0 vf!) ∙∙ map kernel (rev (map (lift 0) vs))
         = lift 0 (vf! ∙∙ (rev vs)!)"
    apply (simp add:kernel_lift_tm list_eq_iff_nth_eq)
    apply(simp add:rev_nth rev_map kernel_lift_tm)
    done
  hence "term (Clo vf vs n)! →*
       Λ (term (apply (lift 0 (Clo vf vs n)) (VU 0 [])))!"
    using term_Clo
    by(simp del:lift_foldl_At add: r_into_rtrancl Red_tm.intros(2))
  moreover
  have "closedML 0 (Λ (term (apply (lift 0 (Clo vf vs n)) (VU 0 []))))"
    using term_Clo by simp
  ultimately show ?case ..
next
  case ctxt_term thus ?case by simp (metis Red_ml_sound)
qed auto

corollary kernel_inv:
 "(t :: tm) ⇒* t'  closedML 0 t  t! →* t'!  closedML 0 t' "
apply(induct rule: rtrancl.induct)
apply (metis rtrancl_eq_or_trancl)
apply (metis Red_term_sound rtrancl_trans)
done

lemma  closed_ML_compile:
  "pure t  i. closedML n (σ i)  closedML n (compile t σ)"
proof(induct arbitrary:n σ pred:pure)
  case (Lam t)
  have 1: "i. closedML (Suc n) ((VML 0 ## σ) i)" using Lam(3-)
    by (auto simp: closed_ML_Suc)
  show ?case using Lam(2)[OF 1] by (simp del:apply_cons_ML)
qed simp_all

theorem nbe_correct: fixes t :: tm
assumes "pure t" and "term (comp_fixed t) ⇒* t'" and "pure t'" shows "t →* t'"
proof -
  have ML_cl: "closedML 0 (term (comp_fixed t))"
    by (simp add: closed_ML_compile[OF pure t])
  have "(term (comp_fixed t))! = t"
    using kernel_compile[OF pure t] by simp
  moreover have "term (comp_fixed t)! →* t'!"
    using kernel_inv[OF assms(2) ML_cl] by auto
  ultimately have "t →* t'!" by simp
  thus ?thesis using kernel_pure[OF pure t'] by simp
qed


section "Normal Forms"

inductive normal :: "tm  bool" where
"tset ts. normal t  normal(V x ∙∙ ts)" |
"normal t  normal(Λ t)" |
"tset ts. normal t 
 σ. (nm',ls,r)R. ¬(nm = nm'  take (size ls) ts = map (subst σ) ls)
  normal(C nm ∙∙ ts)"

fun C_normal_ML :: "ml  bool" (C'_normalML) where
"C_normalML(CU nm vs) =
  ((vset vs. C_normalML v)  no_match_compR nm vs)" |
"C_normalML (CML _) = True" |
"C_normalML (VML _) = True" |
"C_normalML (AML v vs) = (C_normalML v  (v  set vs. C_normalML v))" |
"C_normalML (LamML v) = C_normalML v" |
"C_normalML (VU x vs) = (v  set vs. C_normalML v)" |
"C_normalML (Clo v vs _) = (C_normalML v  (v  set vs. C_normalML v))" |
"C_normalML (apply u v) = (C_normalML u  C_normalML v)"

fun size_tm :: "tm  nat" where
"size_tm (C _) = 1" |
"size_tm (At s t) = size_tm s + size_tm t + 1" |
"size_tm _ = 0"

lemma size_tm_foldl_At: "size_tm(t ∙∙ ts) = size_tm t + size_list size_tm ts"
by (induct ts arbitrary:t) auto

lemma termination_no_match:
  "i < length ss  ss ! i = C nm ∙∙ ts
    sum_list (map size_tm ts) < sum_list (map size_tm ss)"
apply(subgoal_tac "C nm ∙∙ ts : set ss")
 apply(drule sum_list_map_remove1[of _ _ size_tm])
apply(simp add:size_tm_foldl_At size_list_conv_sum_list)
apply (metis in_set_conv_nth)
done

declare conj_cong [fundef_cong]

function no_match :: "tm list  tm list  bool" where
"no_match ps ts =
  (i < min (size ts) (size ps).
   nm nm' rs rs'. ps!i = (C nm) ∙∙ rs  ts!i = (C nm') ∙∙ rs' 
      (nm=nm'  no_match rs rs'))"
by pat_completeness auto
termination
apply(relation "measure(%(ts::tm list,_). tts. size_tm t)")
apply (auto simp:termination_no_match)
done

declare no_match.simps[simp del]

abbreviation
"no_match_R nm ts  (nm',ps,t) R. nm=nm'  no_match ps ts"


lemma no_match: "no_match ps ts  ¬(σ. map (subst σ) ps = ts)"
proof(induct ps ts rule:no_match.induct)
  case (1 ps ts)
  thus ?case
    apply auto
    apply(subst (asm) no_match.simps[of ps])
    apply fastforce
    done
qed

lemma no_match_take: "no_match ps ts  no_match ps (take (size ps) ts)"
apply(subst (asm) no_match.simps)
apply(subst no_match.simps)
apply fastforce
done

fun dterm_ML :: "ml  tm" (dtermML) where
"dtermML (CU nm vs) = C nm ∙∙ map dtermML (rev vs)" |
"dtermML _ = V 0"

fun dterm :: "tm  tm" where
"dterm (V n) = V n" |
"dterm (C nm) = C nm" |
"dterm (s  t) = dterm s  dterm t" |
"dterm (Λ t) = Λ (dterm t)" |
"dterm (term v) = dtermML v"

lemma dterm_pure[simp]: "pure t  dterm t = t"
by (induct pred:pure) auto

lemma map_dterm_pure[simp]: "tset ts. pure t  map dterm ts = ts"
by (induct ts) auto

lemma map_dterm_term[simp]: "map dterm (map term vs) = map dtermML vs"
by (induct vs) auto

lemma dterm_foldl_At[simp]: "dterm(t ∙∙ ts) = dterm t ∙∙ map dterm ts"
by(induct ts arbitrary: t) auto

lemma no_match_coincide:
  "no_matchML ps vs 
  no_match (map dtermML (rev ps)) (map dtermML (rev vs))"
apply(induct ps vs rule:no_match_ML.induct)
apply(rotate_tac 1)
apply(subst (asm) no_match_ML.simps)
apply (elim exE conjE)
apply(case_tac "nm=nm'")
prefer 2
apply(subst no_match.simps)
apply(rule_tac x=i in exI)
apply rule
apply (simp (no_asm))
apply (metis min_less_iff_conj)
apply(simp add:min_less_iff_conj nth_map)
apply safe
apply(erule_tac x=i in meta_allE)
apply(erule_tac x=nm' in meta_allE)
apply(erule_tac x=nm' in meta_allE)
apply(erule_tac x="vs" in meta_allE)
apply(erule_tac x="vs'" in meta_allE)
apply(subst no_match.simps)
apply(rule_tac x=i in exI)
apply rule
apply (simp (no_asm))
apply (metis min_less_iff_conj)
apply(rule_tac x=nm' in exI)
apply(rule_tac x=nm' in exI)
apply(rule_tac x="map dtermML (rev vs)" in exI)
apply(rule_tac x="map dtermML (rev vs')" in exI)
apply(simp)
done

lemma dterm_ML_comp_patD:
  "pattern t  dtermML (comp_pat t) = C nm ∙∙ rs  ts. t = C nm ∙∙ ts"
by(induct pred:pattern) simp_all

lemma no_match_R_coincide_aux[rule_format]: "patterns ts 
  no_match (map (dtermML  comp_pat) ts) rs  no_match ts rs"
apply(induct ts rs rule:no_match.induct)
apply(subst (1 2) no_match.simps)
apply clarsimp
apply(rule_tac x=i in exI)
apply simp
apply(rule_tac x=nm in exI)
apply(cut_tac t = "ps!i" in dterm_ML_comp_patD, simp, assumption)
apply(clarsimp)
apply(erule_tac x = i in meta_allE)
apply(erule_tac x = nm' in meta_allE)
apply(erule_tac x = nm' in meta_allE)
apply(erule_tac x = tsa in meta_allE)
apply(erule_tac x = rs' in meta_allE)
apply (simp add:rev_map)
apply (metis in_set_conv_nth pattern_At_vecD)
done

lemma no_match_R_coincide:
  "no_match_compR nm (rev vs)  no_match_R nm (map dtermML vs)"
apply auto
apply(drule_tac x="(nm, map comp_pat (rev aa), comp_open b)" in bspec)
 unfolding compR_def
 apply (simp add:image_def) 
 apply (force)
apply (simp)
apply(drule no_match_coincide)
apply(frule pure_R)
apply(drule pattern_R)
apply(clarsimp simp add: rev_map no_match.simps[of _ "map dtermML vs"])
apply(rule_tac x=i in exI)
apply simp
apply(cut_tac t = "aa!i" in dterm_ML_comp_patD, simp, assumption)
apply clarsimp
apply(auto simp: rev_map)
apply(rule no_match_R_coincide_aux)
prefer 2 apply assumption
apply (metis in_set_conv_nth pattern_At_vecD)
done


inductive C_normal :: "tm  bool" where
"tset ts. C_normal t  C_normal(V x ∙∙ ts)" |
"C_normal t  C_normal(Λ t)" |
"C_normalML v  C_normal(term v)" |
"tset ts. C_normal t  no_match_R nm (map dterm ts)
  C_normal(C nm ∙∙ ts)"

declare C_normal.intros[simp]

lemma C_normal_term[simp]: "C_normal(term v) = C_normalML v"
apply (auto)
apply(erule C_normal.cases)
apply auto
done

lemma [simp]: "C_normal(Λ t) = C_normal t"
apply (auto)
apply(erule C_normal.cases)
apply auto
done

lemma [simp]: "C_normal(V x)"
using C_normal.intros(1)[of "[]" x]
by simp

lemma [simp]: "dterm (dtermML v) = dtermML v"
apply(induct v rule:dterm_ML.induct)
apply simp_all
done

lemma "u(v::ml)  True" and
  Red_ml_list_length: "vs  vs'  length vs = length vs'"
by(induct rule: Red_ml_Red_ml_list.inducts) simp_all

lemma "(v::ml)  v'  True" and
  Red_ml_list_nth: "(vs::ml list)  vs'
   v' k. k<size vs  vs!k  v'  vs' = vs[k := v']"
apply (induct rule: Red_ml_Red_ml_list.inducts)
apply (auto split:nat.splits)
done

lemma Red_ml_list_pres_no_match:
  "no_matchML ps vs  vs  vs'  no_matchML ps vs'"
proof(induct ps vs arbitrary: vs' rule:no_match_ML.induct)
  case (1 vs os)
  show ?case using 1(2-3)
apply-
apply(frule Red_ml_list_length)
apply(rotate_tac -2)
apply(subst (asm) no_match_ML.simps)
apply clarify
apply(rename_tac i nm nm' us us')
apply(subst no_match_ML.simps)
apply(rule_tac x=i in exI)
apply (simp)
apply(drule Red_ml_list_nth)
apply clarify
apply(rename_tac k)
apply(case_tac "k = length os - Suc i")
prefer 2
apply(rule_tac x=nm' in exI)
apply(rule_tac x=us' in exI)
apply (simp add: rev_nth nth_list_update)
apply (simp add: rev_nth)
apply(erule Red_ml.cases)
apply simp_all
apply(fastforce intro: 1(1) simp add:rev_nth)
done
qed

lemma no_match_ML_subst_ML[rule_format]:
  "vset vs. xfvML v. C_normalML (σ x) 
   no_matchML ps vs  no_matchML ps (map (substML σ) vs)"
apply(induct ps vs rule:no_match_ML.induct)
apply simp
apply(subst (1 2) no_match_ML.simps)
apply clarsimp
apply(rule_tac x=i in exI)
apply simp
apply(rule_tac x=nm' in exI)
apply(rule_tac x="map (substML σ) vs'" in exI)
apply (auto simp:rev_nth)
apply(erule_tac x = i in meta_allE)
apply(erule_tac x = nm' in meta_allE)
apply(erule_tac x = nm' in meta_allE)
apply(erule_tac x = vs in meta_allE)
apply(erule_tac x = vs' in meta_allE)
apply simp
apply (metis UN_I fv_ML.simps(5) in_set_conv_nth length_rev rev_nth set_rev)
done

lemma lift_is_CUD:
  "liftML k v = CU nm vs'  vs. v = CU nm vs  vs' = map (liftML k) vs"
by(cases v) auto

lemma no_match_ML_lift_ML:
  "no_matchML ps (map (liftML k) vs) = no_matchML ps vs"
apply(induct ps vs rule:no_match_ML.induct)
apply simp
apply(subst (1 2) no_match_ML.simps)
apply rule
 apply clarsimp
 apply(rule_tac x=i in exI)
 apply (simp add:rev_nth)
 apply(drule lift_is_CUD)
 apply fastforce
apply clarsimp
apply(rule_tac x=i in exI)
apply simp
apply(rule_tac x=nm' in exI)
apply(rule_tac x="map (liftML k) vs'" in exI)
apply (fastforce simp:rev_nth)
done

lemma C_normal_ML_lift_ML: "C_normalML(liftML k v) = C_normalML v"
by(induct v arbitrary: k rule:C_normal_ML.induct)(auto simp:no_match_ML_lift_ML)

lemma no_match_compR_Cons:
  "no_match_compR nm vs  no_match_compR nm (v # vs)"
apply auto
apply(drule bspec, assumption)
apply simp
apply(subst (asm) no_match_ML.simps)
apply(subst no_match_ML.simps)
apply clarsimp
apply(rule_tac x=i in exI)
apply (simp add:nth_append)
done

lemma C_normal_ML_comp_open: "pure t  C_normalML(comp_open t)"
by (induct pred:pure) (auto simp:comp_open_def)

lemma C_normal_compR_rhs: "(nm, vs, v)  compR  C_normalML v"
by(auto simp: compR_def image_def Bex_def pure_R C_normal_ML_comp_open)


lemma C_normal_ML_subst_ML:
  "C_normalML (substML σ v)  (xfvML v. C_normalML (σ x))"
proof(induct σ v rule:subst_ML.induct)
  case 4 thus ?case
    by(simp del:apply_cons_ML)(force simp add: C_normal_ML_lift_ML)
      (* weird - force suffices in apply style *)
qed auto

lemma C_normal_ML_subst_ML_iff: "C_normalML v 
  C_normalML (substML σ v)  (xfvML v. C_normalML (σ x))"
proof(induct σ v rule:subst_ML.induct)
  case 4 thus ?case
    by(simp del:apply_cons_ML)(force simp add: C_normal_ML_lift_ML)
      (* weird - force suffices in apply style *)
next
  case 5 thus ?case by simp (blast intro: no_match_ML_subst_ML)
qed auto

lemma C_normal_ML_inv: "v  v'  C_normalML v  C_normalML v'" and
      "vs  vs'  vset vs. C_normalML v  v'set vs'. C_normalML v'"
apply(induct rule:Red_ml_Red_ml_list.inducts)
apply(simp_all add: C_normal_ML_subst_ML_iff)
  apply(metis C_normal_ML_subst_ML C_normal_compR_rhs
        fv_compR C_normal_ML_subst_ML_iff)
 apply(blast intro!:no_match_compR_Cons)
apply(blast dest:Red_ml_list_pres_no_match)
done


lemma Red_term_hnf_induct[consumes 1]:
assumes "(t::tm)  t'"
  "nm vs ts. P ((term (CU nm vs)) ∙∙ ts) ((C nm ∙∙ map term (rev vs)) ∙∙ ts)"
  "x vs ts. P (term (VU x vs) ∙∙ ts) ((V x ∙∙ map term (rev vs)) ∙∙ ts)"
  "vf vs n ts.
    P (term (Clo vf vs n) ∙∙ ts)
     ((Λ (term (apply (lift 0 (Clo vf vs n)) (VU 0 [])))) ∙∙ ts)"
  "t t' ts. t  t'; P t t'  P (Λ t ∙∙ ts) (Λ t' ∙∙ ts)"
  "v v' ts. v  v'  P (term v ∙∙ ts) (term v' ∙∙ ts)"
  "x i t' ts. i<size ts  ts!i  t'  P (ts!i) (t')
     P (V x  ∙∙ ts) (V x ∙∙ ts[i:=t'])"
  "nm i t' ts. i<size ts  ts!i  t'  P (ts!i) (t')
     P (C nm  ∙∙ ts) (C nm ∙∙ ts[i:=t'])"
  "t i t' ts. i<size ts  ts!i  t'  P (ts!i) (t')
     P (Λ t ∙∙ ts) (Λ t ∙∙ ts[i:=t'])"
  "v i t' ts. i<size ts  ts!i  t'  P (ts!i) (t')
     P (term v  ∙∙ ts) (term v ∙∙ (ts[i:=t']))"
shows "P t t'"
proof-
  { fix ts from assms have "P (t ∙∙ ts) (t' ∙∙ ts)"
    proof(induct arbitrary: ts rule:Red_term.induct)
      case term_C thus ?case by metis
    next
      case term_V thus ?case by metis
    next
      case term_Clo thus ?case by metis
    next
      case ctxt_Lam thus ?case by simp (metis foldl_Nil)
    next
      case (ctxt_At1 s s' t ts)
      thus ?case using ctxt_At1(2)[of "t#ts"] by simp
    next
      case (ctxt_At2 t t' s ts)
      { fix n rs assume "s = V n ∙∙ rs"
        hence ?case using ctxt_At2(8)[of "size rs" "rs @ t # ts" t' n] ctxt_At2
          by simp (metis foldl_Nil)
      } moreover
      { fix nm rs assume "s = C nm ∙∙ rs"
        hence ?case using ctxt_At2(9)[of "size rs" "rs @ t # ts" t' nm] ctxt_At2
          by simp (metis foldl_Nil)
      } moreover
      { fix r rs assume "s = Λ r ∙∙ rs"
        hence ?case using ctxt_At2(10)[of "size rs" "rs @ t # ts" t'] ctxt_At2
          by simp (metis foldl_Nil)
      } moreover
      { fix v rs assume "s = term v ∙∙ rs"
        hence ?case using ctxt_At2(11)[of "size rs" "rs @ t # ts" t'] ctxt_At2
          by simp (metis foldl_Nil)
      } ultimately show ?case using tm_vector_cases[of s] by blast
    qed
  }
  from this[of "[]"] show ?thesis by simp
qed

corollary Red_term_hnf_cases[consumes 1]:
assumes "(t::tm)  t'"
  "nm vs ts.
  t = term (CU nm vs) ∙∙ ts  t' = (C nm ∙∙ map term (rev vs)) ∙∙ ts  P"
  "x vs ts.
  t = term (VU x vs) ∙∙ ts  t' = (V x ∙∙ map term (rev vs)) ∙∙ ts  P"
  "vf vs n ts. t = term (Clo vf vs n) ∙∙ ts 
     t' = Λ (term (apply (lift 0 (Clo vf vs n)) (VU 0 []))) ∙∙ ts  P"
  "s s' ts. t = Λ s ∙∙ ts  t' = Λ s' ∙∙ ts  s  s'  P"
  "v v' ts. t = term v ∙∙ ts  t' = term v' ∙∙ ts  v  v'  P"
  "x i r' ts. i<size ts  ts!i  r'
     t = V x  ∙∙ ts  t' = V x ∙∙ ts[i:=r']  P"
  "nm i r' ts. i<size ts  ts!i  r'
     t = C nm  ∙∙ ts  t' = C nm ∙∙ ts[i:=r']  P"
  "s i r' ts. i<size ts  ts!i  r'
     t = Λ s ∙∙ ts  t' = Λ s ∙∙ ts[i:=r']  P"
  "v i r' ts. i<size ts  ts!i  r'
     t = term v  ∙∙ ts  t' = term v ∙∙ (ts[i:=r'])  P"
shows "P" using assms
apply -
apply(induct rule:Red_term_hnf_induct)
apply metis+
done


lemma [simp]: "C_normal(term v ∙∙ ts)  C_normalML v  ts = []"
by(fastforce elim: C_normal.cases)

lemma [simp]: "C_normal(Λ t ∙∙ ts)  C_normal t  ts = []"
by(fastforce elim: C_normal.cases)

lemma [simp]: "C_normal(C nm ∙∙ ts) 
  (tset ts. C_normal t)  no_match_R nm (map dterm ts)"
by(fastforce elim: C_normal.cases)

lemma [simp]: "C_normal(V x ∙∙ ts)  (t  set ts. C_normal t)"
by(fastforce elim: C_normal.cases)

lemma no_match_ML_lift:
  "no_matchML ps vs  no_matchML ps (map (lift k) vs)"
apply(induct ps vs rule:no_match_ML.induct)
apply simp
apply(subst (1 2) no_match_ML.simps)
apply clarsimp
apply(rule_tac x=i in exI)
apply simp
apply(rule_tac x=nm' in exI)
apply(rule_tac x="map (lift k) vs'" in exI)
apply (fastforce simp:rev_nth)
done

lemma no_match_compR_lift:
  "no_match_compR nm vs  no_match_compR nm (map (lift k) vs)"
by (fastforce simp: no_match_ML_lift)

lemma [simp]: "C_normalML v  C_normalML(lift k v)"
apply(induct v arbitrary:k rule:lift_ml.induct)
apply(simp_all add:no_match_compR_lift)
done

declare [[simp_depth_limit = 10]]

lemma Red_term_pres_no_match:
  "i < length ts; ts ! i  t'; no_match ps dts; dts = (map dterm ts)
    no_match ps (map dterm (ts[i := t']))"
proof(induct ps dts arbitrary: ts i t' rule:no_match.induct)
  case (1 ps dts ts i t')
  from no_match ps dts dts = map dterm ts
  obtain j nm nm' rs rs' where ob: "j < size ts" "j < size ps"
    "ps!j = C nm ∙∙ rs" "dterm (ts!j) = C nm' ∙∙ rs'"
    "nm = nm'  no_match rs rs'"
    by (subst (asm) no_match.simps) fastforce
  show ?case
  proof (subst no_match.simps)
    show "k<min (length (map dterm (ts[i := t']))) (length ps).
       nm nm' rs rs'. ps!k  = C nm ∙∙ rs 
         map dterm (ts[i := t']) ! k = C nm' ∙∙ rs' 
        (nm = nm'  no_match rs rs')"
      (is "k < ?m. ?P k")
    proof-
      { assume [simp]: "j=i"
        have "rs'. dterm t' = C nm' ∙∙ rs'  (nm = nm'  no_match rs rs')"
          using ts ! i  t'
        proof(cases rule:Red_term_hnf_cases)
          case (5 v v' ts'')
          then obtain vs where [simp]:
            "v = CU nm' vs" "rs' = map dtermML (rev vs) @ map dterm ts''"
            using ob by(cases v) auto
          obtain vs' where [simp]: "v' = CU nm' vs'" "vs  vs'"
            using vv' by(rule Red_ml.cases) auto
          obtain v' k where [arith]: "k<size vs" and "vs!k  v'"
            and [simp]: "vs' = vs[k := v']"
            using Red_ml_list_nth[OF vsvs'] by fastforce
          show ?thesis (is "rs'. ?P rs'  ?Q rs'")
          proof
            let ?rs' = "map dterm ((map term (rev vs) @ ts'')[(size vs - k - 1):=term v'])"
            have "?P ?rs'" using ob 5
              by(simp add: list_update_append map_update[symmetric] rev_update)
            moreover have "?Q ?rs'"
              apply rule
              apply(rule "1.hyps"[OF _ ob(3)])
              using "1.prems" 5 ob
              apply (auto simp:nth_append rev_nth ctxt_term[OF vs!k  v'] simp del: map_map)
              done
            ultimately show "?P ?rs'  ?Q ?rs'" ..
          qed
        next
          case (7 nm'' k r' ts'')
          show ?thesis (is "rs'. ?P rs'")
          proof
            show "?P(map dterm (ts''[k := r']))"
              using 7 ob
              apply clarsimp
              apply(rule "1.hyps"[OF _ ob(3)])
              using 7 "1.prems" ob apply auto
              done
          qed
        next
          case (9 v k r' ts'')
          then obtain vs where [simp]: "v = CU nm' vs" "rs' = map dtermML (rev vs) @ map dterm ts''"
            using ob by(cases v) auto
          show ?thesis (is "rs'. ?P rs'  ?Q rs'")
          proof
            let ?rs' = "map dterm ((map term (rev vs) @ ts'')[k+size vs:=r'])"
            have "?P ?rs'" using ob 9 by (auto simp: list_update_append)
            moreover have "?Q ?rs'"
              apply rule
              apply(rule "1.hyps"[OF _ ob(3)])
              using 9 "1.prems" ob by (auto simp:nth_append simp del: map_map)
            ultimately show "?P ?rs'  ?Q ?rs'" ..
          qed
        qed (insert ob, auto simp del: map_map)
      }
      hence "rs'. dterm (ts[i := t'] ! j) = C nm' ∙∙ rs'  (nm = nm'  no_match rs rs')"
        using i < size ts ob by(simp add:nth_list_update)
      hence "?P j" using ob by auto
      moreover have "j < ?m" using j < length ts j < size ps by simp
      ultimately show ?thesis by blast
    qed
  qed
qed

declare [[simp_depth_limit = 50]]

lemma Red_term_pres_no_match_it:
  "  i < length ts. (ts ! i, ts' ! i) : Red_term ^^ (ns!i);
    size ts' = size ts; size ns = size ts;
    no_match ps (map dterm ts)
    no_match ps (map dterm ts')"
proof(induct "sum_list ns" arbitrary: ts ns)
  case 0
  hence "i < size ts. ns!i = 0" by simp
  with 0 show ?case by simp (metis nth_equalityI)
next
  case (Suc n)
  then have "sum_list ns  0" by arith
  then obtain k l where "k<size ts" and [simp]: "ns!k = Suc l"
    by simp (metis length ns = length ts gr0_implies_Suc in_set_conv_nth)
  let ?ns = "ns[k := l]"
  have "n = sum_list ?ns" using Suc n = sum_list ns k<size ts size ns = size ts
    by (simp add:sum_list_update)
  obtain t' where "ts!k  t'" "(t', ts'!k) : Red_term^^l"
    using Suc(3) k<size ts size ns = size ts ns!k = Suc l
    by (metis relpow_Suc_E2)
  then have 1: "i<size(ts[k:=t']). (ts[k:=t']!i, ts'!i) : Red_term^^(?ns!i)"
    using Suc(3) k<size ts size ns = size ts
    by (auto simp add:nth_list_update)
  note nm1 = Red_term_pres_no_match[OF k<size ts ts!k  t' no_match ps (map dterm ts)]
  show ?case by(rule Suc(1)[OF n = sum_list ?ns 1 _ _ nm1])
               (simp_all add: size ts' = size ts size ns = size ts)
qed


lemma Red_term_pres_no_match_star:
assumes "i < length(ts::tm list). ts ! i ⇒* ts' ! i" and "size ts' = size ts"
    and "no_match ps (map dterm ts)"
shows "no_match ps (map dterm ts')"
proof-
  let ?P = "%ns. size ns = size ts 
   (i < length ts.(ts!i, ts'!i) : Red_term^^(ns!i))"
  have "ns. ?P ns" using assms(1)
    by(subst Skolem_list_nth[symmetric])
      (simp add:rtrancl_power)
  from someI_ex[OF this] show ?thesis
    by(fast intro: Red_term_pres_no_match_it[OF _ assms(2) _ assms(3)])
qed

lemma not_pure_term[simp]: "¬ pure(term v)"
proof
  assume "pure(term v)" thus False
    by cases
qed

abbreviation RedMLs :: "tm list  tm list  bool" (infix [⇒*] 50) where
"ss [⇒*] ts    size ss = size ts  (i<size ss. ss!i ⇒* ts!i)"


fun C_U_args :: "tm  tm list" (CU'_args) where
"CU_args(s  t) = CU_args s @ [t]" |
"CU_args(term(CU nm vs)) = map term (rev vs)" |
"CU_args _ = []"

lemma [simp]: "CU_args(C nm ∙∙ ts) = ts"
by (induct ts rule:rev_induct) auto

lemma redts_term_cong: "v ⇒* v'  term v ⇒* term v'"
apply(erule converse_rtrancl_induct)
apply(rule rtrancl_refl)
apply(fast intro: converse_rtrancl_into_rtrancl dest: ctxt_term)
done

lemma C_Red_term_ML:
  "v  v'  C_normalML v  dtermML v = C nm ∙∙ ts
    dtermML v' = C nm ∙∙ map dterm (CU_args(term v')) 
      CU_args(term v) [⇒*] CU_args(term v') 
      ts = map dterm (CU_args(term v))" and
  "(vs:: ml list)  vs'  i < length vs  vs ! i ⇒* vs' ! i"
apply(induct arbitrary: nm ts and i rule:Red_ml_Red_ml_list.inducts)
apply(simp_all add:Red_ml_list_length del: map_map)
  apply(frule Red_ml_list_length)
  apply(simp add: redts_term_cong rev_nth del: map_map)
 apply(simp add:nth_Cons' r_into_rtrancl del: map_map)
apply(simp add:nth_Cons')
done


lemma C_normal_subterm:
  "C_normal t  dterm t = C nm ∙∙ ts  s  set(CU_args t)  C_normal s"
apply(induct rule: C_normal.induct)
apply auto
apply(case_tac v)
apply auto
done

lemma C_normal_subterms:
  "C_normal t  dterm t = C nm ∙∙ ts  ts = map dterm (CU_args t)"
apply(induct rule: C_normal.induct)
apply auto
apply(case_tac v)
apply auto
done

lemma C_redt: "t  t'  C_normal t  
    C_normal t'  (dterm t = C nm ∙∙ ts 
    (ts'. ts' = map dterm (CU_args t')  dterm t' = C nm ∙∙ ts' 
     CU_args t [⇒*] CU_args t'))"
apply(induct arbitrary: ts nm rule:Red_term_hnf_induct)
apply (simp_all del: map_map)
   apply (metis no_match_R_coincide rev_rev_ident)
  apply rule
   apply (metis C_normal_ML_inv)
  apply clarify
  apply(drule (2) C_Red_term_ML)
  apply clarsimp
 apply clarsimp
 apply (metis insert_iff subsetD set_update_subset_insert)
apply clarsimp
apply(rule)
 apply (metis insert_iff subsetD set_update_subset_insert)
apply rule
 apply clarify
 apply(drule bspec, assumption)
 apply simp
 apply(subst no_match.simps)
 apply(subst (asm) no_match.simps)
 apply clarsimp
 apply(rename_tac j nm nm' rs rs')
 apply(rule_tac x=j in exI)
 apply simp
 apply(case_tac "i=j")
  apply(erule_tac x=rs' in meta_allE)
  apply(erule_tac x=nm' in meta_allE)
  apply (clarsimp simp: all_set_conv_all_nth)
  apply(metis C_normal_subterms Red_term_pres_no_match_star)
 apply (auto simp:nth_list_update)
done


lemma C_redts: "t ⇒* t'  C_normal t 
    C_normal t'  (dterm t = C nm ∙∙ ts 
    (ts'. dterm t' = C nm ∙∙ ts'  CU_args t [⇒*] CU_args t' 
     ts' = map dterm (CU_args t')))"
apply(induct arbitrary: nm ts rule:converse_rtrancl_induct)
apply simp
using tm_vector_cases[of t']
apply(elim disjE)
apply clarsimp
apply clarsimp
apply clarsimp
apply clarsimp
apply(case_tac v)
apply simp
apply simp
apply simp
apply simp
apply clarsimp
apply simp
apply simp
apply simp
apply simp
apply(frule_tac nm=nm and ts="ts" in C_redt)
apply assumption
apply clarify
apply rule
apply metis
apply clarify
apply simp
apply rule
apply (metis rtrancl_trans)
done

lemma no_match_preserved:
  "tset ts. C_normal t  ts [⇒*] ts'
    no_match ps os  os = map dterm ts  no_match ps (map dterm ts')"
proof(induct ps os arbitrary: ts ts' rule: no_match.induct)
  case (1 ps os)
  obtain i nm nm' ps' os' where a: "ps!i = C nm  ∙∙ ps'" "i < size ps"
      "i < size os" "os!i = C nm' ∙∙ os'" "nm=nm'  no_match ps' os'"
    using 1(4) no_match.simps[of ps os] by fastforce
  note 1(5)[simp]
  have "C_normal (ts ! i)" using 1(2) i < size os by auto
  have "ts!i ⇒* ts'!i" using 1(3) i < size os by auto
  have "dterm (ts ! i) = C nm' ∙∙ os'" using os!i = C nm' ∙∙ os' i < size os
    by (simp add:nth_map)
  with C_redts [OF ts!i ⇒* ts'!i C_normal (ts!i)]
    C_normal_subterm[OF C_normal (ts!i)]
    C_normal_subterms[OF C_normal (ts!i)]
  obtain ss' rs rs' :: "tm list" where b: "tset rs. C_normal t"
    "dterm (ts' ! i) = C nm' ∙∙ ss'" "length rs = length rs'"
    "i<length rs. rs ! i ⇒* rs' ! i" "ss' = map dterm rs'" "os' = map dterm rs"
    by fastforce
  show ?case
    apply(subst no_match.simps)
    apply(rule_tac x=i in exI)
    using 1(2-5) a b
    apply clarsimp
    apply(rule 1(1)[of i nm' _ nm' "map dterm rs" rs])
    apply simp_all
    done
qed

lemma Lam_Red_term_itE:
  "(Λ t, t') : Red_term^^i  t''. t' = Λ t''  (t,t'') : Red_term^^i"
apply(induct i arbitrary: t')apply simp
apply(erule relpow_Suc_E)
apply(erule Red_term.cases)
apply (simp_all)
apply blast+
done


lemma Red_term_it: "(V x ∙∙ rs, r) : Red_term^^i
   ts is. r = V x ∙∙ ts  size ts = size rs & size is = size rs 
       (j<size ts. (rs!j, ts!j) : Red_term^^(is!j)  is!j <= i)"
proof(induct i arbitrary:rs)
  case 0
  moreover
  have "is. length is = length rs 
   (j<size rs. (rs!j, rs!j)  Red_term ^^ is!j  is!j = 0)" (is "is. ?P is")
  proof
    show "?P(replicate (size rs) 0)" by simp
  qed
  ultimately show ?case by auto
next
  case (Suc i rs)
  from (V x ∙∙ rs, r)  Red_term ^^ Suc i
  obtain r' where r': "V x ∙∙ rs  r'" and "(r',r)  Red_term ^^ i"
    by (metis relpow_Suc_D2)
  from r' have "k<size rs. s. rs!k  s  r' = V x ∙∙ rs[k:=s]"
  proof(induct rs arbitrary: r' rule:rev_induct)
    case Nil thus ?case by(fastforce elim: Red_term.cases)
  next
    case (snoc r rs)
    hence "(V x ∙∙ rs)  r  r'" by simp
    thus ?case
    proof(cases rule:Red_term.cases)
      case (ctxt_At1 s')
      then obtain k s'' where aux: "k<length rs" "rs ! k  s''" "s' = V x ∙∙ rs[k := s'']"
        using snoc(1) by force
      show ?thesis (is "k < ?n. s. ?P k s")
      proof-
        have "k<?n  ?P k s''" using ctxt_At1 aux
          by (simp add:nth_append) (metis last_snoc butlast_snoc list_update_append1)
        thus ?thesis by blast
      qed
    next
      case (ctxt_At2 t')
      show ?thesis (is "k < ?n. s. ?P k s")
      proof-
        have "size rs<?n  ?P (size rs) t'" using ctxt_At2 by simp
        thus ?thesis by blast
      qed
    qed
  qed
  then obtain k s where "k<size rs" "rs!k  s" and [simp]: "r' = V x ∙∙ rs[k:=s]" by metis
  from Suc(1)[of "rs[k:=s]"] (r',r)  Red_term ^^ i
  show ?case using k<size rs rs!k  s
    apply auto
    apply(rule_tac x="is[k := Suc(is!k)]" in exI)
    apply (auto simp:nth_list_update)
    apply(erule_tac x=k in allE)
    apply auto
    apply (metis relpow_Suc_I2 relpow.simps(2))
    done
qed

lemma C_Red_term_it:  "(C nm ∙∙ rs, r) : Red_term^^i
   ts is. r = C nm ∙∙ ts  size ts = size rs  size is = size rs 
        (j<size ts. (rs!j, ts!j)  Red_term^^(is!j)  is!j  i)"
proof(induct i arbitrary:rs)
  case 0
  moreover
  have "is. length is = length rs 
   (j<size rs. (rs!j, rs!j)  Red_term ^^ is!j  is!j = 0)" (is "is. ?P is")
  proof
    show "?P(replicate (size rs) 0)" by simp
  qed
  ultimately show ?case by auto
next
  case (Suc i rs)
  from (C nm ∙∙ rs, r)  Red_term ^^ Suc i
  obtain r' where r': "C nm ∙∙ rs  r'" and "(r',r)  Red_term ^^ i"
    by (metis relpow_Suc_D2)
  from r' have "k<size rs. s. rs!k  s  r' = C nm ∙∙ rs[k:=s]"
  proof(induct rs arbitrary: r' rule:rev_induct)
    case Nil thus ?case by(fastforce elim: Red_term.cases)
  next
    case (snoc r rs)
    hence "(C nm ∙∙ rs)  r  r'" by simp
    thus ?case
    proof(cases rule:Red_term.cases)
      case (ctxt_At1 s')
      then obtain k s'' where aux: "k<length rs" "rs ! k  s''" "s' = C nm ∙∙ rs[k := s'']"
        using snoc(1) by force
      show ?thesis (is "k < ?n. s. ?P k s")
      proof-
        have "k<?n  ?P k s''" using ctxt_At1 aux
          by (simp add:nth_append) (metis last_snoc butlast_snoc list_update_append1)
        thus ?thesis by blast
      qed
    next
      case (ctxt_At2 t')
      show ?thesis (is "k < ?n. s. ?P k s")
      proof-
        have "size rs<?n  ?P (size rs) t'" using ctxt_At2 by simp
        thus ?thesis by blast
      qed
    qed
  qed
  then obtain k s where "k<size rs" "rs!k  s" and [simp]: "r' = C nm ∙∙ rs[k:=s]" by metis
  from Suc(1)[of "rs[k:=s]"] (r',r)  Red_term ^^ i
  show ?case using k<size rs rs!k  s
    apply auto
    apply(rule_tac x="is[k := Suc(is!k)]" in exI)
    apply (auto simp:nth_list_update)
    apply(erule_tac x=k in allE)
    apply auto
    apply (metis relpow_Suc_I2 relpow.simps(2))
    done
qed


lemma pure_At[simp]: "pure(s  t)  pure s  pure t"
by(fastforce elim: pure.cases)

lemma pure_foldl_At[simp]: "pure(s ∙∙ ts)  pure s  (tset ts. pure t)"
by(induct ts arbitrary: s) auto

lemma nbe_C_normal_ML:
  assumes "term v ⇒* t'" "C_normalML v" "pure t'" shows "normal t'"
proof -
  { fix t t' i v
    assume "(t,t') : Red_term^^i"
    hence "t = term v  C_normalML v  pure t'  normal t'"
    proof(induct i arbitrary: t t' v rule:less_induct)
    case (less k)
    show ?case
    proof (cases k)
      case 0 thus ?thesis using less by auto
    next
      case (Suc i)
      then obtain i' s where "t  s" and red: "(s,t') : Red_term^^i'" and [arith]: "i' <= i"
        by (metis eq_imp_le less(5) Suc relpow_Suc_D2)
      hence "term v  s" using Suc less by simp
      thus ?thesis
      proof cases
        case (term_C nm vs)
        with less have 0:"no_match_compR nm vs" by auto
        let ?n = "size vs"
        have 1: "(C nm ∙∙ map term (rev vs),t') : Red_term^^i'"
          using term_C (s,t') : Red_term^^i' by simp
        with C_Red_term_it[OF 1] 
        obtain ts ks where [simp]: "t' = C nm ∙∙ ts"
          and sz: "size ts = ?n  size ks = ?n 
          (i<?n. (term((rev vs)!i), ts!i) : Red_term^^(ks!i)  ks ! i  i')"
          by(auto cong:conj_cong)
        have pure_ts: "tset ts. pure t" using pure t' by simp
        { fix i assume "i<size vs"
          moreover hence "(term((rev vs)!i), ts!i) : Red_term^^(ks!i)" by(metis sz)
          ultimately have "normal (ts!i)"
            apply -
            apply(rule less(1))
            prefer 5 apply assumption
            using sz Suc apply fastforce
            apply(rule refl)
            using less term_C
            apply(auto)
            apply (metis in_set_conv_nth length_rev set_rev)
            apply (metis in_set_conv_nth pure_ts sz)
            done
        } note 2 = this
        have 3: "no_match_R nm (map dterm (map term (rev vs)))"
          apply(subst map_dterm_term)
          apply(rule no_match_R_coincide) using 0 by simp
        have 4: "map term (rev vs) [⇒*] ts"
        proof -
          have "(C nm ∙∙ map term (rev vs),t'): Red_term^^i'"
            using red term_C by auto
          from C_Red_term_it[OF this] obtain ts' "is" where "t' = C nm  ∙∙ ts'"
            and "length ts' = ?n  length is =?n 
              (j< ?n. (map term (rev vs) ! j, ts' ! j)  Red_term ^^ is ! j  is ! j  i')"
            using sz by auto
          from t' = C nm ∙∙ ts' t' = C nm ∙∙ ts have "ts = ts'" by simp
          show ?thesis using sz by (auto  simp: rtrancl_is_UN_relpow)
        qed
        have 5: "tset(map term vs). C_normal t"
          using less term_C by auto
        have "no_match_R nm (map dterm ts)"
          apply auto
          apply(subgoal_tac "no_match aa (map dterm (map term (rev vs)))")
          prefer 2
          using 3 apply blast 
          using 4 5 no_match_preserved[OF _ _ _ refl, of "map term (rev vs)" "ts"] by simp
        hence 6: "no_match_R nm ts" by(metis map_dterm_pure[OF pure_ts])
        then show "normal t'"
          apply(simp)
          apply(rule normal.intros(3))
          using 2 sz apply(fastforce simp:set_conv_nth)
          apply auto
          apply(subgoal_tac "no_match aa (take (size aa) ts)")
          apply (metis no_match)
          apply(fastforce intro:no_match_take)
          done
      next
        case (term_V x vs)
        let ?n = "size vs"
        have 1: "(V x ∙∙ map term (rev vs),t') : Red_term^^i'"
          using term_V (s,t') : Red_term^^i' by simp
        with Red_term_it[OF 1] obtain ts "is" where [simp]: "t' = V x ∙∙ ts"
          and 2: "length ts = ?n 
            length is = ?n  (j<?n. (term (rev vs ! j), ts ! j)  Red_term ^^ is ! j 
            is ! j  i')"
          by (auto cong:conj_cong)
        have "j<?n. normal(ts!j)"
        proof(clarify)
          fix j assume 0: "j < ?n"
          then have "is!j < k" using k=Suc i 2 by auto
          have red: "(term (rev vs ! j), ts ! j)  Red_term ^^ is ! j" using j < ?n 2 by auto
          have pure: "pure (ts ! j)" using pure t' 0 2 by auto
          have Cnm: "C_normalML (rev vs ! j)" using less term_V
            by simp (metis 0 in_set_conv_nth length_rev set_rev)
          from less(1)[OF is!j < k refl Cnm pure red] show "normal(ts!j)" .
        qed
        note 3=this
        show ?thesis by simp (metis normal.intros(1) in_set_conv_nth 2 3)
      next
        case (term_Clo f vs n)
        let ?u = "apply (lift 0 (Clo f vs n)) (VU 0 [])"
        from term_Clo (s,t') : Red_term^^i'
        obtain t'' where [simp]: "t' = Λ t''" and 1: "(term ?u, t'') : Red_term^^i'"
          by(metis Lam_Red_term_itE)
        have "i' < k" using k = Suc i by arith
        have "pure t''" using pure t' by simp
        have "C_normalML ?u" using less term_Clo by(simp)
        from less(1)[OF i' < k refl C_normalML ?u pure t'' 1]
        show ?thesis by(simp add:normal.intros)
      next
        case (ctxt_term u')
        have "i' < k" using k = Suc i by arith
        have "C_normalML u'" by (rule C_normal_ML_inv) (insert less ctxt_term, simp_all)
        have "(term u', t')  Red_term ^^ i'" using red ctxt_term by auto
        from less(1)[OF i' < k refl C_normalML u' pure t' this] show ?thesis .
      qed
    qed
  qed
  }
  thus ?thesis using assms(2-) rtrancl_imp_relpow[OF assms(1)] by blast
qed

lemma C_normal_ML_compile:
  "pure t  i. C_normalML(σ i)  C_normalML (compile t σ)"
by(induct t arbitrary: σ) (simp_all add: C_normal_ML_lift_ML)

corollary nbe_normal:
  "pure t  term(comp_fixed t) ⇒* t'  pure t'  normal t'"
apply(erule nbe_C_normal_ML)
apply(simp add: C_normal_ML_compile)
apply assumption
done

section‹Refinements›

text‹We ensure that all occurrences of @{term "CU nm vs"} satisfy
the invariant @{prop"size vs = arity nm"}.›

text‹A constructor value:›

fun CUs :: "ml  bool" where
"CUs(CU nm vs) = (size vs = arity nm  (vset vs. CUs v))" |
"CUs _ = False"

lemma size_foldl_At: "size(C nm ∙∙ ts) = size ts + sum_list(map size ts)"
by(induct ts rule:rev_induct) auto


lemma termination_linpats:
  "i < length ts  ts!i = C nm ∙∙ ts'
    length ts' + sum_list (map size ts') < length ts + sum_list (map size ts)"
apply(subgoal_tac "C nm ∙∙ ts' : set ts")
 prefer 2 apply (metis in_set_conv_nth)
apply(drule sum_list_map_remove1[of _ _ size])
apply(simp add:size_foldl_At)
apply (metis gr_implies_not0 length_0_conv)
done

text‹Linear patterns:›

function linpats :: "tm list  bool" where
"linpats ts 
 (i<size ts. (x. ts!i = V x) 
    (nm ts'. ts!i = C nm ∙∙ ts'  arity nm = size ts'  linpats ts')) 
 (i<size ts. j<size ts. ij  fv(ts!i)  fv(ts!j) = {})"
by pat_completeness auto
termination
apply(relation "measure(%ts. size ts + (SUM t<-ts. size t))")
apply (auto simp:termination_linpats)
done

declare linpats.simps[simp del]

(* FIXME move *)
lemma eq_lists_iff_eq_nth:
  "size xs = size ys  (xs=ys) = (i<size xs. xs!i = ys!i)"
by (metis nth_equalityI)

lemma pattern_subst_ML_coincidence:
 "pattern t  ifv t. σ i = σ' i
   subst_ML σ (comp_pat t) = subst_ML σ' (comp_pat t)"
by(induct pred:pattern) auto

lemma linpats_pattern: "linpats ts  patterns ts"
proof(induct ts rule:linpats.induct)
  case (1 ts)
  show ?case
  proof
    fix t assume "t : set ts"
    then obtain i where "i < size ts" and [simp]: "t = ts!i"
      by (auto simp: in_set_conv_nth)
    hence "(x. t = V x)  (nm ts'. t = C nm ∙∙ ts'  arity nm = size ts' & linpats ts')"
      (is "?V | ?C")
      using 1(2) by(simp add:linpats.simps[of ts])
    thus "pattern t"
    proof
      assume "?V" thus ?thesis by(auto simp:pat_V)
    next
      assume "?C" thus ?thesis using 1(1) i < size ts
        by auto (metis pat_C)
    qed
  qed
qed

lemma no_match_ML_swap_rev:
  "length ps = length vs  no_matchML ps (rev vs)  no_matchML (rev ps) vs"
apply(clarsimp simp: no_match_ML.simps[of ps] no_match_ML.simps[of _ vs])
apply(rule_tac x="size ps - i - 1" in exI)
apply (fastforce simp:rev_nth)
done

lemma no_match_ML_aux:
  "v  set cvs. CUs v  linpats ps  size ps = size cvs 
  σ. map (substML σ) (map comp_pat ps)  cvs 
  no_matchML (map comp_pat ps) cvs"
apply(induct ps arbitrary: cvs rule:linpats.induct)
apply(frule linpats_pattern)
apply(subst (asm) linpats.simps) back
apply auto
apply(case_tac "i<size ts. σ. substML σ (comp_pat (ts!i)) = cvs!i")
 apply(clarsimp simp:Skolem_list_nth)
 apply(rename_tac "σs")
 apply(erule_tac x="%x. (σs!(THE i. i<size ts & x : fv(ts!i)))x" in allE)
 apply(clarsimp simp:eq_lists_iff_eq_nth)
 apply(rotate_tac -3)
 apply(erule_tac x=i in allE)
 apply simp
 apply(rotate_tac -1)
 apply(drule sym)
 apply simp
 apply(erule contrapos_np)
 apply(rule pattern_subst_ML_coincidence)
  apply (metis in_set_conv_nth)
 apply clarsimp
 apply(rule_tac a=i in theI2)
   apply simp
  apply (metis disjoint_iff_not_equal)
 apply (metis disjoint_iff_not_equal)
apply clarsimp
apply(subst no_match_ML.simps)
apply(rule_tac x="size ts - i - 1" in exI)
apply simp
apply rule
 apply simp
apply(subgoal_tac "¬(x. ts!i = V x)")
 prefer 2
 apply fastforce
apply(subgoal_tac "nm ts'. ts!i = C nm ∙∙ ts' & size ts' = arity nm & linpats ts'")
 prefer 2
 apply fastforce
apply clarsimp
apply(rule_tac x=nm in exI)
apply(subgoal_tac "nm' vs'. cvs!i = CU nm' vs' & size vs' = arity nm' & (v'  set vs'. CUs v')")
 prefer 2
 apply(drule_tac x="cvs!i" in bspec)
  apply simp
   apply(case_tac "cvs!i")
apply simp_all
apply (clarsimp simp:rev_nth rev_map[symmetric])
apply(erule_tac x=i in meta_allE)
apply(erule_tac x=nm' in meta_allE)
apply(erule_tac x="ts'" in meta_allE)
apply(erule_tac x="rev vs'" in meta_allE)
apply simp
apply(subgoal_tac "no_matchML (map comp_pat ts') (rev vs')")
 apply(rule no_match_ML_swap_rev)
  apply simp
 apply assumption
apply(erule_tac meta_mp)
apply (metis rev_rev_ident)
done



(*<*)
end
(*>*)