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

[Simon Meier]

Hi Alex,

> 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.

Interesting. Just 1 hour ago, I wrote this code:

(*
   A ==> ... ==>  C
   ---------------- (protect_concl)
   A ==> ... ==> #C
*)
fun protect_concl th =
   Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectI;

(* Apply a tactic to the premises of an elim rule *)
fun erule_by_tactic ctxt tac =
   Goal.conclude o rule_by_tactic ctxt tac o protect_concl

With an appropriate adaption of the rule_by_tactic method.

However, now I'm don't know which solution I should use. Yours or mine?
Are there functionality differences or speed issues with mine our your
implementation?

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

The inductive package uses rule_by_tactic with the simpset of the
context. Moreover, rule_by_tactic is used inside a 'try', which implies
that such an error may be visible only very indirectly. For an expert of
this package it may be possible to find a test case.


best regards,
Simon