Re: [isabelle] inductive_set

Hi all,

good to know. Nevertheless, I tried to get rid of the "...p" predicates provided of my inductive sets. After most of the changes went through without problems, I now know again, why I originally used "...p" predicates. It was just in order for "..." in calculational reasoning to work.

In my concrete example I use the proper subterm relation on first-order terms. It is now defined as inductive set "supt" such that "(s, t) : supt" means that s is a superterm of t. Additionally there is an abbreviation "s |> t" standing for "(s, t) : supt".

In calculational reasoning I want to do steps like

  have "s |> t" sorry
  also have "... |> u" sorry

but this doesn't work since the dots do not refer to "t" of the first statement. Can I somehow influence what "..." refers to for special constants? Or is there any other easy way to make this work (previously "s |> t" was an abbreviation for "suptp s t" and hence "..." referred to "t").



On 09/15/2010 12:28 PM, Tobias Nipkow wrote:
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 :)



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