src/HOL/Lambda/Lambda.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 25974 0cb35fa9c6fa
child 36862 952b2b102a0a
permissions -rw-r--r--
added lemmas
     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 imports Main begin
    10 
    11 
    12 subsection {* Lambda-terms in de Bruijn notation and substitution *}
    13 
    14 datatype dB =
    15     Var nat
    16   | App dB dB (infixl "\<degree>" 200)
    17   | Abs dB
    18 
    19 primrec
    20   lift :: "[dB, nat] => dB"
    21 where
    22     "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
    23   | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
    24   | "lift (Abs s) k = Abs (lift s (k + 1))"
    25 
    26 primrec
    27   subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
    28 where (* 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 \<degree> u)[s/k] = t[s/k] \<degree> 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 primrec
    39   liftn :: "[nat, dB, nat] => dB"
    40 where
    41     "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
    42   | "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k"
    43   | "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
    44 
    45 primrec
    46   substn :: "[dB, dB, nat] => dB"
    47 where
    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 \<degree> u) s k = substn t s k \<degree> substn u s k"
    51   | "substn (Abs t) s k = Abs (substn t s (k + 1))"
    52 
    53 
    54 subsection {* Beta-reduction *}
    55 
    56 inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
    57   where
    58     beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
    59   | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
    60   | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
    61   | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t"
    62 
    63 abbreviation
    64   beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50) where
    65   "s ->> t == beta^** s t"
    66 
    67 notation (latex)
    68   beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
    69 
    70 inductive_cases beta_cases [elim!]:
    71   "Var i \<rightarrow>\<^sub>\<beta> t"
    72   "Abs r \<rightarrow>\<^sub>\<beta> s"
    73   "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
    74 
    75 declare if_not_P [simp] not_less_eq [simp]
    76   -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
    77 
    78 
    79 subsection {* Congruence rules *}
    80 
    81 lemma rtrancl_beta_Abs [intro!]:
    82     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
    83   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
    84 
    85 lemma rtrancl_beta_AppL:
    86     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
    87   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
    88 
    89 lemma rtrancl_beta_AppR:
    90     "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
    91   by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
    92 
    93 lemma rtrancl_beta_App [intro]:
    94     "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
    95   by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
    96 
    97 
    98 subsection {* Substitution-lemmas *}
    99 
   100 lemma subst_eq [simp]: "(Var k)[u/k] = u"
   101   by (simp add: subst_Var)
   102 
   103 lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
   104   by (simp add: subst_Var)
   105 
   106 lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
   107   by (simp add: subst_Var)
   108 
   109 lemma lift_lift:
   110     "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
   111   by (induct t arbitrary: i k) auto
   112 
   113 lemma lift_subst [simp]:
   114     "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
   115   by (induct t arbitrary: i j s)
   116     (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
   117 
   118 lemma lift_subst_lt:
   119     "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
   120   by (induct t arbitrary: i j s) (simp_all add: subst_Var lift_lift)
   121 
   122 lemma subst_lift [simp]:
   123     "(lift t k)[s/k] = t"
   124   by (induct t arbitrary: k s) simp_all
   125 
   126 lemma subst_subst:
   127     "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
   128   by (induct t arbitrary: i j u v)
   129     (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
   130       split: nat.split)
   131 
   132 
   133 subsection {* Equivalence proof for optimized substitution *}
   134 
   135 lemma liftn_0 [simp]: "liftn 0 t k = t"
   136   by (induct t arbitrary: k) (simp_all add: subst_Var)
   137 
   138 lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
   139   by (induct t arbitrary: k) (simp_all add: subst_Var)
   140 
   141 lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
   142   by (induct t arbitrary: n) (simp_all add: subst_Var)
   143 
   144 theorem substn_subst_0: "substn t s 0 = t[s/0]"
   145   by simp
   146 
   147 
   148 subsection {* Preservation theorems *}
   149 
   150 text {* Not used in Church-Rosser proof, but in Strong
   151   Normalization. \medskip *}
   152 
   153 theorem subst_preserves_beta [simp]:
   154     "r \<rightarrow>\<^sub>\<beta> s ==> r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i]"
   155   by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
   156 
   157 theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
   158   apply (induct set: rtranclp)
   159    apply (rule rtranclp.rtrancl_refl)
   160   apply (erule rtranclp.rtrancl_into_rtrancl)
   161   apply (erule subst_preserves_beta)
   162   done
   163 
   164 theorem lift_preserves_beta [simp]:
   165     "r \<rightarrow>\<^sub>\<beta> s ==> lift r i \<rightarrow>\<^sub>\<beta> lift s i"
   166   by (induct arbitrary: i set: beta) auto
   167 
   168 theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
   169   apply (induct set: rtranclp)
   170    apply (rule rtranclp.rtrancl_refl)
   171   apply (erule rtranclp.rtrancl_into_rtrancl)
   172   apply (erule lift_preserves_beta)
   173   done
   174 
   175 theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   176   apply (induct t arbitrary: r s i)
   177     apply (simp add: subst_Var r_into_rtranclp)
   178    apply (simp add: rtrancl_beta_App)
   179   apply (simp add: rtrancl_beta_Abs)
   180   done
   181 
   182 theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   183   apply (induct set: rtranclp)
   184    apply (rule rtranclp.rtrancl_refl)
   185   apply (erule rtranclp_trans)
   186   apply (erule subst_preserves_beta2)
   187   done
   188 
   189 end