# 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 \<Rightarrow> 'a set" where
+lemma member_Fset [simp]:
   "member (Fset A) = A"
-
-lemma member_inject [simp]:
-  "member A = member B \<Longrightarrow> 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 \<longleftrightarrow> A = B"
+  by (simp add: Fset_inject)
+
+declare mem_def [simp]
 
 definition Set :: "'a list \<Rightarrow> '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\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
+    \<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
+  [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs"
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation fset :: (random) random
+begin
+
+definition
+  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (setify xs))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 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 \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   [simp]: "insert x A = Fset (Set.insert x (member A))"
@@ -198,9 +223,16 @@
   "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
   by (fact less_le_not_le)
 
-lemma eq_fset_subfset_eq [code]:
-  "eq_class.eq A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
-  by (cases A, cases B) (simp add: eq set_eq)
+instantiation fset :: (type) eq
+begin
+
+definition
+  "eq_fset A B \<longleftrightarrow> A \<le> B \<and> B \<le> (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