Theory Lam_ml

section ‹Introduction›
(*<*) 
theory Lam_ml
imports "HOL-Nominal.Nominal" "HOL-Library.LaTeXsugar"
begin (*>*)
text_raw ‹\label{chap:formal}›

text ‹This article contains a formalization of the strong normalization
theorem for the $\lambda_{ml}$-calculus. The formalization is based on a proof
by Lindley and Stark \<^cite>‹"TT-lifting"›. An informal description of the
formalization can be found in \<^cite>‹"Doczkal:09"›.

This formalization extends the example proof of strong normalization for the
simply-typed $\lambda$-calculus, which is included in the Isabelle distribution
\<^cite>‹"SN.thy"›. The parts of the original proof which have been left unchanged
are not displayed in this document.

The next section deals with the formalization of syntax, typing, and
substitution. Section~\ref{sec:reduction} contains the formalization of the
reduction relation. Section~\ref{sec:stacks} defines stacks which are used to
define the reducibility relation in Section~\ref{sec:reducibility-formal}. The
following sections contain proofs about the reducibility relation, ending with
the normalization theorem in Section~\ref{sec:FTLR}.›

section ‹The Calculus›
text_raw ‹\label{sec:calc}›

atom_decl name

nominal_datatype trm = 
    Var "name" 
  | App "trm" "trm"
  | Lam "«name»trm"      (‹Λ _ . _› [0,120] 120)
  | To "trm" "«name»trm" (‹_ to _ in _› [141,0,140] 140) 
  | Ret "trm" (‹[_]›)


declare trm.inject[simp]
lemmas name_swap_bij = pt_swap_bij''[OF pt_name_inst at_name_inst]
lemmas ex_fresh = exists_fresh'[OF fin_supp]

lemma alpha'' :
  fixes x y :: name and t::trm
  assumes a: "x ♯ t"
  shows "[y].t = [x].([(y,x)] ∙ t)"
proof -
  from a have aux: "y ♯ [(y, x)] ∙ t"
    by (subst fresh_bij[THEN sym, of _ _ "[(x,y)]"]) 
        (auto simp add: perm_swap calc_atm)
  thus ?thesis  
    by(auto simp add: alpha perm_swap name_swap_bij fresh_bij)
qed

text ‹Even though our types do not involve binders, we still need to formalize
them as nominal datatypes to obtain a permutation action. This is required to
establish equivariance of the typing relation.›

nominal_datatype ty =
    TBase
  | TFun "ty" "ty" (infix ‹→› 200)
  | T "ty" 

text‹Since we cannot use typed variables, we have to formalize typing
contexts. Typing contexts are formalized as lists. A context is \textit{valid}
if no name occurs twice.›

inductive 
  valid :: "(name×ty) list ⇒ bool"
where
  v1[intro]: "valid []"
| v2[intro]: "⟦valid Γ;x♯Γ⟧⟹ valid ((x,σ)#Γ)"
equivariance valid 

lemma fresh_ty: 
  fixes x :: name and τ::ty
  shows "x ♯ τ"
by (induct τ rule: ty.induct) (auto)

lemma fresh_context: 
  fixes  Γ :: "(name×ty)list"
  assumes a: "x ♯ Γ"
  shows "¬(∃ τ . (x,τ)∈set Γ)"
using a
by (induct Γ) (auto simp add: fresh_prod fresh_list_cons fresh_atm)

inductive 
  typing :: "(name×ty) list⇒trm⇒ty⇒bool" (‹_ ⊢ _ : _› [60,60,60] 60)
where
  t1[intro]: "⟦valid Γ; (x,τ)∈set Γ⟧ ⟹ Γ ⊢ Var x : τ"
| t2[intro]: "⟦Γ ⊢ s : τ→σ; Γ ⊢ t : τ⟧ ⟹ Γ ⊢ App s t : σ"
| t3[intro]: "⟦x ♯ Γ; ((x,τ)#Γ) ⊢ t : σ⟧ ⟹ Γ ⊢ Λ x . t : τ→σ" 
| t4[intro]: "⟦ Γ ⊢ s : σ ⟧ ⟹ Γ ⊢ [s] : T σ" 
| t5[intro]: "⟦x ♯ (Γ,s); Γ ⊢ s : T σ ; ((x,σ)#Γ) ⊢ t : T τ ⟧ 
                ⟹ Γ ⊢ s to x in t : T τ" 
equivariance typing
nominal_inductive typing 
  by(simp_all add: abs_fresh fresh_ty)

text ‹Except for the explicit requirement that contexts be valid in the
variable case and the freshness requirements in \isa{t3} and \isa{t5}, this
typing
relation is a direct translation of the original typing relation in
\<^cite>‹"TT-lifting"› to Curry-style typing.›

fun
  lookup :: "(name×trm) list ⇒ name ⇒ trm"   
where
  "lookup [] x        = Var x"
| "lookup ((y,e)#θ) x = (if x=y then e else lookup θ x)"

lemma lookup_eqvt[eqvt]:
  fixes pi::"name prm"
  and   θ::"(name×trm) list"
  and   x::"name"
  shows "pi ∙ (lookup θ x) = lookup (pi ∙ θ) (pi ∙ x)"
by (induct θ) (auto simp add: eqvts)

nominal_primrec
  psubst :: "(name×trm) list ⇒ trm ⇒ trm"  (‹_<_>› [95,95] 205)
where 
    "θ<Var x> = lookup θ x"
  | "θ<App s t> = App (θ<s>) (θ<t>)"
  | "x ♯ θ ⟹ θ<Λ x .s> = Λ x . (θ<s>)"
  | "θ<[t]> = [θ<t>]"
  | "⟦ x ♯ θ ; x ♯ t ⟧ ⟹ θ<t to x in s> = (θ<t>) to x in (θ<s>)"
by(finite_guess+ , (simp add: abs_fresh)+ , fresh_guess+)

lemma psubst_eqvt[eqvt]:
  fixes pi::"name prm"
  shows "pi ∙ (θ<t>) = (pi ∙ θ)<(pi ∙ t)>"
by(nominal_induct t avoiding: θ rule:trm.strong_induct)
  (auto simp add: eqvts fresh_bij)

abbreviation 
  subst :: "trm ⇒ name ⇒ trm ⇒ trm" (‹_[_::=_]› [200,100,100] 200)
where 
  "t[x::=t']  ≡ ([(x,t')])<t>"

lemma subst[simp]:
shows "(Var x)[y::=v] = (if x = y then v else Var x)"
  and "(App s t)[y::=v] = App (s[y::=v]) (t[y::=v])"
  and "x ♯ (y,v) ⟹ (Λ x . t)[y::=v] = Λ x .t[y::=v]"
  and "x ♯ (s,y,v) ⟹ (s to x in t)[y::=v] = s[y::=v] to x in t[y::=v]"
  and "([s])[y::=v] = [s[y::=v]]"
by(simp_all add: fresh_list_cons fresh_list_nil)

lemma subst_rename: 
  assumes a: "y ♯ t"
  shows "([(y,x)]∙t)[y::=v] = t[x::=v]"
using a
by(nominal_induct t avoiding: x y v rule: trm.strong_induct)
    (auto simp add: calc_atm fresh_atm abs_fresh fresh_prod fresh_aux)
lemmas subst_rename' = subst_rename[THEN sym]

lemma forget: "x ♯ t ⟹ t[x::=v] = t"
by(nominal_induct t avoiding: x v rule: trm.strong_induct)
    (auto simp add: abs_fresh fresh_atm)

lemma fresh_fact: 
  fixes x::"name"
  assumes x: "x ♯ v"   "x ♯ t"
  shows "x ♯ t[y::=v]"
using x
by(nominal_induct t avoiding: x y v rule: trm.strong_induct)
    (auto simp add: abs_fresh fresh_atm)

lemma fresh_fact': 
  fixes x::"name"
  assumes x: "x ♯ v"
  shows "x ♯ t[x::=v]"
using x
by(nominal_induct t avoiding: x v rule: trm.strong_induct)
    (auto simp add: abs_fresh fresh_atm)

lemma subst_lemma:  
  assumes a: "x≠y"
  and     b: "x ♯ u"
  shows "s[x::=v][y::=u] = s[y::=u][x::=v[y::=u]]"
using a b
by(nominal_induct s avoiding: x y u v rule: trm.strong_induct)
    (auto simp add: fresh_fact forget)

lemma id_subs: 
  shows "t[x::=Var x] = t"
by(nominal_induct t avoiding: x rule:trm.strong_induct) auto

text ‹In addition to the facts on simple substitution we also need some facts
on parallel substitution. In particular we want to be able to extend a parallel
substitution with a simple one.›

lemma lookup_fresh:
  fixes z::"name"
  assumes "z♯θ"   "z♯x"
  shows "z♯ lookup θ x"
using assms 
by(induct rule: lookup.induct) 
  (auto simp add: fresh_list_cons)

lemma lookup_fresh':
  assumes a: "z♯θ"
  shows "lookup θ z = Var z"
using a
by (induct rule: lookup.induct)
   (auto simp add: fresh_list_cons fresh_prod fresh_atm)

lemma psubst_fresh_fact:
  fixes x :: name
  assumes a: "x ♯ t" and b: "x ♯ θ" 
  shows "x ♯ θ<t>"
using a b
by(nominal_induct t avoiding: θ x rule:trm.strong_induct) 
    (auto simp add: lookup_fresh abs_fresh)

lemma psubst_subst:
  assumes a: "x ♯ θ"
  shows "θ<t>[x::=s] = ((x,s)#θ)<t>"
  using a
