Re: [isabelle] inductive_set

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.


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