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:

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





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