[isabelle] Problem with recdef (permissive)



Hi all,

  I have a really big and quite old Isabelle heap, which I use
regularly for regression testing a large collection of theories. Using
this heap, my attempt to load a specific theory breaks at a (permissive)
recdef with an exception trace and an error message [1]. If I start with
a fresh HOL heap and try to load the same theory, the permissive recdef
works without the exception trace and just leaves the error message in
the form of the (to-be-expected) warning [2] in the log. (In the theory,
just after the recdef, the termination condition is shown via
recdef_tc, but I do not think that matters here).

  Naturally, while I could start out with a fresh heap to avoid the
error at least for some time, I would like to understand (and debug)
the reasons leading to this behaviour in the first place.

  My guess is that side effects from loading the additional theories in
the big heap cause this behaviour.  Also, the big heap might have
different global options set than the new one (like, as you see, [1] has
show_types turned on). I have tried to check the obvious things
(simpsets, quick_and_dirty, etc.), but now I am a bit at a loss how to
investigate further.

  What other global settings might influence RecdefPackage in the
described way? How can I compare these settings easily for my two
heaps?

  Are there any trace options for RecdefPackage which I could turn on?

  Is it possible to print a list of all lemmas with attributes (not just
those with [simp] via `print_simpset (the_context());', but also for the
less used attributes)?

  I use PolyML-5-based Isabelle-2005 on a 64-bit machine; system
resources should not be a problem in this case. Also, my experience is
that Isabelle works reliably with large heaps; so, I would for the
moment also exclude plain bit rot for my old heap.

  Thanks for any hints!

  Best regards,

  Mark

  1. ### Trying full Presburger arithmetic ...

     Exception trace for exception - ERROR
     Rules.prove(3)
     Prim.postprocess(9)simplify_tc(3)
     Prim.postprocess(9)loop(5)
     Prim.postprocess(9)
     Prim.postprocess(9)
     Prim.postprocess(9)
     Prim.postprocess(9)
     Prim.postprocess(1)(1)(1)(1)
     Tfl.proof_stage(11)
     Tfl.simplify_defn(10)
     Tfl.define_i(10)
     Tfl.define(9)
     RecdefPackage.gen_add_recdef(10)
     o(2)(1)
     Toplevel.theory(1)(1)
     History.apply_copy(1)(1)(1)
     End of trace
  
     *** Bad final proof state:
     *** ALL (T::nat) new_init_T::nat.
     ***    (EX (tinit::tom_conft) tinp::nat => tom_conf_inputt.
     ***        new_init_T = Suc (last_JISR_before T tinit tinp) &
     ***        exists_JISR_below T tinit tinp) -->
     ***    new_init_T < Suc T
     ***  1. ALL (T::nat) new_init_T::nat.
     ***        (EX (tinit::tom_conft) tinp::nat => tom_conf_inputt.
     ***            new_init_T = Suc (last_JISR_before T tinit tinp) &
     ***            exists_JISR_below T tinit tinp) -->
     ***        new_init_T < Suc T
     *** 1 unsolved goals!
     *** Proof failed!
     *** At command "recdef" (line 1086 of "/tmp/mah/TP2/verification/proof/VAMP/tomasulo_invs_with_interrupts.thy").

  2. ### Trying full Presburger arithmetic ...
     ### Bad final proof state:
     ### ALL T new_init_T.
     ###    (EX tinit tinp.
     ###        new_init_T = Suc (last_JISR_before T tinit tinp) &
     ###        exists_JISR_below T tinit tinp) -->
     ###    new_init_T < Suc T
     ###  1. ALL T new_init_T.
     ###        (EX tinit tinp.
     ###            new_init_T = Suc (last_JISR_before T tinit tinp) &
     ###            exists_JISR_below T tinit tinp) -->
     ###        new_init_T < Suc T
     ### 1 unsolved goals!
     ### Proof failed!

-- 
Dr. Mark A. Hillebrand
German Research Center for Artificial Intelligence
Saarbruecken, Germany
Building E1 1, Room 4.06
Phone: +49 (0)681 302 57379    Fax: +49 (0)681 302 4290
Email: mah at dfki.de

-------------------------------------------------------------
Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH Trippstadter
Strasse 122, D-67663 Kaiserslautern, Germany

Geschaeftsfuehrung:
Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313
-------------------------------------------------------------





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.