1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
module Config
meta "select_inst" "goal"
meta "select_lskept" "goal"
meta "select_lsinst" "goal"
end
module Func
use Config
predicate extensionalEqual (f g:'a -> 'b) =
forall x:'a. f x = g x
(* Assume extensionality of function. *)
axiom functionExtensionality [@W:non_conservative_extension:N] :
forall f g:'a -> 'b. extensionalEqual f g -> f = g
(* Mainly for use in whyml *)
function eval (f:'a -> 'b) (x:'a) : 'b = f x
(* Abstraction definition axiom :
update (f:'a -> 'b) (x:'a) (y:'b) : 'a -> 'b =
(\ z:'a. if x = z then y else f z) *)
function update (f:'a -> 'b) (x:'a) (y:'b) : 'a -> 'b
axiom update_def : forall f:'a -> 'b,x:'a,y:'b,z:'a.
update f x y z = if x = z then y else f z
function ([<-])(f:'a -> 'b) (x:'a) (y:'b) : 'a -> 'b = update f x y
lemma update_eq : forall f:'a -> 'b,x:'a,y:'b.
update f x y x = y
lemma update_neq : forall f:'a -> 'b,x:'a,y:'b,z:'a.
x <> z -> update f x y z = f z
(* Abstraction definition axiom :
constant identity : 'a -> 'a = (\ x:'a. x) *)
constant identity : 'a -> 'a
axiom identity_def : forall x:'a. identity x = x
(* Abstraction definition axiom :
function compose (g:'b -> 'c) (f:'a -> 'b) : func 'a 'c =
(\ x:'a. g (f x)) *)
function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c
axiom compose_def : forall g:'b -> 'c,f:'a -> 'b,x:'a.
compose g f x = g (f x)
function rcompose (f:'a -> 'b) (g:'b -> 'c) : 'a -> 'c = compose g f
let lemma compose_associative (h:'c -> 'd) (g:'b -> 'c) (f:'a -> 'b) : unit
ensures { compose (compose h g) f = compose h (compose g f) }
=
assert { extensionalEqual (compose (compose h g) f) (compose h (compose g f)) }
let lemma identity_neutral (f:'a -> 'b) : unit
ensures { compose f identity = f }
ensures { compose identity f = f }
=
assert { extensionalEqual (compose f identity) f } ;
assert { extensionalEqual (compose identity f) f }
(* Abstraction definition axiom :
function const (x:'b) : 'a -> 'b =
(\ z:'a.x) *)
function const (x: 'b) : 'a -> 'b
axiom const_def : forall x:'b,z:'a. const x z = x
let lemma const_compose_left (f:'a -> 'b) (x:'c) : unit
ensures { compose (const x) f = const x }
=
assert { extensionalEqual (const x) (compose (const x) f) }
let lemma const_compose_right (f:'a -> 'b) (x:'a) (_:'c) : unit
ensures { compose f (const x) = (const (f x): 'c -> 'b) }
=
assert { extensionalEqual (const (f x) : 'c -> 'b) (compose f (const x)) }
end
|
