*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Usability of lift_bnf/copy_bnf*From*: Lars Hupel <hupel at in.tum.de>*Date*: Mon, 1 Aug 2016 09:24:47 +0200*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

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'. Cheers Lars Â Yes, I'm aware of FinFun, Fin_Map and Mapping, but neither of these fit my purpose.

**Follow-Ups**:**Re: [isabelle] Usability of lift_bnf/copy_bnf***From:*Jasmin Blanchette

**Re: [isabelle] Usability of lift_bnf/copy_bnf***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Report from our Isabelle course
- Next by Date: Re: [isabelle] Report from our Isabelle course
- Previous by Thread: Re: [isabelle] Report from our Isabelle course
- 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