131 |
131 |
132 lemma alpha_gen_atom_eqvt: |
132 lemma alpha_gen_atom_eqvt: |
133 assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
133 assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
134 and b: "\<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)" |
134 and b: "\<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)" |
135 shows "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)" |
135 shows "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)" |
136 using b apply - |
136 using b |
|
137 apply - |
137 apply(erule exE) |
138 apply(erule exE) |
138 apply(rule_tac x="pi \<bullet> pia" in exI) |
139 apply(rule_tac x="pi \<bullet> pia" in exI) |
139 apply(simp add: alpha_gen.simps) |
140 apply(simp add: alpha_gen.simps) |
140 apply(erule conjE)+ |
141 apply(erule conjE)+ |
141 apply(rule conjI) |
142 apply(rule conjI) |
142 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
143 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
143 apply(simp add: a[symmetric] atom_eqvt eqvts) |
144 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) |
144 apply(rule conjI) |
145 apply(rule conjI) |
145 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
146 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
146 apply(simp add: a[symmetric] eqvts atom_eqvt) |
147 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) |
147 apply(subst permute_eqvt[symmetric]) |
148 apply(subst permute_eqvt[symmetric]) |
148 apply(simp) |
149 apply(simp) |
149 done |
150 done |
150 |
151 |
151 |
152 |