[isabelle] feature request: defining tuples


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. 


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.


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