111 apply(rotate_tac 6) |
111 apply(rotate_tac 6) |
112 apply(drule_tac pi="pia" in a) |
112 apply(drule_tac pi="pia" in a) |
113 apply(simp) |
113 apply(simp) |
114 done |
114 done |
115 |
115 |
116 lemma alpha_gen_atom_eqvt: |
116 lemma alpha_gen_compose_eqvt: |
117 assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
117 assumes b: "\<exists>pia. (g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)" |
118 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)" |
118 and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)" |
119 shows "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)" |
119 and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
120 using b |
120 shows "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s)" |
|
121 using b |
121 apply - |
122 apply - |
122 apply(erule exE) |
123 apply(erule exE) |
123 apply(rule_tac x="pi \<bullet> pia" in exI) |
124 apply(rule_tac x="pi \<bullet> pia" in exI) |
124 apply(simp add: alpha_gen.simps) |
125 apply(simp add: alpha_gen.simps) |
125 apply(erule conjE)+ |
126 apply(erule conjE)+ |
126 apply(rule conjI) |
127 apply(rule conjI) |
127 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
128 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
128 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) |
129 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
129 apply(rule conjI) |
130 apply(rule conjI) |
130 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
131 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
131 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) |
132 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
132 apply(subst permute_eqvt[symmetric]) |
133 apply(subst permute_eqvt[symmetric]) |
133 apply(simp) |
134 apply(simp) |
134 done |
135 done |
135 |
136 |
136 fun |
137 fun |