176 This usually leads to nicer results. |
176 This usually leads to nicer results. |
177 *) |
177 *) |
178 datatype intyness = Nat of thm | Neg_Nat of thm | No_Nat |
178 datatype intyness = Nat of thm | Neg_Nat of thm | No_Nat |
179 |
179 |
180 fun get_intyness ctxt ct = |
180 fun get_intyness ctxt ct = |
181 if Thm.typ_of_cterm ct = @{typ Real.real} then |
181 if Thm.typ_of_cterm ct = \<^typ>\<open>Real.real\<close> then |
182 let |
182 let |
183 val ctxt' = put_simpset HOL_basic_ss ctxt addsimps @{thms intyness_simps} |
183 val ctxt' = put_simpset HOL_basic_ss ctxt addsimps @{thms intyness_simps} |
184 val conv = |
184 val conv = |
185 Simplifier.rewrite ctxt then_conv Simplifier.rewrite ctxt' |
185 Simplifier.rewrite ctxt then_conv Simplifier.rewrite ctxt' |
186 fun flip (Nat thm) = Neg_Nat (thm RS @{thm intyness_uminus}) |
186 fun flip (Nat thm) = Neg_Nat (thm RS @{thm intyness_uminus}) |
187 | flip _ = No_Nat |
187 | flip _ = No_Nat |
188 fun get_intyness' ct = |
188 fun get_intyness' ct = |
189 case Thm.term_of ct of |
189 case Thm.term_of ct of |
190 @{term "0::real"} => Nat @{thm intyness_0} |
190 \<^term>\<open>0::real\<close> => Nat @{thm intyness_0} |
191 | @{term "1::real"} => Nat @{thm intyness_1} |
191 | \<^term>\<open>1::real\<close> => Nat @{thm intyness_1} |
192 | Const (@{const_name numeral}, _) $ _ => |
192 | Const (\<^const_name>\<open>numeral\<close>, _) $ _ => |
193 Nat (Thm.reflexive (Thm.dest_arg ct) RS @{thm intyness_numeral}) |
193 Nat (Thm.reflexive (Thm.dest_arg ct) RS @{thm intyness_numeral}) |
194 | Const (@{const_name uminus}, _) $ _ => flip (get_intyness' (Thm.dest_arg ct)) |
194 | Const (\<^const_name>\<open>uminus\<close>, _) $ _ => flip (get_intyness' (Thm.dest_arg ct)) |
195 | Const (@{const_name of_nat}, _) $ _ => |
195 | Const (\<^const_name>\<open>of_nat\<close>, _) $ _ => |
196 Nat (Thm.reflexive (Thm.dest_arg ct) RS @{thm intyness_of_nat}) |
196 Nat (Thm.reflexive (Thm.dest_arg ct) RS @{thm intyness_of_nat}) |
197 | _ => No_Nat |
197 | _ => No_Nat |
198 val thm = conv ct |
198 val thm = conv ct |
199 val ct' = thm |> Thm.cprop_of |> Thm.dest_equals_rhs |
199 val ct' = thm |> Thm.cprop_of |> Thm.dest_equals_rhs |
200 in |
200 in |
227 | _ => raise THM ("get_parity", 0, [thm]) |
227 | _ => raise THM ("get_parity", 0, [thm]) |
228 end |
228 end |
229 val get_num = Thm.dest_arg o Thm.dest_arg |
229 val get_num = Thm.dest_arg o Thm.dest_arg |
230 in |
230 in |
231 case Thm.term_of ct of |
231 case Thm.term_of ct of |
232 Const (@{const_name Groups.zero}, _) => Even (inst @{thm even_zero} []) |
232 Const (\<^const_name>\<open>Groups.zero\<close>, _) => Even (inst @{thm even_zero} []) |
233 | Const (@{const_name Groups.one}, _) => Odd (inst @{thm odd_one} []) |
233 | Const (\<^const_name>\<open>Groups.one\<close>, _) => Odd (inst @{thm odd_one} []) |
234 | Const (@{const_name Num.numeral_class.numeral}, _) $ @{term "Num.One"} => |
234 | Const (\<^const_name>\<open>Num.numeral_class.numeral\<close>, _) $ \<^term>\<open>Num.One\<close> => |
235 Odd (inst @{thm odd_Numeral1} []) |
235 Odd (inst @{thm odd_Numeral1} []) |
236 | Const (@{const_name Num.numeral_class.numeral}, _) $ (@{term "Num.Bit0"} $ _) => |
236 | Const (\<^const_name>\<open>Num.numeral_class.numeral\<close>, _) $ (\<^term>\<open>Num.Bit0\<close> $ _) => |
237 Even (inst @{thm even_numeral} [get_num ct]) |
237 Even (inst @{thm even_numeral} [get_num ct]) |
238 | Const (@{const_name Num.numeral_class.numeral}, _) $ (@{term "Num.Bit1"} $ _) => |
238 | Const (\<^const_name>\<open>Num.numeral_class.numeral\<close>, _) $ (\<^term>\<open>Num.Bit1\<close> $ _) => |
239 Odd (inst @{thm odd_numeral} [get_num ct]) |
239 Odd (inst @{thm odd_numeral} [get_num ct]) |
240 | Const (@{const_name Groups.uminus}, _) $ _ => ( |
240 | Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ _ => ( |
241 case get_parity (Thm.dest_arg ct) of |
241 case get_parity (Thm.dest_arg ct) of |
242 Even thm => Even (@{thm even_uminusI} OF [thm]) |
242 Even thm => Even (@{thm even_uminusI} OF [thm]) |
243 | Odd thm => Odd (@{thm odd_uminusI} OF [thm]) |
243 | Odd thm => Odd (@{thm odd_uminusI} OF [thm]) |
244 | _ => Unknown_Parity) |
244 | _ => Unknown_Parity) |
245 | Const (@{const_name Groups.plus}, _) $ _ $ _ => ( |
245 | Const (\<^const_name>\<open>Groups.plus\<close>, _) $ _ $ _ => ( |
246 case apply2 get_parity (Thm.dest_binop ct) of |
246 case apply2 get_parity (Thm.dest_binop ct) of |
247 (Even thm1, Even thm2) => Even (@{thm even_addI(1)} OF [thm1, thm2]) |
247 (Even thm1, Even thm2) => Even (@{thm even_addI(1)} OF [thm1, thm2]) |
248 | (Odd thm1, Odd thm2) => Even (@{thm even_addI(2)} OF [thm1, thm2]) |
248 | (Odd thm1, Odd thm2) => Even (@{thm even_addI(2)} OF [thm1, thm2]) |
249 | (Even thm1, Odd thm2) => Odd (@{thm odd_addI(1)} OF [thm1, thm2]) |
249 | (Even thm1, Odd thm2) => Odd (@{thm odd_addI(1)} OF [thm1, thm2]) |
250 | (Odd thm1, Even thm2) => Odd (@{thm odd_addI(2)} OF [thm1, thm2]) |
250 | (Odd thm1, Even thm2) => Odd (@{thm odd_addI(2)} OF [thm1, thm2]) |
251 | _ => Unknown_Parity) |
251 | _ => Unknown_Parity) |
252 | Const (@{const_name Groups.minus}, _) $ _ $ _ => ( |
252 | Const (\<^const_name>\<open>Groups.minus\<close>, _) $ _ $ _ => ( |
253 case apply2 get_parity (Thm.dest_binop ct) of |
253 case apply2 get_parity (Thm.dest_binop ct) of |
254 (Even thm1, Even thm2) => Even (@{thm even_diffI(1)} OF [thm1, thm2]) |
254 (Even thm1, Even thm2) => Even (@{thm even_diffI(1)} OF [thm1, thm2]) |
255 | (Odd thm1, Odd thm2) => Even (@{thm even_diffI(2)} OF [thm1, thm2]) |
255 | (Odd thm1, Odd thm2) => Even (@{thm even_diffI(2)} OF [thm1, thm2]) |
256 | (Even thm1, Odd thm2) => Odd (@{thm odd_diffI(1)} OF [thm1, thm2]) |
256 | (Even thm1, Odd thm2) => Odd (@{thm odd_diffI(1)} OF [thm1, thm2]) |
257 | (Odd thm1, Even thm2) => Odd (@{thm odd_diffI(2)} OF [thm1, thm2]) |
257 | (Odd thm1, Even thm2) => Odd (@{thm odd_diffI(2)} OF [thm1, thm2]) |
258 | _ => Unknown_Parity) |
258 | _ => Unknown_Parity) |
259 | Const (@{const_name Groups.times}, _) $ _ $ _ => ( |
259 | Const (\<^const_name>\<open>Groups.times\<close>, _) $ _ $ _ => ( |
260 case apply2 get_parity (Thm.dest_binop ct) of |
260 case apply2 get_parity (Thm.dest_binop ct) of |
261 (Even thm1, _) => Even (@{thm even_multI(1)} OF [thm1]) |
261 (Even thm1, _) => Even (@{thm even_multI(1)} OF [thm1]) |
262 | (_, Even thm2) => Even (@{thm even_multI(2)} OF [thm2]) |
262 | (_, Even thm2) => Even (@{thm even_multI(2)} OF [thm2]) |
263 | (Odd thm1, Odd thm2) => Odd (@{thm odd_multI} OF [thm1, thm2]) |
263 | (Odd thm1, Odd thm2) => Odd (@{thm odd_multI} OF [thm1, thm2]) |
264 | _ => Unknown_Parity) |
264 | _ => Unknown_Parity) |
265 | Const (@{const_name Power.power}, _) $ _ $ _ => |
265 | Const (\<^const_name>\<open>Power.power\<close>, _) $ _ $ _ => |
266 let |
266 let |
267 val (a, n) = Thm.dest_binop ct |
267 val (a, n) = Thm.dest_binop ct |
268 in |
268 in |
269 case get_parity a of |
269 case get_parity a of |
270 Odd thm => Odd (inst @{thm odd_powerI} [a, n] OF [thm]) |
270 Odd thm => Odd (inst @{thm odd_powerI} [a, n] OF [thm]) |
316 expr |> dest_comb |> fst |> dest_comb |> snd |> dest_comb |> fst |> dest_comb |> snd |
316 expr |> dest_comb |> fst |> dest_comb |> snd |> dest_comb |> fst |> dest_comb |> snd |
317 |> dest_comb |> snd |
317 |> dest_comb |> snd |
318 |
318 |
319 (* Returns the list of exponents of the leading term *) |
319 (* Returns the list of exponents of the leading term *) |
320 fun get_exponents exp = |
320 fun get_exponents exp = |
321 if fastype_of exp = @{typ real} then |
321 if fastype_of exp = \<^typ>\<open>real\<close> then |
322 [] |
322 [] |
323 else |
323 else |
324 get_exponent exp :: get_exponents (get_coeff exp) |
324 get_exponent exp :: get_exponents (get_coeff exp) |
325 |
325 |
326 (* Returns the function that the expansion corresponds to *) |
326 (* Returns the function that the expansion corresponds to *) |
327 fun get_eval expr = |
327 fun get_eval expr = |
328 if fastype_of expr = @{typ real} then |
328 if fastype_of expr = \<^typ>\<open>real\<close> then |
329 Abs ("x", @{typ real}, expr) |
329 Abs ("x", \<^typ>\<open>real\<close>, expr) |
330 else |
330 else |
331 expr |> dest_comb |> snd |
331 expr |> dest_comb |> snd |
332 |
332 |
333 val eval_simps = @{thms eval_simps [THEN eq_reflection]} |
333 val eval_simps = @{thms eval_simps [THEN eq_reflection]} |
334 |
334 |
335 (* Tries to prove that the given function is eventually zero *) |
335 (* Tries to prove that the given function is eventually zero *) |
336 fun ev_zeroness_oracle ectxt t = |
336 fun ev_zeroness_oracle ectxt t = |
337 let |
337 let |
338 val ctxt = Lazy_Eval.get_ctxt ectxt |
338 val ctxt = Lazy_Eval.get_ctxt ectxt |
339 val goal = |
339 val goal = |
340 betapply (@{term "\<lambda>f::real \<Rightarrow> real. eventually (\<lambda>x. f x = 0) at_top"}, t) |
340 betapply (\<^term>\<open>\<lambda>f::real \<Rightarrow> real. eventually (\<lambda>x. f x = 0) at_top\<close>, t) |
341 |> HOLogic.mk_Trueprop |
341 |> HOLogic.mk_Trueprop |
342 fun tac {context = ctxt, ...} = |
342 fun tac {context = ctxt, ...} = |
343 HEADGOAL (Method.insert_tac ctxt (get_facts ectxt)) |
343 HEADGOAL (Method.insert_tac ctxt (get_facts ectxt)) |
344 THEN Local_Defs.unfold_tac ctxt eval_simps |
344 THEN Local_Defs.unfold_tac ctxt eval_simps |
345 THEN HEADGOAL (Simplifier.asm_full_simp_tac ctxt) |
345 THEN HEADGOAL (Simplifier.asm_full_simp_tac ctxt) |
360 thrown if this fails. |
360 thrown if this fails. |
361 *) |
361 *) |
362 fun zeroness_oracle fail mode ectxt exp = |
362 fun zeroness_oracle fail mode ectxt exp = |
363 let |
363 let |
364 val ctxt = Lazy_Eval.get_ctxt ectxt |
364 val ctxt = Lazy_Eval.get_ctxt ectxt |
365 val eq = (exp, @{term "0::real"}) |> HOLogic.mk_eq |
365 val eq = (exp, \<^term>\<open>0::real\<close>) |> HOLogic.mk_eq |
366 val goal1 = (IsZero, eq |> HOLogic.mk_Trueprop) |
366 val goal1 = (IsZero, eq |> HOLogic.mk_Trueprop) |
367 val goal2 = |
367 val goal2 = |
368 case mode of |
368 case mode of |
369 SOME Pos_Trim => |
369 SOME Pos_Trim => |
370 (IsPos, @{term "(<) (0::real)"} $ exp |> HOLogic.mk_Trueprop) |
370 (IsPos, \<^term>\<open>(<) (0::real)\<close> $ exp |> HOLogic.mk_Trueprop) |
371 | SOME Sgn_Trim => |
371 | SOME Sgn_Trim => |
372 (IsPos, @{term "(<) (0::real)"} $ exp |> HOLogic.mk_Trueprop) |
372 (IsPos, \<^term>\<open>(<) (0::real)\<close> $ exp |> HOLogic.mk_Trueprop) |
373 | SOME Neg_Trim => |
373 | SOME Neg_Trim => |
374 (IsNeg, betapply (@{term "\<lambda>x. x < (0::real)"}, exp) |> HOLogic.mk_Trueprop) |
374 (IsNeg, betapply (\<^term>\<open>\<lambda>x. x < (0::real)\<close>, exp) |> HOLogic.mk_Trueprop) |
375 | _ => |
375 | _ => |
376 (IsNonZero, eq |> HOLogic.mk_not |> HOLogic.mk_Trueprop) |
376 (IsNonZero, eq |> HOLogic.mk_not |> HOLogic.mk_Trueprop) |
377 val goals = |
377 val goals = |
378 (if mode = SOME Sgn_Trim then |
378 (if mode = SOME Sgn_Trim then |
379 [(IsNeg, betapply (@{term "\<lambda>x. x < (0::real)"}, exp) |> HOLogic.mk_Trueprop)] |
379 [(IsNeg, betapply (\<^term>\<open>\<lambda>x. x < (0::real)\<close>, exp) |> HOLogic.mk_Trueprop)] |
380 else |
380 else |
381 []) |
381 []) |
382 val goals = goal2 :: goals |
382 val goals = goal2 :: goals |
383 fun tac {context = ctxt, ...} = |
383 fun tac {context = ctxt, ...} = |
384 HEADGOAL (Method.insert_tac ctxt (get_facts ectxt)) |
384 HEADGOAL (Method.insert_tac ctxt (get_facts ectxt)) |
441 end |
441 end |
442 |
442 |
443 (* Tries to prove a given eventual equality of real functions. *) |
443 (* Tries to prove a given eventual equality of real functions. *) |
444 fun try_prove_ev_eq ectxt (f, g) = |
444 fun try_prove_ev_eq ectxt (f, g) = |
445 let |
445 let |
446 val t = Envir.beta_eta_contract (@{term "\<lambda>(f::real=>real) g x. f x - g x"} $ f $ g) |
446 val t = Envir.beta_eta_contract (\<^term>\<open>\<lambda>(f::real=>real) g x. f x - g x\<close> $ f $ g) |
447 in |
447 in |
448 Option.map (fn thm => thm RS @{thm eventually_diff_zero_imp_eq}) (ev_zeroness_oracle ectxt t) |
448 Option.map (fn thm => thm RS @{thm eventually_diff_zero_imp_eq}) (ev_zeroness_oracle ectxt t) |
449 end |
449 end |
450 |
450 |
451 fun real_less a b = @{term "(<) :: real \<Rightarrow> real \<Rightarrow> bool"} $ a $ b |
451 fun real_less a b = \<^term>\<open>(<) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ a $ b |
452 fun real_eq a b = @{term "(=) :: real \<Rightarrow> real \<Rightarrow> bool"} $ a $ b |
452 fun real_eq a b = \<^term>\<open>(=) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ a $ b |
453 fun real_neq a b = @{term "(\<noteq>) :: real \<Rightarrow> real \<Rightarrow> bool"} $ a $ b |
453 fun real_neq a b = \<^term>\<open>(\<noteq>) :: real \<Rightarrow> real \<Rightarrow> bool\<close> $ a $ b |
454 |
454 |
455 (* The hook that is called by the Lazy_Eval module whenever two real numbers have to be compared *) |
455 (* The hook that is called by the Lazy_Eval module whenever two real numbers have to be compared *) |
456 fun real_sgn_hook ({pctxt = ctxt, facts, verbose, ...}) t = |
456 fun real_sgn_hook ({pctxt = ctxt, facts, verbose, ...}) t = |
457 let |
457 let |
458 val get_rhs = Thm.concl_of #> Logic.dest_equals #> snd |
458 val get_rhs = Thm.concl_of #> Logic.dest_equals #> snd |
511 All constructors on which pattern matching is performed need to be registered for evaluation |
511 All constructors on which pattern matching is performed need to be registered for evaluation |
512 to work. It should be rare for users to add additional ones. |
512 to work. It should be rare for users to add additional ones. |
513 *) |
513 *) |
514 fun get_constructors ctxt = |
514 fun get_constructors ctxt = |
515 let |
515 let |
516 val thms = Named_Theorems.get ctxt @{named_theorems exp_log_eval_constructor} |
516 val thms = Named_Theorems.get ctxt \<^named_theorems>\<open>exp_log_eval_constructor\<close> |
517 fun go _ [] acc = rev acc |
517 fun go _ [] acc = rev acc |
518 | go f (x :: xs) acc = |
518 | go f (x :: xs) acc = |
519 case f x of |
519 case f x of |
520 NONE => go f xs acc |
520 NONE => go f xs acc |
521 | SOME y => go f xs (y :: acc) |
521 | SOME y => go f xs (y :: acc) |
522 fun map_option f xs = go f xs [] |
522 fun map_option f xs = go f xs [] |
523 fun dest_constructor thm = |
523 fun dest_constructor thm = |
524 case Thm.concl_of thm of |
524 case Thm.concl_of thm of |
525 Const (@{const_name HOL.Trueprop}, _) $ |
525 Const (\<^const_name>\<open>HOL.Trueprop\<close>, _) $ |
526 (Const (@{const_name REAL_ASYMP_EVAL_CONSTRUCTOR}, _) $ Const (c, T)) => |
526 (Const (\<^const_name>\<open>REAL_ASYMP_EVAL_CONSTRUCTOR\<close>, _) $ Const (c, T)) => |
527 SOME (c, length (fst (strip_type T))) |
527 SOME (c, length (fst (strip_type T))) |
528 | _ => NONE |
528 | _ => NONE |
529 in |
529 in |
530 thms |> map_option dest_constructor |
530 thms |> map_option dest_constructor |
531 end |
531 end |
563 val (_, _, conv) = match ectxt exp_pat exp (SOME []) |
563 val (_, _, conv) = match ectxt exp_pat exp (SOME []) |
564 val eq_thm = conv (Thm.cterm_of ctxt exp) |
564 val eq_thm = conv (Thm.cterm_of ctxt exp) |
565 val exp' = eq_thm |> Thm.concl_of |> Logic.dest_equals |> snd |
565 val exp' = eq_thm |> Thm.concl_of |> Logic.dest_equals |> snd |
566 in |
566 in |
567 case exp' of |
567 case exp' of |
568 Const (@{const_name MS}, _) $ (Const (@{const_name MSLCons}, _) $ |
568 Const (\<^const_name>\<open>MS\<close>, _) $ (Const (\<^const_name>\<open>MSLCons\<close>, _) $ |
569 (Const (@{const_name Pair}, _) $ c $ _) $ _) $ _ => |
569 (Const (\<^const_name>\<open>Pair\<close>, _) $ c $ _) $ _) $ _ => |
570 (SOME c, @{thm expands_to_meta_eq_cong} OF [thm, eq_thm], eq_thm) |
570 (SOME c, @{thm expands_to_meta_eq_cong} OF [thm, eq_thm], eq_thm) |
571 | Const (@{const_name MS}, _) $ Const (@{const_name MSLNil}, _) $ _ => |
571 | Const (\<^const_name>\<open>MS\<close>, _) $ Const (\<^const_name>\<open>MSLNil\<close>, _) $ _ => |
572 (NONE, @{thm expands_to_meta_eq_cong} OF [thm, eq_thm], eq_thm) |
572 (NONE, @{thm expands_to_meta_eq_cong} OF [thm, eq_thm], eq_thm) |
573 | _ => raise TERM ("whnf_expansion", [exp']) |
573 | _ => raise TERM ("whnf_expansion", [exp']) |
574 end |
574 end |
575 |
575 |
576 fun try_lift_function ectxt (thm, SEmpty) _ = (NONE, thm) |
576 fun try_lift_function ectxt (thm, SEmpty) _ = (NONE, thm) |
620 val exp = get_expansion thm |
620 val exp = get_expansion thm |
621 val ctxt = get_ctxt ectxt |
621 val ctxt = get_ctxt ectxt |
622 val eq_thm = Simplifier.rewrite ctxt (Thm.cterm_of ctxt exp) |
622 val eq_thm = Simplifier.rewrite ctxt (Thm.cterm_of ctxt exp) |
623 val trimmed_cong_thm = |
623 val trimmed_cong_thm = |
624 case trimmed_thm |> concl_of' |> dest_fun of |
624 case trimmed_thm |> concl_of' |> dest_fun of |
625 Const (@{const_name trimmed}, _) => @{thm trimmed_eq_cong} |
625 Const (\<^const_name>\<open>trimmed\<close>, _) => @{thm trimmed_eq_cong} |
626 | Const (@{const_name trimmed_pos}, _) => @{thm trimmed_pos_eq_cong} |
626 | Const (\<^const_name>\<open>trimmed_pos\<close>, _) => @{thm trimmed_pos_eq_cong} |
627 | Const (@{const_name trimmed_neg}, _) => @{thm trimmed_neg_eq_cong} |
627 | Const (\<^const_name>\<open>trimmed_neg\<close>, _) => @{thm trimmed_neg_eq_cong} |
628 | _ => raise THM ("simplify_trimmed_expansion", 2, [thm, trimmed_thm]) |
628 | _ => raise THM ("simplify_trimmed_expansion", 2, [thm, trimmed_thm]) |
629 in |
629 in |
630 (@{thm expands_to_meta_eq_cong} OF [thm, eq_thm], |
630 (@{thm expands_to_meta_eq_cong} OF [thm, eq_thm], |
631 trimmed_cong_thm OF [trimmed_thm, eq_thm]) |
631 trimmed_cong_thm OF [trimmed_thm, eq_thm]) |
632 end |
632 end |
669 *) |
669 *) |
670 fun try_drop_leading_term_ex fail ectxt thm = |
670 fun try_drop_leading_term_ex fail ectxt thm = |
671 let |
671 let |
672 val exp = get_expansion thm |
672 val exp = get_expansion thm |
673 in |
673 in |
674 if fastype_of exp = @{typ real} then |
674 if fastype_of exp = \<^typ>\<open>real\<close> then |
675 NONE |
675 NONE |
676 else if fastype_of (get_coeff exp) = @{typ real} then |
676 else if fastype_of (get_coeff exp) = \<^typ>\<open>real\<close> then |
677 case zeroness_oracle fail (SOME Simple_Trim) ectxt (get_coeff exp) of |
677 case zeroness_oracle fail (SOME Simple_Trim) ectxt (get_coeff exp) of |
678 (IsZero, SOME zero_thm) => SOME (@{thm drop_zero_ms'} OF [zero_thm, thm]) |
678 (IsZero, SOME zero_thm) => SOME (@{thm drop_zero_ms'} OF [zero_thm, thm]) |
679 | _ => NONE |
679 | _ => NONE |
680 else |
680 else |
681 let |
681 let |
682 val c = get_coeff exp |
682 val c = get_coeff exp |
683 val T = fastype_of c |
683 val T = fastype_of c |
684 val t = Const (@{const_name eval}, T --> @{typ "real \<Rightarrow> real"}) $ c |
684 val t = Const (\<^const_name>\<open>eval\<close>, T --> \<^typ>\<open>real \<Rightarrow> real\<close>) $ c |
685 in |
685 in |
686 case ev_zeroness_oracle ectxt t of |
686 case ev_zeroness_oracle ectxt t of |
687 SOME zero_thm => SOME (@{thm expands_to_drop_zero} OF [zero_thm, thm]) |
687 SOME zero_thm => SOME (@{thm expands_to_drop_zero} OF [zero_thm, thm]) |
688 | _ => NONE |
688 | _ => NONE |
689 end |
689 end |
785 | _ => raise TERM ("Unexpected zeroness result in trim_expansion", [])) |
785 | _ => raise TERM ("Unexpected zeroness result in trim_expansion", [])) |
786 fun do_trim es = |
786 fun do_trim es = |
787 let |
787 let |
788 val c = the c |
788 val c = the c |
789 val T = fastype_of c |
789 val T = fastype_of c |
790 val t = Const (@{const_name eval}, T --> @{typ "real \<Rightarrow> real"}) $ c |
790 val t = Const (\<^const_name>\<open>eval\<close>, T --> \<^typ>\<open>real \<Rightarrow> real\<close>) $ c |
791 in |
791 in |
792 if T = @{typ real} then ( |
792 if T = \<^typ>\<open>real\<close> then ( |
793 case zeroness_oracle fail mode ectxt c of |
793 case zeroness_oracle fail mode ectxt c of |
794 (IsZero, SOME zero_thm) => |
794 (IsZero, SOME zero_thm) => |
795 trim_expansion_while_greater strict es fail mode ectxt |
795 trim_expansion_while_greater strict es fail mode ectxt |
796 (@{thm drop_zero_ms'} OF [zero_thm, thm], basis) |
796 (@{thm drop_zero_ms'} OF [zero_thm, thm], basis) |
797 | (nz, SOME nz_thm) => (thm, Trimmed (nz, SOME (nz_thm RS trimmed_real_thm nz)), []) |
797 | (nz, SOME nz_thm) => (thm, Trimmed (nz, SOME (nz_thm RS trimmed_real_thm nz)), []) |
840 SOME thm => |
840 SOME thm => |
841 trim_expansion_while_greater strict es fail mode ectxt (thm, basis) |
841 trim_expansion_while_greater strict es fail mode ectxt (thm, basis) |
842 | NONE => do_trim NONE |> @{apply 3(3)} (fn thms => (IsPos, pos_thm) :: thms)) |
842 | NONE => do_trim NONE |> @{apply 3(3)} (fn thms => (IsPos, pos_thm) :: thms)) |
843 | (IsNeg, SOME neg_thm) => (thm, Aborted LESS, [(IsNeg, neg_thm)]) |
843 | (IsNeg, SOME neg_thm) => (thm, Aborted LESS, [(IsNeg, neg_thm)]) |
844 | (IsZero, SOME zero_thm) => |
844 | (IsZero, SOME zero_thm) => |
845 if not strict andalso fastype_of c = @{typ real} then |
845 if not strict andalso fastype_of c = \<^typ>\<open>real\<close> then |
846 (thm, Aborted EQUAL, [(IsZero, zero_thm)]) |
846 (thm, Aborted EQUAL, [(IsZero, zero_thm)]) |
847 else ( |
847 else ( |
848 case try_drop_leading_term_ex false ectxt thm of |
848 case try_drop_leading_term_ex false ectxt thm of |
849 SOME thm => trim_expansion_while_greater strict es fail mode ectxt (thm, basis) |
849 SOME thm => trim_expansion_while_greater strict es fail mode ectxt (thm, basis) |
850 | NONE => (do_trim es |> @{apply 3(3)} (fn thms => (IsZero, zero_thm) :: thms))) |
850 | NONE => (do_trim es |> @{apply 3(3)} (fn thms => (IsZero, zero_thm) :: thms))) |
898 case nz of |
898 case nz of |
899 IsPos => @{thm lift_trimmed_pos} |
899 IsPos => @{thm lift_trimmed_pos} |
900 | IsNeg => @{thm lift_trimmed_neg} |
900 | IsNeg => @{thm lift_trimmed_neg} |
901 | _ => raise TERM ("Unexpected zeroness result in compare_expansions'", []) |
901 | _ => raise TERM ("Unexpected zeroness result in compare_expansions'", []) |
902 val (e1, e2) = apply2 (get_expansion #> get_exponent) (thm1, thm2) |
902 val (e1, e2) = apply2 (get_expansion #> get_exponent) (thm1, thm2) |
903 val e = @{term "(-) :: real => _"} $ e1 $ e2 |
903 val e = \<^term>\<open>(-) :: real => _\<close> $ e1 $ e2 |
904 fun trim thm = trim_expansion true (SOME Sgn_Trim) ectxt (thm, basis) |
904 fun trim thm = trim_expansion true (SOME Sgn_Trim) ectxt (thm, basis) |
905 val try_drop = Option.map (whnf_expansion ectxt #> #2) o try_drop_leading_term_ex false ectxt |
905 val try_drop = Option.map (whnf_expansion ectxt #> #2) o try_drop_leading_term_ex false ectxt |
906 fun handle_result ord zeroness trimmed_thm thm1 thm2 = |
906 fun handle_result ord zeroness trimmed_thm thm1 thm2 = |
907 let |
907 let |
908 val (e1, e2) = apply2 (get_expansion #> get_exponent) (thm1, thm2) |
908 val (e1, e2) = apply2 (get_expansion #> get_exponent) (thm1, thm2) |
909 val e = @{term "(-) :: real => _"} $ e1 $ e2 |
909 val e = \<^term>\<open>(-) :: real => _\<close> $ e1 $ e2 |
910 val mode = if ord = LESS then Neg_Trim else Pos_Trim |
910 val mode = if ord = LESS then Neg_Trim else Pos_Trim |
911 in |
911 in |
912 case zeroness_oracle true (SOME mode) ectxt e of |
912 case zeroness_oracle true (SOME mode) ectxt e of |
913 (_, SOME e_thm) => Cmp_Dominated (ord, [e_thm], zeroness, trimmed_thm, thm1, thm2) |
913 (_, SOME e_thm) => Cmp_Dominated (ord, [e_thm], zeroness, trimmed_thm, thm1, thm2) |
914 | _ => raise Match |
914 | _ => raise Match |
973 | EQUAL => @{thm compare_expansions_same_exp[OF _ compare_expansions_real]} OF [thm]) |
973 | EQUAL => @{thm compare_expansions_same_exp[OF _ compare_expansions_real]} OF [thm]) |
974 | prove_compare_expansions ord (thm :: thms) = |
974 | prove_compare_expansions ord (thm :: thms) = |
975 @{thm compare_expansions_same_exp} OF [thm, prove_compare_expansions ord thms] |
975 @{thm compare_expansions_same_exp} OF [thm, prove_compare_expansions ord thms] |
976 | prove_compare_expansions _ [] = raise Match |
976 | prove_compare_expansions _ [] = raise Match |
977 |
977 |
978 val ev_zero_pos_thm = Eventuallize.eventuallize @{context} |
978 val ev_zero_pos_thm = Eventuallize.eventuallize \<^context> |
979 @{lemma "\<forall>x::real. f x = 0 \<longrightarrow> g x > 0 \<longrightarrow> f x < g x" by auto} NONE |
979 @{lemma "\<forall>x::real. f x = 0 \<longrightarrow> g x > 0 \<longrightarrow> f x < g x" by auto} NONE |
980 OF @{thms _ expands_to_imp_eventually_pos} |
980 OF @{thms _ expands_to_imp_eventually_pos} |
981 |
981 |
982 val ev_zero_neg_thm = Eventuallize.eventuallize @{context} |
982 val ev_zero_neg_thm = Eventuallize.eventuallize \<^context> |
983 @{lemma "\<forall>x::real. f x = 0 \<longrightarrow> g x < 0 \<longrightarrow> f x > g x" by auto} NONE |
983 @{lemma "\<forall>x::real. f x = 0 \<longrightarrow> g x < 0 \<longrightarrow> f x > g x" by auto} NONE |
984 OF @{thms _ expands_to_imp_eventually_neg} |
984 OF @{thms _ expands_to_imp_eventually_neg} |
985 |
985 |
986 val ev_zero_zero_thm = Eventuallize.eventuallize @{context} |
986 val ev_zero_zero_thm = Eventuallize.eventuallize \<^context> |
987 @{lemma "\<forall>x::real. f x = 0 \<longrightarrow> g x = 0 \<longrightarrow> f x = g x" by auto} NONE |
987 @{lemma "\<forall>x::real. f x = 0 \<longrightarrow> g x = 0 \<longrightarrow> f x = g x" by auto} NONE |
988 |
988 |
989 fun compare_expansions_trivial ectxt (thm1, thm2, basis) = |
989 fun compare_expansions_trivial ectxt (thm1, thm2, basis) = |
990 case try_prove_ev_eq ectxt (apply2 get_expanded_fun (thm1, thm2)) of |
990 case try_prove_ev_eq ectxt (apply2 get_expanded_fun (thm1, thm2)) of |
991 SOME thm => SOME (EQUAL, thm, thm1, thm2) |
991 SOME thm => SOME (EQUAL, thm, thm1, thm2) |
1195 |
1195 |
1196 (* inserts the exponential of a given function at the beginning of the given basis *) |
1196 (* inserts the exponential of a given function at the beginning of the given basis *) |
1197 fun insert_exp _ _ _ _ _ SEmpty = raise TERM ("insert_exp", []) |
1197 fun insert_exp _ _ _ _ _ SEmpty = raise TERM ("insert_exp", []) |
1198 | insert_exp t ln_thm ln_smallo_thm ln_trimmed_thm lim_thm (SNE basis) = |
1198 | insert_exp t ln_thm ln_smallo_thm ln_trimmed_thm lim_thm (SNE basis) = |
1199 let |
1199 let |
1200 val head = Envir.beta_eta_contract (@{term "\<lambda>(f::real\<Rightarrow>real) x. exp (f x)"} $ t) |
1200 val head = Envir.beta_eta_contract (\<^term>\<open>\<lambda>(f::real\<Rightarrow>real) x. exp (f x)\<close> $ t) |
1201 val ln_smallo_thm = ln_smallo_thm RS @{thm ln_smallo_ln_exp} |
1201 val ln_smallo_thm = ln_smallo_thm RS @{thm ln_smallo_ln_exp} |
1202 val wf_thm = @{thm basis_wf_manyI} OF [lim_thm, ln_smallo_thm, get_basis_wf_thm' basis] |
1202 val wf_thm = @{thm basis_wf_manyI} OF [lim_thm, ln_smallo_thm, get_basis_wf_thm' basis] |
1203 val basis' = SNE (SCons ({wf_thm = wf_thm, head = head}, |
1203 val basis' = SNE (SCons ({wf_thm = wf_thm, head = head}, |
1204 {ln_thm = ln_thm, trimmed_thm = ln_trimmed_thm} , basis)) |
1204 {ln_thm = ln_thm, trimmed_thm = ln_trimmed_thm} , basis)) |
1205 in |
1205 in |
1579 @{thm expands_to_root} OF [nz_thm, trimmed_thm, get_basis_wf_thm basis, thm] |
1579 @{thm expands_to_root} OF [nz_thm, trimmed_thm, get_basis_wf_thm basis, thm] |
1580 | (thm, IsNeg, SOME trimmed_thm) => |
1580 | (thm, IsNeg, SOME trimmed_thm) => |
1581 @{thm expands_to_root_neg} OF [nz_thm, trimmed_thm, get_basis_wf_thm basis, thm] |
1581 @{thm expands_to_root_neg} OF [nz_thm, trimmed_thm, get_basis_wf_thm basis, thm] |
1582 | _ => raise TERM ("Unexpected zeroness result in root_expansion", []) |
1582 | _ => raise TERM ("Unexpected zeroness result in root_expansion", []) |
1583 in |
1583 in |
1584 case prove @{term "\<lambda>n::nat. n = 0"} of |
1584 case prove \<^term>\<open>\<lambda>n::nat. n = 0\<close> of |
1585 SOME zero_thm => |
1585 SOME zero_thm => |
1586 @{thm expands_to_0th_root} OF |
1586 @{thm expands_to_0th_root} OF |
1587 [zero_thm, get_basis_wf_thm basis, mk_expansion_level_eq_thm basis, |
1587 [zero_thm, get_basis_wf_thm basis, mk_expansion_level_eq_thm basis, |
1588 Thm.reflexive (Thm.cterm_of ctxt (get_expanded_fun thm))] |
1588 Thm.reflexive (Thm.cterm_of ctxt (get_expanded_fun thm))] |
1589 | NONE => |
1589 | NONE => |
1590 case prove @{term "\<lambda>n::nat. n > 0"} of |
1590 case prove \<^term>\<open>\<lambda>n::nat. n > 0\<close> of |
1591 NONE => err () |
1591 NONE => err () |
1592 | SOME nz_thm => |
1592 | SOME nz_thm => |
1593 case ev_zeroness_oracle ectxt (get_expanded_fun thm) of |
1593 case ev_zeroness_oracle ectxt (get_expanded_fun thm) of |
1594 SOME zero_thm => @{thm expands_to_root_0} OF |
1594 SOME zero_thm => @{thm expands_to_root_0} OF |
1595 [nz_thm, zero_thm, get_basis_wf_thm basis, mk_expansion_level_eq_thm basis] |
1595 [nz_thm, zero_thm, get_basis_wf_thm basis, mk_expansion_level_eq_thm basis] |
1915 datatype limit = |
1915 datatype limit = |
1916 Zero_Limit of bool option |
1916 Zero_Limit of bool option |
1917 | Finite_Limit of term |
1917 | Finite_Limit of term |
1918 | Infinite_Limit of bool option |
1918 | Infinite_Limit of bool option |
1919 |
1919 |
1920 fun is_empty_expansion (Const (@{const_name MS}, _) $ Const (@{const_name MSLNil}, _) $ _) = true |
1920 fun is_empty_expansion (Const (\<^const_name>\<open>MS\<close>, _) $ Const (\<^const_name>\<open>MSLNil\<close>, _) $ _) = true |
1921 | is_empty_expansion _ = false |
1921 | is_empty_expansion _ = false |
1922 |
1922 |
1923 fun limit_of_expansion_aux ectxt basis thm = |
1923 fun limit_of_expansion_aux ectxt basis thm = |
1924 let |
1924 let |
1925 val n = length (get_basis_list basis) |
1925 val n = length (get_basis_list basis) |
1926 val (thm, res, e_thms) = |
1926 val (thm, res, e_thms) = |
1927 trim_expansion_while_greater false (SOME (replicate n @{term "0::real"})) true |
1927 trim_expansion_while_greater false (SOME (replicate n \<^term>\<open>0::real\<close>)) true |
1928 (SOME Simple_Trim) ectxt (thm, basis) |
1928 (SOME Simple_Trim) ectxt (thm, basis) |
1929 val trimmed_thm = case res of Trimmed (_, trimmed_thm) => trimmed_thm | _ => NONE |
1929 val trimmed_thm = case res of Trimmed (_, trimmed_thm) => trimmed_thm | _ => NONE |
1930 val res = case res of Trimmed _ => GREATER | Aborted res => res |
1930 val res = case res of Trimmed _ => GREATER | Aborted res => res |
1931 val exp = get_expansion thm |
1931 val exp = get_expansion thm |
1932 val _ = if res = GREATER andalso is_none trimmed_thm andalso not (is_empty_expansion exp) then |
1932 val _ = if res = GREATER andalso is_none trimmed_thm andalso not (is_empty_expansion exp) then |
1933 raise TERM ("limit_of_expansion", [get_expansion thm]) else () |
1933 raise TERM ("limit_of_expansion", [get_expansion thm]) else () |
1934 fun go thm _ _ [] = ( |
1934 fun go thm _ _ [] = ( |
1935 case zeroness_oracle false (SOME Simple_Trim) ectxt (get_expansion thm) of |
1935 case zeroness_oracle false (SOME Simple_Trim) ectxt (get_expansion thm) of |
1936 (IsZero, _) => (Zero_Limit NONE, @{thm expands_to_real_imp_filterlim} OF [thm]) |
1936 (IsZero, _) => (Zero_Limit NONE, @{thm expands_to_real_imp_filterlim} OF [thm]) |
1937 | _ => (Finite_Limit @{term "0::real"}, @{thm expands_to_real_imp_filterlim} OF [thm])) |
1937 | _ => (Finite_Limit \<^term>\<open>0::real\<close>, @{thm expands_to_real_imp_filterlim} OF [thm])) |
1938 | go thm _ basis ((IsNeg, neg_thm) :: _) = (Zero_Limit NONE, |
1938 | go thm _ basis ((IsNeg, neg_thm) :: _) = (Zero_Limit NONE, |
1939 @{thm expands_to_neg_exponent_imp_filterlim} OF |
1939 @{thm expands_to_neg_exponent_imp_filterlim} OF |
1940 [thm, get_basis_wf_thm basis, neg_thm RS @{thm compare_reals_diff_sgnD(1)}]) |
1940 [thm, get_basis_wf_thm basis, neg_thm RS @{thm compare_reals_diff_sgnD(1)}]) |
1941 | go thm trimmed_thm basis ((IsPos, pos_thm) :: _) = (Infinite_Limit NONE, |
1941 | go thm trimmed_thm basis ((IsPos, pos_thm) :: _) = (Infinite_Limit NONE, |
1942 @{thm expands_to_pos_exponent_imp_filterlim} OF |
1942 @{thm expands_to_pos_exponent_imp_filterlim} OF |
2033 fun err () = raise TERM (s, [get_expanded_fun thm]) |
2033 fun err () = raise TERM (s, [get_expanded_fun thm]) |
2034 val (thm, _, SOME trimmed_thm) = trim_expansion true (SOME mode) ectxt (thm, basis) |
2034 val (thm, _, SOME trimmed_thm) = trim_expansion true (SOME mode) ectxt (thm, basis) |
2035 val trimmed_thm' = trimmed_thm RS |
2035 val trimmed_thm' = trimmed_thm RS |
2036 (if mode = Pos_Trim then @{thm trimmed_pos_imp_trimmed} else @{thm trimmed_neg_imp_trimmed}) |
2036 (if mode = Pos_Trim then @{thm trimmed_pos_imp_trimmed} else @{thm trimmed_neg_imp_trimmed}) |
2037 fun go basis thm trimmed_thm = |
2037 fun go basis thm trimmed_thm = |
2038 if fastype_of (get_expansion thm) = @{typ "real"} then |
2038 if fastype_of (get_expansion thm) = \<^typ>\<open>real\<close> then |
2039 err () |
2039 err () |
2040 else |
2040 else |
2041 case zeroness_oracle true (SOME Pos_Trim) ectxt (get_exponent (get_expansion thm)) of |
2041 case zeroness_oracle true (SOME Pos_Trim) ectxt (get_exponent (get_expansion thm)) of |
2042 (IsPos, SOME pos_thm) => |
2042 (IsPos, SOME pos_thm) => |
2043 @{thm expands_to_pos_exponent_imp_filterlim} OF |
2043 @{thm expands_to_pos_exponent_imp_filterlim} OF |
2127 |
2127 |
2128 fun prove_equivalent theta ectxt (thm1, thm2, basis) = |
2128 fun prove_equivalent theta ectxt (thm1, thm2, basis) = |
2129 let |
2129 let |
2130 val ((thm1, _, SOME trimmed_thm1), (thm2, _, SOME trimmed_thm2)) = |
2130 val ((thm1, _, SOME trimmed_thm1), (thm2, _, SOME trimmed_thm2)) = |
2131 apply2 (trim_expansion true (SOME Simple_Trim) ectxt) ((thm1, basis), (thm2, basis)) |
2131 apply2 (trim_expansion true (SOME Simple_Trim) ectxt) ((thm1, basis), (thm2, basis)) |
2132 val pat = ConsPat (@{const_name Pair}, [ConsPat (@{const_name Lazy_Eval.cmp_result.EQ}, []), |
2132 val pat = ConsPat (\<^const_name>\<open>Pair\<close>, [ConsPat (\<^const_name>\<open>Lazy_Eval.cmp_result.EQ\<close>, []), |
2133 ConsPat (@{const_name Pair}, [AnyPat ("_", 0), AnyPat ("_", 0)])]) |
2133 ConsPat (\<^const_name>\<open>Pair\<close>, [AnyPat ("_", 0), AnyPat ("_", 0)])]) |
2134 val (exp1, exp2) = apply2 get_expansion (thm1, thm2) |
2134 val (exp1, exp2) = apply2 get_expansion (thm1, thm2) |
2135 val T = fastype_of exp1 |
2135 val T = fastype_of exp1 |
2136 val t = mk_compare_expansions_const T $ exp1 $ exp2 |
2136 val t = mk_compare_expansions_const T $ exp1 $ exp2 |
2137 fun eq_thm conv = HOLogic.mk_obj_eq (conv (Thm.cterm_of (get_ctxt ectxt) t)) |
2137 fun eq_thm conv = HOLogic.mk_obj_eq (conv (Thm.cterm_of (get_ctxt ectxt) t)) |
2138 val imp_thm = |
2138 val imp_thm = |
2231 | _ => raise TERM ("prove_eventually_nonzero", [get_expanded_fun thm]) |
2231 | _ => raise TERM ("prove_eventually_nonzero", [get_expanded_fun thm]) |
2232 |
2232 |
2233 fun extract_terms (n, strict) ectxt basis t = |
2233 fun extract_terms (n, strict) ectxt basis t = |
2234 let |
2234 let |
2235 val bs = get_basis_list basis |
2235 val bs = get_basis_list basis |
2236 fun mk_constfun c = (Abs ("x", @{typ real}, c)) |
2236 fun mk_constfun c = (Abs ("x", \<^typ>\<open>real\<close>, c)) |
2237 val const_0 = mk_constfun @{term "0 :: real"} |
2237 val const_0 = mk_constfun \<^term>\<open>0 :: real\<close> |
2238 val const_1 = mk_constfun @{term "1 :: real"} |
2238 val const_1 = mk_constfun \<^term>\<open>1 :: real\<close> |
2239 fun uminus t = Term.betapply (@{term "\<lambda>(f::real\<Rightarrow>real) x. -f x"}, t) |
2239 fun uminus t = Term.betapply (\<^term>\<open>\<lambda>(f::real\<Rightarrow>real) x. -f x\<close>, t) |
2240 fun betapply2 a b c = Term.betapply (Term.betapply (a, b), c) |
2240 fun betapply2 a b c = Term.betapply (Term.betapply (a, b), c) |
2241 |
2241 |
2242 fun mk_sum' [] acc = acc |
2242 fun mk_sum' [] acc = acc |
2243 | mk_sum' ((t, sgn) :: ts) acc = mk_sum' ts ( |
2243 | mk_sum' ((t, sgn) :: ts) acc = mk_sum' ts ( |
2244 if sgn then |
2244 if sgn then |
2245 betapply2 @{term "%(f::real=>real) g x. f x - g x"} acc t |
2245 betapply2 \<^term>\<open>%(f::real=>real) g x. f x - g x\<close> acc t |
2246 else |
2246 else |
2247 betapply2 @{term "%(f::real=>real) g x. f x + g x"} acc t) |
2247 betapply2 \<^term>\<open>%(f::real=>real) g x. f x + g x\<close> acc t) |
2248 fun mk_sum [] = const_0 |
2248 fun mk_sum [] = const_0 |
2249 | mk_sum ((t, sgn) :: ts) = mk_sum' ts (if sgn then uminus t else t) |
2249 | mk_sum ((t, sgn) :: ts) = mk_sum' ts (if sgn then uminus t else t) |
2250 |
2250 |
2251 fun mk_mult a b = |
2251 fun mk_mult a b = |
2252 if a aconv const_0 then |
2252 if a aconv const_0 then |
2253 const_0 |
2253 const_0 |
2254 else if b aconv const_0 then |
2254 else if b aconv const_0 then |
2255 const_0 |
2255 const_0 |
2256 else if a aconv @{term "\<lambda>_::real. 1 :: real"} then |
2256 else if a aconv \<^term>\<open>\<lambda>_::real. 1 :: real\<close> then |
2257 b |
2257 b |
2258 else if b aconv @{term "\<lambda>_::real. 1 :: real"} then |
2258 else if b aconv \<^term>\<open>\<lambda>_::real. 1 :: real\<close> then |
2259 a |
2259 a |
2260 else if a aconv @{term "\<lambda>_::real. -1 :: real"} then |
2260 else if a aconv \<^term>\<open>\<lambda>_::real. -1 :: real\<close> then |
2261 Term.betapply (@{term "\<lambda>(f::real\<Rightarrow>real) x. -f x"}, b) |
2261 Term.betapply (\<^term>\<open>\<lambda>(f::real\<Rightarrow>real) x. -f x\<close>, b) |
2262 else if b aconv @{term "\<lambda>_::real. -1 :: real"} then |
2262 else if b aconv \<^term>\<open>\<lambda>_::real. -1 :: real\<close> then |
2263 Term.betapply (@{term "\<lambda>(f::real\<Rightarrow>real) x. -f x"}, a) |
2263 Term.betapply (\<^term>\<open>\<lambda>(f::real\<Rightarrow>real) x. -f x\<close>, a) |
2264 else |
2264 else |
2265 Abs ("x", @{typ real}, @{term "(*) :: real => _"} $ |
2265 Abs ("x", \<^typ>\<open>real\<close>, \<^term>\<open>(*) :: real => _\<close> $ |
2266 (Term.betapply (a, Bound 0)) $ (Term.betapply (b, Bound 0))) |
2266 (Term.betapply (a, Bound 0)) $ (Term.betapply (b, Bound 0))) |
2267 |
2267 |
2268 fun mk_powr b e = |
2268 fun mk_powr b e = |
2269 if e = @{term "0 :: real"} then |
2269 if e = \<^term>\<open>0 :: real\<close> then |
2270 const_1 |
2270 const_1 |
2271 else |
2271 else |
2272 let |
2272 let |
2273 val n = HOLogic.dest_number e |> snd |
2273 val n = HOLogic.dest_number e |> snd |
2274 in |
2274 in |
2275 if n >= 0 then |
2275 if n >= 0 then |
2276 Term.betapply (Term.betapply (@{term "%(b::real=>real) e x. b x ^ e"}, b), |
2276 Term.betapply (Term.betapply (\<^term>\<open>%(b::real=>real) e x. b x ^ e\<close>, b), |
2277 HOLogic.mk_number @{typ nat} n) |
2277 HOLogic.mk_number \<^typ>\<open>nat\<close> n) |
2278 else |
2278 else |
2279 Term.betapply (Term.betapply (@{term "%(b::real=>real) e x. b x powr e"}, b), e) |
2279 Term.betapply (Term.betapply (\<^term>\<open>%(b::real=>real) e x. b x powr e\<close>, b), e) |
2280 end |
2280 end |
2281 handle TERM _ => |
2281 handle TERM _ => |
2282 Term.betapply (Term.betapply (@{term "%(b::real=>real) e x. b x powr e"}, b), e) |
2282 Term.betapply (Term.betapply (\<^term>\<open>%(b::real=>real) e x. b x powr e\<close>, b), e) |
2283 |
2283 |
2284 fun mk_scale_elem b e acc = |
2284 fun mk_scale_elem b e acc = |
2285 let |
2285 let |
2286 val e = simplify_term ectxt e |
2286 val e = simplify_term ectxt e |
2287 in |
2287 in |
2288 if e = @{term "0 :: real"} then |
2288 if e = \<^term>\<open>0 :: real\<close> then |
2289 acc |
2289 acc |
2290 else if e = @{term "1 :: real"} then |
2290 else if e = \<^term>\<open>1 :: real\<close> then |
2291 mk_mult acc b |
2291 mk_mult acc b |
2292 else |
2292 else |
2293 mk_mult acc (mk_powr b e) |
2293 mk_mult acc (mk_powr b e) |
2294 end |
2294 end |
2295 |
2295 |
2298 mk_scale_elems bs es (mk_scale_elem b e acc) |
2298 mk_scale_elems bs es (mk_scale_elem b e acc) |
2299 | mk_scale_elems _ _ _ = raise Match |
2299 | mk_scale_elems _ _ _ = raise Match |
2300 |
2300 |
2301 fun mk_summand c es = |
2301 fun mk_summand c es = |
2302 let |
2302 let |
2303 val es = mk_scale_elems bs es @{term "\<lambda>_::real. 1 :: real"} |
2303 val es = mk_scale_elems bs es \<^term>\<open>\<lambda>_::real. 1 :: real\<close> |
2304 in |
2304 in |
2305 case c of |
2305 case c of |
2306 Const (@{const_name uminus}, _) $ c => ((c, true), es) |
2306 Const (\<^const_name>\<open>uminus\<close>, _) $ c => ((c, true), es) |
2307 | _ => ((c, false), es) |
2307 | _ => ((c, false), es) |
2308 end |
2308 end |
2309 |
2309 |
2310 fun go _ _ _ acc 0 = (acc, 0) |
2310 fun go _ _ _ acc 0 = (acc, 0) |
2311 | go 0 es t acc n = |
2311 | go 0 es t acc n = |
2312 let |
2312 let |
2313 val c = simplify_term ectxt t |
2313 val c = simplify_term ectxt t |
2314 in |
2314 in |
2315 if strict andalso c = @{term "0 :: real"} then |
2315 if strict andalso c = \<^term>\<open>0 :: real\<close> then |
2316 (acc, n) |
2316 (acc, n) |
2317 else |
2317 else |
2318 (mk_summand c (rev es) :: acc, n - 1) |
2318 (mk_summand c (rev es) :: acc, n - 1) |
2319 end |
2319 end |
2320 | go m es t acc n = |
2320 | go m es t acc n = |
2321 case Lazy_Eval.whnf ectxt t |> fst of |
2321 case Lazy_Eval.whnf ectxt t |> fst of |
2322 Const (@{const_name MS}, _) $ cs $ _ => |
2322 Const (\<^const_name>\<open>MS\<close>, _) $ cs $ _ => |
2323 go' m es (simplify_term ectxt cs) acc n |
2323 go' m es (simplify_term ectxt cs) acc n |
2324 | _ => raise TERM("extract_terms", [t]) |
2324 | _ => raise TERM("extract_terms", [t]) |
2325 and go' _ _ _ acc 0 = (acc, 0) |
2325 and go' _ _ _ acc 0 = (acc, 0) |
2326 | go' m es cs acc n = |
2326 | go' m es cs acc n = |
2327 case Lazy_Eval.whnf ectxt cs |> fst of |
2327 case Lazy_Eval.whnf ectxt cs |> fst of |
2328 Const (@{const_name MSLNil}, _) => (acc, n) |
2328 Const (\<^const_name>\<open>MSLNil\<close>, _) => (acc, n) |
2329 | Const (@{const_name MSLCons}, _) $ c $ cs => ( |
2329 | Const (\<^const_name>\<open>MSLCons\<close>, _) $ c $ cs => ( |
2330 case Lazy_Eval.whnf ectxt c |> fst |> HOLogic.dest_prod of |
2330 case Lazy_Eval.whnf ectxt c |> fst |> HOLogic.dest_prod of |
2331 (c, e) => |
2331 (c, e) => |
2332 case go (m - 1) (e :: es) c acc n of |
2332 case go (m - 1) (e :: es) c acc n of |
2333 (acc, n) => go' m es (simplify_term ectxt cs) acc n) |
2333 (acc, n) => go' m es (simplify_term ectxt cs) acc n) |
2334 | _ => raise TERM("extract_terms", [t]) |
2334 | _ => raise TERM("extract_terms", [t]) |
2335 val (summands, remaining) = go (basis_size basis) [] t [] (n + 1) |
2335 val (summands, remaining) = go (basis_size basis) [] t [] (n + 1) |
2336 val (summands, error) = |
2336 val (summands, error) = |
2337 if remaining = 0 then (rev (tl summands), SOME (snd (hd summands))) else (rev summands, NONE) |
2337 if remaining = 0 then (rev (tl summands), SOME (snd (hd summands))) else (rev summands, NONE) |
2338 val summands = map (fn ((c, sgn), es) => (mk_mult (mk_constfun c) es, sgn)) summands |
2338 val summands = map (fn ((c, sgn), es) => (mk_mult (mk_constfun c) es, sgn)) summands |
2339 val error = Option.map (fn err => Term.betapply (@{term "\<lambda>f::real\<Rightarrow>real. O(f)"}, err)) error |
2339 val error = Option.map (fn err => Term.betapply (\<^term>\<open>\<lambda>f::real\<Rightarrow>real. O(f)\<close>, err)) error |
2340 val expansion = mk_sum summands |
2340 val expansion = mk_sum summands |
2341 in |
2341 in |
2342 (expansion, error) |
2342 (expansion, error) |
2343 end |
2343 end |
2344 |
2344 |