1(* Title: HOL/Proofs/Lambda/Lambda.thy 2 Author: Tobias Nipkow 3 Copyright 1995 TU Muenchen 4*) 5 6section \<open>Basic definitions of Lambda-calculus\<close> 7 8theory Lambda 9imports Main 10begin 11 12declare [[syntax_ambiguity_warning = false]] 13 14 15subsection \<open>Lambda-terms in de Bruijn notation and substitution\<close> 16 17datatype dB = 18 Var nat 19 | App dB dB (infixl "\<degree>" 200) 20 | Abs dB 21 22primrec 23 lift :: "[dB, nat] => dB" 24where 25 "lift (Var i) k = (if i < k then Var i else Var (i + 1))" 26 | "lift (s \<degree> t) k = lift s k \<degree> lift t k" 27 | "lift (Abs s) k = Abs (lift s (k + 1))" 28 29primrec 30 subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300) 31where (* FIXME base names *) 32 subst_Var: "(Var i)[s/k] = 33 (if k < i then Var (i - 1) else if i = k then s else Var i)" 34 | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]" 35 | subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])" 36 37declare subst_Var [simp del] 38 39text \<open>Optimized versions of @{term subst} and @{term lift}.\<close> 40 41primrec 42 liftn :: "[nat, dB, nat] => dB" 43where 44 "liftn n (Var i) k = (if i < k then Var i else Var (i + n))" 45 | "liftn n (s \<degree> t) k = liftn n s k \<degree> liftn n t k" 46 | "liftn n (Abs s) k = Abs (liftn n s (k + 1))" 47 48primrec 49 substn :: "[dB, dB, nat] => dB" 50where 51 "substn (Var i) s k = 52 (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)" 53 | "substn (t \<degree> u) s k = substn t s k \<degree> substn u s k" 54 | "substn (Abs t) s k = Abs (substn t s (k + 1))" 55 56 57subsection \<open>Beta-reduction\<close> 58 59inductive beta :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50) 60 where 61 beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]" 62 | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u" 63 | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t" 64 | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs s \<rightarrow>\<^sub>\<beta> Abs t" 65 66abbreviation 67 beta_reds :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50) where 68 "s \<rightarrow>\<^sub>\<beta>\<^sup>* t == beta\<^sup>*\<^sup>* s t" 69 70inductive_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 75declare if_not_P [simp] not_less_eq [simp] 76 \<comment> \<open>don't add \<open>r_into_rtrancl[intro!]\<close>\<close> 77 78 79subsection \<open>Congruence rules\<close> 80 81lemma 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 85lemma 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 89lemma 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 93lemma 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 98subsection \<open>Substitution-lemmas\<close> 99 100lemma subst_eq [simp]: "(Var k)[u/k] = u" 101 by (simp add: subst_Var) 102 103lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)" 104 by (simp add: subst_Var) 105 106lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j" 107 by (simp add: subst_Var) 108 109lemma 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 113lemma 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 118lemma 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 122lemma subst_lift [simp]: 123 "(lift t k)[s/k] = t" 124 by (induct t arbitrary: k s) simp_all 125 126lemma 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 133subsection \<open>Equivalence proof for optimized substitution\<close> 134 135lemma liftn_0 [simp]: "liftn 0 t k = t" 136 by (induct t arbitrary: k) (simp_all add: subst_Var) 137 138lemma 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 141lemma 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 144theorem substn_subst_0: "substn t s 0 = t[s/0]" 145 by simp 146 147 148subsection \<open>Preservation theorems\<close> 149 150text \<open>Not used in Church-Rosser proof, but in Strong 151 Normalization. \medskip\<close> 152 153theorem 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 157theorem 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 164theorem 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 168theorem 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 175theorem 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 182theorem 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 189end 190