[isabelle-dev] "Exception." fun oddity in Isabelle 2009-2
krauss at in.tum.de
Mon Dec 6 11:53:36 CET 2010
Nice failure :-)
> datatype Ta = C_2 "nat" "nat" | C_1 "Ta" "nat"
> fun f where
> "f (C_2 a b) c = c"
> | "f (C_1 a b) c = f a (f a (f a (f (C_1 a b) b)))"
> (* ... after a long time...
> f :: "Ta ⇒ nat ⇒ nat"
> At command "fun".
This is the termination prover looping. It keeps applying the
psimp-rules, which are still in the simpset in Isabelle2009-2.
I took them out in 150f831ce4a3 since they caused other confusion, so it
is no longer a problem in the next release. Now you can work around it
by taking them out yourself.
I am not sure about the exception. It could be some "physical" interrupt
due to hitting some ressource bound, which aborts the whole toplevel
transaction, so you cannot handle it. But I am just guessing.
More information about the isabelle-dev