Hi Peter, Thanks for the interest. Porting to HOL4 is very feasible. Especially if someone could fund me to do this!
Mark. on 27/7/12 3:18 PM, Peter Vincent Homeier <[email protected]> wrote: > Hello, Mark. > > Are you interested in porting this technology to the HOL4 system? > > Peter > > On Wed, Jul 25, 2012 at 11:05 PM, "Mark" <[email protected]>wrote: > >> 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 >> > > -- > "In Your majesty ride prosperously > because of truth, humility, and righteousness; > and Your right hand shall teach You awesome things." (Psalm 45:4) > > > ------------------------------------------------------------------------------ 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
