[isabelle-dev] Interrupt exception

Lucas Dixon ldixon at inf.ed.ac.uk
Sun Jul 12 23:41:02 CEST 2009

Using the development version of Isabelle (1d4d0b305f16),
I just noticed a strange exception being raised...

theory norm
imports Complex_Main

fun internalise where
     intern_base: "internalise 0 (a,l) = (a, l)"
   | intern_step: "internalise (Suc n) (a,l) = internalise n (Suc a, l)"

fun extr where "extr (a,l) = foldr (op +) l a"

lemma [simp]: "internalise 0 x = x" by (induct x, simp_all)
lemma [simp]: "foldr (op +) l (Suc a) = Suc (foldr (op +) l a)"
by (induct l, simp_all)
lemma [simp]: "internalise (Suc n) (internalise m (a, l))
   = internalise n (internalise m (Suc a,l))"
   by (induct m arbitrary: a, simp_all)

theorem case1: "internalise (n + m) al = internalise n (internalise m al)"
   apply (unfold Product_Type.pair_collapse[symmetric, of "al"])

this gives me:

*** Interrupt.
*** At command "apply".

Interrupt: script management may be in an inconsistent state
            (but it's probably okay)

That's probably not the way it is supposed to fail...
(I'm using ProofGeneral 3.7.1)


The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

More information about the isabelle-dev mailing list