Vince, this is great! May I ask you to learn about miz3? With a little work,
I think miz3.ml can be turned into a general purpose interface for HOL Light,
with much improved readability, with fewer type annotations in particular. The
part of miz3.ml we don't need is what I think is the hard part: the "by"
justifications, dealing with a "by" list, which is order-independent and
comma-separated. We can just use normal HOL Light proofs. The way to learn
about miz3 is to look at Freek's hol_light/miz3/miz3.ml and my example code
hol_light/Examples/inverse_bug_puzzle_miz3.ml and
hol_light/RichterHilbertAxiomGeometry/HilbertAxiom.ml. Anyway:
Then each time you type something that starts with a semi-colon
(e.g., `;blabla`), you obtain the intermediate preterm instead of
the term. If I'm right, this means that you don't have the
backslash problem anymore (since we're going through the John's
parser), but not all the types are infered since we didn't go
through the type checking phasis yet. And you could define a
function disj_preterm easily (once you built your preterm, it is
easy to get the term by using term_of_preterm, generally composed
with retypecheck in order to check that the final term is well
typed).
Thanks! You're explaining something about miz3 I never understood. Let's look
at thm in inverse_bug_puzzle_miz3.ml, which has no unnecessary type
annotations:
let Noncollinear_2Span = thm `;
let u v w be real^2;
assume ~collinear {vec 0,v,w} [H1];
thus ? s t. s % v + t % w = u
proof
!n r. ~(r < n) /\ r <= MIN n n ==> r = n [easy_arith] by ARITH_RULE;
~(w$1 * v$2 = v$1 * w$2) [H1'] by H1, COLLINEAR_3_2Dzero;
consider M such that
M = transp(vector[v;w]):real^2^2 [Mexists];
det M = v$1 * w$2 - w$1 * v$2 by -, DIMINDEX_2, SUM_2,
TRANSP_COMPONENT, VECTOR_2, LAMBDA_BETA, ARITH, CART_EQ, FORALL_2, DET_2;
~(det M = &0) by -, H1', REAL_ARITH;
consider x s t such that
M ** x = u /\ s = x$1 /\ t = x$2 by -, easy_arith, DET_EQ_0_RANK,
RANK_BOUND, MATRIX_FULL_LINEAR_EQUATIONS;
v$1 * s + w$1 * t = u$1 /\ v$2 * s + w$2 * t = u$2 by Mexists, -,
SIMP_TAC[matrix_vector_mul; DIMINDEX_2; SUM_2; TRANSP_COMPONENT; VECTOR_2;
LAMBDA_BETA; ARITH; CART_EQ; FORALL_2] THEN MESON_TAC[];
s % v + t % w = u by -, REAL_MUL_SYM, VECTOR_MUL_COMPONENT,
VECTOR_ADD_COMPONENT, VEC2_TAC;
qed by -;
`;;
The function thm is applied to a term that begins with a semicolon! Just as
you said! And maybe as Freek said, we'd be better to use a different
character, and I see where you use the semicolon, in the if String.sub s 0 1 =
";":
let quotexpander s =
if String.sub s 0 1 = ":" then
"parse_type \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else if String.sub s 0 1 = ";" then
"(fst o parse_preterm o lex o explode) \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else "parse_term \""^(String.escaped s)^"\"";;
OK, I'll go play with that! I hate to be picky, but
1) Freek does not use quotexpander in miz3.ml, and
2) Is there any way to get rid of the initial semicolon?
--
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
