[isabelle] simps_of_case has problems with records



Dear all,

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)"

simps_of_case f_def

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.

Best,
Andreas




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