equal
deleted
inserted
replaced
33 | "bn2 (As x y t) = [atom y]" |
33 | "bn2 (As x y t) = [atom y]" |
34 | "bn3 (As x y t) = [atom x, atom y]" |
34 | "bn3 (As x y t) = [atom x, atom y]" |
35 | "bn4 (BNil) = {}" |
35 | "bn4 (BNil) = {}" |
36 | "bn4 (BAs a as) = {atom a} \<union> bn4 as" |
36 | "bn4 (BAs a as) = {atom a} \<union> bn4 as" |
37 |
37 |
|
38 thm foo.permute_bn |
38 thm foo.perm_bn_alpha |
39 thm foo.perm_bn_alpha |
39 thm foo.perm_bn_simps |
40 thm foo.perm_bn_simps |
40 thm foo.bn_finite |
41 thm foo.bn_finite |
41 |
42 |
42 thm foo.distinct |
43 thm foo.distinct |
52 thm foo.supports |
53 thm foo.supports |
53 thm foo.fsupp |
54 thm foo.fsupp |
54 thm foo.supp |
55 thm foo.supp |
55 thm foo.fresh |
56 thm foo.fresh |
56 thm foo.bn_finite |
57 thm foo.bn_finite |
57 |
|
58 |
|
59 lemma tt1: |
|
60 shows "(p \<bullet> bn1 as) = bn1 (permute_bn1 p as)" |
|
61 apply(induct as rule: foo.inducts(2)) |
|
62 apply(auto)[7] |
|
63 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
|
64 apply(simp add: atom_eqvt) |
|
65 apply(auto) |
|
66 done |
|
67 |
|
68 lemma tt2: |
|
69 shows "(p \<bullet> bn2 as) = bn2 (permute_bn2 p as)" |
|
70 apply(induct as rule: foo.inducts(2)) |
|
71 apply(auto)[7] |
|
72 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
|
73 apply(simp add: atom_eqvt) |
|
74 apply(auto) |
|
75 done |
|
76 |
|
77 lemma tt3: |
|
78 shows "(p \<bullet> bn3 as) = bn3 (permute_bn3 p as)" |
|
79 apply(induct as rule: foo.inducts(2)) |
|
80 apply(auto)[7] |
|
81 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
|
82 apply(simp add: atom_eqvt) |
|
83 apply(auto) |
|
84 done |
|
85 |
|
86 lemma tt4: |
|
87 shows "(p \<bullet> bn4 as) = bn4 (permute_bn4 p as)" |
|
88 apply(induct as rule: foo.inducts(3)) |
|
89 apply(auto)[8] |
|
90 apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq) |
|
91 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
|
92 apply(simp add: atom_eqvt insert_eqvt) |
|
93 done |
|
94 |
58 |
95 lemma strong_exhaust1: |
59 lemma strong_exhaust1: |
96 fixes c::"'a::fs" |
60 fixes c::"'a::fs" |
97 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
61 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
98 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
62 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |