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
See http://isabelle.in.tum.de/testboard/Isabelle/rev/ccafd7d193e7 for a
patch which ignores these rules.
This archive was generated by a fusion of
Pipermail (Mailman edition) and