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