[isabelle-dev] Isabelle cs. 70300f1b6835

[Ondřej Kunčar]

On 10/20/2012 09:45 AM, Florian Haftmann wrote:
> Hi Ondrej,

Hi Florian,

> the changeset
> http://isabelle.in.tum.de/reports/Isabelle/rev/70300f1b6835 broke the
> AFP sessions JinjaThreads and KBPs.

Yes, I know. I already fixed Collections on Friday and I am going to go 
back to this problem on Monday.

> After having a closer look at it, I would suggest two things:
> a) Keeping lemmas lookup_Mapping, Mapping_lookup, Mapping_inject,
> mapping_eq_iff, mapping_eqI since they are really fundamental and help
> in cases where transfer fails.

Well, my philosophy is that when we have lifting and transfer, users 
don't have to fiddle with abstraction and representation functions any 
more. Actually, they shouldn't see them at all. The users can use a lot 
of automation provided by lifting/transfer and achieve the same more 
smoothly. Thus I want to remove any explicit use of abstraction and 
representation functions.

I don't know about any situations where transfer fails and it prevents 
you to do your formalization in the same time. If you know about such a 
case, let us please know. Brian and me will be happy to inspect the 
problem and solve it. Of course, if there would be such a problem before 
the release and it wouldn't be solved, those lemmas would have to be 
added back as a workaround. But if lifting and transfer works, I don't 
see any point in keeping the lemmas. You don't need them and I want to 
encourage users to use lifting/transfer instead.

> b) Try hard to eliminate »rep« again and replace it by »lookup«.  This
> is plain cloning, an this is really bad.  What happens if you substitute
> »lookup« for »rep« in the typedef and drop the separate definition for
> »lookup«?  Maybe it goes through without further ado.

No, it doesn't and the current solution is better because now with 
lifting/transfer you just say that function application for mappings "m 
k" on the raw level is a lookup function on the abstract level (by using 
lift_definition). And then transfer works like a charm for your lemmas. 
But if you use representation function explicitly in your lemmas to 
achieve the same (as you propose), it doesn't work pretty well. And when 
we setup transfer to go also from the raw level to the abstract level 
(which I believe happens soon), you can lift function application on the 
raw level to your custom function on the abstract level, which, I think, 
is pretty cool and needed feature. And again, I believe that my solution 
is much cleaner way than fiddling with abstraction and representation 
functions.

But your observation gave me an idea that actually I should remove the 
explicit names for morphisms in Mapping.thy completely and then you 
wouldn't even notice there are any abstraction and representation 
functions behind the scene.

Cheers,
Ondrej