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