--- 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 \<bullet> {} = {}"
+ unfolding empty_def Collect_def
+ by (simp add: permute_fun_def permute_bool_def)
+
lemma insert_eqvt:
shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
unfolding permute_set_eq_image image_insert ..
@@ -569,6 +575,10 @@
end
+lemma set_eqvt:
+ shows "p \<bullet> (set xs) = set (p \<bullet> 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 \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+ "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+instance
+proof
+ fix x :: "'a fset" and p q :: "perm"
+ show "0 \<bullet> x = x" by (descending) (simp)
+ show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
+qed
+
+end
+
+lemma permute_fset [simp]:
+ fixes S::"('a::pt) fset"
+ shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
+ and "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> 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 \<times> 'b"} is finitely-supported. *}
lemma supp_Pair:
@@ -1037,14 +1081,13 @@
shows "a \<sharp> ()"
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 (\<Union>x\<in>S. supp x)"
@@ -1203,38 +1248,81 @@
proof -
have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>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 "\<dots> \<subseteq> supp S"
by (rule supp_subset_fresh)
(simp add: Union_fresh)
finally show "(\<Union>x\<in>S. supp x) \<subseteq> 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) = (\<Union>x\<in>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 \<union> T) = supp S \<union> 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 \<union> 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 \<bullet> (fset S) = fset (p \<bullet> 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 \<union> 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
--- 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 \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
@@ -128,7 +131,7 @@
apply(rule theI'[OF unique])
done
-section {* Set Operations *}
+subsection {* Equivariance Set Operations *}
lemma not_mem_eqvt:
shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
@@ -152,11 +155,6 @@
unfolding Ball_def
by (perm_simp) (rule refl)
-lemma empty_eqvt[eqvt]:
- shows "p \<bullet> {} = {}"
- 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 \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
-lemma set_eqvt[eqvt]:
- shows "p \<bullet> (set xs) = set (p \<bullet> 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 \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> 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 \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
+ by (lifting map_eqvt)
+
+
+subsection {* Product Operations *}
lemma fst_eqvt[eqvt]:
"p \<bullet> (fst x) = fst (p \<bullet> 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"
--- 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 \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
-is
- "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-instance
-proof
- fix x :: "'a fset" and p q :: "perm"
- show "0 \<bullet> x = x" by (descending) (simp)
- show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x" by (descending) (simp)
-qed
-
-end
-
-lemma permute_fset[simp, eqvt]:
- fixes S::"('a::pt) fset"
- shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
- and "(p \<bullet> insert_fset x S) = insert_fset (p \<bullet> x) (p \<bullet> S)"
- by (lifting permute_list.simps)
-
-lemma map_fset_eqvt[eqvt]:
- shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
- by (lifting map_eqvt)
-
-lemma fset_eqvt[eqvt]:
- shows "p \<bullet> (fset S) = fset (p \<bullet> 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 \<union> 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 \<longleftrightarrow> 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