src/HOL/Lambda/Eta.thy
author krauss
Mon Jul 27 21:47:41 2009 +0200 (2009-07-27 ago)
changeset 32235 8f9b8d14fc9f
parent 26181 fedc257417fc
child 32605 43ed78ee285d
permissions -rw-r--r--
"more standard" argument order of relation composition (op O)
     1 (*  Title:      HOL/Lambda/Eta.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Stefan Berghofer
     4     Copyright   1995, 2005 TU Muenchen
     5 *)
     6 
     7 header {* Eta-reduction *}
     8 
     9 theory Eta imports ParRed begin
    10 
    11 
    12 subsection {* Definition of eta-reduction and relatives *}
    13 
    14 primrec
    15   free :: "dB => nat => bool"
    16 where
    17     "free (Var j) i = (j = i)"
    18   | "free (s \<degree> t) i = (free s i \<or> free t i)"
    19   | "free (Abs s) i = free s (i + 1)"
    20 
    21 inductive
    22   eta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<eta>" 50)
    23 where
    24     eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s[dummy/0]"
    25   | appL [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> s \<degree> u \<rightarrow>\<^sub>\<eta> t \<degree> u"
    26   | appR [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> u \<degree> s \<rightarrow>\<^sub>\<eta> u \<degree> t"
    27   | abs [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> Abs s \<rightarrow>\<^sub>\<eta> Abs t"
    28 
    29 abbreviation
    30   eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50) where
    31   "s -e>> t == eta^** s t"
    32 
    33 abbreviation
    34   eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50) where
    35   "s -e>= t == eta^== s t"
    36 
    37 notation (xsymbols)
    38   eta_reds  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>*" 50) and
    39   eta_red0  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>=" 50)
    40 
    41 inductive_cases eta_cases [elim!]:
    42   "Abs s \<rightarrow>\<^sub>\<eta> z"
    43   "s \<degree> t \<rightarrow>\<^sub>\<eta> u"
    44   "Var i \<rightarrow>\<^sub>\<eta> t"
    45 
    46 
    47 subsection {* Properties of @{text "eta"}, @{text "subst"} and @{text "free"} *}
    48 
    49 lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
    50   by (induct s arbitrary: i t u) (simp_all add: subst_Var)
    51 
    52 lemma free_lift [simp]:
    53     "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
    54   apply (induct t arbitrary: i k)
    55   apply (auto cong: conj_cong)
    56   done
    57 
    58 lemma free_subst [simp]:
    59     "free (s[t/k]) i =
    60       (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
    61   apply (induct s arbitrary: i k t)
    62     prefer 2
    63     apply simp
    64     apply blast
    65    prefer 2
    66    apply simp
    67   apply (simp add: diff_Suc subst_Var split: nat.split)
    68   done
    69 
    70 lemma free_eta: "s \<rightarrow>\<^sub>\<eta> t ==> free t i = free s i"
    71   by (induct arbitrary: i set: eta) (simp_all cong: conj_cong)
    72 
    73 lemma not_free_eta:
    74     "[| s \<rightarrow>\<^sub>\<eta> t; \<not> free s i |] ==> \<not> free t i"
    75   by (simp add: free_eta)
    76 
    77 lemma eta_subst [simp]:
    78     "s \<rightarrow>\<^sub>\<eta> t ==> s[u/i] \<rightarrow>\<^sub>\<eta> t[u/i]"
    79   by (induct arbitrary: u i set: eta) (simp_all add: subst_subst [symmetric])
    80 
    81 theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
    82   by (induct s arbitrary: i dummy) simp_all
    83 
    84 
    85 subsection {* Confluence of @{text "eta"} *}
    86 
    87 lemma square_eta: "square eta eta (eta^==) (eta^==)"
    88   apply (unfold square_def id_def)
    89   apply (rule impI [THEN allI [THEN allI]])
    90   apply simp
    91   apply (erule eta.induct)
    92      apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
    93     apply safe
    94        prefer 5
    95        apply (blast intro!: eta_subst intro: free_eta [THEN iffD1])
    96       apply blast+
    97   done
    98 
    99 theorem eta_confluent: "confluent eta"
   100   apply (rule square_eta [THEN square_reflcl_confluent])
   101   done
   102 
   103 
   104 subsection {* Congruence rules for @{text "eta\<^sup>*"} *}
   105 
   106 lemma rtrancl_eta_Abs: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<eta>\<^sup>* Abs s'"
   107   by (induct set: rtranclp)
   108     (blast intro: rtranclp.rtrancl_into_rtrancl)+
   109 
   110 lemma rtrancl_eta_AppL: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t"
   111   by (induct set: rtranclp)
   112     (blast intro: rtranclp.rtrancl_into_rtrancl)+
   113 
   114 lemma rtrancl_eta_AppR: "t \<rightarrow>\<^sub>\<eta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s \<degree> t'"
   115   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
   116 
   117 lemma rtrancl_eta_App:
   118     "[| s \<rightarrow>\<^sub>\<eta>\<^sup>* s'; t \<rightarrow>\<^sub>\<eta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t'"
   119   by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtranclp_trans)
   120 
   121 
   122 subsection {* Commutation of @{text "beta"} and @{text "eta"} *}
   123 
   124 lemma free_beta:
   125     "s \<rightarrow>\<^sub>\<beta> t ==> free t i \<Longrightarrow> free s i"
   126   by (induct arbitrary: i set: beta) auto
   127 
   128 lemma beta_subst [intro]: "s \<rightarrow>\<^sub>\<beta> t ==> s[u/i] \<rightarrow>\<^sub>\<beta> t[u/i]"
   129   by (induct arbitrary: u i set: beta) (simp_all add: subst_subst [symmetric])
   130 
   131 lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
   132   by (induct t arbitrary: i) (auto elim!: linorder_neqE simp: subst_Var)
   133 
   134 lemma eta_lift [simp]: "s \<rightarrow>\<^sub>\<eta> t ==> lift s i \<rightarrow>\<^sub>\<eta> lift t i"
   135   by (induct arbitrary: i set: eta) simp_all
   136 
   137 lemma rtrancl_eta_subst: "s \<rightarrow>\<^sub>\<eta> t \<Longrightarrow> u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]"
   138   apply (induct u arbitrary: s t i)
   139     apply (simp_all add: subst_Var)
   140     apply blast
   141    apply (blast intro: rtrancl_eta_App)
   142   apply (blast intro!: rtrancl_eta_Abs eta_lift)
   143   done
   144 
   145 lemma rtrancl_eta_subst':
   146   fixes s t :: dB
   147   assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
   148   shows "s[u/i] \<rightarrow>\<^sub>\<eta>\<^sup>* t[u/i]" using eta
   149   by induct (iprover intro: eta_subst)+
   150 
   151 lemma rtrancl_eta_subst'':
   152   fixes s t :: dB
   153   assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
   154   shows "u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" using eta
   155   by induct (iprover intro: rtrancl_eta_subst rtranclp_trans)+
   156 
   157 lemma square_beta_eta: "square beta eta (eta^**) (beta^==)"
   158   apply (unfold square_def)
   159   apply (rule impI [THEN allI [THEN allI]])
   160   apply (erule beta.induct)
   161      apply (slowsimp intro: rtrancl_eta_subst eta_subst)
   162     apply (blast intro: rtrancl_eta_AppL)
   163    apply (blast intro: rtrancl_eta_AppR)
   164   apply simp;
   165   apply (slowsimp intro: rtrancl_eta_Abs free_beta
   166     iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
   167   done
   168 
   169 lemma confluent_beta_eta: "confluent (sup beta eta)"
   170   apply (assumption |
   171     rule square_rtrancl_reflcl_commute confluent_Un
   172       beta_confluent eta_confluent square_beta_eta)+
   173   done
   174 
   175 
   176 subsection {* Implicit definition of @{text "eta"} *}
   177 
   178 text {* @{term "Abs (lift s 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s"} *}
   179 
   180 lemma not_free_iff_lifted:
   181     "(\<not> free s i) = (\<exists>t. s = lift t i)"
   182   apply (induct s arbitrary: i)
   183     apply simp
   184     apply (rule iffI)
   185      apply (erule linorder_neqE)
   186       apply (rule_tac x = "Var nat" in exI)
   187       apply simp
   188      apply (rule_tac x = "Var (nat - 1)" in exI)
   189      apply simp
   190     apply clarify
   191     apply (rule notE)
   192      prefer 2
   193      apply assumption
   194     apply (erule thin_rl)
   195     apply (case_tac t)
   196       apply simp
   197      apply simp
   198     apply simp
   199    apply simp
   200    apply (erule thin_rl)
   201    apply (erule thin_rl)
   202    apply (rule iffI)
   203     apply (elim conjE exE)
   204     apply (rename_tac u1 u2)
   205     apply (rule_tac x = "u1 \<degree> u2" in exI)
   206     apply simp
   207    apply (erule exE)
   208    apply (erule rev_mp)
   209    apply (case_tac t)
   210      apply simp
   211     apply simp
   212     apply blast
   213    apply simp
   214   apply simp
   215   apply (erule thin_rl)
   216   apply (rule iffI)
   217    apply (erule exE)
   218    apply (rule_tac x = "Abs t" in exI)
   219    apply simp
   220   apply (erule exE)
   221   apply (erule rev_mp)
   222   apply (case_tac t)
   223     apply simp
   224    apply simp
   225   apply simp
   226   apply blast
   227   done
   228 
   229 theorem explicit_is_implicit:
   230   "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
   231     (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
   232   by (auto simp add: not_free_iff_lifted)
   233 
   234 
   235 subsection {* Eta-postponement theorem *}
   236 
   237 text {*
   238   Based on a paper proof due to Andreas Abel.
   239   Unlike the proof by Masako Takahashi \cite{Takahashi-IandC}, it does not
   240   use parallel eta reduction, which only seems to complicate matters unnecessarily.
   241 *}
   242 
   243 theorem eta_case:
   244   fixes s :: dB
   245   assumes free: "\<not> free s 0"
   246   and s: "s[dummy/0] => u"
   247   shows "\<exists>t'. Abs (s \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u"
   248 proof -
   249   from s have "lift (s[dummy/0]) 0 => lift u 0" by (simp del: lift_subst)
   250   with free have "s => lift u 0" by (simp add: lift_subst_dummy del: lift_subst)
   251   hence "Abs (s \<degree> Var 0) => Abs (lift u 0 \<degree> Var 0)" by simp
   252   moreover have "\<not> free (lift u 0) 0" by simp
   253   hence "Abs (lift u 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> lift u 0[dummy/0]"
   254     by (rule eta.eta)
   255   hence "Abs (lift u 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta>\<^sup>* u" by simp
   256   ultimately show ?thesis by iprover
   257 qed
   258 
   259 theorem eta_par_beta:
   260   assumes st: "s \<rightarrow>\<^sub>\<eta> t"
   261   and tu: "t => u"
   262   shows "\<exists>t'. s => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" using tu st
   263 proof (induct arbitrary: s)
   264   case (var n)
   265   thus ?case by (iprover intro: par_beta_refl)
   266 next
   267   case (abs s' t)
   268   note abs' = this
   269   from `s \<rightarrow>\<^sub>\<eta> Abs s'` show ?case
   270   proof cases
   271     case (eta s'' dummy)
   272     from abs have "Abs s' => Abs t" by simp
   273     with eta have "s''[dummy/0] => Abs t" by simp
   274     with `\<not> free s'' 0` have "\<exists>t'. Abs (s'' \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t"
   275       by (rule eta_case)
   276     with eta show ?thesis by simp
   277   next
   278     case (abs r u)
   279     hence "r \<rightarrow>\<^sub>\<eta> s'" by simp
   280     then obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs')
   281     from r have "Abs r => Abs t'" ..
   282     moreover from t' have "Abs t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" by (rule rtrancl_eta_Abs)
   283     ultimately show ?thesis using abs by simp iprover
   284   qed simp_all
   285 next
   286   case (app u u' t t')
   287   from `s \<rightarrow>\<^sub>\<eta> u \<degree> t` show ?case
   288   proof cases
   289     case (eta s' dummy)
   290     from app have "u \<degree> t => u' \<degree> t'" by simp
   291     with eta have "s'[dummy/0] => u' \<degree> t'" by simp
   292     with `\<not> free s' 0` have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'"
   293       by (rule eta_case)
   294     with eta show ?thesis by simp
   295   next
   296     case (appL s' t'' u'')
   297     hence "s' \<rightarrow>\<^sub>\<eta> u" by simp
   298     then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app)
   299     from s' and app have "s' \<degree> t => r \<degree> t'" by simp
   300     moreover from r have "r \<degree> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppL)
   301     ultimately show ?thesis using appL by simp iprover
   302   next
   303     case (appR s' t'' u'')
   304     hence "s' \<rightarrow>\<^sub>\<eta> t" by simp
   305     then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app)
   306     from s' and app have "u \<degree> s' => u' \<degree> r" by simp
   307     moreover from r have "u' \<degree> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppR)
   308     ultimately show ?thesis using appR by simp iprover
   309   qed simp
   310 next
   311   case (beta u u' t t')
   312   from `s \<rightarrow>\<^sub>\<eta> Abs u \<degree> t` show ?case
   313   proof cases
   314     case (eta s' dummy)
   315     from beta have "Abs u \<degree> t => u'[t'/0]" by simp
   316     with eta have "s'[dummy/0] => u'[t'/0]" by simp
   317     with `\<not> free s' 0` have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
   318       by (rule eta_case)
   319     with eta show ?thesis by simp
   320   next
   321     case (appL s' t'' u'')
   322     hence "s' \<rightarrow>\<^sub>\<eta> Abs u" by simp
   323     thus ?thesis
   324     proof cases
   325       case (eta s'' dummy)
   326       have "Abs (lift u 1) = lift (Abs u) 0" by simp
   327       also from eta have "\<dots> = s''" by (simp add: lift_subst_dummy del: lift_subst)
   328       finally have s: "s = Abs (Abs (lift u 1) \<degree> Var 0) \<degree> t" using appL and eta by simp
   329       from beta have "lift u 1 => lift u' 1" by simp
   330       hence "Abs (lift u 1) \<degree> Var 0 => lift u' 1[Var 0/0]"
   331         using par_beta.var ..
   332       hence "Abs (Abs (lift u 1) \<degree> Var 0) \<degree> t => lift u' 1[Var 0/0][t'/0]"
   333         using `t => t'` ..
   334       with s have "s => u'[t'/0]" by simp
   335       thus ?thesis by iprover
   336     next
   337       case (abs r r')
   338       hence "r \<rightarrow>\<^sub>\<eta> u" by simp
   339       then obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta)
   340       from r and beta have "Abs r \<degree> t => r''[t'/0]" by simp
   341       moreover from r'' have "r''[t'/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
   342         by (rule rtrancl_eta_subst')
   343       ultimately show ?thesis using abs and appL by simp iprover
   344     qed simp_all
   345   next
   346     case (appR s' t'' u'')
   347     hence "s' \<rightarrow>\<^sub>\<eta> t" by simp
   348     then obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta)
   349     from s' and beta have "Abs u \<degree> s' => u'[r/0]" by simp
   350     moreover from r have "u'[r/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
   351       by (rule rtrancl_eta_subst'')
   352     ultimately show ?thesis using appR by simp iprover
   353   qed simp
   354 qed
   355 
   356 theorem eta_postponement':
   357   assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t" and beta: "t => u"
   358   shows "\<exists>t'. s => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" using eta beta
   359 proof (induct arbitrary: u)
   360   case base
   361   thus ?case by blast
   362 next
   363   case (step s' s'' s''')
   364   then obtain t' where s': "s' => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''"
   365     by (auto dest: eta_par_beta)
   366   from s' obtain t'' where s: "s => t''" and t'': "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* t'" using step
   367     by blast
   368   from t'' and t' have "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" by (rule rtranclp_trans)
   369   with s show ?case by iprover
   370 qed
   371 
   372 theorem eta_postponement:
   373   assumes "(sup beta eta)\<^sup>*\<^sup>* s t"
   374   shows "(beta\<^sup>*\<^sup>* OO eta\<^sup>*\<^sup>*) s t" using assms
   375 proof induct
   376   case base
   377   show ?case by blast
   378 next
   379   case (step s' s'')
   380   from step(3) obtain t' where s: "s \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s'" by blast
   381   from step(2) show ?case
   382   proof
   383     assume "s' \<rightarrow>\<^sub>\<beta> s''"
   384     with beta_subset_par_beta have "s' => s''" ..
   385     with t' obtain t'' where st: "t' => t''" and tu: "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s''"
   386       by (auto dest: eta_postponement')
   387     from par_beta_subset_beta st have "t' \<rightarrow>\<^sub>\<beta>\<^sup>* t''" ..
   388     with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtranclp_trans)
   389     thus ?thesis using tu ..
   390   next
   391     assume "s' \<rightarrow>\<^sub>\<eta> s''"
   392     with t' have "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s''" ..
   393     with s show ?thesis ..
   394   qed
   395 qed
   396 
   397 end