[isabelle-dev] Bug: Possible generalization error in 'Tactic.rule_by_tactic'

[Makarius]

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.)


 	Makarius