Theory Executable_Set

(*  Title:      HOL/Library/Executable_Set.thy
    Author:     Stefan Berghofer, TU Muenchen
*)

header {* Implementation of finite sets by lists *}

theory Executable_Set
imports Main Fset SML_Quickcheck
begin

subsection {* Preprocessor setup *}

declare member [code] 

definition empty :: "'a set" where
  "empty = {}"

declare empty_def [symmetric, code_unfold]

definition inter :: "'a set => 'a set => 'a set" where
  "inter = op ∩"

declare inter_def [symmetric, code_unfold]

definition union :: "'a set => 'a set => 'a set" where
  "union = op ∪"

declare union_def [symmetric, code_unfold]

definition subset :: "'a set => 'a set => bool" where
  "subset = op ≤"

declare subset_def [symmetric, code_unfold]

lemma [code]:
  "subset A B <-> (∀x∈A. x ∈ B)"
  by (simp add: subset_def subset_eq)

definition eq_set :: "'a set => 'a set => bool" where
  [code del]: "eq_set = op ="

(*declare eq_set_def [symmetric, code_unfold]*)

lemma [code]:
  "eq_set A B <-> A ⊆ B ∧ B ⊆ A"
  by (simp add: eq_set_def set_eq)

declare inter [code]

declare List_Set.project_def [symmetric, code_unfold]

definition Inter :: "'a set set => 'a set" where
  "Inter = Complete_Lattice.Inter"

declare Inter_def [symmetric, code_unfold]

definition Union :: "'a set set => 'a set" where
  "Union = Complete_Lattice.Union"

declare Union_def [symmetric, code_unfold]


subsection {* Code generator setup *}

ML {*
nonfix inter;
nonfix union;
nonfix subset;
*}

definition flip :: "('a => 'b => 'c) => 'b => 'a => 'c" where
  "flip f a b = f b a"

types_code
  fset ("(_/ \<module>fset)")
attach {*
datatype 'a fset = Set of 'a list | Coset of 'a list;
*}

consts_code
  Set ("\<module>Set")
  Coset ("\<module>Coset")

consts_code
  "empty"             ("{*Fset.empty*}")
  "List_Set.is_empty" ("{*Fset.is_empty*}")
  "Set.insert"        ("{*Fset.insert*}")
  "List_Set.remove"   ("{*Fset.remove*}")
  "Set.image"         ("{*Fset.map*}")
  "List_Set.project"  ("{*Fset.filter*}")
  "Ball"              ("{*flip Fset.forall*}")
  "Bex"               ("{*flip Fset.exists*}")
  "union"             ("{*Fset.union*}")
  "inter"             ("{*Fset.inter*}")
  "op - :: 'a set => 'a set => 'a set" ("{*flip Fset.subtract*}")
  "Union"             ("{*Fset.Union*}")
  "Inter"             ("{*Fset.Inter*}")
  card                ("{*Fset.card*}")
  fold                ("{*foldl o flip*}")

hide (open) const empty inter union subset eq_set Inter Union flip

end