src/HOL/Lambda/Eta.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 11183 0476c6e07bca
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 (*  Title:      HOL/Lambda/Eta.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995 TU Muenchen
     5 *)
     6 
     7 header {* Eta-reduction *}
     8 
     9 theory Eta = ParRed:
    10 
    11 
    12 subsection {* Definition of eta-reduction and relatives *}
    13 
    14 consts
    15   free :: "dB => nat => bool"
    16 primrec
    17   "free (Var j) i = (j = i)"
    18   "free (s $ t) i = (free s i \<or> free t i)"
    19   "free (Abs s) i = free s (i + 1)"
    20 
    21 consts
    22   eta :: "(dB \<times> dB) set"
    23 
    24 syntax 
    25   "_eta" :: "[dB, dB] => bool"   (infixl "-e>" 50)
    26   "_eta_rtrancl" :: "[dB, dB] => bool"   (infixl "-e>>" 50)
    27   "_eta_reflcl" :: "[dB, dB] => bool"   (infixl "-e>=" 50)
    28 translations
    29   "s -e> t" == "(s, t) \<in> eta"
    30   "s -e>> t" == "(s, t) \<in> eta^*"
    31   "s -e>= t" == "(s, t) \<in> eta^="
    32 
    33 inductive eta
    34   intros [simp, intro]
    35     eta: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
    36     appL: "s -e> t ==> s $ u -e> t $ u"
    37     appR: "s -e> t ==> u $ s -e> u $ t"
    38     abs: "s -e> t ==> Abs s -e> Abs t"
    39 
    40 inductive_cases eta_cases [elim!]:
    41   "Abs s -e> z"
    42   "s $ t -e> u"
    43   "Var i -e> t"
    44 
    45 
    46 subsection "Properties of eta, subst and free"
    47 
    48 lemma subst_not_free [rule_format, simp]:
    49     "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
    50   apply (induct_tac s)
    51     apply (simp_all add: subst_Var)
    52   done
    53 
    54 lemma free_lift [simp]:
    55     "\<forall>i k. free (lift t k) i =
    56       (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
    57   apply (induct_tac t)
    58     apply (auto cong: conj_cong)
    59   apply arith
    60   done
    61 
    62 lemma free_subst [simp]:
    63     "\<forall>i k t. free (s[t/k]) i =
    64       (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
    65   apply (induct_tac s)
    66     prefer 2
    67     apply simp
    68     apply blast
    69    prefer 2
    70    apply simp
    71   apply (simp add: diff_Suc subst_Var split: nat.split)
    72   apply clarify
    73   apply (erule linorder_neqE)
    74   apply simp_all
    75   done
    76 
    77 lemma free_eta [rule_format]:
    78     "s -e> t ==> \<forall>i. free t i = free s i"
    79   apply (erule eta.induct)
    80      apply (simp_all cong: conj_cong)
    81   done
    82 
    83 lemma not_free_eta:
    84     "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
    85   apply (simp add: free_eta)
    86   done
    87 
    88 lemma eta_subst [rule_format, simp]:
    89     "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
    90   apply (erule eta.induct)
    91   apply (simp_all add: subst_subst [symmetric])
    92   done
    93 
    94 
    95 subsection "Confluence of eta"
    96 
    97 lemma square_eta: "square eta eta (eta^=) (eta^=)"
    98   apply (unfold square_def id_def)
    99   apply (rule impI [THEN allI [THEN allI]])
   100   apply simp
   101   apply (erule eta.induct)
   102      apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
   103     apply safe
   104        prefer 5
   105        apply (blast intro!: eta_subst intro: free_eta [THEN iffD1])
   106       apply blast+
   107   done
   108 
   109 theorem eta_confluent: "confluent eta"
   110   apply (rule square_eta [THEN square_reflcl_confluent])
   111   done
   112 
   113 
   114 subsection "Congruence rules for eta*"
   115 
   116 lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
   117   apply (erule rtrancl_induct)
   118    apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   119   done
   120 
   121 lemma rtrancl_eta_AppL: "s -e>> s' ==> s $ t -e>> s' $ t"
   122   apply (erule rtrancl_induct)
   123    apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   124   done
   125 
   126 lemma rtrancl_eta_AppR: "t -e>> t' ==> s $ t -e>> s $ t'"
   127   apply (erule rtrancl_induct)
   128    apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   129   done
   130 
   131 lemma rtrancl_eta_App:
   132     "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'"
   133   apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
   134   done
   135 
   136 
   137 subsection "Commutation of beta and eta"
   138 
   139 lemma free_beta [rule_format]:
   140     "s -> t ==> \<forall>i. free t i --> free s i"
   141   apply (erule beta.induct)
   142      apply simp_all
   143   done
   144 
   145 lemma beta_subst [rule_format, intro]:
   146     "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
   147   apply (erule beta.induct)
   148      apply (simp_all add: subst_subst [symmetric])
   149   done
   150 
   151 lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]"
   152   apply (induct_tac t)
   153   apply (auto elim!: linorder_neqE simp: subst_Var)
   154   done
   155 
   156 lemma eta_lift [rule_format, simp]:
   157     "s -e> t ==> \<forall>i. lift s i -e> lift t i"
   158   apply (erule eta.induct)
   159      apply simp_all
   160   done
   161 
   162 lemma rtrancl_eta_subst [rule_format]:
   163     "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
   164   apply (induct_tac u)
   165     apply (simp_all add: subst_Var)
   166     apply (blast intro: r_into_rtrancl)
   167    apply (blast intro: rtrancl_eta_App)
   168   apply (blast intro!: rtrancl_eta_Abs eta_lift)
   169   done
   170 
   171 lemma square_beta_eta: "square beta eta (eta^*) (beta^=)"
   172   apply (unfold square_def)
   173   apply (rule impI [THEN allI [THEN allI]])
   174   apply (erule beta.induct)
   175      apply (slowsimp intro: r_into_rtrancl rtrancl_eta_subst eta_subst)
   176     apply (blast intro: r_into_rtrancl rtrancl_eta_AppL)
   177    apply (blast intro: r_into_rtrancl rtrancl_eta_AppR)
   178   apply (slowsimp intro: r_into_rtrancl rtrancl_eta_Abs free_beta
   179     iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
   180   done
   181 
   182 lemma confluent_beta_eta: "confluent (beta \<union> eta)"
   183   apply (assumption |
   184     rule square_rtrancl_reflcl_commute confluent_Un
   185       beta_confluent eta_confluent square_beta_eta)+
   186   done
   187 
   188 
   189 subsection "Implicit definition of eta"
   190 
   191 text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
   192 
   193 lemma not_free_iff_lifted [rule_format]:
   194     "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
   195   apply (induct_tac s)
   196     apply simp
   197     apply clarify
   198     apply (rule iffI)
   199      apply (erule linorder_neqE)
   200       apply (rule_tac x = "Var nat" in exI)
   201       apply simp
   202      apply (rule_tac x = "Var (nat - 1)" in exI)
   203      apply simp
   204     apply clarify
   205     apply (rule notE)
   206      prefer 2
   207      apply assumption
   208     apply (erule thin_rl)
   209     apply (case_tac t)
   210       apply simp
   211      apply simp
   212     apply simp
   213    apply simp
   214    apply (erule thin_rl)
   215    apply (erule thin_rl)
   216    apply (rule allI)
   217    apply (rule iffI)
   218     apply (elim conjE exE)
   219     apply (rename_tac u1 u2)
   220     apply (rule_tac x = "u1 $ u2" in exI)
   221     apply simp
   222    apply (erule exE)
   223    apply (erule rev_mp)
   224    apply (case_tac t)
   225      apply simp
   226     apply simp
   227     apply blast
   228    apply simp
   229   apply simp
   230   apply (erule thin_rl)
   231   apply (rule allI)
   232   apply (rule iffI)
   233    apply (erule exE)
   234    apply (rule_tac x = "Abs t" in exI)
   235    apply simp
   236   apply (erule exE)
   237   apply (erule rev_mp)
   238   apply (case_tac t)
   239     apply simp
   240    apply simp
   241   apply simp
   242   apply blast
   243   done
   244 
   245 theorem explicit_is_implicit:
   246   "(\<forall>s u. (\<not> free s 0) --> R (Abs (s $ Var 0)) (s[u/0])) =
   247     (\<forall>s. R (Abs (lift s 0 $ Var 0)) s)"
   248   apply (auto simp add: not_free_iff_lifted)
   249   done
   250 
   251 end