Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Retriving induction scheme for datatype

Email Gateway (Aug 22 2022 at 11:21):

From: Moa Johansson <jomoa@chalmers.se>
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

Email Gateway (Aug 22 2022 at 11:21):

From: Dmitriy Traytel <traytel@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 11:21):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Moa,

There are basically two options:

1. Use the compatibility layer in "HOL/Tools/BNF/bnf_lfp_compat.ML". The function "BNF_LFP_Compat.get_info" has almost the same signature as the old "get_info" and gives you access to both old and new datatypes. The second argument specifies some preferences; you should probably just pass "[]". Examples:

   ML {*
   BNF_LFP_Compat.get_info @{theory} [] @{type_name list}
   |> the
   |> #induct
   *}

   datatype 'a tree = Tree 'a "'a tree list"

   ML {*
   BNF_LFP_Compat.get_info @{theory} [] @{type_name tree}
   |> the
   |> #induct
   *}

   datatype_compat tree

   ML {*
   BNF_LFP_Compat.get_info @{theory} [] @{type_name tree}
   |> the
   |> #induct
   *}

Notice that for types with nesting (like "list"), you get a different induction scheme depending on whether you call "datatype_compat". You can pass the "Keep_Nesting" option if you prefer the new scheme. See our ITP 2014 paper for details about the nested vs. mutual styles.

2. Use the new interface in "HOL/Tools/BNF/bnf_fp_def_sugar.ML".

   ML {*
   BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name list}
   |> the
   |> #fp_co_induct_sugar
   |> #co_inducts
   |> hd
   *}

   datatype 'a tree = Tree 'a "'a tree list"

   ML {*
   BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name tree}
   |> the
   |> #fp_co_induct_sugar
   |> #co_inducts
   |> hd
   *}

I hope this helps.

Cheers,

Jasmin

Last updated: Apr 19 2024 at 20:15 UTC