(* Title: HOL/Lambda/WeakNorm.thy ID: $Id: WeakNorm.thy,v 1.10 2005/09/22 21:56:36 nipkow Exp $ Author: Stefan Berghofer Copyright 2003 TU Muenchen *) header {* Weak normalization for simply-typed lambda calculus *} theory WeakNorm imports Type begin 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 (iprover 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] n) apply (simp only: nat.simps, iprover?)+ done lemma nat_le_dec: "!!n::nat. m < n ∨ ¬ (m < n)" apply (induct m) apply (case_tac n) apply (case_tac [3] n) apply (simp del: simp_thms, iprover?)+ 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 (iprover intro: NF.App) apply simp apply (iprover intro: NF.App) apply simp apply (iprover intro: NF.Abs) done lemma app_Var_NF: "t ∈ NF ==> ∃t'. t ° Var i ->β* t' ∧ t' ∈ NF" apply (induct set: NF) apply (simplesubst app_last) --{*Using @{text subst} makes extraction fail*} 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〉 \<turnstile> t : T ==> u ∈ NF ==> e \<turnstile> u : U ==> ∃t'. t[u/i] ->β* 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〉 \<turnstile> t : T' --> u ∈ NF --> e \<turnstile> u : T --> (∃t'. t[u/i] ->β* 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 \<turnstile> u : T" { case (App ts x e_ T'_ u_ i_) assume appT: "e〈i:T〉 \<turnstile> Var x °° ts : T'" from nat_eq_dec show "∃t'. (Var x °° ts)[u/i] ->β* t' ∧ t' ∈ NF" proof assume eq: "x = i" show ?thesis proof (cases ts) case Nil with eq have "(Var x °° [])[u/i] ->β* u" by simp with Nil and uNF show ?thesis by simp iprover next case (Cons a as) with appT have "e〈i:T〉 \<turnstile> Var x °° (a # as) : T'" by simp then obtain Us where varT': "e〈i:T〉 \<turnstile> Var x : Us \<Rrightarrow> T'" and argsT': "e〈i:T〉 \<tturnstile> 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〉 \<turnstile> Var x : T'' => Ts \<Rrightarrow> T'" by simp from varT eq have T: "T = T'' => Ts \<Rrightarrow> T'" by cases auto with uT have uT': "e \<turnstile> u : T'' => Ts \<Rrightarrow> T'" by simp from argsT' and Us have argsT: "e〈i:T〉 \<tturnstile> as : Ts" by simp from argsT' and Us have argT: "e〈i:T〉 \<turnstile> a : T''" by simp from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) have as: "!!Us. e〈i:T〉 \<tturnstile> as : Us ==> listall ?R as ==> ∃as'. Var 0 °° map (λt. lift (t[u/i]) 0) as ->β* 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〉 \<tturnstile> bs @ [b] : Us" . then obtain Vs W where Us: "Us = Vs @ [W]" and bs: "e〈i:T〉 \<tturnstile> bs : Vs" and bT: "e〈i:T〉 \<turnstile> 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 ->β* Var 0 °° map (λt. lift t 0) bs'" and bsNF: "Var 0 °° map (λt. lift t 0) bs' ∈ NF" by iprover from snoc have "?R b" by simp with bT and uNF and uT have "∃b'. b[u/i] ->β* b' ∧ b' ∈ NF" by iprover then obtain b' where bred: "b[u/i] ->β* b'" and bNF: "b' ∈ NF" by iprover 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 ->β* 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 ->β* (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 (iprover 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 ->β* Var 0 °° map (λt. lift t 0) as'" and asNF: "Var 0 °° map (λt. lift t 0) as' ∈ NF" by iprover from App and Cons have "?R a" by simp with argT and uNF and uT have "∃a'. a[u/i] ->β* a' ∧ a' ∈ NF" by iprover then obtain a' where ared: "a[u/i] ->β* a'" and aNF: "a' ∈ NF" by iprover from uNF have "lift u 0 ∈ NF" by (rule lift_NF) hence "∃u'. lift u 0 ° Var 0 ->β* u' ∧ u' ∈ NF" by (rule app_Var_NF) then obtain u' where ured: "lift u 0 ° Var 0 ->β* u'" and u'NF: "u' ∈ NF" by iprover from T and u'NF have "∃ua. u'[a'/0] ->β* ua ∧ ua ∈ NF" proof (rule MI1) have "e〈0:T''〉 \<turnstile> lift u 0 ° Var 0 : Ts \<Rrightarrow> T'" proof (rule typing.App) from uT' show "e〈0:T''〉 \<turnstile> lift u 0 : T'' => Ts \<Rrightarrow> T'" by (rule lift_type) show "e〈0:T''〉 \<turnstile> Var 0 : T''" by (rule typing.Var) simp qed with ured show "e〈0:T''〉 \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction') from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction') qed then obtain ua where uared: "u'[a'/0] ->β* ua" and uaNF: "ua ∈ NF" by iprover from ared have "(lift u 0 ° Var 0)[a[u/i]/0] ->β* (lift u 0 ° Var 0)[a'/0]" by (rule subst_preserves_beta2') also from ured have "(lift u 0 ° Var 0)[a'/0] ->β* u'[a'/0]" by (rule subst_preserves_beta') also note uared finally have "(lift u 0 ° Var 0)[a[u/i]/0] ->β* ua" . hence uared': "u ° a[u/i] ->β* ua" by simp from T have "∃r. (Var 0 °° map (λt. lift t 0) as')[ua/0] ->β* r ∧ r ∈ NF" proof (rule MI2) have "e〈0:Ts \<Rrightarrow> T'〉 \<turnstile> Var 0 °° map (λt. lift (t[u/i]) 0) as : T'" proof (rule list_app_typeI) show "e〈0:Ts \<Rrightarrow> T'〉 \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp from uT argsT have "e \<tturnstile> map (λt. t[u/i]) as : Ts" by (rule substs_lemma) hence "e〈0:Ts \<Rrightarrow> T'〉 \<tturnstile> map (λt. lift t 0) (map (λt. t[u/i]) as) : Ts" by (rule lift_types) thus "e〈0:Ts \<Rrightarrow> T'〉 \<tturnstile> 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 \<Rrightarrow> T'〉 \<turnstile> Var 0 °° map (λt. lift t 0) as' : T'" by (rule subject_reduction') from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma) with uT' have "e \<turnstile> u ° a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App) with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction') qed then obtain r where rred: "(Var 0 °° map (λt. lift t 0) as')[ua/0] ->β* r" and rnf: "r ∈ NF" by iprover from asred have "(Var 0 °° map (λt. lift (t[u/i]) 0) as)[u ° a[u/i]/0] ->β* (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] ->β* (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] ->β* r" . with rnf Cons eq show ?thesis by (simp add: map_compose [symmetric] o_def) iprover qed next assume neq: "x ≠ i" show ?thesis proof - from appT obtain Us where varT: "e〈i:T〉 \<turnstile> Var x : Us \<Rrightarrow> T'" and argsT: "e〈i:T〉 \<tturnstile> ts : Us" by (rule var_app_typesE) have ts: "!!Us. e〈i:T〉 \<tturnstile> ts : Us ==> listall ?R ts ==> ∃ts'. ∀x'. Var x' °° map (λt. t[u/i]) ts ->β* 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〉 \<tturnstile> bs @ [b] : Us" . then obtain Vs W where Us: "Us = Vs @ [W]" and bs: "e〈i:T〉 \<tturnstile> bs : Vs" and bT: "e〈i:T〉 \<turnstile> 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 ->β* Var x' °° bs'" and bsNF: "!!x'. Var x' °° bs' ∈ NF" by iprover from snoc have "?R b" by simp with bT and uNF and uT have "∃b'. b[u/i] ->β* b' ∧ b' ∈ NF" by iprover then obtain b' where bred: "b[u/i] ->β* b'" and bNF: "b' ∈ NF" by iprover from bsred bred have "!!x'. (Var x' °° map (λt. t[u/i]) bs) ° b[u/i] ->β* (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 (iprover 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 iprover next assume "¬ (i < x)" with NF neq show ?thesis by (simp add: subst_Var) iprover qed qed qed next case (Abs r e_ T'_ u_ i_) assume absT: "e〈i:T〉 \<turnstile> Abs r : T'" then obtain R S where "e〈0:R〉〈Suc i:T〉 \<turnstile> r : S" by (rule abs_typeE) simp moreover have "lift u 0 ∈ NF" by (rule lift_NF) moreover have "e〈0:R〉 \<turnstile> lift u 0 : T" by (rule lift_type) ultimately have "∃t'. r[lift u 0/Suc i] ->β* t' ∧ t' ∈ NF" by (rule Abs) thus "∃t'. Abs r[u/i] ->β* t' ∧ t' ∈ NF" by simp (iprover intro: rtrancl_beta_Abs NF.Abs) } qed qed consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *} rtyping :: "((nat => type) × dB × type) set" syntax "_rtyping" :: "(nat => type) => dB => type => bool" ("_ |-R _ : _" [50, 50, 50] 50) syntax (xsymbols) "_rtyping" :: "(nat => type) => dB => type => bool" ("_ \<turnstile>R _ : _" [50, 50, 50] 50) translations "e \<turnstile>R t : T" \<rightleftharpoons> "(e, t, T) ∈ rtyping" inductive rtyping intros Var: "e x = T ==> e \<turnstile>R Var x : T" Abs: "e〈0:T〉 \<turnstile>R t : U ==> e \<turnstile>R Abs t : (T => U)" App: "e \<turnstile>R s : T => U ==> e \<turnstile>R t : T ==> e \<turnstile>R (s ° t) : U" lemma rtyping_imp_typing: "e \<turnstile>R t : T ==> 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 T: "e \<turnstile>R t : T" shows "∃t'. t ->β* t' ∧ t' ∈ NF" using T 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 T U e s t) from App obtain s' t' where sred: "s ->β* s'" and sNF: "s' ∈ NF" and tred: "t ->β* t'" and tNF: "t' ∈ NF" by iprover have "∃u. (Var 0 ° lift t' 0)[s'/0] ->β* 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〉 \<turnstile> Var 0 ° lift t' 0 : U" proof (rule typing.App) show "e〈0:T => U〉 \<turnstile> Var 0 : T => U" by (rule typing.Var) simp from tred have "e \<turnstile> t' : T" by (rule subject_reduction') (rule rtyping_imp_typing) thus "e〈0:T => U〉 \<turnstile> lift t' 0 : T" by (rule lift_type) qed from sred show "e \<turnstile> s' : T => U" by (rule subject_reduction') (rule rtyping_imp_typing) qed then obtain u where ured: "s' ° t' ->β* u" and unf: "u ∈ NF" by simp iprover from sred tred have "s ° t ->β* s' ° t'" by (rule rtrancl_beta_App) hence "s ° t ->β* u" using ured by (rule rtrancl_trans) with unf show ?case by iprover 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\")") code_module Norm contains 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 = Norm.id_0 | nat_of_int n = Norm.Suc (nat_of_int (n-1)); fun int_of_nat Norm.id_0 = 0 | int_of_nat (Norm.Suc n) = 1 + int_of_nat n; fun dBtype_of_typ (Type ("fun", [T, U])) = Norm.Fun (dBtype_of_typ T, dBtype_of_typ U) | dBtype_of_typ (TFree (s, _)) = (case explode s of ["'", a] => Norm.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) = Norm.dB_Var (nat_of_int i) | dB_of_term (t $ u) = Norm.App (dB_of_term t, dB_of_term u) | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t) | dB_of_term _ = error "dB_of_term: bad term"; fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.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 (Norm.dB_Var n) = Bound (int_of_nat n) | term_of_dB' Ts (Norm.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) = Norm.Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i))) | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of Type ("fun", [T, U]) => Norm.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 Norm.rtypingT_Abs (e, dBT, dB_of_term t, dBtype_of_typ (fastype_of1 (T :: Ts, t)), typing_of_term (T :: Ts) (Norm.shift e Norm.id_0 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, _) = Norm.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, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2)); val ct2' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct2)) dB2); *} end
theorem listall_nil:
listall P []
theorem listall_nil_eq:
listall P [] = True
theorem listall_cons:
[| P x; listall P xs |] ==> listall P (x # xs)
theorem listall_cons_eq:
listall P (x # xs) = (P x ∧ listall P xs)
lemma listall_conj1:
listall (%x. P x ∧ Q x) xs ==> listall P xs
lemma listall_conj2:
listall (%x. P x ∧ Q x) xs ==> listall Q xs
lemma listall_app:
listall P (xs @ ys) = (listall P xs ∧ listall P ys)
lemma listall_snoc:
listall P (xs @ [x]) = (listall P xs ∧ P x)
lemma listall_cong:
xs = ys ==> listall P xs = listall P ys
lemma nat_eq_dec:
m = n ∨ m ≠ n
lemma nat_le_dec:
m < n ∨ ¬ m < n
lemma App_NF_D:
Var n °° ts ∈ NF ==> listall (%t. t ∈ NF) ts
lemma Var_NF:
Var n ∈ NF
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)
lemma subst_Var_NF:
t ∈ NF ==> t[Var i/j] ∈ NF
lemma app_Var_NF:
t ∈ NF ==> ∃t'. t ° Var i ->> t' ∧ t' ∈ NF
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)
lemma lift_NF:
t ∈ NF ==> lift t i ∈ NF
lemma subst_type_NF:
[| t ∈ NF; e〈i:U〉 |- t : T; u ∈ NF; e |- u : U |] ==> ∃t'. t[u/i] ->> t' ∧ t' ∈ NF
lemma rtyping_imp_typing:
e |-R t : T ==> e |- t : T
theorem type_NF:
e |-R t : T ==> ∃t'. t ->> t' ∧ t' ∈ NF
lemmas
trans r == ∀x y z. (x, y) ∈ r --> (y, z) ∈ r --> (x, z) ∈ r
((P ∧ Q) ∧ R) = (P ∧ Q ∧ R)
listall P (x # xs) = (P x ∧ listall P xs)
lemmas
trans r == ∀x y z. (x, y) ∈ r --> (y, z) ∈ r --> (x, z) ∈ r
((P ∧ Q) ∧ R) = (P ∧ Q ∧ R)
listall P (x # xs) = (P x ∧ listall P xs)
lemma rtranclR_rtrancl_eq:
((a, b) ∈ rtranclR r) = ((a, b) ∈ (Collect r)*)
lemma NFR_imp_NF:
(nf, t) ∈ NFR ==> t ∈ NF