src/HOL/Lambda/Lambda.thy
author wenzelm
Wed Oct 31 22:05:37 2001 +0100 (2001-10-31)
changeset 12011 1a3a7b3cd9bb
parent 11943 a9672446b45f
child 13187 e5434b822a96
permissions -rw-r--r--
tuned notation (degree instead of dollar);
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
wenzelm@9811
     9
theory Lambda = Main:
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
wenzelm@9811
    56
consts
wenzelm@9811
    57
  beta :: "(dB \<times> dB) set"
nipkow@1120
    58
wenzelm@9811
    59
syntax
wenzelm@9811
    60
  "_beta" :: "[dB, dB] => bool"  (infixl "->" 50)
wenzelm@9811
    61
  "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "->>" 50)
nipkow@1120
    62
translations
wenzelm@9827
    63
  "s -> t" == "(s, t) \<in> beta"
wenzelm@9827
    64
  "s ->> t" == "(s, t) \<in> beta^*"
nipkow@1120
    65
paulson@1789
    66
inductive beta
wenzelm@11638
    67
  intros
wenzelm@12011
    68
    beta [simp, intro!]: "Abs s \<degree> t -> s[t/0]"
wenzelm@12011
    69
    appL [simp, intro!]: "s -> t ==> s \<degree> u -> t \<degree> u"
wenzelm@12011
    70
    appR [simp, intro!]: "s -> t ==> u \<degree> s -> u \<degree> t"
wenzelm@11638
    71
    abs [simp, intro!]: "s -> t ==> Abs s -> Abs t"
wenzelm@9811
    72
wenzelm@9811
    73
inductive_cases beta_cases [elim!]:
wenzelm@9811
    74
  "Var i -> t"
wenzelm@9811
    75
  "Abs r -> s"
wenzelm@12011
    76
  "s \<degree> t -> u"
wenzelm@9811
    77
wenzelm@9811
    78
declare if_not_P [simp] not_less_eq [simp]
wenzelm@9811
    79
  -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
wenzelm@9811
    80
wenzelm@9811
    81
wenzelm@9811
    82
subsection {* Congruence rules *}
wenzelm@9811
    83
wenzelm@9811
    84
lemma rtrancl_beta_Abs [intro!]:
wenzelm@9811
    85
    "s ->> s' ==> Abs s ->> Abs s'"
wenzelm@9811
    86
  apply (erule rtrancl_induct)
wenzelm@9811
    87
   apply (blast intro: rtrancl_into_rtrancl)+
wenzelm@9811
    88
  done
wenzelm@9811
    89
wenzelm@9811
    90
lemma rtrancl_beta_AppL:
wenzelm@12011
    91
    "s ->> s' ==> s \<degree> t ->> s' \<degree> t"
wenzelm@9811
    92
  apply (erule rtrancl_induct)
wenzelm@9811
    93
   apply (blast intro: rtrancl_into_rtrancl)+
wenzelm@9811
    94
  done
wenzelm@9811
    95
wenzelm@9811
    96
lemma rtrancl_beta_AppR:
wenzelm@12011
    97
    "t ->> t' ==> s \<degree> t ->> s \<degree> t'"
wenzelm@9811
    98
  apply (erule rtrancl_induct)
wenzelm@9811
    99
   apply (blast intro: rtrancl_into_rtrancl)+
wenzelm@9811
   100
  done
wenzelm@9811
   101
wenzelm@9811
   102
lemma rtrancl_beta_App [intro]:
wenzelm@12011
   103
    "[| s ->> s'; t ->> t' |] ==> s \<degree> t ->> s' \<degree> t'"
wenzelm@9811
   104
  apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
wenzelm@9811
   105
    intro: rtrancl_trans)
wenzelm@9811
   106
  done
wenzelm@9811
   107
wenzelm@9811
   108
wenzelm@9811
   109
subsection {* Substitution-lemmas *}
wenzelm@9811
   110
wenzelm@9811
   111
lemma subst_eq [simp]: "(Var k)[u/k] = u"
wenzelm@9811
   112
  apply (simp add: subst_Var)
wenzelm@9811
   113
  done
wenzelm@9811
   114
wenzelm@9811
   115
lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
wenzelm@9811
   116
  apply (simp add: subst_Var)
wenzelm@9811
   117
  done
wenzelm@9811
   118
wenzelm@9811
   119
lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
wenzelm@9811
   120
  apply (simp add: subst_Var)
wenzelm@9811
   121
  done
wenzelm@9811
   122
wenzelm@9941
   123
lemma lift_lift [rule_format]:
wenzelm@9811
   124
    "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
