1signature MULTISERIES_EXPANSION = 2sig 3include MULTISERIES_EXPANSION; 4 5type lower_bound_thm = thm; 6type upper_bound_thm = thm; 7 8datatype limit_result = Exact_Limit of term | Limit_Bounds of term option * term option 9 10type lower_bound = expansion_thm * lower_bound_thm; 11type upper_bound = expansion_thm * upper_bound_thm; 12datatype bounds = 13 Exact of expansion_thm | Bounds of lower_bound option * upper_bound option 14 15val is_vacuous : bounds -> bool 16val lift_bounds : basis -> bounds -> bounds 17val get_expanded_fun_bounds : bounds -> term 18 19val find_smaller_expansion : 20 Lazy_Eval.eval_ctxt -> thm * thm * Asymptotic_Basis.basis -> thm * thm * thm 21val find_greater_expansion : 22 Lazy_Eval.eval_ctxt -> thm * thm * Asymptotic_Basis.basis -> thm * thm * thm 23 24val mult_expansion_bounds : 25 Lazy_Eval.eval_ctxt -> Asymptotic_Basis.basis -> bounds -> bounds -> bounds 26val powr_expansion_bounds : 27 Lazy_Eval.eval_ctxt -> Asymptotic_Basis.basis -> bounds -> bounds -> bounds * basis 28val powr_nat_expansion_bounds : 29 Lazy_Eval.eval_ctxt -> Asymptotic_Basis.basis -> bounds -> bounds -> bounds * basis 30val powr_const_expansion_bounds : Lazy_Eval.eval_ctxt -> bounds * term * basis -> bounds 31val power_expansion_bounds : Lazy_Eval.eval_ctxt -> bounds * term * basis -> bounds 32 33val sgn_expansion_bounds : Lazy_Eval.eval_ctxt -> bounds * basis -> bounds 34 35val expand_term_bounds : Lazy_Eval.eval_ctxt -> term -> basis -> bounds * basis 36val expand_terms_bounds : Lazy_Eval.eval_ctxt -> term list -> basis -> bounds list * basis 37 38val prove_nhds_bounds : Lazy_Eval.eval_ctxt -> bounds * Asymptotic_Basis.basis -> thm 39val prove_at_infinity_bounds : Lazy_Eval.eval_ctxt -> bounds * Asymptotic_Basis.basis -> thm 40val prove_at_top_bounds : Lazy_Eval.eval_ctxt -> bounds * Asymptotic_Basis.basis -> thm 41val prove_at_bot_bounds : Lazy_Eval.eval_ctxt -> bounds * Asymptotic_Basis.basis -> thm 42val prove_at_0_bounds : Lazy_Eval.eval_ctxt -> bounds * Asymptotic_Basis.basis -> thm 43val prove_at_right_0_bounds : Lazy_Eval.eval_ctxt -> bounds * Asymptotic_Basis.basis -> thm 44val prove_at_left_0_bounds : Lazy_Eval.eval_ctxt -> bounds * Asymptotic_Basis.basis -> thm 45val prove_eventually_nonzero_bounds : Lazy_Eval.eval_ctxt -> bounds * Asymptotic_Basis.basis -> thm 46 47val prove_eventually_less_bounds : 48 Lazy_Eval.eval_ctxt -> bounds * bounds * Asymptotic_Basis.basis -> thm 49val prove_eventually_greater_bounds : 50 Lazy_Eval.eval_ctxt -> bounds * bounds * Asymptotic_Basis.basis -> thm 51 52val prove_smallo_bounds : 53 Lazy_Eval.eval_ctxt -> bounds * bounds * Asymptotic_Basis.basis -> thm 54val prove_bigo_bounds : 55 Lazy_Eval.eval_ctxt -> bounds * bounds * Asymptotic_Basis.basis -> thm 56val prove_bigtheta_bounds : 57 Lazy_Eval.eval_ctxt -> bounds * bounds * Asymptotic_Basis.basis -> thm 58val prove_asymp_equiv_bounds : 59 Lazy_Eval.eval_ctxt -> bounds * bounds * Asymptotic_Basis.basis -> thm 60 61val limit_of_expansion_bounds : 62 Lazy_Eval.eval_ctxt -> bounds * Asymptotic_Basis.basis -> limit_result 63 64end 65 66structure Multiseries_Expansion : MULTISERIES_EXPANSION = 67struct 68 69open Multiseries_Expansion; 70open Exp_Log_Expression; 71open Asymptotic_Basis; 72 73type lower_bound_thm = thm; 74type upper_bound_thm = thm; 75 76datatype limit_result = Exact_Limit of term | Limit_Bounds of term option * term option 77 78type lower_bound = expansion_thm * lower_bound_thm; 79type upper_bound = expansion_thm * upper_bound_thm; 80datatype bounds = 81 Exact of expansion_thm | Bounds of lower_bound option * upper_bound option 82 83fun is_vacuous (Bounds (NONE, NONE)) = true 84 | is_vacuous _ = false 85 86fun mk_const_expansion ectxt basis c = 87 let 88 val ctxt = Lazy_Eval.get_ctxt ectxt 89 val thm = Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt c)] 90 @{thm expands_to_const} 91 in 92 thm OF [get_basis_wf_thm basis, mk_expansion_level_eq_thm basis] 93 end 94 95fun dest_eventually (Const (\<^const_name>\<open>Filter.eventually\<close>, _) $ p $ f) = (p, f) 96 | dest_eventually t = raise TERM ("dest_eventually", [t]) 97 98fun dest_binop (f $ a $ b) = (f, a, b) 99 | dest_binop t = raise TERM ("dest_binop", [t]) 100 101fun get_lbound_from_thm thm = 102 thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_eventually |> fst 103 |> strip_abs |> snd |> dest_binop |> #2 104 105fun get_ubound_from_thm thm = 106 thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_eventually |> fst 107 |> strip_abs |> snd |> dest_binop |> #3 108 109fun transfer_bounds eq_thm (Exact thm) = 110 Exact (@{thm expands_to_meta_eq_cong'} OF [thm, eq_thm]) 111 | transfer_bounds eq_thm (Bounds (lb, ub)) = 112 Bounds 113 (Option.map (apsnd (fn thm => @{thm transfer_lower_bound} OF [thm, eq_thm])) lb, 114 Option.map (apsnd (fn thm => @{thm transfer_upper_bound} OF [thm, eq_thm])) ub) 115 116fun dest_le (\<^term>\<open>(<=) :: real => _\<close> $ l $ r) = (l, r) 117 | dest_le t = raise TERM ("dest_le", [t]) 118 119fun abconv (t, t') = Envir.beta_eta_contract t aconv Envir.beta_eta_contract t' 120 121val realT = \<^typ>\<open>Real.real\<close> 122 123fun check_bounds e (Exact thm) = let val _ = check_expansion e thm in Exact thm end 124 | check_bounds e (Bounds bnds) = 125 let 126 fun msg lower = if lower then "check_lower_bound" else "check_upper_bound" 127 fun check lower (exp_thm, le_thm) = 128 let 129 val (expanded_fun, bound_fun) = 130 le_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_eventually |> fst 131 |> strip_abs |> snd |> dest_le |> (if lower then swap else I) 132 |> apply2 (fn t => Abs ("x", realT, t)) 133 in 134 if not (abconv (get_expanded_fun exp_thm, bound_fun)) then 135 raise TERM (msg lower, map Thm.concl_of [exp_thm, le_thm]) 136 else if not (abconv (expr_to_term e, expanded_fun)) then 137 raise TERM (msg lower, [expr_to_term e, Thm.concl_of le_thm]) 138 else 139 () 140 end 141 val _ = (Option.map (check true) (fst bnds), Option.map (check false) (snd bnds)) 142 in 143 Bounds bnds 144 end 145 146fun cong_bounds eq_thm (Exact thm) = 147 Exact (@{thm expands_to_cong_reverse} OF [eq_thm, thm]) 148 | cong_bounds eq_thm (Bounds (lb, ub)) = 149 Bounds 150 (Option.map (apsnd (fn thm => @{thm lower_bound_cong} OF [eq_thm, thm])) lb, 151 Option.map (apsnd (fn thm => @{thm upper_bound_cong} OF [eq_thm, thm])) ub) 152 153fun mk_trivial_bounds ectxt f thm basis = 154 let 155 val eq_thm = Thm.reflexive (Thm.cterm_of (Lazy_Eval.get_ctxt ectxt) f) 156 val lb_thm = @{thm trivial_boundsI(1)} OF [thm, eq_thm] 157 val ub_thm = @{thm trivial_boundsI(2)} OF [thm, eq_thm] 158 val lb = get_lbound_from_thm lb_thm 159 val ub = get_ubound_from_thm ub_thm 160 val (lthm, uthm) = apply2 (mk_const_expansion ectxt basis) (lb, ub) 161 in 162 Bounds (SOME (lthm, lb_thm), SOME (uthm, ub_thm)) 163 end 164 165fun get_basis_size basis = length (get_basis_list basis) 166 167fun trim_expansion_while_pos ectxt (thm, basis) = 168 let 169 val n = get_basis_size basis 170 val es = SOME (replicate n \<^term>\<open>0 :: real\<close>) 171 in 172 trim_expansion_while_greater false es false NONE ectxt (thm, basis) 173 end 174 175fun lift_bounds basis (Exact thm) = Exact (lift basis thm) 176 | lift_bounds basis (Bounds bnds) = 177 bnds |> apply2 (Option.map (apfst (lift basis))) |> Bounds 178 179fun mono_bound mono_thm thm = @{thm mono_bound} OF [mono_thm, thm] 180 181fun get_lower_bound (Bounds (lb, _)) = lb 182 | get_lower_bound (Exact thm) = SOME (thm, thm RS @{thm exact_to_bound}) 183 184fun get_upper_bound (Bounds (_, ub)) = ub 185 | get_upper_bound (Exact thm) = SOME (thm, thm RS @{thm exact_to_bound}) 186 187fun get_expanded_fun_bounds_aux f (_, thm) = 188 let 189 val t = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |> dest_comb |> snd 190 in 191 case Envir.eta_long [] t of 192 Abs (x, T, \<^term>\<open>(<=) :: real => _\<close> $ lhs $ rhs) => Abs (x, T, f (lhs, rhs)) 193 | _ => raise THM ("get_expanded_fun_bounds", 0, [thm]) 194 end 195 196fun get_expanded_fun_bounds (Exact thm) = get_expanded_fun thm 197 | get_expanded_fun_bounds (Bounds (NONE, NONE)) = raise TERM ("get_expanded_fun_bounds", []) 198 | get_expanded_fun_bounds (Bounds (SOME l, _)) = 199 get_expanded_fun_bounds_aux snd l 200 | get_expanded_fun_bounds (Bounds (_, SOME u)) = 201 get_expanded_fun_bounds_aux fst u 202 203fun expand_add_bounds _ [thm, _] (Exact thm1, Exact thm2) basis = 204 Exact (thm OF [get_basis_wf_thm basis, thm1, thm2]) 205 | expand_add_bounds swap [thm1, thm2] bnds basis = 206 let 207 fun comb (SOME (a, b), SOME (c, d)) = 208 SOME (thm1 OF [get_basis_wf_thm basis, a, c], thm2 OF [b, d]) 209 | comb _ = NONE 210 val ((a, b), (c, d)) = (apply2 get_lower_bound bnds, apply2 get_upper_bound bnds) 211 in 212 if swap then 213 Bounds (comb (a, d), comb (c, b)) 214 else 215 Bounds (comb (a, b), comb (c, d)) 216 end 217 | expand_add_bounds _ _ _ _ = raise Match 218 219fun mk_refl_thm ectxt t = 220 let 221 val ctxt = Lazy_Eval.get_ctxt ectxt 222 val ct = Thm.cterm_of ctxt t 223 in 224 Drule.infer_instantiate' ctxt [SOME ct] @{thm eventually_le_self} 225 end 226 227 228fun find_smaller_expansion ectxt (thm1, thm2, basis) = 229 case compare_expansions ectxt (thm1, thm2, basis) of 230 (LESS, less_thm, thm1, _) => 231 (thm1, mk_refl_thm ectxt (get_expanded_fun thm1), less_thm RS @{thm eventually_less_imp_le}) 232 | (GREATER, gt_thm, _, thm2) => 233 (thm2, gt_thm RS @{thm eventually_less_imp_le}, mk_refl_thm ectxt (get_expanded_fun thm2)) 234 | (EQUAL, eq_thm, thm1, _) => 235 (thm1, mk_refl_thm ectxt (get_expanded_fun thm1), eq_thm RS @{thm eventually_eq_imp_le}) 236 237fun find_greater_expansion ectxt (thm1, thm2, basis) = 238 case compare_expansions ectxt (\<^print> (thm1, thm2, basis)) of 239 (LESS, less_thm, _, thm2) => 240 (thm2, less_thm RS @{thm eventually_less_imp_le}, mk_refl_thm ectxt (get_expanded_fun thm2)) 241 | (GREATER, gt_thm, thm1, _) => 242 (thm1, mk_refl_thm ectxt (get_expanded_fun thm1), gt_thm RS @{thm eventually_less_imp_le}) 243 | (EQUAL, eq_thm, thm1, _) => 244 (thm1, mk_refl_thm ectxt (get_expanded_fun thm1), eq_thm RS @{thm eventually_eq_imp_ge}) 245 246fun determine_sign ectxt (thm, basis) = 247 case ev_zeroness_oracle ectxt (get_expanded_fun thm) of 248 SOME zero_thm => (thm, zero_thm, (true, true)) 249 | NONE => ( 250 case trim_expansion true (SOME Sgn_Trim) ectxt (thm, basis) of 251 (thm, IsPos, SOME pos_thm) => 252 (thm, @{thm expands_to_imp_eventually_pos} OF [get_basis_wf_thm basis, thm, pos_thm], 253 (false, true)) 254 | (thm, IsNeg, SOME neg_thm) => 255 (thm, @{thm expands_to_imp_eventually_neg} OF [get_basis_wf_thm basis, thm, neg_thm], 256 (true, false)) 257 | _ => raise TERM ("Unexpected zeroness result in determine_sign", [])) 258 259val mult_bounds_thms = @{thms mult_bounds_real[eventuallized]} 260fun mult_bounds_thm n = List.nth (mult_bounds_thms, n) 261 262val powr_bounds_thms = @{thms powr_bounds_real[eventuallized]} 263fun powr_bounds_thm n = List.nth (powr_bounds_thms, n) 264 265fun mk_nonstrict_thm [thm1, thm2] sgn_thm = ( 266 case Thm.concl_of sgn_thm |> HOLogic.dest_Trueprop of 267 Const (\<^const_name>\<open>Filter.eventually\<close>, _) $ t $ _ => ( 268 case Envir.eta_long [] t of 269 Abs (_, _, Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => sgn_thm RS thm1 270 | _ => sgn_thm RS thm2) 271 | _ => sgn_thm RS thm2) 272 | mk_nonstrict_thm _ _ = raise Match 273 274 275val mk_nonneg_thm = mk_nonstrict_thm @{thms eventually_eq_imp_ge eventually_less_imp_le} 276val mk_nonpos_thm = mk_nonstrict_thm @{thms eventually_eq_imp_le eventually_less_imp_le} 277 278fun mult_expansion_bounds_right basis 279 ((l1_thm, l1_le_thm), (u1_thm, u1_ge_thm)) (thm2, sgn_thm, sgns) = 280 let 281 val in_bounds_thm = @{thm eventually_atLeastAtMostI} OF [l1_le_thm, u1_ge_thm] 282 fun mult_expansions (thm1, thm2) = 283 @{thm expands_to_mult} OF [get_basis_wf_thm basis, thm1, thm2] 284 in 285 if snd sgns then 286 (mult_expansions (l1_thm, thm2), mult_expansions (u1_thm, thm2), 287 @{thm mult_right_bounds(1)[eventuallized]} OF [in_bounds_thm, mk_nonneg_thm sgn_thm]) 288 else 289 (mult_expansions (u1_thm, thm2), mult_expansions (l1_thm, thm2), 290 @{thm mult_right_bounds(2)[eventuallized]} OF [in_bounds_thm, mk_nonpos_thm sgn_thm]) 291 end 292 293fun mult_expansion_bounds_left basis 294 (thm1, sgn_thm, sgns) ((l2_thm, l2_le_thm), (u2_thm, u2_ge_thm)) = 295 let 296 val in_bounds_thm = @{thm eventually_atLeastAtMostI} OF [l2_le_thm, u2_ge_thm] 297 fun mult_expansions (thm1, thm2) = 298 @{thm expands_to_mult} OF [get_basis_wf_thm basis, thm1, thm2] 299 in 300 if snd sgns then 301 (mult_expansions (thm1, l2_thm), mult_expansions (thm1, u2_thm), 302 @{thm mult_left_bounds(1)[eventuallized]} OF [in_bounds_thm, mk_nonneg_thm sgn_thm]) 303 else 304 (mult_expansions (thm1, u2_thm), mult_expansions (thm1, l2_thm), 305 @{thm mult_left_bounds(2)[eventuallized]} OF [in_bounds_thm, mk_nonpos_thm sgn_thm]) 306 end 307 308fun mult_expansion_bounds_2 ectxt basis 309 ((l1, l1_le_thm, l1sgn_thm, l1_sgn), (u1, u1_ge_thm, u1sgn_thm, u1_sgn)) 310 ((l2, l2_le_thm, l2sgn_thm, l2_sgn), (u2, u2_ge_thm, u2sgn_thm, u2_sgn)) = 311 let 312 val sgns = (l1_sgn, u1_sgn, l2_sgn, u2_sgn) 313 val in_bounds_thms = 314 map (fn thms => @{thm eventually_atLeastAtMostI} OF thms) 315 [[l1_le_thm, u1_ge_thm], [l2_le_thm, u2_ge_thm]] 316 fun mult_expansions (thm1, thm2) = 317 @{thm expands_to_mult} OF [get_basis_wf_thm basis, thm1, thm2] 318 in 319 case sgns of 320 ((_, true), _, (_, true), _) => 321 (mult_expansions (l1, l2), mult_expansions (u1, u2), 322 mult_bounds_thm 0 OF ([mk_nonneg_thm l1sgn_thm, mk_nonneg_thm l2sgn_thm] @ in_bounds_thms)) 323 | (_, (true, _), (_, true), _) => 324 (mult_expansions (l1, u2), mult_expansions (u1, l2), 325 mult_bounds_thm 1 OF ([mk_nonpos_thm u1sgn_thm, mk_nonneg_thm l2sgn_thm] @ in_bounds_thms)) 326 | ((_, true), _, _, (true, _)) => 327 (mult_expansions (u1, l2), mult_expansions (l1, u2), 328 mult_bounds_thm 2 OF ([mk_nonneg_thm l1sgn_thm, mk_nonpos_thm u2sgn_thm] @ in_bounds_thms)) 329 | (_, (true, _), _, (true, _)) => 330 (mult_expansions (u1, u2), mult_expansions (l1, l2), 331 mult_bounds_thm 3 OF ([mk_nonpos_thm u1sgn_thm, mk_nonpos_thm u2sgn_thm] @ in_bounds_thms)) 332 | ((true, _), (_, true), (_, true), _) => 333 (mult_expansions (l1, u2), mult_expansions (u1, u2), 334 mult_bounds_thm 4 OF ([mk_nonpos_thm l1sgn_thm, mk_nonneg_thm u1sgn_thm, mk_nonneg_thm l2sgn_thm] @ in_bounds_thms)) 335 | ((true, _), (_, true), _, (true, _)) => 336 (mult_expansions (u1, l2), mult_expansions (l1, l2), 337 mult_bounds_thm 5 OF ([mk_nonpos_thm l1sgn_thm, mk_nonneg_thm u1sgn_thm, mk_nonpos_thm u2sgn_thm] @ in_bounds_thms)) 338 | ((_, true), _, (true, _), (_, true)) => 339 (mult_expansions (u1, l2), mult_expansions (u1, u2), 340 mult_bounds_thm 6 OF ([mk_nonneg_thm l1sgn_thm, mk_nonpos_thm l2sgn_thm, mk_nonneg_thm u2sgn_thm] @ in_bounds_thms)) 341 | (_, (true, _), (true, _), (_, true)) => 342 (mult_expansions (l1, u2), mult_expansions (l1, l2), 343 mult_bounds_thm 7 OF ([mk_nonpos_thm u1sgn_thm, mk_nonpos_thm l2sgn_thm, mk_nonneg_thm u2sgn_thm] @ in_bounds_thms)) 344 | ((true, _), (_, true), (true, _), (_, true)) => 345 let 346 val l1u2 = mult_expansions (l1, u2) 347 val u1l2 = mult_expansions (u1, l2) 348 val l1l2 = mult_expansions (l1, l2) 349 val u1u2 = mult_expansions (u1, u2) 350 val (l, lthm1, lthm2) = find_smaller_expansion ectxt (l1u2, u1l2, basis) 351 val (u, uthm1, uthm2) = find_greater_expansion ectxt (l1l2, u1u2, basis) 352 in 353 (l, u, mult_bounds_thm 8 OF 354 ([mk_nonpos_thm l1sgn_thm, mk_nonneg_thm u1sgn_thm, mk_nonpos_thm l2sgn_thm, 355 mk_nonneg_thm u2sgn_thm, lthm1, lthm2, uthm1, uthm2] @ in_bounds_thms)) 356 end 357 358 | _ => raise Match 359 end 360 361fun convert_bounds (lthm, uthm, in_bounds_thm) = 362 Bounds (SOME (lthm, in_bounds_thm RS @{thm eventually_atLeastAtMostD(1)}), 363 SOME (uthm, in_bounds_thm RS @{thm eventually_atLeastAtMostD(2)})) 364 365fun convert_bounds' (Exact thm) = (thm, thm, thm RS @{thm expands_to_trivial_bounds}) 366 | convert_bounds' (Bounds (SOME (lthm, ge_thm), SOME (uthm, le_thm))) = 367 (lthm, uthm, @{thm eventually_in_atLeastAtMostI} OF [ge_thm, le_thm]) 368 369fun mult_expansion_bounds _ basis (Exact thm1) (Exact thm2) = 370 Exact (@{thm expands_to_mult} OF [get_basis_wf_thm basis, thm1, thm2]) 371 | mult_expansion_bounds ectxt basis (Bounds (SOME l1, SOME u1)) (Exact thm2) = 372 mult_expansion_bounds_right basis (l1, u1) (determine_sign ectxt (thm2, basis)) 373 |> convert_bounds 374 | mult_expansion_bounds ectxt basis (Exact thm1) (Bounds (SOME l2, SOME u2)) = 375 mult_expansion_bounds_left basis (determine_sign ectxt (thm1, basis)) (l2, u2) 376 |> convert_bounds 377 | mult_expansion_bounds ectxt basis (Bounds (SOME l1, SOME u1)) (Bounds (SOME l2, SOME u2)) = 378 let 379 fun prep (thm, le_thm) = 380 case determine_sign ectxt (thm, basis) of 381 (thm, sgn_thm, sgns) => (thm, le_thm, sgn_thm, sgns) 382 in 383 mult_expansion_bounds_2 ectxt basis (prep l1, prep u1) (prep l2, prep u2) 384 |> convert_bounds 385 end 386 | mult_expansion_bounds _ _ _ _ = Bounds (NONE, NONE) 387 388fun inverse_expansion ectxt basis thm = 389 case trim_expansion true (SOME Simple_Trim) ectxt (thm, basis) of 390 (thm, _, SOME trimmed_thm) => 391 @{thm expands_to_inverse} OF [trimmed_thm, get_basis_wf_thm basis, thm] 392 | _ => raise TERM ("zero denominator", [get_expanded_fun thm]) 393 394fun divide_expansion ectxt basis thm1 thm2 = 395 case trim_expansion true (SOME Simple_Trim) ectxt (thm2, basis) of 396 (thm2, _, SOME trimmed_thm) => 397 @{thm expands_to_divide} OF [trimmed_thm, get_basis_wf_thm basis, thm1, thm2] 398 399fun forget_trimmedness_sign trimmed_thm = 400 case Thm.concl_of trimmed_thm |> HOLogic.dest_Trueprop of 401 Const (\<^const_name>\<open>Multiseries_Expansion.trimmed\<close>, _) $ _ => trimmed_thm 402 | Const (\<^const_name>\<open>Multiseries_Expansion.trimmed_pos\<close>, _) $ _ => 403 trimmed_thm RS @{thm trimmed_pos_imp_trimmed} 404 | Const (\<^const_name>\<open>Multiseries_Expansion.trimmed_neg\<close>, _) $ _ => 405 trimmed_thm RS @{thm trimmed_neg_imp_trimmed} 406 | _ => raise THM ("forget_trimmedness_sign", 0, [trimmed_thm]) 407 408fun inverse_expansion_bounds ectxt basis (Exact thm) = 409 Exact (inverse_expansion ectxt basis thm) 410 | inverse_expansion_bounds ectxt basis (Bounds (SOME (lthm, le_thm), SOME (uthm, ge_thm))) = 411 let 412 fun trim thm = trim_expansion true (SOME Sgn_Trim) ectxt (thm, basis) 413 fun inverse thm trimmed_thm = @{thm expands_to_inverse} OF 414 [forget_trimmedness_sign trimmed_thm, get_basis_wf_thm basis, thm] 415 in 416 case (trim lthm, trim uthm) of 417 ((lthm, IsPos, SOME trimmed_thm1), (uthm, _, SOME trimmed_thm2)) => 418 (inverse uthm trimmed_thm2, inverse lthm trimmed_thm1, 419 @{thm inverse_bounds_real(1)[eventuallized, OF expands_to_imp_eventually_pos]} OF 420 [get_basis_wf_thm basis, lthm, trimmed_thm1, le_thm, ge_thm]) |> convert_bounds 421 | ((lthm, _, SOME trimmed_thm1), (uthm, IsNeg, SOME trimmed_thm2)) => 422 (inverse uthm trimmed_thm2, inverse lthm trimmed_thm1, 423 @{thm inverse_bounds_real(2)[eventuallized, OF expands_to_imp_eventually_neg]} OF 424 [get_basis_wf_thm basis, uthm, trimmed_thm2, le_thm, ge_thm]) |> convert_bounds 425 | _ => raise TERM ("zero denominator", map get_expanded_fun [lthm, uthm]) 426 end 427 | inverse_expansion_bounds _ _ _ = Bounds (NONE, NONE) 428 429fun trimmed_thm_to_inverse_sgn_thm basis thm trimmed_thm = 430 case trimmed_thm |> Thm.concl_of |> HOLogic.dest_Trueprop of 431 Const (\<^const_name>\<open>Multiseries_Expansion.trimmed_pos\<close>, _) $ _ => 432 @{thm pos_imp_inverse_pos[eventuallized, OF expands_to_imp_eventually_pos]} OF 433 [get_basis_wf_thm basis, thm, trimmed_thm] 434 | Const (\<^const_name>\<open>Multiseries_Expansion.trimmed_neg\<close>, _) $ _ => 435 @{thm neg_imp_inverse_neg[eventuallized, OF expands_to_imp_eventually_neg]} OF 436 [get_basis_wf_thm basis, thm, trimmed_thm] 437 | _ => raise THM ("trimmed_thm_to_inverse_sgn_thm", 0, [trimmed_thm]) 438 439fun transfer_divide_bounds (lthm, uthm, in_bounds_thm) = 440 let 441 val f = Conv.fconv_rule (Conv.try_conv (Conv.rewr_conv @{thm transfer_divide_bounds(4)})) 442 val conv = Conv.repeat_conv (Conv.rewrs_conv @{thms transfer_divide_bounds(1-3)}) 443 in 444 (f lthm, f uthm, Conv.fconv_rule conv in_bounds_thm) 445 end 446 447fun divide_expansion_bounds ectxt basis (Exact thm1) (Exact thm2) = 448 Exact (divide_expansion ectxt basis thm1 thm2) 449 | divide_expansion_bounds ectxt basis (Bounds (SOME l1, SOME u1)) (Exact thm2) = 450 let 451 val (thm2, sgn, SOME trimmed_thm) = trim_expansion true (SOME Sgn_Trim) ectxt (thm2, basis) 452 val thm2' = @{thm expands_to_inverse} OF 453 [forget_trimmedness_sign trimmed_thm, get_basis_wf_thm basis, thm2] 454 val sgn_thm = trimmed_thm_to_inverse_sgn_thm basis thm2 trimmed_thm 455 in 456 mult_expansion_bounds_right basis (l1, u1) (thm2', sgn_thm, (sgn = IsNeg, sgn = IsPos)) 457 |> transfer_divide_bounds 458 |> convert_bounds 459 end 460 | divide_expansion_bounds ectxt basis bnds1 (Bounds (SOME (lthm, ge_thm), SOME (uthm, le_thm))) = 461 let 462 fun trim thm = 463 case trim_expansion true (SOME Sgn_Trim) ectxt (thm, basis) of 464 (thm, sgn, SOME trimmed_thm) => (thm, sgn, trimmed_thm) 465 | _ => raise TERM ("zero divisor", [get_expanded_fun thm]) 466 fun inverse thm trimmed_thm = @{thm expands_to_inverse} OF 467 [forget_trimmedness_sign trimmed_thm, get_basis_wf_thm basis, thm] 468 469 val (lthm, sgnl, ltrimmed_thm) = trim lthm 470 val (uthm, sgnu, utrimmed_thm) = trim uthm 471 val (uthm', lthm') = (inverse lthm ltrimmed_thm, inverse uthm utrimmed_thm) 472 val in_bounds_thm' = 473 if sgnl = IsPos then 474 @{thm inverse_bounds_real(1)[eventuallized, OF expands_to_imp_eventually_pos]} OF 475 [get_basis_wf_thm basis, lthm, ltrimmed_thm, ge_thm, le_thm] 476 else if sgnu = IsNeg then 477 @{thm inverse_bounds_real(2)[eventuallized, OF expands_to_imp_eventually_neg]} OF 478 [get_basis_wf_thm basis, uthm, utrimmed_thm, ge_thm, le_thm] 479 else 480 raise TERM ("zero divisor", map get_expanded_fun [lthm, uthm]) 481 val [ge_thm', le_thm'] = 482 map (fn thm => in_bounds_thm' RS thm) @{thms eventually_atLeastAtMostD} 483 val bnds2' = ((lthm', ge_thm'), (uthm', le_thm')) 484 val usgn_thm' = trimmed_thm_to_inverse_sgn_thm basis lthm ltrimmed_thm 485 val lsgn_thm' = trimmed_thm_to_inverse_sgn_thm basis uthm utrimmed_thm 486 in 487 case bnds1 of 488 Exact thm1 => 489 (mult_expansion_bounds_left basis (determine_sign ectxt (thm1, basis)) bnds2') 490 |> transfer_divide_bounds 491 |> convert_bounds 492 | Bounds (SOME l1, SOME u1) => 493 let 494 fun prep (thm, le_thm) = 495 case determine_sign ectxt (thm, basis) of 496 (thm, sgn_thm, sgns) => (thm, le_thm, sgn_thm, sgns) 497 in 498 mult_expansion_bounds_2 ectxt basis (prep l1, prep u1) 499 ((lthm', ge_thm', lsgn_thm', (sgnl = IsNeg, sgnl = IsPos)), 500 (uthm', le_thm', usgn_thm', (sgnu = IsNeg, sgnu = IsPos))) 501 |> transfer_divide_bounds 502 |> convert_bounds 503 end 504 | _ => Bounds (NONE, NONE) 505 end 506 | divide_expansion_bounds _ _ _ _ = Bounds (NONE, NONE) 507 508fun abs_expansion ectxt basis thm = 509 let 510 val (thm, nz, SOME trimmed_thm) = trim_expansion true (SOME Sgn_Trim) ectxt (thm, basis) 511 val thm' = 512 case nz of 513 IsPos => @{thm expands_to_abs_pos} 514 | IsNeg => @{thm expands_to_abs_neg} 515 | _ => raise TERM ("Unexpected trim result during expansion of abs", []) 516 in 517 thm' OF [trimmed_thm, get_basis_wf_thm basis, thm] 518 end 519 520fun abs_trivial_bounds ectxt f = 521 let 522 val ctxt = Lazy_Eval.get_ctxt ectxt 523 in 524 Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt f)] @{thm eventually_abs_ge_0} 525 end 526 527fun abs_expansion_bounds ectxt basis (Exact thm) = Exact (abs_expansion ectxt basis thm) 528 | abs_expansion_bounds ectxt basis (bnds as Bounds (SOME (lthm, ge_thm), NONE)) = 529 let 530 val (lthm, lsgn_thm, lsgns) = determine_sign ectxt (lthm, basis) 531 val lbnd = 532 if snd lsgns then 533 (lthm, @{thm eventually_le_abs_nonneg} OF [mk_nonneg_thm lsgn_thm, ge_thm]) 534 else 535 (zero_expansion basis, abs_trivial_bounds ectxt (get_expanded_fun_bounds bnds)) 536 in 537 Bounds (SOME lbnd, NONE) 538 end 539 | abs_expansion_bounds ectxt basis (bnds as Bounds (NONE, SOME (uthm, le_thm))) = 540 let 541 val (uthm, usgn_thm, usgns) = determine_sign ectxt (uthm, basis) 542 val lbnd = 543 if fst usgns then 544 (@{thm expands_to_uminus} OF [get_basis_wf_thm basis, uthm], 545 @{thm eventually_le_abs_nonpos} OF [mk_nonpos_thm usgn_thm, le_thm]) 546 else 547 (zero_expansion basis, abs_trivial_bounds ectxt (get_expanded_fun_bounds bnds)) 548 in 549 Bounds (SOME lbnd, NONE) 550 end 551 | abs_expansion_bounds ectxt basis (Bounds (SOME (lthm, ge_thm), SOME (uthm, le_thm))) = 552 let 553 val in_bounds_thm = @{thm eventually_atLeastAtMostI} OF [ge_thm, le_thm] 554 val (lthm, lsgn_thm, lsgns) = determine_sign ectxt (lthm, basis) 555 val (uthm, usgn_thm, usgns) = determine_sign ectxt (uthm, basis) 556 fun minus thm = @{thm expands_to_uminus} OF [get_basis_wf_thm basis, thm] 557 in ( 558 case (lsgns, usgns) of 559 ((_, true), _) => 560 (lthm, uthm, 561 @{thm nonneg_abs_bounds[eventuallized]} OF [mk_nonneg_thm lsgn_thm, in_bounds_thm]) 562 | (_, (true, _)) => 563 (minus uthm, minus lthm, 564 @{thm nonpos_abs_bounds[eventuallized]} OF [mk_nonpos_thm usgn_thm, in_bounds_thm]) 565 | ((true, _), (_, true)) => ( 566 case find_greater_expansion ectxt (minus lthm, uthm, basis) of 567 (u'_thm, le_thm1, le_thm2) => 568 (mk_const_expansion ectxt basis \<^term>\<open>0::real\<close>, u'_thm, 569 @{thm indet_abs_bounds[eventuallized]} OF 570 [mk_nonpos_thm lsgn_thm, mk_nonneg_thm usgn_thm, 571 in_bounds_thm, le_thm1, le_thm2])) 572 | _ => raise TERM ("Unexpected zeroness result in abs_expansion_bounds", [])) 573 |> convert_bounds 574 end 575 | abs_expansion_bounds _ _ _ = Bounds (NONE, NONE) (* TODO *) 576 577fun abs_expansion_lower_bound ectxt basis (Exact thm) = 578 let 579 val thm' = abs_expansion ectxt basis thm 580 in 581 (thm', thm RS @{thm expands_to_abs_nonneg}, thm' RS @{thm exact_to_bound}) 582 end 583 | abs_expansion_lower_bound ectxt basis (Bounds (SOME (lthm, ge_thm), SOME (uthm, le_thm))) = 584 let 585 val in_bounds_thm = @{thm eventually_atLeastAtMostI} OF [ge_thm, le_thm] 586 val (lthm, lsgn_thm, lsgns) = determine_sign ectxt (lthm, basis) 587 val (uthm, usgn_thm, usgns) = determine_sign ectxt (uthm, basis) 588 fun minus thm = @{thm expands_to_uminus} OF [get_basis_wf_thm basis, thm] 589 val [absthm1, absthm2] = 590 @{thms eventually_atLeastAtMostD(1)[OF nonneg_abs_bounds[eventuallized]] 591 eventually_atLeastAtMostD(1)[OF nonpos_abs_bounds[eventuallized]]} 592 in ( 593 case (lsgns, usgns) of 594 ((_, true), _) => 595 (lthm, mk_nonneg_thm lsgn_thm, 596 absthm1 OF [mk_nonneg_thm lsgn_thm, in_bounds_thm]) 597 | (_, (true, _)) => 598 (minus uthm, mk_nonpos_thm usgn_thm RS @{thm eventually_nonpos_flip}, 599 absthm2 OF [mk_nonpos_thm usgn_thm, in_bounds_thm]) 600 | ((true, _), (_, true)) => raise TERM ("abs_expansion_lower_bound", []) 601 | _ => raise TERM ("Unexpected zeroness result in abs_expansion_bounds", [])) 602 end 603 | abs_expansion_lower_bound _ _ _ = raise TERM ("abs_expansion_lower_bound", []) 604 605fun powr_expansion_bounds_right ectxt basis 606 ((l1_thm, l1_le_thm), (u1_thm, u1_ge_thm)) (thm2, sgn_thm, g_sgns) = 607 let 608 val in_bounds_thm = @{thm eventually_atLeastAtMostI} OF [l1_le_thm, u1_ge_thm] 609 val (l1_thm, l1_sgn_thm, l1_sgns) = determine_sign ectxt (l1_thm, basis) 610 val l1_sgn_thm = if snd g_sgns then mk_nonneg_thm l1_sgn_thm else l1_sgn_thm 611 val (l_thm, basis') = powr_expansion ectxt (l1_thm, thm2, basis) 612 val (u_thm, basis'') = powr_expansion ectxt (lift basis' u1_thm, lift basis' thm2, basis') 613 val l_thm = lift basis'' l_thm 614 in 615 if (snd g_sgns andalso not (snd l1_sgns)) orelse (not (snd g_sgns) andalso fst l1_sgns) then 616 raise TERM ("Non-positive base in powr.", []) 617 else if snd g_sgns then 618 ((l_thm, u_thm, @{thm powr_right_bounds(1)[eventuallized]} 619 OF [l1_sgn_thm, in_bounds_thm, mk_nonneg_thm sgn_thm]), basis'') 620 else 621 ((u_thm, l_thm, @{thm powr_right_bounds(2)[eventuallized]} 622 OF [l1_sgn_thm, in_bounds_thm, mk_nonpos_thm sgn_thm]), basis'') 623 end 624 625fun compare_expansion_to_1 ectxt (thm, basis) = 626 prove_asymptotic_relation ectxt (thm, const_expansion ectxt basis \<^term>\<open>1 :: real\<close>, basis) 627 628fun powr_expansion_bounds_left ectxt basis 629 thm1 ((l2_thm, l2_le_thm), (u2_thm, u2_ge_thm)) = 630 let 631 val in_bounds_thm = @{thm eventually_atLeastAtMostI} OF [l2_le_thm, u2_ge_thm] 632 val (thm1, _, SOME trimmed_pos_thm) = trim_expansion true (SOME Pos_Trim) ectxt (thm1, basis) 633 val pos_thm = @{thm expands_to_imp_eventually_pos} OF 634 [get_basis_wf_thm basis, thm1, trimmed_pos_thm] 635 val (l_thm, basis') = powr_expansion ectxt (thm1, l2_thm, basis) 636 val (u_thm, basis'') = powr_expansion ectxt (lift basis' thm1, lift basis' u2_thm, basis') 637 val l_thm = lift basis'' l_thm 638 val (cmp_1, cmp_1_thm) = compare_expansion_to_1 ectxt (thm1, basis) 639 in 640 case cmp_1 of 641 LESS => 642 ((u_thm, l_thm, @{thm powr_left_bounds(2)[eventuallized]} OF 643 [pos_thm, in_bounds_thm, mk_nonpos_thm cmp_1_thm]), basis'') 644 | _ => 645 ((l_thm, u_thm, @{thm powr_left_bounds(1)[eventuallized]} OF 646 [pos_thm, in_bounds_thm, mk_nonneg_thm cmp_1_thm]), basis'') 647 end 648 649fun powr_expansion_bounds_2 ectxt basis 650 ((l1, l1_le_thm, l1pos_thm, l1_sgn), (u1, u1_ge_thm, _, _)) 651 ((l2, l2_le_thm, l2sgn_thm, l2_sgn), (u2, u2_ge_thm, u2sgn_thm, u2_sgn)) = 652 let 653 fun do_force_pos () = 654 if fst l1_sgn then raise TERM ("Non-positive base in power", []) else () 655 656 fun compare_expansion_to_1' thm = 657 let 658 val (cmp, sgn_thm) = compare_expansion_to_1 ectxt (thm, basis) 659 val sgn = (cmp <> GREATER, cmp <> LESS) 660 in 661 (sgn, sgn_thm) 662 end 663 val (l1_sgn, l1sgn_thm) = compare_expansion_to_1' l1 664 val (u1_sgn, u1sgn_thm) = compare_expansion_to_1' u1 665 666 val sgns = (l1_sgn, u1_sgn, l2_sgn, u2_sgn) 667 val in_bounds_thms = 668 map (fn thms => @{thm eventually_atLeastAtMostI} OF thms) 669 [[l1_le_thm, u1_ge_thm], [l2_le_thm, u2_ge_thm]] 670 fun f n force_pos (a, b) (c, d) thms = 671 let 672 val _ = if force_pos then do_force_pos () else () 673 val l1pos_thm = if force_pos then l1pos_thm else mk_nonneg_thm l1pos_thm 674 val (thm1, basis1) = powr_expansion ectxt (a, b, basis) 675 val (thm2, basis2) = powr_expansion ectxt (lift basis1 c, lift basis1 d, basis1) 676 val thm1 = lift basis2 thm1 677 in 678 ((thm1, thm2, powr_bounds_thm n OF (l1pos_thm :: thms @ in_bounds_thms)), basis2) 679 end 680 in 681 case sgns of 682 ((_, true), _, (_, true), _) => 683 f 0 false (l1, l2) (u1, u2) [mk_nonneg_thm l1sgn_thm, mk_nonneg_thm l2sgn_thm] 684 | (_, (true, _), (_, true), _) => 685 f 1 false (l1, u2) (u1, l2) [mk_nonpos_thm u1sgn_thm, mk_nonneg_thm l2sgn_thm] 686 | ((_, true), _, _, (true, _)) => 687 f 2 false (u1, l2) (l1, u2) [mk_nonneg_thm l1sgn_thm, mk_nonpos_thm u2sgn_thm] 688 | (_, (true, _), _, (true, _)) => 689 f 3 true (u1, u2) (l1, l2) [mk_nonpos_thm u1sgn_thm, mk_nonpos_thm u2sgn_thm] 690 | ((true, _), (_, true), (_, true), _) => 691 f 4 false (l1, u2) (u1, u2) 692 [mk_nonpos_thm l1sgn_thm, mk_nonneg_thm u1sgn_thm, mk_nonneg_thm l2sgn_thm] 693 | ((true, _), (_, true), _, (true, _)) => 694 f 5 true (u1, l2) (l1, l2) 695 [mk_nonpos_thm l1sgn_thm, mk_nonneg_thm u1sgn_thm, mk_nonpos_thm u2sgn_thm] 696 | ((_, true), _, (true, _), (_, true)) => 697 f 6 false (u1, l2) (u1, u2) 698 [mk_nonneg_thm l1sgn_thm, mk_nonpos_thm l2sgn_thm, mk_nonneg_thm u2sgn_thm] 699 | (_, (true, _), (true, _), (_, true)) => 700 f 7 true (l1, u2) (l1, l2) 701 [mk_nonpos_thm u1sgn_thm, mk_nonpos_thm l2sgn_thm, mk_nonneg_thm u2sgn_thm] 702 | ((true, _), (_, true), (true, _), (_, true)) => 703 let 704 val _ = do_force_pos () 705 val (l1u2, basis1) = powr_expansion ectxt (l1, u2, basis) 706 val (u1l2, basis2) = powr_expansion ectxt (lift basis1 u1, lift basis1 l2, basis1) 707 val (l1l2, basis3) = powr_expansion ectxt (lift basis2 l1, lift basis2 l2, basis2) 708 val (u1u2, basis4) = powr_expansion ectxt (lift basis3 u1, lift basis3 u2, basis3) 709 val [l1u2, u1l2, l1l2] = map (lift basis4) [l1u2, u1l2, l1l2] 710 (* TODO The bases might blow up unnecessarily a bit here *) 711 val (l, lthm1, lthm2) = find_smaller_expansion ectxt (l1u2, u1l2, basis4) 712 val (u, uthm1, uthm2) = find_greater_expansion ectxt (l1l2, u1u2, basis4) 713 in 714 ((l, u, powr_bounds_thm 8 OF 715 ([l1pos_thm, mk_nonpos_thm l1sgn_thm, mk_nonneg_thm u1sgn_thm, mk_nonpos_thm l2sgn_thm, 716 mk_nonneg_thm u2sgn_thm, lthm1, lthm2, uthm1, uthm2] @ in_bounds_thms)), basis4) 717 end 718 719 | _ => raise Match 720 end 721 722fun powr_expansion_bounds_aux ectxt basis (Exact thm1) (Exact thm2) = 723 powr_expansion ectxt (thm1, thm2, basis) |> apfst Exact 724 | powr_expansion_bounds_aux ectxt basis (Bounds (SOME l1, SOME u1)) (Exact thm2) = 725 powr_expansion_bounds_right ectxt basis (l1, u1) (determine_sign ectxt (thm2, basis)) 726 |> apfst convert_bounds 727 | powr_expansion_bounds_aux ectxt basis (Exact thm1) (Bounds (SOME l2, SOME u2)) = 728 powr_expansion_bounds_left ectxt basis thm1 (l2, u2) 729 |> apfst convert_bounds 730 | powr_expansion_bounds_aux ectxt basis (Bounds (SOME l1, SOME u1)) (Bounds (SOME l2, SOME u2)) = 731 let 732 fun prep (thm, le_thm) = 733 case determine_sign ectxt (thm, basis) of 734 (thm, sgn_thm, sgns) => (thm, le_thm, sgn_thm, sgns) 735 in 736 powr_expansion_bounds_2 ectxt basis (prep l1, prep u1) (prep l2, prep u2) 737 |> apfst convert_bounds 738 end 739 | powr_expansion_bounds_aux _ basis _ _ = (Bounds (NONE, NONE), basis) 740 741fun powr_expansion_bounds ectxt basis bnds1 bnds2 = 742 case ev_zeroness_oracle ectxt (get_expanded_fun_bounds bnds1) of 743 SOME zero_thm => 744 let 745 val t = Thm.cterm_of (Lazy_Eval.get_ctxt ectxt) (get_expanded_fun_bounds bnds2) 746 val thm = @{thm expands_to_powr_0} OF 747 [zero_thm, Thm.reflexive t, get_basis_wf_thm basis, mk_expansion_level_eq_thm basis] 748 in 749 (Exact thm, basis) 750 end 751 | NONE => powr_expansion_bounds_aux ectxt basis bnds1 bnds2 752 753val powr_nat_bounds_transfer_le = @{thms powr_nat_bounds_transfer_le[eventuallized]} 754fun powr_nat_bounds_transfer_le' n = List.nth (powr_nat_bounds_transfer_le, n - 1) 755 756fun powr_nat_expansion_bounds ectxt basis bnds1 bnds2 = 757 let 758 fun aux (Exact thm1) (Exact thm2) = 759 apfst Exact (powr_nat_expansion ectxt (thm1, thm2, basis)) 760 | aux bnds1 bnds2 = 761 case get_lower_bound bnds1 of 762 NONE => (Bounds (NONE, NONE), basis) 763 | SOME (lthm1, ge_thm1) => 764 let 765 val (lthm1, l1_sgn_thm, sgns1) = determine_sign ectxt (lthm1, basis) 766 val bnds1 = 767 case bnds1 of 768 Exact _ => Exact lthm1 769 | Bounds (SOME (_, ge_thm), upper) => Bounds (SOME (lthm1, ge_thm), upper) 770 | _ => raise Match 771 val _ = if not (snd sgns1) then 772 raise TERM ("Unexpected sign in powr_nat_expansion_bounds", []) else () 773 val (bnds, basis') = powr_expansion_bounds ectxt basis bnds1 bnds2 774 val lower = Option.map (apsnd (fn ge_thm' => 775 @{thm powr_nat_bounds_transfer_ge[eventuallized]} OF 776 [mk_nonneg_thm l1_sgn_thm, ge_thm1, ge_thm'])) (get_lower_bound bnds) 777 fun determine_sign' NONE = NONE 778 | determine_sign' (SOME (thm, le_thm)) = 779 case determine_sign ectxt (thm, basis) of 780 (thm, sgn_thm, sgns) => SOME (thm, sgn_thm, sgns, le_thm) 781 fun do_transfer n thms = powr_nat_bounds_transfer_le' n OF thms 782 fun transfer_upper (uthm', le_thm') = 783 if not (fst sgns1) then 784 (uthm', do_transfer 1 [l1_sgn_thm, ge_thm1, le_thm']) 785 else 786 case determine_sign' (get_lower_bound bnds2) of 787 SOME (_, l2_sgn_thm, (false, true), ge_thm2) => 788 (uthm', do_transfer 2 789 [mk_nonneg_thm l1_sgn_thm, l2_sgn_thm, ge_thm1, ge_thm2, le_thm']) 790 | _ => ( 791 case determine_sign' (get_upper_bound bnds2) of 792 SOME (_, u2_sgn_thm, (true, false), le_thm2) => 793 (uthm', do_transfer 3 794 [mk_nonneg_thm l1_sgn_thm, u2_sgn_thm, ge_thm1, le_thm2, le_thm']) 795 | _ => 796 let 797 val (uthm'', le_u'_thm1, le_u'_thm2) = find_greater_expansion ectxt 798 (uthm', const_expansion ectxt basis \<^term>\<open>1::real\<close>, basis) 799 in 800 (uthm'', do_transfer 4 801 [mk_nonneg_thm l1_sgn_thm, ge_thm1, le_thm', le_u'_thm1, le_u'_thm2]) 802 end) 803 in 804 (Bounds (lower, Option.map transfer_upper (get_upper_bound bnds)), basis') 805 end 806 in 807 case get_lower_bound bnds1 of 808 SOME (lthm, _) => 809 let 810 val (lthm, _, sgns) = determine_sign ectxt (lthm, basis) 811 val bnds1 = 812 case bnds1 of 813 Exact _ => Exact lthm 814 | Bounds (SOME (_, le_thm), upper) => Bounds (SOME (lthm, le_thm), upper) 815 | _ => raise Match 816 in 817 case sgns of 818 (_, true) => aux bnds1 bnds2 819 | _ => 820 let 821 val abs_bnds = abs_expansion_bounds ectxt basis bnds1 822 fun transfer (NONE, _) = (Bounds (NONE, NONE), basis) 823 | transfer (SOME (uthm, le_thm), basis) = 824 let 825 val neg_uthm = @{thm expands_to_uminus} OF [get_basis_wf_thm basis, uthm] 826 val [ge_thm, le_thm] = 827 map (fn thm => le_thm RS thm) @{thms powr_nat_bounds_transfer_abs} 828 in 829 (Bounds (SOME (neg_uthm, ge_thm), SOME (uthm, le_thm)), basis) 830 end 831 in 832 aux abs_bnds bnds2 833 |> apfst get_upper_bound (* TODO better bounds possible *) 834 |> transfer 835 end 836 end 837 | _ => (Bounds (NONE, NONE), basis) 838 end 839 840fun ln_expansion_bounds' ectxt (lthm, ltrimmed_thm, lb_thm) ub basis = 841 let 842 val (lthm', basis') = ln_expansion ectxt ltrimmed_thm lthm basis 843 val wf_thm = get_basis_wf_thm basis 844 val lb_thm' = @{thm expands_to_lb_ln} OF [lthm, ltrimmed_thm, wf_thm, lb_thm] 845 in 846 case ub of 847 NONE => (Bounds (SOME (lthm', lb_thm'), NONE), basis') 848 | SOME (uthm, utrimmed_thm, ub_thm) => 849 let 850 val lifting = mk_lifting (extract_basis_list uthm) basis' 851 val uthm = lift_expands_to_thm lifting uthm 852 val utrimmed_thm = lift_trimmed_pos_thm lifting utrimmed_thm 853 val (uthm, _, utrimmed_thm) = retrim_pos_expansion ectxt (uthm, basis', utrimmed_thm) 854 val (uthm', basis'') = ln_expansion ectxt utrimmed_thm uthm basis' 855 val lthm' = lift basis'' lthm' 856 val ub_thm' = @{thm expands_to_ub_ln} OF [lthm, ltrimmed_thm, wf_thm, lb_thm, ub_thm] 857 in 858 (Bounds (SOME (lthm', lb_thm'), SOME (uthm', ub_thm')), basis'') 859 end 860 end 861 862fun floor_expansion_bounds ectxt (bnds, basis) = 863 let 864 val wf_thm = get_basis_wf_thm basis 865 fun mk_lb (exp_thm, le_thm) = 866 let 867 val exp_thm' = @{thm expands_to_minus} OF 868 [wf_thm, exp_thm, const_expansion ectxt basis \<^term>\<open>1::real\<close>] 869 val le_thm = @{thm rfloor_bound(1)} OF [le_thm] 870 in 871 (exp_thm', le_thm) 872 end 873 val mk_ub = apsnd (fn thm => @{thm rfloor_bound(2)} OF [thm]) 874 val bnds' = 875 Bounds (Option.map mk_lb (get_lower_bound bnds), Option.map mk_ub (get_upper_bound bnds)) 876 in 877 (bnds', basis) 878 end 879 880fun ceiling_expansion_bounds ectxt (bnds, basis) = 881 let 882 val wf_thm = get_basis_wf_thm basis 883 fun mk_ub (exp_thm, le_thm) = 884 let 885 val exp_thm' = @{thm expands_to_add} OF 886 [wf_thm, exp_thm, const_expansion ectxt basis \<^term>\<open>1::real\<close>] 887 val le_thm = @{thm rceil_bound(2)} OF [le_thm] 888 in 889 (exp_thm', le_thm) 890 end 891 val mk_lb = apsnd (fn thm => @{thm rceil_bound(1)} OF [thm]) 892 val bnds' = 893 Bounds (Option.map mk_lb (get_lower_bound bnds), Option.map mk_ub (get_upper_bound bnds)) 894 in 895 (bnds', basis) 896 end 897 898fun natmod_expansion_bounds _ (Bounds (NONE, NONE), _, _) = Bounds (NONE, NONE) 899 | natmod_expansion_bounds _ (_, Bounds (NONE, NONE), _) = Bounds (NONE, NONE) 900 | natmod_expansion_bounds ectxt (bnds1, bnds2, basis) = 901 let 902 val (f, g) = apply2 (Thm.reflexive o Thm.cterm_of (Lazy_Eval.get_ctxt ectxt) o 903 get_expanded_fun_bounds) (bnds1, bnds2) 904 val ge_lower_thm = @{thm natmod_trivial_lower_bound} OF [f, g] 905 fun minus1 thm = @{thm expands_to_minus} OF 906 [get_basis_wf_thm basis, thm, const_expansion ectxt basis \<^term>\<open>1::real\<close>] 907 fun find_upper uthm1 le1_thm u_nonneg_thm = 908 let 909 val upper1 = (uthm1, @{thm natmod_upper_bound'} OF [g, u_nonneg_thm, le1_thm]) 910 val upper2 = 911 case (get_lower_bound bnds2, get_upper_bound bnds2) of 912 (SOME (lthm2, ge2_thm), SOME (uthm2, le2_thm)) => ( 913 case determine_sign ectxt (minus1 lthm2, basis) of 914 (_, sgn_thm, (_, true)) => SOME (minus1 uthm2, 915 @{thm natmod_upper_bound} OF [f, ge2_thm, le2_thm, mk_nonneg_thm sgn_thm]) 916 | _ => NONE) 917 | _ => NONE 918 in 919 case upper2 of 920 NONE => upper1 921 | SOME upper2 => 922 case compare_expansions ectxt (fst upper1, fst upper2, basis) of 923 (GREATER, _, _, _) => upper2 924 | _ => upper1 925 end 926 in 927 case get_upper_bound bnds1 of 928 NONE => Bounds (SOME (zero_expansion basis, ge_lower_thm) , NONE) 929 | SOME (uthm1, le1_thm) => 930 case determine_sign ectxt (uthm1, basis) of 931 (_, sgn_thm, (true, _)) => Exact (@{thm expands_to_natmod_nonpos} OF 932 [g, mk_nonpos_thm sgn_thm, le1_thm, zero_expansion basis]) 933 | (uthm1, sgn_thm, (_, true)) => 934 Bounds (SOME (zero_expansion basis, ge_lower_thm), 935 SOME (find_upper uthm1 le1_thm (mk_nonneg_thm sgn_thm))) 936 | _ => raise TERM ("Unexpected result in natmod_expansion_bounds", []) 937 end 938 939fun sin_cos_expansion thm _ [] = 940 (thm RS @{thm expands_to_sin_real}, thm RS @{thm expands_to_cos_real}) 941 | sin_cos_expansion thm basis ((IsNeg, neg_thm) :: _) = 942 let 943 val neg_thm = @{thm compare_reals_diff_sgnD(1)} OF [neg_thm] 944 val [thm1, thm2] = 945 map (fn thm' => thm' OF [neg_thm, get_basis_wf_thm basis, thm]) 946 @{thms expands_to_sin_ms_neg_exp expands_to_cos_ms_neg_exp} 947 in 948 (thm1, thm2) 949 end 950 | sin_cos_expansion thm basis ((IsZero, zero_thm) :: e_thms) = 951 let 952 val zero_thm = @{thm compare_reals_diff_sgnD(2)} OF [zero_thm] 953 val thm' = expands_to_hd thm 954 val (sin_thm, cos_thm) = (sin_cos_expansion thm' (tl_basis basis) e_thms) 955 fun mk_thm thm' = 956 (thm' OF [zero_thm, get_basis_wf_thm basis, thm, sin_thm, cos_thm]) |> solve_eval_eq 957 val [thm1, thm2] = 958 map mk_thm @{thms expands_to_sin_ms_zero_exp expands_to_cos_ms_zero_exp} 959 in 960 (thm1, thm2) 961 end 962 | sin_cos_expansion _ _ _ = raise Match 963 964fun ln_expansion_bounds ectxt (Exact thm, basis) = 965 let 966 val (thm, _, trimmed_thm) = trim_expansion true (SOME Pos_Trim) ectxt (thm, basis) 967 in 968 case trimmed_thm of 969 NONE => raise TERM ("ln_expansion_bounds", [get_expanded_fun thm]) 970 | SOME trimmed_thm => 971 ln_expansion ectxt trimmed_thm thm basis |> apfst Exact 972 end 973 | ln_expansion_bounds _ (Bounds (NONE, _), _) = 974 raise TERM ("ln_expansion_bounds", []) 975 | ln_expansion_bounds ectxt (Bounds (SOME (lthm, lb_thm), ub), basis) = 976 let 977 fun trim thm = trim_expansion true (SOME Pos_Trim) ectxt (thm, basis) 978 val (lthm, _, trimmed_thm) = trim lthm 979 val ub = 980 Option.mapPartial (fn (uthm, ub_thm) => 981 case trim uthm of 982 (uthm, _, SOME trimmed_thm) => SOME (uthm, trimmed_thm, ub_thm) 983 | _ => NONE) 984 ub 985 in 986 case trimmed_thm of 987 NONE => raise TERM ("ln_expansion_bounds", [get_expanded_fun lthm]) 988 | SOME trimmed_thm => ln_expansion_bounds' ectxt (lthm, trimmed_thm, lb_thm) ub basis 989 end 990 991fun powr_const_expansion_bounds ectxt (Exact thm, p, basis) = 992 Exact (powr_const_expansion ectxt (thm, p, basis)) 993 | powr_const_expansion_bounds _ (Bounds (NONE, NONE), _, _) = Bounds (NONE, NONE) 994 | powr_const_expansion_bounds ectxt (bnds as Bounds (NONE, _), p, basis) = 995 Bounds (SOME (zero_expansion basis, @{thm eventually_powr_const_nonneg} OF 996 map (Thm.reflexive o Thm.cterm_of (Lazy_Eval.get_ctxt ectxt)) 997 [get_expanded_fun_bounds bnds, p]), NONE) 998 | powr_const_expansion_bounds ectxt (bnds as Bounds (SOME (lthm, ge_thm), upper), p, basis) = 999 let 1000 val (lthm, lsgn_thm, sgns) = determine_sign ectxt (lthm, basis) 1001 val _ = if snd sgns then () 1002 else raise TERM ("Negative base for powr.", []) 1003 val (sgn, SOME sgn_thm) = zeroness_oracle true (SOME Sgn_Trim) ectxt p 1004 in 1005 if sgn = IsNeg andalso fst sgns then 1006 Bounds (SOME (zero_expansion basis, 1007 @{thm eventually_powr_const_nonneg} OF 1008 map (Thm.reflexive o Thm.cterm_of (Lazy_Eval.get_ctxt ectxt)) 1009 [get_expanded_fun_bounds bnds, p]), NONE) 1010 else 1011 let 1012 val sgn_thm = 1013 case sgn of 1014 IsPos => sgn_thm RS @{thm less_imp_le} 1015 | IsZero => sgn_thm RS @{thm eq_zero_imp_nonneg} 1016 | IsNeg => sgn_thm RS @{thm less_imp_le} 1017 | _ => raise TERM ("Unexpected zeroness result in powr_const_expansion_bounds", []) 1018 val lthm' = powr_const_expansion ectxt (lthm, p, basis) 1019 val lbnd = (lthm', 1020 if sgn <> IsNeg then 1021 @{thm eventually_powr_const_mono_nonneg[OF _ _ eventually_le_self]} OF 1022 [sgn_thm, mk_nonneg_thm lsgn_thm, ge_thm] 1023 else 1024 @{thm eventually_powr_const_mono_nonpos[OF _ _ eventually_le_self]} OF 1025 [sgn_thm, lsgn_thm, ge_thm]) 1026 fun transfer_upper_bound (uthm, le_thm) = 1027 (powr_const_expansion ectxt (uthm, p, basis), 1028 if sgn <> IsNeg then 1029 @{thm eventually_powr_const_mono_nonneg} OF 1030 [sgn_thm, mk_nonneg_thm lsgn_thm, ge_thm, le_thm] 1031 else 1032 @{thm eventually_powr_const_mono_nonpos} OF 1033 [sgn_thm, lsgn_thm, ge_thm, le_thm]) 1034 in 1035 Bounds ((SOME lbnd, Option.map transfer_upper_bound upper) |> 1036 (if sgn = IsNeg then swap else I)) 1037 end 1038 end 1039 handle Bind => raise TERM ("Unexpected zeroness result in powr_const_expansion_bounds", []) 1040 1041 1042(* TODO stub *) 1043fun nonneg_power_expansion_bounds ectxt (Bounds (SOME (lthm, ge_thm), upper), n, basis) = 1044 let 1045 val (lthm, lsgn_thm, l1sgns) = determine_sign ectxt (lthm, basis) 1046 val _ = if not (snd l1sgns) then 1047 raise TERM ("Unexpected zeroness result in nonneg_power_expansion_bounds", []) else () 1048 val nonneg_thm = mk_nonneg_thm lsgn_thm 1049 val ctxt = Lazy_Eval.get_ctxt ectxt 1050 val n_thm = Thm.reflexive (Thm.cterm_of ctxt n) 1051 val lbnd = 1052 (power_expansion ectxt (lthm, n, basis), 1053 @{thm eventually_power_mono[OF _ eventually_le_self]} OF 1054 [nonneg_thm, ge_thm, n_thm]) 1055 fun transfer_upper (uthm, le_thm) = 1056 (power_expansion ectxt (uthm, n, basis), 1057 @{thm eventually_power_mono} OF 1058 [nonneg_thm, ge_thm, le_thm, n_thm]) 1059 in 1060 Bounds (SOME lbnd, Option.map transfer_upper upper) 1061 end 1062 | nonneg_power_expansion_bounds _ _ = Bounds (NONE, NONE) 1063 1064fun odd_power_expansion_bounds ectxt odd_thm (bnds, n, basis) = 1065 let 1066 fun transfer (thm, le_thm) = 1067 (power_expansion ectxt (thm, n, basis), 1068 @{thm eventually_mono_power_odd} OF [odd_thm, le_thm]) 1069 in 1070 bnds |> apply2 (Option.map transfer) |> Bounds 1071 end 1072 1073fun get_parity' ectxt t = 1074 let 1075 (* TODO: Throw a tactic at it *) 1076 val ctxt = Lazy_Eval.get_ctxt ectxt 1077 val par = get_parity (Thm.cterm_of ctxt t) 1078 fun is_unknown Unknown_Parity = true 1079 | is_unknown _ = false 1080 val _ = 1081 if not (is_unknown par) orelse not (#verbose (#ctxt ectxt)) then () else 1082 let 1083 val p = Pretty.str ("real_asymp failed to determine whether the following term " ^ 1084 "is even or odd:") 1085 val p = Pretty.chunks [p, Pretty.indent 2 (Syntax.pretty_term ctxt t)] 1086 in 1087 Pretty.writeln p 1088 end 1089 in 1090 par 1091 end 1092 1093fun reflexive ectxt t = Thm.reflexive (Thm.cterm_of (Lazy_Eval.get_ctxt ectxt) t) 1094 1095fun unknown_parity_power_expansion_lower_bound ectxt ((SOME (lthm, ge_thm), _), n, basis) = 1096 let 1097 val lpow_thm = power_expansion ectxt (lthm, n, basis) 1098 val (lthm', le_thm1, le_thm2) = 1099 find_smaller_expansion ectxt (lpow_thm, zero_expansion basis, basis) 1100 in 1101 SOME (lthm', @{thm eventually_lower_bound_power_indet} OF [ge_thm, le_thm1, le_thm2]) 1102 end 1103 | unknown_parity_power_expansion_lower_bound _ _ = NONE 1104 1105fun unknown_parity_power_expansion_upper_bound ectxt 1106 ((SOME (lthm, ge_thm), SOME (uthm, le_thm)), n, basis) = 1107 let 1108 val lthm = @{thm expands_to_uminus} OF [get_basis_wf_thm basis, lthm] 1109 val (uthm', ge_thm1, ge_thm2) = 1110 find_greater_expansion ectxt (lthm, uthm, basis) 1111 val uthm' = power_expansion ectxt (uthm', n, basis) 1112 in 1113 SOME (uthm', @{thm eventually_upper_bound_power_indet} OF 1114 [ge_thm, le_thm, ge_thm1, ge_thm2, reflexive ectxt n]) 1115 end 1116 | unknown_parity_power_expansion_upper_bound _ _ = NONE 1117 1118fun even_power_expansion_bounds ectxt even_thm (bnds, n, basis) = 1119 let 1120 fun handle_indet_case bnds = 1121 let 1122 val lower = (zero_expansion basis, @{thm eventually_lower_bound_power_even_indet} OF 1123 [even_thm, reflexive ectxt (get_expanded_fun_bounds (Bounds bnds))]) 1124 val upper = unknown_parity_power_expansion_upper_bound ectxt (bnds, n, basis) 1125 in 1126 (SOME lower, upper) 1127 end 1128 in 1129 case snd bnds of 1130 NONE => handle_indet_case bnds 1131 | SOME (uthm, le_thm) => 1132 let 1133 val (uthm, usgn_thm, usgns) = determine_sign ectxt (uthm, basis) 1134 val bnds = (fst bnds, SOME (uthm, le_thm)) 1135 in 1136 if fst usgns then 1137 let 1138 val lthm' = power_expansion ectxt (uthm, n, basis) 1139 val ge_thm' = @{thm eventually_lower_bound_power_even_nonpos} OF 1140 [even_thm, mk_nonpos_thm usgn_thm, le_thm] 1141 fun transfer_lower_bound (lthm, ge_thm) = 1142 (power_expansion ectxt (lthm, n, basis), 1143 @{thm eventually_upper_bound_power_even_nonpos} OF 1144 [even_thm, mk_nonpos_thm usgn_thm, ge_thm, le_thm]) 1145 in 1146 (SOME (lthm', ge_thm'), Option.map transfer_lower_bound (fst bnds)) 1147 end 1148 else 1149 handle_indet_case bnds 1150 end 1151 end 1152 1153fun power_expansion_bounds ectxt (Exact thm, n, basis) = 1154 Exact (power_expansion ectxt (thm, n, basis)) 1155 | power_expansion_bounds ectxt (Bounds bnds, n, basis) = 1156 let 1157 val parity = get_parity' ectxt n 1158 fun handle_non_nonneg_case bnds = Bounds ( 1159 case parity of 1160 Odd _ => raise Match 1161 | Even even_thm => even_power_expansion_bounds ectxt even_thm (bnds, n, basis) 1162 | Unknown_Parity => 1163 (unknown_parity_power_expansion_lower_bound ectxt (bnds, n, basis), 1164 unknown_parity_power_expansion_upper_bound ectxt (bnds, n, basis))) 1165 in 1166 case parity of 1167 Odd odd_thm => odd_power_expansion_bounds ectxt odd_thm (bnds, n, basis) 1168 | _ => 1169 case fst bnds of 1170 NONE => handle_non_nonneg_case bnds 1171 | SOME (lthm, ge_thm) => 1172 let 1173 val (lthm, lsgn_thm, lsgns) = determine_sign ectxt (lthm, basis) 1174 val bnds = (SOME (lthm, ge_thm), snd bnds) 1175 in 1176 if snd lsgns then 1177 let 1178 val nthm = reflexive ectxt n 1179 val lthm' = power_expansion ectxt (lthm, n, basis) 1180 val ge_thm' = @{thm eventually_power_mono[OF _ eventually_le_self]} OF 1181 [mk_nonneg_thm lsgn_thm, ge_thm, nthm] 1182 fun transfer_upper (uthm, le_thm) = 1183 (power_expansion ectxt (uthm, n, basis), 1184 @{thm eventually_power_mono} OF 1185 [mk_nonneg_thm lsgn_thm, ge_thm, le_thm, nthm]) 1186 in 1187 Bounds (SOME (lthm', ge_thm'), Option.map transfer_upper (snd bnds)) 1188 end 1189 else 1190 handle_non_nonneg_case bnds 1191 end 1192 end 1193 1194fun sgn_expansion_bounds ectxt (Exact thm, basis) = 1195 Exact (sgn_expansion ectxt (thm, basis)) 1196 | sgn_expansion_bounds ectxt (Bounds bnds, basis) = 1197 let 1198 fun aux (thm, le_thm) = 1199 (sgn_expansion ectxt (thm, basis), mono_bound @{thm mono_sgn_real} le_thm) 1200 val (lower, upper) = apply2 (Option.map aux) bnds 1201 fun get_bound_exp (SOME (thm, _)) = SOME (get_expansion thm) 1202 | get_bound_exp _ = NONE 1203 fun is_const (SOME (Const (\<^const_name>\<open>Multiseries_Expansion.const_expansion\<close>, _) $ c'), 1204 c) = c aconv c' 1205 | is_const _ = false 1206 fun aconv' (SOME a, SOME b) = a aconv b 1207 | aconv' _ = false 1208 in 1209 if is_const (get_bound_exp lower, \<^term>\<open>\<lambda>x::real. 1 :: real\<close>) then 1210 let 1211 val SOME (lthm, ge_thm) = lower 1212 in 1213 Exact (@{thm eventually_sgn_ge_1D} OF [ge_thm, lthm]) 1214 end 1215 else if is_const (get_bound_exp upper, \<^term>\<open>\<lambda>x::real. -1 :: real\<close>) then 1216 let 1217 val SOME (uthm, le_thm) = upper 1218 in 1219 Exact (@{thm eventually_sgn_le_neg1D} OF [le_thm, uthm]) 1220 end 1221 else if aconv' (apply2 get_bound_exp (lower, upper)) then 1222 let 1223 val (SOME (lthm, ge_thm), SOME (uthm, le_thm)) = (lower, upper) 1224 in 1225 Exact (@{thm expands_to_squeeze} OF [ge_thm, le_thm, lthm, uthm]) 1226 end 1227 else 1228 Bounds (lower, upper) 1229 end 1230 1231fun sin_cos_expansion_bounds sin ectxt e basis = 1232 let 1233 val f = if sin then fst else snd 1234 fun trivial_bounds basis = 1235 mk_trivial_bounds ectxt (expr_to_term e) 1236 (if sin then @{thm trivial_bounds_sin} else @{thm trivial_bounds_cos}) basis 1237 fun mk_expansion (thm, basis') = 1238 case trim_expansion_while_pos ectxt (thm, basis') of 1239 (_, Trimmed _, _) => (trivial_bounds basis, basis) 1240 | (thm, Aborted _, e_thms) => 1241 (Exact (f (sin_cos_expansion thm basis' e_thms)), basis') 1242 in 1243 case expand_bounds' ectxt e basis of 1244 (Exact thm, basis') => mk_expansion (thm, basis') 1245 | _ => (trivial_bounds basis, basis) 1246 end 1247 1248and mono_expansion mono_thm expand_fun ectxt e basis = 1249 case expand_bounds' ectxt e basis of 1250 (Exact thm, basis) => expand_fun ectxt thm basis |> apfst Exact 1251 | (Bounds (SOME (lthm, lb_thm), NONE), basis) => 1252 expand_fun ectxt lthm basis 1253 |> apfst (fn lthm => Bounds (SOME (lthm, mono_bound mono_thm lb_thm), NONE)) 1254 | (Bounds (NONE, SOME (uthm, ub_thm)), basis) => 1255 expand_fun ectxt uthm basis 1256 |> apfst (fn uthm => Bounds (NONE, SOME (uthm, mono_bound mono_thm ub_thm))) 1257 | (Bounds (SOME (lthm, lb_thm), SOME (uthm, ub_thm)), basis) => 1258 let 1259 val (lthm', basis') = expand_fun ectxt lthm basis 1260 val (uthm', basis'') = expand_fun ectxt (lift basis' uthm) basis' 1261 val lthm' = lift basis'' lthm' 1262 val (lb_thm', ub_thm') = apply2 (mono_bound mono_thm) (lb_thm, ub_thm) 1263 in 1264 (Bounds (SOME (lthm', lb_thm'), SOME (uthm', ub_thm')), basis'') 1265 end 1266 | x => x 1267 1268and minmax_expansion_bounds max thm ectxt (e1, e2) basis = 1269 case try_prove_ev_eq ectxt (apply2 expr_to_term (e1, e2)) of 1270 SOME eq_thm => 1271 let 1272 val eq_thm' = 1273 eq_thm RS (if max then @{thm max_eventually_eq} else @{thm min_eventually_eq}) 1274 in 1275 expand_bounds' ectxt e1 basis |> apfst (cong_bounds eq_thm') 1276 end 1277 | NONE => 1278 let 1279 val (bnds1, basis') = expand_bounds' ectxt e1 basis 1280 val (bnds2, basis'') = expand_bounds' ectxt e2 basis' 1281 val bnds1 = lift_bounds basis'' bnds1 1282 fun f (thm1, thm2) = 1283 (if max then max_expansion else min_expansion) ectxt (thm1, thm2, basis'') 1284 fun handle_bound (SOME (exp_thm1, le_thm1), SOME (exp_thm2, le_thm2)) = 1285 SOME (f (exp_thm1, exp_thm2), thm OF [le_thm1, le_thm2]) 1286 | handle_bound _ = NONE 1287 val bnds = (bnds1, bnds2) 1288 val bnds = 1289 case (bnds1, bnds2) of 1290 (Exact thm1, Exact thm2) => Exact (f (thm1, thm2)) 1291 | _ => 1292 Bounds (handle_bound (apply2 get_lower_bound bnds), 1293 handle_bound (apply2 get_upper_bound bnds)) 1294 in 1295 (bnds, basis'') 1296 end 1297 1298and expand_bin_bounds swap thms ectxt (e1, e2) basis = 1299 let 1300 val (bnds1, basis') = expand_bounds' ectxt e1 basis 1301 val (bnds2, basis'') = expand_bounds' ectxt e2 basis' 1302 val bnds1 = lift_bounds basis'' bnds1 1303 val bnds = expand_add_bounds swap thms (bnds1, bnds2) basis'' 1304 in 1305 (bnds, basis'') 1306 end 1307 1308and expand_bounds'' ectxt (Add e12) basis = 1309 expand_bin_bounds false @{thms expands_to_add combine_bounds_add} ectxt e12 basis 1310 | expand_bounds'' ectxt (Minus e12) basis = 1311 expand_bin_bounds true @{thms expands_to_minus combine_bounds_diff} ectxt e12 basis 1312 | expand_bounds'' ectxt (Uminus e) basis = ( 1313 case expand_bounds' ectxt e basis of 1314 (Exact thm, basis) => 1315 (Exact (@{thm expands_to_uminus} OF [get_basis_wf_thm basis, thm]), basis) 1316 | (Bounds bnds, basis) => 1317 let 1318 fun flip (thm1, thm2) = 1319 (@{thm expands_to_uminus} OF [get_basis_wf_thm basis, thm1], 1320 @{thm bounds_uminus} OF [thm2]) 1321 in 1322 (Bounds (apply2 (Option.map flip) (swap bnds)), basis) 1323 end) 1324 | expand_bounds'' ectxt (Mult (e1, e2)) basis = 1325 let 1326 val (bnds1, basis') = expand_bounds' ectxt e1 basis 1327 val (bnds2, basis'') = expand_bounds' ectxt e2 basis' 1328 val bnds1 = lift_bounds basis'' bnds1 1329 val bnds = mult_expansion_bounds ectxt basis'' bnds1 bnds2 1330 in 1331 (bnds, basis'') 1332 end 1333 | expand_bounds'' ectxt (Powr (e1, e2)) basis = 1334 let 1335 val (bnds1, basis') = expand_bounds' ectxt e1 basis 1336 val (bnds2, basis'') = expand_bounds' ectxt e2 basis' 1337 val bnds1 = lift_bounds basis'' bnds1 1338 in 1339 powr_expansion_bounds ectxt basis'' bnds1 bnds2 1340 end 1341 | expand_bounds'' ectxt (Powr_Nat (e1, e2)) basis = 1342 let 1343 val (bnds1, basis') = expand_bounds' ectxt e1 basis 1344 val (bnds2, basis'') = expand_bounds' ectxt e2 basis' 1345 val bnds1 = lift_bounds basis'' bnds1 1346 in 1347 powr_nat_expansion_bounds ectxt basis'' bnds1 bnds2 1348 end 1349 | expand_bounds'' ectxt (Powr' (e, p)) basis = 1350 let 1351 val (bnds, basis') = expand_bounds' ectxt e basis 1352 in 1353 (powr_const_expansion_bounds ectxt (bnds, p, basis'), basis') 1354 end 1355 | expand_bounds'' ectxt (Power (e, n)) basis = 1356 let 1357 val (bnds, basis') = expand_bounds' ectxt e basis 1358 in 1359 (power_expansion_bounds ectxt (bnds, n, basis'), basis') 1360 end 1361 | expand_bounds'' ectxt (Root (e, n)) basis = 1362 mono_expansion (reflexive ectxt n RS @{thm mono_root_real}) 1363 (fn ectxt => fn thm => fn basis => (root_expansion ectxt (thm, n, basis), basis)) 1364 ectxt e basis 1365 | expand_bounds'' ectxt (Inverse e) basis = 1366 let 1367 val (bnds, basis') = expand_bounds' ectxt e basis 1368 in 1369 (inverse_expansion_bounds ectxt basis' bnds, basis') 1370 end 1371 | expand_bounds'' ectxt (Div (e1, e2)) basis = 1372 let 1373 val (bnds1, basis') = expand_bounds' ectxt e1 basis 1374 val (bnds2, basis'') = expand_bounds' ectxt e2 basis' 1375 val bnds1 = lift_bounds basis'' bnds1 1376 in 1377 (divide_expansion_bounds ectxt basis'' bnds1 bnds2, basis'') 1378 end 1379 | expand_bounds'' ectxt (Sin e) basis = 1380 sin_cos_expansion_bounds true ectxt e basis 1381 | expand_bounds'' ectxt (Cos e) basis = 1382 sin_cos_expansion_bounds false ectxt e basis 1383 | expand_bounds'' ectxt (Exp e) basis = 1384 mono_expansion @{thm mono_exp_real} exp_expansion ectxt e basis 1385 | expand_bounds'' ectxt (Ln e) basis = 1386 ln_expansion_bounds ectxt (expand_bounds' ectxt e basis) 1387 | expand_bounds'' ectxt (ExpLn e) basis = 1388 let 1389 val (bnds, basis') = expand_bounds' ectxt e basis 1390 in 1391 case get_lower_bound bnds of 1392 NONE => (Bounds (NONE, NONE), basis) 1393 | SOME (lthm, ge_thm) => 1394 case trim_expansion true (SOME Pos_Trim) ectxt (lthm, basis') of 1395 (_, _, NONE) => raise TERM ("Non-positive function under logarithm.", []) 1396 | (lthm, _, SOME trimmed_thm) => 1397 let 1398 val bnds = 1399 case bnds of 1400 Exact _ => Exact lthm 1401 | Bounds (_, upper) => Bounds (SOME (lthm, ge_thm), upper) 1402 val eq_thm = @{thm expands_to_imp_exp_ln_eq} OF 1403 [lthm, ge_thm, trimmed_thm, get_basis_wf_thm basis] 1404 in 1405 (cong_bounds eq_thm bnds, basis') 1406 end 1407 end 1408 | expand_bounds'' ectxt (LnPowr (e1, e2)) basis = 1409 let 1410 val (bnds1, basis') = expand_bounds' ectxt e1 basis 1411 val (bnds2, basis'') = expand_bounds' ectxt e2 basis' 1412 val bnds1 = lift_bounds basis'' bnds1 1413 in 1414 case get_lower_bound bnds1 of 1415 NONE => (Bounds (NONE, NONE), basis) 1416 | SOME (lthm, ge_thm) => 1417 case trim_expansion true (SOME Pos_Trim) ectxt (lthm, basis'') of 1418 (_, _, NONE) => raise TERM ("Non-positive base for powr.", []) 1419 | (lthm, _, SOME trimmed_thm) => 1420 let 1421 val bnds1 = 1422 case bnds1 of 1423 Exact _ => Exact lthm 1424 | Bounds (_, upper) => Bounds (SOME (lthm, ge_thm), upper) 1425 val eq_thm = @{thm expands_to_imp_ln_powr_eq} OF 1426 [lthm, ge_thm, trimmed_thm, get_basis_wf_thm basis''] 1427 val (ln_bnds, basis''') = ln_expansion_bounds ectxt (bnds1, basis'') 1428 val bnds2 = lift_bounds basis''' bnds2 1429 val bnds = mult_expansion_bounds ectxt basis''' ln_bnds bnds2 1430 in 1431 (cong_bounds eq_thm bnds, basis''') 1432 end 1433 end 1434 | expand_bounds'' ectxt (Absolute e) basis = 1435 let 1436 val (bnds, basis') = expand_bounds' ectxt e basis 1437 in 1438 (abs_expansion_bounds ectxt basis' bnds, basis') 1439 end 1440 | expand_bounds'' ectxt (Sgn e) basis = 1441 let 1442 val (bnds, basis') = expand_bounds' ectxt e basis 1443 in 1444 (sgn_expansion_bounds ectxt (bnds, basis'), basis') 1445 end 1446 | expand_bounds'' ectxt (Min e12) basis = 1447 minmax_expansion_bounds false @{thm combine_bounds_min} ectxt e12 basis 1448 | expand_bounds'' ectxt (Max e12) basis = 1449 minmax_expansion_bounds true @{thm combine_bounds_max} ectxt e12 basis 1450 | expand_bounds'' ectxt (Floor e) basis = 1451 floor_expansion_bounds ectxt (expand_bounds' ectxt e basis) 1452 | expand_bounds'' ectxt (Ceiling e) basis = 1453 ceiling_expansion_bounds ectxt (expand_bounds' ectxt e basis) 1454 | expand_bounds'' ectxt (Frac e) basis = 1455 (mk_trivial_bounds ectxt (expr_to_term e) @{thm trivial_bounds_frac} basis, basis) 1456 | expand_bounds'' ectxt (NatMod (e1, e2)) basis = 1457 let 1458 val (bnds1, basis') = expand_bounds' ectxt e1 basis 1459 val (bnds2, basis'') = expand_bounds' ectxt e2 basis' 1460 val bnds1 = lift_bounds basis'' bnds1 1461 in 1462 (natmod_expansion_bounds ectxt (bnds1, bnds2, basis''), basis'') 1463 end 1464 | expand_bounds'' ectxt (ArcTan e) basis = 1465 mono_expansion @{thm mono_arctan_real} 1466 (fn ectxt => fn thm => fn basis => (arctan_expansion ectxt basis thm, basis)) ectxt e basis 1467 | expand_bounds'' ectxt e basis = 1468 expand ectxt e basis |> apfst Exact 1469 1470and expand_bounds' ectxt e basis = 1471 expand_bounds'' ectxt e basis |> apfst (check_bounds e) 1472 1473fun expand_term_bounds ectxt t basis = 1474 let 1475 val ctxt = Lazy_Eval.get_ctxt ectxt 1476 val (e, eq_thm) = reify ctxt t 1477 val (bounds, basis) = expand_bounds' ectxt e basis 1478 in 1479 (transfer_bounds eq_thm bounds, basis) 1480 end 1481 1482fun expand_terms_bounds ectxt ts basis = 1483 let 1484 val ctxt = Lazy_Eval.get_ctxt ectxt 1485 val e_eq_thms = map (reify ctxt) ts 1486 fun step (e, eq_thm) (bndss, basis) = 1487 let 1488 val (bnds, basis) = expand_bounds' ectxt e basis 1489 val bnds = transfer_bounds eq_thm bnds 1490 in 1491 (bnds :: bndss, basis) 1492 end 1493 val (thms, basis) = fold step e_eq_thms ([], basis) 1494 fun lift bnds = lift_bounds basis bnds 1495 in 1496 (map lift (rev thms), basis) 1497 end 1498 1499fun prove_nhds_bounds ectxt (Exact thm, basis) = prove_nhds ectxt (thm, basis) 1500 | prove_nhds_bounds ectxt (Bounds (SOME (lthm, ge_thm), SOME (uthm, le_thm)), basis) = 1501 let 1502 fun extract_limit thm = 1503 thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |> dest_comb |> snd 1504 |> dest_comb |> snd 1505 val llim_thm = prove_nhds ectxt (lthm, basis) 1506 val ulim_thm = prove_nhds ectxt (uthm, basis) 1507 val (lim1, lim2) = apply2 extract_limit (llim_thm, ulim_thm) 1508 val eq_thm = the (try_prove_real_eq true ectxt (lim1, lim2)) 1509 in 1510 @{thm tendsto_sandwich'} OF [ge_thm, le_thm, llim_thm, ulim_thm, eq_thm] 1511 end 1512 | prove_nhds_bounds _ _ = raise TERM ("prove_nhds_bounds", []) 1513 1514fun prove_at_top_bounds ectxt (Exact thm, basis) = prove_at_top ectxt (thm, basis) 1515 | prove_at_top_bounds ectxt (Bounds (SOME (lthm, ge_thm), _), basis) = 1516 let 1517 val llim_thm = prove_at_top ectxt (lthm, basis) 1518 in 1519 @{thm filterlim_at_top_mono} OF [llim_thm, ge_thm] 1520 end 1521 | prove_at_top_bounds _ _ = raise TERM ("prove_at_top_bounds", []) 1522 1523fun prove_at_bot_bounds ectxt (Exact thm, basis) = prove_at_bot ectxt (thm, basis) 1524 | prove_at_bot_bounds ectxt (Bounds (_, SOME (uthm, le_thm)), basis) = 1525 let 1526 val ulim_thm = prove_at_bot ectxt (uthm, basis) 1527 in 1528 @{thm filterlim_at_bot_mono} OF [ulim_thm, le_thm] 1529 end 1530 | prove_at_bot_bounds _ _ = raise TERM ("prove_at_bot_bounds", []) 1531 1532fun prove_at_infinity_bounds ectxt (Exact thm, basis) = prove_at_infinity ectxt (thm, basis) 1533 | prove_at_infinity_bounds ectxt (Bounds (lb, ub), basis) = 1534 let 1535 val wf_thm = get_basis_wf_thm basis 1536 fun assert_nz (SOME (thm, le_thm)) = ( 1537 case ev_zeroness_oracle ectxt (get_expanded_fun thm) of 1538 SOME _ => NONE 1539 | NONE => SOME (thm, le_thm)) 1540 | assert_nz NONE = NONE 1541 fun lb_at_top (lthm, ge_thm) = 1542 case trim_expansion true (SOME Sgn_Trim) ectxt (lthm, basis) of 1543 (lthm, IsPos, SOME trimmed_thm) => SOME 1544 let 1545 val lim_thm = prove_at_infinity ectxt (lthm, basis) 1546 val pos_thm = @{thm expands_to_imp_eventually_pos} OF [wf_thm, lthm, trimmed_thm] 1547 val lim_thm' = 1548 @{thm filterlim_at_infinity_imp_filterlim_at_top} OF [lim_thm, pos_thm] 1549 in 1550 @{thm filterlim_at_top_imp_at_infinity[OF filterlim_at_top_mono]} 1551 OF [lim_thm', ge_thm] 1552 end 1553 | _ => NONE 1554 fun ub_at_top (uthm, le_thm) = 1555 case trim_expansion true (SOME Sgn_Trim) ectxt (uthm, basis) of 1556 (uthm, IsNeg, SOME trimmed_thm) => SOME 1557 let 1558 val lim_thm = prove_at_infinity ectxt (uthm, basis) 1559 val neg_thm = @{thm expands_to_imp_eventually_neg} OF [wf_thm, uthm, trimmed_thm] 1560 val lim_thm' = 1561 @{thm filterlim_at_infinity_imp_filterlim_at_bot} OF [lim_thm, neg_thm] 1562 in 1563 @{thm filterlim_at_bot_imp_at_infinity[OF filterlim_at_bot_mono]} 1564 OF [lim_thm', le_thm] 1565 end 1566 | _ => NONE 1567 in 1568 case Option.mapPartial lb_at_top (assert_nz lb) of 1569 SOME thm => thm 1570 | NONE => 1571 case Option.mapPartial ub_at_top (assert_nz ub) of 1572 SOME thm => thm 1573 | NONE => raise TERM ("prove_at_infinity_bounds", []) 1574 end 1575 1576fun prove_eventually_pos_lower_bound ectxt basis (lthm, ge_thm) = 1577 case trim_expansion true (SOME Sgn_Trim) ectxt (lthm, basis) of 1578 (lthm, IsPos, SOME trimmed_thm) => 1579 SOME (@{thm eventually_less_le} OF [@{thm expands_to_imp_eventually_pos} OF 1580 [get_basis_wf_thm basis, lthm, trimmed_thm], ge_thm]) 1581 | _ => NONE 1582 1583 1584fun prove_eventually_neg_upper_bound ectxt basis (uthm, le_thm) = 1585 case trim_expansion true (SOME Sgn_Trim) ectxt (uthm, basis) of 1586 (uthm, IsNeg, SOME trimmed_thm) => 1587 SOME (@{thm eventually_le_less} OF [le_thm, @{thm expands_to_imp_eventually_neg} OF 1588 [get_basis_wf_thm basis, uthm, trimmed_thm]]) 1589 | _ => NONE 1590 1591fun prove_eventually_nonzero_bounds ectxt (Exact thm, basis) = ( 1592 case trim_expansion true (SOME Simple_Trim) ectxt (thm, basis) of 1593 (thm, _, SOME trimmed_thm) => 1594 @{thm expands_to_imp_eventually_nz} OF [get_basis_wf_thm basis, thm, trimmed_thm] 1595 | _ => raise TERM ("prove_eventually_nonzero", [])) 1596 | prove_eventually_nonzero_bounds ectxt (Bounds (l, u), basis) = 1597 case Option.mapPartial (prove_eventually_pos_lower_bound ectxt basis) l of 1598 SOME thm => thm RS @{thm eventually_pos_imp_nz} 1599 | NONE => 1600 case Option.mapPartial (prove_eventually_neg_upper_bound ectxt basis) u of 1601 SOME thm => thm RS @{thm eventually_neg_imp_nz} 1602 | NONE => raise TERM ("prove_eventually_nonzero", []) 1603 1604fun prove_at_0_bounds ectxt (Exact thm, basis) = prove_at_0 ectxt (thm, basis) 1605 | prove_at_0_bounds ectxt (Bounds bnds, basis) = 1606 let 1607 val lim_thm = prove_nhds_bounds ectxt (Bounds bnds, basis) 1608 val nz_thm = prove_eventually_nonzero_bounds ectxt (Bounds bnds, basis) 1609 in 1610 @{thm Topological_Spaces.filterlim_atI} OF [lim_thm, nz_thm] 1611 end 1612 1613fun prove_at_right_0_bounds ectxt (Exact thm, basis) = prove_at_right_0 ectxt (thm, basis) 1614 | prove_at_right_0_bounds ectxt (Bounds (SOME l, SOME u), basis) = 1615 let 1616 val lim_thm = prove_nhds_bounds ectxt (Bounds (SOME l, SOME u), basis) 1617 in 1618 case prove_eventually_pos_lower_bound ectxt basis l of 1619 SOME pos_thm => @{thm tendsto_imp_filterlim_at_right} OF [lim_thm, pos_thm] 1620 | NONE => raise TERM ("prove_at_right_0_bounds", []) 1621 end 1622 | prove_at_right_0_bounds _ _ = raise TERM ("prove_at_right_0_bounds", []) 1623 1624fun prove_at_left_0_bounds ectxt (Exact thm, basis) = prove_at_left_0 ectxt (thm, basis) 1625 | prove_at_left_0_bounds ectxt (Bounds (SOME l, SOME u), basis) = 1626 let 1627 val lim_thm = prove_nhds_bounds ectxt (Bounds (SOME l, SOME u), basis) 1628 in 1629 case prove_eventually_neg_upper_bound ectxt basis u of 1630 SOME neg_thm => @{thm tendsto_imp_filterlim_at_left} OF [lim_thm, neg_thm] 1631 | NONE => raise TERM ("prove_at_left_0_bounds", []) 1632 end 1633 | prove_at_left_0_bounds _ _ = raise TERM ("prove_at_left_0_bounds", []) 1634 1635fun prove_eventually_less_bounds ectxt (bnds1, bnds2, basis) = 1636 case (get_upper_bound bnds1, get_lower_bound bnds2) of 1637 (SOME (ub1_thm, le_ub1_thm), SOME (lb2_thm, ge_lb2_thm)) => 1638 let 1639 val thm = prove_eventually_less ectxt (ub1_thm, lb2_thm, basis) 1640 in 1641 @{thm eventually_le_less[OF _ eventually_less_le]} OF [le_ub1_thm, thm, ge_lb2_thm] 1642 end 1643 | _ => raise TERM ("prove_asymptotically_less_bounds", []) 1644 1645fun prove_eventually_greater_bounds ectxt (bnds1, bnds2, basis) = 1646 prove_eventually_less_bounds ectxt (bnds2, bnds1, basis) 1647 1648 1649 1650fun prove_o_bounds small ectxt (Exact thm1, Exact thm2, basis) = 1651 (if small then prove_smallo else prove_bigo) ectxt (thm1, thm2, basis) 1652 | prove_o_bounds small ectxt (bnds1, bnds2, basis) = 1653 let 1654 val exact = if small then prove_smallo else prove_bigo 1655 val s = if small then "prove_smallo_bounds" else "prove_bigo_bounds" 1656 val (l2thm', nonneg_thm, ge2_thm) = abs_expansion_lower_bound ectxt basis bnds2 1657 val ((l1thm, ge1_thm), (u1thm, le1_thm)) = 1658 case bnds1 of 1659 Exact thm1 => 1660 let val x = (exact ectxt (thm1, l2thm', basis), thm1 RS @{thm exact_to_bound}) 1661 in (x, x) end 1662 | Bounds (SOME (l1thm, ge1_thm), SOME (u1thm, le1_thm)) => 1663 ((exact ectxt (l1thm, l2thm', basis), ge1_thm), 1664 (exact ectxt (u1thm, l2thm', basis), le1_thm)) 1665 | _ => raise TERM (s, []) 1666 val impthm = if small then @{thm bounds_smallo_imp_smallo} else @{thm bounds_bigo_imp_bigo} 1667 in 1668 impthm OF [ge1_thm, le1_thm, ge2_thm, nonneg_thm, l1thm, u1thm] 1669 end 1670 1671val prove_smallo_bounds = prove_o_bounds true 1672val prove_bigo_bounds = prove_o_bounds false 1673 1674fun prove_bigtheta_bounds ectxt (Exact thm1, Exact thm2, basis) = 1675 prove_bigtheta ectxt (thm1, thm2, basis) 1676 | prove_bigtheta_bounds ectxt (bnds1, bnds2, basis) = 1677 let (* TODO inefficient *) 1678 val thms = 1679 Par_List.map (fn x => prove_bigo_bounds ectxt x) 1680 [(bnds1, bnds2, basis), (bnds2, bnds1, basis)] 1681 in 1682 @{thm bigthetaI[unfolded bigomega_iff_bigo]} OF thms 1683 end 1684 1685fun prove_asymp_equivs ectxt basis = 1686 Par_List.map (fn (thm1, thm2) => prove_asymp_equiv ectxt (thm1, thm2, basis)) 1687 1688fun prove_asymp_equiv_bounds ectxt (Exact thm1, Exact thm2, basis) = 1689 prove_asymp_equiv ectxt (thm1, thm2, basis) 1690 | prove_asymp_equiv_bounds ectxt (Exact thm1, 1691 Bounds (SOME (l2, ge2_thm), SOME (u2, le2_thm)), basis) = 1692 let 1693 val thms = prove_asymp_equivs ectxt basis [(thm1, l2), (thm1, u2)] 1694 in 1695 @{thm asymp_equiv_sandwich_real'[OF _ _ eventually_atLeastAtMostI]} OF 1696 (thms @ [ge2_thm, le2_thm]) 1697 end 1698 | prove_asymp_equiv_bounds ectxt (Bounds (SOME (l1, ge1_thm), SOME (u1, le1_thm)), 1699 Exact thm2, basis) = 1700 let 1701 val thms = prove_asymp_equivs ectxt basis [(l1, thm2), (u1, thm2)] 1702 in 1703 @{thm asymp_equiv_sandwich_real[OF _ _ eventually_atLeastAtMostI]} OF 1704 (thms @ [ge1_thm, le1_thm]) 1705 end 1706 | prove_asymp_equiv_bounds ectxt (Bounds (SOME (l1, ge1_thm), SOME (u1, le1_thm)), 1707 Bounds (SOME (l2, ge2_thm), SOME (u2, le2_thm)), basis) = 1708 let 1709 val thms = prove_asymp_equivs ectxt basis [(l1, u1), (u1, l2), (l2, u2)] 1710 in 1711 @{thm asymp_equiv_sandwich_real'' 1712 [OF _ _ _ eventually_atLeastAtMostI eventually_atLeastAtMostI]} OF 1713 (thms @ [ge1_thm, le1_thm, ge2_thm, le2_thm]) 1714 end 1715 | prove_asymp_equiv_bounds _ _ = raise TERM ("prove_asymp_equiv_bounds", []) 1716 1717val dest_fun = dest_comb #> fst 1718val dest_arg = dest_comb #> snd 1719val concl_of' = Thm.concl_of #> HOLogic.dest_Trueprop 1720 1721fun lim_eq ectxt (l1, l2) = (l1 aconv l2) orelse 1722 case (l1, l2) of 1723 (Const (\<^const_name>\<open>nhds\<close>, _) $ a, Const (\<^const_name>\<open>nhds\<close>, _) $ b) => ( 1724 case try_prove_real_eq false ectxt (a, b) of 1725 SOME _ => true 1726 | _ => false) 1727 | _ => false 1728 1729fun limit_of_expansion_bounds ectxt (bnds, basis) = 1730 let 1731 fun get_limit thm = 1732 limit_of_expansion (true, true) ectxt (thm, basis) |> snd |> concl_of' |> dest_fun |> dest_arg 1733 in 1734 case bnds of 1735 Exact thm => get_limit thm |> Exact_Limit 1736 | Bounds (l, u) => 1737 let 1738 val (llim, ulim) = apply2 (Option.map (fst #> get_limit)) (l, u) 1739 in 1740 case (llim, ulim) of 1741 (SOME llim', SOME ulim') => 1742 if lim_eq ectxt (llim', ulim') then Exact_Limit llim' else Limit_Bounds (llim, ulim) 1743 | _ => Limit_Bounds (llim, ulim) 1744 end 1745 end 1746 1747end 1748 1749structure Multiseries_Expansion_Bounds : EXPANSION_INTERFACE = 1750struct 1751open Multiseries_Expansion; 1752 1753type T = bounds 1754 1755val expand_term = expand_term_bounds 1756val expand_terms = expand_terms_bounds 1757 1758val prove_nhds = prove_nhds_bounds 1759val prove_at_infinity = prove_at_infinity_bounds 1760val prove_at_top = prove_at_top_bounds 1761val prove_at_bot = prove_at_bot_bounds 1762val prove_at_0 = prove_at_0_bounds 1763val prove_at_right_0 = prove_at_right_0_bounds 1764val prove_at_left_0 = prove_at_left_0_bounds 1765val prove_eventually_nonzero = prove_eventually_nonzero_bounds 1766 1767val prove_eventually_less = prove_eventually_less_bounds 1768val prove_eventually_greater = prove_eventually_greater_bounds 1769 1770val prove_smallo = prove_smallo_bounds 1771val prove_bigo = prove_bigo_bounds 1772val prove_bigtheta = prove_bigtheta_bounds 1773val prove_asymp_equiv = prove_asymp_equiv_bounds 1774 1775end 1776 1777structure Real_Asymp_Bounds = Real_Asymp(Multiseries_Expansion_Bounds)