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