# HG changeset patch # User haftmann # Date 1276922613 -7200 # Node ID a2a3b62fc819b9a19104fc6e8fba18cf572f02b5 # Parent fcc2c36b37704e29117f1d9628b429c13c5c4dcb quickcheck for fsets diff -r fcc2c36b3770 -r a2a3b62fc819 src/HOL/Library/Fset.thy --- a/src/HOL/Library/Fset.thy Fri Jun 18 21:22:05 2010 +0200 +++ b/src/HOL/Library/Fset.thy Sat Jun 19 06:43:33 2010 +0200 @@ -7,22 +7,26 @@ imports More_Set More_List begin -declare mem_def [simp] - subsection {* Lifting *} -datatype 'a fset = Fset "'a set" +typedef (open) 'a fset = "UNIV :: 'a set set" + morphisms member Fset by rule+ -primrec member :: "'a fset \ 'a set" where +lemma member_Fset [simp]: "member (Fset A) = A" - -lemma member_inject [simp]: - "member A = member B \ A = B" - by (cases A, cases B) simp + by (rule Fset_inverse) rule lemma Fset_member [simp]: "Fset (member A) = A" - by (cases A) simp + by (rule member_inverse) + +declare member_inject [simp] + +lemma Fset_inject [simp]: + "Fset A = Fset B \ A = B" + by (simp add: Fset_inject) + +declare mem_def [simp] definition Set :: "'a list \ 'a fset" where "Set xs = Fset (set xs)" @@ -56,6 +60,27 @@ then show ?thesis by (simp add: image_def) qed +definition (in term_syntax) + setify :: "'a\typerep list \ (unit \ Code_Evaluation.term) + \ 'a fset \ (unit \ Code_Evaluation.term)" where + [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\} xs" + +notation fcomp (infixl "o>" 60) +notation scomp (infixl "o\" 60) + +instantiation fset :: (random) random +begin + +definition + "Quickcheck.random i = Quickcheck.random i o\ (\xs. Pair (setify xs))" + +instance .. + +end + +no_notation fcomp (infixl "o>" 60) +no_notation scomp (infixl "o\" 60) + subsection {* Lattice instantiation *} @@ -117,11 +142,11 @@ lemma empty_Set [code]: "bot = Set []" - by simp + by (simp add: Set_def) lemma UNIV_Set [code]: "top = Coset []" - by simp + by (simp add: Coset_def) definition insert :: "'a \ 'a fset \ 'a fset" where [simp]: "insert x A = Fset (Set.insert x (member A))" @@ -198,9 +223,16 @@ "A < B \ A \ B \ \ B \ (A :: 'a fset)" by (fact less_le_not_le) -lemma eq_fset_subfset_eq [code]: - "eq_class.eq A B \ A \ B \ B \ (A :: 'a fset)" - by (cases A, cases B) (simp add: eq set_eq) +instantiation fset :: (type) eq +begin + +definition + "eq_fset A B \ A \ B \ B \ (A :: 'a fset)" + +instance proof +qed (simp add: eq_fset_def set_eq [symmetric]) + +end subsection {* Functorial operations *} @@ -276,22 +308,6 @@ end -subsection {* Misc operations *} - -lemma size_fset [code]: - "fset_size f A = 0" - "size A = 0" - by (cases A, simp) (cases A, simp) - -lemma fset_case_code [code]: - "fset_case f A = f (member A)" - by (cases A) simp - -lemma fset_rec_code [code]: - "fset_rec f A = f (member A)" - by (cases A) simp - - subsection {* Simplified simprules *} lemma is_empty_simp [simp]: @@ -312,7 +328,7 @@ declare mem_def [simp del] -hide_const (open) is_empty insert remove map filter forall exists card +hide_const (open) setify is_empty insert remove map filter forall exists card Inter Union end