3639 |> HOLogic.dest_Trueprop |
3639 |> HOLogic.dest_Trueprop |
3640 |> Term.strip_comb |> snd |> List.last |
3640 |> Term.strip_comb |> snd |> List.last |
3641 |> HOLogic.dest_list |
3641 |> HOLogic.dest_list |
3642 val p = prec |
3642 val p = prec |
3643 |> HOLogic.mk_number @{typ nat} |
3643 |> HOLogic.mk_number @{typ nat} |
3644 |> Thm.cterm_of (Proof_Context.theory_of ctxt) |
3644 |> Proof_Context.cterm_of ctxt |
3645 in case taylor |
3645 in case taylor |
3646 of NONE => let |
3646 of NONE => let |
3647 val n = vs |> length |
3647 val n = vs |> length |
3648 |> HOLogic.mk_number @{typ nat} |
3648 |> HOLogic.mk_number @{typ nat} |
3649 |> Thm.cterm_of (Proof_Context.theory_of ctxt) |
3649 |> Proof_Context.cterm_of ctxt |
3650 val s = vs |
3650 val s = vs |
3651 |> map lookup_splitting |
3651 |> map lookup_splitting |
3652 |> HOLogic.mk_list @{typ nat} |
3652 |> HOLogic.mk_list @{typ nat} |
3653 |> Thm.cterm_of (Proof_Context.theory_of ctxt) |
3653 |> Proof_Context.cterm_of ctxt |
3654 in |
3654 in |
3655 (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n), |
3655 (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n), |
3656 (@{cpat "?prec::nat"}, p), |
3656 (@{cpat "?prec::nat"}, p), |
3657 (@{cpat "?ss::nat list"}, s)]) |
3657 (@{cpat "?ss::nat list"}, s)]) |
3658 @{thm "approx_form"}) i |
3658 @{thm "approx_form"}) i |
3661 |
3661 |
3662 | SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st])) |
3662 | SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st])) |
3663 else let |
3663 else let |
3664 val t = t |
3664 val t = t |
3665 |> HOLogic.mk_number @{typ nat} |
3665 |> HOLogic.mk_number @{typ nat} |
3666 |> Thm.cterm_of (Proof_Context.theory_of ctxt) |
3666 |> Proof_Context.cterm_of ctxt |
3667 val s = vs |> map lookup_splitting |> hd |
3667 val s = vs |> map lookup_splitting |> hd |
3668 |> Thm.cterm_of (Proof_Context.theory_of ctxt) |
3668 |> Proof_Context.cterm_of ctxt |
3669 in |
3669 in |
3670 rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s), |
3670 rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s), |
3671 (@{cpat "?t::nat"}, t), |
3671 (@{cpat "?t::nat"}, t), |
3672 (@{cpat "?prec::nat"}, p)]) |
3672 (@{cpat "?prec::nat"}, p)]) |
3673 @{thm "approx_tse_form"}) i st |
3673 @{thm "approx_tse_form"}) i st |