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 thm alpha_bn_imps |
|
25 thm distinct |
|
26 thm eq_iff |
|
27 thm fv_defs |
|
28 thm perm_simps |
|
29 thm perm_laws |
|
30 |
|
31 |
24 typ trm |
32 typ trm |
25 typ assg |
33 typ assg |
26 term Var |
34 term Var |
27 term App |
35 term App |
28 term Baz |
36 term Baz |
29 term bn |
37 term bn |
30 term fv_trm |
38 term fv_trm |
31 |
39 term alpha_bn |
32 lemma a1: |
40 |
33 shows "alpha_trm_raw x1 y1 \<Longrightarrow> True" |
41 |
34 and "alpha_assg_raw x2 y2 \<Longrightarrow> alpha_bn_raw x2 y2" |
|
35 and "alpha_bn_raw x3 y3 \<Longrightarrow> True" |
|
36 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
|
37 apply(rule TrueI)+ |
|
38 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
39 sorry |
|
40 |
42 |
41 lemma a2: |
43 lemma a2: |
42 shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1" |
44 shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1" |
43 and "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2" |
45 and "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2" |
44 and "alpha_bn_raw x3 y3 \<Longrightarrow> fv_bn_raw x3 = fv_bn_raw y3" |
46 and "alpha_bn_raw x3 y3 \<Longrightarrow> fv_bn_raw x3 = fv_bn_raw y3" |
45 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
47 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
46 apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) |
48 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) |
47 apply(simp_all only: alphas prod_alpha_def) |
49 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) |
48 apply(auto)[1] |
50 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps) |
49 apply(auto simp add: prod_alpha_def) |
51 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps) |
|
52 -- "" |
|
53 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc) |
|
54 -- "" |
|
55 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps) |
|
56 apply(simp only: Un_assoc set.simps append.simps) |
|
57 apply(simp only: Un_insert_left Un_empty_right Un_empty_left) |
|
58 -- "" |
|
59 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps) |
|
60 apply(simp only: Un_assoc set.simps append.simps) |
|
61 --"" |
|
62 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps) |
|
63 apply(simp only: Un_assoc set.simps append.simps) |
|
64 apply(simp (no_asm) only: simp_thms) |
|
65 --"" |
|
66 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps alphas prod_fv.simps prod_alpha_def ex_simps) |
|
67 apply(simp only: Un_assoc set.simps append.simps) |
50 done |
68 done |
51 |
69 |
52 lemma [quot_respect]: |
70 lemma [quot_respect]: |
53 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
71 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
54 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |
72 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |