src/HOL/Library/Executable_Set.thy
author haftmann
Wed Sep 23 16:32:53 2009 +0200 (2009-09-23)
changeset 32702 457135bdd596
parent 32700 e743ca6e97e7
child 32705 04ce6bb14d85
permissions -rw-r--r--
explicitly hide empty, inter, union
     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 empty :: "'a set" where
    16   "empty = {}"
    17 
    18 declare empty_def [symmetric, code_unfold]
    19 
    20 definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    21   "inter = op \<inter>"
    22 
    23 declare inter_def [symmetric, code_unfold]
    24 
    25 definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    26   "union = op \<union>"
    27 
    28 declare union_def [symmetric, code_unfold]
    29 
    30 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    31   "subset = op \<le>"
    32 
    33 declare subset_def [symmetric, code_unfold]
    34 
    35 lemma [code]:
    36   "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    37   by (simp add: subset_def subset_eq)
    38 
    39 definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    40   [code del]: "eq_set = op ="
    41 
    42 (*declare eq_set_def [symmetric, code_unfold]*)
    43 
    44 lemma [code]:
    45   "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    46   by (simp add: eq_set_def set_eq)
    47 
    48 declare inter [code]
    49 
    50 declare Inter_image_eq [symmetric, code_unfold]
    51 declare Union_image_eq [symmetric, code_unfold]
    52 
    53 declare List_Set.project_def [symmetric, code_unfold]
    54 
    55 definition Inter :: "'a set set \<Rightarrow> 'a set" where
    56   "Inter = Complete_Lattice.Inter"
    57 
    58 declare Inter_def [symmetric, code_unfold]
    59 
    60 definition Union :: "'a set set \<Rightarrow> 'a set" where
    61   "Union = Complete_Lattice.Union"
    62 
    63 declare Union_def [symmetric, code_unfold]
    64 
    65 
    66 subsection {* Code generator setup *}
    67 
    68 ML {*
    69 nonfix inter;
    70 nonfix union;
    71 nonfix subset;
    72 *}
    73 
    74 definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    75   "flip f a b = f b a"
    76 
    77 types_code
    78   fset ("(_/ \<module>fset)")
    79 attach {*
    80 datatype 'a fset = Set of 'a list;
    81 *}
    82 
    83 consts_code
    84   Set ("\<module>Set")
    85 
    86 consts_code
    87   "empty"             ("{*Fset.empty*}")
    88   "List_Set.is_empty" ("{*Fset.is_empty*}")
    89   "Set.insert"        ("{*Fset.insert*}")
    90   "List_Set.remove"   ("{*Fset.remove*}")
    91   "Set.image"         ("{*Fset.map*}")
    92   "List_Set.project"  ("{*Fset.filter*}")
    93   "Ball"              ("{*flip Fset.forall*}")
    94   "Bex"               ("{*flip Fset.exists*}")
    95   "union"             ("{*Fset.union*}")
    96   "inter"             ("{*Fset.inter*}")
    97   "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
    98   "Union"             ("{*Fset.Union*}")
    99   "Inter"             ("{*Fset.Inter*}")
   100   card                ("{*Fset.card*}")
   101   fold                ("{*foldl o flip*}")
   102 
   103 hide (open) const empty inter union subset eq_set Inter Union flip
   104 
   105 end