32 lemma a1: |
32 lemma a1: |
33 shows "alpha_trm_raw x1 y1 \<Longrightarrow> True" |
33 shows "alpha_trm_raw x1 y1 \<Longrightarrow> True" |
34 and "alpha_assg_raw x2 y2 \<Longrightarrow> alpha_bn_raw x2 y2" |
34 and "alpha_assg_raw x2 y2 \<Longrightarrow> alpha_bn_raw x2 y2" |
35 and "alpha_bn_raw x3 y3 \<Longrightarrow> True" |
35 and "alpha_bn_raw x3 y3 \<Longrightarrow> True" |
36 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
36 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
37 apply(simp_all) |
37 apply(rule TrueI)+ |
38 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
38 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
39 apply(assumption) |
39 sorry |
40 done |
|
41 |
40 |
42 lemma a2: |
41 lemma a2: |
43 shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1" |
42 shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1" |
44 and "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2" |
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_bn_raw x3 y3 \<Longrightarrow> fv_bn_raw x3 = fv_bn_raw y3" |
44 and "alpha_bn_raw x3 y3 \<Longrightarrow> fv_bn_raw x3 = fv_bn_raw y3" |
46 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
45 apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts) |
47 apply(simp_all add: alphas a1 prod_alpha_def) |
46 apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps) |
48 apply(auto) |
47 apply(simp_all only: alphas prod_alpha_def) |
|
48 apply(auto)[1] |
|
49 apply(auto simp add: prod_alpha_def) |
49 done |
50 done |
50 |
51 |
51 lemma [quot_respect]: |
52 lemma [quot_respect]: |
52 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
53 "(op= ===> alpha_trm_raw) Var_raw Var_raw" |
53 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |
54 "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw" |