equal
deleted
inserted
replaced
40 thm foo.size_eqvt |
40 thm foo.size_eqvt |
41 thm foo.supports |
41 thm foo.supports |
42 thm foo.fsupp |
42 thm foo.fsupp |
43 thm foo.supp |
43 thm foo.supp |
44 thm foo.fresh |
44 thm foo.fresh |
45 |
|
46 lemma uu1: |
|
47 shows "alpha_bn as (permute_bn p as)" |
|
48 apply(induct as rule: foo.inducts(2)) |
|
49 apply(auto)[5] |
|
50 apply(simp only: foo.perm_bn_simps) |
|
51 apply(simp only: foo.eq_iff) |
|
52 apply(simp only: foo.perm_bn_simps) |
|
53 apply(simp only: foo.eq_iff refl) |
|
54 apply(simp) |
|
55 done |
|
56 |
45 |
57 lemma tt1: |
46 lemma tt1: |
58 shows "(p \<bullet> bn as) = bn (permute_bn p as)" |
47 shows "(p \<bullet> bn as) = bn (permute_bn p as)" |
59 apply(induct as rule: foo.inducts(2)) |
48 apply(induct as rule: foo.inducts(2)) |
60 apply(auto)[5] |
49 apply(auto)[5] |
284 apply(rotate_tac 4) |
273 apply(rotate_tac 4) |
285 apply(assumption) |
274 apply(assumption) |
286 apply(rule conjI) |
275 apply(rule conjI) |
287 apply(assumption) |
276 apply(assumption) |
288 apply(rule conjI) |
277 apply(rule conjI) |
289 apply(rule uu1) |
278 apply(rule foo.perm_bn_alpha) |
290 apply(rule conjI) |
279 apply(rule conjI) |
291 apply(assumption) |
280 apply(assumption) |
292 apply(rule uu1) |
281 apply(rule foo.perm_bn_alpha) |
293 apply(rule at_set_avoiding1) |
282 apply(rule at_set_avoiding1) |
294 apply(simp) |
283 apply(simp) |
295 apply(simp add: finite_supp) |
284 apply(simp add: finite_supp) |
296 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)") |
285 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)") |
297 apply(erule exE) |
286 apply(erule exE) |
346 apply(rule assms(1)) |
335 apply(rule assms(1)) |
347 apply(assumption) |
336 apply(assumption) |
348 apply(erule exE)+ |
337 apply(erule exE)+ |
349 apply(rule assms(2)) |
338 apply(rule assms(2)) |
350 apply(assumption) |
339 apply(assumption) |
351 apply(erule exE)+ |
|
352 apply(rule assms(3)) |
340 apply(rule assms(3)) |
353 apply(auto)[2] |
341 apply(auto)[2] |
354 apply(erule exE)+ |
342 apply(erule exE)+ |
355 apply(rule assms(4)) |
343 apply(rule assms(4)) |
356 apply(auto)[2] |
344 apply(auto)[2] |