Re: [isabelle] inductive_set

Inductive_set is not bad and will not disappear.


Christian Sternagel schrieb:
> Thnx for your replies,
> Does that mean that the general recommendation is to use "inductive"
> instead of "inductive_set"? From the documentation (isar-ref) it was not
> obvious to me that "inductive_set" is something bad :)
> cheers
> chris
> On 09/15/2010 11:01 AM, berghofe at wrote:
>> Quoting Florian Haftmann <florian.haftmann at>:
>>> Hi Christian,
>>>> apparently inductive_set does modify ALL occurrences of inductive
>>>> predicates stemming from other inductive_set commands inside intro
>>>> rules
>>>> as if the attribute [to_set] was used. Is this wanted / necessary / on
>>>> purpose? Can I prevent it? :)
>>> according to the sources inductive_set seems indeed to behave like that.
>>> You may call this a bug or a feature.
>>> The rules used for to_set / to_pred conversions are added using
>>> attribute pred_set_conv. Unfortunately, this only allows addition, not
>>> removal, preventing an ad-hoc solution for your problem. Maybe we have
>>> to think about that.
>> Hi Christian and Florian,
>> note that the purpose of inductive_set is mainly to make existing
>> theories using
>> the old set notation work with the new inductive definition package. The
>> only
>> promise we are making is that everything that used to work with the old
>> inductive command will also work with inductive_set. If you are using the
>> new "...p" predicates introduced by inductive_set to achieve some special
>> effects, you are on your own, i.e. it may or may not work as you expect.
>> Greetings,
>> Stefan

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