[isabelle] simps_of_case has problems with records
The simps_of_case conversion function does not seem to like records. Consider the
following minimal example:
record foo = foo :: nat
definition f :: "foo â nat Ã nat â nat"
where "f s xy = (case xy of (x, y) â foo s + x + y)"
In this example, simps_of_case raises an exception THM, because unification of "TERM _"
and "â?Q â ?P; ?Qâ â ?P" has failed in line 315 in drule.ML. This error occurs only if one
of the parameters of the function is a record.
Is this a general limitation of simps_of_case?
Background on my use case: I want to a function with many cases. Using fun with nested
pattern matching is too slow because the internal splitting procedure creates several
hundred disambiguiations and the internal constructions then take too long. However, it
works nicely with a case expression on the right hand side. So I'd like to get the simp
rules back with simps_of_case. Any suggestions on this are welcome.
This archive was generated by a fusion of
Pipermail (Mailman edition) and