| changeset 2733 | 5f6fefdbf055 |
| parent 2732 | 9abc4a70540c |
| child 2735 | d97e04126a3d |
| 2732:9abc4a70540c | 2733:5f6fefdbf055 |
|---|---|
6 *) |
6 *) |
7 theory Nominal2_Base |
7 theory Nominal2_Base |
8 imports Main |
8 imports Main |
9 "~~/src/HOL/Library/Infinite_Set" |
9 "~~/src/HOL/Library/Infinite_Set" |
10 "~~/src/HOL/Quotient_Examples/FSet" |
10 "~~/src/HOL/Quotient_Examples/FSet" |
11 uses ("nominal_library.ML") |
11 uses ("nominal_basics.ML") |
12 ("nominal_thmdecls.ML") |
|
13 ("nominal_permeq.ML") |
|
14 ("nominal_library.ML") |
|
12 ("nominal_atoms.ML") |
15 ("nominal_atoms.ML") |
16 ("nominal_eqvt.ML") |
|
13 begin |
17 begin |
14 |
18 |
15 section {* Atoms and Sorts *} |
19 section {* Atoms and Sorts *} |
16 |
20 |
17 text {* A simple implementation for atom_sorts is strings. *} |
21 text {* A simple implementation for atom_sorts is strings. *} |
435 apply(simp_all add: permute_bool_def) |
439 apply(simp_all add: permute_bool_def) |
436 done |
440 done |
437 |
441 |
438 end |
442 end |
439 |
443 |
440 lemma Not_eqvt: |
|
441 shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))" |
|
442 by (simp add: permute_bool_def) |
|
443 |
|
444 lemma conj_eqvt: |
|
445 shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))" |
|
446 by (simp add: permute_bool_def) |
|
447 |
|
448 lemma imp_eqvt: |
|
449 shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))" |
|
450 by (simp add: permute_bool_def) |
|
451 |
|
452 lemma ex_eqvt: |
|
453 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
|
454 unfolding permute_fun_def permute_bool_def |
|
455 by (auto, rule_tac x="p \<bullet> x" in exI, simp) |
|
456 |
|
457 lemma all_eqvt: |
|
458 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
|
459 unfolding permute_fun_def permute_bool_def |
|
460 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
|
461 |
|
462 lemma ex1_eqvt: |
|
463 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)" |
|
464 unfolding Ex1_def |
|
465 apply(simp add: ex_eqvt) |
|
466 unfolding permute_fun_def |
|
467 apply(simp add: conj_eqvt all_eqvt) |
|
468 unfolding permute_fun_def |
|
469 apply(simp add: imp_eqvt permute_bool_def) |
|
470 done |
|
471 |
|
472 lemma permute_boolE: |
444 lemma permute_boolE: |
473 fixes P::"bool" |
445 fixes P::"bool" |
474 shows "p \<bullet> P \<Longrightarrow> P" |
446 shows "p \<bullet> P \<Longrightarrow> P" |
475 by (simp add: permute_bool_def) |
447 by (simp add: permute_bool_def) |
476 |
448 |
539 lemma mem_permute_iff: |
511 lemma mem_permute_iff: |
540 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
512 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
541 unfolding mem_def permute_fun_def permute_bool_def |
513 unfolding mem_def permute_fun_def permute_bool_def |
542 by simp |
514 by simp |
543 |
515 |
544 lemma mem_eqvt: |
|
545 shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)" |
|
546 unfolding mem_def |
|
547 by (simp add: permute_fun_app_eq) |
|
548 |
|
549 lemma empty_eqvt: |
516 lemma empty_eqvt: |
550 shows "p \<bullet> {} = {}" |
517 shows "p \<bullet> {} = {}" |
551 unfolding empty_def Collect_def |
518 unfolding empty_def Collect_def |
552 by (simp add: permute_fun_def permute_bool_def) |
519 by (simp add: permute_fun_def permute_bool_def) |
553 |
520 |
554 lemma insert_eqvt: |
521 lemma insert_eqvt: |
555 shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)" |
522 shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)" |
556 unfolding permute_set_eq_image image_insert .. |
523 unfolding permute_set_eq_image image_insert .. |
557 |
|
558 lemma Collect_eqvt: |
|
559 shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}" |
|
560 unfolding Collect_def permute_fun_def .. |
|
561 |
|
562 lemma inter_eqvt: |
|
563 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
|
564 unfolding Int_def |
|
565 apply(simp add: Collect_eqvt) |
|
566 apply(simp add: permute_fun_def) |
|
567 apply(simp add: conj_eqvt) |
|
568 apply(simp add: mem_eqvt) |
|
569 apply(simp add: permute_fun_def) |
|
570 done |
|
571 |
|
572 |
|
573 |
524 |
574 subsection {* Permutations for units *} |
525 subsection {* Permutations for units *} |
575 |
526 |
576 instantiation unit :: pt |
527 instantiation unit :: pt |
577 begin |
528 begin |
633 |
584 |
634 lemma set_eqvt: |
585 lemma set_eqvt: |
635 shows "p \<bullet> (set xs) = set (p \<bullet> xs)" |
586 shows "p \<bullet> (set xs) = set (p \<bullet> xs)" |
636 by (induct xs) (simp_all add: empty_eqvt insert_eqvt) |
587 by (induct xs) (simp_all add: empty_eqvt insert_eqvt) |
637 |
588 |
589 |
|
590 |
|
638 subsection {* Permutations for options *} |
591 subsection {* Permutations for options *} |
639 |
592 |
640 instantiation option :: (pt) pt |
593 instantiation option :: (pt) pt |
641 begin |
594 begin |
642 |
595 |
652 end |
605 end |
653 |
606 |
654 |
607 |
655 subsection {* Permutations for fsets *} |
608 subsection {* Permutations for fsets *} |
656 |
609 |
610 |
|
611 |
|
657 lemma permute_fset_rsp[quot_respect]: |
612 lemma permute_fset_rsp[quot_respect]: |
658 shows "(op = ===> list_eq ===> list_eq) permute permute" |
613 shows "(op = ===> list_eq ===> list_eq) permute permute" |
659 unfolding fun_rel_def |
614 unfolding fun_rel_def |
660 by (simp add: set_eqvt[symmetric]) |
615 by (simp add: set_eqvt[symmetric]) |
661 |
616 |
680 fixes S::"('a::pt) fset" |
635 fixes S::"('a::pt) fset" |
681 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
636 shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)" |
682 and "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)" |
637 and "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)" |
683 by (lifting permute_list.simps) |
638 by (lifting permute_list.simps) |
684 |
639 |
685 |
640 lemma fset_eqvt: |
641 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
|
642 by (lifting set_eqvt) |
|
686 |
643 |
687 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *} |
644 subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *} |
688 |
645 |
689 instantiation char :: pt |
646 instantiation char :: pt |
690 begin |
647 begin |
759 instance nat :: pure |
716 instance nat :: pure |
760 proof qed (rule permute_nat_def) |
717 proof qed (rule permute_nat_def) |
761 |
718 |
762 instance int :: pure |
719 instance int :: pure |
763 proof qed (rule permute_int_def) |
720 proof qed (rule permute_int_def) |
721 |
|
722 |
|
723 |
|
724 subsection {* Basic functions about permutations *} |
|
725 |
|
726 use "nominal_basics.ML" |
|
727 |
|
728 |
|
729 subsection {* Equivariance infrastructure *} |
|
730 |
|
731 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *} |
|
732 |
|
733 use "nominal_thmdecls.ML" |
|
734 setup "Nominal_ThmDecls.setup" |
|
735 |
|
736 |
|
737 lemmas [eqvt] = |
|
738 (* permutations *) |
|
739 uminus_eqvt add_perm_eqvt swap_eqvt |
|
740 |
|
741 (* datatypes *) |
|
742 Pair_eqvt |
|
743 permute_list.simps |
|
744 permute_option.simps |
|
745 permute_sum.simps |
|
746 |
|
747 (* sets *) |
|
748 empty_eqvt insert_eqvt set_eqvt |
|
749 |
|
750 (* fsets *) |
|
751 permute_fset fset_eqvt |
|
752 |
|
753 |
|
754 |
|
755 subsection {* perm_simp infrastructure *} |
|
756 |
|
757 definition |
|
758 "unpermute p = permute (- p)" |
|
759 |
|
760 lemma eqvt_apply: |
|
761 fixes f :: "'a::pt \<Rightarrow> 'b::pt" |
|
762 and x :: "'a::pt" |
|
763 shows "p \<bullet> (f x) \<equiv> (p \<bullet> f) (p \<bullet> x)" |
|
764 unfolding permute_fun_def by simp |
|
765 |
|
766 lemma eqvt_lambda: |
|
767 fixes f :: "'a::pt \<Rightarrow> 'b::pt" |
|
768 shows "p \<bullet> (\<lambda>x. f x) \<equiv> (\<lambda>x. p \<bullet> (f (unpermute p x)))" |
|
769 unfolding permute_fun_def unpermute_def by simp |
|
770 |
|
771 lemma eqvt_bound: |
|
772 shows "p \<bullet> unpermute p x \<equiv> x" |
|
773 unfolding unpermute_def by simp |
|
774 |
|
775 text {* provides perm_simp methods *} |
|
776 |
|
777 use "nominal_permeq.ML" |
|
778 setup Nominal_Permeq.setup |
|
779 |
|
780 method_setup perm_simp = |
|
781 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *} |
|
782 {* pushes permutations inside. *} |
|
783 |
|
784 method_setup perm_strict_simp = |
|
785 {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_strict_simp_meth *} |
|
786 {* pushes permutations inside, raises an error if it cannot solve all permutations. *} |
|
787 |
|
788 (* the normal version of this lemma would cause loops *) |
|
789 lemma permute_eqvt_raw[eqvt_raw]: |
|
790 shows "p \<bullet> permute \<equiv> permute" |
|
791 apply(simp add: fun_eq_iff permute_fun_def) |
|
792 apply(subst permute_eqvt) |
|
793 apply(simp) |
|
794 done |
|
795 |
|
796 subsubsection {* Equivariance of Logical Operators *} |
|
797 |
|
798 lemma eq_eqvt [eqvt]: |
|
799 shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)" |
|
800 unfolding permute_eq_iff permute_bool_def .. |
|
801 |
|
802 lemma Not_eqvt [eqvt]: |
|
803 shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))" |
|
804 by (simp add: permute_bool_def) |
|
805 |
|
806 lemma conj_eqvt [eqvt]: |
|
807 shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))" |
|
808 by (simp add: permute_bool_def) |
|
809 |
|
810 lemma imp_eqvt [eqvt]: |
|
811 shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))" |
|
812 by (simp add: permute_bool_def) |
|
813 |
|
814 declare imp_eqvt[folded induct_implies_def, eqvt] |
|
815 |
|
816 lemma ex_eqvt [eqvt]: |
|
817 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)" |
|
818 unfolding permute_fun_def permute_bool_def |
|
819 by (auto, rule_tac x="p \<bullet> x" in exI, simp) |
|
820 |
|
821 lemma all_eqvt [eqvt]: |
|
822 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)" |
|
823 unfolding permute_fun_def permute_bool_def |
|
824 by (auto, drule_tac x="p \<bullet> x" in spec, simp) |
|
825 |
|
826 declare all_eqvt[folded induct_forall_def, eqvt] |
|
827 |
|
828 lemma ex1_eqvt [eqvt]: |
|
829 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)" |
|
830 unfolding Ex1_def |
|
831 by (perm_simp) (rule refl) |
|
832 |
|
833 lemma mem_eqvt [eqvt]: |
|
834 shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)" |
|
835 unfolding mem_def |
|
836 by (simp add: permute_fun_app_eq) |
|
837 |
|
838 lemma Collect_eqvt [eqvt]: |
|
839 shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}" |
|
840 unfolding Collect_def permute_fun_def .. |
|
841 |
|
842 |
|
843 |
|
844 lemma inter_eqvt [eqvt]: |
|
845 shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)" |
|
846 unfolding Int_def |
|
847 by (perm_simp) (rule refl) |
|
848 |
|
849 lemma image_eqvt [eqvt]: |
|
850 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
|
851 unfolding permute_set_eq_image |
|
852 unfolding permute_fun_def [where f=f] |
|
853 by (simp add: image_image) |
|
854 |
|
855 lemma if_eqvt [eqvt]: |
|
856 shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)" |
|
857 by (simp add: permute_fun_def permute_bool_def) |
|
858 |
|
859 lemma True_eqvt [eqvt]: |
|
860 shows "p \<bullet> True = True" |
|
861 unfolding permute_bool_def .. |
|
862 |
|
863 lemma False_eqvt [eqvt]: |
|
864 shows "p \<bullet> False = False" |
|
865 unfolding permute_bool_def .. |
|
866 |
|
867 lemma disj_eqvt [eqvt]: |
|
868 shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))" |
|
869 by (simp add: permute_bool_def) |
|
870 |
|
871 lemma all_eqvt2: |
|
872 shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))" |
|
873 by (perm_simp add: permute_minus_cancel) (rule refl) |
|
874 |
|
875 lemma ex_eqvt2: |
|
876 shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))" |
|
877 by (perm_simp add: permute_minus_cancel) (rule refl) |
|
878 |
|
879 lemma ex1_eqvt2: |
|
880 shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. p \<bullet> P (- p \<bullet> x))" |
|
881 by (perm_simp add: permute_minus_cancel) (rule refl) |
|
882 |
|
883 lemma the_eqvt: |
|
884 assumes unique: "\<exists>!x. P x" |
|
885 shows "(p \<bullet> (THE x. P x)) = (THE x. (p \<bullet> P) x)" |
|
886 apply(rule the1_equality [symmetric]) |
|
887 apply(rule_tac p="-p" in permute_boolE) |
|
888 apply(perm_simp add: permute_minus_cancel) |
|
889 apply(rule unique) |
|
890 apply(rule_tac p="-p" in permute_boolE) |
|
891 apply(perm_simp add: permute_minus_cancel) |
|
892 apply(rule theI'[OF unique]) |
|
893 done |
|
894 |
|
895 lemma the_eqvt2: |
|
896 assumes unique: "\<exists>!x. P x" |
|
897 shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))" |
|
898 apply(rule the1_equality [symmetric]) |
|
899 apply(simp add: ex1_eqvt2[symmetric]) |
|
900 apply(simp add: permute_bool_def unique) |
|
901 apply(simp add: permute_bool_def) |
|
902 apply(rule theI'[OF unique]) |
|
903 done |
|
904 |
|
905 subsubsection {* Equivariance Set Operations *} |
|
906 |
|
907 lemma Bex_eqvt[eqvt]: |
|
908 shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
|
909 unfolding Bex_def |
|
910 by (perm_simp) (rule refl) |
|
911 |
|
912 lemma Ball_eqvt[eqvt]: |
|
913 shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)" |
|
914 unfolding Ball_def |
|
915 by (perm_simp) (rule refl) |
|
916 |
|
917 lemma UNIV_eqvt[eqvt]: |
|
918 shows "p \<bullet> UNIV = UNIV" |
|
919 unfolding UNIV_def |
|
920 by (perm_simp) (rule refl) |
|
921 |
|
922 lemma union_eqvt[eqvt]: |
|
923 shows "p \<bullet> (A \<union> B) = (p \<bullet> A) \<union> (p \<bullet> B)" |
|
924 unfolding Un_def |
|
925 by (perm_simp) (rule refl) |
|
926 |
|
927 lemma Diff_eqvt[eqvt]: |
|
928 fixes A B :: "'a::pt set" |
|
929 shows "p \<bullet> (A - B) = p \<bullet> A - p \<bullet> B" |
|
930 unfolding set_diff_eq |
|
931 by (perm_simp) (rule refl) |
|
932 |
|
933 lemma Compl_eqvt[eqvt]: |
|
934 fixes A :: "'a::pt set" |
|
935 shows "p \<bullet> (- A) = - (p \<bullet> A)" |
|
936 unfolding Compl_eq_Diff_UNIV |
|
937 by (perm_simp) (rule refl) |
|
938 |
|
939 lemma subset_eqvt[eqvt]: |
|
940 shows "p \<bullet> (S \<subseteq> T) \<longleftrightarrow> (p \<bullet> S) \<subseteq> (p \<bullet> T)" |
|
941 unfolding subset_eq |
|
942 by (perm_simp) (rule refl) |
|
943 |
|
944 lemma psubset_eqvt[eqvt]: |
|
945 shows "p \<bullet> (S \<subset> T) \<longleftrightarrow> (p \<bullet> S) \<subset> (p \<bullet> T)" |
|
946 unfolding psubset_eq |
|
947 by (perm_simp) (rule refl) |
|
948 |
|
949 lemma vimage_eqvt[eqvt]: |
|
950 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
|
951 unfolding vimage_def |
|
952 by (perm_simp) (rule refl) |
|
953 |
|
954 lemma Union_eqvt[eqvt]: |
|
955 shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)" |
|
956 unfolding Union_eq |
|
957 by (perm_simp) (rule refl) |
|
958 |
|
959 lemma Sigma_eqvt: |
|
960 shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)" |
|
961 unfolding Sigma_def |
|
962 unfolding UNION_eq_Union_image |
|
963 by (perm_simp) (rule refl) |
|
964 |
|
965 lemma finite_permute_iff: |
|
966 shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" |
|
967 unfolding permute_set_eq_vimage |
|
968 using bij_permute by (rule finite_vimage_iff) |
|
969 |
|
970 lemma finite_eqvt[eqvt]: |
|
971 shows "p \<bullet> finite A = finite (p \<bullet> A)" |
|
972 unfolding finite_permute_iff permute_bool_def .. |
|
973 |
|
974 |
|
975 subsubsection {* Product Operations *} |
|
976 |
|
977 lemma fst_eqvt[eqvt]: |
|
978 "p \<bullet> (fst x) = fst (p \<bullet> x)" |
|
979 by (cases x) simp |
|
980 |
|
981 lemma snd_eqvt[eqvt]: |
|
982 "p \<bullet> (snd x) = snd (p \<bullet> x)" |
|
983 by (cases x) simp |
|
984 |
|
985 lemma split_eqvt[eqvt]: |
|
986 shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)" |
|
987 unfolding split_def |
|
988 by (perm_simp) (rule refl) |
|
989 |
|
990 |
|
991 |
|
764 |
992 |
765 subsection {* Supp, Freshness and Supports *} |
993 subsection {* Supp, Freshness and Supports *} |
766 |
994 |
767 context pt |
995 context pt |
768 begin |
996 begin |
841 also have "\<dots> \<longleftrightarrow> a \<sharp> x" |
1069 also have "\<dots> \<longleftrightarrow> a \<sharp> x" |
842 unfolding fresh_def supp_def by simp |
1070 unfolding fresh_def supp_def by simp |
843 finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" . |
1071 finally show "(p \<bullet> a) \<sharp> (p \<bullet> x) \<longleftrightarrow> a \<sharp> x" . |
844 qed |
1072 qed |
845 |
1073 |
846 lemma fresh_eqvt: |
1074 lemma fresh_eqvt [eqvt]: |
847 shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)" |
1075 shows "p \<bullet> (a \<sharp> x) = (p \<bullet> a) \<sharp> (p \<bullet> x)" |
848 unfolding permute_bool_def |
1076 unfolding permute_bool_def |
849 by (simp add: fresh_permute_iff) |
1077 by (simp add: fresh_permute_iff) |
850 |
1078 |
851 lemma supp_eqvt: |
1079 lemma supp_eqvt [eqvt]: |
852 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
1080 shows "p \<bullet> (supp x) = supp (p \<bullet> x)" |
853 unfolding supp_conv_fresh |
1081 unfolding supp_conv_fresh |
854 unfolding Collect_def |
1082 unfolding Collect_def |
855 unfolding permute_fun_def |
1083 unfolding permute_fun_def |
856 by (simp add: Not_eqvt fresh_eqvt) |
1084 by (simp add: Not_eqvt fresh_eqvt) |
966 alpha-equivalence does not coincide with equality. |
1194 alpha-equivalence does not coincide with equality. |
967 *} |
1195 *} |
968 |
1196 |
969 definition |
1197 definition |
970 "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}" |
1198 "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}" |
971 |
|
972 |
1199 |
973 |
1200 |
974 section {* Finitely-supported types *} |
1201 section {* Finitely-supported types *} |
975 |
1202 |
976 class fs = pt + |
1203 class fs = pt + |
1244 lemma fresh_append: |
1471 lemma fresh_append: |
1245 shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys" |
1472 shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys" |
1246 by (induct xs) (simp_all add: fresh_Nil fresh_Cons) |
1473 by (induct xs) (simp_all add: fresh_Nil fresh_Cons) |
1247 |
1474 |
1248 |
1475 |
1476 subsubsection {* List Operations *} |
|
1477 |
|
1478 lemma append_eqvt[eqvt]: |
|
1479 shows "p \<bullet> (xs @ ys) = (p \<bullet> xs) @ (p \<bullet> ys)" |
|
1480 by (induct xs) auto |
|
1481 |
|
1482 lemma rev_eqvt[eqvt]: |
|
1483 shows "p \<bullet> (rev xs) = rev (p \<bullet> xs)" |
|
1484 by (induct xs) (simp_all add: append_eqvt) |
|
1485 |
|
1486 lemma supp_rev: |
|
1487 shows "supp (rev xs) = supp xs" |
|
1488 by (induct xs) (auto simp add: supp_append supp_Cons supp_Nil) |
|
1489 |
|
1490 lemma fresh_rev: |
|
1491 shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs" |
|
1492 by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil) |
|
1493 |
|
1494 lemma map_eqvt[eqvt]: |
|
1495 shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)" |
|
1496 by (induct xs) (simp_all, simp only: permute_fun_app_eq) |
|
1497 |
|
1498 lemma removeAll_eqvt[eqvt]: |
|
1499 shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)" |
|
1500 by (induct xs) (auto) |
|
1501 |
|
1502 lemma supp_removeAll: |
|
1503 fixes x::"atom" |
|
1504 shows "supp (removeAll x xs) = supp xs - {x}" |
|
1505 by (induct xs) |
|
1506 (auto simp add: supp_Nil supp_Cons supp_atom) |
|
1507 |
|
1508 lemma filter_eqvt[eqvt]: |
|
1509 shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)" |
|
1510 apply(induct xs) |
|
1511 apply(simp) |
|
1512 apply(simp only: filter.simps permute_list.simps if_eqvt) |
|
1513 apply(simp only: permute_fun_app_eq) |
|
1514 done |
|
1515 |
|
1516 lemma distinct_eqvt[eqvt]: |
|
1517 shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)" |
|
1518 apply(induct xs) |
|
1519 apply(simp add: permute_bool_def) |
|
1520 apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt) |
|
1521 done |
|
1522 |
|
1523 lemma length_eqvt[eqvt]: |
|
1524 shows "p \<bullet> (length xs) = length (p \<bullet> xs)" |
|
1525 by (induct xs) (simp_all add: permute_pure) |
|
1526 |
|
1527 |
|
1249 instance list :: (fs) fs |
1528 instance list :: (fs) fs |
1250 apply default |
1529 apply default |
1251 apply (induct_tac x) |
1530 apply (induct_tac x) |
1252 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
1531 apply (simp_all add: supp_Nil supp_Cons finite_supp) |
1253 done |
1532 done |
1263 |
1542 |
1264 lemma fresh_conv_MOST: |
1543 lemma fresh_conv_MOST: |
1265 shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)" |
1544 shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)" |
1266 unfolding fresh_def supp_def |
1545 unfolding fresh_def supp_def |
1267 unfolding MOST_iff_cofinite by simp |
1546 unfolding MOST_iff_cofinite by simp |
1268 |
|
1269 lemma supp_subset_fresh: |
|
1270 assumes a: "\<And>a. a \<sharp> x \<Longrightarrow> a \<sharp> y" |
|
1271 shows "supp y \<subseteq> supp x" |
|
1272 using a |
|
1273 unfolding fresh_def |
|
1274 by blast |
|
1275 |
1547 |
1276 lemma fresh_fun_app: |
1548 lemma fresh_fun_app: |
1277 assumes "a \<sharp> f" and "a \<sharp> x" |
1549 assumes "a \<sharp> f" and "a \<sharp> x" |
1278 shows "a \<sharp> f x" |
1550 shows "a \<sharp> f x" |
1279 using assms |
1551 using assms |
1313 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1585 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1314 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1586 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1315 unfolding fresh_def |
1587 unfolding fresh_def |
1316 using supp_fun_app by auto |
1588 using supp_fun_app by auto |
1317 qed |
1589 qed |
1590 |
|
1591 lemma supp_fun_app_eqvt: |
|
1592 assumes a: "eqvt f" |
|
1593 shows "supp (f x) \<subseteq> supp x" |
|
1594 proof - |
|
1595 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
|
1596 then show "supp (f x) \<subseteq> supp x" using supp_fun_app by blast |
|
1597 qed |
|
1598 |
|
1599 |
|
1318 |
1600 |
1319 text {* equivariance of a function at a given argument *} |
1601 text {* equivariance of a function at a given argument *} |
1320 |
1602 |
1321 definition |
1603 definition |
1322 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |
1604 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |
1351 using fresh |
1633 using fresh |
1352 unfolding fresh_def |
1634 unfolding fresh_def |
1353 using supp_eqvt_at[OF asm fin] |
1635 using supp_eqvt_at[OF asm fin] |
1354 by auto |
1636 by auto |
1355 |
1637 |
1356 text {* helper functions for nominal_functions *} |
1638 |
1639 subsection {* helper functions for nominal_functions *} |
|
1357 |
1640 |
1358 lemma the_default_eqvt: |
1641 lemma the_default_eqvt: |
1359 assumes unique: "\<exists>!x. P x" |
1642 assumes unique: "\<exists>!x. P x" |
1360 shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))" |
1643 shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))" |
1361 apply(rule THE_default1_equality [symmetric]) |
1644 apply(rule THE_default1_equality [symmetric]) |
1443 assumes "finite S" |
1726 assumes "finite S" |
1444 shows "a \<sharp> S - T \<longleftrightarrow> (a \<notin> T \<longrightarrow> a \<sharp> S)" |
1727 shows "a \<sharp> S - T \<longleftrightarrow> (a \<notin> T \<longrightarrow> a \<sharp> S)" |
1445 unfolding fresh_def |
1728 unfolding fresh_def |
1446 by (auto simp add: supp_finite_atom_set assms) |
1729 by (auto simp add: supp_finite_atom_set assms) |
1447 |
1730 |
1448 |
|
1449 lemma Union_fresh: |
|
1450 shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)" |
|
1451 unfolding Union_image_eq[symmetric] |
|
1452 apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app) |
|
1453 unfolding eqvt_def |
|
1454 unfolding permute_fun_def |
|
1455 apply(simp) |
|
1456 unfolding UNION_def |
|
1457 unfolding Collect_def |
|
1458 unfolding Bex_def |
|
1459 apply(simp add: ex_eqvt) |
|
1460 unfolding permute_fun_def |
|
1461 apply(simp add: conj_eqvt) |
|
1462 apply(simp add: mem_eqvt) |
|
1463 apply(simp add: supp_eqvt) |
|
1464 unfolding permute_fun_def |
|
1465 apply(simp) |
|
1466 apply(assumption) |
|
1467 done |
|
1468 |
|
1469 lemma Union_supports_set: |
1731 lemma Union_supports_set: |
1470 shows "(\<Union>x \<in> S. supp x) supports S" |
1732 shows "(\<Union>x \<in> S. supp x) supports S" |
1471 proof - |
1733 proof - |
1472 { fix a b |
1734 { fix a b |
1473 have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S" |
1735 have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S" |
1487 lemma Union_included_in_supp: |
1749 lemma Union_included_in_supp: |
1488 fixes S::"('a::fs set)" |
1750 fixes S::"('a::fs set)" |
1489 assumes fin: "finite S" |
1751 assumes fin: "finite S" |
1490 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
1752 shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S" |
1491 proof - |
1753 proof - |
1754 have eqvt: "eqvt (\<lambda>S. \<Union> supp ` S)" |
|
1755 unfolding eqvt_def |
|
1756 by (perm_simp) (simp) |
|
1492 have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)" |
1757 have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)" |
1493 by (rule supp_finite_atom_set[symmetric]) |
1758 by (rule supp_finite_atom_set[symmetric]) (rule Union_of_finite_supp_sets[OF fin]) |
1494 (rule Union_of_finite_supp_sets[OF fin]) |
1759 also have "\<dots> = supp ((\<lambda>S. \<Union> supp ` S) S)" by simp |
1495 also have "\<dots> \<subseteq> supp S" |
1760 also have "\<dots> \<subseteq> supp S" using eqvt |
1496 by (rule supp_subset_fresh) |
1761 by (rule supp_fun_app_eqvt) |
1497 (simp add: Union_fresh) |
|
1498 finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" . |
1762 finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" . |
1499 qed |
1763 qed |
1500 |
1764 |
1501 lemma supp_of_finite_sets: |
1765 lemma supp_of_finite_sets: |
1502 fixes S::"('a::fs set)" |
1766 fixes S::"('a::fs set)" |
1562 by (simp add: supp_set) |
1826 by (simp add: supp_set) |
1563 |
1827 |
1564 |
1828 |
1565 subsection {* Type @{typ "'a fset"} is finitely supported *} |
1829 subsection {* Type @{typ "'a fset"} is finitely supported *} |
1566 |
1830 |
1567 lemma fset_eqvt: |
|
1568 shows "p \<bullet> (fset S) = fset (p \<bullet> S)" |
|
1569 by (lifting set_eqvt) |
|
1570 |
|
1571 lemma supp_fset [simp]: |
1831 lemma supp_fset [simp]: |
1572 shows "supp (fset S) = supp S" |
1832 shows "supp (fset S) = supp S" |
1573 unfolding supp_def |
1833 unfolding supp_def |
1574 by (simp add: fset_eqvt fset_cong) |
1834 by (simp add: fset_eqvt fset_cong) |
1575 |
1835 |
1607 instance fset :: (fs) fs |
1867 instance fset :: (fs) fs |
1608 apply (default) |
1868 apply (default) |
1609 apply (rule fset_finite_supp) |
1869 apply (rule fset_finite_supp) |
1610 done |
1870 done |
1611 |
1871 |
1872 |
|
1873 lemma in_fset_eqvt[eqvt]: |
|
1874 shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))" |
|
1875 unfolding in_fset |
|
1876 by (perm_simp) (simp) |
|
1877 |
|
1878 lemma union_fset_eqvt[eqvt]: |
|
1879 shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))" |
|
1880 by (induct S) (simp_all) |
|
1881 |
|
1882 lemma supp_union_fset: |
|
1883 fixes S T::"'a::fs fset" |
|
1884 shows "supp (S |\<union>| T) = supp S \<union> supp T" |
|
1885 by (induct S) (auto) |
|
1886 |
|
1887 lemma fresh_union_fset: |
|
1888 fixes S T::"'a::fs fset" |
|
1889 shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T" |
|
1890 unfolding fresh_def |
|
1891 by (simp add: supp_union_fset) |
|
1892 |
|
1893 lemma map_fset_eqvt[eqvt]: |
|
1894 shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)" |
|
1895 by (lifting map_eqvt) |
|
1612 |
1896 |
1613 section {* Freshness and Fresh-Star *} |
1897 section {* Freshness and Fresh-Star *} |
1614 |
1898 |
1615 lemma fresh_Unit_elim: |
1899 lemma fresh_Unit_elim: |
1616 shows "(a \<sharp> () \<Longrightarrow> PROP C) \<equiv> PROP C" |
1900 shows "(a \<sharp> () \<Longrightarrow> PROP C) \<equiv> PROP C" |
1749 lemma fresh_star_permute_iff: |
2033 lemma fresh_star_permute_iff: |
1750 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
2034 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
1751 unfolding fresh_star_def |
2035 unfolding fresh_star_def |
1752 by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) |
2036 by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff) |
1753 |
2037 |
1754 lemma fresh_star_eqvt: |
2038 lemma fresh_star_eqvt [eqvt]: |
1755 shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
2039 shows "p \<bullet> (as \<sharp>* x) \<longleftrightarrow> (p \<bullet> as) \<sharp>* (p \<bullet> x)" |
1756 unfolding fresh_star_def |
2040 unfolding fresh_star_def |
1757 unfolding Ball_def |
2041 by (perm_simp) (rule refl) |
1758 apply(simp add: all_eqvt) |
|
1759 apply(subst permute_fun_def) |
|
1760 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt) |
|
1761 done |
|
1762 |
|
1763 |
2042 |
1764 |
2043 |
1765 section {* Induction principle for permutations *} |
2044 section {* Induction principle for permutations *} |
1766 |
2045 |
1767 |
2046 |
2189 class at_base = pt + |
2468 class at_base = pt + |
2190 fixes atom :: "'a \<Rightarrow> atom" |
2469 fixes atom :: "'a \<Rightarrow> atom" |
2191 assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b" |
2470 assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b" |
2192 assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)" |
2471 assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)" |
2193 |
2472 |
2473 declare atom_eqvt[eqvt] |
|
2474 |
|
2194 class at = at_base + |
2475 class at = at_base + |
2195 assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" |
2476 assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" |
2196 |
2477 |
2197 lemma supp_at_base: |
2478 lemma supp_at_base: |
2198 fixes a::"'a::at_base" |
2479 fixes a::"'a::at_base" |
2298 definition |
2579 definition |
2299 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
2580 flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')") |
2300 where |
2581 where |
2301 "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)" |
2582 "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)" |
2302 |
2583 |
2584 |
|
2303 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0" |
2585 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0" |
2304 unfolding flip_def by (rule swap_self) |
2586 unfolding flip_def by (rule swap_self) |
2305 |
2587 |
2306 lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)" |
2588 lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)" |
2307 unfolding flip_def by (rule swap_commute) |
2589 unfolding flip_def by (rule swap_commute) |
2316 unfolding permute_plus [symmetric] add_flip_cancel by simp |
2598 unfolding permute_plus [symmetric] add_flip_cancel by simp |
2317 |
2599 |
2318 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x" |
2600 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x" |
2319 by (simp add: flip_commute) |
2601 by (simp add: flip_commute) |
2320 |
2602 |
2321 lemma flip_eqvt: |
2603 lemma flip_eqvt [eqvt]: |
2322 fixes a b c::"'a::at_base" |
2604 fixes a b c::"'a::at_base" |
2323 shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)" |
2605 shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)" |
2324 unfolding flip_def |
2606 unfolding flip_def |
2325 by (simp add: swap_eqvt atom_eqvt) |
2607 by (simp add: swap_eqvt atom_eqvt) |
2326 |
2608 |
2636 text {* at the moment only single-sort concrete atoms are supported *} |
2918 text {* at the moment only single-sort concrete atoms are supported *} |
2637 |
2919 |
2638 use "nominal_atoms.ML" |
2920 use "nominal_atoms.ML" |
2639 |
2921 |
2640 |
2922 |
2923 section {* automatic equivariance procedure for inductive definitions *} |
|
2924 |
|
2925 use "nominal_eqvt.ML" |
|
2926 |
|
2927 |
|
2641 |
2928 |
2642 end |
2929 end |