Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 20 Apr 1994 16:25:36 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA21504;
          Wed, 20 Apr 1994 09:03:11 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from irafs1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA21490;
          Wed, 20 Apr 1994 09:01:29 -0600
Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP);
          Wed, 20 Apr 1994 16:57:28 +0200
Received: from ira.uka.de by i80fs2.ira.uka.de id <00377-0@i80fs2.ira.uka.de>;
          Wed, 20 Apr 1994 15:26:03 +0200
Date: Wed, 20 Apr 94 15:26:01 EDT
From: reetz <reetz@ira.uka.de>
To: info-hol@leopard.cs.byu.edu
Subject: Overloading of constants
Message-Id: <"i80fs2.ira.967:20.03.94.15.03.07"@ira.uka.de>

Dear all,
variables in HOL90 can be overloaded, i.e.
you can have variables in the same scope
with same names, but different types and
these variables are distinct, e.g.

let
 val x_num      = mk_var{Name="x",Ty=(==`:num`==)}
 val x_bool     = mk_var{Name="x",Ty=(==`:bool`==)}
 val x_num_eq_0 = mk_eq{lhs=x_num,rhs=(--`0`--)}
in
 mk_conj{conj1=x_num_eq_0,conj2=x_bool}
end;

leads to

val it = (--`((x :num) = (0 :num)) /\ (x :bool)`--) : term
- Compat.frees it;
val it = [(--`(x :num)`--),(--`(x :bool)`--)] : term list
-

but you can't define overloaded constants, e.g.

new_definition("x",--`x=0`--);
val it = |- (x :num) = (0 :num) : thm
- (
  new_definition("x",
   mk_eq{lhs=(mk_var{Name="x",Ty=(==`:bool`==)}),rhs=(--`T`--)});
  ()) handle e => print_HOL_ERR e;
 
Exception raised at Const_spec.check_specification:
attempt to specify an existing constant: x
val it = () : unit
-

So, what makes variables different from constants in respect to
overloading? Can't we have constants with same name, but different
types for some theoretical reasons? But why does it works with
free variables? Or is it just not implemented in HOL90?

Ralf


(*****************************************************************************)
(*                                                                           *)
(*  Ralf Reetz                            SFB 358 of the german research     *)
(*  reetz@informatik.uni-karlsruhe.de     society (DFG)                      *)
(*  reetz@ira.uka.de                      University of Karlsruhe, Germany   *)
(*                                                                           *)
(*                "we prove around in a ring and suppose,                    *)
(*                 the goal sits right in the middle and knows."             *)
(*                                                                           *)
(*****************************************************************************)