Quelle  Standardization.thy   Sprache: Isabelle

(*  Title:      HOL/Nominal/Examples/Standardization.thy
    Author:     Stefan Berghofer and Tobias Nipkow
    Copyright   2005, 2008 TU Muenchen
*)

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"
  by (finite_guess | simp add: fresh_nat | fresh_guess)+

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\<^sub>1 \ t\<^sub>2)[y::=s] = t\<^sub>1[y::=s] \ t\<^sub>2[y::=s]"
| subst_Lam: "x \ (y, s) \ (Lam [x].t)[y::=s] = (Lam [x].(t[y::=s]))"
  by (finite_guess | simp add: abs_fresh | fresh_guess)+

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)
     (perm_simp add: fresh_bij)+

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)
     (simp_all add: fresh_atm calc_atm abs_fresh)

lemma fresh_subst: 
  "(x::name) \ t \ x \ u \ x \ t[y::=u]"
  by (nominal_induct t avoiding: x y u rule: lam.strong_induct)
     (auto simp add: abs_fresh fresh_atm)

lemma fresh_subst':
  "(x::name) \ u \ x \ t[x::=u]"
  by (nominal_induct t avoiding: x u rule: lam.strong_induct)
     (auto simp add: abs_fresh fresh_atm)

lemma subst_forget: "(x::name) \ t \ t[x::=u] = t"
  by (nominal_induct t avoiding: x u rule: lam.strong_induct)
     (auto simp add: abs_fresh fresh_atm)

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)
     (auto simp add: fresh_subst subst_forget)

declare subst_Var [simp del]

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

lemma subst_neq [simp]: "x \ y \ (Var x)[y::=u] = Var x"
  by (simp add: subst_Var)

inductive beta :: "lam \ lam \ bool"  (infixl ‹→🚫β› 50)
  where
    beta: "x \ t \ (Lam [x].s) \ t \\<^sub>\ s[x::=t]"
  | appL [simp, intro!]: "s \\<^sub>\ t \ s \ u \\<^sub>\ t \ u"
  | appR [simp, intro!]: "s \\<^sub>\ t \ u \ s \\<^sub>\ u \ t"
  | abs [simp, intro!]: "s \\<^sub>\ t \ (Lam [x].s) \\<^sub>\ (Lam [x].t)"

