296 text {* |
296 text {* |
297 tests by cu |
297 tests by cu |
298 *} |
298 *} |
299 |
299 |
300 |
300 |
|
301 thm at_set_avoiding2 supp_perm_eq at_set_avoiding |
|
302 |
|
303 lemma abs_rename_set: |
|
304 fixes x::"'a::fs" |
|
305 assumes "b' \<sharp> x" "sort_of b = sort_of b'" |
|
306 shows "\<exists>y. [{b}]set. x = [{b'}]set. y" |
|
307 apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI) |
|
308 apply(subst Abs_swap1[where a="b" and b="b'"]) |
|
309 apply(simp) |
|
310 using assms |
|
311 apply(simp add: fresh_def) |
|
312 apply(perm_simp) |
|
313 using assms |
|
314 apply(simp) |
|
315 done |
|
316 |
|
317 lemma abs_rename_list: |
|
318 fixes x::"'a::fs" |
|
319 assumes "b' \<sharp> x" "sort_of b = sort_of b'" |
|
320 shows "\<exists>y. [[b]]lst. x = [[b']]lst. y" |
|
321 apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI) |
|
322 apply(subst Abs_swap2[where a="b" and b="b'"]) |
|
323 apply(simp) |
|
324 using assms |
|
325 apply(simp add: fresh_def) |
|
326 apply(perm_simp) |
|
327 using assms |
|
328 apply(simp) |
|
329 done |
|
330 |
301 lemma test3: |
331 lemma test3: |
302 fixes c::"'a::fs" |
332 fixes c::"'a::fs" |
303 assumes a: "y = Let2 x1 x2 trm1 trm2" |
333 assumes a: "y = Let2 x1 x2 trm1 trm2" |
304 and b: "\<forall>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<longrightarrow> P" |
334 and b: "\<forall>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<longrightarrow> P" |
305 shows "P" |
335 shows "P" |
306 using b[simplified a] |
336 using b[simplified a] |
307 apply - |
337 apply - |
308 apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)") |
338 apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)") |
309 apply(erule exE) |
339 apply(erule exE) |
310 apply(drule_tac p="- q" in permute_boolI) |
340 apply(perm_simp) |
311 apply(perm_simp) |
341 apply(drule_tac x="q \<bullet> x1" in spec) |
|
342 apply(drule_tac x="q \<bullet> x2" in spec) |
312 apply(simp only: foo.eq_iff) |
343 apply(simp only: foo.eq_iff) |
313 apply(drule_tac x="x1" in spec) |
344 apply(simp) |
314 apply(drule_tac x="x2" in spec) |
345 apply(erule mp) |
315 apply(simp) |
|
316 apply(drule mp) |
|
317 apply(rule conjI) |
346 apply(rule conjI) |
318 defer |
347 apply(simp add: fresh_star_prod) |
319 apply(rule_tac p="q" in permute_boolE) |
|
320 apply(perm_simp add: permute_minus_cancel) |
|
321 apply(rule conjI) |
348 apply(rule conjI) |
322 prefer 2 |
349 prefer 2 |
323 apply(rule_tac x="(atom x2 \<rightleftharpoons> atom (q \<bullet> x2)) \<bullet> trm2" in exI) |
350 apply(rule abs_rename_list) |
324 apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"]) |
351 apply(simp add: fresh_star_prod) |
325 apply(simp) |
352 apply(simp add: fresh_star_def) |
326 apply(simp add: fresh_star_def) |
|
327 apply(simp add: fresh_def supp_Pair) |
|
328 apply(simp) |
353 apply(simp) |
329 apply(case_tac "x1=x2") |
354 apply(case_tac "x1=x2") |
330 apply(simp) |
355 apply(simp) |
331 apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"]) |
356 apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"]) |
332 apply(simp) |
357 apply(simp) |
361 apply(rule exI) |
386 apply(rule exI) |
362 apply(rule refl) |
387 apply(rule refl) |
363 apply(simp add: fresh_star_def) |
388 apply(simp add: fresh_star_def) |
364 apply(simp add: fresh_def supp_Pair) |
389 apply(simp add: fresh_def supp_Pair) |
365 apply(simp add: supp_at_base) |
390 apply(simp add: supp_at_base) |
366 apply(simp) |
|
367 defer |
|
368 apply(rule_tac p="q" in permute_boolE) |
|
369 apply(perm_simp add: permute_minus_cancel fresh_star_prod) |
|
370 apply(simp) |
|
371 apply(rule at_set_avoiding3[where x="()", simplified]) |
391 apply(rule at_set_avoiding3[where x="()", simplified]) |
372 apply(simp) |
392 apply(simp) |
373 apply(simp add: finite_supp) |
393 apply(simp add: finite_supp) |
374 apply(simp add: finite_supp) |
394 apply(simp add: finite_supp) |
375 apply(simp add: fresh_star_def fresh_Unit) |
395 apply(simp add: fresh_star_def fresh_Unit) |
384 apply(rule a) |
404 apply(rule a) |
385 using b |
405 using b |
386 apply(auto) |
406 apply(auto) |
387 done |
407 done |
388 |
408 |
|
409 lemma test5: |
|
410 fixes c::"'a::fs" |
|
411 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
412 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
413 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
414 and "\<And>assn1 trm1 assn2 trm2. |
|
415 \<lbrakk>((set (bn assn1)) \<union> (set (bn assn2))) \<sharp>* c; y = Let1 assn1 trm1 assn2 trm2\<rbrakk> \<Longrightarrow> P" |
|
416 and "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
|
417 shows "P" |
|
418 apply(rule_tac y="y" in foo.exhaust(1)) |
|
419 apply (erule assms) |
|
420 apply (erule assms) |
|
421 prefer 3 |
|
422 apply(erule test4[where c="c"]) |
|
423 apply (rule assms(5)) |
|
424 apply assumption |
|
425 apply(simp) |
|
426 oops |
|
427 |
389 |
428 |
390 end |
429 end |
391 |
430 |
392 |
431 |
393 |
432 |