Re: [isabelle] simps_of_case has problems with records

On 02.06.2015 11:55, Andreas Lochbihler wrote:
> 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?

The problem is that "#splits o Ctr_Sugar.ctr_sugar_of ctxt" returns
Drule.dummy_thm for records, which has not the expected format for a
split rule.

See for a
patch which ignores these rules.

  -- Lars

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