Quelle  WeakNorm.thy

(*  Title:      HOL/Proofs/Lambda/WeakNorm.thy
    Author:     Stefan Berghofer
    Copyright   2003 TU Muenchen
*)

section ‹Weak normalization for simply-typed lambda calculus›

theory WeakNorm
imports LambdaType NormalForm "HOL-Library.Realizers" "HOL-Library.Code_Target_Int"
begin

text ‹
  by Stefan Berghofer. Partly based on a paper proof by
  Joachimski and Ralph Matthes cite‹"Matthes-Joachimski-AML"›.
 ›


subsection ‹Main theorems›

lemma norm_list:
  assumes f_compat: "∧t t'. t →_\<beta>^* t' ==> f t →_\<beta>^* f t'"
  and f_NF: "∧t. NF t ==> NF (f t)"
  and uNF: "NF u" and uT: "e ⊨ u : T"
  shows "∧Us. e⟨i:T⟩ ⊨!!! as : Us ==>
    listall (λt. ∀e T' u i. e⟨i:T⟩ ⊨ t : T' ⟶
      NF u ⟶ e ⊨ u : T ⟶ (∃t'. t[u/i] →_\<beta>^* t' ∧ NF t')) as ==>
    ∃as'. ∀j. Var j 🚫🚫 map (λt. f (t[u/i])) as →_\<beta>^*
      Var j 🚫🚫 map f as' ∧ NF (Var j 🚫🚫 map f as')"
  (is "∧Us. _ ==> listall ?R as ==> ∃as'. ?ex Us as as'")
proof (induct as rule: rev_induct)
  case (Nil Us)
  with Var_NF have "?ex Us [] []" by simp
  thus ?case ..
next
  case (snoc b bs Us)
  have "e⟨i:T⟩ ⊨!!! bs @ [b] : Us" by fact
  then obtain Vs W where Us: "Us = Vs @ [W]"
    and bs: "e⟨i:T⟩ ⊨!!! bs : Vs" and bT: "e⟨i:T⟩ ⊨ b : W"
    by (rule types_snocE)
  from snoc have "listall ?R bs" by simp
  with bs have "∃bs'. ?ex Vs bs bs'" by (rule snoc)
  then obtain bs' where bsred: "Var j 🚫🚫 map (λt. f (t[u/i])) bs →_\<beta>^* Var j 🚫🚫 map f bs'"
    and bsNF: "NF (Var j 🚫🚫 map f bs')" for j
    by iprover
  from snoc have "?R b" by simp
  with bT and uNF and uT have "∃b'. b[u/i] →_\<beta>^* b' ∧ NF b'"
    by iprover
  then obtain b' where bred: "b[u/i] →_\<beta>^* b'" and bNF: "NF b'"
    by iprover
  from bsNF [of 0] have "listall NF (map f bs')"
    by (rule App_NF_D)
  moreover have "NF (f b')" using bNF by (rule f_NF)
  ultimately have "listall NF (map f (bs' @ [b']))"
    by simp
  hence "∧j. NF (Var j 🚫🚫 map f (bs' @ [b']))" by (rule NF.App)
  moreover from bred have "f (b[u/i]) →_\<beta>^* f b'"
    by (rule f_compat)
  with bsred have
    "∧j. (Var j 🚫🚫 map (λt. f (t[u/i])) bs) 🚫 f (b[u/i]) →_\<beta>^*
     (Var j 🚫🚫 map f bs') 🚫 f b'" by (rule rtrancl_beta_App)
  ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
  thus ?case ..
qed

lemma subst_type_NF:
  "∧t e T u i. NF t ==> e⟨i:U⟩ ⊨ t : T ==> NF u ==> e ⊨ u : U ==> ∃t'. t[u/i] →_\<beta>^* t' ∧ NF t'"
  (is "PROP ?P U" is "∧t e T u i. _ ==> PROP ?Q t e T u i U")
proof (induct U)
  fix T t
  let ?R = "λt. ∀e T' u i.
    e⟨i:T⟩ ⊨ t : T' ⟶ NF u ⟶ e ⊨ u : T ⟶ (∃t'. t[u/i] →_\<beta>^* t' ∧ NF t')"
  assume MI1: "∧T1 T2. T = T1 → T2 ==> PROP ?P T1"
  assume MI2: "∧T1 T2. T = T1 → T2 ==> PROP ?P T2"
  assume "NF t"
  thus "∧e T' u i. PROP ?Q t e T' u i T"
  proof induct
    fix e T' u i assume uNF: "NF u" and uT: "e ⊨ u : T"
    {
      case (App ts x e1 T'1 u1 i1)
      assume "e⟨i:T⟩ ⊨ Var x 🚫🚫 ts : T'"
      then obtain Us
        where varT: "e⟨i:T⟩ ⊨ Var x : Us ⇛ T'"
        and argsT: "e⟨i:T⟩ ⊨!!! ts : Us"
        by (rule var_app_typesE)
      from nat_eq_dec show "∃t'. (Var x 🚫🚫 ts)[u/i] →_\<beta>^* t' ∧ NF t'"
      proof
        assume eq: "x = i"
        show ?thesis
        proof (cases ts)
          case Nil
          with eq have "(Var x 🚫🚫 [])[u/i] →_\<beta>^* u" by simp
          with Nil and uNF show ?thesis by simp iprover
        next
          case (Cons a as)
          with argsT obtain T'' Ts where Us: "Us = T'' # Ts"
            by (cases Us) (rule FalseE, simp)
          from varT and Us have varT: "e⟨i:T⟩ ⊨ Var x : T'' → Ts ⇛ T'"
            by simp
          from varT eq have T: "T = T'' → Ts ⇛ T'" by cases auto
          with uT have uT': "e ⊨ u : T'' → Ts ⇛ T'" by simp
          from argsT Us Cons have argsT': "e⟨i:T⟩ ⊨!!! as : Ts" by simp
          from argsT Us Cons have argT: "e⟨i:T⟩ ⊨ a : T''" by simp
          from argT uT refl have aT: "e ⊨ a[u/i] : T''" by (rule subst_lemma)
          from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)
          with lift_preserves_beta' lift_NF uNF uT argsT'
          have "∃as'. ∀j. Var j 🚫🚫 map (λt. lift (t[u/i]) 0) as →_\<beta>^*
            Var j 🚫🚫 map (λt. lift t 0) as' ∧
            NF (Var j 🚫🚫 map (λt. lift t 0) as')" by (rule norm_list)
          then obtain as' where
            asred: "Var 0 🚫🚫 map (λt. lift (t[u/i]) 0) as →_\<beta>^*
              Var 0 🚫🚫 map (λt. lift t 0) as'"
            and asNF: "NF (Var 0 🚫🚫 map (λt. lift t 0) as')" by iprover
          from App and Cons have "?R a" by simp
          with argT and uNF and uT have "∃a'. a[u/i] →_\<beta>^* a' ∧ NF a'"
            by iprover
          then obtain a' where ared: "a[u/i] →_\<beta>^* a'" and aNF: "NF a'" by iprover
          from uNF have "NF (lift u 0)" by (rule lift_NF)
          hence "∃u'. lift u 0 🚫 Var 0 →_\<beta>^* u' ∧ NF u'" by (rule app_Var_NF)
          then obtain u' where ured: "lift u 0 🚫 Var 0 →_\<beta>^* u'" and u'NF: "NF u'"
            by iprover
          from T and u'NF have "∃ua. u'[a'/0] →_\<beta>^* ua ∧ NF ua"
          proof (rule MI1)
            have "e⟨0:T''⟩ ⊨ lift u 0 🚫 Var 0 : Ts ⇛ T'"
            proof (rule typing.App)
              from uT' show "e⟨0:T''⟩ ⊨ lift u 0 : T'' → Ts ⇛ T'" by (rule lift_type)
              show "e⟨0:T''⟩ ⊨ Var 0 : T''" by (rule typing.Var) simp
            qed
            with ured show "e⟨0:T''⟩ ⊨ u' : Ts ⇛ T'" by (rule subject_reduction')
            from ared aT show "e ⊨ a' : T''" by (rule subject_reduction')
            show "NF a'" by fact
          qed
          then obtain ua where uared: "u'[a'/0] →_\<beta>^* ua" and uaNF: "NF ua"
            by iprover
          from ared have "(lift u 0 🚫 Var 0)[a[u/i]/0] →_\<beta>^* (lift u 0 🚫 Var 0)[a'/0]"
            by (rule subst_preserves_beta2')
          also from ured have "(lift u 0 🚫 Var 0)[a'/0] →_\<beta>^* u'[a'/0]"
            by (rule subst_preserves_beta')
          also note uared
          finally have "(lift u 0 🚫 Var 0)[a[u/i]/0] →_\<beta>^* ua" .
          hence uared': "u 🚫 a[u/i] →_\<beta>^* ua" by simp
          from T asNF _ uaNF have "∃r. (Var 0 🚫🚫 map (λt. lift t 0) as')[ua/0] →_\<beta>^* r ∧ NF r"
          proof (rule MI2)
            have "e⟨0:Ts ⇛ T'⟩ ⊨ Var 0 🚫🚫 map (λt. lift (t[u/i]) 0) as : T'"
            proof (rule list_app_typeI)
              show "e⟨0:Ts ⇛ T'⟩ ⊨ Var 0 : Ts ⇛ T'" by (rule typing.Var) simp
              from uT argsT' have "e ⊨!!! map (λt. t[u/i]) as : Ts"
                by (rule substs_lemma)
              hence "e⟨0:Ts ⇛ T'⟩ ⊨!!! map (λt. lift t 0) (map (λt. t[u/i]) as) : Ts"
                by (rule lift_types)
              thus "e⟨0:Ts ⇛ T'⟩ ⊨!!! map (λt. lift (t[u/i]) 0) as : Ts"
                by (simp_all add: o_def)
            qed
            with asred show "e⟨0:Ts ⇛ T'⟩ ⊨ Var 0 🚫🚫 map (λt. lift t 0) as' : T'"
              by (rule subject_reduction')
            from argT uT refl have "e ⊨ a[u/i] : T''" by (rule subst_lemma)
            with uT' have "e ⊨ u 🚫 a[u/i] : Ts ⇛ T'" by (rule typing.App)
            with uared' show "e ⊨ ua : Ts ⇛ T'" by (rule subject_reduction')
          qed
          then obtain r where rred: "(Var 0 🚫🚫 map (λt. lift t 0) as')[ua/0] →_\<beta>^* r"
            and rnf: "NF r" by iprover
          from asred have
            "(Var 0 🚫🚫 map (λt. lift (t[u/i]) 0) as)[u 🚫 a[u/i]/0] →_\<beta>^*
            (Var 0 🚫🚫 map (λt. lift t 0) as')[u 🚫 a[u/i]/0]"
            by (rule subst_preserves_beta')
          also from uared' have "(Var 0 🚫🚫 map (λt. lift t 0) as')[u 🚫 a[u/i]/0] →_\<beta>^*
            (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2')
          also note rred
          finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" .
          with rnf Cons eq show ?thesis
            by (simp add: o_def) iprover
        qed
      next
        assume neq: "x \<noteq> i"
        from App have "listall ?R ts" by (iprover dest: listall_conj2)
        with uNF uT argsT
        have "\<exists>ts'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> ts' \<and>
          NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
          by (rule norm_list [of "\<lambda>t. t", simplified])
        then obtain ts' where NF: "?ex ts'" ..
        from nat_le_dec show ?thesis
        proof
          assume "i < x"
          with NF show ?thesis by simp iprover
        next
          assume "\<not> (i < x)"
          with NF neq show ?thesis by (simp add: subst_Var) iprover
        qed
      qed
    next
      case (Abs r e1 T'1 u1 i1)
      assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
      then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp
      moreover have "NF (lift u 0)" using \<open>NF u\<close> by (rule lift_NF)
      moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type)
      ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
      thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
        by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
    }
  qed
qed


\<comment> \<open>A computationally relevant copy of @{term "e \<turnstile> t : T"}\<close>
inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  (\<open>_ \<turnstile>\<^sub>R _ : _\<close> [50, 50, 50] 50)
  where
    Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
  | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
  | App: "e \<turnstile>\<^sub>R s : T \<Rightarrow> U \<Longrightarrow> e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile>\<^sub>R (s \<degree> t) : U"

lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T"
  apply (induct set: rtyping)
  apply (erule typing.Var)
  apply (erule typing.Abs)
  apply (erule typing.App)
  apply assumption
  done


theorem type_NF:
  assumes "e \<turnstile>\<^sub>R t : T"
  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" using assms
proof induct
  case Var
  show ?case by (iprover intro: Var_NF)
next
  case Abs
  thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
next
  case (App e s T U t)
  from App obtain s' t' where
    sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and "NF s'"
    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover
  have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> NF u"
  proof (rule subst_type_NF)
    have "NF (lift t' 0)" using tNF by (rule lift_NF)
    hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil)
    hence "NF (Var 0 \<degree>\<degree> [lift t' 0])" by (rule NF.App)
    thus "NF (Var 0 \<degree> lift t' 0)" by simp
    show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U"
    proof (rule typing.App)
      show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
        by (rule typing.Var) simp
      from tred have "e \<turnstile> t' : T"
        by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
      thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T"
        by (rule lift_type)
    qed
    from sred show "e \<turnstile> s' : T \<Rightarrow> U"
      by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
    show "NF s'" by fact
  qed
  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover
  from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
  hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans)
  with unf show ?case by iprover
qed


subsection \<open>Extracting the program\<close>

declare NF.induct [ind_realizer]
declare rtranclp.induct [ind_realizer irrelevant]
declare rtyping.induct [ind_realizer]
lemmas [extraction_expand] = conj_assoc listall_cons_eq subst_all equal_allI

extract type_NF

lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
proof
  show "rtranclpR r a b \<Longrightarrow> r\<^sup>*\<^sup>* a b"
    apply (erule rtranclpR.induct)
     apply (rule rtranclp.rtrancl_refl)
    apply (metis rtranclp.rtrancl_into_rtrancl)
    done
  show "r\<^sup>*\<^sup>* a b \<Longrightarrow> rtranclpR r a b"
    apply (erule rtranclp.induct)
     apply (rule rtranclpR.rtrancl_refl)
    apply (metis rtranclpR.rtrancl_into_rtrancl)
    done
qed

lemma NFR_imp_NF: "NFR nf t \<Longrightarrow> NF t"
  apply (erule NFR.induct)
  apply (rule NF.intros)
  apply (simp add: listall_def)
  apply (erule NF.intros)
  done

text_raw \<open>
\begin{figure}
\renewcommand{\isastyle}{\scriptsize\it}%
@{thm [display,eta_contract=false,margin=100] subst_type_NF_def}
\renewcommand{\isastyle}{\small\it}%
\caption{Program extracted from \<open>subst_type_NF\<close>}
\label{fig:extr-subst-type-nf}
\end{figure}

\begin{figure}
\renewcommand{\isastyle}{\scriptsize\it}%
@{thm [display,margin=100] subst_Var_NF_def}
@{thm [display,margin=100] app_Var_NF_def}
@{thm [display,margin=100] lift_NF_def}
@{thm [display,eta_contract=false,margin=100] type_NF_def}
\renewcommand{\isastyle}{\small\it}%
\caption{Program extracted from lemmas and main theorem}
\label{fig:extr-type-nf}
\end{figure}
\<close>

text \<open>
The program corresponding to the proof of the central lemma, which
performs substitution and normalization, is shown in Figure
\ref{fig:extr-subst-type-nf}. The correctness
theorem corresponding to the program \<open>subst_type_NF\<close> is
@{thm [display,margin=100] subst_type_NF_correctness
  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
where \<open>NFR\<close> is the realizability predicate corresponding to
the datatype \<open>NFT\<close>, which is inductively defined by the rules
\pagebreak
@{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]}

The programs corresponding to the main theorem \<open>type_NF\<close>, as
well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.
The correctness statement for the main function \<open>type_NF\<close> is
@{thm [display,margin=100] type_NF_correctness
  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
where the realizability predicate \<open>rtypingR\<close> corresponding to the
computationally relevant version of the typing judgement is inductively
defined by the rules
@{thm [display,margin=100] rtypingR.Var [no_vars]
  rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]}
\<close>

subsection \<open>Generating executable code\<close>

instantiation NFT :: default
begin

definition "default = Dummy ()"

instance ..

end

instantiation dB :: default
begin

definition "default = dB.Var 0"

instance ..

end

instantiation prod :: (default, default) default
begin

definition "default = (default, default)"

instance ..

end

instantiation list :: (type) default
begin

definition "default = []"

instance ..

end

instantiation "fun" :: (type, default) default
begin

definition "default = (\<lambda>x. default)"

instance ..

end

definition int_of_nat :: "nat \<Rightarrow> int" where
  "int_of_nat = of_nat"

text \<open>
  The following functions convert between Isabelle's built-in {\tt term}
  datatype and the generated {\tt dB} datatype. This allows to
  generate example terms using Isabelle's parser and inspect
  normalized terms using Isabelle's pretty printer.
\<close>

ML \<open>
val nat_of_integer = @{code nat} o @{code int_of_integer};

fun dBtype_of_typ (Type ("fun", [T, U])) =
      @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
        ["'", a] => @{code Atom} (nat_of_integer (ord a - 97))
      | _ => error "dBtype_of_typ: variable name")
  | dBtype_of_typ _ = error "dBtype_of_typ: bad type";

fun dB_of_term (Bound i) = @{code dB.Var} (nat_of_integer i)
  | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
  | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
  | dB_of_term _ = error "dB_of_term: bad term";

fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
      Abs ("x", T, term_of_dB (T :: Ts) U dBt)
  | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code integer_of_nat} n)
  | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
      let val t = term_of_dB' Ts dBt
      in case fastype_of1 (Ts, t) of
          Type ("fun", [T, _]) => t $ term_of_dB Ts T dBu
        | _ => error "term_of_dB: function type expected"
      end
  | term_of_dB' _ _ = error "term_of_dB: term not in normal form";

fun typing_of_term Ts e (Bound i) =
      @{code Var} (e, nat_of_integer i, dBtype_of_typ (nth Ts i))
  | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
        Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
          dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
          typing_of_term Ts e t, typing_of_term Ts e u)
      | _ => error "typing_of_term: function type expected")
  | typing_of_term Ts e (Abs (_, T, t)) =
      let val dBT = dBtype_of_typ T
      in @{code Abs} (e, dBT, dB_of_term t,
        dBtype_of_typ (fastype_of1 (T :: Ts, t)),
        typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
      end
  | typing_of_term _ _ _ = error "typing_of_term: bad term";

fun dummyf _ = error "dummy";

val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct1));
val ct1' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);

val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
val ct2' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
\<close>

end