307 trm4 :: pt |
307 trm4 :: pt |
308 begin |
308 begin |
309 |
309 |
310 (* does not work yet *) |
310 (* does not work yet *) |
311 primrec |
311 primrec |
312 permute_trm4 |
312 permute_trm4 and permute_trm4_list |
313 where |
313 where |
314 "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)" |
314 "permute_trm4 pi (Vr4 a) = Vr4 (pi \<bullet> a)" |
315 | "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute pi ts)" |
315 | "permute_trm4 pi (Ap4 t ts) = Ap4 (permute_trm4 pi t) (permute_trm4_list pi ts)" |
316 | "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)" |
316 | "permute_trm4 pi (Lm4 a t) = Lm4 (pi \<bullet> a) (permute_trm4 pi t)" |
317 |
317 | "permute_trm4_list pi ([]) = []" |
318 end |
318 | "permute_trm4_list pi (t#ts) = (permute_trm4 pi t) # (permute_trm4_list pi ts)" |
|
319 |
|
320 lemma pt_trm4_list_zero: |
|
321 fixes t::trm4 |
|
322 and ts::"trm4 list" |
|
323 shows "0 \<bullet> t = t" |
|
324 and "permute_trm4_list 0 ts = ts" |
|
325 apply(induct t and ts rule: trm4.inducts) |
|
326 apply(simp_all) |
|
327 done |
|
328 |
|
329 lemma pt_trm4_list_plus: |
|
330 fixes t::trm4 |
|
331 and ts::"trm4 list" |
|
332 shows "((p + q) \<bullet> t) = p \<bullet> (q \<bullet> t)" |
|
333 and "(permute_trm4_list (p + q) ts) = permute_trm4_list p (permute_trm4_list q ts)" |
|
334 apply(induct t and ts rule: trm4.inducts) |
|
335 apply(simp_all) |
|
336 done |
|
337 |
|
338 |
|
339 instance |
|
340 apply(default) |
|
341 apply(simp_all add: pt_trm4_list_zero pt_trm4_list_plus) |
|
342 done |
|
343 |
|
344 end |
|
345 |
|
346 (* "repairing" of the permute function *) |
|
347 lemma repaired: |
|
348 fixes ts::"trm4 list" |
|
349 shows "permute_trm4_list p ts = p \<bullet> ts" |
|
350 apply(induct ts) |
|
351 apply(simp_all) |
|
352 done |
|
353 |
|
354 thm permute_trm4_permute_trm4_list.simps[simplified repaired] |
319 |
355 |
320 inductive |
356 inductive |
321 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |
357 alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100) |
322 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) |
358 and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) |
323 where |
359 where |
324 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)" |
360 a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)" |
325 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2" |
361 | a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2" |
326 | a4: "\<exists>pi::name prm. (fv_trm4 t - {a} = fv_trm4 s - {b} \<and> |
362 | a4: "\<exists>pi. (fv_trm4 t - {atom a} = fv_trm4 s - {atom b} \<and> |
327 (fv_trm4 t - {a})\<sharp>* pi \<and> |
363 (fv_trm4 t - {atom a})\<sharp>* pi \<and> |
328 (pi \<bullet> t) \<approx>4 s \<and> |
364 (pi \<bullet> t) \<approx>4 s \<and> |
329 (pi \<bullet> a) = b) |
365 (pi \<bullet> a) = b) |
330 \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s" |
366 \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s" |
331 | a5: "[] \<approx>4list []" |
367 | a5: "[] \<approx>4list []" |
332 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)" |
368 | a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)" |
333 |
369 |
334 lemma alpha4_equivp: "equivp alpha4" sorry |
370 lemma alpha4_equivp: "equivp alpha4" sorry |