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