src/HOL/Lambda/Eta.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 20217 25b068a99d2b
child 20503 503ac4c5ef91
permissions -rw-r--r--
simplified code generator setup
nipkow@1269
     1
(*  Title:      HOL/Lambda/Eta.thy
nipkow@1269
     2
    ID:         $Id$
berghofe@15522
     3
    Author:     Tobias Nipkow and Stefan Berghofer
berghofe@15522
     4
    Copyright   1995, 2005 TU Muenchen
nipkow@1269
     5
*)
nipkow@1269
     6
wenzelm@9811
     7
header {* Eta-reduction *}
wenzelm@9811
     8
haftmann@16417
     9
theory Eta imports ParRed begin
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@12011
    18
  "free (s \<degree> 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@19363
    24
abbreviation
wenzelm@19086
    25
  eta_red :: "[dB, dB] => bool"   (infixl "-e>" 50)
wenzelm@19363
    26
  "s -e> t == (s, t) \<in> eta"
wenzelm@19086
    27
  eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50)
wenzelm@19363
    28
  "s -e>> t == (s, t) \<in> eta^*"
wenzelm@19086
    29
  eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50)
wenzelm@19363
    30
  "s -e>= t == (s, t) \<in> eta^="
nipkow@1269
    31
paulson@1789
    32
inductive eta
wenzelm@11638
    33
  intros
wenzelm@12011
    34
    eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) -e> s[dummy/0]"
wenzelm@12011
    35
    appL [simp, intro]: "s -e> t ==> s \<degree> u -e> t \<degree> u"
wenzelm@12011
    36
    appR [simp, intro]: "s -e> t ==> u \<degree> s -e> u \<degree> t"
wenzelm@11638
    37
    abs [simp, intro]: "s -e> t ==> Abs s -e> Abs t"
wenzelm@9811
    38
wenzelm@9811
    39
inductive_cases eta_cases [elim!]:
wenzelm@9811
    40
  "Abs s -e> z"
wenzelm@12011
    41
  "s \<degree> t -e> u"
wenzelm@9811
    42
  "Var i -e> t"
wenzelm@9811
    43
wenzelm@9811
    44
wenzelm@9811
    45
subsection "Properties of eta, subst and free"
wenzelm@9811
    46
wenzelm@18241
    47
lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
wenzelm@18241
    48
  by (induct s fixing: i t u) (simp_all add: subst_Var)
wenzelm@9811
    49
wenzelm@9811
    50
lemma free_lift [simp]:
wenzelm@18241
    51
    "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
wenzelm@18241
    52
  apply (induct t fixing: i k)
webertj@20217
    53
  apply (auto cong: conj_cong)
wenzelm@9811
    54
  done
wenzelm@9811
    55
wenzelm@9811
    56
lemma free_subst [simp]:
wenzelm@18241
    57
    "free (s[t/k]) i =
