equal
deleted
inserted
replaced
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_simps |
27 thm foo.perm_bn_simps |
28 |
28 |
29 |
|
30 thm foo.distinct |
29 thm foo.distinct |
31 thm foo.induct |
30 thm foo.induct |
32 thm foo.inducts |
31 thm foo.inducts |
33 thm foo.exhaust |
32 thm foo.exhaust |
34 thm foo.fv_defs |
33 thm foo.fv_defs |
244 apply(perm_simp) |
243 apply(perm_simp) |
245 apply(erule conjE)+ |
244 apply(erule conjE)+ |
246 apply(rule conjI) |
245 apply(rule conjI) |
247 apply(assumption) |
246 apply(assumption) |
248 apply(simp add: foo.eq_iff) |
247 apply(simp add: foo.eq_iff) |
249 defer |
248 apply(rule at_set_avoiding1) |
|
249 apply(simp) |
|
250 apply(simp add: finite_supp) |
250 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
251 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)") |
251 apply(erule exE) |
252 apply(erule exE) |
252 apply(rule assms(4)) |
253 apply(rule assms(4)) |
253 apply(simp only:) |
254 apply(simp only:) |
254 apply(simp only: foo.eq_iff) |
255 apply(simp only: foo.eq_iff) |
283 apply(rule conjI) |
284 apply(rule conjI) |
284 apply(rule uu1) |
285 apply(rule uu1) |
285 apply(rule conjI) |
286 apply(rule conjI) |
286 apply(assumption) |
287 apply(assumption) |
287 apply(rule uu1) |
288 apply(rule uu1) |
288 defer |
289 apply(rule at_set_avoiding1) |
|
290 apply(simp) |
|
291 apply(simp add: finite_supp) |
289 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)") |
292 apply(subgoal_tac "\<exists>p. (p \<bullet> ({atom name1} \<union> {atom name2})) \<sharp>* (c, atom name1, atom name2, trm1, trm2)") |
290 apply(erule exE) |
293 apply(erule exE) |
291 apply(rule assms(5)) |
294 apply(rule assms(5)) |
292 apply(simp only:) |
295 apply(simp only:) |
293 apply(simp only: foo.eq_iff) |
296 apply(simp only: foo.eq_iff) |
315 apply(rule conjI) |
318 apply(rule conjI) |
316 apply(assumption) |
319 apply(assumption) |
317 apply(assumption) |
320 apply(assumption) |
318 apply(simp add: fresh_star_prod) |
321 apply(simp add: fresh_star_prod) |
319 apply(simp add: fresh_star_def) |
322 apply(simp add: fresh_star_def) |
320 sorry |
323 apply(rule at_set_avoiding1) |
|
324 apply(simp) |
|
325 apply(simp add: finite_supp) |
|
326 done |
321 |
327 |
322 |
328 |
323 |
329 |
324 lemma test5: |
330 lemma test5: |
325 fixes c::"'a::fs" |
331 fixes c::"'a::fs" |