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



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.