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



Am Samstag, den 13.07.2019, 18:17 +0300 schrieb Wolfgang Jeltsch:
> 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.

What I had overlooked is that when using `(insert TrueI, simp only:
True_implies_equals)`, the `simp` invocation can still use the chained
facts as simplification rules, which can modify the goal further.

That said, I learned from fellow mailing list members that tactics turn
chained facts into goal premises. My new proof method for moving chained
facts into the goal is `(insert TrueI, erule_tac TrueE)`. This also
doesn’t have the disadvantage of removing `True` premises that might
have been there in the first place.

All the best,
Wolfgang





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