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