56 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) |
56 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) |
57 Foo_raw Foo_raw" |
57 Foo_raw Foo_raw" |
58 "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw" |
58 "(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" |
59 "(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" |
60 "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw" |
61 apply(auto) |
61 apply(simp only: fun_rel_def) |
62 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
62 apply(rule allI | rule impI)+ |
63 apply(rule refl) |
63 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
64 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
64 apply(assumption) |
65 apply(assumption) |
65 apply(simp only: fun_rel_def) |
66 apply(assumption) |
66 apply(rule allI | rule impI)+ |
|
67 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
68 apply(assumption) |
|
69 apply(assumption) |
|
70 apply(simp only: fun_rel_def) |
|
71 apply(rule allI | rule impI)+ |
67 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
72 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
68 apply(rule_tac x="0" in exI) |
73 apply(rule_tac x="0" in exI) |
69 apply(simp add: alphas fresh_star_def fresh_zero_perm a2) |
74 apply(simp add: alphas fresh_star_def fresh_zero_perm a2) |
70 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
75 apply(simp only: fun_rel_def) |
71 apply(rule_tac x="0" in exI) |
76 apply(rule allI | rule impI)+ |
72 apply(simp add: alphas fresh_star_def fresh_zero_perm a2) |
77 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
73 apply(simp add: a1) |
78 apply(rule_tac x="0" in exI) |
74 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
79 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps) |
75 apply(rule_tac x="0" in exI) |
80 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps) |
76 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
81 apply(simp only: fun_rel_def) |
77 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
82 apply(rule allI | rule impI)+ |
78 apply(rule_tac x="0" in exI) |
83 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
79 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
84 apply(rule_tac x="0" in exI) |
80 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
85 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
81 apply(rule_tac x="0" in exI) |
86 apply(simp only: fun_rel_def) |
82 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
87 apply(rule allI | rule impI)+ |
83 apply(rule_tac x="0" in exI) |
88 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
84 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
89 apply(rule_tac x="0" in exI) |
85 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
90 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
86 apply(rule_tac x="0" in exI) |
91 apply(simp only: fun_rel_def) |
87 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
92 apply(rule allI | rule impI)+ |
88 apply(rule refl) |
93 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
94 apply(rule_tac x="0" in exI) |
|
95 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
96 apply(rule_tac x="0" in exI) |
|
97 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
98 apply(simp only: fun_rel_def) |
|
99 apply(rule allI | rule impI)+ |
|
100 apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros) |
|
101 apply(rule_tac x="0" in exI) |
|
102 apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def) |
|
103 apply(assumption) |
89 done |
104 done |
90 |
105 |
91 lemma [quot_respect]: |
106 lemma [quot_respect]: |
92 "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw" |
107 "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw" |
93 "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw" |
108 "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw" |