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



Hi,

Goal focus is another way to inline chained facts. However, I am not sure
if this is the right usage of goal focus. It might be just a hacky style
from me.

Best wishes,
Yakoub.

On Sun, Jul 14, 2019 at 12:16 PM Gidon Ernst <gidon.ernst at lmu.de> wrote:

> Hi!,
>
> there is "elim" and "intro" which use chained facts (but apparently no
> "dest") that correspond to (erule ...)+ and (rule ...)+ respectively.
> Note that they might loop.
>
> Best,
>   Gidon
>
> On 7/13/19 11:17 AM, Wolfgang Jeltsch wrote:
> > Hi!
> >
> > I’m developing a proof method that involves applications of `drule`.
> > This proof methods doesn’t work in the presence of chained facts,
> > because its `drule` invocations fail in this situation.
> >
> > Consider the following minimal example code:
> >
> >     lemma "P ∧ Q ⟹ R"
> >       apply (drule conjunct1)
> >       oops
> >
> > The invocation of `drule` correctly turns the goal into `P ⟹ R`.
> > However, it fails in the following situation:
> >
> >     lemma "P ∧ Q ⟹ R"
> >       using TrueI
> >       apply (drule conjunct1)
> >       oops
> >
> > Why is that, and how can `drule` been made work also in the presence of
> > chained facts?
> >
> > I also tried to use `erule` instead of `drule`, but the same problem
> > occurred with that.
> >
> > In my use case, I actually want to turn all chained facts into goal
> > premises anyhow. I can add the chained facts to the list of goal
> > premises by invoking `insert method_facts`, but this leaves the chained
> > facts in place, so that the problem with `drule` remains. Is there
> > perhaps a proof method that removes all chained facts?
> >
> > I know that `simp` turns chained facts into goal premises. Therefore, my
> > current workaround is to invoke `simp` in a way where it essentially
> > doesn’t rewrite anything but only moves chained facts into the goal. To
> > this end, I’m using `(insert TrueI, simp only: True_implies_equals)`.
> This has the side effect of removing all previously existing
> > `True` premises, but this isn’t a problem in my use case. Still, I’d be
> > happy to use a cleaner solution.
> >
> > All the best,
> > Wolfgang
> >
> >
>
> --
> Gidon Ernst
> Software and Computational Systems Lab, LMU Munich
> https://www.sosy-lab.org/people/ernst/
>
>



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