equal
deleted
inserted
replaced
807 by (rule a3) |
807 by (rule a3) |
808 ultimately show "False" by simp |
808 ultimately show "False" by simp |
809 qed |
809 qed |
810 qed |
810 qed |
811 |
811 |
|
812 section {* Finitely-supported types *} |
|
813 |
|
814 class fs = pt + |
|
815 assumes finite_supp: "finite (supp x)" |
|
816 |
|
817 lemma pure_supp: |
|
818 shows "supp (x::'a::pure) = {}" |
|
819 unfolding supp_def by (simp add: permute_pure) |
|
820 |
|
821 lemma pure_fresh: |
|
822 fixes x::"'a::pure" |
|
823 shows "a \<sharp> x" |
|
824 unfolding fresh_def by (simp add: pure_supp) |
|
825 |
|
826 instance pure < fs |
|
827 by default (simp add: pure_supp) |
|
828 |
|
829 |
|
830 subsection {* Type @{typ atom} is finitely-supported. *} |
|
831 |
|
832 lemma supp_atom: |
|
833 shows "supp a = {a}" |
|
834 apply (rule finite_supp_unique) |
|
835 apply (clarsimp simp add: supports_def) |
|
836 apply simp |
|
837 apply simp |
|
838 done |
|
839 |
|
840 lemma fresh_atom: |
|
841 shows "a \<sharp> b \<longleftrightarrow> a \<noteq> b" |
|
842 unfolding fresh_def supp_atom by simp |
|
843 |
|
844 instance atom :: fs |
|
845 by default (simp add: supp_atom) |
|
846 |
812 section {* Support for finite sets of atoms *} |
847 section {* Support for finite sets of atoms *} |
813 |
|
814 |
848 |
815 lemma supp_finite_atom_set: |
849 lemma supp_finite_atom_set: |
816 fixes S::"atom set" |
850 fixes S::"atom set" |
817 assumes "finite S" |
851 assumes "finite S" |
818 shows "supp S = S" |
852 shows "supp S = S" |
821 apply(simp add: swap_set_not_in) |
855 apply(simp add: swap_set_not_in) |
822 apply(rule assms) |
856 apply(rule assms) |
823 apply(simp add: swap_set_in) |
857 apply(simp add: swap_set_in) |
824 done |
858 done |
825 |
859 |
826 |
860 lemma supp_atom_insert: |
827 |
861 fixes S::"atom set" |
828 section {* Finitely-supported types *} |
862 assumes a: "finite S" |
829 |
863 shows "supp (insert a S) = supp a \<union> supp S" |
830 class fs = pt + |
864 using a by (simp add: supp_finite_atom_set supp_atom) |
831 assumes finite_supp: "finite (supp x)" |
|
832 |
|
833 lemma pure_supp: |
|
834 shows "supp (x::'a::pure) = {}" |
|
835 unfolding supp_def by (simp add: permute_pure) |
|
836 |
|
837 lemma pure_fresh: |
|
838 fixes x::"'a::pure" |
|
839 shows "a \<sharp> x" |
|
840 unfolding fresh_def by (simp add: pure_supp) |
|
841 |
|
842 instance pure < fs |
|
843 by default (simp add: pure_supp) |
|
844 |
|
845 |
|
846 subsection {* Type @{typ atom} is finitely-supported. *} |
|
847 |
|
848 lemma supp_atom: |
|
849 shows "supp a = {a}" |
|
850 apply (rule finite_supp_unique) |
|
851 apply (clarsimp simp add: supports_def) |
|
852 apply simp |
|
853 apply simp |
|
854 done |
|
855 |
|
856 lemma fresh_atom: |
|
857 shows "a \<sharp> b \<longleftrightarrow> a \<noteq> b" |
|
858 unfolding fresh_def supp_atom by simp |
|
859 |
|
860 instance atom :: fs |
|
861 by default (simp add: supp_atom) |
|
862 |
|
863 |
865 |
864 section {* Type @{typ perm} is finitely-supported. *} |
866 section {* Type @{typ perm} is finitely-supported. *} |
865 |
867 |
866 lemma perm_swap_eq: |
868 lemma perm_swap_eq: |
867 shows "(a \<rightleftharpoons> b) \<bullet> p = p \<longleftrightarrow> (p \<bullet> (a \<rightleftharpoons> b)) = (a \<rightleftharpoons> b)" |
869 shows "(a \<rightleftharpoons> b) \<bullet> p = p \<longleftrightarrow> (p \<bullet> (a \<rightleftharpoons> b)) = (a \<rightleftharpoons> b)" |