wenzelm@9811
    58
      (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
wenzelm@18241
    59
  apply (induct s fixing: i k t)
wenzelm@9811
    60
    prefer 2
wenzelm@9811
    61
    apply simp
wenzelm@9811
    62
    apply blast
wenzelm@9811
    63
   prefer 2
wenzelm@9811
    64
   apply simp
wenzelm@9811
    65
  apply (simp add: diff_Suc subst_Var split: nat.split)
wenzelm@9811
    66
  done
wenzelm@9811
    67
wenzelm@18257
    68
lemma free_eta: "s -e> t ==> free t i = free s i"
wenzelm@18257
    69
  by (induct fixing: i set: eta) (simp_all cong: conj_cong)
wenzelm@9811
    70
wenzelm@9811
    71
lemma not_free_eta:
wenzelm@9811
    72
    "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
wenzelm@18241
    73
  by (simp add: free_eta)
wenzelm@9811
    74
wenzelm@18241
    75
lemma eta_subst [simp]:
wenzelm@18257
    76
    "s -e> t ==> s[u/i] -e> t[u/i]"
wenzelm@18257
    77
  by (induct fixing: u i set: eta) (simp_all add: subst_subst [symmetric])
wenzelm@9811
    78
wenzelm@18241
    79
theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
wenzelm@18241
    80
  by (induct s fixing: i dummy) simp_all
berghofe@15522
    81
wenzelm@9811
    82
wenzelm@9811
    83
subsection "Confluence of eta"
wenzelm@9811
    84
wenzelm@9811
    85
lemma square_eta: "square eta eta (eta^=) (eta^=)"
wenzelm@9811
    86
  apply (unfold square_def id_def)
wenzelm@9811
    87
  apply (rule impI [THEN allI [THEN allI]])
wenzelm@9811
    88
  apply simp
wenzelm@9811
    89
  apply (erule eta.induct)
wenzelm@9811
    90
     apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
wenzelm@9811
    91
    apply safe
wenzelm@9811
    92
       prefer 5
wenzelm@9811
    93
       apply (blast intro!: eta_subst intro: free_eta [THEN iffD1])
wenzelm@9811
    94
      apply blast+
wenzelm@9811
    95
  done
wenzelm@9811
    96
wenzelm@9811
    97
theorem eta_confluent: "confluent eta"
wenzelm@9811
    98
  apply (rule square_eta [THEN square_reflcl_confluent])
wenzelm@9811
    99
  done
wenzelm@9811
   100
wenzelm@9811
   101
wenzelm@9811
   102
subsection "Congruence rules for eta*"
wenzelm@9811
   103
wenzelm@9811
   104
lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
wenzelm@18241
   105
  by (induct set: rtrancl)
wenzelm@18241
   106
    (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
wenzelm@9811
   107
wenzelm@12011
   108
lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t"
wenzelm@18241
   109
  by (induct set: rtrancl)
wenzelm@18241
   110
    (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
wenzelm@9811
   111
wenzelm@12011
   112
lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'"
wenzelm@18241
   113
  by (induct set: rtrancl) (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
wenzelm@9811
   114
wenzelm@9811
   115
lemma rtrancl_eta_App:
wenzelm@12011
   116
    "[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'"
wenzelm@18241
   117
  by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
wenzelm@9811
   118
wenzelm@9811
   119
wenzelm@9811
   120
subsection "Commutation of beta and eta"
berghofe@1900
   121
wenzelm@18241
   122
lemma free_beta:
wenzelm@18257
   123
    "s -> t ==> free t i \<Longrightarrow> free s i"
wenzelm@18257
   124
  by (induct fixing: i set: beta) auto
wenzelm@9811
   125
wenzelm@18257
   126
lemma beta_subst [intro]: "s -> t ==> s[u/i] -> t[u/i]"
wenzelm@18257
   127
  by (induct fixing: u i set: beta) (simp_all add: subst_subst [symmetric])
wenzelm@9811
   128
wenzelm@18241
   129
lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
wenzelm@18241
   130
  by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
wenzelm@9811
   131
wenzelm@18257
   132
lemma eta_lift [simp]: "s -e> t ==> lift s i -e> lift t i"
wenzelm@18257
   133
  by (induct fixing: i set: eta) simp_all
wenzelm@9811
   134
wenzelm@18241
   135
lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
wenzelm@18241
   136
  apply (induct u fixing: s t i)
wenzelm@9811
   137
    apply (simp_all add: subst_Var)
wenzelm@18241
   138
    apply blast
wenzelm@9811
   139
   apply (blast intro: rtrancl_eta_App)
wenzelm@9811
   140
  apply (blast intro!: rtrancl_eta_Abs eta_lift)
wenzelm@9811
   141
  done
wenzelm@9811
   142
wenzelm@9811
   143
lemma square_beta_eta: "square beta eta (eta^*) (beta^=)"
wenzelm@9811
   144
  apply (unfold square_def)
wenzelm@9811
   145
  apply (rule impI [THEN allI [THEN allI]])
wenzelm@9811
   146
  apply (erule beta.induct)
paulson@11183
   147
     apply (slowsimp intro: rtrancl_eta_subst eta_subst)
paulson@11183
   148
    apply (blast intro: rtrancl_eta_AppL)
paulson@11183
   149
   apply (blast intro: rtrancl_eta_AppR)
paulson@11183
   150
  apply simp;
paulson@11183
   151
  apply (slowsimp intro: rtrancl_eta_Abs free_beta
wenzelm@9858
   152
    iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
wenzelm@9811
   153
  done
wenzelm@9811
   154
wenzelm@9811
   155
lemma confluent_beta_eta: "confluent (beta \<union> eta)"
wenzelm@9811
   156
  apply (assumption |
wenzelm@9811
   157
    rule square_rtrancl_reflcl_commute confluent_Un
wenzelm@9811
   158
      beta_confluent eta_confluent square_beta_eta)+
wenzelm@9811
   159
  done
wenzelm@9811
   160
wenzelm@9811
   161
wenzelm@9811
   162
subsection "Implicit definition of eta"
wenzelm@9811
   163
wenzelm@12011
   164
text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *}
wenzelm@9811
   165
wenzelm@18241
   166
lemma not_free_iff_lifted:
wenzelm@18241
   167
    "(\<not> free s i) = (\<exists>t. s = lift t i)"
wenzelm@18241
   168
  apply (induct s fixing: i)
wenzelm@9811
   169
    apply simp
wenzelm@9811
   170
    apply (rule iffI)
wenzelm@9811
   171
     apply (erule linorder_neqE)
wenzelm@9811
   172
      apply (rule_tac x = "Var nat" in exI)
wenzelm@9811
   173
      apply simp
wenzelm@9811
   174
     apply (rule_tac x = "Var (nat - 1)" in exI)
wenzelm@9811
   175
     apply simp
wenzelm@9811
   176
    apply clarify
wenzelm@9811
   177
    apply (rule notE)
wenzelm@9811
   178
     prefer 2
wenzelm@9811
   179
     apply assumption
wenzelm@9811
   180
    apply (erule thin_rl)
wenzelm@9811
   181
    apply (case_tac t)
wenzelm@9811
   182
      apply simp
wenzelm@9811
   183
     apply simp
wenzelm@9811
   184
    apply simp
wenzelm@9811
   185
   apply simp
wenzelm@9811
   186
   apply (erule thin_rl)
wenzelm@9811
   187
   apply (erule thin_rl)
wenzelm@9811
   188
   apply (rule iffI)
wenzelm@9811
   189
    apply (elim conjE exE)
wenzelm@9811
   190
    apply (rename_tac u1 u2)
wenzelm@12011
   191
    apply (rule_tac x = "u1 \<degree> u2" in exI)
wenzelm@9811
   192
    apply simp
wenzelm@9811
   193
   apply (erule exE)
wenzelm@9811
   194
   apply (erule rev_mp)
wenzelm@9811
   195
   apply (case_tac t)
wenzelm@9811
   196
     apply simp
wenzelm@9811
   197
    apply simp
wenzelm@9811
   198
    apply blast
wenzelm@9811
   199
   apply simp
wenzelm@9811
   200
  apply simp
wenzelm@9811
   201
  apply (erule thin_rl)
wenzelm@9811
   202
  apply (rule iffI)
wenzelm@9811
   203
   apply (erule exE)
wenzelm@9811
   204
   apply (rule_tac x = "Abs t" in exI)
wenzelm@9811
   205
   apply simp
wenzelm@9811
   206
  apply (erule exE)
wenzelm@9811
   207
  apply (erule rev_mp)
wenzelm@9811
   208
  apply (case_tac t)
wenzelm@9811
   209
    apply simp
wenzelm@9811
   210
   apply simp
wenzelm@9811
   211
  apply simp
wenzelm@9811
   212
  apply blast
wenzelm@9811
   213
  done
wenzelm@9811
   214
wenzelm@9811
   215
theorem explicit_is_implicit:
wenzelm@12011
   216
  "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
wenzelm@12011
   217
    (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
wenzelm@18241
   218
  by (auto simp add: not_free_iff_lifted)
wenzelm@9811
   219
berghofe@15522
   220
berghofe@15522
   221
subsection {* Parallel eta-reduction *}
berghofe@15522
   222
berghofe@15522
   223
consts
berghofe@15522
   224
  par_eta :: "(dB \<times> dB) set"
berghofe@15522
   225
wenzelm@19363
   226
abbreviation
wenzelm@19086
   227
  par_eta_red :: "[dB, dB] => bool"   (infixl "=e>" 50)
wenzelm@19363
   228
  "s =e> t == (s, t) \<in> par_eta"
berghofe@15522
   229
wenzelm@19656
   230
const_syntax (xsymbols)
wenzelm@19656
   231
  par_eta_red  (infixl "\<Rightarrow>\<^sub>\<eta>" 50)
berghofe@15522
   232
berghofe@15522
   233
inductive par_eta
berghofe@15522
   234
intros
berghofe@15522
   235
  var [simp, intro]: "Var x \<Rightarrow>\<^sub>\<eta> Var x"
berghofe@15522
   236
  eta [simp, intro]: "\<not> free s 0 \<Longrightarrow> s \<Rightarrow>\<^sub>\<eta> s'\<Longrightarrow> Abs (s \<degree> Var 0) \<Rightarrow>\<^sub>\<eta> s'[dummy/0]"
berghofe@15522
   237
  app [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> s' \<Longrightarrow> t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> s \<degree> t \<Rightarrow>\<^sub>\<eta> s' \<degree> t'"
berghofe@15522
   238
  abs [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> Abs s \<Rightarrow>\<^sub>\<eta> Abs t"
berghofe@15522
   239
wenzelm@18241
   240
lemma free_par_eta [simp]:
wenzelm@18241
   241
  assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
wenzelm@18241
   242
  shows "free t i = free s i" using eta
wenzelm@18241
   243
  by (induct fixing: i) (simp_all cong: conj_cong)
berghofe@15522
   244
berghofe@15522
   245
lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t"
berghofe@15522
   246
  by (induct t) simp_all
berghofe@15522
   247
berghofe@15522
   248
lemma par_eta_lift [simp]:
berghofe@15522
   249
  assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
wenzelm@18241
   250
  shows "lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
wenzelm@18241
   251
  by (induct fixing: i) simp_all
berghofe@15522
   252
berghofe@15522
   253
lemma par_eta_subst [simp]:
berghofe@15522
   254
  assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
wenzelm@18241
   255
  shows "u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
wenzelm@18241
   256
  by (induct fixing: u u' i) (simp_all add: subst_subst [symmetric] subst_Var)
berghofe@15522
   257
berghofe@15522
   258
theorem eta_subset_par_eta: "eta \<subseteq> par_eta"
berghofe@15522
   259
  apply (rule subsetI)
berghofe@15522
   260
  apply clarify
berghofe@15522
   261
  apply (erule eta.induct)
berghofe@15522
   262
  apply (blast intro!: par_eta_refl)+
berghofe@15522
   263
  done
berghofe@15522
   264
berghofe@15522
   265
theorem par_eta_subset_eta: "par_eta \<subseteq> eta\<^sup>*"
berghofe@15522
   266
  apply (rule subsetI)
berghofe@15522
   267
  apply clarify
berghofe@15522
   268
  apply (erule par_eta.induct)
berghofe@15522
   269
  apply blast
berghofe@15522
   270
  apply (rule rtrancl_into_rtrancl)
berghofe@15522
   271
  apply (rule rtrancl_eta_Abs)
berghofe@15522
   272
  apply (rule rtrancl_eta_AppL)
berghofe@15522
   273
  apply assumption
berghofe@15522
   274
  apply (rule eta.eta)
berghofe@15522
   275
  apply simp
berghofe@15522
   276
  apply (rule rtrancl_eta_App)
berghofe@15522
   277
  apply assumption+
berghofe@15522
   278
  apply (rule rtrancl_eta_Abs)
berghofe@15522
   279
  apply assumption
berghofe@15522
   280
  done
berghofe@15522
   281
berghofe@15522
   282
berghofe@15522
   283
subsection {* n-ary eta-expansion *}
berghofe@15522
   284
berghofe@15522
   285
consts eta_expand :: "nat \<Rightarrow> dB \<Rightarrow> dB"
berghofe@15522
   286
primrec
berghofe@15522
   287
  eta_expand_0: "eta_expand 0 t = t"
berghofe@15522
   288
  eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 \<degree> Var 0)"
berghofe@15522
   289
berghofe@15522
   290
lemma eta_expand_Suc':
wenzelm@18241
   291
  "eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
wenzelm@18241
   292
  by (induct n fixing: t) simp_all
berghofe@15522
   293
berghofe@15522
   294
theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)"
berghofe@15522
   295
  by (induct k) (simp_all add: lift_lift)
berghofe@15522
   296
berghofe@15522
   297
theorem eta_expand_beta:
berghofe@15522
   298
  assumes u: "u => u'"
wenzelm@18241
   299
  shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
wenzelm@18241
   300
proof (induct k fixing: t t')
wenzelm@19656
   301
  case 0
wenzelm@19656
   302
  with u show ?case by simp
berghofe@15522
   303
next
berghofe@15522
   304
  case (Suc k)
berghofe@15522
   305
  hence "Abs (lift t (Suc 0)) \<degree> Var 0 => lift t' (Suc 0)[Var 0/0]"
berghofe@15522
   306
    by (blast intro: par_beta_lift)
berghofe@15522
   307
  with Suc show ?case by (simp del: eta_expand_Suc add: eta_expand_Suc')
berghofe@15522
   308
qed
berghofe@15522
   309
berghofe@15522
   310
theorem eta_expand_red:
berghofe@15522
   311
  assumes t: "t => t'"
berghofe@15522
   312
  shows "eta_expand k t => eta_expand k t'"
berghofe@15522
   313
  by (induct k) (simp_all add: t)
berghofe@15522
   314
wenzelm@18241
   315
theorem eta_expand_eta: "t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
wenzelm@18241
   316
proof (induct k fixing: t t')
berghofe@15522
   317
  case 0
berghofe@15522
   318
  show ?case by simp
berghofe@15522
   319
next
berghofe@15522
   320
  case (Suc k)
berghofe@15522
   321
  have "Abs (lift (eta_expand k t) 0 \<degree> Var 0) \<Rightarrow>\<^sub>\<eta> lift t' 0[arbitrary/0]"
berghofe@15522
   322
    by (fastsimp intro: par_eta_lift Suc)
berghofe@15522
   323
  thus ?case by simp
berghofe@15522
   324
qed
berghofe@15522
   325
berghofe@15522
   326
berghofe@15522
   327
subsection {* Elimination rules for parallel eta reduction *}
berghofe@15522
   328
berghofe@15522
   329
theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u"
wenzelm@18241
   330
  shows "u = u1' \<degree> u2' \<Longrightarrow>
berghofe@15522
   331
    \<exists>u1 u2 k. t = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2'" using eta
wenzelm@18241
   332
proof (induct fixing: u1' u2')
berghofe@15522
   333
  case (app s s' t t')
berghofe@15522
   334
  have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp
berghofe@15522
   335
  with app show ?case by blast
berghofe@15522
   336
next
berghofe@15522
   337
  case (eta dummy s s')
berghofe@15522
   338
  then obtain u1'' u2'' where s': "s' = u1'' \<degree> u2''"
berghofe@15522
   339
    by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
berghofe@15522
   340
  then have "\<exists>u1 u2 k. s = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1'' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2''" by (rule eta)
berghofe@15522
   341
  then obtain u1 u2 k where s: "s = eta_expand k (u1 \<degree> u2)"
nipkow@17589
   342
    and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by iprover
berghofe@15522
   343
  from u1 u2 eta s' have "\<not> free u1 0" and "\<not> free u2 0"
berghofe@15522
   344
    by (simp_all del: free_par_eta add: free_par_eta [symmetric])
berghofe@15522
   345
  with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (u1[dummy/0] \<degree> u2[dummy/0])"
berghofe@15522
   346
    by (simp del: lift_subst add: lift_subst_dummy lift_eta_expand)
berghofe@15522
   347
  moreover from u1 par_eta_refl have "u1[dummy/0] \<Rightarrow>\<^sub>\<eta> u1''[dummy/0]"
berghofe@15522
   348
    by (rule par_eta_subst)
berghofe@15522
   349
  moreover from u2 par_eta_refl have "u2[dummy/0] \<Rightarrow>\<^sub>\<eta> u2''[dummy/0]"
berghofe@15522
   350
    by (rule par_eta_subst)
berghofe@15522
   351
  ultimately show ?case using eta s'
berghofe@15522
   352
    by (simp only: subst.simps dB.simps) blast
berghofe@15522
   353
next
berghofe@15522
   354
  case var thus ?case by simp
berghofe@15522
   355
next
berghofe@15522
   356
  case abs thus ?case by simp
berghofe@15522
   357
qed
berghofe@15522
   358
berghofe@15522
   359
theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'"
wenzelm@18241
   360
  shows "t' = Abs u' \<Longrightarrow>
berghofe@15522
   361
    \<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta
wenzelm@18241
   362
proof (induct fixing: u')
berghofe@15522
   363
  case (abs s t)
berghofe@15522
   364
  have "Abs s = eta_expand 0 (Abs s)" by simp
berghofe@15522
   365
  with abs show ?case by blast
berghofe@15522
   366
next
berghofe@15522
   367
  case (eta dummy s s')
berghofe@15522
   368
  then obtain u'' where s': "s' = Abs u''"
berghofe@15522
   369
    by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
berghofe@15522
   370
  then have "\<exists>u k. s = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u''" by (rule eta)
nipkow@17589
   371
  then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by iprover
berghofe@15522
   372
  from eta u s' have "\<not> free u (Suc 0)"
berghofe@15522
   373
    by (simp del: free_par_eta add: free_par_eta [symmetric])
berghofe@15522
   374
  with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))"
berghofe@15522
   375
    by (simp del: lift_subst add: lift_eta_expand lift_subst_dummy)
berghofe@15522
   376
  moreover from u par_eta_refl have "u[lift dummy 0/Suc 0] \<Rightarrow>\<^sub>\<eta> u''[lift dummy 0/Suc 0]"
berghofe@15522
   377
    by (rule par_eta_subst)
berghofe@15522
   378
  ultimately show ?case using eta s' by fastsimp
berghofe@15522
   379
next
berghofe@15522
   380
  case var thus ?case by simp
berghofe@15522
   381
next
berghofe@15522
   382
  case app thus ?case by simp
berghofe@15522
   383
qed
berghofe@15522
   384
berghofe@15522
   385
berghofe@15522
   386
subsection {* Eta-postponement theorem *}
berghofe@15522
   387
berghofe@15522
   388
text {*
wenzelm@19656
   389
  Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
berghofe@15522
   390
*}
berghofe@15522
   391
wenzelm@18241
   392
theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
wenzelm@18460
   393
proof (induct t fixing: s u taking: "size :: dB \<Rightarrow> nat" rule: measure_induct_rule)
wenzelm@18460
   394
  case (less t)
wenzelm@18460
   395
  from `t => u`
berghofe@15522
   396
  show ?case
berghofe@15522
   397
  proof cases
berghofe@15522
   398
    case (var n)
wenzelm@18460
   399
    with less show ?thesis
berghofe@15522
   400
      by (auto intro: par_beta_refl)
berghofe@15522
   401
  next
berghofe@15522
   402
    case (abs r' r'')
wenzelm@18460
   403
    with less have "s \<Rightarrow>\<^sub>\<eta> Abs r'" by simp
berghofe@15522
   404
    then obtain r k where s: "s = eta_expand k (Abs r)" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
berghofe@15522
   405
      by (blast dest: par_eta_elim_abs)
berghofe@15522
   406
    from abs have "size r' < size t" by simp
berghofe@15522
   407
    with abs(2) rr obtain t' where rt: "r => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> r''"
paulson@18557
   408
      by (blast dest: less(1))
berghofe@15522
   409
    with s abs show ?thesis
berghofe@15522
   410
      by (auto intro: eta_expand_red eta_expand_eta)
berghofe@15522
   411
  next
berghofe@15522
   412
    case (app q' q'' r' r'')
wenzelm@18460
   413
    with less have "s \<Rightarrow>\<^sub>\<eta> q' \<degree> r'" by simp
berghofe@15522
   414
    then obtain q r k where s: "s = eta_expand k (q \<degree> r)"
berghofe@15522
   415
      and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
berghofe@15522
   416
      by (blast dest: par_eta_elim_app [OF _ refl])
berghofe@15522
   417
    from app have "size q' < size t" and "size r' < size t" by simp_all
berghofe@15522
   418
    with app(2,3) qq rr obtain t' t'' where "q => t'" and
berghofe@15522
   419
      "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
paulson@18557
   420
      by (blast dest: less(1))
berghofe@15522
   421
    with s app show ?thesis
berghofe@15522
   422
      by (fastsimp intro: eta_expand_red eta_expand_eta)
berghofe@15522
   423
  next
berghofe@15522
   424
    case (beta q' q'' r' r'')
wenzelm@18460
   425
    with less have "s \<Rightarrow>\<^sub>\<eta> Abs q' \<degree> r'" by simp
berghofe@15522
   426
    then obtain q r k k' where s: "s = eta_expand k (eta_expand k' (Abs q) \<degree> r)"
berghofe@15522
   427
      and qq: "q \<Rightarrow>\<^sub>\<eta> q'" and rr: "r \<Rightarrow>\<^sub>\<eta> r'"
berghofe@15522
   428
      by (blast dest: par_eta_elim_app par_eta_elim_abs)
berghofe@15522
   429
    from beta have "size q' < size t" and "size r' < size t" by simp_all
wenzelm@19656
   430
    with beta(2-3) qq rr obtain t' t'' where "q => t'" and
berghofe@15522
   431
      "t' \<Rightarrow>\<^sub>\<eta> q''" and "r => t''" and "t'' \<Rightarrow>\<^sub>\<eta> r''"
paulson@18557
   432
      by (blast dest: less(1))
berghofe@15522
   433
    with s beta show ?thesis
berghofe@15522
   434
      by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst)
berghofe@15522
   435
  qed
berghofe@15522
   436
qed
berghofe@15522
   437
berghofe@15522
   438
theorem eta_postponement': assumes eta: "s -e>> t"
wenzelm@18241
   439
  shows "t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
berghofe@15522
   440
  using eta [simplified rtrancl_subset
berghofe@15522
   441
    [OF eta_subset_par_eta par_eta_subset_eta, symmetric]]
wenzelm@18241
   442
proof (induct fixing: u)
berghofe@15522
   443
  case 1
berghofe@15522
   444
  thus ?case by blast
berghofe@15522
   445
next
berghofe@15522
   446
  case (2 s' s'' s''')
berghofe@15522
   447
  from 2 obtain t' where s': "s' => t'" and t': "t' \<Rightarrow>\<^sub>\<eta> s'''"
berghofe@15522
   448
    by (auto dest: par_eta_beta)
paulson@18557
   449
  from s' obtain t'' where s: "s => t''" and t'': "t'' -e>> t'" using 2
paulson@18557
   450
    by blast
berghofe@15522
   451
  from par_eta_subset_eta t' have "t' -e>> s'''" ..
berghofe@15522
   452
  with t'' have "t'' -e>> s'''" by (rule rtrancl_trans)
nipkow@17589
   453
  with s show ?case by iprover
berghofe@15522
   454
qed
berghofe@15522
   455
berghofe@15522
   456
theorem eta_postponement:
berghofe@15522
   457
  assumes st: "(s, t) \<in> (beta \<union> eta)\<^sup>*"
berghofe@15522
   458
  shows "(s, t) \<in> eta\<^sup>* O beta\<^sup>*" using st
berghofe@15522
   459
proof induct
berghofe@15522
   460
  case 1
berghofe@15522
   461
  show ?case by blast
berghofe@15522
   462
next
berghofe@15522
   463
  case (2 s' s'')
berghofe@15522
   464
  from 2(3) obtain t' where s: "s \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and t': "t' -e>> s'" by blast
berghofe@15522
   465
  from 2(2) show ?case
berghofe@15522
   466
  proof
berghofe@15522
   467
    assume "s' -> s''"
berghofe@15522
   468
    with beta_subset_par_beta have "s' => s''" ..
berghofe@15522
   469
    with t' obtain t'' where st: "t' => t''" and tu: "t'' -e>> s''"
berghofe@15522
   470
      by (auto dest: eta_postponement')
berghofe@15522
   471
    from par_beta_subset_beta st have "t' \<rightarrow>\<^sub>\<beta>\<^sup>* t''" ..
berghofe@15522
   472
    with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtrancl_trans)
berghofe@15522
   473
    thus ?thesis using tu ..
berghofe@15522
   474
  next
berghofe@15522
   475
    assume "s' -e> s''"
berghofe@15522
   476
    with t' have "t' -e>> s''" ..
berghofe@15522
   477
    with s show ?thesis ..
berghofe@15522
   478
  qed
berghofe@15522
   479
qed
berghofe@15522
   480
wenzelm@11638
   481
end