Quelle  NBE.thy

(*  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 (‹C_ML›) (* ref to compiled code *)
| V_ML ml_vname (‹V_ML›)
| A_ML ml "(ml list)" (‹A_ML›)
| Lam_ML ml (‹Lam_ML›)
 ― ‹the universal datatype›
| C_U cname "(ml list)"
| V_U 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(s∙t)"

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" (‹closed_ML›) where
"closed_ML i (C_ML nm) = True" |
"closed_ML i (V_ML X) = (X<i)"  |
"closed_ML i (A_ML v vs) = (closed_ML i v ∧ (∀v ∈ set vs. closed_ML i v))" |
"closed_ML i (Lam_ML v) = closed_ML (i+1) v" |
"closed_ML i (C_U nm vs) = (∀v ∈ set vs. closed_ML i v)" |
"closed_ML i (V_U nm vs) = (∀v ∈ set vs. closed_ML i v)" |
"closed_ML i (Clo f vs n) = (closed_ML i f ∧ (∀v ∈ set vs. closed_ML i v))" |
"closed_ML i (apply v w) = (closed_ML i v ∧ closed_ML i w)"

fun closed_tm_ML :: "nat ==> tm ==> bool" (‹closed_ML›) where
"closed_tm_ML i (r∙s) = (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" (‹fv_ML›) where
"fv_ML (C_ML nm) = {}" |
"fv_ML (V_ML X) = {X}"  |
"fv_ML (A_ML v vs) = fv_ML v ∪ (∪v ∈ set vs. fv_ML v)" |
"fv_ML (Lam_ML v) = {X. Suc X : fv_ML v}" |
"fv_ML (C_U nm vs) = (∪v ∈ set vs. fv_ML v)" |
"fv_ML (V_U nm vs) = (∪v ∈ set vs. fv_ML v)" |
"fv_ML (Clo f vs n) = fv_ML f ∪ (∪v ∈ set vs. fv_ML v)" |
"fv_ML (apply v w) = fv_ML v ∪ fv_ML 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 ∪ (∪t∈set ts. fv t)"
by(induct ts arbitrary:t) auto


subsection "Lifting and Substitution"

fun lift_ml :: "nat ==> ml ==> ml" (‹lift›) where
"lift i (C_ML nm) = C_ML nm" |
"lift i (V_ML X) = V_ML X" |
"lift i (A_ML v vs) = A_ML (lift i v) (map (lift i) vs)" |
"lift i (Lam_ML v) = Lam_ML (lift i v)" |
"lift i (C_U nm vs) = C_U nm (map (lift i) vs)" |
"lift i (V_U x vs) = V_U (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 (s∙t) = (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" (‹lift_ML›) where
"lift_ML i (C_ML nm) = C_ML nm" |
"lift_ML i (V_ML X) = V_ML (if X < i then X else X+1)" |
"lift_ML i (A_ML v vs) = A_ML (lift_ML i v) (map (lift_ML i) vs)" |
"lift_ML i (Lam_ML v) = Lam_ML (lift_ML (i+1) v)" |
"lift_ML i (C_U nm vs) = C_U nm (map (lift_ML i) vs)" |
"lift_ML i (V_U x vs) = V_U x (map (lift_ML i) vs)" |
"lift_ML i (Clo v vs n) = Clo (lift_ML i v) (map (lift_ML i) vs) n" |
"lift_ML i (apply u v) = apply (lift_ML i u) (lift_ML 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 ==> lift_ML 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 σ (s∙t) = (subst σ s) ∙ (subst σ t)"

fun subst_ML :: "(nat ==> ml) ==> ml ==> ml" (‹subst_ML›) where
"subst_ML σ (C_ML nm) = C_ML nm" |
"subst_ML σ (V_ML X) = σ X" |
"subst_ML σ (A_ML v vs) = A_ML (subst_ML σ v) (map (subst_ML σ) vs)" |
"subst_ML σ (Lam_ML v) = Lam_ML (subst_ML (V_ML 0 ## σ) v)" |
"subst_ML σ (C_U nm vs) = C_U nm (map (subst_ML σ) vs)" |
"subst_ML σ (V_U x vs) = V_U 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)"
(* 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 V_ML n else if n=k then v else V_ML(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] ≡ subst_ML (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 lift_ML 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 ==> lift_ML (Suc k) (lift_ML i v) = lift_ML i (lift_ML k v)"
by(induct v arbitrary: i rule:lift_ML.induct)
  simp_all

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

lemma V_ML_cons_ML_subst_decr[simp]:
  "V_ML 0 ## subst_decr_ML k v = subst_decr_ML (Suc k) (lift_ML 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 ==> subst_ML σ v = subst_ML σ' 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]: "(V_ML 0 ## V_ML) = V_ML"
by(rule ext) simp

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

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

lemma lift_subst_ML:
 "lift k (subst_ML σ v) = subst_ML (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:
 "lift_ML k (subst_ML σ v) =
  subst_ML (λi. if i<k then lift_ML k (σ i) else if i=k then V_ML k else lift_ML k (σ(i - 1))) (lift_ML k v)"
  (is "_ = subst_ML (?insrt k σ) (lift_ML k v)")
apply (induct k v arbitrary: σ k rule: lift_ML.induct)
apply (simp_all add: o_assoc lift_o_shift)
apply(subgoal_tac "V_ML 0 ## ?insrt k σ = ?insrt (Suc k) (V_ML 0 ## σ)")
 apply simp
apply (simp add:fun_eq_iff lift_lift_ML cons_ML_def split:nat.split)
done

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

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

lemma subst_ML_id:
  "closed_ML k v ==> ∀i<k. σ i = V_ML i ==> subst_ML σ 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]: "closed_ML 0 v ==> subst_ML σ v = v"
using subst_ML_id[where k=0] by simp

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

lemma subst_ML_comp:
  "subst_ML σ (subst_ML σ' v) = subst_ML (subst_ML σ ∘ σ') 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 = subst_ML σ (σ' i) ==> subst_ML σ (subst_ML σ' v) = subst_ML σ'' v"
by(simp add:subst_ML_comp subst_ML_ext)

lemma closed_tm_ML_foldl_At:
  "closed_ML k (t ∙∙ ts) ⟷ closed_ML k t ∧ (∀t ∈ set ts. closed_ML k t)"
by(induct ts arbitrary: t) simp_all

lemma closed_ML_lift[simp]:
  fixes v :: ml shows "closed_ML k v ==> closed_ML 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: "closed_ML n v ==> closed_ML (Suc n) (lift_ML k v)"
by (induct k v arbitrary: n rule: lift_ML.induct) simp_all

lemma closed_ML_subst_ML:
  "∀i. closed_ML k (σ i) ==> closed_ML k (subst_ML σ v)"
by(induct σ v arbitrary: k rule: subst_ML.induct) (auto simp: closed_ML_Suc)

lemma closed_ML_subst_ML2:
  "closed_ML k v ==> ∀i<k. closed_ML l (σ i) ==> closed_ML l (subst_ML σ 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) ==>
   ∀i≥k. σ'(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 ≡ ∀t∈set 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
  actual definition is given in \S\ref{sec:Compiler} below.›

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

lemma termination_no_match_ML:
  "i < length ps ==> rev ps ! i = C_U nm vs
   ==> sum_list (map size vs) < sum_list (map size ps)"
apply(subgoal_tac "C_U 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'_match_ML›) where
"no_match_ML ps os =
  (∃i < min (size os) (size ps).
   ∃nm nm' vs vs'. (rev ps)!i = C_U nm vs ∧ (rev os)!i = C_U nm' vs' ∧
      (nm=nm' ⟶ no_match_ML vs vs'))"
by pat_completeness auto
termination
apply(relation "measure(%(vs::ml list,_). ∑v←vs. size v)")
apply (auto simp:termination_no_match_ML)
done


abbreviation
"no_match_compR nm os ≡
  ∀(nm',ps,v)∈ compR. nm=nm' ⟶ no_match_ML 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›
| "A_ML (Lam_ML u) [v] ==> u[v/0]"
 ― ‹Execution of a compiled rewrite rule›
| "(nm,vs,v) : compR ==> ∀ i. closed_ML 0 (σ i) ==>
   A_ML (C_ML nm) (map (subst_ML σ) vs) ==> subst_ML σ v"
― ‹default rule:›
| "∀i. closed_ML 0 (σ i)
   ==> vs = map V_ML [0..<arity nm] ==> vs' = map (subst_ML σ) vs
   ==> no_match_compR nm vs'
   ==> A_ML (C_ML nm) vs' ==> subst_ML σ (C_U nm vs)"
 ― ‹Equations for function \texttt{apply}›
| apply_Clo1: "apply (Clo f vs (Suc 0)) v ==> A_ML f (v # vs)"
| apply_Clo2: "n > 0 ==>
 apply (Clo f vs (Suc n)) v ==> Clo f (v # vs) n"
| apply_C: "apply (C_U nm vs) v ==> C_U nm (v # vs)"
| apply_V: "apply (V_U x vs) v ==> V_U x (v # vs)"
 ― ‹Context rules›
| ctxt_C: "vs ==> vs' ==> C_U nm vs ==> C_U nm vs'"
| ctxt_V: "vs ==> vs' ==> V_U x vs ==> V_U 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' ==> A_ML f vs ==> A_ML f' vs"
| ctxt_A_ML2: "vs ==> vs' ==> A_ML f vs ==> A_ML 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 (C_U nm vs) ==> (C nm) ∙∙ (map term (rev vs))"
| term_V: "term (V_U x vs) ==> (V x) ∙∙ (map term (rev vs))"
| term_Clo: "term(Clo vf vs n) ==> Λ (term (apply (lift 0 (Clo vf vs n)) (V_U 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
  proof of the kernel function.›

fun size' :: "ml ==> nat" where
"size' (C_ML nm) = 1" |
"size' (V_ML X) = 1"  |
"size' (A_ML v vs) = (size' v + (∑v←vs. size' v))+1" |
"size' (Lam_ML v) = size' v + 1" |
"size' (C_U nm vs) = (∑v←vs. size' v)+1" |
"size' (V_U nm vs) = (∑v←vs. size' v)+1" |
"size' (Clo f vs n) = (size' f + (∑v←vs. 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' (lift_ML 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' (subst_ML σ 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
"(C_ML nm)! = C nm" |
"(A_ML v vs)! = v! ∙∙ (map kernel (rev vs))" |
"(Lam_ML v)! = Λ (((lift 0 v)[V_U 0 []/0])!)" |
"(C_U nm vs)! = (C nm) ∙∙ (map kernel (rev vs))" |
"(V_U x vs)! = (V x) ∙∙ (map kernel (rev vs))" |
"(Clo f vs n)! = f! ∙∙ (map kernel (rev vs))" |
"(apply v w)! = v! ∙ (w!)" |
"(V_ML 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 ==> ∀t∈set 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 "closed_ML 0 v ==> pure(v!)"
proof(induct v rule:kernel.induct)
  case (3 v)
  hence "closed_ML (Suc 0) (lift 0 v)" by simp
  then have "subst_ML (λn. V_U 0 []) (lift 0 v) = lift 0 v[V_U 0 []/0]"
    by(rule subst_ML_coincidence) simp
  moreover have "closed_ML 0 (subst_ML (λn. V_U 0 []) (lift 0 v))"
    by(simp add: closed_ML_subst_ML)
  ultimately have "closed_ML 0 (lift 0 v[V_U 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
  "closed_ML 0 v ==> subst V (v!) = v!"
by (metis pure_kernel subst_V)

lemma kernel_lift_tm: fixes v :: ml shows
  "closed_ML 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 V_U 0 [] else V_ML (n - 1)) = (λn. if n = 0 then V_U 0 [] else V_ML (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
  ‹kernel_subst1› below.›

fun subst_ml :: "(nat ==> nat) ==> ml ==> ml" where
"subst_ml σ (C_ML nm) = C_ML nm" |
"subst_ml σ (V_ML X) = V_ML X" |
"subst_ml σ (A_ML v vs) = A_ML (subst_ml σ v) (map (subst_ml σ) vs)" |
"subst_ml σ (Lam_ML v) = Lam_ML (subst_ml σ v)" |
"subst_ml σ (C_U nm vs) = C_U nm (map (subst_ml σ) vs)" |
"subst_ml σ (V_U x vs) = V_U (σ 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:
  "lift_ML k (subst_ml σ v) = subst_ml σ (lift_ML 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 σ (subst_ML σ' v) = subst_ML (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 σ' ∘ V_ML 0 ## σ) = V_ML 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:
  "closed_ML 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 V_U 0 [] else V_ML (n - 1)))
             = (λn. if n = 0 then V_U 0 [] else V_ML (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:
  "closed_ML 0 v ==> closed_ML (Suc 0) u ==>
   kernel(u[v/0]) = (kernel((lift 0 u)[V_U 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[lift_ML 0 v/Suc 0])[V_U 0 []/0] !)"
      by (simp cong:if_cong0)
    also have "… = Λ((lift 0 w)[lift_ML 0 (lift 0 v)/Suc 0][V_U 0 []/0]!)"
      by(simp only: lift_subst_ML1 lift_lift_ML_comm)
    also have "… = Λ(subst_ML (λn. if n=0 then V_U 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_comp2)
      using 3
      apply auto
      done
    also have "… = Λ((lift 0 w)[V_U 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)[V_U 0 []/0]))[V_U 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 "closed_ML (Suc(Suc 0)) w")
      defer
      using 3
      apply force
      apply(subgoal_tac  "closed_ML (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)[V_U 1 []/0])[V_U 0 []/0]![(lift 0 v)!/0])" (is "_ = ?M")
      apply(subgoal_tac "lift_ml 0 (lift_ml 0 w[V_U 0 []/0])[V_U 0 []/0] =
                         lift_ml 0 (lift_ml 0 w)[V_U 1 []/0][V_U 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[V_U 0 []/Suc 0])[V_U 0 []/0]!))"
      apply(subgoal_tac "(V_ML 0 ## (λn. if n = 0 then V_U 0 [] else V_ML (n - Suc 0))) = subst_decr_ML (Suc 0) (V_U 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))[V_U 1 []/Suc 0][V_U 0 []/0]!))"
      apply(subgoal_tac "lift 0 (lift 0 w[V_U 0 []/Suc 0]) = lift 0 (lift 0 w)[V_U 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))[V_U 1 []/Suc 0][V_U 0 []/0] =
               (lift 0 (lift_ml 0 w))[V_U 0 []/0][V_U 1 []/ 0]" (is "?l = ?r")
    proof -
      have "?l = subst_ML (λn. if n= 0 then V_U 0 [] else if n = 1 then V_U 1 [] else
                      V_ML (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)[V_U 0 []/0][V_U 1 []/0]!) =
    subst (subst_decr 0 (kernel(lift_ml 0 v))) (lift_ml 0 (lift_ml 0 w)[V_U 1 []/0][V_U 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)[V_U 0 []/0][V_U 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)[V_U 0 []/0][V_U 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)[V_U 0 []/0][V_U 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)[V_U 0 []/0][V_U 1 []/0]) =
             lift_ml 0 (lift_ml 0 w)[V_U 1 []/0][V_U 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 (C_ML nm) [] (arity nm) else A_ML (C_ML nm) [])"
| "compile (s ∙ t) σ = apply (compile s σ) (compile t σ)"
| "compile (Λ t) σ = Clo (Lam_ML (compile t (V_ML 0 ## σ))) [] 1"

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

definition "comp_open t = compile t V_ML"
abbreviation "comp_fixed t ≡ compile t (λi. V_U 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 ==> C_U nm (map comp_pat (rev (args_tm t)))
   | V X ==> V_ML X)"

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

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

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

lemma comp_pat_C_Nil[simp]: "comp_pat(C nm) = C_U 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 ==> fv_ML(comp_open t) = fv t"
by(induct t pred:pure) (simp_all add:comp_open_def)

lemma fv_ML_comp_pat: "pattern t ==> fv_ML(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 ∈ fv_ML (comp_open t')
   ==> ∃t∈set ts. x ∈ fv_ML(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 ∈ fv_ML v ==> ∃u∈set vs. x ∈ fv_ML 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 ==> subst_ML σ' (compile t σ) = compile t (subst_ML σ' o σ)"
apply(induct arbitrary: σ σ' pred:pure)
apply simp_all
apply(erule_tac x="V_ML 0 ## σ'" in meta_allE)
apply(erule_tac x= "V_ML 0 ## (lift_ML 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 = V_U 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 "(subst_ML (λn. if n = 0 then V_U 0 [] else V_ML (n - 1)) ∘
               (lift 0 ∘ V_ML 0 ## σ)) = (λa. V_U a [])")
apply(simp)
apply(rule ext)
apply(simp)
done

lemma kernel_subst_ML_pat:
  "pure t ==> pattern t ==> ∀i. closed_ML 0 (σ i) ==>
   (subst_ML σ (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. closed_ML 0 (σ i) ==>
   (subst_ML σ (comp_open t))! = subst (kernel ∘ σ) t"
proof(induct arbitrary: σ pred:pure)
  case (Lam t)
  have "lift 0 o V_ML = V_ML" by (simp add:fun_eq_iff)
  hence "(subst_ML σ (comp_open (Λ t)))! =
    Λ (subst_ML (lift 0 ∘ V_ML 0 ## σ) (comp_open t)[V_U 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. closed_ML 0 (σ i) ==>
   map kernel (map (subst_ML σ) (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. closed_ML 0 (σ i)
  ==> C nm ∙∙ (map (subst_ML σ) (rev vs))! →* (subst_ML σ 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' ==> closed_ML 0 v ==> v! →* v'! ∧ closed_ML 0 v'" and
  "vs ==> vs' ==> ∀v∈set vs. closed_ML 0 v ==>
   vs! →* vs'! ∧ (∀v'∈set vs'. closed_ML 0 v')"
proof(induct rule:Red_ml_Red_ml_list.inducts)
  fix u v
  let ?v = "A_ML (Lam_ML u) [v]"
  assume cl: "closed_ML 0 (A_ML (Lam_ML u) [v])"
  let ?u' = "(lift_ml 0 u)[V_U 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(A_ML (Lam_ML u) [v]) →* kernel(u[v/0])" (is ?A)
    by(rule r_into_rtrancl)
  moreover have "closed_ML 0 (u[v/0])" (is "?C")
  proof -
    let ?σ = "λn. if n = 0 then v else V_ML (n - 1)"
    let ?σ' = "λn. v"
    have clu: "closed_ML (Suc 0) u" and clv: "closed_ML 0 v" using cl by simp+
    have "closed_ML 0 (subst_ML ?σ' u)"
      by (metis closed_ML_subst_ML clv)
    hence "closed_ML 0 (subst_ML ?σ 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. closed_ML 0 (σ i)"  and compR: "(nm, vs, v) ∈ compR"
  have "map (subst V) (map (subst_ML σ) (rev vs)!) = map (subst_ML σ) (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 (subst_ML σ) (rev vs)) !) →* (subst_ML σ v)!"
    by(simp add:subst_V_kernel closed_ML_subst_ML[OF σ])
  hence "A_ML (C_ML nm) (map (subst_ML σ) vs)! →* subst_ML σ v!" (is ?A)
    by(simp add:rev_map)
  moreover
  have "closed_ML 0 (subst_ML σ 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' ==> closed_ML 0 t ==> kernelt t →* kernelt t' ∧ closed_ML 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)) (V_U 0 [])))!"
    using term_Clo
    by(simp del:lift_foldl_At add: r_into_rtrancl Red_tm.intros(2))
  moreover
  have "closed_ML 0 (Λ (term (apply (lift 0 (Clo vf vs n)) (V_U 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' ==> closed_ML 0 t ==> t! →* t'! ∧ closed_ML 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. closed_ML n (σ i) ==> closed_ML n (compile t σ)"
proof(induct arbitrary:n σ pred:pure)
  case (Lam t)
  have 1: "∀i. closed_ML (Suc n) ((V_ML 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: "closed_ML 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
"∀t∈set ts. normal t ==> normal(V x ∙∙ ts)" |
"normal t ==> normal(Λ t)" |
"∀t∈set 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'_normal_ML›) where
"C_normal_ML(C_U nm vs) =
  ((∀v∈set vs. C_normal_ML v) ∧ no_match_compR nm vs)" |
"C_normal_ML (C_ML _) = True" |
"C_normal_ML (V_ML _) = True" |
"C_normal_ML (A_ML v vs) = (C_normal_ML v ∧ (∀v ∈ set vs. C_normal_ML v))" |
"C_normal_ML (Lam_ML v) = C_normal_ML v" |
"C_normal_ML (V_U x vs) = (∀v ∈ set vs. C_normal_ML v)" |
"C_normal_ML (Clo v vs _) = (C_normal_ML v ∧ (∀v ∈ set vs. C_normal_ML v))" |
"C_normal_ML (apply u v) = (C_normal_ML u ∧ C_normal_ML 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,_). ∑t←ts. 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" (‹dterm_ML›) where
"dterm_ML (C_U nm vs) = C nm ∙∙ map dterm_ML (rev vs)" |
"dterm_ML _ = 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) = dterm_ML v"

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

lemma map_dterm_pure[simp]: "∀t∈set ts. pure t ==> map dterm ts = ts"
by (induct ts) auto

lemma map_dterm_term[simp]: "map dterm (map term vs) = map dterm_ML 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_match_ML ps vs ==>
  no_match (map dterm_ML (rev ps)) (map dterm_ML (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 dterm_ML (rev vs)" in exI)
apply(rule_tac x="map dterm_ML (rev vs')" in exI)
apply(simp)
done

lemma dterm_ML_comp_patD:
  "pattern t ==> dterm_ML (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 (dterm_ML ∘ 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 dterm_ML 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 dterm_ML 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
"∀t∈set ts. C_normal t ==> C_normal(V x ∙∙ ts)" |
"C_normal t ==> C_normal(Λ t)" |
"C_normal_ML v ==> C_normal(term v)" |
"∀t∈set 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_normal_ML 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 (dterm_ML v) = dterm_ML 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_match_ML ps vs ==> vs ==> vs' ==> no_match_ML 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]:
  "∀v∈set vs. ∀x∈fv_ML v. C_normal_ML (σ x) ==>
   no_match_ML ps vs ⟶ no_match_ML ps (map (subst_ML σ) 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 (subst_ML σ) 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:
  "lift_ML k v = C_U nm vs' ==> ∃vs. v = C_U nm vs ∧ vs' = map (lift_ML k) vs"
by(cases v) auto

lemma no_match_ML_lift_ML:
  "no_match_ML ps (map (lift_ML k) vs) = no_match_ML 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 (lift_ML k) vs'" in exI)
apply (fastforce simp:rev_nth)
done

lemma C_normal_ML_lift_ML: "C_normal_ML(lift_ML k v) = C_normal_ML 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_normal_ML(comp_open t)"
by (induct pred:pure) (auto simp:comp_open_def)

lemma C_normal_compR_rhs: "(nm, vs, v) ∈ compR ==> C_normal_ML v"
by(auto simp: compR_def image_def Bex_def pure_R C_normal_ML_comp_open)


lemma C_normal_ML_subst_ML:
  "C_normal_ML (subst_ML σ v) ==> (∀x∈fv_ML v. C_normal_ML (σ 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_normal_ML v ==>
  C_normal_ML (subst_ML σ v) ⟷ (∀x∈fv_ML v. C_normal_ML (σ 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_normal_ML v ==> C_normal_ML v'" and
      "vs ==> vs' ==> ∀v∈set vs. C_normal_ML v ==> ∀v'∈set vs'. C_normal_ML 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 (C_U nm vs)) ∙∙ ts) ((C nm ∙∙ map term (rev vs)) ∙∙ ts)"
  "∧x vs ts. P (term (V_U 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)) (V_U 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 (C_U nm vs) ∙∙ ts ==> t' = (C nm ∙∙ map term (rev vs)) ∙∙ ts ==> P"
  "∧x vs ts.
  t = term (V_U 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)) (V_U 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_normal_ML 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) ⟷
  (∀t∈set 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_match_ML ps vs ⟶ no_match_ML 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_normal_ML v ==> C_normal_ML(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 = C_U nm' vs" "rs' = map dterm_ML (rev vs) @ map dterm ts''"
            using ob by(cases v) auto
          obtain vs' where [simp]: "v' = C_U nm' vs'" "vs ==> vs'"
            using ‹v==>v'› 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 ‹vs==>vs'›] 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: rev_update list_update_append list_update_beyond flip: map_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 = C_U nm' vs" "rs' = map dterm_ML (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" (‹C_U'_args›) where
"C_{U_args}(s ∙ t) = C_{U_args} s @ [t]" |
"C_{U_args}(term(C_U nm vs)) = map term (rev vs)" |
"C_{U_args} _ = []"

lemma [simp]: "C_{U_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_normal_ML v ==> dterm_ML v = C nm ∙∙ ts
   ==> dterm_ML v' = C nm ∙∙ map dterm (C_{U_args}(term v')) ∧
      C_{U_args}(term v) [==>*] C_{U_args}(term v') ∧
      ts = map dterm (C_{U_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(C_{U_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 (C_{U_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 (C_{U_args} t') ∧ dterm t' = C nm ∙∙ ts' ∧
     C_{U_args} t [==>*] C_{U_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' ∧ C_{U_args} t [==>*] C_{U_args} t' ∧
     ts' = map dterm (C_{U_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:
  "∀t∈set 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: "∀t∈set 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 ∧ (∀t∈set ts. pure t)"
by(induct ts arbitrary: s) auto

lemma nbe_C_normal_ML:
  assumes "term v ==>* t'" "C_normal_ML v" "pure t'" shows "normal t'"
proof -
  { fix t t' i v
    assume "(t,t') : Red_term^^i"
    hence "t = term v ==> C_normal_ML 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: "∀t∈set 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: "∀t∈set(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_normal_ML (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)) (V_U 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_normal_ML ?u" using less term_Clo by(simp)
        from less(1)[OF ‹i' < k› refl ‹C_normal_ML ?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_normal_ML 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_normal_ML 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_normal_ML(σ i) ==> C_normal_ML (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 "C_U nm vs"} satisfy
  invariant @{prop"size vs = arity nm"}.›

text‹A constructor value:›

fun C_Us :: "ml ==> bool" where
"C_Us(C_U nm vs) = (size vs = arity nm ∧ (∀v∈set vs. C_Us v))" |
"C_Us _ = 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. i≠j ⟶ 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 ==> ∀i∈fv 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_match_ML ps (rev vs) ==> no_match_ML (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. C_Us v ==> linpats ps ==> size ps = size cvs ==>
  ∀σ. map (subst_ML σ) (map comp_pat ps) ≠ cvs ==>
  no_match_ML (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. ∃σ. subst_ML σ (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 = C_U nm' vs' & size vs' = arity nm' & (∀v' ∈ set vs'. C_Us 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 (metis length_map no_match_ML_swap_rev rev_rev_ident)
done



(*<*)
end
(*>*)