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