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