Re: [isabelle] Retriving induction scheme for datatype



Hi Moa,

> 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.

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





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