IntervalArithScript.sml 17.4 KB
 Heiko Becker committed Jan 03, 2017 1 2 3 4 5 ``````(** Formalization of real valued interval arithmetic Used in soundness proofs for error bound validator. **) open preamble `````` Heiko Becker committed Jan 05, 2017 6 ``````open realTheory realLib RealArith `````` Heiko Becker committed Feb 27, 2017 7 ``````open AbbrevsTheory ExpressionsTheory RealSimpsTheory; `````` Heiko Becker committed Jan 03, 2017 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 `````` val _ = new_theory "IntervalArith"; (** Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound. Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound. **) val valid_def = Define ` valid (iv:interval) = (IVlo iv <= IVhi iv)`; val contained_def = Define ` contained (a:real) (iv:interval) = (IVlo iv <= a /\ a <= IVhi iv)`; (** Subset definition; when an interval is a subinterval of another **) val isSupersetInterval_def = Define ` isSupersetInterval (iv1:interval) (iv2:interval) = ((IVlo iv2 <= IVlo iv1) /\ (IVhi iv1 <= IVhi iv2))`; val pointInterval_def = Define `pointInterval (x:real) = (x,x)`; (** Definitions of validity conditions for interval operations: Addition, Subtraction, Multiplication and Division **) val validIntervalAdd_def = Define ` validIntervalAdd (iv1:interval) (iv2:interval) (iv3:interval) = (! a b. contained a iv1 /\ contained b iv2 ==> contained (a + b) iv3)`; val validIntervalSub_def = Define ` validIntervalSub (iv1:interval) (iv2:interval) (iv3:interval) = (! a b. contained a iv1 /\ contained b iv2 ==> contained (a - b) iv3)`; val validIntervalMult_def = Define` validIntervalMult (iv1:interval) (iv2:interval) (iv3:interval) = (! a b. contained a iv1 /\ contained b iv2 ==> contained (a * b) iv3)`; val validIntervalDiv_def = Define ` validIntervalDiv (iv1:interval) (iv2:interval) (iv3:interval) = (! a b. contained a iv1 /\ contained b iv2 ==> contained (a / b) iv3)`; val min4_def = Define ` min4 a b c d = min a (min b (min c d))`; val max4_def = Define ` max4 a b c d = max a (max b (max c d))`; val absIntvUpd_def = Define ` absIntvUpd (op:real->real->real) (iv1:interval) (iv2:interval) = ( min4 (op (IVlo iv1) (IVlo iv2)) (op (IVlo iv1) (IVhi iv2)) (op (IVhi iv1) (IVlo iv2)) (op (IVhi iv1) (IVhi iv2)), max4 (op (IVlo iv1) (IVlo iv2)) (op (IVlo iv1) (IVhi iv2)) (op (IVhi iv1) (IVlo iv2)) (op (IVhi iv1) (IVhi iv2)) )`; val widenInterval_def = Define ` widenInterval (iv:interval) (v:real) = ((IVlo iv - v), (IVhi iv + v))`; val negateInterval_def = Define ` negateInterval (iv:interval) = ((- IVhi iv), (- IVlo iv))`; val invertInterval_def = Define ` `````` Heiko Becker committed Jan 31, 2017 76 ``````invertInterval (iv:interval) = (1 /(IVhi iv), 1 /(IVlo iv))`; `````` Heiko Becker committed Jan 03, 2017 77 78 79 80 81 82 83 84 85 86 87 88 89 `````` val addInterval_def = Define ` addInterval (iv1:interval) (iv2:interval) = absIntvUpd (+) iv1 iv2`; val subtractInterval_def = Define ` subtractInterval (iv1:interval) (iv2:interval) = addInterval iv1 (negateInterval iv2)`; val multInterval_def = Define ` multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2`; val divideInterval_def = Define ` divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)`; `````` Heiko Becker committed Mar 06, 2017 90 91 ``````val maxAbs_def = Define ` maxAbs iv = max (abs (FST iv)) (abs (SND iv))`; `````` Heiko Becker committed Jan 03, 2017 92 `````` `````` Heiko Becker committed Jan 13, 2017 93 94 ``````val minAbsFun_def = Define ` minAbsFun iv = min (abs (FST iv)) (abs (SND iv))`; `````` Heiko Becker committed Jan 03, 2017 95 96 97 98 99 100 101 102 103 104 105 `````` val iv_ss = [IVlo_def, IVhi_def, valid_def, contained_def, isSupersetInterval_def, pointInterval_def, validIntervalAdd_def, validIntervalSub_def, validIntervalMult_def, validIntervalDiv_def, min4_def, max4_def, absIntvUpd_def, widenInterval_def, negateInterval_def, invertInterval_def, addInterval_def, subtractInterval_def, multInterval_def, divideInterval_def, `````` Heiko Becker committed Mar 06, 2017 106 `````` maxAbs_def, minAbsFun_def `````` Heiko Becker committed Jan 03, 2017 107 108 `````` ]; `````` Heiko Becker committed Jan 03, 2017 109 ``````val contained_implies_valid = store_thm ("contained_implies_valid", `````` Heiko Becker committed Jan 10, 2017 110 111 112 ````````!(a:real) (iv:interval). contained a iv ==> valid iv``, metis_tac (iv_ss @ [REAL_LE_TRANS])); `````` Heiko Becker committed Jan 03, 2017 113 `````` `````` Heiko Becker committed Jan 03, 2017 114 ``````val contained_implies_subset = store_thm ("contained_implies_subset", `````` Heiko Becker committed Jan 10, 2017 115 116 ````````!(a:real) (iv:interval). contained a iv ==> isSupersetInterval (pointInterval a) iv``, `````` Heiko Becker committed Jan 03, 2017 117 118 ``````fs iv_ss); `````` Heiko Becker committed Jan 10, 2017 119 120 121 122 ``````val validPointInterval = store_thm("validPointInterval", ``!(a:real). contained a (pointInterval a)``, fs iv_ss); `````` Heiko Becker committed Jan 03, 2017 123 `````` `````` Heiko Becker committed Jan 03, 2017 124 ``````val min4_correct = store_thm ("min4_correct", `````` Heiko Becker committed Jan 10, 2017 125 126 127 128 129 130 131 ````````!a b c d. let m = min4 a b c d in m <= a /\ m <= b /\ m <= c /\ m <= d``, rpt strip_tac \\fs [min4_def] \\ conj_tac \\ try (fs [REAL_MIN_LE1]) \\ conj_tac >- (`min b (min c d) <= b` by fs[REAL_MIN_LE1] \\ match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 132 133 134 135 `````` HINT_EXISTS_TAC \\ fs [REAL_MIN_LE2]) >- (conj_tac >- (`min c d <= c` by fs [REAL_MIN_LE1] \\ `````` Heiko Becker committed Jan 10, 2017 136 `````` match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 137 138 `````` HINT_EXISTS_TAC \\ fs [REAL_MIN_LE2] \\ `````` Heiko Becker committed Jan 10, 2017 139 `````` match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 140 141 `````` `min b (min c d) <= min c d` by fs[REAL_MIN_LE2] \\ HINT_EXISTS_TAC \\ `````` Heiko Becker committed Jan 10, 2017 142 `````` fs [REAL_MIN_LE2] ) `````` Heiko Becker committed Jan 03, 2017 143 `````` >- (`min c d <= d` by fs [REAL_MIN_LE2] \\ `````` Heiko Becker committed Jan 10, 2017 144 `````` match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 145 146 `````` HINT_EXISTS_TAC \\ fs [REAL_MIN_LE2] \\ `````` Heiko Becker committed Jan 10, 2017 147 `````` match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 148 149 150 151 `````` `min b (min c d) <= min c d` by fs[REAL_MIN_LE2] \\ HINT_EXISTS_TAC \\ fs [REAL_MIN_LE2]))); `````` Heiko Becker committed Jan 03, 2017 152 ``````val max4_correct = store_thm ("max4_correct", `````` Heiko Becker committed Jan 10, 2017 153 154 155 156 157 ````````!a b c d. let m = max4 a b c d in a <= m /\ b <= m /\ c <= m /\ d <= m``, rpt strip_tac \\fs [max4_def] \\ conj_tac \\ try (fs [REAL_LE_MAX1]) \\ conj_tac `````` Heiko Becker committed Jan 03, 2017 158 ``````>-(`b <= max b (max c d)` by fs[REAL_LE_MAX1] \\ `````` Heiko Becker committed Jan 10, 2017 159 ``````match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 160 161 162 163 ``````HINT_EXISTS_TAC \\ fs [REAL_LE_MAX2]) >- (conj_tac >- (`c <= max c d` by fs [REAL_LE_MAX1] \\ `````` Heiko Becker committed Jan 10, 2017 164 `````` match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 165 166 `````` HINT_EXISTS_TAC \\ fs [REAL_LE_MAX2] \\ `````` Heiko Becker committed Jan 10, 2017 167 `````` match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 168 169 170 171 `````` `max c d <= max b (max c d)` by fs[REAL_LE_MAX2] \\ HINT_EXISTS_TAC \\ fs [REAL_LE_MAX2] ) >- (`d <= max c d` by fs [REAL_LE_MAX2] \\ `````` Heiko Becker committed Jan 10, 2017 172 `````` match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 173 174 `````` HINT_EXISTS_TAC \\ fs [REAL_LE_MAX2] \\ `````` Heiko Becker committed Jan 10, 2017 175 `````` match_mp_tac REAL_LE_TRANS \\ `````` Heiko Becker committed Jan 03, 2017 176 `````` `max c d <= max b (max c d)` by fs[REAL_LE_MAX2] \\ `````` Heiko Becker committed Jan 10, 2017 177 178 `````` HINT_EXISTS_TAC \\ fs [REAL_LE_MAX2] ))); `````` Heiko Becker committed Jan 03, 2017 179 `````` `````` Heiko Becker committed Jan 03, 2017 180 181 `````` val interval_negation_valid = store_thm ("interval_negation_valid", `````` Heiko Becker committed Jan 10, 2017 182 183 ````````!iv a. contained a iv ==> contained (- a) (negateInterval iv)``, `````` Heiko Becker committed Jan 03, 2017 184 185 ``````fs iv_ss); `````` Heiko Becker committed Jan 04, 2017 186 ``````val interval_inversion_valid = store_thm ("interval_inversion_valid", `````` Heiko Becker committed Jan 10, 2017 187 188 189 ````````!iv a. (IVhi iv < 0 \/ 0 < IVlo iv) /\ contained a iv ==> contained (inv a) (invertInterval iv)``, `````` Heiko Becker committed Jan 31, 2017 190 ``````fs iv_ss \\ rpt strip_tac \\ once_rewrite_tac [GSYM REAL_INV_1OVER] `````` Heiko Becker committed Jan 04, 2017 191 ``````(* First subgoal *) `````` Heiko Becker committed Jan 10, 2017 192 ``````>- (once_rewrite_tac [GSYM REAL_LE_NEG] \\ `````` 193 194 195 196 `````` `0 < - a` by REAL_ASM_ARITH_TAC \\ `a <> 0` by REAL_ASM_ARITH_TAC \\ `0 < - SND iv` by REAL_ASM_ARITH_TAC \\ `SND iv <> 0` by REAL_ASM_ARITH_TAC \\ `````` Heiko Becker committed Jan 10, 2017 197 198 199 200 `````` `-a⁻¹ = (-a)⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp[]) \\ `-(SND iv)⁻¹ = (-(SND iv))⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp []) \\ asm_rewrite_tac [] \\ `inv(-a) ≤ inv (-SND iv) <=> (- SND iv) <= - a` by match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) `````` Heiko Becker committed Jan 04, 2017 201 ``````(* Second subgoal *) `````` Heiko Becker committed Jan 10, 2017 202 203 204 205 206 207 208 209 210 211 212 ``````>- (once_rewrite_tac [GSYM REAL_LE_NEG] \\ `a < 0` by REAL_ASM_ARITH_TAC \\ `0 < -a` by REAL_ASM_ARITH_TAC \\ `- a <> 0` by REAL_ASM_ARITH_TAC \\ `a <> 0` by REAL_ASM_ARITH_TAC \\ `-a⁻¹ = (-a)⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp []) \\ `-(FST iv)⁻¹ = (-(FST iv))⁻¹` by (match_mp_tac REAL_NEG_INV \\ simp [] \\ try REAL_ASM_ARITH_TAC \\ asm_rewrite_tac []) \\ `inv (- (FST iv)) <= inv (- a) <=> - a <= - (FST iv)` by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\ REAL_ASM_ARITH_TAC) `````` Heiko Becker committed Jan 04, 2017 213 ``````(* Third subgoal *) `````` Heiko Becker committed Jan 10, 2017 214 215 216 217 ``````>- (rewrite_tac [GSYM REAL_INV_1OVER] \\ `inv (SND iv) <= inv a <=> a <= SND iv` by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\ REAL_ASM_ARITH_TAC) `````` Heiko Becker committed Jan 04, 2017 218 ``````(* Fourth subgoal *) `````` Heiko Becker committed Jan 10, 2017 219 220 221 222 ``````>- (rewrite_tac [GSYM REAL_INV_1OVER] \\ `inv a <= inv (FST iv) <=> FST iv <= a` by (match_mp_tac REAL_INV_LE_ANTIMONO \\ fs []) \\ REAL_ASM_ARITH_TAC)); `````` Heiko Becker committed Jan 04, 2017 223 224 225 `````` val interval_addition_valid = store_thm ("interval_addition_valid", ``!iv1 iv2. validIntervalAdd iv1 iv2 (addInterval iv1 iv2)``, `````` Heiko Becker committed Jan 10, 2017 226 ``````fs iv_ss \\ rpt strip_tac `````` Heiko Becker committed Jan 04, 2017 227 ``````(* First subgoal, lower bound *) `````` Heiko Becker committed Jan 10, 2017 228 229 230 231 ``````>- (`FST iv1 + FST iv2 <= a + b` by (match_mp_tac REAL_LE_ADD2 \\ fs []) \\ match_mp_tac REAL_LE_TRANS \\ HINT_EXISTS_TAC \\ strip_tac \\ fs[REAL_MIN_LE1]) `````` Heiko Becker committed Jan 04, 2017 232 ``````(* Second subgoal, upper bound *) `````` Heiko Becker committed Jan 10, 2017 233 234 235 236 ``````>- (`a + b <= SND iv1 + SND iv2` by (match_mp_tac REAL_LE_ADD2 \\ fs []) \\ match_mp_tac REAL_LE_TRANS \\ HINT_EXISTS_TAC \\ strip_tac \\ fs [REAL_LE_MAX])); `````` Heiko Becker committed Jan 04, 2017 237 238 `````` val interval_subtraction_valid = store_thm ("interval_subtraction_valid", `````` Heiko Becker committed Jan 10, 2017 239 240 241 242 243 244 ````````!iv1 iv2. validIntervalSub iv1 iv2 (subtractInterval iv1 iv2)``, rpt gen_tac \\ Cases_on `iv2` \\ rewrite_tac (iv_ss @ [real_sub]) \\ rpt gen_tac \\ strip_tac \\ (** TODO: FIXME, use qspecl_then or sth else **) match_mp_tac (REWRITE_RULE (iv_ss @ [FST,SND]) (SPECL [``iv1:interval``,``(-r,-q):interval``] interval_addition_valid)) \\ `````` Heiko Becker committed Jan 04, 2017 245 ``````fs []); `````` Heiko Becker committed Jan 03, 2017 246 `````` `````` Heiko Becker committed Jan 04, 2017 247 ``````val interval_multiplication_valid = store_thm ("interval_multiplication_valid", `````` Heiko Becker committed Jan 10, 2017 248 249 250 ````````!iv1 iv2 a b. contained a iv1 /\ contained b iv2 ==> contained (a * b) (multInterval iv1 iv2)``, fs iv_ss \\ rpt strip_tac `````` Heiko Becker committed Jan 04, 2017 251 252 ``````(* Lower Bound *) (* Case distinction for a *) `````` Heiko Becker committed Jan 10, 2017 253 ``````>- (qspecl_then [`a`,`0`] DISJ_CASES_TAC REAL_LTE_TOTAL `````` Heiko Becker committed Jan 04, 2017 254 255 256 `````` (* First case: a < 0 *) >- (`a <= 0 /\ a <> 0` by fs[REAL_LT_LE] \\ (* Case distinction for SND iv2 *) `````` Heiko Becker committed Jan 10, 2017 257 `````` qspecl_then [`SND iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL `````` Heiko Becker committed Jan 04, 2017 258 `````` (* First case: SND iv2 < 0 *) `````` Heiko Becker committed Jan 10, 2017 259 260 261 262 263 264 265 266 267 268 269 270 271 `````` >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``SND (iv1:interval) * SND (iv2:interval)`` \\ conj_tac >- (qspecl_then [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`] (fn thm => rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)]) min4_correct) >- (once_rewrite_tac[REAL_MUL_SYM] \\ match_mp_tac REAL_LE_TRANS \\ exists_tac ``SND (iv2:interval) * (a:real)`` \\ conj_tac >- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ `````` Heiko Becker committed Jan 04, 2017 272 `````` fs [REAL_LT_LE]) `````` Heiko Becker committed Jan 10, 2017 273 274 `````` >- (once_rewrite_tac [REAL_MUL_SYM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ `````` Heiko Becker committed Jan 04, 2017 275 276 `````` fs []))) (* Second case: 0 <= SND iv2 *) `````` Heiko Becker committed Jan 10, 2017 277 278 279 280 281 282 283 284 285 286 287 `````` >- (match_mp_tac REAL_LE_TRANS\\ exists_tac ``FST (iv1:interval) * SND (iv2:interval)`` \\ conj_tac >- (qspecl_then [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`] (fn thm => rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)]) min4_correct) >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``(a:real) * SND (iv2:interval)`` \\ conj_tac \\ fs[REAL_LE_RMUL_IMP, REAL_MUL_LE_COMPAT_NEG_L]))) `````` Heiko Becker committed Jan 04, 2017 288 289 `````` (* Second case: 0 <= a*) (* Case distinction for FST iv2 *) `````` Heiko Becker committed Jan 10, 2017 290 `````` >- (qspecl_then [`FST iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL `````` Heiko Becker committed Jan 04, 2017 291 `````` (* First case: FST iv2 < 0 *) `````` Heiko Becker committed Jan 10, 2017 292 293 294 295 296 297 298 299 300 301 302 303 304 `````` >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``SND (iv1:interval) * FST (iv2:interval)`` \\ conj_tac >- (qspecl_then [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`] (fn thm => rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)]) min4_correct) >- (once_rewrite_tac [REAL_MUL_SYM] \\ match_mp_tac REAL_LE_TRANS \\ exists_tac ``FST (iv2:interval) * (a:real)`` \\ conj_tac >- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ fs[REAL_LT_LE]) `````` Heiko Becker committed Jan 04, 2017 305 306 `````` >- (fs [REAL_LE_RMUL_IMP]))) (* Second case: 0 <= FST iv2 *) `````` Heiko Becker committed Jan 10, 2017 307 308 309 310 311 312 313 314 315 316 317 `````` >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``FST (iv1:interval) * FST (iv2:interval)`` \\ conj_tac >- (qspecl_then [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`] (fn thm => rewrite_tac [SIMP_RULE bool_ss [min4_def] (CONV_RULE let_CONV thm)]) min4_correct) >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``a:real * FST (iv2:interval)`` \\ conj_tac \\ fs [REAL_LE_RMUL_IMP, REAL_LE_LMUL_IMP])))) `````` Heiko Becker committed Jan 04, 2017 318 319 ``````(* Upper Bound *) (* Case distinction for a *) `````` Heiko Becker committed Jan 10, 2017 320 ``````>- (qspecl_then [`a`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL `````` Heiko Becker committed Jan 04, 2017 321 322 323 `````` (* First case: a < 0 *) >- (`a <= 0 /\ a <> 0` by fs[REAL_LT_LE] \\ (* Case distinction for SND iv2 *) `````` Heiko Becker committed Jan 10, 2017 324 `````` qspecl_then [`FST iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL `````` Heiko Becker committed Jan 04, 2017 325 `````` (* First case: FST iv2 < 0 *) `````` Heiko Becker committed Jan 10, 2017 326 327 328 329 330 331 332 333 334 `````` >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``FST (iv1:interval) * FST (iv2:interval)`` \\ conj_tac >- (once_rewrite_tac[REAL_MUL_SYM] \\ match_mp_tac REAL_LE_TRANS \\ exists_tac ``FST (iv2:interval) * (a:real)`` \\ conj_tac >- (once_rewrite_tac [REAL_MUL_SYM] \\ match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ `````` Heiko Becker committed Jan 04, 2017 335 `````` fs []) `````` Heiko Becker committed Jan 10, 2017 336 `````` >- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ `````` Heiko Becker committed Jan 04, 2017 337 `````` fs [REAL_LT_LE])) `````` Heiko Becker committed Jan 10, 2017 338 339 340 341 342 `````` >- (qspecl_then [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`] (fn thm => rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)]) max4_correct)) `````` Heiko Becker committed Jan 04, 2017 343 `````` (* Second case: 0 <= FST iv2 *) `````` Heiko Becker committed Jan 10, 2017 344 345 346 347 348 349 350 351 352 353 354 355 `````` >- (match_mp_tac REAL_LE_TRANS\\ exists_tac ``SND (iv1:interval) * FST (iv2:interval)`` \\ conj_tac >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``(a:real) * FST (iv2:interval)`` \\ conj_tac \\ fs[REAL_LE_RMUL_IMP, REAL_MUL_LE_COMPAT_NEG_L]) >- (qspecl_then [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`] (fn thm => rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)]) max4_correct))) (* Second case 0 <= a *) `````` Heiko Becker committed Jan 04, 2017 356 `````` (* Case distinction for FST iv2 *) `````` Heiko Becker committed Jan 10, 2017 357 `````` >- (qspecl_then [`SND iv2`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL `````` Heiko Becker committed Jan 04, 2017 358 `````` (* First case: FST iv2 < 0 *) `````` Heiko Becker committed Jan 10, 2017 359 360 361 362 363 364 365 `````` >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``FST (iv1:interval) * SND (iv2:interval)`` \\ conj_tac >- (once_rewrite_tac [REAL_MUL_SYM] \\ match_mp_tac REAL_LE_TRANS \\ exists_tac ``SND (iv2:interval) * (a:real)`` \\ conj_tac `````` Heiko Becker committed Jan 04, 2017 366 `````` >- (fs [REAL_LE_RMUL_IMP]) `````` Heiko Becker committed Jan 10, 2017 367 368 369 370 371 372 `````` >- (match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ fs[REAL_LT_LE])) >- (qspecl_then [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`] (fn thm => rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)]) max4_correct)) `````` Heiko Becker committed Jan 04, 2017 373 `````` (* Second case: 0 <= FST iv2 *) `````` Heiko Becker committed Jan 10, 2017 374 375 376 377 378 379 380 381 382 383 384 `````` >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``SND (iv1:interval) * SND (iv2:interval)`` \\ conj_tac >- (match_mp_tac REAL_LE_TRANS \\ exists_tac ``a:real * SND (iv2:interval)`` \\ conj_tac \\ fs [REAL_LE_RMUL_IMP, REAL_LE_LMUL_IMP]) >- (qspecl_then [`FST iv1 * FST iv2`, `FST iv1 * SND iv2`,`SND iv1 * FST iv2`, `SND iv1 * SND iv2`] (fn thm => rewrite_tac [SIMP_RULE bool_ss [max4_def] (CONV_RULE let_CONV thm)]) max4_correct))))); `````` Heiko Becker committed Jan 04, 2017 385 386 `````` val interval_division_valid = store_thm ( "interval_division_valid", `````` Heiko Becker committed Jan 30, 2017 387 ````````!(iv1:interval) (iv2:interval) (a:real) (b:real). `````` Heiko Becker committed Jan 04, 2017 388 389 390 391 `````` (IVhi iv2 < 0 \/ 0 < IVlo iv2) /\ contained a iv1 /\ contained b iv2 ==> contained (a / b) (divideInterval iv1 iv2)``, `````` Heiko Becker committed Jan 10, 2017 392 393 394 395 396 397 ``````rpt gen_tac \\ Cases_on `iv2` \\ rewrite_tac (iv_ss @ [real_div, REAL_MUL_LID]) \\ rpt gen_tac \\ strip_tac \\ (** TODO: FIXME use qspecl_then **) match_mp_tac (REWRITE_RULE (iv_ss @ [FST,SND]) (SPECL [``iv1:interval``, ``(inv r, inv q):interval``] interval_multiplication_valid)) \\ `````` Heiko Becker committed Jan 04, 2017 398 ``````fs [] \\ `````` Heiko Becker committed Jan 10, 2017 399 400 401 ``````match_mp_tac (REWRITE_RULE (iv_ss @ [FST, SND, real_div, REAL_MUL_LID]) (SPECL [``(q,r):interval``, ``b:real``] interval_inversion_valid)) \\ `````` Heiko Becker committed Jan 04, 2017 402 403 ``````fs[]); `````` Heiko Becker committed Jan 05, 2017 404 405 ``````(** Properties of the maxAbs function **) val contained_leq_maxAbs = store_thm ("contained_leq_maxAbs", `````` Heiko Becker committed Mar 06, 2017 406 `````` ``!a iv. contained a iv ==> abs a <= maxAbs iv``, `````` Heiko Becker committed Jan 30, 2017 407 `````` rpt strip_tac\\ fs iv_ss \\ match_mp_tac maxAbs \\ fs []); `````` Heiko Becker committed Jan 05, 2017 408 `````` `````` Heiko Becker committed Jan 25, 2017 409 ``````val contained_leq_maxAbs_val = store_thm ("contained_leq_maxAbs_val", `````` Heiko Becker committed Mar 06, 2017 410 `````` ``!a iv. contained a iv ==> a <= maxAbs iv``, `````` Heiko Becker committed Jan 30, 2017 411 412 413 414 `````` rpt strip_tac \\ fs iv_ss \\ `abs a <= max (abs (FST iv)) (abs (SND iv))` by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\ REAL_ASM_ARITH_TAC); `````` Heiko Becker committed Jan 25, 2017 415 `````` `````` Heiko Becker committed Jan 05, 2017 416 ``````val contained_leq_maxAbs_neg_val = store_thm ("contained_leq_maxAbs_neg_val", `````` Heiko Becker committed Mar 06, 2017 417 `````` ``!a iv. contained a iv ==> - a <= maxAbs iv``, `````` Heiko Becker committed Jan 30, 2017 418 419 420 `````` rpt strip_tac\\ fs iv_ss \\ `abs a <= max (abs (FST iv)) (abs (SND iv))` by (match_mp_tac (REWRITE_RULE iv_ss contained_leq_maxAbs) \\ fs []) \\ REAL_ASM_ARITH_TAC); `````` Heiko Becker committed Jan 05, 2017 421 422 `````` val distance_gives_iv = store_thm ("distance_gives_iv", `````` Heiko Becker committed Jan 30, 2017 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 `````` ``!a b e iv. contained a iv /\ abs (a - b) <= e ==> contained b (widenInterval iv e)``, fs iv_ss \\ rpt strip_tac \\ `(b:real) - e <= a /\ a <= b + e` by REAL_ASM_ARITH_TAC \\ REAL_ASM_ARITH_TAC); val minAbs_positive_iv_is_lo = store_thm ("minAbs_positive_iv_is_lo", ``!(a b:real). (0 < a) /\ (a <= b) ==> (minAbsFun (a,b) = a)``, rpt (strip_tac) \\ fs[minAbsFun_def] \\ `abs a = a` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\ `abs b = b` by (fs[ABS_REFL] \\ REAL_ASM_ARITH_TAC) \\ fs[REAL_MIN_ALT]); val minAbs_negative_iv_is_hi = store_thm ("minAbs_negative_iv_is_hi", ``!(a b:real). (b < 0) /\ (a <= b) ==> (minAbsFun (a,b) = - b)``, rpt (strip_tac) \\ fs[minAbsFun_def] \\ `abs a = - a` by REAL_ASM_ARITH_TAC \\ `abs b = - b` by REAL_ASM_ARITH_TAC \\ `````` Heiko Becker committed Jan 31, 2017 448 `````` fs[REAL_MIN_ALT]); `````` Heiko Becker committed Jan 05, 2017 449 `````` `````` Heiko Becker committed Jan 03, 2017 450 ``val _ = export_theory();``