Email Gateway (Aug 19 2022 at 08:36): Email Gateway (Aug 19 2022 at 08:36):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Hi,
Suppose I have three simple theorems:
(1) theorem the_ordered_pair_property_simp:
"!u. !v. !r. !s. (u = r & v = s) --> (<u,v> = <r,s>)"
by simp
(2) theorem "(a = c & b = c) --> a = b"
by simp
(3) theorem "!u. !v. !A. !B. (A = {u,v} & B = {u,v}) --> A = B"
by simp
I think my question can be summarized be generalized by this question,
"What do names mean in Isabelle?"
My specific question would be, "Are these theorems that would need to be
proved if they're not restatements of prior theorems in HOL, or do they
come by default because of how name substitution works?"
I see these 4 axioms in HOL.thy:
axiomatization where
refl: "t = (t::'a)" and
subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
the_eq_trivial: "(THE x. x = a) = (a::'a)"
and
lemma the_sym_eq_trivial: "(THE y. x=y) = x"
and
lemmas [simp] =
...
the_eq_trivial
the_sym_eq_trivial
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.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:37):From: Ramana Kumar <rk436@cam.ac.uk>
On Mon, Sep 3, 2012 at 6:24 PM, Gottfried Barrow
<gottfried.barrow@gmx.com>wrote:
Hi,
Suppose I have three simple theorems:
(1) theorem the_ordered_pair_property_**simp:
"!u. !v. !r. !s. (u = r & v = s) --> (<u,v> = <r,s>)"
by simp(2) theorem "(a = c & b = c) --> a = b"
by simp(3) theorem "!u. !v. !A. !B. (A = {u,v} & B = {u,v}) --> A = B"
by simpI think my question can be summarized be generalized by this question,
"What do names mean in Isabelle?"My specific question would be, "Are these theorems that would need to be
proved if they're not restatements of prior theorems in HOL, or do they
come by default because of how name substitution works?"
Your question seems to me to be more about equality and less about names.
I see these 4 axioms in HOL.thy:
axiomatization where
refl: "t = (t::'a)" and
subst: "s = t \<Longrightarrow> P s \<Longrightarrow> P t" and
ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
the_eq_trivial: "(THE x. x = a) = (a::'a)"and
lemma the_sym_eq_trivial: "(THE y. x=y) = x"
and
lemmas [simp] =
...
the_eq_trivial
the_sym_eq_trivialSo 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.
Regards,
GB
Email Gateway (Aug 19 2022 at 08:38):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Last updated: Apr 19 2024 at 16:20 UTC