stdlib/set.mlw

   1
   2 (** {1 Set theories}
   3
   4   - polymorphic sets to be used in specification/ghost only
   5     (no executable functions)
   6
   7     - `Set`, `Cardinal`: possibly infinite sets
   8     - `Fset`, `FsetInt`, `FsetInduction`, `FsetSum`: finite sets
   9
  10   - monomorphic finite sets to be used in programs only (no logical functions)
  11
  12     a program function `eq` deciding equality on the element type must be
  13     provided when cloned
  14
  15     - `SetApp`, `SetAppInt`: immutable sets
  16     - `SetImp`, `SetImpInt`: mutable sets
  17
  18 *)
  19
  20 (** {2 Potentially infinite sets} *)
  21
  22 module Set
  23
  24   use map.Map
  25   use map.Const
  26
  27   type set 'a = map 'a bool
  28
  29   (** if `'a` is an infinite type, then `set 'a` is infinite *)
  30   meta "material_type_arg" type set, 0
  31
  32   (** membership *)
  33   predicate mem (x: 'a) (s: set 'a) = s[x]
  34
  35   use map.MapExt (* this imports extensionality for sets *)
  36 (*
  37 (** equality *)
  38   predicate (==) (s1 s2: set 'a) = forall x: 'a. mem x s1 <-> mem x s2
  39
  40   lemma extensionality:
  41     forall s1 s2: set 'a. s1 == s2 -> s1 = s2
  42
  43   meta extensionality predicate (==)
  44 *)
  45
  46   (** inclusion *)
  47   predicate subset (s1 s2: set 'a) = forall x : 'a. mem x s1 -> mem x s2
  48
  49   lemma subset_refl:
  50     forall s: set 'a. subset s s
  51
  52   lemma subset_trans:
  53     forall s1 s2 s3: set 'a. subset s1 s2 -> subset s2 s3 -> subset s1 s3
  54
  55   (** empty set *)
  56   predicate is_empty (s: set 'a) = forall x: 'a. not (mem x s)
  57
  58   let constant empty: set 'a = const false
  59
  60   lemma is_empty_empty: is_empty (empty: set 'a)
  61
  62   lemma empty_is_empty:
  63     forall s: set 'a. is_empty s -> s = empty
  64
  65   (** whole set *)
  66   let constant all: set 'a = const true
  67
  68   (** addition *)
  69   function add (x: 'a) (s: set 'a): set 'a = s[x <- true]
  70
  71   function singleton (x: 'a): set 'a = add x empty
  72
  73   lemma mem_singleton:
  74     forall x, y: 'a. mem y (singleton x) -> y = x
  75
  76   (** removal *)
  77   function remove (x: 'a) (s: set 'a): set 'a = s[x <- false]
  78
  79   lemma add_remove:
  80     forall x: 'a, s: set 'a. mem x s -> add x (remove x s) = s
  81
  82   lemma remove_add:
  83     forall x: 'a, s: set 'a. remove x (add x s) = remove x s
  84
  85   lemma subset_remove:
  86     forall x: 'a, s: set 'a. subset (remove x s) s
  87
  88   (** union *)
  89   function union (s1 s2: set 'a): set 'a
  90   = fun x -> mem x s1 \/ mem x s2
  91
  92   lemma subset_union_1:
  93     forall s1 s2: set 'a. subset s1 (union s1 s2)
  94   lemma subset_union_2:
  95     forall s1 s2: set 'a. subset s2 (union s1 s2)
  96
  97   (** intersection *)
  98   function inter (s1 s2: set 'a): set 'a
  99   = fun x -> mem x s1 /\ mem x s2
 100
 101   lemma subset_inter_1:
 102     forall s1 s2: set 'a. subset (inter s1 s2) s1
 103   lemma subset_inter_2:
 104     forall s1 s2: set 'a. subset (inter s1 s2) s2
 105
 106   (** difference *)
 107   function diff (s1 s2: set 'a): set 'a
 108   = fun x -> mem x s1 /\ not (mem x s2)
 109
 110   lemma subset_diff:
 111     forall s1 s2: set 'a. subset (diff s1 s2) s1
 112
 113   (** complement *)
 114   function complement (s: set 'a): set 'a
 115   = fun x -> not (mem x s)
 116
 117   (** arbitrary element *)
 118   function pick (s: set 'a): 'a
 119
 120   axiom pick_def: forall s: set 'a. not (is_empty s) -> mem (pick s) s
 121
 122   (** disjoint sets *)
 123   predicate disjoint (s1 s2: set 'a) =
 124     forall x. not (mem x s1) \/ not (mem x s2)
 125
 126   lemma disjoint_inter_empty:
 127     forall s1 s2: set 'a. disjoint s1 s2 <-> is_empty (inter s1 s2)
 128
 129   lemma disjoint_diff_eq:
 130     forall s1 s2: set 'a. disjoint s1 s2 <-> diff s1 s2 = s1
 131
 132   lemma disjoint_diff_s2:
 133     forall s1 s2: set 'a. disjoint (diff s1 s2) s2
 134
 135   (** `{ (x, y) | x in s1 /\ y in s2 }` *)
 136   function product (s1: set 'a) (s2: set 'b) : set ('a, 'b)
 137   axiom product_def:
 138     forall s1: set 'a, s2: set 'b, x : 'a, y : 'b.
 139     mem (x, y) (product s1 s2) <-> mem x s1 /\ mem y s2
 140
 141   (** `{ x | x in s /\ p x }` *)
 142   function filter (s: set 'a) (p: 'a -> bool) : set 'a
 143   axiom filter_def:
 144     forall s: set 'a, p: 'a -> bool, x: 'a. mem x (filter s p) <-> mem x s /\ p x
 145
 146   lemma subset_filter:
 147     forall s: set 'a, p: 'a -> bool. subset (filter s p) s
 148
 149   (** `{ f x | x in U }` *)
 150   function map (f: 'a -> 'b) (u: set 'a) : set 'b =
 151     fun (y: 'b) -> exists x: 'a. mem x u /\ y = f x
 152
 153   lemma mem_map:
 154     forall f: 'a -> 'b, u: set 'a.
 155     forall x: 'a. mem x u -> mem (f x) (map f u)
 156
 157 end
 158
 159 module Cardinal
 160
 161   use Set
 162
 163   predicate is_finite (s: set 'a)
 164
 165   axiom is_finite_empty:
 166     forall s: set 'a. is_empty s -> is_finite s
 167
 168   axiom is_finite_subset:
 169     forall s1 s2: set 'a. is_finite s2 -> subset s1 s2 -> is_finite s1
 170
 171   axiom is_finite_add:
 172     forall x: 'a, s: set 'a. is_finite s -> is_finite (add x s)
 173   axiom is_finite_add_rev:
 174     forall x: 'a, s: set 'a. is_finite (add x s) -> is_finite s
 175
 176   lemma is_finite_singleton:
 177     forall x: 'a. is_finite (singleton x)
 178
 179   axiom is_finite_remove:
 180     forall x: 'a, s: set 'a. is_finite s -> is_finite (remove x s)
 181   axiom is_finite_remove_rev:
 182     forall x: 'a, s: set 'a. is_finite (remove x s) -> is_finite s
 183
 184   axiom is_finite_union:
 185     forall s1 s2: set 'a.
 186     is_finite s1 -> is_finite s2 -> is_finite (union s1 s2)
 187   axiom is_finite_union_rev:
 188     forall s1 s2: set 'a.
 189     is_finite (union s1 s2) -> is_finite s1 /\ is_finite s2
 190
 191   axiom is_finite_inter_left:
 192     forall s1 s2: set 'a. is_finite s1 -> is_finite (inter s1 s2)
 193   axiom is_finite_inter_right:
 194     forall s1 s2: set 'a. is_finite s2 -> is_finite (inter s1 s2)
 195
 196   axiom is_finite_diff:
 197     forall s1 s2: set 'a. is_finite s1 -> is_finite (diff s1 s2)
 198
 199   lemma is_finite_map:
 200     forall f: 'a -> 'b, s: set 'a. is_finite s -> is_finite (map f s)
 201
 202   lemma is_finite_product:
 203     forall s1: set 'a, s2 : set 'b. is_finite s1 -> is_finite s2 ->
 204            is_finite (product s1 s2)
 205
 206   (** `cardinal` function *)
 207
 208   use int.Int
 209
 210   function cardinal (set 'a): int
 211
 212   axiom cardinal_nonneg:
 213     forall s: set 'a. cardinal s >= 0
 214
 215   axiom cardinal_empty:
 216     forall s: set 'a. is_finite s -> (is_empty s <-> cardinal s = 0)
 217
 218   axiom cardinal_add:
 219     forall x: 'a. forall s: set 'a. is_finite s ->
 220     if mem x s then cardinal (add x s) = cardinal s
 221                else cardinal (add x s) = cardinal s + 1
 222
 223   axiom cardinal_remove:
 224     forall x: 'a. forall s: set 'a. is_finite s ->
 225     if mem x s then cardinal (remove x s) = cardinal s - 1
 226                else cardinal (remove x s) = cardinal s
 227
 228   axiom cardinal_subset:
 229     forall s1 s2: set 'a. is_finite s2 ->
 230     subset s1 s2 -> cardinal s1 <= cardinal s2
 231
 232   lemma subset_eq:
 233     forall s1 s2: set 'a. is_finite s2 ->
 234     subset s1 s2 -> cardinal s1 = cardinal s2 -> s1 = s2
 235
 236   lemma cardinal1:
 237     forall s: set 'a. cardinal s = 1 ->
 238     forall x: 'a. mem x s -> x = pick s
 239
 240   axiom cardinal_union:
 241     forall s1 s2: set 'a. is_finite s1 -> is_finite s2 ->
 242     cardinal (union s1 s2) = cardinal s1 + cardinal s2 - cardinal (inter s1 s2)
 243
 244   lemma cardinal_inter_disjoint:
 245     forall s1 s2: set 'a. disjoint s1 s2 -> cardinal (inter s1 s2) = 0
 246
 247   axiom cardinal_diff:
 248     forall s1 s2: set 'a. is_finite s1 ->
 249     cardinal (diff s1 s2) = cardinal s1 - cardinal (inter s1 s2)
 250
 251   lemma cardinal_map:
 252     forall f: 'a -> 'b, s: set 'a. is_finite s ->
 253     cardinal (map f s) <= cardinal s
 254
 255   lemma cardinal_product:
 256     forall s1: set 'a, s2 : set 'b. is_finite s1 -> is_finite s2 ->
 257     cardinal (product s1 s2) = cardinal s1 * cardinal s2
 258 end
 259
 260 (** {2 Finite sets} *)
 261
 262 module Fset
 263
 264   type fset 'a
 265
 266   (** if `'a` is an infinite type, then `fset 'a` is infinite *)
 267   meta "material_type_arg" type fset, 0
 268
 269   (** membership *)
 270   predicate mem (x: 'a) (s: fset 'a) (* = s.to_map[x] *)
 271
 272   (** equality *)
 273   predicate (==) (s1 s2: fset 'a) = forall x: 'a. mem x s1 <-> mem x s2
 274
 275   lemma extensionality:
 276     forall s1 s2: fset 'a. s1 == s2 -> s1 = s2
 277
 278   meta extensionality predicate (==)
 279
 280   (** inclusion *)
 281   predicate subset (s1 s2: fset 'a) = forall x : 'a. mem x s1 -> mem x s2
 282
 283   lemma subset_refl:
 284     forall s: fset 'a. subset s s
 285
 286   lemma subset_trans:
 287     forall s1 s2 s3: fset 'a. subset s1 s2 -> subset s2 s3 -> subset s1 s3
 288
 289   (** empty set *)
 290   predicate is_empty (s: fset 'a) = forall x: 'a. not (mem x s)
 291
 292   constant empty: fset 'a
 293   (* axiom empty_def: (empty: fset 'a).to_map = const false *)
 294
 295   axiom is_empty_empty: is_empty (empty: fset 'a)
 296
 297   lemma empty_is_empty:
 298     forall s: fset 'a. is_empty s -> s = empty
 299
 300   (** addition *)
 301   function add (x: 'a) (s: fset 'a) : fset 'a
 302   axiom add_def:
 303     forall x: 'a, s: fset 'a, y: 'a. mem y (add x s) <-> (mem y s \/ y = x)
 304
 305   function singleton (x: 'a): fset 'a = add x empty
 306
 307   lemma mem_singleton:
 308     forall x, y: 'a. mem y (singleton x) -> y = x
 309
 310   (** removal *)
 311   function remove (x: 'a) (s: fset 'a) : fset 'a
 312   axiom remove_def:
 313     forall x: 'a, s: fset 'a, y: 'a. mem y (remove x s) <-> (mem y s /\ y <> x)
 314
 315   lemma add_remove:
 316     forall x: 'a, s: fset 'a. mem x s -> add x (remove x s) = s
 317
 318   lemma remove_add:
 319     forall x: 'a, s: fset 'a. remove x (add x s) = remove x s
 320
 321   lemma subset_remove:
 322     forall x: 'a, s: fset 'a. subset (remove x s) s
 323
 324   (** union *)
 325   function union (s1 s2: fset 'a): fset 'a
 326   axiom union_def:
 327     forall s1 s2: fset 'a, x: 'a. mem x (union s1 s2) <-> mem x s1 \/ mem x s2
 328
 329   lemma subset_union_1:
 330     forall s1 s2: fset 'a. subset s1 (union s1 s2)
 331   lemma subset_union_2:
 332     forall s1 s2: fset 'a. subset s2 (union s1 s2)
 333
 334   (** intersection *)
 335   function inter (s1 s2: fset 'a): fset 'a
 336   axiom inter_def:
 337     forall s1 s2: fset 'a, x: 'a. mem x (inter s1 s2) <-> mem x s1 /\ mem x s2
 338
 339   lemma subset_inter_1:
 340     forall s1 s2: fset 'a. subset (inter s1 s2) s1
 341   lemma subset_inter_2:
 342     forall s1 s2: fset 'a. subset (inter s1 s2) s2
 343
 344   (** difference *)
 345   function diff (s1 s2: fset 'a): fset 'a
 346   axiom diff_def:
 347     forall s1 s2: fset 'a, x: 'a. mem x (diff s1 s2) <-> mem x s1 /\ not (mem x s2)
 348
 349   lemma subset_diff:
 350     forall s1 s2: fset 'a. subset (diff s1 s2) s1
 351
 352   (** arbitrary element *)
 353   function pick (s: fset 'a): 'a
 354
 355   axiom pick_def: forall s: fset 'a. not (is_empty s) -> mem (pick s) s
 356
 357   (** disjoint sets *)
 358   predicate disjoint (s1 s2: fset 'a) =
 359     forall x. not (mem x s1) \/ not (mem x s2)
 360
 361   lemma disjoint_inter_empty:
 362     forall s1 s2: fset 'a. disjoint s1 s2 <-> is_empty (inter s1 s2)
 363
 364   lemma disjoint_diff_eq:
 365     forall s1 s2: fset 'a. disjoint s1 s2 <-> diff s1 s2 = s1
 366
 367   lemma disjoint_diff_s2:
 368     forall s1 s2: fset 'a. disjoint (diff s1 s2) s2
 369
 370   (** `{ x | x in s /\ p x }` *)
 371   function filter (s: fset 'a) (p: 'a -> bool) : fset 'a
 372   axiom filter_def:
 373     forall s: fset 'a, p: 'a -> bool, x: 'a. mem x (filter s p) <-> mem x s /\ p x
 374
 375   lemma subset_filter:
 376     forall s: fset 'a, p: 'a -> bool. subset (filter s p) s
 377
 378   (** `{ f x | x in U }` *)
 379   function map (f: 'a -> 'b) (u: fset 'a) : fset 'b
 380   axiom map_def:
 381     forall f: 'a -> 'b, u: fset 'a, y: 'b.
 382     mem y (map f u) <-> exists x: 'a. mem x u /\ y = f x
 383
 384   lemma mem_map:
 385     forall f: 'a -> 'b, u: fset 'a.
 386     forall x: 'a. mem x u -> mem (f x) (map f u)
 387
 388   (** cardinal *)
 389
 390   use int.Int
 391
 392   function cardinal (fset 'a) : int
 393
 394   axiom cardinal_nonneg:
 395     forall s: fset 'a. cardinal s >= 0
 396
 397   axiom cardinal_empty:
 398     forall s: fset 'a. is_empty s <-> cardinal s = 0
 399
 400   axiom cardinal_add:
 401     forall x: 'a. forall s: fset 'a.
 402     if mem x s then cardinal (add x s) = cardinal s
 403                else cardinal (add x s) = cardinal s + 1
 404
 405   axiom cardinal_remove:
 406     forall x: 'a. forall s: fset 'a.
 407     if mem x s then cardinal (remove x s) = cardinal s - 1
 408                else cardinal (remove x s) = cardinal s
 409
 410   axiom cardinal_subset:
 411     forall s1 s2: fset 'a.
 412     subset s1 s2 -> cardinal s1 <= cardinal s2
 413
 414   lemma subset_eq:
 415     forall s1 s2: fset 'a.
 416     subset s1 s2 -> cardinal s1 = cardinal s2 -> s1 = s2
 417
 418   lemma cardinal1:
 419     forall s: fset 'a. cardinal s = 1 ->
 420     forall x: 'a. mem x s -> x = pick s
 421
 422   axiom cardinal_union:
 423     forall s1 s2: fset 'a.
 424     cardinal (union s1 s2) = cardinal s1 + cardinal s2 - cardinal (inter s1 s2)
 425
 426   lemma cardinal_inter_disjoint:
 427     forall s1 s2: fset 'a. disjoint s1 s2 -> cardinal (inter s1 s2) = 0
 428
 429   axiom cardinal_diff:
 430     forall s1 s2: fset 'a.
 431     cardinal (diff s1 s2) = cardinal s1 - cardinal (inter s1 s2)
 432
 433   lemma cardinal_filter:
 434     forall s: fset 'a, p: 'a -> bool.
 435     cardinal (filter s p) <= cardinal s
 436
 437   lemma cardinal_map:
 438     forall f: 'a -> 'b, s: fset 'a.
 439     cardinal (map f s) <= cardinal s
 440
 441 end
 442
 443 (** {2 Induction principle on finite sets} *)
 444
 445 module FsetInduction
 446
 447   use Fset
 448
 449   type t
 450
 451   predicate p (fset t)
 452
 453   lemma Induction:
 454     (forall s: fset t. is_empty s -> p s) ->
 455     (forall s: fset t. p s -> forall t. p (add t s)) ->
 456     forall s: fset t. p s
 457
 458 end
 459
 460 (** {2 Finite sets of integers} *)
 461
 462 module FsetInt
 463
 464   use int.Int
 465   use export Fset
 466
 467   function min_elt (s: fset int) : int
 468
 469   axiom min_elt_def:
 470     forall s: fset int. not (is_empty s) ->
 471     mem (min_elt s) s /\ forall x. mem x s -> min_elt s <= x
 472
 473   function max_elt (s: fset int) : int
 474
 475   axiom max_elt_def:
 476     forall s: fset int. not (is_empty s) ->
 477     mem (max_elt s) s /\ forall x. mem x s -> x <= max_elt s
 478
 479   function interval (l r: int) : fset int
 480   axiom interval_def:
 481     forall l r x. mem x (interval l r) <-> l <= x < r
 482
 483   lemma cardinal_interval:
 484     forall l r. cardinal (interval l r) = if l <= r then r - l else 0
 485
 486 end
 487
 488 (** {2 Sum of a function over a finite set} *)
 489
 490 module FsetSum
 491
 492   use int.Int
 493   use Fset
 494
 495   function sum (fset 'a) ('a -> int) : int
 496   (** `sum s f` is the sum `\sum_{mem x s} f x` *)
 497
 498   axiom sum_def_empty:
 499     forall s: fset 'a, f. is_empty s -> sum s f = 0
 500
 501   axiom sum_add:
 502     forall s: fset 'a, f, x.
 503     if mem x s then sum (add x s) f = sum s f
 504                else sum (add x s) f = sum s f + f x
 505
 506   axiom sum_remove:
 507     forall s: fset 'a, f, x.
 508     if mem x s then sum (remove x s) f = sum s f - f x
 509                else sum (remove x s) f = sum s f
 510
 511   lemma sum_union:
 512     forall s1 s2: fset 'a. forall f.
 513     sum (union s1 s2) f = sum s1 f + sum s2 f - sum (inter s1 s2) f
 514
 515   lemma sum_eq:
 516     forall s: fset 'a. forall f g.
 517     (forall x. mem x s -> f x = g x) -> sum s f = sum s g
 518
 519   axiom cardinal_is_sum:
 520     forall s: fset 'a. cardinal s = sum s (fun _ -> 1)
 521
 522 end
 523
 524 (** {2 Finite Monomorphic sets}
 525
 526     To be used in programs. *)
 527
 528 (** {3 Applicative sets} *)
 529
 530 module SetApp
 531
 532   use int.Int
 533   use export Fset
 534
 535   type elt
 536
 537   val eq (x y: elt) : bool
 538     ensures { result <-> x = y }
 539
 540   type set = abstract {
 541     to_fset: fset elt;
 542   }
 543   meta coercion function to_fset
 544
 545   val ghost function mk (s: fset elt) : set
 546     ensures { result.to_fset = s }
 547
 548   val mem (x: elt) (s: set) : bool
 549     ensures { result <-> mem x s }
 550
 551   val (==) (s1 s2: set) : bool
 552     ensures { result <-> s1 == s2 }
 553
 554   val subset (s1 s2: set) : bool
 555     ensures { result <-> subset s1 s2 }
 556
 557   val empty () : set
 558     ensures { result.to_fset = empty }
 559     ensures { cardinal result = 0 }
 560
 561   val is_empty (s: set) : bool
 562     ensures { result <-> is_empty s }
 563
 564   val add (x: elt) (s: set) : set
 565     ensures { result = add x s }
 566     ensures { if mem x s then cardinal result = cardinal s
 567                          else cardinal result = cardinal s + 1 }
 568
 569   let singleton (x: elt) : set
 570     ensures { result = singleton x }
 571     ensures { cardinal result = 1 }
 572   = add x (empty ())
 573
 574   val remove (x: elt) (s: set): set
 575     ensures { result = remove x s }
 576     ensures { if mem x s then cardinal result = cardinal s - 1
 577                          else cardinal result = cardinal s }
 578
 579   val union (s1 s2: set): set
 580     ensures { result = union s1 s2 }
 581
 582   val inter (s1 s2: set) : set
 583     ensures { result = inter s1 s2 }
 584
 585   val diff (s1 s2: set) : set
 586     ensures { result = diff s1 s2 }
 587
 588   val function choose (s: set) : elt
 589     requires { not (is_empty s) }
 590     ensures  { mem result s }
 591
 592   val disjoint (s1 s2: set) : bool
 593     ensures { result <-> disjoint s1 s2 }
 594
 595   val cardinal (s: set) : int (* Peano.t *)
 596     ensures { result = cardinal s }
 597
 598 end
 599
 600 (** {3 Applicative sets of integers} *)
 601
 602 module SetAppInt
 603
 604   use int.Int
 605   use export FsetInt
 606
 607   clone export SetApp with type elt = int, val eq = Int.(=), axiom .
 608
 609   val min_elt (s: set) : int
 610     requires { not (is_empty s) }
 611     ensures  { result = min_elt s }
 612
 613   val max_elt (s: set) : int
 614     requires { not (is_empty s) }
 615     ensures  { result = max_elt s }
 616
 617   val interval (l r: int) : set
 618     ensures  { result = interval l r }
 619     ensures  { cardinal result = if l <= r then r - l else 0 }
 620
 621 end
 622
 623 (** {3 Imperative sets} *)
 624
 625 module SetImp
 626
 627   use int.Int
 628   use export Fset
 629
 630   type elt
 631
 632   val eq (x y: elt) : bool
 633     ensures { result <-> x = y }
 634
 635   type set = abstract {
 636     mutable to_fset: fset elt;
 637   }
 638   meta coercion function to_fset
 639
 640   val mem (x: elt) (s: set) : bool
 641     ensures { result <-> mem x s }
 642
 643   val (==) (s1 s2: set) : bool
 644     ensures { result <-> s1 == s2 }
 645
 646   val subset (s1 s2: set) : bool
 647     ensures { result <-> subset s1 s2 }
 648
 649   val empty () : set
 650     ensures { result = empty }
 651     ensures { cardinal result = 0 }
 652
 653   val clear (s: set) : unit
 654     writes  { s }
 655     ensures { s = empty }
 656
 657   val is_empty (s: set) : bool
 658     ensures { result <-> is_empty s }
 659
 660   val add (x: elt) (s: set) : unit
 661     writes  { s }
 662     ensures { s = add x (old s) }
 663     ensures { if mem x (old s) then cardinal s = cardinal (old s)
 664                                else cardinal s = cardinal (old s) + 1 }
 665
 666   let singleton (x: elt) : set
 667     ensures { result = singleton x }
 668     ensures { cardinal result = 1 }
 669   = let s = empty () in
 670     add x s;
 671     s
 672
 673   val remove (x: elt) (s: set) : unit
 674     writes  { s }
 675     ensures { s = remove x (old s) }
 676     ensures { if mem x (old s) then cardinal s = cardinal (old s) - 1
 677                                else cardinal s = cardinal (old s) }
 678
 679   val function choose (s: set) : elt
 680     requires { not (is_empty s) }
 681     ensures  { mem result s }
 682
 683   val choose_and_remove (s: set) : elt
 684     requires { not (is_empty s) }
 685     writes   { s }
 686     ensures  { result = choose (old s) }
 687     ensures  { mem result (old s) }
 688     ensures  { s = remove result (old s) }
 689
 690   val disjoint (s1 s2: set) : bool
 691     ensures { result <-> disjoint s1 s2 }
 692
 693   val cardinal (s: set) : int (* Peano.t? *)
 694     ensures { result = cardinal s }
 695
 696 end
 697
 698 (** {3 Imperative sets of integers}
 699
 700     This module is mapped to OCaml's Hashtbl in the OCaml driver.
 701 *)
 702
 703 module SetImpInt
 704
 705   use int.Int
 706   use export FsetInt
 707
 708   clone export SetImp with type elt = int, val eq = Int.(=), axiom .
 709
 710 end