Re: [isabelle] inductive_set

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 :)



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


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