Re: [isabelle] questions



1. Is there a way to make a purely syntactic abbreviation for a constant? For example, I have:

   datatype object = Symbol nat | ...

Right now I can write:

   constdefs foo :: object
             "foo == Symbol 0"
             bar :: object
             "bar == Symbol 1"
             ...

This is almost what I want, since I can now write "foo" and "bar" in definitions and theorems. But unfortunately I now need to add foo_def and bar_def for simp to make progress in some cases, and if I do that I will see "Symbol 0" instead of foo, etc.

Is there a way to make these syntactic abbreviations so that Isabelle sees Symbol 0 when I type foo, but still prints foo back to me?

If you use Isabelle 2005, you may use introduce sytactic symbols and "translations", eg

syntax foo :: object
       bar :: object

translations "foo" == "Symbol 0"
             "bar" == "Symbol 1"

There are restrictions here (no var may occur twice on the lhs or rhs), and you should read the ref manual for the details.

In the development version there are the much slicker "abbreviations".

2. Is there a way to write a function/macro that takes a variable number of arguments? For example, could I define a function to "and" together an
arbitrary number of boolean arguments?

No. Not typeable.

3. Is there a local scoping mechanism I can use so that if I define a lemma, it goes out of scope after I prove some theorems with it? I.e., imagine a sequence such as:

    lemma "lemma1" ...
    lemma "lemma2" ...
    theorem "thm1" ...
    theorem "thm2" ...

Can I wrap something around this to make the lemmas disappear so I can reuse their names, etc.?

Locales provide some of that. You can reuse thm names anyway.

4. What is the "right" way to write a theorem that has multiple hyps? I could write something like,

    hyp1 --> hyp2 --> ... --> hypN --> concl

Or I could write:

    [| hyp1; hyp2; ...; hypN |] ==> concl

Is there any difference to doing this? Which will be better for the simplifier?

The simplifier does not care but other tools do. Always use the second form, it supports backward chaining.

5. Is there a good way to debug looping rewrite rules? I tried activating the "trace simplifier" to do this but it started printing lots of output and wouldn't respond to the stop button, so I had to forcibly kill the xemacs session.

That is a problem of the xemacs and Proof General interface which we also suffer from :-( In the development version you can set the trace depth level (eg to 1), which often helps.

Tobias






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