equivariance beta
nominal_inductive beta
  by (simp_all add: abs_fresh fresh_subst')

lemma better_beta [simp, intro!]: "(Lam [x].s) \ t \\<^sub>\ 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 \\<^sub>\ ([(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 \\<^sub>\\<^sup>* t \ beta\<^sup>*\<^sup>* 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)"
proof (induct rs arbitrary: ss rule: rev_induct)
  case Nil then show ?case by (auto simp add: lam.inject)
next
  case (snoc x xs) then show ?case 
  by (induct ss rule: rev_induct) (auto simp add: lam.inject)
qed

lemma App_eq_foldl_conv:
  "(r \ s = t \\ ts) =
    (if ts = [] then r 🍋 s = t
    else (∃ss. ts = ss @ [s] ∧ r = t 🍋🍋 ss))"
  by (rule rev_exhaust [of ts]) (auto simp: lam.inject)

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"
proof (induct ss arbitrary: ts rule: rev_induct)
  case Nil then show ?case by simp
next
  case (snoc x xs) then show ?case
  by (induct ts rule: rev_induct) (auto simp add: lam.inject)
qed

lemma ex_head_tail:
  "\ts h. t = h \\ ts \ ((\n. h = Var n) \ (\x u. h = (Lam [x].u)))"
proof (induct t rule: lam.induct)
  case (App lam1 lam2)
  then show ?case
    by (metis foldl_Cons foldl_Nil foldl_append)
qed auto

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 Apps_lam_induct_aux:
  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"
proof (induct n arbitrary: t z rule: less_induct)
  case (less n)
  obtain ts h where t: "t = h \\ ts" and D: "(\a. h = Var a) \ (\x u. h = (Lam [x].u))"
    using ex_head_tail [of t] by metis
  show ?case 
    using D
  proof (elim exE disjE)
    fix a :: name
    assume h: "h = Var a"
    have "P z t" if "t \ set ts" for z t
    proof -
      have "size t < length ts + fold (+) (map size ts) 0"
        using that
        by (fastforce simp add: sum_list_map_remove1 fold_plus_sum_list_rev)
      then have "size t < size (Var a \\ ts)"
        by simp (simp add: add.commute foldl_conv_fold)
      then show ?thesis
        using h less.hyps less.prems t by blast
    qed
    then show "P z t"
      unfolding t h by (blast intro: assms)
  next
    fix x u
    assume h: "h = (Lam [x].u)"
    obtain y::name where y: "y \ (x, u, z)"
      by (metis exists_fresh' fin_supp)
    then have eq: "(Lam [x].u) = (Lam [y].([(y, x)] \ u))"
      by (metis alpha' fresh_prod lam.inject(3) perm_fresh_fresh)
    show "P z t"
      unfolding t h eq
    proof (intro assms strip)
      show "y \ z"
        by (simp add: y)
      have "size ([(y, x)] \ u) < size ((Lam [x].u) \\ ts)"
        by (simp add: eq)
      then show "P z ([(y, x)] \ u)" for z
        using h less.hyps less.prems t by blast
      show "P z t" if "t\set ts" for z t
      proof -
        have 2: "size t < size ((Lam [x].u) \\ ts)"
          using that
          apply (simp add: eq)
          apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
          apply (fastforce simp add: sum_list_map_remove1)
          done
        then show ?thesis
          using h less.hyps less.prems t by blast
      qed
    qed
  qed
qed

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"
  using Apps_lam_induct_aux [of P] assms by blast


subsection ‹Congruence rules›

lemma apps_preserves_beta [simp]:
    "r \\<^sub>\ s \ r \\ ss \\<^sub>\ s \\ ss"
  by (induct ss rule: rev_induct) auto

lemma rtrancl_beta_Abs [intro!]:
    "s \\<^sub>\\<^sup>* s' \ (Lam [x].s) \\<^sub>\\<^sup>* (Lam [x].s')"
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_AppL:
    "s \\<^sub>\\<^sup>* s' \ s \ t \\<^sub>\\<^sup>* s' \ t"
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_AppR:
    "t \\<^sub>\\<^sup>* t' \ s \ t \\<^sub>\\<^sup>* s \ t'"
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+

lemma rtrancl_beta_App [intro]:
    "s \\<^sub>\\<^sup>* s' \ t \\<^sub>\\<^sup>* t' \ s \ t \\<^sub>\\<^sup>* 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"
  by (simp add: step1_def)

lemma not_step1_Nil [iff]: "\ step1 r xs []"
  by (simp add: step1_def)

lemma Cons_step1_Cons [iff]:
    "step1 r (y # ys) (x # xs) \ r y x \ xs = ys \ x = y \ step1 r ys xs"
  apply (rule )
   apply (smt (verit, ccfv_SIG) append_eq_Cons_conv list.inject step1_def)
  by (metis append_Cons append_Nil step1_def)

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
  by (metis Cons_step1_Cons assms list.exhaust not_Nil_step1)

lemma append_step1I:
  "step1 r ys xs \ vs = us \ ys = xs \ step1 r vs us
    ==> step1 r (ys @ vs) (xs @ us)"
  by (smt (verit) append_Cons append_assoc step1_def)

lemma Snoc_step1_SnocD:
  assumes "step1 r (ys @ [y]) (xs @ [x])"
  shows "(step1 r ys xs \ y = x \ ys = xs \ r y x)"
  using assms
    apply (clarsimp simp: step1_def)
  by (metis butlast.simps(2) butlast_append butlast_snoc last.simps last_appendR list.simps(3))


subsection ‹Lifting beta-reduction to lists›

abbreviation
  list_beta :: "lam list \ lam list \ bool"  (infixl ‹[→🚫β]🚫1› 50) where
  "rs [\\<^sub>\]\<^sub>1 ss \ step1 beta rs ss"

lemma head_Var_reduction:
  "Var n \\ rs \\<^sub>\ v \ \ss. rs [\\<^sub>\]\<^sub>1 ss \ v = Var n \\ ss"
proof (induct u ≡ "Var n \\ rs" v arbitrary: rs set: beta)
  case (appL s t u)
  then show ?case
    by (smt (verit, best) App_eq_foldl_conv app_last append_step1I lam.distinct(1))
next
  case (appR s t u)
  then show ?case
    by (smt (verit, ccfv_SIG) App_eq_foldl_conv Cons_step1_Cons app_last append_step1I lam.distinct(1))
qed auto

lemma apps_betasE [case_names appL appR beta, consumes 1]:
  assumes major: "r \\ rs \\<^sub>\ s"
    and cases: "\r'. r \\<^sub>\ r' \ s = r' \\ rs \ R"
      "\rs'. rs [\\<^sub>\]\<^sub>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 -
  note [[simproc del: defined_all]]
  from major have
   "(\r'. r \\<^sub>\ r' \ s = r' \\ rs) \
    (∃rs'. rs [\\<^sub>\]\<^sub>1 rs' ∧ s = r 🍋🍋 rs') \
    (∃t u us. x ♯ r ⟶ r = (Lam [x].t) ∧ rs = u # us ∧ s = t[x::=u] 🍋🍋 us)"
  proof (nominal_induct u ≡ "r \\ rs" s avoiding: x r rs rule: beta.strong_induct)
    case (beta y t s)
    then show ?case
      apply (simp add: App_eq_foldl_conv split: if_split_asm)
       apply blast
      by (metis (no_types, lifting) abs_fresh(1) alpha' lam.fresh(3) lam.inject(3) subst_rename)
  next
    case (appL s t u)
    then show ?case
      apply (simp add: App_eq_foldl_conv split: if_split_asm)
      apply blast
      by (smt (verit) append_Cons append_step1I snoc_eq_iff_butlast)
  next
    case (appR s t u)
    then show ?case
      apply (simp add: App_eq_foldl_conv step1_def split: if_split_asm)
      apply force
      by (metis snoc_eq_iff_butlast)
  next
    case (abs s t x)
    then show ?case
      by blast
  qed
  with cases show ?thesis by blast
qed

lemma apps_preserves_betas [simp]:
    "rs [\\<^sub>\]\<^sub>1 ss \ r \\ rs \\<^sub>\ r \\ ss"
proof (induct rs arbitrary: ss rule: rev_induct)
  case Nil
  then show ?case by simp
next
  case (snoc x ts)
  then show ?case 
    apply (simp add: step1_def)
    by (smt (verit) appR app_last apps_preserves_beta foldl_Cons foldl_append)
qed


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 [\\<^sub>s] t \ listrelp (\\<^sub>s) s t"
| Var: "rs [\\<^sub>s] rs' \ Var x \\ rs \\<^sub>s Var x \\ rs'"
| Abs: "x \ (ss, ss') \ r \\<^sub>s r' \ ss [\\<^sub>s] ss' \ (Lam [x].r) \\ ss \\<^sub>s (Lam [x].r') \\ ss'"
| Beta: "x \ (s, ss, t) \ r[x::=s] \\ ss \\<^sub>s t \ (Lam [x].r) \ s \\ ss \\<^sub>s t"

equivariance sred
nominal_inductive sred
  by (simp add: abs_fresh)+

lemma better_sred_Abs:
  assumes H1: "r \\<^sub>s r'"
  and H2: "ss [\\<^sub>s] ss'"
  shows "(Lam [x].r) \\ ss \\<^sub>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 \\<^sub>s r')" by (rule perm_boolI)
  then have "([(y, x)] \ r) \\<^sub>s ([(y, x)] \ r')" by (simp add: eqvts)
  ultimately have "(Lam [y]. [(y, x)] \ r) \\ ss \\<^sub>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 \\<^sub>s t"
  shows "(Lam [x].r) \ s \\ ss \\<^sub>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 \\<^sub>s t"
    by (simp add: subst_rename)
  ultimately have "(Lam [y].[(y, x)] \ r) \ s \\ ss \\<^sub>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 \\<^sub>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 \\<^sub>s r'" and s: "s \\<^sub>s s'"
  shows "r \ s \\<^sub>s r' \ s'" using r
proof induct
  case (Var rs rs' x)
  then have "rs [\\<^sub>s] rs'" by (rule listrelp_conj1)
  moreover have "[s] [\\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
  ultimately have "rs @ [s] [\\<^sub>s] rs' @ [s']" by (rule listrelp_app)
  hence "Var x \\ (rs @ [s]) \\<^sub>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 [\\<^sub>s] ss'" by (rule listrelp_conj1)
  moreover have "[s] [\\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
  ultimately have "ss @ [s] [\\<^sub>s] ss' @ [s']" by (rule listrelp_app)
  with ‹r →🚫s r'\ have "(Lam [x].r) \\ (ss @ [s]) \\<^sub>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]) \\<^sub>s t \ s'" by (simp only: app_last)
  hence "(Lam [x].r) \ u \\ (ss @ [s]) \\<^sub>s t \ s'" by (rule better_sred_Beta)
  thus ?case by (simp only: app_last)
qed

lemma lemma1':
  assumes ts: "ts [\\<^sub>s] ts'"
  shows "r \\<^sub>s r' \ r \\ ts \\<^sub>s r' \\ ts'" using ts
  by (induct arbitrary: r r') (auto intro: lemma1)

lemma listrelp_betas:
  assumes ts: "listrelp (\\<^sub>\\<^sup>*) ts ts'"
  shows "\t t'. t \\<^sub>\\<^sup>* t' \ t \\ ts \\<^sub>\\<^sup>* t' \\ ts'" using ts
  by induct auto

lemma lemma2:
  assumes t: "t \\<^sub>s u"
  shows "t \\<^sub>\\<^sup>* u" using t
  by induct (auto dest: listrelp_conj2
    intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp)

lemma lemma3:
  assumes r: "r \\<^sub>s r'"
  shows "s \\<^sub>s s' \ r[x::=s] \\<^sub>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 [\\<^sub>s] map (\t. t[x::=s']) rs'"
    by induct (auto intro: listrelp.intros Var)
  moreover have "Var y[x::=s] \\<^sub>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] \\<^sub>s r'[x::=s']" by fast
  moreover from Abs(8) ‹s →🚫s s'\ have "map (\t. t[x::=s]) ss [\\<^sub>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 \\<^sub>s u \ (\r. u \\<^sub>\ r \ t \\<^sub>s r)) rs rs'"
  shows "rs' [\\<^sub>\]\<^sub>1 ss \ rs [\\<^sub>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 \\<^sub>\ y' ∧ ys' = ys \ y' = y ∧ ys [→🚫β]🚫1 ys'" by simp
    hence "x # xs [\\<^sub>s] y' # ys'"
    proof
      assume H: "y \\<^sub>\ y' \ ys' = ys"
      with Cons' have "x \\<^sub>s y'" by blast
      moreover from Cons' have "xs [\\<^sub>s] ys" by (iprover dest: listrelp_conj1)
      ultimately have "x # xs [\\<^sub>s] y' # ys" by (rule listrelp.Cons)
      with H show ?thesis by simp
    next
      assume H: "y' = y \ ys [\\<^sub>\]\<^sub>1 ys'"
      with Cons' have "x \\<^sub>s y'" by blast
      moreover from H have "xs [\\<^sub>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 \\<^sub>s r'"
  shows "r' \\<^sub>\ r'' \ r \\<^sub>s r''" using r
proof (nominal_induct avoiding: r'' rule: sred.strong_induct)
  case (Var rs rs' x)
  then obtain ss where rs: "rs' [\\<^sub>\]\<^sub>1 ss" and r'': "r'' = Var x \\ ss"
    by (blast dest: head_Var_reduction)
  from Var(1) [simplified] rs have "rs [\\<^sub>s] ss" by (rule lemma4_aux)
  hence "Var x \\ rs \\<^sub>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' \\<^sub>\ r'''" using \x \ r''\
      by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha)
    from r''' have "r \\<^sub>s r'''" by (blast intro: Abs)
    moreover from Abs have "ss [\\<^sub>s] ss'" by (iprover dest: listrelp_conj1)
    ultimately have "(Lam [x].r) \\ ss \\<^sub>s (Lam [x].r''') \\ ss'" by (rule better_sred_Abs)
    with appL s show "(Lam [x].r) \\ ss \\<^sub>s r''" by simp
  next
    case (appR rs')
    from Abs(6) [simplified] ‹ss' [\\<^sub>\]\<^sub>1 rs'›
    have "ss [\\<^sub>s] rs'" by (rule lemma4_aux)
    with ‹r →🚫s r'\ have "(Lam [x].r) \\ ss \\<^sub>s (Lam [x].r') 🍋🍋 rs'" by (rule better_sred_Abs)
    with appR show "(Lam [x].r) \\ ss \\<^sub>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'"
      by (simp_all add: abs_fresh)
    from Abs(6) ss' obtain u us where
      ss: "ss = u # us" and u: "u \\<^sub>s u'" and us: "us [\\<^sub>s] us'"
      by cases (auto dest!: listrelp_conj1)
    have "r[x::=u] \\<^sub>s r'[x::=u']" using ‹r →🚫s r'\ and u by (rule lemma3)
    with us have "r[x::=u] \\ us \\<^sub>s r'[x::=u'] \\ us'" by (rule lemma1')
    hence "(Lam [x].r) \ u \\ us \\<^sub>s r'[x::=u'] \\ us'" by (rule better_sred_Beta)
    with ss r'' Lam_eq show "(Lam [x].r) \\ ss \\<^sub>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 \\<^sub>\\<^sup>* r'"
  shows "r \\<^sub>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
by induction (use perm_app in force)+

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
  by (simp add: abs_fresh)

lemma Abs_NF:
  assumes NF: "NF ((Lam [x].t) \\ ts)"
  shows "ts = []" using NF
  by (metis Abs_eq_apps_conv NF.cases Var_apps_neq_Abs_apps)

text ‹
🍋‹NF› characterizes exactly the terms that are in normal form.
›
  
lemma NF_eq: "NF t = (\t'. \ t \\<^sub>\ t')"
proof
  assume H: "NF t"
  show "\t'. \ t \\<^sub>\ t'"
  proof
    fix t'
    from H show "\ t \\<^sub>\ t'"
    proof (nominal_induct avoiding: t' rule: NF.strong_induct)
      case (App ts t)
      show ?case
      proof
        assume "Var t \\ ts \\<^sub>\ t'"
        then obtain rs where "ts [\\<^sub>\]\<^sub>1 rs"
          by (iprover dest: head_Var_reduction)
        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) \\<^sub>\ 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 \\<^sub>\ t'"
  then show "NF t"
  proof (nominal_induct t rule: Apps_lam_induct)
    case (1 n ts)
    then have "\ts'. \ ts [\\<^sub>\]\<^sub>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 \\<^sub>\ u[x::=r]" ..
      then have "(Lam [x].u) \ r \\ rs \\<^sub>\ u[x::=r] \\ rs"
        by (rule apps_preserves_beta)
      with Cons have "(Lam [x].u) \\ ts \\<^sub>\ 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 [\\<^sub>l] t \ listrelp (\\<^sub>l) s t"
| Var: "rs [\\<^sub>l] rs' \ Var x \\ rs \\<^sub>l Var x \\ rs'"
| Abs: "r \\<^sub>l r' \ (Lam [x].r) \\<^sub>l (Lam [x].r')"
| Beta: "r[x::=s] \\ ss \\<^sub>l t \ (Lam [x].r) \ s \\ ss \\<^sub>l t"

lemma lred_imp_sred:
  assumes lred: "s \\<^sub>l t"
  shows "s \\<^sub>s t" using lred
proof induct
  case (Var rs rs' x)
  then have "rs [\\<^sub>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) \\ [] \\<^sub>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 \\<^sub>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 \\<^sub>l r'" using wn
proof induct
  case (Var rs n)
  then have "\rs'. rs [\\<^sub>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 \\<^sub>s r'"
  shows "NF r' \ r \\<^sub>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 [\\<^sub>l] rs'"
  proof induct
    case Nil
    show ?case by (rule listrelp.Nil)
  next
    case (Cons x y xs ys) 
    hence "x \\<^sub>l y" and "xs [\\<^sub>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 \\<^sub>l r'" by simp
  hence "(Lam [x].r) \\<^sub>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 \\<^sub>l t" by simp
  thus ?case by (rule lred.Beta)
qed

lemma WN_eq: "WN t = (\t'. t \\<^sub>\\<^sup>* t' \ NF t')"
proof
  assume "WN t"
  then have "\t'. t \\<^sub>l t'" by (rule lemma6)
  then obtain t' where t': "t \\<^sub>l t'" ..
  then have NF: "NF t'" by (rule lemma5)
  from t' have "t \\<^sub>s t'" by (rule lred_imp_sred)
  then have "t \\<^sub>\\<^sup>* t'" by (rule lemma2)
  with NF show "\t'. t \\<^sub>\\<^sup>* t' \ NF t'" by iprover
next
  assume "\t'. t \\<^sub>\\<^sup>* t' \ NF t'"
  then obtain t' where t': "t \\<^sub>\\<^sup>* t'" and NF: "NF t'"
    by iprover
  from t' have "t \\<^sub>s t'" by (rule rtrancl_beta_sred)
  then have "t \\<^sub>l t'" using NF by (rule lemma7)
  then show "WN t" by (rule lemma5)
qed

end