Re: [isabelle] Retriving induction scheme for datatype



Hi Moa,

the proper way would be as follows:

ML ‹
  BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name list}
  |> the
  |> #fp_co_induct_sugar
  |> #co_inducts;
›

The fp_sugar records are quite rich in comparison to the old info record of a datatype---they should contain everything that the datatype command spits out.

Note that for nested datatypes such as rose trees (datatype 'a tree = Node 'a "'a tree list") the induction principle will look different from the one output by the old package. (Using datatype_compat is one way around it, but the new format is more compositional---so there is a point of adjusting tools to work with it.)

Dmitriy

On 29.09.2015 11:11, Moa Johansson wrote:
Hi,

We are updating our tools for inductive theorem proving to Isabelle2015.

We noticed that the Datatype package has changed, and wonder what the proper way of fetching the induction theorem for a given datatype is now (working on the ML-level, as we have a tactic for automated induction).

We can get things to work by using "Old_Datatype_Data.get_info", and registering all our datatypes with "datatype_compat". However, we would obviously want to do this in the proper way intended instead.

Grateful for help on where to look!

Best,
Moa







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