(to read this easily save it first to file.doc
do conv_extended and then look at it with xpp)
Here is my reproduction of Steve's problem:
=SML
open_theory "z_library";
new_theory "temp";
%SZS%S[X,Y]%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%
%BV% a, b, c: X %fun% Y
%EZ%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%
=SML
set_goal ([], %SZT%%exists%f : S %fun% S%spot% T%>%);
a(z_%exists%_tac %SZT%id S%>%);
=TEX
which gives:
Exception-
Fail
* %SZT%id S%>% cannot be interpreted as a binding that
matches %SZT%%SML%decl_of%SZT%[f :
S %fun% S]%>%%>%%>% [z_%exists%_tac.41021] * raised
Exception+ Fail * %SZT%id S%>% cannot be interpreted as a
binding that matches %SZT%%SML%decl_of%SZT%[f : S %fun%
S]%>%%>%%>% [z_%exists%_tac.41021] * raised
Steve's diagnostic trail was:
=SML
val (asms,concl) = top_goal();
val (decl,_,_) = dest_z_%exists% concl;
val decs = dest_z_decl decl;
val bvars = flat (map (fst o dest_z_dec) decs);
val x = z_type_of (hd bvars);
val y = z_type_of (%SZT%id S%>%);
=TEX
Which ends up with:
val x = %SZT%[a, b, c : (_ %rel% _)] %rel% [a, b, c : (_ %rel%
_)]%>% : TERM
val y = %SZT%[a, b, c : (_ %rel% _)] %rel% [a, b, c : (_ %rel%
_)]%>% : TERM
Unfortunately "z_type_of" yeilds a Z TERM which does not print
with adequate information to discriminate fully between types.
First we show that the values x and y are not the same:
=SML
x =$ y;
=TEX
which gives:
val it = false : bool
A more complete picture can be obtained by looking at the
real type using plain "type_of":
=SML
val hx = type_of (hd bvars);
val hy = type_of (%SZT%id S%>%);
=TEX
which gives:
val hx =
%<:%((('a, 'b) $"Z'T[2]" SET, ('a, 'b) $"Z'T[2]" SET, ('a,
'b) $"Z'T[2]" SET)
$"Z'S[a,b,c]",
(('c, 'd) $"Z'T[2]" SET,
('c, 'd) $"Z'T[2]" SET,
('c, 'd) $"Z'T[2]" SET) $"Z'S[a,b,c]")
$"Z'T[2]" SET%>% : TYPE
:) val hy =
%<:%((('a, 'b) $"Z'T[2]" SET, ('a, 'b) $"Z'T[2]" SET, ('a,
'b) $"Z'T[2]" SET)
$"Z'S[a,b,c]",
(('a, 'b) $"Z'T[2]" SET,
('a, 'b) $"Z'T[2]" SET,
('a, 'b) $"Z'T[2]" SET) $"Z'S[a,b,c]")
$"Z'T[2]" SET%>% : TYPE
Now you can see that hx is more polymorphic than hy since
hx has type variables 'a, 'b, 'c, 'd whereas hy has only 'a, 'b.
The goal above is too general to be proved using the
identity function.
We either need a more specific goal, e.g.:
=SML
set_goal ([], %SZT%%exists%f : S[X,Y] %fun% S[X,Y]%spot% T%>%);
a(z_%exists%_tac %SZT%id S%>%);
=TEX
which gives:
(* *** Goal "" *** *)
(* ?%thm% *) %SZT%id S %mem% S[X, Y] %fun% S[X, Y] %and% true
%and% T%>%
or a more general witness:
=SML
set_goal ([], %SZT%[X,Y,V,W](%exists%f : S[X,Y] %fun%
S[V,W]%spot% T)%>%);
a(REPEAT strip_tac);
a (z_%exists%_tac %SZT%%fn%S[X,Y]%spot%
(%mu%x:S[V,W]%spot%x)%>%);
=TEX
which gives:
(* *** Goal "" *** *)
(* ?%thm% *) %SZT%(%fn% (S[X, Y]) %spot% (%mu% x : S[V, W]))
%mem% S[X, Y] %fun% S[V, W] %and% true %and% T%>%
[and I suspect the proof will fail because we don't know that
the generic sets are non-empty. The goal is false if X and Y are
non-empty but V or W is empty.]
In order to get the types right when generic constants are in
play
it is a good idea to work with generic conjectures.
ProofPower will accept the goal without them, and will give it
its
most general type using lots of type variables, but you won't
know
what the type variables are and you won't have any way of
ensuring
that your witness uses the same type variables.
If you put the explicit generics in then you can force your
witnesses
to the right type by explicitly instantiating them to the generic
sets.
Whether this is indeed the problem that Steve is having its
impossible for me to tell, if not, I need a script which
will reproduce the problem.
Roger Jones