43 lemma a2: |
43 lemma a2: |
44 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" |
45 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" |
46 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" |
47 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) |
48 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) |
48 apply(simp_all 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 Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms) |
49 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) |
|
50 apply(simp only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps alphas prod_alpha_def ex_simps) |
|
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) |
|
68 done |
49 done |
69 |
50 |
70 lemma [quot_respect]: |
51 lemma [quot_respect]: |
71 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
52 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
72 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |
53 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |