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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
|
let assign = new_definition
`Assign (f:S->S) (q:S->bool) = q o f`;;
parse_as_infix(";;",(18,"right"));;
let sequence = new_definition
`(c1:(S->bool)->(S->bool)) ;; (c2:(S->bool)->(S->bool)) = c1 o c2`;;
let if_def = new_definition
`If e (c:(S->bool)->(S->bool)) q = {s | if e s then c q s else q s}`;;
let ite_def = new_definition
`Ite e (c1:(S->bool)->(S->bool)) c2 q =
{s | if e s then c1 q s else c2 q s}`;;
let while_RULES,while_INDUCT,while_CASES = new_inductive_definition
`!q s. If e (c ;; while e c) q s ==> while e c q s`;;
let while_def = new_definition
`While e c q =
{s | !w. (!s:S. (if e(s) then c w s else q s) ==> w s) ==> w s}`;;
let monotonic = new_definition
`monotonic c <=> !q q'. q SUBSET q' ==> (c q) SUBSET (c q')`;;
let MONOTONIC_ASSIGN = prove
(`monotonic (Assign f)`,
SIMP_TAC[monotonic; assign; SUBSET; o_THM; IN]);;
let MONOTONIC_IF = prove
(`monotonic c ==> monotonic (If e c)`,
REWRITE_TAC[monotonic; if_def] THEN SET_TAC[]);;
let MONOTONIC_ITE = prove
(`monotonic c1 /\ monotonic c2 ==> monotonic (Ite e c1 c2)`,
REWRITE_TAC[monotonic; ite_def] THEN SET_TAC[]);;
let MONOTONIC_SEQ = prove
(`monotonic c1 /\ monotonic c2 ==> monotonic (c1 ;; c2)`,
REWRITE_TAC[monotonic; sequence; o_THM] THEN SET_TAC[]);;
let MONOTONIC_WHILE = prove
(`monotonic c ==> monotonic(While e c)`,
REWRITE_TAC[monotonic; while_def] THEN SET_TAC[]);;
let WHILE_THM = prove
(`!e c q:S->bool.
monotonic c
==> (!s. If e (c ;; While e c) q s ==> While e c q s) /\
(!w'. (!s. If e (c ;; (\q. w')) q s ==> w' s)
==> (!a. While e c q a ==> w' a)) /\
(!s. While e c q s <=> If e (c ;; While e c) q s)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
(MP_TAC o GEN_ALL o DISCH_ALL o derive_nonschematic_inductive_relations)
`!s:S. (if e s then c w s else q s) ==> w s` THEN
REWRITE_TAC[if_def; sequence; o_THM; IN_ELIM_THM; IMP_IMP] THEN
DISCH_THEN MATCH_MP_TAC THEN
REWRITE_TAC[FUN_EQ_THM; while_def; IN_ELIM_THM] THEN
POP_ASSUM MP_TAC THEN REWRITE_TAC[monotonic] THEN SET_TAC[]);;
let WHILE_FIX = prove
(`!e c. monotonic c ==> (While e c = If e (c ;; While e c))`,
REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[WHILE_THM]);;
let correct = new_definition
`correct p c q <=> p SUBSET (c q)`;;
let CORRECT_PRESTRENGTH = prove
(`!p p' c q. p SUBSET p' /\ correct p' c q ==> correct p c q`,
REWRITE_TAC[correct; SUBSET_TRANS]);;
let CORRECT_POSTWEAK = prove
(`!p c q q'. monotonic c /\ correct p c q' /\ q' SUBSET q ==> correct p c q`,
REWRITE_TAC[correct; monotonic] THEN SET_TAC[]);;
let CORRECT_ASSIGN = prove
(`!p f q. (p SUBSET (q o f)) ==> correct p (Assign f) q`,
REWRITE_TAC[correct; assign]);;
let CORRECT_SEQ = prove
(`!p q r c1 c2.
monotonic c1 /\ correct p c1 r /\ correct r c2 q
==> correct p (c1 ;; c2) q`,
REWRITE_TAC[correct; sequence; monotonic; o_THM] THEN SET_TAC[]);;
let CORRECT_ITE = prove
(`!p e c1 c2 q.
correct (p INTER e) c1 q /\ correct (p INTER (UNIV DIFF e)) c2 q
==> correct p (Ite e c1 c2) q`,
REWRITE_TAC[correct; ite_def] THEN SET_TAC[]);;
let CORRECT_IF = prove
(`!p e c q.
correct (p INTER e) c q /\ p INTER (UNIV DIFF e) SUBSET q
==> correct p (If e c) q`,
REWRITE_TAC[correct; if_def] THEN SET_TAC[]);;
let CORRECT_WHILE = prove
(`!(<<) p c q e invariant.
monotonic c /\
WF(<<) /\
p SUBSET invariant /\
(UNIV DIFF e) INTER invariant SUBSET q /\
(!X:S. correct (invariant INTER e INTER (\s. X = s)) c
(invariant INTER (\s. s << X)))
==> correct p (While e c) q`,
REWRITE_TAC[correct; SUBSET; IN_INTER; IN_UNIV; IN_DIFF; IN] THEN
REPEAT GEN_TAC THEN STRIP_TAC THEN
SUBGOAL_THEN `!s:S. invariant s ==> While e c q s` MP_TAC THENL
[ALL_TAC; ASM_MESON_TAC[]] THEN
FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[WF_IND]) THEN
X_GEN_TAC `s:S` THEN REPEAT DISCH_TAC THEN
FIRST_ASSUM(fun th -> ONCE_REWRITE_TAC[MATCH_MP WHILE_FIX th]) THEN
REWRITE_TAC[if_def; sequence; o_THM; IN_ELIM_THM] THEN
COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
FIRST_X_ASSUM(MP_TAC o SPECL [`s:S`; `s:S`]) THEN ASM_REWRITE_TAC[] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [monotonic]) THEN
REWRITE_TAC[SUBSET; IN; RIGHT_IMP_FORALL_THM] THEN
DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC[INTER; IN_ELIM_THM; IN]);;
let assert_def = new_definition
`assert (p:S->bool) (q:S->bool) = q`;;
let variant_def = new_definition
`variant ((<<):S->S->bool) (q:S->bool) = q`;;
let CORRECT_SEQ_VC = prove
(`!p q r c1 c2.
monotonic c1 /\ correct p c1 r /\ correct r c2 q
==> correct p (c1 ;; assert r ;; c2) q`,
REWRITE_TAC[correct; sequence; monotonic; assert_def; o_THM] THEN SET_TAC[]);;
let CORRECT_WHILE_VC = prove
(`!(<<) p c q e invariant.
monotonic c /\
WF(<<) /\
p SUBSET invariant /\
(UNIV DIFF e) INTER invariant SUBSET q /\
(!X:S. correct (invariant INTER e INTER (\s. X = s)) c
(invariant INTER (\s. s << X)))
==> correct p (While e (assert invariant ;; variant(<<) ;; c)) q`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[sequence; variant_def; assert_def; o_DEF; ETA_AX] THEN
ASM_MESON_TAC[CORRECT_WHILE]);;
let MONOTONIC_ASSERT = prove
(`monotonic (assert p)`,
REWRITE_TAC[assert_def; monotonic]);;
let MONOTONIC_VARIANT = prove
(`monotonic (variant p)`,
REWRITE_TAC[variant_def; monotonic]);;
let MONO_TAC =
REPEAT(MATCH_MP_TAC MONOTONIC_WHILE ORELSE
(MAP_FIRST MATCH_MP_TAC
[MONOTONIC_SEQ; MONOTONIC_IF; MONOTONIC_ITE] THEN CONJ_TAC)) THEN
MAP_FIRST MATCH_ACCEPT_TAC
[MONOTONIC_ASSIGN; MONOTONIC_ASSERT; MONOTONIC_VARIANT];;
let VC_TAC =
FIRST
[MATCH_MP_TAC CORRECT_SEQ_VC THEN CONJ_TAC THENL [MONO_TAC; CONJ_TAC];
MATCH_MP_TAC CORRECT_ITE THEN CONJ_TAC;
MATCH_MP_TAC CORRECT_IF THEN CONJ_TAC;
MATCH_MP_TAC CORRECT_WHILE_VC THEN REPEAT CONJ_TAC THENL
[MONO_TAC; TRY(MATCH_ACCEPT_TAC WF_MEASURE); ALL_TAC; ALL_TAC;
REWRITE_TAC[FORALL_PAIR_THM; MEASURE] THEN REPEAT GEN_TAC];
MATCH_MP_TAC CORRECT_ASSIGN];;
needs "Library/prime.ml";;
(* ------------------------------------------------------------------------- *)
(* x = m, y = n; *)
(* while (!(x == 0 || y == 0)) *)
(* { if (x < y) y = y - x; *)
(* else x = x - y; *)
(* } *)
(* if (x == 0) x = y; *)
(* ------------------------------------------------------------------------- *)
g `correct
(\(m,n,x,y). T)
(Assign (\(m,n,x,y). m,n,m,n) ;; // x,y := m,n
assert (\(m,n,x,y). x = m /\ y = n) ;;
While (\(m,n,x,y). ~(x = 0 \/ y = 0))
(assert (\(m,n,x,y). gcd(x,y) = gcd(m,n)) ;;
variant(MEASURE(\(m,n,x,y). x + y)) ;;
Ite (\(m,n,x,y). x < y)
(Assign (\(m,n,x,y). m,n,x,y - x))
(Assign (\(m,n,x,y). m,n,x - y,y))) ;;
assert (\(m,n,x,y). (x = 0 \/ y = 0) /\ gcd(x,y) = gcd(m,n)) ;;
If (\(m,n,x,y). x = 0) (Assign (\(m,n,x,y). (m,n,y,y))))
(\(m,n,x,y). gcd(m,n) = x)`;;
e(REPEAT VC_TAC);;
b();;
e(REPEAT VC_TAC THEN REWRITE_TAC[SUBSET; FORALL_PAIR_THM] THEN
MAP_EVERY X_GEN_TAC [`m:num`; `n:num`; `x:num`; `y:num`] THEN
REWRITE_TAC[IN; INTER; UNIV; DIFF; o_DEF; IN_ELIM_THM; PAIR_EQ] THEN
CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV) THEN SIMP_TAC[]);;
e(SIMP_TAC[GCD_SUB; LT_IMP_LE]);;
e ARITH_TAC;;
e(SIMP_TAC[GCD_SUB; NOT_LT] THEN ARITH_TAC);;
e(MESON_TAC[GCD_0]);;
e(MESON_TAC[GCD_0; GCD_SYM]);;
parse_as_infix("refines",(12,"right"));;
let refines = new_definition
`c2 refines c1 <=> !q. c1(q) SUBSET c2(q)`;;
let REFINES_REFL = prove
(`!c. c refines c`,
REWRITE_TAC[refines; SUBSET_REFL]);;
let REFINES_TRANS = prove
(`!c1 c2 c3. c3 refines c2 /\ c2 refines c1 ==> c3 refines c1`,
REWRITE_TAC[refines] THEN MESON_TAC[SUBSET_TRANS]);;
let REFINES_CORRECT = prove
(`correct p c1 q /\ c2 refines c1 ==> correct p c2 q`,
REWRITE_TAC[correct; refines] THEN MESON_TAC[SUBSET_TRANS]);;
let REFINES_WHILE = prove
(`c' refines c ==> While e c' refines While e c`,
REWRITE_TAC[refines; while_def; SUBSET; IN_ELIM_THM; IN] THEN MESON_TAC[]);;
let specification = new_definition
`specification(p,q) r = if q SUBSET r then p else {}`;;
let REFINES_SPECIFICATION = prove
(`c refines specification(p,q) ==> correct p c q`,
REWRITE_TAC[specification; correct; refines] THEN
MESON_TAC[SUBSET_REFL; SUBSET_EMPTY]);;
|
