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