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
231Theorem LEAST_LESS_EQ[simp]:
232  (LEAST x. y <= x) = y
233Proof
234  DEEP_INTRO_TAC LEAST_ELIM >> SRW_TAC [][]
235  >- (Q.EXISTS_TAC ���y��� >> SIMP_TAC (srw_ss()) [LESS_EQ_REFL]) >>
236  FULL_SIMP_TAC (srw_ss()) [LESS_OR_EQ] >> RES_TAC >>
237  FULL_SIMP_TAC (srw_ss()) []
238QED
239
240(* ----------------------------------------------------------------------
241    OLEAST ("option LEAST") returns NONE if the argument is a predicate
242    that is everywhere false.  Otherwise it returns SOME n, where n is the
243    least number making the predicate true.
244   ---------------------------------------------------------------------- *)
245
246val OLEAST_def = new_definition(
247  "OLEAST_def",
248  ``(OLEAST) P = if ?n. P n then SOME (LEAST n. P n) else NONE``)
249val _ = set_fixity "OLEAST" Binder
250
251val OLEAST_INTRO = store_thm(
252  "OLEAST_INTRO",
253  ``((!n. ~ P n) ==> Q NONE) /\
254    (!n. P n /\ (!m. m < n ==> ~P m) ==> Q (SOME n)) ==>
255    Q ((OLEAST) P)``,
256  STRIP_TAC THEN SIMP_TAC (srw_ss()) [OLEAST_def] THEN SRW_TAC [][] THENL [
257    DEEP_INTRO_TAC LEAST_ELIM THEN METIS_TAC [],
258    FULL_SIMP_TAC (srw_ss()) []
259  ]);
260
261val OLEAST_EQNS = store_thm(
262  "OLEAST_EQNS",
263  ``((OLEAST n. n = x) = SOME x) /\
264    ((OLEAST n. x = n) = SOME x) /\
265    ((OLEAST n. F) = NONE) /\
266    ((OLEAST n. T) = SOME 0)``,
267  REPEAT STRIP_TAC THEN DEEP_INTRO_TAC OLEAST_INTRO THEN SRW_TAC [][] THEN
268  METIS_TAC [arithmeticTheory.NOT_ZERO_LT_ZERO]);
269val _ = export_rewrites ["OLEAST_EQNS"]
270
271val OLEAST_EQ_NONE = Q.store_thm(
272  "OLEAST_EQ_NONE[simp]",
273  ���((OLEAST) P = NONE) <=> !n. ~P n���,
274  DEEP_INTRO_TAC OLEAST_INTRO >> SRW_TAC [][] >> METIS_TAC[]);
275
276val OLEAST_EQ_SOME = Q.store_thm(
277  "OLEAST_EQ_SOME",
278  ���((OLEAST) P = SOME n) <=> P n /\ !m. m < n ==> ~P m���,
279  DEEP_INTRO_TAC OLEAST_INTRO >>
280  SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] >> REPEAT STRIP_TAC >>
281  METIS_TAC[NOT_LESS, LESS_EQUAL_ANTISYM]);
282
283(* ----------------------------------------------------------------------
284    OWHILE ("option while") which returns SOME result if the loop
285    terminates, NONE otherwise.
286   ---------------------------------------------------------------------- *)
287
288
289val OWHILE_def = new_definition(
290  "OWHILE_def",
291  ``OWHILE G f s = if ?n. ~ G (FUNPOW f n s) then
292                     SOME (FUNPOW f (LEAST n. ~ G (FUNPOW f n s)) s)
293                   else NONE``)
294
295val LEAST_ELIM_TAC = DEEP_INTRO_TAC LEAST_ELIM
296
297val OWHILE_THM = store_thm(
298  "OWHILE_THM",
299  ``OWHILE G f (s:'a) = if G s then OWHILE G f (f s) else SOME s``,
300  SIMP_TAC (srw_ss()) [OWHILE_def] THEN
301  ASM_CASES_TAC ``(G:'a ->bool) s`` THENL [
302    ASM_REWRITE_TAC [] THEN
303    ASM_CASES_TAC ``?n. ~ (G:'a->bool) (FUNPOW f n s)`` THENL [
304      ASM_REWRITE_TAC [] THEN
305      FULL_SIMP_TAC (srw_ss()) [] THEN
306      Q.SUBGOAL_THEN `~(n = 0)` ASSUME_TAC THEN1
307        (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
308      Q.SUBGOAL_THEN `?m. n = SUC m` STRIP_ASSUME_TAC THEN1
309        (Q.SPEC_THEN `n` FULL_STRUCT_CASES_TAC num_CASES THEN
310         FULL_SIMP_TAC (srw_ss()) []) THEN
311      Q.SUBGOAL_THEN `?n. ~G(FUNPOW f n (f s))` ASSUME_TAC THEN1
312        (Q.EXISTS_TAC `m` THEN FULL_SIMP_TAC (srw_ss()) [FUNPOW]) THEN
313      POP_ASSUM (fn th => REWRITE_TAC [th]) THEN
314      SRW_TAC [][] THEN
315      DEEP_INTROk_TAC LEAST_ELIM
316        (FULL_SIMP_TAC (srw_ss()) [FUNPOW] THEN CONJ_TAC THEN1
317          (Q.EXISTS_TAC `SUC m` THEN SRW_TAC [][FUNPOW])) THEN
318      Q.X_GEN_TAC `N` THEN STRIP_TAC THEN
319      LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
320      REWRITE_TAC [] THEN
321      Q.X_GEN_TAC `M` THEN STRIP_TAC THEN
322      Q_TAC SUFF_TAC `N = SUC M` THEN1 SIMP_TAC (srw_ss()) [FUNPOW] THEN
323      Q.SPECL_THEN [`N`, `SUC M`] STRIP_ASSUME_TAC LESS_LESS_CASES THENL [
324        (* N < SUC M *)
325        Q.SUBGOAL_THEN `(N = 0) \/ (?N0. N = SUC N0)` STRIP_ASSUME_TAC THEN1
326          METIS_TAC [num_CASES] THEN
327        FULL_SIMP_TAC (srw_ss()) [LESS_MONO_EQ, FUNPOW] THEN
328        METIS_TAC [],
329        (* SUC M < N *)
330        RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [FUNPOW]
331      ],
332
333      FULL_SIMP_TAC (srw_ss()) [] THEN
334      POP_ASSUM (Q.SPEC_THEN `SUC n` (ASSUME_TAC o Q.GEN `n`)) THEN
335      FULL_SIMP_TAC (srw_ss()) [FUNPOW]
336    ],
337
338    ASM_REWRITE_TAC [] THEN
339    Q.SUBGOAL_THEN `?n. ~G(FUNPOW f n s)` ASSUME_TAC THEN1
340      (Q.EXISTS_TAC `0` THEN SRW_TAC [][]) THEN
341    ASM_REWRITE_TAC [optionTheory.SOME_11] THEN
342    LEAST_ELIM_TAC THEN ASM_REWRITE_TAC [] THEN
343    Q.X_GEN_TAC `N` THEN STRIP_TAC THEN
344    Q_TAC SUFF_TAC `N = 0` THEN1 SRW_TAC [][] THEN
345    FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
346    ASM_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [NOT_ZERO_LT_ZERO]
347  ]);
348
349val OWHILE_EQ_NONE = store_thm(
350  "OWHILE_EQ_NONE",
351  ``(OWHILE G f (s:'a) = NONE) <=> !n. G (FUNPOW f n s)``,
352  SRW_TAC [][OWHILE_def] THEN FULL_SIMP_TAC (srw_ss()) []);
353
354val OWHILE_ENDCOND = store_thm(
355  "OWHILE_ENDCOND",
356  ``(OWHILE G f (s:'a) = SOME s') ==> ~G s'``,
357  SRW_TAC [][OWHILE_def] THEN LEAST_ELIM_TAC THEN METIS_TAC []);
358
359val OWHILE_WHILE = store_thm(
360  "OWHILE_WHILE",
361  ``(OWHILE G f s = SOME s') ==> (WHILE G f s = s')``,
362  SIMP_TAC (srw_ss()) [OWHILE_def] THEN
363  STRIP_TAC THEN
364  SRW_TAC [][] THEN LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
365  REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN
366  Q.X_GEN_TAC `n` THEN MAP_EVERY Q.ID_SPEC_TAC [`s`, `n`] THEN
367  INDUCT_TAC THENL [
368    ONCE_REWRITE_TAC [WHILE] THEN SRW_TAC [][],
369    SRW_TAC [][FUNPOW] THEN
370    ONCE_REWRITE_TAC [WHILE] THEN
371    Q.SUBGOAL_THEN `G s` (fn th => REWRITE_TAC [th]) THEN1
372      (FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
373       SRW_TAC [][prim_recTheory.LESS_0]) THEN
374    FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN
375    FIRST_X_ASSUM (Q.SPEC_THEN `SUC m` MP_TAC) THEN
376    SRW_TAC [][FUNPOW, LESS_MONO_EQ]
377  ]);
378
379val OWHILE_INV_IND = store_thm(
380  "OWHILE_INV_IND",
381  ``!G f s. P s /\ (!x. P x /\ G x ==> P (f x)) ==>
382            !s'. (OWHILE G f s = SOME s') ==> P s'``,
383  SIMP_TAC (srw_ss()) [OWHILE_def] THEN REPEAT STRIP_TAC THEN
384  FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN
385  LEAST_ELIM_TAC THEN CONJ_TAC THEN1 METIS_TAC [] THEN
386  REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) THEN Q.X_GEN_TAC `n` THEN
387  Q.UNDISCH_THEN `P s` MP_TAC THEN REWRITE_TAC [AND_IMP_INTRO] THEN
388  MAP_EVERY Q.ID_SPEC_TAC [`s`, `n`] THEN INDUCT_TAC THENL [
389    SRW_TAC [][],
390    SRW_TAC [][FUNPOW] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
391    FIRST_X_ASSUM (fn th => Q.SPEC_THEN `0` MP_TAC th THEN
392                            Q.SPEC_THEN `SUC m` (MP_TAC o Q.GEN `m`) th) THEN
393    SRW_TAC [][LESS_MONO_EQ, FUNPOW, LESS_0]
394  ]);
395
396val IF_SOME_EQ_SOME_LEMMA = prove(
397  ``!b (x:'a) y. ((if b then SOME x else NONE) = SOME y) <=> b /\ (x = y)``,
398  Cases THEN
399  FULL_SIMP_TAC bool_ss [optionTheory.NOT_NONE_SOME,optionTheory.SOME_11]);
400
401val OWHILE_IND = store_thm(
402  "OWHILE_IND",
403  ``!P G (f:'a->'a).
404      (!s. ~(G s) ==> P s s) /\
405      (!s1 s2. G s1 /\ P (f s1) s2 ==> P s1 s2) ==>
406      !s1 s2. (OWHILE G f s1 = SOME s2) ==> P s1 s2``,
407  SIMP_TAC bool_ss [OWHILE_def,IF_SOME_EQ_SOME_LEMMA] THEN REPEAT STRIP_TAC
408  THEN (Q.SPEC `\n. ~G (FUNPOW f n s1)` LEAST_EXISTS_IMP
409      |> SIMP_RULE bool_ss [PULL_EXISTS] |> IMP_RES_TAC)
410  THEN NTAC 2 (POP_ASSUM MP_TAC)
411  THEN Q.SPEC_TAC (`($LEAST (\n. ~G (FUNPOW f n s1)))`,`k`)
412  THEN Q.SPEC_TAC (`s1`,`s1`)
413  THEN Induct_on `k` THEN FULL_SIMP_TAC bool_ss [FUNPOW]
414  THEN REPEAT STRIP_TAC
415  THEN Q.PAT_ASSUM `!xx yy. bb` MATCH_MP_TAC
416  THEN STRIP_TAC THEN1
417   (`0 < SUC k` by REWRITE_TAC [prim_recTheory.LESS_0]
418    THEN RES_TAC THEN FULL_SIMP_TAC bool_ss [FUNPOW])
419  THEN FULL_SIMP_TAC bool_ss [AND_IMP_INTRO]
420  THEN Q.PAT_ASSUM `!s1. bb /\ bbb ==> bbbb` MATCH_MP_TAC
421  THEN FULL_SIMP_TAC bool_ss [] THEN REPEAT STRIP_TAC
422  THEN IMP_RES_TAC prim_recTheory.LESS_MONO THEN RES_TAC
423  THEN FULL_SIMP_TAC bool_ss [FUNPOW]);
424
425val _ =
426 computeLib.add_persistent_funs
427   ["WHILE"
428   ,"LEAST_DEF"];
429
430val _ = export_theory();
431