[isabelle-dev] Isabelle cs. 70300f1b6835
kuncar at in.tum.de
Sun Oct 21 00:25:53 CEST 2012
On 10/20/2012 09:45 AM, Florian Haftmann wrote:
> Hi Ondrej,
> 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
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
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.
More information about the isabelle-dev