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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and