Commit 31c7a755 authored by Heiko Becker's avatar Heiko Becker

WIP finish unary operators for IV validator

parent 024abf5d
......@@ -177,20 +177,29 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
\\ irule Unop_neg' \\ qexistsl_tac [`M0`, `vR`] \\ fs[evalUnop_def])
(* Inversion case *)
(* MARKER *)
\\ qexists_tac `1 / vR` \\ fs[invertInterval_def, isSupersetInterval_def]
\\ Cases_on `iv` \\ fs[IVlo_def, IVhi_def]
\\ rpt conj_tac \\ TRY REAL_ASM_ARITH_TAC
\\ qexists_tac `1 / vR`
\\ conj_tac
>- (irule Unop_inv' \\ fs[] \\ qexistsl_tac [`0`, `vR`]
\\ fs[evalUnop_def, perturb_def, REAL_INV_1OVER, mTypeToQ_pos]
\\ fs[evalUnop_def, perturb_def, REAL_INV_1OVER, mTypeToQ_pos, IVhi_def, IVlo_def]
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ `0 < 0:real` by (irule REAL_LET_TRANS \\ qexists_tac `r` \\ fs[])
\\ `0 < 0:real` by (REAL_ASM_ARITH_TAC)
\\ fs[])
\\ conj_tac
\\ fs[invertInterval_def, isSupersetInterval_def]
\\ Cases_on `iv` \\ fs[IVlo_def, IVhi_def]
>- (irule REAL_LE_TRANS \\ qexists_tac `1 / r` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPL \\ fs[]
\\ REAL_ASM_ARITH_TAC)
>- (irule REAL_LE_TRANS \\ qexists_tac `1 / r` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]
\\ REAL_ASM_ARITH_TAC)
>- (irule REAL_LE_TRANS \\ qexists_tac `1 / q` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPL \\ fs[]
\\ REAL_ASM_ARITH_TAC)
\\ irule REAL_LE_TRANS \\ qexists_tac `1/q` \\ conj_tac \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPL \\ fs[]
\\ fs[GSYM REAL_INV_1OVER] \\ irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[]
\\ REAL_ASM_ARITH_TAC)
(* MARKER *)
(* Binary operator case *)
>- (rename1 `Binop b f1 f2`
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment