[isabelle-dev] "Exception." fun oddity in Isabelle 2009-2

[Alexander Krauss]

Hi Lucas,

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...
> 
> constants
>   f :: "Ta ⇒ nat ⇒ nat"
> Exception.
> 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.

Alex