[isabelle-dev] Bug: Possible generalization error in 'Tactic.rule_by_tactic'
krauss at in.tum.de
Fri Apr 9 22:28:08 CEST 2010
Simon Meier wrote:
> 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
I would expect that they are equivalent. What I do not fully understand
is why your comment/names talk about elim rules... shouldn't this apply
to any kind of rules? I am using my code for refining induction rules.
> > 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.
We should try to prove that it is broken and then fix it. I'll try to
look into that next week.
More information about the isabelle-dev