(* Title: HOL/Library/ExecutableSet.thy ID: $Id: ExecutableSet.thy,v 1.1 2005/09/25 18:12:26 berghofe Exp $ Author: Stefan Berghofer, TU Muenchen *) header {* Implementation of finite sets by lists *} theory ExecutableSet imports Main begin lemma [code target: Set]: "(A = B) = (A ⊆ B ∧ B ⊆ A)" by blast declare bex_triv_one_point1 [symmetric, standard, code] types_code set ("_ list") attach (term_of) {* fun term_of_set f T [] = Const ("{}", Type ("set", [T])) | term_of_set f T (x :: xs) = Const ("insert", T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs; *} attach (test) {* fun gen_set' aG i j = frequency [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] () and gen_set aG i = gen_set' aG i i; *} consts_code "{}" ("[]") "insert" ("(_ ins _)") "op Un" ("(_ union _)") "op Int" ("(_ inter _)") "op -" :: "'a set => 'a set => 'a set" ("(_ \\\\ _)") "image" ("\<module>image") attach {* fun image f S = distinct (map f S); *} "UNION" ("\<module>UNION") attach {* fun UNION S f = Library.foldr Library.union (map f S, []); *} "INTER" ("\<module>INTER") attach {* fun INTER S f = Library.foldr1 Library.inter (map f S); *} "Bex" ("\<module>Bex") attach {* fun Bex S P = Library.exists P S; *} "Ball" ("\<module>Ball") attach {* fun Ball S P = Library.forall P S; *} end
lemma
(A = B) = (A ⊆ B ∧ B ⊆ A)