author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 25107 dbf09ca6a80e
child 36862 952b2b102a0a
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/Lambda/Standardization.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer
     4     Copyright   2005 TU Muenchen
     5 *)
     7 header {* Standardization *}
     9 theory Standardization
    10 imports NormalForm
    11 begin
    13 text {*
    14 Based on lecture notes by Ralph Matthes \cite{Matthes-ESSLLI2000},
    15 original proof idea due to Ralph Loader \cite{Loader1998}.
    16 *}
    19 subsection {* Standard reduction relation *}
    21 declare listrel_mono [mono_set]
    23 inductive
    24   sred :: "dB \<Rightarrow> dB \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>s" 50)
    25   and sredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool"  (infixl "[\<rightarrow>\<^sub>s]" 50)
    26 where
    27   "s [\<rightarrow>\<^sub>s] t \<equiv> listrelp op \<rightarrow>\<^sub>s s t"
    28 | Var: "rs [\<rightarrow>\<^sub>s] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> rs'"
    29 | Abs: "r \<rightarrow>\<^sub>s r' \<Longrightarrow> ss [\<rightarrow>\<^sub>s] ss' \<Longrightarrow> Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> ss'"
    30 | Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>s t"
    32 lemma refl_listrelp: "\<forall>x\<in>set xs. R x x \<Longrightarrow> listrelp R xs xs"
    33   by (induct xs) (auto intro: listrelp.intros)
    35 lemma refl_sred: "t \<rightarrow>\<^sub>s t"
    36   by (induct t rule: Apps_dB_induct) (auto intro: refl_listrelp sred.intros)
    38 lemma refl_sreds: "ts [\<rightarrow>\<^sub>s] ts"
    39   by (simp add: refl_sred refl_listrelp)
    41 lemma listrelp_conj1: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp R x y"
    42   by (erule listrelp.induct) (auto intro: listrelp.intros)
    44 lemma listrelp_conj2: "listrelp (\<lambda>x y. R x y \<and> S x y) x y \<Longrightarrow> listrelp S x y"
    45   by (erule listrelp.induct) (auto intro: listrelp.intros)
    47 lemma listrelp_app:
    48   assumes xsys: "listrelp R xs ys"
    49   shows "listrelp R xs' ys' \<Longrightarrow> listrelp R (xs @ xs') (ys @ ys')" using xsys
    50   by (induct arbitrary: xs' ys') (auto intro: listrelp.intros)
    52 lemma lemma1:
    53   assumes r: "r \<rightarrow>\<^sub>s r'" and s: "s \<rightarrow>\<^sub>s s'"
    54   shows "r \<degree> s \<rightarrow>\<^sub>s r' \<degree> s'" using r
    55 proof induct
    56   case (Var rs rs' x)
    57   then have "rs [\<rightarrow>\<^sub>s] rs'" by (rule listrelp_conj1)
    58   moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
    59   ultimately have "rs @ [s] [\<rightarrow>\<^sub>s] rs' @ [s']" by (rule listrelp_app)
    60   hence "Var x \<degree>\<degree> (rs @ [s]) \<rightarrow>\<^sub>s Var x \<degree>\<degree> (rs' @ [s'])" by (rule sred.Var)
    61   thus ?case by (simp only: app_last)
    62 next
    63   case (Abs r r' ss ss')
    64   from Abs(3) have "ss [\<rightarrow>\<^sub>s] ss'" by (rule listrelp_conj1)
    65   moreover have "[s] [\<rightarrow>\<^sub>s] [s']" by (iprover intro: s listrelp.intros)
    66   ultimately have "ss @ [s] [\<rightarrow>\<^sub>s] ss' @ [s']" by (rule listrelp_app)
    67   with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> (ss' @ [s'])"
    68     by (rule sred.Abs)
    69   thus ?case by (simp only: app_last)
    70 next
    71   case (Beta r u ss t)
    72   hence "r[u/0] \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (simp only: app_last)
    73   hence "Abs r \<degree> u \<degree>\<degree> (ss @ [s]) \<rightarrow>\<^sub>s t \<degree> s'" by (rule sred.Beta)
    74   thus ?case by (simp only: app_last)
    75 qed
    77 lemma lemma1':
    78   assumes ts: "ts [\<rightarrow>\<^sub>s] ts'"
    79   shows "r \<rightarrow>\<^sub>s r' \<Longrightarrow> r \<degree>\<degree> ts \<rightarrow>\<^sub>s r' \<degree>\<degree> ts'" using ts
    80   by (induct arbitrary: r r') (auto intro: lemma1)
    82 lemma lemma2_1:
    83   assumes beta: "t \<rightarrow>\<^sub>\<beta> u"
    84   shows "t \<rightarrow>\<^sub>s u" using beta
    85 proof induct
    86   case (beta s t)
    87   have "Abs s \<degree> t \<degree>\<degree> [] \<rightarrow>\<^sub>s s[t/0] \<degree>\<degree> []" by (iprover intro: sred.Beta refl_sred)
    88   thus ?case by simp
    89 next
    90   case (appL s t u)
    91   thus ?case by (iprover intro: lemma1 refl_sred)
    92 next
    93   case (appR s t u)
    94   thus ?case by (iprover intro: lemma1 refl_sred)
    95 next
    96   case (abs s t)
    97   hence "Abs s \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs t \<degree>\<degree> []" by (iprover intro: sred.Abs listrelp.Nil)
    98   thus ?case by simp
    99 qed
   101 lemma listrelp_betas:
   102   assumes ts: "listrelp op \<rightarrow>\<^sub>\<beta>\<^sup>* ts ts'"
   103   shows "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> t \<degree>\<degree> ts \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<degree>\<degree> ts'" using ts
   104   by induct auto
   106 lemma lemma2_2:
   107   assumes t: "t \<rightarrow>\<^sub>s u"
   108   shows "t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using t
   109   by induct (auto dest: listrelp_conj2
   110     intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp)
   112 lemma sred_lift:
   113   assumes s: "s \<rightarrow>\<^sub>s t"
   114   shows "lift s i \<rightarrow>\<^sub>s lift t i" using s
   115 proof (induct arbitrary: i)
   116   case (Var rs rs' x)
   117   hence "map (\<lambda>t. lift t i) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) rs'"
   118     by induct (auto intro: listrelp.intros)
   119   thus ?case by (cases "x < i") (auto intro: sred.Var)
   120 next
   121   case (Abs r r' ss ss')
   122   from Abs(3) have "map (\<lambda>t. lift t i) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. lift t i) ss'"
   123     by induct (auto intro: listrelp.intros)
   124   thus ?case by (auto intro: sred.Abs Abs)
   125 next
   126   case (Beta r s ss t)
   127   thus ?case by (auto intro: sred.Beta)
   128 qed
   130 lemma lemma3:
   131   assumes r: "r \<rightarrow>\<^sub>s r'"
   132   shows "s \<rightarrow>\<^sub>s s' \<Longrightarrow> r[s/x] \<rightarrow>\<^sub>s r'[s'/x]" using r
   133 proof (induct arbitrary: s s' x)
   134   case (Var rs rs' y)
   135   hence "map (\<lambda>t. t[s/x]) rs [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) rs'"
   136     by induct (auto intro: listrelp.intros Var)
   137   moreover have "Var y[s/x] \<rightarrow>\<^sub>s Var y[s'/x]"
   138   proof (cases "y < x")
   139     case True thus ?thesis by simp (rule refl_sred)
   140   next
   141     case False
   142     thus ?thesis
   143       by (cases "y = x") (auto simp add: Var intro: refl_sred)
   144   qed
   145   ultimately show ?case by simp (rule lemma1')
   146 next
   147   case (Abs r r' ss ss')
   148   from Abs(4) have "lift s 0 \<rightarrow>\<^sub>s lift s' 0" by (rule sred_lift)
   149   hence "r[lift s 0/Suc x] \<rightarrow>\<^sub>s r'[lift s' 0/Suc x]" by (fast intro: Abs.hyps)
   150   moreover from Abs(3) have "map (\<lambda>t. t[s/x]) ss [\<rightarrow>\<^sub>s] map (\<lambda>t. t[s'/x]) ss'"
   151     by induct (auto intro: listrelp.intros Abs)
   152   ultimately show ?case by simp (rule sred.Abs)
   153 next
   154   case (Beta r u ss t)
   155   thus ?case by (auto simp add: subst_subst intro: sred.Beta)
   156 qed
   158 lemma lemma4_aux:
   159   assumes rs: "listrelp (\<lambda>t u. t \<rightarrow>\<^sub>s u \<and> (\<forall>r. u \<rightarrow>\<^sub>\<beta> r \<longrightarrow> t \<rightarrow>\<^sub>s r)) rs rs'"
   160   shows "rs' => ss \<Longrightarrow> rs [\<rightarrow>\<^sub>s] ss" using rs
   161 proof (induct arbitrary: ss)
   162   case Nil
   163   thus ?case by cases (auto intro: listrelp.Nil)
   164 next
   165   case (Cons x y xs ys)
   166   note Cons' = Cons
   167   show ?case
   168   proof (cases ss)
   169     case Nil with Cons show ?thesis by simp
   170   next
   171     case (Cons y' ys')
   172     hence ss: "ss = y' # ys'" by simp
   173     from Cons Cons' have "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys \<or> y' = y \<and> ys => ys'" by simp
   174     hence "x # xs [\<rightarrow>\<^sub>s] y' # ys'"
   175     proof
   176       assume H: "y \<rightarrow>\<^sub>\<beta> y' \<and> ys' = ys"
   177       with Cons' have "x \<rightarrow>\<^sub>s y'" by blast
   178       moreover from Cons' have "xs [\<rightarrow>\<^sub>s] ys" by (iprover dest: listrelp_conj1)
   179       ultimately have "x # xs [\<rightarrow>\<^sub>s] y' # ys" by (rule listrelp.Cons)
   180       with H show ?thesis by simp
   181     next
   182       assume H: "y' = y \<and> ys => ys'"
   183       with Cons' have "x \<rightarrow>\<^sub>s y'" by blast
   184       moreover from H have "xs [\<rightarrow>\<^sub>s] ys'" by (blast intro: Cons')
   185       ultimately show ?thesis by (rule listrelp.Cons)
   186     qed
   187     with ss show ?thesis by simp
   188   qed
   189 qed
   191 lemma lemma4:
   192   assumes r: "r \<rightarrow>\<^sub>s r'"
   193   shows "r' \<rightarrow>\<^sub>\<beta> r'' \<Longrightarrow> r \<rightarrow>\<^sub>s r''" using r
   194 proof (induct arbitrary: r'')
   195   case (Var rs rs' x)
   196   then obtain ss where rs: "rs' => ss" and r'': "r'' = Var x \<degree>\<degree> ss"
   197     by (blast dest: head_Var_reduction)
   198   from Var(1) rs have "rs [\<rightarrow>\<^sub>s] ss" by (rule lemma4_aux)
   199   hence "Var x \<degree>\<degree> rs \<rightarrow>\<^sub>s Var x \<degree>\<degree> ss" by (rule sred.Var)
   200   with r'' show ?case by simp
   201 next
   202   case (Abs r r' ss ss')
   203   from `Abs r' \<degree>\<degree> ss' \<rightarrow>\<^sub>\<beta> r''` show ?case
   204   proof
   205     fix s
   206     assume r'': "r'' = s \<degree>\<degree> ss'"
   207     assume "Abs r' \<rightarrow>\<^sub>\<beta> s"
   208     then obtain r''' where s: "s = Abs r'''" and r''': "r' \<rightarrow>\<^sub>\<beta> r'''" by cases auto
   209     from r''' have "r \<rightarrow>\<^sub>s r'''" by (blast intro: Abs)
   210     moreover from Abs have "ss [\<rightarrow>\<^sub>s] ss'" by (iprover dest: listrelp_conj1)
   211     ultimately have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r''' \<degree>\<degree> ss'" by (rule sred.Abs)
   212     with r'' s show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
   213   next
   214     fix rs'
   215     assume "ss' => rs'"
   216     with Abs(3) have "ss [\<rightarrow>\<^sub>s] rs'" by (rule lemma4_aux)
   217     with `r \<rightarrow>\<^sub>s r'` have "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> rs'" by (rule sred.Abs)
   218     moreover assume "r'' = Abs r' \<degree>\<degree> rs'"
   219     ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" by simp
   220   next
   221     fix t u' us'
   222     assume "ss' = u' # us'"
   223     with Abs(3) obtain u us where
   224       ss: "ss = u # us" and u: "u \<rightarrow>\<^sub>s u'" and us: "us [\<rightarrow>\<^sub>s] us'"
   225       by cases (auto dest!: listrelp_conj1)
   226     have "r[u/0] \<rightarrow>\<^sub>s r'[u'/0]" using Abs(1) and u by (rule lemma3)
   227     with us have "r[u/0] \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule lemma1')
   228     hence "Abs r \<degree> u \<degree>\<degree> us \<rightarrow>\<^sub>s r'[u'/0] \<degree>\<degree> us'" by (rule sred.Beta)
   229     moreover assume "Abs r' = Abs t" and "r'' = t[u'/0] \<degree>\<degree> us'"
   230     ultimately show "Abs r \<degree>\<degree> ss \<rightarrow>\<^sub>s r''" using ss by simp
   231   qed
   232 next
   233   case (Beta r s ss t)
   234   show ?case
   235     by (rule sred.Beta) (rule Beta)+
   236 qed
   238 lemma rtrancl_beta_sred:
   239   assumes r: "r \<rightarrow>\<^sub>\<beta>\<^sup>* r'"
   240   shows "r \<rightarrow>\<^sub>s r'" using r
   241   by induct (iprover intro: refl_sred lemma4)+
   244 subsection {* Leftmost reduction and weakly normalizing terms *}
   246 inductive
   247   lred :: "dB \<Rightarrow> dB \<Rightarrow> bool"  (infixl "\<rightarrow>\<^sub>l" 50)
   248   and lredlist :: "dB list \<Rightarrow> dB list \<Rightarrow> bool"  (infixl "[\<rightarrow>\<^sub>l]" 50)
   249 where
   250   "s [\<rightarrow>\<^sub>l] t \<equiv> listrelp op \<rightarrow>\<^sub>l s t"
   251 | Var: "rs [\<rightarrow>\<^sub>l] rs' \<Longrightarrow> Var x \<degree>\<degree> rs \<rightarrow>\<^sub>l Var x \<degree>\<degree> rs'"
   252 | Abs: "r \<rightarrow>\<^sub>l r' \<Longrightarrow> Abs r \<rightarrow>\<^sub>l Abs r'"
   253 | Beta: "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t \<Longrightarrow> Abs r \<degree> s \<degree>\<degree> ss \<rightarrow>\<^sub>l t"
   255 lemma lred_imp_sred:
   256   assumes lred: "s \<rightarrow>\<^sub>l t"
   257   shows "s \<rightarrow>\<^sub>s t" using lred
   258 proof induct
   259   case (Var rs rs' x)
   260   then have "rs [\<rightarrow>\<^sub>s] rs'"
   261     by induct (iprover intro: listrelp.intros)+
   262   then show ?case by (rule sred.Var)
   263 next
   264   case (Abs r r')
   265   from `r \<rightarrow>\<^sub>s r'`
   266   have "Abs r \<degree>\<degree> [] \<rightarrow>\<^sub>s Abs r' \<degree>\<degree> []" using listrelp.Nil
   267     by (rule sred.Abs)
   268   then show ?case by simp
   269 next
   270   case (Beta r s ss t)
   271   from `r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>s t`
   272   show ?case by (rule sred.Beta)
   273 qed
   275 inductive WN :: "dB => bool"
   276   where
   277     Var: "listsp WN rs \<Longrightarrow> WN (Var n \<degree>\<degree> rs)"
   278   | Lambda: "WN r \<Longrightarrow> WN (Abs r)"
   279   | Beta: "WN ((r[s/0]) \<degree>\<degree> ss) \<Longrightarrow> WN ((Abs r \<degree> s) \<degree>\<degree> ss)"
   281 lemma listrelp_imp_listsp1:
   282   assumes H: "listrelp (\<lambda>x y. P x) xs ys"
   283   shows "listsp P xs" using H
   284   by induct auto
   286 lemma listrelp_imp_listsp2:
   287   assumes H: "listrelp (\<lambda>x y. P y) xs ys"
   288   shows "listsp P ys" using H
   289   by induct auto
   291 lemma lemma5:
   292   assumes lred: "r \<rightarrow>\<^sub>l r'"
   293   shows "WN r" and "NF r'" using lred
   294   by induct
   295     (iprover dest: listrelp_conj1 listrelp_conj2
   296      listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros
   297      NF.intros [simplified listall_listsp_eq])+
   299 lemma lemma6:
   300   assumes wn: "WN r"
   301   shows "\<exists>r'. r \<rightarrow>\<^sub>l r'" using wn
   302 proof induct
   303   case (Var rs n)
   304   then have "\<exists>rs'. rs [\<rightarrow>\<^sub>l] rs'"
   305     by induct (iprover intro: listrelp.intros)+
   306   then show ?case by (iprover intro: lred.Var)
   307 qed (iprover intro: lred.intros)+
   309 lemma lemma7:
   310   assumes r: "r \<rightarrow>\<^sub>s r'"
   311   shows "NF r' \<Longrightarrow> r \<rightarrow>\<^sub>l r'" using r
   312 proof induct
   313   case (Var rs rs' x)
   314   from `NF (Var x \<degree>\<degree> rs')` have "listall NF rs'"
   315     by cases simp_all
   316   with Var(1) have "rs [\<rightarrow>\<^sub>l] rs'"
   317   proof induct
   318     case Nil
   319     show ?case by (rule listrelp.Nil)
   320   next
   321     case (Cons x y xs ys)
   322     hence "x \<rightarrow>\<^sub>l y" and "xs [\<rightarrow>\<^sub>l] ys" by simp_all
   323     thus ?case by (rule listrelp.Cons)
   324   qed
   325   thus ?case by (rule lred.Var)
   326 next
   327   case (Abs r r' ss ss')
   328   from `NF (Abs r' \<degree>\<degree> ss')`
   329   have ss': "ss' = []" by (rule Abs_NF)
   330   from Abs(3) have ss: "ss = []" using ss'
   331     by cases simp_all
   332   from ss' Abs have "NF (Abs r')" by simp
   333   hence "NF r'" by cases simp_all
   334   with Abs have "r \<rightarrow>\<^sub>l r'" by simp
   335   hence "Abs r \<rightarrow>\<^sub>l Abs r'" by (rule lred.Abs)
   336   with ss ss' show ?case by simp
   337 next
   338   case (Beta r s ss t)
   339   hence "r[s/0] \<degree>\<degree> ss \<rightarrow>\<^sub>l t" by simp
   340   thus ?case by (rule lred.Beta)
   341 qed
   343 lemma WN_eq: "WN t = (\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')"
   344 proof
   345   assume "WN t"
   346   then have "\<exists>t'. t \<rightarrow>\<^sub>l t'" by (rule lemma6)
   347   then obtain t' where t': "t \<rightarrow>\<^sub>l t'" ..
   348   then have NF: "NF t'" by (rule lemma5)
   349   from t' have "t \<rightarrow>\<^sub>s t'" by (rule lred_imp_sred)
   350   then have "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" by (rule lemma2_2)
   351   with NF show "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by iprover
   352 next
   353   assume "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
   354   then obtain t' where t': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and NF: "NF t'"
   355     by iprover
   356   from t' have "t \<rightarrow>\<^sub>s t'" by (rule rtrancl_beta_sred)
   357   then have "t \<rightarrow>\<^sub>l t'" using NF by (rule lemma7)
   358   then show "WN t" by (rule lemma5)
   359 qed
   361 end