Commit faf1b7e9 authored by Heiko Becker's avatar Heiko Becker

Prove error inversion property

parent fa973ffc
......@@ -23,6 +23,10 @@ hol4/*Theory*
hol4/*.ui
hol4/*.uo
hol4/.*
hol4/*/*Theory*
hol4/*/*.ui
hol4/*/*.uo
hol4/*/.*
hol4/heap
daisy
rawdata/*
......
......@@ -330,37 +330,53 @@ val err_prop_inversion_neg = store_thm ("err_prop_inversion_neg",
>- (`- (nR * (nR - err)) <= - ((ehi + err) * (nR - err))`
by (once_rewrite_tac [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC) \\
REAL_ASM_ARITH_TAC)))
>- cheat);
(** FIXME: UNDONE
>- (fs[] \\
`nR <= nF` by REAL_ASM_ARITH_TAC \\
`0 < nF` by REAL_ASM_ARITH_TAC \\
`0 < nR` by REAL_ASM_ARITH_TAC \\
`inv nF <= inv nR` by fs [GSYM REAL_INV_LE_ANTIMONO] \\
`0 <= inv nR - inv nF` by REAL_ASM_ARITH_TAC \\ qpat_x_assum `inv nF <= inv nR` kall_tac \\
`abs (inv nR - inv nF) = inv nR - inv nF` by fs[ABS_REFL] \\ qpat_x_assum `0 <= inv a - b` kall_tac \\
simp [REAL_INV_1OVER, real_sub, REAL_NEG_ADD] \\
rpt (qpat_x_assum `abs x = y` kall_tac) \\
qspec_then `1 / nR + - (1 / (nR + err))` match_mp_tac real_le_trans2 \\ conj_tac
>- (match_mp_tac REAL_LE_LADD_IMP \\
simp [GSYM REAL_INV_1OVER, GSYM REAL_NEG_INV, REAL_LE_NEG] \\
`0 < nR + err /\ nF <= nR + err` by REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\
conj_tac \\ REAL_ASM_ARITH_TAC)
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC \\
`- (1 / (nR + err)) = 1 / - (nR + err)` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC) \\
`- (nR + err) <> 0` by REAL_ASM_ARITH_TAC \\
`nR <> 0` by REAL_ASM_ARITH_TAC \\
fs [REAL_ADD_RAT] \\
`- (nR + err) + nR = - err` by REAL_ASM_ARITH_TAC \\
qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL \\
simp [REAL_NEG_RMUL, REAL_NEG_INV] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[] \\
match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
>- (match_mp_tac REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC)))));
**)
>- (fs [] \\
`nR <= nF` by REAL_ASM_ARITH_TAC \\
`0 < -nF /\ nF <> 0` by REAL_ASM_ARITH_TAC \\
`0 < -nR /\ nR <> 0` by REAL_ASM_ARITH_TAC \\
`inv (- nR) <= inv (- nF)`
by (match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac \\
REAL_ASM_ARITH_TAC) \\
`inv (- nR) - inv (- nF) <= 0` by REAL_ASM_ARITH_TAC \\
`0 <= - (inv (- nR) - inv (-nR)) ` by REAL_ASM_ARITH_TAC \\
`abs (- (inv (- nR) - inv (- nF))) = - (inv (- nR) - inv (- nF))` by fs [ABS_REFL] \\
`abs (inv (- nR) - inv (- nF)) = - (inv (- nR) - inv (- nF))` by fs [ABS_NEG] \\
`inv (- nR) - inv (- nF) = inv nF - inv nR` by (fs[GSYM REAL_NEG_INV, real_sub] \\ REAL_ASM_ARITH_TAC) \\
`abs (inv nF - inv nR) = - (inv (- nR) - inv (- nF))` by fs[] \\
`abs (inv nR - inv nF) = - (inv (- nR) - inv (- nF))` by fs[ABS_SUB] \\
simp[REAL_INV_1OVER, real_sub, REAL_NEG_ADD] \\
rpt (qpat_x_assum `abs v = v'` kall_tac) \\
`- (1 / nF) = 1 / - nF` by (fs [real_div] \\ match_mp_tac REAL_NEG_INV \\ REAL_ASM_ARITH_TAC) \\
simp[] \\
qspec_then `1 / -(nR + err) + 1 / nR` match_mp_tac real_le_trans2 \\ conj_tac
>- (once_rewrite_tac [REAL_ADD_COMM] \\ match_mp_tac REAL_LE_LADD_IMP \\
simp [GSYM REAL_INV_1OVER, REAL_LE_NEG] \\
`0 < - (nR + err) /\ nF <= nR + err` by REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\
conj_tac \\ REAL_ASM_ARITH_TAC)
>- (` - nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC \\
`- (nR + err) <> 0` by REAL_ASM_ARITH_TAC \\
fs [REAL_ADD_RAT] \\
`nR + - (nR + err) = - err` by REAL_ASM_ARITH_TAC \\
fs [real_div, GSYM REAL_NEG_RMUL] \\
simp [GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL] \\
`inv (- ((nR + err) * nR)) = - (inv ((nR + err) * nR))`
by (match_mp_tac (GSYM REAL_NEG_INV) \\ fs[] \\ REAL_ASM_ARITH_TAC) \\
simp[GSYM REAL_NEG_RMUL] \\
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[] \\
`0 < - (ehi + err)` by REAL_ASM_ARITH_TAC \\
`0 < - (ehi + err) * -(ehi + err)` by (match_mp_tac REAL_LT_MUL \\ fs[]) \\
`0 < (ehi + err) * (ehi + err)` by REAL_ASM_ARITH_TAC \\
`0 < - nR * - (nR + err)` by (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC) \\
`0 < nR * (nR + err)` by REAL_ASM_ARITH_TAC \\
match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac \\ TRY (REAL_ASM_ARITH_TAC) \\
conj_tac \\ TRY(REAL_ASM_ARITH_TAC) \\
qspec_then `(nR + err) * (ehi + err)` match_mp_tac real_le_trans2 \\
conj_tac
>- (once_rewrite_tac [REAL_MUL_COMM] \\
match_mp_tac REAL_MUL_LE_COMPAT_NEG_L \\ conj_tac \\ REAL_ASM_ARITH_TAC)
>- (`- (nR * (nR + err)) <= - ((ehi + err) * (nR + err))`
by (once_rewrite_tac [REAL_NEG_RMUL] \\ match_mp_tac REAL_LE_RMUL_IMP \\ REAL_ASM_ARITH_TAC) \\
REAL_ASM_ARITH_TAC))));
val _ = export_theory();
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