1(* ------------------------------------------------------------------------- *) 2(* Iteration Period Computation *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "iterateCompute"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* open dependent theories *) 17val _ = load("iterateTheory"); 18open helperFunctionTheory; 19open helperSetTheory; 20open helperNumTheory; 21 22(* arithmeticTheory -- load by default *) 23open arithmeticTheory pred_setTheory; 24open dividesTheory; (* for divides_def *) 25 26open iterateTheory; 27open listTheory; 28open listRangeTheory; 29open helperListTheory; (* for listRangeINC_SNOC *) 30 31(* val _ = load "helperTheory"; *) 32open helperTheory; (* for WHILE_RULE_PRE_POST *) 33open whileTheory; (* for WHILE definition *) 34 35 36(* ------------------------------------------------------------------------- *) 37(* Iteration Period Computation Documentation *) 38(* ------------------------------------------------------------------------- *) 39(* Overloading: 40! iterate x f j = FUNPOW f j x 41*) 42(* 43 44 Helper Theorems: 45 46 FUNPOW with incremental cons: 47 FUNPOW_cons_head |- !f n ls. HD (FUNPOW (\ls. f (HD ls)::ls) n ls) = FUNPOW f n (HD ls) 48 FUNPOW_cons_eq_map_0|- !f u n. FUNPOW (\ls. f (HD ls)::ls) n [u] = 49 MAP (\j. FUNPOW f j u) (n downto 0) 50 FUNPOW_cons_eq_map_1|- !f u n. 0 < n ==> 51 FUNPOW (\ls. f (HD ls)::ls) (n - 1) [f u] = 52 MAP (\j. FUNPOW f j u) (n downto 1) 53 54 Iterative Search, by recursion with cutoff: 55 iterate_search_def |- !x j g f c b. iterate_search f g x c b j = 56 if c <= j then b 57 else if g x then x 58 else iterate_search f g (f x) c b (j + 1) 59 iterate_search_over |- !f g x c b j. c <= j ==> iterate_search f g x c b j = b 60 iterate_search_exit |- !f g x c b j. j < c /\ g x ==> iterate_search f g x c b j = x 61 iterate_search_next |- !f g x c b j. j < c /\ ~g x ==> 62 iterate_search f g x c b j = 63 iterate_search f g (f x) c b (j + 1) 64 iterate_search_run |- !f g x c b j k. 0 < k /\ j + k <= c /\ 65 (!i. i < k ==> ~g (FUNPOW f i x)) ==> 66 iterate_search f g x c b j = 67 iterate_search f g (FUNPOW f k x) c b (j + k) 68 iterate_search_done |- !f g x c b j n. 0 < n /\ j + n < c /\ 69 (!i. i < n ==> ~g (FUNPOW f i x)) /\ 70 g (FUNPOW f n x) ==> iterate_search f g x c b j = FUNPOW f n x 71 iterate_search_thm |- !f g x c b n. n < c /\ (!i. i < n ==> ~g (FUNPOW f i x)) /\ 72 g (FUNPOW f n x) ==> iterate_search f g x c b 0 = FUNPOW f n x 73 74 Iterative Loop, using WHILE construct: 75 iterate_trace_def |- !a b c. iterate_trace a b c = MAP (\j. iterate a b j) [0 .. c] 76 iterate_trace_length|- !a b c. LENGTH (iterate_trace a b c) = 1 + c 77 iterate_trace_non_nil 78 |- !a b c. iterate_trace a b c <> [] 79 iterate_trace_sing |- !a b. iterate_trace a b 0 = [a] 80 iterate_trace_head |- !a b c. HD (iterate_trace a b c) = a 81 iterate_trace_last |- !a b c. LAST (iterate_trace a b c) = iterate a b c 82 iterate_trace_element 83 |- !a b c j. j <= c ==> EL j (iterate_trace a b c) = iterate a b j 84 iterate_trace_element_idx 85 |- !a b c ls j. ls = iterate_trace a b c /\ ALL_DISTINCT ls /\ 86 j <= c ==> findi (iterate a b j) ls = j 87 iterate_trace_member|- !a b c ls x. ls = iterate_trace a b c /\ x <> iterate a b c /\ 88 MEM x ls ==> MEM (b x) ls 89 iterate_trace_member_iff 90 |- !a b c ls x. ls = iterate_trace a b c ==> 91 (MEM x ls <=> ?j. j <= c /\ (x = iterate a b j)) 92 iterate_trace_index |- !a b c ls x. ls = iterate_trace a b c /\ x <> iterate a b c /\ 93 MEM x ls /\ ALL_DISTINCT ls ==> 94 (findi (b x) ls = 1 + findi x ls) 95 iterate_trace_all_distinct 96 |- !s a b c p. FINITE s /\ b PERMUTES s /\ a IN s /\ 97 p = iterate_period b a /\ c < p ==> 98 ALL_DISTINCT (iterate_trace a b c) 99 iterate_while_hoare |- !s a b c p g n. FINITE s /\ b PERMUTES s /\ a IN s /\ 100 p = iterate_period b a /\ n < c /\ c < p /\ 101 ~g (iterate a b n) /\ (!j. j < n ==> g (iterate a b j)) ==> 102 HOARE_SPEC {a} (WHILE g b) {iterate a b n} 103 iterate_while_thm_1 |- !s a b c p g n. FINITE s /\ b PERMUTES s /\ a IN s /\ 104 p = iterate_period b a /\ n < c /\ c < p /\ 105 ~g (iterate a b n) /\ (!j. j < n ==> g (iterate a b j)) ==> 106 WHILE g b a = iterate a b n 107 iterate_while_hoare_0 108 |- !a b g. ~g a ==> HOARE_SPEC {a} (WHILE g b) {a} 109 iterate_while_thm_0 |- !a b g. ~g a ==> WHILE g b a = a 110 111 Direct from WHILE definition: 112 iterate_while_eqn |- !g b x k. (!j. j < k ==> g (FUNPOW b j x)) ==> 113 WHILE g b x = 114 if g (FUNPOW b k x) then WHILE g b (FUNPOW b (k + 1) x) 115 else FUNPOW b k x 116 iterate_while_thm |- !g b x k. (!j. j < k ==> g (FUNPOW b j x)) /\ ~g (FUNPOW b k x) ==> 117 WHILE g b x = FUNPOW b k x 118*) 119 120(* ------------------------------------------------------------------------- *) 121(* Helper Theorems *) 122(* ------------------------------------------------------------------------- *) 123 124(* Note from HelperList: m downto n = REVERSE [m .. n] *) 125 126(* ------------------------------------------------------------------------- *) 127(* FUNPOW with incremental cons. *) 128(* ------------------------------------------------------------------------- *) 129 130(* Idea: when applying incremental cons (f head) to a list for n times, 131 head of the result is f^n (head of list). *) 132 133(* Theorem: HD (FUNPOW (\ls. f (HD ls)::ls) n ls) = FUNPOW f n (HD ls) *) 134(* Proof: 135 Let h = (\ls. f (HD ls)::ls). 136 By induction on n. 137 Base: !ls. HD (FUNPOW h 0 ls) = FUNPOW f 0 (HD ls) 138 HD (FUNPOW h 0 ls) 139 = HD ls by FUNPOW_0 140 = FUNPOW f 0 (HD ls) by FUNPOW_0 141 Step: !ls. HD (FUNPOW h n ls) = FUNPOW f n (HD ls) ==> 142 !ls. HD (FUNPOW h (SUC n) ls) = FUNPOW f (SUC n) (HD ls) 143 HD (FUNPOW h (SUC n) ls) 144 = HD (FUNPOW h n (h ls)) by FUNPOW 145 = FUNPOW f n (HD (h ls)) by induction hypothesis 146 = FUNPOW f n (f (HD ls)) by definition of h 147 = FUNPOW f (SUC n) (HD ls) by FUNPOW 148*) 149Theorem FUNPOW_cons_head: 150 !f n ls. HD (FUNPOW (\ls. f (HD ls)::ls) n ls) = FUNPOW f n (HD ls) 151Proof 152 strip_tac >> 153 qabbrev_tac `h = \ls. f (HD ls)::ls` >> 154 Induct >- 155 simp[] >> 156 rw[FUNPOW, Abbr`h`] 157QED 158 159(* Idea: when applying incremental cons (f head) to a singleton [u] for n times, 160 the result is the list [f^n(u), .... f(u), u]. *) 161 162(* Theorem: FUNPOW (\ls. f (HD ls)::ls) n [u] = 163 MAP (\j. FUNPOW f j u) (n downto 0) *) 164(* Proof: 165 Let g = (\ls. f (HD ls)::ls), 166 h = (\j. FUNPOW f j u). 167 By induction on n. 168 Base: FUNPOW g 0 [u] = MAP h (0 downto 0) 169 FUNPOW g 0 [u] 170 = [u] by FUNPOW_0 171 = [FUNPOW f 0 u] by FUNPOW_0 172 = MAP h [0] by MAP 173 = MAP h (0 downto 0) by REVERSE 174 Step: FUNPOW g n [u] = MAP h (n downto 0) ==> 175 FUNPOW g (SUC n) [u] = MAP h (SUC n downto 0) 176 FUNPOW g (SUC n) [u] 177 = g (FUNPOW g n [u]) by FUNPOW_SUC 178 = g (MAP h (n downto 0)) by induction hypothesis 179 = f (HD (MAP h (n downto 0))) :: 180 MAP h (n downto 0) by definition of g 181 Now f (HD (MAP h (n downto 0))) 182 = f (HD (MAP h (MAP (\x. n - x) [0 .. n]))) by listRangeINC_REVERSE 183 = f (HD (MAP h o (\x. n - x) [0 .. n])) by MAP_COMPOSE 184 = f ((h o (\x. n - x)) 0) by MAP 185 = f (h n) 186 = f (FUNPOW f n u) by definition of h 187 = FUNPOW (n + 1) u by FUNPOW_SUC 188 = h (n + 1) by definition of h 189 so h (n + 1) :: MAP h (n downto 0) 190 = MAP h ((n + 1) :: (n downto 0)) by MAP 191 = MAP h (REVERSE (SNOC (n+1) [0 .. n])) by REVERSE_SNOC 192 = MAP h (SUC n downto 0) by listRangeINC_SNOC 193*) 194Theorem FUNPOW_cons_eq_map_0: 195 !f u n. FUNPOW (\ls. f (HD ls)::ls) n [u] = 196 MAP (\j. FUNPOW f j u) (n downto 0) 197Proof 198 ntac 2 strip_tac >> 199 Induct >- 200 rw[] >> 201 qabbrev_tac `g = \ls. f (HD ls)::ls` >> 202 qabbrev_tac `h = \j. FUNPOW f j u` >> 203 rw[] >> 204 `f (HD (MAP h (n downto 0))) = h (n + 1)` by 205 (`[0 .. n] = 0 :: [1 .. n]` by rw[listRangeINC_CONS] >> 206 fs[listRangeINC_REVERSE, MAP_COMPOSE, GSYM FUNPOW_SUC, ADD1, Abbr`h`]) >> 207 `FUNPOW g (SUC n) [u] = g (FUNPOW g n [u])` by rw[FUNPOW_SUC] >> 208 `_ = g (MAP h (n downto 0))` by fs[] >> 209 `_ = h (n + 1) :: MAP h (n downto 0)` by rw[Abbr`g`] >> 210 `_ = MAP h ((n + 1) :: (n downto 0))` by rw[] >> 211 `_ = MAP h (REVERSE (SNOC (n+1) [0 .. n]))` by rw[REVERSE_SNOC] >> 212 rw[listRangeINC_SNOC, ADD1] 213QED 214 215(* Idea: when applying incremental cons (f head) to a singleton [f(u)] for (n-1) times, 216 the result is the list [f^n(u), .... f(u)]. *) 217 218(* Theorem: 0 < n ==> (FUNPOW (\ls. f (HD ls)::ls) (n - 1) [f u] = 219 MAP (\j. FUNPOW f j u) (n downto 1)) *) 220(* Proof: 221 Let g = (\ls. f (HD ls)::ls), 222 h = (\j. FUNPOW f j u). 223 By induction on n. 224 Base: FUNPOW g 0 [f u] = MAP h (REVERSE [1 .. 1]) 225 FUNPOW g 0 [f u] 226 = [f u] by FUNPOW_0 227 = [FUNPOW f 1 u] by FUNPOW_1 228 = MAP h [1] by MAP 229 = MAP h (REVERSE [1 .. 1]) by REVERSE 230 Step: 0 < n ==> FUNPOW g (n-1) [f u] = MAP h (n downto 1) ==> 231 FUNPOW g n [f u] = MAP h (REVERSE [1 .. SUC n]) 232 The case n = 0 is the base case. For n <> 0, 233 FUNPOW g n [f u] 234 = g (FUNPOW g (n-1) [f u]) by FUNPOW_SUC 235 = g (MAP h (n downto 1)) by induction hypothesis 236 = f (HD (MAP h (n downto 1))) :: 237 MAP h (n downto 1) by definition of g 238 Now f (HD (MAP h (n downto 1))) 239 = f (HD (MAP h (MAP (\x. n + 1 - x) [1 .. n]))) by listRangeINC_REVERSE 240 = f (HD (MAP h o (\x. n + 1 - x) [1 .. n])) by MAP_COMPOSE 241 = f ((h o (\x. n + 1 - x)) 1) by MAP 242 = f (h n) 243 = f (FUNPOW f n u) by definition of h 244 = FUNPOW (n + 1) u by FUNPOW_SUC 245 = h (n + 1) by definition of h 246 so h (n + 1) :: MAP h (n downto 1) 247 = MAP h ((n + 1) :: (n downto 1)) by MAP 248 = MAP h (REVERSE (SNOC (n+1) [1 .. n])) by REVERSE_SNOC 249 = MAP h (REVERSE [1 .. SUC n]) by listRangeINC_SNOC 250*) 251Theorem FUNPOW_cons_eq_map_1: 252 !f u n. 0 < n ==> (FUNPOW (\ls. f (HD ls)::ls) (n - 1) [f u] = 253 MAP (\j. FUNPOW f j u) (n downto 1)) 254Proof 255 ntac 2 strip_tac >> 256 Induct >- 257 simp[] >> 258 rw[] >> 259 qabbrev_tac `g = \ls. f (HD ls)::ls` >> 260 qabbrev_tac `h = \j. FUNPOW f j u` >> 261 Cases_on `n = 0` >- 262 rw[Abbr`g`, Abbr`h`] >> 263 `f (HD (MAP h (n downto 1))) = h (n + 1)` by 264 (`[1 .. n] = 1 :: [2 .. n]` by rw[listRangeINC_CONS] >> 265 fs[listRangeINC_REVERSE, MAP_COMPOSE, GSYM FUNPOW_SUC, ADD1, Abbr`h`]) >> 266 `n = SUC (n-1)` by decide_tac >> 267 `FUNPOW g n [f u] = g (FUNPOW g (n - 1) [f u])` by metis_tac[FUNPOW_SUC] >> 268 `_ = g (MAP h (n downto 1))` by fs[] >> 269 `_ = h (n + 1) :: MAP h (n downto 1)` by rw[Abbr`g`] >> 270 `_ = MAP h ((n + 1) :: (n downto 1))` by rw[] >> 271 `_ = MAP h (REVERSE (SNOC (n+1) [1 .. n]))` by rw[REVERSE_SNOC] >> 272 rw[listRangeINC_SNOC, ADD1] 273QED 274 275(* ------------------------------------------------------------------------- *) 276(* Iterative Search, by recursion with cutoff. *) 277(* ------------------------------------------------------------------------- *) 278 279(* Idea: recursion with cutoff c, starting count j. *) 280 281(* The starting point is x:'a, iterating over function f:'a -> 'a, 282 that is, f x <- x, until guard g:'a -> bool checks (g x) is true. *) 283val iterate_search_def = tDefine "iterate_search" ` 284 iterate_search f g x c b j = 285 if (c <= j) then b else if (g x) then x 286 else iterate_search f g (f x) c b (j + 1) 287`(WF_REL_TAC `measure (\(f,g,x,c,b,j). c - j)`); 288(* Note: the bad b can be just x, as it is relevant only for the cutoff. *) 289 290(* Idea: iteration goes on only for j < c; if not, game over. *) 291 292(* Theorem: c <= j ==> iterate_search f g x c b j = b *) 293(* Proof: by iterate_search_def *) 294Theorem iterate_search_over: 295 !f g x c b j. c <= j ==> iterate_search f g x c b j = b 296Proof 297 simp[Once iterate_search_def] 298QED 299 300(* Idea: iteration goes on for j < c, but exits when (g x). *) 301 302(* Theorem: j < c /\ g x ==> iterate_search f g x c b j = x *) 303(* Proof: by iterate_search_def *) 304Theorem iterate_search_exit: 305 !f g x c b j. j < c /\ g x ==> iterate_search f g x c b j = x 306Proof 307 simp[Once iterate_search_def] 308QED 309 310(* Idea: iteration goes on for one step when j < c and ~(g x). *) 311 312(* Theorem: j < c /\ ~g x ==> 313 iterate_search f g x c b j = iterate_search f g (f x) c b (j + 1) *) 314(* Proof: by iterate_search_def *) 315Theorem iterate_search_next: 316 !f g x c b j. j < c /\ ~g x ==> 317 iterate_search f g x c b j = iterate_search f g (f x) c b (j + 1) 318Proof 319 simp[Once iterate_search_def] 320QED 321 322 323(* Idea: iteration goes on for k more steps. 324 Extend iterate_search_next by induction, with 0 < k. *) 325 326(* Theorem: 0 < k /\ j + k <= c /\ (!i. i < k ==> ~g (FUNPOW f i x)) ==> 327 iterate_search f g x c b j = iterate_search f g (FUNPOW f k x) c b (j + k) *) 328(* Proof: 329 By induction on k, starting from k = 1. 330 Base: j + 1 <= c /\ (!i. i < 1 ==> ~g (FUNPOW f i x)) ==> 331 (iterate_search f g x c b j = iterate_search f g (FUNPOW f 1 x) c b (j + 1)) 332 This simplifies, by FUNPOW_0, FUNPOW_1, to: 333 j < c /\ ~g x ==> iterate_search f g x c b j = iterate_search f g (f x) c b (j + 1) 334 which is true by iterate_search_next. 335 Step: !k. 0 < k /\ j + (k + 1) <= c /\ 336 (!i. i < k ==> ~g (FUNPOW f i (f x))) ==> 337 (iterate_search f g (f x) c b (j + 1) = 338 iterate_search f g (FUNPOW f k (f x)) c b (j + (k + 1))) ==> 339 0 < k /\ j + k <= c /\ (!i. i < k ==> ~g (FUNPOW f i x)) ==> 340 iterate_search f g x c b j = iterate_search f g (FUNPOW f k x) c b (j + k) 341 The case k = 1 has been covered. 342 For k <> 1, 1 < k, so k = k - 1 + 1 by arithmetic 343 Putting !k for the specific (k-1), 344 Thus 0 < k - 1, j + (k-1 +1) <= c, and note 345 !i. i < k ==> ~g (FUNPOW f i x) by given 346 <=> !i. i - 1 < k - 1 ==> ~g (FUNPOW f (i - 1 + 1) x) 347 <=> !j. j < k - 1 ==> ~g (FUNPOW f (j + 1) x) 348 <=> !j. j < k - 1 ==> ~g (FUNPOW f j (f x)) by FUNPOW 349 Thus the induction assumption conditions are all satisfied, 350 iterate_search f g x c b j 351 = iterate_search f g (FUNPOW f (k - 1) (f x)) c b (j + k) 352 by induction hypothesis 353 = iterate_search f g (FUNPOW f k x) c b (j + k) by FUNPOW, ADD1 354 *) 355Theorem iterate_search_run: 356 !f g x c b j k. 0 < k /\ j + k <= c /\ 357 (!i. i < k ==> ~g (FUNPOW f i x)) ==> 358 iterate_search f g x c b j = 359 iterate_search f g (FUNPOW f k x) c b (j + k) 360Proof 361 ho_match_mp_tac (theorem "iterate_search_ind") >> 362 rw[] >> 363 `~(c <= j)` by decide_tac >> 364 `~g x` by metis_tac[FUNPOW_0] >> 365 fs[] >> 366 `iterate_search f g x c b j = iterate_search f g (f x) c b (j + 1)` by fs[iterate_search_next] >> 367 (Cases_on `k = 1` >> simp[]) >> 368 `0 < k - 1` by decide_tac >> 369 last_x_assum (qspecl_then [`k-1`] strip_assume_tac) >> 370 rfs[] >> 371 `!i. i < k - 1 ==> ~g (FUNPOW f i (f x))` by 372 (rpt strip_tac >> 373 `~g (FUNPOW f (i + 1) x)` by fs[] >> 374 metis_tac[FUNPOW, ADD1]) >> 375 `k - 1 + 1 = k` by decide_tac >> 376 metis_tac[FUNPOW, ADD1] 377QED 378 379(* Idea: iteration when k more steps becomes n, when now g (FUNPOW f n x). *) 380 381(* Theorem: 0 < n /\ j + n < c /\ 382 (!i. i < n ==> ~g (FUNPOW f i x)) /\ g (FUNPOW f n x) ==> 383 iterate_search f g x c b j = FUNPOW f n x *) 384(* Proof: 385 iterate_search f g x c b j 386 = iterate_search f g (FUNPOW f n x) c b (j + n) by iterate_search_run, j + n <= c 387 = FUNPOW f n x by iterate_search_exit, j + n < c 388*) 389Theorem iterate_search_done: 390 !f g x c b j n. 0 < n /\ j + n < c /\ 391 (!i. i < n ==> ~g (FUNPOW f i x)) /\ g (FUNPOW f n x) ==> 392 iterate_search f g x c b j = FUNPOW f n x 393Proof 394 metis_tac[iterate_search_run, iterate_search_exit, LESS_IMP_LESS_OR_EQ] 395QED 396 397(* Idea: the same result, but start with j = 0, and remove 0 < n. *) 398 399(* Theorem: n < c /\ (!i. i < n ==> ~g (FUNPOW f i x)) /\ 400 g (FUNPOW f n x) ==> iterate_search f g x c b 0 = FUNPOW f n x *) 401(* Proof: 402 If n = 0, true by iterate_search_exit 403 If n <> 0, true by iterate_search_done 404*) 405Theorem iterate_search_thm: 406 !f g x c b n. n < c /\ (!i. i < n ==> ~g (FUNPOW f i x)) /\ 407 g (FUNPOW f n x) ==> 408 iterate_search f g x c b 0 = FUNPOW f n x 409Proof 410 rpt strip_tac >> 411 Cases_on `n = 0` >- 412 fs[iterate_search_exit] >> 413 simp[iterate_search_done] 414QED 415 416(* ------------------------------------------------------------------------- *) 417(* Iterative Loop, using WHILE construct. *) 418(* ------------------------------------------------------------------------- *) 419 420(* Define the iterate WHILE loop: 421 with a guard g and a body b, both functions of x, of type alpha. *) 422(* no need to define! 423val iterate_while_def = Define` 424 iterate_while (g:'a -> bool) (b:'a -> 'a) = WHILE g b 425`; 426*) 427 428(* Overload FUNPOW f j x with index j as the last parameter. *) 429val _ = temp_overload_on ("iterate", ``\x f j. FUNPOW f j x``); 430(* FUNPOW f j x is pretty-printed as: f^{j}(x). *) 431(* iterate x f j is pretty-printed as: (x)f^{j}. *) 432 433(* for temporary overloading, otherwise all FUNPOW becomes iterate! *) 434 435(* Define the trace of the iterate WHILE, starting with a, up to a cutoff c. *) 436Definition iterate_trace_def: 437 iterate_trace (a:'a) (b:'a -> 'a) (c:num) = MAP (iterate a b) [0 .. c] 438End 439 440(* Properties of iteration trace *) 441 442(* Theorem: LENGTH (iterate_trace a b c) = 1 + c *) 443(* Proof: 444 LENGTH (iterate_trace a b c) 445 = LENGTH (MAP (iterate a b) [0 .. c]) by iterate_trace_def 446 = LENGTH [0 .. c] by LENGTH_MAP 447 = 1 + c by listRangeINC_LEN 448*) 449Theorem iterate_trace_length: 450 !a b c. LENGTH (iterate_trace a b c) = 1 + c 451Proof 452 simp[iterate_trace_def, listRangeINC_LEN] 453QED 454 455(* Theorem: iterate_trace a b c <> [] *) 456(* Proof: 457 Let ls = iterate a b c. 458 Note LENGTH ls = 1 + c by iterate_trace_length 459 <> 0 by arithmetic 460 so ls <> [] by LENGTH_NIL 461*) 462Theorem iterate_trace_non_nil: 463 !a b c. iterate_trace a b c <> [] 464Proof 465 metis_tac[iterate_trace_length, LENGTH_NIL, DECIDE``1 + n <> 0``] 466QED 467 468(* Theorem: iterate_trace a b 0 = [a] *) 469(* Proof: 470 iterate_trace a b 0 471 = MAP (iterate a b) [0 .. 0] by iterate_trace_def 472 = MAP (iterate a b) [0] by listRangeINC_SING 473 = [(iterate a b) 0] by MAP_SING 474 = [a] by FUNPOW_0 475*) 476Theorem iterate_trace_sing: 477 !a b. iterate_trace a b 0 = [a] 478Proof 479 rpt strip_tac >> 480 qabbrev_tac `f = iterate a b` >> 481 `iterate_trace a b 0 = MAP f [0 .. 0]` by rw[iterate_trace_def, Abbr`f`] >> 482 `_ = MAP f [0]` by rw[listRangeINC_SING] >> 483 `_ = [f 0]` by rw[MAP_SING] >> 484 simp[Abbr`f`] 485QED 486 487(* Theorem: HD (iterate_trace a b c) = a *) 488(* Proof: 489 HD (iterate_trace a b c) 490 = HD (MAP (iterate a b) [0 .. c]) by iterate_trace_def 491 = HD (MAP (iterate a b) (0::[1 .. c])) by listRangeINC_CONS 492 = HD ((iterate a b) 0 :: MAP (iterate a b) [1 .. c]) 493 by MAP 494 = (iterate a b) 0 by HD 495 = a by FUNPOW_0 496*) 497Theorem iterate_trace_head: 498 !a b c. HD (iterate_trace a b c) = a 499Proof 500 rpt strip_tac >> 501 qabbrev_tac `f = iterate a b` >> 502 `HD (iterate_trace a b c) = HD (MAP f [0 .. c])` by rw[iterate_trace_def, Abbr`f`] >> 503 `_ = HD (MAP f (0::[1 .. c]))` by rw[listRangeINC_CONS] >> 504 `_ = HD (f 0 :: MAP f [1 .. c])` by rw[] >> 505 simp[Abbr`f`] 506QED 507 508(* Theorem: LAST (iterate_trace a b c) = iterate a b c *) 509(* Proof: 510 If c = 0, 511 LAST (iterate_trace a b 0) 512 = LAST [a] by iterate_trace_sing 513 = a by LAST_CONS 514 = iterate a b 0 by FUNPOW_0 515 516 If c <> 0, 517 LAST (iterate_trace a b c) 518 = LAST (MAP (iterate a b) [0 .. c]) by iterate_trace_def 519 = LAST (MAP (iterate a b) (SNOC c [0 .. (c-1)])) by listRangeINC_SNOC 520 = LAST (SNOC ((iterate a b) c) (MAP (iterate a b) [0 .. (c-1)])) 521 by MAP_SNOC 522 = (iterate a b) c by LAST_SNOC 523 = iterate a b c by function application 524*) 525Theorem iterate_trace_last: 526 !a b c. LAST (iterate_trace a b c) = iterate a b c 527Proof 528 rpt strip_tac >> 529 qabbrev_tac `f = iterate a b` >> 530 Cases_on `c = 0` >- 531 rw[iterate_trace_sing, Abbr`f`] >> 532 `(c = c - 1 + 1) /\ (0 <= c)` by decide_tac >> 533 `LAST (iterate_trace a b c) = LAST (MAP f [0 .. c])` by rw[iterate_trace_def, Abbr`f`] >> 534 `_ = LAST (MAP f (SNOC c [0 .. (c-1)]))` by metis_tac[listRangeINC_SNOC] >> 535 `_ = LAST (SNOC (f c) (MAP f [0 .. (c-1)]))` by rw[MAP_SNOC] >> 536 `_ = f c` by rw[LAST_SNOC] >> 537 simp[Abbr`f`] 538QED 539 540(* Theorem: j <= c ==> EL j (iterate_trace a b c) = iterate a b j *) 541(* Proof: 542 Note j <= c means j < c + 1. 543 EL j (iterate_trace a b c) 544 = EL j (MAP (iterate a b) [0 .. c]) by iterate_trace_def 545 = (iterate a b) (EL j [0 .. c]) by EL_MAP, listRangeINC_LEN 546 = (iterate a b) (0 + j) by listRangeINC_EL 547 = iterate a b j 548*) 549Theorem iterate_trace_element: 550 !a b c j. j <= c ==> EL j (iterate_trace a b c) = iterate a b j 551Proof 552 rpt strip_tac >> 553 qabbrev_tac `f = iterate a b` >> 554 `EL j (iterate_trace a b c) = EL j (MAP f [0 .. c])` by rw[iterate_trace_def, Abbr`f`] >> 555 `_ = f (EL j [0 .. c])` by rw[EL_MAP, listRangeINC_LEN] >> 556 `_ = f j` by rw[listRangeINC_EL] >> 557 simp[Abbr`f`] 558QED 559 560(* Theorem: ls = iterate_trace a b c /\ ALL_DISTINCT ls /\ 561 j <= c ==> findi (iterate a b j) ls = j *) 562(* Proof: 563 Note LENGTH ls = 1 + c by iterate_trace_length 564 findi (iterate a b j) ls 565 = findi (EL j ls) by iterate_trace_element 566 = j by findi_EL, ALL_DISTINCT ls 567*) 568Theorem iterate_trace_element_idx: 569 !a b c ls j. ls = iterate_trace a b c /\ ALL_DISTINCT ls /\ 570 j <= c ==> findi (iterate a b j) ls = j 571Proof 572 rpt strip_tac >> 573 `LENGTH ls = 1 + c` by rw[iterate_trace_length] >> 574 `iterate a b j = EL j ls` by rw[iterate_trace_element] >> 575 rw[indexedListsTheory.findi_EL] 576QED 577 578(* Theorem: ls = iterate_trace a b c /\ x <> iterate a b c /\ 579 MEM x ls ==> MEM (b x) ls *) 580(* Proof: 581 MEM x ls 582 <=> ?j. j < LENGTH ls /\ (x = EL j ls) by MEM_EL 583 <=> ?j. j < 1 + c /\ (x = EL j ls) by iterate_trace_length 584 <=> ?j. j < 1 + c /\ (x = iterate a b j) by iterate_trace_element 585 ==> j <> c since x <> LAST ls, by iterate_trace_last 586 ==> j < c, so j + 1 < 1 + c by arithmetic 587 ==> b x = iterate a b (j + 1) by FUNPOW_SUC 588 ==> b x = EL (j + 1) ls by iterate_trace_element 589 ==> MEM (b x) ls by MEM_EL 590*) 591Theorem iterate_trace_member: 592 !a b c ls x. ls = iterate_trace a b c /\ x <> iterate a b c /\ 593 MEM x ls ==> MEM (b x) ls 594Proof 595 rpt strip_tac >> 596 qabbrev_tac `f = iterate a b` >> 597 rfs[MEM_EL, iterate_trace_length, iterate_trace_element] >> 598 `PRE (1 + c) = c` by decide_tac >> 599 `ls <> []` by fs[iterate_trace_non_nil] >> 600 `iterate a b c = LAST ls` by fs[iterate_trace_last] >> 601 `_ = EL c ls` by metis_tac[LAST_EL, iterate_trace_length] >> 602 `n <> c` by metis_tac[] >> 603 `n + 1 < c + 1` by decide_tac >> 604 qexists_tac `n + 1` >> 605 simp[] >> 606 `b (f n) = b (iterate a b n)` by fs[Abbr`f`] >> 607 `_ = iterate a b (SUC n)` by fs[GSYM FUNPOW_SUC] >> 608 `_ = EL (SUC n) ls` by rw[iterate_trace_element] >> 609 simp[ADD1] 610QED 611 612(* Theorem: ls = iterate_trace a b c ==> 613 (MEM x ls <=> ?j. j <= c /\ (x = iterate a b j)) *) 614(* Proof: 615 MEM x ls 616 <=> ?j. j < LENGTH ls /\ (x = EL j ls) by MEM_EL 617 <=> ?j. j < 1 + c /\ (x = EL j ls) by iterate_trace_length 618 <=> ?j. j < 1 + c /\ (x = iterate a b j) by iterate_trace_element 619*) 620Theorem iterate_trace_member_iff: 621 !a b c ls x. ls = iterate_trace a b c ==> 622 (MEM x ls <=> ?j. j <= c /\ (x = iterate a b j)) 623Proof 624 rw[MEM_EL, iterate_trace_length] >> 625 `!n c. n < c + 1 <=> n <= c` by decide_tac >> 626 metis_tac[iterate_trace_element] 627QED 628 629(* Theorem: ls = iterate_trace a b c /\ x <> iterate a b c /\ 630 MEM x ls /\ ALL_DISTINCT ls ==> (findi (b x) ls = 1 + findi x ls) *) 631(* Proof: 632 MEM x ls 633 <=> ?j. j < LENGTH ls /\ (x = EL j ls) by MEM_EL 634 <=> ?j. j < 1 + c /\ (x = EL j ls) by iterate_trace_length 635 Thus findi x ls = j by findi_EL 636 Also j <> c since x <> LAST ls by iterate_trace_last 637 ==> j < c, so j + 1 < 1 + c by arithmetic 638 b x 639 = iterate a b (j + 1) by FUNPOW_SUC 640 = EL (j + 1) ls by iterate_trace_element 641 Thus findi (b x) ls = 1 + j by findi_EL, iterate_trace_length 642 = 1 + findi x ls by above 643indexedListsTheory.findi_EL 644|- !l n. n < LENGTH l /\ ALL_DISTINCT l ==> (findi (EL n l) l = n) 645*) 646Theorem iterate_trace_index: 647 !a b c ls x. ls = iterate_trace a b c /\ x <> iterate a b c /\ 648 MEM x ls /\ ALL_DISTINCT ls ==> (findi (b x) ls = 1 + findi x ls) 649Proof 650 rpt strip_tac >> 651 qabbrev_tac `f = iterate a b` >> 652 rfs[MEM_EL, iterate_trace_length, iterate_trace_element] >> 653 `f n = x` by fs[iterate_trace_element, Abbr`f`] >> 654 `PRE (1 + c) = c` by decide_tac >> 655 `ls <> []` by fs[iterate_trace_non_nil] >> 656 `iterate a b c = LAST ls` by fs[iterate_trace_last] >> 657 `_ = EL c ls` by metis_tac[LAST_EL, iterate_trace_length] >> 658 `n <> c` by metis_tac[] >> 659 `n + 1 < c + 1` by decide_tac >> 660 `b (f n) = b (iterate a b n)` by fs[Abbr`f`] >> 661 `_ = iterate a b (SUC n)` by fs[GSYM FUNPOW_SUC] >> 662 `_ = EL (n + 1) ls` by rw[iterate_trace_element, ADD1] >> 663 fs[iterate_trace_length, indexedListsTheory.findi_EL] 664QED 665 666(* Theorem: FINITE s /\ b PERMUTES s /\ a IN s /\ 667 p = iterate_period b a /\ c < p ==> 668 ALL_DISTINCT (iterate_trace a b c) *) 669(* Proof: 670 Let ls = iterate_trace a b c. 671 By EL_ALL_DISTINCT_EL_EQ, this is to show: 672 n1 < LENGTH ls /\ n2 < LENGTH ls ==> (EL n1 ls = EL n2 ls) <=> (n1 = n2) 673 The only-if part is trivial, so just do the if-part. 674 675 Note LENGTH ls = 1 + c by iterate_trace_length 676 and c < p implies 1 + c <= p by arithmetic 677 ==> n1 < p and n2 < p by n1, n2 < LENGTH ls 678 Now EL n1 ls = iterate a b n1 by iterate_trace_element 679 and EL n2 ls = iterate a b n2 by iterate_trace_element 680 ==> n1 MOD p = n2 MOD p by iterate_period_mod_eq 681 or n1 = n2 by LESS_MOD 682*) 683Theorem iterate_trace_all_distinct: 684 !s a b c p. FINITE s /\ b PERMUTES s /\ a IN s /\ 685 p = iterate_period b a /\ c < p ==> 686 ALL_DISTINCT (iterate_trace a b c) 687Proof 688 rewrite_tac[EL_ALL_DISTINCT_EL_EQ] >> 689 rpt strip_tac >> 690 qabbrev_tac `ls = iterate_trace a b c` >> 691 `LENGTH ls = 1 + c` by fs[iterate_trace_length, Abbr`ls`] >> 692 `n1 < p /\ n2 < p` by decide_tac >> 693 `EL n1 ls = iterate a b n1` by fs[iterate_trace_element, Abbr`ls`] >> 694 `EL n2 ls = iterate a b n2` by fs[iterate_trace_element, Abbr`ls`] >> 695 metis_tac[iterate_period_mod_eq, LESS_MOD] 696QED 697 698(* Theorem: FINITE s /\ b PERMUTES s /\ a IN s /\ 699 p = iterate_period b a /\ c < p /\ n < c /\ 700 ~g (iterate a b n) /\ (!j. j < n ==> g (iterate a b j)) ==> 701 HOARE_SPEC {a} (WHILE g b) {iterate a b n} *) 702(* Proof: 703 Note 0 < p by iterate_period_pos 704 Let ls = iterate_trace a b c. 705 then LENGTH ls = 1 + c by iterate_trace_length 706 and ALL_DISTINCT ls by iterate_trace_all_distinct 707 708 By WHILE_RULE_PRE_POST, 709 with Invariant x = MEM x ls /\ findi x ls <= n, 710 Measure x = 1 + c - findi x ls. 711 Guard x = g x, Cmd x = b x, 712 Precond x = x IN {a}, Postcond x = x IN {iterate a b n}. 713 this is to show: 714 (1) MEM a ls for (!x. Precond x ==> Invariant x) 715 Note a = HD ls by iterate_trace_head 716 and ls <> [] by iterate_trace_non_nil 717 so MEM a ls by HEAD_MEM 718 (2) findi a ls <= n for (!x. Precond x ==> Invariant x) 719 Note a = iterate a b 0 by FUNPOW_0 720 so findi a ls = 0 by iterate_trace_element_idx 721 and surely, 0 <= n by arithmetic 722 (3) MEM x ls /\ findi x ls <= n /\ g x ==> 723 c + 1 < findi (b x) ls + (c + 1 - findi x ls) 724 for (!x. Invariant x /\ Guard x ==> Measure (Cmd x) < Measure x) 725 Let y = iterate a b c, which is LAST ls by iterate_trace_last 726 Then findi y ls = c by iterate_trace_element_idx 727 ==> x <> y by c <= n and n < c are incompatible 728 Thus findi (b x) ls 729 = 1 + findi x ls by iterate_trace_index, MEM x ls 730 the inequality is true by arithmetic 731 (4) MEM x ls /\ findi x ls <= n /\ ~g x ==> x = iterate a b n 732 for (!x. Invariant x /\ ~Guard x ==> Postcond x) 733 Note ?j. j <= c /\ (x = iterate a b j) by iterate_trace_member_iff, MEM x ls 734 so findi x ls = j by iterate_trace_element_idx 735 Thus ~(j < n) by ~g x, x = iterate a b j 736 so j = n by j <= n, ~(j < n) 737 and x = iterate a b j = iterate a b n. 738 (5) HOARE_SPEC (\x. (MEM x ls /\ findi x ls <= n) /\ g x) b 739 (\x. MEM x ls /\ findi x ls <= n) 740 for HOARE_SPEC (\x. Invariant x /\ Guard x) Cmd Invariant 741 By HOARE_SPEC_DEF, this is to show: 742 MEM x ls /\ findi x ls <= n /\ g x ==> MEM (b x) ls /\ findi (b x) ls <= n 743 744 Let y = iterate a b c, which is LAST ls by iterate_trace_last 745 Then findi y ls = c by iterate_trace_element_idx 746 ==> x <> y by c <= n and n < c are incompatible 747 Thus MEM (b x) ls by iterate_trace_member, MEM x ls, x <> y 748 Also findi (b x) ls 749 = 1 + findi x ls by iterate_trace_index, MEM x ls 750 Note ?j. j <= c /\ (x = iterate a b j) by iterate_trace_member_iff, MEM x ls 751 so findi x ls = j by iterate_trace_element_idx 752 But j <> n by ~g (iterate a b n) 753 so j < n by j <= n, j <> n 754 Thus findi (b x) ls <= n by arithmetic 755*) 756Theorem iterate_while_hoare: 757 !s a b c p g n. FINITE s /\ b PERMUTES s /\ a IN s /\ 758 p = iterate_period b a /\ n < c /\ c < p /\ 759 (* guard g is true before n, but false for n, to exit. *) 760 ~g (iterate a b n) /\ (!j. j < n ==> g (iterate a b j)) ==> 761 HOARE_SPEC {a} (WHILE g b) {iterate a b n} 762Proof 763 rpt strip_tac >> 764 `0 < p` by metis_tac[iterate_period_pos] >> 765 qabbrev_tac `ls = iterate_trace a b c` >> 766 `LENGTH ls = 1 + c` by rw[iterate_trace_length, Abbr`ls`] >> 767 `ALL_DISTINCT ls` by metis_tac[iterate_trace_all_distinct] >> 768 irule WHILE_RULE_PRE_POST >> 769 qexists_tac `\x. MEM x ls /\ findi x ls <= n` >> 770 qexists_tac `\x. 1 + c - findi x ls` >> 771 rw[] >| [ 772 `a = HD ls` by rw[iterate_trace_head, Abbr`ls`] >> 773 metis_tac[HEAD_MEM, iterate_trace_non_nil], 774 `a = iterate a b 0` by simp[] >> 775 `findi a ls = 0` by metis_tac[iterate_trace_element_idx, DECIDE``0 <= c``] >> 776 decide_tac, 777 qabbrev_tac `p = iterate_period b a` >> 778 qabbrev_tac `y = iterate a b c` >> 779 `findi y ls = c` by metis_tac[iterate_trace_element_idx, DECIDE``c <= c``] >> 780 `x <> y` by metis_tac[NOT_LESS] >> 781 `findi (b x) ls = 1 + findi x ls` by metis_tac[iterate_trace_index] >> 782 decide_tac, 783 qabbrev_tac `p = iterate_period b a` >> 784 `?j. j <= c /\ (x = iterate a b j)` by metis_tac[iterate_trace_member_iff] >> 785 `findi x ls = j` by metis_tac[iterate_trace_element_idx] >> 786 `~(j < n)` by metis_tac[] >> 787 `j = n` by decide_tac >> 788 fs[], 789 qabbrev_tac `p = iterate_period b a` >> 790 qabbrev_tac `y = iterate a b c` >> 791 `findi y ls = c` by metis_tac[iterate_trace_element_idx, DECIDE``c <= c``] >> 792 simp[whileTheory.HOARE_SPEC_DEF] >> 793 rpt strip_tac >| [ 794 `x <> y` by metis_tac[NOT_LESS] >> 795 metis_tac[iterate_trace_member], 796 `x <> y` by metis_tac[NOT_LESS] >> 797 `findi (b x) ls = 1 + findi x ls` by metis_tac[iterate_trace_index] >> 798 `?j. j <= c /\ (x = iterate a b j)` by metis_tac[iterate_trace_member_iff] >> 799 `findi x ls = j` by metis_tac[iterate_trace_element_idx] >> 800 `j <> n` by metis_tac[] >> 801 `j < n` by decide_tac >> 802 decide_tac 803 ] 804 ] 805QED 806 807(* Theorem: FINITE s /\ b PERMUTES s /\ a IN s /\ 808 p = iterate_period b a /\ n < c /\ c < p /\ 809 ~g (iterate a b n) /\ (!j. j < n ==> g (iterate a b j)) ==> 810 WHILE g b a = iterate a b n *) 811(* Proof: 812 Note HOARE_SPEC {a} (WHILE g b) 813 {iterate a b n} by iterate_while_hoare 814 Now a IN {a} by IN_SING 815 so {a} a by set as function 816 ==> {iterate a b n} ((WHILE g b) a) by HOARE_SPEC_DEF 817 or WHILE g b a IN {iterate a b n} by set as function 818 Thus WHILE g b a = iterate a b n by IN_SING 819> whileTheory.HOARE_SPEC_DEF; 820val it = |- !P C Q. HOARE_SPEC P C Q <=> !s. P s ==> Q (C s): thm 821Put C = (WHILE g b) 822*) 823Theorem iterate_while_thm_1: 824 !s a b c p g n. FINITE s /\ b PERMUTES s /\ a IN s /\ 825 p = iterate_period b a /\ n < c /\ c < p /\ 826 ~g (iterate a b n) /\ (!j. j < n ==> g (iterate a b j)) ==> 827 WHILE g b a = iterate a b n 828Proof 829 rpt strip_tac >> 830 `HOARE_SPEC {a} (WHILE g b) {iterate a b n}` by metis_tac[iterate_while_hoare] >> 831 fs[whileTheory.HOARE_SPEC_DEF] 832QED 833 834(* This is another milestone. Now depreciated, see iterate_while_thm below. *) 835 836(* Theorem: ~g a ==> HOARE_SPEC {a} (WHILE g b) {a} *) 837(* Proof: 838 By WHILE_RULE_PRE_POST, 839 set Invariant as (\x. x = a), 840 and Measure as any, e.g. (\x. 1). 841 This is to show: 842 (1) ~g a /\ g a ==> F, which is trivial. 843 (2) ~g a ==> HOARE_SPEC (\x. (x = a) /\ g x) b (\x. x = a) 844 This is also trival by HOARE_SPEC_DEF 845*) 846Theorem iterate_while_hoare_0: 847 !a b g. ~g a ==> HOARE_SPEC {a} (WHILE g b) {a} 848Proof 849 rpt strip_tac >> 850 irule WHILE_RULE_PRE_POST >> 851 qexists_tac `\x. x = a` >> 852 qexists_tac `\x. 1` >> 853 rw[] >- 854 metis_tac[] >> 855 rw[whileTheory.HOARE_SPEC_DEF] 856QED 857 858(* Theorem: ~g a ==> WHILE g b a = a *) 859(* Proof: 860 Note HOARE_SPEC {a} (WHILE g b) {a} by iterate_while_hoare_0 861 Thus WHILE g b a = a by HOARE_SPEC_DEF 862*) 863Theorem iterate_while_thm_0: 864 !a b g. ~g a ==> WHILE g b a = a 865Proof 866 rpt strip_tac >> 867 `HOARE_SPEC {a} (WHILE g b) {a}` by rw[iterate_while_hoare_0] >> 868 fs[whileTheory.HOARE_SPEC_DEF] 869QED 870 871(* ------------------------------------------------------------------------- *) 872(* Direct from WHILE definition. *) 873(* ------------------------------------------------------------------------- *) 874 875(* from whileTheory: 876 877WHILE 878|- !P g x. WHILE P g x = if P x then WHILE P g (g x) else x 879WHILE |> ISPEC ``g:'a -> bool`` |> ISPEC ``b:'a -> 'a``; 880val it = |- !x. WHILE g b x = if g x then WHILE g b (b x) else x: thm 881WHILE |> ISPEC ``g:'a -> bool`` |> ISPEC ``b:'a -> 'a`` |> ISPEC ``FUNPOW b n x``; 882|- WHILE g b (FUNPOW b n x) = 883 if g (FUNPOW b n x) then WHILE g b (b (FUNPOW b n x)) else FUNPOW b n x: thm 884*) 885 886 887(* Theorem: (!j. j < k ==> g (FUNPOW b j x)) ==> 888 (WHILE g b x = 889 if g (FUNPOW b k x) then WHILE g b (FUNPOW b (k + 1) x) else FUNPOW b k x) *) 890(* Proof: 891 Note FUNPOW b (k + 1) x to b (FUNPOW b k x) by FUNPOW_SUC, ADD1 892 By induction on k. 893 Base: WHILE g b x = 894 if g (FUNPOW b 0 x) then WHILE g b (b (FUNPOW b 0 x)) else FUNPOW b 0 x 895 which simplifies to show: 896 WHILE g b x = if g x then WHILE g b (b x) else x by FUNPOW_0 897 This is true by WHILE 898 Step: (!j. j < k ==> g (FUNPOW b j x)) ==> 899 (WHILE g b x = if g (FUNPOW b k x) then WHILE g b (b (FUNPOW b k x)) else FUNPOW b k x) 900 ==> (!j. j < SUC k ==> g (FUNPOW b j x)) ==> 901 (WHILE g b x = if g (FUNPOW b (SUC k) x) then WHILE g b (b (FUNPOW b (SUC k) x)) else FUNPOW b (SUC k) x) 902 Note !j. j < SUC k ==> g (FUNPOW b j x) means 903 !j. j < k ==> g (FUNPOW b j x) and g (FUNPOW b k x) 904 WHILE g b x 905 = WHILE g b (b (FUNPOW b k x)) by induction hypothesis 906 = WHILE g b (FUNPOW (SUC b) k x) by FUNPOW_SUC 907 = if g (FUNPOW b (SUC k) x) then WHILE g b (b (FUNPOW b (SUC k x)) else FUNPOW b (SUC k) x 908 by WHILE 909*) 910Theorem iterate_while_eqn: 911 !g b x k. (!j. j < k ==> g (FUNPOW b j x)) ==> 912 WHILE g b x = 913 if g (FUNPOW b k x) then WHILE g b (FUNPOW b (k + 1) x) 914 else FUNPOW b k x 915Proof 916 simp[FUNPOW_SUC, GSYM ADD1] >> 917 ntac 3 strip_tac >> 918 Induct >- 919 rw[Once WHILE] >> 920 rw[Once WHILE, FUNPOW_SUC] 921QED 922 923(* Theorem: (!j. j < k ==> g (FUNPOW b j x)) /\ ~g (FUNPOW b k x) ==> 924 WHILE g b x = FUNPOW b k x *) 925(* Proof: by iterate_while_eqn. *) 926Theorem iterate_while_thm: 927 !g b x k. (!j. j < k ==> g (FUNPOW b j x)) /\ ~g (FUNPOW b k x) ==> 928 WHILE g b x = FUNPOW b k x 929Proof 930 metis_tac[iterate_while_eqn] 931QED 932 933 934 935(* ------------------------------------------------------------------------- *) 936 937(* export theory at end *) 938val _ = export_theory(); 939 940(*===========================================================================*) 941