Re: [isabelle] Usability of lift_bnf/copy_bnf

Hi Lars,

> On 01 Aug 2016, at 09:24, Lars Hupel <hupel at> 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,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.