Re: [isabelle] using and simp add:


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"

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

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

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*)

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.



2016-03-10 9:45 GMT+01:00 Buday Gergely <gbuday at>:
> Hi,
> is there any difference using
> show "lemma" using fact1 and fact 2 by simp
> and
> show "lemma" by (simp add: fact1 fact2)
> ?
> - Gergely

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