[isabelle] questions


I am new to Isabelle and have several 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?

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?

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.?

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?

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.



Jared Davis <jared at cs.utexas.edu>
3600 Greystone Drive #604 - Austin, TX 78731
(512) 879-3858

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