src/HOL/Library/Executable_Set.thy
author haftmann
Sun Jun 28 11:02:27 2009 +0200 (2009-06-28)
changeset 31847 7de0e20ca24d
parent 30664 167da873c3b3
child 31850 e81d0f04ffdf
permissions -rw-r--r--
Executable_Set now based on Code_Set
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@31847
     8
imports Main Code_Set
haftmann@23854
     9
begin
haftmann@23854
    10
haftmann@31847
    11
subsection {* Derived set operations *}
haftmann@31847
    12
haftmann@31847
    13
declare member [code] 
haftmann@23854
    14
haftmann@28522
    15
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
haftmann@28522
    16
  "subset = op \<le>"
haftmann@28522
    17
haftmann@28522
    18
declare subset_def [symmetric, code unfold]
haftmann@28522
    19
haftmann@31847
    20
lemma [code]:
haftmann@31847
    21
  "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
haftmann@31847
    22
  by (simp add: subset_def subset_eq)
haftmann@28522
    23
haftmann@28522
    24
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
haftmann@28522
    25
  [code del]: "eq_set = op ="
haftmann@28522
    26
nipkow@29107
    27
(* FIXME allow for Stefan's code generator:
nipkow@29107
    28
declare set_eq_subset[code unfold]
nipkow@29107
    29
*)
nipkow@29107
    30
haftmann@23854
    31
lemma [code]:
haftmann@31847
    32
  "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
haftmann@31847
    33
  by (simp add: eq_set_def set_eq)
haftmann@23854
    34
haftmann@31847
    35
declare inter [code]
haftmann@23854
    36
haftmann@31847
    37
declare Inter_image_eq [symmetric, code]
haftmann@31847
    38
declare Union_image_eq [symmetric, code]
haftmann@23854
    39
haftmann@23854
    40
haftmann@31847
    41
subsection {* Rewrites for primitive operations *}
haftmann@23854
    42
haftmann@31847
    43
declare List_Set.project_def [symmetric, code unfold]
haftmann@23854
    44
haftmann@23854
    45
haftmann@31847
    46
subsection {* code generator setup *}
haftmann@23854
    47
haftmann@31847
    48
text {* eliminate popular infixes *}
haftmann@23854
    49
haftmann@23854
    50
ML {*
haftmann@23854
    51
nonfix inter;
haftmann@23854
    52
nonfix union;
haftmann@23854
    53
nonfix subset;
haftmann@23854
    54
*}
haftmann@23854
    55
haftmann@31847
    56
text {* type @{typ "'a fset"} *}
haftmann@31847
    57
haftmann@31847
    58
types_code
haftmann@31847
    59
  fset ("(_/ list)")
haftmann@31847
    60
haftmann@31847
    61
consts_code
haftmann@31847
    62
  Set ("_")
haftmann@31847
    63
haftmann@31847
    64
text {* primitive operations *}
haftmann@31847
    65
haftmann@31847
    66
definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
haftmann@31847
    67
  "flip f a b = f b a"
haftmann@23854
    68
haftmann@23854
    69
consts_code
haftmann@31847
    70
  "Set.empty"         ("{*Code_Set.empty*}")
haftmann@31847
    71
  "List_Set.is_empty" ("{*Code_Set.is_empty*}")
haftmann@31847
    72
  "Set.insert"        ("{*Code_Set.insert*}")
haftmann@31847
    73
  "List_Set.remove"   ("{*Code_Set.remove*}")
haftmann@31847
    74
  "Set.image"         ("{*Code_Set.map*}")
haftmann@31847
    75
  "List_Set.project"  ("{*Code_Set.filter*}")
haftmann@31847
    76
  "Ball"              ("{*flip Code_Set.forall*}")
haftmann@31847
    77
  "Bex"               ("{*flip Code_Set.exists*}")
haftmann@31847
    78
  "op \<union>"              ("{*Code_Set.union*}")
haftmann@31847
    79
  "op \<inter>"              ("{*Code_Set.inter*}")
haftmann@31847
    80
  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip subtract*}")
haftmann@31847
    81
  "Set.Union"         ("{*Code_Set.union*}")
haftmann@31847
    82
  "Set.Inter"         ("{*Code_Set.inter*}")
haftmann@31847
    83
  fold                ("{*foldl o flip*}")
haftmann@23854
    84
haftmann@31847
    85
end