[isabelle] Usability of lift_bnf/copy_bnf



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.




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