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

[Alexander Krauss]

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