Email Gateway (Aug 19 2022 at 14:24): Email Gateway (Aug 19 2022 at 14:24):From: Mathieu Giorgino <mathieu.giorgino@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
Email Gateway (Aug 19 2022 at 14:24):From: Mathieu Giorgino <mathieu.giorgino@gmail.com>
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
Email Gateway (Aug 19 2022 at 14:34):From: Mathieu Giorgino <mathieu.giorgino@gmail.com>
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
Email Gateway (Aug 19 2022 at 14:34):From: Ondřej Kunčar <kuncar@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
Last updated: Apr 25 2024 at 08:20 UTC