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.


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