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