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

[Simon Meier]

Hi Alex,

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

best regards,
Simon