[isabelle-dev] How to activate/de-activate unifier-trace from ML-level

[Makarius]

On Wed, 11 Feb 2015, Dmitriy Traytel wrote:

>>  What remains are slightly odd entry points without context:
>>  resolve0_tac/rtac, eresolve_tac/etac, dresolve_tac/dtac.  We could
>>  probably remove them altogether, but there are a lot of remaining uses
>>  in the new datatype implementation, which I don't want to change
>>  myself.
>
> indeed approximately 2/3 of all usages of rtac in the Isabelle 
> distribution + AFP are in our BNF tactics (roughly 2000 occurrences).
>
> Adding a context to each of them would make the tactics even harder to 
> read/maintain compared to their current state. The only decent way of 
> adding the context everywhere would be via some combinators à la
>
> THEN'': (ctxt -> int -> tactic) * (ctxt -> int -> tactic) -> ctxt -> int 
> ->  tactic
>
> assuming that rtac has type "thm -> ctxt -> int -> tactic"
>
> or reuse the polymorphism of THEN' and work with an uncurried version of 
> rtac: thm -> (ctxt, int) -> tactic (and other tactics). Needless to say 
> that I could do this only locally in the BNF package, but maybe this is 
> a general question of how tactics should look like.

There is indeed a general question in the background what tactics should 
look like, for a few decades already.

The most compact (or rather hermetic) way you be to put the context into 
the goal state, but in recent decades the direction of movement has been 
the opposite.  The context is the static part and the goal state the 
dynamic part.  The subgoal address is somehow in the middle.  So the 
canonical argument order for that came out as follows:

   context --> arguments --> subgoal_address -> tactic


For Eisbach the distinction of static vs. dynamic part has become very 
relevant again, and not all questions are answered, especially concerning 
"arguments" in some cases.


 	Makarius