Theory NBE

(*  ID:         $Id: NBE.thy,v 1.12 2009-06-16 19:32:37 nipkow Exp $
    Author:     Klaus Aehlig, Tobias Nipkow
    Normalization by Evaluation
*)
(*<*)
theory NBE imports Main begin

ML"Syntax.ambiguity_level := 1000000"

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

types vname = nat
      ml_vname = nat

(* FIXME only for codegen*)
types 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(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" ("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 (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" ("fvML") where
"fvML (CML nm) = {}" |
"fvML (VML X) = {X}"  |
"fvML (AML v vs) = fvML v ∪ (\<Union>v ∈ set vs. fvML v)" |
"fvML (LamML v) = {X. Suc X : fvML v}" |
"fvML (CU nm vs) = (\<Union>v ∈ set vs. fvML v)" |
"fvML (VU nm vs) = (\<Union>v ∈ set vs. fvML v)" |
"fvML (Clo f vs n) = fvML f ∪ (\<Union>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 (op •) 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 fastsimp
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", standard, simp]
  tm_eq_iff[of _ "h •• ts", standard, simp]

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
apply (metis append_is_Nil_conv args_tm.simps(2) args_tm.simps(5) args_tm_foldl_At butlast.simps(2) butlast_append butlast_snoc eta_head_args head_tm.simps(2) head_tm.simps(4) head_tm.simps(5) head_tm_foldl_At last_snoc list.simps(2) not_Cons_self rotate1_is_Nil_conv rotate_simps self_append_conv self_append_conv2 tm.simps(12) tm.simps(22))
done

lemma fv_head_C[simp]: "fv (t •• ts) = fv t ∪ (\<Union>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 (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", standard]

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" ("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 σ (s•t) = (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 o (VML 0 ## σ) = (VML 0 ## (lift k o σ))"
by(rule ext)(simp add: lift_lift_ML_comm)

lemma lift_subst_ML:
 "lift k (substML σ v) = substML (lift k o σ) (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:expand_fun_eq 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 σ  o σ') 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) ==>
   ∀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:split_if_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 (fastsimp 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
(* FIXME fails using At apply (metis foldl_Cons foldl_Nil foldl_append pattern_AtD1) *)
    using pattern_AtD12[OF At.prems] At(1)[of s2]
    by clarsimp (metis append_is_Nil_conv butlast_snoc last_snoc not_Cons_self)
qed (auto elim!: pattern.cases split:split_if_asm)


subsection "Reduction of @{text λ}-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
   ==> listsum (map size vs) < listsum (map size ps)"
apply(subgoal_tac "CU nm vs : set ps")
 apply(drule listsum_map_remove1[of _ _ size])
 apply (simp add:list_size_conv_listsum)
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,_). ∑v\<leftarrow>vs. 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 + (∑v\<leftarrow>vs. size' v))+1" |
"size' (LamML v) = size' v + 1" |
"size' (CU nm vs) = (∑v\<leftarrow>vs. size' v)+1" |
"size' (VU nm vs) = (∑v\<leftarrow>vs. size' v)+1" |
"size' (Clo f vs n) = (size' f + (∑v\<leftarrow>vs. size' v))+1" |
"size' (apply v w) = (size' v + size' w)+1"

lemma listsum_size'[simp]:
 "v ∈ set vs ==> size' v < Suc(listsum (map size' vs))"
by(induct vs)(auto)

corollary cor_listsum_size'[simp]:
 "v ∈ set vs ==> size' v < Suc(m + listsum (map size' vs))"
using listsum_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 = listsum])
   apply(rule map_ext)
   apply simp
  apply(rule arg_cong[where f = listsum])
  apply(rule map_ext)
  apply simp
 apply(rule arg_cong[where f = listsum])
 apply(rule map_ext)
 apply simp
apply(rule arg_cong[where f = listsum])
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 = listsum])
    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 = listsum])
  apply(rule map_ext)
  apply simp
 apply(rule arg_cong[where f = listsum])
 apply(rule map_ext)
 apply simp
