equal
deleted
inserted
replaced
135 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
135 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
136 apply(induct rule: alpha.induct) |
136 apply(induct rule: alpha.induct) |
137 apply(simp add: a1) |
137 apply(simp add: a1) |
138 apply(simp add: a2) |
138 apply(simp add: a2) |
139 apply(rule a3) |
139 apply(rule a3) |
140 apply(rule alpha_gen_atom_sym) |
140 apply(erule alpha_gen_compose_sym) |
141 apply(rule alpha_eqvt) |
141 apply(erule alpha_eqvt) |
142 apply(assumption)+ |
|
143 done |
142 done |
144 |
143 |
145 lemma alpha_trans: |
144 lemma alpha_trans: |
146 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
145 shows "t1 \<approx> t2 \<Longrightarrow> t2 \<approx> t3 \<Longrightarrow> t1 \<approx> t3" |
147 apply(induct arbitrary: t3 rule: alpha.induct) |
146 apply(induct arbitrary: t3 rule: alpha.induct) |
150 apply(erule alpha.cases) |
149 apply(erule alpha.cases) |
151 apply(simp_all add: a2) |
150 apply(simp_all add: a2) |
152 apply(erule alpha.cases) |
151 apply(erule alpha.cases) |
153 apply(simp_all) |
152 apply(simp_all) |
154 apply(rule a3) |
153 apply(rule a3) |
155 apply(rule alpha_gen_atom_trans) |
154 apply(erule alpha_gen_compose_trans) |
156 apply(rule alpha_eqvt) |
155 apply(assumption) |
157 apply(assumption)+ |
156 apply(erule alpha_eqvt) |
158 done |
157 done |
159 |
158 |
160 lemma alpha_equivp: |
159 lemma alpha_equivp: |
161 shows "equivp alpha" |
160 shows "equivp alpha" |
162 apply(rule equivpI) |
161 apply(rule equivpI) |