37 term bn |
38 term bn |
38 term fv_trm |
39 term fv_trm |
39 term alpha_bn |
40 term alpha_bn |
40 |
41 |
41 |
42 |
42 |
|
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_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) |
48 apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps |
|
49 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 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" |
57 Foo_raw Foo_raw" |
58 Foo_raw Foo_raw" |
58 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" |
59 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" |
59 "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" |
60 "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw" |
60 "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" |
61 "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" |
61 apply(simp only: fun_rel_def) |
62 apply(simp only: fun_rel_def) |
62 apply(rule allI | rule impI)+ |
63 apply(simp only: eq_iff) |
63 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
64 apply(simp only: simp_thms) |
64 apply(assumption) |
65 apply(simp only: fun_rel_def) |
65 apply(simp only: fun_rel_def) |
66 apply(simp only: eq_iff) |
66 apply(rule allI | rule impI)+ |
67 apply(tactic {* asm_full_simp_tac HOL_ss 1*}) |
67 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
68 apply(simp only: fun_rel_def) |
68 apply(assumption) |
69 apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2) |
69 apply(assumption) |
70 apply(rule allI | rule impI)+ |
70 apply(simp only: fun_rel_def) |
71 apply(rule_tac x="0" in exI) |
71 apply(rule allI | rule impI)+ |
72 apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2 permute_zero a2) |
72 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
73 apply(simp add: a2) |
73 apply(rule_tac x="0" in exI) |
|
74 apply(simp add: alphas fresh_star_def fresh_zero_perm a2) |
|
75 apply(simp only: fun_rel_def) |
|
76 apply(rule allI | rule impI)+ |
|
77 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
78 apply(rule_tac x="0" in exI) |
|
79 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps) |
|
80 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps) |
74 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps) |
81 apply(simp only: fun_rel_def) |
75 apply(simp only: fun_rel_def) |
82 apply(rule allI | rule impI)+ |
76 apply(rule allI | rule impI)+ |
83 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
77 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
84 apply(rule_tac x="0" in exI) |
78 apply(rule_tac x="0" in exI) |