src/HOL/Library/Executable_Set.thy
author haftmann
Fri Sep 18 14:09:38 2009 +0200 (2009-09-18)
changeset 32606 b5c3a8a75772
parent 32587 caa5ada96a00
child 32647 e54f47f9e28b
child 32683 7c1fe854ca6a
permissions -rw-r--r--
INTER and UNION are mere abbreviations for INFI and SUPR
     1 (*  Title:      HOL/Library/Executable_Set.thy
     2     Author:     Stefan Berghofer, TU Muenchen
     3 *)
     4 
     5 header {* Implementation of finite sets by lists *}
     6 
     7 theory Executable_Set
     8 imports Main Fset
     9 begin
    10 
    11 subsection {* Preprocessor setup *}
    12 
    13 declare member [code] 
    14 
    15 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    16   "subset = op \<le>"
    17 
    18 declare subset_def [symmetric, code_unfold]
    19 
    20 lemma [code]:
    21   "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    22   by (simp add: subset_def subset_eq)
    23 
    24 definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    25   [code del]: "eq_set = op ="
    26 
    27 (*declare eq_set_def [symmetric, code_unfold]*)
    28 
    29 lemma [code]:
    30   "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    31   by (simp add: eq_set_def set_eq)
    32 
    33 declare inter [code]
    34 
    35 declare Inter_image_eq [symmetric, code_unfold]
    36 declare Union_image_eq [symmetric, code_unfold]
    37 
    38 declare List_Set.project_def [symmetric, code_unfold]
    39 
    40 definition Inter :: "'a set set \<Rightarrow> 'a set" where
    41   "Inter = Complete_Lattice.Inter"
    42 
    43 declare Inter_def [symmetric, code_unfold]
    44 
    45 definition Union :: "'a set set \<Rightarrow> 'a set" where
    46   "Union = Complete_Lattice.Union"
    47 
    48 declare Union_def [symmetric, code_unfold]
    49 
    50 
    51 subsection {* Code generator setup *}
    52 
    53 ML {*
    54 nonfix inter;
    55 nonfix union;
    56 nonfix subset;
    57 *}
    58 
    59 definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    60   "flip f a b = f b a"
    61 
    62 types_code
    63   fset ("(_/ \<module>fset)")
    64 attach {*
    65 datatype 'a fset = Set of 'a list;
    66 *}
    67 
    68 consts_code
    69   Set ("\<module>Set")
    70 
    71 consts_code
    72   "Set.empty"         ("{*Fset.empty*}")
    73   "List_Set.is_empty" ("{*Fset.is_empty*}")
    74   "Set.insert"        ("{*Fset.insert*}")
    75   "List_Set.remove"   ("{*Fset.remove*}")
    76   "Set.image"         ("{*Fset.map*}")
    77   "List_Set.project"  ("{*Fset.filter*}")
    78   "Ball"              ("{*flip Fset.forall*}")
    79   "Bex"               ("{*flip Fset.exists*}")
    80   "op \<union>"              ("{*Fset.union*}")
    81   "op \<inter>"              ("{*Fset.inter*}")
    82   "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
    83   "Union"             ("{*Fset.Union*}")
    84   "Inter"             ("{*Fset.Inter*}")
    85   card                ("{*Fset.card*}")
    86   fold                ("{*foldl o flip*}")
    87 
    88 end