equal
deleted
inserted
replaced
19 binder |
19 binder |
20 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
21 where |
21 where |
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
23 |
23 |
|
24 |
|
25 |
24 thm alpha_sym_thms |
26 thm alpha_sym_thms |
25 thm alpha_trans_thms |
27 thm alpha_trans_thms |
26 thm size_eqvt |
28 thm size_eqvt |
27 thm size_simps |
29 thm size_simps |
28 thm size_rsp |
30 thm size_rsp |
32 thm eq_iff_simps |
34 thm eq_iff_simps |
33 thm fv_defs |
35 thm fv_defs |
34 thm perm_simps |
36 thm perm_simps |
35 thm perm_laws |
37 thm perm_laws |
36 thm funs_rsp |
38 thm funs_rsp |
|
39 thm constrs_rsp |
37 |
40 |
38 declare size_rsp[quot_respect] |
41 declare constrs_rsp[quot_respect] |
39 declare funs_rsp[quot_respect] |
42 (* declare funs_rsp[quot_respect] *) |
40 |
43 |
41 typ trm |
44 typ trm |
42 typ assg |
45 typ assg |
43 term Var |
46 term Var |
44 term App |
47 term App |
45 term Baz |
48 term Baz |
46 term bn |
49 term bn |
47 term fv_trm |
50 term fv_trm |
48 term alpha_bn |
51 term alpha_bn |
49 |
|
50 lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto |
|
51 |
|
52 ML {* |
|
53 val pre_ss = @{thms fun_rel_def} |
|
54 val post_ss = @{thms alphas prod_alpha_def prod_rel.simps |
|
55 prod_fv.simps fresh_star_zero permute_zero funs_rsp prod.cases alpha_bn_imps} |
|
56 |
|
57 val tac = |
|
58 asm_full_simp_tac (HOL_ss addsimps pre_ss) |
|
59 THEN' REPEAT o (resolve_tac @{thms allI impI}) |
|
60 THEN' resolve_tac @{thms alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros} |
|
61 THEN_ALL_NEW (TRY o (rtac @{thm exi_zero}) THEN' asm_full_simp_tac (HOL_ss addsimps post_ss)) |
|
62 *} |
|
63 |
|
64 lemma [quot_respect]: |
|
65 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
|
66 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |
|
67 "(op= ===> alpha_trm_raw ===> alpha_trm_raw) Lam_raw Lam_raw" |
|
68 "(alpha_assg_raw ===> alpha_trm_raw ===> alpha_trm_raw) Let_raw Let_raw" |
|
69 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) |
|
70 Foo_raw Foo_raw" |
|
71 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" |
|
72 "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" |
|
73 "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" |
|
74 apply(tactic {* ALLGOALS tac *}) |
|
75 sorry |
|
76 |
52 |
77 lemma [quot_respect]: |
53 lemma [quot_respect]: |
78 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
54 "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute" |
79 apply(simp) |
55 apply(simp) |
80 sorry |
56 sorry |