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 http://isabelle.in.tum.de/testboard/Isabelle/rev/ccafd7d193e7 for a
patch which ignores these rules.

  -- Lars




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