diff --git a/Holmakefile b/Holmakefile
index 53d736c31728464cf0c1465cddbd548cc0423458..65724144f1e9f0f58fec43e2a4c2f83b2e539272 100644
--- a/Holmakefile
+++ b/Holmakefile
@@ -1 +1 @@
-INCLUDES = $(FLOVERDIR)/hol4/semantics $(HOLDIR)/examples/algebra/polynomial
+INCLUDES = $(FLOVERDIR)/hol4 $(FLOVERDIR)/hol4/semantics $(HOLDIR)/examples/algebra/polynomial
diff --git a/approxPolyScript.sml b/approxPolyScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..554978498aaafc6e0bfc2e729a88c9973a4895e4
--- /dev/null
+++ b/approxPolyScript.sml
@@ -0,0 +1,497 @@
+(** **)
+open realTheory realLib RealArith transcTheory;
+open realPolyTheory realPolyProofsTheory mcLaurinApproxTheory transcLangTheory;
+open preamble;
+
+val _ = new_theory "approxPoly";
+
+(** functions computing the McLaurin series for transcendental functions **)
+Definition expPoly_def:
+ expPoly 0 = [] ∧ (* x pow 0 * inv FACT 0 *)
+ expPoly (SUC n) = (expPoly n) ++ [inv (&FACT n)]
+End
+
+Definition cosPoly_def:
+ cosPoly 0 = [] ∧
+ cosPoly (SUC n) =
+ if (EVEN n) then
+ cosPoly n ++ [-1 pow (n DIV 2) * inv (&FACT n)]
+ else cosPoly n ++ [0]
+End
+
+Definition sinPoly_def:
+ sinPoly 0 = [] ∧
+ sinPoly (SUC n) =
+ if (EVEN n) then sinPoly n ++ [0]
+ else sinPoly n ++ [-1 pow ((n - 1) DIV 2) * inv (&FACT n)]
+End
+
+(** Define an approximation function that translates transcendental functions into
+ polynomials **)
+(* Error for exp if upper bound ≤ 1/2 *)
+Definition expErrSmall_def:
+ expErrSmall approxSteps = inv (&FACT approxSteps * 2 pow (approxSteps - 1))
+End
+
+(* General, more coarse bound *)
+Definition expErrBig_def:
+ expErrBig n approxSteps =
+ 2 pow n * &n pow approxSteps * inv (&FACT approxSteps * 2 pow approxSteps)
+End
+
+Definition cosErr_def:
+ cosErr iv approxSteps = (max (abs (FST iv)) (abs (SND iv))) pow approxSteps * (* ^(cosErr_EVAL_THM |> concl |> rhs)*)
+ inv (&FACT approxSteps)
+End
+
+Definition sinErr_def:
+ sinErr iv approxSteps = (max (abs (FST iv)) (abs (SND iv))) pow approxSteps * (* ^(sinErr_EVAL_THM |> concl |> rhs) *)
+ inv (&FACT approxSteps)
+End
+
+Definition internalSteps_def:
+ internalSteps:num = 40
+End
+
+(**
+ Approximate a function described by transcLang with a real-number polynomial,
+ also returns the approximation error
+**)
+Definition approxPoly_def:
+ approxPoly (transc:trFun) (iv:real#real) approxSteps :(poly#real) option =
+ case transc of
+ | Exp =>
+ if iv = (0, inv 2) then
+ SOME (expPoly approxSteps, expErrSmall approxSteps)
+ else if FST iv = 0 then
+ SOME (expPoly approxSteps, expErrBig (clg (SND iv * 2)) approxSteps)
+ else NONE
+ | Sin => SOME (sinPoly approxSteps, sinErr iv approxSteps)
+ | Cos => SOME (cosPoly approxSteps, cosErr iv approxSteps)
+End
+
+(** Simple properties of polynomials used for proofs later **)
+Theorem expPoly_LENGTH:
+ LENGTH (expPoly n) = n
+Proof
+ Induct_on ‘n’ >> gs[expPoly_def]
+QED
+
+Theorem cosPoly_LENGTH:
+ LENGTH (cosPoly n) = n
+Proof
+ Induct_on ‘n’ >> gs[cosPoly_def]
+ >> cond_cases_tac >> gs[]
+QED
+
+Theorem sinPoly_LENGTH:
+ LENGTH (sinPoly n) = n
+Proof
+ Induct_on ‘n’ >> gs[sinPoly_def]
+ >> cond_cases_tac >> gs[]
+QED
+
+(** The polynomials compute the sum part of the McLaurin series **)
+Theorem exp_sum_to_poly:
+ ∀ n x. evalPoly (expPoly n) x = sum (0,n) (λ m. x pow m / &FACT m)
+Proof
+ Induct_on ‘n’ >> gs[expPoly_def, evalPoly_def, sum]
+ >> rpt strip_tac >> gs[evalPoly_app, evalPoly_def, expPoly_LENGTH]
+QED
+
+Theorem cos_sum_to_poly:
+ ∀ n x. evalPoly (cosPoly n) x =
+ sum(0,n)
+ (λm.
+ (&FACT m)â»Â¹ * x pow m *
+ if EVEN m then cos 0 * -1 pow (m DIV 2)
+ else sin 0 * -1 pow ((SUC m) DIV 2))
+Proof
+ Induct_on ‘n’ >> gs[sum, evalPoly_def, cosPoly_def]
+ >> cond_cases_tac
+ >> gs[evalPoly_app, COS_0, SIN_0, evalPoly_def, cosPoly_LENGTH]
+QED
+
+Theorem sin_sum_to_poly:
+ ∀ n x.
+ evalPoly (sinPoly n) x =
+ sum(0,n)
+ (λm.
+ (&FACT m)â»Â¹ * x pow m *
+ if EVEN m then sin 0 * -1 pow (m DIV 2)
+ else cos 0 * -1 pow ((m - 1) DIV 2))
+Proof
+ Induct_on ‘n’ >> gs[sum, evalPoly_def, sinPoly_def]
+ >> cond_cases_tac
+ >> gs[evalPoly_app, SIN_0, COS_0, evalPoly_def, sinPoly_LENGTH]
+QED
+
+(** Theorems about the remainder term of the McLaurin series **)
+Theorem exp_remainder_bounded_small:
+ ∀ n x t.
+ 0 < n ∧ abs t ≤ abs x ∧ 0 ≤ x ∧
+ t ≤ inv 2 ∧ x ≤ inv 2 ⇒
+ abs (exp t / &FACT n * x pow n) ≤ inv (&FACT n * 2 pow (n - 1))
+Proof
+ rpt strip_tac >> rewrite_tac[real_div, abs]
+ >> qmatch_goalsub_abbrev_tac ‘(if 0 ≤ exp_bound then _ else _) ≤ _’
+ >> ‘0 ≤ exp_bound’
+ by (
+ unabbrev_all_tac
+ >> rpt (irule REAL_LE_MUL >> gs[POW_POS, EXP_POS_LE]))
+ >> simp[] >> unabbrev_all_tac
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘(1 + 2 * inv 2) * (inv (&FACT n) * x pow n)’
+ >> conj_tac
+ >- (
+ rewrite_tac[GSYM REAL_MUL_ASSOC]
+ >> irule REAL_LE_RMUL_IMP
+ >> conj_tac
+ >- (
+ Cases_on ‘0 ≤ t’
+ >- (
+ irule REAL_LE_TRANS
+ >> qexists_tac ‘1 + 2 * t’ >> conj_tac
+ >- (irule REAL_EXP_BOUND_LEMMA >> gs[])
+ >> real_tac)
+ >> ‘t = - (- t)’ by real_tac
+ >> pop_assum $ once_rewrite_tac o single
+ >> once_rewrite_tac[EXP_NEG]
+ >> ‘- (inv 2) ≤ -t’ by real_tac
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘inv (exp (- (inv 2)))’
+ >> conj_tac
+ >- (irule REAL_INV_LE_ANTIMONO_IMPR >> gs[EXP_POS_LT, EXP_MONO_LE])
+ >> rewrite_tac[EXP_NEG, REAL_INV_INV]
+ >> irule REAL_EXP_BOUND_LEMMA >> gs[])
+ >> irule REAL_LE_MUL >> gs[REAL_LE_INV, POW_POS])
+ >> ‘1 + 2 * inv 2 = 2’ by gs[]
+ >> pop_assum $ rewrite_tac o single
+ >> rewrite_tac[GSYM REAL_MUL_ASSOC, REAL_INV_MUL']
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘2 * (inv (&FACT n) * inv 2 pow n)’
+ >> conj_tac
+ >- (
+ irule REAL_LE_LMUL_IMP >> reverse conj_tac >- gs[]
+ >> irule REAL_LE_LMUL_IMP >> reverse conj_tac >- gs[REAL_LE_INV]
+ >> irule POW_LE >> gs[])
+ >> Cases_on ‘n’ >- gs[]
+ >> rewrite_tac[pow]
+ >> gs[REAL_INV_MUL']
+QED
+
+Theorem exp_remainder_bounded_big:
+ ∀ n m x t.
+ 0 < n ∧ abs t ≤ abs x ∧ EVEN n ∧
+ abs x ≤ &m * (inv 2) ∧
+ t ≤ &m * (inv 2) ⇒
+ abs (exp t / &FACT n * x pow n) ≤ 2 pow m * &m pow n * (inv (&FACT n * 2 pow n))
+Proof
+ rpt strip_tac >> rewrite_tac[real_div, abs]
+ >> qmatch_goalsub_abbrev_tac ‘(if 0 ≤ exp_bound then _ else _) ≤ _’
+ >> ‘0 ≤ exp_bound’
+ by (
+ unabbrev_all_tac
+ >> rpt (irule REAL_LE_MUL >> gs[POW_POS, EXP_POS_LE]))
+ >> pop_assum $ rewrite_tac o single
+ >> unabbrev_all_tac
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘exp (&m * inv 2) * (inv (&FACT n) * x pow n)’
+ >> conj_tac
+ >- (
+ rewrite_tac[GSYM REAL_MUL_ASSOC]
+ >> irule REAL_LE_RMUL_IMP
+ >> conj_tac
+ >- gs[EXP_MONO_LE]
+ >> irule REAL_LE_MUL >> gs[REAL_LE_INV, POW_POS])
+ >> rewrite_tac[EXP_N]
+ >> qmatch_goalsub_abbrev_tac ‘_ * cst_err ≤ _’
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘(1 + 2 * inv 2) pow m * cst_err’
+ >> conj_tac
+ >- (
+ irule REAL_LE_RMUL_IMP
+ >> conj_tac
+ >- (
+ irule POW_LE >> rewrite_tac[EXP_POS_LE]
+ >> irule REAL_EXP_BOUND_LEMMA >> gs[])
+ >> unabbrev_all_tac
+ >> irule REAL_LE_MUL >> gs[REAL_LE_INV, POW_POS])
+ >> ‘1 + 2 * inv 2 = 2’ by gs[]
+ >> pop_assum $ rewrite_tac o single
+ >> unabbrev_all_tac
+ >> rewrite_tac[REAL_MUL_ASSOC]
+ >> qmatch_goalsub_abbrev_tac ‘cst_err * x pow n’
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘cst_err * (&m * inv 2) pow n’ >> conj_tac
+ >- (
+ irule REAL_LE_LMUL_IMP >> conj_tac
+ >- (irule REAL_LE_TRANS >> qexists_tac ‘abs x pow n’
+ >> gs[POW_LE, POW_ABS, ABS_LE])
+ >> unabbrev_all_tac >> irule REAL_LE_MUL
+ >> gs[REAL_LE_INV, POW_POS])
+ >> rewrite_tac [POW_MUL]
+ >> unabbrev_all_tac
+ >> qmatch_goalsub_abbrev_tac ‘curr_bound ≤ _’
+ >> ‘curr_bound = 2 pow m * &m pow n * (inv (&FACT n * 2 pow n))’
+ by (unabbrev_all_tac >> gs[REAL_POW_INV])
+ >> pop_assum $ rewrite_tac o single
+ >> unabbrev_all_tac >> gs[]
+QED
+
+Theorem sin_even_remainder_bounded:
+ ∀ n.
+ EVEN n ⇒
+ inv (&FACT n) * sin t * x pow n * -1 pow (n DIV 2) ≤
+ abs(inv (&FACT n) * x pow n * -1 pow (n DIV 2))
+Proof
+ rpt strip_tac
+ >> ‘inv (&FACT n) * x pow n * -1 pow (n DIV 2) = inv (&FACT n) * 1 * x pow n * -1 pow (n DIV 2)’
+ by real_tac
+ >> pop_assum $ rewrite_tac o single
+ >> rewrite_tac[GSYM REAL_MUL_ASSOC]
+ >> once_rewrite_tac[REAL_ABS_MUL]
+ >> ‘0 ≤ inv (&FACT n)’
+ by gs[REAL_LE_INV]
+ >> ‘abs (inv (&FACT n)) = inv (&FACT n)’ by gs[abs]
+ >> pop_assum $ rewrite_tac o single
+ >> irule REAL_LE_LMUL_IMP
+ >> reverse conj_tac >- gs[]
+ >> once_rewrite_tac[REAL_ABS_MUL]
+ >> Cases_on ‘0 ≤ x pow n * -1 pow (n DIV 2)’
+ >- (
+ ‘abs (x pow n * -1 pow (n DIV 2)) = x pow n * -1 pow (n DIV 2)’ by gs[abs]
+ >> pop_assum $ rewrite_tac o single
+ >> irule REAL_LE_RMUL_IMP >> gs[SIN_BOUNDS])
+ >> ‘x pow n * -1 pow (n DIV 2) < 0’ by real_tac
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘-1 * (x pow n * -1 pow (n DIV 2))’
+ >> conj_tac
+ >- (
+ once_rewrite_tac [REAL_MUL_COMM]
+ >> drule REAL_LE_LMUL_NEG
+ >> disch_then $ qspecl_then [‘sin t’, ‘-1’] $ rewrite_tac o single
+ >> gs[SIN_BOUNDS])
+ >> ‘∃ y. x pow n * -1 pow (n DIV 2) = -1 * y ∧ 0 ≤ y’
+ by (qexists_tac ‘-1 * x pow n * -1 pow (n DIV 2)’
+ >> real_tac)
+ >> qpat_x_assum `_ = -1 * y` $ rewrite_tac o single
+ >> gs[ABS_LE]
+QED
+
+Theorem cos_even_remainder_bounded:
+ ∀ n.
+ EVEN n ⇒
+ inv (&FACT n) * cos t * x pow n * -1 pow (n DIV 2) ≤
+ abs(inv (&FACT n) * x pow n * -1 pow (n DIV 2))
+Proof
+ rpt strip_tac
+ >> ‘inv (&FACT n) * x pow n * -1 pow (n DIV 2) = inv (&FACT n) * 1 * x pow n * -1 pow (n DIV 2)’
+ by real_tac
+ >> pop_assum $ rewrite_tac o single
+ >> rewrite_tac[GSYM REAL_MUL_ASSOC]
+ >> once_rewrite_tac[REAL_ABS_MUL]
+ >> ‘0 ≤ inv (&FACT n)’
+ by gs[REAL_LE_INV]
+ >> ‘abs (inv (&FACT n)) = inv (&FACT n)’ by gs[abs]
+ >> pop_assum $ rewrite_tac o single
+ >> irule REAL_LE_LMUL_IMP
+ >> reverse conj_tac >- gs[]
+ >> once_rewrite_tac[REAL_ABS_MUL]
+ >> Cases_on ‘0 ≤ x pow n * -1 pow (n DIV 2)’
+ >- (
+ ‘abs (x pow n * -1 pow (n DIV 2)) = x pow n * -1 pow (n DIV 2)’ by gs[abs]
+ >> pop_assum $ rewrite_tac o single
+ >> irule REAL_LE_RMUL_IMP >> gs[COS_BOUNDS])
+ >> ‘x pow n * -1 pow (n DIV 2) < 0’ by real_tac
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘-1 * (x pow n * -1 pow (n DIV 2))’
+ >> conj_tac
+ >- (
+ once_rewrite_tac [REAL_MUL_COMM]
+ >> drule REAL_LE_LMUL_NEG
+ >> disch_then $ qspecl_then [‘cos t’, ‘-1’] $ rewrite_tac o single
+ >> gs[COS_BOUNDS])
+ >> ‘∃ y. x pow n * -1 pow (n DIV 2) = -1 * y ∧ 0 ≤ y’
+ by (qexists_tac ‘-1 * x pow n * -1 pow (n DIV 2)’
+ >> real_tac)
+ >> qpat_x_assum `_ = -1 * y` $ rewrite_tac o single
+ >> gs[ABS_LE]
+QED
+
+Definition approxPolySideCond_def:
+ approxPolySideCond approxSteps =
+ (0 < approxSteps ∧ EVEN approxSteps ∧ EVEN (approxSteps DIV 2))
+End
+
+Theorem approxPoly_soundness:
+ ∀ transc iv approxSteps p err.
+ approxPolySideCond approxSteps ∧
+ approxPoly transc iv approxSteps = SOME (p, err) ⇒
+ ∀ x.
+ FST iv ≤ x ∧ x ≤ SND iv ⇒
+ abs (getFun transc x - evalPoly p x) ≤ err
+Proof
+ Cases_on ‘transc’ >> gs[approxPoly_def]
+ >> rpt strip_tac >> gs[approxPolySideCond_def]
+ (* exp function *)
+ >- (
+ gs[interp_def, getFun_def]
+ >> Cases_on ‘iv = (0, inv 2)’ >> gs[]
+ (* exp function, 0 to 1/2 *)
+ >- (
+ qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_EXP_LE
+ >> pop_assum $ rewrite_tac o single
+ >> rpt VAR_EQ_TAC
+ >> rewrite_tac[exp_sum_to_poly]
+ >> qmatch_goalsub_abbrev_tac ‘abs (exp_taylor + taylor_rem - exp_taylor) ≤ _’
+ >> ‘exp_taylor + taylor_rem - exp_taylor = taylor_rem’ by real_tac
+ >> pop_assum $ rewrite_tac o single
+ >> unabbrev_all_tac
+ >> ‘expErrSmall approxSteps = inv (&FACT approxSteps * 2 pow (approxSteps - 1))’
+ by EVAL_TAC
+ >> rename1 ‘exp t’
+ >> qspecl_then [‘approxSteps’, ‘x’,‘t’] mp_tac exp_remainder_bounded_small
+ >> impl_tac >> gs[]
+ >> real_tac)
+ (* exp function, 0 to 1 *)
+ >> ‘1 ≠inv 2’
+ by (once_rewrite_tac [GSYM REAL_INV1]
+ >> CCONTR_TAC
+ >> pop_assum $ mp_tac o SIMP_RULE std_ss []
+ >> rewrite_tac[REAL_INV_INJ] >> real_tac)
+ >> rpt VAR_EQ_TAC
+ >> rewrite_tac[GSYM poly_compat, eval_simps]
+ >> pop_assum $ rewrite_tac o single
+ >> rewrite_tac[exp_sum_to_poly]
+ >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_EXP_LE
+ >> pop_assum $ rewrite_tac o single
+ >> qmatch_goalsub_abbrev_tac ‘abs (exp_taylor + taylor_rem - exp_taylor) ≤ _’
+ >> ‘exp_taylor + taylor_rem - exp_taylor = taylor_rem’ by real_tac
+ >> pop_assum $ rewrite_tac o single
+ >> unabbrev_all_tac
+ >> qmatch_goalsub_abbrev_tac ‘expErrBig n _’
+ >> ‘expErrBig n approxSteps = 2 pow n * &n pow approxSteps * inv (&FACT approxSteps * 2 pow approxSteps)’
+ by (rewrite_tac[] >> EVAL_TAC)
+ >> pop_assum $ rewrite_tac o single
+ >> qspecl_then [‘approxSteps’, ‘n’, ‘x’,‘t’] mp_tac exp_remainder_bounded_big
+ >> impl_tac
+ >- (
+ rpt conj_tac >> TRY (gs[] >> real_tac >> NO_TAC)
+ >> ‘2 * x ≤ &n’
+ by (unabbrev_all_tac >> cond_cases_tac
+ >> gs[]
+ >- (
+ ‘SND iv = 0’ by real_tac
+ >> pop_assum $ rewrite_tac o single
+ >> ‘x = 0’ by real_tac
+ >> pop_assum $ rewrite_tac o single
+ >> gs[REAL_MUL_RZERO, REAL_DIV_LZERO, EVAL “flr 0â€])
+ >- (
+ pop_assum $ rewrite_tac o single o GSYM
+ >> real_tac)
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘&clg (2 * x)’
+ >> gs[LE_NUM_CEILING]
+ >> cond_cases_tac >> gs[]
+ >> rewrite_tac[GSYM REAL_OF_NUM_LE]
+ >> irule REAL_LE_TRANS >> qexists_tac ‘&flr (2 * SND iv)’
+ >> conj_tac
+ >> gs[REAL_OF_NUM_LE]
+ >> irule NUM_FLOOR_MONO
+ >> rpt conj_tac >> real_tac)
+ >- gs[abs]
+ >> irule REAL_LE_TRANS >> qexists_tac ‘abs t’
+ >> conj_tac >- gs[ABS_LE]
+ >> irule REAL_LE_TRANS >> qexists_tac ‘abs x’
+ >> gs[abs])
+ >> rewrite_tac[])
+ (* sin *)
+ >- (
+ gs[interp_def, getFun_def] >> rpt VAR_EQ_TAC
+ >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_SIN_LE
+ >> gs[]
+ >> pop_assum $ rewrite_tac o single
+ >> gs[sin_sum_to_poly]
+ >> qmatch_goalsub_abbrev_tac ‘abs (sin_taylor + taylor_rem - sin_taylor) ≤ _’
+ >> ‘sin_taylor + taylor_rem - sin_taylor = taylor_rem’ by real_tac
+ >> pop_assum $ rewrite_tac o single
+ >> unabbrev_all_tac
+ >> ‘inv (&FACT approxSteps) * sin t * x pow approxSteps * -1 pow (approxSteps DIV 2) =
+ (sin t * ((x pow approxSteps) * inv (&FACT approxSteps) * -1 pow (approxSteps DIV 2)))’
+ by real_tac
+ >> ‘-(x pow approxSteps) * inv (&FACT approxSteps) * sin t =
+ -(sin t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
+ by real_tac
+ >> rewrite_tac []
+ >> ntac 2 $ pop_assum $ rewrite_tac o single
+ >> rewrite_tac[GSYM REAL_MUL_ASSOC]
+ >> qmatch_goalsub_abbrev_tac ‘_ * err_sin_concr’
+ >> rewrite_tac [ABS_NEG, Once ABS_MUL]
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘ 1 * abs err_sin_concr’ >> conj_tac
+ >- (irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[SIN_BOUND, ABS_POS])
+ >> rewrite_tac [REAL_MUL_LID, sinErr_def, ABS_MUL]
+ >> ‘abs err_sin_concr = err_sin_concr’
+ by (unabbrev_all_tac
+ >> rewrite_tac[ABS_REFL]
+ >> irule REAL_LE_MUL >> conj_tac
+ >> gs[REAL_POW_GE0]
+ >> irule REAL_LE_MUL >> gs[REAL_POS, REAL_POW_GE0])
+ >> pop_assum $ rewrite_tac o single
+ >> unabbrev_all_tac
+ >> rewrite_tac [sinErr_def]
+ >> imp_res_tac EVEN_ODD_EXISTS >> gs[POW_MINUS1]
+ >> irule REAL_LE_LMUL_IMP >> gs[GSYM POW_ABS]
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘abs (x pow (2 * m))’ >> gs[ABS_LE, GSYM POW_ABS]
+ >> irule POW_LE >> gs[ABS_POS]
+ >> irule RealSimpsTheory.maxAbs >> gs[])
+ (* cos function *)
+ >- (
+ gs[interp_def, getFun_def] >> rpt VAR_EQ_TAC
+ >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_COS_LE
+ >> gs[]
+ >> pop_assum $ rewrite_tac o single
+ >> gs[cos_sum_to_poly]
+ >> qmatch_goalsub_abbrev_tac ‘abs (cos_taylor + taylor_rem - cos_taylor) ≤ _’
+ >> ‘cos_taylor + taylor_rem - cos_taylor = taylor_rem’ by real_tac
+ >> pop_assum $ rewrite_tac o single
+ >> unabbrev_all_tac
+ >> ‘(x pow approxSteps) * cos t * inv (&FACT approxSteps) =
+ (cos t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
+ by real_tac
+ >> ‘-(x pow approxSteps) * cos t * inv (&FACT approxSteps) =
+ -(cos t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
+ by real_tac
+ >> rewrite_tac []
+ >> ntac 2 $ pop_assum $ rewrite_tac o single
+ >> rewrite_tac [GSYM REAL_MUL_ASSOC]
+ >> qmatch_goalsub_abbrev_tac ‘abs (cos _ * err_cos_concr)’
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘ 1 * abs err_cos_concr’ >> conj_tac
+ >- (rewrite_tac[ABS_MUL] >> irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[COS_BOUND, ABS_POS])
+ >> rewrite_tac[REAL_MUL_LID]
+ >> ‘abs err_cos_concr = err_cos_concr’
+ by (unabbrev_all_tac
+ >> rewrite_tac[ABS_REFL]
+ >> irule REAL_LE_MUL >> conj_tac
+ >- (irule REAL_LE_INV >> gs[REAL_POS])
+ >> irule REAL_LE_MUL >> conj_tac
+ >> gs[REAL_POW_GE0])
+ >> pop_assum $ rewrite_tac o single
+ >> unabbrev_all_tac
+ >> rewrite_tac [cosErr_def]
+ >> imp_res_tac EVEN_ODD_EXISTS >> gs[POW_MINUS1]
+ >> irule REAL_LE_LMUL_IMP >> gs[GSYM POW_ABS]
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘abs (x pow (2 * m))’ >> gs[ABS_LE, GSYM POW_ABS]
+ >> irule POW_LE >> gs[ABS_POS]
+ >> irule RealSimpsTheory.maxAbs >> gs[])
+ (* Tan function *)
+ >- ( cheat )
+ (* Sqrt function *)
+ >> cheat
+QED
+
+val _ = export_theory();
diff --git a/checkerScript.sml b/checkerScript.sml
index c60c734de4f76d012eb07c36725bda8185522a3e..5fc8f1a87a716b1c7d0f61c3a48c24f43227ff25 100644
--- a/checkerScript.sml
+++ b/checkerScript.sml
@@ -10,120 +10,6 @@ open preamble;
val _ = new_theory "checker";
-Definition approx_steps_def[simp]:
- approx_steps:num = 14
-End
-
-Theorem exp_err_small_EVAL_THM = EVAL “inv (&FACT approx_steps * 2 pow (approx_steps - 1))â€
-Theorem exp_err_big_EVAL_THM = EVAL “ inv (&FACT approx_steps * 2 pow approx_steps)â€
-Theorem exp_poly_cst_EVAL_THM = EVAL “exp_poly approx_stepsâ€
-
-Definition exp_err_small_def:
- exp_err_small approxSteps = (* ^(exp_err_small_EVAL_THM |> concl |> rhs) *)
- inv (&FACT approxSteps * 2 pow (approxSteps - 1))
-End
-
-Definition exp_err_big_def:
- exp_err_big n approxSteps = 2 pow n * &n pow approxSteps * (* ^(exp_err_big_EVAL_THM |> rhs o concl)*)
- inv (&FACT approxSteps * 2 pow approxSteps)
-End
-
-Definition exp_poly_cst:
- exp_poly_cst = ^(exp_poly_cst_EVAL_THM |> concl |> rhs)
-End
-
-Triviality one_inv_one:
- 1 * inv 1 = 1
-Proof
- gs[REAL_MUL_RINV]
-QED
-
-Triviality mul_neg_one:
- -1 * x = - x:real
-Proof
- real_tac
-QED
-
-(** Still needs to be multiplied with x pow n **)
-Theorem cos_err_EVAL_THM = EVAL “inv (&FACT approx_steps)â€
-Theorem cos_poly_cst_EVAL_THM = EVAL “cos_poly approx_steps†|> SIMP_RULE std_ss [one_inv_one, REAL_MUL_LID, mul_neg_one]
-
-Definition cos_err_def:
- cos_err iv approxSteps = (max (abs (FST iv)) (abs (SND iv))) pow approxSteps * (* ^(cos_err_EVAL_THM |> concl |> rhs)*)
- inv (&FACT approxSteps)
-End
-
-Definition cos_poly_cst_def:
- cos_poly_cst = ^(cos_poly_cst_EVAL_THM |> concl |> rhs)
-End
-
-Theorem sin_err_EVAL_THM = EVAL “inv (&FACT approx_steps)â€
-Theorem sin_poly_cst_EVAL_THM = EVAL “sin_poly approx_steps†|> SIMP_RULE std_ss [one_inv_one, REAL_MUL_LID, mul_neg_one]
-
-Definition sin_err_def:
- sin_err iv approxSteps = (max (abs (FST iv)) (abs (SND iv))) pow approxSteps * (* ^(sin_err_EVAL_THM |> concl |> rhs) *)
- inv (&FACT approxSteps)
-End
-
-Definition sin_poly_cst_def:
- sin_poly_cst = ^(sin_poly_cst_EVAL_THM |> concl |> rhs)
-End
-
-Definition internalSteps_def:
- internalSteps:num = 40
-End
-
-Definition ubTransc_def:
- ubTransc tr ub =
- if tr = "exp" then
- let expPoly = exp_poly internalSteps in
- evalPoly expPoly ub + exp_err_big (clg (ub * 2)) internalSteps
- else if tr = "cos" ∨ tr = "sin" then 1
- else 0
-End
-
-(**
- Approximate a function described by transcLang with a real-number polynomial,
- also returns the approximation error
-**)
-Definition approxPoly_def:
- approxPoly transc (iv:real#real) approxSteps :(poly#real) option =
- case transc of
- | Fun tr Var =>
- if tr = "exp" then
- if iv = (0, 1 * inv 2) then
- SOME (exp_poly approxSteps, exp_err_small approxSteps)
- else if FST iv = 0 then SOME (exp_poly approxSteps, exp_err_big (clg (SND iv * 2)) approxSteps)
- else NONE
- else if tr = "cos" then
- SOME (cos_poly approxSteps, cos_err iv approxSteps)
- else if tr = "sin" then
- SOME (sin_poly approxSteps, sin_err iv approxSteps)
- else NONE
- | Add tr1 tr2 =>
- (case approxPoly tr1 iv approxSteps of
- | NONE => NONE
- | SOME (appr1, err1) =>
- case approxPoly tr2 iv approxSteps of
- | NONE => NONE
- | SOME (appr2, err2) =>
- SOME (appr1 +p appr2, err1 + err2))
- | Sub tr1 tr2 =>
- (case approxPoly tr1 iv approxSteps of
- | NONE => NONE
- | SOME (appr1, err1) =>
- case approxPoly tr2 iv approxSteps of
- | NONE => NONE
- | SOME (appr2, err2) =>
- SOME (appr1 -p appr2, err1 + err2))
- | Neg tr1 =>
- (case approxPoly tr1 iv approxSteps of
- | NONE => NONE
- | SOME (appr1, err1) =>
- SOME (--p appr1, err1))
- | _ => NONE
-End
-
(**
Checks that the zero intervals encoded in the certificate actually are
all of the zeros of derivative of the difference between the approximated
@@ -380,212 +266,6 @@ Proof
Induct_on ‘hints’ >> gs[getExpHint_def, CaseEq"hint"]
QED
-Definition approxPolySideCond_def:
- approxPolySideCond approxSteps =
- (0 < approxSteps ∧ EVEN approxSteps ∧ EVEN (approxSteps DIV 2))
-End
-
-Theorem approxPoly_soundness:
- ∀ transc iv approxSteps p err.
- approxPolySideCond approxSteps ∧
- approxPoly transc iv approxSteps = SOME (p, err) ⇒
- ∀ x.
- FST iv ≤ x ∧ x ≤ SND iv ⇒
- abs (interp transc x - evalPoly p x) ≤ err
-Proof
- ho_match_mp_tac approxPoly_ind
- >> rpt strip_tac
- >> qpat_x_assum ‘approxPoly _ _ _ = SOME _’ mp_tac
- >> Cases_on ‘transc’ >> simp[Once approxPoly_def, CaseEq"transc", CaseEq"option", CaseEq"prod"]
- >> rpt strip_tac >> gs[approxPolySideCond_def]
- >- (
- ‘s = "exp" ∨ s = "cos" ∨ s = "sin"’
- by (every_case_tac >> gs[getExpHint_SOME_MEM])
- (* exp function *)
- >- (
- gs[interp_def, getFun_def]
- >> Cases_on ‘iv = (0, inv 2)’ >> gs[]
- (* exp function, 0 to 1/2 *)
- >- (
- qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_EXP_LE
- >> pop_assum $ rewrite_tac o single
- >> rpt VAR_EQ_TAC
- >> rewrite_tac[exp_sum_to_poly]
- >> qmatch_goalsub_abbrev_tac ‘abs (exp_taylor + taylor_rem - exp_taylor) ≤ _’
- >> ‘exp_taylor + taylor_rem - exp_taylor = taylor_rem’ by real_tac
- >> pop_assum $ rewrite_tac o single
- >> unabbrev_all_tac
- >> ‘exp_err_small approxSteps = inv (&FACT approxSteps * 2 pow (approxSteps - 1))’ by EVAL_TAC
- >> rename1 ‘exp t’
- >> qspecl_then [‘approxSteps’, ‘x’,‘t’] mp_tac exp_remainder_bounded_small
- >> impl_tac >> gs[]
- >> real_tac)
- (* exp function, 0 to 1 *)
- >> ‘1 ≠inv 2’
- by (once_rewrite_tac [GSYM REAL_INV1]
- >> CCONTR_TAC
- >> pop_assum $ mp_tac o SIMP_RULE std_ss []
- >> rewrite_tac[REAL_INV_INJ] >> real_tac)
- >> rpt VAR_EQ_TAC
- >> rewrite_tac[GSYM poly_compat, eval_simps]
- >> pop_assum $ rewrite_tac o single
- >> rewrite_tac[exp_sum_to_poly]
- >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_EXP_LE
- >> pop_assum $ rewrite_tac o single
- >> qmatch_goalsub_abbrev_tac ‘abs (exp_taylor + taylor_rem - exp_taylor) ≤ _’
- >> ‘exp_taylor + taylor_rem - exp_taylor = taylor_rem’ by real_tac
- >> pop_assum $ rewrite_tac o single
- >> unabbrev_all_tac
- >> qmatch_goalsub_abbrev_tac ‘exp_err_big n _’
- >> ‘exp_err_big n approxSteps = 2 pow n * &n pow approxSteps * inv (&FACT approxSteps * 2 pow approxSteps)’
- by (rewrite_tac[] >> EVAL_TAC)
- >> pop_assum $ rewrite_tac o single
- >> qspecl_then [‘approxSteps’, ‘n’, ‘x’,‘t’] mp_tac exp_remainder_bounded_big
- >> impl_tac
- >- (
- rpt conj_tac >> TRY (gs[] >> real_tac >> NO_TAC)
- >> ‘2 *x ≤ &n’
- by (unabbrev_all_tac >> cond_cases_tac
- >> gs[]
- >- (
- ‘SND iv = 0’ by real_tac
- >> pop_assum $ rewrite_tac o single
- >> ‘x = 0’ by real_tac
- >> pop_assum $ rewrite_tac o single
- >> gs[REAL_MUL_RZERO, REAL_DIV_LZERO, EVAL “flr 0â€])
- >- (
- pop_assum $ rewrite_tac o single o GSYM
- >> real_tac)
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘&clg (2 * x)’
- >> gs[LE_NUM_CEILING]
- >> cond_cases_tac >> gs[]
- >> rewrite_tac[GSYM REAL_OF_NUM_LE]
- >> irule REAL_LE_TRANS >> qexists_tac ‘&flr (2 * SND iv)’
- >> conj_tac
- >> gs[REAL_OF_NUM_LE]
- >> irule NUM_FLOOR_MONO
- >> rpt conj_tac >> real_tac)
- >- gs[]
- >> irule REAL_LE_TRANS >> qexists_tac ‘abs t’
- >> conj_tac >- gs[ABS_LE]
- >> irule REAL_LE_TRANS >> qexists_tac ‘abs x’
- >> gs[abs])
- >> rewrite_tac[])
- (* cos function *)
- >- (
- gs[interp_def, getFun_def] >> rpt VAR_EQ_TAC
- >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_COS_LE
- >> gs[]
- >> pop_assum $ rewrite_tac o single
- >> gs[cos_sum_to_poly]
- >> qmatch_goalsub_abbrev_tac ‘abs (cos_taylor + taylor_rem - cos_taylor) ≤ _’
- >> ‘cos_taylor + taylor_rem - cos_taylor = taylor_rem’ by real_tac
- >> pop_assum $ rewrite_tac o single
- >> unabbrev_all_tac
- >> ‘(x pow approxSteps) * cos t * inv (&FACT approxSteps) =
- (cos t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
- by real_tac
- >> ‘-(x pow approxSteps) * cos t * inv (&FACT approxSteps) =
- -(cos t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
- by real_tac
- >> rewrite_tac []
- >> ntac 2 $ pop_assum $ rewrite_tac o single
- >> rewrite_tac [GSYM REAL_MUL_ASSOC]
- >> qmatch_goalsub_abbrev_tac ‘abs (cos _ * err_cos_concr)’
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘ 1 * abs err_cos_concr’ >> conj_tac
- >- (rewrite_tac[ABS_MUL] >> irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[COS_BOUND, ABS_POS])
- >> rewrite_tac[REAL_MUL_LID]
- >> ‘abs err_cos_concr = err_cos_concr’
- by (unabbrev_all_tac
- >> rewrite_tac[ABS_REFL]
- >> irule REAL_LE_MUL >> conj_tac
- >- (irule REAL_LE_INV >> gs[REAL_POS])
- >> irule REAL_LE_MUL >> conj_tac
- >> gs[REAL_POW_GE0])
- >> pop_assum $ rewrite_tac o single
- >> unabbrev_all_tac
- >> rewrite_tac [cos_err_def]
- >> imp_res_tac EVEN_ODD_EXISTS >> gs[POW_MINUS1]
- >> irule REAL_LE_LMUL_IMP >> gs[GSYM POW_ABS]
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘abs (x pow (2 * m))’ >> gs[ABS_LE, GSYM POW_ABS]
- >> irule POW_LE >> gs[ABS_POS]
- >> irule RealSimpsTheory.maxAbs >> gs[])
- (* sin *)
- >> gs[interp_def, getFun_def] >> rpt VAR_EQ_TAC
- >> qspecl_then [‘x’, ‘approxSteps’] strip_assume_tac MCLAURIN_SIN_LE
- >> gs[]
- >> pop_assum $ rewrite_tac o single
- >> gs[sin_sum_to_poly]
- >> qmatch_goalsub_abbrev_tac ‘abs (sin_taylor + taylor_rem - sin_taylor) ≤ _’
- >> ‘sin_taylor + taylor_rem - sin_taylor = taylor_rem’ by real_tac
- >> pop_assum $ rewrite_tac o single
- >> unabbrev_all_tac
- >> ‘inv (&FACT approxSteps) * sin t * x pow approxSteps * -1 pow (approxSteps DIV 2) =
- (sin t * ((x pow approxSteps) * inv (&FACT approxSteps) * -1 pow (approxSteps DIV 2)))’
- by real_tac
- >> ‘-(x pow approxSteps) * inv (&FACT approxSteps) * sin t =
- -(sin t * ((x pow approxSteps) * inv (&FACT approxSteps)))’
- by real_tac
- >> rewrite_tac []
- >> ntac 2 $ pop_assum $ rewrite_tac o single
- >> rewrite_tac[GSYM REAL_MUL_ASSOC]
- >> qmatch_goalsub_abbrev_tac ‘_ * err_sin_concr’
- >> rewrite_tac [ABS_NEG, Once ABS_MUL]
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘ 1 * abs err_sin_concr’ >> conj_tac
- >- (irule REAL_LE_RMUL_IMP >> unabbrev_all_tac >> gs[SIN_BOUND, ABS_POS])
- >> rewrite_tac [REAL_MUL_LID, sin_err_def, ABS_MUL]
- >> ‘abs err_sin_concr = err_sin_concr’
- by (unabbrev_all_tac
- >> rewrite_tac[ABS_REFL]
- >> irule REAL_LE_MUL >> conj_tac
- >> gs[REAL_POW_GE0]
- >> irule REAL_LE_MUL >> gs[REAL_POS, REAL_POW_GE0])
- >> pop_assum $ rewrite_tac o single
- >> unabbrev_all_tac
- >> rewrite_tac [sin_err_def]
- >> imp_res_tac EVEN_ODD_EXISTS >> gs[POW_MINUS1]
- >> irule REAL_LE_LMUL_IMP >> gs[GSYM POW_ABS]
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘abs (x pow (2 * m))’ >> gs[ABS_LE, GSYM POW_ABS]
- >> irule POW_LE >> gs[ABS_POS]
- >> irule RealSimpsTheory.maxAbs >> gs[])
- >- (
- rpt VAR_EQ_TAC
- >> gs[interp_def, eval_simps]
- >> qmatch_goalsub_abbrev_tac ‘abs (f_x + g_x - (f_poly_x + g_poly_x)) ≤ _’
- >> ‘f_x + g_x - (f_poly_x + g_poly_x) = (f_x - f_poly_x) + (g_x - g_poly_x)’
- by real_tac
- >> pop_assum $ rewrite_tac o single
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘abs (f_x - f_poly_x) + abs (g_x - g_poly_x)’
- >> gs[REAL_ABS_TRIANGLE]
- >> irule REAL_LE_ADD2 >> unabbrev_all_tac >> gs[])
- >- (
- rpt VAR_EQ_TAC
- >> gs[interp_def, eval_simps]
- >> qmatch_goalsub_abbrev_tac ‘abs (f_x - g_x - (f_poly_x - g_poly_x)) ≤ _’
- >> ‘f_x - g_x - (f_poly_x - g_poly_x) = (f_x - f_poly_x) - (g_x - g_poly_x)’
- by real_tac
- >> pop_assum $ rewrite_tac o single
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘abs (f_x - f_poly_x) + abs (- (g_x - g_poly_x))’
- >> conj_tac
- >- (rewrite_tac[real_sub] >> irule REAL_ABS_TRIANGLE)
- >> gs[real_sub]
- >> irule REAL_LE_ADD2 >> unabbrev_all_tac >> gs[])
- >> rpt VAR_EQ_TAC
- >> gs[interp_def, eval_simps, real_sub]
- >> qmatch_goalsub_abbrev_tac ‘abs (- f_x + f_poly_x)’
- >> ‘- f_x + f_poly_x = f_poly_x - f_x’ by real_tac
- >> pop_assum $ rewrite_tac o single
- >> once_rewrite_tac [ABS_SUB]
- >> unabbrev_all_tac >> gs[real_sub]
-QED
-
(*
Theorem checker_soundness:
∀ cert approxSteps.
diff --git a/mcLaurinApproxScript.sml b/mcLaurinApproxScript.sml
index ae5728ea525e82cadd863fe76d779eb922823810..4a44a00f4b45f64f9816d20b2470d3248b762389 100644
--- a/mcLaurinApproxScript.sml
+++ b/mcLaurinApproxScript.sml
@@ -114,46 +114,6 @@ Proof
>> gs[]
QED
-Theorem sin_even_remainder_bounded:
- ∀ n.
- EVEN n ⇒
- inv (&FACT n) * sin t * x pow n * -1 pow (n DIV 2) ≤
- abs(inv (&FACT n) * x pow n * -1 pow (n DIV 2))
-Proof
- rpt strip_tac
- >> ‘inv (&FACT n) * x pow n * -1 pow (n DIV 2) = inv (&FACT n) * 1 * x pow n * -1 pow (n DIV 2)’
- by real_tac
- >> pop_assum $ rewrite_tac o single
- >> rewrite_tac[GSYM REAL_MUL_ASSOC]
- >> once_rewrite_tac[REAL_ABS_MUL]
- >> ‘0 ≤ inv (&FACT n)’
- by gs[REAL_LE_INV]
- >> ‘abs (inv (&FACT n)) = inv (&FACT n)’ by gs[abs]
- >> pop_assum $ rewrite_tac o single
- >> irule REAL_LE_LMUL_IMP
- >> reverse conj_tac >- gs[]
- >> once_rewrite_tac[REAL_ABS_MUL]
- >> Cases_on ‘0 ≤ x pow n * -1 pow (n DIV 2)’
- >- (
- ‘abs (x pow n * -1 pow (n DIV 2)) = x pow n * -1 pow (n DIV 2)’ by gs[abs]
- >> pop_assum $ rewrite_tac o single
- >> irule REAL_LE_RMUL_IMP >> gs[SIN_BOUNDS])
- >> ‘x pow n * -1 pow (n DIV 2) < 0’ by real_tac
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘-1 * (x pow n * -1 pow (n DIV 2))’
- >> conj_tac
- >- (
- once_rewrite_tac [REAL_MUL_COMM]
- >> drule REAL_LE_LMUL_NEG
- >> disch_then $ qspecl_then [‘sin t’, ‘-1’] $ rewrite_tac o single
- >> gs[SIN_BOUNDS])
- >> ‘∃ y. x pow n * -1 pow (n DIV 2) = -1 * y ∧ 0 ≤ y’
- by (qexists_tac ‘-1 * x pow n * -1 pow (n DIV 2)’
- >> real_tac)
- >> qpat_x_assum `_ = -1 * y` $ rewrite_tac o single
- >> gs[ABS_LE]
-QED
-
Theorem MCLAURIN_COS_LE:
∀ x n. ∃t. abs(t) ≤ abs (x) ∧
(\n. if EVEN n then
@@ -229,7 +189,6 @@ Proof
>> gs[]
QED
-
(*** Prove lemma for bound on exp in the interval, x ∈ [0, 0.5]
based on John Harrison's paper **)
@@ -324,275 +283,7 @@ Proof
>> MATCH_MP_TAC REAL_LE_MUL >> gs[]
QED
-Definition exp_poly_def:
- exp_poly 0 = [] ∧ (* x pow 0 * inv FACT 0 *)
- exp_poly (SUC n) = (exp_poly n) ++ [inv (&FACT n)]
-End
-
-Theorem exp_poly_LENGTH:
- LENGTH (exp_poly n) = n
-Proof
- Induct_on ‘n’ >> gs[exp_poly_def]
-QED
-
-Theorem exp_sum_to_poly:
- ∀ n x. evalPoly (exp_poly n) x = sum (0,n) (λ m. x pow m / &FACT m)
-Proof
- Induct_on ‘n’ >> gs[exp_poly_def, evalPoly_def, sum]
- >> rpt strip_tac >> gs[evalPoly_app, evalPoly_def, exp_poly_LENGTH]
-QED
-
-Theorem exp_remainder_bounded_small:
- ∀ n x t.
- 0 < n ∧ abs t ≤ abs x ∧ 0 ≤ x ∧
- t ≤ inv 2 ∧ x ≤ inv 2 ⇒
- abs (exp t / &FACT n * x pow n) ≤ inv (&FACT n * 2 pow (n - 1))
-Proof
- rpt strip_tac >> rewrite_tac[real_div, abs]
- >> qmatch_goalsub_abbrev_tac ‘(if 0 ≤ exp_bound then _ else _) ≤ _’
- >> ‘0 ≤ exp_bound’
- by (
- unabbrev_all_tac
- >> rpt (irule REAL_LE_MUL >> gs[POW_POS, EXP_POS_LE]))
- >> simp[] >> unabbrev_all_tac
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘(1 + 2 * inv 2) * (inv (&FACT n) * x pow n)’
- >> conj_tac
- >- (
- rewrite_tac[GSYM REAL_MUL_ASSOC]
- >> irule REAL_LE_RMUL_IMP
- >> conj_tac
- >- (
- Cases_on ‘0 ≤ t’
- >- (
- irule REAL_LE_TRANS
- >> qexists_tac ‘1 + 2 * t’ >> conj_tac
- >- (irule REAL_EXP_BOUND_LEMMA >> gs[])
- >> real_tac)
- >> ‘t = - (- t)’ by real_tac
- >> pop_assum $ once_rewrite_tac o single
- >> once_rewrite_tac[EXP_NEG]
- >> ‘- (inv 2) ≤ -t’ by real_tac
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘inv (exp (- (inv 2)))’
- >> conj_tac
- >- (irule REAL_INV_LE_ANTIMONO_IMPR >> gs[EXP_POS_LT, EXP_MONO_LE])
- >> rewrite_tac[EXP_NEG, REAL_INV_INV]
- >> irule REAL_EXP_BOUND_LEMMA >> gs[])
- >> irule REAL_LE_MUL >> gs[REAL_LE_INV, POW_POS])
- >> ‘1 + 2 * inv 2 = 2’ by gs[]
- >> pop_assum $ rewrite_tac o single
- >> rewrite_tac[GSYM REAL_MUL_ASSOC, REAL_INV_MUL']
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘2 * (inv (&FACT n) * inv 2 pow n)’
- >> conj_tac
- >- (
- irule REAL_LE_LMUL_IMP >> reverse conj_tac >- gs[]
- >> irule REAL_LE_LMUL_IMP >> reverse conj_tac >- gs[REAL_LE_INV]
- >> irule POW_LE >> gs[])
- >> Cases_on ‘n’ >- gs[]
- >> rewrite_tac[pow]
- >> gs[REAL_INV_MUL']
-QED
-
-Theorem exp_remainder_bounded_big:
- ∀ n m x t.
- 0 < n ∧ abs t ≤ abs x ∧ 0 ≤ x ∧
- x ≤ &m * (inv 2) ∧
- t ≤ &m * (inv 2) ⇒
- abs (exp t / &FACT n * x pow n) ≤ 2 pow m * &m pow n * (inv (&FACT n * 2 pow n))
-Proof
- rpt strip_tac >> rewrite_tac[real_div, abs]
- >> qmatch_goalsub_abbrev_tac ‘(if 0 ≤ exp_bound then _ else _) ≤ _’
- >> ‘0 ≤ exp_bound’
- by (
- unabbrev_all_tac
- >> rpt (irule REAL_LE_MUL >> gs[POW_POS, EXP_POS_LE]))
- >> pop_assum $ rewrite_tac o single
- >> unabbrev_all_tac
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘exp (&m * inv 2) * (inv (&FACT n) * x pow n)’
- >> conj_tac
- >- (
- rewrite_tac[GSYM REAL_MUL_ASSOC]
- >> irule REAL_LE_RMUL_IMP
- >> conj_tac
- >- gs[EXP_MONO_LE]
- >> irule REAL_LE_MUL >> gs[REAL_LE_INV, POW_POS])
- >> rewrite_tac[EXP_N]
- >> qmatch_goalsub_abbrev_tac ‘_ * cst_err ≤ _’
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘(1 + 2 * inv 2) pow m * cst_err’
- >> conj_tac
- >- (
- irule REAL_LE_RMUL_IMP
- >> conj_tac
- >- (
- irule POW_LE >> rewrite_tac[EXP_POS_LE]
- >> irule REAL_EXP_BOUND_LEMMA >> gs[])
- >> unabbrev_all_tac
- >> irule REAL_LE_MUL >> gs[REAL_LE_INV, POW_POS])
- >> ‘1 + 2 * inv 2 = 2’ by gs[]
- >> pop_assum $ rewrite_tac o single
- >> unabbrev_all_tac
- >> rewrite_tac[REAL_MUL_ASSOC]
- >> qmatch_goalsub_abbrev_tac ‘cst_err * x pow n’
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘cst_err * (&m * inv 2) pow n’ >> conj_tac
- >- (
- irule REAL_LE_LMUL_IMP >> conj_tac
- >- gs[POW_LE]
- >> unabbrev_all_tac >> irule REAL_LE_MUL
- >> gs[REAL_LE_INV, POW_POS])
- >> rewrite_tac [POW_MUL]
- >> unabbrev_all_tac
- >> qmatch_goalsub_abbrev_tac ‘curr_bound ≤ _’
- >> ‘curr_bound = 2 pow m * &m pow n * (inv (&FACT n * 2 pow n))’
- by (unabbrev_all_tac >> gs[REAL_POW_INV])
- >> pop_assum $ rewrite_tac o single
- >> unabbrev_all_tac >> gs[]
-QED
-
-Definition cos_poly_def:
- cos_poly 0 = [] ∧
- cos_poly (SUC n) =
- if (EVEN n) then
- cos_poly n ++ [-1 pow (n DIV 2) * inv (&FACT n)]
- else cos_poly n ++ [0]
-End
-
-Theorem LENGTH_cos_poly:
- LENGTH (cos_poly n) = n
-Proof
- Induct_on ‘n’ >> gs[cos_poly_def]
- >> cond_cases_tac >> gs[]
-QED
-
-Theorem cos_sum_to_poly:
- ∀ n x. evalPoly (cos_poly n) x =
- sum(0,n)
- (λm.
- (&FACT m)â»Â¹ * x pow m *
- if EVEN m then cos 0 * -1 pow (m DIV 2)
- else sin 0 * -1 pow ((SUC m) DIV 2))
-Proof
- Induct_on ‘n’ >> gs[sum, evalPoly_def, cos_poly_def]
- >> cond_cases_tac
- >> gs[evalPoly_app, COS_0, SIN_0, evalPoly_def, LENGTH_cos_poly]
-QED
-
-Theorem cos_even_remainder_bounded:
- ∀ n.
- EVEN n ⇒
- inv (&FACT n) * cos t * x pow n * -1 pow (n DIV 2) ≤
- abs(inv (&FACT n) * x pow n * -1 pow (n DIV 2))
-Proof
- rpt strip_tac
- >> ‘inv (&FACT n) * x pow n * -1 pow (n DIV 2) = inv (&FACT n) * 1 * x pow n * -1 pow (n DIV 2)’
- by real_tac
- >> pop_assum $ rewrite_tac o single
- >> rewrite_tac[GSYM REAL_MUL_ASSOC]
- >> once_rewrite_tac[REAL_ABS_MUL]
- >> ‘0 ≤ inv (&FACT n)’
- by gs[REAL_LE_INV]
- >> ‘abs (inv (&FACT n)) = inv (&FACT n)’ by gs[abs]
- >> pop_assum $ rewrite_tac o single
- >> irule REAL_LE_LMUL_IMP
- >> reverse conj_tac >- gs[]
- >> once_rewrite_tac[REAL_ABS_MUL]
- >> Cases_on ‘0 ≤ x pow n * -1 pow (n DIV 2)’
- >- (
- ‘abs (x pow n * -1 pow (n DIV 2)) = x pow n * -1 pow (n DIV 2)’ by gs[abs]
- >> pop_assum $ rewrite_tac o single
- >> irule REAL_LE_RMUL_IMP >> gs[COS_BOUNDS])
- >> ‘x pow n * -1 pow (n DIV 2) < 0’ by real_tac
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘-1 * (x pow n * -1 pow (n DIV 2))’
- >> conj_tac
- >- (
- once_rewrite_tac [REAL_MUL_COMM]
- >> drule REAL_LE_LMUL_NEG
- >> disch_then $ qspecl_then [‘cos t’, ‘-1’] $ rewrite_tac o single
- >> gs[COS_BOUNDS])
- >> ‘∃ y. x pow n * -1 pow (n DIV 2) = -1 * y ∧ 0 ≤ y’
- by (qexists_tac ‘-1 * x pow n * -1 pow (n DIV 2)’
- >> real_tac)
- >> qpat_x_assum `_ = -1 * y` $ rewrite_tac o single
- >> gs[ABS_LE]
-QED
-
-(** sin **)
-Definition sin_poly_def:
- sin_poly 0 = [] ∧
- sin_poly (SUC n) =
- if (EVEN n) then sin_poly n ++ [0]
- else sin_poly n ++ [-1 pow ((n - 1) DIV 2) * inv (&FACT n)]
-End
-
-Theorem LENGTH_sin_poly:
- LENGTH (sin_poly n) = n
-Proof
- Induct_on ‘n’ >> gs[sin_poly_def]
- >> cond_cases_tac >> gs[]
-QED
-
-Theorem sin_sum_to_poly:
- ∀ n x.
- evalPoly (sin_poly n) x =
- sum(0,n)
- (λm.
- (&FACT m)â»Â¹ * x pow m *
- if EVEN m then sin 0 * -1 pow (m DIV 2)
- else cos 0 * -1 pow ((m - 1) DIV 2))
-Proof
- Induct_on ‘n’ >> gs[sum, evalPoly_def, sin_poly_def]
- >> cond_cases_tac
- >> gs[evalPoly_app, SIN_0, COS_0, evalPoly_def, LENGTH_sin_poly]
-QED
-
-Theorem sin_even_remainder_bounded:
- ∀ n.
- EVEN n ⇒
- inv (&FACT n) * sin t * x pow n * -1 pow (n DIV 2) ≤
- abs(inv (&FACT n) * x pow n * -1 pow (n DIV 2))
-Proof
- rpt strip_tac
- >> ‘inv (&FACT n) * x pow n * -1 pow (n DIV 2) = inv (&FACT n) * 1 * x pow n * -1 pow (n DIV 2)’
- by real_tac
- >> pop_assum $ rewrite_tac o single
- >> rewrite_tac[GSYM REAL_MUL_ASSOC]
- >> once_rewrite_tac[REAL_ABS_MUL]
- >> ‘0 ≤ inv (&FACT n)’
- by gs[REAL_LE_INV]
- >> ‘abs (inv (&FACT n)) = inv (&FACT n)’ by gs[abs]
- >> pop_assum $ rewrite_tac o single
- >> irule REAL_LE_LMUL_IMP
- >> reverse conj_tac >- gs[]
- >> once_rewrite_tac[REAL_ABS_MUL]
- >> Cases_on ‘0 ≤ x pow n * -1 pow (n DIV 2)’
- >- (
- ‘abs (x pow n * -1 pow (n DIV 2)) = x pow n * -1 pow (n DIV 2)’ by gs[abs]
- >> pop_assum $ rewrite_tac o single
- >> irule REAL_LE_RMUL_IMP >> gs[SIN_BOUNDS])
- >> ‘x pow n * -1 pow (n DIV 2) < 0’ by real_tac
- >> irule REAL_LE_TRANS
- >> qexists_tac ‘-1 * (x pow n * -1 pow (n DIV 2))’
- >> conj_tac
- >- (
- once_rewrite_tac [REAL_MUL_COMM]
- >> drule REAL_LE_LMUL_NEG
- >> disch_then $ qspecl_then [‘sin t’, ‘-1’] $ rewrite_tac o single
- >> gs[SIN_BOUNDS])
- >> ‘∃ y. x pow n * -1 pow (n DIV 2) = -1 * y ∧ 0 ≤ y’
- by (qexists_tac ‘-1 * x pow n * -1 pow (n DIV 2)’
- >> real_tac)
- >> qpat_x_assum `_ = -1 * y` $ rewrite_tac o single
- >> gs[ABS_LE]
-QED
-
-
(** Mclaurin series for sqrt fucntion **)
-
(** Idea is to convert the sqrt function to exp (ln x /2) **)
Theorem diff_chain:
∀x. ((λx. 1 + x) diffl 1) x
@@ -609,7 +300,6 @@ Proof
>> gs[limTheory.DIFF_X]
QED
-
Theorem SQRT_EXPLN_DIFF:
∀x. 0 <= x ⇒ ((λx. exp ((\x. (ln (1+x)) / &2) x)) diffl
(exp ((\x. (ln (1+x)) / &2) x) * (inv (1+x) / &2))) x
@@ -649,7 +339,6 @@ Proof
>> gs[REAL_LET_ADD]
QED
-
Theorem exp_add_EXPLN:
∀ m t. m ≠0 ⇒ 0 ≤ t ⇒
exp (ln (1 + t) * &(2 * m + 1) / &2) =
@@ -898,7 +587,6 @@ Proof
(λx. &FACT (2 * PRE m) *( (\x.
(exp (ln (1 + x) * &(2 * PRE m + 1) / 2))â»Â¹ ) x)) ’
by gs[FUN_EQ_THM]
-
>> pop_assum $ rewrite_tac o single
>> irule limTheory.DIFF_CMUL
>> ‘ &(2 * m) = &2 * &m ’ by gs[GSYM REAL_OF_NUM_MUL]
@@ -1018,7 +706,6 @@ fun real_rw (t:Q.tmquote) =
fun transitivity_for t =
irule REAL_LE_TRANS >> qexists_tac t
-
Theorem EXP_MINUS_ONE_POS:
∀ x. 0 ≤ x ⇒
0 ≤ exp x - 1
@@ -1029,6 +716,7 @@ Proof
>> gs[EXP_0, EXP_MONO_LE]
QED
+(** TODO: Move?
Theorem MCLAURIN_EXP_COMPOSITE_ERR:
∀ (f:real->real) (q:poly) (r:real->real) x n lb ub ubQ.
0 ≤ ubQ ∧ (* The upper bound is positive *)
@@ -1093,6 +781,7 @@ Proof
>> qspec_then ‘r x’ mp_tac REAL_EXP_BOUND_LEMMA
>> gs[]
QED
+ **)
Theorem MCLAURIN_SIN_COMPOSITE:
∀ f q r x.
diff --git a/transcIntvSemScript.sml b/transcIntvSemScript.sml
new file mode 100644
index 0000000000000000000000000000000000000000..256fd2345aaa7f89c86347b48cb98c9d91af52ff
--- /dev/null
+++ b/transcIntvSemScript.sml
@@ -0,0 +1,257 @@
+(**
+ Define a simple "language" for describing transcendental
+ functions. For now we only allow combinations, i.e.
+ exp (sin (cos ...) but no additional operators like +,-,*,/
+**)
+open realTheory realLib RealArith transcTheory;
+open IntervalArithTheory sqrtApproxTheory IntervalValidationTheory;
+open realPolyTheory transcLangTheory approxPolyTheory;
+open preamble;
+
+val _ = new_theory "transcIntvSem";
+
+Definition intvUop_def:
+ intvUop (Neg:transcLang$unop) iv = negateInterval iv ∧
+ intvUop Inv iv = invertInterval iv
+End
+
+Definition intvBop_def:
+ intvBop (Add:transcLang$binop) iv1 iv2 = addInterval iv1 iv2 ∧
+ intvBop Sub iv1 iv2 = subtractInterval iv1 iv2 ∧
+ intvBop Mul iv1 iv2 = multInterval iv1 iv2 ∧
+ intvBop Div iv1 iv2 = divideInterval iv1 iv2
+End
+
+Definition evalPolyIntv_def:
+ evalPolyIntv [] iv = (0,0) ∧
+ evalPolyIntv (c::cs) iv = intvBop Add (c,c) (intvBop Mul iv (evalPolyIntv cs iv))
+End
+
+Definition internalSteps_def:
+ internalSteps:num = 40
+End
+
+Definition newtonIters_def:
+ newtonIters:num = 4
+End
+
+(**
+ compute an interval bound for a transcendental/ HOL4 uncomputable function.
+ We include sqrt here as it cannot be evaluated in HOL4 directly.
+ The newton approximation trick is borrowed from FloVer.
+ As we have to validate the newton approximation afterwards, it may fail
+ to compute an interval bound thus we return an option here.
+ In practice, we have not yet encountered a case where 4 iterations where not
+ sufficient in combination with the multiplications
+**)
+Definition getFunIv_def:
+ getFunIv Exp iv =
+ (let
+ lbExp = evalPoly (expPoly internalSteps) (FST iv);
+ ubExp = evalPoly (expPoly internalSteps) (SND iv) +
+ if iv = (0, inv 2) then expErrSmall internalSteps
+ else expErrBig (clg (abs (SND iv) * 2)) internalSteps;
+ in
+ SOME (lbExp, ubExp)) ∧
+ getFunIv Sin iv = SOME (-1, 1) ∧
+ getFunIv Cos iv = SOME (-1, 1) ∧
+ getFunIv Tan iv = SOME (-1, 1) ∧
+ getFunIv Sqrt iv =
+ (* we do a newton approximation of the lower and upper bounds,
+ 0 < FST iv has to be checked before *)
+ let sqrtLo = newton newtonIters (FST iv * 0.99) (IVlo iv * 0.99);
+ sqrtHi = newton newtonIters (SND iv * 1.01) (SND iv * 1.01);
+ newIV = (sqrtLo, sqrtHi)
+ in
+ if (validate_newton_down sqrtLo (FST iv) ∧
+ validate_newton_up sqrtHi (SND iv)) then
+ SOME newIV
+ else NONE
+End
+
+Definition interpIntv_def:
+ interpIntv (Var x) (env:(string#(real#real)) list) =
+ do xv <- FIND (λ (y, iv). y = x) env;
+ return (SND xv);
+ od ∧
+ interpIntv (Cst c) env = SOME (c,c) ∧
+ interpIntv (Uop uop t) env =
+ do r <- interpIntv t env;
+ assert ((~ (uop = Inv)) ∨ (SND r < 0 ∨ 0 < FST r ));
+ return (intvUop uop r)
+ od ∧
+ interpIntv (Bop bop t1 t2) env =
+ do
+ r1 <- interpIntv t1 env;
+ r2 <- interpIntv t2 env;
+ if bop = Div ∧ ~(SND r2 < 0 ∨ 0 < FST r2)
+ then NONE
+ else return (intvBop bop r1 r2);
+ od ∧
+ interpIntv (Fun s t) env =
+ do
+ r <- interpIntv t env;
+ (* Sqrt defined for positive values only *)
+ assert ((~ (s = Sqrt)) ∨ (0 < FST r));
+ (* Tan cannot be done at 0 because we approximate it with sin x/cos x *)
+ assert ((~ (s = Tan)) ∨ (SND r < 0 ∨ 0 < FST r ));
+ getFunIv s r;
+ od ∧
+ interpIntv (Poly p t) env =
+ do
+ r <- interpIntv t env;
+ return (evalPolyIntv p r)
+ od
+End
+
+Definition varsContained_def:
+ varsContained (cenv:(string#real) list) (ivenv:(string#(real#real)) list) =
+ ∀ x xiv.
+ FIND (λ (y,r). y = x) ivenv = SOME xiv ⇒
+ ∃ xr.
+ FIND (λ (y,r). y = x) cenv = SOME xr ∧
+ FST (SND xiv) ≤ SND xr ∧ SND xr ≤ SND (SND xiv)
+End
+
+Theorem evalPolyIntv_sound:
+ ∀ p x iv.
+ FST iv ≤ x ∧
+ x ≤ SND iv ⇒
+ FST (evalPolyIntv p iv) ≤ evalPoly p x ∧
+ evalPoly p x ≤ SND (evalPolyIntv p iv)
+Proof
+ Induct_on ‘p’ >> gs[evalPolyIntv_def, evalPoly_def]
+ >> rpt strip_tac
+ >> first_x_assum $ drule_then $ drule_then assume_tac
+ >> ‘contained (evalPoly p x) (evalPolyIntv p iv)’ by gs[contained_def]
+ >> ‘contained x iv’ by gs[contained_def]
+ >> pop_assum $ mp_then Any mp_tac interval_multiplication_valid
+ >> disch_then (fn th => pop_assum $ mp_then Any mp_tac th)
+ >> qspec_then ‘h’ (assume_tac o SIMP_RULE std_ss [pointInterval_def]) validPointInterval
+ >> pop_assum $ mp_then Any mp_tac (SIMP_RULE std_ss [validIntervalAdd_def] interval_addition_valid)
+ >> disch_then (fn th => disch_then $ mp_then Any mp_tac th)
+ >> strip_tac >> gs[contained_def, intvBop_def]
+QED
+
+Theorem interpIntv_sound:
+ ∀ t cenv ivenv iv r.
+ varsContained cenv ivenv ∧
+ interpIntv t ivenv = SOME iv ⇒
+ ∃ r.
+ interp t cenv = SOME r ∧
+ FST iv ≤ r ∧ r ≤ SND iv
+Proof
+ Induct_on ‘t’ >> gs[interpIntv_def, interp_def]
+ >> rpt strip_tac
+ >- (
+ last_x_assum drule >> disch_then $ drule_then strip_assume_tac
+ >> gs[PULL_EXISTS]
+ >> Cases_on ‘t0’ >> gs[getFun_def, getFunIv_def]
+ >> rpt VAR_EQ_TAC >> gs[SIN_BOUNDS, COS_BOUNDS]
+ (* exp *)
+ >- (
+ conj_tac
+ (* lower bound *)
+ >- (
+ irule REAL_LE_TRANS >> qexists_tac ‘exp (FST r)’
+ >> gs[EXP_MONO_LE]
+ >> qspecl_then [‘FST r’, ‘internalSteps’] strip_assume_tac MCLAURIN_EXP_LE
+ >> pop_assum $ rewrite_tac o single
+ >> gs[exp_sum_to_poly]
+ >> irule REAL_LE_MUL
+ >> gs[POW_POS, internalSteps_def]
+ >> irule REAL_LE_MUL
+ >> gs[EXP_POS_LE])
+ (* upper bound *)
+ >> irule REAL_LE_TRANS >> qexists_tac ‘exp (SND r)’
+ >> gs[EXP_MONO_LE]
+ >> qspecl_then [‘SND r’, ‘internalSteps’] strip_assume_tac MCLAURIN_EXP_LE
+ >> pop_assum $ rewrite_tac o single
+ >> gs[exp_sum_to_poly]
+ >> qmatch_goalsub_abbrev_tac ‘exp_err ≤ _’
+ >> irule REAL_LE_TRANS >> qexists_tac ‘abs exp_err’ >> gs[ABS_LE]
+ >> unabbrev_all_tac
+ >> Cases_on ‘r = (0, inv 2)’
+ >> asm_rewrite_tac[expErrSmall_def, GSYM real_div]
+ >- (
+ irule exp_remainder_bounded_small
+ >> Cases_on ‘r’ >> gs[internalSteps_def]
+ >> gs[abs] >> every_case_tac >> real_tac)
+ >> asm_rewrite_tac[expErrBig_def]
+ >> irule exp_remainder_bounded_big
+ >> qmatch_goalsub_abbrev_tac ‘abs (SND r) ≤ upExp’
+ >> ‘abs (SND r) ≤ upExp’
+ by (
+ unabbrev_all_tac
+ >> cond_cases_tac >> gs[]
+ >- (pop_assum $ rewrite_tac o single o GSYM >> gs[])
+ >> irule REAL_LE_TRANS >> qexists_tac ‘&clg (2 * abs (SND r))’
+ >> gs[LE_NUM_CEILING])
+ >> Cases_on ‘r’ >> rpt conj_tac >> TRY( gs[internalSteps_def] >> NO_TAC)
+ >> irule REAL_LE_TRANS
+ >> qexists_tac ‘abs (SND (q,r''))’ >> gs[]
+ >> irule REAL_LE_TRANS >> qexists_tac ‘abs t'’ >> gs[ABS_LE])
+ (* tan 1 *)
+ >- ( cheat )
+ (* tan 2 *)
+ >- ( cheat )
+ (* sqrt *)
+ >> first_x_assum $ mp_then Any mp_tac validate_newton_lb_valid
+ >> impl_tac >> gs[]
+ >- (
+ reverse conj_tac >- real_tac
+ >> irule newton_method_pos >> conj_tac
+ >> irule REAL_LE_MUL >> gs[] >> real_tac)
+ >> first_x_assum $ mp_then Any mp_tac validate_newton_ub_valid
+ >> impl_tac >> gs[]
+ >- (
+ reverse conj_tac >- real_tac
+ >> irule newton_method_pos >> conj_tac
+ >> irule REAL_LE_MUL >> gs[] >> real_tac)
+ >> rpt strip_tac
+ >> irule REAL_LE_TRANS
+ THENL [
+ qexists_tac ‘sqrt (FST r)’,
+ qexists_tac ‘sqrt (SND r)’]
+ >> gs[]
+ >> irule SQRT_MONO_LE >> real_tac)
+ >- (
+ first_x_assum $ drule_then $ drule_then strip_assume_tac
+ >> drule_then drule evalPolyIntv_sound
+ >> disch_then $ qspec_then ‘l’ assume_tac
+ >> gs[PULL_EXISTS])
+ >- (
+ gs[PULL_EXISTS]
+ >> ntac 2 (
+ last_x_assum drule
+ >> disch_then $ drule_then strip_assume_tac)
+ >> Cases_on ‘b’ >> gs[interp_def, intvBop_def]
+ >- (
+ qspecl_then [‘r1’, ‘r2’] mp_tac interval_addition_valid
+ >> gs[validIntervalAdd_def, contained_def, appBop_def]
+ >> rpt $ disch_then drule)
+ >- (
+ qspecl_then [‘r1’, ‘r2’] mp_tac interval_subtraction_valid
+ >> gs[validIntervalSub_def, contained_def, appBop_def]
+ >> rpt $ disch_then drule)
+ >- (
+ qspecl_then [‘r1’, ‘r2’] mp_tac interval_multiplication_valid
+ >> gs[contained_def, appBop_def])
+ >> qspecl_then [‘r1’, ‘r2’] mp_tac interval_division_valid
+ >> gs[contained_def, appBop_def])
+ >- (
+ gs[PULL_EXISTS]
+ >> last_x_assum drule
+ >> disch_then $ drule_then strip_assume_tac
+ >> Cases_on ‘u’ >> gs[interp_def, intvUop_def, appUop_def]
+ >- (
+ qspec_then ‘r’ mp_tac interval_negation_valid
+ >> gs[contained_def])
+ >> qspec_then ‘r’ mp_tac interval_inversion_valid
+ >> gs[contained_def])
+ >> gs[varsContained_def, PULL_EXISTS]
+ >> res_tac
+ >> gs[]
+QED
+
+val _ = export_theory();
diff --git a/transcLangScript.sml b/transcLangScript.sml
index 8277a11298268ca90e46441ebdc3b9a29881bafb..911e75f6f9d3ef7791bd6904c4a89903912ac962 100644
--- a/transcLangScript.sml
+++ b/transcLangScript.sml
@@ -4,37 +4,138 @@
exp (sin (cos ...) but no additional operators like +,-,*,/
**)
open realTheory realLib RealArith transcTheory;
+open realPolyTheory;
open preamble;
val _ = new_theory "transcLang";
+val _ = monadsyntax.enable_monadsyntax();
+val _ = monadsyntax.enable_monad "option";
+
+Datatype:
+ binop = Add | Sub | Mul | Div
+End
+
+Datatype:
+ unop = Neg | Inv
+End
+
+Datatype:
+ trFun = Exp | Sin | Cos | Tan | Sqrt
+End
+
Datatype:
transc =
- Fun string transc
- | Add transc transc
- | Sub transc transc
- | Neg transc
- | Var
+ Fun trFun transc
+ | Poly poly transc
+ | Bop binop transc transc
+ | Uop unop transc
+ | Cst real
+ | Var string
End
Definition getFun_def:
- getFun s =
- case s of
- |"sqrt" => sqrt
- | "exp" => exp
- | "sin" => sin
- | "cos" => cos
- | "tan" => tan
- | _ => λ x. x
+ getFun Exp = exp ∧
+ getFun Sin = sin ∧
+ getFun Cos = cos ∧
+ getFun Tan = tan ∧
+ getFun Sqrt = sqrt
+End
+
+Definition appUop_def:
+ appUop Neg r = - r ∧
+ appUop Inv r = inv r
+End
+
+Definition appBop_def:
+ appBop Add = realax$real_add ∧
+ appBop Sub = $- ∧
+ appBop Mul = $* ∧
+ appBop Div = $/
End
Definition interp_def:
- interp Var x = x ∧
- interp (Neg t) x = - (interp t x) ∧
- interp (Add t1 t2) x = (interp t1 x) + (interp t2 x) ∧
- interp (Sub t1 t2) x = (interp t1 x) - (interp t2 x) ∧
- interp (Fun s trans) x =
- (getFun s) (interp trans x)
+ interp (Var x) env =
+ do v <- FIND (λ (y,r). y = x) env;
+ return (SND v);
+ od ∧
+ interp (Cst c) env = SOME c ∧
+ interp (Uop uop t) env =
+ do r <- interp t env;
+ return (appUop uop r)
+ od ∧
+ interp (Bop bop t1 t2) env =
+ do
+ r1 <- interp t1 env;
+ r2 <- interp t2 env;
+ return (appBop bop r1 r2);
+ od ∧
+ interp (Fun s t) env =
+ do
+ r <- interp t env;
+ return ((getFun s) r);
+ od ∧
+ interp (Poly p t) env =
+ do
+ r <- interp t env;
+ return (evalPoly p r)
+ od
+End
+
+Datatype:
+ transcProg =
+ Let string transc transcProg
+ | Ret transc
+End
+
+Definition interpProg_def:
+ interpProg (Let x e p) env =
+ do
+ r <- interp e env;
+ interpProg p ((x, r)::env)
+ od ∧
+ interpProg (Ret e) env = interp e env
End
+Definition transcProgEq_def:
+ transcProgEq p1 p2 =
+ ∀ env.
+ interpProg p1 env = interpProg p2 env
+End
+
+Theorem transcProgEq_sym:
+ transcProgEq p1 p1
+Proof
+ gs[transcProgEq_def]
+QED
+
+Theorem transcProgEq_tan_ret:
+ ∀ x t.
+ transcProgEq (Ret (Fun Tan t)) (Ret (Bop Div (Fun Sin t) (Fun Cos t)))
+Proof
+ gs[transcProgEq_def, interpProg_def, interp_def]
+ >> rpt strip_tac
+ >> Cases_on ‘interp t env’ >> gs[getFun_def, tan, appBop_def]
+QED
+
+Theorem transcProgEq_Let_rule:
+ x = y ∧
+ (∀ env. interp e1 env = interp e2 env) ∧
+ transcProgEq p1 p2 ⇒
+ transcProgEq (Let x e1 p1) (Let y e2 p2)
+Proof
+ rpt strip_tac >> gs[transcProgEq_def]
+ >> rpt strip_tac >> gs[interpProg_def]
+QED
+
+Theorem transcProgEq_tan_let:
+ ∀ x t.
+ transcProgEq (Let x (Fun Tan t) p) (Let x (Bop Div (Fun Sin t) (Fun Cos t)) p)
+Proof
+ rpt gen_tac >> irule transcProgEq_Let_rule >> gs[transcProgEq_sym]
+ >> rpt strip_tac
+ >> gs[interp_def]
+ >> Cases_on ‘interp t env’ >> gs[getFun_def, appBop_def, tan]
+QED
+
val _ = export_theory();