Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014



On Tue, 24 Feb 2015, Sven Schneider wrote:

Is rename_tac using 'ubiquitious backtracking'? I would not have
expected rename_tac to be so complex.

I had a more simple implementation in mind: a tactic-wrapper which
operates as follows.
(1) obtain the current list of variables
(2) apply rename_tac
(3) obtain the new list of variables
(4) print a warning if old-list = new-list

Then rename_tac could be replaced everywhere by the wrapper-tactic..

Ubiquitious backtracking means you participate in a general situation of any number of results -- in a compostion of lazy functions that produce them. This means that in general, warnings or errors don't work without extra thought and extra machinery.

(The problem is similar in parse translations: sometimes people emit warnings there, but it merely means some confusing messages pop up out of nothing, without relation to the actual result.)


A canonical way to get the above effect is to make rename_tac strict, in the sense that it simply fails on vacous renaming. Thus it would behave like the "simp" method in that respect, in contrast to the internal simp_tac.

From the concrete information exposed so far, I am not yet convinced that
it is worth the while to revisit such ancient tactical relics in the Isar method name space at all.

So just the standard questions:

  * What are typical remaining applications of rename_tac?

  * Is it feasible to dispose it eventually, e.g. after Eisbach has been
    properly established.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.