[isabelle-dev] Bug: Possible generalization error in 'Tactic.rule_by_tactic'
makarius at sketis.net
Sat Apr 10 12:47:46 CEST 2010
On Fri, 9 Apr 2010, Lawrence Paulson wrote:
> rule_by_tactic is about 16 years old...
Yes, this old operation can indeed afford some deficiencies concerning
context handling, and I would have never called it a bug. It just happens
to be a "global" function, albeit one that can probably be easily
localized. I am more worried about seemingly new code that still ignores
the proper context (or local theory).
The "localization" effort has been going on for many years already, and we
have recently reached the point where most of Isabelle/Pure is properly
localized, and many of the newer packages of Isabelle/HOL as well. (The
packages dependening on typedef can now follow, too.)
In order to make the situation concerning context more clear to tool
implementors, I have recently started to maintain explicit naming
conventions like this:
val pretty_thm: Proof.context -> thm -> Pretty.T
val pretty_thm_global: theory -> thm -> Pretty.T
val pretty_thm_without_context: thm -> Pretty.T
Plain pretty_thm is the regular local version -- eveything is local by
default. You need a proper context for almost everything.
The "global" version works in an initial (empty) context relative a given
background theory. Many years ago "theory" would act as a context, but
since 5 years or more it only serves as a background certificate and
default starting point for a global context. Global operations work in
global situations, and it requires substantial expertise on localization
to get it half right. Paradoxically, global operations are harder to use
properly than local ones.
The "without_context" is a really ancient form that still happens to be
required in some historical situations.
Proper migration of tools is a very tedious process, requiring many years
of careful maintenance. The survial strategy is to keep things going into
the right direction, and problems will dissolve sooner than expected.
(Around 2006, when the localization of packages was started seriously, we
had been a bit too quick attempting too many changes at the same time,
causing considerable entropy in the overall system.)
More information about the isabelle-dev