Re: [Hol-info] Problem understanding (and translating to isabelle) a theorem in realax.ml

[Jonathan v. S. <jon...@df...>]

Hi all,
im currently having a problem figuring out the meaning of the following
theorem (from realax.ml):

# real_neg;;
> val it : thm =
>   |- --x1 = mk_real (\u. ?x1. treal_neg x1 treal_eq u /\ dest_real x1 x1)


What puzzles me mostly is the fact, that neither I nor HolLight can figure
out a correct typing for x1:

# `--x1 = mk_real (\u. ?x1. treal_neg x1 treal_eq u /\ dest_real x1 x1)`;;
> Exception: Failure "typechecking error (initial type assignment)".


But I also don't really get why the rhs doesn't seem to "depend" on x1 from
the lhs since the x1 on the rhs is bound by the existential quantification.

I would understand the theorem if it had the following form:

 `--x1 = mk_real (\u. ?x2. treal_neg x2 treal_eq u /\ dest_real x1 x2)`;;


Because then we'd build the equivalence class of all negatives of
hreal*hreal's that are in the equivalence class x1 (if we take real to be
the set of equivalence classes of hreal*hreal as specified by the quotient
type).

I'd greatly appreciate and information or suggestions that can shed light on
my issue end point me to any misconceptions I might have.

Jonathan