1
2%----------------------------------------------------------------------------%
3% The stuff in this file is just `doodlings` and does not work!              %
4%----------------------------------------------------------------------------%
5
6new_theory`ITL`;;
7
8% Test if an interval function only depends on the start time
9  of the interval %
10
11new_definition
12 (`IS_SIG`,
13  "IS_SIG (X:num->num->*) = ?f. !m n. X m n = f m");;
14
15% Make an interval function out of a signal %
16
17new_definition
18 (`MK_SIG`, 
19  "MK_SIG (f:num->*) = \m (n:num). f m");;
20
21% Test if an interval function is a constant function %
22
23new_definition
24 (`IS_STATIC`,
25  "IS_STATIC (X:num->num->*) = ?c. !m n. X m n = c");;
26
27% Make an interval function out of a constant %
28
29new_definition
30 (`MK_STATIC`,
31  "MK_STATIC (c:*) = \m:num.\n:num. c");;
32
33% The ITL next operator for expressions. This is called "O" in Ben's papers
34  but I use that name for the next operator for formulas (see below) %
35
36new_definition
37 (`NEXT`,
38  "NEXT (X:num->num->*) = \m n. X (m+1) n");;
39
40% ITL Equality %
41
42new_infix_definition
43 (`==`,
44  "== (X:num->num->*) (Y:num->num->*) = \m n. ((X m n) = (Y m n))");;
45
46% ITL negation %
47
48new_definition
49 (`NOT`,
50  "NOT (X:num->num->bool) = \m n. ~(X m n)");;
51
52% ITL conjunction %
53
54new_infix_definition
55 (`AND`, 
56  "AND (X:num->num->bool) (Y:num->num->bool) = 
57   \m n. (X m n) /\ (Y m n)");;
58
59% The ITL next operator for formulas %
60
61new_definition
62 (`O`,
63  "O X = \m n. (n > m) /\ X (m+1) n");;
64
65% The ITL always operator %
66
67new_definition
68 (`BOX`,
69  "BOX X = \m n. !i. (m <= i) /\ (i <= n) ==> X i n");;
70
71% ITL chop operator (";" in Ben's notation - HOL won't allow ";" to be
72  made an infix) %
73
74new_infix_definition
75 (`THEN`,
76  "THEN X Y = \m n. ?i. (m<=i) /\ (i<=n) /\ (X m i) /\ (Y i n)");;
77
78% ITL existential quantification %
79
80new_binder_definition
81 (`EXISTS`,
82  "EXISTS (P:(num->num->*)->num->num->bool) = \m n. ?X. (P X m n)");;
83
84% The ITL validity predicate ("|=" in standard notation) %
85
86new_definition
87 (`VALID`,
88  "VALID (X:num->num->bool) = !m n. X m n");;
89
90
91% Now for some derived constants and operators %
92
93new_definition(`TRUE` , "TRUE  = MK_STATIC T");;
94new_definition(`FALSE`, "FALSE = MK_STATIC F");;
95
96new_definition(`ZERO`, "ZERO = MK_STATIC 0");;
97new_definition(`ONE` , "ONE  = MK_STATIC 1");;
98new_definition(`TWO` , "TWO  = MK_STATIC 2");;
99
100new_infix_definition
101 (`OR`,
102  "OR X Y = NOT(NOT X AND NOT Y)");;
103
104new_infix_definition
105 (`IMPLIES`,
106  "IMPLIES X Y = NOT X OR Y");;
107
108new_definition
109 (`EMPTY`,
110  "EMPTY = NOT(O TRUE)");;
111
112new_definition
113 (`SKIP`,
114  "SKIP = O EMPTY");;
115
116new_infix_definition
117 (`GETS`,
118  "GETS (X:num->num->*) (Y:num->num->*) =
119    BOX(NOT EMPTY IMPLIES (NEXT X == Y))");;
120
121% ITL stability operator %
122
123new_definition
124 (`STABLE`,
125  "STABLE(X:num->num->*) = X GETS X");;
126
127new_definition
128 (`FIN`,
129  "FIN X = BOX(EMPTY IMPLIES X)");;
130
131hide_constant `S`;;
132
133new_infix_definition
134 (`-->`,
135  "--> (X:num->num->*) (Y:num->num->*) =
136    EXISTS S. IS_STATIC S AND (S == X) AND FIN(S == Y)");;
137  
138% Some useful lemmas %
139
140let defs = 
141 maptok 
142  (definition `ITL`)
143  `IS_SIG MK_SIG IS_STATIC MK_STATIC NEXT == NOT AND O BOX THEN
144   EXISTS VALID TRUE FALSE ZERO ONE TWO OR IMPLIES EMPTY GETS STABLE`;;
145
146let TRUE_SEM  = prove_thm(`TRUE_SEM` , "TRUE  = \m n. T", REWRITE_TAC defs)
147and FALSE_SEM = prove_thm(`FALSE_SEM`, "FALSE = \m n. F", REWRITE_TAC defs)
148and ZERO_SEM  = prove_thm(`ZERO_SEM` , "ZERO  = \m n. 0", REWRITE_TAC defs)
149and ONE_SEM   = prove_thm(`ONE_SEM`  , "ONE   = \m n. 1", REWRITE_TAC defs)
150and TWO_SEM   = prove_thm(`TWO_SEM`  , "TWO   = \m n. 2", REWRITE_TAC defs);;
151
152let OR_SEM =
153 prove_thm
154  (`OR_SEM`,
155   "OR (X:num->num->bool) (Y:num->num->bool) = \m n. (X m n) \/ (Y m n)",
156   REWRITE_TAC defs
157    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
158    THEN REWRITE_TAC[DE_MORGAN_THM]);;
159
160let OR_IMP_THM =
161 prove_thm
162  (`OR_IMP_THM`,
163   "(~t1 \/ t2) = (t1 ==> t2)",
164   BOOL_CASES_TAC "t1:bool"
165    THEN REWRITE_TAC[]);;
166
167let IMPLIES_SEM =
168 prove_thm
169  (`IMPLIES_SEM`,
170   "IMPLIES (X:num->num->bool) (Y:num->num->bool) = 
171    \m n. (X m n) ==> (Y m n)",
172   REWRITE_TAC(OR_SEM.defs)
173    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
174    THEN REWRITE_TAC[OR_IMP_THM]);;
175
176let EMPTY_SEM =
177 prove_thm
178  (`EMPTY_SEM`,
179   "EMPTY = \m n. n<=m",
180   REWRITE_TAC(TRUE_SEM.defs)
181    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
182    THEN REWRITE_TAC[NOT_LESS;GREATER]);;
183
184let IMP_CONJ_THM =
185prove_thm
186 (`IMP_CONJ_THM`,
187  "(t1 ==> t2 ==> t3) = (t1 /\ t2 ==> t3)",
188  BOOL_CASES_TAC "t1:bool"
189   THEN REWRITE_TAC[]);;
190
191let LESS_AND_LESS_EQ_THM =
192 prove_thm
193  (`LESS_AND_LESS_EQ_THM`,
194   "m <= n /\ m < n = m < n",
195   EQ_TAC
196   THEN REPEAT STRIP_TAC
197   THEN ASM_REWRITE_TAC[LESS_OR_EQ]);;
198
199let GETS_SEM =
200 prove_thm
201  (`GETS_SEM`,
202   "GETS (X:num->num->*) (Y:num->num->*) =
203    \m n. !i. (m<=i) /\ (i<n) ==> (X(SUC i)n = Y i n)",
204   REWRITE_TAC(EMPTY_SEM.IMPLIES_SEM.defs)
205    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
206    THEN REWRITE_TAC
207          [ADD1;IMP_CONJ_THM;
208           GREATER;LESS_AND_LESS_EQ_THM;SYM(SPEC_ALL CONJ_ASSOC)]);;
209
210% The following is not yet done
211
212let STABLE_SEM_LEMMA
213 prove_thm
214  (`STABLE_SEM_LEMMA`,
215   "STABLE (X:num->num->*) m n = !i. (m<=i) /\ (i<=n) ==> (X i n = X m n)",
216   REWRITE_TAC [definition `ITL` `STABLE`;GETS_SEM]
217    THEN CONV_TAC(DEPTH_CONV BETA_CONV)
218    THEN EQ_TAC
219    THEN DISCH_TAC
220    THEN INDUCT_TAC
221    THEN REWRITE_TAC[LESS_OR_EQ;NOT_LESS_0]
222    THEN REPEAT STRIP_TAC
223    THEN ASM_REWRITE_TAC[]
224
225Need to prove:
226
227
2285 subgoals
229"X(SUC(SUC i))n = X(SUC i)n"
230    [ "!i. m <= i /\ i <= n ==> (X i n = X m n)" ]
231    [ "m <= i /\ i < n ==> (X(SUC i)n = X i n)" ]
232    [ "m = SUC i" ]
233    [ "(SUC i) < n" ]
234
235"X(SUC(SUC i))n = X(SUC i)n"
236    [ "!i. m <= i /\ i <= n ==> (X i n = X m n)" ]
237    [ "m <= i /\ i < n ==> (X(SUC i)n = X i n)" ]
238    [ "m < (SUC i)" ]
239    [ "(SUC i) < n" ]
240
241"X(SUC 0)n = X 0 n"
242    [ "!i. m <= i /\ i <= n ==> (X i n = X m n)" ]
243    [ "m = 0" ]
244    [ "0 < n" ]
245
246"X n n = X m n"
247    [ "!i. m <= i /\ i < n ==> (X(SUC i)n = X i n)" ]
248    [ "m <= i /\ i <= n ==> (X i n = X m n)" ]
249    [ "m < (SUC i)" ]
250    [ "SUC i = n" ]
251
252"X(SUC i)n = X m n"
253    [ "!i. m <= i /\ i < n ==> (X(SUC i)n = X i n)" ]
254    [ "m <= i /\ i <= n ==> (X i n = X m n)" ]
255    [ "m < (SUC i)" ]
256    [ "(SUC i) < n" ]
257
258
259let STABLE_SEM
260 prove_thm
261  (`STABLE_SEM`,
262   "STABLE (X:num->num->*) = \m n. !i. (m<=i) /\ (i<=n) ==> (X i n = X m n)",
263   REWRITE_TAC [definition `ITL` `STABLE`;GETS_SEM]
264
265must prove:
266
267"(\m n. !i. m <= i /\ i < n ==> (X(SUC i)n = X i n)) =
268 (\m n. !i. m <= i /\ i <= n ==> (X i n = X m n))"
269%
270
271
272% Now we prove a theorem suggested by Ben %
273
274let SUB_REFL =
275 prove_thm
276  (`SUB_REFL`,
277   "!m. (m - m) = 0",
278   INDUCT_TAC
279    THEN REWRITE_TAC[SUB;LESS_SUC_REFL]);;
280
281let SUC_SUB_LEMMA =
282 prove_thm
283  (`SUC_SUB_LEMMA`,
284   "(n <= m) ==> ((SUC m) - n = (m - n) + 1)",
285   REWRITE_TAC[SUB;ADD1;SYM(SPEC_ALL NOT_LESS)]
286    THEN STRIP_TAC
287    THEN ASM_REWRITE_TAC[]);;
288
289% Some arithmetic operators %
290
291new_infix_definition
292 (`++`,
293  "++ X Y = \m n. (X m n) + (Y m n)");;
294
295new_infix_definition
296 (`**`,
297  "** X Y = \m n. (X m n) * (Y m n)");;
298
299let defs_sem = 
300 [IMPLIES_SEM;GETS_SEM] @
301 subtract defs (maptok (definition `ITL`) `IMPLIES GETS`) @
302 maptok (definition `ITL`) `++ **`;;
303
304prove_thm
305 (`BENS_THM`,
306  "VALID (EXISTS X. (X == ZERO) AND (X GETS (X ++ ONE)))",
307  REWRITE_TAC defs_sem
308   THEN CONV_TAC(DEPTH_CONV BETA_CONV)
309   THEN REPEAT GEN_TAC
310   THEN EXISTS_TAC"\m' n.(m'-m)"
311   THEN CONV_TAC(DEPTH_CONV BETA_CONV)
312   THEN REPEAT STRIP_TAC
313   THEN IMP_RES_TAC LESS_EQ_TRANS
314   THEN IMP_RES_TAC SUC_SUB_LEMMA
315   THEN REWRITE_TAC[SUB_REFL]);;
316
317let g:goal =
318 ([], "VALID(((I == ZERO)          AND
319              (J == ZERO)          AND
320              (I GETS (I ++ ONE))  AND
321              (J GETS (J ++ TWO))) IMPLIES
322              BOX(J == (TWO ** I)))");;
323
324% Proof not yet done ... feel free to finish it!
325
326prove_thm
327 (`ROGERS_THM`,
328  "VALID(((I == ZERO)          AND
329          (J == ZERO)          AND
330          (I GETS (I ++ ONE))  AND
331          (J GETS (J ++ TWO))) IMPLIES
332          BOX(J == (TWO ** I)))",
333  REWRITE_TAC defs_sem
334   THEN CONV_TAC(DEPTH_CONV BETA_CONV)
335   THEN REPEAT GEN_TAC
336   THEN REPEAT STRIP_TAC
337   THEN INDUCT_TAC
338
339%
340