# Theory Standardization

theory Standardization
imports Nominal
```(*  Title:      HOL/Nominal/Examples/Standardization.thy
Author:     Stefan Berghofer and Tobias Nipkow
*)

section ‹Standardization›

theory Standardization
imports "HOL-Nominal.Nominal"
begin

text ‹
The proof of the standardization theorem, as well as most of the theorems about
lambda calculus in the following sections, are taken from ‹HOL/Lambda›.
›

subsection ‹Lambda terms›

atom_decl name

nominal_datatype lam =
Var "name"
| App "lam" "lam" (infixl "°" 200)
| Lam "«name»lam" ("Lam [_]._" [0, 10] 10)

instantiation lam :: size
begin

nominal_primrec size_lam
where
"size (Var n) = 0"
| "size (t ° u) = size t + size u + 1"
| "size (Lam [x].t) = size t + 1"
apply finite_guess+
apply (rule TrueI)+
apply fresh_guess+
done

instance ..

end

nominal_primrec
subst :: "lam ⇒ name ⇒ lam ⇒ lam"  ("_[_::=_]" [300, 0, 0] 300)
where
subst_Var: "(Var x)[y::=s] = (if x=y then s else (Var x))"
| subst_App: "(t⇩1 ° t⇩2)[y::=s] = t⇩1[y::=s] ° t⇩2[y::=s]"
| subst_Lam: "x ♯ (y, s) ⟹ (Lam [x].t)[y::=s] = (Lam [x].(t[y::=s]))"
apply(finite_guess)+
apply(rule TrueI)+
apply(fresh_guess)+
done

lemma subst_eqvt [eqvt]:
"(pi::name prm) ∙ (t[x::=u]) = (pi ∙ t)[(pi ∙ x)::=(pi ∙ u)]"
by (nominal_induct t avoiding: x u rule: lam.strong_induct)

lemma subst_rename:
"y ♯ t ⟹ ([(y, x)] ∙ t)[y::=u] = t[x::=u]"
by (nominal_induct t avoiding: x y u rule: lam.strong_induct)

lemma fresh_subst:
"(x::name) ♯ t ⟹ x ♯ u ⟹ x ♯ t[y::=u]"
by (nominal_induct t avoiding: x y u rule: lam.strong_induct)

lemma fresh_subst':
"(x::name) ♯ u ⟹ x ♯ t[x::=u]"
by (nominal_induct t avoiding: x u rule: lam.strong_induct)

lemma subst_forget: "(x::name) ♯ t ⟹ t[x::=u] = t"
by (nominal_induct t avoiding: x u rule: lam.strong_induct)

lemma subst_subst:
"x ≠ y ⟹ x ♯ v ⟹ t[y::=v][x::=u[y::=v]] = t[x::=u][y::=v]"
by (nominal_induct t avoiding: x y u v rule: lam.strong_induct)

declare subst_Var [simp del]

lemma subst_eq [simp]: "(Var x)[x::=u] = u"

lemma subst_neq [simp]: "x ≠ y ⟹ (Var x)[y::=u] = Var x"

inductive beta :: "lam ⇒ lam ⇒ bool"  (infixl "→⇩β" 50)
where
beta: "x ♯ t ⟹ (Lam [x].s) ° t →⇩β s[x::=t]"
| appL [simp, intro!]: "s →⇩β t ⟹ s ° u →⇩β t ° u"
| appR [simp, intro!]: "s →⇩β t ⟹ u ° s →⇩β u ° t"
| abs [simp, intro!]: "s →⇩β t ⟹ (Lam [x].s) →⇩β (Lam [x].t)"

equivariance beta
nominal_inductive beta

lemma better_beta [simp, intro!]: "(Lam [x].s) ° t →⇩β s[x::=t]"
proof -
obtain y::name where y: "y ♯ (x, s, t)"
by (rule exists_fresh) (rule fin_supp)
then have "y ♯ t" by simp
then have "(Lam [y]. [(y, x)] ∙ s) ° t →⇩β ([(y, x)] ∙ s)[y::=t]"
by (rule beta)
moreover from y have "(Lam [x].s) = (Lam [y]. [(y, x)] ∙ s)"
by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
ultimately show ?thesis using y by (simp add: subst_rename)
qed

abbreviation
beta_reds :: "lam ⇒ lam ⇒ bool"  (infixl "→⇩β⇧*" 50) where
"s →⇩β⇧* t ≡ beta⇧*⇧* s t"

subsection ‹Application of a term to a list of terms›

abbreviation
list_application :: "lam ⇒ lam list ⇒ lam"  (infixl "°°" 150) where
"t °° ts ≡ foldl (°) t ts"

lemma apps_eq_tail_conv [iff]: "(r °° ts = s °° ts) = (r = s)"
by (induct ts rule: rev_induct) (auto simp add: lam.inject)

lemma Var_eq_apps_conv [iff]: "(Var m = s °° ss) = (Var m = s ∧ ss = [])"
by (induct ss arbitrary: s) auto

lemma Var_apps_eq_Var_apps_conv [iff]:
"(Var m °° rs = Var n °° ss) = (m = n ∧ rs = ss)"
apply (induct rs arbitrary: ss rule: rev_induct)
apply blast
apply (induct_tac ss rule: rev_induct)
done

lemma App_eq_foldl_conv:
"(r ° s = t °° ts) =
(if ts = [] then r ° s = t
else (∃ss. ts = ss @ [s] ∧ r = t °° ss))"
apply (rule_tac xs = ts in rev_exhaust)
done

lemma Abs_eq_apps_conv [iff]:
"((Lam [x].r) = s °° ss) = ((Lam [x].r) = s ∧ ss = [])"
by (induct ss rule: rev_induct) auto

lemma apps_eq_Abs_conv [iff]: "(s °° ss = (Lam [x].r)) = (s = (Lam [x].r) ∧ ss = [])"
by (induct ss rule: rev_induct) auto

lemma Abs_App_neq_Var_apps [iff]:
"(Lam [x].s) ° t ≠ Var n °° ss"
by (induct ss arbitrary: s t rule: rev_induct) (auto simp add: lam.inject)

lemma Var_apps_neq_Abs_apps [iff]:
"Var n °° ts ≠ (Lam [x].r) °° ss"
apply (induct ss arbitrary: ts rule: rev_induct)
apply simp
apply (induct_tac ts rule: rev_induct)
done

"∃ts h. t = h °° ts ∧ ((∃n. h = Var n) ∨ (∃x u. h = (Lam [x].u)))"
apply (induct t rule: lam.induct)
apply (metis foldl_Nil)
apply (metis foldl_Cons foldl_Nil foldl_append)
apply (metis foldl_Nil)
done

lemma size_apps [simp]:
"size (r °° rs) = size r + foldl (+) 0 (map size rs) + length rs"
by (induct rs rule: rev_induct) auto

lemma lem0: "(0::nat) < k ⟹ m ≤ n ⟹ m < n + k"
by simp

lemma subst_map [simp]:
"(t °° ts)[x::=u] = t[x::=u] °° map (λt. t[x::=u]) ts"
by (induct ts arbitrary: t) simp_all

lemma app_last: "(t °° ts) ° u = t °° (ts @ [u])"
by simp

lemma perm_apps [eqvt]:
"(pi::name prm) ∙ (t °° ts) = ((pi ∙ t) °° (pi ∙ ts))"
by (induct ts rule: rev_induct) (auto simp add: append_eqvt)

lemma fresh_apps [simp]: "(x::name) ♯ (t °° ts) = (x ♯ t ∧ x ♯ ts)"
by (induct ts rule: rev_induct)
(auto simp add: fresh_list_append fresh_list_nil fresh_list_cons)

text ‹A customized induction schema for ‹°°›.›

lemma lem:
assumes "⋀n ts (z::'a::fs_name). (⋀z. ∀t ∈ set ts. P z t) ⟹ P z (Var n °° ts)"
and "⋀x u ts z. x ♯ z ⟹ (⋀z. P z u) ⟹ (⋀z. ∀t ∈ set ts. P z t) ⟹ P z ((Lam [x].u) °° ts)"
shows "size t = n ⟹ P z t"
apply (induct n arbitrary: t z rule: nat_less_induct)
apply (cut_tac t = t in ex_head_tail)
apply clarify
apply (erule disjE)
apply clarify
apply (rule assms)
apply clarify
apply (erule allE, erule impE)
prefer 2
apply (erule allE, erule impE, rule refl, erule spec)
apply simp
apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
apply clarify
apply (subgoal_tac "∃y::name. y ♯ (x, u, z)")
prefer 2
apply (blast intro: exists_fresh' fin_supp)
apply (erule exE)
apply (subgoal_tac "(Lam [x].u) = (Lam [y].([(y, x)] ∙ u))")
prefer 2
apply (auto simp add: lam.inject alpha' fresh_prod fresh_atm)[]
apply (simp (no_asm_simp))
apply (rule assms)
apply (erule allE, erule impE)
prefer 2
apply (erule allE, erule impE, rule refl, erule spec)
apply simp
apply clarify
apply (erule allE, erule impE)
prefer 2
apply blast
apply simp
apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
done

theorem Apps_lam_induct:
assumes "⋀n ts (z::'a::fs_name). (⋀z. ∀t ∈ set ts. P z t) ⟹ P z (Var n °° ts)"
and "⋀x u ts z. x ♯ z ⟹ (⋀z. P z u) ⟹ (⋀z. ∀t ∈ set ts. P z t) ⟹ P z ((Lam [x].u) °° ts)"
shows "P z t"
apply (rule_tac t = t and z = z in lem)
prefer 3
apply (rule refl)
using assms apply blast+
done

subsection ‹Congruence rules›

lemma apps_preserves_beta [simp]:
"r →⇩β s ⟹ r °° ss →⇩β s °° ss"
by (induct ss rule: rev_induct) auto

lemma rtrancl_beta_Abs [intro!]:
"s →⇩β⇧* s' ⟹ (Lam [x].s) →⇩β⇧* (Lam [x].s')"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_AppL:
"s →⇩β⇧* s' ⟹ s ° t →⇩β⇧* s' ° t"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_AppR:
"t →⇩β⇧* t' ⟹ s ° t →⇩β⇧* s ° t'"
by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_App [intro]:
"s →⇩β⇧* s' ⟹ t →⇩β⇧* t' ⟹ s ° t →⇩β⇧* s' ° t'"
by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)

subsection ‹Lifting an order to lists of elements›

definition
step1 :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool" where
"step1 r =
(λys xs. ∃us z z' vs. xs = us @ z # vs ∧ r z' z ∧ ys =
us @ z' # vs)"

lemma not_Nil_step1 [iff]: "¬ step1 r [] xs"
apply (unfold step1_def)
apply blast
done

lemma not_step1_Nil [iff]: "¬ step1 r xs []"
apply (unfold step1_def)
apply blast
done

lemma Cons_step1_Cons [iff]:
"(step1 r (y # ys) (x # xs)) =
(r y x ∧ xs = ys ∨ x = y ∧ step1 r ys xs)"
apply (unfold step1_def)
apply (rule iffI)
apply (erule exE)
apply (rename_tac ts)
apply (case_tac ts)
apply fastforce
apply force
apply (erule disjE)
apply blast
apply (blast intro: Cons_eq_appendI)
done

lemma append_step1I:
"step1 r ys xs ∧ vs = us ∨ ys = xs ∧ step1 r vs us
⟹ step1 r (ys @ vs) (xs @ us)"
apply (unfold step1_def)
apply auto
apply blast
apply (blast intro: append_eq_appendI)
done

lemma Cons_step1E [elim!]:
assumes "step1 r ys (x # xs)"
and "⋀y. ys = y # xs ⟹ r y x ⟹ R"
and "⋀zs. ys = x # zs ⟹ step1 r zs xs ⟹ R"
shows R
using assms
apply (cases ys)
apply blast
done

lemma Snoc_step1_SnocD:
"step1 r (ys @ [y]) (xs @ [x])
⟹ (step1 r ys xs ∧ y = x ∨ ys = xs ∧ r y x)"
apply (unfold step1_def)
apply (clarify del: disjCI)
apply (rename_tac vs)
apply (rule_tac xs = vs in rev_exhaust)
apply force
apply simp
apply blast
done

subsection ‹Lifting beta-reduction to lists›

abbreviation
list_beta :: "lam list ⇒ lam list ⇒ bool"  (infixl "[→⇩β]⇩1" 50) where
"rs [→⇩β]⇩1 ss ≡ step1 beta rs ss"

"Var n °° rs →⇩β v ⟹ ∃ss. rs [→⇩β]⇩1 ss ∧ v = Var n °° ss"
apply (induct u ≡ "Var n °° rs" v arbitrary: rs set: beta)
apply simp
apply (rule_tac xs = rs in rev_exhaust)
apply simp
apply (atomize, force intro: append_step1I iff: lam.inject)
apply (rule_tac xs = rs in rev_exhaust)
apply simp
apply (auto 0 3 intro: disjI2 [THEN append_step1I] simp add: lam.inject)
done

lemma apps_betasE [case_names appL appR beta, consumes 1]:
assumes major: "r °° rs →⇩β s"
and cases: "⋀r'. r →⇩β r' ⟹ s = r' °° rs ⟹ R"
"⋀rs'. rs [→⇩β]⇩1 rs' ⟹ s = r °° rs' ⟹ R"
"⋀t u us. (x ♯ r ⟹ r = (Lam [x].t) ∧ rs = u # us ∧ s = t[x::=u] °° us) ⟹ R"
shows R
proof -
from major have
"(∃r'. r →⇩β r' ∧ s = r' °° rs) ∨
(∃rs'. rs [→⇩β]⇩1 rs' ∧ s = r °° rs') ∨
(∃t u us. x ♯ r ⟶ r = (Lam [x].t) ∧ rs = u # us ∧ s = t[x::=u] °° us)"
apply (nominal_induct u ≡ "r °° rs" s avoiding: x r rs rule: beta.strong_induct)
apply (split if_split_asm)
apply simp
apply blast
apply simp
apply (rule impI)+
apply (rule disjI2)
apply (rule disjI2)
apply (subgoal_tac "r = [(xa, x)] ∙ (Lam [x].s)")
prefer 2
apply (drule conjunct1)
apply (subgoal_tac "r = (Lam [xa]. [(xa, x)] ∙ s)")
prefer 2
apply (thin_tac "r = _")
apply simp
apply (rule exI)
apply (rule conjI)
apply (rule refl)
apply (simp add: abs_fresh fresh_atm fresh_left calc_atm subst_rename)
apply (drule App_eq_foldl_conv [THEN iffD1])
apply (split if_split_asm)
apply simp
apply blast
apply (force intro!: disjI1 [THEN append_step1I] simp add: fresh_list_append)
apply (drule App_eq_foldl_conv [THEN iffD1])
apply (split if_split_asm)
apply simp
apply blast
apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
done
with cases show ?thesis by blast
qed

lemma apps_preserves_betas [simp]:
"rs [→⇩β]⇩1 ss ⟹ r °° rs →⇩β r °° ss"
apply (induct rs arbitrary: ss rule: rev_induct)
apply simp
apply simp
apply (rule_tac xs = ss in rev_exhaust)
apply simp
apply simp
apply (drule Snoc_step1_SnocD)
apply blast
done

subsection ‹Standard reduction relation›

text ‹
Based on lecture notes by Ralph Matthes,
original proof idea due to Ralph Loader.
›

declare listrel_mono [mono_set]

lemma listrelp_eqvt [eqvt]:
fixes f :: "'a::pt_name ⇒ 'b::pt_name ⇒ bool"
assumes xy: "listrelp f (x::'a::pt_name list) y"
shows "listrelp ((pi::name prm) ∙ f) (pi ∙ x) (pi ∙ y)" using xy
by induct (simp_all add: listrelp.intros perm_app [symmetric])

inductive
sred :: "lam ⇒ lam ⇒ bool"  (infixl "→⇩s" 50)
and sredlist :: "lam list ⇒ lam list ⇒ bool"  (infixl "[→⇩s]" 50)
where
"s [→⇩s] t ≡ listrelp (→⇩s) s t"
| Var: "rs [→⇩s] rs' ⟹ Var x °° rs →⇩s Var x °° rs'"
| Abs: "x ♯ (ss, ss') ⟹ r →⇩s r' ⟹ ss [→⇩s] ss' ⟹ (Lam [x].r) °° ss →⇩s (Lam [x].r') °° ss'"
| Beta: "x ♯ (s, ss, t) ⟹ r[x::=s] °° ss →⇩s t ⟹ (Lam [x].r) ° s °° ss →⇩s t"

equivariance sred
nominal_inductive sred

lemma better_sred_Abs:
assumes H1: "r →⇩s r'"
and H2: "ss [→⇩s] ss'"
shows "(Lam [x].r) °° ss →⇩s (Lam [x].r') °° ss'"
proof -
obtain y::name where y: "y ♯ (x, r, r', ss, ss')"
by (rule exists_fresh) (rule fin_supp)
then have "y ♯ (ss, ss')" by simp
moreover from H1 have "[(y, x)] ∙ (r →⇩s r')" by (rule perm_boolI)
then have "([(y, x)] ∙ r) →⇩s ([(y, x)] ∙ r')" by (simp add: eqvts)
ultimately have "(Lam [y]. [(y, x)] ∙ r) °° ss →⇩s (Lam [y]. [(y, x)] ∙ r') °° ss'" using H2
by (rule sred.Abs)
moreover from y have "(Lam [x].r) = (Lam [y]. [(y, x)] ∙ r)"
by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
moreover from y have "(Lam [x].r') = (Lam [y]. [(y, x)] ∙ r')"
by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
ultimately show ?thesis by simp
qed

lemma better_sred_Beta:
assumes H: "r[x::=s] °° ss →⇩s t"
shows "(Lam [x].r) ° s °° ss →⇩s t"
proof -
obtain y::name where y: "y ♯ (x, r, s, ss, t)"
by (rule exists_fresh) (rule fin_supp)
then have "y ♯ (s, ss, t)" by simp
moreover from y H have "([(y, x)] ∙ r)[y::=s] °° ss →⇩s t"
ultimately have "(Lam [y].[(y, x)] ∙ r) ° s °° ss →⇩s t"
by (rule sred.Beta)
moreover from y have "(Lam [x].r) = (Lam [y]. [(y, x)] ∙ r)"
by (auto simp add: lam.inject alpha' fresh_prod fresh_atm)
ultimately show ?thesis by simp
qed

lemmas better_sred_intros = sred.Var better_sred_Abs better_sred_Beta

lemma refl_listrelp: "∀x∈set xs. R x x ⟹ listrelp R xs xs"
by (induct xs) (auto intro: listrelp.intros)

lemma refl_sred: "t →⇩s t"
by (nominal_induct t rule: Apps_lam_induct) (auto intro: refl_listrelp better_sred_intros)

lemma listrelp_conj1: "listrelp (λx y. R x y ∧ S x y) x y ⟹ listrelp R x y"
by (erule listrelp.induct) (auto intro: listrelp.intros)

lemma listrelp_conj2: "listrelp (λx y. R x y ∧ S x y) x y ⟹ listrelp S x y"
by (erule listrelp.induct) (auto intro: listrelp.intros)

lemma listrelp_app:
assumes xsys: "listrelp R xs ys"
shows "listrelp R xs' ys' ⟹ listrelp R (xs @ xs') (ys @ ys')" using xsys
by (induct arbitrary: xs' ys') (auto intro: listrelp.intros)

lemma lemma1:
assumes r: "r →⇩s r'" and s: "s →⇩s s'"
shows "r ° s →⇩s r' ° s'" using r
proof induct
case (Var rs rs' x)
then have "rs [→⇩s] rs'" by (rule listrelp_conj1)
moreover have "[s] [→⇩s] [s']" by (iprover intro: s listrelp.intros)
ultimately have "rs @ [s] [→⇩s] rs' @ [s']" by (rule listrelp_app)
hence "Var x °° (rs @ [s]) →⇩s Var x °° (rs' @ [s'])" by (rule sred.Var)
thus ?case by (simp only: app_last)
next
case (Abs x ss ss' r r')
from Abs(4) have "ss [→⇩s] ss'" by (rule listrelp_conj1)
moreover have "[s] [→⇩s] [s']" by (iprover intro: s listrelp.intros)
ultimately have "ss @ [s] [→⇩s] ss' @ [s']" by (rule listrelp_app)
with ‹r →⇩s r'› have "(Lam [x].r) °° (ss @ [s]) →⇩s (Lam [x].r') °° (ss' @ [s'])"
by (rule better_sred_Abs)
thus ?case by (simp only: app_last)
next
case (Beta x u ss t r)
hence "r[x::=u] °° (ss @ [s]) →⇩s t ° s'" by (simp only: app_last)
hence "(Lam [x].r) ° u °° (ss @ [s]) →⇩s t ° s'" by (rule better_sred_Beta)
thus ?case by (simp only: app_last)
qed

lemma lemma1':
assumes ts: "ts [→⇩s] ts'"
shows "r →⇩s r' ⟹ r °° ts →⇩s r' °° ts'" using ts
by (induct arbitrary: r r') (auto intro: lemma1)

lemma listrelp_betas:
assumes ts: "listrelp (→⇩β⇧*) ts ts'"
shows "⋀t t'. t →⇩β⇧* t' ⟹ t °° ts →⇩β⇧* t' °° ts'" using ts
by induct auto

lemma lemma2:
assumes t: "t →⇩s u"
shows "t →⇩β⇧* u" using t
by induct (auto dest: listrelp_conj2
intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp)

lemma lemma3:
assumes r: "r →⇩s r'"
shows "s →⇩s s' ⟹ r[x::=s] →⇩s r'[x::=s']" using r
proof (nominal_induct avoiding: x s s' rule: sred.strong_induct)
case (Var rs rs' y)
hence "map (λt. t[x::=s]) rs [→⇩s] map (λt. t[x::=s']) rs'"
by induct (auto intro: listrelp.intros Var)
moreover have "Var y[x::=s] →⇩s Var y[x::=s']"
by (cases "y = x") (auto simp add: Var intro: refl_sred)
ultimately show ?case by simp (rule lemma1')
next
case (Abs y ss ss' r r')
then have "r[x::=s] →⇩s r'[x::=s']" by fast
moreover from Abs(8) ‹s →⇩s s'› have "map (λt. t[x::=s]) ss [→⇩s] map (λt. t[x::=s']) ss'"
by induct (auto intro: listrelp.intros Abs)
ultimately show ?case using Abs(6) ‹y ♯ x› ‹y ♯ s› ‹y ♯ s'›
by simp (rule better_sred_Abs)
next
case (Beta y u ss t r)
thus ?case by (auto simp add: subst_subst fresh_atm intro: better_sred_Beta)
qed

lemma lemma4_aux:
assumes rs: "listrelp (λt u. t →⇩s u ∧ (∀r. u →⇩β r ⟶ t →⇩s r)) rs rs'"
shows "rs' [→⇩β]⇩1 ss ⟹ rs [→⇩s] ss" using rs
proof (induct arbitrary: ss)
case Nil
thus ?case by cases (auto intro: listrelp.Nil)
next
case (Cons x y xs ys)
note Cons' = Cons
show ?case
proof (cases ss)
case Nil with Cons show ?thesis by simp
next
case (Cons y' ys')
hence ss: "ss = y' # ys'" by simp
from Cons Cons' have "y →⇩β y' ∧ ys' = ys ∨ y' = y ∧ ys [→⇩β]⇩1 ys'" by simp
hence "x # xs [→⇩s] y' # ys'"
proof
assume H: "y →⇩β y' ∧ ys' = ys"
with Cons' have "x →⇩s y'" by blast
moreover from Cons' have "xs [→⇩s] ys" by (iprover dest: listrelp_conj1)
ultimately have "x # xs [→⇩s] y' # ys" by (rule listrelp.Cons)
with H show ?thesis by simp
next
assume H: "y' = y ∧ ys [→⇩β]⇩1 ys'"
with Cons' have "x →⇩s y'" by blast
moreover from H have "xs [→⇩s] ys'" by (blast intro: Cons')
ultimately show ?thesis by (rule listrelp.Cons)
qed
with ss show ?thesis by simp
qed
qed

lemma lemma4:
assumes r: "r →⇩s r'"
shows "r' →⇩β r'' ⟹ r →⇩s r''" using r
proof (nominal_induct avoiding: r'' rule: sred.strong_induct)
case (Var rs rs' x)
then obtain ss where rs: "rs' [→⇩β]⇩1 ss" and r'': "r'' = Var x °° ss"
from Var(1) [simplified] rs have "rs [→⇩s] ss" by (rule lemma4_aux)
hence "Var x °° rs →⇩s Var x °° ss" by (rule sred.Var)
with r'' show ?case by simp
next
case (Abs x ss ss' r r')
from ‹(Lam [x].r') °° ss' →⇩β r''› show ?case
proof (cases rule: apps_betasE [where x=x])
case (appL s)
then obtain r''' where s: "s = (Lam [x].r''')" and r''': "r' →⇩β r'''" using ‹x ♯ r''›
by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha)
from r''' have "r →⇩s r'''" by (blast intro: Abs)
moreover from Abs have "ss [→⇩s] ss'" by (iprover dest: listrelp_conj1)
ultimately have "(Lam [x].r) °° ss →⇩s (Lam [x].r''') °° ss'" by (rule better_sred_Abs)
with appL s show "(Lam [x].r) °° ss →⇩s r''" by simp
next
case (appR rs')
from Abs(6) [simplified] ‹ss' [→⇩β]⇩1 rs'›
have "ss [→⇩s] rs'" by (rule lemma4_aux)
with ‹r →⇩s r'› have "(Lam [x].r) °° ss →⇩s (Lam [x].r') °° rs'" by (rule better_sred_Abs)
with appR show "(Lam [x].r) °° ss →⇩s r''" by simp
next
case (beta t u' us')
then have Lam_eq: "(Lam [x].r') = (Lam [x].t)" and ss': "ss' = u' # us'"
and r'': "r'' = t[x::=u'] °° us'"
from Abs(6) ss' obtain u us where
ss: "ss = u # us" and u: "u →⇩s u'" and us: "us [→⇩s] us'"
by cases (auto dest!: listrelp_conj1)
have "r[x::=u] →⇩s r'[x::=u']" using ‹r →⇩s r'› and u by (rule lemma3)
with us have "r[x::=u] °° us →⇩s r'[x::=u'] °° us'" by (rule lemma1')
hence "(Lam [x].r) ° u °° us →⇩s r'[x::=u'] °° us'" by (rule better_sred_Beta)
with ss r'' Lam_eq show "(Lam [x].r) °° ss →⇩s r''" by (simp add: lam.inject alpha)
qed
next
case (Beta x s ss t r)
show ?case
by (rule better_sred_Beta) (rule Beta)+
qed

lemma rtrancl_beta_sred:
assumes r: "r →⇩β⇧* r'"
shows "r →⇩s r'" using r
by induct (iprover intro: refl_sred lemma4)+

subsection ‹Terms in normal form›

lemma listsp_eqvt [eqvt]:
assumes xs: "listsp p (xs::'a::pt_name list)"
shows "listsp ((pi::name prm) ∙ p) (pi ∙ xs)" using xs
apply induct
apply simp
apply simp
apply (rule listsp.intros)
apply (drule_tac pi=pi in perm_boolI)
apply perm_simp
apply assumption
done

inductive NF :: "lam ⇒ bool"
where
App: "listsp NF ts ⟹ NF (Var x °° ts)"
| Abs: "NF t ⟹ NF (Lam [x].t)"

equivariance NF
nominal_inductive NF

lemma Abs_NF:
assumes NF: "NF ((Lam [x].t) °° ts)"
shows "ts = []" using NF
proof cases
case (App us i)
thus ?thesis by (simp add: Var_apps_neq_Abs_apps [THEN not_sym])
next
case (Abs u)
thus ?thesis by simp
qed

text ‹
@{term NF} characterizes exactly the terms that are in normal form.
›

lemma NF_eq: "NF t = (∀t'. ¬ t →⇩β t')"
proof
assume H: "NF t"
show "∀t'. ¬ t →⇩β t'"
proof
fix t'
from H show "¬ t →⇩β t'"
proof (nominal_induct avoiding: t' rule: NF.strong_induct)
case (App ts t)
show ?case
proof
assume "Var t °° ts →⇩β t'"
then obtain rs where "ts [→⇩β]⇩1 rs"
with App show False
by (induct rs arbitrary: ts) (auto del: in_listspD)
qed
next
case (Abs t x)
show ?case
proof
assume "(Lam [x].t) →⇩β t'"
then show False using Abs
by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha)
qed
qed
qed
next
assume H: "∀t'. ¬ t →⇩β t'"
then show "NF t"
proof (nominal_induct t rule: Apps_lam_induct)
case (1 n ts)
then have "∀ts'. ¬ ts [→⇩β]⇩1 ts'"
by (iprover intro: apps_preserves_betas)
with 1(1) have "listsp NF ts"
by (induct ts) (auto simp add: in_listsp_conv_set)
then show ?case by (rule NF.App)
next
case (2 x u ts)
show ?case
proof (cases ts)
case Nil thus ?thesis by (metis 2 NF.Abs abs foldl_Nil)
next
case (Cons r rs)
have "(Lam [x].u) ° r →⇩β u[x::=r]" ..
then have "(Lam [x].u) ° r °° rs →⇩β u[x::=r] °° rs"
by (rule apps_preserves_beta)
with Cons have "(Lam [x].u) °° ts →⇩β u[x::=r] °° rs"
by simp
with 2 show ?thesis by iprover
qed
qed
qed

subsection ‹Leftmost reduction and weakly normalizing terms›

inductive
lred :: "lam ⇒ lam ⇒ bool"  (infixl "→⇩l" 50)
and lredlist :: "lam list ⇒ lam list ⇒ bool"  (infixl "[→⇩l]" 50)
where
"s [→⇩l] t ≡ listrelp (→⇩l) s t"
| Var: "rs [→⇩l] rs' ⟹ Var x °° rs →⇩l Var x °° rs'"
| Abs: "r →⇩l r' ⟹ (Lam [x].r) →⇩l (Lam [x].r')"
| Beta: "r[x::=s] °° ss →⇩l t ⟹ (Lam [x].r) ° s °° ss →⇩l t"

lemma lred_imp_sred:
assumes lred: "s →⇩l t"
shows "s →⇩s t" using lred
proof induct
case (Var rs rs' x)
then have "rs [→⇩s] rs'"
by induct (iprover intro: listrelp.intros)+
then show ?case by (rule sred.Var)
next
case (Abs r r' x)
from ‹r →⇩s r'›
have "(Lam [x].r) °° [] →⇩s (Lam [x].r') °° []" using listrelp.Nil
by (rule better_sred_Abs)
then show ?case by simp
next
case (Beta r x s ss t)
from ‹r[x::=s] °° ss →⇩s t›
show ?case by (rule better_sred_Beta)
qed

inductive WN :: "lam ⇒ bool"
where
Var: "listsp WN rs ⟹ WN (Var n °° rs)"
| Lambda: "WN r ⟹ WN (Lam [x].r)"
| Beta: "WN ((r[x::=s]) °° ss) ⟹ WN (((Lam [x].r) ° s) °° ss)"

lemma listrelp_imp_listsp1:
assumes H: "listrelp (λx y. P x) xs ys"
shows "listsp P xs" using H
by induct auto

lemma listrelp_imp_listsp2:
assumes H: "listrelp (λx y. P y) xs ys"
shows "listsp P ys" using H
by induct auto

lemma lemma5:
assumes lred: "r →⇩l r'"
shows "WN r" and "NF r'" using lred
by induct
(iprover dest: listrelp_conj1 listrelp_conj2
listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros
NF.intros)+

lemma lemma6:
assumes wn: "WN r"
shows "∃r'. r →⇩l r'" using wn
proof induct
case (Var rs n)
then have "∃rs'. rs [→⇩l] rs'"
by induct (iprover intro: listrelp.intros)+
then show ?case by (iprover intro: lred.Var)
qed (iprover intro: lred.intros)+

lemma lemma7:
assumes r: "r →⇩s r'"
shows "NF r' ⟹ r →⇩l r'" using r
proof induct
case (Var rs rs' x)
from ‹NF (Var x °° rs')› have "listsp NF rs'"
by cases simp_all
with Var(1) have "rs [→⇩l] rs'"
proof induct
case Nil
show ?case by (rule listrelp.Nil)
next
case (Cons x y xs ys)
hence "x →⇩l y" and "xs [→⇩l] ys" by (auto del: in_listspD)
thus ?case by (rule listrelp.Cons)
qed
thus ?case by (rule lred.Var)
next
case (Abs x ss ss' r r')
from ‹NF ((Lam [x].r') °° ss')›
have ss': "ss' = []" by (rule Abs_NF)
from Abs(4) have ss: "ss = []" using ss'
by cases simp_all
from ss' Abs have "NF (Lam [x].r')" by simp
hence "NF r'" by (cases rule: NF.strong_cases) (auto simp add: abs_fresh lam.inject alpha)
with Abs have "r →⇩l r'" by simp
hence "(Lam [x].r) →⇩l (Lam [x].r')" by (rule lred.Abs)
with ss ss' show ?case by simp
next
case (Beta x s ss t r)
hence "r[x::=s] °° ss →⇩l t" by simp
thus ?case by (rule lred.Beta)
qed

lemma WN_eq: "WN t = (∃t'. t →⇩β⇧* t' ∧ NF t')"
proof
assume "WN t"
then have "∃t'. t →⇩l t'" by (rule lemma6)
then obtain t' where t': "t →⇩l t'" ..
then have NF: "NF t'" by (rule lemma5)
from t' have "t →⇩s t'" by (rule lred_imp_sred)
then have "t →⇩β⇧* t'" by (rule lemma2)
with NF show "∃t'. t →⇩β⇧* t' ∧ NF t'" by iprover
next
assume "∃t'. t →⇩β⇧* t' ∧ NF t'"
then obtain t' where t': "t →⇩β⇧* t'" and NF: "NF t'"
by iprover
from t' have "t →⇩s t'" by (rule rtrancl_beta_sred)
then have "t →⇩l t'" using NF by (rule lemma7)
then show "WN t" by (rule lemma5)
qed

end

```