src/HOL/Proofs/Lambda/Eta.thy
author huffman
Mon, 26 Mar 2012 19:03:27 +0200
changeset 47124 960f0a4404c7
parent 39157 b98909faaea8
child 58273 9f0bfcd15097
permissions -rw-r--r--
remove old-style semicolon
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 34990
diff changeset
     1
(*  Title:      HOL/Proofs/Lambda/Eta.thy
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
     2
    Author:     Tobias Nipkow and Stefan Berghofer
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
     3
    Copyright   1995, 2005 TU Muenchen
1269
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
     4
*)
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
     5
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
     6
header {* Eta-reduction *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15522
diff changeset
     8
theory Eta imports ParRed begin
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
     9
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    10
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    11
subsection {* Definition of eta-reduction and relatives *}
1269
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
    12
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    13
primrec
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    14
  free :: "dB => nat => bool"
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    15
where
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    16
    "free (Var j) i = (j = i)"
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    17
  | "free (s \<degree> t) i = (free s i \<or> free t i)"
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    18
  | "free (Abs s) i = free s (i + 1)"
1269
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
    19
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    20
inductive
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    21
  eta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<eta>" 50)
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    22
where
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    23
    eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s[dummy/0]"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    24
  | appL [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> s \<degree> u \<rightarrow>\<^sub>\<eta> t \<degree> u"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    25
  | appR [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> u \<degree> s \<rightarrow>\<^sub>\<eta> u \<degree> t"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    26
  | abs [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> Abs s \<rightarrow>\<^sub>\<eta> Abs t"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    27
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    28
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    29
  eta_reds :: "[dB, dB] => bool"   (infixl "-e>>" 50) where
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    30
  "s -e>> t == eta^** s t"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    31
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    32
abbreviation
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
    33
  eta_red0 :: "[dB, dB] => bool"   (infixl "-e>=" 50) where
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    34
  "s -e>= t == eta^== s t"
1269
ee011b365770 New version with eta reduction.
nipkow
parents:
diff changeset
    35
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    36
notation (xsymbols)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    37
  eta_reds  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>*" 50) and
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    38
  eta_red0  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>=" 50)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    39
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
    40
inductive_cases eta_cases [elim!]:
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    41
  "Abs s \<rightarrow>\<^sub>\<eta> z"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    42
  "s \<degree> t \<rightarrow>\<^sub>\<eta> u"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    43
  "Var i \<rightarrow>\<^sub>\<eta> t"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    44
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    45
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    46
subsection {* Properties of @{text "eta"}, @{text "subst"} and @{text "free"} *}
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    47
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
    48
lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
    49
  by (induct s arbitrary: i t u) (simp_all add: subst_Var)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    50
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    51
lemma free_lift [simp]:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
    52
    "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
    53
  apply (induct t arbitrary: i k)
20217
25b068a99d2b linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents: 19656
diff changeset
    54
  apply (auto cong: conj_cong)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    55
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    56
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    57
lemma free_subst [simp]:
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
    58
    "free (s[t/k]) i =
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    59
      (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
    60
  apply (induct s arbitrary: i k t)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    61
    prefer 2
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    62
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    63
    apply blast
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    64
   prefer 2
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    65
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    66
  apply (simp add: diff_Suc subst_Var split: nat.split)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    67
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    68
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    69
lemma free_eta: "s \<rightarrow>\<^sub>\<eta> t ==> free t i = free s i"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
    70
  by (induct arbitrary: i set: eta) (simp_all cong: conj_cong)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    71
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    72
lemma not_free_eta:
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    73
    "[| s \<rightarrow>\<^sub>\<eta> t; \<not> free s i |] ==> \<not> free t i"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
    74
  by (simp add: free_eta)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    75
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
    76
lemma eta_subst [simp]:
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    77
    "s \<rightarrow>\<^sub>\<eta> t ==> s[u/i] \<rightarrow>\<^sub>\<eta> t[u/i]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
    78
  by (induct arbitrary: u i set: eta) (simp_all add: subst_subst [symmetric])
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    79
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
    80
theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
    81
  by (induct s arbitrary: i dummy) simp_all
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
    82
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    83
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
    84
subsection {* Confluence of @{text "eta"} *}
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    85
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
    86
lemma square_eta: "square eta eta (eta^==) (eta^==)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    87
  apply (unfold square_def id_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    88
  apply (rule impI [THEN allI [THEN allI]])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    89
  apply (erule eta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    90
     apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    91
    apply safe
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    92
       prefer 5
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    93
       apply (blast intro!: eta_subst intro: free_eta [THEN iffD1])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    94
      apply blast+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    95
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    96
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    97
theorem eta_confluent: "confluent eta"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    98
  apply (rule square_eta [THEN square_reflcl_confluent])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
    99
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   100
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   101
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
   102
subsection {* Congruence rules for @{text "eta\<^sup>*"} *}
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   103
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   104
lemma rtrancl_eta_Abs: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<eta>\<^sup>* Abs s'"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
   105
  by (induct set: rtranclp)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
   106
    (blast intro: rtranclp.rtrancl_into_rtrancl)+
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   107
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   108
lemma rtrancl_eta_AppL: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
   109
  by (induct set: rtranclp)
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
   110
    (blast intro: rtranclp.rtrancl_into_rtrancl)+
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   111
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   112
lemma rtrancl_eta_AppR: "t \<rightarrow>\<^sub>\<eta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s \<degree> t'"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
   113
  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   114
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   115
lemma rtrancl_eta_App:
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   116
    "[| s \<rightarrow>\<^sub>\<eta>\<^sup>* s'; t \<rightarrow>\<^sub>\<eta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t'"
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
   117
  by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtranclp_trans)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   118
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   119
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
   120
subsection {* Commutation of @{text "beta"} and @{text "eta"} *}
1900
c7a869229091 Simplified primrec definitions.
berghofe
parents: 1789
diff changeset
   121
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
   122
lemma free_beta:
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   123
    "s \<rightarrow>\<^sub>\<beta> t ==> free t i \<Longrightarrow> free s i"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
   124
  by (induct arbitrary: i set: beta) auto
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   125
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   126
lemma beta_subst [intro]: "s \<rightarrow>\<^sub>\<beta> t ==> s[u/i] \<rightarrow>\<^sub>\<beta> t[u/i]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
   127
  by (induct arbitrary: u i set: beta) (simp_all add: subst_subst [symmetric])
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   128
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
   129
lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
   130
  by (induct t arbitrary: i) (auto elim!: linorder_neqE simp: subst_Var)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   131
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   132
lemma eta_lift [simp]: "s \<rightarrow>\<^sub>\<eta> t ==> lift s i \<rightarrow>\<^sub>\<eta> lift t i"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
   133
  by (induct arbitrary: i set: eta) simp_all
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   134
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   135
lemma rtrancl_eta_subst: "s \<rightarrow>\<^sub>\<eta> t \<Longrightarrow> u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
   136
  apply (induct u arbitrary: s t i)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   137
    apply (simp_all add: subst_Var)
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
   138
    apply blast
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   139
   apply (blast intro: rtrancl_eta_App)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   140
  apply (blast intro!: rtrancl_eta_Abs eta_lift)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   141
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   142
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   143
lemma rtrancl_eta_subst':
24231
85fb973a8207 added type constraints to resolve syntax ambiguities;
wenzelm
parents: 23750
diff changeset
   144
  fixes s t :: dB
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   145
  assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   146
  shows "s[u/i] \<rightarrow>\<^sub>\<eta>\<^sup>* t[u/i]" using eta
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   147
  by induct (iprover intro: eta_subst)+
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   148
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   149
lemma rtrancl_eta_subst'':
24231
85fb973a8207 added type constraints to resolve syntax ambiguities;
wenzelm
parents: 23750
diff changeset
   150
  fixes s t :: dB
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   151
  assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   152
  shows "u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" using eta
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
   153
  by induct (iprover intro: rtrancl_eta_subst rtranclp_trans)+
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   154
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   155
lemma square_beta_eta: "square beta eta (eta^**) (beta^==)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   156
  apply (unfold square_def)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   157
  apply (rule impI [THEN allI [THEN allI]])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   158
  apply (erule beta.induct)
11183
0476c6e07bca minor tweaks to speed the proofs
paulson
parents: 9941
diff changeset
   159
     apply (slowsimp intro: rtrancl_eta_subst eta_subst)
0476c6e07bca minor tweaks to speed the proofs
paulson
parents: 9941
diff changeset
   160
    apply (blast intro: rtrancl_eta_AppL)
0476c6e07bca minor tweaks to speed the proofs
paulson
parents: 9941
diff changeset
   161
   apply (blast intro: rtrancl_eta_AppR)
47124
960f0a4404c7 remove old-style semicolon
huffman
parents: 39157
diff changeset
   162
  apply simp
11183
0476c6e07bca minor tweaks to speed the proofs
paulson
parents: 9941
diff changeset
   163
  apply (slowsimp intro: rtrancl_eta_Abs free_beta
9858
c3ac6128b649 use 'iff' modifier;
wenzelm
parents: 9827
diff changeset
   164
    iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   165
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   166
22422
ee19cdb07528 stepping towards uniform lattice theory development in HOL
haftmann
parents: 22272
diff changeset
   167
lemma confluent_beta_eta: "confluent (sup beta eta)"
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   168
  apply (assumption |
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   169
    rule square_rtrancl_reflcl_commute confluent_Un
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   170
      beta_confluent eta_confluent square_beta_eta)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   171
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   172
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   173
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
   174
subsection {* Implicit definition of @{text "eta"} *}
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   175
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   176
text {* @{term "Abs (lift s 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s"} *}
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   177
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
   178
lemma not_free_iff_lifted:
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
   179
    "(\<not> free s i) = (\<exists>t. s = lift t i)"
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
   180
  apply (induct s arbitrary: i)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   181
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   182
    apply (rule iffI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   183
     apply (erule linorder_neqE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   184
      apply (rule_tac x = "Var nat" in exI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   185
      apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   186
     apply (rule_tac x = "Var (nat - 1)" in exI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   187
     apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   188
    apply clarify
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   189
    apply (rule notE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   190
     prefer 2
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   191
     apply assumption
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   192
    apply (erule thin_rl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   193
    apply (case_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   194
      apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   195
     apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   196
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   197
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   198
   apply (erule thin_rl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   199
   apply (erule thin_rl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   200
   apply (rule iffI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   201
    apply (elim conjE exE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   202
    apply (rename_tac u1 u2)
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11638
diff changeset
   203
    apply (rule_tac x = "u1 \<degree> u2" in exI)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   204
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   205
   apply (erule exE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   206
   apply (erule rev_mp)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   207
   apply (case_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   208
     apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   209
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   210
    apply blast
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   211
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   212
  apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   213
  apply (erule thin_rl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   214
  apply (rule iffI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   215
   apply (erule exE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   216
   apply (rule_tac x = "Abs t" in exI)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   217
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   218
  apply (erule exE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   219
  apply (erule rev_mp)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   220
  apply (case_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   221
    apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   222
   apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   223
  apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   224
  apply blast
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   225
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   226
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   227
theorem explicit_is_implicit:
12011
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11638
diff changeset
   228
  "(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
1a3a7b3cd9bb tuned notation (degree instead of dollar);
wenzelm
parents: 11638
diff changeset
   229
    (\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
18241
afdba6b3e383 tuned induction proofs;
wenzelm
parents: 17589
diff changeset
   230
  by (auto simp add: not_free_iff_lifted)
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 9102
diff changeset
   231
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   232
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   233
subsection {* Eta-postponement theorem *}
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   234
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   235
text {*
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   236
  Based on a paper proof due to Andreas Abel.
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   237
  Unlike the proof by Masako Takahashi \cite{Takahashi-IandC}, it does not
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   238
  use parallel eta reduction, which only seems to complicate matters unnecessarily.
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   239
*}
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   240
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   241
theorem eta_case:
24231
85fb973a8207 added type constraints to resolve syntax ambiguities;
wenzelm
parents: 23750
diff changeset
   242
  fixes s :: dB
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   243
  assumes free: "\<not> free s 0"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   244
  and s: "s[dummy/0] => u"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   245
  shows "\<exists>t'. Abs (s \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   246
proof -
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   247
  from s have "lift (s[dummy/0]) 0 => lift u 0" by (simp del: lift_subst)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   248
  with free have "s => lift u 0" by (simp add: lift_subst_dummy del: lift_subst)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   249
  hence "Abs (s \<degree> Var 0) => Abs (lift u 0 \<degree> Var 0)" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   250
  moreover have "\<not> free (lift u 0) 0" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   251
  hence "Abs (lift u 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta> lift u 0[dummy/0]"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   252
    by (rule eta.eta)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   253
  hence "Abs (lift u 0 \<degree> Var 0) \<rightarrow>\<^sub>\<eta>\<^sup>* u" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   254
  ultimately show ?thesis by iprover
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   255
qed
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   256
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   257
theorem eta_par_beta:
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   258
  assumes st: "s \<rightarrow>\<^sub>\<eta> t"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   259
  and tu: "t => u"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   260
  shows "\<exists>t'. s => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" using tu st
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   261
proof (induct arbitrary: s)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   262
  case (var n)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   263
  thus ?case by (iprover intro: par_beta_refl)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   264
next
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   265
  case (abs s' t)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   266
  note abs' = this
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   267
  from `s \<rightarrow>\<^sub>\<eta> Abs s'` show ?case
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   268
  proof cases
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   269
    case (eta s'' dummy)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   270
    from abs have "Abs s' => Abs t" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   271
    with eta have "s''[dummy/0] => Abs t" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   272
    with `\<not> free s'' 0` have "\<exists>t'. Abs (s'' \<degree> Var 0) => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   273
      by (rule eta_case)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   274
    with eta show ?thesis by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   275
  next
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   276
    case (abs r)
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   277
    from `r \<rightarrow>\<^sub>\<eta> s'`
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   278
    obtain t' where r: "r => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* t" by (iprover dest: abs')
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   279
    from r have "Abs r => Abs t'" ..
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   280
    moreover from t' have "Abs t' \<rightarrow>\<^sub>\<eta>\<^sup>* Abs t" by (rule rtrancl_eta_Abs)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   281
    ultimately show ?thesis using abs by simp iprover
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   282
  qed
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   283
next
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   284
  case (app u u' t t')
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   285
  from `s \<rightarrow>\<^sub>\<eta> u \<degree> t` show ?case
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   286
  proof cases
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   287
    case (eta s' dummy)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   288
    from app have "u \<degree> t => u' \<degree> t'" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   289
    with eta have "s'[dummy/0] => u' \<degree> t'" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   290
    with `\<not> free s' 0` have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   291
      by (rule eta_case)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   292
    with eta show ?thesis by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   293
  next
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   294
    case (appL s')
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   295
    from `s' \<rightarrow>\<^sub>\<eta> u`
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   296
    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: app)
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   297
    from s' and app have "s' \<degree> t => r \<degree> t'" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   298
    moreover from r have "r \<degree> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppL)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   299
    ultimately show ?thesis using appL by simp iprover
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   300
  next
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   301
    case (appR s')
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   302
    from `s' \<rightarrow>\<^sub>\<eta> t`
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   303
    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: app)
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   304
    from s' and app have "u \<degree> s' => u' \<degree> r" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   305
    moreover from r have "u' \<degree> r \<rightarrow>\<^sub>\<eta>\<^sup>* u' \<degree> t'" by (simp add: rtrancl_eta_AppR)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   306
    ultimately show ?thesis using appR by simp iprover
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   307
  qed
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   308
next
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   309
  case (beta u u' t t')
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   310
  from `s \<rightarrow>\<^sub>\<eta> Abs u \<degree> t` show ?case
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   311
  proof cases
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   312
    case (eta s' dummy)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   313
    from beta have "Abs u \<degree> t => u'[t'/0]" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   314
    with eta have "s'[dummy/0] => u'[t'/0]" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   315
    with `\<not> free s' 0` have "\<exists>r. Abs (s' \<degree> Var 0) => r \<and> r \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   316
      by (rule eta_case)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   317
    with eta show ?thesis by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   318
  next
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   319
    case (appL s')
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   320
    from `s' \<rightarrow>\<^sub>\<eta> Abs u` show ?thesis
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   321
    proof cases
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   322
      case (eta s'' dummy)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   323
      have "Abs (lift u 1) = lift (Abs u) 0" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   324
      also from eta have "\<dots> = s''" by (simp add: lift_subst_dummy del: lift_subst)
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   325
      finally have s: "s = Abs (Abs (lift u 1) \<degree> Var 0) \<degree> t" using appL and eta by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   326
      from beta have "lift u 1 => lift u' 1" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   327
      hence "Abs (lift u 1) \<degree> Var 0 => lift u' 1[Var 0/0]"
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
   328
        using par_beta.var ..
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   329
      hence "Abs (Abs (lift u 1) \<degree> Var 0) \<degree> t => lift u' 1[Var 0/0][t'/0]"
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
   330
        using `t => t'` ..
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   331
      with s have "s => u'[t'/0]" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   332
      thus ?thesis by iprover
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   333
    next
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   334
      case (abs r)
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   335
      from `r \<rightarrow>\<^sub>\<eta> u`
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   336
      obtain r'' where r: "r => r''" and r'': "r'' \<rightarrow>\<^sub>\<eta>\<^sup>* u'" by (iprover dest: beta)
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   337
      from r and beta have "Abs r \<degree> t => r''[t'/0]" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   338
      moreover from r'' have "r''[t'/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
25973
4a584b094aba tuned document;
wenzelm
parents: 24231
diff changeset
   339
        by (rule rtrancl_eta_subst')
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   340
      ultimately show ?thesis using abs and appL by simp iprover
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   341
    qed
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   342
  next
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   343
    case (appR s')
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   344
    from `s' \<rightarrow>\<^sub>\<eta> t`
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   345
    obtain r where s': "s' => r" and r: "r \<rightarrow>\<^sub>\<eta>\<^sup>* t'" by (iprover dest: beta)
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   346
    from s' and beta have "Abs u \<degree> s' => u'[r/0]" by simp
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   347
    moreover from r have "u'[r/0] \<rightarrow>\<^sub>\<eta>\<^sup>* u'[t'/0]"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   348
      by (rule rtrancl_eta_subst'')
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   349
    ultimately show ?thesis using appR by simp iprover
34990
81e8fdfeb849 Adapted to changes in cases method.
berghofe
parents: 32605
diff changeset
   350
  qed
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   351
qed
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   352
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   353
theorem eta_postponement':
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   354
  assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t" and beta: "t => u"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   355
  shows "\<exists>t'. s => t' \<and> t' \<rightarrow>\<^sub>\<eta>\<^sup>* u" using eta beta
20503
503ac4c5ef91 induct method: renamed 'fixing' to 'arbitrary';
wenzelm
parents: 20217
diff changeset
   356
proof (induct arbitrary: u)
26181
fedc257417fc Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents: 25973
diff changeset
   357
  case base
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   358
  thus ?case by blast
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   359
next
26181
fedc257417fc Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents: 25973
diff changeset
   360
  case (step s' s'' s''')
fedc257417fc Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents: 25973
diff changeset
   361
  then obtain t' where s': "s' => t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''"
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   362
    by (auto dest: eta_par_beta)
26181
fedc257417fc Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents: 25973
diff changeset
   363
  from s' obtain t'' where s: "s => t''" and t'': "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* t'" using step
18557
60a0f9caa0a2 Provers/classical: stricter checks to ensure that supplied intro, dest and
paulson
parents: 18460
diff changeset
   364
    by blast
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
   365
  from t'' and t' have "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" by (rule rtranclp_trans)
17589
58eeffd73be1 renamed rules to iprover
nipkow
parents: 16417
diff changeset
   366
  with s show ?case by iprover
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   367
qed
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   368
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   369
theorem eta_postponement:
26181
fedc257417fc Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents: 25973
diff changeset
   370
  assumes "(sup beta eta)\<^sup>*\<^sup>* s t"
32235
8f9b8d14fc9f "more standard" argument order of relation composition (op O)
krauss
parents: 26181
diff changeset
   371
  shows "(beta\<^sup>*\<^sup>* OO eta\<^sup>*\<^sup>*) s t" using assms
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   372
proof induct
26181
fedc257417fc Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents: 25973
diff changeset
   373
  case base
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   374
  show ?case by blast
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   375
next
26181
fedc257417fc Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents: 25973
diff changeset
   376
  case (step s' s'')
fedc257417fc Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents: 25973
diff changeset
   377
  from step(3) obtain t' where s: "s \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and t': "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s'" by blast
fedc257417fc Transitive_Closure: induct and cases rules now declare proper case_names;
wenzelm
parents: 25973
diff changeset
   378
  from step(2) show ?case
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   379
  proof
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   380
    assume "s' \<rightarrow>\<^sub>\<beta> s''"
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   381
    with beta_subset_par_beta have "s' => s''" ..
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   382
    with t' obtain t'' where st: "t' => t''" and tu: "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s''"
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   383
      by (auto dest: eta_postponement')
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   384
    from par_beta_subset_beta st have "t' \<rightarrow>\<^sub>\<beta>\<^sup>* t''" ..
23750
a1db5f819d00 - Renamed inductive2 to inductive
berghofe
parents: 22422
diff changeset
   385
    with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtranclp_trans)
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   386
    thus ?thesis using tu ..
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   387
  next
22272
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   388
    assume "s' \<rightarrow>\<^sub>\<eta> s''"
aac2ac7c32fd - Adapted to new inductive definition package
berghofe
parents: 21404
diff changeset
   389
    with t' have "t' \<rightarrow>\<^sub>\<eta>\<^sup>* s''" ..
15522
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   390
    with s show ?thesis ..
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   391
  qed
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   392
qed
ec0fd05b2f2c Added proof of eta-postponement theorem (using parallel eta-reduction).
berghofe
parents: 13187
diff changeset
   393
11638
2c3dee321b4b inductive: no collective atts;
wenzelm
parents: 11183
diff changeset
   394
end