test-settheory.why 1.17 KB
 MARCHE Claude committed Oct 20, 2012 1 2 3 `````` theory TestOverriding `````` Andrei Paskevich committed Jun 15, 2018 4 5 6 7 `````` use settheory.Relation use settheory.InverseDomRan use settheory.Overriding use settheory.Function `````` MARCHE Claude committed Oct 20, 2012 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 `````` Andrei Paskevich committed Jun 15, 2018 31 32 33 34 `````` use settheory.Relation use settheory.InverseDomRan use settheory.Composition use settheory.Function `````` MARCHE Claude committed Oct 20, 2012 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 `````` Andrei Paskevich committed Jun 15, 2018 40 `````` use settheory.Interval `````` MARCHE Claude committed Oct 20, 2012 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 ``````