WhileScript.sml
1(*===========================================================================*)
2(* Define WHILE loops, give Hoare rules, and define LEAST operator as a *)
3(* binder. *)
4(*===========================================================================*)
5Theory While[bare]
6Ancestors
7 combin option sum prim_rec arithmetic relation
8Libs
9 HolKernel boolLib Parse BasicProvers Prim_rec simpLib boolSimps
10 metisLib
11
12
13local open OpenTheoryMap
14 val ns = ["While"]
15in
16 fun ot0 x y = OpenTheory_const_name{const={Thy="While",Name=x},name=(ns,y)}
17 fun ot x = ot0 x x
18end
19
20fun INDUCT_TAC g = INDUCT_THEN numTheory.INDUCTION ASSUME_TAC g;
21fun simp ths = asm_simp_tac (srw_ss()) ths
22
23Theorem cond_lemma[local]:
24 (if ~p then q else r) = (if p then r else q)
25Proof
26 Q.ASM_CASES_TAC `p` THEN ASM_REWRITE_TAC []
27QED
28
29(* ----------------------------------------------------------------------
30 Existence of WHILE
31 ---------------------------------------------------------------------- *)
32
33Theorem ITERATION:
34 !P g. ?f. !x. f x = if P x then x else f (g x)
35Proof
36 REPEAT GEN_TAC THEN
37 Q.EXISTS_TAC `\x. if ?n. P (FUNPOW g n x) then
38 FUNPOW g (@n. P (FUNPOW g n x) /\
39 !m. m < n ==> ~P (FUNPOW g m x)) x
40 else ARB` THEN BETA_TAC THEN
41 GEN_TAC THEN COND_CASES_TAC THENL [
42 POP_ASSUM STRIP_ASSUME_TAC THEN
43 COND_CASES_TAC THENL [
44 SELECT_ELIM_TAC THEN CONJ_TAC THENL [
45 Q.EXISTS_TAC `0` THEN
46 ASM_REWRITE_TAC [FUNPOW, NOT_LESS_0],
47 Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN
48 Q.SUBGOAL_THEN `m = 0` (fn th => REWRITE_TAC [th, FUNPOW]) THEN
49 Q.SPEC_THEN `m` (STRIP_ALL_THEN SUBST_ALL_TAC)
50 num_CASES THEN
51 REWRITE_TAC [] THEN
52 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
53 ASM_REWRITE_TAC [FUNPOW, LESS_0]
54 ],
55 SELECT_ELIM_TAC THEN
56 CONJ_TAC THENL [
57 Q.SPEC_THEN `\n. P (FUNPOW g n x)` (IMP_RES_TAC o BETA_RULE) WOP THEN
58 METIS_TAC [],
59 Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN
60 Q.SUBGOAL_THEN `?p. m = SUC p` (CHOOSE_THEN SUBST_ALL_TAC) THENL [
61 Q.SPEC_THEN `m` (STRIP_ALL_THEN SUBST_ALL_TAC)
62 num_CASES THEN
63 FULL_SIMP_TAC bool_ss [FUNPOW] THEN METIS_TAC [],
64 ALL_TAC
65 ] THEN
66 FULL_SIMP_TAC bool_ss [FUNPOW] THEN
67 Q.SUBGOAL_THEN `?n. P (FUNPOW g n (g x))`
68 (fn th => REWRITE_TAC [th]) THEN1 METIS_TAC [] THEN
69 POP_ASSUM (Q.SPEC_THEN `SUC m` (ASSUME_TAC o GEN_ALL o
70 SIMP_RULE bool_ss [FUNPOW,
71 LESS_MONO_EQ])) THEN
72 SELECT_ELIM_TAC THEN CONJ_TAC THENL [
73 METIS_TAC [],
74 Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN
75 METIS_TAC [LESS_LESS_CASES]
76 ]
77 ]
78 ],
79 POP_ASSUM (ASSUME_TAC o SIMP_RULE bool_ss []) THEN
80 FIRST_ASSUM (ASSUME_TAC o SIMP_RULE bool_ss [FUNPOW] o
81 GEN_ALL o SPEC ``SUC n``) THEN
82 ASM_REWRITE_TAC [] THEN METIS_TAC [FUNPOW]
83 ]
84QED
85
86
87(*---------------------------------------------------------------------------*)
88(* WHILE = |- !P g x. WHILE P g x = if P x then WHILE P g (g x) else x *)
89(*---------------------------------------------------------------------------*)
90
91val WHILE = new_specification
92 ("WHILE", ["WHILE"],
93 (CONV_RULE (BINDER_CONV SKOLEM_CONV THENC SKOLEM_CONV) o GEN_ALL o
94 REWRITE_RULE [o_THM, cond_lemma] o
95 SPEC ``$~ o P : 'a -> bool``) ITERATION);
96val _ = ot0 "WHILE" "while"
97
98Theorem WHILE_INDUCTION:
99 !B C R.
100 WF R /\ (!s. B s ==> R (C s) s)
101 ==> !P. (!s. (B s ==> P (C s)) ==> P s) ==> !v. P v
102Proof
103 METIS_TAC [WF_INDUCTION_THM]
104QED
105
106
107val HOARE_SPEC_DEF = new_definition
108 ("HOARE_SPEC_DEF",
109 ``HOARE_SPEC P C Q = !s. P s ==> Q (C s)``);
110
111(*---------------------------------------------------------------------------
112 The while rule from Hoare logic, total correctness version.
113 ---------------------------------------------------------------------------*)
114
115Theorem WHILE_RULE:
116 !R B C.
117 WF R /\ (!s. B s ==> R (C s) s)
118 ==>
119 HOARE_SPEC (\s. P s /\ B s) C P
120 (*------------------------------------------*) ==>
121 HOARE_SPEC P (WHILE B C) (\s. P s /\ ~B s)
122Proof
123 REPEAT GEN_TAC THEN STRIP_TAC
124 THEN REWRITE_TAC [HOARE_SPEC_DEF] THEN BETA_TAC THEN DISCH_TAC
125 THEN MP_TAC (SPEC_ALL WHILE_INDUCTION) THEN ASM_REWRITE_TAC[]
126 THEN DISCH_THEN HO_MATCH_MP_TAC (* recInduct *)
127 THEN METIS_TAC [WHILE]
128QED
129
130
131(*---------------------------------------------------------------------------*)
132(* LEAST number satisfying a predicate. *)
133(*---------------------------------------------------------------------------*)
134
135val LEAST_DEF = new_definition(
136 "LEAST_DEF",
137 ``LEAST P = WHILE ($~ o P) SUC 0``);
138
139val _ = ot0 "LEAST" "least"
140val _ = set_fixity "LEAST" Binder;
141
142Theorem LEAST_INTRO:
143 !P x. P x ==> P ($LEAST P)
144Proof
145 GEN_TAC THEN SIMP_TAC (srw_ss()) [LEAST_DEF] THEN
146 Q_TAC SUFF_TAC `!m n. P (m + n) ==> P (WHILE ($~ o P) SUC n)`
147 THENL [
148 SRW_TAC [][] THEN
149 FIRST_X_ASSUM (Q.SPECL_THEN [`x`,`0`] MP_TAC) THEN
150 ASM_SIMP_TAC bool_ss [ADD_CLAUSES],
151 ALL_TAC
152 ] THEN
153 INDUCT_TAC THENL [
154 ONCE_REWRITE_TAC [WHILE] THEN
155 ASM_SIMP_TAC bool_ss [ADD_CLAUSES, o_THM],
156 ONCE_REWRITE_TAC [WHILE] THEN
157 SRW_TAC [][ADD_CLAUSES] THEN
158 FIRST_X_ASSUM MATCH_MP_TAC THEN
159 ASM_SIMP_TAC bool_ss [ADD_CLAUSES]
160 ]
161QED
162
163Theorem LESS_LEAST:
164 !P m. m < $LEAST P ==> ~ P m
165Proof
166 GEN_TAC THEN
167 Q.ASM_CASES_TAC `?x. P x` THENL [
168 POP_ASSUM STRIP_ASSUME_TAC THEN
169 REWRITE_TAC [LEAST_DEF] THEN
170 Q_TAC SUFF_TAC `!y n. n + y < WHILE ($~ o P) SUC n ==> ~P(n + y)` THENL [
171 STRIP_TAC THEN GEN_TAC THEN
172 POP_ASSUM (Q.SPECL_THEN [`m`, `0`] MP_TAC) THEN
173 SIMP_TAC bool_ss [ADD_CLAUSES],
174 ALL_TAC
175 ] THEN
176 INDUCT_TAC THENL [
177 ONCE_REWRITE_TAC [WHILE] THEN SRW_TAC [][LESS_REFL, ADD_CLAUSES],
178 GEN_TAC THEN
179 Q.SUBGOAL_THEN `n + SUC y = SUC n + y` SUBST_ALL_TAC THEN1
180 SRW_TAC [][ADD_CLAUSES] THEN
181 STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
182 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [WHILE]) THEN
183 Q.ASM_CASES_TAC `P n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
184 Q.SUBGOAL_THEN `SUC n + y = n + SUC y` SUBST_ALL_TAC THEN1
185 SRW_TAC [][ADD_CLAUSES] THEN
186 METIS_TAC [LESS_ADD_SUC, LESS_TRANS, LESS_REFL]
187 ],
188 METIS_TAC []
189 ]
190QED
191
192Theorem FULL_LEAST_INTRO:
193 !x. P x ==> P ($LEAST P) /\ $LEAST P <= x
194Proof
195 METIS_TAC [LEAST_INTRO, NOT_LESS, LESS_LEAST]
196QED
197
198Theorem LEAST_ELIM:
199 !Q P. (?n. P n) /\ (!n. (!m. m < n ==> ~ P m) /\ P n ==> Q n) ==>
200 Q ($LEAST P)
201Proof
202 METIS_TAC [LEAST_INTRO, LESS_LEAST]
203QED
204
205Theorem LEAST_EXISTS:
206 !p. (?n. p n) = (p ($LEAST p) /\ !n. n < $LEAST p ==> ~p n)
207Proof
208 GEN_TAC
209 THEN MATCH_MP_TAC EQ_TRANS
210 THEN Q.EXISTS_TAC `?n. p n /\ (!m. m < n ==> ~p m)`
211 THEN CONJ_TAC
212 THENL [(Tactical.REVERSE EQ_TAC THEN1 METIS_TAC [])
213 THEN REPEAT STRIP_TAC
214 THEN CCONTR_TAC
215 THEN (SUFF_TAC ``!n : num. ~p n`` THEN1 METIS_TAC [])
216 THEN HO_MATCH_MP_TAC COMPLETE_INDUCTION
217 THEN METIS_TAC [],
218 (Tactical.REVERSE EQ_TAC THEN1 METIS_TAC [])
219 THEN STRIP_TAC
220 THEN METIS_TAC [LESS_LEAST, LEAST_INTRO]]
221QED
222
223Theorem LEAST_EXISTS_IMP:
224 !p. (?n. p n) ==> (p ($LEAST p) /\ !n. n < $LEAST p ==> ~p n)
225Proof
226 REWRITE_TAC [LEAST_EXISTS]
227QED
228
229Theorem LEAST_EQ[simp]:
230 ((LEAST n. n = x) = x) /\ ((LEAST n. x = n) = x)
231Proof
232 CONJ_TAC THEN
233 Q.SPEC_THEN `\n. n = x` (MATCH_MP_TAC o BETA_RULE) LEAST_ELIM THEN
234 SIMP_TAC (srw_ss()) []
235QED
236
237Theorem LEAST_T[simp]:
238 (LEAST x. T) = 0
239Proof
240 DEEP_INTRO_TAC LEAST_ELIM THEN SIMP_TAC (srw_ss()) [] THEN
241 Q.X_GEN_TAC `n` THEN STRIP_TAC THEN SPOSE_NOT_THEN ASSUME_TAC THEN
242 FULL_SIMP_TAC (srw_ss()) [NOT_ZERO_LT_ZERO] THEN METIS_TAC[]
243QED
244
245Theorem LEAST_LESS_EQ[simp]:
246 (LEAST x. y <= x) = y
247Proof
248 DEEP_INTRO_TAC LEAST_ELIM >> SRW_TAC [][]
249 >- (Q.EXISTS_TAC ‘y’ >> SIMP_TAC (srw_ss()) [LESS_EQ_REFL]) >>
250 FULL_SIMP_TAC (srw_ss()) [LESS_OR_EQ] >> RES_TAC >>
251 FULL_SIMP_TAC (srw_ss()) []
252QED
253
254(* ----------------------------------------------------------------------
255 OLEAST ("option LEAST") returns NONE if the argument is a predicate
256 that is everywhere false. Otherwise it returns SOME n, where n is the
257 least number making the predicate true.
258 ---------------------------------------------------------------------- *)
259
260val OLEAST_def = new_definition(
261 "OLEAST_def",
262 ``(OLEAST) P = if ?n. P n then SOME (LEAST n. P n) else NONE``)
263val _ = set_fixity "OLEAST" Binder
264
265Theorem OLEAST_INTRO:
266 ((!n. ~ P n) ==> Q NONE) /\
267 (!n. P n /\ (!m. m < n ==> ~P m) ==> Q (SOME n)) ==>
268 Q ((OLEAST) P)
269Proof
270 STRIP_TAC THEN SIMP_TAC (srw_ss()) [OLEAST_def] THEN SRW_TAC [][] THENL [
271 DEEP_INTRO_TAC LEAST_ELIM THEN METIS_TAC [],
272 FULL_SIMP_TAC (srw_ss()) []
273 ]
274QED
275
276Theorem OLEAST_EQNS[simp]:
277 ((OLEAST n. n = x) = SOME x) /\
278 ((OLEAST n. x = n) = SOME x) /\
279 ((OLEAST n. F) = NONE) /\
280 ((OLEAST n. T) = SOME 0)
281Proof
282 REPEAT STRIP_TAC THEN DEEP_INTRO_TAC OLEAST_INTRO THEN SRW_TAC [][] THEN
283 METIS_TAC [NOT_ZERO_LT_ZERO]
284QED
285
286Theorem OLEAST_EQ_NONE[simp]:
287 ((OLEAST) P = NONE) <=> !n. ~P n
288Proof
289 DEEP_INTRO_TAC OLEAST_INTRO >> SRW_TAC [][] >> METIS_TAC[]
290QED
291
292Theorem OLEAST_EQ_SOME:
293 ((OLEAST) P = SOME n) <=> P n /\ !m. m < n ==> ~P m
294Proof
295 DEEP_INTRO_TAC OLEAST_INTRO >>
296 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] >> REPEAT STRIP_TAC >>
297 METIS_TAC[NOT_LESS, LESS_EQUAL_ANTISYM]
298QED
299
300(* ----------------------------------------------------------------------
301 OWHILE ("option while") which returns SOME result if the loop
302 terminates, NONE otherwise.
303 ---------------------------------------------------------------------- *)
304
305
306val OWHILE_def = new_definition(
307 "OWHILE_def",
308 ``OWHILE G f s = if ?n. ~ G (FUNPOW f n s) then
309 SOME (FUNPOW f (LEAST n. ~ G (FUNPOW f n s)) s)
310 else NONE``)
311
312val LEAST_ELIM_TAC = DEEP_INTRO_TAC LEAST_ELIM
313
314Theorem OWHILE_THM:
315 OWHILE G f (s:'a) = if G s then OWHILE G f (f s) else SOME s
316Proof
317 SIMP_TAC (srw_ss()) [OWHILE_def] THEN
318 ASM_CASES_TAC ``(G:'a ->bool) s`` THENL [
319 ASM_REWRITE_TAC [] THEN
320 ASM_CASES_TAC ``?n. ~ (G:'a->bool) (FUNPOW f n s)`` THENL [
321 ASM_REWRITE_TAC [] THEN
322 FULL_SIMP_TAC (srw_ss()) [] THEN
323 Q.SUBGOAL_THEN `~(n = 0)` ASSUME_TAC THEN1
324 (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
325 Q.SUBGOAL_THEN `?m. n = SUC m` STRIP_ASSUME_TAC THEN1
326 (Q.SPEC_THEN `n` FULL_STRUCT_CASES_TAC num_CASES THEN
327 FULL_SIMP_TAC (srw_ss()) []) THEN
328 Q.SUBGOAL_THEN `?n. ~G(FUNPOW f n (f s))` ASSUME_TAC THEN1
329 (Q.EXISTS_TAC `m` THEN FULL_SIMP_TAC (srw_ss()) [FUNPOW]) THEN
330 POP_ASSUM (fn th => REWRITE_TAC [th]) THEN
331 SRW_TAC [][] THEN
332 DEEP_INTROk_TAC LEAST_ELIM
333 (FULL_SIMP_TAC (srw_ss()) [FUNPOW] THEN CONJ_TAC THEN1
334 (Q.EXISTS_TAC `SUC m` THEN SRW_TAC [][FUNPOW])) THEN
335 Q.X_GEN_TAC `N` THEN STRIP_TAC THEN
336 LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
337 REWRITE_TAC [] THEN
338 Q.X_GEN_TAC `M` THEN STRIP_TAC THEN
339 Q_TAC SUFF_TAC `N = SUC M` THEN1 SIMP_TAC (srw_ss()) [FUNPOW] THEN
340 Q.SPECL_THEN [`N`, `SUC M`] STRIP_ASSUME_TAC LESS_LESS_CASES THENL [
341 (* N < SUC M *)
342 Q.SUBGOAL_THEN `(N = 0) \/ (?N0. N = SUC N0)` STRIP_ASSUME_TAC THEN1
343 METIS_TAC [num_CASES] THEN
344 FULL_SIMP_TAC (srw_ss()) [LESS_MONO_EQ, FUNPOW] THEN
345 METIS_TAC [],
346 (* SUC M < N *)
347 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [FUNPOW]
348 ],
349
350 FULL_SIMP_TAC (srw_ss()) [] THEN
351 POP_ASSUM (Q.SPEC_THEN `SUC n` (ASSUME_TAC o Q.GEN `n`)) THEN
352 FULL_SIMP_TAC (srw_ss()) [FUNPOW]
353 ],
354
355 ASM_REWRITE_TAC [] THEN
356 Q.SUBGOAL_THEN `?n. ~G(FUNPOW f n s)` ASSUME_TAC THEN1
357 (Q.EXISTS_TAC `0` THEN SRW_TAC [][]) THEN
358 ASM_REWRITE_TAC [optionTheory.SOME_11] THEN
359 LEAST_ELIM_TAC THEN ASM_REWRITE_TAC [] THEN
360 Q.X_GEN_TAC `N` THEN STRIP_TAC THEN
361 Q_TAC SUFF_TAC `N = 0` THEN1 SRW_TAC [][] THEN
362 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
363 ASM_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [NOT_ZERO_LT_ZERO]
364 ]
365QED
366
367Theorem OWHILE_EQ_NONE:
368 (OWHILE G f (s:'a) = NONE) <=> !n. G (FUNPOW f n s)
369Proof
370 SRW_TAC [][OWHILE_def] THEN FULL_SIMP_TAC (srw_ss()) []
371QED
372
373Theorem OWHILE_ENDCOND:
374 (OWHILE G f (s:'a) = SOME s') ==> ~G s'
375Proof
376 SRW_TAC [][OWHILE_def] THEN LEAST_ELIM_TAC THEN METIS_TAC []
377QED
378
379Theorem OWHILE_WHILE:
380 (OWHILE G f s = SOME s') ==> (WHILE G f s = s')
381Proof
382 SIMP_TAC (srw_ss()) [OWHILE_def] THEN
383 STRIP_TAC THEN
384 SRW_TAC [][] THEN LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
385 REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN
386 Q.X_GEN_TAC `n` THEN MAP_EVERY Q.ID_SPEC_TAC [`s`, `n`] THEN
387 INDUCT_TAC THENL [
388 ONCE_REWRITE_TAC [WHILE] THEN SRW_TAC [][],
389 SRW_TAC [][FUNPOW] THEN
390 ONCE_REWRITE_TAC [WHILE] THEN
391 Q.SUBGOAL_THEN `G s` (fn th => REWRITE_TAC [th]) THEN1
392 (FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
393 SRW_TAC [][prim_recTheory.LESS_0]) THEN
394 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN
395 FIRST_X_ASSUM (Q.SPEC_THEN `SUC m` MP_TAC) THEN
396 SRW_TAC [][FUNPOW, LESS_MONO_EQ]
397 ]
398QED
399
400Theorem OWHILE_INV_IND:
401 !G f s. P s /\ (!x. P x /\ G x ==> P (f x)) ==>
402 !s'. (OWHILE G f s = SOME s') ==> P s'
403Proof
404 SIMP_TAC (srw_ss()) [OWHILE_def] THEN REPEAT STRIP_TAC THEN
405 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN
406 LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
407 REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN Q.X_GEN_TAC `n` THEN
408 Q.UNDISCH_THEN `P s` MP_TAC THEN REWRITE_TAC [AND_IMP_INTRO] THEN
409 MAP_EVERY Q.ID_SPEC_TAC [`s`, `n`] THEN INDUCT_TAC THENL [
410 SRW_TAC [][],
411 SRW_TAC [][FUNPOW] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
412 FIRST_X_ASSUM (fn th => Q.SPEC_THEN `0` MP_TAC th THEN
413 Q.SPEC_THEN `SUC m` (MP_TAC o Q.GEN `m`) th) THEN
414 SRW_TAC [][LESS_MONO_EQ, FUNPOW, LESS_0]
415 ]
416QED
417
418Theorem IF_SOME_EQ_SOME_LEMMA[local]:
419 !b (x:'a) y. ((if b then SOME x else NONE) = SOME y) <=> b /\ (x = y)
420Proof
421 Cases THEN
422 FULL_SIMP_TAC bool_ss [optionTheory.NOT_NONE_SOME,optionTheory.SOME_11]
423QED
424
425Theorem OWHILE_IND:
426 !P G (f:'a->'a).
427 (!s. ~(G s) ==> P s s) /\
428 (!s1 s2. G s1 /\ P (f s1) s2 ==> P s1 s2) ==>
429 !s1 s2. (OWHILE G f s1 = SOME s2) ==> P s1 s2
430Proof
431 SIMP_TAC bool_ss [OWHILE_def,IF_SOME_EQ_SOME_LEMMA] THEN REPEAT STRIP_TAC
432 THEN (Q.SPEC `\n. ~G (FUNPOW f n s1)` LEAST_EXISTS_IMP
433 |> SIMP_RULE bool_ss [PULL_EXISTS] |> IMP_RES_TAC)
434 THEN NTAC 2 (POP_ASSUM MP_TAC)
435 THEN Q.SPEC_TAC (`($LEAST (\n. ~G (FUNPOW f n s1)))`,`k`)
436 THEN Q.SPEC_TAC (`s1`,`s1`)
437 THEN Induct_on `k` THEN FULL_SIMP_TAC bool_ss [FUNPOW]
438 THEN REPEAT STRIP_TAC
439 THEN Q.PAT_ASSUM `!xx yy. bb` MATCH_MP_TAC
440 THEN STRIP_TAC THEN1
441 (`0 < SUC k` by REWRITE_TAC [prim_recTheory.LESS_0]
442 THEN RES_TAC THEN FULL_SIMP_TAC bool_ss [FUNPOW])
443 THEN FULL_SIMP_TAC bool_ss [AND_IMP_INTRO]
444 THEN Q.PAT_ASSUM `!s1. bb /\ bbb ==> bbbb` MATCH_MP_TAC
445 THEN FULL_SIMP_TAC bool_ss [] THEN REPEAT STRIP_TAC
446 THEN IMP_RES_TAC prim_recTheory.LESS_MONO THEN RES_TAC
447 THEN FULL_SIMP_TAC bool_ss [FUNPOW]
448QED
449
450Theorem WHILE_FUNPOW:
451 (?n. ~P (FUNPOW f n s))
452 ==> WHILE P f s = FUNPOW f (LEAST n. ~P (FUNPOW f n s)) s
453Proof
454 strip_tac
455 \\ `~!n. P (FUNPOW f n s)` by PROVE_TAC[]
456 \\ `?x. OWHILE P f s = SOME x` by PROVE_TAC[OWHILE_EQ_NONE, option_CASES]
457 \\ irule OWHILE_WHILE
458 \\ rewrite_tac[OWHILE_def]
459 \\ IF_CASES_TAC
460 \\ FULL_SIMP_TAC(srw_ss())[]
461QED
462
463Theorem TAILREC_EXISTS[local]:
464 ?tailrec.
465 !(f:'a -> 'a + 'b) (x:'a).
466 tailrec f x =
467 case f x of
468 | INL z => tailrec f z
469 | INR y => y
470Proof
471 EXISTS_TAC “λ(f:'a -> 'a + 'b) x. OUTR (f (WHILE (ISL o f) (OUTL o f) x))”
472 THEN rpt strip_tac
473 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
474 THEN CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [WHILE]))
475 THEN REWRITE_TAC [combinTheory.o_DEF]
476 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
477 THEN Cases_on ‘f x’
478 THEN ASM_REWRITE_TAC [TypeBase.case_def_of “:'a + 'b”,sumTheory.ISL]
479 THEN CONV_TAC (DEPTH_CONV BETA_CONV)
480 THEN ASM_REWRITE_TAC [sumTheory.OUTL,sumTheory.OUTR]
481QED
482
483val TAILREC = new_specification("TAILREC",["TAILREC"],TAILREC_EXISTS);
484
485val TAILCALL_def = new_definition(
486 "TAILCALL_def",
487 “TAILCALL f k x = case f x of INL cv => k cv | INR tv => tv”);
488
489Theorem TAILREC_TAILCALL:
490 TAILREC f x = TAILCALL f (TAILREC f) x
491Proof
492 ONCE_REWRITE_TAC[TAILCALL_def, TAILREC] >>
493 REWRITE_TAC[]
494QED
495
496(* This theorem can be used to eliminate guards on tail-recursive equations.
497 The recursion equation you don't like is the last assumption:
498 f has an equation but the whole thing is guarded by the annoying P
499 But if the other conditions hold, you can use TAILREC c everywhere you
500 were using f instead.
501 The other two conditions spell out:
502 1. guard actually holds on all recursive calls;
503 2. guard guarantees that something gets smaller with every call (this is
504 super general version of this; an easier version is below)
505*)
506Theorem TAILREC_GUARD_ELIMINATION:
507 (!x y. P x /\ c x = INL y ==> P y) /\
508 (!x. P x ==>
509 ?R. WFP R x /\ !y z. P y /\ R^* y x /\ c y = INL z ==> R z y) /\
510 (!x. P x ==> f x = TAILCALL c f x) ==>
511 (!x. P x ==> f x = TAILREC c x)
512Proof
513 rpt strip_tac >>
514 Q.PAT_X_ASSUM ‘!x. P x ==> ?R. _’ (drule_then strip_assume_tac) >>
515 Q.PAT_X_ASSUM ‘WFP R x’ (fn th => ntac 2 (pop_assum mp_tac) >> mp_tac th) >>
516 Q.ID_SPEC_TAC ‘x’ >>
517 ho_match_mp_tac WFP_STRONG_INDUCT >> rpt strip_tac >>
518 simp[TAILCALL_def] >>
519 Cases_on ‘c x’ >> simp[]
520 >- (simp[TAILREC_TAILCALL] >> simp[TAILCALL_def] >>
521 first_x_assum irule >> simp[] >>
522 rpt strip_tac >> first_assum irule >> simp[]
523 >- METIS_TAC[] >>
524 irule (cj 2 RTC_RULES_RIGHT1) >>
525 first_assum $ irule_at (Pat ‘RTC _ _ _’) >> first_assum irule >>
526 simp[]) >>
527 simp[TAILREC_TAILCALL] >> simp[TAILCALL_def]
528QED
529
530Theorem TAILREC_GUARD_ELIMINATION_SIMPLER:
531 WF R /\
532 (!x y. P x /\ c x = INL y ==> P y) /\
533 (!x y. P x /\ c x = INL y ==> R y x) /\
534 (!x. P x ==> f x = TAILCALL c f x) ==>
535 (!x. P x ==> f x = TAILREC c x)
536Proof
537 strip_tac >> MATCH_MP_TAC TAILREC_GUARD_ELIMINATION >> rpt strip_tac >>
538 simp[]
539 >- METIS_TAC[] >>
540 Q.EXISTS_TAC ‘R’ >> full_simp_tac (srw_ss())[WF_EQ_WFP]
541QED
542
543val _ =
544 computeLib.add_persistent_funs
545 ["WHILE"
546 ,"LEAST_DEF"
547 ,"TAILREC"];
548