*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Mere synonyms or the properties of equality being used?*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Mon, 3 Sep 2012 19:18:23 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5044E7D2.10005@gmx.com>*References*: <5044E7D2.10005@gmx.com>*Sender*: ramana.kumar at gmail.com

On Mon, Sep 3, 2012 at 6:24 PM, Gottfried Barrow <gottfried.barrow at 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 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?" > 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_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. > No, those two rules are about definite choice (THE), which doesn't appear anywhere in your three simple theorems above. > > Regards, > GB > > > > > > > > >

**Follow-Ups**:**Re: [isabelle] Mere synonyms or the properties of equality being used?***From:*Gottfried Barrow

**References**:**[isabelle] Mere synonyms or the properties of equality being used?***From:*Gottfried Barrow

- Previous by Date: [isabelle] Mere synonyms or the properties of equality being used?
- Next by Date: Re: [isabelle] Mere synonyms or the properties of equality being used?
- Previous by Thread: [isabelle] Mere synonyms or the properties of equality being used?
- Next by Thread: Re: [isabelle] Mere synonyms or the properties of equality being used?
- Cl-isabelle-users September 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list