5 (* ------------------------------------------------------------------ *)
6 (* Theorems that construct and propagate equality and inequality *)
7 (* ------------------------------------------------------------------ *)
9 (* ------------------------------------------------------------------ *)
10 (* Propagation of =EQUAL= *)
11 (* ------------------------------------------------------------------ *)
13 unambiguous_interface();;
16 let REAL_MUL_LTIMES = prove (`!x a b. (x*.a = x*.b) ==> (~(x=(&.0))) ==> (a =b)`,
17 MESON_TAC[REAL_EQ_MUL_LCANCEL]);;
19 let REAL_MUL_RTIMES = prove (`!x a b. (a*.x = b*.x) ==> (~(x=(&.0))) ==> (a =b)`,
20 MESON_TAC[REAL_EQ_MUL_RCANCEL]);;
22 let REAL_PROP_EQ_LMUL = REAL_MUL_LTIMES;;
23 let REAL_PROP_EQ_RMUL = REAL_MUL_RTIMES;;
25 let REAL_PROP_EQ_LMUL_' = REAL_EQ_MUL_LCANCEL (* |- !x y z. (x * y = x * z) = (x = &0) \/ (y = z) *);;
26 let REAL_PROP_EQ_RMUL_' = REAL_EQ_MUL_LCANCEL (* |- !x y z. (x * z = y * z) = (x = y) \/ (z = &0) *);;
27 (* see also minor variations REAL_LT_LMUL_EQ, REAL_LT_RMUL_EQ *)
29 let REAL_PROP_EQ_SQRT = SQRT_INJ;; (* |- !x y. &0 <= x /\ &0 <= y ==> ((sqrt x = sqrt y) = x = y) *)
31 (* ------------------------------------------------------------------ *)
32 (* Construction of <=. *)
33 (* ------------------------------------------------------------------ *)
34 let REAL_MK_LE_SQUARE = REAL_LE_SQUARE_POW ;; (* |- !x. &0 <= x pow 2 *)
36 (* ------------------------------------------------------------------ *)
37 (* Propagation of <=. *)
38 (* ------------------------------------------------------------------ *)
40 let REAL_MUL_LTIMES_LE = prove (`!x a b. (x*.a <=. x*.b) ==> (&.0 < x) ==> (a <=. b)`,
41 MESON_TAC[REAL_LE_LMUL_EQ]);;
42 (* virtually identical to REAL_LE_LCANCEL_IMP, REAL_LE_LMUL_EQ *)
44 let REAL_MUL_RTIMES_LE = prove (`!x a b. (a*.x <=. b*.x) ==> (&.0 < x) ==> (a <=. b)`,
45 MESON_TAC[REAL_LE_RMUL_EQ]);;
46 (* virtually identical to REAL_LE_RCANCEL_IMP, REAL_LE_RMUL_EQ *)
48 let REAL_PROP_LE_LCANCEL = REAL_MUL_LTIMES_LE;;
49 let REAL_PROP_LE_RCANCEL = REAL_MUL_RTIMES_LE;;
50 let REAL_PROP_LE_LMUL = REAL_LE_LMUL (* |- !x y z. &0 <= x /\ y <= z ==> x * y <= x * z *);;
51 let REAL_PROP_LE_RMUL = REAL_LE_RMUL (* |- !x y z. x <= y /\ &0 <= z ==> x * z <= y * z *);;
52 let REAL_PROP_LE_LRMUL = REAL_LE_MUL2;; (* |- !w x y z. &0 <= w /\ w <= x /\ &0 <= y /\ y <= z ==> w * y <= x * z *)
53 let REAL_PROP_LE_POW = POW_LE;; (* |- !n x y. &0 <= x /\ x <= y ==> x pow n <= y pow n *)
54 let REAL_PROP_LE_SQRT = SQRT_MONO_LE_EQ;; (* |- !x y. &0 <= x /\ &0 <= y ==> (sqrt x <= sqrt y = x <= y) *)
56 (* ------------------------------------------------------------------ *)
57 (* Construction of LT *)
58 (* ------------------------------------------------------------------ *)
60 let REAL_MK_LT_SQUARE = REAL_LT_SQUARE;; (* |- !x. &0 < x * x = ~(x = &0) *)
62 (* ------------------------------------------------------------------ *)
63 (* Propagation of LT *)
64 (* ------------------------------------------------------------------ *)
66 let REAL_PROP_LT_LCANCEL = REAL_LT_LCANCEL_IMP (* |- !x y z. &0 < x /\ x * y < x * z ==> y < z *);;
67 let REAL_PROP_LT_RCANCEL = REAL_LT_RCANCEL_IMP (* |- !x y z. &0 < z /\ x * z < y * z ==> x < y *);;
68 let REAL_PROP_LT_LMUL = REAL_LT_LMUL (* |- !x y z. &0 < x /\ y < z ==> x * y < x * z *);;
69 let REAL_PROP_LT_RMUL = REAL_LT_RMUL (* |- !x y z. x < y /\ &0 < z ==> x * z < y * z *);;
70 (* minor variation REAL_LT_LMUL_IMP, REAL_LT_RMUL_IMP *)
72 let REAL_PROP_LT_LRMUL= REAL_LT_MUL2;; (* |- !w x y z. &0 <= w /\ w < x /\ &0 <= y /\ y < z ==> w * y < x * z *)
73 let REAL_PROP_LT_SQRT = SQRT_MONO_LT_EQ;; (* |- !x y. &0 <= x /\ &0 <= y ==> (sqrt x < sqrt y = x < y) *)
75 (* ------------------------------------------------------------------ *)
76 (* Constructors of Non-negative *)
77 (* ------------------------------------------------------------------ *)
79 let REAL_MK_NN_SQUARE = REAL_LE_SQUARE;; (* |- !x. &0 <= x * x *)
80 let REAL_MK_NN_ABS = ABS_POS;; (* |- !x. &0 <= abs x *)
82 (* ------------------------------------------------------------------ *)
83 (* Propagation of Non-negative *)
84 (* ------------------------------------------------------------------ *)
86 let REAL_PROP_NN_POS = prove(`! x y. x<. y ==> x <= y`,MESON_TAC[REAL_LT_LE]);;
87 let REAL_PROP_NN_ADD2 = REAL_LE_ADD (* |- !x y. &0 <= x /\ &0 <= y ==> &0 <= x + y *);;
88 let REAL_PROP_NN_DOUBLE = REAL_LE_DOUBLE (* |- !x. &0 <= x + x <=> &0 <= x *);;
89 let REAL_PROP_NN_RCANCEL= prove(`!x y. &.0 <. x /\ (&.0) <=. y*.x ==> ((&.0) <=. y)`,
90 MESON_TAC[REAL_PROP_LE_RCANCEL;REAL_MUL_LZERO]);;
91 let REAL_PROP_NN_LCANCEL= prove(`!x y. &.0 <. x /\ (&.0) <=. x*.y ==> ((&.0) <=. y)`,
92 MESON_TAC[REAL_PROP_LE_LCANCEL;REAL_MUL_RZERO]);;
93 let REAL_PROP_NN_MUL2 = REAL_LE_MUL (* |- !x y. &0 <= x /\ &0 <= y ==> &0 <= x * y *);;
94 let REAL_PROP_NN_POW = REAL_POW_LE (* |- !x n. &0 <= x ==> &0 <= x pow n *);;
95 let REAL_PROP_NN_SQUARE = REAL_LE_POW_2;; (* |- !x. &0 <= x pow 2 *)
96 let REAL_PROP_NN_SQRT = SQRT_POS_LE;; (* |- !x. &0 <= x ==> &0 <= sqrt x *)
97 let REAL_PROP_NN_INV = REAL_LE_INV_EQ (* |- !x. &0 <= inv x = &0 <= x *);;
98 let REAL_PROP_NN_SIN = SIN_POS_PI_LE;; (* |- !x. &0 <= x /\ x <= pi ==> &0 <= sin x *)
99 let REAL_PROP_NN_ATN = ATN_POS_LE;; (* |- &0 <= atn x = &0 <= x *)
102 (* ------------------------------------------------------------------ *)
103 (* Constructor of POS *)
104 (* ------------------------------------------------------------------ *)
106 let REAL_MK_POS_ABS = REAL_ABS_NZ (* |- !x. ~(x = &0) = &0 < abs x *);;
107 let REAL_MK_POS_EXP = REAL_EXP_POS_LT;; (* |- !x. &0 < exp x *)
108 let REAL_MK_POS_LN = LN_POS_LT;; (* |- !x. &1 < x ==> &0 < ln x *)
109 let REAL_MK_POS_PI = PI_POS;; (* |- &0 < pi *)
112 (* ------------------------------------------------------------------ *)
113 (* Propagation of POS *)
114 (* ------------------------------------------------------------------ *)
116 let REAL_PROP_POS_ADD2 = REAL_LT_ADD (* |- !x y. &0 < x /\ &0 < y ==> &0 < x + y *);;
117 let REAL_PROP_POS_LADD = REAL_LET_ADD (* |- !x y. &0 <= x /\ &0 < y ==> &0 < x + y *);;
118 let REAL_PROP_POS_RADD = REAL_LTE_ADD (* |- !x y. &0 < x /\ &0 <= y ==> &0 < x + y *);;
119 let REAL_PROP_POS_LMUL = REAL_LT_LMUL_0;; (* |- !x y. &0 < x ==> (&0 < x * y = &0 < y) *)
120 let REAL_PROP_POS_RMUL = REAL_LT_RMUL_0;; (* |- !x y. &0 < y ==> (&0 < x * y = &0 < x) *)
121 let REAL_PROP_POS_MUL2 = REAL_LT_MUL (* |- !x y. &0 < x /\ &0 < y ==> &0 < x * y *);;
122 let REAL_PROP_POS_SQRT = SQRT_POS_LT;; (* |- !x. &0 < x ==> &0 < sqrt x *)
123 let REAL_PROP_POS_POW = REAL_POW_LT (* |- !x n. &0 < x ==> &0 < x pow n *);;
124 let REAL_PROP_POS_INV = REAL_LT_INV (* |- !x. &0 < x ==> &0 < inv x *);;
125 let REAL_PROP_POS_SIN = SIN_POS_PI;; (* |- !x. &0 < x /\ x < pi ==> &0 < sin x *)
126 let REAL_PROP_POS_TAN = TAN_POS_PI2;; (* |- !x. &0 < x /\ x < pi / &2 ==> &0 < tan x *)
127 let REAL_PROP_POS_ATN = ATN_POS_LT;; (* |- &0 < atn x = &0 < x *)
129 (* ------------------------------------------------------------------ *)
130 (* Construction of NZ *)
131 (* ------------------------------------------------------------------ *)
133 (* renamed from REAL_MK_NZ_OF_POS *)
134 let REAL_MK_NZ_POS = REAL_POS_NZ (* |- !x. &0 < x ==> ~(x = &0) *);;
135 let REAL_MK_NZ_EXP = REAL_EXP_NZ;; (* |- !x. ~(exp x = &0) *)
137 (* ------------------------------------------------------------------ *)
138 (* Propagation of NZ *)
139 (* ------------------------------------------------------------------ *)
141 (* renamed from REAL_ABS_NZ, moved from float.ml *)
142 let REAL_PROP_NZ_ABS = prove(`!x. (~(x = (&.0))) ==> (~(abs(x) = (&.0)))`,
143 REWRITE_TAC[ABS_ZERO]);;
144 let REAL_PROP_NZ_POW = REAL_POW_NZ (* |- !x n. ~(x = &0) ==> ~(x pow n = &0) *);;
145 let REAL_PROP_NZ_INV = REAL_INV_NZ;; (* |- !x. ~(x = &0) ==> ~(inv x = &0) *)
148 (* ------------------------------------------------------------------ *)
149 (* Propagation of ZERO *)
150 (* ------------------------------------------------------------------ *)
152 let REAL_PROP_ZERO_ABS = REAL_ABS_ZERO (* |- !x. (abs x = &0) = x = &0); *);;
153 let REAL_PROP_ZERO_NEG = REAL_NEG_EQ_0 ;; (* |- !x. (--x = &0) = x = &0 *)
154 let REAL_PROP_ZERO_INV = REAL_INV_EQ_0 (* |- !x. (inv x = &0) = x = &0 *);;
155 let REAL_PROP_ZERO_NEG = REAL_NEG_EQ0;; (* |- !x. (--x = &0) = x = &0 *)
156 let REAL_PROP_ZERO_SUMSQ = REAL_SUMSQ;; (* |- !x y. (x * x + y * y = &0) = (x = &0) /\ (y = &0) *)
157 let REAL_PROP_ZERO_POW = REAL_POW_EQ_0;; (* |- !x n. (x pow n = &0) = (x = &0) /\ ~(n = 0) *)
158 let REAL_PROP_ZERO_SQRT = SQRT_EQ_0;; (* |- !x. &0 <= x ==> (x / sqrt x = sqrt x) *)
160 (* ------------------------------------------------------------------ *)
161 (* Special values of functions *)
162 (* ------------------------------------------------------------------ *)
164 let REAL_SV_LADD_0 = REAL_ADD_LID (* |- !x. &0 + x = x); *);;
165 let REAL_SV_INV_0 = REAL_INV_0 (* |- inv (&0) = &0 *);;
166 let REAL_SV_RMUL_0 = REAL_MUL_RZERO (* |- !x. x * &0 = &0 *);;
167 let REAL_SV_LMUL_0 = REAL_MUL_LZERO (* |- !x. &0 * x = &0 *);;
168 let REAL_SV_NEG_0 = REAL_NEG_0 (* |- -- &0 = &0 *);;
169 let REAL_SV_ABS_0 = REAL_ABS_0 (* |- abs (&0) = &0 *);;
170 let REAL_SV_EXP_0 = REAL_EXP_0;; (* |- exp (&0) = &1 *)
171 let REAL_SV_LN_1 = LN_1;; (* |- ln (&1) = &0 *)
172 let REAL_SV_SQRT_0 = SQRT_0;; (* |- sqrt (&0) = &0 *)
173 let REAL_SV_TAN_0 = TAN_0;; (* |- tan (&0) = &0 *)
174 let REAL_SV_TAN_PI = TAN_PI;; (* |- tan pi = &0 *)
176 (* ------------------------------------------------------------------ *)
177 (* A tactic that multiplies a real on the left *)
178 (* ------------------------------------------------------------------ *)
181 #g `a:real = b:real`;;
182 #e (REAL_LMUL_TAC `c:real`);;
183 it : goalstack = 2 subgoals (2 total)
191 (* ------------------------------------------------------------------ *)
195 let REAL_LMUL_TAC t =
196 let REAL_MUL_LTIMES =
198 (((~(x=(&0)) ==> (x*a = x*b)) /\ ~(x=(&0))) ==> (a = b))`),
199 MESON_TAC[REAL_EQ_MUL_LCANCEL]) in
200 (MATCH_MP_TAC (SPEC t REAL_MUL_LTIMES))
202 THENL [DISCH_TAC; ALL_TAC];;
204 (* ------------------------------------------------------------------ *)
205 (* Right multiply by a real *)
206 (* ------------------------------------------------------------------ *)
208 let REAL_RMUL_TAC t =
209 let REAL_MUL_RTIMES =
211 ((~(x=(&0))==>(a*x = b*x)) /\ ~(x=(&0))) ==> (a = b)`,
212 MESON_TAC[REAL_EQ_MUL_RCANCEL]) in
213 (MATCH_MP_TAC (SPEC t REAL_MUL_RTIMES))
215 THENL [DISCH_TAC; ALL_TAC];;