Email Gateway (Aug 18 2022 at 09:40): Email Gateway (Aug 18 2022 at 09:40):From: Jared Davis <jared@cs.utexas.edu>
Hi,
I am new to Isabelle and have several questions:
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?
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?
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.?
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?
Thanks!
Jared
Email Gateway (Aug 18 2022 at 09:40):From: Tobias Nipkow <nipkow@in.tum.de>
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".
- 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.
- 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.
- 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.
- 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
Email Gateway (Aug 18 2022 at 09:40):From: Makarius <makarius@sketis.net>
On Mon, 18 Sep 2006, Jared Davis wrote:
- 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?
Just use an explicit list of arguments.
An alternative is to use polymorphic recursion (overloading), e.g. see
http://isabelle.in.tum.de/nominal/ for definitions of generic permutations
and freshness predicates for lists, pairs, options, numbers, etc. This is
advanced matter, though.
- What is the "right" way to write a theorem that has multiple hyps?
The most general / scalable way is this:
lemma
assumes hyp1 and hyp2 and ... and hypN
shows concl
This has the advantage that the hypothesis are immediately available for
reasoning in the proof body, can be named separately etc. Small
statements are usually written as a single !! / ==> formula.
Makarius
Last updated: May 03 2024 at 08:18 UTC