by(nominal_induct t avoiding: θ x s rule: trm.strong_induct)
    (auto simp add: fresh_list_cons fresh_atm forget 
      lookup_fresh lookup_fresh' fresh_prod psubst_fresh_fact)

section ‹The Reduction Relation›
text_raw ‹\label{sec:reduction}›

text ‹With substitution in place, we can now define the reduction relation on
$\lambda_{ml}$-terms. To derive strong induction and case rules, all the rules
must be vc-compatible (cf. \<^cite>‹"nominal-techniques"›). This requires some
additional freshness conditions. Note that in this particular case the
additional freshness conditions only serve the technical purpose of
automatically deriving strong reasoning principles. To show that the version
with freshness conditions defines the same relation as the one without the
freshness conditions, we also state this version and prove equality of the two
relations. 

This requires quite some effort and is something that is certainly undesirable
in nominal reasoning. Unfortunately, handling the reduction rule \isa{r10} which
rearranges the binding structure, appeared to be impossible without going
through this.›


inductive std_reduction :: "trm ⇒ trm ⇒ bool" (‹_ ↝ _› [80,80] 80)
where
  std_r1[intro!]:"s ↝ s' ⟹ App s t ↝ App s' t"
| std_r2[intro!]:"t ↝ t' ⟹ App s t ↝ App s t'"
| std_r3[intro!]:"App (Λ x . t) s ↝ t[x::=s]"

| std_r4[intro!]:"t ↝ t' ⟹ Λ x . t ↝ Λ x . t'"
| std_r5[intro!]:"x ♯ t ⟹ Λ x . App t (Var x) ↝ t"

| std_r6[intro!]:"⟦ s ↝ s' ⟧ ⟹ s to x in t ↝ s' to x in t"
| std_r7[intro!]:"⟦ t ↝ t' ⟧ ⟹ s to x in t ↝ s  to x in t'"
| std_r8[intro!]:"[s] to x in t ↝ t[x::=s]"
| std_r9[intro!]:"x ♯ s ⟹ s to x in [Var x] ↝ s"
| std_r10[intro!]: "⟦ x ♯ y; x ♯ u⟧ 
                     ⟹ (s to x in t) to y in u ↝ s to x in (t to y in u)"
| std_r11[intro!]: "s ↝ s' ⟹ [s] ↝ [s']"

inductive 
  reduction :: "trm ⇒ trm ⇒ bool" (‹_ ↦ _› [80,80] 80)
where
  r1[intro!]:"s ↦ s' ⟹ App s t ↦ App s' t"
| r2[intro!]:"t ↦ t' ⟹ App s t ↦ App s t'"
| r3[intro!]:"x ♯ s ⟹ App (Λ x . t) s ↦ t[x::=s]"

| r4[intro!]:"t ↦ t' ⟹ Λ x . t ↦ Λ x . t'"
| r5[intro!]:"x ♯ t ⟹ Λ x . App t (Var x) ↦ t"

| r6[intro!]:"⟦ x ♯ (s,s') ; s ↦ s' ⟧ ⟹ s to x in t ↦ s' to x in t"
| r7[intro!]:"⟦ x ♯ s ; t ↦ t' ⟧ ⟹ s to x in t ↦ s  to x in t'"
| r8[intro!]:"x ♯ s ⟹ [s] to x in t ↦ t[x::=s]"
| r9[intro!]:"x ♯ s ⟹ s to x in [Var x] ↦ s"
| r10[intro!]: "⟦ x ♯ (y,s,u) ; y ♯ (s,t) ⟧ 
                  ⟹ (s to x in t) to y in u ↦ s to x in (t to y in u)"
| r11[intro!]: "s ↦ s' ⟹ [s] ↦ [s']" 
equivariance reduction
nominal_inductive reduction
  by(auto simp add: abs_fresh fresh_fact' fresh_prod fresh_atm)


text ‹In order to show adequacy, the extra freshness conditions in the rules
\isa{r3}, \isa{r6}, \isa{r7}, \isa{r8}, \isa{r9}, and \isa{r10} need to be
discharged.›

text_raw ‹\label{pg:alpha-begin}›

lemma r3'[intro!]: "App (Λ x . t) s ↦ t[x::=s]"
proof -
  obtain x'::name where s: "x' ♯ s" and t: "x' ♯ t"
    using ex_fresh[of "(s,t)"] by (auto simp add: fresh_prod)
  from t have "App (Λ x . t) s = App (Λ x' . ([(x,x')] ∙ t)) s" 
    by (simp add: alpha'')
  also from s have "… ↦ ([(x, x')] ∙ t)[x'::=s]" ..
  also have "… = t[x::=s]" using t 
    by (auto simp add: subst_rename') (metis perm_swap)
  finally show ?thesis .
qed 
declare r3[rule del]


lemma r6'[intro]:
  fixes s :: trm 
  assumes r: "s ↦ s'"
  shows "s to x in t ↦ s' to x in t"
using assms
proof -
  obtain x'::name where s: "x' ♯ (s, s')" and t: "x' ♯ t"
    using ex_fresh[of "(s,s',t)"] by (auto simp add: fresh_prod)
  from t have "s to x in t = s to x' in ([(x,x')] ∙ t)"
    by (simp add: alpha'')
  also from s r have "… ↦ s' to x' in ([(x, x')] ∙ t)" ..
  also from t have "… = s' to x in t"
    by (simp add: alpha'')
  finally show ?thesis .
qed
declare r6[rule del]

lemma r7'[intro]: 
  fixes t :: trm
  assumes "t ↦ t'"
  shows "s to x in t ↦ s to x in t'"
using assms
proof -
  obtain x'::name where f: "x' ♯ t"   "x' ♯ t'"   "x' ♯ s"   "x' ♯ x" 
    using ex_fresh[of "(t,t',s,x)"] by(auto simp add:fresh_prod)
  hence a: "s to x in t = s to x' in ([(x,x')] ∙ t)" 
    by (auto simp add: alpha'')
  from assms have "([(x,x')] ∙ t) ↦ [(x,x')] ∙ t'" 
    by (simp add: eqvts)
  hence r: "s to x' in ([(x,x')] ∙ t) ↦ s to x' in ([(x,x')] ∙ t')" 
    using f by auto 
  from f have "s to x in t' = s to x' in ([(x,x')] ∙ t')" 
    by (auto simp add: alpha'')
  with a r show ?thesis by (simp del: trm.inject)
qed
declare r7[rule del]

lemma r8'[intro!]: "[s] to x in t ↦ t[x::=s]"
proof - 
  obtain x'::name where s: "x' ♯ s" and t: "x' ♯ t"
    using ex_fresh[of "(s,t)"] by (auto simp add: fresh_prod)
  from t have "[s] to x in t = [s] to x' in ([(x,x')] ∙ t)" 
    by (simp add: alpha'')
  also from s have "… ↦ ([(x, x')] ∙ t)[x'::=s]" ..
  also have "… = t[x::=s]" using t 
    by (auto simp add: subst_rename') (metis perm_swap)
  finally show ?thesis .
qed
declare r8[rule del]

lemma r9'[intro!]: "s to x in [Var x] ↦ s"
proof - 
  obtain x'::name where f: "x' ♯ s"   "x' ♯ x" 
    using ex_fresh[of "(s,x)"] by(auto simp add:fresh_prod)
  hence "s to x' in [Var x'] ↦ s" by auto
  moreover have "s to x' in ([Var x']) = s to x in ([Var x])"
    by (auto simp add: alpha fresh_atm swap_simps)
  ultimately show ?thesis by simp
qed
declare r9[rule del]

text ‹While discharging these freshness conditions is easy for rules involving
only one binder it unfortunately becomes quite tedious for the assoc rule
\isa{r10}. This is due to the complex binding structure of this rule which
includes \textit{four} binding occurrences of two different names. Furthermore,
the binding structure changes from the left to the right: On the left hand
side, $x$ is only bound in $t$, whereas on the right hand side the scope of $x$
extends over the whole term @{term "(t to y in u)"}.›

lemma r10'[intro!]: 
  assumes xf: "x ♯ y"   "x ♯ u"
  shows "(s to x in t) to y in u ↦ s to x in (t to y in u)"
proof -
  obtain y'::name ― ‹suitably fresh›
    where y: "y' ♯ s"   "y' ♯ x"   "y' ♯ t"   "y' ♯ u" 
    using ex_fresh[of "(s,x,t,u,[(x, x')] ∙ t)"] 
    by (auto simp add: fresh_prod)
  obtain x'::name 
    where x: "x' ♯ s"   "x' ♯ y'"   "x' ♯ y"  "x' ♯ t"   "x' ♯ u"   
             "x' ♯ ([(y,y')] ∙ u)"
    using ex_fresh[of "(s,y',y,t,u,([(y,y')] ∙ u))"] 
    by (auto simp add: fresh_prod)
  from x y have yaux: "y' ♯ [(x, x')] ∙ t"
    by(simp add: fresh_left perm_fresh_fresh fresh_atm)
   have "(s to x in t) to y in u = (s to x in t) to y' in ([(y,y')] ∙ u)"
    using ‹y' ♯ u› by (simp add: alpha'')
  also have "… = (s to x' in ([(x,x')] ∙ t)) to y' in ([(y,y')] ∙ u)"
    using ‹x' ♯ t› by (simp add: alpha'')
  also have "… ↦ s to x' in (([(x,x')] ∙ t) to y' in ([(y,y')] ∙ u))"
    using x y yaux by (auto simp add: fresh_prod) 
  also have " … = s to x' in (([(x,x')] ∙ t) to y in u)"
    using ‹y' ♯ u› by (simp add: abs_fun_eq1 alpha'')
  also have "… = s to x in (t to y in u)"
  proof (subst trm.inject)
    from xf x have swap: "[(x,x')] ∙ y = y"   "[(x,x')] ∙ u = u " 
      by(auto simp add: fresh_atm perm_fresh_fresh )
    with x show "s = s ∧ [x'].([(x, x')] ∙ t) to y in u = [x].t to y in u"
      by (auto simp add: alpha''[of x' _ x] abs_fresh abs_fun_eq1 swap)
  qed
  finally show ?thesis .
qed
declare r10[rule del]

text_raw ‹\label{pg:alpha-end}›

text ‹Since now all the introduction rules of the vc-compatible reduction
relation exactly match their standard counterparts, both directions of the
adequacy proof are trivial inductions.›

theorem adequacy: "s ↦ t = s ↝ t"
by (auto elim:reduction.induct std_reduction.induct)

text ‹Next we show that the reduction relation preserves freshness and is in
turn preserved under substitution.›

lemma reduction_fresh: 
  fixes x::"name"
  assumes r: "t ↦ t'"
  shows "x ♯ t ⟹ x ♯ t'"
using r
by(nominal_induct t t' avoiding: x rule: reduction.strong_induct)
    (auto simp add: abs_fresh fresh_fact fresh_atm)

lemma reduction_subst:
  assumes a: " t ↦ t' "
  shows "t[x::=v] ↦ t'[x::=v]"
using a
by(nominal_induct t t' avoiding: x v rule: reduction.strong_induct)
  (auto simp add: fresh_atm fresh_fact subst_lemma fresh_prod abs_fresh)


(*section {* Strong Normalization *}
text_raw {* \label{sec:SN-formal} *} *)

text ‹Following \<^cite>‹"SN.thy"›, we use an inductive variant of strong
normalization, as it allows for inductive proofs on terms being strongly
normalizing, without establishing that
the reduction relation is finitely branching.›   


inductive 
  SN :: "trm ⇒ bool"
where
  SN_intro: "(⋀ t' . t ↦ t' ⟹ SN t') ⟹ SN t" 

(*
text {* It remains to be shown that this definition actually excludes infinite
sequences of reductions. We define a term $t$ to be diverging, written @{term
"DIV t"}, if there is some infinite sequence $S$ of reductions beginning at
$t$. *}

definition DIV :: "trm ⇒ bool"
where
  "DIV t ≡ ∃ (S::nat ⇒ trm) .  t = S 0 ∧ (∀ n . S n ↦ S (n + 1))"

theorem "SN t ⟹ ¬ DIV t"
proof (induct rule:SN.induct)
  case (SN_intro t)
  have ih: "⋀t'. t ↦ t' ⟹ ¬ DIV t'" by fact
  moreover have "DIV t ⟹ ∃ t' . t ↦ t' ∧ DIV t'"
  proof -
    assume "DIV t" from this obtain S::"nat⇒trm" 
      where S: "t = S 0 ∧ (∀ n . S n ↦ S (n + 1))"
      unfolding DIV_def .. 
    let ?t = "S 1" let ?S = "λ n . S (n + 1)"
    from S have " t ↦ ?t" by auto
    moreover { 
      from S have "?t = ?S 0 ∧ (∀ n . ?S n ↦ ?S (n + 1))" by auto
      hence "DIV ?t" unfolding DIV_def by auto}
    ultimately show ?thesis by blast
  qed
  ultimately show "¬ DIV t" using ih by blast
qed


theorem "¬ SN t ⟹ DIV t"
proof -
  fix t assume t: "¬ SN t"
  let ?NSN = "{ t . ¬ SN t }"
  have "∀ t ∈ ?NSN .  ∃ t' . t ↦ t' ∧ ¬ SN t'"
    by (auto intro: SN_intro)
  hence " ∃ f . ∀ t ∈ ?NSN . t ↦ f t ∧ ¬ SN (f t)"
    by (rule bchoice)
  from this obtain f where f: "∀ t ∈ ?NSN . t ↦ f t ∧ ¬ SN (f t)" ..
  let ?S = "λ n . (f^^n) t"
  { fix n from t f have  "?S n ↦ ?S (n + 1) ∧ ¬ SN (?S (n + 1))"
      by (induct n) auto }
  hence "t = ?S 0 ∧ (∀ n . ?S n ↦ ?S (n + 1))" by auto
  thus "DIV t" unfolding DIV_def  by(rule exI[where x="?S"])
qed

text{* For the normalization theorem, we merely need that strong normalization
is preserved under reduction and some lemmas on normal terms. *}
*)

lemma SN_preserved[intro]: 
  assumes a: "SN t"   "t ↦ t'"
  shows "SN t'"
using a by (cases) (auto)

definition "NORMAL" :: "trm ⇒ bool"
where
  "NORMAL t ≡ ¬(∃t'. t ↦ t')"

lemma normal_var: "NORMAL (Var x)"
unfolding NORMAL_def by (auto elim: reduction.cases)

lemma normal_implies_sn : "NORMAL s ⟹ SN s"
unfolding NORMAL_def by(auto intro: SN_intro)

section ‹Stacks›
text_raw ‹\label{sec:stacks}›

text‹As explained in \<^cite>‹"TT-lifting"›, the monadic type structure of
the $\lambda_{ml}$-calculus does not lend itself to an easy definition of a
logical relation along the type structure of the calculus. Therefore, we need to
introduce stacks as an auxiliary notion to handle the monadic type constructor
$T$. Stacks can be thought of as lists of term abstractions @{term "[x].t"}. The
notation for stacks is chosen with this resemblance in mind.›

nominal_datatype stack = Id | St "«name»trm" "stack" (‹[_]_≫_›)

lemma stack_exhaust :
  fixes c :: "'a::fs_name"
  shows "k = Id ∨ (∃ y n l  . y ♯ l ∧ y ♯ c ∧ k = [y]n≫l)"
by(nominal_induct k avoiding: c rule: stack.strong_induct) (auto)

nominal_primrec 
  length :: "stack ⇒ nat" ( ‹|_|›)
where
  "|Id| = 0" 
| "y ♯ L ⟹ length ([y]n≫L) = 1 + |L|"
by(finite_guess+,auto simp add: fresh_nat,fresh_guess)


text‹Together with the stack datatype, we introduce the notion of dismantling
a term onto a stack. Unfortunately, the dismantling operation has no easy
primitive recursive formulation. The Nominal package, however, only provides a
recursion combinator for primitive recursion. This means that for dismantling
one has to prove pattern completeness, right uniqueness, and termination
explicitly.›

function
  dismantle :: "trm ⇒ stack ⇒ trm" (‹_ ⋆ _› [160,160] 160)
where
  "t ⋆ Id = t" |
  "x ♯ (K,t) ⟹ t ⋆ ([x]s≫K) = (t to x in s) ⋆ K"
proof -    ― ‹pattern completeness›
  fix P :: bool and arg::"trm × stack"
  assume id: "⋀t. arg = (t, stack.Id) ⟹ P"
    and st: "⋀x K t s. ⟦x ♯ (K, t); arg = (t, [x]s≫K)⟧ ⟹ P"
  { assume "snd arg = Id"
    hence P by (metis id[where t="fst arg"] surjective_pairing) }
  moreover 
  { fix y n L assume "snd arg = [y]n≫L"   "y ♯ (L, fst arg)"
    hence P by (metis st[where t="fst arg"] surjective_pairing) }
  ultimately show P using stack_exhaust[of   "snd arg"   "fst arg"] by auto
next
    ― ‹right uniqueness›
    ― ‹only the case of the second equation matching both args needs to be
shown.›
  fix t t' :: trm and x x' :: name and s s' :: trm and K K' :: stack
  let ?g = dismantle_sumC ― ‹graph of dismantle›
  assume "x ♯ (K, t)"   "x' ♯ (K', t')" 
    and  "(t, [x]s≫K) = (t', [x']s'≫K')"
  thus "?g (t to x in s, K) = ?g (t' to x' in s', K')" 
    by (auto intro!: arg_cong[where f="?g"] simp add: stack.inject)
qed (simp_all add: stack.inject) ― ‹all other cases are trivial›

termination dismantle
by(relation "measure (λ(t,K). |K| )")(auto)

text‹Like all our constructions, dismantling is equivariant. Also, freshness
can be pushed over dismantling, and the freshness requirement in the second
defining equation is not needed›

lemma dismantle_eqvt[eqvt]:
  fixes pi :: "(name × name) list"
  shows "pi ∙ (t ⋆ K) =  (pi ∙ t) ⋆ (pi ∙ K)"
by(nominal_induct K avoiding: pi t rule:stack.strong_induct)
  (auto simp add: eqvts fresh_bij)

lemma dismantle_fresh[iff]:
  fixes  x :: name
  shows "(x ♯ (t ⋆ k)) = (x ♯ t ∧ x ♯ k)"
by(nominal_induct k avoiding: t x rule: stack.strong_induct) 
  (simp_all)

lemma dismantle_simp[simp]: "s ⋆ [y]n≫L = (s to y in n) ⋆ L"
proof - 
  obtain x::name where f: "x ♯ s"   "x ♯ L"   "x ♯ n"  
    using ex_fresh[of "(s,L,n)"] by(auto simp add:fresh_prod)
  hence t: "s to y in n = s to x in ([(y,x)] ∙ n)" 
    by(auto simp add: alpha'')
  from f have "[y]n≫L = [x]([(y,x)] ∙ n)≫L" 
    by (auto simp add: stack.inject alpha'')
  hence "s ⋆ [y]n≫L = s ⋆ [x]([(y,x)] ∙ n)≫L" by simp
  also have " … = (s to y in n) ⋆ L" using f t by(simp del:trm.inject)
  finally show ?thesis .
qed


text ‹We also need a notion of reduction on stacks. This reduction relation
allows us to define strong normalization not only for terms but also for stacks
and is needed to prove the properties of the logical relation later on.›

definition stack_reduction :: "stack ⇒ stack ⇒ bool" (‹ _ ↦ _ ›)
where
  "k ↦ k' ≡ ∀ (t::trm) . (t ⋆ k)  ↦ (t ⋆ k')" 


lemma stack_reduction_fresh:
  fixes k :: stack  and x :: name
  assumes r : "k ↦ k'" and f :"x ♯ k"
  shows "x ♯ k'"
proof -
  from ex_fresh[of x] obtain z::name where f': "z ♯ x" ..
  from r have "Var z ⋆ k ↦ Var z ⋆ k'" unfolding stack_reduction_def ..
  moreover from f f' have "x ♯ Var z ⋆ k" by(auto simp add: fresh_atm)
  ultimately have "x ♯ Var z ⋆ k'" by(rule reduction_fresh)
  thus "x ♯ k'" by simp
qed

lemma dismantle_red[intro]:
  fixes m :: trm
  assumes r: " m ↦ m'"
  shows "m ⋆ k ↦ m' ⋆ k"
using r
by (nominal_induct k avoiding: m m' rule:stack.strong_induct) auto


text ‹Next we define a substitution operation for stacks. The main purpose of
this is to distribute substitution over dismantling.›

nominal_primrec
  ssubst :: "name ⇒ trm ⇒ stack ⇒ stack" 
where
    "ssubst x v Id = Id"
  | " y ♯ (k,x,v)  ⟹ ssubst x v ([y]n≫k) = [y](n[x::=v])≫(ssubst x v k)"
by(finite_guess+ , (simp add: abs_fresh)+ , fresh_guess+)

lemma ssubst_fresh:
  fixes y :: name
  assumes " y ♯ (x,v,k) "
  shows  "y ♯ ssubst x v k"
using assms
by(nominal_induct k avoiding: y x v rule: stack.strong_induct)
  (auto simp add: fresh_prod fresh_atm abs_fresh fresh_fact)

lemma ssubst_forget: 
  fixes x :: name
  assumes "x ♯ k"
  shows "ssubst x v k = k"
using assms
by(nominal_induct k avoiding: x v rule: stack.strong_induct)
  (auto simp add: abs_fresh fresh_atm forget)

lemma subst_dismantle[simp]: "(t ⋆ k)[x ::= v] = (t[x::=v]) ⋆ ssubst x v k"
by(nominal_induct k avoiding: t x v  rule: stack.strong_induct)
  (auto simp add: ssubst_fresh fresh_prod fresh_fact)

section ‹Reducibility for Terms and Stacks›
text_raw ‹\label{sec:reducibility-formal}›

text ‹Following \<^cite>‹"SN.thy"›, we formalize the logical relation as a function
@{term "RED"} of type @{typ "ty ⇒ trm set"} for the term part and accordingly
@{term SRED} of type @{typ "ty ⇒ stack set"} for the stack part of the logical
relation.›

lemma ty_exhaust: "ty = TBase ∨ (∃ σ τ . ty = σ → τ) ∨ (∃ σ . ty = T σ)"
by(induct ty rule:ty.induct) (auto)

function RED :: "ty ⇒ trm set"
and     SRED :: "ty ⇒ stack set"
where
  "RED (TBase) = {t. SN(t)}"
| "RED (τ→σ) = {t. ∀ u ∈ RED τ . (App t u) ∈ RED σ }"
| "RED (T σ) = {t. ∀ k ∈ SRED σ . SN(t ⋆ k) }" 
| "SRED τ = {k. ∀ t ∈ RED τ . SN ([t] ⋆ k) }"
by(auto simp add: ty.inject, case_tac x rule: sum.exhaust,insert ty_exhaust)
  (blast)+

text ‹This is the second non-primitive function in the formalization. Since
types do not involve binders, pattern completeness and right uniqueness are
mostly trivial. The termination argument is not as simple as for the dismantling
function, because the definiton of @{term "SRED τ"} involves a recursive call to
@{term "RED τ"} without reducing the size of @{term "τ"}.›

nominal_primrec
  tsize :: "ty ⇒ nat"
where
    "tsize TBase = 1"
  | "tsize (σ→τ) = 1 + tsize σ + tsize τ"
  | "tsize (T τ) = 1 + tsize τ"
by (rule TrueI)+

text ‹In the termination argument below, @{term "Inl τ"} corresponds to the
call @{term "RED τ"}, whereas @{term "Inr τ"}  corresponds to @{term "SRED τ"}
›

termination RED
by(relation "measure 
    (λ x . case x of Inl τ ⇒ 2 * tsize τ 
                      | Inr τ ⇒ 2 * tsize τ + 1)") (auto)

section ‹Properties of the Reducibility Relation›

text ‹After defining the logical relations we need to prove that the relation
implies strong normalization, is preserved under reduction, and satisfies the
head expansion property.›

definition NEUT :: "trm ⇒ bool"
where
  "NEUT t ≡ (∃a. t = Var a) ∨ (∃t1 t2. t = App t1 t2)" 

definition "CR1" :: "ty ⇒ bool"
where
  "CR1 τ ≡ ∀t. (t∈RED τ ⟶ SN t)"

definition "CR2" :: "ty ⇒ bool"
where
  "CR2 τ ≡ ∀t t'. (t∈RED τ ∧ t ↦ t') ⟶ t'∈RED τ"

definition "CR3_RED" :: "trm ⇒ ty ⇒ bool"
where
  "CR3_RED t τ ≡ ∀t'. t ↦ t' ⟶  t'∈RED τ" 

definition "CR3" :: "ty ⇒ bool"
where
  "CR3 τ ≡ ∀t. (NEUT t ∧ CR3_RED t τ) ⟶ t∈RED τ"
   
definition "CR4" :: "ty ⇒ bool"
where
  "CR4 τ ≡ ∀t. (NEUT t ∧ NORMAL t) ⟶t∈RED τ"

lemma CR3_implies_CR4[intro]: "CR3 τ ⟹ CR4 τ"
by (auto simp add: CR3_def CR3_RED_def CR4_def NORMAL_def)

lemma%invisible sub_induction: 
  assumes a: "SN(u)"
  and     b: "u∈RED τ"
  and     c1: "NEUT t"
  and     c2: "CR2 τ"
  and     c3: "CR3 σ"
  and     c4: "CR3_RED t (τ→σ)"
  shows "(App t u)∈RED σ"
using a b
proof(induct)
  fix u
  assume as: "u∈RED τ"
  assume ih: " ⋀u'. ⟦u ↦ u'; u' ∈ RED τ⟧ ⟹ App t u' ∈ RED σ"
  have "NEUT (App t u)" using c1 by (auto simp add: NEUT_def)
  moreover
  have "CR3_RED (App t u) σ" unfolding CR3_RED_def
  proof (intro strip)
    fix r
    assume red: "App t u ↦ r"
    moreover
    { assume "∃t'. t ↦ t' ∧ r = App t' u"
      then obtain t' where a1: "t ↦ t'" and a2: "r = App t' u" by blast
      have "t'∈RED (τ→σ)" using c4 a1 by (simp add: CR3_RED_def)
      then have "App t' u∈RED σ" using as by simp
      then have "r∈RED σ" using a2 by simp
    }
    moreover
    { assume "∃u'. u ↦ u' ∧ r = App t u'"
      then obtain u' where b1: "u ↦ u'" and b2: "r = App t u'" by blast
      have "u'∈RED τ" using as b1 c2 by (auto simp add: CR2_def)
      with ih have "App t u' ∈ RED σ" using b1 by simp
      then have "r∈RED σ" using b2 by simp
    }
    moreover
    { assume "∃x t'. t = Λ x .t'"
      then obtain x t' where "t = Λ x .t'" by blast
      then have "NEUT (Λ x .t')" using c1 by simp
      then have "False" by (simp add: NEUT_def)
      then have "r∈RED σ" by simp
    }
    ultimately show "r ∈ RED σ" by (cases) (auto)
  qed
  ultimately show "App t u ∈ RED σ" using c3 by (simp add: CR3_def)
qed


inductive 
  FST :: "trm⇒trm⇒bool" (‹ _ » _› [80,80] 80)
where
  fst[intro!]:  "(App t s) » t"

lemma SN_of_FST_of_App: 
  assumes a: "SN (App t s)"
  shows "SN t"
proof - 
  from a have "∀z. (App t s » z) ⟶ SN z"
    by (induct rule: SN.induct)
       (blast elim: FST.cases intro: SN_intro)
  then show "SN t" by blast
qed

text ‹The lemma above is a simplified version of the one used in
\<^cite>‹"SN.thy"›. Since we have generalized our notion of reduction from terms to
stacks, we can also generalize the notion of strong normalization. The new
induction principle will be used to prove the @{term "T"} case of the
properties of the reducibility relation.›

inductive 
  SSN :: "stack ⇒ bool"
where
  SSN_intro: "(⋀ k' . k ↦ k' ⟹ SSN k') ⟹ SSN k"

text ‹Furthermore, the approach for deriving strong normalization of
subterms from above can be generalized to terms of the form @{term "t ⋆ k"}. In
contrast to the case of applications, @{term "t ⋆ k"} does \textit{not} uniquely
determine @{term t} and @{term k}. Thus, the extraction is a proper relation in
this case.›

inductive
  SND_DIS :: "trm ⇒ stack ⇒ bool" (‹_ ⊳ _›)
where
  snd_dis[intro!]: "t ⋆ k ⊳ k"

lemma SN_SSN:
  assumes a: "SN (t ⋆ k)"
  shows " SSN k"
proof - 
  from a have "∀z. (t ⋆ k ⊳ z) ⟶ SSN z"  by (induct rule: SN.induct)
       (metis SND_DIS.cases SSN_intro snd_dis stack_reduction_def)
  thus "SSN k" by blast
qed

text ‹To prove CR1-3, the authors of
\<^cite>‹"TT-lifting"› use a case distinction on the reducts of @{term "t ⋆ k"},
where $t$ is a neutral term and therefore no interaction occurs between $t$ and
$k$.

%auto generated stuff
\begin{isamarkuptext}%
\renewcommand\isacharquery{}
$$\inferrule{
    \isa{{\isacharquery}t\ {\isasymstar}\ {\isacharquery}k\ {\isasymmapsto}\
{\isacharquery}r}\\
    \isa{{\isasymAnd}t{\isacharprime}{\isachardot}\
{\isasymlbrakk}{\isacharquery}t\ {\isasymmapsto}\
t{\isacharprime}{\isacharsemicolon}\ {\isacharquery}r\ {\isacharequal}\
t{\isacharprime}\ {\isasymstar}\ {\isacharquery}k{\isasymrbrakk}\
{\isasymLongrightarrow}\ {\isacharquery}P}\\
    \isa{NEUT\ {\isacharquery}t}\\
    \isa{{\isasymAnd}k{\isacharprime}{\isachardot}\ {\isasymlbrakk}\
{\isacharquery}k\ {\isasymmapsto}\ k{\isacharprime}\ {\isacharsemicolon}\
{\isacharquery}r\ {\isacharequal}\ {\isacharquery}t\ {\isasymstar}\
k{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P}\\
    }{
    \isa{{\isacharquery}P}}$$%
\end{isamarkuptext}%›

text ‹We strive for a proof of this rule by structural induction on $k$. The
general idea of the case where @{term "k = [y]n≫l"} is to move the first stack
frame into the term $t$ and then apply the induction hypothesis as a case
rule. Unfortunately, this term is no longer neutral, so, for the induction to go
through, we need to generalize the claim to also include the possible
interactions of non-neutral terms and stacks.›


lemma dismantle_cases:
  fixes t :: trm
  assumes r: "t ⋆ k ↦ r"
  and T: "⋀ t' . ⟦ t ↦ t' ; r = t' ⋆ k ⟧ ⟹ P"
  and K: "⋀ k' . ⟦ k ↦ k' ; r = t ⋆ k' ⟧ ⟹ P" 
  and B: "⋀ s y n l .⟦ t = [s] ; k = [y]n≫l ; r = (n[y::=s]) ⋆ l ⟧ ⟹ P"
  and A: "⋀ u x v y n l.⟦ x ♯ y; x ♯ n ; t = u to x in v ; 
             k = [y]n≫l ; r = (u to x in (v to y in n)) ⋆ l ⟧ ⟹ P "
  shows "P"
using assms
proof (nominal_induct k avoiding: t r rule:stack.strong_induct)
  case (St y n L) note  yfresh = ‹y ♯ t› ‹y ♯ r› ‹y ♯ L› 
  note IH = St(4) 
    and T = St(6) and K = St(7) and B = St(8) and A = St(9) 
  thus "P" proof (cases rule:IH[where b="t to y in n" and ba="r"])
    case (2 r') have red: "t to y in n ↦ r'" and r: " r = r' ⋆ L" by fact+
txt ‹If @{term "m to y in n"} makes a step we reason by case distinction      
on the successors of @{term "m to y in n"}. We want to use the strong inversion
principle for the reduction relation. For this we need that $y$ is fresh for
@{term "t to y in n"} and $r'$.›
    from yfresh r have y: "y ♯  t to y in n"   "y ♯ r'" 
      by (auto simp add: abs_fresh)
    obtain z where z: "z ≠ y"   "z ♯ r'"   "z ♯ t to y in n" 
      using ex_fresh[of "(y,r',t to y in n)"] 
      by(auto simp add:fresh_prod fresh_atm)
    from red  r show "P" 
    proof (cases rule:reduction.strong_cases
        [ where x="y"and xa="y" and xb="y" and xc="y" and xd="y" 
          and xe="y" and xf="y" and xg="z" and y="y"])
      case (r6 s t' u) ― ‹if $t$ makes a step we use assumption T›
      with y have m: "t ↦ t'"   "r' = t' to y in n" by auto
      thus "P" using T[of t'] r by auto
    next
      case (r7 _ _ n') with y have n: "n ↦ n'" and r': "r' = t to y in n'"
        by (auto simp add: alpha)
      txt ‹Since @{term "k = [y]n≫L"}, the reduction @{thm n} occurs within
        the stack $k$. Hence, we need to establish this stack reduction.›
      have "[y]n≫L ↦ [y]n'≫L" unfolding stack_reduction_def
      proof 
        fix u have "u to y in n ↦ u to y in n'" using n .. 
        hence "(u to y in n) ⋆ L ↦ (u to y in n') ⋆ L" ..
        thus " u ⋆ [y]n≫L ↦ u ⋆ [y]n'≫L" 
          by simp
      qed
      moreover have "r = t ⋆ [y]n'≫L" using r r' by simp
      ultimately show "P" by (rule K)
    next 
      case (r8 s _) ― ‹the case of a $\beta$-reduction is exactly B›
      with y have "t = [s]"   "r' = n[y::=s]" by(auto simp add: alpha) 
      thus "P" using B[of "s" "y" "n" "L"] r by auto 
    next 
      case (r9 _) ― ‹The case of an $\eta$-reduction is a stack
reduction as well.›
      with y have n: "n = [Var y]" and r': "r' = t" 
        by(auto simp add: alpha)
      { fix u have "u to y in n ↦ u" unfolding n ..
        hence "(u to y in n) ⋆ L ↦ u ⋆ L " ..
        hence "u ⋆ [y]n≫L ↦ u ⋆ L" by simp
      } hence "[y]n≫L ↦ L" unfolding stack_reduction_def ..
      moreover have "r = t ⋆ L" using r r' by simp
      ultimately show "P" by (rule K)
    next
      case (r10 u _ v) ― ‹The assoc case holds by A.›
      with y z have 
        "t = (u to z in v)" 
        "r' = u to z in (v to y in n)" 
        "z ♯ (y,n)" by (auto simp add: fresh_prod alpha)
      thus "P" using A[of z y n] r by auto
    qed (insert y, auto)  ― ‹No other reductions are possible.›
  next 
    txt ‹Next we have to solve the case where a reduction occurs deep within
$L$. We get a reduction of the stack $k$ by moving the first stack frame
``[y]n'' back to the right hand side of the dismantling operator.›
    case (3 L')
    hence L: "L ↦ L'" and  r: "r = (t to y in n) ⋆ L'" by auto
    { fix s from L have  "(s to y in n) ⋆ L ↦ (s to y in n) ⋆ L'" 
        unfolding stack_reduction_def ..
      hence "s ⋆ [y]n≫L ↦ s ⋆ [y]n≫L'" by simp
    } hence "[y]n≫L ↦ [y]n≫L'" unfolding stack_reduction_def by auto
    moreover from r have "r = t ⋆ [y]n≫L'" by simp
    ultimately show "P" by (rule K) 
  next
    case (5 x z n' s v K) ― ‹The ``assoc'' case is again a stack reduction›
    have xf: "x ♯ z"   "x ♯ n'" 
      ― ‹We get the following equalities›
    and red: "t to y in n = s to x in v"
             "L = [z]n'≫K"
             "r = (s to x in v to z in n') ⋆ K" by fact+
    { fix u from red have "u ⋆ [y]n≫L = ((u to x in v) to z in n') ⋆ K "
        by(auto intro: arg_cong[where f="λ x . x ⋆ K"])
      moreover 
      { from xf have "(u to x in v) to z in n' ↦ u to x in (v to z in n')" ..
        hence "((u to x in v) to z in n') ⋆ K ↦ (u to x in (v to z in n')) ⋆ K"
          by rule 
      } ultimately  have "u ⋆ [y]n≫L ↦ (u to x in (v to z in n')) ⋆ K" 
        by (simp (no_asm_simp) del:dismantle_simp)
      hence "u ⋆ [y]n≫L ↦ u ⋆ [x](v to z in n')≫K" by simp
    } hence "[y]n≫L ↦  [x](v to z in n')≫ K" 
      unfolding stack_reduction_def by simp
    moreover have "r = t ⋆ ([x](v to z in n')≫K)" using red 
      by (auto)
    ultimately show "P" by (rule K)
  qed (insert St, auto )
qed auto

text ‹Now that we have established the general claim, we can restrict $t$ to
neutral terms only and drop the cases dealing with possible interactions.›

lemma dismantle_cases'[consumes 2, case_names T K]:
  fixes m :: trm
  assumes r: "t ⋆ k ↦ r"
  and "NEUT t"
  and "⋀ t' . ⟦ t ↦ t' ; r = t' ⋆ k ⟧ ⟹ P"
  and "⋀ k' . ⟦ k ↦ k' ; r = t ⋆ k' ⟧ ⟹ P" 
  shows "P"  
using assms unfolding NEUT_def
by (cases rule: dismantle_cases[of t k r]) (auto) 

lemma red_Ret:
  fixes t :: trm
  assumes "[s] ↦ t"
  shows " ∃ s' . t = [s'] ∧ s  ↦ s'"
using assms by cases (auto)

lemma SN_Ret: "SN u ⟹ SN [u]"
by(induct rule:SN.induct) (metis SN.intros red_Ret)

text ‹All the properties of reducibility are shown simultaneously by induction
on the type. Lindley and Stark \<^cite>‹"TT-lifting"› only spell out the cases
dealing with the monadic type constructor $T$. We do the same by reusing the
proofs from \<^cite>‹"SN.thy"› for the other cases. To shorten the presentation,
these proofs are omitted›
    
lemma RED_props: 
  shows "CR1 τ" and "CR2 τ" and "CR3 τ"
proof (nominal_induct τ rule: ty.strong_induct)
  case TBase {%invisible case 1 show "CR1 TBase" 
      by (simp add: CR1_def)
  next
    case 2 show "CR2 TBase" 
      by (auto intro: SN_preserved simp add: CR2_def)
  next
    case 3 show "CR3 TBase" 
      by (auto intro: SN_intro simp add: CR3_def CR3_RED_def)
  }
next
  case (TFun τ1 τ2) {%invisible case 1
    have ih_CR3_τ1: "CR3 τ1" by fact
    have ih_CR1_τ2: "CR1 τ2" by fact
    have "⋀t. t ∈ RED (τ1 → τ2) ⟹ SN t" 
    proof - 
      fix t
      assume "t ∈ RED (τ1 → τ2)"
      then have a: "∀u. u ∈ RED τ1 ⟶ App t u ∈ RED τ2" by simp
      from ih_CR3_τ1 have "CR4 τ1" by (simp add: CR3_implies_CR4) 
      moreover
      fix a have "NEUT (Var a)" by (force simp add: NEUT_def)
      moreover
      have "NORMAL (Var a)" by (rule normal_var)
      ultimately have "(Var a)∈ RED τ1" by (simp add: CR4_def)
      with a have "App t (Var a) ∈ RED τ2" by simp
      hence "SN (App t (Var a))" using ih_CR1_τ2 by (simp add: CR1_def)
      thus "SN t" by (auto dest: SN_of_FST_of_App)
    qed
    then show "CR1 (τ1 → τ2)" unfolding CR1_def by simp
  next
    case 2
    have ih_CR2_τ2: "CR2 τ2" by fact
    then show "CR2 (τ1 → τ2)" unfolding CR2_def by auto 
  next
    case 3
    have ih_CR1_τ1: "CR1 τ1" by fact
    have ih_CR2_τ1: "CR2 τ1" by fact
    have ih_CR3_τ2: "CR3 τ2" by fact
    show "CR3 (τ1 → τ2)" unfolding CR3_def
    proof (simp, intro strip)
      fix t u
      assume a1: "u ∈ RED τ1"
      assume a2: "NEUT t ∧ CR3_RED t (τ1 → τ2)"
      have "SN(u)" using a1 ih_CR1_τ1 by (simp add: CR1_def)
      then show "(App t u)∈RED τ2" 
        using ih_CR2_τ1 ih_CR3_τ2 a1 a2 by (blast intro: sub_induction)
    qed
  }
next
  case (T σ)
  { case 1 ― ‹follows from the fact that @{term "Id ∈ SRED σ"}›
    have ih_CR1_σ: "CR1 σ" by fact
    { fix t assume t_red: "t ∈ RED (T σ)"
      { fix s assume "s ∈ RED σ" 
        hence "SN s" using ih_CR1_σ by (auto simp add: CR1_def)
        hence "SN ([s])" by (rule SN_Ret)
        hence "SN ([s] ⋆ Id)" by simp
      } hence "Id ∈ SRED σ" by simp
      with t_red have "SN (t)" by (auto simp del: SRED.simps)
    } thus "CR1 (T σ)" unfolding CR1_def by blast
  next
    case 2 ― ‹follows since \isa{SN} is preserved under redcution›
    { fix t t'::trm  assume t_red: "t ∈ RED (T σ)" and t_t': "t ↦ t'" 
      { fix k assume k: "k ∈ SRED σ"
        with t_red have "SN(t ⋆ k)" by simp
        moreover from t_t' have "t ⋆ k ↦ t' ⋆ k" ..
        ultimately have "SN(t' ⋆ k)" by (rule SN_preserved) 
      } hence "t' ∈ RED (T σ)"  by (simp del: SRED.simps)
    } thus "CR2 (T σ)"unfolding CR2_def by blast
  next
    case 3 from ‹CR3 σ› have ih_CR4_σ : "CR4 σ" ..
    { fix t assume t'_red: "⋀ t' . t ↦ t' ⟹ t' ∈ RED (T σ)" 
      and neut_t: "NEUT t"
      { fix k assume k_red: "k ∈ SRED σ" 
        fix x have "NEUT (Var x)" unfolding NEUT_def by simp 
        hence "Var x ∈ RED σ" using normal_var ih_CR4_σ 
          by (simp add: CR4_def)
        hence "SN ([Var x] ⋆ k)" using k_red by simp
        hence "SSN k" by (rule SN_SSN)
        then have "SN (t ⋆ k)" using k_red
        proof (induct k rule:SSN.induct)
          case (SSN_intro k)
          have ih : "⋀k'. ⟦ k ↦ k' ; k' ∈ SRED σ ⟧  ⟹ SN (t ⋆ k')"
            and k_red: "k ∈ SRED σ" by fact+
          { fix r assume r: "t ⋆ k ↦ r"
            hence "SN r" using neut_t
            proof (cases rule:dismantle_cases')
              case (T t') hence t_t': "t ↦ t'" and r_def: "r = t' ⋆ k" . 
              from t_t' have "t' ∈ RED (T σ)" by (rule t'_red)
              thus "SN r" using k_red r_def by simp
            next
              case (K k') hence k_k': "k ↦ k'" and r_def: "r = t ⋆ k'" .
              { fix s assume "s ∈ RED σ" 
                hence "SN ([s] ⋆ k)" using k_red
                  by simp
                moreover have "[s] ⋆ k ↦ [s] ⋆ k'"
                  using k_k' unfolding stack_reduction_def ..   
                ultimately have "SN ([s] ⋆ k')" ..
              } hence "k' ∈ SRED σ" by simp
              with k_k' show "SN r" unfolding r_def by (rule ih)
            qed } thus "SN (t ⋆ k)" .. 
        qed } hence "t ∈ RED (T σ)" by simp
    } thus "CR3 (T σ)" unfolding CR3_def CR3_RED_def by blast
  }
qed

text ‹The last case above shows that, once all the reasoning principles have
been established, some proofs have a formalization which is amazingly close to
the informal version. For a direct comparison, the informal proof is presented
in Figure~\ref{fig:cr3}.›

text_raw ‹\input{figureCR3}›

text ‹Now that we have established the properties of the reducibility
relation, we need to show that reducibility is preserved by the various term
constructors. The only nontrivial cases are abstraction and sequencing.›

section ‹Abstraction Preserves Reducibility›    

text ‹Once again we could reuse the proofs from \<^cite>‹"SN.thy"›. The proof uses
the \isa{double-SN} rule and the lemma \isa{red-Lam} below. Unfortunately, this
time the proofs are not fully identical to the proofs in \<^cite>‹"SN.thy"› because
we consider $\beta\eta$-reduction rather than $\beta$-reduction only. However,
the differences are only minor.›
    
lemma%invisible double_SN_aux:
  assumes a: "SN a"
  and b: "SN b"
  and hyp: "⋀x z.
    ⟦⋀y. x ↦ y ⟹ SN y; ⋀y. x ↦ y ⟹ P y z;
     ⋀u. z ↦ u ⟹ SN u; ⋀u. z ↦ u ⟹ P x u⟧ ⟹ P x z"
  shows "P a b"
proof -
  from a
  have r: "⋀b. SN b ⟹ P a b"
  proof (induct a rule: SN.induct)
    case (SN_intro x)
    note SNI' = SN_intro
    have "SN b" by fact
    thus ?case
    proof (induct b rule: SN.induct)
      case (SN_intro y)
      show ?case
        apply (rule hyp)
        apply (erule SNI')
        apply (erule SNI')
        apply (rule SN.SN_intro)
        apply (erule SN_intro)+
        done
    qed
  qed
  from b show ?thesis by (rule r)
qed

lemma double_SN[consumes 2]:
  assumes a: "SN a"
  and     b: "SN b" 
  and     c: "⋀(x::trm) (z::trm). 
             ⟦⋀y. x ↦ y ⟹ P y z; ⋀u. z ↦ u ⟹ P x u⟧ ⟹ P x z"
  shows "P a b"
using a b c
by%invisible (blast intro: double_SN_aux)

lemma red_Lam:
  assumes a: "Λ x . t ↦ r" 
  shows " (∃t'. r = Λ x . t' ∧ t ↦ t') ∨ (t = App r (Var x) ∧ x ♯ r ) "
proof -
  obtain z::name where z: "z ♯ x"   "z ♯ t"   "z ♯ r" 
    using ex_fresh[of "(x,t,r)"] by (auto simp add: fresh_prod)
  have "x ♯ Λ x . t" by (simp add: abs_fresh)
  with a have "x ♯ r" by (simp add: reduction_fresh)
  with a show ?thesis using z
    by(cases rule: reduction.strong_cases
       [where x ="x" and xa="x" and xb="x" and xc="x" and 
              xd="x" and xe="x" and xf="x" and xg="x" and y="z"])
        (auto simp add: abs_fresh alpha fresh_atm)
qed

lemma abs_RED: 
  assumes asm: "∀s∈RED τ. t[x::=s]∈RED σ"
  shows "Λ x . t ∈RED (τ→σ)"
proof %invisible -
  have b1: "SN t" 
  proof -
    have "Var x∈RED τ"
    proof -
      have "CR4 τ" by (simp add: RED_props CR3_implies_CR4)
      moreover
      have "NEUT (Var x)" by (auto simp add: NEUT_def)
      moreover
      have "NORMAL (Var x)" by (rule normal_var) 
      ultimately show "Var x∈RED τ" by (simp add: CR4_def)
    qed
    then have "t[x::=Var x]∈RED σ" using asm by simp
    then have "t∈RED σ" by (simp add: id_subs)
    moreover 
    have "CR1 σ" by (simp add: RED_props)
    ultimately show "SN t" by (simp add: CR1_def)
  qed
  show "Λ x .t∈RED (τ→σ)"
  proof (simp, intro strip)
    fix u
    assume b2: "u∈RED τ"
    then have b3: "SN u" using RED_props by (auto simp add: CR1_def)
    show "App (Λ x .t) u ∈ RED σ" using b1 b3 b2 asm
    proof(induct t u rule: double_SN)
      fix t u
      assume ih1: "⋀t'.  ⟦t ↦ t'; u∈RED τ; ∀s∈RED τ. t'[x::=s]∈RED σ⟧ ⟹ App (Λ x
.t') u ∈
RED σ" 
      assume ih2: "⋀u'.  ⟦u ↦ u'; u'∈RED τ; ∀s∈RED τ. t[x::=s]∈RED σ⟧ ⟹ App (Λ x
.t) u' ∈
RED σ"
      assume as1: "u ∈ RED τ"
      assume as2: "∀s∈RED τ. t[x::=s]∈RED σ"
      have "CR3_RED (App (Λ x. t) u) σ" unfolding CR3_RED_def
      proof(intro strip)
        fix r
        assume red: "App (Λ x .t) u ↦ r"
        moreover
        { assume "∃t'. t ↦ t' ∧ r = App (Λ x . t') u"
          then obtain t' where a1: "t ↦ t'" and a2: "r = App (Λ x .t') u" by
blast
          have "App (Λ x .t') u∈RED σ" using ih1 a1 as1 as2
            apply(auto)
            apply(drule_tac x="t'" in meta_spec)
            apply(simp)
            apply(drule meta_mp)
            prefer 2
            apply(auto)[1]
            apply(rule ballI)
            apply(drule_tac x="s" in bspec)
            apply(simp)
            apply(subgoal_tac "CR2 σ")(*A*)
            apply(unfold CR2_def)[1]
            apply(drule_tac x="t[x::=s]" in spec)
            apply(drule_tac x="t'[x::=s]" in spec)
            apply(simp add: reduction_subst)
            (*A*)
            apply(simp add: RED_props)
            done
          then have "r∈RED σ" using a2 by simp
        } note rt = this
        moreover
        { assume "∃u'. u ↦ u' ∧ r = App (Λ x . t) u'"
          then obtain u' where b1: "u ↦ u'" and b2: "r = App (Λ x .t) u'" by
blast
          have "App (Λ x .t) u'∈RED σ" using ih2 b1 as1 as2
            apply(auto)
            apply(drule_tac x="u'" in meta_spec)
            apply(simp)
            apply(drule meta_mp)
            apply(subgoal_tac "CR2 τ")
            apply(unfold CR2_def)[1]
            apply(drule_tac x="u" in spec)
            apply(drule_tac x="u'" in spec)
            apply(simp)
            apply(simp add: RED_props)
            apply(simp)
            done
          then have "r∈RED σ" using b2 by simp
        } note ru= this
        moreover
        { assume "r = t[x::=u]"
          then have "r∈RED σ" using as1 as2 by auto
        } note r = this
        
        ultimately show "r ∈ RED σ" 
          (* one wants to use the strong elimination principle; for this one 
             has to know that x♯u *)
        apply(cases) 
        apply(auto)
        apply(drule red_Lam)
        apply(drule disjE)prefer 3 apply simp
        apply(auto)[1]
        prefer 2
        apply(auto simp add: alpha subst_rename')[1]
        apply(subgoal_tac "App s' u = t[x::=u]")
        apply(auto)
        apply(auto simp add: forget)
        done
    qed
    moreover 
    have "NEUT (App (Λ x . t) u)" unfolding NEUT_def by (auto)
    ultimately show "App (Λ x . t) u ∈ RED σ"  using RED_props by (simp add:
CR3_def)
  qed
qed
qed


section ‹Sequencing Preserves Reducibility›

text ‹This section corresponds to the main part of the paper being formalized
and as such deserves special attention. In the lambda case one has to formalize
doing induction on $\max(s) + max(t)$ for two strongly normalizing terms $s$ and
$t$ (cf. \<^cite>‹‹Section 6.3› in "proofs+types"›). Above, this was done through a
\isa{double-SN}
rule. The central Lemma 7 of Lindley and Stark's paper uses an even more
complicated induction scheme. They assume terms $p$ and $n$ as well as a stack
$K$ such that @{term "SN(p)"} and @{term "SN(n[x::=p] ⋆ K)"}. The induction is
then done on $|K| + max(n \star K) + max(p)$. See Figure~\ref{fig:lemma7} in
for details.›

text_raw ‹\input{figureLemma7}›


text ‹Since we have settled for a different characterization of strong
normalization, we have to derive an induction principle similar in spirit to the
\isa{double-SN} rule. 

Furthermore, it turns out that it is not necessary to formalize the fact that
stack reductions do not increase the length of the stack.\footnote{This
possibility was only discovered \textit{after} having formalized $ K \mapsto K'
\Rightarrow |K| \geq |K'|$. The proof of this seemingly simple fact
was about 90 lines of Isar code.} Doing induction on the sum above, this is
necessary to handle the case of a reduction occurring in $K$. We differ
from \<^cite>‹"TT-lifting"› and establish an induction principle which to some extent
resembles the lexicographic order on $$(\SN,\mapsto) \times (\SN,\mapsto) \times
(\N,>)\,.$$›

lemma triple_induct[consumes 2]: 
  assumes a: "SN (p)"
  and b: "SN (q)"
  and hyp: "⋀ (p::trm) (q::trm) (k::stack) . 
  ⟦ ⋀ p' . p ↦ p' ⟹ P p' q k ; 
    ⋀ q' k . q ↦ q' ⟹ P p q' k; 
    ⋀ k' .  |k'| < |k| ⟹ P p q k' ⟧ ⟹ P p q k "
  shows "P p q k"
proof -
  from a have "⋀q K . SN q ⟹ P p q K"
  proof (induct p)
    case (SN_intro p) 
    have sn1: "⋀ p' q K . ⟦p ↦ p'; SN q⟧ ⟹ P p' q K" by fact
    have sn_q: "SN q"   "SN q" by fact+
    thus "P p q K"
    proof (induct q arbitrary: K) 
      case (SN_intro q K)
      have sn2: "⋀ q' K . ⟦q ↦ q'; SN q'⟧ ⟹ P p q' K" by fact
      show "P p q K"
      proof (induct K rule: measure_induct_rule[where f="length"])
        case (less k)
        have le: "⋀ k' . |k'| < |k| ⟹ P p q k'" by fact
        { fix p' assume "p ↦ p'"
          moreover have "SN q" by fact
          ultimately have "P p' q k" using sn1 by auto }
        moreover
        { fix q' K  assume r: "q ↦ q'" 
          have "SN q" by fact
          hence "SN q'" using r by (rule SN_preserved)
          with r have "P p q' K" using sn2 by auto }
        ultimately show ?case using le
          by (auto intro:hyp)
      qed
    qed
  qed 
  with b show ?thesis by blast
qed


text ‹Here we strengthen the case rule for terms of the form @{term "t ⋆ k ↦
r"}. The freshness requirements on $x$,$y$, and $z$
correspond to those for the rule \isa{reduction.strong-cases}, the strong
inversion principle for the reduction relation.›


lemma dismantle_strong_cases:
  fixes t :: trm
  assumes r: "t ⋆ k ↦ r"
  and f: "y ♯ (t,k,r)"   "x ♯ (z,t,k,r)"   "z ♯ (t,k,r)"
  and T: "⋀ t' . ⟦ t ↦ t' ; r = t' ⋆ k ⟧ ⟹ P"
  and K: "⋀ k' . ⟦ k ↦ k' ; r = t ⋆ k' ⟧ ⟹ P" 
  and B: "⋀ s n l . ⟦ t = [s] ; 
                       k = [y]n≫l ; r = (n[y::=s]) ⋆ l ⟧ ⟹ P "
  and A: "⋀ u v n l . 
           ⟦ x ♯ (z,n); t = u to x in v ; k = [z]n≫l ; 
             r = (u to x in (v to z in n)) ⋆ l ⟧ ⟹ P "
  shows "P"
proof (cases rule:dismantle_cases[of t k r P])
  case (4 s y' n L) have ch:
    "t = [s]"
    "k = [y']n≫L"
    "r = n[y'::=s] ⋆ L" by fact+
  txt ‹The equations we get look almost like those we need to instantiate the
hypothesis \isa{B}. The only difference is that \isa{B} only applies to $y$, and
since we want $y$ to become an instantiation variable of the strengthened rule,
we only know that $y$ satisfies \isa{f} and nothing else. But the condition
\isa{f} is just strong enough to rename $y'$ to $y$ and apply \isa{B}.›
  with f have "y = y' ∨ y ♯ n" 
    by (auto simp add: fresh_prod abs_fresh)
  hence "n[y'::=s] = ([(y,y')] ∙ n)[y::=s]" 
    and "[y']n≫L = [y]([(y,y')] ∙ n)≫L"
    by(auto simp add: name_swap_bij subst_rename' stack.inject alpha' )
  with ch have "t = [s]" 
    "k = [y]([(y,y')] ∙ n)≫L" 
    "r = ([(y,y')] ∙ n)[y::=s] ⋆ L"
    by (auto)
  thus "P" by (rule B) 
next 
  case (5 u x' v z' n L) have ch:
    "x' ♯ z'"   "x' ♯ n"
    "t = u to x' in v"
    "k = [z']n≫L"
    "r = (u to x' in v to z' in n) ⋆ L" by fact+ 
  txt ‹We want to do the same trick as above but at this point we have to take
care of the possibility that $x$ might coincide with $x'$ or $z'$. Similarly,
$z$
might coincide with $z'$.›
  with f have x: "x = x' ∨ x ♯ v to z' in n" 
    and z: "z = z' ∨ z ♯ n"
    by (auto simp add: fresh_prod abs_fresh)
  from f ch have x': "x' ♯ n"   " x' ♯ z'" 
    and xz': "x = z' ∨ x ♯ n" 
    by (auto simp add:name_swap_bij alpha fresh_prod fresh_atm abs_fresh)
  from f ch have "x ♯ z" "x ♯ [z'].n" by (auto simp add:  fresh_prod)
  with xz' z have  " x ♯ (z , ([(z, z')] ∙ n))" 
    by (auto simp add: fresh_atm fresh_bij name_swap_bij 
          fresh_prod abs_fresh calc_atm fresh_aux fresh_left)
  moreover from x ch have "t = u to x in ([(x,x')] ∙ v)" 
    by (auto simp add:name_swap_bij alpha')
  moreover from z ch have "k = [z]([(z,z')] ∙ n)≫L"
    by (auto simp add:name_swap_bij stack.inject alpha')
  txt ‹The first two $\alpha$-renamings are simple, but here we have to handle
the nested binding structure of the assoc rule. Since $x$ scopes over the whole
term @{term "(v to z' in n)" }, we have to push the swapping over $z'$›
  moreover { from x have 
    "u to x' in (v to z' in n) = u to x in ([(x,x')] ∙ (v to z' in n))"
      by (auto simp add:name_swap_bij alpha' simp del: trm.perm)
    also from xz' x' have "… = u to x in (([(x,x')] ∙ v) to z' in n)"
      by (auto simp add: abs_fun_eq1 swap_simps alpha'') 
           (metis alpha'' fresh_atm perm_fresh_fresh swap_simps(1) x')
    also from z have " … = u to x in (([(x,x')] ∙ v) to z in ([(z,z')] ∙ n))"
      by (auto simp add: abs_fun_eq1 alpha' name_swap_bij )
    finally 
      have "r =  (u to x in (([(x, x')] ∙ v) to z in ([(z, z')] ∙ n))) ⋆ L" 
        using ch by (simp del: trm.inject) }
  ultimately show "P" 
    by (rule A[where n="[(z, z')] ∙ n" and v="([(x, x')] ∙ v)"]) 
qed (insert r T K, auto)


text ‹The lemma in Figure~\ref{fig:lemma7} assumes @{term "SN(n[x::=p] ⋆ K)"}
but the actual induction in done on @{term "SN(n ⋆ K)"}. The stronger
assumption @{term "SN (n[x::=p] ⋆ K)"} is needed to handle the $\beta$ and
$\eta$ cases.›

lemma sn_forget:
  assumes a: "SN(t[x::=v])"
  shows "SN t"
proof -
  define q where "q = t[x::=v]"
  from a have "SN q" unfolding q_def .
  thus "SN t" using q_def
  proof (induct q arbitrary: t)
    case (SN_intro t)
    hence ih: "⋀ t'. ⟦t[x::=v] ↦ t'[x::=v]⟧ ⟹ SN t'" by auto
    { fix t' assume "t ↦ t'"
      hence "t[x::=v] ↦ t'[x::=v]" by (rule reduction_subst)
      hence "SN t'" by (rule ih) }
    thus "SN t" ..
  qed
qed

          
lemma sn_forget': 
  assumes sn: "SN (t[x::=p] ⋆ k)" 
  and x: "x ♯ k"
  shows "SN (t ⋆ k)"
proof -
  from x have "t[x::=p] ⋆ k = (t ⋆ k)[x::=p]" by (simp add: ssubst_forget)
  with sn have "SN( (t ⋆ k)[x::=p] )" by simp
  thus ?thesis by (rule sn_forget)
qed

abbreviation
redrtrans :: "trm ⇒ trm ⇒ bool" (‹ _ ↦⇧* _ › )
where "redrtrans ≡ reduction^**" 

text ‹To be able to handle the case where $p$ makes a step, we need to
establish @{term "p ↦ p' ⟹ (m[x::=p]) ↦⇧* (m[x::=p'])"} as well as the
fact that strong normalization is preserved for an arbitrary number of reduction
steps. The first claim involves a number of simple transitivity lemmas. Here we
can benefit from having removed the freshness conditions from the reduction
relation as this allows all the cases to be proven automatically. Similarly, in
the \isa{red-subst} lemma, only those cases where substitution is pushed to two
subterms needs to be proven explicitly.›

lemma red_trans:
  shows r1_trans: " s ↦⇧* s' ⟹ App s t ↦⇧* App s' t"
  and r2_trans: " t ↦⇧* t' ⟹ App s t ↦⇧* App s t'"
  and r4_trans: "t ↦⇧* t' ⟹ Λ x . t ↦⇧* Λ x . t' "
  and r6_trans: " s ↦⇧* s'  ⟹ s to x in t ↦⇧* s' to x in t"
  and r7_trans: "⟦ t ↦⇧* t'  ⟧ ⟹ s to x in t ↦⇧* s  to x in t'"
  and r11_trans: "s ↦⇧* s' ⟹ [s] ↦⇧* ([s'])"
by - (induct rule: rtranclp_induct , (auto intro:
transitive_closurep_trans')[2])+

lemma red_subst: "p ↦ p' ⟹ (m[x::=p]) ↦⇧* (m[x::=p'])"
proof(nominal_induct m avoiding: x p p' rule:trm.strong_induct)
  case (App s t) 
  hence "App (s[x::=p]) (t[x::=p]) ↦⇧* App (s[x::=p']) (t[x::=p])" 
    by (auto intro: r1_trans)
  also from App have "… ↦⇧* App (s[x::=p']) ( t[x::=p'])"
    by (auto intro: r2_trans)
  finally show ?case by auto
next
  case (To s y n) hence 
    "(s[x::=p]) to y in (n[x::=p]) ↦⇧* (s[x::=p']) to y in (n[x::=p])" 
    by (auto intro: r6_trans)
  also from To have " … ↦⇧* (s[x::=p']) to y in (n[x::=p']) "
    by (auto intro: r7_trans)
  finally show ?case using To by auto
qed (auto intro:red_trans)

lemma SN_trans : "⟦  p ↦⇧* p' ; SN p ⟧ ⟹ SN p' "
by (induct rule: rtranclp_induct) (auto intro: SN_preserved)

subsection ‹Central lemma›
text_raw ‹\label{sec:central}›

text ‹Now we have everything in place we need to tackle the central ``Lemma
7'' of \<^cite>‹"TT-lifting"› (cf. Figure~\ref{fig:lemma7}). The proof is quite long,
but for the most part, the reasoning is that of \<^cite>‹"TT-lifting"›.›

lemma to_RED_aux: 
  assumes p: "SN p"
  and x: "x ♯ p"   "x ♯ k"
  and npk: " SN (n[x::=p] ⋆ k)"
  shows "SN (([p] to x in n) ⋆ k)"
proof -
  { fix q assume "SN q" with p 
    have  "⋀ m . ⟦ q = m ⋆ k ; SN(m[x::=p] ⋆ k) ⟧ 
               ⟹ SN (([p] to x in m) ⋆ k)"
      using x
    proof (induct p q rule:triple_induct[where k="k"]) 
      case (1 p q k) ― ‹We obtain an induction hypothesis for $p$, $q$, and
$k$.›
      have ih_p: 
        "⋀ p' m . ⟦p ↦ p'; q = m ⋆ k; SN (m[x::=p'] ⋆ k); x ♯ p'; x ♯ k⟧
            ⟹ SN (([p'] to x in m) ⋆ k)" by fact
      have ih_q: 
        "⋀ q' m k . ⟦q ↦ q'; q' = m ⋆ k; SN (m[x::=p] ⋆ k); x ♯ p; x ♯ k⟧
            ⟹ SN (([p] to x in m) ⋆ k)" by fact
      have ih_k: 
        "⋀ k' m . ⟦ |k'| < |k|; q = m ⋆ k'; SN (m[x::=p] ⋆ k'); x ♯ p; x ♯ k'⟧
            ⟹ SN (([p] to x in m) ⋆ k')" by fact
      have q: "q = m ⋆ k" and sn: "SN (m[x::=p] ⋆ k)" by fact+
      have xp: "x ♯ p" and xk: "x ♯ k" by fact+

txt ‹Once again we want to reason via case distinction on the successors of a
term including a dismantling operator. Since this time we also need to handle
the cases where interactions occur, we want to use the strengthened case
rule. We already require $x$ to be suitably fresh. To instantiate the rule, we
need another fresh name.›

      { fix r assume red: "([p] to x in m) ⋆ k ↦ r"
        from xp xk have x1 : "x ♯ ([p] to x in m) ⋆ k "  
          by (simp add: abs_fresh)
        with red have x2: "x ♯ r" by (rule reduction_fresh)
        obtain z::name where z: "z ♯ (x,p,m,k,r)" 
          using ex_fresh[of "(x,p,m,k,r)"] by (auto simp add: fresh_prod)
        have "SN r"
        proof (cases rule:dismantle_strong_cases
            [of   "[p] to x in m"   k r x x z ])
          case (5 r') have r: "r = r' ⋆ k" and r': "[p] to x in m ↦ r'" by fact+
          txt ‹To handle the case of a reduction occurring somewhere in @{term
"[p] to x in m" }, we need to contract the freshness conditions to this subterm.
This allows the use of the strong inversion rule for the reduction relation.›
          from x1 x2 r 
          have xl:"(x ♯ [p] to x in m)" and xr:"x ♯ r'" by auto
          from z have zl: "z ♯ ([p] to x in m)"   "x ≠ z" 
            by (auto simp add: abs_fresh fresh_prod fresh_atm)
          with r' have zr: "z ♯ r'"  by (blast intro:reduction_fresh)
          ― ‹handle all reductions of @{term "[p] to x in m"}›
          from r' show "SN r" proof (cases rule:reduction.strong_cases
              [where x="x" and xa="x" and xb="x" and xc="x" and xd="x" 
                and xe="x" and xf="x"and xg="x" and y="z"])
txt ‹The case where @{term "p ↦ p'"} is interesting, because it requires
reasioning about the reflexive transitive closure of the reduction relation.›
            case (r6 s s' t)  hence ch: "[p] ↦ s'"   "r' = s' to x in m" 
              using xl xr by (auto)
            from this obtain p' where s: "s' = [p']" and  p : "p ↦ p'" 
              by (blast dest:red_Ret)
            from p have "((m⋆k)[x::=p]) ↦⇧* ((m⋆k)[x::=p'])" 
              by (rule red_subst)
            with xk have "((m[x::=p]) ⋆ k) ↦⇧* ((m[x::=p']) ⋆ k)" 
              by (simp add: ssubst_forget)
            hence sn: "SN ((m[x::=p']) ⋆ k)" using sn by (rule SN_trans)
            from p xp have xp' : "x ♯ p'" by (rule reduction_fresh)
            from ch s have rr: "r' = [p'] to x in m" by simp
            from p q  sn xp' xk
            show "SN r" unfolding r rr by (rule ih_p)
          next

            case(r7 s t m') hence "r' = [p] to x in m'" and "m ↦ m'" 
              using xl xr by (auto simp add: alpha)
            hence rr: "r' = [p] to x in m'" by simp
            from q ‹m ↦ m'› have  "q ↦ m' ⋆ k" by(simp add: dismantle_red)
            moreover have "m' ⋆ k = m' ⋆ k" .. ― ‹a triviality›
            moreover { from ‹m ↦ m'› have "(m[x::=p]) ⋆ k ↦ (m'[x::=p]) ⋆ k"
                by (simp add: dismantle_red reduction_subst)
              with sn have "SN(m'[x::=p] ⋆ k)" .. }
            ultimately show "SN r" using xp xk unfolding r rr by (rule ih_q)
          next  
              
            case (r8 s t) ― ‹the $\beta$-case is handled by assumption›
            hence "r' = m[x::=p]" using xl xr by(auto simp add: alpha)
            thus "SN r" unfolding r using sn by simp
          next 

            case (r9 s) ― ‹the $\eta$-case is handled by assumption as well› 
            hence "m = [Var x]" and "r' = [p]" using xl xr 
              by(auto simp add: alpha)
            hence "r' = m[x::=p]" by simp
            thus "SN r" unfolding r using sn by simp
          qed (simp_all only: xr xl zl zr abs_fresh , auto)
          ― ‹There are no other possible reductions of @{term "[p] to x in
m"}.›
        next

          case (6 k') 
          have k: "k ↦ k'" and r: "r = ([p] to x in m) ⋆ k'" by fact+
          from q k have "q ↦ m ⋆ k'" unfolding stack_reduction_def by blast
          moreover have "m ⋆ k' = m ⋆ k'" ..
          moreover { have "SN (m[x::=p] ⋆ k)" by fact
            moreover have "(m[x::=p]) ⋆ k ↦ (m[x::=p]) ⋆ k'" 
              using k unfolding stack_reduction_def .. 
            ultimately have "SN (m[x::=p] ⋆ k')" .. }
          moreover note xp 
          moreover from k xk  have "x ♯ k'"
            by (rule stack_reduction_fresh)
          ultimately show "SN r" unfolding r by (rule ih_q)
        next
txt ‹The case of an assoc interaction between @{term "[p] to x in m" } and
@{term "k"} is easily handled by the induction hypothesis, since @{term
"(m[x::=p]) ⋆ k"} remains fixed under assoc.›
          case (8 s t u L)
          hence k: "k = [z]u≫L"
            and r: "r = ([p] to x in (m to z in u)) ⋆ L" 
            and u: "x ♯ u" 
            by(auto simp add: alpha fresh_prod)
          let ?k = L and ?m = "m to z in u"
          from k z have "|?k| < |k|" by (simp add: fresh_prod)
          moreover have "q =  ?m ⋆ ?k" using k q by simp
          moreover { from k u z xp have "(?m[x::=p] ⋆ ?k) = (m[x::=p]) ⋆ k" 
            by(simp add: fresh_prod forget)
          hence "SN (?m[x::=p] ⋆ ?k)" using sn by simp }
          moreover from xp xk k have "x ♯ p" and "x ♯ ?k" by auto
          ultimately show "SN r" unfolding r by (rule ih_k)
        qed (insert red z x1 x2 xp xk ,
            auto simp add: fresh_prod fresh_atm abs_fresh)
      } thus "SN (([p] to x in m) ⋆ k)" ..
    qed } 
  moreover have "SN ((n[x::=p]) ⋆ k)" by fact
  moreover hence "SN (n ⋆ k)" using ‹x ♯ k› by (rule sn_forget') 
  ultimately show ?thesis by blast
qed

text ‹Having established the claim above, we use it show that
\textsf{to}-bindings preserve reducibility.›

lemma to_RED:
  assumes s: "s ∈ RED (T σ)"
  and t : " ∀ p ∈ RED σ . t[x::=p] ∈ RED (T τ)"
  shows "s to x in t ∈ RED (T τ)"
proof -
  { fix K assume k: "K ∈ SRED τ" 
    { fix p assume p: "p ∈ RED σ"
      hence snp: "SN p" using RED_props by(simp add: CR1_def)
      obtain x'::name where x: "x' ♯ (t, p, K)" 
        using ex_fresh[of "(t,p,K)"] by (auto)
      from p t k have "SN((t[x::=p]) ⋆ K)" by auto
      with x have "SN ((([(x',x)] ∙ t )[x'::=p]) ⋆ K)" 
        by (simp add: fresh_prod subst_rename)
      with snp x  have snx': "SN (([p] to x' in ([(x',x)] ∙ t )) ⋆ K)" 
        by (auto intro: to_RED_aux)
      from x have "[p] to x' in ([(x',x)] ∙ t ) = [p] to x in t" 
        by simp (metis alpha' fresh_prod name_swap_bij x)
      moreover have "([p] to x in t) ⋆ K  = [p] ⋆ [x]t≫K" by simp
      ultimately have snx: "SN([p] ⋆ [x]t≫K)" using snx' 
        by (simp del: trm.inject)
    } hence "[x]t≫K ∈ SRED σ" by simp
    with s have "SN((s to x in t) ⋆ K)" by(auto simp del: SRED.simps) 
  } thus "s to x in t ∈ RED (T τ)" by simp
qed


section ‹Fundamental Theorem›
text_raw ‹\label{sec:FTLR}›

text ‹The remainder of this section follows \<^cite>‹"SN.thy"› very closely.  We
first establish that all well typed terms are reducible if we substitute
reducible terms for the free variables.›

abbreviation 
 mapsto :: "(name×trm) list ⇒ name ⇒ trm ⇒ bool" (‹_ maps _ to _› [55,55,55] 55)
where
 "θ maps x to e ≡ (lookup θ x) = e"

abbreviation 
  closes :: "(name×trm) list ⇒ (name×ty) list ⇒ bool" (‹_ closes _› [55,55] 55) 
where
  "θ closes Γ ≡ ∀x τ. ((x,τ) ∈ set Γ ⟶ (∃t. θ maps x to t ∧ t ∈ RED τ))"

theorem fundamental_theorem: 
  assumes a: "Γ ⊢ t : τ"   and   b: "θ closes Γ"
  shows "θ<t> ∈ RED τ"
using a b
proof(nominal_induct  avoiding: θ rule: typing.strong_induct)
  case (t3 a Γ σ t τ θ) ― ‹lambda case› 
  {%invisible 
  have ih: "⋀θ. θ closes ((a,σ)#Γ) ⟹ θ<t> ∈ RED τ" by fact
  have θ_cond: "θ closes Γ" by fact
  have fresh: "a♯Γ"   "a♯θ" by fact+
  from ih have "∀s∈RED σ. ((a,s)#θ)<t> ∈ RED τ" 
    using fresh θ_cond fresh_context by simp
  then have "∀s∈RED σ. θ<t>[a::=s] ∈ RED τ" 
    using fresh by (simp add: psubst_subst)
  then have "Λ a . (θ<t>) ∈ RED (σ → τ)" by (simp only: abs_RED)
  then show "θ<(Λ a . t)> ∈ RED (σ → τ)" using fresh by simp }
next
  case (t5 x Γ s σ t τ θ) ― ‹to case›
  have ihs : "⋀ θ . θ closes Γ ⟹ θ<s> ∈ RED (T σ)" by fact
  have iht : "⋀ θ . θ closes ((x, σ) # Γ) ⟹ θ<t> ∈ RED (T τ)" by fact
  have θ_cond: "θ closes Γ" by fact
  have fresh: "x ♯ θ"  "x ♯ Γ"   "x ♯ s" by fact+
  from ihs have "θ<s> ∈ RED (T σ)" using θ_cond by simp
  moreover 
  { from iht have "∀s∈RED σ. ((x,s)#θ)<t> ∈ RED (T τ)" 
      using fresh θ_cond fresh_context by simp
    hence "∀s∈RED σ. θ<t>[x::=s] ∈ RED (T τ)" 
      using fresh by (simp add: psubst_subst) }
  ultimately have "(θ<s>) to x in (θ<t>) ∈ RED (T τ)" by (simp only: to_RED)
  thus "θ<s to x in t> ∈ RED (T τ)" using fresh by simp
qed auto ― ‹all other cases are trivial›

text ‹The final result then follows using the identity substitution, which is
$\Gamma$-closing since all variables are reducible at any type.›

fun
  "id" :: "(name×ty) list ⇒ (name×trm) list"
where
  "id []    = []"
| "id ((x,τ)#Γ) = (x,Var x)#(id Γ)"

lemma id_maps: 
  shows "(id Γ) maps a to (Var a)"
by (induct Γ) (auto)

lemma id_fresh:
  fixes x::"name"
  assumes x: "x ♯ Γ"
  shows "x ♯ (id Γ)"
using x
by (induct Γ) (auto simp add: fresh_list_nil fresh_list_cons)

lemma id_apply: 
  shows "(id Γ)<t> = t"
by (nominal_induct t avoiding: Γ rule: trm.strong_induct)
   (auto simp add: id_maps id_fresh)

lemma id_closes:
  shows "(id Γ) closes Γ"
proof - 
  { fix x τ assume "(x,τ) ∈ set Γ"
    have "CR4 τ" by(simp add: RED_props CR3_implies_CR4)
    hence "Var x ∈ RED τ" 
      by(auto simp add: NEUT_def normal_var CR4_def)
    hence "(id Γ) maps x to Var x ∧ Var x ∈ RED τ"
      by (simp add: id_maps) 
  } thus ?thesis by blast
qed

subsection ‹Strong normalization theorem›

lemma typing_implies_RED:  
  assumes a: "Γ ⊢ t : τ"
  shows "t ∈ RED τ"
proof -
  have "(id Γ)<t>∈RED τ" 
  proof -
    have "(id Γ) closes Γ" by (rule id_closes)
    with a show ?thesis by (rule fundamental_theorem)
  qed
  thus"t ∈ RED τ" by (simp add: id_apply)
qed

theorem strong_normalization: 
  assumes a: "Γ ⊢ t : τ"
  shows "SN(t)"
proof -
  from a have "t ∈ RED τ" by (rule typing_implies_RED)
  moreover have "CR1 τ" by (rule RED_props)
  ultimately show "SN(t)" by (simp add: CR1_def)
qed

text ‹This finishes our formalization effort. This article is generated
from the Isabelle theory file, which consists of roughly 1500 lines of proof
code. The reader is invited to replay some of the more technical proofs using
the theory file provided.›

(*<*)end(*>*)