src/HOL/Lambda/Lambda.thy
author berghofe
Wed Feb 07 17:44:07 2007 +0100 (2007-02-07)
changeset 22271 51a80e238b29
parent 21404 eb85850d3eb7
child 23750 a1db5f819d00
permissions -rw-r--r--
Adapted to new inductive definition package.
nipkow@1269
     1
(*  Title:      HOL/Lambda/Lambda.thy
nipkow@1120
     2
    ID:         $Id$
nipkow@1120
     3
    Author:     Tobias Nipkow
nipkow@1120
     4
    Copyright   1995 TU Muenchen
nipkow@1120
     5
*)
nipkow@1120
     6
wenzelm@9811
     7
header {* Basic definitions of Lambda-calculus *}
wenzelm@9811
     8
haftmann@16417
     9
theory Lambda imports Main begin
wenzelm@9811
    10
nipkow@1120
    11
wenzelm@9811
    12
subsection {* Lambda-terms in de Bruijn notation and substitution *}
wenzelm@9811
    13
wenzelm@9811
    14
datatype dB =
wenzelm@9811
    15
    Var nat
wenzelm@12011
    16
  | App dB dB (infixl "\<degree>" 200)
wenzelm@9811
    17
  | Abs dB
nipkow@1120
    18
nipkow@1120
    19
consts
wenzelm@9811
    20
  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
wenzelm@9811
    21
  lift :: "[dB, nat] => dB"
nipkow@1153
    22
berghofe@5184
    23
primrec
wenzelm@9811
    24
  "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
wenzelm@12011
    25
  "lift (s \<degree> t) k = lift s k \<degree> lift t k"
wenzelm@9811
    26
  "lift (Abs s) k = Abs (lift s (k + 1))"
wenzelm@9811
    27
wenzelm@9811
    28
primrec  (* FIXME base names *)
wenzelm@9811
    29
  subst_Var: "(Var i)[s/k] =
wenzelm@9811
    30
    (if k < i then Var (i - 1) else if i = k then s else Var i)"
wenzelm@12011
    31
  subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
wenzelm@9811
    32
  subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
wenzelm@9811
    33
wenzelm@9811
    34
declare subst_Var [simp del]
wenzelm@9811
    35
wenzelm@9811
    36
text {* Optimized versions of @{term subst} and @{term lift}. *}
wenzelm@9811
    37
wenzelm@9811
    38
consts
wenzelm@9811
    39
  substn :: "[dB, dB, nat] => dB"
wenzelm@9811
    40
  liftn :: "[nat, dB, nat] => dB"
wenzelm@9811
    41
wenzelm@9811
    42
primrec
wenzelm@9811
    43
  "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
wenzelm@12011
    44
  "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
wenzelm@9811
    45
  "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
nipkow@1120
    46
berghofe@5184
    47
primrec
wenzelm@9811
    48
  "substn (Var i) s k =
wenzelm@9811
    49
    (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
wenzelm@12011
    50
  "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k"
wenzelm@9811
    51
  "substn (Abs t) s k = Abs (substn t s (k + 1))"
nipkow@1120
    52
wenzelm@9811
    53
wenzelm@9811
    54
subsection {* Beta-reduction *}
nipkow@1153
    55
berghofe@22271
    56
inductive2 beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
berghofe@22271
    57
  where
berghofe@22271
    58
    beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
berghofe@22271
    59
  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
berghofe@22271
    60
  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
berghofe@22271
    61
  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
wenzelm@21404
    62
wenzelm@21404
    63
abbreviation
wenzelm@21404
    64
  beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50) where
berghofe@22271
    65
  "s ->> t == beta^** s t"
wenzelm@19086
    66
wenzelm@21210
    67
notation (latex)
wenzelm@19656
    68
  beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
nipkow@1120
    69
berghofe@22271
    70
inductive_cases2 beta_cases [elim!]:
berghofe@14065
    71
  "Var i \<rightarrow>\<^sub>\<beta> t"
berghofe@14065
    72
  "Abs r \<rightarrow>\<^sub>\<beta> s"
berghofe@14065
    73
  "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
wenzelm@9811
    74
wenzelm@9811
    75
declare if_not_P [simp] not_less_eq [simp]
wenzelm@9811
    76
  -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
wenzelm@9811
    77
wenzelm@9811
    78
wenzelm@9811
    79
subsection {* Congruence rules *}
wenzelm@9811
    80
wenzelm@9811
    81
lemma rtrancl_beta_Abs [intro!]:
berghofe@14065
    82
    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
berghofe@22271
    83
  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
wenzelm@9811
    84
wenzelm@9811
    85
lemma rtrancl_beta_AppL:
berghofe@14065
    86
    "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
berghofe@22271
    87
  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
wenzelm@9811
    88
wenzelm@9811
    89
lemma rtrancl_beta_AppR:
berghofe@14065
    90
    "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
berghofe@22271
    91
  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
wenzelm@9811
    92
wenzelm@9811
    93
lemma rtrancl_beta_App [intro]:
berghofe@14065
    94
    "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
berghofe@22271
    95
  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans')
