Update from HH
[hl193./.git] / Tutorial / HOLs_number_systems.ml
1 REAL_ARITH `!x y:real. (abs(x) - abs(y)) <= abs(x - y)`;;
2
3 INT_ARITH
4  `!a b a' b' D:int.
5      (a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) =
6      (a * a' + D * b * b') pow 2 - D * (a * b' + a' * b) pow 2`;;
7
8 REAL_ARITH
9  `!x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11:real.
10         x3 = abs(x2) - x1 /\
11         x4 = abs(x3) - x2 /\
12         x5 = abs(x4) - x3 /\
13         x6 = abs(x5) - x4 /\
14         x7 = abs(x6) - x5 /\
15         x8 = abs(x7) - x6 /\
16         x9 = abs(x8) - x7 /\
17         x10 = abs(x9) - x8 /\
18         x11 = abs(x10) - x9
19         ==> x1 = x10 /\ x2 = x11`;;
20
21 REAL_ARITH `!x y:real. x < y ==> x < (x + y) / &2 /\ (x + y) / &2 < y`;;
22
23 REAL_ARITH
24  `((x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2) =
25   ((&1 / &6) * ((x1 + x2) pow 4 + (x1 + x3) pow 4 + (x1 + x4) pow 4 +
26                 (x2 + x3) pow 4 + (x2 + x4) pow 4 + (x3 + x4) pow 4) +
27    (&1 / &6) * ((x1 - x2) pow 4 + (x1 - x3) pow 4 + (x1 - x4) pow 4 +
28                 (x2 - x3) pow 4 + (x2 - x4) pow 4 + (x3 - x4) pow 4))`;;
29
30 ARITH_RULE `x < 2 ==> 2 * x + 1 < 4`;;
31
32 (**** Fails
33 ARITH_RULE `~(2 * m + 1 = 2 * n)`;;
34  ****)
35
36 ARITH_RULE `x < 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
37
38 (**** Fails
39 ARITH_RULE `x <= 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
40  ****)
41
42 (**** Fails
43 ARITH_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
44  ****)
45
46 (**** Fails
47 REAL_ARITH `!x y:real. x = y ==> x * y = y pow 2`;;
48  ****)
49
50 prioritize_real();;
51
52 REAL_RING
53   `s = (a + b + c) / &2
54    ==> s * (s - b) * (s - c) + s * (s - c) * (s - a) +
55        s * (s - a) * (s - b) - (s - a) * (s - b) * (s - c) =
56        a * b * c`;;
57
58 REAL_RING `a pow 2 = &2 /\ x pow 2 + a * x + &1 = &0 ==> x pow 4 + &1 = &0`;;
59
60 REAL_RING
61  `(a * x pow 2 + b * x + c = &0) /\
62   (a * y pow 2 + b * y + c = &0) /\
63   ~(x = y)
64   ==> (a * x * y = c) /\ (a * (x + y) + b = &0)`;;
65
66 REAL_RING
67  `p = (&3 * a1 - a2 pow 2) / &3 /\
68   q = (&9 * a1 * a2 - &27 * a0 - &2 * a2 pow 3) / &27 /\
69   x = z + a2 / &3 /\
70   x * w = w pow 2 - p / &3
71   ==> (z pow 3 + a2 * z pow 2 + a1 * z + a0 = &0 <=>
72        if p = &0 then x pow 3 = q
73        else (w pow 3) pow 2 - q * (w pow 3) - p pow 3 / &27 = &0)`;;
74
75 REAL_FIELD `&0 < x ==> &1 / x - &1 / (&1 + x) = &1 / (x * (&1 + x))`;;
76
77 REAL_FIELD
78 `s pow 2 = b pow 2 - &4 * a * c
79  ==> (a * x pow 2 + b * x + c = &0 <=>
80       if a = &0 then
81          if b = &0 then
82             if c = &0 then T else F
83          else x = --c / b
84       else x = (--b + s) / (&2 * a) \/ x = (--b + --s) / (&2 * a))`;;
85
86 (**** This needs an external SDP solver to assist with proof
87
88 needs "Examples/sos.ml";;
89
90 SOS_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
91
92 REAL_SOS
93  `!a1 a2 a3 a4:real.
94       &0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4
95       ==> a1 pow 2 +
96           ((a1 + a2) / &2) pow 2 +
97           ((a1 + a2 + a3) / &3) pow 2 +
98           ((a1 + a2 + a3 + a4) / &4) pow 2
99          <= &4 * (a1 pow 2 + a2 pow 2 + a3 pow 2 + a4 pow 2)`;;
100
101 REAL_SOS
102  `!a b c:real.
103       a >= &0 /\ b >= &0 /\ c >= &0
104       ==> &3 / &2 * (b + c) * (a + c) * (a + b) <=
105           a * (a + c) * (a + b) +
106           b * (b + c) * (a + b) +
107           c * (b + c) * (a + c)`;;
108
109 SOS_CONV `&2 * x pow 4 + &2 * x pow 3 * y - x pow 2 * y pow 2 + &5 * y pow 4`;;
110
111 PURE_SOS
112 `x pow 4 + &2 * x pow 2 * z + x pow 2 - &2 * x * y * z +
113           &2 * y pow 2 * z pow 2 + &2 * y * z pow 2 + &2 * z pow 2 - &2 * x +
114           &2 *  y * z + &1 >= &0`;;
115
116 ****)
117
118 needs "Examples/cooper.ml";;
119
120 COOPER_RULE `ODD n ==> 2 * n DIV 2 < n`;;
121
122 COOPER_RULE `!n. n >= 8 ==> ?a b. n = 3 * a + 5 * b`;;
123
124 needs "Rqe/make.ml";;
125
126 REAL_QELIM_CONV `!x. &0 <= x ==> ?y. y pow 2 = x`;;