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



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.