Why does `by (simp add: assms)`

work here, but `using assms by simp`

would not work?

```
lemma
fixes f :: "'a ⇒ 'a ⇒ 'a" (infixr "⊕" 80)
and e :: 'a
assumes "∀x. ∀y. x ⊕ y = y ⊕ x"
and "∀x. ∀y. ∀z. x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"
and "∀x. e ⊕ x = x"
shows "u ⊕ v = e ⟶ (v ⊕ w) ⊕ u = w"
by (simp add: assms)
```

Compare

```
lemma
fixes f :: "'a ⇒ 'a ⇒ 'a" (infixr "⊕" 80)
and e :: 'a
assumes "⋀x y. x ⊕ y = y ⊕ x"
and "⋀ x y z. x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"
and "⋀x. e ⊕ x = x"
shows "u ⊕ v = e ⟶ (v ⊕ w) ⊕ u = w"
supply [[simp_trace_new,simp_trace_depth_limit=5]]
using assms apply (simp)
```

with:

```
lemma
fixes f :: "'a ⇒ 'a ⇒ 'a" (infixr "⊕" 80)
and e :: 'a
assumes "⋀x y. x ⊕ y = y ⊕ x"
and "⋀ x y z. x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z"
and "⋀x. e ⊕ x = x"
shows "u ⊕ v = e ⟶ (v ⊕ w) ⊕ u = w"
supply [[simp_trace_new,simp_trace_depth_limit=5]]
using assms apply (simp (no_asm_simp))
```

With `using assms`

"x ⊕ (y ⊕ z) = (x ⊕ y) ⊕ z" gets inverted because `x ⊕ (y ⊕ z)`

is the more natural version, which cannot happen with `(simp add: assms)

(Trigger Warning: please immediately forget the existence of `no_asm_simp`

and do not ever use it)

I see. For most proofs I did so far both ways always worked that's why I was confused here. Is there any documentation that explains why `using`

does this?

In its default setup, the simplifier picks up premises of your goal and adds them to the simpset. This is so that if e.g. you have something like `∀x. f x = g x ⟶ P x`

and you do `auto`

(which results in you getting a premise `f x = g x`

in the goal), the simplifier will use `f x = g x`

for rewriting.

There is some heuristic that figures out whether to flip the equation when it gets picked up; e.g. if you have something like `f a b c = x`

(where the right-hand side is just a variable and the left-hand side is something more complicated) you typically want to flip the equation for rewriting for the best effect.

The `using`

command really just sets up the facts you give to it as "chained facts" (i.e. they get "chained into" the proof method, in this case `simp`

). Most proof methods (like `simp`

) simply add the chained facts to the goal as premises.

If you, on the other hand, do `simp add:`

there is no reorientation going on; it just uses the rules in the form that you give it to it as rewrite rules.

(Well, more or less – it still does things like if you give it a rule like `P`

it turns it into `P = True`

and similarly for `¬P`

)

So the take-away message here is: If you have facts that make good rewrite rules, do `simp add:`

and not `using`

.

This also keeps your goal state cleaner; if you do `using`

to chain in a lot of facts, it will make your goal state very big and unreadable.

@Manuel Eberl Thanks for the explanation. I didn't really know about the implications of using either style. I will keep that in mind!

waynee95 has marked this topic as resolved.

Last updated: Sep 25 2022 at 23:25 UTC