wenzelm@9811
    96
wenzelm@9811
    97
wenzelm@9811
    98
subsection {* Substitution-lemmas *}
wenzelm@9811
    99
wenzelm@9811
   100
lemma subst_eq [simp]: "(Var k)[u/k] = u"
wenzelm@18241
   101
  by (simp add: subst_Var)
wenzelm@9811
   102
wenzelm@9811
   103
lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
wenzelm@18241
   104
  by (simp add: subst_Var)
wenzelm@9811
   105
wenzelm@9811
   106
lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
wenzelm@18241
   107
  by (simp add: subst_Var)
wenzelm@9811
   108
wenzelm@18241
   109
lemma lift_lift:
wenzelm@18241
   110
    "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
wenzelm@20503
   111
  by (induct t arbitrary: i k) auto
wenzelm@9811
   112
wenzelm@9811
   113
lemma lift_subst [simp]:
wenzelm@18241
   114
    "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
wenzelm@20503
   115
  by (induct t arbitrary: i j s)
wenzelm@18241
   116
    (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
wenzelm@9811
   117
wenzelm@9811
   118
lemma lift_subst_lt:
wenzelm@18241
   119
    "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
wenzelm@20503
   120
  by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)
wenzelm@9811
   121
wenzelm@9811
   122
lemma subst_lift [simp]:
wenzelm@18241
   123
    "(lift t k)[s/k] = t"
wenzelm@20503
   124
  by (induct t arbitrary: k s) simp_all
wenzelm@9811
   125
wenzelm@18241
   126
lemma subst_subst:
wenzelm@18241
   127
    "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
wenzelm@20503
   128
  by (induct t arbitrary: i j u v)
wenzelm@18241
   129
    (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
wenzelm@9811
   130
      split: nat.split)
wenzelm@9811
   131
wenzelm@9811
   132
wenzelm@9811
   133
subsection {* Equivalence proof for optimized substitution *}
wenzelm@9811
   134
wenzelm@18241
   135
lemma liftn_0 [simp]: "liftn 0 t k = t"
wenzelm@20503
   136
  by (induct t arbitrary: k) (simp_all add: subst_Var)
wenzelm@9811
   137
wenzelm@18241
   138
lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
wenzelm@20503
   139
  by (induct t arbitrary: k) (simp_all add: subst_Var)
wenzelm@9811
   140
wenzelm@18241
   141
lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
wenzelm@20503
   142
  by (induct t arbitrary: n) (simp_all add: subst_Var)
wenzelm@9811
   143
wenzelm@9811
   144
theorem substn_subst_0: "substn t s 0 = t[s/0]"
wenzelm@18241
   145
  by simp
wenzelm@9811
   146
wenzelm@9811
   147
wenzelm@9811
   148
subsection {* Preservation theorems *}
wenzelm@9811
   149
wenzelm@9811
   150
text {* Not used in Church-Rosser proof, but in Strong
wenzelm@9811
   151
  Normalization. \medskip *}
wenzelm@9811
   152
berghofe@13915
   153
theorem subst_preserves_beta [simp]:
wenzelm@18257
   154
    "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
wenzelm@20503
   155
  by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
wenzelm@9811
   156
berghofe@14065
   157
theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
wenzelm@18241
   158
  apply (induct set: rtrancl)
berghofe@22271
   159
   apply (rule rtrancl.rtrancl_refl)
berghofe@22271
   160
  apply (erule rtrancl.rtrancl_into_rtrancl)
berghofe@14065
   161
  apply (erule subst_preserves_beta)
berghofe@14065
   162
  done
berghofe@14065
   163
berghofe@13915
   164
theorem lift_preserves_beta [simp]:
wenzelm@18257
   165
    "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
wenzelm@20503
   166
  by (induct arbitrary: i set: beta) auto
wenzelm@9811
   167
berghofe@14065
   168
theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
wenzelm@18241
   169
  apply (induct set: rtrancl)
berghofe@22271
   170
   apply (rule rtrancl.rtrancl_refl)
berghofe@22271
   171
  apply (erule rtrancl.rtrancl_into_rtrancl)
berghofe@14065
   172
  apply (erule lift_preserves_beta)
berghofe@14065
   173
  done
berghofe@14065
   174
wenzelm@18241
   175
theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
wenzelm@20503
   176
  apply (induct t arbitrary: r s i)
berghofe@22271
   177
    apply (simp add: subst_Var r_into_rtrancl')
wenzelm@9811
   178
   apply (simp add: rtrancl_beta_App)
wenzelm@9811
   179
  apply (simp add: rtrancl_beta_Abs)
wenzelm@9811
   180
  done
wenzelm@9811
   181
berghofe@14065
   182
theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
wenzelm@18241
   183
  apply (induct set: rtrancl)
berghofe@22271
   184
   apply (rule rtrancl.rtrancl_refl)
berghofe@22271
   185
  apply (erule rtrancl_trans')
berghofe@14065
   186
  apply (erule subst_preserves_beta2)
berghofe@14065
   187
  done
berghofe@14065
   188
wenzelm@11638
   189
end