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