tests/test-settheory.why

   1
   2 theory TestOverriding
   3
   4   use settheory.Relation
   5   use settheory.InverseDomRan
   6   use settheory.Overriding
   7   use settheory.Function
   8
   9   constant f : rel int int = singleton (3,4)
  10   constant g : rel int int = f <+ (singleton (5,6))
  11   constant h : rel int int = g <+ (singleton (3,7))
  12
  13   goal testdom1: mem 3 (dom g)
  14   goal testdom2: mem 3 (dom h)
  15
  16   goal testapply1: apply f 3 = 4
  17
  18   goal testapply2: apply g 3 = 4
  19   goal testapply3: apply g 5 = 6
  20
  21   goal testapply4: apply h 3 = 7
  22   goal testapply5: apply h 5 = 6
  23
  24   goal testapply_smoke1: apply h 3 = 8
  25   goal testapply_smoke2: apply h 5 = 9
  26
  27 end
  28
  29 theory TestCompose
  30
  31   use settheory.Relation
  32   use settheory.InverseDomRan
  33   use settheory.Composition
  34   use settheory.Function
  35
  36   constant f : rel int int = singleton (3,4)
  37   constant g : rel int int = singleton (4,6)
  38   constant h : rel int int = semicolon f g
  39
  40   use settheory.Interval
  41
  42   constant fun_int_int : set (rel int int) = integer +-> integer
  43
  44 (*
  45   lemma f_is_fun : mem f fun_int_int
  46
  47   lemma g_is_fun : mem g fun_int_int
  48
  49   lemma h_is_fun : mem h fun_int_int
  50 *)
  51
  52   goal test1: mem (apply h 3) (Interval.mk 0 10)
  53
  54   goal test2: 0 <= apply h 3 <= 10
  55
  56   goal test3: apply h 3 = 6
  57
  58
  59 end
  60