src/HOL/Lambda/Lambda.thy
author wenzelm
Mon, 04 Sep 2000 11:21:24 +0200
changeset 9827 ce6e22ff89c3
parent 9811 39ffdb8cab03
child 9906 5c027cca6262
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1269
ee011b365770 New version with eta reduction.
nipkow
parents: 1153
diff changeset
     1
(*  Title:      HOL/Lambda/Lambda.thy
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     4
    Copyright   1995 TU Muenchen
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     5
*)
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
     6
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
     7
header {* Basic definitions of Lambda-calculus *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
     8
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
     9
theory Lambda = Main:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    10
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    11
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    12
subsection {* Lambda-terms in de Bruijn notation and substitution *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    13
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    14
datatype dB =
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    15
    Var nat
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    16
  | App dB dB (infixl "$" 200)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    17
  | Abs dB
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    18
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    19
consts
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    20
  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    21
  lift :: "[dB, nat] => dB"
1153
5c5daf97cf2d Simplified the confluence proofs.
nipkow
parents: 1124
diff changeset
    22
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5146
diff changeset
    23
primrec
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    24
  "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    25
  "lift (s $ t) k = lift s k $ lift t k"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    26
  "lift (Abs s) k = Abs (lift s (k + 1))"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    27
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    28
primrec  (* FIXME base names *)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    29
  subst_Var: "(Var i)[s/k] =
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    30
    (if k < i then Var (i - 1) else if i = k then s else Var i)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    31
  subst_App: "(t $ u)[s/k] = t[s/k] $ u[s/k]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    32
  subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    33
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    34
declare subst_Var [simp del]
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    35
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    36
text {* Optimized versions of @{term subst} and @{term lift}. *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    37
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    38
consts
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    39
  substn :: "[dB, dB, nat] => dB"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    40
  liftn :: "[nat, dB, nat] => dB"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    41
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    42
primrec
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    43
  "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    44
  "liftn n (s $ t) k = liftn n s k $ liftn n t k"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    45
  "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    46
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5146
diff changeset
    47
primrec
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    48
  "substn (Var i) s k =
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    49
    (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    50
  "substn (t $ u) s k = substn t s k $ substn u s k"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    51
  "substn (Abs t) s k = Abs (substn t s (k + 1))"
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    52
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    53
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    54
subsection {* Beta-reduction *}
1153
5c5daf97cf2d Simplified the confluence proofs.
nipkow
parents: 1124
diff changeset
    55
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    56
consts
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    57
  beta :: "(dB \<times> dB) set"
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    58
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    59
syntax
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    60
  "_beta" :: "[dB, dB] => bool"  (infixl "->" 50)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    61
  "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "->>" 50)
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    62
translations
9827
wenzelm
parents: 9811
diff changeset
    63
  "s -> t" == "(s, t) \<in> beta"
wenzelm
parents: 9811
diff changeset
    64
  "s ->> t" == "(s, t) \<in> beta^*"
1120
ff7dd80513e6 Lambda calculus in de Bruijn notation.
nipkow
parents:
diff changeset
    65
1789
aade046ec6d5 Quotes now optional around inductive set
paulson
parents: 1376
diff changeset
    66
inductive beta
9811
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    67
  intros [simp, intro!]
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    68
    beta: "Abs s $ t -> s[t/0]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    69
    appL: "s -> t ==> s $ u -> t $ u"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    70
    appR: "s -> t ==> u $ s -> u $ t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    71
    abs: "s -> t ==> Abs s -> Abs t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    72
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    73
inductive_cases beta_cases [elim!]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    74
  "Var i -> t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    75
  "Abs r -> s"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    76
  "s $ t -> u"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    77
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    78
declare if_not_P [simp] not_less_eq [simp]
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    79
  -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    80
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    81
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    82
subsection {* Congruence rules *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    83
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    84
lemma rtrancl_beta_Abs [intro!]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    85
    "s ->> s' ==> Abs s ->> Abs s'"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    86
  apply (erule rtrancl_induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    87
   apply (blast intro: rtrancl_into_rtrancl)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    88
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    89
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    90
lemma rtrancl_beta_AppL:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    91
    "s ->> s' ==> s $ t ->> s' $ t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    92
  apply (erule rtrancl_induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    93
   apply (blast intro: rtrancl_into_rtrancl)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    94
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    95
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    96
lemma rtrancl_beta_AppR:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    97
    "t ->> t' ==> s $ t ->> s $ t'"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    98
  apply (erule rtrancl_induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
    99
   apply (blast intro: rtrancl_into_rtrancl)+
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   100
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   101
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   102
lemma rtrancl_beta_App [intro]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   103
    "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   104
  apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   105
    intro: rtrancl_trans)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   106
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   107
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   108
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   109
subsection {* Substitution-lemmas *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   110
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   111
lemma subst_eq [simp]: "(Var k)[u/k] = u"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   112
  apply (simp add: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   113
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   114
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   115
lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   116
  apply (simp add: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   117
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   118
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   119
lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   120
  apply (simp add: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   121
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   122
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   123
lemma lift_lift [rulify]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   124
    "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   125
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   126
    apply auto
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   127
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   128
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   129
lemma lift_subst [simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   130
    "\<forall>i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   131
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   132
    apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   133
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   134
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   135
lemma lift_subst_lt:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   136
    "\<forall>i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   137
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   138
    apply (simp_all add: subst_Var lift_lift)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   139
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   140
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   141
lemma subst_lift [simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   142
    "\<forall>k s. (lift t k)[s/k] = t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   143
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   144
    apply simp_all
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   145
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   146
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   147
lemma subst_subst [rulify]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   148
    "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   149
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   150
    apply (simp_all
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   151
      add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   152
      split: nat.split)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   153
  apply (auto elim: nat_neqE)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   154
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   155
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   156
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   157
subsection {* Equivalence proof for optimized substitution *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   158
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   159
lemma liftn_0 [simp]: "\<forall>k. liftn 0 t k = t"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   160
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   161
    apply (simp_all add: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   162
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   163
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   164
lemma liftn_lift [simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   165
    "\<forall>k. liftn (Suc n) t k = lift (liftn n t k) k"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   166
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   167
    apply (simp_all add: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   168
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   169
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   170
lemma substn_subst_n [simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   171
    "\<forall>n. substn t s n = t[liftn n s 0 / n]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   172
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   173
    apply (simp_all add: subst_Var)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   174
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   175
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   176
theorem substn_subst_0: "substn t s 0 = t[s/0]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   177
  apply simp
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   178
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   179
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   180
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   181
subsection {* Preservation theorems *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   182
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   183
text {* Not used in Church-Rosser proof, but in Strong
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   184
  Normalization. \medskip *}
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   185
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   186
theorem subst_preserves_beta [rulify, simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   187
    "r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   188
  apply (erule beta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   189
     apply (simp_all add: subst_subst [symmetric])
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   190
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   191
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   192
theorem lift_preserves_beta [rulify, simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   193
    "r -> s ==> \<forall>i. lift r i -> lift s i"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   194
  apply (erule beta.induct)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   195
     apply auto
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   196
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   197
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   198
theorem subst_preserves_beta2 [rulify, simp]:
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   199
    "\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   200
  apply (induct_tac t)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   201
    apply (simp add: subst_Var r_into_rtrancl)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   202
   apply (simp add: rtrancl_beta_App)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   203
  apply (simp add: rtrancl_beta_Abs)
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   204
  done
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   205
39ffdb8cab03 HOL/Lambda: converted into new-style theory and document;
wenzelm
parents: 6453
diff changeset
   206
end