Here's a toy version of the miz3 interface for HOL Light that I'm aiming for,
with 3 easy proofs. I've coded up quite a bit more (although not case_split),
but this is short enough to show the idea. This was really a lot of fun to
code up. Thanks again to Vince and Freek!
--
Best,
Bill
#load "str.cma";;
let parse_qproof s = (String.sub s 1 (String.length s - 1));;
let thmlist_tactics = [
"fol",MESON_TAC;
"SIMP_TAC",SIMP_TAC;
"REWRITE_TAC",REWRITE_TAC;
"SET_TAC",SET_TAC
];;
let tactics = [
"arith",ARITH_TAC;
"REAL_ARITH_TAC",REAL_ARITH_TAC
];;
let (make_env: goal -> (string * pretype) list) =
fun (asl,w) -> map ((fun (s,ty) -> s,pretype_of_type ty) o dest_var)
(freesl (w::(map (concl o snd) asl)));;
let parse_env_string env s = (term_of_preterm o retypecheck env)
((fst o parse_preterm o lex o explode) s);;
let (exists_TAC: string -> tactic) =
fun stm (asl,w) -> let env = make_env (asl,w) in
EXISTS_TAC (parse_env_string env stm) (asl,w);;
let CleanMathFontsForHOL_Light s =
let s = Str.global_replace (Str.regexp "∀") "!" s in
Str.global_replace (Str.regexp "∃") "?" s;;
let StringRegexpEqual r s = Str.string_match r s 0 &&
s = Str.matched_string s;;
let rec ConvertToHOL s =
if StringRegexpEqual (Str.regexp "[ \t\n]*\([^ \t\n]*\)[ \t\n]*") s
then
let tac = (Str.matched_group 1 s) in
assoc tac tactics
else
if StringRegexpEqual (Str.regexp "[ \t\n]*INTRO_TAC \([^][]*\)") s
then
let labstring = (Str.matched_group 1 s) in
INTRO_TAC (Str.global_replace (Str.regexp ",") ";" labstring)
else
if StringRegexpEqual (Str.regexp "[ \t\n]*exists_TAC \([^][]*\)") s
then
exists_TAC (Str.matched_group 1 s)
else
if StringRegexpEqual (Str.regexp
"[ \t\n]*HYP[ \t\n]*\([^ \t\n]+\)\([^[]+\)\[\([^]]*\)\][ \t\n]*") s
then
let ttac = Str.matched_group 1 s and
labs = Str.matched_group 2 s and
listofThms = Str.split (Str.regexp "[ \t\n]*,[ \t\n]*")
(Str.matched_group 3 s) in
HYP (assoc ttac thmlist_tactics) labs
(map (fun ts -> assoc ts !theorems) listofThms)
else ALL_TAC;;
let organizeTHEN s =
let rec THENify listofString =
match listofString with
[] -> ALL_TAC
| hd::tl -> (ConvertToHOL hd) THEN (THENify tl) in
THENify (Str.split (Str.regexp "[ \t\n]*;[ \t\n]*") s);;
let theorem s =
let sl = Str.split (Str.regexp "[ \t\n]*proof[ \t\n]*")
(CleanMathFontsForHOL_Light s) in
prove (parse_env_string [] (hd sl), organizeTHEN (hd (tl sl)));;
let AXIOM_OF_CHOICE = prove
(`(!x:A. ?y:B. P x y) ==> ?f. !x. P x (f x)`,
STRIP_TAC THEN EXISTS_TAC `\x:A. @y:B. P x y` THEN ASM_MESON_TAC[]);;
let AXIOM_OF_CHOICE = theorem `;
∀P. (∀x. ∃y. P x y) ==> ∃f. ∀x. P x (f x)
proof
INTRO_TAC ∀P, H1 ;
exists_TAC \x. @y. P x y ;
HYP fol H1 []`;;
let ActuallyUsedAtacticByItself = theorem `;
6 + 7 = 13
proof
arith`;;
------------------------------------------------------------------------------
Get 100% visibility into Java/.NET code with AppDynamics Lite
It's a free troubleshooting tool designed for production
Get down to code-level detail for bottlenecks, with <2% overhead.
Download for free and get started troubleshooting in minutes.
http://p.sf.net/sfu/appdyn_d2d_ap2
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
