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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
