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

[Simon Meier]

Dear Isabelle-Devs,

while working on my Isabelle extension for an embedded security protocol 
logic, I stumbled upon the code of 'rule_by_tactic' in Pure/tactic.ML:

(*Makes a rule by applying a tactic to an existing rule*)
fun rule_by_tactic tac rl =
   let
     val ctxt = Variable.thm_context rl;
     val ((_, [st]), ctxt') = Variable.import true [rl] ctxt;
   in
     (case Seq.pull (tac st) of
       NONE => raise THM ("rule_by_tactic", 0, [rl])
     | SOME (st', _) =>
         zero_var_indexes (singleton (Variable.export ctxt' ctxt) st'))
   end;


As the following ISAR snippet shows this code suffers from the problem 
of conjuring up a context from the given theorem.


locale test =
   fixes t x
   assumes ensure_clash [simp]: "t = x"
begin

(* The command below fails because the meta-variables ?t::?'a
    in @{thm refl} are converted to the free variables t::'a.
    These variables are not completely free; i.e., they are known in
    some rules in the simpset. Hence, the simplifier rewrites it
    and later generalization fails.
*)

ML{*

Tactic.rule_by_tactic (PRIMITIVE (simplify @{simpset})) @{thm refl}

*}

Taking the context as an additional argument obviously solves this problem.

I don't know how relevant this problem is. It seems that 
'rule_by_tactic' is used in a few places. So the above problem may occur 
in a few seldom cases...

best regards,
Simon Meier


-- 
ETH Zurich, Simon Meier, Department of Computer Science
CNB F 109.2, Universitätstrasse 6, 8092 Zürich
Tel +41 44 632 83 84, Fax +41 44 632 11 72,
www.infsec.ethz.ch