192 inductive |
192 inductive |
193 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
193 alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100) |
194 where |
194 where |
195 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
195 a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)" |
196 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
196 | a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2" |
197 | a3: "\<exists>pi::name prm. (fv_trm3 t - {a} = fv_trm3 s - {b} \<and> (fv_trm3 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>3 s \<and> (pi \<bullet> a) = b) |
197 | a3: "\<exists>pi::name prm. (fv_trm3 t - {a} = fv_trm3 s - {b} \<and> |
|
198 (fv_trm3 t - {a})\<sharp>* pi \<and> |
|
199 (pi \<bullet> t) \<approx>3 s \<and> |
|
200 (pi \<bullet> a) = b) |
198 \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
201 \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s" |
199 | a4: "\<exists>pi::name prm. ( |
202 | a4: "\<exists>pi::name prm. ( |
200 fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and> |
203 fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and> |
201 (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and> |
204 (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and> |
202 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
205 pi \<bullet> t1 = t2 (* \<and> (pi \<bullet> b1 = b2) *) |
205 lemma alpha3_equivp: "equivp alpha3" sorry |
208 lemma alpha3_equivp: "equivp alpha3" sorry |
206 |
209 |
207 quotient_type qtrm3 = trm3 / alpha3 |
210 quotient_type qtrm3 = trm3 / alpha3 |
208 by (rule alpha3_equivp) |
211 by (rule alpha3_equivp) |
209 |
212 |
210 end |
213 |
|
214 section {*** lam with indirect list recursion ***} |
|
215 |
|
216 datatype trm4 = |
|
217 Vr4 "name" |
|
218 | Ap4 "trm4" "trm4 list" |
|
219 | Lm4 "name" "trm4" |
|
220 |
|
221 thm trm4.recs |
|
222 |
|
223 primrec |
|
224 fv_trm4 and fv_trm4_list |
|
225 where |
|
226 "fv_trm4 (Vr4 x) = {x}" |
|
227 | "fv_trm4 (Ap4 t ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)" |
|
228 | "fv_trm4 (Lm4 x t) = (fv_trm4 t) - {x}" |
|
229 | "fv_trm4_list ([]) = {}" |
|
230 | "fv_trm4_list (t#ts) = (fv_trm4 t) \<union> (fv_trm4_list ts)" |
|
231 |
|
232 |
|
233 (* needs to be stated by the package *) |
|
234 (* there cannot be a clause for lists, as *) |
|
235 (* permutations are already defined in Nominal (also functions, options, and so on) *) |
|
236 overloading |
|
237 perm_trm4 \<equiv> "perm :: 'x prm \<Rightarrow> trm4 \<Rightarrow> trm4" (unchecked) |
|
238 begin |
|
239 |
|
240 primrec |
|
241 perm_trm4 |
|
242 where |
|
243 "perm_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)" |
|
244 | "perm_trm4 pi (Ap4 t ts) = Ap4 (perm_trm4 pi t) (pi \<bullet> ts)" |
|
245 | "perm_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (perm_trm4 pi t)" |
|
246 |
|
247 end |
|
248 |
|
249 inductive |
|
250 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |
|
251 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) |
|
252 where |
|
253 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)" |
|
254 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2" |
|
255 | a4: "\<exists>pi::name prm. (fv_trm4 t - {a} = fv_trm4 s - {b} \<and> |
|
256 (fv_trm4 t - {a})\<sharp>* pi \<and> |
|
257 (pi \<bullet> t) \<approx>4 s \<and> |
|
258 (pi \<bullet> a) = b) |
|
259 \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s" |
|
260 | a5: "[] \<approx>4list []" |
|
261 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)" |
|
262 |
|
263 lemma alpha4_equivp: "equivp alpha4" sorry |
|
264 lemma alpha4list_equivp: "equivp alpha4list" sorry |
|
265 |
|
266 quotient_type |
|
267 qtrm4 = trm4 / alpha4 and |
|
268 qtrm4list = "trm4 list" / alpha4list |
|
269 by (simp_all add: alpha4_equivp alpha4list_equivp) |
|
270 |
|
271 end |