Re: [isabelle] feature request: defining tuples



That would indeed be convenient and I have frequently felt like adding it to
Isabelle/HOL. HOL Light supports this, and maybe HOL4 too.

Tobias

Am 28/11/2013 15:55, schrieb John Wickerson:
> Hi,
> 
> Could I make a feature request regarding the "definition" package?
> 
> Current status
> --------------
> 
> Statements like { definition "foo (a,b) == blah /\ bleh" } are not accepted, since the definition package does not support tupled arguments. 
> 
> Proposal
> --------
> 
> That the definition package allows tupled arguments. Slightly more generally, since (a,b) is just shorthand for the constructed term "Pair a b", I propose that the definition package should support pattern-matching of arguments whenever the types of those arguments have exactly *one* constructor. For instance, I could then write { datatype proc = Procedure string command } and { definition "exec (Procedure s c) == ..." }.
> 
> Current workarounds
> -------------------
> 
> 1. Write { definition "foo == %(a,b). blah /\ bleh" }. But this changes the foo_def theorem, and doesn't look so visually nice.
> 
> 2. Write { fun foo where "foo (a,b) = (blah /\ bleh)" }. But this changes the foo_def theorem, and I have to remember to use foo.simps instead. And I have to put extra parentheses around the definiens, because "=" has different precedence to "==". And I have to remove foo.simps from the simplifier if I don't want foo expanding all the time. And I prefer to reserve "fun" for proper recursive functions, which foo isn't.
> 
> 3. Write { definition "foo a b == blah /\ bleh" }. But there are times when it's more idiomatic to tuple than to curry.
> 
> 
> cheers,
> John
> 




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