equal
deleted
inserted
replaced
22 bn::"assg \<Rightarrow> atom list" |
22 bn::"assg \<Rightarrow> atom list" |
23 where |
23 where |
24 "bn (As x y t a) = [atom x] @ bn a" |
24 "bn (As x y t a) = [atom x] @ bn a" |
25 | "bn (As_Nil) = []" |
25 | "bn (As_Nil) = []" |
26 |
26 |
|
27 thm foo.perm_bn_alpha |
27 thm foo.perm_bn_simps |
28 thm foo.perm_bn_simps |
|
29 thm foo.bn_finite |
28 |
30 |
29 thm foo.distinct |
31 thm foo.distinct |
30 thm foo.induct |
32 thm foo.induct |
31 thm foo.inducts |
33 thm foo.inducts |
32 thm foo.exhaust |
34 thm foo.exhaust |
43 |
45 |
44 lemma uu1: |
46 lemma uu1: |
45 shows "alpha_bn as (permute_bn p as)" |
47 shows "alpha_bn as (permute_bn p as)" |
46 apply(induct as rule: foo.inducts(2)) |
48 apply(induct as rule: foo.inducts(2)) |
47 apply(auto)[5] |
49 apply(auto)[5] |
48 apply(simp add: foo.perm_bn_simps) |
50 apply(simp only: foo.perm_bn_simps) |
49 apply(simp add: foo.eq_iff) |
51 apply(simp only: foo.eq_iff) |
50 apply(simp add: foo.perm_bn_simps) |
52 apply(simp only: foo.perm_bn_simps) |
51 apply(simp add: foo.eq_iff) |
53 apply(simp only: foo.eq_iff refl) |
|
54 apply(simp) |
52 done |
55 done |
53 |
56 |
54 lemma tt1: |
57 lemma tt1: |
55 shows "(p \<bullet> bn as) = bn (permute_bn p as)" |
58 shows "(p \<bullet> bn as) = bn (permute_bn p as)" |
56 apply(induct as rule: foo.inducts(2)) |
59 apply(induct as rule: foo.inducts(2)) |
57 apply(auto)[5] |
60 apply(auto)[5] |
58 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
61 apply(simp only: foo.perm_bn_simps foo.bn_defs) |
59 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
62 apply(perm_simp) |
60 apply(simp add: atom_eqvt) |
63 apply(simp only:) |
|
64 apply(simp only: foo.perm_bn_simps foo.bn_defs) |
|
65 apply(perm_simp add: foo.fv_bn_eqvt) |
|
66 apply(simp only:) |
61 done |
67 done |
62 |
68 |
63 text {* |
69 text {* |
64 tests by cu |
70 tests by cu |
65 *} |
71 *} |