Email Gateway (Aug 22 2022 at 10:25): Email Gateway (Aug 22 2022 at 10:25):From: Lars Hupel <hupel@in.tum.de>
Dear Makarius and Dan,
what is the reason for Eisbach residing in HOL instead of Pure? As far
as I can tell, the only dependency on HOL is for the "match" method,
which treats "Trueprop" specially (makes sense to me), but appears to
also deal with numerals (I don't understand the corresponding sources).
Anyway, making an exact copy of "Eisbach.thy", removing the line
ML_file "match_method.ML"
... and changing the import from "Main" to "Pure", it still works. I've
made a tiny experiment with some "simp" and "rule" invocations and the
method I defined behaves exactly as expected.
Cheers
Lars
Email Gateway (Aug 22 2022 at 10:26):From: Daniel Matichuk <daniel.matichuk@nicta.com.au>
You're correct, there is no deeper reason for residing in HOL other than giving it a default place to live.
The match method's dependence on HOL is also superficial and could be removed by using the proper Object_Logic interface where appropriate.
The use of numerals is a workaround for limitations in the method combinators, in order to pass information inside of a goal state. The proper fix here is to have a more rich type for methods (which has already been discussed), but the existing workaround could be adjusted to use more primitive operations (ultimately it just needs "int -> term" and "term -> int" regardless of the encoding).
These are all things that would disappear if/when Eisbach is integrated into Isar proper, rather than being a separate entity.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:26):From: Larry Paulson <lp15@cam.ac.uk>
I agree that it would be right for Eisbach to be installed generically, and available to all object-logics. Everything is Isabelle/HOL these days, but you never know when Isabelle/ZF might get a small revival. The original idea of Isabelle is that everything is available everywhere as much as possible.
Larry Paulson
Email Gateway (Aug 22 2022 at 10:27):From: Makarius <makarius@sketis.net>
Indeed, I still subscribe to this principle. Apart from Isabelle/ZF,
someone might even re-activate the ancient Martin-Löf Type Theory
(Isabelle/CTT), which has become popular again due to the HoTT movement.
The reasons why Eisbach ended up as isolated subsession derived from HOL
are pragmatic. Due to this convenient place in the session hierarchy for
its own development, it was possible to make many last-minute changes and
still ship everything on-time for the release.
Next time it should be done more according to the Pure rules of Isabelle,
but it also requires a second big reform on the instantiation are ("where"
and "of" attributes). More than half of Eisbach are actually just the
usual reforms, to make the application then rather obvious.
Makarius
Last updated: Apr 26 2024 at 04:17 UTC