[isabelle-dev] HOL-ODE-Numerics FAILED

[Florian Haftmann]

isabelle: 4acc029f69e9 tip
afp: c0882468fab2 tip

> HOL-ODE-Numerics FAILED
> (see also /home/haftmann/.isabelle/heaps/polyml-5.7.1_x86_64-linux/log/HOL-ODE-Numerics)
>    thm ->
>      int ->
>        int ->
>          int ->
>            int ->
>              (int * int * string) list ->
>                string -> Proof.context -> int -> tactic
> val poincare'_bnds_tac = fn:
>    thm ->
>      int ->
>        int ->
>          int ->
>            int ->
>              (int * int * string) list ->
>                string -> Proof.context -> int -> tactic
> ### Rule already declared as elimination (elim)
> ### \<lbrakk>(?f has_derivative ?f') ?F;
> ###  bounded_linear ?f' \<Longrightarrow> PROP ?W\<rbrakk>
> ### \<Longrightarrow> PROP ?W
> ### theory "HOL-ODE-Numerics.Example_Utilities"
> ### 52.579s elapsed time, 113.340s cpu time, 12.052s GC time
> Loading theory "HOL-ODE-Numerics.ODE_Numerics"
> ### Introduced fixed type variable(s): 'b in "X__"
> ### theory "HOL-ODE-Numerics.ODE_Numerics"
> ### 0.056s elapsed time, 0.168s cpu time, 0.000s GC time
> *** Failed to apply initial proof method (line 985 of "~/data/tum/afp/master/thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy"):
> *** using this:
> ***   convex (T \<times> X)
> ***   \<forall>x\<in>T \<times> X.
> ***      ((\<lambda>(t, x). f t x) has_derivative f' x)
> ***       (at x within T \<times> X)
> ***   \<forall>x\<in>T \<times> X. onorm (f' x) \<le> B'
> ***   (t, x) \<in> T \<times> X
> ***   (t, y) \<in> T \<times> X
> *** goal (1 subgoal):
> ***  1. norm
> ***      ((case (t, x) of (t, x) \<Rightarrow> f t x) -
> ***       (case (t, y) of (t, x) \<Rightarrow> f t x))
> ***     \<le> B' * norm ((t, x) - (t, y))
> *** At command "by" (line 985 of "~/data/tum/afp/master/thys/Ordinary_Differential_Equations/Numerics/Runge_Kutta.thy")

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180521/0a80724c/attachment-0001.asc>