Lars Hupel

2016-08-01 07:31:10 UTC

Permalink

Dear BNF experts,Raw Message

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.