30 end |
30 end |
31 |
31 |
32 declare perm_rlam.simps[eqvt] |
32 declare perm_rlam.simps[eqvt] |
33 |
33 |
34 instance rlam::pt_name |
34 instance rlam::pt_name |
35 apply(default) |
35 apply(default) |
36 apply(induct_tac [!] x rule: rlam.induct) |
36 apply(induct_tac [!] x rule: rlam.induct) |
37 apply(simp_all add: pt_name2 pt_name3) |
37 apply(simp_all add: pt_name2 pt_name3) |
38 done |
38 done |
39 |
39 |
40 instance rlam::fs_name |
40 instance rlam::fs_name |
41 apply(default) |
41 apply(default) |
42 apply(induct_tac [!] x rule: rlam.induct) |
42 apply(induct_tac [!] x rule: rlam.induct) |
43 apply(simp add: supp_def) |
43 apply(simp add: supp_def) |
44 apply(fold supp_def) |
44 apply(fold supp_def) |
45 apply(simp add: supp_atm) |
45 apply(simp add: supp_atm) |
46 apply(simp add: supp_def Collect_imp_eq Collect_neg_eq) |
46 apply(simp add: supp_def Collect_imp_eq Collect_neg_eq) |
47 apply(simp add: supp_def) |
47 apply(simp add: supp_def) |
48 apply(simp add: supp_def Collect_imp_eq Collect_neg_eq[symmetric]) |
48 apply(simp add: supp_def Collect_imp_eq Collect_neg_eq[symmetric]) |
49 apply(fold supp_def) |
49 apply(fold supp_def) |
50 apply(simp add: supp_atm) |
50 apply(simp add: supp_atm) |
51 done |
51 done |
52 |
52 |
53 declare set_diff_eqvt[eqvt] |
53 declare set_diff_eqvt[eqvt] |
54 |
54 |
55 lemma rfv_eqvt[eqvt]: |
55 lemma rfv_eqvt[eqvt]: |
56 fixes pi::"name prm" |
56 fixes pi::"name prm" |
478 apply(rule conjI) |
478 apply(rule conjI) |
479 apply(simp) |
479 apply(simp) |
480 apply(simp) |
480 apply(simp) |
481 sorry |
481 sorry |
482 |
482 |
483 lemma hom_reg:" |
483 lemma hom_res: " |
484 (\<exists>hom\<in>Respects (alpha ===> op =). |
484 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
485 (\<forall>x. hom (rVar x) = f_var x) \<and> |
485 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
486 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
486 \<exists>hom\<in>Respects (alpha ===> op =). |
487 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa)))) \<longrightarrow> |
487 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
488 (\<exists>hom. |
488 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
489 (\<forall>x. hom (rVar x) = f_var x) \<and> |
489 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
490 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
490 apply(rule allI) |
491 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" |
491 apply(rule ballI)+ |
492 by(regularize) |
492 apply(rule_tac x="rlam_rec f_var f_app XX" in bexI) |
493 |
493 apply(rule conjI) |
494 lemma hom_pre:" |
494 apply(simp) |
495 (\<exists>hom. |
495 apply(rule conjI) |
496 (\<forall>x. hom (rVar x) = f_var x) \<and> |
496 apply(simp) |
497 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
497 apply(simp_all only: in_respects) |
498 (\<forall>xa a. hom (rLam a xa) = f_lam (\<lambda>b. [(a, b)] \<bullet> xa) (\<lambda>b. hom ([(a, b)] \<bullet> xa))))" |
498 sorry |
499 apply (rule impE[OF hom_reg]) |
|
500 apply (rule hom) |
|
501 apply (assumption) |
|
502 done |
|
503 |
499 |
504 lemma hom': |
500 lemma hom': |
505 "\<exists>hom. |
501 "\<exists>hom. |
506 ((\<forall>x. hom (Var x) = f_var x) \<and> |
502 ((\<forall>x. hom (Var x) = f_var x) \<and> |
507 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
503 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
508 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
504 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
509 apply (lifting hom) |
505 apply (lifting hom_res) |
510 done |
506 done |
511 |
507 |
512 (* test test |
508 (* test test |
513 lemma raw_hom_correct: |
509 lemma raw_hom_correct: |
514 assumes f1: "f_var \<in> Respects (op= ===> op=)" |
510 assumes f1: "f_var \<in> Respects (op= ===> op=)" |