[isabelle] feature request: defining tuples



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.