Tactician is a free and open source utility for refactoring HOL Light
tactic proof scripts. Version 1.3 is out now and can be downloaded
from the Tactician webpage:
www.proof-technologies.com/tactician/index.html
HOL Light's source code contains hundreds of tactic proofs that have
each been neatly packaged up into a single-tactic proof. Although
concise, it can be difficult to step through these proofs
tactic-by-tactic, which is what every user wants to do if they want to
understand a proof. It becomes almost impossible for large tactic
proofs that branch into many subgoals.
However, with Tactician this becomes easy. Just load Tactician into
the HOL Light session immediately before the proof you want to step
through, then process the proof as normal, and then simply execute the
Tactician command "print_flat_proof ();;". This will print out to
screen a flattened version of the proof script that can be stepped
through, with ML comments pointing out where the proof branches.
For example, the following original proof:
let REAL_POW_LT = prove
(`!x n. &0 < x ==> &0 < x pow n`,
REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN
INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_LT_01] THEN
MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]);;
Gets flattened out to this:
g `!x n. &0 < x ==> &0 < x pow n`;;
e (REPEAT STRIP_TAC);;
e (SPEC_TAC (`n:num`,`n:num`));;
e (INDUCT_TAC);;
(* *** Subgoal 1 *** *)
e (REWRITE_TAC [real_pow;REAL_LT_01]);;
(* *** Subgoal 2 *** *)
e (REWRITE_TAC [real_pow;REAL_LT_01]);;
e (MATCH_MP_TAC REAL_LT_MUL);;
e (ASM_REWRITE_TAC []);;
Mark.
------------------------------------------------------------------------------
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
