Commit 39362c71 authored by Heiko Becker's avatar Heiko Becker
Browse files

Update to latest develop

parent 235966b1
89e07c5a43c0637bc614b4396e6a8b3cb902cedb
52ffdc8f01c5cf044427bf6f3a12e8300e91765a
......@@ -447,16 +447,13 @@ Proof
QED
Theorem err_prop_inversion_pos:
!(nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
0 < elo - err /\ 0 < elo /\
abs (nR - nF) <= err /\
elo <= nR /\
nR <= ehi /\
elo - err <= nF /\
nF <= ehi + err /\
0 <=
err ==>
abs (inv nR - inv nF) <= err * inv ((elo - err) * (elo - err))
(nF:real) (nR:real) (err:real) (elo:real) (ehi:real).
0 < elo - err 0 < elo
abs (nR - nF) <= err
elo <= nR nR <= ehi
elo - err <= nF nF <= ehi + err
0 <= err
abs (inv nR - inv nF) <= err * inv ((elo - err) * (elo - err))
Proof
rpt strip_tac
\\ `! (x:real). ((abs x = x) /\ 0 < x) \/ ((abs x = - x) /\ x <= 0)`
......@@ -481,26 +478,25 @@ Proof
>- (match_mp_tac REAL_LE_LADD_IMP
\\ 0 < nR - err nR - err nF by REAL_ASM_ARITH_TAC
\\ simp[])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ (nR - err + -nR) / (-nR * (nR - err)) err * (1 / (elo + -err) pow 2)
suffices_by (rewrite_tac[REAL_INV_1OVER] \\ fs[REAL_ADD_RAT])
\\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
\\ pop_assum (rewrite_tac o single)
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
(* Goal: -(err * inv (-(nR * (nR − err)))) ≤ err * inv ((elo + -err) pow 2) *)
\\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
\\ fs [GSYM REAL_NEG_INV, GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL]
(* Goal: err * inv (nR * (nR − err)) ≤ err * inv ((elo + -err) pow 2) *)
\\ rewrite_tac [REAL_POW_INV]
\\ match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
\\ rpt (qpat_x_assum `T` kall_tac)
\\ `0 < elo + - err` by REAL_ASM_ARITH_TAC
\\ `0 < (elo + - err) * (elo + - err)` by fs[REAL_LT_MUL]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
\\ conj_tac
>- (fs[POW_2])
\\ once_rewrite_tac [POW_2] \\ irule REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC))
\\ `- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ (nR - err + -nR) / (-nR * (nR - err)) err * (1 / (elo + -err) pow 2)
suffices_by (rewrite_tac[REAL_INV_1OVER] \\ fs[REAL_ADD_RAT])
\\ `nR - err + - nR = - err` by REAL_ASM_ARITH_TAC
\\ pop_assum (rewrite_tac o single)
\\ qspec_then `nR` (fn thm => fs [real_div, GSYM thm]) REAL_NEG_LMUL
\\ `nR * (nR - err) <> 0` by fs[REAL_ENTIRE]
\\ err * inv (nR * (nR err)) err * inv ((elo + -err) pow 2)
by (
match_mp_tac REAL_LE_LMUL_IMP \\ conj_tac \\ simp[]
\\ rpt (qpat_x_assum `T` kall_tac)
\\ `0 < elo + - err` by REAL_ASM_ARITH_TAC
\\ `0 < (elo + - err) * (elo + - err)` by fs[REAL_LT_MUL]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
>- (match_mp_tac REAL_LT_MUL \\ REAL_ASM_ARITH_TAC)
\\ conj_tac
>- (fs[POW_2])
\\ once_rewrite_tac [POW_2] \\ irule REAL_LE_MUL2 \\ REAL_ASM_ARITH_TAC)
\\ fs[REAL_INV_MUL'] \\ pop_assum mp_tac \\ fs[])
>- (fs[]
\\ `nR <= nF` by REAL_ASM_ARITH_TAC
\\ `0 < nF` by REAL_ASM_ARITH_TAC
......@@ -617,61 +613,61 @@ Proof
>- (`- (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)))
>- (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 metis_tac[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_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] \\ rewrite_tac [REAL_INV_1OVER]
\\ pop_assum (rewrite_tac o single)
\\ match_mp_tac REAL_LE_LADD_IMP
\\ `0 < - (nR + err) /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
\\ simp [REAL_LE_NEG, REAL_INV_LE_ANTIMONO])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
\\ 1 / - (nR + err) + 1 / nR = (1 * nR + - (nR + err) * 1) / (- (nR + err) * nR)
by (fs[REAL_ADD_RAT])
\\ pop_assum (rewrite_tac o single)
\\ `nR + - (nR + err) = - err` by REAL_ASM_ARITH_TAC
\\ rewrite_tac [REAL_MUL_RID, REAL_MUL_LID, real_div, GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL]
\\ pop_assum (rewrite_tac o single)
\\ `inv (- ((nR + err) * nR)) = - (inv ((nR + err) * nR))`
by (match_mp_tac (GSYM REAL_NEG_INV) \\ fs[] \\ REAL_ASM_ARITH_TAC)
\\ pop_assum (rewrite_tac o single)
\\ simp[GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL, REAL_NEG_NEG]
\\ 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
\\ asm_rewrite_tac[GSYM REAL_NEG_RMUL]
\\ once_rewrite_tac [REAL_MUL_COMM]
\\ asm_rewrite_tac[REAL_NEG_INV, REAL_NEGNEG]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
\\ once_rewrite_tac [POW_2] \\ 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)))
\\ 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 metis_tac[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_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] \\ rewrite_tac [REAL_INV_1OVER]
\\ pop_assum (rewrite_tac o single)
\\ match_mp_tac REAL_LE_LADD_IMP
\\ `0 < - (nR + err) /\ nF <= nR + err` by REAL_ASM_ARITH_TAC
\\ simp [REAL_LE_NEG, REAL_INV_LE_ANTIMONO, REAL_MUL_LNEG])
>- (`- nR <> 0 /\ nR - err <> 0` by REAL_ASM_ARITH_TAC
\\ `- (nR + err) <> 0` by REAL_ASM_ARITH_TAC
\\ 1 / - (nR + err) + 1 / nR = (1 * nR + - (nR + err) * 1) / (- (nR + err) * nR)
by (fs[REAL_ADD_RAT])
\\ pop_assum (rewrite_tac o single)
\\ rewrite_tac [REAL_MUL_RID, REAL_MUL_LID, real_div, GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL]
\\ `nR + - (nR + err) = - err` by REAL_ASM_ARITH_TAC
\\ pop_assum (rewrite_tac o single)
\\ `inv (- ((nR + err) * nR)) = - (inv ((nR + err) * nR))`
by (match_mp_tac (GSYM REAL_NEG_INV) \\ fs[] \\ REAL_ASM_ARITH_TAC)
\\ pop_assum (rewrite_tac o single)
\\ simp[GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL, REAL_NEG_NEG]
\\ 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
\\ asm_rewrite_tac[GSYM REAL_NEG_RMUL]
\\ once_rewrite_tac [REAL_MUL_COMM]
\\ asm_rewrite_tac[REAL_NEG_INV, REAL_NEGNEG, GSYM REAL_INV_1OVER]
\\ match_mp_tac REAL_INV_LE_ANTIMONO_IMPR \\ conj_tac
\\ once_rewrite_tac [POW_2] \\ 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)
QED
val _ = export_theory();
......@@ -366,7 +366,7 @@ QED
local
val trivial_up_tac =
fs[REAL_LE_ADD] (* remove lhs of addition *)
irule REAL_LE_LADD_IMP (* remove lhs of addition *)
(* Try first proving by transitivity only *)
\\ TRY (
irule REAL_LE_RMUL_IMP \\ fs[] \\ NO_TAC)
......@@ -470,7 +470,8 @@ Proof
(* 0 ≤ -(nR2 + err2) *)
\\ irule REAL_LE_TRANS
\\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 + err2)` \\ conj_tac
>- trivial_up_tac
>- (irule REAL_LE_LADD_IMP
\\ irule REAL_LE_RMUL_IMP \\ fs[])
\\ real_rewrite
`nR1 * nR2 + (nR1 + err1) * - (nR2 + err2) = - nR1 * err2 + - nR2 * err1 + - err1 * err2`
\\ simp[] \\ irule REAL_LE_ADD2 \\ conj_tac \\ TRY(simp[GSYM REAL_NEG_LMUL])
......@@ -479,7 +480,9 @@ Proof
>- (
irule REAL_LE_TRANS
\\ qexists_tac `nR1 * nR2 + nF1 * - (nR2 - err2)` \\ conj_tac
>- trivial_up_tac
>- (irule REAL_LE_LADD_IMP \\ once_rewrite_tac [REAL_NEG_RMUL]
\\ irule REAL_LE_LMUL_IMP \\ fs[real_sub]
\\ qpat_x_assum ‘∀ x. _ kall_tac \\ REAL_ASM_ARITH_TAC)
\\ qspecl_then [`- (nR2 - err2)`, `0`] DISJ_CASES_TAC REAL_LTE_TOTAL
(* -(nR2 - err2) < 0 *)
>- (irule REAL_LE_TRANS
......@@ -494,7 +497,7 @@ Proof
>- (
irule REAL_LE_TRANS
\\ qexists_tac `nR1 * nR2 + (nR1 + err1) * - (nR2 - err2)` \\ conj_tac
>- trivial_up_tac
>- (irule REAL_LE_LADD_IMP \\ irule REAL_LE_RMUL_IMP \\ fs[])
\\ real_rewrite
`nR1 * nR2 + (nR1 + err1) * - (nR2 - err2) = nR1 * err2 + - nR2 * err1 + err1 * err2`
\\ simp[] \\ irule REAL_LE_ADD2 \\ conj_tac \\ simp[GSYM REAL_NEG_LMUL])))
......
......@@ -219,6 +219,8 @@ val by_monotonicity =
\\ fs[FloverMapTree_mem_def]
\\ EVERY_CASE_TAC \\ fs[];
val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
Theorem getValidMap_mono:
e Gamma akk res.
getValidMap Gamma e akk = Succes res
......
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