Re: [isabelle] Problems with `drule` and `erule` in the presence of chained facts



Am Samstag, den 13.07.2019, 17:41 +0100 schrieb Wenda Li:
> Although there might be better solutions and deeper understandings, my
> usual quick and dirty ways are:
> 
>   lemma "P ∧ Q ⟹ R"
>      using TrueI
>      apply -
>      apply (drule conjunct1)
>      oops
> 
> Or 
> 
>   lemma "P ∧ Q ⟹ R"
>      using TrueI
>      apply (drule_tac conjunct1)
>      oops

I think the trick with `apply -` has nothing to do with the proof
method `-` but only works because the second `apply` never sees the
chained facts from the `using` that comes before the first `apply`.
Therefore this trick doesn’t work in an Eisbach definition, where you
use the comma operator to compose several proof methods into a single
one.

The trick with `drule_tac` works though.

All the best,
Wolfgang





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.