apply(rule arg_cong[where f = listsum])
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 = listsum])
   apply(rule map_ext)
   apply simp
  apply(rule arg_cong[where f = listsum])
  apply(rule map_ext)
  apply simp
 apply(rule arg_cong[where f = listsum])
 apply(rule map_ext)
 apply simp
apply(rule arg_cong[where f = listsum])
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 o 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 "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) o (λ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 @{text 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 σ' o VML 0 ## σ) = VML 0 ## (subst_ml σ' o σ)")
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:expand_fun_eq split:nat.split)
apply(simp add:lift_is_subst_ml subst_ml_comp)
apply(rule arg_cong[where f = kernel])
apply(subgoal_tac "(nat_case 0 (λk. Suc (σ k)) o Suc) = Suc o σ")
prefer 2 apply(simp add:expand_fun_eq split:nat.split)
apply(subgoal_tac "(subst_ml (nat_case 0 (λk. Suc (σ k))) o
               (λ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: expand_fun_eq)
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:expand_fun_eq 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-
      def pi == "λn::nat. if n = 0 then 1 else if n = 1 then 0 else n"
      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 o (Suc o Suc) = (Suc o Suc)")
          apply(simp)
          apply(simp add:pi_def expand_fun_eq)
          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) σ = Clo (CML nm) [] (arity 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)


defs compR_def:
 "compR ≡ (λ(nm,ts,t). (nm, map comp_pat (rev ts), comp_open t)) ` R"


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')
   ==> ∃t∈set 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 ==> ∃u∈set vs. x ∈ fvML u"
by(fastsimp simp add:compR_def image_def dest: fv_compR_aux)

lemma lift_compile:
  "pure t ==> ∀σ k. lift k (compile t σ) = compile t (lift k o σ)"
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 o σ)" 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)) o
               (lift 0 o 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 o σ) 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 o σ) t"
proof(induct arbitrary: σ pred:pure)
  case (Lam t)
  have "lift 0 o VML = VML" by (simp add:expand_fun_eq)
  hence "(substML σ (comp_open (Λ t)))! =
    Λ (substML (lift 0 o 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 o σ)) 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 o σ)) 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' ==> ∀v∈set 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
