src/HOL/Library/Executable_Set.thy
changeset 31850 e81d0f04ffdf
parent 31847 7de0e20ca24d
child 31998 2c7a24f74db9
     1.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Jun 29 12:18:55 2009 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Jun 29 12:18:56 2009 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Implementation of finite sets by lists *}
     1.5  
     1.6  theory Executable_Set
     1.7 -imports Main Code_Set
     1.8 +imports Main Fset
     1.9  begin
    1.10  
    1.11  subsection {* Derived set operations *}
    1.12 @@ -45,41 +45,39 @@
    1.13  
    1.14  subsection {* code generator setup *}
    1.15  
    1.16 -text {* eliminate popular infixes *}
    1.17 -
    1.18  ML {*
    1.19  nonfix inter;
    1.20  nonfix union;
    1.21  nonfix subset;
    1.22  *}
    1.23  
    1.24 -text {* type @{typ "'a fset"} *}
    1.25 -
    1.26 -types_code
    1.27 -  fset ("(_/ list)")
    1.28 -
    1.29 -consts_code
    1.30 -  Set ("_")
    1.31 -
    1.32 -text {* primitive operations *}
    1.33 -
    1.34  definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.35    "flip f a b = f b a"
    1.36  
    1.37 +types_code
    1.38 +  fset ("(_/ \<module>fset)")
    1.39 +attach {*
    1.40 +datatype 'a fset = Set of 'a list;
    1.41 +*}
    1.42 +
    1.43  consts_code
    1.44 -  "Set.empty"         ("{*Code_Set.empty*}")
    1.45 -  "List_Set.is_empty" ("{*Code_Set.is_empty*}")
    1.46 -  "Set.insert"        ("{*Code_Set.insert*}")
    1.47 -  "List_Set.remove"   ("{*Code_Set.remove*}")
    1.48 -  "Set.image"         ("{*Code_Set.map*}")
    1.49 -  "List_Set.project"  ("{*Code_Set.filter*}")
    1.50 -  "Ball"              ("{*flip Code_Set.forall*}")
    1.51 -  "Bex"               ("{*flip Code_Set.exists*}")
    1.52 -  "op \<union>"              ("{*Code_Set.union*}")
    1.53 -  "op \<inter>"              ("{*Code_Set.inter*}")
    1.54 -  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip subtract*}")
    1.55 -  "Set.Union"         ("{*Code_Set.union*}")
    1.56 -  "Set.Inter"         ("{*Code_Set.inter*}")
    1.57 +  Set ("\<module>Set")
    1.58 +
    1.59 +consts_code
    1.60 +  "Set.empty"         ("{*Fset.empty*}")
    1.61 +  "List_Set.is_empty" ("{*Fset.is_empty*}")
    1.62 +  "Set.insert"        ("{*Fset.insert*}")
    1.63 +  "List_Set.remove"   ("{*Fset.remove*}")
    1.64 +  "Set.image"         ("{*Fset.map*}")
    1.65 +  "List_Set.project"  ("{*Fset.filter*}")
    1.66 +  "Ball"              ("{*flip Fset.forall*}")
    1.67 +  "Bex"               ("{*flip Fset.exists*}")
    1.68 +  "op \<union>"              ("{*Fset.union*}")
    1.69 +  "op \<inter>"              ("{*Fset.inter*}")
    1.70 +  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
    1.71 +  "Set.Union"         ("{*Fset.Union*}")
    1.72 +  "Set.Inter"         ("{*Fset.Inter*}")
    1.73 +  card                ("{*Fset.card*}")
    1.74    fold                ("{*foldl o flip*}")
    1.75  
    1.76  end
    1.77 \ No newline at end of file