26 "perm_rlam pi (rVar a) = rVar (pi \<bullet> a)" |
26 "perm_rlam pi (rVar a) = rVar (pi \<bullet> a)" |
27 | "perm_rlam pi (rApp t1 t2) = rApp (perm_rlam pi t1) (perm_rlam pi t2)" |
27 | "perm_rlam pi (rApp t1 t2) = rApp (perm_rlam pi t1) (perm_rlam pi t2)" |
28 | "perm_rlam pi (rLam a t) = rLam (pi \<bullet> a) (perm_rlam pi t)" |
28 | "perm_rlam pi (rLam a t) = rLam (pi \<bullet> a) (perm_rlam pi t)" |
29 |
29 |
30 end |
30 end |
|
31 |
|
32 instance rlam::pt_name |
|
33 apply(default) |
|
34 apply(induct_tac [!] x rule: rlam.induct) |
|
35 apply(simp_all add: pt_name2 pt_name3) |
|
36 done |
|
37 |
|
38 instance rlam::fs_name |
|
39 apply(default) |
|
40 apply(induct_tac [!] x rule: rlam.induct) |
|
41 apply(simp add: supp_def) |
|
42 apply(fold supp_def) |
|
43 apply(simp add: supp_atm) |
|
44 apply(simp add: supp_def Collect_imp_eq Collect_neg_eq) |
|
45 apply(simp add: supp_def) |
|
46 apply(simp add: supp_def Collect_imp_eq Collect_neg_eq[symmetric]) |
|
47 apply(fold supp_def) |
|
48 apply(simp add: supp_atm) |
|
49 done |
31 |
50 |
32 inductive |
51 inductive |
33 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
52 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
34 where |
53 where |
35 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
54 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
360 apply(simp add: var_supp1) |
379 apply(simp add: var_supp1) |
361 done |
380 done |
362 |
381 |
363 (* lemma hom_reg: *) |
382 (* lemma hom_reg: *) |
364 |
383 |
|
384 lemma rlam_rec_eqvt: |
|
385 fixes pi::"name prm" |
|
386 and f1::"name \<Rightarrow> ('a::pt_name)" |
|
387 shows "(pi\<bullet>rlam_rec f1 f2 f3 t) = rlam_rec (pi\<bullet>f1) (pi\<bullet>f2) (pi\<bullet>f3) (pi\<bullet>t)" |
|
388 apply(induct t) |
|
389 apply(simp_all) |
|
390 apply(simp add: perm_fun_def) |
|
391 apply(perm_simp) |
|
392 apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst]) |
|
393 back |
|
394 apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst]) |
|
395 apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst]) |
|
396 apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst]) |
|
397 apply(simp) |
|
398 apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst]) |
|
399 back |
|
400 apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst]) |
|
401 apply(subst pt_fun_app_eq[OF pt_name_inst at_name_inst]) |
|
402 apply(simp) |
|
403 done |
|
404 |
|
405 |
|
406 lemma rlam_rec_respects: |
|
407 assumes f1: "f_var \<in> Respects (op= ===> op=)" |
|
408 and f2: "f_app \<in> Respects (alpha ===> alpha ===> op= ===> op= ===> op=)" |
|
409 and f3: "f_lam \<in> Respects (op= ===> alpha ===> op= ===> op=)" |
|
410 shows "rlam_rec f_var f_app f_lam \<in> Respects (alpha ===> op =)" |
|
411 apply(simp add: mem_def) |
|
412 apply(simp add: Respects_def) |
|
413 apply(rule allI) |
|
414 apply(rule allI) |
|
415 apply(rule impI) |
|
416 apply(erule alpha.induct) |
|
417 apply(simp) |
|
418 apply(simp) |
|
419 using f2 |
|
420 apply(simp add: mem_def) |
|
421 apply(simp add: Respects_def) |
|
422 using f3[simplified mem_def Respects_def] |
|
423 apply(simp) |
|
424 apply(case_tac "a=b") |
|
425 apply(clarify) |
|
426 apply(simp) |
|
427 apply(subst pt_swap_bij'') |
|
428 apply(rule pt_name_inst) |
|
429 apply(rule at_name_inst) |
|
430 apply(subst pt_swap_bij'') |
|
431 apply(rule pt_name_inst) |
|
432 apply(rule at_name_inst) |
|
433 apply(simp) |
|
434 apply(generate_fresh "name") |
|
435 (* probably true *) |
|
436 sorry |
|
437 |
365 lemma hom: |
438 lemma hom: |
366 "\<exists>hom\<in>Respects (alpha ===> op =). |
439 "\<exists>hom\<in>Respects (alpha ===> op =). |
367 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
440 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
368 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
441 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
369 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
442 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |