[isabelle-dev] Bug: Possible generalization error in 'Tactic.rule_by_tactic'
Simon Meier
simon.meier at inf.ethz.ch
Fri Apr 9 20:49:23 CEST 2010
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
More information about the isabelle-dev
mailing list