Freek, can you explain your code miz3.ml in really broad detail? I think
miz3.ml is an amazing accomplishment, but I don't understand it, and much of
what I don't understand involves parsing.
Petros, thanks for your new stuff, which I haven't understood yet. I ran your
code, which works:
needs "IsabelleLight/make.ml";;
prove (` (?x . x = 5) ==> ?y . y > 4`,
DISCH_THEN (X_MATCH_CHOOSE_TAC `x`) THEN
EXISTS_TAC `x:num` THEN
FIRST_ASSUM SUBST1_TAC THEN ARITH_TAC);;
But I can't figure out from this example what X_MATCH_CHOOSE_TAC is supposed to
be doing. I can prove your result a different way:
let TACtoThmTactic tac = fun ths -> MAP_EVERY MP_TAC ths THEN tac;;
let ARITH_thmTAC = TACtoThmTactic ARITH_TAC;;
let PetrosExample = prove
(`(?x . x = 5) ==> ?y . y > 4`,
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
INTRO_TAC "!x; x5" THEN
EXISTS_TAC `x:num` THEN
HYP ARITH_thmTAC "x5" []);;
Consequence: each time you write `bla`, you automatically go through the
whole process of type inference.
Vincent, thanks for explaining this, and for your new stuff, which I haven't
understood. I had thought that preterm_of_term wouldn't go through type
inference, but it does:
# preterm_of_term `&1 + 1`;;
Exception: Failure "typechecking error (overload resolution)".
So I was wrong. Thanks. However,
1) maybe we can use preterm_of_term if we don't have typechecking error, and
2) I'm sure it's possible to avoid this problem, because miz3 does so. I
usually start an HOL session with
ocaml
#use "hol.ml";;
#load "unix.cma";;
loadt "miz3/miz3.ml";;
and this allows me to evaluate miz3 code, and it doesn't (much) interfere with
straight HOL Light code.
Let me give you a dumb example of what I don't understand about miz3 parsing.
Evaluating this code
`;
let P be point;
let l be point_set;
assume Line l /\ P IN l [H1];
thus ? Q. Q IN l /\ ~(P = Q)
proof
consider A B such that
A IN l /\ B IN l /\ ~(A = B) [l_line] by H1, I2;
cases;
suppose P = A;
qed by -, l_line;
suppose ~(P = A);
qed by -, l_line;
end;
`;;
yields the error message
Error: Unbound value parse_qproof
But first evaluate
#load "unix.cma";;
loadt "miz3/miz3.ml";;
and then evaluate the above, and you'll get sensible miz3 output, i.e. a lot of
errors because none of the terms have been defined. So I know that it's
possible to get the parser to do interesting nonstandard things. I just don't
know how to do them myself.
--
Best,
Bill
------------------------------------------------------------------------------
Minimize network downtime and maximize team effectiveness.
Reduce network management and security costs.Learn how to hire
the most talented Cisco Certified professionals. Visit the
Employer Resources Portal
http://www.cisco.com/web/learning/employer_resources/index.html
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