wenzelm@9811
   125
  apply (induct_tac t)
wenzelm@9811
   126
    apply auto
wenzelm@9811
   127
  done
wenzelm@9811
   128
wenzelm@9811
   129
lemma lift_subst [simp]:
wenzelm@9811
   130
    "\<forall>i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
wenzelm@9811
   131
  apply (induct_tac t)
wenzelm@9811
   132
    apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
wenzelm@9811
   133
  done
wenzelm@9811
   134
wenzelm@9811
   135
lemma lift_subst_lt:
wenzelm@9811
   136
    "\<forall>i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
wenzelm@9811
   137
  apply (induct_tac t)
wenzelm@9811
   138
    apply (simp_all add: subst_Var lift_lift)
wenzelm@9811
   139
  done
wenzelm@9811
   140
wenzelm@9811
   141
lemma subst_lift [simp]:
wenzelm@9811
   142
    "\<forall>k s. (lift t k)[s/k] = t"
wenzelm@9811
   143
  apply (induct_tac t)
wenzelm@9811
   144
    apply simp_all
wenzelm@9811
   145
  done
wenzelm@9811
   146
wenzelm@9941
   147
lemma subst_subst [rule_format]:
wenzelm@9811
   148
    "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
wenzelm@9811
   149
  apply (induct_tac t)
wenzelm@9811
   150
    apply (simp_all
wenzelm@9811
   151
      add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
wenzelm@9811
   152
      split: nat.split)
paulson@10851
   153
  apply (auto simp add: linorder_neq_iff)
wenzelm@9811
   154
  done
wenzelm@9811
   155
wenzelm@9811
   156
wenzelm@9811
   157
subsection {* Equivalence proof for optimized substitution *}
wenzelm@9811
   158
wenzelm@9811
   159
lemma liftn_0 [simp]: "\<forall>k. liftn 0 t k = t"
wenzelm@9811
   160
  apply (induct_tac t)
wenzelm@9811
   161
    apply (simp_all add: subst_Var)
wenzelm@9811
   162
  done
wenzelm@9811
   163
wenzelm@9811
   164
lemma liftn_lift [simp]:
wenzelm@9811
   165
    "\<forall>k. liftn (Suc n) t k = lift (liftn n t k) k"
wenzelm@9811
   166
  apply (induct_tac t)
wenzelm@9811
   167
    apply (simp_all add: subst_Var)
wenzelm@9811
   168
  done
wenzelm@9811
   169
wenzelm@9811
   170
lemma substn_subst_n [simp]:
wenzelm@9811
   171
    "\<forall>n. substn t s n = t[liftn n s 0 / n]"
wenzelm@9811
   172
  apply (induct_tac t)
wenzelm@9811
   173
    apply (simp_all add: subst_Var)
wenzelm@9811
   174
  done
wenzelm@9811
   175
wenzelm@9811
   176
theorem substn_subst_0: "substn t s 0 = t[s/0]"
wenzelm@9811
   177
  apply simp
wenzelm@9811
   178
  done
wenzelm@9811
   179
wenzelm@9811
   180
wenzelm@9811
   181
subsection {* Preservation theorems *}
wenzelm@9811
   182
wenzelm@9811
   183
text {* Not used in Church-Rosser proof, but in Strong
wenzelm@9811
   184
  Normalization. \medskip *}
wenzelm@9811
   185
wenzelm@9941
   186
theorem subst_preserves_beta [rule_format, simp]:
wenzelm@9811
   187
    "r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
wenzelm@9811
   188
  apply (erule beta.induct)
wenzelm@9811
   189
     apply (simp_all add: subst_subst [symmetric])
wenzelm@9811
   190
  done
wenzelm@9811
   191
wenzelm@9941
   192
theorem lift_preserves_beta [rule_format, simp]:
wenzelm@9811
   193
    "r -> s ==> \<forall>i. lift r i -> lift s i"
wenzelm@9811
   194
  apply (erule beta.induct)
wenzelm@9811
   195
     apply auto
wenzelm@9811
   196
  done
wenzelm@9811
   197
wenzelm@9941
   198
theorem subst_preserves_beta2 [rule_format, simp]:
wenzelm@9811
   199
    "\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
wenzelm@9811
   200
  apply (induct_tac t)
wenzelm@9811
   201
    apply (simp add: subst_Var r_into_rtrancl)
wenzelm@9811
   202
   apply (simp add: rtrancl_beta_App)
wenzelm@9811
   203
  apply (simp add: rtrancl_beta_Abs)
wenzelm@9811
   204
  done
wenzelm@9811
   205
wenzelm@11638
   206
end