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

[Alexander Krauss]

Hi Simon,

> (*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;

Thanks for pointing this out. It is a nice example for what typically 
goes wrong if the context discipline is not observed.

It happens to be that I just wrote a similar function last week for an 
experiment, not knowing about rule_by_tactic. Here is what I used:

val protect_conv = Conv.rewr_conv (Thm.symmetric @{thm prop_def})
val mk_goal = Conv.fconv_rule (Conv.concl_conv ~1 protect_conv)

fun refine_rule tac ctxt =
     singleton (Variable.trade (fn ctxt =>
       map (mk_goal #> tac ctxt #> Seq.hd #> Goal.conclude)) ctxt)

I think, the only difference, except for having a context is that the 
conclusion of the rule is protected according to the convention, which 
makes it a goal state. However, since the conclusion is always atomic, 
this may be overly paranoid.

I wonder if the context-less behaviour of rule_by_tactic can break code 
on top of it... Anyone with an evil test case?

Alex