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)
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)
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))
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.
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
So the take-away message here is: If you have facts that make good rewrite rules, do
simp add: and not
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