equal
deleted
inserted
replaced
4 |
4 |
5 text {* |
5 text {* |
6 Contrived example that has more than one |
6 Contrived example that has more than one |
7 binding function |
7 binding function |
8 *} |
8 *} |
|
9 |
9 |
10 |
10 atom_decl name |
11 atom_decl name |
11 |
12 |
12 nominal_datatype foo: trm = |
13 nominal_datatype foo: trm = |
13 Var "name" |
14 Var "name" |
47 thm foo.size_eqvt |
48 thm foo.size_eqvt |
48 thm foo.supports |
49 thm foo.supports |
49 thm foo.fsupp |
50 thm foo.fsupp |
50 thm foo.supp |
51 thm foo.supp |
51 thm foo.fresh |
52 thm foo.fresh |
|
53 thm foo.bn_finite |
52 |
54 |
53 lemma uu1: |
55 lemma uu1: |
54 shows "alpha_bn1 as (permute_bn1 p as)" |
56 shows "alpha_bn1 as (permute_bn1 p as)" |
55 apply(induct as rule: foo.inducts(2)) |
57 apply(induct as rule: foo.inducts(2)) |
56 apply(auto)[7] |
58 apply(auto)[7] |
122 apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq) |
124 apply(simp add: foo.perm_bn_simps foo.bn_defs permute_set_eq) |
123 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
125 apply(simp add: foo.perm_bn_simps foo.bn_defs) |
124 apply(simp add: atom_eqvt insert_eqvt) |
126 apply(simp add: atom_eqvt insert_eqvt) |
125 done |
127 done |
126 |
128 |
127 lemma bn_finite: |
|
128 shows "(\<lambda>x. True) t" |
|
129 and "finite (set (bn1 as)) \<and> finite (set (bn2 as)) \<and> finite (set (bn3 as))" |
|
130 and "finite (bn4 as')" |
|
131 apply(induct "t::trm" and as and as' rule: foo.inducts) |
|
132 apply(simp_all add: foo.bn_defs) |
|
133 done |
|
134 |
129 |
135 |
130 |
136 lemma strong_exhaust1: |
131 lemma strong_exhaust1: |
137 fixes c::"'a::fs" |
132 fixes c::"'a::fs" |
138 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
133 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
152 apply(erule exE) |
147 apply(erule exE) |
153 apply(erule conjE) |
148 apply(erule conjE) |
154 apply(rule assms(3)) |
149 apply(rule assms(3)) |
155 apply(perm_simp) |
150 apply(perm_simp) |
156 apply(assumption) |
151 apply(assumption) |
|
152 apply(simp) |
157 apply(drule supp_perm_eq[symmetric]) |
153 apply(drule supp_perm_eq[symmetric]) |
158 apply(perm_simp) |
154 apply(perm_simp) |
159 apply(simp) |
155 apply(simp) |
160 apply(rule at_set_avoiding2) |
156 apply(rule at_set_avoiding2) |
161 apply(simp add: finite_supp) |
157 apply(simp add: finite_supp) |
214 apply(simp add: foo.eq_iff) |
210 apply(simp add: foo.eq_iff) |
215 apply(drule supp_perm_eq[symmetric]) |
211 apply(drule supp_perm_eq[symmetric]) |
216 apply(simp) |
212 apply(simp) |
217 apply(simp add: tt4 uu4) |
213 apply(simp add: tt4 uu4) |
218 apply(rule at_set_avoiding2) |
214 apply(rule at_set_avoiding2) |
219 apply(simp add: bn_finite) |
215 apply(simp add: foo.bn_finite) |
220 apply(simp add: finite_supp) |
216 apply(simp add: finite_supp) |
221 apply(simp add: finite_supp) |
217 apply(simp add: finite_supp) |
222 apply(simp add: Abs_fresh_star) |
218 apply(simp add: Abs_fresh_star) |
223 done |
219 done |
|
220 |
224 |
221 |
225 lemma strong_exhaust2: |
222 lemma strong_exhaust2: |
226 assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" |
223 assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" |
227 shows "P" |
224 shows "P" |
228 apply(rule_tac y="as" in foo.exhaust(2)) |
225 apply(rule_tac y="as" in foo.exhaust(2)) |