Back to my other question, there's something about USE_THEN and type
annotations I don't understand. I get the same problem with FIRST_ASSUM. In
Multivariate/topology.ml there's a theorem
let FRONTIER_CLOSURES = prove
(`!s:real^N->bool. frontier s = (closure s) INTER (closure(UNIV DIFF s))`,
let lemma = prove(`s DIFF (UNIV DIFF t) = s INTER t`,SET_TAC[]) in
REWRITE_TAC[frontier; INTERIOR_CLOSURE; lemma]);;
val FRONTIER_CLOSURES : thm =
|- !s. frontier s = closure s INTER closure ((:real^N) DIFF s)
It's fine to get rid of the type annotations and make other changes:
let FRONTIER_CLOSURES = prove
(`!s. frontier s = (closure s) INTER (closure(UNIV DIFF s))`,
REWRITE_TAC [frontier; INTERIOR_CLOSURE;
SET_RULE `!s t. s DIFF (UNIV DIFF t) = s INTER t`]);;
val FRONTIER_CLOSURES : thm =
|- !s. frontier s = closure s INTER closure ((:real^?218238) DIFF s)
however, this doesn't work:
g `!s. frontier s = (closure s) INTER (closure(UNIV DIFF s))`;;
e(SUBGOAL_TAC "EZset" `!s t. s DIFF (UNIV DIFF t) = s INTER t`
[SET_TAC []]);;
e(USE_THEN "EZset" (fun thm -> REWRITE_TAC [frontier; INTERIOR_CLOSURE; thm]));;
# val it : goalstack = 1 subgoal (1 total)
0 [`!s t. s DIFF ((:?218285) DIFF t) = s INTER t`] (EZset)
`!s. closure s DIFF ((:real^?218259) DIFF closure ((:real^?218259) DIFF s)) =
closure s INTER closure ((:real^?218259) DIFF s)`
I get a glimmer of an explanation seeing that the two polymorphic types ?218285
and ?218259. It does work if we type:
g `!s:real^N->bool. frontier s = (closure s) INTER (closure(UNIV DIFF s))`;;
e(SUBGOAL_TAC "EZset" `!s t:real^N->bool. s DIFF (UNIV DIFF t) = s INTER t`
[SET_TAC []]);;
e(USE_THEN "EZset" (fun thm -> REWRITE_TAC [frontier; INTERIOR_CLOSURE; thm]));;
0 [`!s t. s DIFF ((:real^N) DIFF t) = s INTER t`] (EZset)
`!s. frontier s = closure s INTER closure ((:real^N) DIFF s)`
# val it : goalstack = No subgoals
So I have two questions.
1) In what didn't work, why can't the 2nd polymorphic type ?218259 be
"instantiated" as the first polymorphic type ?218285?
2) Why don't we get this polymorphic type incompatibility with the previous
untyped working SET_RULE example?
This shows that it's not a problem with labels or USE_THEN. The same problem
arises without labels:
g `!s. frontier s = (closure s) INTER (closure(UNIV DIFF s))`;;
e(SUBGOAL_TAC "" `!s t. s DIFF (UNIV DIFF t) = s INTER t` [SET_TAC []] THEN
FIRST_ASSUM (fun thm -> REWRITE_TAC [frontier; INTERIOR_CLOSURE; thm]));;
g `!s:real^N->bool. frontier s = (closure s) INTER (closure(UNIV DIFF s))`;;
e(SUBGOAL_TAC "" `!s t:real^N->bool. s DIFF (UNIV DIFF t) = s INTER t`
[SET_TAC []] THEN
FIRST_ASSUM (fun thm -> REWRITE_TAC [frontier; INTERIOR_CLOSURE; thm]));;
# Warning: inventing type variables
val it : goalstack = 1 subgoal (1 total)
0 [`!s t. s DIFF ((:?218607) DIFF t) = s INTER t`]
`!s. closure s DIFF ((:real^?218581) DIFF closure ((:real^?218581) DIFF s)) =
closure s INTER closure ((:real^?218581) DIFF s)`
# val it : goalstack = 1 subgoal (1 total)
`!s. frontier s = closure s INTER closure ((:real^N) DIFF s)`
# val it : goalstack = No subgoals
--
Best,
Bill
------------------------------------------------------------------------------
Managing the Performance of Cloud-Based Applications
Take advantage of what the Cloud has to offer - Avoid Common Pitfalls.
Read the Whitepaper.
http://pubads.g.doubleclick.net/gampad/clk?id=121054471&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
