# HG changeset patch # User berghofe # Date 1056443832 -7200 # Node ID e61a310cde02614e783a0b474493b840e1886e58 # Parent 7f0d5cc526158cfeab717a90dccd33c85dd5ed75 New proof of weak normalization with program extraction. diff -r 7f0d5cc52615 -r e61a310cde02 src/HOL/Lambda/WeakNorm.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Lambda/WeakNorm.thy Tue Jun 24 10:37:12 2003 +0200 @@ -0,0 +1,604 @@ +(* Title: HOL/Lambda/WeakNorm.thy + ID: $Id$ + Author: Stefan Berghofer + Copyright 2003 TU Muenchen +*) + +header {* Weak normalization for simply-typed lambda calculus *} + +theory WeakNorm = Type: + +text {* +Formalization by Stefan Berghofer. Partly based on a paper proof by +Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}. +*} + + +subsection {* Terms in normal form *} + +constdefs + listall :: "('a \ bool) \ 'a list \ bool" + "listall P xs \ (\i. i < length xs \ P (xs ! i))" + +declare listall_def [extraction_expand] + +theorem listall_nil: "listall P []" + by (simp add: listall_def) + +theorem listall_nil_eq [simp]: "listall P [] = True" + by (rules intro: listall_nil) + +theorem listall_cons: "P x \ listall P xs \ listall P (x # xs)" + apply (simp add: listall_def) + apply (rule allI impI)+ + apply (case_tac i) + apply simp+ + done + +theorem listall_cons_eq [simp]: "listall P (x # xs) = (P x \ listall P xs)" + apply (rule iffI) + prefer 2 + apply (erule conjE) + apply (erule listall_cons) + apply assumption + apply (unfold listall_def) + apply (rule conjI) + apply (erule_tac x=0 in allE) + apply simp + apply simp + apply (rule allI) + apply (erule_tac x="Suc i" in allE) + apply simp + done + +lemma listall_conj1: "listall (\x. P x \ Q x) xs \ listall P xs" + by (induct xs) simp+ + +lemma listall_conj2: "listall (\x. P x \ Q x) xs \ listall Q xs" + by (induct xs) simp+ + +lemma listall_app: "listall P (xs @ ys) = (listall P xs \ listall P ys)" + apply (induct xs) + apply (rule iffI, simp, simp) + apply (rule iffI, simp, simp) + done + +lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \ P x)" + apply (rule iffI) + apply (simp add: listall_app)+ + done + +lemma listall_cong [cong, extraction_expand]: + "xs = ys \ listall P xs = listall P ys" + -- {* Currently needed for strange technical reasons *} + by (unfold listall_def) simp + +consts NF :: "dB set" +inductive NF +intros + App: "listall (\t. t \ NF) ts \ Var x \\ ts \ NF" + Abs: "t \ NF \ Abs t \ NF" +monos listall_def + +lemma nat_eq_dec: "\n::nat. m = n \ m \ n" + apply (induct m) + apply (case_tac n) + apply (case_tac [3] na) + apply (simp only: nat.simps, rules?)+ + done + +lemma nat_le_dec: "\n::nat. m < n \ \ (m < n)" + apply (induct m) + apply (case_tac n) + apply (case_tac [3] na) + apply (simp del: simp_thms, rules?)+ + done + +lemma App_NF_D: assumes NF: "Var n \\ ts \ NF" + shows "listall (\t. t \ NF) ts" using NF + by cases simp_all + + +subsection {* Properties of @{text NF} *} + +lemma Var_NF: "Var n \ NF" + apply (subgoal_tac "Var n \\ [] \ NF") + apply simp + apply (rule NF.App) + apply simp + done + +lemma subst_terms_NF: "listall (\t. t \ NF) ts \ + listall (\t. \i j. t[Var i/j] \ NF) ts \ + listall (\t. t \ NF) (map (\t. t[Var i/j]) ts)" + by (induct ts) simp+ + +lemma subst_Var_NF: "t \ NF \ (\i j. t[Var i/j] \ NF)" + apply (induct set: NF) + apply simp + apply (frule listall_conj1) + apply (drule listall_conj2) + apply (drule_tac i=i and j=j in subst_terms_NF) + apply assumption + apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard]) + apply simp + apply (erule NF.App) + apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard]) + apply simp + apply (rules intro: NF.App) + apply simp + apply (rules intro: NF.App) + apply simp + apply (rules intro: NF.Abs) + done + +lemma app_Var_NF: "t \ NF \ \t'. t \ Var i \\<^sub>\\<^sup>* t' \ t' \ NF" + apply (induct set: NF) + apply (subst app_last) + apply (rule exI) + apply (rule conjI) + apply (rule rtrancl_refl) + apply (rule NF.App) + apply (drule listall_conj1) + apply (simp add: listall_app) + apply (rule Var_NF) + apply (rule exI) + apply (rule conjI) + apply (rule rtrancl_into_rtrancl) + apply (rule rtrancl_refl) + apply (rule beta) + apply (erule subst_Var_NF) + done + +lemma lift_terms_NF: "listall (\t. t \ NF) ts \ + listall (\t. \i. lift t i \ NF) ts \ + listall (\t. t \ NF) (map (\t. lift t i) ts)" + by (induct ts) simp+ + +lemma lift_NF: "t \ NF \ (\i. lift t i \ NF)" + apply (induct set: NF) + apply (frule listall_conj1) + apply (drule listall_conj2) + apply (drule_tac i=i in lift_terms_NF) + apply assumption + apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard]) + apply simp + apply (rule NF.App) + apply assumption + apply simp + apply (rule NF.App) + apply assumption + apply simp + apply (rule NF.Abs) + apply simp + done + + +subsection {* Main theorems *} + +lemma subst_type_NF: + "\t e T u i. t \ NF \ e\i:U\ \ t : T \ u \ NF \ e \ u : U \ \t'. t[u/i] \\<^sub>\\<^sup>* t' \ t' \ NF" + (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' \ u \ NF \ e \ u : T \ (\t'. t[u/i] \\<^sub>\\<^sup>* t' \ t' \ NF)" + assume MI1: "\T1 T2. T = T1 \ T2 \ PROP ?P T1" + assume MI2: "\T1 T2. T = T1 \ T2 \ PROP ?P T2" + assume "t \ NF" + thus "\e T' u i. PROP ?Q t e T' u i T" + proof induct + fix e T' u i assume uNF: "u \ NF" and uT: "e \ u : T" + { + case (App ts x e_ T'_ u_ i_) + assume appT: "e\i:T\ \ Var x \\ ts : T'" + from nat_eq_dec show "\t'. (Var x \\ ts)[u/i] \\<^sub>\\<^sup>* t' \ t' \ NF" + 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 rules + next + case (Cons a as) + with appT have "e\i:T\ \ Var x \\ (a # as) : T'" by simp + then obtain Us + where varT': "e\i:T\ \ Var x : Us \ T'" + and argsT': "e\i:T\ \ a # as : Us" + by (rule var_app_typesE) + from 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' and Us have argsT: "e\i:T\ \ as : Ts" by simp + from argsT' and Us have argT: "e\i:T\ \ a : T''" by simp + from argT uT refl have aT: "e \ a[u/i] : T''" by (rule subst_lemma) + have as: "\Us. e\i:T\ \ as : Us \ listall ?R as \ + \as'. Var 0 \\ map (\t. lift (t[u/i]) 0) as \\<^sub>\\<^sup>* + Var 0 \\ map (\t. lift t 0) as' \ + Var 0 \\ map (\t. lift t 0) as' \ NF" + (is "\Us. _ \ _ \ \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" . + 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 0 \\ map (\t. lift (t[u/i]) 0) bs \\<^sub>\\<^sup>* + Var 0 \\ map (\t. lift t 0) bs'" + and bsNF: "Var 0 \\ map (\t. lift t 0) bs' \ NF" by rules + from snoc have "?R b" by simp + with bT and uNF and uT have "\b'. b[u/i] \\<^sub>\\<^sup>* b' \ b' \ NF" by rules + then obtain b' where bred: "b[u/i] \\<^sub>\\<^sup>* b'" and bNF: "b' \ NF" by rules + from bsNF have "listall (\t. t \ NF) (map (\t. lift t 0) bs')" + by (rule App_NF_D) + moreover have "lift b' 0 \ NF" by (rule lift_NF) + ultimately have "listall (\t. t \ NF) (map (\t. lift t 0) (bs' @ [b']))" + by simp + hence "Var 0 \\ map (\t. lift t 0) (bs' @ [b']) \ NF" by (rule NF.App) + moreover from bred have "lift (b[u/i]) 0 \\<^sub>\\<^sup>* lift b' 0" + by (rule lift_preserves_beta') + with bsred have + "(Var 0 \\ map (\t. lift (t[u/i]) 0) bs) \ lift (b[u/i]) 0 \\<^sub>\\<^sup>* + (Var 0 \\ map (\t. lift t 0) bs') \ lift b' 0" by (rule rtrancl_beta_App) + ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp + thus ?case .. + qed + from App and Cons have "listall ?R as" by simp (rules dest: listall_conj2) + with argsT have "\as'. ?ex Ts as as'" by (rule as) + then obtain as' where + asred: "Var 0 \\ map (\t. lift (t[u/i]) 0) as \\<^sub>\\<^sup>* + Var 0 \\ map (\t. lift t 0) as'" + and asNF: "Var 0 \\ map (\t. lift t 0) as' \ NF" by rules + from App and Cons have "?R a" by simp + with argT and uNF and uT have "\a'. a[u/i] \\<^sub>\\<^sup>* a' \ a' \ NF" + by rules + then obtain a' where ared: "a[u/i] \\<^sub>\\<^sup>* a'" and aNF: "a' \ NF" by rules + from uNF have "lift u 0 \ NF" by (rule lift_NF) + hence "\u'. lift u 0 \ Var 0 \\<^sub>\\<^sup>* u' \ u' \ NF" by (rule app_Var_NF) + then obtain u' where ured: "lift u 0 \ Var 0 \\<^sub>\\<^sup>* u'" and u'NF: "u' \ NF" + by rules + from T and u'NF have "\ua. u'[a'/0] \\<^sub>\\<^sup>* ua \ ua \ NF" + 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') + qed + then obtain ua where uared: "u'[a'/0] \\<^sub>\\<^sup>* ua" and uaNF: "ua \ NF" + by rules + 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 have "\r. (Var 0 \\ map (\t. lift t 0) as')[ua/0] \\<^sub>\\<^sup>* r \ r \ NF" + 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: map_compose [symmetric] 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: "r \ NF" by rules + from asred have + "(Var 0 \\ map (\t. lift (t[u/i]) 0) as)[u \ a[u/i]/0] \\<^sub>\\<^sup>* + (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] \\<^sub>\\<^sup>* + (Var 0 \\ map (\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: map_compose [symmetric] o_def) rules + qed + next + assume neq: "x \ i" + show ?thesis + proof - + from appT obtain Us + where varT: "e\i:T\ \ Var x : Us \ T'" + and argsT: "e\i:T\ \ ts : Us" + by (rule var_app_typesE) + have ts: "\Us. e\i:T\ \ ts : Us \ listall ?R ts \ + \ts'. \x'. Var x' \\ map (\t. t[u/i]) ts \\<^sub>\\<^sup>* Var x' \\ ts' \ + Var x' \\ ts' \ NF" + (is "\Us. _ \ _ \ \ts'. ?ex Us ts ts'") + proof (induct ts 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" . + 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: "\x'. Var x' \\ map (\t. t[u/i]) bs \\<^sub>\\<^sup>* Var x' \\ bs'" + and bsNF: "\x'. Var x' \\ bs' \ NF" by rules + from snoc have "?R b" by simp + with bT and uNF and uT have "\b'. b[u/i] \\<^sub>\\<^sup>* b' \ b' \ NF" by rules + then obtain b' where bred: "b[u/i] \\<^sub>\\<^sup>* b'" and bNF: "b' \ NF" by rules + from bsred bred have "\x'. (Var x' \\ map (\t. t[u/i]) bs) \ b[u/i] \\<^sub>\\<^sup>* + (Var x' \\ bs') \ b'" by (rule rtrancl_beta_App) + moreover from bsNF [of 0] have "listall (\t. t \ NF) bs'" + by (rule App_NF_D) + with bNF have "listall (\t. t \ NF) (bs' @ [b'])" by simp + hence "\x'. Var x' \\ (bs' @ [b']) \ NF" by (rule NF.App) + ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp + thus ?case .. + qed + from App have "listall ?R ts" by (rules dest: listall_conj2) + with argsT have "\ts'. ?ex Ts ts ts'" by (rule ts) + then obtain ts' where NF: "?ex Ts ts ts'" .. + from nat_le_dec show ?thesis + proof + assume "i < x" + with NF show ?thesis by simp rules + next + assume "\ (i < x)" + with NF neq show ?thesis by (simp add: subst_Var) rules + qed + qed + qed + next + case (Abs r e_ T'_ u_ i_) + 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 "lift u 0 \ NF" by (rule lift_NF) + moreover have "e\0:R\ \ lift u 0 : T" by (rule lift_type) + ultimately have "\t'. r[lift u 0/Suc i] \\<^sub>\\<^sup>* t' \ t' \ NF" by (rule Abs) + thus "\t'. Abs r[u/i] \\<^sub>\\<^sup>* t' \ t' \ NF" + by simp (rules intro: rtrancl_beta_Abs NF.Abs) + } + qed +qed + + +consts -- {* A computationally relevant copy of @{term "e \ t : T"} *} + rtyping :: "((nat \ type) \ dB \ type) set" + +syntax + "_rtyping" :: "(nat \ type) \ dB \ type \ bool" ("_ |-\<^sub>R _ : _" [50, 50, 50] 50) +syntax (xsymbols) + "_rtyping" :: "(nat \ type) \ dB \ type \ bool" ("_ \\<^sub>R _ : _" [50, 50, 50] 50) +translations + "e \\<^sub>R t : T" \ "(e, t, T) \ rtyping" + +inductive rtyping + intros + 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 T: "e \\<^sub>R t : T" + shows "\t'. t \\<^sub>\\<^sup>* t' \ t' \ NF" using T +proof induct + case Var + show ?case by (rules intro: Var_NF) +next + case Abs + thus ?case by (rules intro: rtrancl_beta_Abs NF.Abs) +next + case (App T U e s t) + from App obtain s' t' where + sred: "s \\<^sub>\\<^sup>* s'" and sNF: "s' \ NF" + and tred: "t \\<^sub>\\<^sup>* t'" and tNF: "t' \ NF" by rules + have "\u. (Var 0 \ lift t' 0)[s'/0] \\<^sub>\\<^sup>* u \ u \ NF" + proof (rule subst_type_NF) + have "lift t' 0 \ NF" by (rule lift_NF) + hence "listall (\t. t \ NF) [lift t' 0]" by (rule listall_cons) (rule listall_nil) + hence "Var 0 \\ [lift t' 0] \ NF" by (rule NF.App) + thus "Var 0 \ lift t' 0 \ NF" 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) + 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) + qed + then obtain u where ured: "s' \ t' \\<^sub>\\<^sup>* u" and unf: "u \ NF" by simp rules + 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 rtrancl_trans) + with unf show ?case by rules +qed + + +subsection {* Extracting the program *} + +declare NF.induct [ind_realizer] +declare rtrancl.induct [ind_realizer irrelevant] +declare rtyping.induct [ind_realizer] +lemmas [extraction_expand] = trans_def conj_assoc listall_cons_eq + +extract type_NF + +lemma rtranclR_rtrancl_eq: "((a, b) \ rtranclR r) = ((a, b) \ rtrancl (Collect r))" + apply (rule iffI) + apply (erule rtranclR.induct) + apply (rule rtrancl_refl) + apply (erule rtrancl_into_rtrancl) + apply (erule CollectI) + apply (erule rtrancl.induct) + apply (rule rtranclR.rtrancl_refl) + apply (erule rtranclR.rtrancl_into_rtrancl) + apply (erule CollectD) + done + +lemma NFR_imp_NF: "(nf, t) \ NFR \ t \ NF" + apply (erule NFR.induct) + apply (rule NF.intros) + apply (simp add: listall_def) + apply (erule NF.intros) + done + +text_raw {* +\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 @{text subst_type_NF}} +\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} +*} + +text {* +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 @{text "subst_type_NF"} is +@{thm [display,margin=100] subst_type_NF_correctness + [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]} +where @{text NFR} is the realizability predicate corresponding to +the datatype @{text NFT}, 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 @{text "type_NF"}, as +well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}. +The correctness statement for the main function @{text "type_NF"} is +@{thm [display,margin=100] type_NF_correctness + [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]} +where the realizability predicate @{text "rtypingR"} 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]} +*} + +subsection {* Generating executable code *} + +consts_code + arbitrary :: "'a" ("(error \"arbitrary\")") + arbitrary :: "'a \ 'b" ("(fn '_ => error \"arbitrary\")") + +generate_code + test = "type_NF" + +text {* +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. +*} + +ML {* +fun nat_of_int 0 = id0 + | nat_of_int n = Suc (nat_of_int (n-1)); + +fun int_of_nat id0 = 0 + | int_of_nat (Suc n) = 1 + int_of_nat n; + +fun dBtype_of_typ (Type ("fun", [T, U])) = + Fun (dBtype_of_typ T, dBtype_of_typ U) + | dBtype_of_typ (TFree (s, _)) = (case explode s of + ["'", a] => Atom (nat_of_int (ord a - 97)) + | _ => error "dBtype_of_typ: variable name") + | dBtype_of_typ _ = error "dBtype_of_typ: bad type"; + +fun dB_of_term (Bound i) = dB_Var (nat_of_int i) + | dB_of_term (t $ u) = dB_App (dB_of_term t, dB_of_term u) + | dB_of_term (Abs (_, _, t)) = dB_Abs (dB_of_term t) + | dB_of_term _ = error "dB_of_term: bad term"; + +fun term_of_dB Ts (Type ("fun", [T, U])) (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 (dB_Var n) = Bound (int_of_nat n) + | term_of_dB' Ts (dB_App (dBt, dBu)) = + let val t = term_of_dB' Ts dBt + in case fastype_of1 (Ts, t) of + Type ("fun", [T, U]) => 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) = + rtypingT_Var (e, nat_of_int i, dBtype_of_typ (nth_elem (i, Ts))) + | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of + Type ("fun", [T, U]) => rtypingT_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 (s, T, t)) = + let val dBT = dBtype_of_typ T + in rtypingT_Abs (e, dBT, dB_of_term t, + dBtype_of_typ (fastype_of1 (T :: Ts, t)), + typing_of_term (T :: Ts) (shift e id0 dBT) t) + end + | typing_of_term _ _ _ = error "typing_of_term: bad term"; + +fun dummyf _ = error "dummy"; +*} + +text {* +We now try out the extracted program @{text "type_NF"} on some example terms. +*} + +ML {* +val sg = sign_of (the_context()); +fun rd s = read_cterm sg (s, TypeInfer.logicT); + +val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"; +val (dB1, _) = type_NF (typing_of_term [] dummyf (term_of ct1)); +val ct1' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct1)) dB1); + +val ct2 = rd + "%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, _) = type_NF (typing_of_term [] dummyf (term_of ct2)); +val ct2' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct2)) dB2); +*} + +end