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

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

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