Re: [isabelle] inductive_set

Quite independent of inductive_set, I have on occasion wished I could
use "..." to denote particular subterms other than in the default setup.
But this would require a change to Isar and one would need a new concept
for describing "..." positions in terms.

For the time being I recommend to use (is "_ |> ?t") to create your own
"..." in each step. The overhead is bearable, and you can even reuse ?t
in each step and do not have to use ?t1, ?t2 etc.


Christian Sternagel schrieb:
> 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").
> cheers
> chris
> On 09/15/2010 12:28 PM, Tobias Nipkow wrote:
>> Inductive_set is not bad and will not disappear.
>> Tobias
>> 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.