"∀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'_normalML") where
"C_normalML(CU nm vs) =
  ((∀v∈set 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 + list_size size_tm ts"
by (induct ts arbitrary:t) auto

lemma termination_no_match:
  "i < length ss ==> ss ! i = C nm •• ts
   ==> listsum (map size_tm ts) < listsum (map size_tm ss)"
apply(subgoal_tac "C nm •• ts : set ss")
 apply(drule listsum_map_remove1[of _ _ size_tm])
apply(simp add:size_tm_foldl_At list_size_conv_listsum)
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\<leftarrow>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 fastsimp
    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 fastsimp
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]: "∀t∈set 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 o 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
"∀t∈set ts. C_normal t ==> C_normal(V x •• ts)" |
"C_normal t ==> C_normal(Λ t)" |
"C_normalML 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_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(fastsimp intro: 1(1) simp add:rev_nth)
done
qed

lemma no_match_ML_subst_ML[rule_format]:
  "∀v∈set vs. ∀x∈fvML 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 fastsimp
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 (fastsimp 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) ==> (∀x∈fvML 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) <-> (∀x∈fvML 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' ==> ∀v∈set 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(fastsimp elim: C_normal.cases)

lemma [simp]: "C_normal(Λ t •• ts) <-> C_normal t ∧ ts = []"
by(fastsimp 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(fastsimp elim: C_normal.cases)

lemma [simp]: "C_normal(V x •• ts) <-> (∀t ∈ set ts. C_normal t)"
by(fastsimp 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 (fastsimp simp:rev_nth)
done

lemma no_match_compR_lift:
  "no_match_compR nm vs ==> no_match_compR nm (map (lift k) vs)"
by (fastsimp 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) fastsimp
  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 `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 fastsimp
          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 prems 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]]

(* FIXME move *)

lemma listsimps_eq_0_iff: "listsum ns = (0::nat) <-> (∀ n ∈ set ns. n = 0)"
by(metis listsum sum_eq_0_conv)

(* Generalize to suitable type class? *)
lemma elem_le_listsum_nat: "k<size ns ==> ns!k <= listsum(ns::nat list)"
apply(induct ns arbitrary: k)
apply(auto simp:nth_Cons')
apply(metis diff_less less_imp_diff_less nat_neq_iff not_less_eq trans_le_add2)
done

lemma listsum_update: "k<size ns ==>
  listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
apply(induct ns arbitrary:k)
apply (auto split:nat.split)
apply(drule elem_le_listsum_nat)
apply arith
done
(*
lemma lem: "finite A ==>
  (∑x∈A. if P x then f x else g x) =
  setsum f {a:A. P a} + setsum g {a:A. ~P a}"
*)

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 n ≡ "listsum ns" arbitrary: ts ns)
  case 0
  hence "∀i < size ts. ns!i = 0" by (simp add:listsimps_eq_0_iff)
  with 0 show ?case by simp (metis nth_equalityI)
next
  case (Suc n)
  then have "listsum ns ≠ 0" by arith
  then obtain k l where "k<size ts" and [simp]: "ns!k = Suc l"
    by(simp add:listsimps_eq_0_iff)
      (metis Suc(4) gr0_implies_Suc in_set_conv_nth)
  let ?ns = "ns[k := l]"
  have "n = listsum ?ns" using Suc(6) `k<size ts` `size ns = size ts`
    by (simp add:listsum_update)
  obtain t' where "ts!k => t'" "(t', ts'!k) : Red_term^^l"
    using Suc(2) `k<size ts` `size ns = size ts` `ns!k = Suc l`
    by (metis rel_pow_Suc_E2)
  then have 1: "∀i<size(ts[k:=t']). (ts[k:=t']!i, ts'!i) : Red_term^^(?ns!i)"
    using Suc(2) `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'` Suc(5)]
  show ?case by(rule Suc(1)[OF 1 _ _ nm1 `n = listsum ?ns`])
               (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
  proof cases qed auto
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')) ∧
      (∀t∈set(CU_args(term v)). C_normal t) ∧
      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_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' &
     (∀t∈set(CU_args t). C_normal t) ∧
     CU_args t [=>*] CU_args t' ∧ ts = map dterm (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 clarsimp
apply rule
apply (metis C_normal_ML_inv)
apply clarify
apply(drule (2) C_Red_term_ML)
apply clarsimp
apply clarsimp
apply (metis List.set.simps(2) insert_code mem_def predicate1D set_update_subset_insert)
apply clarsimp
apply(rule)
apply (metis List.set.simps(2) insert_code mem_def predicate1D 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 simp
apply(rule_tac x=nm' in exI)
apply(erule_tac x=rs' in meta_allE)
apply(erule_tac x=nm' in meta_allE)
apply clarsimp
apply(metis 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' ∧
     (∀t∈set(CU_args t). C_normal t) ∧ CU_args t [=>*] CU_args t' ∧
     ts' = map dterm (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
apply simp
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 "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 fastsimp
  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)
  from C_redts [OF `ts!i =>* ts'!i` `C_normal (ts!i)`] this obtain ss' rs rs' :: "tm list"
    where "∀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 fastsimp
  show ?case
    apply(subst no_match.simps)
    apply(rule_tac x=i in exI)
    using prems
    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 rel_pow_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 rel_pow_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(fastsimp 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 s' t)
      then obtain k s'' where "k<length rs" "rs ! k => s''" "s' = V x •• rs[k := s'']"
        using snoc(1) by force
      then show ?thesis (is "∃k < ?n. ∃s. ?P k s")
      proof-
        have "k<?n ∧ ?P k s''" using prems
          by (simp add:nth_append) (metis last_snoc butlast_snoc list_update_append1)
        thus ?thesis by blast
      qed
    next
      case (ctxt_At2 t t' s)
      then show ?thesis (is "∃k < ?n. ∃s. ?P k s")
      proof-
        have "size rs<?n ∧ ?P (size rs) t'" using prems by simp
        thus ?thesis by blast
      qed
    qed auto
  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 rel_pow_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 rel_pow_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(fastsimp 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 s' t)
      then obtain k s'' where "k<length rs" "rs ! k => s''" "s' = C nm •• rs[k := s'']"
        using snoc(1) by force
      then show ?thesis (is "∃k < ?n. ∃s. ?P k s")
      proof-
        have "k<?n ∧ ?P k s''" using prems
          by (simp add:nth_append) (metis last_snoc butlast_snoc list_update_append1)
        thus ?thesis by blast
      qed
    next
      case (ctxt_At2 t t' s)
      then show ?thesis (is "∃k < ?n. ∃s. ?P k s")
      proof-
        have "size rs<?n ∧ ?P (size rs) t'" using prems by simp
        thus ?thesis by blast
      qed
    qed auto
  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 rel_pow_Suc_I2 relpow.simps(2))
    done
qed


lemma pure_At[simp]: "pure(s • t) <-> pure s ∧ pure t"
by(fastsimp 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_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" "(s,t') : Red_term^^i'" and [arith]: "i' <= i"
        by (metis eq_imp_le less(5) Suc rel_pow_Suc_D2)
      hence "term v => s" using Suc less by simp
      thus ?thesis
      proof cases
        case (term_C nm vs)
        have 0:"no_match_compR nm vs" using prems 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 fastsimp
            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 prems by auto
          from C_Red_term_it[OF this] obtain ts' "is"
            where "t' = C nm  •• ts'"  "length ts' = ?n ∧ length is =?n ∧
           (∀j< ?n. (map term (rev vs) ! j, ts' ! j) ∈ Red_term ^^ is ! j ∧ is ! j ≤ i')"
            using prems by auto
          from `t' = C nm •• ts'` `t' = C nm •• ts` have "ts = ts'" by simp
          show ?thesis using prems by (auto  simp: rtrancl_is_UN_rel_pow)
        qed
        have 5: "∀t∈set(map term vs). C_normal t"  using prems 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(fastsimp simp:set_conv_nth)
          apply auto
          apply(subgoal_tac "no_match aa (take (size aa) ts)")
          apply (metis no_match)
          apply(fastsimp 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 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 prems by auto
        from less(1)[OF `i' < k` refl `C_normalML u'` `pure t'` this] show ?thesis .
      qed auto
    qed
  qed
  }
  thus ?thesis using assms(2-) rtrancl_imp_rel_pow[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 ∧ (∀v∈set vs. CUs v))" |
"CUs _ = False"

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


lemma termination_linpats:
  "i < length ts ==> ts!i = C nm •• ts'
   ==> length ts' + listsum (map size ts') < length ts + listsum (map size ts)"
apply(subgoal_tac "C nm •• ts' : set ts")
 prefer 2 apply (metis in_set_conv_nth)
apply(drule listsum_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 <->
 (ALL i<size ts. (EX x. ts!i = V x) |
    (EX nm ts'. ts!i = C nm •• ts' ∧ arity nm = size ts' ∧ linpats ts')) &
 (ALL i<size ts. ALL 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) = (ALL i<size xs. xs!i = ys!i)"
by (metis nth_equalityI)

lemma pattern_subst_ML_coincidence:
 "pattern t ==> ALL 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 "(EX x. t = V x) | (EX 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 (fastsimp simp:rev_nth)
done

lemma no_match_ML_aux:
  "ALL 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 "ALL i<size ts. EX σ. 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 "~(EX x. ts!i = V x)")
 prefer 2
 apply fastsimp
apply(subgoal_tac "EX nm ts'. ts!i = C nm •• ts' & size ts' = arity nm & linpats ts'")
 prefer 2
 apply fastsimp
apply clarsimp
apply(rule_tac x=nm in exI)
apply(subgoal_tac "EX nm' vs'. cvs!i = CU nm' vs' & size vs' = arity nm' & (ALL 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_map rev_rev_ident)
done



(*<*)
end
(*>*)