Re: [isabelle] inductive_set
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
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
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 in.tum.de wrote:
Quoting Florian Haftmann<florian.haftmann at informatik.tu-muenchen.de>:
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
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