Hi Mark, Thanks for this. This is VERY useful.
Kevin. ________________________________________ From: "Mark" [[email protected]] Sent: July 25, 2012 11:05 PM To: [email protected] Subject: [Hol-info] Tactician 1.3 release 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 ------------------------------------------------------------------------------ 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
