# Re: [isabelle] Mere synonyms or the properties of equality being used?

On 9/3/2012 1:18 PM, Ramana Kumar wrote:

Your question seems to me to be more about equality and less about names.

`Yea, and I think I figured out the proper question. The right question
``is not, "Am I proving something, or do I have to prove something?", but
``"Does the proof of my theorem require the properties that I want it to
``require?"
`
To make sense of that, here's what I knew was a fairly vacuous statement:
(1) theorem "!u. !v. !r. !s. (r = {u,v}) & (s = {u,v}) --> r = s"
by simp
But that this isn't:

` (2) theorem "!u. !v. !r. r = {u,v} --> (!x. x inS r --> (x = u | x =
``v))"
` by(metis upA)
It is best not to use auto proofs in a mindless manner.

`I figured out a good test to test whether a theorem is vacuous: put it
``before the axioms or theorems that normally make it true. If it's true
``by simp there, then there's a good chance that's not the right way to
``state your theorem.
`

`This goes back to my past thoughts of what equality means. Equality
``doesn't mean identical, because 1/2 = 2/4. But in normal math, when we
``give different names to the same object, we sometimes start
``interchanging the names with no appeal to the properties of equality. We
``treat the names like synonyms.
`

`The meaning of names aren't ever discussed. That's low-level, and I
``started thinking about names after I saw that two congruence classes can
``be equal, but yet not "act the same" sometimes.
`

So maybe those last two rules are what simp is using to prove (1), (2),
and (3). And if simp is proving something, it must mean that something has
to be proved, if it hasn't already been proved.

No, those two rules are about definite choice (THE), which doesn't appear
anywhere in your three simple theorems above.

I'll postpone "choice" for another day, many days into the future.
Thanks,
GB

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