--- 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