Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Message-Id: <199111071607.AA10112@panther.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: witnesses
In-Reply-To: Your message of Thu, 07 Nov 91 14:34:20 +0000. <"swan.cl.ca.784:07.10.91.14.34.30"@cl.cam.ac.uk>
Date: Thu, 07 Nov 91 08:07:34 -0800
From: Phil Windley <windley@edu.uidaho.cs.panther>


OK, I'm sorry.  I made the problem so trivial that it didn't get the point
across. My fault.

Here's a more complex example:

I define the group *structure* using the abstract data type facilities of
HOL:

let GROUP_lemma = define_type
    `group_def`
    `group = MK_GROUP * *->*->* *->*`;;


Next, I define selectors that represent the identity, operand, and inverse:

let id_def = new_recursive_definition
    false
    GROUP_lemma
    `id`
    "id
       ((MK_GROUP x1 x2 x3):^(abs_type_info GROUP_lemma)) = x1";;

...etc.

Now I define a predicate stating which things with the group *structure*
are REALLY groups:

let IS_GROUP_def = new_definition
   (`IS_GROUP`,
    "!g:(*)group . IS_GROUP g =
       (!x:* .mult g x (id g) = x) /\
       (!x:* .mult g (id g) x = x) /\
       (!x:* .mult g x (inv g x) = (id g)) /\
       (!x:* .mult g (inv g x) x = (id g)) /\
       (! x y z:*. (mult g x (mult g y z)) = (mult g (mult g x y) z))"
   );;

Now I want to prove:

g(
"? g:(*)group . IS_GROUP g"
);;


Tom Melham wrote:
+------------
|
| Polymorphic existential witnesses.
| ----------------------------------
|
| In general, when you have a goal of the form
|
|     [1]      ?x:*. P[x]
|
| you must supply as a witness some term of type *.  It is just not
| possible to instantiate the type * to some type ty in the hope of
| supplying a witness this type.  The goal [1] behaves as if there
| is a universal quantification over the type variable *.
|

So, the problem involves coming up with a group on type * (i.e. a group so
trivial its a group for every type).  The identity element has to be
something created with the choice operator (I assume).

I apologize for my previous posting.  This one, I hope, makes more sense.


--phil--