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



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




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