Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: WeakNorm.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Weak normalization for simply-typed lambda calculus\<close>

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

text \<open>
Formalization by Stefan Berghofer. Partly based on a paper proof by
Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
\<close>

subsection \<open>Main theorems\<close>

lemma norm_list:
  assumes f_compat: "\t t'. t \\<^sub>\\<^sup>* t' \ f t \\<^sub>\\<^sup>* 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 (\<lambda>t. \<forall>e T' u i. e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow>
      NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')) as \<Longrightarrow>
    \<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) as \<rightarrow>\<^sub>\<beta>\<^sup>*
      Var j \<degree>\<degree> map f as' \<and> NF (Var j \<degree>\<degree> 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 \\<^sub>\\<^sup>* 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] \\<^sub>\\<^sup>* b' \ NF b'"
    by iprover
  then obtain b' where bred: "b[u/i] \\<^sub>\\<^sup>* 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]) \\<^sub>\\<^sup>* f b'"
    by (rule f_compat)
  with bsred have
    "\j. (Var j \\ map (\t. f (t[u/i])) bs) \ f (b[u/i]) \\<^sub>\\<^sup>*
     (Var j \<degree>\<degree> map f bs') \<degree> 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] \\<^sub>\\<^sup>* 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\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> 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] \\<^sub>\\<^sup>* t' \ NF t'"
      proof
        assume eq: "x = i"
        show ?thesis
        proof (cases ts)
          case Nil
          with eq have "(Var x \\ [])[u/i] \\<^sub>\\<^sup>* 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 \\<^sub>\\<^sup>*
            Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and>
            NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list)
          then obtain as' where
            asred: "Var 0 \\ map (\t. lift (t[u/i]) 0) as \\<^sub>\\<^sup>*
              Var 0 \<degree>\<degree> map (\<lambda>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] \\<^sub>\\<^sup>* a' \ NF a'"
            by iprover
          then obtain a' where ared: "a[u/i] \\<^sub>\\<^sup>* 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 \\<^sub>\\<^sup>* u' \ NF u'" by (rule app_Var_NF)
          then obtain u' where ured: "lift u 0 \ Var 0 \\<^sub>\\<^sup>* u'" and u'NF: "NF u'"
            by iprover
          from T and u'NF have "\ua. u'[a'/0] \\<^sub>\\<^sup>* 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] \\<^sub>\\<^sup>* ua" and uaNF: "NF ua"
            by iprover
          from ared have "(lift u 0 \ Var 0)[a[u/i]/0] \\<^sub>\\<^sup>* (lift u 0 \ Var 0)[a'/0]"
            by (rule subst_preserves_beta2')
          also from ured have "(lift u 0 \ Var 0)[a'/0] \\<^sub>\\<^sup>* u'[a'/0]"
            by (rule subst_preserves_beta')
          also note uared
          finally have "(lift u 0 \ Var 0)[a[u/i]/0] \\<^sub>\\<^sup>* ua" .
          hence uared': "u \ a[u/i] \\<^sub>\\<^sup>* ua" by simp
          from T asNF _ uaNF have "\r. (Var 0 \\ map (\t. lift t 0) as')[ua/0] \\<^sub>\\<^sup>* 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] \\<^sub>\\<^sup>* 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] \\<^sub>\\<^sup>*
            (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> 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] \\<^sub>\\<^sup>*
            (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 \\ map (\t. lift (t[u/i]) 0) as)[u \ a[u/i]/0] \\<^sub>\\<^sup>* r" .
          with rnf Cons eq show ?thesis
            by (simp add: o_def) iprover
        qed
      next
        assume neq: "x \ i"
        from App have "listall ?R ts" by (iprover dest: listall_conj2)
        with uNF uT argsT
        have "\ts'. \j. Var j \\ map (\t. t[u/i]) ts \\<^sub>\\<^sup>* Var j \\ ts' \
          NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
          by (rule norm_list [of "\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 "\ (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\i:T\ \ Abs r : T'"
      then obtain R S where "e\0:R\\Suc i:T\ \ 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\0:R\ \ lift u 0 : T" using uT by (rule lift_type)
      ultimately have "\t'. r[lift u 0/Suc i] \\<^sub>\\<^sup>* t' \ NF t'" by (rule Abs)
      thus "\t'. Abs r[u/i] \\<^sub>\\<^sup>* t' \ 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 \ type) \ dB \ type \ bool" ("_ \\<^sub>R _ : _" [50, 50, 50] 50)
  where
    Var: "e x = T \ e \\<^sub>R Var x : T"
  | Abs: "e\0:T\ \\<^sub>R t : U \ e \\<^sub>R Abs t : (T \ U)"
  | App: "e \\<^sub>R s : T \ U \ e \\<^sub>R t : T \ e \\<^sub>R (s \ t) : U"

lemma rtyping_imp_typing: "e \\<^sub>R t : T \ e \ 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 \\<^sub>R t : T"
  shows "\t'. t \\<^sub>\\<^sup>* t' \ 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 \\<^sub>\\<^sup>* s'" and "NF s'"
    and tred: "t \\<^sub>\\<^sup>* t'" and tNF: "NF t'" by iprover
  have "\u. (Var 0 \ lift t' 0)[s'/0] \\<^sub>\\<^sup>* u \ 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 \\ [lift t' 0])" by (rule NF.App)
    thus "NF (Var 0 \ lift t' 0)" by simp
    show "e\0:T \ U\ \ Var 0 \ lift t' 0 : U"
    proof (rule typing.App)
      show "e\0:T \ U\ \ Var 0 : T \ U"
        by (rule typing.Var) simp
      from tred have "e \ t' : T"
        by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
      thus "e\0:T \ U\ \ lift t' 0 : T"
        by (rule lift_type)
    qed
    from sred show "e \ s' : T \ U"
      by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
    show "NF s'" by fact
  qed
  then obtain u where ured: "s' \ t' \\<^sub>\\<^sup>* u" and unf: "NF u" by simp iprover
  from sred tred have "s \ t \\<^sub>\\<^sup>* s' \ t'" by (rule rtrancl_beta_App)
  hence "s \ t \\<^sub>\\<^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"
  apply (rule iffI)
  apply (erule rtranclpR.induct)
  apply (rule rtranclp.rtrancl_refl)
  apply (erule rtranclp.rtrancl_into_rtrancl)
  apply assumption
  apply (erule rtranclp.induct)
  apply (rule rtranclpR.rtrancl_refl)
  apply (erule rtranclpR.rtrancl_into_rtrancl)
  apply assumption
  done

lemma NFR_imp_NF: "NFR nf t \ 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 = (\x. default)"

instance ..

end

definition int_of_nat :: "nat \ 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

¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.