[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.