Hi Bill,
| I'm really happy these two proofs worked, because now I know I can
| code up my Hilbert axiom paper. But I'd prefer (change ray to rag):
|
| let Rag_DEF = new_definition
| `!A B. rag(A, B) = if (A = B) {} else {X | Collinear(A, B, X) /\ ~
Between(X, A, B)`;;
|
| let IN_RAG = prove
| (`!A. !X:point. !B. X IN rag(A, B) <=> ~(A = B) /\ Collinear(A, B, X) /\ ~
Between(X, A, B)`,
| REWRITE_TAC[IN_ELIM_THM; DELETE]);;
|
| Ray_DEF worked but IN_RAY gave the error message
|
| Exception: Failure "term after binary operator expected".
Are you sure there isn't a cut-and-paste error, or that the problem
wasn't actually with Ray_DEF? On the face of it your if-then-else
expression is missing a "then" and shouldn't parse.
| I'm so ignorant, I'm not surprised, so I tried a stunt from sets.ml:
|
| let IN_RAG = prove
| (`!A. !X:point. !B. X IN rag(A, B) <=> ~(A = B) /\ Collinear(A, B, X) /\ ~
Between(X, A, B)`,
| REWRITE_TAC[IN_ELIM_THM; DELETE] THEN SET_TAC[]);;
The basic issue here is that SET_TAC (in common with the other
built-in HOL inference rules and tactics) never implicitly uses
definitions, so you need to either expand them or supply them as
lemmas. It's all at sea here with rag, Collinear and Between.
With that understood, SET_TAC does a fairly competent job of most
routine facts of set theory. Roughly speaking it rewrites with
extensionality and the definition of SUBSET then expands away
set-theoretic definitions to get a pure first-order core that is
solved by MESON. So it can prove really trivial identities like
`{a,b} = {c,d} <=> a = c /\ b = d \/ a = d /\ b = c`
as well as somewhat more interesting lemmas, e.g.
`(!x. f(f x) = x) /\
(!x. x IN s ==> f x IN t) /\ (!x. x IN t ==> f x IN s)
==> IMAGE f s = t /\ IMAGE f t = s`
There are (at least) two notable restrictions/bugs. Neither of these
is hard to fix and I should eventually get round to it, but it would
mean a lot of regression testing to make sure I don't break any
existing proofs.
* The treatment of if-then-else expressions is incomplete since it
isn't properly integrated with the elimination of set-theoretic
concepts.
* Higher-order set concepts (sets of sets etc.) can get expanded
too clumsily and result in a non-first-order goal that is likely
to be unsolvable by MESON, even when a more delicate reduction
would have worked.
John.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
