1 (* ========================================================================= *)
3 (* ========================================================================= *)
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`;;
11 (* ========================================================================= *)
12 (* Propositional logic *)
13 (* ========================================================================= *)
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))`;;
49 ==> (o1 <=> ~i1) /\ (o2 <=> ~i2) /\ (o3 <=> ~i3)`;;
51 (* ========================================================================= *)
52 (* Abstractions and quantifiers *)
53 (* ========================================================================= *)
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))))`;;
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)`;;
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))`;;
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))`;;
80 MESON[] `(?!x. g(f x) = x) <=> (?!y. f(g y) = y)`;;
82 MESON [ADD_ASSOC; ADD_SYM] `m + (n + p) = n + (m + p)`;;
84 (* ========================================================================= *)
85 (* Tactics and tacticals *)
86 (* ========================================================================= *)
88 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
91 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
93 e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
95 e(ASM_REWRITE_TAC[]);;
96 e(CONV_TAC ARITH_RULE);;
97 let trivial = top_thm();;
99 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
100 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
102 e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
104 e(ASM_REWRITE_TAC[]);;
105 e(CONV_TAC ARITH_RULE);;
106 let trivial = top_thm();;
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();;
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);;
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);;
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);;
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);;
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);;
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);;
142 (* ========================================================================= *)
143 (* HOL's number systems *)
144 (* ========================================================================= *)
146 REAL_ARITH `!x y:real. (abs(x) - abs(y)) <= abs(x - y)`;;
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`;;
154 `!x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11:real.
162 x10 = abs(x9) - x8 /\
164 ==> x1 = x10 /\ x2 = x11`;;
166 REAL_ARITH `!x y:real. x < y ==> x < (x + y) / &2 /\ (x + y) / &2 < y`;;
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))`;;
175 ARITH_RULE `x < 2 ==> 2 * x + 1 < 4`;;
178 ARITH_RULE `~(2 * m + 1 = 2 * n)`;;
181 ARITH_RULE `x < 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
184 ARITH_RULE `x <= 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
188 ARITH_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
192 REAL_ARITH `!x y:real. x = y ==> x * y = y pow 2`;;
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) =
203 REAL_RING `a pow 2 = &2 /\ x pow 2 + a * x + &1 = &0 ==> x pow 4 + &1 = &0`;;
206 `(a * x pow 2 + b * x + c = &0) /\
207 (a * y pow 2 + b * y + c = &0) /\
209 ==> (a * x * y = c) /\ (a * (x + y) + b = &0)`;;
212 `p = (&3 * a1 - a2 pow 2) / &3 /\
213 q = (&9 * a1 * a2 - &27 * a0 - &2 * a2 pow 3) / &27 /\
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)`;;
220 REAL_FIELD `&0 < x ==> &1 / x - &1 / (&1 + x) = &1 / (x * (&1 + x))`;;
223 `s pow 2 = b pow 2 - &4 * a * c
224 ==> (a * x pow 2 + b * x + c = &0 <=>
227 if c = &0 then T else F
229 else x = (--b + s) / (&2 * a) \/ x = (--b + --s) / (&2 * a))`;;
231 (**** This needs an external SDP solver to assist with proof
233 needs "Examples/sos.ml";;
235 SOS_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
239 &0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4
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)`;;
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)`;;
254 SOS_CONV `&2 * x pow 4 + &2 * x pow 3 * y - x pow 2 * y pow 2 + &5 * y pow 4`;;
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`;;
263 needs "Examples/cooper.ml";;
265 COOPER_RULE `ODD n ==> 2 * n DIV 2 < n`;;
267 COOPER_RULE `!n. n >= 8 ==> ?a b. n = 3 * a + 5 * b`;;
269 needs "Rqe/make.ml";;
271 REAL_QELIM_CONV `!x. &0 <= x ==> ?y. y pow 2 = x`;;
273 (* ========================================================================= *)
274 (* Inductive definitions *)
275 (* ========================================================================= *)
277 (* ------------------------------------------------------------------------- *)
279 (* ------------------------------------------------------------------------- *)
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))`;;
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)`;;
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`;;
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);;
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]);;
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);;
319 (* ------------------------------------------------------------------------- *)
320 (* Verification of a simple concurrent program. *)
321 (* ------------------------------------------------------------------------- *)
323 let init = new_definition
324 `init (x,y,pc1,pc2,sem) <=>
325 pc1 = 10 /\ pc2 = 10 /\ x = 0 /\ y = 0 /\ sem = 1`;;
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)`;;
342 let mutex = new_definition
343 `mutex (x,y,pc1,pc2,sem) <=> pc1 = 10 \/ pc2 = 10`;;
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`;;
349 needs "Library/rstc.ml";;
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
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
368 (* ========================================================================= *)
369 (* Wellfounded induction *)
370 (* ========================================================================= *)
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`]);;
384 (* ========================================================================= *)
385 (* Changing proof style *)
386 (* ========================================================================= *)
388 let fix ts = MAP_EVERY X_GEN_TAC ts;;
391 DISCH_THEN(fun th -> if concl th = t then LABEL_TAC lab th
392 else failwith "assume");;
394 let we're finished tac = tac;;
396 let suffices_to_prove q tac = SUBGOAL_THEN q (fun th -> MP_TAC th THEN tac);;
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);;
402 let have t = note("",t);;
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));;
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];;
412 let trivial = MESON_TAC[];;
413 let algebra = CONV_TAC NUM_RING;;
414 let arithmetic = ARITH_TAC;;
416 let by labs tac = MAP_EVERY (fun l -> USE_THEN l MP_TAC) labs THEN tac;;
418 let using ths tac = MAP_EVERY MP_TAC ths THEN tac;;
420 let so constr arg tac = constr arg (FIRST_ASSUM MP_TAC THEN tac);;
423 (`!p q. p * p = 2 * q * q ==> q = 0`,
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
429 assume("A") `!m. m < p ==> !q. m * m = 2 * q * q ==> q = 0` 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);
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)]);;
443 (* ========================================================================= *)
444 (* Recursive definitions *)
445 (* ========================================================================= *)
448 `fib n = if n = 0 \/ n = 1 then 1 else fib(n - 1) + fib(n - 2)`;;
453 (fib2 (n + 2) = fib2(n) + fib2(n + 1))`;;
455 let halve = define `halve (2 * n) = n`;;
457 let unknown = define `unknown n = unknown(n + 1)`;;
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)`;;
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))`;;
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);;
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))`;;
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]);;
486 let BINOM_REFL = prove
487 (`!n. binom(n,n) = 1`,
488 INDUCT_TAC THEN ASM_SIMP_TAC[binom; BINOM_LT; LT; ARITH]);;
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);;
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]);;
513 (* ========================================================================= *)
514 (* Sets and functions *)
515 (* ========================================================================= *)
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[]);;
521 let INJECTIVE_IFF_LEFT_INVERSE = prove
522 (`(!x y. f x = f y ==> x = y) <=> (?g. g o f = I)`,
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[]);;
527 let cantor = new_definition
528 `cantor(x,y) = ((x + y) EXP 2 + 3 * x + y) DIV 2`;;
530 (**** Needs external SDP solver
532 needs "Examples/sos.ml";;
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);;
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]);;
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]);;
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);;
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
568 (* ========================================================================= *)
569 (* Inductive datatypes *)
570 (* ========================================================================= *)
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";;
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";;
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];;
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` ;;
588 let fano_clause (i,j) = mk_conj(mk_eq(p,fano_point i),mk_eq(l,fano_line j));;
590 parse_as_infix("ON",(11,"right"));;
592 let ON = new_definition
593 (mk_eq(`((ON):point->line->bool) p l`,
594 list_mk_disj(map fano_clause fano_incidence)));;
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`))
601 REWRITE_TAC[ON; distinctness "line"; distinctness "point"]);;
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]]);;
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]]);;
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]);;
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]);;
626 GEN_REWRITE_TAC DEPTH_CONV
627 [FORALL_POINT; EXISTS_LINE; EXISTS_POINT; FORALL_LINE] THEN
628 GEN_REWRITE_TAC DEPTH_CONV
630 [ON_CLAUSES; distinctness "point"; distinctness "line"]);;
632 let FANO_RULE tm = prove(tm,FANO_TAC);;
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`;;
638 let AXIOM_2 = FANO_RULE
639 `!l l'. ?p. p ON l /\ p ON l'`;;
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)`;;
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`;;
649 (* ========================================================================= *)
650 (* Semantics of programming languages *)
651 (* ========================================================================= *)
653 let string_INDUCT,string_RECURSION =
654 define_type "string = String (int list)";;
656 let expression_INDUCT,expression_RECURSION = define_type
657 "expression = Literal num
659 | Plus expression expression
660 | Times expression expression";;
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";;
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`);;
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)`;;
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'')`;;
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'`;;
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[]);;
705 let wlp = new_definition
706 `wlp c q s <=> !s'. sem c s s' ==> q s'`;;
708 let terminates = new_definition
709 `terminates c s <=> ?s'. sem c s s'`;;
711 let wp = new_definition
712 `wp c q s <=> terminates c s /\ wlp c q s`;;
715 (`!c. (wp c EMPTY = EMPTY)`,
716 REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; EMPTY] THEN MESON_TAC[]);;
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[]);;
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]);;
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]);;
734 let correct = new_definition
735 `correct p c q <=> p SUBSET (wp c q)`;;
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]);;
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]);;
745 let CORRECT_SEQ = prove
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]);;
751 (* ------------------------------------------------------------------------- *)
752 (* Need a fresh HOL session here; now doing shallow embedding. *)
753 (* ------------------------------------------------------------------------- *)
755 let assign = new_definition
756 `Assign (f:S->S) (q:S->bool) = q o f`;;
758 parse_as_infix(";;",(18,"right"));;
760 let sequence = new_definition
761 `(c1:(S->bool)->(S->bool)) ;; (c2:(S->bool)->(S->bool)) = c1 o c2`;;
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}`;;
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}`;;
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`;;
773 let while_def = new_definition
775 {s | !w. (!s:S. (if e(s) then c w s else q s) ==> w s) ==> w s}`;;
777 let monotonic = new_definition
778 `monotonic c <=> !q q'. q SUBSET q' ==> (c q) SUBSET (c q')`;;
780 let MONOTONIC_ASSIGN = prove
781 (`monotonic (Assign f)`,
782 SIMP_TAC[monotonic; assign; SUBSET; o_THM; IN]);;
784 let MONOTONIC_IF = prove
785 (`monotonic c ==> monotonic (If e c)`,
786 REWRITE_TAC[monotonic; if_def] THEN SET_TAC[]);;
788 let MONOTONIC_ITE = prove
789 (`monotonic c1 /\ monotonic c2 ==> monotonic (Ite e c1 c2)`,
790 REWRITE_TAC[monotonic; ite_def] THEN SET_TAC[]);;
792 let MONOTONIC_SEQ = prove
793 (`monotonic c1 /\ monotonic c2 ==> monotonic (c1 ;; c2)`,
794 REWRITE_TAC[monotonic; sequence; o_THM] THEN SET_TAC[]);;
796 let MONOTONIC_WHILE = prove
797 (`monotonic c ==> monotonic(While e c)`,
798 REWRITE_TAC[monotonic; while_def] THEN SET_TAC[]);;
800 let WHILE_THM = prove
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[]);;
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]);;
819 let correct = new_definition
820 `correct p c q <=> p SUBSET (c q)`;;
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]);;
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[]);;
830 let CORRECT_ASSIGN = prove
831 (`!p f q. (p SUBSET (q o f)) ==> correct p (Assign f) q`,
832 REWRITE_TAC[correct; assign]);;
834 let CORRECT_SEQ = prove
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[]);;
840 let CORRECT_ITE = prove
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[]);;
846 let CORRECT_IF = prove
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[]);;
852 let CORRECT_WHILE = prove
853 (`!(<<) p c q e invariant.
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]);;
875 let assert_def = new_definition
876 `assert (p:S->bool) (q:S->bool) = q`;;
878 let variant_def = new_definition
879 `variant ((<<):S->S->bool) (q:S->bool) = q`;;
881 let CORRECT_SEQ_VC = prove
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[]);;
887 let CORRECT_WHILE_VC = prove
888 (`!(<<) p c q e invariant.
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]);;
900 let MONOTONIC_ASSERT = prove
901 (`monotonic (assert p)`,
902 REWRITE_TAC[assert_def; monotonic]);;
904 let MONOTONIC_VARIANT = prove
905 (`monotonic (variant p)`,
906 REWRITE_TAC[variant_def; monotonic]);;
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];;
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];;
925 needs "Library/prime.ml";;
927 (* ------------------------------------------------------------------------- *)
929 (* while (!(x == 0 || y == 0)) *)
930 (* { if (x < y) y = y - x; *)
931 (* else x = x - y; *)
933 (* if (x == 0) x = y; *)
934 (* ------------------------------------------------------------------------- *)
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)`;;
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[]);;
958 e(SIMP_TAC[GCD_SUB; LT_IMP_LE]);;
961 e(SIMP_TAC[GCD_SUB; NOT_LT] THEN ARITH_TAC);;
963 e(MESON_TAC[GCD_0]);;
965 e(MESON_TAC[GCD_0; GCD_SYM]);;
967 parse_as_infix("refines",(12,"right"));;
969 let refines = new_definition
970 `c2 refines c1 <=> !q. c1(q) SUBSET c2(q)`;;
972 let REFINES_REFL = prove
974 REWRITE_TAC[refines; SUBSET_REFL]);;
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]);;
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]);;
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[]);;
988 let specification = new_definition
989 `specification(p,q) r = if q SUBSET r then p else {}`;;
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]);;
996 (* ========================================================================= *)
998 (* ========================================================================= *)
1000 needs "Library/prime.ml";;
1001 needs "Library/pocklington.ml";;
1002 needs "Library/binomial.ml";;
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;;
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;;
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]);;
1024 let LITTLE_CHECK_CONV tm =
1025 EQT_ELIM((RATOR_CONV(LAND_CONV NUM_EXP_CONV) THENC CONG_CONV) tm);;
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)`;;
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`]]);;
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`]);;
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]);;
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`]);;
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
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]]);;
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]);;
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];
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]);;
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]);;
1106 (* ========================================================================= *)
1108 (* ========================================================================= *)
1110 needs "Library/analysis.ml";;
1111 needs "Library/transc.ml";;
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)`;;
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]);;
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);;
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]);;
1140 let add_tm = `(+):num->num->num`
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');;
1148 let [pth0;pth1;pth2] = CONJUNCTS cheb in
1150 (GEN_REWRITE_CONV I [pth0; pth1] ORELSEC
1151 (LAND_CONV NUM_ADD2_CONV THENC
1152 GEN_REWRITE_CONV I [pth2] THENC
1154 (funpow 3 RAND_CONV ((LAND_CONV NUM_ADD_CONV) THENC conv))
1156 REAL_POLY_CONV)) tm in
1159 CHEB_CONV `cheb 8 x`;;
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
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`;
1175 CONV_TAC REAL_RING);;
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]);;
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
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);;
1196 (* ========================================================================= *)
1197 (* Embedding of logics *)
1198 (* ========================================================================= *)
1200 let string_INDUCT,string_RECURSION = define_type
1201 "string = String num";;
1203 parse_as_infix("&&",(16,"right"));;
1204 parse_as_infix("||",(15,"right"));;
1205 parse_as_infix("-->",(14,"right"));;
1206 parse_as_infix("<->",(13,"right"));;
1208 parse_as_prefix "Not";;
1209 parse_as_prefix "Box";;
1210 parse_as_prefix "Diamond";;
1212 let form_INDUCT,form_RECURSION = define_type
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')`;;
1238 let holds_in = new_definition
1239 `holds_in (W,R) p = !V w. w IN W ==> holds (W,R) V p w`;;
1241 parse_as_infix("|=",(11,"right"));;
1243 let valid = new_definition
1244 `L |= p <=> !f. L f ==> holds_in f p`;;
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)`;;
1251 let LTL = new_definition
1252 `LTL(W,R) <=> (W = UNIV) /\ !x y:num. R x y <=> x <= y`;;
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)`;;
1259 REWRITE_TAC[valid; FORALL_PAIR_THM; holds_in; holds] THEN MESON_TAC[];;
1261 let MODAL_RULE tm = prove(tm,MODAL_TAC);;
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`;;
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]);;
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]);;
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[]);;
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[]);;
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[]);;
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[]);;
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
1317 (* ------------------------------------------------------------------------- *)
1318 (* Need a fresh HOL session here: doing shallow embedding. *)
1319 (* ------------------------------------------------------------------------- *)
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"));;
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`;;
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'`;;
1338 let next = define `next p = \t:num. p(t + 1)`;;
1340 parse_as_infix("until",(17,"right"));;
1344 \t:num. ?t'. t <= t' /\ (!t''. t <= t'' /\ t'' < t' ==> p t'') /\ q t'`;;
1346 (* ========================================================================= *)
1347 (* HOL as a functional programming language *)
1348 (* ========================================================================= *)
1350 type ite = False | True | Atomic of int | Ite of ite*ite*ite;;
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)))
1360 let ite_INDUCT,ite_RECURSION = define_type
1361 "ite = False | True | Atomic num | Ite ite ite ite";;
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)))`;;
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))`;;
1383 EXISTS_TAC `MEASURE sizeof` THEN
1384 REWRITE_TAC[WF_MEASURE; MEASURE_LE; MEASURE; sizeof] THEN ARITH_TAC) in
1387 let norm = new_specification ["norm"] eth';;
1389 let SIZEOF_INDUCT = REWRITE_RULE[WF_IND; MEASURE] (ISPEC`sizeof` WF_MEASURE);;
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]);;
1395 let ITE_INDUCT = prove
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))
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]);;
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)`;;
1427 let NORMALIZED_NORM = prove
1428 (`!e. normalized(norm e)`,
1429 MATCH_MP_TAC ITE_INDUCT THEN REWRITE_TAC[norm; normalized]);;
1431 let NORMALIZED_INDUCT = prove
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]);;
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)`;;
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);;
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)`;;
1460 let tautology = define `tautology e = taut([],[]) (norm e)`;;
1462 let NORMALIZED_TAUT = prove
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))
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
1480 let TAUTOLOGY = prove
1481 (`!e. tautology e <=> !v. holds v e`,
1482 MESON_TAC[tautology; HOLDS_NORM; NORMALIZED_TAUT; MEM; NORMALIZED_NORM]);;
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);;
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)`];;
1500 let rec COMPUTE_DEPTH_CONV conv tm =
1502 (RATOR_CONV(LAND_CONV(COMPUTE_DEPTH_CONV conv)) THENC
1504 COMPUTE_DEPTH_CONV conv) tm
1505 else if is_conj tm then
1506 (LAND_CONV (COMPUTE_DEPTH_CONV conv) THENC
1508 COMPUTE_DEPTH_CONV conv) tm
1509 else if is_disj tm then
1510 (LAND_CONV (COMPUTE_DEPTH_CONV conv) THENC
1512 COMPUTE_DEPTH_CONV conv) tm
1514 (SUB_CONV (COMPUTE_DEPTH_CONV conv) THENC
1515 TRY_CONV(conv THENC COMPUTE_DEPTH_CONV conv)) tm;;
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`;;
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]);;
1525 time e (GEN_REWRITE_TAC COMPUTE_DEPTH_CONV [norm; taut; MEM; ARITH_EQ]);;
1527 ignore(b()); time e (REWRITE_TAC[norm; taut; MEM; ARITH_EQ]);;
1529 (* ========================================================================= *)
1531 (* ========================================================================= *)
1533 needs "Multivariate/vectors.ml";;
1535 needs "Examples/solovay.ml";;
1537 g `orthogonal (A - B) (C - B)
1538 ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`;;
1540 e SOLOVAY_VECTOR_TAC;;
1541 e(CONV_TAC REAL_RING);;
1543 g`!x y:real^N. x dot y <= norm x * norm y`;;
1544 e SOLOVAY_VECTOR_TAC;;
1546 (**** Needs external SDP solver
1547 needs "Examples/sos.ml";;
1549 e(CONV_TAC REAL_SOS);;
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);;
1556 needs "Rqe/make.ml";;
1557 let EXAMPLE_10 = prove
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);;
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)`]);;
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]);;
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]);;
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]);;
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]);;
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]);;
1596 parse_as_infix("cross",(20,"right"));;
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`;;
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;;
1609 let VEC3_RULE tm = prove(tm,VEC3_TAC);;
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)`;;
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)`;;
1620 let LEMMA_1 = VEC3_RULE `!u v. u dot (u cross v) = &0`;;
1622 let LEMMA_2 = VEC3_RULE `!u v. v dot (u cross v) = &0`;;
1624 let LEMMA_3 = VEC3_RULE `!u:real^3. vec 0 dot u = &0`;;
1626 let LEMMA_4 = VEC3_RULE `!u:real^3. u dot vec 0 = &0`;;
1628 let LEMMA_5 = VEC3_RULE `!x. x cross x = vec 0`;;
1630 let LEMMA_6 = VEC3_RULE
1632 ==> ~(u cross basis 1 = vec 0) \/
1633 ~(u cross basis 2 = vec 0) \/
1634 ~(u cross basis 3 = vec 0)`;;
1636 let LEMMA_7 = VEC3_RULE
1637 `!u v w. (u cross v = vec 0) ==> (u dot (v cross w) = &0)`;;
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]);;
1647 (* ========================================================================= *)
1648 (* Custom tactics *)
1649 (* ========================================================================= *)
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))];;
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);;
1677 let opairs = filter ortho (allpairs (fun a b -> a,b) points points);;
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);;
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;;
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]));;
1691 let SQRT_2_POW = prove
1692 (`sqrt(&2) pow 2 = &2`,
1693 SIMP_TAC[SQRT_POW_2; REAL_POS]);;
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);;
1701 let PROVE_ORTHOGONAL =
1702 let ptm = `orthogonal:real^3->real^3->bool` in
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);;
1708 let ppoint = let p = `P:real^3->bool` in fun v -> mk_comb(p,hol_of_point v);;
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
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)
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
1728 let a,b,_ = find (fun (a,b,c) -> c = x) prf_0 in DEDUCE_POINT_TAC [a;b]
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'
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];;
1743 let KOCHEN_SPECKER_LEMMA = prove
1744 (`!P. (!x y:real^3. ~(x = vec 0) /\ ~(y = vec 0) /\ orthogonal x 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))
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 [] []);;
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);;
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]);;
1774 (* ========================================================================= *)
1775 (* Defining new types *)
1776 (* ========================================================================= *)
1778 let direction_tybij = new_type_definition "direction" ("mk_dir","dest_dir")
1779 (MESON[LEMMA_0] `?x:real^3. ~(x = vec 0)`);;
1781 parse_as_infix("||",(11,"right"));;
1782 parse_as_infix("_|_",(11,"right"));;
1784 let perpdir = new_definition
1785 `x _|_ y <=> orthogonal (dest_dir x) (dest_dir y)`;;
1787 let pardir = new_definition
1788 `x || y <=> (dest_dir x) cross (dest_dir y) = vec 0`;;
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]);;
1795 let [PARDIR_REFL; PARDIR_SYM; PARDIR_TRANS] = (CONJUNCTS o prove)
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);;
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);;
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]);;
1814 let DIRECTION_AXIOM_3 = prove
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
1823 let CROSS_0 = VEC3_RULE `x cross vec 0 = vec 0 /\ vec 0 cross x = vec 0`;;
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
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]]);;
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);;
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]);;
1849 let line_tybij = define_quotient_type "line" ("mk_line","dest_line") `(||)`;;
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);;
1855 let perpl,perpl_th =
1856 lift_function (snd line_tybij) (PARDIR_REFL,PARDIR_TRANS)
1857 "perpl" PERPDIR_WELLDEF;;
1859 let line_lift_thm = lift_theorem line_tybij
1860 (PARDIR_REFL,PARDIR_SYM,PARDIR_TRANS) [perpl_th];;
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;;
1867 let point_tybij = new_type_definition "point" ("mk_point","dest_point")
1868 (prove(`?x:line. T`,REWRITE_TAC[]));;
1870 parse_as_infix("on",(11,"right"));;
1872 let on = new_definition `p on l <=> perpl (dest_point p) l`;;
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]);;
1880 let POINT_TAC th = REWRITE_TAC[on; POINT_CLAUSES] THEN ACCEPT_TAC th;;
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);;
1888 (`!l l'. ?p. p on l /\ p on l'`,
1889 POINT_TAC LINE_AXIOM_2);;
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);;
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);;
1901 (* ========================================================================= *)
1902 (* Custom inference rules *)
1903 (* ========================================================================= *)
1905 let near_ring_axioms =
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))`;;
1912 (**** Works eventually but takes a very long time
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`;;
1922 let is_realvar w x = is_var x & not(mem x w);;
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];;
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;;
1933 let rec lexord ord l1 l2 =
1935 (h1::t1,h2::t2) -> if ord h1 h2 then length t1 = length t2
1936 else h1 = h2 & lexord ord t1 t2
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;;
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";;
1955 let rec unify w env tp =
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";;
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
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;;
1971 let rec listcases fn rfn lis 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;;
1977 let LIST_MK_COMB f ths = rev_itlist (fun s t -> MK_COMB(t,s)) ths (REFL f);;
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 _ -> []);;
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));;
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;;
1997 let renamepair (th1,th2) = fixvariables "x" th1,fixvariables "y" th2;;
1999 let critical_pairs w tha thb =
2000 let th1,th2 = renamepair (tha,thb) in crit1 w th1 th2 @ crit1 w th2 th1;;
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";;
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");
2014 let left_reducible eqs eq =
2015 can (CHANGED_CONV(GEN_REWRITE_CONV (LAND_CONV o ONCE_DEPTH_CONV) eqs))
2018 let rec complete w (eqs,crits) =
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
2028 ocrits @ crits' @ itlist ((@) o critical_pairs w eq') eqs'' []
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
2036 let complete_equations wts eqs =
2037 let eqs' = map (normalize_and_orient wts []) eqs in
2038 complete wts ([],eqs');;
2040 complete_equations [`1`; `( * ):num->num->num`; `i:num->num`]
2041 [SPEC_ALL(ASSUME `!a b. i(a) * a * b = b`)];;
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)`)));;
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);;
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';;
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`;;
2062 e (DISCH_THEN(COMPLETE_TAC [`1`; `( * ):num->num->num`; `i:num->num`]));;
2063 e(ASM_REWRITE_TAC[]);;
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) =
2073 e (DISCH_THEN(COMPLETE_TAC
2074 [`0`; `(+):num->num->num`; `neg:num->num`; `( * ):num->num->num`]));;
2075 e(ASM_REWRITE_TAC[]);;
2077 (**** Could have done this instead
2078 e (DISCH_THEN(COMPLETE_TAC
2079 [`0`; `(+):num->num->num`; `( * ):num->num->num`; `neg:num->num`]));;
2082 (* ========================================================================= *)
2083 (* Linking external tools *)
2084 (* ========================================================================= *)
2087 let filename = Filename.temp_file "maxima" ".out" in
2089 "echo 'linel:10000; display2d:false;" ^ e ^
2090 ";' | maxima | grep '^(%o3)' | sed -e 's/^(%o3) //' >" ^
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;;
2098 let maxima_ops = ["+",`(+)`; "-",`(-)`; "*",`( * )`; "/",`(/)`; "^",`(pow)`];;
2099 let maxima_funs = ["sin",`sin`; "cos",`cos`];;
2101 let mk_uneg = curry mk_comb `(--)`;;
2105 fun tm -> let op,t = dest_comb tm in
2106 if op = ntm then t else failwith "dest_uneg";;
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);;
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 ^ ")";;
2121 string_of_hol `(x + sin(-- &2 * x)) pow 2 - cos(x - &22 / &7)`;;
2123 let lexe s = map (function Resword s -> s | Ident s -> s) (lex(explode s));;
2125 let parse_bracketed prs inp =
2127 ast,")"::rst -> ast,rst
2128 | _ -> failwith "Closing bracket expected";;
2130 let rec parse_ginfix op opup sof prs inp =
2132 e1,hop::rst when hop = op -> parse_ginfix op opup (opup sof e1) prs rst
2133 | e1,rest -> sof e1,rest;;
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);;
2142 let rec parse_atomic_expression inp =
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
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;;
2160 let hol_of_string = fst o parse_expression o lexe;;
2162 hol_of_string "sin(x) - cos(-(- - 1 + x))";;
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'));;
2169 FACTOR_CONV `&1234567890`;;
2171 FACTOR_CONV `x pow 6 - &1`;;
2173 FACTOR_CONV `r * (r * x * (&1 - x)) * (&1 - r * x * (&1 - x)) - x`;;
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);;
2184 ANTIDERIV_CONV `\x. (x + &5) pow 2 + &77 * x`;;
2186 ANTIDERIV_CONV `\x. sin(x) + x pow 11`;;
2188 (**** This one fails
2189 ANTIDERIV_CONV `\x. sin(x) pow 3`;;
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);;
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;;
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);;
2223 time ANTIDERIV_CONV `\x. sin(x) pow 3`;;
2225 time ANTIDERIV_CONV `\x. sin(x) * sin(x) pow 5 * cos(x) pow 4 + cos(x)`;;
2227 let FCT1_WEAK = prove
2228 (`(!x. (f diffl f'(x)) x) ==> !x. &0 <= x ==> defint(&0,x) f' (f x - f(&0))`,
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;;
2237 INTEGRAL_CONV `\x. sin(x) pow 13`;;
git://colo12-c703.uibk.ac.at / hl193./.git / blob