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