[isabelle-dev] map/rel/set for lift_bnf

[Dmitriy Traytel]

Hi Lars,

thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f.

Note that this still doesn’t provide the interface to Lifting and Transfer via transfer rules for the BNF constants (which is more complicated since lift_bnf doesn’t know about Lifting, in particular about the correspondence relations).

Dmitriy


> On 11 Jul 2017, at 16:18, Lars Hupel <hupel at in.tum.de> wrote:
> 
> Dear BNF experts,
> 
> a while ago [0] I posted some comments on the "lift_bnf" command. I'm
> currently in the process of cleaning up the "Finite_Map" theory and
> found out that now, "lift_bnf" exports the definitional theorems for
> map/rel/set.
> 
> In this case, the theorem looks like this:
> 
> fmmap ≡ λf. Abs_fmap ∘ Finite_Map.fmap.fun.map_fun f ∘ fmlookup
> 
> But if I look at "BNF_Def.map_def_of_bnf", the theorem looks like this:
> 
> fmmap ≡ λf. Abs_fmap ∘ op ∘ (map_option f) ∘ fmlookup
> 
> I couldn't find any way to unfold "Finite_Map.fmap.fun.map_fun" (which
> is presumably some internal constant), which means I still have to use
> the workaround of manually registering the lemmas I want.
> 
> This is not urgent, but it would be cool if I could get rid of the
> workaround for Isabelle2017.
> 
> Cheers
> Lars
> 
> 
> [0]
> <https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2016-August/msg00001.html>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev