# HG changeset patch # User Christian Urban # Date 1289732722 0 # Node ID 6bf33236051019d35f485310593b3bc91d6e84b7 # Parent 5be8e34c2c0e7784bd7db3e61632dc69c9807972 moved most material fron Nominal2_FSet into the Nominal_Base theory diff -r 5be8e34c2c0e -r 6bf332360510 Nominal-General/Nominal2_Base.thy --- a/Nominal-General/Nominal2_Base.thy Sun Nov 14 10:02:30 2010 +0000 +++ b/Nominal-General/Nominal2_Base.thy Sun Nov 14 11:05:22 2010 +0000 @@ -6,6 +6,7 @@ *) theory Nominal2_Base imports Main Infinite_Set + "~~/src/HOL/Quotient_Examples/FSet" uses ("nominal_library.ML") ("nominal_atoms.ML") begin @@ -504,6 +505,11 @@ unfolding mem_def by (simp add: permute_fun_app_eq) +lemma empty_eqvt: + shows "p \ {} = {}" + unfolding empty_def Collect_def + by (simp add: permute_fun_def permute_bool_def) + lemma insert_eqvt: shows "p \ (insert x A) = insert (p \ x) (p \ A)" unfolding permute_set_eq_image image_insert .. @@ -569,6 +575,10 @@ end +lemma set_eqvt: + shows "p \ (set xs) = set (p \ xs)" + by (induct xs) (simp_all add: empty_eqvt insert_eqvt) + subsection {* Permutations for options *} instantiation option :: (pt) pt @@ -585,6 +595,39 @@ end + +subsection {* Permutations for fsets *} + +lemma permute_fset_rsp[quot_respect]: + shows "(op = ===> list_eq ===> list_eq) permute permute" + unfolding fun_rel_def + by (simp add: set_eqvt[symmetric]) + +instantiation fset :: (pt) pt +begin + +quotient_definition + "permute_fset :: perm \ 'a fset \ 'a fset" +is + "permute :: perm \ 'a list \ 'a list" + +instance +proof + fix x :: "'a fset" and p q :: "perm" + show "0 \ x = x" by (descending) (simp) + show "(p + q) \ x = p \ q \ x" by (descending) (simp) +qed + +end + +lemma permute_fset [simp]: + fixes S::"('a::pt) fset" + shows "(p \ {||}) = ({||} ::('a::pt) fset)" + and "(p \ insert_fset x S) = insert_fset (p \ x) (p \ S)" + by (lifting permute_list.simps) + + + subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *} instantiation char :: pt @@ -1019,6 +1062,7 @@ section {* Finite Support instances for other types *} + subsection {* Type @{typ "'a \ 'b"} is finitely-supported. *} lemma supp_Pair: @@ -1037,14 +1081,13 @@ shows "a \ ()" by (simp add: fresh_def supp_Unit) - - instance prod :: (fs, fs) fs apply default apply (induct_tac x) apply (simp add: supp_Pair finite_supp) done + subsection {* Type @{typ "'a + 'b"} is finitely supported *} lemma supp_Inl: @@ -1069,6 +1112,7 @@ apply (simp_all add: supp_Inl supp_Inr finite_supp) done + subsection {* Type @{typ "'a option"} is finitely supported *} lemma supp_None: @@ -1093,6 +1137,7 @@ apply (simp_all add: supp_None supp_Some finite_supp) done + subsubsection {* Type @{typ "'a list"} is finitely supported *} lemma supp_Nil: @@ -1190,7 +1235,7 @@ by (simp add: fresh_def[symmetric] swap_fresh_fresh) qed -lemma Union_of_fin_supp_sets: +lemma Union_of_finite_supp_sets: fixes S::"('a::fs set)" assumes fin: "finite S" shows "finite (\x\S. supp x)" @@ -1203,38 +1248,81 @@ proof - have "(\x\S. supp x) = supp (\x\S. supp x)" by (rule supp_finite_atom_set[symmetric]) - (rule Union_of_fin_supp_sets[OF fin]) + (rule Union_of_finite_supp_sets[OF fin]) also have "\ \ supp S" by (rule supp_subset_fresh) (simp add: Union_fresh) finally show "(\x\S. supp x) \ supp S" . qed -lemma supp_of_fin_sets: +lemma supp_of_finite_sets: fixes S::"('a::fs set)" assumes fin: "finite S" shows "(supp S) = (\x\S. supp x)" apply(rule subset_antisym) apply(rule supp_is_subset) apply(rule Union_supports_set) -apply(rule Union_of_fin_supp_sets[OF fin]) +apply(rule Union_of_finite_supp_sets[OF fin]) apply(rule Union_included_in_supp[OF fin]) done -lemma supp_of_fin_union: +lemma finite_sets_supp: + fixes S::"('a::fs set)" + assumes "finite S" + shows "finite (supp S)" +using assms +by (simp only: supp_of_finite_sets Union_of_finite_supp_sets) + +lemma supp_of_finite_union: fixes S T::"('a::fs) set" assumes fin1: "finite S" and fin2: "finite T" shows "supp (S \ T) = supp S \ supp T" using fin1 fin2 - by (simp add: supp_of_fin_sets) + by (simp add: supp_of_finite_sets) -lemma supp_of_fin_insert: +lemma supp_of_finite_insert: fixes S::"('a::fs) set" assumes fin: "finite S" shows "supp (insert x S) = supp x \ supp S" using fin - by (simp add: supp_of_fin_sets) + by (simp add: supp_of_finite_sets) + + +subsection {* Type @{typ "'a fset"} is finitely supported *} + +lemma fset_eqvt: + shows "p \ (fset S) = fset (p \ S)" + by (lifting set_eqvt) + +lemma supp_fset [simp]: + shows "supp (fset S) = supp S" + unfolding supp_def + by (simp add: fset_eqvt fset_cong) + +lemma supp_empty_fset [simp]: + shows "supp {||} = {}" + unfolding supp_def + by simp + +lemma supp_insert_fset [simp]: + fixes x::"'a::fs" + and S::"'a fset" + shows "supp (insert_fset x S) = supp x \ supp S" + apply(subst supp_fset[symmetric]) + apply(simp add: supp_fset supp_of_finite_insert) + done + +lemma fset_finite_supp: + fixes S::"('a::fs) fset" + shows "finite (supp S)" + by (induct S) (simp_all add: finite_supp) + + +instance fset :: (fs) fs + apply (default) + apply (rule fset_finite_supp) + done section {* Fresh-Star *} @@ -1577,7 +1665,7 @@ lemma supp_finite_set_at_base: assumes a: "finite S" shows "supp S = atom ` S" -apply(simp add: supp_of_fin_sets[OF a]) +apply(simp add: supp_of_finite_sets[OF a]) apply(simp add: supp_at_base) apply(auto) done diff -r 5be8e34c2c0e -r 6bf332360510 Nominal-General/Nominal2_Eqvt.thy --- a/Nominal-General/Nominal2_Eqvt.thy Sun Nov 14 10:02:30 2010 +0000 +++ b/Nominal-General/Nominal2_Eqvt.thy Sun Nov 14 11:05:22 2010 +0000 @@ -33,10 +33,13 @@ swap_eqvt flip_eqvt (* datatypes *) - Pair_eqvt permute_list.simps + Pair_eqvt permute_list.simps (* sets *) - mem_eqvt insert_eqvt + mem_eqvt empty_eqvt insert_eqvt set_eqvt + + (* fsets *) + permute_fset fset_eqvt text {* helper lemmas for the perm_simp *} @@ -79,7 +82,7 @@ apply(simp) done -section {* Logical Operators *} +subsection {* Equivariance of Logical Operators *} lemma eq_eqvt[eqvt]: shows "p \ (x = y) \ (p \ x) = (p \ y)" @@ -128,7 +131,7 @@ apply(rule theI'[OF unique]) done -section {* Set Operations *} +subsection {* Equivariance Set Operations *} lemma not_mem_eqvt: shows "p \ (x \ A) \ (p \ x) \ (p \ A)" @@ -152,11 +155,6 @@ unfolding Ball_def by (perm_simp) (rule refl) -lemma empty_eqvt[eqvt]: - shows "p \ {} = {}" - unfolding empty_def - by (perm_simp) (rule refl) - lemma supp_set_empty: shows "supp {} = {}" unfolding supp_def @@ -223,7 +221,7 @@ shows "supp (set xs) = supp xs" apply(induct xs) apply(simp add: supp_set_empty supp_Nil) -apply(simp add: supp_Cons supp_of_fin_insert) +apply(simp add: supp_Cons supp_of_finite_insert) done @@ -253,21 +251,19 @@ shows "a \ rev xs \ a \ xs" by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil) -lemma set_eqvt[eqvt]: - shows "p \ (set xs) = set (p \ xs)" - by (induct xs) (simp_all add: empty_eqvt insert_eqvt) - -(* needs finite support premise -lemma supp_set: - fixes x :: "'a::pt" - shows "supp (set xs) = supp xs" -*) - lemma map_eqvt[eqvt]: shows "p \ (map f xs) = map (p \ f) (p \ xs)" by (induct xs) (simp_all, simp only: permute_fun_app_eq) -section {* Product Operations *} + +subsection {* Equivariance for fsets *} + +lemma map_fset_eqvt[eqvt]: + shows "p \ (map_fset f S) = map_fset (p \ f) (p \ S)" + by (lifting map_eqvt) + + +subsection {* Product Operations *} lemma fst_eqvt[eqvt]: "p \ (fst x) = fst (p \ x)" @@ -379,7 +375,7 @@ ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} -section {* Automatic equivariance procedure for inductive definitions *} +section {* automatic equivariance procedure for inductive definitions *} use "nominal_eqvt.ML" diff -r 5be8e34c2c0e -r 6bf332360510 Nominal/Nominal2_FSet.thy --- a/Nominal/Nominal2_FSet.thy Sun Nov 14 10:02:30 2010 +0000 +++ b/Nominal/Nominal2_FSet.thy Sun Nov 14 11:05:22 2010 +0000 @@ -1,75 +1,8 @@ theory Nominal2_FSet imports "../Nominal-General/Nominal2_Base" - "../Nominal-General/Nominal2_Eqvt" - "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" -begin - -lemma permute_fset_rsp[quot_respect]: - shows "(op = ===> list_eq ===> list_eq) permute permute" - unfolding fun_rel_def - by (simp add: set_eqvt[symmetric]) - -instantiation fset :: (pt) pt + "../Nominal-General/Nominal2_Eqvt" begin -quotient_definition - "permute_fset :: perm \ 'a fset \ 'a fset" -is - "permute :: perm \ 'a list \ 'a list" - -instance -proof - fix x :: "'a fset" and p q :: "perm" - show "0 \ x = x" by (descending) (simp) - show "(p + q) \ x = p \ q \ x" by (descending) (simp) -qed - -end - -lemma permute_fset[simp, eqvt]: - fixes S::"('a::pt) fset" - shows "(p \ {||}) = ({||} ::('a::pt) fset)" - and "(p \ insert_fset x S) = insert_fset (p \ x) (p \ S)" - by (lifting permute_list.simps) - -lemma map_fset_eqvt[eqvt]: - shows "p \ (map_fset f S) = map_fset (p \ f) (p \ S)" - by (lifting map_eqvt) - -lemma fset_eqvt[eqvt]: - shows "p \ (fset S) = fset (p \ S)" - by (lifting set_eqvt) - -lemma supp_fset [simp]: - shows "supp (fset S) = supp S" - unfolding supp_def - by (perm_simp) (simp add: fset_cong) - -lemma supp_empty_fset [simp]: - shows "supp {||} = {}" - unfolding supp_def - by simp - -lemma supp_insert_fset [simp]: - fixes x::"'a::fs" - and S::"'a fset" - shows "supp (insert_fset x S) = supp x \ supp S" - apply(subst supp_fset[symmetric]) - apply(simp add: supp_fset supp_of_fin_insert) - done - -lemma fset_finite_supp: - fixes S::"('a::fs) fset" - shows "finite (supp S)" - by (induct S) (simp_all add: finite_supp) - - -subsection {* finite sets are fs-types *} - -instance fset :: (fs) fs - apply (default) - apply (rule fset_finite_supp) - done lemma atom_map_fset_cong: shows "map_fset atom x = map_fset atom y \ x = y" @@ -100,7 +33,7 @@ apply (simp add: fresh_set_empty) apply simp apply (unfold fresh_def) - apply (simp add: supp_of_fin_insert) + apply (simp add: supp_of_finite_insert) apply (rule conjI) apply (unfold fresh_star_def) apply simp