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

2017-07-12 Thread Lars Hupel
> thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f.

Great, thanks!

> 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).

That's fair enough. The proofs are not that complicated.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


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

2017-07-12 Thread 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  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]
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev