# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256756480 -3600
# Node ID c643938b846ae5c4ee8cadaf40163ab5ec5cb896
# Parent  84a356e3d38bed2d78ea383fb82050dd4dd07f36
updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)

diff -r 84a356e3d38b -r c643938b846a FSet.thy
--- a/FSet.thy	Wed Oct 28 19:46:15 2009 +0100
+++ b/FSet.thy	Wed Oct 28 20:01:20 2009 +0100
@@ -34,31 +34,32 @@
 thm "Rep_fset"
 thm "ABS_fset_def"
 
-ML {* @{term "Abs_fset"} *}
-local_setup {*
-  old_make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  EMPTY :: "'a fset"
+where
+  "EMPTY \<equiv> ([]::'a list)"
 
 term Nil
 term EMPTY
 thm EMPTY_def
 
-
-local_setup {*
-  old_make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fet"
+where
+  "INSERT \<equiv> op #"
 
 term Cons
 term INSERT
 thm INSERT_def
 
-local_setup {*
-  old_make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+where
+  "FUNION \<equiv> (op @)"
 
 term append
-term UNION
-thm UNION_def
+term FUNION
+thm FUNION_def
 
 thm QUOTIENT_fset
 
@@ -77,13 +78,14 @@
   card1_nil: "(card1 []) = 0"
 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
-local_setup {*
-  old_make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  CARD :: "'a fset \<Rightarrow> nat"
+where
+  "CARD \<equiv> card1"
 
 term card1
-term card
-thm card_def
+term CARD
+thm CARD_def
 
 (* text {*
  Maybe make_const_def should require a theorem that says that the particular lifted function
@@ -142,14 +144,21 @@
   apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)
   done
 
-local_setup {*
-  old_make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool"
+where
+  "IN \<equiv> membship"
 
 term membship
 term IN
 thm IN_def
 
+(* FIXME: does not work yet 
+quotient_def (for "'a fset")
+  FOLD :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
+where
+  "FOLD \<equiv> fold1"
+*)
 local_setup {*
   old_make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
@@ -158,6 +167,7 @@
 term fold
 thm fold_def
 
+(* FIXME: does not work yet for all types*)
 quotient_def (for "'a fset")
   fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
@@ -167,7 +177,7 @@
 term fmap
 thm fmap_def
 
-ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
+ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def card_def INSERT_def fmap_def fold_def} *}
 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)
 
 ML {*
@@ -177,6 +187,7 @@
                 @{const_name "map"}];
 *}
 
+(* FIXME: does not work anymore :o( *)
 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}
 
 lemma memb_rsp:
@@ -498,8 +509,6 @@
 ML {* lift @{thm map_append} *}
 ML {* lift @{thm eq_r[OF append_assoc]} *}
 
-thm
-
 
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)