*To*: Lars Hupel <hupel at in.tum.de>*Subject*: Re: [isabelle] Usability of lift_bnf/copy_bnf*From*: Dmitriy Traytel <traytel at inf.ethz.ch>*Date*: Mon, 1 Aug 2016 22:38:51 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <43654e1b-bb65-ff46-6878-ad6abaf6c176@in.tum.de>*References*: <43654e1b-bb65-ff46-6878-ad6abaf6c176@in.tum.de>

Hi Lars, > On 01 Aug 2016, at 09:24, Lars Hupel <hupel at in.tum.de> wrote: > > Dear BNF experts, > > on the weekend I was toying with introducing a new type for finite maps > for my own formalization.Â > > typedef ('a, 'b) fmap = "{m. finite (dom m)} :: ('a â 'b) set" > morphisms fmlookup Abs_fmap > > Luckily enough, registering this as a BNF is very simple: > > lift_bnf ('a, 'b) fmap [wits: Map.empty] > by auto > > This is very nice â thanks for that facility! > > Constants such as 'map_fmap', 'set_fmap', 'rel_fmap' and 'pred_fmap' are > defined using composition of their underlying counterparts and the > abstraction function. For example: > > map_fmap â Îf. Abs_fmap â op â (map_option f) â fmlookup > > This is as expected. However, I noticed some problems when working with > these constants wrt to other Isabelle tools and the BNF package itself: > > * The defining equations are not exported. I had to obtain them via > > BNF_Def.bnf_of @{context} @{type_name fmap} > |> the > |> BNF_Def.map_def_of_bnf > > * I can't give them a custom name. If I want to rename 'map_fmap' to > 'fmmap', I need to explicitly add an abbreviation. > > * Lifting is not set up for these constants which makes proving lemmas > over e.g. 'map_fmap' and the lifted version of 'op ++' very tedious. > Here's an example: > > private lift_definition > fmmap0 :: "('b â 'c) â ('a, 'b) fmap â ('a, 'c) fmap" > is "Îf m. map_option f â m" > by simp > > lemma fmmap0: "fmmap = fmmap0" > unfolding fmmap0_def (* prove via defining equation of 'fmmap' *) > > lemma fmmap_add[simp]: "fmmap f (m ++âf n) = fmmap f m ++âf fmmap f n" > unfolding fmmap0 > by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits) > > I introduced an auxiliary constant which is equivalent to 'map_fmap', > but defined using 'lift_definition' instead of manually. I can use that > equivalence to rewrite propositions to make them amenable for 'transferâ. coincidentally, I was using lift_bnf myself last week and run into exactly the same limitations as you did (except for the custom names which work fine as Jasmin pointed out). I think your way of dealing with those limitations (they also apply to set and rel) are as good as it can get for now. They are on my list of things to improve. Eventually, Iâll report here when this happens. Thanks for sharing, Dmitriy

**Follow-Ups**:**Re: [isabelle] Usability of lift_bnf/copy_bnf***From:*Lars Hupel

**References**:**[isabelle] Usability of lift_bnf/copy_bnf***From:*Lars Hupel

- Previous by Date: Re: [isabelle] Proposal: An update to Multiset theory
- Next by Date: Re: [isabelle] Usability of lift_bnf/copy_bnf
- Previous by Thread: Re: [isabelle] Usability of lift_bnf/copy_bnf
- Next by Thread: Re: [isabelle] Usability of lift_bnf/copy_bnf
- Cl-isabelle-users August 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list