1(* ------------------------------------------------------------------------- *) 2(* Loop Recurrence with Decreasing argument *) 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 "loopDecrease"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* Get dependent theories in lib *) 21(* val _ = load "loopTheory"; *) 22open loopTheory; 23 24(* open dependent theories *) 25open arithmeticTheory; 26open dividesTheory; 27open helperNumTheory helperListTheory helperFunctionTheory; (* replace DIV_EQ_0 *) 28open listTheory rich_listTheory; 29open listRangeTheory; 30 31 32(* ------------------------------------------------------------------------- *) 33(* Loop Recurrence with Decreasing argument Documentation *) 34(* ------------------------------------------------------------------------- *) 35(* Type and Overload: 36 decreasing = decrease_by 1 37*) 38(* Definitions and Theorems (# are exported): 39 40 Helper Theorems: 41 42 Decreasing Count: 43 hop_def |- !n b. hop b n = if b = 0 \/ n = 0 then 0 else SUC (hop b (n - b)) 44 hop_alt |- !n b. hop b n = if b = 0 \/ n = 0 then 0 else 1 + hop b (n - b) 45 hop_0 |- !b n. b = 0 \/ n = 0 ==> hop b n = 0 46 hop_suc |- !b n. 0 < b /\ 0 < n ==> hop b n = SUC (hop b (n - b)) 47 hop_zero |- !b n. hop b 0 = 0 /\ hop 0 n = 0 48 hop_nonzero |- !b n. 0 < b /\ 0 < n ==> hop b n = 1 + hop b (n - b) 49 hop_pos |- !b n. 0 < b /\ 0 < n ==> 0 < hop b n 50 hop_property |- !b n. 0 < b /\ 0 < n ==> !j. b * j < n <=> j < hop b n 51 hop_exceeds |- !b n. 0 < b ==> n <= b * hop b n 52 hop_eqn |- !b n. hop b n = if b = 0 then 0 else n DIV b + if n MOD b = 0 then 0 else 1 53 hop_DIV |- !b n. hop b n <= 1 + n DIV b 54 hop_1_n |- !n. hop 1 n = n 55 hop_eq_loop_count 56 |- !b x. 0 < b ==> hop b x = loop_count (\x. x = 0) (\x. x - b) x 57 hop_eq_loop2_count 58 |- !b f x y. 0 < b ==> hop b y = loop2_count (\x y. y = 0) (\y. y - b) f x y 59 decrease_falling |- !b. FALLING (\x. x - b) 60 iterating_dec_eqn |- !b n x. FUNPOW (\x. x - b) n x = x - n * b 61 iterating_dec_hop |- !b x. 0 < b ==> FUNPOW (\x. x - b) (hop b x) x = 0 62 iterating_dec_hop_alt |- !b x. 0 < b ==> x <= hop b x * b 63 64 Decrease Loop: 65 loop_dec_count_eqn |- !loop body b c. 0 < b /\ 66 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 67 !x. loop x = c + SUM (GENLIST (\j. body (x - j * b)) (hop b x)) 68 loop_dec_count_exit_sum_le 69 |- !loop body exit b c. 0 < b /\ 70 (!x. loop x = 71 if x = 0 then c 72 else body x + if exit x then 0 else loop (x - b)) ==> 73 !x. loop x <= c + SUM (GENLIST (\j. body (x - j * b)) (hop b x)) 74 loop_dec_count_cover_exit_le 75 |- !loop body cover exit b c. 0 < b /\ 76 (!x. body x <= cover x) /\ MONO cover /\ 77 (!x. loop x = 78 if x = 0 then c 79 else body x + if exit x then 0 else loop (x - b)) ==> 80 !x. loop x <= c + hop b x * cover x 81 loop_dec_count_exit_le |- !loop body exit b c. 0 < b /\ MONO body /\ 82 (!x. loop x = 83 if x = 0 then c 84 else body x + if exit x then 0 else loop (x - b)) ==> 85 !x. loop x <= c + hop b x * body x 86 loop_dec_count_cover_le |- !loop body cover b c. 0 < b /\ 87 (!x. body x <= cover x) /\ MONO cover /\ 88 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 89 !x. loop x <= c + hop b x * cover x 90 loop_dec_count_le |- !loop body b c. 0 < b /\ MONO body /\ 91 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 92 !x. loop x <= c + hop b x * body x 93 loop_dec_count_rcover_exit_le 94 |- !loop body cover exit b c. 0 < b /\ 95 (!x. body x <= cover x) /\ RMONO cover /\ 96 (!x. loop x = 97 if x = 0 then c 98 else body x + if exit x then 0 else loop (x - b)) ==> 99 !x. loop x <= c + hop b x * cover 0 100 loop_dec_count_rbody_exit_le 101 |- !loop body exit b c. 0 < b /\ RMONO body /\ 102 (!x. loop x = 103 if x = 0 then c 104 else body x + if exit x then 0 else loop (x - b)) ==> 105 !x. loop x <= c + hop b x * body 0 106 loop_dec_count_rcover_le|- !loop body cover b c. 0 < b /\ 107 (!x. body x <= cover x) /\ RMONO cover /\ 108 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 109 !x. loop x <= c + hop b x * cover 0 110 loop_dec_count_rbody_le |- !loop body b c. 0 < b /\ RMONO body /\ 111 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 112 !x. loop x <= c + hop b x * body 0 113 114 Decrease Loop with Transform: 115 loop2_dec_count_eqn |- !loop f body quit b. 0 < b /\ 116 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 117 !x y. loop x y = quit (FUNPOW f (hop b y) x) + 118 SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) (hop b y)) 119 loop2_dec_count_sum_le |- !loop f body quit exit b. 0 < b /\ 120 (!x y. loop x y = 121 if y = 0 then quit x 122 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 123 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 124 SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) (hop b y)) 125 126 Decreasing Loop with Transform-independent Body: 127 loop2_dec_count_mono_cover_exit_le 128 |- !loop f body quit cover exit b g. 0 < b /\ 129 (!x y. body x y <= cover x y) /\ cover = (\x y. g y) /\ MONO g /\ 130 (!x y. loop x y = 131 if y = 0 then quit x 132 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 133 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * g y 134 loop2_dec_count_mono_exit_le 135 |- !loop f body quit exit b g. 0 < b /\ body = (\x y. g y) /\ MONO g /\ 136 (!x y. loop x y = 137 if y = 0 then quit x 138 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 139 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * g y 140 loop2_dec_count_mono_cover_le 141 |- !loop f body quit cover b g. 0 < b /\ 142 (!x y. body x y <= cover x y) /\ cover = (\x y. g y) /\ MONO g /\ 143 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 144 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * g y 145 loop2_dec_count_mono_le 146 |- !loop f body quit b g. 0 < b /\ body = (\x y. g y) /\ MONO g /\ 147 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 148 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * g y 149 loop2_dec_count_rmono_cover_exit_le 150 |- !loop f body quit cover exit b g. 0 < b /\ 151 (!x y. body x y <= cover x y) /\ cover = (\x y. g y) /\ RMONO g /\ 152 (!x y. loop x y = 153 if y = 0 then quit x 154 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 155 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * g 0 156 loop2_dec_count_rmono_exit_le 157 |- !loop f body quit exit b g. 0 < b /\ body = (\x y. g y) /\ RMONO g /\ 158 (!x y. loop x y = 159 if y = 0 then quit x 160 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 161 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * g 0 162 loop2_dec_count_rmono_cover_le 163 |- !loop f body quit cover b g. 0 < b /\ 164 (!x y. body x y <= cover x y) /\ cover = (\x y. g y) /\ RMONO g /\ 165 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 166 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * g 0 167 loop2_dec_count_rmono_le 168 |- !loop f body quit b g. 0 < b /\ body = (\x y. g y) /\ RMONO g /\ 169 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 170 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * g 0 171 172 Decreasing Loop with Numeric Transform: 173 loop2_dec_rise_count_cover_exit_le 174 |- !loop f body quit cover exit b. 0 < b /\ 175 (!x y. body x y <= cover x y) /\ MONO2 cover /\ RISING f /\ 176 (!x y. loop x y = 177 if y = 0 then quit x 178 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 179 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 180 hop b y * cover (FUNPOW f (hop b y) x) y 181 loop2_dec_rise_count_exit_le 182 |- !loop f body quit exit b. 0 < b /\ MONO2 body /\ RISING f /\ 183 (!x y. loop x y = 184 if y = 0 then quit x 185 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 186 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 187 hop b y * body (FUNPOW f (hop b y) x) y 188 loop2_dec_rise_count_cover_le 189 |- !loop f body quit cover b. 0 < b /\ 190 (!x y. body x y <= cover x y) /\ MONO2 cover /\ RISING f /\ 191 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 192 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 193 hop b y * cover (FUNPOW f (hop b y) x) y 194 loop2_dec_rise_count_le |- !loop f body quit b. 0 < b /\ MONO2 body /\ RISING f /\ 195 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 196 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 197 hop b y * body (FUNPOW f (hop b y) x) y 198 loop2_dec_fall_count_cover_exit_le 199 |- !loop f body quit cover exit b. 0 < b /\ 200 (!x y. body x y <= cover x y) /\ MONO2 cover /\ FALLING f /\ 201 (!x y. loop x y = 202 if y = 0 then quit x 203 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 204 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover x y 205 loop2_dec_fall_count_exit_le 206 |- !loop f body quit exit b. 0 < b /\ MONO2 body /\ FALLING f /\ 207 (!x y. loop x y = 208 if y = 0 then quit x 209 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 210 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body x y 211 loop2_dec_fall_count_cover_le 212 |- !loop f body quit cover b. 0 < b /\ 213 (!x y. body x y <= cover x y) /\ MONO2 cover /\ FALLING f /\ 214 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 215 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover x y 216 loop2_dec_fall_count_le |- !loop f body quit b. 0 < b /\ MONO2 body /\ FALLING f /\ 217 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 218 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body x y 219 220 Decreasing Loop with Transform cover: 221 loop2_dec_mono_count_cover_exit_le 222 |- !loop f g body quit cover exit b. 0 < b /\ 223 (!x y. body x y <= cover x y) /\ MONO2 cover /\ 224 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 225 (!x y. loop x y = 226 if y = 0 then quit x 227 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 228 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 229 hop b y * cover (FUNPOW g (hop b y) x) y 230 loop2_dec_mono_count_exit_le 231 |- !loop f g body quit exit b. 0 < b /\ MONO2 body /\ 232 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 233 (!x y. loop x y = 234 if y = 0 then quit x 235 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 236 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 237 hop b y * body (FUNPOW g (hop b y) x) y 238 loop2_dec_mono_count_cover_le 239 |- !loop f g body quit cover b. 0 < b /\ 240 (!x y. body x y <= cover x y) /\ MONO2 cover /\ 241 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 242 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 243 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 244 hop b y * cover (FUNPOW g (hop b y) x) y 245 loop2_dec_mono_count_le |- !loop f g body quit b. 0 < b /\ MONO2 body /\ 246 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 247 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 248 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 249 hop b y * body (FUNPOW g (hop b y) x) y 250 251 Original: 252 Decreasing List: 253 decrease_by_def |- !n b. decrease_by b n = 254 if b = 0 \/ n = 0 then [] else n::decrease_by b (n - b) 255 decrease_by_nil |- !b n. b = 0 \/ n = 0 ==> decrease_by b n = [] 256 decrease_by_cons |- !b n. 0 < b /\ 0 < n ==> decrease_by b n = n::decrease_by b (n - b) 257 decrease_by_0_n |- !n. decrease_by 0 n = [] 258 decrease_by_b_0 |- !b. decrease_by b 0 = [] 259 decrease_by_b_nonzero |- !b n. 0 < b /\ n <> 0 ==> decrease_by b n = n::decrease_by b (n - b) 260 decrease_by_eqn |- !b n. decrease_by b n = GENLIST (\j. n - j * b) (hop b n) 261 decrease_by_member |- !b n j. 0 < b /\ 0 < n /\ j * b < n ==> MEM (n - j * b) (decrease_by b n) 262 decrease_by_head |- !b n. 0 < b /\ 0 < n ==> MEM n (decrease_by b n) 263 decrease_by_length |- !b n. LENGTH (decrease_by b n) = hop b n 264 decrease_by_element |- !b n j. j < hop b n ==> EL j (decrease_by b n) = n - j * b 265 decreasing_length |- !n. LENGTH (decreasing n) = n 266 decreasing_eqn |- !n. decreasing n = REVERSE [1 .. n] 267 decrease_by_eq_loop_arg |- !b x. 0 < b ==> decrease_by b x = loop_arg (\x. x = 0) (\x. x - b) x 268 iterating_decrease_eq_loop2_arg 269 |- !b body f x y. 0 < b ==> 270 MAP2 body (iterating f x (hop b y)) (decrease_by b y) = 271 MAP (UNCURRY body) (loop2_arg (\x y. y = 0) (\y. y - b) f x y) 272 273 loop_dec_count_by_sum |- !loop body b c. 0 < b /\ 274 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 275 !x. loop x = c + SUM (MAP body (decrease_by b x)) 276 loop_dec_count_exit_by_sum 277 |- !loop body b c exit. 0 < b /\ 278 (!x. loop x = 279 if x = 0 then c 280 else body x + if exit x then 0 else loop (x - b)) ==> 281 !x. loop x <= c + SUM (MAP body (decrease_by b x)) 282 loop_dec_count_cover_exit_upper 283 |- !loop body cover exit b c. 0 < b /\ 284 (!x. body x <= cover x) /\ MONO cover /\ 285 (!x. loop x = 286 if x = 0 then c 287 else body x + if exit x then 0 else loop (x - b)) ==> 288 !x. loop x <= c + cover x * hop b x 289 loop_dec_count_exit_upper 290 |- !loop body b c exit. 0 < b /\ MONO body /\ 291 (!x. loop x = 292 if x = 0 then c 293 else body x + if exit x then 0 else loop (x - b)) ==> 294 !x. loop x <= c + body x * hop b x 295 loop_dec_count_cover_upper 296 |- !loop body b c cover. 0 < b /\ 297 (!x. body x <= cover x) /\ MONO cover /\ 298 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 299 !x. loop x <= c + cover x * hop b x 300 loop_dec_count_upper |- !loop body b c. 0 < b /\ MONO body /\ 301 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 302 !x. loop x <= c + body x * hop b x 303 304 loop2_dec_count_by_sum 305 |- !loop f body b c. 0 < b /\ 306 (!x y. loop x y = if y = 0 then c else body x y + loop (f x) (y - b)) ==> 307 !x y. loop x y = c + SUM (MAP2 body (iterating f x (hop b y)) (decrease_by b y)) 308 loop2_dec_count_exit_by_sum 309 |- !loop f body b c exit. 0 < b /\ 310 (!x y. loop x y = 311 if y = 0 then c 312 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 313 !x y. loop x y <= c + SUM (MAP2 body (iterating f x (hop b y)) (decrease_by b y)) 314 loop2_dec_count_cover_exit_upper 315 |- !loop f body cover exit b c. 0 < b /\ (!x y. body x y <= cover x y) /\ 316 (!x1 x2 y1 y2. y1 <= y2 ==> cover x1 y1 <= cover x2 y2) /\ 317 (!x y. loop x y = 318 if y = 0 then c 319 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 320 !x y. loop x y <= c + cover x y * hop b y 321 loop2_dec_count_exit_upper 322 |- !loop f body exit b c. 0 < b /\ 323 (!x1 x2 y1 y2. y1 <= y2 ==> body x1 y1 <= body x2 y2) /\ 324 (!x y. loop x y = 325 if y = 0 then c 326 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 327 !x y. loop x y <= c + body x y * hop b y 328 loop2_dec_count_cover_upper 329 |- !loop f body cover b c. 0 < b /\ (!x y. body x y <= cover x y) /\ 330 (!x1 x2 y1 y2. y1 <= y2 ==> cover x1 y1 <= cover x2 y2) /\ 331 (!x y. loop x y = if y = 0 then c else body x y + loop (f x) (y - b)) ==> 332 !x y. loop x y <= c + cover x y * hop b y 333 loop2_dec_count_upper 334 |- !loop f body b c. 0 < b /\ 335 (!x1 x2 y1 y2. y1 <= y2 ==> body x1 y1 <= body x2 y2) /\ 336 (!x y. loop x y = if y = 0 then c else body x y + loop (f x) (y - b)) ==> 337 !x y. loop x y <= c + body x y * hop b y 338*) 339 340(* ------------------------------------------------------------------------- *) 341(* Loop Recurrence with Decreasing argument *) 342(* ------------------------------------------------------------------------- *) 343 344(* ------------------------------------------------------------------------- *) 345(* Decreasing Count. *) 346(* ------------------------------------------------------------------------- *) 347 348(* Define a hop function, count of hops to zero. *) 349val hop_def = Define` 350 hop b n = if (b = 0) \/ (n = 0) then 0 else SUC (hop b (n - b)) 351`; 352 353(* alternate form *) 354val hop_alt = save_thm("hop_alt", hop_def |> REWRITE_RULE [SUC_ONE_ADD]); 355(* val hop_alt = |- !n b. hop b n = if b = 0 \/ n = 0 then 0 else 1 + hop b (n - b): thm *) 356 357(* Theorem: ((b = 0) \/ (n = 0) ==> (hop b n = 0) *) 358(* Proof: by hop_def *) 359val hop_0 = store_thm( 360 "hop_0", 361 ``!b n. (b = 0) \/ (n = 0) ==> (hop b n = 0)``, 362 rw[Once hop_def]); 363 364(* Theorem: 0 < b /\ 0 < n ==> (hop b n = SUC (hop b (n - b))) *) 365(* Proof: by hop_def *) 366val hop_suc = store_thm( 367 "hop_suc", 368 ``!b n. 0 < b /\ 0 < n ==> (hop b n = SUC (hop b (n - b)))``, 369 rw[Once hop_def]); 370 371(* Theorem: (hop b 0 = 0) /\ (hop 0 n = 0) *) 372(* Proof: by hop_def *) 373val hop_zero = store_thm( 374 "hop_zero", 375 ``!b n. (hop b 0 = 0) /\ (hop 0 n = 0)``, 376 rw[Once hop_def] >> 377 rw[Once hop_def]); 378 379(* Theorem: 0 < b /\ 0 < n ==> (hop b n = 1 + hop b (n - b)) *) 380(* Proof: by hop_def *) 381val hop_nonzero = store_thm( 382 "hop_nonzero", 383 ``!b n. 0 < b /\ 0 < n ==> (hop b n = 1 + hop b (n - b))``, 384 rw[Once hop_def]); 385 386(* Theorem: 0 < b /\ 0 < n ==> 0 < hop b n *) 387(* Proof: by hop_def *) 388val hop_pos = store_thm( 389 "hop_pos", 390 ``!b n. 0 < b /\ 0 < n ==> 0 < hop b n``, 391 rw[Once hop_def]); 392 393(* Theorem: 0 < b /\ 0 < n ==> !j. b * j < n <=> j < hop b n *) 394(* Proof: 395 By induction from hop_def. 396 If n - b = 0, 397 Then n <= b by SUB_EQ_0 398 and hop b n = 1 + hop b 0 by hop_def 399 = 1 + 0 = 1 by hop_zero 400 If j = 0, LHS = T = RHS by hop_pos, 0 < b, 0 < n 401 If j <> 0, LHS = F = RHS by b <= b * j when j <> 0 402 If n - b <> 0, 403 Then 0 < n - b by arithmetic 404 so b * (j - 1) < n - b <=> j - 1 < hop b (n - b) 405 by induction hypothesis 406 If j = 0, LHS = T = RHS by hop_pos, 0 < b, 0 < n 407 If j <> 0, 408 b * j - b < n - b <=> j < 1 + hop b (n - b) by above 409 or b * j < n <=> j < hop b n by hop_nonzero 410*) 411val hop_property = store_thm( 412 "hop_property", 413 ``!b n. 0 < b /\ 0 < n ==> !j. b * j < n <=> j < hop b n``, 414 ho_match_mp_tac (theorem "hop_ind") >> 415 rw[] >> 416 Cases_on `n - b = 0` >| [ 417 `n <= b` by decide_tac >> 418 (Cases_on `j = 0` >> simp[Once hop_def]) >> 419 `b <= b * j` by rw[] >> 420 rw[Once hop_def], 421 `(j - 1) * b < n - b <=> j - 1 < hop b (n - b)` by rw[] >> 422 (Cases_on `j = 0` >> simp[Once hop_def]) 423 ]); 424 425(* Theorem: 0 < b ==> n <= b * hop b n *) 426(* Proof: 427 If n = 0, this is trivial. 428 If n <> 0, 429 Note b * hop b n < n 430 <=> hop b n < hop b n by hop_property, 0 < n 431 <=> F 432 Thus n <= b * hop b n is true. 433*) 434val hop_exceeds = store_thm( 435 "hop_exceeds", 436 ``!b n. 0 < b ==> n <= b * hop b n``, 437 rpt strip_tac >> 438 (Cases_on `n = 0` >> simp[]) >> 439 metis_tac[hop_property, LESS_EQ_REFL, NOT_LESS, NOT_ZERO]); 440 441 442(* 443val foo_def = Define` 444 foo b n = if (b = 0) then 0 else (n DIV b + if n MOD b = 0 then 0 else 1) 445`; 446 447> EVAL ``MAP (hop 7) [1 .. 20]``; = [1; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 3; 3; 3; 3; 3; 3]: thm 448> EVAL ``MAP (foo 7) [1 .. 20]``; = [1; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 3; 3; 3; 3; 3; 3]: thm 449*) 450 451(* Theorem: hop b n = if (b = 0) then 0 else (n DIV b + if n MOD b = 0 then 0 else 1) *) 452(* Proof: 453 By complete induction on n. 454 If b = 0, then hop 0 n = 0 by hop_def 455 If n = 0, 456 LHS = hop b 0 = 0 by hop_def 457 RHS = 0 + 0 = 0 = LHS by ZERO_DIV, ZERO_MOD 458 Otherwise, b <> 0 and n <> 0. 459 If n < b, 460 Then n - b = 0 by n < b 461 LHS = hop b n 462 = SUC (hop b (n - b)) by hop_def 463 = SUC (hop b 0) by n - b = 0 464 = SUC 0 = 1 by hop_def, ADD1 465 Now n MOD b = n <> 0 by LESS_MOD, n < b 466 and n DIV b = 0 by LESS_DIV_EQ_ZERO, n < b 467 RHS = 0 + 1 = 1 = LHS by above 468 If b <= n, 469 Then b = n or b < n. 470 If b = n, 471 LHS = hop b n 472 = SUC (hop b 0) by hop_def 473 = SUC 0 = 1 by hop_def, ADD1 474 RHS = 1 + 0 = 1 = LHS by DIVMOD_ID, 0 < b 475 If b < n, 476 LHS = hop b n 477 = SUC (hop b (n - b)) by hop_def 478 = SUC ((n - b) DIV b + if (n - b) MOD b = 0 then 0 else 1) 479 by induction hypothesis 480 But (n - b) DIV b = n DIV b - 1 by SUB_DIV, 0 < b, b <= n 481 and (n - m) MOD b = n MOD b by SUB_MOD, 0 < b, b <= n 482 and n DIV b <> 0 by DIV_EQ_0, 0 < b, ~(n < b) 483 LHS = 1 + (n DIV b - 1 + if (n MOD b = 0) then 0 else 1) by ADD1 484 = n DIV m + (if (n MOD b = 0) then 0 else 1) by n DIV b <> 0 485 = RHS 486*) 487val hop_eqn = store_thm( 488 "hop_eqn", 489 ``!b n. hop b n = if (b = 0) then 0 else (n DIV b + if n MOD b = 0 then 0 else 1)``, 490 strip_tac >> 491 completeInduct_on `n` >> 492 Cases_on `b = 0` >- 493 rw[Once hop_def] >> 494 fs[] >> 495 Cases_on `n = 0` >| [ 496 `0 DIV b = 0` by rw[ZERO_DIV] >> 497 `0 MOD b = 0` by rw[] >> 498 rw[Once hop_def], 499 Cases_on `n < b` >| [ 500 `n - b = 0` by decide_tac >> 501 `n DIV b = 0` by rw[LESS_DIV_EQ_ZERO] >> 502 `n MOD b = n` by rw[] >> 503 `0 DIV b = 0` by rw[ZERO_DIV] >> 504 rw[Once hop_def], 505 `b <= n` by decide_tac >> 506 `(n - b) DIV b = n DIV b - 1` by rw[SUB_DIV] >> 507 `(n - b) MOD b = n MOD b` by rw[SUB_MOD] >> 508 `n DIV b <> 0` by rw[DIV_EQ_0] >> 509 rw[Once hop_def] 510 ] 511 ]); 512 513(* Theorem: hop b n <= 1 + n DIV b *) 514(* Proof: by hop_eqn *) 515val hop_DIV = store_thm( 516 "hop_DIV", 517 ``!b n. hop b n <= 1 + n DIV b``, 518 rw[hop_eqn]); 519 520(* Theorem: hop 1 n = n *) 521(* Proof: 522 hop 1 n 523 = n DIV 1 + if n MOD 1 = 0 then 0 else 1 by hop_eqn 524 = n + if 0 = 0 then 0 else 1 by DIV_1, MOD_1 525 = n 526*) 527val hop_1_n = store_thm( 528 "hop_1_n", 529 ``!n. hop 1 n = n``, 530 rw[hop_eqn]); 531 532(* Theorem: 0 < b ==> (hop b x = loop_count (\x. x = 0) (\x. x - b) x) *) 533(* Proof: 534 By induction from hop_def. 535 Let guard = (\x. x = 0), 536 modify = (\x. x - b), 537 R = measure (\x. x). 538 The goal is: hop b x = loop_count guard modify x 539 540 Note WF R by WF_measure 541 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 542 If guard x, 543 Then x = 0 by guard x 544 hop b 0 545 = 0 by hop_0 546 = loop_count guard modify 0 by loop_count_0, guard x 547 If ~guard x, 548 Then x <> 0 by ~guard x 549 hop b x 550 = SUC (hop b (x - b)) by hop_suc 551 = SUC (loop_count guard modify (x - b)) 552 by induction hypothesis 553 = loop_count guard modify x by loop_count_suc 554*) 555val hop_eq_loop_count = store_thm( 556 "hop_eq_loop_count", 557 ``!b x. 0 < b ==> (hop b x = loop_count (\x. x = 0) (\x. x - b) x)``, 558 ho_match_mp_tac (theorem "hop_ind") >> 559 rw[] >> 560 qabbrev_tac `guard = \x. x = 0` >> 561 qabbrev_tac `modify = \x. x - b` >> 562 qabbrev_tac `R = measure (\x. x)` >> 563 `WF R` by rw[Abbr`R`] >> 564 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`modify`, Abbr`R`] >> 565 Cases_on `guard x` >| [ 566 `x = 0` by metis_tac[] >> 567 metis_tac[hop_0, loop_count_0], 568 `x <> 0` by metis_tac[] >> 569 `hop b x = SUC (hop b (x - b))` by rw[hop_suc] >> 570 `_ = SUC (loop_count guard modify (x - b))` by metis_tac[NOT_ZERO] >> 571 `_ = loop_count guard modify x` by metis_tac[loop_count_suc] >> 572 decide_tac 573 ]); 574 575(* Theorem: 0 < b ==> (hop b y = loop2_count (\x y. y = 0) (\y. y - b) f x y) *) 576(* Proof: 577 By induction from hop_def. 578 Let guard = (\x y. y = 0), 579 modify = (\y. y - b), 580 R = measure (\(x,y). y). 581 The goal is: hop b y = loop2_count guard modify f x y 582 583 Note WF R by WF_measure 584 and !x y. ~guard x y ==> R (f x,modify y) (x,y) by y - b < y, 0 < b 585 If guard x y, 586 Then y = 0 by guard x y 587 hop b 0 588 = 0 by hop_0 589 = loop2_count guard modify f x 0 by loop2_count_0, guard x y 590 If ~guard x y, 591 Then y <> 0 by ~guard x y 592 hop b y 593 = SUC (hop b (y - b)) by hop_suc 594 = SUC (loop2_count guard modify f (f x) (y - b)) 595 by induction hypothesis, take (f x). 596 = loop2_count guard modify f x y by loop2_count_suc 597*) 598val hop_eq_loop2_count = store_thm( 599 "hop_eq_loop2_count", 600 ``!b f x y. 0 < b ==> (hop b y = loop2_count (\x y. y = 0) (\y. y - b) f x y)``, 601 ntac 4 strip_tac >> 602 qid_spec_tac `x` >> 603 qid_spec_tac `y` >> 604 qid_spec_tac `b` >> 605 ho_match_mp_tac (theorem "hop_ind") >> 606 rw[] >> 607 qabbrev_tac `guard = \x y. y = 0` >> 608 qabbrev_tac `modify = \y. y - b` >> 609 qabbrev_tac `R = measure (\(x,y). y)` >> 610 `WF R` by rw[Abbr`R`] >> 611 `!x y. ~guard x y ==> R (f x,modify y) (x,y)` by rw[Abbr`guard`, Abbr`modify`, Abbr`R`] >> 612 Cases_on `guard x y` >| [ 613 `y = 0` by metis_tac[] >> 614 metis_tac[hop_0, loop2_count_0], 615 `y <> 0` by metis_tac[] >> 616 `hop b y = SUC (hop b (y - b))` by rw[hop_suc] >> 617 `_ = SUC (loop2_count guard modify f (f x) (y - b))` by metis_tac[NOT_ZERO] >> 618 `_ = loop2_count guard modify f x y` by metis_tac[loop2_count_suc] >> 619 decide_tac 620 ]); 621 622(* Theorem: FALLING (\x. x - b) *) 623(* Proof: 624 By FALLING, this is to show: !x. x - b <= x, which is true. 625*) 626val decrease_falling = store_thm( 627 "decrease_falling", 628 ``!b. FALLING (\x. x - b)``, 629 simp[]); 630 631(* Theorem: FUNPOW (\x. x - b) n x = x - n * b *) 632(* Proof: 633 Let f = (\x. x - b). 634 By induction on n. 635 Base: !x. FUNPOW f 0 x = x - 0 * b 636 FUNPOW f 0 x 637 = x by FUNPOW_0 638 = x - 0 * b by arithmetic 639 Step: !x. FUNPOW f n x = x - n * b ==> 640 !x. FUNPOW f (SUC n) x = x - SUC n * b 641 FUNPOW f (SUC n) x 642 = f (FUNPOW f n x) by FUNPOW_SUC 643 = f (x - n * b) by induction hypothesis 644 = (x - n * b) - b by function application 645 = x - (SUC n) * b by arithmetic, ADD1 646*) 647val iterating_dec_eqn = store_thm( 648 "iterating_dec_eqn", 649 ``!b n x. FUNPOW (\x. x - b) n x = x - n * b``, 650 strip_tac >> 651 Induct >- 652 rw[] >> 653 rw[FUNPOW_SUC, ADD1]); 654 655(* 656> EVAL ``MAP (\x. x - (hop 2 x) * 2) [1 .. 10]``; = [0; 0; 0; 0; 0; 0; 0; 0; 0; 0]: thm 657> EVAL ``MAP (\x. x - (hop 3 x) * 3) [1 .. 10]``; = [0; 0; 0; 0; 0; 0; 0; 0; 0; 0]: thm 658*) 659 660(* Theorem: 0 < b ==> (FUNPOW (\x. x - b) (hop b x) x = 0) *) 661(* Proof: 662 Let guard = (\x. x = 0), 663 modify = (\x. x - b), 664 R = measure (\x. x). 665 Then WF R by WF_measure 666 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 667 Note hop b x = loop_count guard modify x by hop_eq_loop_count 668 and guard (FUNPOW modify (loop_count guard modify x) x) by loop_count_iterating 669 or FUNPOW modify (loop_count guard modify x) x = 0 by guard 670*) 671val iterating_dec_hop = store_thm( 672 "iterating_dec_hop", 673 ``!b x. 0 < b ==> (FUNPOW (\x. x - b) (hop b x) x = 0)``, 674 rw[hop_eq_loop_count] >> 675 qabbrev_tac `guard = \x. x = 0` >> 676 qabbrev_tac `modify = \x. x - b` >> 677 qabbrev_tac `R = measure (\x. x)` >> 678 `WF R` by rw[Abbr`R`] >> 679 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`modify`, Abbr`R`] >> 680 metis_tac[loop_count_iterating]); 681 682(* Theorem: 0 < b ==> x <= (hop b x) * b *) 683(* Proof: 684 Note FUNPOW (\x. x - b) (hop b x) x = 0 by iterating_dec_hop 685 or x - (hop b x) * b = 0 by iterating_dec_eqn 686 or x <= (hop b x) * b by SUB_EQ_0 687*) 688val iterating_dec_hop_alt = store_thm( 689 "iterating_dec_hop_alt", 690 ``!b x. 0 < b ==> x <= (hop b x) * b``, 691 metis_tac[iterating_dec_hop, iterating_dec_eqn, SUB_EQ_0]); 692 693(* This is the same as hop_exceeds: |- !b n. 0 < b ==> n <= b * hop b n *) 694 695(* ------------------------------------------------------------------------- *) 696(* Decrease Loop *) 697(* ------------------------------------------------------------------------- *) 698 699(* Theorem: 0 < b /\ 700 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 701 !x. loop x = c + SUM (GENLIST (\j. body (x - j * b)) (hop b x)) *) 702(* Proof: 703 Let guard = (\x. x = 0), 704 modify = (\x. x - b), 705 R = measure (\x. x), 706 Then WF R by WF_measure 707 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 708 Let quit = K c, 709 Then !x. loop x = if guard x then quit x else body x + loop (modify x) 710 by given 711 Let f = (\j. body (FUNPOW modify j x)). 712 z = FUNPOW modify (hop b x) x. 713 Then f = (\j. body (x - j * b)) by iterating_dec_eqn, FUN_EQ_THM 714 and z = x - (hop b x) * b by iterating_dec_eqn 715 = 0 by iterating_dec_hop_alt 716 Thus loop x 717 = quit z + SUM (GENLIST f (loop_count guard modify x)) by loop_modify_count_eqn 718 = c + SUM (GENLIST f (hop b x)) by hop_eq_loop_count 719 = c + SUM (GENLIST f (hop b x)) by iterating_dec_hop_alt 720*) 721val loop_dec_count_eqn = store_thm( 722 "loop_dec_count_eqn", 723 ``!loop body b c. 0 < b /\ 724 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 725 !x. loop x = c + SUM (GENLIST (\j. body (x - j * b)) (hop b x))``, 726 rpt strip_tac >> 727 qabbrev_tac `guard = \x. x = 0` >> 728 qabbrev_tac `modify = \x. x - b` >> 729 qabbrev_tac `R = measure (\x. x)` >> 730 `WF R` by rw[Abbr`R`] >> 731 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 732 qabbrev_tac `quit = \x:num. c` >> 733 `!x. loop x = if guard x then quit x else body x + loop (modify x)` by metis_tac[] >> 734 imp_res_tac loop_modify_count_eqn >> 735 first_x_assum (qspec_then `x` strip_assume_tac) >> 736 `loop_count guard modify x = hop b x` by rw[hop_eq_loop_count, Abbr`guard`, Abbr`modify`] >> 737 qabbrev_tac `f1 = \j. body (FUNPOW modify j x)` >> 738 qabbrev_tac `f2 = \j. body (x - j * b)` >> 739 `f1 = f2` by rw[FUN_EQ_THM, iterating_dec_eqn, Abbr`modify`, Abbr`f1`, Abbr`f2`] >> 740 metis_tac[]); 741 742(* Theorem: 0 < b /\ 743 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 744 !x. loop x <= c + SUM (GENLIST (\j. body (x - j * b)) (hop b x)) *) 745(* Proof: 746 Let guard = (\x. x = 0), 747 modify = (\x. x - b), 748 R = measure (\x. x), 749 Then WF R by WF_measure 750 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 751 Let quit = K c, 752 Then !x. loop x = if guard x then quit x else body x + loop (modify x) 753 by given 754 Let f = (\j. body (FUNPOW modify j x)). 755 z = FUNPOW modify (hop b x) x. 756 Then f = (\j. body (x - j * b)) by iterating_dec_eqn, FUN_EQ_THM 757 and z = x - (hop b x) * b by iterating_dec_eqn 758 = 0 by iterating_dec_hop_alt 759 Thus loop x 760 <= quit z + SUM (GENLIST f (loop_count guard modify x)) by loop_modify_count_exit_le 761 = c + SUM (GENLIST f (hop b x)) by hop_eq_loop_count 762*) 763val loop_dec_count_exit_sum_le = store_thm( 764 "loop_dec_count_exit_sum_le", 765 ``!loop body exit b c. 0 < b /\ 766 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 767 !x. loop x <= c + SUM (GENLIST (\j. body (x - j * b)) (hop b x))``, 768 rpt strip_tac >> 769 qabbrev_tac `guard = \x. x = 0` >> 770 qabbrev_tac `modify = \x. x - b` >> 771 qabbrev_tac `R = measure (\x. x)` >> 772 `WF R` by rw[Abbr`R`] >> 773 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 774 qabbrev_tac `quit = \x:num. c` >> 775 `!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)` by metis_tac[] >> 776 imp_res_tac loop_modify_count_exit_le >> 777 first_x_assum (qspec_then `x` strip_assume_tac) >> 778 `loop_count guard modify x = hop b x` by rw[hop_eq_loop_count, Abbr`guard`, Abbr`modify`] >> 779 `quit (FUNPOW modify (loop_count guard modify x) x) = c` by rw[Abbr`quit`] >> 780 qabbrev_tac `f1 = \j. body (FUNPOW modify j x)` >> 781 qabbrev_tac `f2 = \j. body (x - j * b)` >> 782 `f1 = f2` by rw[FUN_EQ_THM, iterating_dec_eqn, Abbr`modify`, Abbr`f1`, Abbr`f2`] >> 783 metis_tac[]); 784 785(* Theorem: 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 786 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 787 !x. loop x <= c + hop b x * cover x *) 788(* Proof: 789 Let guard = (\x. x = 0), 790 modify = (\x. x - b), 791 R = measure (\x. x), 792 Then WF R by WF_measure 793 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 794 and FALLIG modify by decrease_falling 795 Let quit = K c, 796 Then !x. loop x = if guard x then quit x else body x + loop (modify x) 797 by given 798 Let n = loop_count guard modify x, 799 z = FUNPOW modify (hop b x) x. 800 loop x 801 <= quit z + n * cover x by loop_fall_count_cover_exit_le, MONO cover 802 = c + hop b x * cover x by hop_eq_loop_count 803*) 804val loop_dec_count_cover_exit_le = store_thm( 805 "loop_dec_count_cover_exit_le", 806 ``!loop body cover exit b c. 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 807 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 808 !x. loop x <= c + hop b x * cover x``, 809 rpt strip_tac >> 810 qabbrev_tac `guard = \x. x = 0` >> 811 qabbrev_tac `modify = \x. x - b` >> 812 qabbrev_tac `R = measure (\x. x)` >> 813 `WF R` by rw[Abbr`R`] >> 814 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 815 `FALLING modify` by rw[decrease_falling, Abbr`modify`] >> 816 qabbrev_tac `quit = \x:num. c` >> 817 `!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)` by metis_tac[] >> 818 imp_res_tac loop_fall_count_cover_exit_le >> 819 first_x_assum (qspecl_then [`x`, `cover`] strip_assume_tac) >> 820 `loop_count guard modify x = hop b x` by rw[hop_eq_loop_count, Abbr`guard`, Abbr`modify`] >> 821 metis_tac[]); 822 823(* Other similar theorems -- directly *) 824 825(* Theorem: 0 < b /\ MONO body /\ 826 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 827 !x. loop x <= c + hop b x * body x *) 828(* Proof: by loop_dec_count_cover_exit_le with cover = body. *) 829val loop_dec_count_exit_le = store_thm( 830 "loop_dec_count_exit_le", 831 ``!loop body exit b c. 0 < b /\ MONO body /\ 832 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 833 !x. loop x <= c + hop b x * body x``, 834 rpt strip_tac >> 835 `!x. body x <= body x` by rw[] >> 836 imp_res_tac loop_dec_count_cover_exit_le >> 837 first_x_assum (qspec_then `x` strip_assume_tac)); 838 839(* Theorem: 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 840 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 841 !x. loop x <= c + hop b x * cover x *) 842(* Proof: by loop_dec_count_cover_exit_le with exit = F. *) 843val loop_dec_count_cover_le = store_thm( 844 "loop_dec_count_cover_le", 845 ``!loop body cover b c. 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 846 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 847 !x. loop x <= c + hop b x * cover x``, 848 rpt strip_tac >> 849 qabbrev_tac `exit = \x:num. F` >> 850 `!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)` by metis_tac[] >> 851 imp_res_tac loop_dec_count_cover_exit_le >> 852 first_x_assum (qspec_then `x` strip_assume_tac)); 853 854(* Theorem: 0 < b /\ MONO body /\ 855 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 856 !x. loop x <= c + hop b x * body x *) 857(* Proof: by loop_dec_count_cover_le with cover = body. *) 858val loop_dec_count_cover_le = store_thm( 859 "loop_dec_count_cover_le", 860 ``!loop body cover b c. 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 861 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 862 !x. loop x <= c + hop b x * cover x``, 863 rpt strip_tac >> 864 qabbrev_tac `exit = \x:num. F` >> 865 `!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)` by metis_tac[] >> 866 imp_res_tac loop_dec_count_cover_exit_le >> 867 first_x_assum (qspec_then `x` strip_assume_tac)); 868 869(* ------------------------------------------------------------------------- *) 870 871(* Theorem: 0 < b /\ (!x. body x <= cover x) /\ RMONO cover /\ 872 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 873 !x. loop x <= c + hop b x * cover 0 *) 874(* Proof: 875 Let guard = (\x. x = 0), 876 modify = (\x. x - b), 877 R = measure (\x. x), 878 Then WF R by WF_measure 879 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 880 and FALLING modify by decrease_falling 881 Let quit = K c, 882 Then !x. loop x = if guard x then quit x else body x + loop (modify x) 883 by given 884 885 Let n = loop_count guard modify x, 886 z = FUNPOW modify n x. 887 loop x 888 <= quit z + n * cover (FUNPOW modify n x) by loop_fall_count_rcover_exit_le, RMONO cover 889 = c + n * cover (FUNPOW (\x. x - b) n x) by notation 890 = c + n * cover (x - n * b) by iterating_dec_eqn 891 = c + hop b x * cover (x - hop b x * b) by hop_eq_loop_count 892 = c + hop b x * cover 0 by hop_exceeds 893*) 894val loop_dec_count_rcover_exit_le = store_thm( 895 "loop_dec_count_rcover_exit_le", 896 ``!loop body cover exit b c. 0 < b /\ (!x. body x <= cover x) /\ RMONO cover /\ 897 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 898 !x. loop x <= c + hop b x * cover 0``, 899 rpt strip_tac >> 900 qabbrev_tac `guard = \x. x = 0` >> 901 qabbrev_tac `modify = \x. x - b` >> 902 qabbrev_tac `R = measure (\x. x)` >> 903 `WF R` by rw[Abbr`R`] >> 904 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 905 `FALLING modify` by rw[decrease_falling, Abbr`modify`] >> 906 qabbrev_tac `quit = \x:num. c` >> 907 `!x. loop x = if guard x then quit x else body x + if exit x then 0 else loop (modify x)` by metis_tac[] >> 908 imp_res_tac loop_fall_count_rcover_exit_le >> 909 first_x_assum (qspecl_then [`x`, `cover`] strip_assume_tac) >> 910 `loop_count guard modify x = hop b x` by rw[hop_eq_loop_count, Abbr`guard`, Abbr`modify`] >> 911 `loop x <= c + hop b x * cover (FUNPOW modify (hop b x) x)` by metis_tac[] >> 912 `FUNPOW modify (hop b x) x = 0` by rw[GSYM iterating_dec_hop, Abbr`modify`] >> 913 metis_tac[]); 914 915(* Other similar theorems -- directly *) 916 917(* Theorem: 0 < b /\ RMONO body /\ 918 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 919 !x. loop x <= c + hop b x * body 0 *) 920(* Proof: by loop_dec_count_rcover_exit_le with cover = body. *) 921val loop_dec_count_rbody_exit_le = store_thm( 922 "loop_dec_count_rbody_exit_le", 923 ``!loop body exit b c. 0 < b /\ RMONO body /\ 924 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 925 !x. loop x <= c + hop b x * body 0``, 926 rpt strip_tac >> 927 `!x. body x <= body x` by rw[] >> 928 imp_res_tac loop_dec_count_rcover_exit_le >> 929 first_x_assum (qspec_then `x` strip_assume_tac)); 930 931(* Theorem: 0 < b /\ (!x. body x <= cover x) /\ RMONO cover /\ 932 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 933 !x. loop x <= c + hop b x * cover 0 *) 934(* Proof: by loop_dec_count_rcover_exit_le with exit = F. *) 935val loop_dec_count_rcover_le = store_thm( 936 "loop_dec_count_rcover_le", 937 ``!loop body cover b c. 0 < b /\ (!x. body x <= cover x) /\ RMONO cover /\ 938 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 939 !x. loop x <= c + hop b x * cover 0``, 940 rpt strip_tac >> 941 qabbrev_tac `exit = \x:num. F` >> 942 `!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)` by metis_tac[] >> 943 imp_res_tac loop_dec_count_rcover_exit_le >> 944 first_x_assum (qspec_then `x` strip_assume_tac)); 945 946(* Theorem: 0 < b /\ RMONO body /\ 947 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 948 !x. loop x <= c + hop b x * body 0*) 949(* Proof: by loop_dec_count_rcover_le with cover = body. *) 950val loop_dec_count_rbody_le = store_thm( 951 "loop_dec_count_rbody_le", 952 ``!loop body b c. 0 < b /\ RMONO body /\ 953 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 954 !x. loop x <= c + hop b x * body 0``, 955 rpt strip_tac >> 956 `!x. body x <= body x` by rw[] >> 957 imp_res_tac loop_dec_count_rcover_le >> 958 first_x_assum (qspec_then `x` strip_assume_tac)); 959 960(* ------------------------------------------------------------------------- *) 961(* Decrease Loop with Transform *) 962(* ------------------------------------------------------------------------- *) 963 964(* Theorem: 0 < b /\ 965 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 966 !x y. loop x y = quit (FUNPOW f (hop b y) x) + 967 SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) (hop b y)) *) 968(* Proof: 969 Let guard = (\x y. y = 0), 970 modify = (\y. y - b), 971 R = measure (\(x,y). y). 972 Then WF R by WF_measure 973 and !x y. ~guard x y ==> R (f x,modify y) (x,y) by y - b < y, 0 < b 974 Let quit2 = (\x y. quit x). 975 and !x y. loop x y = if guard x y then quit2 x y else body x y + loop (f x) (modify y) 976 by given 977 Let g = \j. body (FUNPOW f j x) (FUNPOW modify j y), 978 n = loop2_count guard modify f x y, 979 p = FUNPOW f n x, 980 q = FUNPOW modify n y. 981 Note n = hop b y by hop_eq_loop2_count 982 so q = 0 by iterating_dec_hop 983 and g = \j. body (FUNPOW f j x) (y - j * b) by iterating_dec_eqn 984 loop x y 985 = quit2 p q + SUM (GENLIST g n) by loop2_modify_count_eqn 986 = quit p 0 + SUM (GENLIST g (hop b y)) by hop_eq_loop2_count 987 = quit (FUNPOW f (hop b y) x) + SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) (hop b y)) 988*) 989val loop2_dec_count_eqn = store_thm( 990 "loop2_dec_count_eqn", 991 ``!loop f body quit b. 0 < b /\ 992 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 993 !x y. loop x y = quit (FUNPOW f (hop b y) x) + 994 SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) (hop b y))``, 995 rpt strip_tac >> 996 imp_res_tac hop_eq_loop2_count >> 997 first_x_assum (qspecl_then [`y`, `x`, `f`] strip_assume_tac) >> 998 qabbrev_tac `guard = \x y. y = 0` >> 999 qabbrev_tac `modify = \y. y - b` >> 1000 qabbrev_tac `R = measure (\(x,y). y)` >> 1001 `WF R` by rw[Abbr`R`] >> 1002 `!x y. ~guard x y ==> R (f x,modify y) (x,y)` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 1003 qabbrev_tac `quit2 = \x y:num. quit x` >> 1004 `!x y. loop x y = if guard x y then quit2 x y else body x y + loop (f x) (modify y)` by metis_tac[] >> 1005 imp_res_tac loop2_modify_count_eqn >> 1006 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 1007 qabbrev_tac `n = loop2_count guard modify f x y` >> 1008 `n = hop b y` by rw[hop_eq_loop2_count, Abbr`n`] >> 1009 qabbrev_tac `u = \j. body (FUNPOW f j x) (FUNPOW modify j y)` >> 1010 qabbrev_tac `v = \j. body (FUNPOW f j x) (y - j * b)` >> 1011 `u = v` by rw[FUN_EQ_THM, iterating_dec_eqn, Abbr`modify`, Abbr`u`, Abbr`v`] >> 1012 metis_tac[]); 1013 1014(* Theorem: 0 < b /\ 1015 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1016 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 1017 SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) (hop b y)) *) 1018(* Proof: 1019 Let guard = (\x y. y = 0), 1020 modify = (\y. y - b), 1021 R = measure (\(x,y). y). 1022 Then WF R by WF_measure 1023 and !x y. ~guard x y ==> R (f x,modify y) (x,y) by y - b < y, 0 < b 1024 Let quit2 = (\x y. quit x). 1025 Thus !x y. loop x y = if guard x y then quit2 x y else body x y + if exit x y then 0 else loop (f x) (modify y) 1026 by given 1027 Let g = \j. body (FUNPOW f j x) (FUNPOW modify j y), 1028 n = loop2_count guard modify f x y, 1029 p = FUNPOW f n x, 1030 q = FUNPOW modify n y. 1031 Note n = hop b y by hop_eq_loop2_count 1032 so q = 0 by iterating_dec_hop 1033 and g = \j. body (FUNPOW f j x) (y - j * b) by iterating_dec_eqn 1034 loop x y 1035 <= quit2 p q + SUM (GENLIST g n) by loop2_modify_count_exit_le 1036 = quit q + SUM (GENLIST g (hop b y)) by bop_eq_loop2_count 1037 = quit (FUNPOW f (hop b y) x) + SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) (hop b y)) 1038*) 1039val loop2_dec_count_sum_le = store_thm( 1040 "loop2_dec_count_sum_le", 1041 ``!loop f body quit exit b. 0 < b /\ 1042 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1043 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + 1044 SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) (hop b y))``, 1045 rpt strip_tac >> 1046 imp_res_tac hop_eq_loop2_count >> 1047 first_x_assum (qspecl_then [`y`, `x`, `f`] strip_assume_tac) >> 1048 qabbrev_tac `guard = \x y. y = 0` >> 1049 qabbrev_tac `modify = \y. y - b` >> 1050 qabbrev_tac `R = measure (\(x,y). y)` >> 1051 `WF R` by rw[Abbr`R`] >> 1052 `!x y. ~guard x y ==> R (f x,modify y) (x,y)` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 1053 qabbrev_tac `quit2 = \x y:num. quit x` >> 1054 `!x y. loop x y = if guard x y then quit2 x y else body x y + if exit x y then 0 else loop (f x) (modify y)` by metis_tac[] >> 1055 imp_res_tac loop2_modify_count_exit_le >> 1056 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 1057 qabbrev_tac `n = loop2_count guard modify f x y` >> 1058 `n = hop b y` by rw[hop_eq_loop2_count, Abbr`n`] >> 1059 qabbrev_tac `u = \j. body (FUNPOW f j x) (FUNPOW modify j y)` >> 1060 qabbrev_tac `v = \j. body (FUNPOW f j x) (y - j * b)` >> 1061 `u = v` by rw[FUN_EQ_THM, iterating_dec_eqn, Abbr`modify`, Abbr`u`, Abbr`v`] >> 1062 metis_tac[]); 1063 1064(* ------------------------------------------------------------------------- *) 1065(* Decreasing Loop with Transform-independent Body *) 1066(* ------------------------------------------------------------------------- *) 1067 1068(* Theorem: 0 < b /\ 1069 (!x y. body x y <= cover x y) /\ (cover = \x y. g y) /\ MONO g /\ 1070 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1071 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g y *) 1072(* Proof: 1073 Let n = hop b y, z = FUNPOW f n x. 1074 loop x y 1075 <= quit z + SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) n) by loop2_dec_count_sum_le 1076 <= quit z + SUM (GENLIST (\j. cover (FUNPOW f j x) (y - j * b)) n) by SUM_LE, body cover 1077 = quit z + SUM (GENLIST (\j. g (y - j * b)) n) by expanding cover 1078 <= quit z + SUM (GENLIST (K (g y)) n) by SUM_LE, MONO g 1079 = quit z + g y * n by SUM_GENLIST_K 1080 = quit z + n * g y by MULT_COMM 1081*) 1082val loop2_dec_count_mono_cover_exit_le = store_thm( 1083 "loop2_dec_count_mono_cover_exit_le", 1084 ``!loop f body quit cover exit b g. 0 < b /\ 1085 (!x y. body x y <= cover x y) /\ (cover = \x y. g y) /\ MONO g /\ 1086 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1087 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g y``, 1088 rpt strip_tac >> 1089 imp_res_tac loop2_dec_count_sum_le >> 1090 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 1091 qabbrev_tac `n = hop b y` >> 1092 `SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) n) <= 1093 SUM (GENLIST (\j. cover (FUNPOW f j x) (y - j * b)) n)` by fs[SUM_LE] >> 1094 `SUM (GENLIST (\j. cover (FUNPOW f j x) (y - j * b)) n) <= SUM (GENLIST (K (g y)) n)` by rw[SUM_LE] >> 1095 `SUM (GENLIST (K (g y)) n) = g y * n` by rw[SUM_GENLIST_K] >> 1096 decide_tac); 1097 1098(* Other similar theorems -- directly *) 1099 1100(* Theorem: 0 < b /\ (body = \x y. g y) /\ MONO g /\ 1101 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1102 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g y *) 1103(* Proof: by loop2_dec_count_mono_cover_exit_le with cover = body. *) 1104val loop2_dec_count_mono_exit_le = store_thm( 1105 "loop2_dec_count_mono_exit_le", 1106 ``!loop f body quit exit b g. 0 < b /\ (body = \x y. g y) /\ MONO g /\ 1107 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1108 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g y``, 1109 rpt strip_tac >> 1110 `!x y. body x y <= body x y` by rw[] >> 1111 imp_res_tac loop2_dec_count_mono_cover_exit_le >> 1112 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1113 1114(* Theorem: 0 < b /\ 1115 (!x y. body x y <= cover x y) /\ (cover = \x y. g y) /\ MONO g /\ 1116 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1117 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g y *) 1118(* Proof: by loop2_dec_count_mono_cover_exit_le with exit = F. *) 1119val loop2_dec_count_mono_cover_le = store_thm( 1120 "loop2_dec_count_mono_cover_le", 1121 ``!loop f body quit cover b g. 0 < b /\ 1122 (!x y. body x y <= cover x y) /\ (cover = \x y. g y) /\ MONO g /\ 1123 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1124 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g y``, 1125 rpt strip_tac >> 1126 qabbrev_tac `exit = \x:'a y:num. F` >> 1127 `!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)` by metis_tac[] >> 1128 imp_res_tac loop2_dec_count_mono_cover_exit_le >> 1129 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1130 1131(* Theorem: 0 < b /\ (body = \x y. g y) /\ MONO g /\ 1132 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1133 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g y *) 1134(* Proof: by loop2_dec_count_mono_cover_le with cover = body. *) 1135val loop2_dec_count_mono_le = store_thm( 1136 "loop2_dec_count_mono_le", 1137 ``!loop f body quit b g. 0 < b /\ (body = \x y. g y) /\ MONO g /\ 1138 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1139 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g y``, 1140 rpt strip_tac >> 1141 `!x y. body x y <= body x y` by rw[] >> 1142 imp_res_tac loop2_dec_count_mono_cover_le >> 1143 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1144 1145(* ------------------------------------------------------------------------- *) 1146 1147(* Theorem: 0 < b /\ 1148 (!x y. body x y <= cover x y) /\ (cover = \x y. g y) /\ RMONO g /\ 1149 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1150 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g 0 *) 1151(* Proof: 1152 Let n = hop b y, z = FUNPOW f n x. 1153 loop x y 1154 <= quit z + SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) n) by loop2_dec_count_sum_le 1155 <= quit z + SUM (GENLIST (\j. cover (FUNPOW f j x) (y - j * b)) n) by SUM_LE, body cover 1156 = quit z + SUM (GENLIST (\j. g (y - j * b)) n) by expanding cover 1157 <= quit z + SUM (GENLIST (K (g 0)) n) by SUM_LE, RMONO g 1158 = quit z + g 0 * n by SUM_GENLIST_K 1159 = quit z + n * g 0 by MULT_COMM 1160*) 1161val loop2_dec_count_rmono_cover_exit_le = store_thm( 1162 "loop2_dec_count_rmono_cover_exit_le", 1163 ``!loop f body quit cover exit b g. 0 < b /\ 1164 (!x y. body x y <= cover x y) /\ (cover = \x y. g y) /\ RMONO g /\ 1165 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1166 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g 0``, 1167 rpt strip_tac >> 1168 imp_res_tac loop2_dec_count_sum_le >> 1169 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 1170 qabbrev_tac `n = hop b y` >> 1171 `SUM (GENLIST (\j. body (FUNPOW f j x) (y - j * b)) n) <= 1172 SUM (GENLIST (\j. cover (FUNPOW f j x) (y - j * b)) n)` by fs[SUM_LE] >> 1173 `SUM (GENLIST (\j. cover (FUNPOW f j x) (y - j * b)) n) <= SUM (GENLIST (K (g 0)) n)` by rw[SUM_LE] >> 1174 `SUM (GENLIST (K (g 0)) n) = g 0 * n` by rw[SUM_GENLIST_K] >> 1175 decide_tac); 1176 1177(* Other similar theorems -- directly *) 1178 1179(* Theorem: 0 < b /\ (body = \x y. g y) /\ RMONO g /\ 1180 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1181 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g 0 *) 1182(* Proof: by loop2_dec_count_rmono_cover_exit_le with cover = body. *) 1183val loop2_dec_count_rmono_exit_le = store_thm( 1184 "loop2_dec_count_rmono_exit_le", 1185 ``!loop f body quit exit b g. 0 < b /\ (body = \x y. g y) /\ RMONO g /\ 1186 (!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1187 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g 0``, 1188 rpt strip_tac >> 1189 `!x y. body x y <= body x y` by rw[] >> 1190 imp_res_tac loop2_dec_count_rmono_cover_exit_le >> 1191 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1192 1193(* Theorem: 0 < b /\ 1194 (!x y. body x y <= cover x y) /\ (cover = \x y. g y) /\ RMONO g /\ 1195 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1196 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g 0 *) 1197(* Proof: by loop2_dec_count_rmono_cover_exit_le with exit = F. *) 1198val loop2_dec_count_rmono_cover_le = store_thm( 1199 "loop2_dec_count_rmono_cover_le", 1200 ``!loop f body quit cover b g. 0 < b /\ 1201 (!x y. body x y <= cover x y) /\ (cover = \x y. g y) /\ RMONO g /\ 1202 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1203 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g 0``, 1204 rpt strip_tac >> 1205 qabbrev_tac `exit = \x:'a y:num. F` >> 1206 `!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)` by metis_tac[] >> 1207 imp_res_tac loop2_dec_count_rmono_cover_exit_le >> 1208 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1209 1210(* Theorem: 0 < b /\ (body = \x y. g y) /\ RMONO g /\ 1211 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1212 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g 0 *) 1213(* Proof: by loop2_dec_count_rmono_cover_le with cover = body. *) 1214val loop2_dec_count_rmono_le = store_thm( 1215 "loop2_dec_count_rmono_le", 1216 ``!loop f body quit b g. 0 < b /\ (body = \x y. g y) /\ RMONO g /\ 1217 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1218 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + (hop b y) * g 0``, 1219 rpt strip_tac >> 1220 `!x y. body x y <= body x y` by rw[] >> 1221 imp_res_tac loop2_dec_count_rmono_cover_le >> 1222 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1223 1224(* ------------------------------------------------------------------------- *) 1225(* Decreasing Loop with Numeric Transform *) 1226(* ------------------------------------------------------------------------- *) 1227 1228(* Theorem: 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ RISING f /\ 1229 (!x y. loop x y = 1230 if y = 0 then quit x 1231 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1232 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover (FUNPOW f (hop b y) x) y *) 1233(* Proof: 1234 Let guard = (\x y. y = 0), 1235 modify = (\y. y - b), 1236 R = measure (\(x,y). y). 1237 Then WF R by WF_measure 1238 and !x y. ~guard x y ==> R (f x,modify y) (x,y) by y - b < y, 0 < b 1239 Let quit2 = (\x y. quit x). 1240 Then !x y. loop x y = if guard x y then quit2 x y else body x y + if exit x y then 0 else loop (f x) (modify y) 1241 by given 1242 and FALLING modify by decrease_falling 1243 Let n = loop2_count guard modify f x y 1244 p = FUNPOW f n x, 1245 q = FUNPOW modify n y. 1246 Note n = hop b y by hop_eq_loop2_count 1247 so q = 0 by iterating_dec_hop 1248 loop x y 1249 <= quit2 p q + n * cover (FUNPOW f n x) y by loop2_rise_fall_count_cover_exit_le 1250 = quit (FUNPOW f (hop b y) x) + (hop b y) * cover (FUNPOW f (hop b y) x) y 1251*) 1252val loop2_dec_rise_count_cover_exit_le = store_thm( 1253 "loop2_dec_rise_count_cover_exit_le", 1254 ``!loop f body quit cover exit b. 1255 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ RISING f /\ 1256 (!x y. loop x y = 1257 if y = 0 then quit x 1258 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1259 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover (FUNPOW f (hop b y) x) y``, 1260 rpt strip_tac >> 1261 assume_tac (hop_eq_loop2_count |> ISPEC ``b:num`` |> ISPEC ``f:num -> num``) >> 1262 first_x_assum (qspecl_then [`x`, `y`] strip_assume_tac) >> 1263 qabbrev_tac `guard = \x:num y. y = 0` >> 1264 qabbrev_tac `modify = \y. y - b` >> 1265 qabbrev_tac `R = measure (\(x:num,y:num). y)` >> 1266 `WF R` by rw[Abbr`R`] >> 1267 `!x y. ~guard x y ==> R (f x,modify y) (x,y)` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 1268 qabbrev_tac `quit2 = \x y:num. quit x` >> 1269 `!x y. loop x y = if guard x y then quit2 x y else body x y + if exit x y then 0 else loop (f x) (modify y)` by metis_tac[] >> 1270 `FALLING modify` by rw[decrease_falling, Abbr`modify`] >> 1271 imp_res_tac loop2_rise_fall_count_cover_exit_le >> 1272 first_x_assum (qspecl_then [`y`, `x`, `cover`] strip_assume_tac) >> 1273 qabbrev_tac `n = loop2_count guard modify f x y` >> 1274 `n = hop b y` by rw[hop_eq_loop2_count, Abbr`n`] >> 1275 metis_tac[]); 1276 1277(* Other similar theorems -- directly *) 1278 1279(* Theorem: 0 < b /\ MONO2 body /\ RISING f /\ 1280 (!x y. loop x y = 1281 if y = 0 then quit x 1282 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1283 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body (FUNPOW f (hop b y) x) y *) 1284(* Proof: by loop2_dec_rise_count_cover_exit_le with cover = body. *) 1285val loop2_dec_rise_count_exit_le = store_thm( 1286 "loop2_dec_rise_count_exit_le", 1287 ``!loop f body quit exit b. 0 < b /\ MONO2 body /\ RISING f /\ 1288 (!x y. loop x y = 1289 if y = 0 then quit x 1290 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1291 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body (FUNPOW f (hop b y) x) y``, 1292 rpt strip_tac >> 1293 `!x y. body x y <= body x y` by rw[] >> 1294 imp_res_tac loop2_dec_rise_count_cover_exit_le >> 1295 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1296 1297(* Theorem: 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ RISING f /\ 1298 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1299 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover (FUNPOW f (hop b y) x) y *) 1300(* Proof: by loop2_dec_rise_count_cover_exit_le with exit = F. *) 1301val loop2_dec_rise_count_cover_le = store_thm( 1302 "loop2_dec_rise_count_cover_le", 1303 ``!loop f body quit cover b. 1304 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ RISING f /\ 1305 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1306 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover (FUNPOW f (hop b y) x) y``, 1307 rpt strip_tac >> 1308 qabbrev_tac `exit = \x:num y:num. F` >> 1309 `!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)` by metis_tac[] >> 1310 imp_res_tac loop2_dec_rise_count_cover_exit_le >> 1311 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1312 1313(* Theorem: 0 < b /\ MONO2 body /\ RISING f /\ 1314 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1315 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body (FUNPOW f (hop b y) x) y *) 1316(* Proof: by loop2_dec_rise_count_cover_le with cover = body. *) 1317val loop2_dec_rise_count_le = store_thm( 1318 "loop2_dec_rise_count_le", 1319 ``!loop f body quit b. 0 < b /\ MONO2 body /\ RISING f /\ 1320 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1321 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body (FUNPOW f (hop b y) x) y``, 1322 rpt strip_tac >> 1323 `!x y. body x y <= body x y` by rw[] >> 1324 imp_res_tac loop2_dec_rise_count_cover_le >> 1325 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1326 1327(* ------------------------------------------------------------------------- *) 1328 1329(* Theorem: 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ FALLING f /\ 1330 (!x y. loop x y = 1331 if y = 0 then quit x 1332 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1333 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover x y *) 1334(* Proof: 1335 Let guard = (\x y. y = 0), 1336 modify = (\y. y - b), 1337 R = measure (\(x,y). y). 1338 Then WF R by WF_measure 1339 and !x y. ~guard x y ==> R (f x,modify y) (x,y) by y - b < y, 0 < b 1340 Let quit2 = (\x y. quit x). 1341 Then !x y. loop x y = if guard x y then quit2 x y else body x y + if exit x y then 0 else loop (f x) (modify y) 1342 by given 1343 and FALLING modify by decrease_falling 1344 Let n = loop2_count guard modify f x y, 1345 p = FUNPOW f n x, 1346 q = FUNPOW modify n y. 1347 Note n = hop b y by hop_eq_loop2_count 1348 so q = 0 by iterating_dec_hop 1349 loop x y 1350 <= quit2 p q + n * cover x y by loop2_fall_fall_count_cover_exit_le 1351 = quit (FUNPOW f (hop b y) x) + (hop b y) * cover x y 1352*) 1353val loop2_dec_fall_count_cover_exit_le = store_thm( 1354 "loop2_dec_fall_count_cover_exit_le", 1355 ``!loop f body quit cover exit b. 1356 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ FALLING f /\ 1357 (!x y. loop x y = 1358 if y = 0 then quit x 1359 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1360 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover x y``, 1361 rpt strip_tac >> 1362 assume_tac (hop_eq_loop2_count |> ISPEC ``b:num`` |> ISPEC ``f:num -> num``) >> 1363 first_x_assum (qspecl_then [`x`, `y`] strip_assume_tac) >> 1364 qabbrev_tac `guard = \x:num y. y = 0` >> 1365 qabbrev_tac `modify = \y. y - b` >> 1366 qabbrev_tac `R = measure (\(x:num,y:num). y)` >> 1367 `WF R` by rw[Abbr`R`] >> 1368 `!x y. ~guard x y ==> R (f x,modify y) (x,y)` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 1369 qabbrev_tac `quit2 = \x y:num. quit x` >> 1370 `!x y. loop x y = if guard x y then quit2 x y else body x y + if exit x y then 0 else loop (f x) (modify y)` by metis_tac[] >> 1371 `FALLING modify` by rw[decrease_falling, Abbr`modify`] >> 1372 assume_tac loop2_fall_fall_count_cover_exit_le >> 1373 first_x_assum (qspecl_then [`loop`, `guard`, `body`, `quit2`, `exit`, `modify`, `f`, `R`] strip_assume_tac) >> 1374 first_x_assum (drule_all_then strip_assume_tac) >> 1375 first_x_assum (qspecl_then [`x`, `y`, `cover`] strip_assume_tac) >> 1376 qabbrev_tac `n = loop2_count guard modify f x y` >> 1377 `n = hop b y` by rw[hop_eq_loop2_count, Abbr`n`] >> 1378 metis_tac[]); 1379 1380(* Other similar theorems -- directly *) 1381 1382(* Theorem: 0 < b /\ MONO2 body /\ FALLING f /\ 1383 (!x y. loop x y = 1384 if y = 0 then quit x 1385 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1386 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body x y *) 1387(* Proof: by loop2_dec_fall_count_cover_exit_le with cover = body. *) 1388val loop2_dec_fall_count_exit_le = store_thm( 1389 "loop2_dec_fall_count_exit_le", 1390 ``!loop f body quit exit b. 0 < b /\ MONO2 body /\ FALLING f /\ 1391 (!x y. loop x y = 1392 if y = 0 then quit x 1393 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1394 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body x y``, 1395 rpt strip_tac >> 1396 `!x y. body x y <= body x y` by rw[] >> 1397 imp_res_tac loop2_dec_fall_count_cover_exit_le >> 1398 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1399 1400(* Theorem: 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ FALLING f /\ 1401 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1402 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover x y *) 1403(* Proof: by loop2_dec_fall_count_cover_exit_le with exit = F. *) 1404val loop2_dec_fall_count_cover_le = store_thm( 1405 "loop2_dec_fall_count_cover_le", 1406 ``!loop f body quit cover b. 1407 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ FALLING f /\ 1408 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1409 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover x y``, 1410 rpt strip_tac >> 1411 qabbrev_tac `exit = \x:num y:num. F` >> 1412 `!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)` by metis_tac[] >> 1413 imp_res_tac loop2_dec_fall_count_cover_exit_le >> 1414 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1415 1416(* Theorem: 0 < b /\ MONO2 body /\ FALLING f /\ 1417 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1418 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body x y *) 1419(* Proof: by loop2_dec_fall_count_cover_le with cover = body. *) 1420val loop2_dec_fall_count_le = store_thm( 1421 "loop2_dec_fall_count_le", 1422 ``!loop f body quit b. 0 < b /\ MONO2 body /\ FALLING f /\ 1423 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1424 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body x y``, 1425 rpt strip_tac >> 1426 `!x y. body x y <= body x y` by rw[] >> 1427 imp_res_tac loop2_dec_fall_count_cover_le >> 1428 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1429 1430(* ------------------------------------------------------------------------- *) 1431(* Decreasing Loop with Transform cover *) 1432(* ------------------------------------------------------------------------- *) 1433 1434(* Theorem: 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ 1435 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 1436 (!x y. loop x y = 1437 if y = 0 then quit x 1438 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1439 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover (FUNPOW g (hop b y) x) y *) 1440(* Proof: 1441 Let n = hop b y, 1442 f1 = (\j. body (FUNPOW f j x) (y - j * b)), 1443 f2 = K (cover (FUNPOW g n x) y). 1444 1445 Claim: SUM (GENLIST f1 n) <= SUM (GENLIST f2 n) 1446 Proof: By SUM_LE, LENGTH_MAP, EL_MAP, 1447 this is to show: k < n ==> 1448 body (FUNPOW f k x) (y - b * k) <= cover (FUNPOW g n x) y 1449 Note y - b * k <= y by arithmetic 1450 Now FUNPOW f k x <= FUNPOW g k x by FUNPOW_LE_MONO, MONO g 1451 and FUNPOW g k x <= FUNPOW g n x by FUNPOW_LE_RISING, k < n, RISING g 1452 Thus body (FUNPOW f k x) (y - b * k) 1453 <= cover (FUNPOW f k x) (y - b * k) by body and cover property 1454 <= cover (FUNPOW g n x) y by MONO2 cover 1455 1456 Let p = FUNPOW f n x. 1457 loop x y 1458 <= quit p + SUM (GENLIST f1 n) by loop2_dec_count_sum_le 1459 <= quit p + SUM (GENLIST f2 n) by claim 1460 = quit p + SUM (GENLIST (K cover (FUNPOW g n x) y) n) by notation 1461 = quit p + n * cover (FUNPOW g n x) by SUM_GENLIST_K 1462 = quit (FUNPOW f (hop b y) x) + (hop b y) * cover (FUNPOW g (hop b y) x) y 1463*) 1464val loop2_dec_mono_count_cover_exit_le = store_thm( 1465 "loop2_dec_mono_count_cover_exit_le", 1466 ``!loop f g body quit cover exit b. 1467 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ 1468 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 1469 (!x y. loop x y = 1470 if y = 0 then quit x 1471 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1472 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover (FUNPOW g (hop b y) x) y``, 1473 rpt strip_tac >> 1474 imp_res_tac loop2_dec_count_sum_le >> 1475 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac) >> 1476 qabbrev_tac `n = hop b y` >> 1477 qabbrev_tac `f1 = \j. body (FUNPOW f j x) (y - j * b)` >> 1478 qabbrev_tac `f2:num -> num = K (cover (FUNPOW g n x) y)` >> 1479 `SUM (GENLIST f1 n) <= SUM (GENLIST f2 n)` by 1480 (irule SUM_LE >> 1481 rw[Abbr`f1`, Abbr`f2`] >> 1482 `y - b * k <= y` by decide_tac >> 1483 `FUNPOW f k x <= FUNPOW g k x` by rw[FUNPOW_LE_MONO] >> 1484 `FUNPOW g k x <= FUNPOW g n x` by rw[FUNPOW_LE_RISING] >> 1485 `FUNPOW f k x <= FUNPOW g n x` by decide_tac >> 1486 `body (FUNPOW f k x) (y - b * k) <= cover (FUNPOW f k x) (y - b * k)` by rw[] >> 1487 `cover (FUNPOW f k x) (y - b * k) <= cover (FUNPOW g n x) y` by rw[] >> 1488 decide_tac) >> 1489 `SUM (GENLIST f2 n) = n * cover (FUNPOW g n x) y` by rw[SUM_GENLIST_K, Abbr`f2`] >> 1490 decide_tac); 1491 1492(* Other similar theorems -- directly *) 1493 1494(* Theorem: 0 < b /\ MONO2 body /\ 1495 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 1496 (!x y. loop x y = 1497 if y = 0 then quit x 1498 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1499 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body (FUNPOW g (hop b y) x) y *) 1500(* Proof: by loop2_dec_mono_count_cover_exit_le with cover = body. *) 1501val loop2_dec_mono_count_exit_le = store_thm( 1502 "loop2_dec_mono_count_exit_le", 1503 ``!loop f g body quit exit b. 0 < b /\ MONO2 body /\ 1504 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 1505 (!x y. loop x y = 1506 if y = 0 then quit x 1507 else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 1508 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body (FUNPOW g (hop b y) x) y``, 1509 rpt strip_tac >> 1510 `!x y. body x y <= body x y` by rw[] >> 1511 imp_res_tac loop2_dec_mono_count_cover_exit_le >> 1512 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1513 1514(* Theorem: 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ 1515 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 1516 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1517 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover (FUNPOW g (hop b y) x) y *) 1518(* Proof: by loop2_dec_mono_count_cover_exit_le with exit = F. *) 1519val loop2_dec_mono_count_cover_le = store_thm( 1520 "loop2_dec_mono_count_cover_le", 1521 ``!loop f g body quit cover b. 1522 0 < b /\ (!x y. body x y <= cover x y) /\ MONO2 cover /\ 1523 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 1524 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1525 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * cover (FUNPOW g (hop b y) x) y``, 1526 rpt strip_tac >> 1527 qabbrev_tac `exit = \x:num y:num. F` >> 1528 `!x y. loop x y = if y = 0 then quit x else body x y + if exit x y then 0 else loop (f x) (y - b)` by metis_tac[] >> 1529 imp_res_tac loop2_dec_mono_count_cover_exit_le >> 1530 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1531 1532(* Theorem: 0 < b /\ MONO2 body /\ 1533 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 1534 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1535 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body (FUNPOW g (hop b y) x) y *) 1536(* Proof: by loop2_dec_mono_count_cover_le with cover = body. *) 1537val loop2_dec_mono_count_le = store_thm( 1538 "loop2_dec_mono_count_le", 1539 ``!loop f g body quit b. 0 < b /\ MONO2 body /\ 1540 (!x. f x <= g x) /\ MONO g /\ RISING g /\ 1541 (!x y. loop x y = if y = 0 then quit x else body x y + loop (f x) (y - b)) ==> 1542 !x y. loop x y <= quit (FUNPOW f (hop b y) x) + hop b y * body (FUNPOW g (hop b y) x) y``, 1543 rpt strip_tac >> 1544 `!x y. body x y <= body x y` by rw[] >> 1545 imp_res_tac loop2_dec_mono_count_cover_le >> 1546 first_x_assum (qspecl_then [`y`, `x`] strip_assume_tac)); 1547 1548(* ------------------------------------------------------------------------- *) 1549(* Original investigation, some with quit = constant. *) 1550(* ------------------------------------------------------------------------- *) 1551 1552(* ------------------------------------------------------------------------- *) 1553(* Decreasing List. *) 1554(* ------------------------------------------------------------------------- *) 1555 1556(* Given a number n, generate a decreasing list of n, down to before 0. *) 1557val decrease_by_def = Define` 1558 decrease_by b n = 1559 if (b = 0) \/ (n = 0) then [] else n::decrease_by b (n - b) 1560`; 1561(* Overload decrease_by 1 *) 1562val _ = overload_on ("decreasing", ``decrease_by 1``); 1563 1564(* 1565EVAL ``decreasing 10``; = [10; 9; 8; 7; 6; 5; 4; 3; 2; 1]: thm 1566*) 1567 1568(* Theorem: (b = 0) \/ (n = 0) ==> (decrease_by b n = []) *) 1569(* Proof: by decrease_by_def *) 1570val decrease_by_nil = store_thm( 1571 "decrease_by_nil", 1572 ``!b n. (b = 0) \/ (n = 0) ==> (decrease_by b n = [])``, 1573 rw[Once decrease_by_def]); 1574 1575(* Theorem: 0 < b /\ 0 < n ==> (decrease_by b n = n::decrease_by b (n - b)) *) 1576(* Proof: by decrease_by_def *) 1577val decrease_by_cons = store_thm( 1578 "decrease_by_cons", 1579 ``!b n. 0 < b /\ 0 < n ==> (decrease_by b n = n::decrease_by b (n - b))``, 1580 rw[Once decrease_by_def]); 1581 1582(* Theorem: decrease_by 0 n = [] *) 1583(* Proof: by decrease_by_def *) 1584val decrease_by_0_n = store_thm( 1585 "decrease_by_0_n", 1586 ``!n. decrease_by 0 n = []``, 1587 rw[Once decrease_by_def]); 1588 1589(* Theorem: decrease_by b 0 = [] *) 1590(* Proof: by decrease_by_def *) 1591val decrease_by_b_0 = store_thm( 1592 "decrease_by_b_0", 1593 ``!b. decrease_by b 0 = []``, 1594 rw[Once decrease_by_def]); 1595 1596(* Theorem: 0 < b /\ n <> 0 ==> (decrease_by b n = n :: decrease_by b (n - b)) *) 1597(* Proof: by decrease_by_def *) 1598val decrease_by_b_nonzero = store_thm( 1599 "decrease_by_b_nonzero", 1600 ``!b n. 0 < b /\ n <> 0 ==> (decrease_by b n = n :: decrease_by b (n - b))``, 1601 rw[Once decrease_by_def]); 1602 1603(* 1604EVAL ``decrease_by 3 10``; = [10; 7; 4; 1]: thm 1605EVAL ``GENLIST (\j. 10 - 3 * j) (hop 3 10)``; = [10; 7; 4; 1]: thm 1606*) 1607 1608(* Theorem: decrease_by b n = GENLIST (\j. n - j * b) (hop b n) *) 1609(* Proof: 1610 Let f = (\j. n - (b + b * j)), g = (\j. n - b * j). 1611 Note f = g o SUC by FUN_EQ_THM 1612 and g 0 = n - 0 = n by arithmetic 1613 By induction from decrease_by_def. 1614 If b = 0 \/ n = 0, 1615 decrease_by b n 1616 = [] by decrease_by_nil 1617 = GENLIST g 0 by GENLIST_0 1618 = GENLIST g (hop b n) by hop_0 1619 Otherwise, b <> 0 /\ n <> 0. 1620 b <> 0 /\ n <> 0 /\ decrease_by b (n - b) = GENLIST f (hop b (n - b)) ==> 1621 decrease_by b n = GENLIST (\j. n - b * j) (hop b n) 1622 1623 decrease_by b n 1624 = n :: decrease_by b (n - b) by decrease_by_cons 1625 = n :: GENLIST f (hop b (n - b)) by induction hypothesis 1626 = g 0 :: GENLIST (g o SUC) (hop b (n - b)) by f = g o SUC, n = g 0 1627 = GENLIST g (SUC (hop b (n - b))) by GENLIST_CONS 1628 = GENLIST g (hop b n) by hop_suc 1629*) 1630val decrease_by_eqn = store_thm( 1631 "decrease_by_eqn", 1632 ``!b n. decrease_by b n = GENLIST (\j. n - j * b) (hop b n)``, 1633 ho_match_mp_tac (theorem "decrease_by_ind") >> 1634 rw[] >> 1635 Cases_on `(b = 0) \/ (n = 0)` >- 1636 metis_tac[hop_0, decrease_by_nil, GENLIST_0] >> 1637 `b <> 0 /\ n <> 0` by decide_tac >> 1638 first_x_assum (drule_all_then strip_assume_tac) >> 1639 rw[Once decrease_by_def] >> 1640 qabbrev_tac `f = \j. n - (b + b * j)` >> 1641 qabbrev_tac `g = \j. n - b * j` >> 1642 `f = g o SUC` by rw[FUN_EQ_THM, ADD1, Abbr`f`, Abbr`g`] >> 1643 `n :: GENLIST f (hop b (n - b)) = g 0 :: GENLIST (g o SUC) (hop b (n - b))` by rw[Abbr`g`] >> 1644 `_ = GENLIST g (SUC (hop b (n - b)))` by rw[GENLIST_CONS] >> 1645 `_ = GENLIST g (hop b n)` by metis_tac[hop_def] >> 1646 rw[]); 1647 1648(* Theorem: 0 < b /\ 0 < n /\ j * b < n ==> MEM (n - j * b) (decrease_by b n) *) 1649(* Proof: 1650 MEM (n - j * b) (decrease_by b n) 1651 <=> MEM (n - j * b) (GENLIST (\j. n - j * b) (hop b n)) by decrease_by_eqn 1652 <=> ?m. m < hop b n /\ n - j * b = n - m * b by MEM_GENLIST 1653 <=> take m = j, with j < hop b n by hop_property 1654*) 1655val decrease_by_member = store_thm( 1656 "decrease_by_member", 1657 ``!b n j. 0 < b /\ 0 < n /\ j * b < n ==> MEM (n - j * b) (decrease_by b n)``, 1658 rw[decrease_by_eqn] >> 1659 rw[MEM_GENLIST] >> 1660 metis_tac[hop_property]); 1661 1662(* Theorem: 0 < b /\ 0 < n ==> MEM n (decrease_by b n) *) 1663(* Proof: put j = 0 in decrease_by_member *) 1664(* Derive a theorem: put j = 0 in decrease_by_member *) 1665val decrease_by_head = save_thm("decrease_by_head", 1666 decrease_by_member |> SPEC ``b:num`` |> SPEC ``n:num`` |> SPEC ``0`` 1667 |> SIMP_RULE (srw_ss()) [] |> GEN ``n:num`` |> GEN ``b:num``); 1668(* val decrease_by_head = |- !b n. 0 < b /\ 0 < n ==> MEM n (decrease_by b n): thm *) 1669 1670(* Theorem: LENGTH (decrease_by b n) = hop b n *) 1671(* Proof: 1672 Let f = (\j. n - j * b). 1673 LENGTH (decrease_by b n) 1674 = LENGTH (GENLIST f (hop b n)) by decrease_by_eqn 1675 = hop b n by LENGTH_GENLIST 1676*) 1677val decrease_by_length = store_thm( 1678 "decrease_by_length", 1679 ``!b n. LENGTH (decrease_by b n) = hop b n``, 1680 rw[decrease_by_eqn, LENGTH_GENLIST]); 1681 1682(* Theorem: j < hop b n ==> (EL j (decrease_by b n) = n - j * b) *) 1683(* Proof: 1684 Let g = (\j. n - j * b). 1685 EL j (decrease_by b n) 1686 = EL j (GENLIST g (hop b n)) by decrease_by_eqn 1687 = g j by EL_GENLIST, j < hop b n 1688 = n - j * b by notation 1689*) 1690val decrease_by_element = store_thm( 1691 "decrease_by_element", 1692 ``!b n j. j < hop b n ==> (EL j (decrease_by b n) = n - j * b)``, 1693 rw[decrease_by_eqn]); 1694 1695(* Theorem: LENGTH (decreasing n) = n *) 1696(* Proof: 1697 LENGTH (decreasing n) 1698 = LENGTH (decrease_by 1 n) by notation 1699 = hop_1_n by decrease_by_length 1700 = n by hop_1_n 1701*) 1702val decreasing_length = store_thm( 1703 "decreasing_length", 1704 ``!n. LENGTH (decreasing n) = n``, 1705 rw[decrease_by_length, hop_1_n]); 1706 1707(* Theorem: decreasing n = REVERSE [1 .. n] *) 1708(* Proof: 1709 decreasing n 1710 = GENLIST (\j. n - j * 1) (hop 1 n) by decrease_by_eqn 1711 = GENLIST (\j. n - j) n by hop_1_n 1712 1713 REVERSE [1 .. n] 1714 = REVERSE (GENLIST (\i. 1 + i) (n + 1 - 1)) by listRangeINC_def 1715 = REVERSE (GENLIST SUC n) by ADD1 1716 = GENLIST (\m. SUC (PRE n - m)) n by REVERSE_GENLIST 1717 = GENLIST (\m. n - m) n by m < n in GENLIST 1718 1719 Thus decreasing n = REVERSE [1 .. n] by GENLIST_EQ 1720*) 1721val decreasing_eqn = store_thm( 1722 "decreasing_eqn", 1723 ``!n. decreasing n = REVERSE [1 .. n]``, 1724 rw[decrease_by_eqn, hop_1_n, listRangeINC_def] >> 1725 rw[REVERSE_GENLIST] >> 1726 irule GENLIST_EQ >> 1727 rw[FUN_EQ_THM]); 1728 1729(* Theorem: 0 < b ==> (decrease_by b x = loop_arg (\x. x = 0) (\x. x - b) x) *) 1730(* Proof: 1731 By induction from decrease_by_def. 1732 Let guard = (\x. x = 0), 1733 modify = (\x. x - b), 1734 R = measure (\x. x). 1735 The goal is: decrease_by b x = loop_arg guard modify x 1736 Then WF R by WF_measure 1737 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 1738 1739 If guard x, 1740 Then x = 0 by guard x 1741 decrease_by b 0 1742 = [] by decrease_by_nil 1743 = loop_arg guard modify 0 by loop_arg_nil 1744 If ~guard x, 1745 Then x <> 0 by ~guard x 1746 decrease_by b x 1747 = x :: decrease_by b (x - b) by decrease_by_cons 1748 = x :: loop_arg guard modify (x - b) by induction hypothesis 1749 = loop_arg guard modify x by loop_arg_cons, ~guard x 1750*) 1751val decrease_by_eq_loop_arg = store_thm( 1752 "decrease_by_eq_loop_arg", 1753 ``!b x. 0 < b ==> (decrease_by b x = loop_arg (\x. x = 0) (\x. x - b) x)``, 1754 ho_match_mp_tac (theorem "decrease_by_ind") >> 1755 rw[] >> 1756 qabbrev_tac `guard = \x. x = 0` >> 1757 qabbrev_tac `modify = \x. x - b` >> 1758 qabbrev_tac `R = measure (\x. x)` >> 1759 `WF R` by rw[Abbr`R`] >> 1760 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`modify`, Abbr`R`] >> 1761 Cases_on `guard x` >| [ 1762 `x = 0` by metis_tac[] >> 1763 metis_tac[decrease_by_nil, loop_arg_nil], 1764 `x <> 0` by metis_tac[] >> 1765 `decrease_by b x = x :: decrease_by b (x - b)` by rw[decrease_by_cons] >> 1766 `_ = x :: loop_arg guard modify (x - b)` by metis_tac[NOT_ZERO] >> 1767 `_ = loop_arg guard modify x` by metis_tac[loop_arg_cons] >> 1768 rw[] 1769 ]); 1770 1771(* Theorem: 0 < b ==> (MAP2 body (iterating f x (hop b y)) (decrease_by b y) = 1772 MAP (UNCURRY body) (loop2_arg (\x y. y = 0) (\y. y - b) f x y)) *) 1773(* Proof: 1774 By induction from decrease_by_def. 1775 Let guard = (\x y. y = 0), 1776 modify = (\y. y - b), 1777 R = measure (\(x,y). y). 1778 Then WF R by WF_measure 1779 and !x y. ~guard x y ==> R (f x,modify y) (x,y) by x - b < x, 0 < b 1780 1781 If guard x y, 1782 Then y = 0 by notation 1783 LHS = MAP2 body (iterating f x (hop b 0)) (decrease_by b 0) 1784 = MAP2 body (iterating f x 0) [] by hop_0, decrease_by_nil 1785 = MAP2 body [] [] by iterating_nil 1786 = [] by MAP2 1787 RHS = MAP (UNCURRY body) (loop2_arg guard modify f x y) 1788 = MAP (UNCURRY body) [] by loop2_arg_nil, guard x y 1789 = [] = LHS by MAP 1790 1791 If ~guard x y, 1792 Then y <> 0 by notation 1793 MAP2 body (iterating f x (hop b y)) (decrease_by b y) 1794 = MAP2 body (iterating f x (SUC (hop b (y - b)))) (y::decrease_by b (y - b)) 1795 by hop_suc, decrease_by_cons 1796 = MAP2 body (x::iterating f (f x) (hop b (y - b))) (y::decrease_by b (y - b)) 1797 by iterating_cons 1798 = body x y::MAP2 body (iterating f (f x) (hop b (y - b))) (decrease_by b (y - b)) 1799 by MAP2 1800 = body x y::MAP (UNCURRY body) (loop2_arg guard modify f (f x) (y - b)) 1801 by induction hypothesis 1802 = MAP (UNCURRY body) ((x,y):: loop2_arg guard modify f (f x) (y - b)) 1803 by MAP, UNCURRY 1804 = MAP (UNCURRY body) (loop2_arg guard modify f x y) 1805 by loop2_arg_cons 1806*) 1807val iterating_decrease_eq_loop2_arg = store_thm( 1808 "iterating_decrease_eq_loop2_arg", 1809 ``!b body f x y. 0 < b ==> 1810 (MAP2 body (iterating f x (hop b y)) (decrease_by b y) = 1811 MAP (UNCURRY body) (loop2_arg (\x y. y = 0) (\y. y - b) f x y))``, 1812 ntac 5 strip_tac >> 1813 qid_spec_tac `x` >> 1814 qid_spec_tac `y` >> 1815 qid_spec_tac `b` >> 1816 ho_match_mp_tac (theorem "decrease_by_ind") >> 1817 rw[] >> 1818 qabbrev_tac `guard = \x y. y = 0` >> 1819 qabbrev_tac `modify = \y. y - b` >> 1820 qabbrev_tac `R = measure (\(x,y). y)` >> 1821 `WF R` by rw[Abbr`R`] >> 1822 `!x y. ~guard x y ==> R (f x,modify y) (x,y)` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 1823 Cases_on `guard x y` >| [ 1824 `y = 0` by metis_tac[] >> 1825 rw[iterating_nil, hop_0, decrease_by_nil] >> 1826 metis_tac[loop2_arg_nil], 1827 `y <> 0` by metis_tac[] >> 1828 rw[iterating_cons, hop_suc, decrease_by_cons] >> 1829 `body x y:: MAP2 body (iterating f (f x) (hop b (modify y))) (decrease_by b (modify y)) = 1830 body x y:: MAP2 body (iterating f (f x) (hop b (y - b))) (decrease_by b (y - b))` by rw[Abbr`modify`] >> 1831 `_ = body x y::MAP (UNCURRY body) (loop2_arg guard modify f (f x) (y - b))` by metis_tac[NOT_ZERO] >> 1832 `_ = MAP (UNCURRY body) ((x,y)::loop2_arg guard modify f (f x) (modify y))` by rw[Abbr`modify`] >> 1833 metis_tac[loop2_arg_cons] 1834 ]); 1835 1836(* ------------------------------------------------------------------------- *) 1837(* Decrease Loop -- original *) 1838(* ------------------------------------------------------------------------- *) 1839 1840(* 1841loop_modify_count_by_sum |> SPEC_ALL |> INST_TYPE [alpha |-> ``:num``] 1842 |> Q.INST [`modify` |-> `(\x. x - b)`, `guard` |-> `(\x. x = 0)`, `R` |-> `measure (\x. x)`] 1843 |> ADD_ASSUM ``0 < b`` |> DISCH_ALL 1844 |> SIMP_RULE (srw_ss()) [GSYM decrease_by_eq_loop_arg]; 1845-- the last one will not work, due to loop being recursive. 1846*) 1847 1848(* Theorem: 0 < b /\ (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 1849 !x. loop x = c + SUM (MAP body (decrease_by b x)) *) 1850(* Proof: 1851 Let guard = (\x. x = 0), 1852 modify = (\x. x - b), 1853 R = measure (\x. x), 1854 Then WF R by WF_measure 1855 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 1856 Also !x. loop x = if guard x then c else body x + loop (modify x) 1857 by given 1858 Thus loop x 1859 = c + SUM (MAP body (loop_arg guard modify x)) by loop_modify_count_by_sum 1860 = c + SUM (MAP body (decrease_by b x)) by decrease_by_eq_loop_arg 1861*) 1862val loop_dec_count_by_sum = store_thm( 1863 "loop_dec_count_by_sum", 1864 ``!loop body b c. 0 < b /\ (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 1865 !x. loop x = c + SUM (MAP body (decrease_by b x))``, 1866 rpt strip_tac >> 1867 qabbrev_tac `guard = \x. x = 0` >> 1868 qabbrev_tac `modify = \x. x - b` >> 1869 qabbrev_tac `R = measure (\x. x)` >> 1870 `WF R` by rw[Abbr`R`] >> 1871 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 1872 `!x. loop x = if guard x then c else body x + loop (modify x)` by metis_tac[] >> 1873 imp_res_tac loop_modify_count_by_sum >> 1874 `loop_arg guard modify x = decrease_by b x` by rw[decrease_by_eq_loop_arg, Abbr`guard`, Abbr`modify`] >> 1875 metis_tac[]); 1876 1877(* Theorem: 0 < b /\ 1878 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 1879 !x. loop x <= c + SUM (MAP body (decrease_by b x)) *) 1880(* Proof: 1881 Let guard = (\x. x = 0), 1882 modify = (\x. x - b), 1883 R = measure (\x. x), 1884 Then WF R by WF_measure 1885 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 1886 Also !x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x) 1887 by given 1888 Thus loop x 1889 <= c + SUM (MAP body (loop_arg guard modify x)) by loop_modify_count_exit_by_sum 1890 = c + SUM (MAP body (decrease_by b x)) by decrease_by_eq_loop_arg 1891*) 1892val loop_dec_count_exit_by_sum = store_thm( 1893 "loop_dec_count_exit_by_sum", 1894 ``!loop body b c exit. 0 < b /\ 1895 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 1896 !x. loop x <= c + SUM (MAP body (decrease_by b x))``, 1897 rpt strip_tac >> 1898 qabbrev_tac `guard = \x. x = 0` >> 1899 qabbrev_tac `modify = \x. x - b` >> 1900 qabbrev_tac `R = measure (\x. x)` >> 1901 `WF R` by rw[Abbr`R`] >> 1902 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 1903 `!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)` by metis_tac[] >> 1904 imp_res_tac loop_modify_count_exit_by_sum >> 1905 `loop_arg guard modify x = decrease_by b x` by rw[decrease_by_eq_loop_arg, Abbr`guard`, Abbr`modify`] >> 1906 metis_tac[]); 1907 1908(* Theorem: 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 1909 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 1910 !x. loop x <= c + cover x * hop b x *) 1911(* Proof: 1912 Let guard = (\x. x = 0), 1913 modify = (\x. x - b), 1914 R = measure (\x. x), 1915 Then WF R by WF_measure 1916 and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b 1917 and !x y. R x y ==> cover x <= cover y by R, LESS_IMP_LESS_OR_EQ, MONO cover 1918 Also !x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x) 1919 by given 1920 loop x 1921 <= c + cover x * loop_count guard modify x by loop_modify_count_cover_exit_upper 1922 = c + cover x * hop b x by hop_eq_loop_count 1923*) 1924val loop_dec_count_cover_exit_upper = store_thm( 1925 "loop_dec_count_cover_exit_upper", 1926 ``!loop body cover exit b c. 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 1927 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 1928 !x. loop x <= c + cover x * hop b x``, 1929 rpt strip_tac >> 1930 qabbrev_tac `guard = \x. x = 0` >> 1931 qabbrev_tac `modify = \x. x - b` >> 1932 qabbrev_tac `R = measure (\x. x)` >> 1933 `WF R` by rw[Abbr`R`] >> 1934 `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 1935 `!x y. R x y ==> cover x <= cover y` by rw[Abbr`R`] >> 1936 `!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)` by metis_tac[] >> 1937 assume_tac (loop_modify_count_cover_exit_upper |> ISPEC ``loop:num -> num``) >> 1938 last_x_assum (qspecl_then [`guard`, `body`, `c`, `cover`, `exit`, `modify`, `R`] strip_assume_tac) >> 1939 `loop_count guard modify x = hop b x` by rw[hop_eq_loop_count, Abbr`guard`, Abbr`modify`] >> 1940 metis_tac[]); 1941 1942(* This is the same, but directly from the SUM *) 1943 1944(* Theorem: 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 1945 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 1946 !x. loop x <= c + cover x * hop b x *) 1947(* Proof: 1948 Let ls = decrease_by b x. 1949 loop x 1950 <= c + SUM (MAP body ls) by loop_dec_count_guard_by_sum 1951 <= SUM (MAP (K (cover n)) ls) by SUM_LE, decrease_by_length, decrease_by_element, MONO cover 1952 = (cover x) * LENGTH ls by SUM_MAP_K 1953 = (cover x) * (hop b x) by decrease_by_length 1954*) 1955val loop_dec_count_cover_exit_upper = store_thm( 1956 "loop_dec_count_cover_exit_upper", 1957 ``!loop body cover exit b c. 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 1958 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 1959 !x. loop x <= c + (cover x) * (hop b x)``, 1960 rpt strip_tac >> 1961 qabbrev_tac `ls = decrease_by b x` >> 1962 `loop x <= c + SUM (MAP body ls)` by metis_tac[loop_dec_count_exit_by_sum] >> 1963 `SUM (MAP body ls) <= SUM (MAP (K (cover x)) ls)` by 1964 (irule SUM_LE >> 1965 rw[decrease_by_length, decrease_by_element, EL_MAP, Abbr`ls`] >> 1966 `body (x - b * k) <= cover (x - b * k)` by rw[] >> 1967 `cover (x - b * k) <= cover x` by rw[] >> 1968 decide_tac) >> 1969 `SUM (MAP (K (cover x)) ls) = (cover x) * LENGTH ls` by rw[SUM_MAP_K] >> 1970 `_ = (cover x) * (hop b x)` by rw[decrease_by_length, Abbr`ls`] >> 1971 decide_tac); 1972 1973(* Theorem: 0 < b /\ MONO body /\ 1974 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 1975 !x. loop x <= c + (body x) * (hop b x) *) 1976(* Proof: by loop_dec_count_cover_exit_upper with cover = body. *) 1977val loop_dec_count_exit_upper = store_thm( 1978 "loop_dec_count_exit_upper", 1979 ``!loop body b c exit. 0 < b /\ MONO body /\ 1980 (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> 1981 !x. loop x <= c + (body x) * (hop b x)``, 1982 metis_tac[loop_dec_count_cover_exit_upper, LESS_EQ_REFL]); 1983 1984(* Theorem: 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 1985 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 1986 !x. loop x <= c + (body x) * (hop b x) *) 1987(* Proof: by loop_dec_count_cover_exit_upper with exit = F. *) 1988val loop_dec_count_cover_upper = store_thm( 1989 "loop_dec_count_cover_upper", 1990 ``!loop body b c cover. 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ 1991 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 1992 !x. loop x <= c + (cover x) * (hop b x)``, 1993 rpt strip_tac >> 1994 qabbrev_tac `exit = (\x:num. F)` >> 1995 metis_tac[loop_dec_count_cover_exit_upper]); 1996 1997(* Theorem: 0 < b /\ MONO body /\ 1998 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 1999 !x. loop x <= c + (body x) * (hop b x) *) 2000(* Proof: by loop_dec_count_cover_upper with body = cover. *) 2001val loop_dec_count_upper = store_thm( 2002 "loop_dec_count_upper", 2003 ``!loop body b c. 0 < b /\ MONO body /\ 2004 (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> 2005 !x. loop x <= c + (body x) * (hop b x)``, 2006 metis_tac[loop_dec_count_cover_upper, LESS_EQ_REFL]); 2007 2008(* ------------------------------------------------------------------------- *) 2009(* Decrease Loop with Transform -- original *) 2010(* ------------------------------------------------------------------------- *) 2011 2012(* Theorem: 0 < b /\ 2013 (!x y. loop x y = if y = 0 then c else body x y + loop (f x) (y - b)) ==> 2014 !x y. loop x y = c + SUM (MAP2 body (iterating f x (hop b y)) (decrease_by b y)) *) 2015(* Proof: 2016 Let guard = (\x y. y = 0), 2017 modify = (\y. y - b), 2018 R = measure (\(x,y). y). 2019 Then WF R by WF_measure 2020 and !x y. ~guard x y ==> R (f x,modify y) (x,y) by x - b < x, 0 < b 2021 and !x y. loop x y = if guard x y then c else body x y + loop (f x) (modify y) by given 2022 loop x y 2023 = c + SUM (MAP (UNCURRY body) (loop2_arg guard modify f x y)) by loop2_modify_count_by_sum 2024 = c + SUM (MAP2 body (iterating f x (hop b y)) (decrease_by b y)) by iterating_decrease_eq_loop2_arg 2025*) 2026val loop2_dec_count_by_sum = store_thm( 2027 "loop2_dec_count_by_sum", 2028 ``!loop f body b c. 0 < b /\ 2029 (!x y. loop x y = if y = 0 then c else body x y + loop (f x) (y - b)) ==> 2030 !x y. loop x y = c + SUM (MAP2 body (iterating f x (hop b y)) (decrease_by b y))``, 2031 rpt strip_tac >> 2032 qabbrev_tac `guard = \x y. y = 0` >> 2033 qabbrev_tac `modify = \y. y - b` >> 2034 qabbrev_tac `R = measure (\(x,y). y)` >> 2035 `WF R` by rw[Abbr`R`] >> 2036 `!x y. ~guard x y ==> R (f x,modify y) (x,y)` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 2037 `!x y. loop x y = if guard x y then c else body x y + loop (f x) (modify y)` by metis_tac[] >> 2038 `loop x y = c + SUM (MAP (UNCURRY body) (loop2_arg guard modify f x y))` by metis_tac[loop2_modify_count_by_sum] >> 2039 `MAP (UNCURRY body) (loop2_arg guard modify f x y) = 2040 MAP2 body (iterating f x (hop b y)) (decrease_by b y)` by rw[iterating_decrease_eq_loop2_arg, Abbr`guard`, Abbr`modify`] >> 2041 metis_tac[]); 2042 2043(* Theorem: 0 < b /\ 2044 (!x y. loop x y = if y = 0 then c else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 2045 !x y. loop x y <= c + SUM (MAP2 body (iterating f x (hop b y)) (decrease_by b y)) *) 2046(* Proof: 2047 Let guard = (\x y. y = 0), 2048 modify = (\y. y - b), 2049 R = measure (\(x,y). y). 2050 Then WF R by WF_measure 2051 and !x y. ~guard x y ==> R (f x,modify y) (x,y) by x - b < x, 0 < b 2052 and !x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (f x) (modify y) 2053 by given 2054 loop x y 2055 <= c + SUM (MAP (UNCURRY body) (loop2_arg guard modify f x y)) by loop2_modify_count_exit_by_sum 2056 = c + SUM (MAP2 body (iterating f x (hop b y)) (decrease_by b y)) by iterating_decrease_eq_loop2_arg 2057*) 2058val loop2_dec_count_exit_by_sum = store_thm( 2059 "loop2_dec_count_exit_by_sum", 2060 ``!loop f body b c exit. 0 < b /\ 2061 (!x y. loop x y = if y = 0 then c else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 2062 !x y. loop x y <= c + SUM (MAP2 body (iterating f x (hop b y)) (decrease_by b y))``, 2063 rpt strip_tac >> 2064 qabbrev_tac `guard = \x y. y = 0` >> 2065 qabbrev_tac `modify = \y. y - b` >> 2066 qabbrev_tac `R = measure (\(x,y). y)` >> 2067 `WF R` by rw[Abbr`R`] >> 2068 `!x y. ~guard x y ==> R (f x,modify y) (x,y)` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 2069 `!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (f x) (modify y)` by metis_tac[] >> 2070 assume_tac (loop2_modify_count_exit_by_sum |> ISPEC ``loop:'a -> num -> num``) >> 2071 last_x_assum (qspecl_then [`guard`, `body`, `c`, `exit`, `modify`, `f`, `R`] strip_assume_tac) >> 2072 `loop x y <= c + SUM (MAP (UNCURRY body) (loop2_arg guard modify f x y))` by metis_tac[] >> 2073 `MAP (UNCURRY body) (loop2_arg guard modify f x y) = 2074 MAP2 body (iterating f x (hop b y)) (decrease_by b y)` by rw[iterating_decrease_eq_loop2_arg, Abbr`guard`, Abbr`modify`] >> 2075 metis_tac[]); 2076 2077(* Theorem: 0 < b /\ (!x y. body x y <= cover x y) /\ 2078 (!x1 x2 y1 y2. y1 <= y2 ==> cover x1 y1 <= cover x2 y2) /\ 2079 (!x y. loop x y = if y = 0 then c else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 2080 !x y. loop x y <= c + cover x y * hop b y *) 2081(* Proof: 2082 Let guard = (\x y. y = 0), 2083 modify = (\y. y - b), 2084 R = measure (\(x,y). y). 2085 Then WF R by WF_measure 2086 and !x y. ~guard x y ==> R (f x,modify y) (x,y) by x - b < x, 0 < b 2087 and !x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> cover x1 y1 <= cover x2 y2 by R 2088 and !x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (f x) (modify y) 2089 by given 2090 loop x y 2091 <= c + cover x y * loop2_count guard modify f x y by loop2_modify_count_bcover_exit_upper 2092 = c + cover x y * hop b y by hop_eq_loop2_count 2093*) 2094val loop2_dec_count_cover_exit_upper = store_thm( 2095 "loop2_dec_count_cover_exit_upper", 2096 ``!loop f body cover exit b c. 0 < b /\ 2097 (!x y. body x y <= cover x y) /\ 2098 (!x1 x2 y1 y2. y1 <= y2 ==> cover x1 y1 <= cover x2 y2) /\ 2099 (!x y. loop x y = if y = 0 then c else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 2100 !x y. loop x y <= c + cover x y * hop b y``, 2101 rpt strip_tac >> 2102 qabbrev_tac `guard = \x y. y = 0` >> 2103 qabbrev_tac `modify = \y. y - b` >> 2104 qabbrev_tac `R = measure (\(x,y). y)` >> 2105 `WF R` by rw[Abbr`R`] >> 2106 `!x y. ~guard x y ==> R (f x,modify y) (x,y)` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> 2107 `!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> cover x1 y1 <= cover x2 y2` by rw[Abbr`R`] >> 2108 `!x y. loop x y = if guard x y then c else body x y + if exit x y then 0 else loop (f x) (modify y)` by metis_tac[] >> 2109 assume_tac (loop2_modify_count_bcover_exit_upper |> ISPEC ``loop:'a -> num -> num``) >> 2110 last_x_assum (qspecl_then [`guard`, `body`, `c`, `exit`, `cover`, `modify`, `f`, `R`] strip_assume_tac) >> 2111 `loop2_count guard modify f x y = hop b y` by rw[hop_eq_loop2_count, Abbr`guard`, Abbr`modify`] >> 2112 metis_tac[]); 2113 2114(* Theorem: 0 < b /\ (!x1 x2 y1 y2. y1 <= y2 ==> body x1 y1 <= body x2 y2) /\ 2115 (!x y. loop x y = if y = 0 then c else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 2116 !x y. loop x y <= c + body x y * hop b y *) 2117(* Proof: by loop2_dec_count_cover_exit_upper, with cover = body. *) 2118val loop2_dec_count_exit_upper = store_thm( 2119 "loop2_dec_count_exit_upper", 2120 ``!loop f body exit b c. 0 < b /\ 2121 (!x1 x2 y1 y2. y1 <= y2 ==> body x1 y1 <= body x2 y2) /\ 2122 (!x y. loop x y = if y = 0 then c else body x y + if exit x y then 0 else loop (f x) (y - b)) ==> 2123 !x y. loop x y <= c + body x y * hop b y``, 2124 rpt strip_tac >> 2125 assume_tac loop2_dec_count_cover_exit_upper >> 2126 last_x_assum (qspecl_then [`loop`, `f`, `body`, `body`, `exit`, `b`, `c`] strip_assume_tac) >> 2127 metis_tac[LESS_EQ_REFL]); 2128 2129(* Theorem: 0 < b /\ (!x y. body x y <= cover x y) /\ 2130 (!x1 x2 y1 y2. y1 <= y2 ==> cover x1 y1 <= cover x2 y2) /\ 2131 (!x y. loop x y = if y = 0 then c else body x y + loop (f x) (y - b)) ==> 2132 !x y. loop x y <= c + cover x y * hop b y *) 2133(* Proof: by loop2_dec_count_cover_exit_upper, with exit = F. *) 2134val loop2_dec_count_cover_upper = store_thm( 2135 "loop2_dec_count_cover_upper", 2136 ``!loop f body cover b c. 0 < b /\ (!x y. body x y <= cover x y) /\ 2137 (!x1 x2 y1 y2. y1 <= y2 ==> cover x1 y1 <= cover x2 y2) /\ 2138 (!x y. loop x y = if y = 0 then c else body x y + loop (f x) (y - b)) ==> 2139 !x y. loop x y <= c + cover x y * hop b y``, 2140 rpt strip_tac >> 2141 qabbrev_tac `exit = \x:'a y:num. F` >> 2142 assume_tac loop2_dec_count_cover_exit_upper >> 2143 last_x_assum (qspecl_then [`loop`, `f`, `body`, `cover`, `exit`, `b`, `c`] strip_assume_tac) >> 2144 metis_tac[]); 2145 2146(* Theorem: 0 < b /\ (!x1 x2 y1 y2. y1 <= y2 ==> body x1 y1 <= body x2 y2) /\ 2147 (!x y. loop x y = if y = 0 then c else body x y + loop (f x) (y - b)) ==> 2148 !x y. loop x y <= c + body x y * hop b y *) 2149(* Proof: loop2_dec_count_cover_upper, with body = cover. *) 2150val loop2_dec_count_upper = store_thm( 2151 "loop2_dec_count_upper", 2152 ``!loop f body b c. 0 < b /\ (!x1 x2 y1 y2. y1 <= y2 ==> body x1 y1 <= body x2 y2) /\ 2153 (!x y. loop x y = if y = 0 then c else body x y + loop (f x) (y - b)) ==> 2154 !x y. loop x y <= c + body x y * hop b y``, 2155 rpt strip_tac >> 2156 assume_tac loop2_dec_count_cover_upper >> 2157 last_x_assum (qspecl_then [`loop`, `f`, `body`, `body`, `b`, `c`] strip_assume_tac) >> 2158 metis_tac[LESS_EQ_REFL]); 2159 2160(* ------------------------------------------------------------------------- *) 2161 2162(* export theory at end *) 2163val _ = export_theory(); 2164 2165(*===========================================================================*) 2166