Update from HH
[hl193./.git] / Tutorial / all.ml
1 (* ========================================================================= *)
2 (* HOL basics                                                                *)
3 (* ========================================================================= *)
4
5 ARITH_RULE
6  `(a * x + b * y + a * y) EXP 3 + (b * x) EXP 3 +
7   (a * x + b * y + b * x) EXP 3 + (a * y) EXP 3 =
8   (a * x + a * y + b * x) EXP 3 + (b * y) EXP 3 +
9   (a * y + b * y + b * x) EXP 3 + (a * x) EXP 3`;;
10
11 (* ========================================================================= *)
12 (* Propositional logic                                                       *)
13 (* ========================================================================= *)
14
15 TAUT
16  `(~input_a ==> (internal <=> T)) /\
17   (~input_b ==> (output <=> internal)) /\
18   (input_a ==> (output <=> F)) /\
19   (input_b ==> (output <=> F))
20   ==> (output <=> ~(input_a \/ input_b))`;;
21
22 TAUT
23 `(i1 /\ i2 <=> a) /\
24  (i1 /\ i3 <=> b) /\
25  (i2 /\ i3 <=> c) /\
26  (i1 /\ c <=> d) /\
27  (m /\ r <=> e) /\
28  (m /\ w <=> f) /\
29  (n /\ w <=> g) /\
30  (p /\ w <=> h) /\
31  (q /\ w <=> i) /\
32  (s /\ x <=> j) /\
33  (t /\ x <=> k) /\
34  (v /\ x <=> l) /\
35  (i1 \/ i2 <=> m) /\
36  (i1 \/ i3 <=> n) /\
37  (i1 \/ q <=> p) /\
38  (i2 \/ i3 <=> q) /\
39  (i3 \/ a <=> r) /\
40  (a \/ w <=> s) /\
41  (b \/ w <=> t) /\
42  (d \/ h <=> u) /\
43  (c \/ w <=> v) /\
44  (~e <=> w) /\
45  (~u <=> x) /\
46  (i \/ l <=> o1) /\
47  (g \/ k <=> o2) /\
48  (f \/ j <=> o3)
49  ==> (o1 <=> ~i1) /\ (o2 <=> ~i2) /\ (o3 <=> ~i3)`;;
50
51 (* ========================================================================= *)
52 (* Abstractions and quantifiers                                              *)
53 (* ========================================================================= *)
54
55 MESON[]
56  `((?x. !y. P(x) <=> P(y)) <=> ((?x. Q(x)) <=> (!y. Q(y)))) <=>
57   ((?x. !y. Q(x) <=> Q(y)) <=> ((?x. P(x)) <=> (!y. P(y))))`;;
58
59 MESON[]
60 `(!x y z. P x y /\ P y z ==> P x z) /\
61  (!x y z. Q x y /\ Q y z ==> Q x z) /\
62  (!x y. P x y ==> P y x) /\
63  (!x y. P x y \/ Q x y)
64  ==> (!x y. P x y) \/ (!x y. Q x y)`;;
65
66 let ewd1062 = MESON[]
67  `(!x. x <= x) /\
68   (!x y z. x <= y /\ y <= z ==> x <= z) /\
69   (!x y. f(x) <= y <=> x <= g(y))
70   ==> (!x y. x <= y ==> f(x) <= f(y)) /\
71       (!x y. x <= y ==> g(x) <= g(y))`;;
72
73 let ewd1062 = MESON[]
74  `(!x. R x x) /\
75   (!x y z. R x y /\ R y z ==> R x z) /\
76   (!x y. R (f x) y <=> R x (g y))
77   ==> (!x y. R x y ==> R (f x) (f y)) /\
78       (!x y. R x y ==> R (g x) (g y))`;;
79
80 MESON[] `(?!x. g(f x) = x) <=> (?!y. f(g y) = y)`;;
81
82 MESON [ADD_ASSOC; ADD_SYM] `m + (n + p) = n + (m + p)`;;
83
84 (* ========================================================================= *)
85 (* Tactics and tacticals                                                     *)
86 (* ========================================================================= *)
87
88 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
89 e DISCH_TAC;;
90 b();;
91 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
92 e(SIMP_TAC[]);;
93 e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
94 e DISCH_TAC;;
95 e(ASM_REWRITE_TAC[]);;
96 e(CONV_TAC ARITH_RULE);;
97 let trivial = top_thm();;
98
99 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
100 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
101 e(SIMP_TAC[]);;
102 e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
103 e DISCH_TAC;;
104 e(ASM_REWRITE_TAC[]);;
105 e(CONV_TAC ARITH_RULE);;
106 let trivial = top_thm();;
107
108 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
109 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]) THEN
110   SIMP_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
111   DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_RULE);;
112 let trivial = top_thm();;
113
114 let trivial = prove
115  (`2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`,
116   CONV_TAC(REWRITE_CONV[LE_ANTISYM]) THEN
117   SIMP_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
118   DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_RULE);;
119
120 let trivial = prove
121  (`!x y:real. &0 < x * y ==> (&0 < x <=> &0 < y)`,
122   REPEAT GEN_TAC THEN MP_TAC(SPECL [`--x`; `y:real`] REAL_LE_MUL) THEN
123   MP_TAC(SPECL [`x:real`; `--y`] REAL_LE_MUL) THEN REAL_ARITH_TAC);;
124
125 let trivial = prove
126  (`!x y:real. &0 < x * y ==> (&0 < x <=> &0 < y)`,
127   MATCH_MP_TAC REAL_WLOG_LE THEN CONJ_TAC THEN REPEAT GEN_TAC THEN
128   MP_TAC(SPECL [`--x`; `y:real`] REAL_LE_MUL) THEN REAL_ARITH_TAC);;
129
130 let SUM_OF_NUMBERS = prove
131  (`!n. nsum(1..n) (\i. i) = (n * (n + 1)) DIV 2`,
132   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
133
134 let SUM_OF_SQUARES = prove
135  (`!n. nsum(1..n) (\i. i * i) = (n * (n + 1) * (2 * n + 1)) DIV 6`,
136   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
137
138 let SUM_OF_CUBES = prove
139  (`!n. nsum(1..n) (\i. i*i*i) = (n * n * (n + 1) * (n + 1)) DIV 4`,
140   INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
141
142 (* ========================================================================= *)
143 (* HOL's number systems                                                      *)
144 (* ========================================================================= *)
145
146 REAL_ARITH `!x y:real. (abs(x) - abs(y)) <= abs(x - y)`;;
147
148 INT_ARITH
149  `!a b a' b' D:int.
150      (a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) =
151      (a * a' + D * b * b') pow 2 - D * (a * b' + a' * b) pow 2`;;
152
153 REAL_ARITH
154  `!x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11:real.
155         x3 = abs(x2) - x1 /\
156         x4 = abs(x3) - x2 /\
157         x5 = abs(x4) - x3 /\
158         x6 = abs(x5) - x4 /\
159         x7 = abs(x6) - x5 /\
160         x8 = abs(x7) - x6 /\
161         x9 = abs(x8) - x7 /\
162         x10 = abs(x9) - x8 /\
163         x11 = abs(x10) - x9
164         ==> x1 = x10 /\ x2 = x11`;;
165
166 REAL_ARITH `!x y:real. x < y ==> x < (x + y) / &2 /\ (x + y) / &2 < y`;;
167
168 REAL_ARITH
169  `((x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2) =
170   ((&1 / &6) * ((x1 + x2) pow 4 + (x1 + x3) pow 4 + (x1 + x4) pow 4 +
171                 (x2 + x3) pow 4 + (x2 + x4) pow 4 + (x3 + x4) pow 4) +
172    (&1 / &6) * ((x1 - x2) pow 4 + (x1 - x3) pow 4 + (x1 - x4) pow 4 +
173                 (x2 - x3) pow 4 + (x2 - x4) pow 4 + (x3 - x4) pow 4))`;;
174
175 ARITH_RULE `x < 2 ==> 2 * x + 1 < 4`;;
176
177 (**** Fails
178 ARITH_RULE `~(2 * m + 1 = 2 * n)`;;
179  ****)
180
181 ARITH_RULE `x < 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
182
183 (**** Fails
184 ARITH_RULE `x <= 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
185  ****)
186
187 (**** Fails
188 ARITH_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
189  ****)
190
191 (**** Fails
192 REAL_ARITH `!x y:real. x = y ==> x * y = y pow 2`;;
193  ****)
194
195 prioritize_real();;
196
197 REAL_RING
198   `s = (a + b + c) / &2
199    ==> s * (s - b) * (s - c) + s * (s - c) * (s - a) +
200        s * (s - a) * (s - b) - (s - a) * (s - b) * (s - c) =
201        a * b * c`;;
202
203 REAL_RING `a pow 2 = &2 /\ x pow 2 + a * x + &1 = &0 ==> x pow 4 + &1 = &0`;;
204
205 REAL_RING
206  `(a * x pow 2 + b * x + c = &0) /\
207   (a * y pow 2 + b * y + c = &0) /\
208   ~(x = y)
209   ==> (a * x * y = c) /\ (a * (x + y) + b = &0)`;;
210
211 REAL_RING
212  `p = (&3 * a1 - a2 pow 2) / &3 /\
213   q = (&9 * a1 * a2 - &27 * a0 - &2 * a2 pow 3) / &27 /\
214   x = z + a2 / &3 /\
215   x * w = w pow 2 - p / &3
216   ==> (z pow 3 + a2 * z pow 2 + a1 * z + a0 = &0 <=>
217        if p = &0 then x pow 3 = q
218        else (w pow 3) pow 2 - q * (w pow 3) - p pow 3 / &27 = &0)`;;
219
220 REAL_FIELD `&0 < x ==> &1 / x - &1 / (&1 + x) = &1 / (x * (&1 + x))`;;
221
222 REAL_FIELD
223 `s pow 2 = b pow 2 - &4 * a * c
224  ==> (a * x pow 2 + b * x + c = &0 <=>
225       if a = &0 then
226          if b = &0 then
227             if c = &0 then T else F
228          else x = --c / b
229       else x = (--b + s) / (&2 * a) \/ x = (--b + --s) / (&2 * a))`;;
230
231 (**** This needs an external SDP solver to assist with proof
232
233 needs "Examples/sos.ml";;
234
235 SOS_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
236
237 REAL_SOS
238  `!a1 a2 a3 a4:real.
239       &0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4
240       ==> a1 pow 2 +
241           ((a1 + a2) / &2) pow 2 +
242           ((a1 + a2 + a3) / &3) pow 2 +
243           ((a1 + a2 + a3 + a4) / &4) pow 2
244          <= &4 * (a1 pow 2 + a2 pow 2 + a3 pow 2 + a4 pow 2)`;;
245
246 REAL_SOS
247  `!a b c:real.
248       a >= &0 /\ b >= &0 /\ c >= &0
249       ==> &3 / &2 * (b + c) * (a + c) * (a + b) <=
250           a * (a + c) * (a + b) +
251           b * (b + c) * (a + b) +
252           c * (b + c) * (a + c)`;;
253
254 SOS_CONV `&2 * x pow 4 + &2 * x pow 3 * y - x pow 2 * y pow 2 + &5 * y pow 4`;;
255
256 PURE_SOS
257 `x pow 4 + &2 * x pow 2 * z + x pow 2 - &2 * x * y * z +
258           &2 * y pow 2 * z pow 2 + &2 * y * z pow 2 + &2 * z pow 2 - &2 * x +
259           &2 *  y * z + &1 >= &0`;;
260
261 *****)
262
263 needs "Examples/cooper.ml";;
264
265 COOPER_RULE `ODD n ==> 2 * n DIV 2 < n`;;
266
267 COOPER_RULE `!n. n >= 8 ==> ?a b. n = 3 * a + 5 * b`;;
268
269 needs "Rqe/make.ml";;
270
271 REAL_QELIM_CONV `!x. &0 <= x ==> ?y. y pow 2 = x`;;
272
273 (* ========================================================================= *)
274 (* Inductive definitions                                                     *)
275 (* ========================================================================= *)
276
277 (* ------------------------------------------------------------------------- *)
278 (* Bug puzzle.                                                               *)
279 (* ------------------------------------------------------------------------- *)
280
281 prioritize_real();;
282
283 let move = new_definition
284  `move ((ax,ay),(bx,by),(cx,cy)) ((ax',ay'),(bx',by'),(cx',cy')) <=>
285         (?a. ax' = ax + a * (cx - bx) /\ ay' = ay + a * (cy - by) /\
286              bx' = bx /\ by' = by /\ cx' = cx /\ cy' = cy) \/
287         (?b. bx' = bx + b * (ax - cx) /\ by' = by + b * (ay - cy) /\
288              ax' = ax /\ ay' = ay /\ cx' = cx /\ cy' = cy) \/
289         (?c. ax' = ax /\ ay' = ay /\ bx' = bx /\ by' = by /\
290              cx' = cx + c * (bx - ax) /\ cy' = cy + c * (by - ay))`;;
291
292 let reachable_RULES,reachable_INDUCT,reachable_CASES =
293  new_inductive_definition
294   `(!p. reachable p p) /\
295    (!p q r. move p q /\ reachable q r ==> reachable p r)`;;
296
297 let oriented_area = new_definition
298  `oriented_area ((ax,ay),(bx,by),(cx,cy)) =
299       ((bx - ax) * (cy - ay) - (cx - ax) * (by - ay)) / &2`;;
300
301 let MOVE_INVARIANT = prove
302  (`!p p'. move p p' ==> oriented_area p = oriented_area p'`,
303   REWRITE_TAC[FORALL_PAIR_THM; move; oriented_area] THEN CONV_TAC REAL_RING);;
304
305 let REACHABLE_INVARIANT = prove
306  (`!p p'. reachable p p' ==> oriented_area p = oriented_area p'`,
307   MATCH_MP_TAC reachable_INDUCT THEN MESON_TAC[MOVE_INVARIANT]);;
308
309 let IMPOSSIBILITY_B = prove
310  (`~(reachable ((&0,&0),(&3,&0),(&0,&3)) ((&1,&2),(&2,&5),(-- &2,&3)) \/
311      reachable ((&0,&0),(&3,&0),(&0,&3)) ((&1,&2),(-- &2,&3),(&2,&5)) \/
312      reachable ((&0,&0),(&3,&0),(&0,&3)) ((&2,&5),(&1,&2),(-- &2,&3)) \/
313      reachable ((&0,&0),(&3,&0),(&0,&3)) ((&2,&5),(-- &2,&3),(&1,&2)) \/
314      reachable ((&0,&0),(&3,&0),(&0,&3)) ((-- &2,&3),(&1,&2),(&2,&5)) \/
315      reachable ((&0,&0),(&3,&0),(&0,&3)) ((-- &2,&3),(&2,&5),(&1,&2)))`,
316   STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP REACHABLE_INVARIANT) THEN
317   REWRITE_TAC[oriented_area] THEN REAL_ARITH_TAC);;
318
319 (* ------------------------------------------------------------------------- *)
320 (* Verification of a simple concurrent program.                              *)
321 (* ------------------------------------------------------------------------- *)
322
323 let init = new_definition
324  `init (x,y,pc1,pc2,sem) <=>
325         pc1 = 10 /\ pc2 = 10 /\ x = 0 /\ y = 0 /\ sem = 1`;;
326
327 let trans = new_definition
328  `trans (x,y,pc1,pc2,sem) (x',y',pc1',pc2',sem') <=>
329         pc1 = 10 /\ sem > 0 /\ pc1' = 20 /\ sem' = sem - 1 /\
330                    (x',y',pc2') = (x,y,pc2) \/
331         pc2 = 10 /\ sem > 0 /\ pc2' = 20 /\ sem' = sem - 1 /\
332                    (x',y',pc1') = (x,y,pc1) \/
333         pc1 = 20 /\ pc1' = 30 /\ x' = x + 1 /\
334                    (y',pc2',sem') = (y,pc2,sem) \/
335         pc2 = 20 /\ pc2' = 30 /\ y' = y + 1 /\ x' = x /\
336                    pc1' = pc1 /\ sem' = sem \/
337         pc1 = 30 /\ pc1' = 10 /\ sem' = sem + 1 /\
338                    (x',y',pc2') = (x,y,pc2) \/
339         pc2 = 30 /\ pc2' = 10 /\ sem' = sem + 1 /\
340                    (x',y',pc1') = (x,y,pc1)`;;
341
342 let mutex = new_definition
343  `mutex (x,y,pc1,pc2,sem) <=> pc1 = 10 \/ pc2 = 10`;;
344
345 let indinv = new_definition
346  `indinv (x:num,y:num,pc1,pc2,sem) <=>
347         sem + (if pc1 = 10 then 0 else 1) + (if pc2 = 10 then 0 else 1) = 1`;;
348
349 needs "Library/rstc.ml";;
350
351 let INDUCTIVE_INVARIANT = prove
352  (`!init invariant transition P.
353         (!s. init s ==> invariant s) /\
354         (!s s'. invariant s /\ transition s s' ==> invariant s') /\
355         (!s. invariant s ==> P s)
356         ==> !s s':A. init s /\ RTC transition s s' ==> P s'`,
357   REPEAT GEN_TAC THEN MP_TAC(ISPECL
358    [`transition:A->A->bool`;
359     `\s s':A. invariant s ==> invariant s'`] RTC_INDUCT) THEN
360   MESON_TAC[]);;
361
362 let MUTEX = prove
363  (`!s s'. init s /\ RTC trans s s' ==> mutex s'`,
364   MATCH_MP_TAC INDUCTIVE_INVARIANT THEN EXISTS_TAC `indinv` THEN
365   REWRITE_TAC[init; trans; indinv; mutex; FORALL_PAIR_THM; PAIR_EQ] THEN
366   ARITH_TAC);;
367
368 (* ========================================================================= *)
369 (* Wellfounded induction                                                     *)
370 (* ========================================================================= *)
371
372 let NSQRT_2 = prove
373  (`!p q. p * p = 2 * q * q ==> q = 0`,
374   MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
375   REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
376   REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
377   DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
378   FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
379   ASM_REWRITE_TAC[ARITH_RULE
380    `q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
381     (2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
382   ASM_MESON_TAC[LE_MULT2; MULT_EQ_0; ARITH_RULE `2 * x <= x <=> x = 0`]);;
383
384 (* ========================================================================= *)
385 (* Changing proof style                                                      *)
386 (* ========================================================================= *)
387
388 let fix ts = MAP_EVERY X_GEN_TAC ts;;
389
390 let assume lab t =
391   DISCH_THEN(fun th -> if concl th = t then LABEL_TAC lab th
392                        else failwith "assume");;
393
394 let we're finished tac = tac;;
395
396 let suffices_to_prove q tac = SUBGOAL_THEN q (fun th -> MP_TAC th THEN tac);;
397
398 let note(lab,t) tac =
399   SUBGOAL_THEN t MP_TAC THENL [tac; ALL_TAC] THEN
400   DISCH_THEN(fun th -> LABEL_TAC lab th);;
401
402 let have t = note("",t);;
403
404 let cases (lab,t) tac =
405   SUBGOAL_THEN t MP_TAC THENL [tac; ALL_TAC] THEN
406   DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab));;
407
408 let consider (x,lab,t) tac =
409   let tm = mk_exists(x,t) in
410   SUBGOAL_THEN tm (X_CHOOSE_THEN x (LABEL_TAC lab)) THENL [tac; ALL_TAC];;
411
412 let trivial = MESON_TAC[];;
413 let algebra = CONV_TAC NUM_RING;;
414 let arithmetic = ARITH_TAC;;
415
416 let by labs tac = MAP_EVERY (fun l -> USE_THEN l MP_TAC) labs THEN tac;;
417
418 let using ths tac = MAP_EVERY MP_TAC ths THEN tac;;
419
420 let so constr arg tac = constr arg (FIRST_ASSUM MP_TAC THEN tac);;
421
422 let NSQRT_2 = prove
423  (`!p q. p * p = 2 * q * q ==> q = 0`,
424   suffices_to_prove
425    `!p. (!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0))
426         ==> (!q. p * p = 2 * q * q ==> q = 0)`
427    (MATCH_ACCEPT_TAC num_WF) THEN
428   fix [`p:num`] THEN
429   assume("A") `!m. m < p ==> !q. m * m = 2 * q * q ==> q = 0` THEN
430   fix [`q:num`] THEN
431   assume("B") `p * p = 2 * q * q` THEN
432   so have `EVEN(p * p) <=> EVEN(2 * q * q)` (trivial) THEN
433   so have `EVEN(p)` (using [ARITH; EVEN_MULT] trivial) THEN
434   so consider (`m:num`,"C",`p = 2 * m`) (using [EVEN_EXISTS] trivial) THEN
435   cases ("D",`q < p \/ p <= q`) (arithmetic) THENL
436    [so have `q * q = 2 * m * m ==> m = 0` (by ["A"] trivial) THEN
437     so we're finished (by ["B"; "C"] algebra);
438
439     so have `p * p <= q * q` (using [LE_MULT2] trivial) THEN
440     so have `q * q = 0` (by ["B"] arithmetic) THEN
441     so we're finished (algebra)]);;
442
443 (* ========================================================================= *)
444 (* Recursive definitions                                                     *)
445 (* ========================================================================= *)
446
447 let fib = define
448  `fib n = if n = 0 \/ n = 1 then 1 else fib(n - 1) + fib(n - 2)`;;
449
450 let fib2 = define
451  `(fib2 0 = 1) /\
452   (fib2 1 = 1) /\
453   (fib2 (n + 2) = fib2(n) + fib2(n + 1))`;;
454
455 let halve = define `halve (2 * n) = n`;;
456
457 let unknown = define `unknown n = unknown(n + 1)`;;
458
459 define
460  `!n. collatz(n) = if n <= 1 then n
461                    else if EVEN(n) then collatz(n DIV 2)
462                    else collatz(3 * n + 1)`;;
463
464 let fusc_def = define
465  `(fusc (2 * n) = if n = 0 then 0 else fusc(n)) /\
466   (fusc (2 * n + 1) = if n = 0 then 1 else fusc(n) + fusc(n + 1))`;;
467
468 let fusc = prove
469  (`fusc 0 = 0 /\
470    fusc 1 = 1 /\
471    fusc (2 * n) = fusc(n) /\
472    fusc (2 * n + 1) = fusc(n) + fusc(n + 1)`,
473   REWRITE_TAC[fusc_def] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
474   MP_TAC(INST [`0`,`n:num`] fusc_def) THEN ARITH_TAC);;
475
476 let binom = define
477  `(!n. binom(n,0) = 1) /\
478   (!k. binom(0,SUC(k)) = 0) /\
479   (!n k. binom(SUC(n),SUC(k)) = binom(n,SUC(k)) + binom(n,k))`;;
480
481 let BINOM_LT = prove
482  (`!n k. n < k ==> (binom(n,k) = 0)`,
483   INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[binom; ARITH; LT_SUC; LT] THEN
484   ASM_SIMP_TAC[ARITH_RULE `n < k ==> n < SUC(k)`; ARITH]);;
485
486 let BINOM_REFL = prove
487  (`!n. binom(n,n) = 1`,
488   INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);;
489
490 let BINOM_FACT = prove
491  (`!n k. FACT n * FACT k * binom(n+k,k) = FACT(n + k)`,
492   INDUCT_TAC THEN REWRITE_TAC[FACT; ADD_CLAUSES; MULT_CLAUSES; BINOM_REFL] THEN
493   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; FACT; MULT_CLAUSES; binom] THEN
494   FIRST_X_ASSUM(MP_TAC o SPEC `SUC k`) THEN POP_ASSUM MP_TAC THEN
495   REWRITE_TAC[ADD_CLAUSES; FACT; binom] THEN CONV_TAC NUM_RING);;
496
497 let BINOMIAL_THEOREM = prove
498  (`!n. (x + y) EXP n = nsum(0..n) (\k. binom(n,k) * x EXP k * y EXP (n - k))`,
499   INDUCT_TAC THEN ASM_REWRITE_TAC[EXP] THEN
500   REWRITE_TAC[NSUM_SING_NUMSEG; binom; SUB_REFL; EXP; MULT_CLAUSES] THEN
501   SIMP_TAC[NSUM_CLAUSES_LEFT; ADD1; ARITH_RULE `0 <= n + 1`; NSUM_OFFSET] THEN
502   ASM_REWRITE_TAC[EXP; binom; GSYM ADD1; GSYM NSUM_LMUL] THEN
503   REWRITE_TAC[RIGHT_ADD_DISTRIB; NSUM_ADD_NUMSEG; MULT_CLAUSES; SUB_0] THEN
504   MATCH_MP_TAC(ARITH_RULE `a = e /\ b = c + d ==> a + b = c + d + e`) THEN
505   CONJ_TAC THENL [REWRITE_TAC[MULT_AC; SUB_SUC]; REWRITE_TAC[GSYM EXP]] THEN
506   SIMP_TAC[ADD1; SYM(REWRITE_CONV[NSUM_OFFSET]`nsum(m+1..n+1) (\i. f i)`)] THEN
507   REWRITE_TAC[NSUM_CLAUSES_NUMSEG; GSYM ADD1; LE_SUC; LE_0] THEN
508   SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0] THEN
509   SIMP_TAC[BINOM_LT; LT; MULT_CLAUSES; ADD_CLAUSES; SUB_0; EXP; binom] THEN
510   SIMP_TAC[ARITH; ARITH_RULE `k <= n ==> SUC n - k = SUC(n - k)`; EXP] THEN
511   REWRITE_TAC[MULT_AC]);;
512
513 (* ========================================================================= *)
514 (* Sets and functions                                                        *)
515 (* ========================================================================= *)
516
517 let SURJECTIVE_IFF_RIGHT_INVERSE = prove
518  (`(!y. ?x. g x = y) <=> (?f. g o f = I)`,
519   REWRITE_TAC[FUN_EQ_THM; o_DEF; I_DEF] THEN MESON_TAC[]);;
520
521 let INJECTIVE_IFF_LEFT_INVERSE = prove
522  (`(!x y. f x = f y ==> x = y) <=> (?g. g o f = I)`,
523   let lemma = MESON[]
524    `(!x x'. f x = f x' ==> x = x') <=> (!y:B. ?u:A. !x. f x = y ==> u = x)` in
525   REWRITE_TAC[lemma; FUN_EQ_THM; o_DEF; I_DEF] THEN MESON_TAC[]);;
526
527 let cantor = new_definition
528  `cantor(x,y) = ((x + y) EXP 2 + 3 * x + y) DIV 2`;;
529
530 (**** Needs external SDP solver
531
532 needs "Examples/sos.ml";;
533
534 let CANTOR_LEMMA = prove
535  (`cantor(x,y) = cantor(x',y') ==> x + y = x' + y'`,
536   REWRITE_TAC[cantor] THEN CONV_TAC SOS_RULE);;
537
538 ****)
539
540 let CANTOR_LEMMA_LEMMA = prove
541  (`x + y < x' + y' ==> cantor(x,y) < cantor(x',y')`,
542   REWRITE_TAC[ARITH_RULE `x + y < z <=> x + y + 1 <= z`] THEN DISCH_TAC THEN
543   REWRITE_TAC[cantor; ARITH_RULE `3 * x + y = (x + y) + 2 * x`] THEN
544   MATCH_MP_TAC(ARITH_RULE `x + 2 <= y ==> x DIV 2 < y DIV 2`) THEN
545   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `(x + y + 1) EXP 2 + (x + y + 1)` THEN
546   CONJ_TAC THENL [ARITH_TAC; ALL_TAC] THEN
547   MATCH_MP_TAC(ARITH_RULE `a:num <= b /\ c <= d ==> a + c <= b + d + e`) THEN
548   ASM_SIMP_TAC[EXP_2; LE_MULT2]);;
549
550 let CANTOR_LEMMA = prove
551  (`cantor(x,y) = cantor(x',y') ==> x + y = x' + y'`,
552   MESON_TAC[LT_CASES; LT_REFL; CANTOR_LEMMA_LEMMA]);;
553
554 let CANTOR_INJ = prove
555  (`!w z. cantor w = cantor z ==> w = z`,
556   REWRITE_TAC[FORALL_PAIR_THM; PAIR_EQ] THEN REPEAT GEN_TAC THEN
557   DISCH_THEN(fun th -> MP_TAC th THEN ASSUME_TAC(MATCH_MP CANTOR_LEMMA th)) THEN
558   ASM_REWRITE_TAC[cantor; ARITH_RULE `3 * x + y = (x + y) + 2 * x`] THEN
559   REWRITE_TAC[ARITH_RULE `(a + b + 2 * x) DIV 2 = (a + b) DIV 2 + x`] THEN
560   POP_ASSUM MP_TAC THEN ARITH_TAC);;
561
562 let CANTOR_THM = prove
563  (`~(?f:(A->bool)->A. (!x y. f(x) = f(y) ==> x = y))`,
564   REWRITE_TAC[INJECTIVE_IFF_LEFT_INVERSE; FUN_EQ_THM; I_DEF; o_DEF] THEN
565   STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `\x:A. ~(g x x)`) THEN
566   MESON_TAC[]);;
567
568 (* ========================================================================= *)
569 (* Inductive datatypes                                                       *)
570 (* ========================================================================= *)
571
572 let line_INDUCT,line_RECURSION = define_type
573  "line = Line_1 | Line_2 | Line_3 | Line_4 |
574          Line_5 | Line_6 | Line_7";;
575
576 let point_INDUCT,point_RECURSION = define_type
577  "point = Point_1 | Point_2 | Point_3 | Point_4 |
578           Point_5 | Point_6 | Point_7";;
579
580 let fano_incidence =
581   [1,1; 1,2; 1,3; 2,1; 2,4; 2,5; 3,1; 3,6; 3,7; 4,2; 4,4;
582    4,6; 5,2; 5,5; 5,7; 6,3; 6,4; 6,7; 7,3; 7,5; 7,6];;
583
584 let fano_point i = mk_const("Point_"^string_of_int i,[]);;
585 let fano_line i = mk_const("Line_"^string_of_int i,[]);;
586 let p = `p:point` and l = `l:line` ;;
587
588 let fano_clause (i,j) = mk_conj(mk_eq(p,fano_point i),mk_eq(l,fano_line j));;
589
590 parse_as_infix("ON",(11,"right"));;
591
592 let ON = new_definition
593  (mk_eq(`((ON):point->line->bool) p l`,
594         list_mk_disj(map fano_clause fano_incidence)));;
595
596 let ON_CLAUSES = prove
597  (list_mk_conj(allpairs
598     (fun i j -> mk_eq(mk_comb(mk_comb(`(ON)`,fano_point i),fano_line j),
599                       if mem (i,j) fano_incidence then `T` else `F`))
600     (1--7) (1--7)),
601   REWRITE_TAC[ON; distinctness "line"; distinctness "point"]);;
602
603 let FORALL_POINT = prove
604  (`(!p. P p) <=> P Point_1 /\ P Point_2 /\ P Point_3 /\ P Point_4 /\
605                  P Point_5 /\ P Point_6 /\ P Point_7`,
606   EQ_TAC THENL [SIMP_TAC[]; REWRITE_TAC[point_INDUCT]]);;
607
608 let FORALL_LINE = prove
609  (`(!p. P p) <=> P Line_1 /\ P Line_2 /\ P Line_3 /\ P Line_4 /\
610                  P Line_5 /\ P Line_6 /\ P Line_7`,
611   EQ_TAC THENL [SIMP_TAC[]; REWRITE_TAC[line_INDUCT]]);;
612
613 let EXISTS_POINT = prove
614  (`(?p. P p) <=> P Point_1 \/ P Point_2 \/ P Point_3 \/ P Point_4 \/
615                  P Point_5 \/ P Point_6 \/ P Point_7`,
616   MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
617   REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_POINT]);;
618
619 let EXISTS_LINE = prove
620  (`(?p. P p) <=> P Line_1 \/ P Line_2 \/ P Line_3 \/ P Line_4 \/
621                  P Line_5 \/ P Line_6 \/ P Line_7`,
622   MATCH_MP_TAC(TAUT `(~p <=> ~q) ==> (p <=> q)`) THEN
623   REWRITE_TAC[DE_MORGAN_THM; NOT_EXISTS_THM; FORALL_LINE]);;
624
625 let FANO_TAC =
626   GEN_REWRITE_TAC DEPTH_CONV
627    [FORALL_POINT; EXISTS_LINE; EXISTS_POINT; FORALL_LINE] THEN
628   GEN_REWRITE_TAC DEPTH_CONV
629    (basic_rewrites() @
630     [ON_CLAUSES; distinctness "point"; distinctness "line"]);;
631
632 let FANO_RULE tm = prove(tm,FANO_TAC);;
633
634 let AXIOM_1 = FANO_RULE
635 `!p p'. ~(p = p') ==> ?l. p ON l /\ p' ON l /\
636                           !l'. p ON l' /\ p' ON l' ==> l' = l`;;
637
638 let AXIOM_2 = FANO_RULE
639  `!l l'. ?p. p ON l /\ p ON l'`;;
640
641 let AXIOM_3 = FANO_RULE
642  `?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
643              ~(?l. p ON l /\ p' ON l /\ p'' ON l)`;;
644
645 let AXIOM_4 = FANO_RULE
646   `!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
647                   p ON l /\ p' ON l /\ p'' ON l`;;
648
649 (* ========================================================================= *)
650 (* Semantics of programming languages                                        *)
651 (* ========================================================================= *)
652
653 let string_INDUCT,string_RECURSION =
654   define_type "string = String (int list)";;
655
656 let expression_INDUCT,expression_RECURSION = define_type
657 "expression = Literal num
658             | Variable string
659             | Plus expression expression
660             | Times expression expression";;
661
662 let command_INDUCT,command_RECURSION = define_type
663   "command = Assign string expression
664            | Sequence command command
665            | If expression command command
666            | While expression command";;
667
668 parse_as_infix(";;",(18,"right"));;
669 parse_as_infix(":=",(20,"right"));;
670 override_interface(";;",`Sequence`);;
671 override_interface(":=",`Assign`);;
672 overload_interface("+",`Plus`);;
673 overload_interface("*",`Times`);;
674
675 let value = define
676  `(value (Literal n) s = n) /\
677   (value (Variable x) s = s(x)) /\
678   (value (e1 + e2) s = value e1 s + value e2 s) /\
679   (value (e1 * e2) s = value e1 s * value e2 s)`;;
680
681 let sem_RULES,sem_INDUCT,sem_CASES = new_inductive_definition
682   `(!x e s s'. s'(x) = value e s /\ (!y. ~(y = x) ==> s'(y) = s(y))
683                ==> sem (x := e) s s') /\
684    (!c1 c2 s s' s''. sem(c1) s s' /\ sem(c2) s' s'' ==> sem(c1 ;; c2) s s'') /\
685    (!e c1 c2 s s'. ~(value e s = 0) /\ sem(c1) s s' ==> sem(If e c1 c2) s s') /\
686    (!e c1 c2 s s'. value e s = 0 /\ sem(c2) s s' ==> sem(If e c1 c2) s s') /\
687    (!e c s. value e s = 0 ==> sem(While e c) s s) /\
688    (!e c s s' s''. ~(value e s = 0) /\ sem(c) s s' /\ sem(While e c) s' s''
689                    ==> sem(While e c) s s'')`;;
690
691 (**** Fails
692   define
693    `sem(While e c) s s' <=> if value e s = 0 then (s' = s)
694                             else ?s''. sem c s s'' /\ sem(While e c) s'' s'`;;
695 ****)
696
697 let DETERMINISM = prove
698  (`!c s s' s''. sem c s s' /\ sem c s s'' ==> (s' = s'')`,
699   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
700   MATCH_MP_TAC sem_INDUCT THEN REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
701   DISCH_TAC THEN ONCE_REWRITE_TAC[sem_CASES] THEN
702   REWRITE_TAC[distinctness "command"; injectivity "command"] THEN
703   REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]);;
704
705 let wlp = new_definition
706  `wlp c q s <=> !s'. sem c s s' ==> q s'`;;
707
708 let terminates = new_definition
709  `terminates c s <=> ?s'. sem c s s'`;;
710
711 let wp = new_definition
712  `wp c q s <=> terminates c s /\ wlp c q s`;;
713
714 let WP_TOTAL = prove
715  (`!c. (wp c EMPTY = EMPTY)`,
716   REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; EMPTY] THEN MESON_TAC[]);;
717
718 let WP_MONOTONIC = prove
719  (`q SUBSET r ==> wp c q SUBSET wp c r`,
720   REWRITE_TAC[SUBSET; IN; wp; wlp; terminates] THEN MESON_TAC[]);;
721
722 let WP_DISJUNCTIVE = prove
723  (`(wp c p) UNION (wp c q) = wp c (p UNION q)`,
724   REWRITE_TAC[FUN_EQ_THM; IN; wp; wlp; IN_ELIM_THM; UNION; terminates] THEN
725   MESON_TAC[DETERMINISM]);;
726
727 let WP_SEQ = prove
728  (`!c1 c2 q. wp (c1 ;; c2) = wp c1 o wp c2`,
729   REWRITE_TAC[wp; wlp; terminates; FUN_EQ_THM; o_THM] THEN REPEAT GEN_TAC THEN
730   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [sem_CASES] THEN
731   REWRITE_TAC[injectivity "command"; distinctness "command"] THEN
732   MESON_TAC[DETERMINISM]);;
733
734 let correct = new_definition
735  `correct p c q <=> p SUBSET (wp c q)`;;
736
737 let CORRECT_PRESTRENGTH = prove
738  (`!p p' c q. p SUBSET p' /\ correct p' c q ==> correct p c q`,
739   REWRITE_TAC[correct; SUBSET_TRANS]);;
740
741 let CORRECT_POSTWEAK = prove
742  (`!p c q q'. correct p c q' /\ q' SUBSET q ==> correct p c q`,
743   REWRITE_TAC[correct] THEN MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;
744
745 let CORRECT_SEQ = prove
746  (`!p q r c1 c2.
747         correct p c1 r /\ correct r c2 q ==> correct p (c1 ;; c2) q`,
748   REWRITE_TAC[correct; WP_SEQ; o_THM] THEN
749   MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;
750
751 (* ------------------------------------------------------------------------- *)
752 (* Need a fresh HOL session here; now doing shallow embedding.               *)
753 (* ------------------------------------------------------------------------- *)
754
755 let assign = new_definition
756   `Assign (f:S->S) (q:S->bool) = q o f`;;
757
758 parse_as_infix(";;",(18,"right"));;
759
760 let sequence = new_definition
761  `(c1:(S->bool)->(S->bool)) ;; (c2:(S->bool)->(S->bool)) = c1 o c2`;;
762
763 let if_def = new_definition
764  `If e (c:(S->bool)->(S->bool)) q = {s | if e s then c q s else q s}`;;
765
766 let ite_def = new_definition
767  `Ite e (c1:(S->bool)->(S->bool)) c2 q =
768     {s | if e s then c1 q s else c2 q s}`;;
769
770 let while_RULES,while_INDUCT,while_CASES = new_inductive_definition
771          `!q s. If e (c ;; while e c) q s ==> while e c q s`;;
772
773 let while_def = new_definition
774  `While e c q =
775     {s | !w. (!s:S. (if e(s) then c w s else q s) ==> w s) ==> w s}`;;
776
777 let monotonic = new_definition
778  `monotonic c <=> !q q'. q SUBSET q' ==> (c q) SUBSET (c q')`;;
779
780 let MONOTONIC_ASSIGN = prove
781  (`monotonic (Assign f)`,
782   SIMP_TAC[monotonic; assign; SUBSET; o_THM; IN]);;
783
784 let MONOTONIC_IF = prove
785  (`monotonic c ==> monotonic (If e c)`,
786   REWRITE_TAC[monotonic; if_def] THEN SET_TAC[]);;
787
788 let MONOTONIC_ITE = prove
789  (`monotonic c1 /\ monotonic c2 ==> monotonic (Ite e c1 c2)`,
790   REWRITE_TAC[monotonic; ite_def] THEN SET_TAC[]);;
791
792 let MONOTONIC_SEQ = prove
793  (`monotonic c1 /\ monotonic c2 ==> monotonic (c1 ;; c2)`,
794   REWRITE_TAC[monotonic; sequence; o_THM] THEN SET_TAC[]);;
795
796 let MONOTONIC_WHILE = prove
797  (`monotonic c ==> monotonic(While e c)`,
798   REWRITE_TAC[monotonic; while_def] THEN SET_TAC[]);;
799
800 let WHILE_THM = prove
801  (`!e c q:S->bool.
802     monotonic c
803     ==> (!s. If e (c ;; While e c) q s ==> While e c q s) /\
804         (!w'. (!s. If e (c ;; (\q. w')) q s ==> w' s)
805               ==> (!a. While e c q a ==> w' a)) /\
806         (!s. While e c q s <=> If e (c ;; While e c) q s)`,
807   REPEAT GEN_TAC THEN DISCH_TAC THEN
808   (MP_TAC o GEN_ALL o DISCH_ALL o derive_nonschematic_inductive_relations)
809    `!s:S. (if e s then c w s else q s) ==> w s` THEN
810   REWRITE_TAC[if_def; sequence; o_THM; IN_ELIM_THM; IMP_IMP] THEN
811   DISCH_THEN MATCH_MP_TAC THEN
812   REWRITE_TAC[FUN_EQ_THM; while_def; IN_ELIM_THM] THEN
813   POP_ASSUM MP_TAC THEN REWRITE_TAC[monotonic] THEN SET_TAC[]);;
814
815 let WHILE_FIX = prove
816  (`!e c. monotonic c ==> (While e c = If e (c ;; While e c))`,
817   REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[WHILE_THM]);;
818
819 let correct = new_definition
820  `correct p c q <=> p SUBSET (c q)`;;
821
822 let CORRECT_PRESTRENGTH = prove
823  (`!p p' c q. p SUBSET p' /\ correct p' c q ==> correct p c q`,
824   REWRITE_TAC[correct; SUBSET_TRANS]);;
825
826 let CORRECT_POSTWEAK = prove
827  (`!p c q q'. monotonic c /\ correct p c q' /\ q' SUBSET q ==> correct p c q`,
828   REWRITE_TAC[correct; monotonic] THEN SET_TAC[]);;
829
830 let CORRECT_ASSIGN = prove
831  (`!p f q. (p SUBSET (q o f)) ==> correct p (Assign f) q`,
832   REWRITE_TAC[correct; assign]);;
833
834 let CORRECT_SEQ = prove
835  (`!p q r c1 c2.
836         monotonic c1 /\ correct p c1 r /\ correct r c2 q
837         ==> correct p (c1 ;; c2) q`,
838   REWRITE_TAC[correct; sequence; monotonic; o_THM] THEN SET_TAC[]);;
839
840 let CORRECT_ITE = prove
841  (`!p e c1 c2 q.
842        correct (p INTER e) c1 q /\ correct (p INTER (UNIV DIFF e)) c2 q
843        ==> correct p (Ite e c1 c2) q`,
844   REWRITE_TAC[correct; ite_def] THEN SET_TAC[]);;
845
846 let CORRECT_IF = prove
847  (`!p e c q.
848        correct (p INTER e) c q /\ p INTER (UNIV DIFF e) SUBSET q
849        ==> correct p (If e c) q`,
850   REWRITE_TAC[correct; if_def] THEN SET_TAC[]);;
851
852 let CORRECT_WHILE = prove
853  (`!(<<) p c q e invariant.
854       monotonic c /\
855       WF(<<) /\
856       p SUBSET invariant /\
857       (UNIV DIFF e) INTER invariant SUBSET q /\
858       (!X:S. correct (invariant INTER e INTER (\s. X = s)) c
859                      (invariant INTER (\s. s << X)))
860       ==> correct p (While e c) q`,
861   REWRITE_TAC[correct; SUBSET; IN_INTER; IN_UNIV; IN_DIFF; IN] THEN
862   REPEAT GEN_TAC THEN STRIP_TAC THEN
863   SUBGOAL_THEN `!s:S. invariant s ==> While e c q s` MP_TAC THENL
864    [ALL_TAC; ASM_MESON_TAC[]] THEN
865   FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[WF_IND]) THEN
866   X_GEN_TAC `s:S` THEN REPEAT DISCH_TAC THEN
867   FIRST_ASSUM(fun th -> ONCE_REWRITE_TAC[MATCH_MP WHILE_FIX th]) THEN
868   REWRITE_TAC[if_def; sequence; o_THM; IN_ELIM_THM] THEN
869   COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
870   FIRST_X_ASSUM(MP_TAC o SPECL [`s:S`; `s:S`]) THEN ASM_REWRITE_TAC[] THEN
871   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [monotonic]) THEN
872   REWRITE_TAC[SUBSET; IN; RIGHT_IMP_FORALL_THM] THEN
873   DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC[INTER; IN_ELIM_THM; IN]);;
874
875 let assert_def = new_definition
876  `assert (p:S->bool) (q:S->bool) = q`;;
877
878 let variant_def = new_definition
879  `variant ((<<):S->S->bool) (q:S->bool) = q`;;
880
881 let CORRECT_SEQ_VC = prove
882  (`!p q r c1 c2.
883         monotonic c1 /\ correct p c1 r /\ correct r c2 q
884         ==> correct p (c1 ;; assert r ;; c2) q`,
885   REWRITE_TAC[correct; sequence; monotonic; assert_def; o_THM] THEN SET_TAC[]);;
886
887 let CORRECT_WHILE_VC = prove
888  (`!(<<) p c q e invariant.
889       monotonic c /\
890       WF(<<) /\
891       p SUBSET invariant /\
892       (UNIV DIFF e) INTER invariant SUBSET q /\
893       (!X:S. correct (invariant INTER e INTER (\s. X = s)) c
894                      (invariant INTER (\s. s << X)))
895       ==> correct p (While e (assert invariant ;; variant(<<) ;; c)) q`,
896   REPEAT STRIP_TAC THEN
897   REWRITE_TAC[sequence; variant_def; assert_def; o_DEF; ETA_AX] THEN
898   ASM_MESON_TAC[CORRECT_WHILE]);;
899
900 let MONOTONIC_ASSERT = prove
901  (`monotonic (assert p)`,
902   REWRITE_TAC[assert_def; monotonic]);;
903
904 let MONOTONIC_VARIANT = prove
905  (`monotonic (variant p)`,
906   REWRITE_TAC[variant_def; monotonic]);;
907
908 let MONO_TAC =
909   REPEAT(MATCH_MP_TAC MONOTONIC_WHILE ORELSE
910          (MAP_FIRST MATCH_MP_TAC
911            [MONOTONIC_SEQ; MONOTONIC_IF; MONOTONIC_ITE] THEN CONJ_TAC)) THEN
912   MAP_FIRST MATCH_ACCEPT_TAC
913    [MONOTONIC_ASSIGN; MONOTONIC_ASSERT; MONOTONIC_VARIANT];;
914
915 let VC_TAC =
916   FIRST
917    [MATCH_MP_TAC CORRECT_SEQ_VC THEN CONJ_TAC THENL [MONO_TAC; CONJ_TAC];
918     MATCH_MP_TAC CORRECT_ITE THEN CONJ_TAC;
919     MATCH_MP_TAC CORRECT_IF THEN CONJ_TAC;
920     MATCH_MP_TAC CORRECT_WHILE_VC THEN REPEAT CONJ_TAC THENL
921      [MONO_TAC; TRY(MATCH_ACCEPT_TAC WF_MEASURE); ALL_TAC; ALL_TAC;
922       REWRITE_TAC[FORALL_PAIR_THM; MEASURE] THEN REPEAT GEN_TAC];
923     MATCH_MP_TAC CORRECT_ASSIGN];;
924
925 needs "Library/prime.ml";;
926
927 (* ------------------------------------------------------------------------- *)
928 (* x = m, y = n;                                                             *)
929 (* while (!(x == 0 || y == 0))                                               *)
930 (*  { if (x < y) y = y - x;                                                  *)
931 (*    else x = x - y;                                                        *)
932 (*  }                                                                        *)
933 (* if (x == 0) x = y;                                                        *)
934 (* ------------------------------------------------------------------------- *)
935
936 g `correct
937     (\(m,n,x,y). T)
938     (Assign (\(m,n,x,y). m,n,m,n) ;;         // x,y := m,n
939      assert (\(m,n,x,y). x = m /\ y = n) ;;
940      While (\(m,n,x,y). ~(x = 0 \/ y = 0))
941       (assert (\(m,n,x,y). gcd(x,y) = gcd(m,n)) ;;
942        variant(MEASURE(\(m,n,x,y). x + y)) ;;
943        Ite (\(m,n,x,y). x < y)
944            (Assign (\(m,n,x,y). m,n,x,y - x))
945            (Assign (\(m,n,x,y). m,n,x - y,y))) ;;
946      assert (\(m,n,x,y). (x = 0 \/ y = 0) /\ gcd(x,y) = gcd(m,n)) ;;
947      If (\(m,n,x,y). x = 0) (Assign (\(m,n,x,y). (m,n,y,y))))
948   (\(m,n,x,y). gcd(m,n) = x)`;;
949
950 e(REPEAT VC_TAC);;
951
952 b();;
953 e(REPEAT VC_TAC THEN REWRITE_TAC[SUBSET; FORALL_PAIR_THM] THEN
954   MAP_EVERY X_GEN_TAC [`m:num`; `n:num`; `x:num`; `y:num`] THEN
955   REWRITE_TAC[IN; INTER; UNIV; DIFF; o_DEF; IN_ELIM_THM; PAIR_EQ] THEN
956   CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV) THEN SIMP_TAC[]);;
957
958 e(SIMP_TAC[GCD_SUB; LT_IMP_LE]);;
959 e ARITH_TAC;;
960
961 e(SIMP_TAC[GCD_SUB; NOT_LT] THEN ARITH_TAC);;
962
963 e(MESON_TAC[GCD_0]);;
964
965 e(MESON_TAC[GCD_0; GCD_SYM]);;
966
967 parse_as_infix("refines",(12,"right"));;
968
969 let refines = new_definition
970  `c2 refines c1 <=> !q. c1(q) SUBSET c2(q)`;;
971
972 let REFINES_REFL = prove
973  (`!c. c refines c`,
974   REWRITE_TAC[refines; SUBSET_REFL]);;
975
976 let REFINES_TRANS = prove
977  (`!c1 c2 c3. c3 refines c2 /\ c2 refines c1 ==> c3 refines c1`,
978   REWRITE_TAC[refines] THEN MESON_TAC[SUBSET_TRANS]);;
979
980 let REFINES_CORRECT = prove
981  (`correct p c1 q /\ c2 refines c1 ==> correct p c2 q`,
982   REWRITE_TAC[correct; refines] THEN MESON_TAC[SUBSET_TRANS]);;
983
984 let REFINES_WHILE = prove
985  (`c' refines c ==> While e c' refines While e c`,
986   REWRITE_TAC[refines; while_def; SUBSET; IN_ELIM_THM; IN] THEN MESON_TAC[]);;
987
988 let specification = new_definition
989  `specification(p,q) r = if q SUBSET r then p else {}`;;
990
991 let REFINES_SPECIFICATION = prove
992  (`c refines specification(p,q) ==> correct p c q`,
993   REWRITE_TAC[specification; correct; refines] THEN
994   MESON_TAC[SUBSET_REFL; SUBSET_EMPTY]);;
995
996 (* ========================================================================= *)
997 (* Number theory                                                             *)
998 (* ========================================================================= *)
999
1000 needs "Library/prime.ml";;
1001 needs "Library/pocklington.ml";;
1002 needs "Library/binomial.ml";;
1003
1004 prioritize_num();;
1005
1006 let FERMAT_PRIME_CONV n =
1007   let tm = subst [mk_small_numeral n,`x:num`] `prime(2 EXP (2 EXP x) + 1)` in
1008   (RAND_CONV NUM_REDUCE_CONV THENC PRIME_CONV) tm;;
1009
1010 FERMAT_PRIME_CONV 0;;
1011 FERMAT_PRIME_CONV 1;;
1012 FERMAT_PRIME_CONV 2;;
1013 FERMAT_PRIME_CONV 3;;
1014 FERMAT_PRIME_CONV 4;;
1015 FERMAT_PRIME_CONV 5;;
1016 FERMAT_PRIME_CONV 6;;
1017 FERMAT_PRIME_CONV 7;;
1018 FERMAT_PRIME_CONV 8;;
1019
1020 let CONG_TRIVIAL = prove
1021  (`!x y. n divides x /\ n divides y ==> (x == y) (mod n)`,
1022   MESON_TAC[CONG_0; CONG_SYM; CONG_TRANS]);;
1023
1024 let LITTLE_CHECK_CONV tm =
1025   EQT_ELIM((RATOR_CONV(LAND_CONV NUM_EXP_CONV) THENC CONG_CONV) tm);;
1026
1027 LITTLE_CHECK_CONV `(9 EXP 8 == 9) (mod 3)`;;
1028 LITTLE_CHECK_CONV `(9 EXP 3 == 9) (mod 3)`;;
1029 LITTLE_CHECK_CONV `(10 EXP 7 == 10) (mod 7)`;;
1030 LITTLE_CHECK_CONV `(2 EXP 7 == 2) (mod 7)`;;
1031 LITTLE_CHECK_CONV `(777 EXP 13 == 777) (mod 13)`;;
1032
1033 let DIVIDES_FACT_PRIME = prove
1034  (`!p. prime p ==> !n. p divides (FACT n) <=> p <= n`,
1035   GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[FACT; LE] THENL
1036    [ASM_MESON_TAC[DIVIDES_ONE; PRIME_0; PRIME_1];
1037     ASM_MESON_TAC[PRIME_DIVPROD_EQ; DIVIDES_LE; NOT_SUC; DIVIDES_REFL;
1038                   ARITH_RULE `~(p <= n) /\ p <= SUC n ==> p = SUC n`]]);;
1039
1040 let DIVIDES_BINOM_PRIME = prove
1041  (`!n p. prime p /\ 0 < n /\ n < p ==> p divides binom(p,n)`,
1042   REPEAT STRIP_TAC THEN
1043   MP_TAC(AP_TERM `(divides) p` (SPECL [`p - n`; `n:num`] BINOM_FACT)) THEN
1044   ASM_SIMP_TAC[DIVIDES_FACT_PRIME; PRIME_DIVPROD_EQ; SUB_ADD; LT_IMP_LE] THEN
1045   ASM_REWRITE_TAC[GSYM NOT_LT; LT_REFL] THEN
1046   ASM_SIMP_TAC[ARITH_RULE `0 < n /\ n < p ==> p - n < p`]);;
1047
1048 let DIVIDES_NSUM = prove
1049  (`!m n. (!i. m <= i /\ i <= n ==> p divides f(i)) ==> p divides nsum(m..n) f`,
1050   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN
1051   ASM_MESON_TAC[LE; LE_TRANS; DIVIDES_0; DIVIDES_ADD; LE_REFL]);;
1052
1053 let FLT_LEMMA = prove
1054  (`!p a b. prime p ==> ((a + b) EXP p == a EXP p + b EXP p) (mod p)`,
1055   REPEAT STRIP_TAC THEN REWRITE_TAC[BINOMIAL_THEOREM] THEN
1056   SUBGOAL_THEN `1 <= p /\ 0 < p` STRIP_ASSUME_TAC THENL
1057    [FIRST_ASSUM(MP_TAC o MATCH_MP PRIME_IMP_NZ) THEN ARITH_TAC; ALL_TAC] THEN
1058   ASM_SIMP_TAC[NSUM_CLAUSES_LEFT; LE_0; ARITH; NSUM_CLAUSES_RIGHT] THEN
1059   REWRITE_TAC[SUB_0; SUB_REFL; EXP; binom; BINOM_REFL; MULT_CLAUSES] THEN
1060   GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a + b = (b + 0) + a`] THEN
1061   REPEAT(MATCH_MP_TAC CONG_ADD THEN REWRITE_TAC[CONG_REFL]) THEN
1062   REWRITE_TAC[CONG_0] THEN MATCH_MP_TAC DIVIDES_NSUM THEN
1063   ASM_MESON_TAC[DIVIDES_RMUL; DIVIDES_BINOM_PRIME; ARITH_RULE
1064    `0 < p /\ 1 <= i /\ i <= p - 1 ==> 0 < i /\ i < p`]);;
1065
1066 let FERMAT_LITTLE = prove
1067  (`!p a. prime p ==> (a EXP p == a) (mod p)`,
1068   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
1069   INDUCT_TAC THENL
1070    [ASM_MESON_TAC[EXP_EQ_0; CONG_REFL; PRIME_0];
1071     ASM_MESON_TAC[ADD1; FLT_LEMMA; EXP_ONE; CONG_ADD; CONG_TRANS; CONG_REFL]]);;
1072
1073 let FERMAT_LITTLE_COPRIME = prove
1074  (`!p a. prime p /\ coprime(a,p) ==> (a EXP (p - 1) == 1) (mod p)`,
1075   REPEAT STRIP_TAC THEN MATCH_MP_TAC CONG_MULT_LCANCEL THEN
1076   EXISTS_TAC `a:num` THEN ASM_REWRITE_TAC[GSYM(CONJUNCT2 EXP)] THEN
1077   ASM_SIMP_TAC[PRIME_IMP_NZ; ARITH_RULE `~(p = 0) ==> SUC(p - 1) = p`] THEN
1078   ASM_SIMP_TAC[FERMAT_LITTLE; MULT_CLAUSES]);;
1079
1080 let FERMAT_LITTLE_VARIANT = prove
1081  (`!p a. prime p ==> (a EXP (1 + m * (p - 1)) == a) (mod p)`,
1082   REPEAT STRIP_TAC THEN
1083   FIRST_ASSUM(DISJ_CASES_TAC o SPEC `a:num` o MATCH_MP PRIME_COPRIME_STRONG)
1084   THENL [ASM_MESON_TAC[CONG_TRIVIAL; ADD_AC; ADD1; DIVIDES_REXP_SUC];
1085          ALL_TAC] THEN
1086   GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `a = a * 1`] THEN
1087   REWRITE_TAC[EXP_ADD; EXP_1] THEN MATCH_MP_TAC CONG_MULT THEN
1088   REWRITE_TAC[GSYM EXP_EXP; CONG_REFL] THEN
1089   ASM_MESON_TAC[COPRIME_SYM; COPRIME_EXP; PHI_PRIME; FERMAT_LITTLE_COPRIME]);;
1090
1091 let RSA = prove
1092  (`prime p /\ prime q /\ ~(p = q) /\
1093    (d * e == 1) (mod ((p - 1) * (q - 1))) /\
1094    plaintext < p * q /\ (ciphertext = (plaintext EXP e) MOD (p * q))
1095    ==> (plaintext = (ciphertext EXP d) MOD (p * q))`,
1096   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1097   ASM_SIMP_TAC[MOD_EXP_MOD; MULT_EQ_0; PRIME_IMP_NZ; EXP_EXP] THEN
1098   SUBGOAL_THEN `(plaintext == plaintext EXP (e * d)) (mod (p * q))` MP_TAC THENL
1099    [ALL_TAC; ASM_SIMP_TAC[CONG; MULT_EQ_0; PRIME_IMP_NZ; MOD_LT]] THEN
1100   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
1101   FIRST_X_ASSUM(DISJ_CASES_TAC o GEN_REWRITE_RULE I [CONG_TO_1]) THENL
1102    [ASM_MESON_TAC[MULT_EQ_1; ARITH_RULE `p - 1 = 1 <=> p = 2`]; ALL_TAC] THEN
1103   MATCH_MP_TAC CONG_CHINESE THEN ASM_SIMP_TAC[DISTINCT_PRIME_COPRIME] THEN
1104   ASM_MESON_TAC[FERMAT_LITTLE_VARIANT; MULT_AC; CONG_SYM]);;
1105
1106 (* ========================================================================= *)
1107 (* Real analysis                                                             *)
1108 (* ========================================================================= *)
1109
1110 needs "Library/analysis.ml";;
1111 needs "Library/transc.ml";;
1112
1113 let cheb = define
1114  `(!x. cheb 0 x = &1) /\
1115   (!x. cheb 1 x = x) /\
1116   (!n x. cheb (n + 2) x = &2 * x * cheb (n + 1) x - cheb n x)`;;
1117
1118 let CHEB_INDUCT = prove
1119  (`!P. P 0 /\ P 1 /\ (!n. P n /\ P(n + 1) ==> P(n + 2)) ==> !n. P n`,
1120   GEN_TAC THEN STRIP_TAC THEN
1121   SUBGOAL_THEN `!n. P n /\ P(n + 1)` (fun th -> MESON_TAC[th]) THEN
1122   INDUCT_TAC THEN ASM_SIMP_TAC[ADD1; GSYM ADD_ASSOC] THEN
1123   ASM_SIMP_TAC[ARITH]);;
1124
1125 let CHEB_COS = prove
1126  (`!n x. cheb n (cos x) = cos(&n * x)`,
1127   MATCH_MP_TAC CHEB_INDUCT THEN
1128   REWRITE_TAC[cheb; REAL_MUL_LZERO; REAL_MUL_LID; COS_0] THEN
1129   REPEAT STRIP_TAC THEN
1130   ASM_REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_MUL_LID; REAL_ADD_RDISTRIB] THEN
1131   REWRITE_TAC[COS_ADD; COS_DOUBLE; SIN_DOUBLE] THEN
1132   MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN CONV_TAC REAL_RING);;
1133
1134 let CHEB_RIPPLE = prove
1135  (`!x. abs(x) <= &1 ==> abs(cheb n x) <= &1`,
1136   REWRITE_TAC[GSYM REAL_BOUNDS_LE] THEN
1137   MESON_TAC[CHEB_COS; ACS_COS; COS_BOUNDS]);;
1138
1139 let NUM_ADD2_CONV =
1140   let add_tm = `(+):num->num->num`
1141   and two_tm = `2` in
1142   fun tm ->
1143     let m = mk_numeral(dest_numeral tm -/ Int 2) in
1144     let tm' = mk_comb(mk_comb(add_tm,m),two_tm) in
1145     SYM(NUM_ADD_CONV tm');;
1146
1147 let CHEB_CONV =
1148   let [pth0;pth1;pth2] = CONJUNCTS cheb in
1149   let rec conv tm =
1150    (GEN_REWRITE_CONV I [pth0; pth1] ORELSEC
1151     (LAND_CONV NUM_ADD2_CONV THENC
1152      GEN_REWRITE_CONV I [pth2] THENC
1153      COMB2_CONV
1154       (funpow 3 RAND_CONV ((LAND_CONV NUM_ADD_CONV) THENC conv))
1155       conv THENC
1156      REAL_POLY_CONV)) tm in
1157   conv;;
1158
1159 CHEB_CONV `cheb 8 x`;;
1160
1161 let CHEB_2N1 = prove
1162  (`!n x. ((x - &1) * (cheb (2 * n + 1) x - &1) =
1163           (cheb (n + 1) x - cheb n x) pow 2) /\
1164          (&2 * (x pow 2 - &1) * (cheb (2 * n + 2) x - &1) =
1165           (cheb (n + 2) x - cheb n x) pow 2)`,
1166   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN GEN_TAC THEN
1167   MATCH_MP_TAC CHEB_INDUCT THEN REWRITE_TAC[ARITH; cheb; CHEB_2; CHEB_3] THEN
1168   REPEAT(CHANGED_TAC
1169    (REWRITE_TAC[GSYM ADD_ASSOC; LEFT_ADD_DISTRIB; ARITH] THEN
1170     REWRITE_TAC[ARITH_RULE `n + 5 = (n + 3) + 2`;
1171                 ARITH_RULE `n + 4 = (n + 2) + 2`;
1172                 ARITH_RULE `n + 3 = (n + 1) + 2`;
1173
1174                 cheb])) THEN
1175   CONV_TAC REAL_RING);;
1176
1177 let IVT_LEMMA1 = prove
1178  (`!f. (!x. f contl x)
1179        ==> !x y. f(x) <= &0 /\ &0 <= f(y) ==> ?x. f(x) = &0`,
1180   ASM_MESON_TAC[IVT; IVT2; REAL_LE_TOTAL]);;
1181
1182 let IVT_LEMMA2 = prove
1183  (`!f. (!x. f contl x) /\ (?x. f(x) <= x) /\ (?y. y <= f(y)) ==> ?x. f(x) = x`,
1184   REPEAT STRIP_TAC THEN MP_TAC(SPEC `\x. f x - x` IVT_LEMMA1) THEN
1185   ASM_SIMP_TAC[CONT_SUB; CONT_X] THEN
1186   SIMP_TAC[REAL_LE_SUB_LADD; REAL_LE_SUB_RADD; REAL_SUB_0; REAL_ADD_LID] THEN
1187   ASM_MESON_TAC[]);;
1188
1189 let SARKOVSKII_TRIVIAL = prove
1190  (`!f:real->real. (!x. f contl x) /\ (?x. f(f(f(x))) = x) ==> ?x. f(x) = x`,
1191   REPEAT STRIP_TAC THEN MATCH_MP_TAC IVT_LEMMA2 THEN ASM_REWRITE_TAC[] THEN
1192   CONJ_TAC THEN MATCH_MP_TAC
1193    (MESON[] `P x \/ P (f x) \/ P (f(f x)) ==> ?x:real. P x`) THEN
1194   FIRST_ASSUM(UNDISCH_TAC o check is_eq o concl) THEN REAL_ARITH_TAC);;
1195
1196 (* ========================================================================= *)
1197 (* Embedding of logics                                                       *)
1198 (* ========================================================================= *)
1199
1200 let string_INDUCT,string_RECURSION = define_type
1201  "string = String num";;
1202
1203 parse_as_infix("&&",(16,"right"));;
1204 parse_as_infix("||",(15,"right"));;
1205 parse_as_infix("-->",(14,"right"));;
1206 parse_as_infix("<->",(13,"right"));;
1207
1208 parse_as_prefix "Not";;
1209 parse_as_prefix "Box";;
1210 parse_as_prefix "Diamond";;
1211
1212 let form_INDUCT,form_RECURSION = define_type
1213  "form = False
1214        | True
1215        | Atom string
1216        | Not form
1217        | && form form
1218        | || form form
1219        | --> form form
1220        | <-> form form
1221        | Box form
1222        | Diamond form";;
1223
1224 let holds = define
1225  `(holds (W,R) V False w <=> F) /\
1226   (holds (W,R) V True w <=> T) /\
1227   (holds (W,R) V (Atom a) w <=> V a w) /\
1228   (holds (W,R) V (Not p) w <=> ~(holds (W,R) V p w)) /\
1229   (holds (W,R) V (p && q) w <=> holds (W,R) V p w /\ holds (W,R) V q w) /\
1230   (holds (W,R) V (p || q) w <=> holds (W,R) V p w \/ holds (W,R) V q w) /\
1231   (holds (W,R) V (p --> q) w <=> holds (W,R) V p w ==> holds (W,R) V q w) /\
1232   (holds (W,R) V (p <-> q) w <=> holds (W,R) V p w <=> holds (W,R) V q w) /\
1233   (holds (W,R) V (Box p) w <=>
1234         !w'. w' IN W /\ R w w' ==> holds (W,R) V p w') /\
1235   (holds (W,R) V (Diamond p) w <=>
1236         ?w'. w' IN W /\ R w w' /\ holds (W,R) V p w')`;;
1237
1238 let holds_in = new_definition
1239  `holds_in (W,R) p = !V w. w IN W ==> holds (W,R) V p w`;;
1240
1241 parse_as_infix("|=",(11,"right"));;
1242
1243 let valid = new_definition
1244  `L |= p <=> !f. L f ==> holds_in f p`;;
1245
1246 let S4 = new_definition
1247  `S4(W,R) <=> ~(W = {}) /\ (!x y. R x y ==> x IN W /\ y IN W) /\
1248               (!x. x IN W ==> R x x) /\
1249               (!x y z. R x y /\ R y z ==> R x z)`;;
1250
1251 let LTL = new_definition
1252  `LTL(W,R) <=> (W = UNIV) /\ !x y:num. R x y <=> x <= y`;;
1253
1254 let GL = new_definition
1255  `GL(W,R) <=> ~(W = {}) /\ (!x y. R x y ==> x IN W /\ y IN W) /\
1256               WF(\x y. R y x) /\ (!x y z:num. R x y /\ R y z ==> R x z)`;;
1257
1258 let MODAL_TAC =
1259   REWRITE_TAC[valid; FORALL_PAIR_THM; holds_in; holds] THEN MESON_TAC[];;
1260
1261 let MODAL_RULE tm = prove(tm,MODAL_TAC);;
1262
1263 let TAUT_1 = MODAL_RULE `L |= Box True`;;
1264 let TAUT_2 = MODAL_RULE `L |= Box(A --> B) --> Box A --> Box B`;;
1265 let TAUT_3 = MODAL_RULE `L |= Diamond(A --> B) --> Box A --> Diamond B`;;
1266 let TAUT_4 = MODAL_RULE `L |= Box(A --> B) --> Diamond A --> Diamond B`;;
1267 let TAUT_5 = MODAL_RULE `L |= Box(A && B) --> Box A && Box B`;;
1268 let TAUT_6 = MODAL_RULE `L |= Diamond(A || B) --> Diamond A || Diamond B`;;
1269
1270 let HOLDS_FORALL_LEMMA = prove
1271  (`!W R P. (!A V. P(holds (W,R) V A)) <=> (!p:W->bool. P p)`,
1272   REPEAT GEN_TAC THEN EQ_TAC THENL [DISCH_TAC THEN GEN_TAC; SIMP_TAC[]] THEN
1273   POP_ASSUM(MP_TAC o SPECL [`Atom a`; `\a:string. (p:W->bool)`]) THEN
1274   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
1275   REWRITE_TAC[holds] THEN REWRITE_TAC[ETA_AX]);;
1276
1277 let MODAL_SCHEMA_TAC =
1278   REWRITE_TAC[holds_in; holds] THEN MP_TAC HOLDS_FORALL_LEMMA THEN
1279   REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
1280   DISCH_THEN(fun th -> REWRITE_TAC[th]);;
1281
1282 let MODAL_REFL = prove
1283  (`!W R. (!w:W. w IN W ==> R w w) <=> !A. holds_in (W,R) (Box A --> A)`,
1284   MODAL_SCHEMA_TAC THEN MESON_TAC[]);;
1285
1286 let MODAL_TRANS = prove
1287  (`!W R. (!w w' w'':W. w IN W /\ w' IN W /\ w'' IN W /\
1288                        R w w' /\ R w' w'' ==> R w w'') <=>
1289          (!A. holds_in (W,R) (Box A --> Box(Box A)))`,
1290   MODAL_SCHEMA_TAC THEN MESON_TAC[]);;
1291
1292 let MODAL_SERIAL = prove
1293  (`!W R. (!w:W. w IN W ==> ?w'. w' IN W /\ R w w') <=>
1294          (!A. holds_in (W,R) (Box A --> Diamond A))`,
1295   MODAL_SCHEMA_TAC THEN MESON_TAC[]);;
1296
1297 let MODAL_SYM = prove
1298  (`!W R. (!w w':W. w IN W /\ w' IN W /\ R w w' ==> R w' w) <=>
1299          (!A. holds_in (W,R) (A --> Box(Diamond A)))`,
1300   MODAL_SCHEMA_TAC THEN EQ_TAC THENL [MESON_TAC[]; REPEAT STRIP_TAC] THEN
1301   FIRST_X_ASSUM(MP_TAC o SPECL [`\v:W. v = w`; `w:W`]) THEN ASM_MESON_TAC[]);;
1302
1303 let MODAL_WFTRANS = prove
1304  (`!W R. (!x y z:W. x IN W /\ y IN W /\ z IN W /\ R x y /\ R y z ==> R x z) /\
1305          WF(\x y. x IN W /\ y IN W /\ R y x) <=>
1306          (!A. holds_in (W,R) (Box(Box A --> A) --> Box A))`,
1307   MODAL_SCHEMA_TAC THEN REWRITE_TAC[WF_IND] THEN EQ_TAC THEN
1308   STRIP_TAC THEN REPEAT CONJ_TAC THENL
1309    [REPEAT GEN_TAC THEN REPEAT DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC;
1310     X_GEN_TAC `w:W` THEN FIRST_X_ASSUM(MP_TAC o SPECL
1311      [`\v:W. v IN W /\ R w v /\ !w''. w'' IN W /\ R v w'' ==> R w w''`; `w:W`]);
1312     X_GEN_TAC `P:W->bool` THEN DISCH_TAC THEN
1313     FIRST_X_ASSUM(MP_TAC o SPEC `\x:W. !w:W. x IN W /\ R w x ==> P x`) THEN
1314     MATCH_MP_TAC MONO_FORALL] THEN
1315   ASM_MESON_TAC[]);;
1316
1317 (* ------------------------------------------------------------------------- *)
1318 (* Need a fresh HOL session here: doing shallow embedding.                   *)
1319 (* ------------------------------------------------------------------------- *)
1320
1321 parse_as_prefix "Not";;
1322 parse_as_infix("&&",(16,"right"));;
1323 parse_as_infix("||",(15,"right"));;
1324 parse_as_infix("-->",(14,"right"));;
1325 parse_as_infix("<->",(13,"right"));;
1326
1327 let false_def = define `False = \t:num. F`;;
1328 let true_def = define `True = \t:num. T`;;
1329 let not_def = define `Not p = \t:num. ~(p t)`;;
1330 let and_def = define `p && q = \t:num. p t /\ q t`;;
1331 let or_def = define `p || q = \t:num. p t \/ q t`;;
1332 let imp_def = define `p --> q = \t:num. p t ==> q t`;;
1333 let iff_def = define `p <-> q = \t:num. p t <=> q t`;;
1334
1335 let forever = define `forever p = \t:num. !t'. t <= t' ==> p t'`;;
1336 let sometime = define `sometime p = \t:num. ?t'. t <= t' /\ p t'`;;
1337
1338 let next = define `next p = \t:num. p(t + 1)`;;
1339
1340 parse_as_infix("until",(17,"right"));;
1341
1342 let until = define
1343   `p until q =
1344     \t:num. ?t'. t <= t' /\ (!t''. t <= t'' /\ t'' < t' ==> p t'') /\ q t'`;;
1345
1346 (* ========================================================================= *)
1347 (* HOL as a functional programming language                                  *)
1348 (* ========================================================================= *)
1349
1350 type ite = False | True | Atomic of int | Ite of ite*ite*ite;;
1351
1352 let rec norm e =
1353   match e with
1354     Ite(False,y,z) -> norm z
1355   | Ite(True,y,z) -> norm y
1356   | Ite(Atomic i,y,z) -> Ite(Atomic i,norm y,norm z)
1357   | Ite(Ite(u,v,w),y,z) -> norm(Ite(u,Ite(v,y,z),Ite(w,y,z)))
1358   | _ -> e;;
1359
1360 let ite_INDUCT,ite_RECURSION = define_type
1361  "ite = False | True | Atomic num | Ite ite ite ite";;
1362
1363 let eth = prove_general_recursive_function_exists
1364  `?norm. (norm False = False) /\
1365          (norm True = True) /\
1366          (!i. norm (Atomic i) = Atomic i) /\
1367          (!y z. norm (Ite False y z) = norm z) /\
1368          (!y z. norm (Ite True y z) = norm y) /\
1369          (!i y z. norm (Ite (Atomic i) y z) =
1370                     Ite (Atomic i) (norm y) (norm z)) /\
1371          (!u v w y z. norm (Ite (Ite u v w) y z) =
1372                         norm (Ite u (Ite v y z) (Ite w y z)))`;;
1373
1374 let sizeof = define
1375  `(sizeof False = 1) /\
1376   (sizeof True = 1) /\
1377   (sizeof(Atomic i) = 1) /\
1378   (sizeof(Ite x y z) = sizeof x * (1 + sizeof y + sizeof z))`;;
1379
1380 let eth' =
1381   let th = prove
1382    (hd(hyp eth),
1383     EXISTS_TAC `MEASURE sizeof` THEN
1384     REWRITE_TAC[WF_MEASURE; MEASURE_LE; MEASURE; sizeof] THEN ARITH_TAC) in
1385   PROVE_HYP th eth;;
1386
1387 let norm = new_specification ["norm"] eth';;
1388
1389 let SIZEOF_INDUCT = REWRITE_RULE[WF_IND; MEASURE]  (ISPEC`sizeof` WF_MEASURE);;
1390
1391 let SIZEOF_NZ = prove
1392  (`!e. ~(sizeof e = 0)`,
1393   MATCH_MP_TAC ite_INDUCT THEN SIMP_TAC[sizeof; ADD_EQ_0; MULT_EQ_0; ARITH]);;
1394
1395 let ITE_INDUCT = prove
1396  (`!P. P False /\
1397        P True /\
1398        (!i. P(Atomic i)) /\
1399        (!y z. P z ==> P(Ite False y z)) /\
1400        (!y z. P y ==> P(Ite True y z)) /\
1401        (!i y z. P y /\ P z ==> P (Ite (Atomic i) y z)) /\
1402        (!u v w x y z. P(Ite u (Ite v y z) (Ite w y z))
1403                       ==> P(Ite (Ite u v w) y z))
1404        ==> !e. P e`,
1405   GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC SIZEOF_INDUCT THEN
1406   MATCH_MP_TAC ite_INDUCT THEN ASM_REWRITE_TAC[] THEN
1407   MATCH_MP_TAC ite_INDUCT THEN POP_ASSUM_LIST
1408    (fun ths -> REPEAT STRIP_TAC THEN FIRST(mapfilter MATCH_MP_TAC ths)) THEN
1409   REPEAT CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
1410   POP_ASSUM_LIST(K ALL_TAC) THEN
1411   REWRITE_TAC[sizeof] THEN TRY ARITH_TAC THEN
1412   REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
1413   REWRITE_TAC[MULT_AC; ADD_AC; LT_ADD_LCANCEL] THEN
1414   REWRITE_TAC[ADD_ASSOC; LT_ADD_RCANCEL] THEN
1415   MATCH_MP_TAC(ARITH_RULE `~(b = 0) /\ ~(c = 0) ==> a < (b + a) + c`) THEN
1416   REWRITE_TAC[MULT_EQ_0; SIZEOF_NZ]);;
1417
1418 let normalized = define
1419  `(normalized False <=> T) /\
1420   (normalized True <=> T) /\
1421   (normalized(Atomic a) <=> T) /\
1422   (normalized(Ite False x y) <=> F) /\
1423   (normalized(Ite True x y) <=> F) /\
1424   (normalized(Ite (Atomic a) x y) <=> normalized x /\ normalized y) /\
1425   (normalized(Ite (Ite u v w) x y) <=> F)`;;
1426
1427 let NORMALIZED_NORM = prove
1428  (`!e. normalized(norm e)`,
1429   MATCH_MP_TAC ITE_INDUCT THEN REWRITE_TAC[norm; normalized]);;
1430
1431 let NORMALIZED_INDUCT = prove
1432  (`P False /\
1433    P True /\
1434    (!i. P (Atomic i)) /\
1435    (!i x y. P x /\ P y ==> P (Ite (Atomic i) x y))
1436    ==> !e. normalized e ==> P e`,
1437   STRIP_TAC THEN MATCH_MP_TAC ite_INDUCT THEN ASM_REWRITE_TAC[normalized] THEN
1438   MATCH_MP_TAC ite_INDUCT THEN ASM_MESON_TAC[normalized]);;
1439
1440 let holds = define
1441  `(holds v False <=> F) /\
1442   (holds v True <=> T) /\
1443   (holds v (Atomic i) <=> v(i)) /\
1444   (holds v (Ite b x y) <=> if holds v b then holds v x else holds v y)`;;
1445
1446 let HOLDS_NORM = prove
1447  (`!e v. holds v (norm e) <=> holds v e`,
1448   MATCH_MP_TAC ITE_INDUCT THEN SIMP_TAC[holds; norm] THEN
1449   REPEAT STRIP_TAC THEN CONV_TAC TAUT);;
1450
1451 let taut = define
1452  `(taut (t,f) False <=> F) /\
1453   (taut (t,f) True <=> T) /\
1454   (taut (t,f) (Atomic i) <=> MEM i t) /\
1455   (taut (t,f) (Ite (Atomic i) x y) <=>
1456       if MEM i t then taut (t,f) x
1457       else if MEM i f then taut (t,f) y
1458       else taut (CONS i t,f) x /\ taut (t,CONS i f) y)`;;
1459
1460 let tautology = define `tautology e = taut([],[]) (norm e)`;;
1461
1462 let NORMALIZED_TAUT = prove
1463  (`!e. normalized e
1464        ==> !f t. (!a. ~(MEM a t /\ MEM a f))
1465                  ==> (taut (t,f) e <=>
1466                       !v. (!a. MEM a t ==> v(a)) /\ (!a. MEM a f ==> ~v(a))
1467                           ==> holds v e)`,
1468   MATCH_MP_TAC NORMALIZED_INDUCT THEN REWRITE_TAC[holds; taut] THEN
1469   REWRITE_TAC[NOT_FORALL_THM] THEN REPEAT CONJ_TAC THENL
1470    [REPEAT STRIP_TAC THEN EXISTS_TAC `\a:num. MEM a t` THEN ASM_MESON_TAC[];
1471     REPEAT STRIP_TAC THEN EQ_TAC THENL
1472      [ALL_TAC; DISCH_THEN MATCH_MP_TAC] THEN ASM_MESON_TAC[];
1473     REPEAT STRIP_TAC THEN REPEAT(COND_CASES_TAC THEN ASM_SIMP_TAC[])] THEN
1474   ASM_SIMP_TAC[MEM; RIGHT_OR_DISTRIB; LEFT_OR_DISTRIB;
1475                MESON[] `(!a. ~(MEM a t /\ a = i)) <=> ~(MEM i t)`;
1476                MESON[] `(!a. ~(a = i /\ MEM a f)) <=> ~(MEM i f)`] THEN
1477   ASM_REWRITE_TAC[AND_FORALL_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN
1478   MESON_TAC[]);;
1479
1480 let TAUTOLOGY = prove
1481  (`!e. tautology e <=> !v. holds v e`,
1482   MESON_TAC[tautology; HOLDS_NORM; NORMALIZED_TAUT; MEM; NORMALIZED_NORM]);;
1483
1484 let HOLDS_BACK = prove
1485  (`!v. (F <=> holds v False) /\
1486        (T <=> holds v True) /\
1487        (!i. v i <=> holds v (Atomic i)) /\
1488        (!p. ~holds v p <=> holds v (Ite p False True)) /\
1489        (!p q. (holds v p /\ holds v q) <=> holds v (Ite p q False)) /\
1490        (!p q. (holds v p \/ holds v q) <=> holds v (Ite p True q)) /\
1491        (!p q. (holds v p <=> holds v q) <=>
1492                    holds v (Ite p q (Ite q False True))) /\
1493        (!p q. holds v p ==> holds v q <=> holds v (Ite p q True))`,
1494   REWRITE_TAC[holds] THEN CONV_TAC TAUT);;
1495
1496 let COND_CONV = GEN_REWRITE_CONV I [COND_CLAUSES];;
1497 let AND_CONV = GEN_REWRITE_CONV I [TAUT `(F /\ a <=> F) /\ (T /\ a <=> a)`];;
1498 let OR_CONV = GEN_REWRITE_CONV I [TAUT `(F \/ a <=> a) /\ (T \/ a <=> T)`];;
1499
1500 let rec COMPUTE_DEPTH_CONV conv tm =
1501   if is_cond tm then
1502    (RATOR_CONV(LAND_CONV(COMPUTE_DEPTH_CONV conv)) THENC
1503     COND_CONV THENC
1504     COMPUTE_DEPTH_CONV conv) tm
1505   else if is_conj tm then
1506    (LAND_CONV (COMPUTE_DEPTH_CONV conv) THENC
1507     AND_CONV THENC
1508     COMPUTE_DEPTH_CONV conv) tm
1509   else if is_disj tm then
1510    (LAND_CONV (COMPUTE_DEPTH_CONV conv) THENC
1511     OR_CONV THENC
1512     COMPUTE_DEPTH_CONV conv) tm
1513   else
1514    (SUB_CONV (COMPUTE_DEPTH_CONV conv) THENC
1515     TRY_CONV(conv THENC COMPUTE_DEPTH_CONV conv)) tm;;
1516
1517 g `!v. v 1 \/ v 2 \/ v 3 \/ v 4 \/ v 5 \/ v 6 \/
1518        ~v 1 \/ ~v 2 \/ ~v 3 \/ ~v 4 \/ ~v 5 \/ ~v 6`;;
1519
1520 e(MP_TAC HOLDS_BACK THEN MATCH_MP_TAC MONO_FORALL THEN
1521   GEN_TAC THEN DISCH_THEN(fun th -> REWRITE_TAC[th]) THEN
1522   SPEC_TAC(`v:num->bool`,`v:num->bool`) THEN
1523   REWRITE_TAC[GSYM TAUTOLOGY; tautology]);;
1524
1525 time e (GEN_REWRITE_TAC COMPUTE_DEPTH_CONV [norm; taut; MEM; ARITH_EQ]);;
1526
1527 ignore(b()); time e (REWRITE_TAC[norm; taut; MEM; ARITH_EQ]);;
1528
1529 (* ========================================================================= *)
1530 (* Vectors                                                                   *)
1531 (* ========================================================================= *)
1532
1533 needs "Multivariate/vectors.ml";;
1534
1535 needs "Examples/solovay.ml";;
1536
1537 g `orthogonal (A - B) (C - B)
1538    ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`;;
1539
1540 e SOLOVAY_VECTOR_TAC;;
1541 e(CONV_TAC REAL_RING);;
1542
1543 g`!x y:real^N. x dot y <= norm x * norm y`;;
1544 e SOLOVAY_VECTOR_TAC;;
1545
1546 (**** Needs external SDP solver
1547 needs "Examples/sos.ml";;
1548
1549 e(CONV_TAC REAL_SOS);;
1550
1551 let EXAMPLE_0 = prove
1552  (`!a x y:real^N. (y - x) dot (a - y) >= &0 ==> norm(y - a) <= norm(x - a)`,
1553   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
1554 ****)
1555
1556 needs "Rqe/make.ml";;
1557 let EXAMPLE_10 = prove
1558  (`!x:real^N y.
1559         x dot y > &0
1560         ==> ?u. &0 < u /\
1561                 !v. &0 < v /\ v <= u ==> norm(v % y - x) < norm x`,
1562   SOLOVAY_VECTOR_TAC THEN
1563   W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
1564   CONV_TAC REAL_QELIM_CONV);;
1565
1566 let FORALL_3 = prove
1567  (`(!i. 1 <= i /\ i <= 3 ==> P i) <=> P 1 /\ P 2 /\ P 3`,
1568   MESON_TAC[ARITH_RULE `1 <= i /\ i <= 3 <=> (i = 1) \/ (i = 2) \/ (i = 3)`]);;
1569
1570 let SUM_3 = prove
1571  (`!t. sum(1..3) t = t(1) + t(2) + t(3)`,
1572   REWRITE_TAC[num_CONV `3`; num_CONV `2`; SUM_CLAUSES_NUMSEG] THEN
1573   REWRITE_TAC[SUM_SING_NUMSEG; ARITH; REAL_ADD_ASSOC]);;
1574
1575 let VECTOR_3 = prove
1576  (`(vector [x;y;z] :real^3)$1 = x /\
1577    (vector [x;y;z] :real^3)$2 = y /\
1578    (vector [x;y;z] :real^3)$3 = z`,
1579   SIMP_TAC[vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
1580   REWRITE_TAC[num_CONV `2`; num_CONV `1`; EL; HD; TL]);;
1581
1582 let DOT_VECTOR = prove
1583  (`(vector [x1;y1;z1] :real^3) dot (vector [x2;y2;z2]) =
1584        x1 * x2 + y1 * y2 + z1 * z2`,
1585   REWRITE_TAC[dot; DIMINDEX_3; SUM_3; VECTOR_3]);;
1586
1587 let VECTOR_ZERO = prove
1588  (`(vector [x;y;z] :real^3 = vec 0) <=> x = &0 /\ y = &0 /\ z = &0`,
1589   SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]);;
1590
1591 let ORTHOGONAL_VECTOR = prove
1592  (`orthogonal (vector [x1;y1;z1] :real^3) (vector [x2;y2;z2]) =
1593         (x1 * x2 + y1 * y2 + z1 * z2 = &0)`,
1594   REWRITE_TAC[orthogonal; DOT_VECTOR]);;
1595
1596 parse_as_infix("cross",(20,"right"));;
1597
1598 let cross = new_definition
1599  `(a:real^3) cross (b:real^3) =
1600     vector [a$2 * b$3 - a$3 * b$2;
1601             a$3 * b$1 - a$1 * b$3;
1602             a$1 * b$2 - a$2 * b$1] :real^3`;;
1603
1604 let VEC3_TAC =
1605   SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
1606            vector_add; vec; dot; cross; orthogonal; basis; ARITH] THEN
1607   CONV_TAC REAL_RING;;
1608
1609 let VEC3_RULE tm = prove(tm,VEC3_TAC);;
1610
1611 let ORTHOGONAL_CROSS = VEC3_RULE
1612  `!x y. orthogonal (x cross y) x /\ orthogonal (x cross y) y /\
1613         orthogonal x (x cross y) /\ orthogonal y (x cross y)`;;
1614
1615 let LEMMA_0 = VEC3_RULE
1616  `~(basis 1 :real^3 = vec 0) /\
1617   ~(basis 2 :real^3 = vec 0) /\
1618   ~(basis 3 :real^3 = vec 0)`;;
1619
1620 let LEMMA_1 = VEC3_RULE `!u v. u dot (u cross v) = &0`;;
1621
1622 let LEMMA_2 = VEC3_RULE `!u v. v dot (u cross v) = &0`;;
1623
1624 let LEMMA_3 = VEC3_RULE `!u:real^3. vec 0 dot u = &0`;;
1625
1626 let LEMMA_4 = VEC3_RULE `!u:real^3. u dot vec 0 = &0`;;
1627
1628 let LEMMA_5 = VEC3_RULE `!x. x cross x = vec 0`;;
1629
1630 let LEMMA_6 = VEC3_RULE
1631  `!u. ~(u = vec 0)
1632       ==> ~(u cross basis 1 = vec 0) \/
1633           ~(u cross basis 2 = vec 0) \/
1634           ~(u cross basis 3 = vec 0)`;;
1635
1636 let LEMMA_7 = VEC3_RULE
1637  `!u v w. (u cross v = vec 0) ==> (u dot (v cross w) = &0)`;;
1638
1639 let NORMAL_EXISTS = prove
1640  (`!u v:real^3. ?w. ~(w = vec 0) /\ orthogonal u w /\ orthogonal v w`,
1641   REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
1642    [`u:real^3 = vec 0`; `v:real^3 = vec 0`; `u cross v = vec 0`] THEN
1643   ASM_REWRITE_TAC[orthogonal] THEN
1644   ASM_MESON_TAC[LEMMA_0; LEMMA_1; LEMMA_2; LEMMA_3; LEMMA_4;
1645                 LEMMA_5; LEMMA_6; LEMMA_7]);;
1646
1647 (* ========================================================================= *)
1648 (* Custom tactics                                                            *)
1649 (* ========================================================================= *)
1650
1651 let points =
1652 [((0, -1), (0, -1), (2, 0)); ((0, -1), (0, 0), (2, 0));
1653  ((0, -1), (0, 1), (2, 0)); ((0, -1), (2, 0), (0, -1));
1654  ((0, -1), (2, 0), (0, 0)); ((0, -1), (2, 0), (0, 1));
1655  ((0, 0), (0, -1), (2, 0)); ((0, 0), (0, 0), (2, 0));
1656  ((0, 0), (0, 1), (2, 0)); ((0, 0), (2, 0), (-2, 0));
1657  ((0, 0), (2, 0), (0, -1)); ((0, 0), (2, 0), (0, 0));
1658  ((0, 0), (2, 0), (0, 1)); ((0, 0), (2, 0), (2, 0));
1659  ((0, 1), (0, -1), (2, 0)); ((0, 1), (0, 0), (2, 0));
1660  ((0, 1), (0, 1), (2, 0)); ((0, 1), (2, 0), (0, -1));
1661  ((0, 1), (2, 0), (0, 0)); ((0, 1), (2, 0), (0, 1));
1662  ((2, 0), (-2, 0), (0, 0)); ((2, 0), (0, -1), (0, -1));
1663  ((2, 0), (0, -1), (0, 0)); ((2, 0), (0, -1), (0, 1));
1664  ((2, 0), (0, 0), (-2, 0)); ((2, 0), (0, 0), (0, -1));
1665  ((2, 0), (0, 0), (0, 0)); ((2, 0), (0, 0), (0, 1));
1666  ((2, 0), (0, 0), (2, 0)); ((2, 0), (0, 1), (0, -1));
1667  ((2, 0), (0, 1), (0, 0)); ((2, 0), (0, 1), (0, 1));
1668  ((2, 0), (2, 0), (0, 0))];;
1669
1670 let ortho =
1671   let mult (x1,y1) (x2,y2) = (x1 * x2 + 2 * y1 * y2,x1 * y2 + y1 * x2)
1672   and add (x1,y1) (x2,y2) = (x1 + x2,y1 + y2) in
1673   let dot (x1,y1,z1) (x2,y2,z2) =
1674     end_itlist add [mult x1 x2; mult y1 y2; mult z1 z2] in
1675   fun (v1,v2) -> dot v1 v2 = (0,0);;
1676
1677 let opairs = filter ortho (allpairs (fun a b -> a,b) points points);;
1678
1679 let otrips = filter (fun (a,b,c) -> ortho(a,b) & ortho(a,c))
1680                     (allpairs (fun a (b,c) -> a,b,c) points opairs);;
1681
1682 let hol_of_value =
1683   let tm0 = `&0` and tm1 = `&2` and tm2 = `-- &2`
1684   and tm3 = `sqrt(&2)` and tm4 = `--sqrt(&2)` in
1685   function 0,0 -> tm0 | 2,0 -> tm1 | -2,0 -> tm2 | 0,1 -> tm3 | 0,-1 -> tm4;;
1686
1687 let hol_of_point =
1688   let ptm = `vector:(real)list->real^3` in
1689   fun (x,y,z) -> mk_comb(ptm,mk_flist(map hol_of_value [x;y;z]));;
1690
1691 let SQRT_2_POW = prove
1692  (`sqrt(&2) pow 2 = &2`,
1693   SIMP_TAC[SQRT_POW_2; REAL_POS]);;
1694
1695 let PROVE_NONTRIVIAL =
1696   let ptm = `~(x :real^3 = vec 0)` and xtm = `x:real^3` in
1697   fun x -> prove(vsubst [hol_of_point x,xtm] ptm,
1698                  GEN_REWRITE_TAC RAND_CONV [VECTOR_ZERO] THEN
1699                  MP_TAC SQRT_2_POW THEN CONV_TAC REAL_RING);;
1700
1701 let PROVE_ORTHOGONAL =
1702   let ptm = `orthogonal:real^3->real^3->bool` in
1703   fun (x,y) ->
1704    prove(list_mk_comb(ptm,[hol_of_point x;hol_of_point y]),
1705          ONCE_REWRITE_TAC[ORTHOGONAL_VECTOR] THEN
1706          MP_TAC SQRT_2_POW THEN CONV_TAC REAL_RING);;
1707
1708 let ppoint = let p = `P:real^3->bool` in fun v -> mk_comb(p,hol_of_point v);;
1709
1710 let DEDUCE_POINT_TAC pts =
1711   FIRST_X_ASSUM MATCH_MP_TAC THEN
1712   MAP_EVERY EXISTS_TAC (map hol_of_point pts) THEN
1713   ASM_REWRITE_TAC[];;
1714
1715 let rec KOCHEN_SPECKER_TAC set_0 set_1 =
1716   if intersect set_0 set_1 <> [] then
1717     let p = ppoint(hd(intersect set_0 set_1)) in
1718     let th1 = ASSUME(mk_neg p) and th2 = ASSUME p in
1719     ACCEPT_TAC(EQ_MP (EQF_INTRO th1) th2)
1720   else
1721     let prf_1 = filter (fun (a,b) -> mem a set_0) opairs
1722     and prf_0 = filter (fun (a,b,c) -> mem a set_1 & mem b set_1) otrips in
1723     let new_1 = map snd prf_1 and new_0 = map (fun (a,b,c) -> c) prf_0 in
1724     let set_0' = union new_0 set_0 and set_1' = union new_1 set_1 in
1725     let del_0 = subtract set_0' set_0 and del_1 = subtract set_1' set_1 in
1726     if del_0 <> [] or del_1 <> [] then
1727        let prv_0 x =
1728          let a,b,_ = find (fun (a,b,c) -> c = x) prf_0 in DEDUCE_POINT_TAC [a;b]
1729        and prv_1 x =
1730          let a,_ = find (fun (a,c) -> c = x) prf_1 in DEDUCE_POINT_TAC [a] in
1731       let newuns = list_mk_conj
1732         (map ppoint del_1 @ map (mk_neg o ppoint) del_0)
1733       and tacs = map prv_1 del_1 @ map prv_0 del_0 in
1734       SUBGOAL_THEN newuns STRIP_ASSUME_TAC THENL
1735        [REPEAT CONJ_TAC THENL tacs; ALL_TAC] THEN
1736       KOCHEN_SPECKER_TAC set_0' set_1'
1737     else
1738       let v = find (fun i -> not(mem i set_0) & not(mem i set_1)) points in
1739       ASM_CASES_TAC (ppoint v) THENL
1740        [KOCHEN_SPECKER_TAC set_0 (v::set_1);
1741         KOCHEN_SPECKER_TAC (v::set_0) set_1];;
1742
1743 let KOCHEN_SPECKER_LEMMA = prove
1744  (`!P. (!x y:real^3. ~(x = vec 0) /\ ~(y = vec 0) /\ orthogonal x y /\
1745                      ~(P x) ==> P y) /\
1746        (!x y z. ~(x = vec 0) /\ ~(y = vec 0) /\ ~(z = vec 0) /\
1747                 orthogonal x y /\ orthogonal x z /\ orthogonal y z /\
1748                 P x /\ P y ==> ~(P z))
1749        ==> F`,
1750   REPEAT STRIP_TAC THEN
1751   MAP_EVERY (ASSUME_TAC o PROVE_NONTRIVIAL) points THEN
1752   MAP_EVERY (ASSUME_TAC o PROVE_ORTHOGONAL) opairs THEN
1753   KOCHEN_SPECKER_TAC [] []);;
1754
1755 let NONTRIVIAL_CROSS = prove
1756  (`!x y. orthogonal x y /\ ~(x = vec 0) /\ ~(y = vec 0)
1757          ==> ~(x cross y = vec 0)`,
1758   REWRITE_TAC[GSYM DOT_EQ_0] THEN VEC3_TAC);;
1759
1760 let KOCHEN_SPECKER_PARADOX = prove
1761  (`~(?spin:real^3->num.
1762         !x y z. ~(x = vec 0) /\ ~(y = vec 0) /\ ~(z = vec 0) /\
1763                 orthogonal x y /\ orthogonal x z /\ orthogonal y z
1764                 ==> (spin x = 0) /\ (spin y = 1) /\ (spin z = 1) \/
1765                     (spin x = 1) /\ (spin y = 0) /\ (spin z = 1) \/
1766                     (spin x = 1) /\ (spin y = 1) /\ (spin z = 0))`,
1767   REPEAT STRIP_TAC THEN
1768   MP_TAC(SPEC `\x:real^3. spin(x) = 1` KOCHEN_SPECKER_LEMMA) THEN
1769   ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
1770   POP_ASSUM MP_TAC THEN REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
1771   DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
1772   ASM_MESON_TAC[ARITH_RULE `~(1 = 0)`; NONTRIVIAL_CROSS; ORTHOGONAL_CROSS]);;
1773
1774 (* ========================================================================= *)
1775 (* Defining new types                                                        *)
1776 (* ========================================================================= *)
1777
1778 let direction_tybij = new_type_definition "direction" ("mk_dir","dest_dir")
1779  (MESON[LEMMA_0] `?x:real^3. ~(x = vec 0)`);;
1780
1781 parse_as_infix("||",(11,"right"));;
1782 parse_as_infix("_|_",(11,"right"));;
1783
1784 let perpdir = new_definition
1785  `x _|_ y <=> orthogonal (dest_dir x) (dest_dir y)`;;
1786
1787 let pardir = new_definition
1788  `x || y <=> (dest_dir x) cross (dest_dir y) = vec 0`;;
1789
1790 let DIRECTION_CLAUSES = prove
1791  (`((!x. P(dest_dir x)) <=> (!x. ~(x = vec 0) ==> P x)) /\
1792    ((?x. P(dest_dir x)) <=> (?x. ~(x = vec 0) /\ P x))`,
1793   MESON_TAC[direction_tybij]);;
1794
1795 let [PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS] = (CONJUNCTS o prove)
1796  (`(!x. x || x) /\
1797    (!x y. x || y <=> y || x) /\
1798    (!x y z. x || y /\ y || z ==> x || z)`,
1799   REWRITE_TAC[pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
1800
1801 let DIRECTION_AXIOM_1 = prove
1802  (`!p p'. ~(p || p') ==> ?l. p _|_ l /\ p' _|_ l /\
1803                              !l'. p _|_ l' /\ p' _|_ l' ==> l' || l`,
1804   REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN REPEAT STRIP_TAC THEN
1805   MP_TAC(SPECL [`p:real^3`; `p':real^3`] NORMAL_EXISTS) THEN
1806   MATCH_MP_TAC MONO_EXISTS THEN
1807   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
1808
1809 let DIRECTION_AXIOM_2 = prove
1810  (`!l l'. ?p. p _|_ l /\ p _|_ l'`,
1811   REWRITE_TAC[perpdir; DIRECTION_CLAUSES] THEN
1812   MESON_TAC[NORMAL_EXISTS; ORTHOGONAL_SYM]);;
1813
1814 let DIRECTION_AXIOM_3 = prove
1815  (`?p p' p''.
1816         ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
1817         ~(?l. p _|_ l /\ p' _|_ l /\ p'' _|_ l)`,
1818   REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN
1819   MAP_EVERY (fun t -> EXISTS_TAC t THEN REWRITE_TAC[LEMMA_0])
1820    [`basis 1 :real^3`; `basis 2 : real^3`; `basis 3 :real^3`] THEN
1821   VEC3_TAC);;
1822
1823 let CROSS_0 = VEC3_RULE `x cross vec 0 = vec 0 /\ vec 0 cross x = vec 0`;;
1824
1825 let DIRECTION_AXIOM_4_WEAK = prove
1826  (`!l. ?p p'. ~(p || p') /\ p _|_ l /\ p' _|_ l`,
1827   REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN REPEAT STRIP_TAC THEN
1828   SUBGOAL_THEN
1829    `orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 2) l /\
1830     ~((l cross basis 1) cross (l cross basis 2) = vec 0) \/
1831     orthogonal (l cross basis 1) l /\ orthogonal (l cross basis 3) l /\
1832     ~((l cross basis 1) cross (l cross basis 3) = vec 0) \/
1833     orthogonal (l cross basis 2) l /\ orthogonal (l cross basis 3) l /\
1834     ~((l cross basis 2) cross (l cross basis 3) = vec 0)`
1835   MP_TAC THENL [POP_ASSUM MP_TAC THEN VEC3_TAC; MESON_TAC[CROSS_0]]);;
1836
1837 let ORTHOGONAL_COMBINE = prove
1838  (`!x a b. a _|_ x /\ b _|_ x /\ ~(a || b)
1839            ==> ?c. c _|_ x /\ ~(a || c) /\ ~(b || c)`,
1840   REWRITE_TAC[DIRECTION_CLAUSES; pardir; perpdir] THEN
1841   REPEAT STRIP_TAC THEN EXISTS_TAC `a + b:real^3` THEN
1842   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN VEC3_TAC);;
1843
1844 let DIRECTION_AXIOM_4 = prove
1845  (`!l. ?p p' p''. ~(p || p') /\ ~(p' || p'') /\ ~(p || p'') /\
1846                   p _|_ l /\ p' _|_ l /\ p'' _|_ l`,
1847   MESON_TAC[DIRECTION_AXIOM_4_WEAK; ORTHOGONAL_COMBINE]);;
1848
1849 let line_tybij = define_quotient_type "line" ("mk_line","dest_line") `(||)`;;
1850
1851 let PERPDIR_WELLDEF = prove
1852  (`!x y x' y'. x || x' /\ y || y' ==> (x _|_ y <=> x' _|_ y')`,
1853   REWRITE_TAC[perpdir; pardir; DIRECTION_CLAUSES] THEN VEC3_TAC);;
1854
1855 let perpl,perpl_th =
1856   lift_function (snd line_tybij) (PARDIR_REFL,PARDIR_TRANS)
1857                 "perpl" PERPDIR_WELLDEF;;
1858
1859 let line_lift_thm = lift_theorem line_tybij
1860  (PARDIR_REFL,PARDIR_SYM,PARDIR_TRANS) [perpl_th];;
1861
1862 let LINE_AXIOM_1 = line_lift_thm DIRECTION_AXIOM_1;;
1863 let LINE_AXIOM_2 = line_lift_thm DIRECTION_AXIOM_2;;
1864 let LINE_AXIOM_3 = line_lift_thm DIRECTION_AXIOM_3;;
1865 let LINE_AXIOM_4 = line_lift_thm DIRECTION_AXIOM_4;;
1866
1867 let point_tybij = new_type_definition "point" ("mk_point","dest_point")
1868  (prove(`?x:line. T`,REWRITE_TAC[]));;
1869
1870 parse_as_infix("on",(11,"right"));;
1871
1872 let on = new_definition `p on l <=> perpl (dest_point p) l`;;
1873
1874 let POINT_CLAUSES = prove
1875  (`((p = p') <=> (dest_point p = dest_point p')) /\
1876    ((!p. P (dest_point p)) <=> (!l. P l)) /\
1877    ((?p. P (dest_point p)) <=> (?l. P l))`,
1878   MESON_TAC[point_tybij]);;
1879
1880 let POINT_TAC th = REWRITE_TAC[on; POINT_CLAUSES] THEN ACCEPT_TAC th;;
1881
1882 let AXIOM_1 = prove
1883  (`!p p'. ~(p = p') ==> ?l. p on l /\ p' on l /\
1884           !l'. p on l' /\ p' on l' ==> (l' = l)`,
1885   POINT_TAC LINE_AXIOM_1);;
1886
1887 let AXIOM_2 = prove
1888  (`!l l'. ?p. p on l /\ p on l'`,
1889   POINT_TAC LINE_AXIOM_2);;
1890
1891 let AXIOM_3 = prove
1892  (`?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
1893     ~(?l. p on l /\ p' on l /\ p'' on l)`,
1894   POINT_TAC LINE_AXIOM_3);;
1895
1896 let AXIOM_4 = prove
1897  (`!l. ?p p' p''. ~(p = p') /\ ~(p' = p'') /\ ~(p = p'') /\
1898     p on l /\ p' on l /\ p'' on l`,
1899   POINT_TAC LINE_AXIOM_4);;
1900
1901 (* ========================================================================= *)
1902 (* Custom inference rules                                                    *)
1903 (* ========================================================================= *)
1904
1905 let near_ring_axioms =
1906   `(!x. 0 + x = x) /\
1907    (!x. neg x + x = 0) /\
1908    (!x y z. (x + y) + z = x + y + z) /\
1909    (!x y z. (x * y) * z = x * y * z) /\
1910    (!x y z. (x + y) * z = (x * z) + (y * z))`;;
1911
1912 (**** Works eventually but takes a very long time
1913 MESON[]
1914  `(!x. 0 + x = x) /\
1915   (!x. neg x + x = 0) /\
1916   (!x y z. (x + y) + z = x + y + z) /\
1917   (!x y z. (x * y) * z = x * y * z) /\
1918   (!x y z. (x + y) * z = (x * z) + (y * z))
1919   ==> !a. 0 * a = 0`;;
1920  ****)
1921
1922 let is_realvar w x = is_var x & not(mem x w);;
1923
1924 let rec real_strip w tm =
1925   if mem tm w then tm,[] else
1926   let l,r = dest_comb tm in
1927   let f,args = real_strip w l in f,args@[r];;
1928
1929 let weight lis (f,n) (g,m) =
1930   let i = index f lis and j = index g lis in
1931   i > j or i = j & n > m;;
1932
1933 let rec lexord ord l1 l2 =
1934   match (l1,l2) with
1935     (h1::t1,h2::t2) -> if ord h1 h2 then length t1 = length t2
1936                        else h1 = h2 & lexord ord t1 t2
1937   | _ -> false;;
1938
1939 let rec lpo_gt w s t =
1940   if is_realvar w t then not(s = t) & mem t (frees s)
1941   else if is_realvar w s or is_abs s or is_abs t then false else
1942   let f,fargs = real_strip w s and g,gargs = real_strip w t in
1943   exists (fun si -> lpo_ge w si t) fargs or
1944         forall (lpo_gt w s) gargs &
1945         (f = g & lexord (lpo_gt w) fargs gargs or
1946          weight w (f,length fargs) (g,length gargs))
1947 and lpo_ge w s t = (s = t) or lpo_gt w s t;;
1948
1949 let rec istriv w env x t =
1950   if is_realvar w t then t = x or defined env t & istriv w env x (apply env t)
1951   else if is_const t then false else
1952   let f,args = strip_comb t in
1953   exists (istriv w env x) args & failwith "cyclic";;
1954
1955 let rec unify w env tp =
1956   match tp with
1957    ((Var(_,_) as x),t) | (t,(Var(_,_) as x)) when not(mem x w) ->
1958         if defined env x then unify w env (apply env x,t)
1959         else if istriv w env x t then env else (x|->t) env
1960   | (Comb(f,x),Comb(g,y)) -> unify w (unify w env (x,y)) (f,g)
1961   | (s,t) -> if s = t then env else failwith "unify: not unifiable";;
1962
1963 let fullunify w (s,t) =
1964   let env = unify w undefined (s,t) in
1965   let th = map (fun (x,t) -> (t,x)) (graph env) in
1966   let rec subs t =
1967     let t' = vsubst th t in
1968     if t' = t then t else subs t' in
1969   map (fun (t,x) -> (subs t,x)) th;;
1970
1971 let rec listcases fn rfn lis acc =
1972   match lis with
1973     [] -> acc
1974   | h::t -> fn h (fun i h' -> rfn i (h'::map REFL t)) @
1975             listcases fn (fun i t' -> rfn i (REFL h::t')) t acc;;
1976
1977 let LIST_MK_COMB f ths = rev_itlist (fun s t -> MK_COMB(t,s)) ths (REFL f);;
1978
1979 let rec overlaps w th tm rfn =
1980   let l,r = dest_eq(concl th) in
1981   if not (is_comb tm) then [] else
1982   let f,args = strip_comb tm in
1983   listcases (overlaps w th) (fun i a -> rfn i (LIST_MK_COMB f a)) args
1984             (try [rfn (fullunify w (l,tm)) th] with Failure _ -> []);;
1985
1986 let crit1 w eq1 eq2 =
1987   let l1,r1 = dest_eq(concl eq1)
1988   and l2,r2 = dest_eq(concl eq2) in
1989   overlaps w eq1 l2 (fun i th -> TRANS (SYM(INST i th)) (INST i eq2));;
1990
1991 let fixvariables s th =
1992   let fvs = subtract (frees(concl th)) (freesl(hyp th)) in
1993   let gvs = map2 (fun v n -> mk_var(s^string_of_int n,type_of v))
1994                  fvs (1--length fvs) in
1995   INST (zip gvs fvs) th;;
1996
1997 let renamepair (th1,th2) = fixvariables "x" th1,fixvariables "y" th2;;
1998
1999 let critical_pairs w tha thb =
2000   let th1,th2 = renamepair (tha,thb) in crit1 w th1 th2 @ crit1 w th2 th1;;
2001
2002 let normalize_and_orient w eqs th =
2003   let th' = GEN_REWRITE_RULE TOP_DEPTH_CONV eqs th in
2004   let s',t' = dest_eq(concl th') in
2005   if lpo_ge w s' t' then th' else if lpo_ge w t' s' then SYM th'
2006   else failwith "Can't orient equation";;
2007
2008 let status(eqs,crs) eqs0 =
2009   if eqs = eqs0 & (length crs) mod 1000 <> 0 then () else
2010   (print_string(string_of_int(length eqs)^" equations and "^
2011                 string_of_int(length crs)^" pending critical pairs");
2012    print_newline());;
2013
2014 let left_reducible eqs eq =
2015   can (CHANGED_CONV(GEN_REWRITE_CONV (LAND_CONV o ONCE_DEPTH_CONV) eqs))
2016       (concl eq);;
2017
2018 let rec complete w (eqs,crits) =
2019   match crits with
2020     (eq::ocrits) ->
2021         let trip =
2022           try let eq' = normalize_and_orient w eqs eq in
2023               let s',t' = dest_eq(concl eq') in
2024               if s' = t' then (eqs,ocrits) else
2025               let crits',eqs' = partition(left_reducible [eq']) eqs in
2026               let eqs'' = eq'::eqs' in
2027               eqs'',
2028               ocrits @ crits' @ itlist ((@) o critical_pairs w eq') eqs'' []
2029           with Failure _ ->
2030               if exists (can (normalize_and_orient w eqs)) ocrits
2031               then (eqs,ocrits@[eq])
2032               else failwith "complete: no orientable equations" in
2033         status trip eqs; complete w trip
2034   | [] -> eqs;;
2035
2036 let complete_equations wts eqs =
2037   let eqs' = map (normalize_and_orient wts []) eqs in
2038   complete wts ([],eqs');;
2039
2040 complete_equations [`1`; `( * ):num->num->num`; `i:num->num`]
2041   [SPEC_ALL(ASSUME `!a b. i(a) * a * b = b`)];;
2042
2043 complete_equations [`c:A`; `f:A->A`]
2044  (map SPEC_ALL (CONJUNCTS (ASSUME
2045    `((f(f(f(f(f c))))) = c:A) /\ (f(f(f c)) = c)`)));;
2046
2047 let eqs = map SPEC_ALL (CONJUNCTS (ASSUME
2048   `(!x. 1 * x = x) /\ (!x. i(x) * x = 1) /\
2049    (!x y z. (x * y) * z = x * y * z)`)) in
2050 map concl (complete_equations [`1`; `( * ):num->num->num`; `i:num->num`] eqs);;
2051
2052 let COMPLETE_TAC w th =
2053   let eqs = map SPEC_ALL (CONJUNCTS(SPEC_ALL th)) in
2054   let eqs' = complete_equations w eqs in
2055   MAP_EVERY (ASSUME_TAC o GEN_ALL) eqs';;
2056
2057 g `(!x. 1 * x = x) /\
2058    (!x. i(x) * x = 1) /\
2059    (!x y z. (x * y) * z = x * y * z)
2060    ==> !x y. i(y) * i(i(i(x * i(y)))) * x = 1`;;
2061
2062 e (DISCH_THEN(COMPLETE_TAC [`1`; `( * ):num->num->num`; `i:num->num`]));;
2063 e(ASM_REWRITE_TAC[]);;
2064
2065 g `(!x. 0 + x = x) /\
2066      (!x. neg x + x = 0) /\
2067      (!x y z. (x + y) + z = x + y + z) /\
2068      (!x y z. (x * y) * z = x * y * z) /\
2069      (!x y z. (x + y) * z = (x * z) + (y * z))
2070      ==> (neg 0  * (x * y + z + neg(neg(w + z))) + neg(neg b + neg a) =
2071           a + b)`;;
2072
2073 e (DISCH_THEN(COMPLETE_TAC
2074      [`0`; `(+):num->num->num`; `neg:num->num`; `( * ):num->num->num`]));;
2075 e(ASM_REWRITE_TAC[]);;
2076
2077 (**** Could have done this instead
2078 e (DISCH_THEN(COMPLETE_TAC
2079       [`0`; `(+):num->num->num`; `( * ):num->num->num`; `neg:num->num`]));;
2080 ****)
2081
2082 (* ========================================================================= *)
2083 (* Linking external tools                                                    *)
2084 (* ========================================================================= *)
2085
2086 let maximas e =
2087   let filename = Filename.temp_file "maxima" ".out" in
2088   let s =
2089     "echo 'linel:10000; display2d:false;" ^ e ^
2090     ";' | maxima | grep '^(%o3)' | sed -e 's/^(%o3) //' >" ^
2091     filename in
2092   if Sys.command s <> 0 then failwith "maxima" else
2093   let fd = Pervasives.open_in filename in
2094   let data = input_line fd in
2095   close_in fd; Sys.remove filename; data;;
2096
2097 prioritize_real();;
2098 let maxima_ops = ["+",`(+)`; "-",`(-)`; "*",`( * )`;  "/",`(/)`; "^",`(pow)`];;
2099 let maxima_funs = ["sin",`sin`; "cos",`cos`];;
2100
2101 let mk_uneg = curry mk_comb `(--)`;;
2102
2103 let dest_uneg =
2104   let ntm = `(--)` in
2105   fun tm -> let op,t = dest_comb tm in
2106             if op = ntm then t else failwith "dest_uneg";;
2107
2108 let mk_pow = let f = mk_binop `(pow)` in fun x y -> f x (rand y);;
2109 let mk_realvar = let real_ty = `:real` in fun x -> mk_var(x,real_ty);;
2110
2111 let rec string_of_hol tm =
2112   if is_ratconst tm then "("^string_of_num(rat_of_term tm)^")"
2113   else if is_numeral tm then string_of_num(dest_numeral tm)
2114   else if is_var tm then fst(dest_var tm)
2115   else if can dest_uneg tm then "-(" ^ string_of_hol(rand tm) ^ ")" else
2116   let lop,r = dest_comb tm in
2117   try let op,l = dest_comb lop in
2118       "("^string_of_hol l^" "^ rev_assoc op maxima_ops^" "^string_of_hol r^")"
2119   with Failure _ -> rev_assoc lop maxima_funs ^ "(" ^ string_of_hol r ^ ")";;
2120
2121 string_of_hol `(x + sin(-- &2 * x)) pow 2 - cos(x - &22 / &7)`;;
2122
2123 let lexe s = map (function Resword s -> s | Ident s -> s) (lex(explode s));;
2124
2125 let parse_bracketed prs inp =
2126   match prs inp with
2127     ast,")"::rst -> ast,rst
2128   | _ -> failwith "Closing bracket expected";;
2129
2130 let rec parse_ginfix op opup sof prs inp =
2131   match prs inp with
2132     e1,hop::rst when hop = op -> parse_ginfix op opup (opup sof e1) prs rst
2133   | e1,rest -> sof e1,rest;;
2134
2135 let parse_general_infix op =
2136   let opcon = if op = "^" then mk_pow else mk_binop (assoc op maxima_ops) in
2137   let constr = if op <> "^" & snd(get_infix_status op) = "right"
2138                then fun f e1 e2 -> f(opcon e1 e2)
2139                else fun f e1 e2 -> opcon(f e1) e2 in
2140   parse_ginfix op constr (fun x -> x);;
2141
2142 let rec parse_atomic_expression inp =
2143   match inp with
2144    [] -> failwith "expression expected"
2145   | "(" :: rest -> parse_bracketed parse_expression rest
2146   | s :: rest when forall isnum (explode s) ->
2147         term_of_rat(num_of_string s),rest
2148   | s :: "(" :: rest when forall isalnum (explode s) ->
2149         let e,rst = parse_bracketed parse_expression rest in
2150         mk_comb(assoc s maxima_funs,e),rst
2151   | s :: rest when forall isalnum (explode s) -> mk_realvar s,rest
2152 and parse_exp inp = parse_general_infix "^" parse_atomic_expression inp
2153 and parse_neg inp =
2154   match inp with
2155    | "-" :: rest -> let e,rst = parse_neg rest in mk_uneg e,rst
2156    | _ -> parse_exp inp
2157 and parse_expression inp =
2158   itlist parse_general_infix (map fst maxima_ops) parse_neg inp;;
2159
2160 let hol_of_string = fst o parse_expression o lexe;;
2161
2162 hol_of_string "sin(x) - cos(-(- - 1 + x))";;
2163
2164 let FACTOR_CONV tm =
2165   let s = "factor("^string_of_hol tm^")" in
2166   let tm' = hol_of_string(maximas s) in
2167   REAL_RING(mk_eq(tm,tm'));;
2168
2169 FACTOR_CONV `&1234567890`;;
2170
2171 FACTOR_CONV `x pow 6 - &1`;;
2172
2173 FACTOR_CONV `r * (r * x * (&1 - x)) * (&1 - r * x * (&1 - x)) - x`;;
2174
2175 let ANTIDERIV_CONV tm =
2176   let x,bod = dest_abs tm in
2177   let s = "integrate("^string_of_hol bod^","^fst(dest_var x)^")" in
2178   let tm' = mk_abs(x,hol_of_string(maximas s)) in
2179   let th1 = CONV_RULE (NUM_REDUCE_CONV THENC REAL_RAT_REDUCE_CONV)
2180                       (SPEC x (DIFF_CONV tm')) in
2181   let th2 = REAL_RING(mk_eq(lhand(concl th1),bod)) in
2182   GEN x (GEN_REWRITE_RULE LAND_CONV [th2] th1);;
2183
2184 ANTIDERIV_CONV `\x. (x + &5) pow 2 + &77 * x`;;
2185
2186 ANTIDERIV_CONV `\x. sin(x) + x pow 11`;;
2187
2188 (**** This one fails
2189 ANTIDERIV_CONV `\x. sin(x) pow 3`;;
2190  ****)
2191
2192 let SIN_N_CLAUSES = prove
2193  (`(sin(&(NUMERAL(BIT0 n)) * x) =
2194     &2 * sin(&(NUMERAL n) * x) * cos(&(NUMERAL n) * x)) /\
2195    (sin(&(NUMERAL(BIT1 n)) * x) =
2196         sin(&(NUMERAL(BIT0 n)) * x) * cos(x) +
2197         sin(x) * cos(&(NUMERAL(BIT0 n)) * x)) /\
2198    (cos(&(NUMERAL(BIT0 n)) * x) =
2199         cos(&(NUMERAL n) * x) pow 2 - sin(&(NUMERAL n) * x) pow 2) /\
2200    (cos(&(NUMERAL(BIT1 n)) * x) =
2201         cos(&(NUMERAL(BIT0 n)) * x) * cos(x) -
2202         sin(x) * sin(&(NUMERAL(BIT0 n)) * x))`,
2203   REWRITE_TAC[REAL_MUL_2; REAL_POW_2] THEN
2204   REWRITE_TAC[NUMERAL; BIT0; BIT1] THEN
2205   REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN
2206   REWRITE_TAC[REAL_ADD_RDISTRIB; SIN_ADD; COS_ADD; REAL_MUL_LID] THEN
2207   CONV_TAC REAL_RING);;
2208
2209 let TRIG_IDENT_TAC x =
2210   REWRITE_TAC[SIN_N_CLAUSES; SIN_ADD; COS_ADD] THEN
2211   REWRITE_TAC[REAL_MUL_LZERO; SIN_0; COS_0; REAL_MUL_RZERO] THEN
2212   MP_TAC(SPEC x SIN_CIRCLE) THEN CONV_TAC REAL_RING;;
2213
2214 let ANTIDERIV_CONV tm =
2215   let x,bod = dest_abs tm in
2216   let s = "expand(integrate("^string_of_hol bod^","^fst(dest_var x)^"))" in
2217   let tm' = mk_abs(x,hol_of_string(maximas s)) in
2218   let th1 = CONV_RULE (NUM_REDUCE_CONV THENC REAL_RAT_REDUCE_CONV)
2219                       (SPEC x (DIFF_CONV tm')) in
2220   let th2 = prove(mk_eq(lhand(concl th1),bod),TRIG_IDENT_TAC x) in
2221   GEN x (GEN_REWRITE_RULE LAND_CONV [th2] th1);;
2222
2223 time ANTIDERIV_CONV `\x. sin(x) pow 3`;;
2224
2225 time ANTIDERIV_CONV `\x. sin(x) * sin(x) pow 5 * cos(x) pow 4 + cos(x)`;;
2226
2227 let FCT1_WEAK = prove
2228  (`(!x. (f diffl f'(x)) x) ==> !x. &0 <= x ==> defint(&0,x) f' (f x - f(&0))`,
2229   MESON_TAC[FTC1]);;
2230
2231 let INTEGRAL_CONV tm =
2232   let th1 = MATCH_MP FCT1_WEAK (ANTIDERIV_CONV tm) in
2233   (CONV_RULE REAL_RAT_REDUCE_CONV o
2234    REWRITE_RULE[SIN_0; COS_0; REAL_MUL_LZERO; REAL_MUL_RZERO] o
2235    CONV_RULE REAL_RAT_REDUCE_CONV o BETA_RULE) th1;;
2236
2237 INTEGRAL_CONV `\x. sin(x) pow 13`;;