120 using assms |
120 using assms |
121 apply(erule_tac alpha.cases) |
121 apply(erule_tac alpha.cases) |
122 apply(auto) |
122 apply(auto) |
123 done |
123 done |
124 |
124 |
|
125 lemma alpha_gen_eqvt_atom: |
|
126 assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
|
127 shows "\<exists>pia. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2) f pia ({atom b}, s) \<Longrightarrow> \<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)" |
|
128 apply(erule exE) |
|
129 apply(rule_tac x="pi \<bullet> pia" in exI) |
|
130 apply(simp add: alpha_gen.simps) |
|
131 apply(erule conjE)+ |
|
132 apply(rule conjI)+ |
|
133 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
134 apply(simp add: a[symmetric] atom_eqvt eqvts) |
|
135 apply(rule conjI) |
|
136 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
137 apply(simp add: a[symmetric] eqvts atom_eqvt) |
|
138 apply(subst permute_eqvt[symmetric]) |
|
139 apply(simp) |
|
140 done |
|
141 |
125 text {* should be automatic with new version of eqvt-machinery *} |
142 text {* should be automatic with new version of eqvt-machinery *} |
126 lemma alpha_eqvt: |
143 lemma alpha_eqvt: |
127 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
144 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
128 apply(induct rule: alpha.induct) |
145 apply(induct rule: alpha.induct) |
129 apply(simp add: a1) |
146 apply(simp add: a1) |
130 apply(simp add: a2) |
147 apply(simp add: a2) |
131 apply(simp) |
148 apply(simp) |
132 apply(rule a3) |
149 apply(rule a3) |
133 apply(erule exE) |
150 apply(rule alpha_gen_eqvt_atom) |
134 apply(rule_tac x="pi \<bullet> pia" in exI) |
151 apply(rule rfv_eqvt) |
135 apply(simp add: alpha_gen.simps) |
152 apply assumption |
136 apply(erule conjE)+ |
|
137 apply(rule conjI)+ |
|
138 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
139 apply(simp add: eqvts atom_eqvt) |
|
140 apply(rule conjI) |
|
141 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
142 apply(simp add: eqvts atom_eqvt) |
|
143 apply(subst permute_eqvt[symmetric]) |
|
144 apply(simp) |
|
145 done |
153 done |
146 |
154 |
147 lemma alpha_refl: |
155 lemma alpha_refl: |
148 shows "t \<approx> t" |
156 shows "t \<approx> t" |
149 apply(induct t rule: rlam.induct) |
157 apply(induct t rule: rlam.induct) |