Re: [isabelle] questions
On Mon, 18 Sep 2006, Jared Davis wrote:
> 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?
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.
> 4. What is the "right" way to write a theorem that has multiple hyps?
The most general / scalable way is this:
assumes hyp1 and hyp2 and ... and hypN
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and