[isabelle-dev] Bug: Possible generalization error in 'Tactic.rule_by_tactic'
simon.meier at inf.ethz.ch
Fri Apr 9 23:06:21 CEST 2010
Alexander Krauss wrote:
> Hi Simon,
> 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.
You are right. It grew out of only considering elim rules and I didn't
adapt the name. Your name makes much more sense :-)
>> > 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.
OK. I'm curious what comes out.
More information about the isabelle-dev