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

Hi all,

IMO the cleanest way is to use the "use" method, which takes another method and overwrites what gets chained into the proof mehod. For example,

using TrueI
apply(use nothing in \<open>drule ...\<close>)

should work as expected. Note that "nothing" is the empty list of theorems. If you want to chain in other theorems, just use their names.

The _tac versions of (d/e)rule are considered legacy because they allow access to raw goal parameter names (which should be made available in the proof context using "subgoal" first).

Moreoer, elim and intro try to apply the given rules as often as possible, not just once like (d/e)rule, and they behave differently when it comes to instantiating schematic variables in the goals.

Hope this helps,

On 13/07/2019 21:40, Gidon Ernst wrote:

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.


On 7/13/19 11:17 AM, Wolfgang Jeltsch wrote:

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)

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)

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,

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