201 apply (simp only: eq_iff) |
201 apply (simp only: eq_iff) |
202 apply (simp add: alpha_perm_bn) |
202 apply (simp add: alpha_perm_bn) |
203 apply (rule_tac x="q" in exI) |
203 apply (rule_tac x="q" in exI) |
204 apply (simp add: alphas) |
204 apply (simp add: alphas) |
205 apply (simp add: perm_bv2[symmetric]) |
205 apply (simp add: perm_bv2[symmetric]) |
206 apply (simp add: eqvts[symmetric]) |
|
207 apply (simp add: supp_abs) |
206 apply (simp add: supp_abs) |
208 apply (simp add: fv_supp) |
207 apply (simp add: fv_supp) |
|
208 apply (simp add: supp_eqvt[symmetric] set_eqvt[symmetric] Diff_eqvt[symmetric]) |
209 apply (rule supp_perm_eq[symmetric]) |
209 apply (rule supp_perm_eq[symmetric]) |
210 apply (subst supp_finite_atom_set) |
210 apply (subst supp_finite_atom_set) |
211 apply (rule finite_Diff) |
211 apply (rule finite_Diff) |
212 apply (simp add: finite_supp) |
212 apply (simp add: finite_supp) |
213 apply (assumption) |
213 apply (assumption) |
393 apply (rule_tac x="-pa" in exI) |
393 apply (rule_tac x="-pa" in exI) |
394 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
394 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
395 apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}" |
395 apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}" |
396 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
396 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
397 apply (simp add: eqvts) |
397 apply (simp add: eqvts) |
398 apply (simp add: eqvts[symmetric]) |
398 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
399 apply (rule conjI) |
399 apply (rule conjI) |
400 apply (rule supp_perm_eq) |
400 apply (rule supp_perm_eq) |
401 apply (simp add: eqvts) |
401 apply (simp add: eqvts) |
402 apply (subst supp_finite_atom_set) |
402 apply (subst supp_finite_atom_set) |
403 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
403 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
404 apply (simp add: eqvts) |
|
405 apply (simp add: eqvts) |
404 apply (simp add: eqvts) |
406 apply (subst supp_perm_eq) |
405 apply (subst supp_perm_eq) |
407 apply (subst supp_finite_atom_set) |
406 apply (subst supp_finite_atom_set) |
408 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
407 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
409 apply (simp add: eqvts) |
|
410 apply assumption |
408 apply assumption |
411 apply (simp add: fresh_star_minus_perm) |
409 apply (simp add: fresh_star_minus_perm) |
412 apply (rule a08) |
410 apply (rule a08) |
413 apply simp |
411 apply simp |
414 apply(rotate_tac 1) |
412 apply(rotate_tac 1) |
433 apply (rule_tac x="-pa" in exI) |
431 apply (rule_tac x="-pa" in exI) |
434 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
432 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
435 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}" |
433 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}" |
436 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst) |
434 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom cvar})" in subst) |
437 apply (simp add: eqvts) |
435 apply (simp add: eqvts) |
438 apply (simp add: eqvts[symmetric]) |
436 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
439 apply (rule conjI) |
437 apply (rule conjI) |
440 apply (rule supp_perm_eq) |
438 apply (rule supp_perm_eq) |
441 apply (simp add: eqvts) |
439 apply (simp add: eqvts) |
442 apply (subst supp_finite_atom_set) |
440 apply (subst supp_finite_atom_set) |
443 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
441 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
444 apply (simp add: eqvts) |
|
445 apply (simp add: eqvts) |
442 apply (simp add: eqvts) |
446 apply (subst supp_perm_eq) |
443 apply (subst supp_perm_eq) |
447 apply (subst supp_finite_atom_set) |
444 apply (subst supp_finite_atom_set) |
448 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
445 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
449 apply (simp add: eqvts) |
|
450 apply assumption |
446 apply assumption |
451 apply (simp add: fresh_star_minus_perm) |
447 apply (simp add: fresh_star_minus_perm) |
452 apply (rule a15) |
448 apply (rule a15) |
453 apply simp |
449 apply simp |
454 apply(rotate_tac 1) |
450 apply(rotate_tac 1) |
474 apply (rule_tac x="-pa" in exI) |
470 apply (rule_tac x="-pa" in exI) |
475 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
471 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
476 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
472 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}" |
477 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
473 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst) |
478 apply (simp add: eqvts) |
474 apply (simp add: eqvts) |
479 apply (simp add: eqvts[symmetric]) |
475 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
480 apply (rule conjI) |
476 apply (rule conjI) |
481 apply (rule supp_perm_eq) |
477 apply (rule supp_perm_eq) |
482 apply (simp add: eqvts) |
478 apply (simp add: eqvts) |
483 apply (subst supp_finite_atom_set) |
479 apply (subst supp_finite_atom_set) |
484 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
480 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
485 apply (simp add: eqvts) |
|
486 apply (simp add: eqvts) |
481 apply (simp add: eqvts) |
487 apply (subst supp_perm_eq) |
482 apply (subst supp_perm_eq) |
488 apply (subst supp_finite_atom_set) |
483 apply (subst supp_finite_atom_set) |
489 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
484 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
490 apply (simp add: eqvts) |
|
491 apply assumption |
485 apply assumption |
492 apply (simp add: fresh_star_minus_perm) |
486 apply (simp add: fresh_star_minus_perm) |
493 apply (rule a29) |
487 apply (rule a29) |
494 apply simp |
488 apply simp |
495 apply(rotate_tac 1) |
489 apply(rotate_tac 1) |
514 apply (rule_tac x="-pa" in exI) |
508 apply (rule_tac x="-pa" in exI) |
515 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
509 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
516 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}" |
510 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}" |
517 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst) |
511 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom cvar})" in subst) |
518 apply (simp add: eqvts) |
512 apply (simp add: eqvts) |
519 apply (simp add: eqvts[symmetric]) |
513 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
520 apply (rule conjI) |
514 apply (rule conjI) |
521 apply (rule supp_perm_eq) |
515 apply (rule supp_perm_eq) |
522 apply (simp add: eqvts) |
516 apply (simp add: eqvts) |
523 apply (subst supp_finite_atom_set) |
517 apply (subst supp_finite_atom_set) |
524 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
518 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
525 apply (simp add: eqvts) |
|
526 apply (simp add: eqvts) |
519 apply (simp add: eqvts) |
527 apply (subst supp_perm_eq) |
520 apply (subst supp_perm_eq) |
528 apply (subst supp_finite_atom_set) |
521 apply (subst supp_finite_atom_set) |
529 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
522 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
530 apply (simp add: eqvts) |
|
531 apply assumption |
523 apply assumption |
532 apply (simp add: fresh_star_minus_perm) |
524 apply (simp add: fresh_star_minus_perm) |
533 apply (rule a30) |
525 apply (rule a30) |
534 apply simp |
526 apply simp |
535 apply(rotate_tac 1) |
527 apply(rotate_tac 1) |
555 apply (rule_tac x="-pa" in exI) |
547 apply (rule_tac x="-pa" in exI) |
556 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
548 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
557 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}" |
549 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}" |
558 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst) |
550 and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom var})" in subst) |
559 apply (simp add: eqvts) |
551 apply (simp add: eqvts) |
560 apply (simp add: eqvts[symmetric]) |
552 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
561 apply (rule conjI) |
553 apply (rule conjI) |
562 apply (rule supp_perm_eq) |
554 apply (rule supp_perm_eq) |
563 apply (simp add: eqvts) |
555 apply (simp add: eqvts) |
564 apply (subst supp_finite_atom_set) |
556 apply (subst supp_finite_atom_set) |
565 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
557 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
566 apply (simp add: eqvts) |
|
567 apply (simp add: eqvts) |
558 apply (simp add: eqvts) |
568 apply (subst supp_perm_eq) |
559 apply (subst supp_perm_eq) |
569 apply (subst supp_finite_atom_set) |
560 apply (subst supp_finite_atom_set) |
570 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
561 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
571 apply (simp add: eqvts) |
|
572 apply assumption |
562 apply assumption |
573 apply (simp add: fresh_star_minus_perm) |
563 apply (simp add: fresh_star_minus_perm) |
574 apply (rule a32) |
564 apply (rule a32) |
575 apply simp |
565 apply simp |
576 apply(rotate_tac 1) |
566 apply(rotate_tac 1) |
596 apply (rule_tac x="-pa" in exI) |
586 apply (rule_tac x="-pa" in exI) |
597 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
587 apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp) |
598 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}" |
588 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}" |
599 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst) |
589 and s="pa \<bullet> (p \<bullet> supp trm2 - {p \<bullet> atom var})" in subst) |
600 apply (simp add: eqvts) |
590 apply (simp add: eqvts) |
601 apply (simp add: eqvts[symmetric]) |
591 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric]) |
602 apply (rule conjI) |
592 apply (rule conjI) |
603 apply (rule supp_perm_eq) |
593 apply (rule supp_perm_eq) |
604 apply (simp add: eqvts) |
594 apply (simp add: eqvts) |
605 apply (subst supp_finite_atom_set) |
595 apply (subst supp_finite_atom_set) |
606 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
596 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
607 apply (simp add: eqvts) |
|
608 apply (simp add: eqvts) |
597 apply (simp add: eqvts) |
609 apply (subst supp_perm_eq) |
598 apply (subst supp_perm_eq) |
610 apply (subst supp_finite_atom_set) |
599 apply (subst supp_finite_atom_set) |
611 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
600 apply (simp add: supp_eqvt[symmetric] atom_eqvt[symmetric] Diff_eqvt[symmetric] finite_eqvt[symmetric] finite_supp True_eqvt) |
612 apply (simp add: eqvts) |
|
613 apply assumption |
601 apply assumption |
614 apply (simp add: fresh_star_minus_perm) |
602 apply (simp add: fresh_star_minus_perm) |
615 apply (rule a34) |
603 apply (rule a34) |
616 apply simp |
604 apply simp |
617 apply simp |
605 apply simp |
657 |
645 |
658 (* this should not be an equivariance rule *) |
646 (* this should not be an equivariance rule *) |
659 (* for the moment, we force it to be *) |
647 (* for the moment, we force it to be *) |
660 |
648 |
661 (*declare permute_pure[eqvt]*) |
649 (*declare permute_pure[eqvt]*) |
662 (*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *) |
650 (*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} *) |
663 |
651 |
664 thm eqvts |
652 thm eqvts |
665 thm eqvts_raw |
653 thm eqvts_raw |
666 |
654 |
667 declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt] |
655 declare permute_tkind_raw_permute_ckind_raw_permute_ty_raw_permute_ty_lst_raw_permute_co_raw_permute_co_lst_raw_permute_trm_raw_permute_assoc_lst_raw_permute_pat_raw_permute_vars_raw_permute_tvars_raw_permute_cvars_raw.simps[eqvt] |
668 declare alpha_gen_eqvt[eqvt] |
|
669 |
656 |
670 equivariance alpha_tkind_raw |
657 equivariance alpha_tkind_raw |
671 |
658 |
672 thm eqvts |
659 thm eqvts |
673 thm eqvts_raw |
660 thm eqvts_raw |