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

[Lawrence Paulson]

rule_by_tactic is about 16 years old...
Larry

On 9 Apr 2010, at 21:28, 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.
> 
>> > 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.
> 
> Alex
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev