1% PROOF		: Transistor Implementation of a Counter		%
2% FILE		: tempabs.ml						%
3%									%
4% DESCRIPTION	: Defines the predicates `Next`, `Inf`, `IsTimeOf`	%
5%		  and `TimeOf` and derives several major theorems	%
6%		  which provide a basis for temporal abstraction.	%
7%									%
8%		  These predicates and theorems are taken from		%
9%		  T.Melham's paper, "Abstraction Mechanisms for		%
10%		  Hardware Verification", Hardware Verification		%
11%		  Workshop, University of Calgary, January 1987.	%
12%									%
13% AUTHOR	: J.Joyce						%
14% DATE		: 31 March 1987						%
15
16new_theory `tempabs`;;
17
18new_parent `wop`;;
19
20let Next = new_definition (
21	`Next`, 
22	"Next (t1,t2) g =
23	  (t1 < t2) /\ (g t2)  /\ (!t. (t1 < t) /\ (t < t2) ==> ~g t)");;
24
25let Inf = new_definition (
26	`Inf`,
27	"Inf g = !t.?t'. t'>t /\ (g t')");;
28
29let IsTimeOf = new_prim_rec_definition (
30	`IsTimeOf`,
31	"(IsTimeOf 0 g t = g (t) /\ !t'. t' < t ==> ~g (t')) /\
32	 (IsTimeOf (SUC n) g t =
33	  g (t) /\
34	  ?t'.
35	    t' < t /\
36	    IsTimeOf n g t' /\
37	    (!t''. ((t' < t'') /\ (t'' < t)) ==> ~g (t'')))");;
38
39let TimeOf = new_definition (
40	`TimeOf`,
41	"TimeOf g n = @t. IsTimeOf n g t");;
42
43let when = new_infix_definition (
44	`when`,
45	"when (s1:num->*) (s2:num->bool) = (\n. s1 (TimeOf s2 n))");;
46
47let WOP = theorem `wop` `WOP`;;
48
49let BETA_RULE = CONV_RULE (DEPTH_CONV BETA_CONV);;
50
51let Next_ADD1 = prove_thm (
52	`Next_ADD1`,
53	"!s t. (s (t + 1) ==> Next (t,t + 1) s)",
54	PURE_REWRITE_TAC [Next;SYM (SPEC "t" ADD1)] THEN
55	REPEAT STRIP_TAC THENL
56	[REWRITE_TAC [LESS_SUC_REFL];
57	 FIRST_ASSUM ACCEPT_TAC;
58	 IMP_RES_TAC LESS_NOT_EQ THEN
59	 ASSUME_TAC (NOT_EQ_SYM (ASSUME "~(t = t')")) THEN
60	 IMP_RES_TAC LESS_SUC_IMP THEN
61	 IMP_RES_TAC LESS_ANTISYM]);;
62
63let Next_INCREASE = prove_thm (
64	`Next_INCREASE`,
65	"!s t1 t2.
66	  (~(s (t1 + 1)) /\ Next (t1 + 1,t2) s) ==> Next (t1,t2) s",
67	PURE_REWRITE_TAC [Next;SYM (SPEC "t" ADD1)] THEN
68	REPEAT STRIP_TAC THENL
69	[IMP_RES_TAC SUC_LESS;
70	 FIRST_ASSUM ACCEPT_TAC;
71	 IMP_RES_TAC LESS_SUC_EQ THEN
72	 DISJ_CASES_TAC
73	   (PURE_REWRITE_RULE [LESS_OR_EQ] (ASSUME "(SUC t1) <= t")) THENL
74	 [RES_TAC;
75	  ASSUME_TAC (SUBS [ASSUME "SUC t1 = t"] (ASSUME "~s(SUC t1)")) THEN
76	  RES_TAC]]);;
77
78let Next_IDENTITY = prove_thm (
79	`Next_IDENTITY`,
80	"!s t1 t2 t3.
81	  (Next (t1,t2) s /\ Next (t1,t3) s) ==> (t2 = t3)",
82	PURE_REWRITE_TAC [Next] THEN
83	REPEAT STRIP_TAC THEN
84	DISJ_CASES_TAC (SPEC "t2 = t3" EXCLUDED_MIDDLE) THENL
85	[FIRST_ASSUM ACCEPT_TAC;
86	 DISJ_CASES_TAC (SPEC "t2 < t3" EXCLUDED_MIDDLE) THENL
87	 [RES_TAC;IMP_RES_TAC LESS_CASES_IMP THEN RES_TAC]]);;
88
89% lemma1 = . |- ?n. g n /\ (!m. m < n ==> ~g m) %
90let th1 = SPEC "t" (PURE_REWRITE_RULE [Inf] (ASSUME "Inf g"));;
91let th2 = ASSUME (snd (dest_exists (concl th1)));;
92let th3 = CONJUNCT2 th2;;
93let th4 = EXISTS (mk_exists ("t'",concl th3),"t'") th3;;
94let th5 = CHOOSE ("t'",th1) th4;;
95let lemma1 = MATCH_MP WOP th5;;
96
97let lemma2 = TAC_PROOF (
98	([],"(a ==> ~(b /\ c)) = ((b /\ a) ==> ~c)"),
99	REWRITE_TAC [DE_MORGAN_THM;SYM (SPEC_ALL IMP_DISJ_THM)] THEN
100	EQ_TAC THEN (REPEAT STRIP_TAC) THEN RES_TAC);;
101
102%
103lemma3 = 
104.. |- ?t'.
105       g t' /\
106       (?t. t < t' /\ IsTimeOf n g t /\ (!m. t < m /\ m < t' ==> ~g m))
107%
108let th1 = ASSUME "?t. IsTimeOf n g t";;
109let th2 = ASSUME (snd (dest_exists (concl th1)));;
110let th3 = SPEC "t" (PURE_REWRITE_RULE [Inf] (ASSUME "Inf g"));;
111let th4 = ASSUME (snd (dest_exists (concl th3)));;
112let th5 = BETA_CONV (mk_comb (mk_abs ("t'",concl th4),"t'"));;
113let th6 = EQ_MP (SYM th5) th4;;
114let th7 = EXISTS (mk_exists ("t'",concl th6),"t'") th6;;
115let th8 = CHOOSE ("t'",th3) th7;;
116let th9 = BETA_RULE (MATCH_MP WOP th8);;
117let th10 = EQ_MP (GEN_ALPHA_CONV "t'" (concl th9)) th9;;
118let th11 = PURE_REWRITE_RULE [GREATER;lemma2] th10;;
119let th12 = ASSUME (snd (dest_exists (concl th11)));;
120let th13 = CONJUNCT1 (CONJUNCT1 th12);;
121let th14 = CONJUNCT2 (CONJUNCT1 th12);;
122let th15 = CONJUNCT2 th12;;
123let th16 = LIST_CONJ [th13;th2;th15];;
124let th17 = EXISTS (mk_exists ("t",concl th16),"t") th16;;
125let th18 = LIST_CONJ [th14;th17];;
126let th19 = EXISTS (mk_exists ("t'",concl th18),"t'") th18;;
127let th20 = CHOOSE ("t'",th11) th19;;
128let lemma3 = CHOOSE ("t",th1) th20;;
129
130let IsTimeOf_EXISTS = prove_thm (
131	`IsTimeOf_EXISTS`,
132	"!g. Inf g ==> !n. ?t. IsTimeOf n g t",
133	GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
134	[REWRITE_TAC [IsTimeOf;lemma1];REWRITE_TAC [IsTimeOf;lemma3]]);;
135
136let TimeOf_DEFINED = prove_thm (
137	`TimeOf_DEFINED`,
138	"!g. Inf g ==> !n. IsTimeOf n g (TimeOf g n)",
139	REPEAT STRIP_TAC THEN
140	IMP_RES_TAC IsTimeOf_EXISTS THEN
141	ACCEPT_TAC
142	  (PURE_REWRITE_RULE [SYM TimeOf]
143	    (SELECT_RULE (SPEC "n" (ASSUME "!n. ?t. IsTimeOf n g t")))));;
144
145let TimeOf_TRUE = prove_thm (
146	`TimeOf_TRUE`,
147	"!g. Inf g ==> !n. g (TimeOf g n)",
148	REPEAT STRIP_TAC THEN
149	IMP_RES_TAC TimeOf_DEFINED THEN
150	DISJ_CASES_TAC (SPEC "n" num_CASES) THENL
151	[SUBST1_TAC (ASSUME "n = 0") THEN
152	 STRIP_ASSUME_TAC
153	   (PURE_REWRITE_RULE [IsTimeOf]
154	     (SPEC "0" (ASSUME "!n. IsTimeOf n g (TimeOf g n)")));
155	 FIRST_ASSUM
156	   (\thm.
157	     if is_exists (concl thm)
158	       then (CHOOSE_THEN SUBST1_TAC thm) else NO_TAC) THEN
159	 STRIP_ASSUME_TAC
160	   (PURE_REWRITE_RULE [IsTimeOf]
161	     (SPEC "SUC n'" (ASSUME "!n. IsTimeOf n g (TimeOf g n)")))]);;
162
163let tm = "!t''. t' < t'' /\ t'' < t1 ==> ~g t''";;
164
165let IsTimeOf_IDENTITY = prove_thm (
166	`IsTimeOf_IDENTITY`,
167	"!g n t1 t2. IsTimeOf n g t1 /\ IsTimeOf n g t2 ==> (t1 = t2)",
168	GEN_TAC THEN
169	INDUCT_TAC THENL
170	[PURE_REWRITE_TAC [IsTimeOf] THEN
171	 REPEAT STRIP_TAC THEN
172	 DISJ_CASES_TAC (SPECL ["t1";"t2"] LESS_CASES) THENL
173	 [RES_TAC;
174	  DISJ_CASES_TAC
175	    (PURE_REWRITE_RULE [LESS_OR_EQ] (ASSUME "t2 <= t1")) THENL
176	  [RES_TAC;ACCEPT_TAC (SYM (ASSUME "t2 = t1"))]];
177	 PURE_REWRITE_TAC [IsTimeOf] THEN
178	 REPEAT STRIP_TAC THEN
179	 RES_TAC THEN
180	 ASSUME_TAC
181	  (SUBS [ASSUME "t'' = t'"]
182	    (ASSUME "!t'''. t'' < t''' /\ t''' < t2 ==> ~g t'''")) THEN
183	 ASSUME_TAC
184	   (SUBS [ASSUME "t' = t''"]
185	     (EQ_MP (GEN_ALPHA_CONV "t''':num" tm) (ASSUME tm))) THEN
186	 DISJ_CASES_TAC (SPECL ["t1";"t2"] LESS_CASES) THENL
187	 [RES_TAC;
188	  DISJ_CASES_TAC
189	    (PURE_REWRITE_RULE [LESS_OR_EQ] (ASSUME "t2 <= t1")) THENL
190	  [RES_TAC;
191	   ASSUME_TAC (SYM (ASSUME "t2 = t1")) THEN
192	   RES_TAC THEN
193	   ACCEPT_TAC (SYM (ASSUME "t2 = t1"))]]]);;
194
195%
196TimeOf_INCREASING = 
197|- !g. Inf g ==> (!n. (TimeOf g n) < (TimeOf g(n + 1)))
198%
199let th1 =
200	PURE_REWRITE_RULE [IsTimeOf]
201	  (SPEC "SUC n" (UNDISCH (SPEC "g" TimeOf_DEFINED)));;
202let th2 = CONJUNCT2 th1;;
203let th3 = ASSUME (snd (dest_exists (concl th2)));;
204let th4 = CONJUNCT1 th3;;
205let th5 = CONJUNCT1 (CONJUNCT2 th3);;
206let th6 = SPEC "n" (UNDISCH (SPEC "g" TimeOf_DEFINED));;
207let th7 = MATCH_MP IsTimeOf_IDENTITY (LIST_CONJ [th5;th6]);;
208let th8 = SUBS [th7] th4;;
209let th9 = CHOOSE ("t'",th2) th8;;
210let th10 = GEN "g" (DISCH_ALL (GEN "n" th9));;
211let th11 = PURE_REWRITE_RULE [ADD1] th10;;
212let TimeOf_INCREASING = save_thm (`TimeOf_INCREASING`,th11);;
213
214%
215TimeOf_INTERVAL = 
216|- !g.
217    Inf g ==> (!n t. (TimeOf g n) < t /\ t < (TimeOf g(n + 1)) ==> ~g t)
218%
219let th1 =
220	PURE_REWRITE_RULE [IsTimeOf]
221	  (SPEC "SUC n" (UNDISCH (SPEC "g" TimeOf_DEFINED)));;
222let th2 = CONJUNCT2 th1;;
223let th3 = ASSUME (snd (dest_exists (concl th2)));;
224let th4 = CONJUNCT2 (CONJUNCT2 th3);;
225let th5 = CONJUNCT1 (CONJUNCT2 th3);;
226let th6 = SPEC "n" (UNDISCH (SPEC "g" TimeOf_DEFINED));;
227let th7 = MATCH_MP IsTimeOf_IDENTITY (LIST_CONJ [th5;th6]);;
228let th8 = SUBS [th7] th4;;
229let th9 = EQ_MP (GEN_ALPHA_CONV "t" (concl th8)) th8;;
230let th10 = CHOOSE ("t'",th2) th9;;
231let th11 = GEN "g" (DISCH_ALL (GEN "n" th10));;
232let th12 = PURE_REWRITE_RULE [ADD1] th11;;
233let TimeOf_INTERVAL = save_thm (`TimeOf_Interval`,th12);;
234
235let TimeOf_Next = prove_thm (
236	`TimeOf_Next`,
237	"!g. Inf g ==> Next (TimeOf g n,TimeOf g (n+1)) g",
238	PURE_REWRITE_TAC [Next] THEN
239	REPEAT STRIP_TAC THEN
240	IMP_RES_THEN (\thm. REWRITE_TAC [thm]) TimeOf_INCREASING THEN
241	IMP_RES_THEN (\thm. REWRITE_TAC [thm]) TimeOf_TRUE THEN
242	IMP_RES_THEN (\thm. REWRITE_TAC [thm]) TimeOf_INTERVAL);;
243
244close_theory ();;
245