1(* FILE : tempabs.ml *) 2(* DESCRIPTION : Theory of temporal abstraction for signals. *) 3(* *) 4(* READS FILES : wop.th, next.th, stable.th *) 5(* WRITES FILES : tempabs.th *) 6(* *) 7(* AUTHOR : T. Melham *) 8(* DATE : 85.04.17 *) 9(* *) 10(* PORTED HOL98 : M. Gordon *) 11(* DATE : 00.10.03 *) 12(* MODIFIED : M. Gordon *) 13(* DATE : 02.01.08 *) 14 15 16(* 17load "hol88Lib"; 18load "nextTheory"; 19load "stableTheory"; 20*) 21 22open Globals HolKernel Parse boolLib proofManagerLib; 23open Psyntax; 24open bossLib; 25open arithmeticTheory; 26open prim_recTheory; 27open combinTheory; 28open hol88Lib; 29open pairTheory; 30open numLib; 31open numTheory; 32open nextTheory; 33open stableTheory; 34 35(* Create the new theory, "tempabs.th". *) 36val _ = new_theory "tempabs"; 37 38val SUB_MONO_EQ = 39 store_thm 40 ("SUB_MONO_EQ", 41 ``!n m. (SUC n) - (SUC m) = (n - m)``, 42 DECIDE_TAC); 43 44val SUB_PLUS = 45 store_thm 46 ("SUB_PLUS", 47 ``!a b c. a - (b + c) = (a - b) - c``, 48 DECIDE_TAC); 49 50val INV_PRE_LESS = 51 store_thm 52 ("INV_PRE_LESS", 53 ``!m n. 0 < m /\ 0 < n ==> ((PRE m < PRE n) = (m < n))``, 54 DECIDE_TAC); 55 56val INV_PRE_LESS_EQ = 57 store_thm 58 ("INV_PRE_LESS_EQ", 59 ``!m n. 0 < m /\ 0 < n ==> ((PRE m <= PRE n) = (m <= n))``, 60 DECIDE_TAC); 61 62val SUB_LESS_EQ = 63 store_thm 64 ("SUB_LESS_EQ", 65 ``!n m. (n - m) <= n``, 66 DECIDE_TAC); 67 68val SUB_EQ_EQ_0 = 69 store_thm 70 ("SUB_EQ_EQ_0", 71 ``!m n. (m - n = m) = ((m = 0) \/ (n = 0))``, 72 DECIDE_TAC); 73 74 75(* --------------------------------------------------------------------- *) 76(* Preliminary lemmas, etc. *) 77(* --------------------------------------------------------------------- *) 78 79(* Define a little rule for deriving consequences from WOP. *) 80fun MATCH_WOP_MP th = 81 let val (e,lam) = dest_comb (concl th) 82 val wop_spec = SPEC lam WOP 83 in 84 MP (REWRITE_RULE [BETA_CONV ``^lam ^(fst(dest_abs lam))``] wop_spec) th 85 end; 86 87(* Prove that a non-empty bounded subset of P has a greatest element. *) 88val Bounded = 89 TAC_PROOF(([],``!n. (?m. P(m) /\ m < n) ==> 90 (?m. P(m) /\ m < n /\ !i. m<i /\ i<n ==> ~P(i))``), 91 REPEAT STRIP_TAC THEN 92 POP_ASSUM (STRIP_THM_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN 93 REWRITE_TAC [ADD_CLAUSES,num_CONV ``1``] THEN 94 SPEC_TAC (``p:num``,``p:num``) THEN 95 INDUCT_TAC THENL 96 [EXISTS_TAC ``m:num`` THEN 97 ASM_REWRITE_TAC [ADD_CLAUSES,LESS_SUC_REFL,LESS_LESS_SUC], 98 POP_ASSUM STRIP_ASSUME_TAC THEN 99 ASM_CASES_TAC ``P(SUC(m+p)):bool`` THENL 100 [EXISTS_TAC ``SUC(m+p)`` THEN 101 ASM_REWRITE_TAC[LESS_SUC_REFL,LESS_LESS_SUC,ADD_CLAUSES], 102 EXISTS_TAC ``m':num`` THEN 103 IMP_RES_TAC LESS_SUC THEN 104 ASM_REWRITE_TAC[ADD_CLAUSES] THEN 105 CONV_TAC (DEPTH_CONV ANTE_CONJ_CONV) THEN 106 GEN_TAC THEN DISCH_TAC THEN 107 DISCH_THEN 108 (STRIP_ASSUME_TAC o 109 MATCH_MP (fst(EQ_IMP_RULE (SPEC_ALL LESS_THM)))) THENL 110 [ASM_REWRITE_TAC[],RES_TAC]]]); 111 112(* less_lemma = |- m < (SUC n) = m <= n *) 113val less_lemma = 114 REWRITE_RULE [SYM(SPEC_ALL ADD1)] 115 (REWRITE_RULE [ADD1,LESS_EQ_MONO_ADD_EQ] 116 (SPECL [``m:num``,``SUC n``] LESS_EQ)); 117 118(* --------------------------------------------------------------------- *) 119(* DEFINITIONS *) 120(* --------------------------------------------------------------------- *) 121 122(* Define the relation Istimeof. *) 123(* Istimeof n sig t <==> "t" is the time of the "n"th high value of "sig"*) 124(* i.e. sig is high for the nth time at time t. *) 125val Istimeof = new_recursive_definition 126 {name = "Istimeof", 127 def = ``(Istimeof 0 sig t = (sig t /\ !t'. t'<t ==> ~sig t')) /\ 128 (Istimeof (SUC n) sig t = 129 ?t'.(Istimeof n sig t') /\ Next t' t sig)``, 130 rec_axiom = num_Axiom} 131 132(* Timeof n sig = the time of the nth occurence of a high value on sig. *) 133val Timeof = 134 new_definition 135 ("Timeof", ``!n sig. Timeof sig n = @t. Istimeof n sig t``); 136 137(* Inf(sig) = the signal, "sig", is high infinitely often. *) 138val Inf = new_definition("Inf", ``!sig. Inf sig = !t. ?t'. t<t' /\ sig(t')``); 139 140(* Incr(f) = the function, ``f``, is increasing. *) 141val Incr = new_definition("Incr", ``!f. Incr f = !n m. n<m ==> f(n) < f(m)``); 142 143(* Define the abstraction function, ``when``. *) 144val when = 145 new_definition 146 ("when",``!cntl sig. $when sig cntl= sig o (Timeof cntl)``); 147 148val _ = set_fixity "when" (Infixl 350); 149 150(* --------------------------------------------------------------------- *) 151(* Theorems about Inf. *) 152(* --------------------------------------------------------------------- *) 153 154(* Prove that Inf could be alternatively defined as follows: *) 155Theorem Inf_thm1: 156 !sig. Inf(sig) <=> (?t.sig(t)) /\ (!t. sig t ==> ?t'. t < t' /\ sig t') 157Proof 158 REWRITE_TAC [Inf] THEN GEN_TAC THEN EQ_TAC THENL 159 [REPEAT STRIP_TAC THENL 160 [POP_ASSUM (STRIP_ASSUME_TAC o SPEC_ALL) THEN 161 EXISTS_TAC ``t':num`` THEN FIRST_ASSUM ACCEPT_TAC, 162 FIRST_ASSUM MATCH_ACCEPT_TAC], 163 STRIP_TAC THEN 164 INDUCT_TAC THENL 165 [REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC 166 (SPEC ``t:num`` num_CASES) THENL 167 [RES_TAC, 168 EXISTS_TAC ``SUC n`` THEN ASM_REWRITE_TAC [LESS_0]] 169 THEN PROVE_TAC[], 170 POP_ASSUM STRIP_ASSUME_TAC 171 THEN RES_TAC 172 THEN IMP_RES_TAC(DECIDE``t' < t'' ==> t'' < t''' ==> SUC t' < t'''``) 173 THEN PROVE_TAC[]]] 174QED 175 176(* Prove that Inf could be alternatively defined as follows: *) 177val Inf_thm2 = 178 store_thm("Inf_thm2", 179 ``!sig. Inf sig = !t. ?t'. t<=t' /\ sig(t')``, 180 REWRITE_TAC [Inf,LESS_OR_EQ] THEN 181 REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL 182 [POP_ASSUM (STRIP_ASSUME_TAC o SPEC ``t:num``) THEN 183 EXISTS_TAC ``t':num`` THEN 184 ASM_REWRITE_TAC[], 185 POP_ASSUM (STRIP_ASSUME_TAC o SPEC ``SUC t``) THENL 186 [IMP_RES_TAC SUC_LESS THEN 187 EXISTS_TAC ``t':num`` THEN ASM_REWRITE_TAC[], 188 EXISTS_TAC ``t':num`` THEN 189 ASM_REWRITE_TAC [LESS_EQ,LESS_EQ_REFL]]]); 190 191(* Conditions for ~Inf(sig) *) 192Theorem Not_Inf: 193 !sig. (~Inf(sig)) <=> 194 (!t.~sig(t)) \/ (?t. sig t /\ !t'. t < t' ==> ~sig t') 195Proof 196 REWRITE_TAC [Inf_thm1,IMP_DISJ_THM,DE_MORGAN_THM] THEN 197 CONV_TAC 198 (REDEPTH_CONV (NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV)) THEN 199 REWRITE_TAC [DE_MORGAN_THM] THEN 200 CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) THEN 201 REWRITE_TAC [DE_MORGAN_THM] 202QED 203 204(* --------------------------------------------------------------------- *) 205(* THEOREMS about Istimeof *) 206(* --------------------------------------------------------------------- *) 207 208(* Proof that |- sig (t) = ?n. Istimeof n sig t. We first prove the *) 209(* following lemma: *) 210val n_exists_lemma = 211 TAC_PROOF(([], ``!sig t t'. sig(t') /\ t'<=t ==> ?n. Istimeof n sig t'``), 212 GEN_TAC THEN 213 INDUCT_TAC THENL 214 [REWRITE_TAC [NOT_LESS_0,LESS_OR_EQ] THEN 215 REPEAT STRIP_TAC THEN EXISTS_TAC ``0`` THEN 216 ASM_REWRITE_TAC [Istimeof,NOT_LESS_0], 217 REWRITE_TAC [LESS_THM,LESS_OR_EQ] THEN 218 REWRITE_TAC [SYM(SPEC_ALL(CONV_RULE(ONCE_DEPTH_CONV 219 (REWR_CONV DISJ_SYM)) LESS_OR_EQ))] THEN 220 REPEAT STRIP_TAC THENL 221 [RES_TAC, 222 POP_ASSUM SUBST_ALL_TAC THEN 223 ASM_CASES_TAC ``?t'.sig(t') /\ t'<(SUC t)`` THENL 224 [POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [less_lemma] o 225 MATCH_MP Bounded) THEN 226 RES_TAC THEN 227 POP_ASSUM STRIP_ASSUME_TAC THEN 228 EXISTS_TAC ``SUC n'`` THEN 229 ASM_REWRITE_TAC [Istimeof,Next] THEN 230 EXISTS_TAC ``m:num`` THEN 231 ASM_REWRITE_TAC[less_lemma], 232 POP_ASSUM (ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV) THEN 233 EXISTS_TAC ``0`` THEN 234 ASM_REWRITE_TAC [Istimeof] THEN 235 REPEAT STRIP_TAC THEN 236 RES_TAC]]] THEN PROVE_TAC[]); 237 238(* We now show that |- !sig t. sig t ==> (?n. Istimeof n sig t). *) 239(* I.e., whenever sig is true at some time t, there exists an n such *) 240(* that n is the nth time sig is true. *) 241val Istimeof_thm1 = 242 save_thm("Istimeof_thm1", 243 GEN_ALL(REWRITE_RULE [LESS_EQ_REFL] 244 (SPECL [``sig:num->bool``,``t:num``,``t:num``] n_exists_lemma))); 245 246(* We now show that if (Istimeof n sig t) holds then sig(t). *) 247val Istimeof_thm2 = 248 store_thm 249 ("Istimeof_thm2", 250 ``!sig t. (?n. Istimeof n sig t) ==> sig t``, 251 REPEAT STRIP_TAC THEN 252 POP_ASSUM MP_TAC THEN 253 (REPEAT_TCL STRIP_THM_THEN) SUBST1_TAC (SPEC ``n:num`` num_CASES) THEN 254 REWRITE_TAC [Istimeof,Next] THEN 255 STRIP_TAC); 256 257(* There is an n such that Istimeof n sig t only if sig(t). *) 258val Istimeof_thm3 = 259 store_thm("Istimeof_thm3", 260 ``!sig t. sig t = ?n. Istimeof n sig t``, 261 PROVE_TAC[Istimeof_thm1,Istimeof_thm2]); 262 263(* If sig is true infinitely often, then, for any n, there always exists *) 264(* a time t such that sig is true for the nth time at time t. *) 265(* *) 266(* I.e. Inf(sig) ==> !n.?t.Istimeof n sig t *) 267(* *) 268(* This will be proven by induction on n. *) 269val Istimeof_thm4 = 270 store_thm("Istimeof_thm4", 271 ``!sig. Inf(sig) ==> !n.?t.Istimeof n sig t``, 272 PURE_REWRITE_TAC [Inf] THEN 273 REPEAT (FILTER_STRIP_TAC ``n:num``) THEN 274 INDUCT_TAC THEN 275 REWRITE_TAC [Istimeof] THENL 276 [MATCH_MP_TAC WOP THEN 277 POP_ASSUM (STRIP_ASSUME_TAC o SPEC_ALL) THEN 278 EXISTS_TAC ``t':num`` THEN FIRST_ASSUM ACCEPT_TAC, 279 POP_ASSUM STRIP_ASSUME_TAC THEN 280 CONV_TAC SWAP_EXISTS_CONV THEN 281 EXISTS_TAC ``t:num`` THEN 282 POP_ASSUM (fn th => REWRITE_TAC [th,Next]) THEN 283 POP_ASSUM (STRIP_ASSUME_TAC o MATCH_WOP_MP o SPEC_ALL) THEN 284 EXISTS_TAC ``n:num`` THEN 285 ASM_REWRITE_TAC[] THEN 286 REPEAT STRIP_TAC THEN RES_TAC THEN RES_TAC]); 287 288(* Istimeof defines a Unique time: *) 289(* Istimeof n sig t /\ Istimeof n sig t' ==> (t=t') *) 290val Istimeof_thm5 = 291 store_thm("Istimeof_thm5", 292 ``!n sig t t'.Istimeof n sig t /\ Istimeof n sig t' ==> (t=t')``, 293 INDUCT_TAC THEN 294 REWRITE_TAC [Istimeof] THENL 295 [CONV_TAC (ONCE_DEPTH_CONV (CONTRAPOS_CONV)) THEN 296 REPEAT STRIP_TAC THEN 297 ASM_CASES_TAC ``t < t'`` THENL 298 [RES_TAC,IMP_RES_TAC LESS_CASES_IMP THEN RES_TAC], 299 REPEAT STRIP_TAC THEN 300 RES_TAC THEN REPEAT (POP_ASSUM SUBST_ALL_TAC) THEN 301 IMP_RES_TAC Next_Unique]); 302 303(* If there is always a time when sig is true for the nth time, then sig *) 304(* is true infinitely often. *) 305val Istimeof_thm6 = 306 store_thm 307 ("Istimeof_thm6", 308 ``!sig. (!n.?t.Istimeof n sig t) ==> Inf sig``, 309 CONV_TAC (ONCE_DEPTH_CONV CONTRAPOS_CONV) THEN 310 CONV_TAC (REDEPTH_CONV (NOT_FORALL_CONV ORELSEC NOT_EXISTS_CONV)) THEN 311 REWRITE_TAC [Not_Inf] THEN 312 REPEAT STRIP_TAC THENL 313 [EXISTS_TAC ``0`` THEN ASM_REWRITE_TAC [Istimeof], 314 IMP_RES_THEN STRIP_ASSUME_TAC Istimeof_thm1 THEN 315 EXISTS_TAC ``SUC n`` THEN REWRITE_TAC [Istimeof,Next] THEN 316 CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) THEN 317 REWRITE_TAC [DE_MORGAN_THM,SYM(SPEC_ALL IMP_DISJ_THM)] THEN 318 REPEAT STRIP_TAC THEN 319 IMP_RES_TAC Istimeof_thm5 THEN 320 REPEAT (POP_ASSUM SUBST_ALL_TAC) THEN 321 RES_TAC]); 322 323(* Inf sig iff there is always an nth time sig is true. *) 324val Istimeof_thm7 = 325 store_thm("Istimeof_thm7", 326 ``!sig. Inf(sig) = !n. ?t. Istimeof n sig t``, 327 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL 328 [IMP_RES_TAC Istimeof_thm4, IMP_RES_TAC Istimeof_thm6]); 329 330(* --------------------------------------------------------------------- *) 331(* THEOREMS about Timeof *) 332(* --------------------------------------------------------------------- *) 333 334(* We prove the theorem relating Timeof and Next: *) 335(* ``!sig. Inf(sig) ==> !n. Next (Timeof n sig) (Timeof (n+1) sig) sig`` *) 336val Timeof_thm1 = 337 store_thm 338 ("Timeof_thm1", 339 ``!sig. Inf(sig) ==> !n. Next (Timeof sig n) (Timeof sig (SUC n)) sig``, 340 REPEAT STRIP_TAC THEN 341 REWRITE_TAC [Timeof,Istimeof] THEN 342 IMP_RES_THEN 343 (ASSUME_TAC o SELECT_RULE o (SPEC ``SUC n``)) Istimeof_thm4 THEN 344 POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE[Istimeof]) THEN 345 FIRST_ASSUM 346 (fn th => ASSUME_TAC 347 (EXISTS (``?t'.Istimeof n sig t'``,``t':num``) th) ORELSE NO_TAC) THEN 348 POP_ASSUM (ASSUME_TAC o SELECT_RULE) THEN 349 POP_ASSUM 350 (ASSUME_TAC o GEN_ALL o (MATCH_MP (hd(RES_CANON Istimeof_thm5)))) THEN 351 RES_THEN SUBST1_TAC THEN 352 FIRST_ASSUM ACCEPT_TAC); 353 354val Timeof_thm2 = 355 store_thm 356 ("Timeof_thm2", 357 ``!sig. Inf(sig) ==> !n. (Timeof sig n) < (Timeof sig (SUC n))``, 358 REPEAT STRIP_TAC THEN 359 IMP_RES_THEN MP_TAC Timeof_thm1 THEN 360 REWRITE_TAC [Next] THEN 361 DISCH_THEN (STRIP_ASSUME_TAC o SPEC ``n:num``) THEN 362 FIRST_ASSUM ACCEPT_TAC); 363 364val Timeof_thm3 = 365 store_thm 366 ("Timeof_thm3", 367 ``!sig. Inf(sig) ==> 368 !n t. ((Timeof sig n) < t /\ t < (Timeof sig (SUC n))) ==> ~sig t``, 369 REPEAT STRIP_TAC THEN 370 IMP_RES_THEN MP_TAC Timeof_thm1 THEN 371 REWRITE_TAC [Next] THEN 372 DISCH_THEN (STRIP_ASSUME_TAC o SPEC ``n:num``) THEN 373 RES_TAC); 374 375(* Also prove that: Inf(sig) ==> sig(Timeof n sig) *) 376val Timeof_thm4 = 377 store_thm 378 ("Timeof_thm4", 379 ``!sig. Inf(sig) ==> !n. sig(Timeof sig n)``, 380 REPEAT STRIP_TAC THEN 381 REWRITE_TAC [Timeof] THEN 382 IMP_RES_THEN (MP_TAC o SELECT_RULE o SPEC_ALL) Istimeof_thm4 THEN 383 STRIP_ASSUME_TAC (SPEC ``n:num`` num_CASES) THEN 384 ASM_REWRITE_TAC [Istimeof,Next] THEN 385 REPEAT STRIP_TAC); 386 387val Timeof_thm5 = 388 store_thm 389 ("Timeof_thm5", 390 ``!sig t. sig(t) ==> ?n. t = Timeof sig n``, 391 REPEAT STRIP_TAC THEN 392 IMP_RES_THEN STRIP_ASSUME_TAC Istimeof_thm1 THEN 393 EXISTS_TAC ``n:num`` THEN 394 ASSUME_TAC (SELECT_RULE (EXISTS (``?t.Istimeof n sig t``,``t:num``) 395 (ASSUME ``Istimeof n sig t``))) THEN 396 REWRITE_TAC [Timeof] THEN 397 IMP_RES_TAC Istimeof_thm5); 398 399 400val Timeof_thm6 = 401 store_thm 402 ("Timeof_thm6", 403 ``!sig. Inf sig ==> !t. 0 < (Timeof sig (SUC t) - Timeof sig t)``, 404 REPEAT STRIP_TAC THEN 405 IMP_RES_THEN 406 (STRIP_THM_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1 o SPEC ``t:num``) 407 Timeof_thm2 THEN 408 REWRITE_TAC [ADD_ASSOC,num_CONV ``1``,ADD_CLAUSES,SUB] THEN 409 REWRITE_TAC [REWRITE_RULE[SYM(SPEC_ALL NOT_LESS)] LESS_EQ_ADD] THEN 410 REWRITE_TAC [LESS_0]); 411 412val Timeof_thm7 = 413 store_thm 414 ("Timeof_thm7", 415 ``!c. Inf c ==> !t. (Timeof c (SUC t) - 1) < Timeof c (SUC t)``, 416 REPEAT STRIP_TAC THEN 417 STRIP_ASSUME_TAC (SPECL [``Timeof c (SUC t)``,``1``] SUB_LESS_EQ) THEN 418 POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [LESS_OR_EQ]) THEN 419 POP_ASSUM 420 (ASSUME_TAC o REWRITE_RULE [SUB_EQ_EQ_0,num_CONV ``1``,NOT_SUC]) THEN 421 IMP_RES_THEN (MP_TAC o SPEC ``t:num``) Timeof_thm2 THEN 422 ASM_REWRITE_TAC [NOT_LESS_0]); 423 424 425(* --------------------------------------------------------------------- *) 426(* THEOREMS about Incr *) 427(* --------------------------------------------------------------------- *) 428 429(* A little lemma about Incr. *) 430val Incr_lemma1 = 431 TAC_PROOF(([], ``!f. Incr(f) ==> !n. n <= f(n)``), 432 PURE_REWRITE_TAC [Incr] THEN 433 GEN_TAC THEN 434 CONV_TAC CONTRAPOS_CONV THEN 435 DISCH_THEN (ASSUME_TAC o (CONV_RULE NOT_FORALL_CONV)) THEN 436 POP_ASSUM 437 (STRIP_ASSUME_TAC o 438 REWRITE_RULE [SYM(SPEC_ALL NOT_LESS)] o MATCH_WOP_MP) THEN 439 STRIP_TAC THEN RES_TAC); 440 441(* Another lemma about Incr. *) 442val Incr_lemma2 = 443 TAC_PROOF(([], ``!f. Incr(f) ==> !n. n < f(SUC n)``), 444 REPEAT STRIP_TAC THEN 445 IMP_RES_TAC Incr_lemma1 THEN 446 POP_ASSUM (STRIP_ASSUME_TAC o 447 REWRITE_RULE [LESS_OR_EQ] o SPEC ``SUC n``) THENL 448 [ASSUME_TAC (SPEC ``n:num`` LESS_SUC_REFL) THEN 449 IMP_RES_TAC LESS_TRANS, 450 POP_ASSUM (SUBST1_TAC o SYM) THEN 451 MATCH_ACCEPT_TAC LESS_SUC_REFL]); 452 453(* A lemma relating Incr and Inf. *) 454val Incr_lemma3 = 455 TAC_PROOF(([], ``!f. Incr(f) ==> Inf(\n.?m. n = f m)``), 456 PURE_REWRITE_TAC [Inf] THEN 457 CONV_TAC (DEPTH_CONV BETA_CONV) THEN 458 REPEAT STRIP_TAC THEN 459 IMP_RES_THEN (STRIP_ASSUME_TAC o SPEC ``t:num``) Incr_lemma2 THEN 460 EXISTS_TAC ``f (SUC t):num`` THEN 461 ASM_REWRITE_TAC [] THEN 462 EXISTS_TAC ``SUC t`` THEN REFL_TAC);; 463 464val LESS_SUC_EQ = DECIDE ``m < n ==> SUC m < n \/ (SUC m = n)``; 465 466(* A lemma concerning Incr and Istimeof. *) 467val Istimeof_lemma = 468 TAC_PROOF(([], ``Incr(f) ==> !n. Istimeof n (\n.?m. n = f m) (f n)``), 469 REWRITE_TAC [Incr] THEN 470 DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC [Istimeof] THEN 471 CONV_TAC (DEPTH_CONV BETA_CONV) THENL 472 [CONJ_TAC THENL 473 [EXISTS_TAC ``0`` THEN REFL_TAC, 474 REPEAT STRIP_TAC THEN 475 POP_ASSUM SUBST_ALL_TAC THEN 476 STRIP_ASSUME_TAC (SPEC ``m:num`` LESS_0_CASES) THENL 477 [POP_ASSUM (SUBST_ALL_TAC o SYM) THEN IMP_RES_TAC LESS_REFL, 478 RES_TAC THEN IMP_RES_TAC LESS_ANTISYM]], 479 EXISTS_TAC ``(f:num->num) n`` THEN 480 ASM_REWRITE_TAC[Next] THEN 481 CONV_TAC (DEPTH_CONV BETA_CONV) THEN 482 REPEAT STRIP_TAC THENL 483 [ANTE_RES_THEN ACCEPT_TAC (SPEC ``n:num`` LESS_SUC_REFL), 484 EXISTS_TAC ``SUC n`` THEN REFL_TAC, 485 POP_ASSUM SUBST_ALL_TAC THEN 486 STRIP_ASSUME_TAC 487 (SPEC_ALL (REWRITE_RULE [LESS_OR_EQ] LESS_CASES)) THENL 488 [RES_TAC THEN IMP_RES_TAC LESS_ANTISYM, 489 POP_ASSUM (STRIP_ASSUME_TAC o 490 (MATCH_MP (REWRITE_RULE [LESS_OR_EQ] LESS_SUC_EQ))) THENL 491 [RES_TAC THEN IMP_RES_TAC LESS_ANTISYM, 492 POP_ASSUM SUBST_ALL_TAC THEN IMP_RES_TAC LESS_REFL], 493 POP_ASSUM SUBST_ALL_TAC THEN IMP_RES_TAC LESS_REFL]]]); 494 495(* --------------------------------------------------------------------- *) 496(* A theorem relating Incr, Inf and Timeof. *) 497(* --------------------------------------------------------------------- *) 498 499val Incr_Inf_thm = 500 store_thm("Incr_Inf_thm", 501 ``!f.Incr f = ?g. Inf(g) /\ (f = Timeof g)``, 502 REPEAT (FIRST [STRIP_TAC, EQ_TAC]) THENL 503 [EXISTS_TAC ``\n:num.?m:num. n = f m`` THEN 504 CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN 505 IMP_RES_TAC Incr_lemma3 THEN 506 ASM_REWRITE_TAC[Timeof] THEN 507 GEN_TAC THEN 508 IMP_RES_THEN 509 (ASSUME_TAC o SELECT_RULE o SPEC ``n:num``) Istimeof_thm4 THEN 510 IMP_RES_THEN 511 (ASSUME_TAC o SPEC ``n:num``) Istimeof_lemma THEN 512 IMP_RES_TAC Istimeof_thm5, 513 POP_ASSUM SUBST1_TAC THEN 514 PURE_REWRITE_TAC [Incr] THEN 515 REPEAT GEN_TAC THEN 516 DISCH_THEN 517 (STRIP_THM_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) THEN 518 PURE_REWRITE_TAC [num_CONV ``1``,ADD_CLAUSES] THEN 519 SPEC_TAC (``p:num``,``p:num``) THEN 520 INDUCT_TAC THENL 521 [REWRITE_TAC [ADD_CLAUSES] THEN 522 IMP_RES_THEN 523 (STRIP_ASSUME_TAC o SPEC ``n:num`` o REWRITE_RULE [Next]) 524 Timeof_thm1, 525 REWRITE_TAC [ADD_CLAUSES] THEN 526 POP_ASSUM (MATCH_MP_TAC o 527 MATCH_MP (CONV_RULE ANTE_CONJ_CONV 528 (SPEC_ALL LESS_TRANS))) THEN 529 IMP_RES_THEN 530 (STRIP_ASSUME_TAC o 531 SPEC ``SUC(n+p)`` o REWRITE_RULE [Next]) Timeof_thm1]]); 532 533(* --------------------------------------------------------------------- *) 534(* Theorems about when. *) 535(* --------------------------------------------------------------------- *) 536 537val when_thm1 = 538 store_thm 539 ("when_thm1", 540 ``!f g c. (((\t.(f t,g t))when c)t) = (((f when c) t),((g when c) t))``, 541 REPEAT STRIP_TAC THEN 542 REWRITE_TAC [when,o_THM] THEN 543 CONV_TAC (DEPTH_CONV BETA_CONV) THEN REFL_TAC); 544 545val when_thm2 = 546 store_thm 547 ("when_thm2", 548 ``!c. Inf(c) ==> !t. (c when c) t``, 549 REPEAT STRIP_TAC THEN 550 IMP_RES_TAC Timeof_thm4 THEN 551 ASM_REWRITE_TAC [when,o_THM]); 552 553(* --------------------------------------------------------------------- *) 554(* Iteration theorems. *) 555(* --------------------------------------------------------------------- *) 556 557val Funpow_DEF = new_recursive_definition 558 {name = "Funpow_DEF", 559 def = ``(Funpow 0 f = I) /\ (Funpow (SUC n) f = (f o (Funpow n f)))``, 560 rec_axiom = num_Axiom} 561 562val Funpow1 = 563 store_thm("Funpow1", 564 ``!f. (Funpow 0 f x = x) /\ 565 (!n. Funpow (SUC n) f x = f((Funpow n f)x))``, 566 REWRITE_TAC [Funpow_DEF,I_THM,o_THM]); 567 568val Dev = 569 new_definition 570 ("Dev", 571 ``Dev f g (c,a,b,s) = 572 !t:num. s(t+1) = if c t then f (a t) (b t) (s t) else g (a t) (s t)``); 573 574val tempabs = 575 store_thm 576 ("tempabs", 577 ``!a b s c f g. 578 Dev f g (c,a,b,s) ==> 579 (!t. Stable (Timeof c t) (Timeof c (t+1)) a) ==> 580 Inf(c) ==> 581 !n t.((Timeof c n < t) /\ (t <= Timeof c (n+1))) ==> 582 (s t = 583 Funpow (t - ((Timeof c n)+1)) (g ((a when c) n)) 584 (f((a when c) n) ((b when c) n) ((s when c) n)))``, 585 PURE_ONCE_REWRITE_TAC [Dev] THEN 586 CONV_TAC (DEPTH_CONV num_CONV) THEN 587 REWRITE_TAC [ADD_CLAUSES,when,o_THM,Stable] THEN 588 REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN GEN_TAC THEN 589 INDUCT_TAC THENL 590 [REWRITE_TAC [NOT_LESS_0], 591 REWRITE_TAC [LESS_THM] THEN 592 REPEAT STRIP_TAC THENL 593 [IMP_RES_THEN (ASSUME_TAC o SPEC ``n:num``) Timeof_thm4 THEN 594 EVERY_ASSUM (fn th => SUBST1_TAC(SYM th) handle _ => ALL_TAC) THEN 595 ASM_REWRITE_TAC [SUB,LESS_SUC_REFL,Funpow1,I_THM], 596 IMP_RES_THEN (ASSUME_TAC o MATCH_MP LESS_IMP_LESS_OR_EQ) 597 OR_LESS THEN 598 IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [Next] o SPEC ``n:num``) 599 Timeof_thm1 THEN 600 IMP_RES_TAC OR_LESS THEN 601 RES_TAC THEN 602 IMP_RES_TAC LESS_LESS_SUC THEN 603 POP_ASSUM (ASSUME_TAC o NOT_INTRO) THEN 604 ASM_REWRITE_TAC[SUB,Funpow1,o_THM] THEN 605 POP_ASSUM (ASSUME_TAC o (REWRITE_RULE [NOT_LESS])) THEN 606 POP_ASSUM (ASSUME_TAC o (MATCH_MP OR_LESS)) THEN 607 IMP_RES_TAC LESS_IMP_LESS_OR_EQ THEN 608 RES_TAC THEN ASM_REWRITE_TAC[]]]); 609 610val tempabs' = 611 store_thm 612 ("tempabs'", 613 ``!a b s c f g. 614 Dev f g (c,a,b,s) ==> 615 (!t. Stable (Timeof c t) (Timeof c (t+1)) a) ==> 616 Inf(c) ==> 617 !n.(s when c) (n+1) = 618 Funpow ((Timeof c (n+1)) - ((Timeof c n)+1)) (g ((a when c) n)) 619 (f((a when c) n) ((b when c) n) ((s when c) n))``, 620 REPEAT (DISCH_TAC ORELSE GEN_TAC) THEN 621 REWRITE_TAC [when,o_THM] THEN 622 MATCH_MP_TAC (REWRITE_RULE [when,o_THM] 623 (UNDISCH_ALL (SPEC_ALL tempabs))) THEN 624 IMP_RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE [Next] o SPEC ``n:num``) 625 Timeof_thm1 THEN 626 ASM_REWRITE_TAC [LESS_OR_EQ,num_CONV ``1``,ADD_CLAUSES]); 627 628 629val _ = export_theory(); 630