180 done |
180 done |
181 have "as \<sharp>* f as x c" by (rule fcb1) |
181 have "as \<sharp>* f as x c" by (rule fcb1) |
182 then have "q \<bullet> (as \<sharp>* f as x c)" |
182 then have "q \<bullet> (as \<sharp>* f as x c)" |
183 by (simp add: permute_bool_def) |
183 by (simp add: permute_bool_def) |
184 then have "(q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
184 then have "(q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
185 apply(simp add: fresh_star_eqvt set_eqvt) |
185 apply(simp only: fresh_star_eqvt set_eqvt) |
186 apply(subst (asm) perm1) |
186 apply(subst (asm) perm1) |
187 using inc fresh1 fr1 |
187 using inc fresh1 fr1 |
188 apply(auto simp add: fresh_star_def fresh_Pair) |
188 apply(auto simp add: fresh_star_def fresh_Pair) |
189 done |
189 done |
190 then have "(r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
190 then have "(r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
191 then have "r \<bullet> (bs \<sharp>* f bs y c)" |
191 then have "r \<bullet> (bs \<sharp>* f bs y c)" |
192 apply(simp add: fresh_star_eqvt set_eqvt) |
192 apply(simp only: fresh_star_eqvt set_eqvt) |
193 apply(subst (asm) perm2[symmetric]) |
193 apply(subst (asm) perm2[symmetric]) |
194 using qq3 fresh2 fr1 |
194 using qq3 fresh2 fr1 |
195 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
195 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
196 done |
196 done |
197 then have fcb2: "bs \<sharp>* f bs y c" by (simp add: permute_bool_def) |
197 then have fcb2: "bs \<sharp>* f bs y c" by (simp add: permute_bool_def) |
262 done |
262 done |
263 have "(as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c" by (rule fcb1) |
263 have "(as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c" by (rule fcb1) |
264 then have "q \<bullet> ((as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c)" |
264 then have "q \<bullet> ((as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c)" |
265 by (simp add: permute_bool_def) |
265 by (simp add: permute_bool_def) |
266 then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c" |
266 then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c" |
267 apply(simp add: fresh_star_eqvt set_eqvt) |
267 apply(simp only: fresh_star_eqvt set_eqvt) |
268 apply(subst (asm) perm1) |
268 apply(subst (asm) perm1) |
269 using inc fresh1 fr1 |
269 using inc fresh1 fr1 |
270 apply(auto simp add: fresh_star_def fresh_Pair) |
270 apply(auto simp add: fresh_star_def fresh_Pair) |
271 done |
271 done |
272 then have "(r \<bullet> (bs \<inter> supp y)) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq1 qq2 |
272 then have "(r \<bullet> (bs \<inter> supp y)) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq1 qq2 |
273 apply(perm_simp) |
273 apply(perm_simp) |
274 apply simp |
274 apply simp |
275 done |
275 done |
276 then have "r \<bullet> ((bs \<inter> supp y) \<sharp>* f (bs \<inter> supp y) y c)" |
276 then have "r \<bullet> ((bs \<inter> supp y) \<sharp>* f (bs \<inter> supp y) y c)" |
277 apply(simp add: fresh_star_eqvt set_eqvt) |
277 apply(simp only: fresh_star_eqvt set_eqvt) |
278 apply(subst (asm) perm2[symmetric]) |
278 apply(subst (asm) perm2[symmetric]) |
279 using qq3 fresh2 fr1 |
279 using qq3 fresh2 fr1 |
280 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
280 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
281 done |
281 done |
282 then have fcb2: "(bs \<inter> supp y) \<sharp>* f (bs \<inter> supp y) y c" by (simp add: permute_bool_def) |
282 then have fcb2: "(bs \<inter> supp y) \<sharp>* f (bs \<inter> supp y) y c" by (simp add: permute_bool_def) |
348 done |
348 done |
349 have "(set as) \<sharp>* f as x c" by (rule fcb1) |
349 have "(set as) \<sharp>* f as x c" by (rule fcb1) |
350 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
350 then have "q \<bullet> ((set as) \<sharp>* f as x c)" |
351 by (simp add: permute_bool_def) |
351 by (simp add: permute_bool_def) |
352 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
352 then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" |
353 apply(simp add: fresh_star_eqvt set_eqvt) |
353 apply(simp only: fresh_star_eqvt set_eqvt) |
354 apply(subst (asm) perm1) |
354 apply(subst (asm) perm1) |
355 using inc fresh1 fr1 |
355 using inc fresh1 fr1 |
356 apply(auto simp add: fresh_star_def fresh_Pair) |
356 apply(auto simp add: fresh_star_def fresh_Pair) |
357 done |
357 done |
358 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
358 then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp |
359 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
359 then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" |
360 apply(simp add: fresh_star_eqvt set_eqvt) |
360 apply(simp only: fresh_star_eqvt set_eqvt) |
361 apply(subst (asm) perm2[symmetric]) |
361 apply(subst (asm) perm2[symmetric]) |
362 using qq3 fresh2 fr1 |
362 using qq3 fresh2 fr1 |
363 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
363 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) |
364 done |
364 done |
365 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |
365 then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) |