src/HOL/Lambda/WeakNorm.thy
 author wenzelm Sat Apr 08 22:51:06 2006 +0200 (2006-04-08) changeset 19363 667b5ea637dd parent 19086 1b3780be6cc2 child 19380 b808efaa5828 permissions -rw-r--r--
refined 'abbreviation';
     1 (*  Title:      HOL/Lambda/WeakNorm.thy

     2     ID:         $Id$

     3     Author:     Stefan Berghofer

     4     Copyright   2003 TU Muenchen

     5 *)

     6

     7 header {* Weak normalization for simply-typed lambda calculus *}

     8

     9 theory WeakNorm imports Type begin

    10

    11 text {*

    12 Formalization by Stefan Berghofer. Partly based on a paper proof by

    13 Felix Joachimski and Ralph Matthes \cite{Matthes-Joachimski-AML}.

    14 *}

    15

    16

    17 subsection {* Terms in normal form *}

    18

    19 definition

    20   listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"

    21   "listall P xs == (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"

    22

    23 declare listall_def [extraction_expand]

    24

    25 theorem listall_nil: "listall P []"

    26   by (simp add: listall_def)

    27

    28 theorem listall_nil_eq [simp]: "listall P [] = True"

    29   by (iprover intro: listall_nil)

    30

    31 theorem listall_cons: "P x \<Longrightarrow> listall P xs \<Longrightarrow> listall P (x # xs)"

    32   apply (simp add: listall_def)

    33   apply (rule allI impI)+

    34   apply (case_tac i)

    35   apply simp+

    36   done

    37

    38 theorem listall_cons_eq [simp]: "listall P (x # xs) = (P x \<and> listall P xs)"

    39   apply (rule iffI)

    40   prefer 2

    41   apply (erule conjE)

    42   apply (erule listall_cons)

    43   apply assumption

    44   apply (unfold listall_def)

    45   apply (rule conjI)

    46   apply (erule_tac x=0 in allE)

    47   apply simp

    48   apply simp

    49   apply (rule allI)

    50   apply (erule_tac x="Suc i" in allE)

    51   apply simp

    52   done

    53

    54 lemma listall_conj1: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall P xs"

    55   by (induct xs) simp_all

    56

    57 lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs"

    58   by (induct xs) simp_all

    59

    60 lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)"

    61   apply (induct xs)

    62    apply (rule iffI, simp, simp)

    63   apply (rule iffI, simp, simp)

    64   done

    65

    66 lemma listall_snoc [simp]: "listall P (xs @ [x]) = (listall P xs \<and> P x)"

    67   apply (rule iffI)

    68   apply (simp add: listall_app)+

    69   done

    70

    71 lemma listall_cong [cong, extraction_expand]:

    72   "xs = ys \<Longrightarrow> listall P xs = listall P ys"

    73   -- {* Currently needed for strange technical reasons *}

    74   by (unfold listall_def) simp

    75

    76 consts NF :: "dB set"

    77 inductive NF

    78 intros

    79   App: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow> Var x \<degree>\<degree> ts \<in> NF"

    80   Abs: "t \<in> NF \<Longrightarrow> Abs t \<in> NF"

    81 monos listall_def

    82

    83 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"

    84   apply (induct m)

    85   apply (case_tac n)

    86   apply (case_tac [3] n)

    87   apply (simp only: nat.simps, iprover?)+

    88   done

    89

    90 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"

    91   apply (induct m)

    92   apply (case_tac n)

    93   apply (case_tac [3] n)

    94   apply (simp del: simp_thms, iprover?)+

    95   done

    96

    97 lemma App_NF_D: assumes NF: "Var n \<degree>\<degree> ts \<in> NF"

    98   shows "listall (\<lambda>t. t \<in> NF) ts" using NF

    99   by cases simp_all

   100

   101

   102 subsection {* Properties of @{text NF} *}

   103

   104 lemma Var_NF: "Var n \<in> NF"

   105   apply (subgoal_tac "Var n \<degree>\<degree> [] \<in> NF")

   106    apply simp

   107   apply (rule NF.App)

   108   apply simp

   109   done

   110

   111 lemma subst_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>

   112     listall (\<lambda>t. \<forall>i j. t[Var i/j] \<in> NF) ts \<Longrightarrow>

   113     listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. t[Var i/j]) ts)"

   114   by (induct ts) simp_all

   115

   116 lemma subst_Var_NF: "t \<in> NF \<Longrightarrow> t[Var i/j] \<in> NF"

   117   apply (induct fixing: i j set: NF)

   118   apply simp

   119   apply (frule listall_conj1)

   120   apply (drule listall_conj2)

   121   apply (drule_tac i=i and j=j in subst_terms_NF)

   122   apply assumption

   123   apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard])

   124   apply simp

   125   apply (erule NF.App)

   126   apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])

   127   apply simp

   128   apply (iprover intro: NF.App)

   129   apply simp

   130   apply (iprover intro: NF.App)

   131   apply simp

   132   apply (iprover intro: NF.Abs)

   133   done

   134

   135 lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"

   136   apply (induct set: NF)

   137   apply (simplesubst app_last)  --{*Using @{text subst} makes extraction fail*}

   138   apply (rule exI)

   139   apply (rule conjI)

   140   apply (rule rtrancl_refl)

   141   apply (rule NF.App)

   142   apply (drule listall_conj1)

   143   apply (simp add: listall_app)

   144   apply (rule Var_NF)

   145   apply (rule exI)

   146   apply (rule conjI)

   147   apply (rule rtrancl_into_rtrancl)

   148   apply (rule rtrancl_refl)

   149   apply (rule beta)

   150   apply (erule subst_Var_NF)

   151   done

   152

   153 lemma lift_terms_NF: "listall (\<lambda>t. t \<in> NF) ts \<Longrightarrow>

   154     listall (\<lambda>t. \<forall>i. lift t i \<in> NF) ts \<Longrightarrow>

   155     listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t i) ts)"

   156   by (induct ts) simp_all

   157

   158 lemma lift_NF: "t \<in> NF \<Longrightarrow> lift t i \<in> NF"

   159   apply (induct fixing: i set: NF)

   160   apply (frule listall_conj1)

   161   apply (drule listall_conj2)

   162   apply (drule_tac i=i in lift_terms_NF)

   163   apply assumption

   164   apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard])

   165   apply simp

   166   apply (rule NF.App)

   167   apply assumption

   168   apply simp

   169   apply (rule NF.App)

   170   apply assumption

   171   apply simp

   172   apply (rule NF.Abs)

   173   apply simp

   174   done

   175

   176

   177 subsection {* Main theorems *}

   178

   179 lemma norm_list:

   180   assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'"

   181   and f_NF: "\<And>t. t \<in> NF \<Longrightarrow> f t \<in> NF"

   182   and uNF: "u \<in> NF" and uT: "e \<turnstile> u : T"

   183   shows "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> as : Us \<Longrightarrow>

   184     listall (\<lambda>t. \<forall>e T' u i. e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow>

   185       u \<in> NF \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF)) as \<Longrightarrow>

   186     \<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) as \<rightarrow>\<^sub>\<beta>\<^sup>*

   187       Var j \<degree>\<degree> map f as' \<and> Var j \<degree>\<degree> map f as' \<in> NF"

   188   (is "\<And>Us. _ \<Longrightarrow> listall ?R as \<Longrightarrow> \<exists>as'. ?ex Us as as'")

   189 proof (induct as rule: rev_induct)

   190   case (Nil Us)

   191   with Var_NF have "?ex Us [] []" by simp

   192   thus ?case ..

   193 next

   194   case (snoc b bs Us)

   195   have "e\<langle>i:T\<rangle> \<tturnstile> bs  @ [b] : Us" .

   196   then obtain Vs W where Us: "Us = Vs @ [W]"

   197     and bs: "e\<langle>i:T\<rangle> \<tturnstile> bs : Vs" and bT: "e\<langle>i:T\<rangle> \<turnstile> b : W"

   198     by (rule types_snocE)

   199   from snoc have "listall ?R bs" by simp

   200   with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)

   201   then obtain bs' where

   202     bsred: "\<And>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"

   203     and bsNF: "\<And>j. Var j \<degree>\<degree> map f bs' \<in> NF" by iprover

   204   from snoc have "?R b" by simp

   205   with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF"

   206     by iprover

   207   then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF"

   208     by iprover

   209   from bsNF [of 0] have "listall (\<lambda>t. t \<in> NF) (map f bs')"

   210     by (rule App_NF_D)

   211   moreover have "f b' \<in> NF" by (rule f_NF)

   212   ultimately have "listall (\<lambda>t. t \<in> NF) (map f (bs' @ [b']))"

   213     by simp

   214   hence "\<And>j. Var j \<degree>\<degree> map f (bs' @ [b']) \<in> NF" by (rule NF.App)

   215   moreover from bred have "f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>* f b'"

   216     by (rule f_compat)

   217   with bsred have

   218     "\<And>j. (Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs) \<degree> f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>*

   219      (Var j \<degree>\<degree> map f bs') \<degree> f b'" by (rule rtrancl_beta_App)

   220   ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp

   221   thus ?case ..

   222 qed

   223

   224 lemma subst_type_NF:

   225   "\<And>t e T u i. t \<in> NF \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> u \<in> NF \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> \<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"

   226   (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")

   227 proof (induct U)

   228   fix T t

   229   let ?R = "\<lambda>t. \<forall>e T' u i.

   230     e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> u \<in> NF \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF)"

   231   assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"

   232   assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"

   233   assume "t \<in> NF"

   234   thus "\<And>e T' u i. PROP ?Q t e T' u i T"

   235   proof induct

   236     fix e T' u i assume uNF: "u \<in> NF" and uT: "e \<turnstile> u : T"

   237     {

   238       case (App ts x e_ T'_ u_ i_)

   239       assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"

   240       then obtain Us

   241 	where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"

   242 	and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us"

   243 	by (rule var_app_typesE)

   244       from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"

   245       proof

   246 	assume eq: "x = i"

   247 	show ?thesis

   248 	proof (cases ts)

   249 	  case Nil

   250 	  with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp

   251 	  with Nil and uNF show ?thesis by simp iprover

   252 	next

   253 	  case (Cons a as)

   254           with argsT obtain T'' Ts where Us: "Us = T'' # Ts"

   255 	    by (cases Us) (rule FalseE, simp+)

   256 	  from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'"

   257 	    by simp

   258           from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto

   259           with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp

   260 	  from argsT Us Cons have argsT': "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" by simp

   261 	  from argsT Us Cons have argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" by simp

   262 	  from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)

   263 	  from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)

   264 	  with lift_preserves_beta' lift_NF uNF uT argsT'

   265 	  have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*

   266             Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and>

   267 	    Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by (rule norm_list)

   268 	  then obtain as' where

   269 	    asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*

   270 	      Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"

   271 	    and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by iprover

   272 	  from App and Cons have "?R a" by simp

   273 	  with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> a' \<in> NF"

   274 	    by iprover

   275 	  then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by iprover

   276 	  from uNF have "lift u 0 \<in> NF" by (rule lift_NF)

   277 	  hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> u' \<in> NF" by (rule app_Var_NF)

   278 	  then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "u' \<in> NF"

   279 	    by iprover

   280 	  from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> ua \<in> NF"

   281 	  proof (rule MI1)

   282 	    have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"

   283 	    proof (rule typing.App)

   284 	      from uT' show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by (rule lift_type)

   285 	      show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" by (rule typing.Var) simp

   286 	    qed

   287 	    with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction')

   288 	    from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')

   289 	  qed

   290 	  then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "ua \<in> NF"

   291 	    by iprover

   292 	  from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]"

   293 	    by (rule subst_preserves_beta2')

   294 	  also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]"

   295 	    by (rule subst_preserves_beta')

   296 	  also note uared

   297 	  finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" .

   298 	  hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp

   299 	  from T have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> r \<in> NF"

   300 	  proof (rule MI2)

   301 	    have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'"

   302 	    proof (rule list_app_typeI)

   303 	      show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp

   304 	      from uT argsT' have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"

   305 		by (rule substs_lemma)

   306 	      hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts"

   307 		by (rule lift_types)

   308 	      thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts"

   309 		by (simp_all add: map_compose [symmetric] o_def)

   310 	    qed

   311 	    with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'"

   312 	      by (rule subject_reduction')

   313 	    from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)

   314 	    with uT' have "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App)

   315 	    with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')

   316 	  qed

   317 	  then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"

   318 	    and rnf: "r \<in> NF" by iprover

   319 	  from asred have

   320 	    "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*

   321 	    (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"

   322 	    by (rule subst_preserves_beta')

   323 	  also from uared' have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*

   324 	    (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2')

   325 	  also note rred

   326 	  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" .

   327 	  with rnf Cons eq show ?thesis

   328 	    by (simp add: map_compose [symmetric] o_def) iprover

   329 	qed

   330       next

   331 	assume neq: "x \<noteq> i"

   332 	from App have "listall ?R ts" by (iprover dest: listall_conj2)

   333 	with TrueI TrueI uNF uT argsT

   334 	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>

   335 	  Var j \<degree>\<degree> ts' \<in> NF" (is "\<exists>ts'. ?ex ts'")

   336 	  by (rule norm_list [of "\<lambda>t. t", simplified])

   337 	then obtain ts' where NF: "?ex ts'" ..

   338 	from nat_le_dec show ?thesis

   339 	proof

   340 	  assume "i < x"

   341 	  with NF show ?thesis by simp iprover

   342 	next

   343 	  assume "\<not> (i < x)"

   344 	  with NF neq show ?thesis by (simp add: subst_Var) iprover

   345 	qed

   346       qed

   347     next

   348       case (Abs r e_ T'_ u_ i_)

   349       assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"

   350       then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp

   351       moreover have "lift u 0 \<in> NF" by (rule lift_NF)

   352       moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" by (rule lift_type)

   353       ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" by (rule Abs)

   354       thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"

   355 	by simp (iprover intro: rtrancl_beta_Abs NF.Abs)

   356     }

   357   qed

   358 qed

   359

   360

   361 consts -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}

   362   rtyping :: "((nat \<Rightarrow> type) \<times> dB \<times> type) set"

   363

   364 abbreviation

   365   rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ |-\<^sub>R _ : _" [50, 50, 50] 50)

   366   "e |-\<^sub>R t : T == (e, t, T) \<in> rtyping"

   367

   368 abbreviation (xsymbols)

   369   rtyping_rel :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"    ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)

   370   "e \<turnstile>\<^sub>R t : T == e |-\<^sub>R t : T"

   371

   372 inductive rtyping

   373   intros

   374     Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"

   375     Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"

   376     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"

   377

   378 lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T"

   379   apply (induct set: rtyping)

   380   apply (erule typing.Var)

   381   apply (erule typing.Abs)

   382   apply (erule typing.App)

   383   apply assumption

   384   done

   385

   386

   387 theorem type_NF:

   388   assumes "e \<turnstile>\<^sub>R t : T"

   389   shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using prems

   390 proof induct

   391   case Var

   392   show ?case by (iprover intro: Var_NF)

   393 next

   394   case Abs

   395   thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)

   396 next

   397   case (App T U e s t)

   398   from App obtain s' t' where

   399     sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "s' \<in> NF"

   400     and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by iprover

   401   have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> u \<in> NF"

   402   proof (rule subst_type_NF)

   403     have "lift t' 0 \<in> NF" by (rule lift_NF)

   404     hence "listall (\<lambda>t. t \<in> NF) [lift t' 0]" by (rule listall_cons) (rule listall_nil)

   405     hence "Var 0 \<degree>\<degree> [lift t' 0] \<in> NF" by (rule NF.App)

   406     thus "Var 0 \<degree> lift t' 0 \<in> NF" by simp

   407     show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U"

   408     proof (rule typing.App)

   409       show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"

   410       	by (rule typing.Var) simp

   411       from tred have "e \<turnstile> t' : T"

   412       	by (rule subject_reduction') (rule rtyping_imp_typing)

   413       thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T"

   414       	by (rule lift_type)

   415     qed

   416     from sred show "e \<turnstile> s' : T \<Rightarrow> U"

   417       by (rule subject_reduction') (rule rtyping_imp_typing)

   418   qed

   419   then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp iprover

   420   from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)

   421   hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans)

   422   with unf show ?case by iprover

   423 qed

   424

   425

   426 subsection {* Extracting the program *}

   427

   428 declare NF.induct [ind_realizer]

   429 declare rtrancl.induct [ind_realizer irrelevant]

   430 declare rtyping.induct [ind_realizer]

   431 lemmas [extraction_expand] = trans_def conj_assoc listall_cons_eq

   432

   433 extract type_NF

   434

   435 lemma rtranclR_rtrancl_eq: "((a, b) \<in> rtranclR r) = ((a, b) \<in> rtrancl (Collect r))"

   436   apply (rule iffI)

   437   apply (erule rtranclR.induct)

   438   apply (rule rtrancl_refl)

   439   apply (erule rtrancl_into_rtrancl)

   440   apply (erule CollectI)

   441   apply (erule rtrancl.induct)

   442   apply (rule rtranclR.rtrancl_refl)

   443   apply (erule rtranclR.rtrancl_into_rtrancl)

   444   apply (erule CollectD)

   445   done

   446

   447 lemma NFR_imp_NF: "(nf, t) \<in> NFR \<Longrightarrow> t \<in> NF"

   448   apply (erule NFR.induct)

   449   apply (rule NF.intros)

   450   apply (simp add: listall_def)

   451   apply (erule NF.intros)

   452   done

   453

   454 text_raw {*

   455 \begin{figure}

   456 \renewcommand{\isastyle}{\scriptsize\it}%

   457 @{thm [display,eta_contract=false,margin=100] subst_type_NF_def}

   458 \renewcommand{\isastyle}{\small\it}%

   459 \caption{Program extracted from @{text subst_type_NF}}

   460 \label{fig:extr-subst-type-nf}

   461 \end{figure}

   462

   463 \begin{figure}

   464 \renewcommand{\isastyle}{\scriptsize\it}%

   465 @{thm [display,margin=100] subst_Var_NF_def}

   466 @{thm [display,margin=100] app_Var_NF_def}

   467 @{thm [display,margin=100] lift_NF_def}

   468 @{thm [display,eta_contract=false,margin=100] type_NF_def}

   469 \renewcommand{\isastyle}{\small\it}%

   470 \caption{Program extracted from lemmas and main theorem}

   471 \label{fig:extr-type-nf}

   472 \end{figure}

   473 *}

   474

   475 text {*

   476 The program corresponding to the proof of the central lemma, which

   477 performs substitution and normalization, is shown in Figure

   478 \ref{fig:extr-subst-type-nf}. The correctness

   479 theorem corresponding to the program @{text "subst_type_NF"} is

   480 @{thm [display,margin=100] subst_type_NF_correctness

   481   [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}

   482 where @{text NFR} is the realizability predicate corresponding to

   483 the datatype @{text NFT}, which is inductively defined by the rules

   484 \pagebreak

   485 @{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]}

   486

   487 The programs corresponding to the main theorem @{text "type_NF"}, as

   488 well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.

   489 The correctness statement for the main function @{text "type_NF"} is

   490 @{thm [display,margin=100] type_NF_correctness

   491   [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}

   492 where the realizability predicate @{text "rtypingR"} corresponding to the

   493 computationally relevant version of the typing judgement is inductively

   494 defined by the rules

   495 @{thm [display,margin=100] rtypingR.Var [no_vars]

   496   rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]}

   497 *}

   498

   499 subsection {* Generating executable code *}

   500

   501 consts_code

   502   arbitrary :: "'a"       ("(error \"arbitrary\")")

   503   arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")

   504

   505 code_module Norm

   506 contains

   507   test = "type_NF"

   508

   509 text {*

   510 The following functions convert between Isabelle's built-in {\tt term}

   511 datatype and the generated {\tt dB} datatype. This allows to

   512 generate example terms using Isabelle's parser and inspect

   513 normalized terms using Isabelle's pretty printer.

   514 *}

   515

   516 ML {*

   517 fun nat_of_int 0 = Norm.id_0

   518   | nat_of_int n = Norm.Suc (nat_of_int (n-1));

   519

   520 fun int_of_nat Norm.id_0 = 0

   521   | int_of_nat (Norm.Suc n) = 1 + int_of_nat n;

   522

   523 fun dBtype_of_typ (Type ("fun", [T, U])) =

   524       Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)

   525   | dBtype_of_typ (TFree (s, _)) = (case explode s of

   526         ["'", a] => Norm.Atom (nat_of_int (ord a - 97))

   527       | _ => error "dBtype_of_typ: variable name")

   528   | dBtype_of_typ _ = error "dBtype_of_typ: bad type";

   529

   530 fun dB_of_term (Bound i) = Norm.dB_Var (nat_of_int i)

   531   | dB_of_term (t $u) = Norm.App (dB_of_term t, dB_of_term u)   532 | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t)   533 | dB_of_term _ = error "dB_of_term: bad term";   534   535 fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.Abs dBt) =   536 Abs ("x", T, term_of_dB (T :: Ts) U dBt)   537 | term_of_dB Ts _ dBt = term_of_dB' Ts dBt   538 and term_of_dB' Ts (Norm.dB_Var n) = Bound (int_of_nat n)   539 | term_of_dB' Ts (Norm.App (dBt, dBu)) =   540 let val t = term_of_dB' Ts dBt   541 in case fastype_of1 (Ts, t) of   542 Type ("fun", [T, U]) => t$ term_of_dB Ts T dBu

   543         | _ => error "term_of_dB: function type expected"

   544       end

   545   | term_of_dB' _ _ = error "term_of_dB: term not in normal form";

   546

   547 fun typing_of_term Ts e (Bound i) =

   548       Norm.Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i)))

   549   | typing_of_term Ts e (t \$ u) = (case fastype_of1 (Ts, t) of

   550         Type ("fun", [T, U]) => Norm.rtypingT_App (e, dB_of_term t,

   551           dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,

   552           typing_of_term Ts e t, typing_of_term Ts e u)

   553       | _ => error "typing_of_term: function type expected")

   554   | typing_of_term Ts e (Abs (s, T, t)) =

   555       let val dBT = dBtype_of_typ T

   556       in Norm.rtypingT_Abs (e, dBT, dB_of_term t,

   557         dBtype_of_typ (fastype_of1 (T :: Ts, t)),

   558         typing_of_term (T :: Ts) (Norm.shift e Norm.id_0 dBT) t)

   559       end

   560   | typing_of_term _ _ _ = error "typing_of_term: bad term";

   561

   562 fun dummyf _ = error "dummy";

   563 *}

   564

   565 text {*

   566 We now try out the extracted program @{text "type_NF"} on some example terms.

   567 *}

   568

   569 ML {*

   570 val sg = sign_of (the_context());

   571 fun rd s = read_cterm sg (s, TypeInfer.logicT);

   572

   573 val ct1 = rd "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))";

   574 val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));

   575 val ct1' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct1)) dB1);

   576

   577 val ct2 = rd

   578   "%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)))))";

   579 val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));

   580 val ct2' = cterm_of sg (term_of_dB [] (#T (rep_cterm ct2)) dB2);

   581 *}

   582

   583 end