Thanks, Ramana! I created my thmlist_tactics list in the same way that HOL
Light creates the theorems database in hol_light/database.ml:
needs "help.ml";;
theorems :=
[
"ABSORPTION",ABSORPTION;
"ABS_SIMP",ABS_SIMP;
"ADD",ADD;
[...]
"vector",vector
];;
That doesn't strike me as a painful solution, but I am curious that the only
place that the association list theorems is referred to is help.ml and
update_database.ml.
But the [theorems database] doesn't solve the problem of being able to
represent and evaluate an OCaml expression within OCaml. [...]
[The Scheme-style quote] would not at all be an easy extension to HOL4 or
HOL Light.
Thanks! I'm having a problem with regular expressions. The Str library was
quite helpful, and e.g. I implemented a consider function using
(Str.regexp
"[ \t\n]*consider[ \t\n]+\([^][]+[ \t\n]+such[ \t\n]+that[ \t\n]+[^][]+[
\t\n]+\)\[\([^][]*\)\][ \t\n]+\[\([^!]*\)\][ \t\n]*")
But Str doesn't seem to do everything I want. Take a HOL Light proof that has
only THENs and no THENLs. Suppose we represent the proof as a string s where
THENs are written as semicolons (;). Then
Str.split (Str.regexp "[ \t\n]*;[ \t\n]*") s
returns a list of the substrings delimited by ; and the surrounding whitespace.
In very simple cases, these substrings will represent tactics which should be
joined by THEN. But in more general cases, this won't work, as my tactics
often themselves contain THENs, always contained in a square brace pair []. So
I really want to break the string s up into substrings delimited by semicolons
which are not captured by a square brace pair []. That doesn't sound too
clear, so let me give an example of such a string s representing a proof:
INTRO_TAC ∀A B C A' B', H1, H2 ;
consider X such that
move (A,B,C) (A,B,X) ∧ move (A,B,X) (A',B,X) [ABX]
[HYP fol H1 H2 [Basic2move_THM]];
¬collinear {A,B,X} ∧ ¬collinear {A',B,X} []
[so (HYP fol H1 [moveInvariant, ORIENTED_AREA_COLLINEAR_CONG])];
¬collinear {B,A',X} []
[so (fol [collinearSymmetry])];
consider Y such that move (B,A',X) (B,A',Y) ∧ move (B,A',Y) (B',A',Y)
[BA'Y]
[so (HYP fol H2 [Basic2move_THM])];
move (A',B,X) (A',B,Y) ∧ move (A',B,Y) (A',B',Y) []
[HYP fol BA'Y [moveSymmetry]] ;
so (HYP fol ABX [] );
That's actually too simple, because no proof inside a square brace pair
contains a semicolon. Here's an example of such a substring in another proof:
∀n. (∃ q. reachableN p q n ∧ move q p') ⇒ reachableN p p' (SUC n)
[Imp2]
[INTRO_TAC ∀n; REWRITE_TAC[IMP_CONJ, LEFT_IMP_EXISTS_THM];
So I want to delimit my proof string s only using only the semicolons like the
last one, and not the semicolons like the one in the square brace proof
[INTRO_TAC ... THM]
I'm sure I could write a recursive function to do this, but it makes sense for
ocaml to already have functions of this sort. I figure that I want to break up
the string s as
s1 ; s2 ; ... ; sn
where each substring si has the same number of [s as ]s. Do such regexp issues
arise in HOL4 and SML?
--
Best,
Bill
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and
their applications. This 200-page book is written by three acclaimed
leaders in the field. The early access version is available now.
Download your free book today! http://p.sf.net/sfu/neotech_d2d_may
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
