Re: [isabelle] using and simp add:



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 at 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)
>
> ?
>
> - Gergely
>




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