# 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,
Andreas

On 13/07/2019 21:40, Gidon Ernst 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

```
```
```
```

```

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