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



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.