1(*===========================================================================*)
2(* Define WHILE loops, give Hoare rules, and define LEAST operator as a      *)
3(* binder.                                                                   *)
4(*===========================================================================*)
5
6open HolKernel boolLib Parse Prim_rec simpLib boolSimps metisLib
7     combinTheory prim_recTheory arithmeticTheory BasicProvers
8     optionTheory
9
10val _ = new_theory "while";
11
12local open OpenTheoryMap
13  val ns = ["While"]
14in
15  fun ot0 x y = OpenTheory_const_name{const={Thy="while",Name=x},name=(ns,y)}
16  fun ot x = ot0 x x
17end
18
19fun INDUCT_TAC g = INDUCT_THEN numTheory.INDUCTION ASSUME_TAC g;
20
21val cond_lemma = prove(
22  ``(if ~p then q else r) = (if p then r else q)``,
23  Q.ASM_CASES_TAC `p` THEN ASM_REWRITE_TAC []);
24
25(* ----------------------------------------------------------------------
26    Existence of WHILE
27   ---------------------------------------------------------------------- *)
28
29val ITERATION = Q.store_thm
30("ITERATION",
31  `!P g. ?f. !x. f x = if P x then x else f (g x)`,
32  REPEAT GEN_TAC THEN
33  Q.EXISTS_TAC `\x. if ?n. P (FUNPOW g n x) then
34                      FUNPOW g (@n. P (FUNPOW g n x) /\
35                                    !m.  m < n ==> ~P (FUNPOW g m x)) x
36                    else ARB` THEN BETA_TAC THEN
37  GEN_TAC THEN COND_CASES_TAC THENL [
38    POP_ASSUM STRIP_ASSUME_TAC THEN
39    COND_CASES_TAC THENL [
40      SELECT_ELIM_TAC THEN CONJ_TAC THENL [
41        Q.EXISTS_TAC `0` THEN
42        ASM_REWRITE_TAC [FUNPOW, NOT_LESS_0],
43        Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN
44        Q.SUBGOAL_THEN `m = 0` (fn th => REWRITE_TAC [th, FUNPOW]) THEN
45        Q.SPEC_THEN `m` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC)
46                    num_CASES THEN
47        REWRITE_TAC [] THEN
48        FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
49        ASM_REWRITE_TAC [FUNPOW, LESS_0]
50      ],
51      SELECT_ELIM_TAC THEN
52      CONJ_TAC THENL [
53        Q.SPEC_THEN `\n. P (FUNPOW g n x)` (IMP_RES_TAC o BETA_RULE) WOP THEN
54        METIS_TAC [],
55        Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN
56        Q.SUBGOAL_THEN `?p. m = SUC p` (CHOOSE_THEN SUBST_ALL_TAC) THENL [
57          Q.SPEC_THEN `m` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC)
58                      num_CASES THEN
59          FULL_SIMP_TAC bool_ss [FUNPOW] THEN METIS_TAC [],
60          ALL_TAC
61        ] THEN
62        FULL_SIMP_TAC bool_ss [FUNPOW] THEN
63        Q.SUBGOAL_THEN `?n. P (FUNPOW g n (g x))`
64                       (fn th => REWRITE_TAC [th]) THEN1 METIS_TAC [] THEN
65        POP_ASSUM (Q.SPEC_THEN `SUC m` (ASSUME_TAC o GEN_ALL o
66                                        SIMP_RULE bool_ss [FUNPOW,
67                                                           LESS_MONO_EQ])) THEN
68        SELECT_ELIM_TAC THEN CONJ_TAC THENL [
69          METIS_TAC [],
70          Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN
71          METIS_TAC [LESS_LESS_CASES]
72        ]
73      ]
74    ],
75    POP_ASSUM (ASSUME_TAC o SIMP_RULE bool_ss []) THEN
76    FIRST_ASSUM (ASSUME_TAC o SIMP_RULE bool_ss [FUNPOW] o
77                 GEN_ALL o SPEC ``SUC n``) THEN
78    ASM_REWRITE_TAC [] THEN METIS_TAC [FUNPOW]
79  ]);
80
81
82(*---------------------------------------------------------------------------*)
83(*  WHILE = |- !P g x. WHILE P g x = if P x then WHILE P g (g x) else x      *)
84(*---------------------------------------------------------------------------*)
85
86val WHILE = new_specification
87 ("WHILE", ["WHILE"],
88  (CONV_RULE (BINDER_CONV SKOLEM_CONV THENC SKOLEM_CONV) o GEN_ALL o
89   REWRITE_RULE [o_THM, cond_lemma] o
90   SPEC ``$~ o P : 'a -> bool``) ITERATION);
91val _ = ot0 "WHILE" "while"
92
93val WHILE_INDUCTION = Q.store_thm
94("WHILE_INDUCTION",
95 `!B C R.
96     WF R /\ (!s. B s ==> R (C s) s)
97     ==> !P. (!s. (B s ==> P (C s)) ==> P s) ==> !v. P v`,
98 METIS_TAC [relationTheory.WF_INDUCTION_THM]);
99
100
101val HOARE_SPEC_DEF = new_definition
102 ("HOARE_SPEC_DEF",
103 ``HOARE_SPEC P C Q = !s. P s ==> Q (C s)``);
104
105(*---------------------------------------------------------------------------
106       The while rule from Hoare logic, total correctness version.
107 ---------------------------------------------------------------------------*)
108
109val WHILE_RULE = Q.store_thm
110("WHILE_RULE",
111 `!R B C.
112     WF R /\ (!s. B s ==> R (C s) s)
113      ==>
114        HOARE_SPEC (\s. P s /\ B s) C P
115     (*------------------------------------------*) ==>
116        HOARE_SPEC P (WHILE B C) (\s. P s /\ ~B s)`,
117 REPEAT GEN_TAC THEN STRIP_TAC
118  THEN REWRITE_TAC [HOARE_SPEC_DEF] THEN BETA_TAC THEN DISCH_TAC
119  THEN MP_TAC (SPEC_ALL WHILE_INDUCTION) THEN ASM_REWRITE_TAC[]
120  THEN DISCH_THEN HO_MATCH_MP_TAC (* recInduct *)
121  THEN METIS_TAC [WHILE]);
122
123
124(*---------------------------------------------------------------------------*)
125(* LEAST number satisfying a predicate.                                      *)
126(*---------------------------------------------------------------------------*)
127
128val LEAST_DEF = new_definition(
129  "LEAST_DEF",
130  ``LEAST P = WHILE ($~ o P) SUC 0``);
131
132val _ = ot0 "LEAST" "least"
133val _ = set_fixity "LEAST" Binder;
134
135val LEAST_INTRO = store_thm(
136  "LEAST_INTRO",
137  ``!P x. P x ==> P ($LEAST P)``,
138  GEN_TAC THEN SIMP_TAC (srw_ss()) [LEAST_DEF] THEN
139  Q_TAC SUFF_TAC `!m n. P (m + n) ==> P (WHILE ($~ o P) SUC n)`
140  THENL [
141    SRW_TAC [][] THEN
142    FIRST_X_ASSUM (Q.SPECL_THEN [`x`,`0`] MP_TAC) THEN
143    ASM_SIMP_TAC bool_ss [ADD_CLAUSES],
144    ALL_TAC
145  ] THEN
146  INDUCT_TAC THENL [
147    ONCE_REWRITE_TAC [WHILE] THEN
148    ASM_SIMP_TAC bool_ss [ADD_CLAUSES, o_THM],
149    ONCE_REWRITE_TAC [WHILE] THEN
150    SRW_TAC [][ADD_CLAUSES] THEN
151    FIRST_X_ASSUM MATCH_MP_TAC THEN
152    ASM_SIMP_TAC bool_ss [ADD_CLAUSES]
153  ]);
154
155val LESS_LEAST = store_thm(
156  "LESS_LEAST",
157  ``!P m. m < $LEAST P ==> ~ P m``,
158  GEN_TAC THEN
159  Q.ASM_CASES_TAC `?x. P x` THENL [
160    POP_ASSUM STRIP_ASSUME_TAC THEN
161    REWRITE_TAC [LEAST_DEF] THEN
162    Q_TAC SUFF_TAC `!y n. n + y < WHILE ($~ o P) SUC n ==> ~P(n + y)` THENL [
163      STRIP_TAC THEN GEN_TAC THEN
164      POP_ASSUM (Q.SPECL_THEN [`m`, `0`] MP_TAC) THEN
165      SIMP_TAC bool_ss [ADD_CLAUSES],
166      ALL_TAC
167    ] THEN
168    INDUCT_TAC THENL [
169      ONCE_REWRITE_TAC [WHILE] THEN SRW_TAC [][LESS_REFL, ADD_CLAUSES],
170      GEN_TAC THEN
171      Q.SUBGOAL_THEN `n + SUC y = SUC n + y` SUBST_ALL_TAC THEN1
172        SRW_TAC [][ADD_CLAUSES] THEN
173      STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
174      RULE_ASSUM_TAC (ONCE_REWRITE_RULE [WHILE]) THEN
175      Q.ASM_CASES_TAC `P n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
176      Q.SUBGOAL_THEN `SUC n + y = n + SUC y` SUBST_ALL_TAC THEN1
177        SRW_TAC [][ADD_CLAUSES] THEN
178      METIS_TAC [LESS_ADD_SUC, LESS_TRANS, LESS_REFL]
179    ],
180    METIS_TAC []
181  ]);
182
183val FULL_LEAST_INTRO = store_thm(
184  "FULL_LEAST_INTRO",
185  ``!x. P x ==> P ($LEAST P) /\ $LEAST P <= x``,
186  METIS_TAC [LEAST_INTRO, NOT_LESS, LESS_LEAST]);
187
188val LEAST_ELIM = store_thm(
189  "LEAST_ELIM",
190  ``!Q P. (?n. P n) /\ (!n. (!m. m < n ==> ~ P m) /\ P n ==> Q n) ==>
191          Q ($LEAST P)``,
192  METIS_TAC [LEAST_INTRO, LESS_LEAST]);
193
194val LEAST_EXISTS = store_thm
195  ("LEAST_EXISTS",
196   ``!p. (?n. p n) = (p ($LEAST p) /\ !n. n < $LEAST p ==> ~p n)``,
197   GEN_TAC
198   THEN MATCH_MP_TAC EQ_TRANS
199   THEN Q.EXISTS_TAC `?n. p n /\ (!m. m < n ==> ~p m)`
200   THEN CONJ_TAC
201   THENL [(Tactical.REVERSE EQ_TAC THEN1 METIS_TAC [])
202          THEN REPEAT STRIP_TAC
203          THEN CCONTR_TAC
204          THEN (SUFF_TAC ``!n : num. ~p n`` THEN1 METIS_TAC [])
205          THEN HO_MATCH_MP_TAC COMPLETE_INDUCTION
206          THEN METIS_TAC [],
207          (Tactical.REVERSE EQ_TAC THEN1 METIS_TAC [])
208          THEN STRIP_TAC
209          THEN METIS_TAC [LESS_LEAST, LEAST_INTRO]]);
210
211val LEAST_EXISTS_IMP = store_thm
212  ("LEAST_EXISTS_IMP",
213   ``!p. (?n. p n) ==> (p ($LEAST p) /\ !n. n < $LEAST p ==> ~p n)``,
214   REWRITE_TAC [LEAST_EXISTS]);
215
216val LEAST_EQ = store_thm(
217  "LEAST_EQ",
218  ``((LEAST n. n = x) = x) /\ ((LEAST n. x = n) = x)``,
219  CONJ_TAC THEN
220  Q.SPEC_THEN `\n. n = x` (MATCH_MP_TAC o BETA_RULE) LEAST_ELIM THEN
221  SIMP_TAC (srw_ss()) []);
222val _ = export_rewrites ["LEAST_EQ"]
223
224val LEAST_T = store_thm(
225  "LEAST_T[simp]",
226  ``(LEAST x. T) = 0``,
227  DEEP_INTRO_TAC LEAST_ELIM THEN SIMP_TAC (srw_ss()) [] THEN
228  Q.X_GEN_TAC `n` THEN STRIP_TAC THEN SPOSE_NOT_THEN ASSUME_TAC THEN
229  FULL_SIMP_TAC (srw_ss()) [NOT_ZERO_LT_ZERO] THEN METIS_TAC[]);
230
231(* ----------------------------------------------------------------------
232    OLEAST ("option LEAST") returns NONE if the argument is a predicate
233    that is everywhere false.  Otherwise it returns SOME n, where n is the
234    least number making the predicate true.
235   ---------------------------------------------------------------------- *)
236
237val OLEAST_def = new_definition(
238  "OLEAST_def",
239  ``(OLEAST) P = if ?n. P n then SOME (LEAST n. P n) else NONE``)
240val _ = set_fixity "OLEAST" Binder
241
242val OLEAST_INTRO = store_thm(
243  "OLEAST_INTRO",
244  ``((!n. ~ P n) ==> Q NONE) /\
245    (!n. P n /\ (!m. m < n ==> ~P m) ==> Q (SOME n)) ==>
246    Q ((OLEAST) P)``,
247  STRIP_TAC THEN SIMP_TAC (srw_ss()) [OLEAST_def] THEN SRW_TAC [][] THENL [
248    DEEP_INTRO_TAC LEAST_ELIM THEN METIS_TAC [],
249    FULL_SIMP_TAC (srw_ss()) []
250  ]);
251
252val OLEAST_EQNS = store_thm(
253  "OLEAST_EQNS",
254  ``((OLEAST n. n = x) = SOME x) /\
255    ((OLEAST n. x = n) = SOME x) /\
256    ((OLEAST n. F) = NONE) /\
257    ((OLEAST n. T) = SOME 0)``,
258  REPEAT STRIP_TAC THEN DEEP_INTRO_TAC OLEAST_INTRO THEN SRW_TAC [][] THEN
259  METIS_TAC [arithmeticTheory.NOT_ZERO_LT_ZERO]);
260val _ = export_rewrites ["OLEAST_EQNS"]
261
262val OLEAST_EQ_NONE = Q.store_thm(
263  "OLEAST_EQ_NONE[simp]",
264  ���((OLEAST) P = NONE) <=> !n. ~P n���,
265  DEEP_INTRO_TAC OLEAST_INTRO >> SRW_TAC [][] >> METIS_TAC[]);
266
267val OLEAST_EQ_SOME = Q.store_thm(
268  "OLEAST_EQ_SOME",
269  ���((OLEAST) P = SOME n) <=> P n /\ !m. m < n ==> ~P m���,
270  DEEP_INTRO_TAC OLEAST_INTRO >>
271  SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] >> REPEAT STRIP_TAC >>
272  METIS_TAC[NOT_LESS, LESS_EQUAL_ANTISYM]);
273
274(* ----------------------------------------------------------------------
275    OWHILE ("option while") which returns SOME result if the loop
276    terminates, NONE otherwise.
277   ---------------------------------------------------------------------- *)
278
279
280val OWHILE_def = new_definition(
281  "OWHILE_def",
282  ``OWHILE G f s = if ?n. ~ G (FUNPOW f n s) then
283                     SOME (FUNPOW f (LEAST n. ~ G (FUNPOW f n s)) s)
284                   else NONE``)
285
286val LEAST_ELIM_TAC = DEEP_INTRO_TAC LEAST_ELIM
287
288val OWHILE_THM = store_thm(
289  "OWHILE_THM",
290  ``OWHILE G f (s:'a) = if G s then OWHILE G f (f s) else SOME s``,
291  SIMP_TAC (srw_ss()) [OWHILE_def] THEN
292  ASM_CASES_TAC ``(G:'a ->bool) s`` THENL [
293    ASM_REWRITE_TAC [] THEN
294    ASM_CASES_TAC ``?n. ~ (G:'a->bool) (FUNPOW f n s)`` THENL [
295      ASM_REWRITE_TAC [] THEN
296      FULL_SIMP_TAC (srw_ss()) [] THEN
297      Q.SUBGOAL_THEN `~(n = 0)` ASSUME_TAC THEN1
298        (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
299      Q.SUBGOAL_THEN `?m. n = SUC m` STRIP_ASSUME_TAC THEN1
300        (Q.SPEC_THEN `n` FULL_STRUCT_CASES_TAC num_CASES THEN
301         FULL_SIMP_TAC (srw_ss()) []) THEN
302      Q.SUBGOAL_THEN `?n. ~G(FUNPOW f n (f s))` ASSUME_TAC THEN1
303        (Q.EXISTS_TAC `m` THEN FULL_SIMP_TAC (srw_ss()) [FUNPOW]) THEN
304      POP_ASSUM (fn th => REWRITE_TAC [th]) THEN
305      SRW_TAC [][] THEN
306      DEEP_INTROk_TAC LEAST_ELIM
307        (FULL_SIMP_TAC (srw_ss()) [FUNPOW] THEN CONJ_TAC THEN1
308          (Q.EXISTS_TAC `SUC m` THEN SRW_TAC [][FUNPOW])) THEN
309      Q.X_GEN_TAC `N` THEN STRIP_TAC THEN
310      LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
311      REWRITE_TAC [] THEN
312      Q.X_GEN_TAC `M` THEN STRIP_TAC THEN
313      Q_TAC SUFF_TAC `N = SUC M` THEN1 SIMP_TAC (srw_ss()) [FUNPOW] THEN
314      Q.SPECL_THEN [`N`, `SUC M`] STRIP_ASSUME_TAC LESS_LESS_CASES THENL [
315        (* N < SUC M *)
316        Q.SUBGOAL_THEN `(N = 0) \/ (?N0. N = SUC N0)` STRIP_ASSUME_TAC THEN1
317          METIS_TAC [num_CASES] THEN
318        FULL_SIMP_TAC (srw_ss()) [LESS_MONO_EQ, FUNPOW] THEN
319        METIS_TAC [],
320        (* SUC M < N *)
321        RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [FUNPOW]
322      ],
323
324      FULL_SIMP_TAC (srw_ss()) [] THEN
325      POP_ASSUM (Q.SPEC_THEN `SUC n` (ASSUME_TAC o Q.GEN `n`)) THEN
326      FULL_SIMP_TAC (srw_ss()) [FUNPOW]
327    ],
328
329    ASM_REWRITE_TAC [] THEN
330    Q.SUBGOAL_THEN `?n. ~G(FUNPOW f n s)` ASSUME_TAC THEN1
331      (Q.EXISTS_TAC `0` THEN SRW_TAC [][]) THEN
332    ASM_REWRITE_TAC [optionTheory.SOME_11] THEN
333    LEAST_ELIM_TAC THEN ASM_REWRITE_TAC [] THEN
334    Q.X_GEN_TAC `N` THEN STRIP_TAC THEN
335    Q_TAC SUFF_TAC `N = 0` THEN1 SRW_TAC [][] THEN
336    FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
337    ASM_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [NOT_ZERO_LT_ZERO]
338  ]);
339
340val OWHILE_EQ_NONE = store_thm(
341  "OWHILE_EQ_NONE",
342  ``(OWHILE G f (s:'a) = NONE) <=> !n. G (FUNPOW f n s)``,
343  SRW_TAC [][OWHILE_def] THEN FULL_SIMP_TAC (srw_ss()) []);
344
345val OWHILE_ENDCOND = store_thm(
346  "OWHILE_ENDCOND",
347  ``(OWHILE G f (s:'a) = SOME s') ==> ~G s'``,
348  SRW_TAC [][OWHILE_def] THEN LEAST_ELIM_TAC THEN METIS_TAC []);
349
350val OWHILE_WHILE = store_thm(
351  "OWHILE_WHILE",
352  ``(OWHILE G f s = SOME s') ==> (WHILE G f s = s')``,
353  SIMP_TAC (srw_ss()) [OWHILE_def] THEN
354  STRIP_TAC THEN
355  SRW_TAC [][] THEN LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
356  REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN
357  Q.X_GEN_TAC `n` THEN MAP_EVERY Q.ID_SPEC_TAC [`s`, `n`] THEN
358  INDUCT_TAC THENL [
359    ONCE_REWRITE_TAC [WHILE] THEN SRW_TAC [][],
360    SRW_TAC [][FUNPOW] THEN
361    ONCE_REWRITE_TAC [WHILE] THEN
362    Q.SUBGOAL_THEN `G s` (fn th => REWRITE_TAC [th]) THEN1
363      (FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
364       SRW_TAC [][prim_recTheory.LESS_0]) THEN
365    FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN
366    FIRST_X_ASSUM (Q.SPEC_THEN `SUC m` MP_TAC) THEN
367    SRW_TAC [][FUNPOW, LESS_MONO_EQ]
368  ]);
369
370val OWHILE_INV_IND = store_thm(
371  "OWHILE_INV_IND",
372  ``!G f s. P s /\ (!x. P x /\ G x ==> P (f x)) ==>
373            !s'. (OWHILE G f s = SOME s') ==> P s'``,
374  SIMP_TAC (srw_ss()) [OWHILE_def] THEN REPEAT STRIP_TAC THEN
375  FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN
376  LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
377  REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN Q.X_GEN_TAC `n` THEN
378  Q.UNDISCH_THEN `P s` MP_TAC THEN REWRITE_TAC [AND_IMP_INTRO] THEN
379  MAP_EVERY Q.ID_SPEC_TAC [`s`, `n`] THEN INDUCT_TAC THENL [
380    SRW_TAC [][],
381    SRW_TAC [][FUNPOW] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
382    FIRST_X_ASSUM (fn th => Q.SPEC_THEN `0` MP_TAC th THEN
383                            Q.SPEC_THEN `SUC m` (MP_TAC o Q.GEN `m`) th) THEN
384    SRW_TAC [][LESS_MONO_EQ, FUNPOW, LESS_0]
385  ]);
386
387val IF_SOME_EQ_SOME_LEMMA = prove(
388  ``!b (x:'a) y. ((if b then SOME x else NONE) = SOME y) = b /\ (x = y)``,
389  Cases THEN
390  FULL_SIMP_TAC bool_ss [optionTheory.NOT_NONE_SOME,optionTheory.SOME_11]);
391
392val OWHILE_IND = store_thm(
393  "OWHILE_IND",
394  ``!P G (f:'a->'a).
395      (!s. ~(G s) ==> P s s) /\
396      (!s1 s2. G s1 /\ P (f s1) s2 ==> P s1 s2) ==>
397      !s1 s2. (OWHILE G f s1 = SOME s2) ==> P s1 s2``,
398  SIMP_TAC bool_ss [OWHILE_def,IF_SOME_EQ_SOME_LEMMA] THEN REPEAT STRIP_TAC
399  THEN (Q.SPEC `\n. ~G (FUNPOW f n s1)` LEAST_EXISTS_IMP
400      |> SIMP_RULE bool_ss [PULL_EXISTS] |> IMP_RES_TAC)
401  THEN NTAC 2 (POP_ASSUM MP_TAC)
402  THEN Q.SPEC_TAC (`($LEAST (\n. ~G (FUNPOW f n s1)))`,`k`)
403  THEN Q.SPEC_TAC (`s1`,`s1`)
404  THEN Induct_on `k` THEN FULL_SIMP_TAC bool_ss [FUNPOW]
405  THEN REPEAT STRIP_TAC
406  THEN Q.PAT_ASSUM `!xx yy. bb` MATCH_MP_TAC
407  THEN STRIP_TAC THEN1
408   (`0 < SUC k` by REWRITE_TAC [prim_recTheory.LESS_0]
409    THEN RES_TAC THEN FULL_SIMP_TAC bool_ss [FUNPOW])
410  THEN FULL_SIMP_TAC bool_ss [AND_IMP_INTRO]
411  THEN Q.PAT_ASSUM `!s1. bb /\ bbb ==> bbbb` MATCH_MP_TAC
412  THEN FULL_SIMP_TAC bool_ss [] THEN REPEAT STRIP_TAC
413  THEN IMP_RES_TAC prim_recTheory.LESS_MONO THEN RES_TAC
414  THEN FULL_SIMP_TAC bool_ss [FUNPOW]);
415
416val _ =
417 computeLib.add_persistent_funs
418   ["WHILE"
419   ,"LEAST_DEF"];
420
421val _ = export_theory();
422