test-settheory.why 1.17 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3

theory TestOverriding

4 5 6 7
  use settheory.Relation
  use settheory.InverseDomRan
  use settheory.Overriding
  use settheory.Function
MARCHE Claude's avatar
MARCHE Claude committed
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30

  constant f : rel int int = singleton (3,4)
  constant g : rel int int = f <+ (singleton (5,6))
  constant h : rel int int = g <+ (singleton (3,7))

  goal testdom1: mem 3 (dom g)
  goal testdom2: mem 3 (dom h)

  goal testapply1: apply f 3 = 4

  goal testapply2: apply g 3 = 4
  goal testapply3: apply g 5 = 6

  goal testapply4: apply h 3 = 7
  goal testapply5: apply h 5 = 6

  goal testapply_smoke1: apply h 3 = 8
  goal testapply_smoke2: apply h 5 = 9

end

theory TestCompose

31 32 33 34
  use settheory.Relation
  use settheory.InverseDomRan
  use settheory.Composition
  use settheory.Function
MARCHE Claude's avatar
MARCHE Claude committed
35 36 37 38 39

  constant f : rel int int = singleton (3,4)
  constant g : rel int int = singleton (4,6)
  constant h : rel int int = semicolon f g

40
  use settheory.Interval
MARCHE Claude's avatar
MARCHE Claude committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60

  constant fun_int_int : set (rel int int) = integer +-> integer

(*
  lemma f_is_fun : mem f fun_int_int

  lemma g_is_fun : mem g fun_int_int

  lemma h_is_fun : mem h fun_int_int
*)

  goal test1: mem (apply h 3) (Interval.mk 0 10)

  goal test2: 0 <= apply h 3 <= 10

  goal test3: apply h 3 = 6


end