Re: [isabelle] How to use transfer when lifting_forget has been called ?



Ok, I have now seen that "includ*" are given in isar-ref, both in the
section 5.3 (Bundled declarations) and 12.3 (Lifting package).

This looks really useful, thanks to the Isabelle/devs !

-- Mathieu



2014-05-28 18:49 GMT-07:00 Mathieu Giorgino <mathieu.giorgino at gmail.com>:

> Ok, Great !
>
> I didn't know bundles, can we define and use them for anything ? For
> example can we make a bundle containing specific intro, elim and
> simplifications rules ? Looks like a convenient feature.
>
> Thanks a lot,
>
> -- Mathieu
>
>
> 2014-05-28 18:30 GMT-07:00 Ondřej Kunčar <kuncar at in.tum.de>:
>
> Hi Mathieu.
>> Bundles can be imported by three different means:
>> 1)
>> context
>> includes fset.lifting
>> begin
>> ...
>> end
>> 2)
>> lemma "..."
>> proof -
>>   include fset.lifting
>> ...
>> qed
>> 3)
>> lemma "..."
>> apply ...
>> including fset.lifting
>> apply ...
>> done
>>
>> Your lemma can be proved for example like this:
>>
>> lemma fcard_fimage:"inj_on f (fset xs) ⟹ fcard (f |`| xs) = fcard xs"
>> including fset.lifting by transfer (auto intro:card_image)
>>
>> Best,
>> Ondrej
>>
>>
>> On 05/29/2014 02:54 AM, Mathieu Giorgino wrote:
>>
>>> Hi all,
>>>
>>> I am using the library "Library/FSet" and I wanted to add this missing
>>> lemma:
>>>
>>> lemma fcard_fimage:"inj_on f (fset xs) ⟹ fcard (f |`| xs) = fcard xs"
>>>    by transfer (auto intro:card_image)
>>>
>>> I still haven't digged in the details of Transfer and Lifting and don't
>>> know exactly how they work, and I have simply mimicked what was already
>>> done in FSet.
>>>
>>> This lemma can easily be proved by using Transfer (as given above) as
>>> long
>>> as it is before the call "lifting_forget fset.lifting", ie once Lifting
>>> and
>>> Transfer have been un-setup for fset, which is totally expected.
>>> However, I
>>> haven't been able to restore the lifting bundle for FSet afterwards
>>> either
>>> using lifting_setup or lifting_update and I am then forced to either
>>> remove
>>> lifting_forget from FSet or add this lemma before it.
>>>
>>> Is there a mean to restore the bundle, and if it is the case, how ?
>>>
>>> Thanks,
>>>
>>> -- Mathieu
>>>
>>>
>>
>>
>>
>



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