Email Gateway (Aug 22 2022 at 12:55): Email Gateway (Aug 22 2022 at 12:55):From: Buday Gergely <gbuday@karolyrobert.hu>
Hi,
is there any difference using
show "lemma" using fact1 and fact 2 by simp
and
show "lemma" by (simp add: fact1 fact2)
?
Email Gateway (Aug 22 2022 at 12:55):From: Lars Hupel <hupel@in.tum.de>
In many cases, these forms are equivalent, but there are subtle differences.
show "lemma" using fact1 and fact 2 by simp
"using" adds facts locally. Some methods treat local facts specially,
others don't. "simp" just inserts them as premises to the goal:
P_fact1 ==> P_fact2 ==> lemma
Because of the way polymorphism works in Isabelle/Pure, this means the
facts you specified can only be used monomorphically. Also, because the
simplifier simplifies premises, your facts are subject to simplification
themselves.
show "lemma" by (simp add: fact1 fact2)
This adds facts to the simpset. That means the simplifier may rewrite
occurrences of the left-hand sides of your facts in your lemma.
Cheers
Lars
Email Gateway (Aug 22 2022 at 12:55):From: Johannes Hölzl <hoelzl@in.tum.de>
There are also more subtle differences. AFAIK, if your fact is
polymorphic and you add it with "using", it is only applied for one
type. If you add it with "simp add" it can be applied with different
types.
In general I prefer "simp add", as this feels more deterministic.
Email Gateway (Aug 22 2022 at 12:55):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
there is a small difference. I mainly stumble upon it if my lemmas are
not in simp normal form [1].
For example, let's say we have proven sorry1.
lemma sorry1: fixes P::"'a × 'a ⇒ bool" shows "(x1, x2) = X ⟹ P (x1,
x2) ∧ Y ⟶ Z"
sorry
If you apply simp to sorry1, you will see that the simplifier will
rewrite "P (x1, x2)" to "P X". Hence, my lemma statement is not very
good.
Let's look at the difference.
lemma fixes P::"'a × 'a ⇒ bool" shows "P X ∧ Y ⟹ Z"
using sorry1[of _ _ X P Y Z] apply simp
oops
Here, in the above using-statement, you are throwing sorry1 into the
proof state and then invoke the simplifier. The simplifier will first
simplify sorry1 and then realize that it can apply it to your goal.
Second version:
lemma fixes P::"'a × 'a ⇒ bool" shows "P X ∧ Y ⟹ Z"
apply(simp add: sorry1[of _ _ X P Y Z]) (fails)
oops
Here, the simplifier fails to rewrite anything because it uses sorry1
directly as simp rule and does not try to simplify it first.
My personal practical conclusion: There is a technical difference, if
you ever encounter the difference, the main problem is that your facts
are not stated in a way the simplifier likes.
Best,
Cornelius
[1] http://proofcraft.org/blog/isabelle-style-part2.html
2016-03-10 9:45 GMT+01:00 Buday Gergely <gbuday@karolyrobert.hu>:
Last updated: Apr 23 2024 at 08:19 UTC