Dear list, please find at https://github.com/aravantv/HOL4-impconv the *HOL4* version of my "implicational conversion" library (originally developped for HOL Light).
Like the HOL Light version, it provides, among other: - a tactic called IMP_REWRITE_TAC, that I discussed a few times here, which takes a theorem of the form P ==> l = r and replaces l by r in a goal adding whatever it needs to make it work properly -- typically conjunction with P; but can also be an implication or even existentials. - a new tactic called TARGET_REWRITE_TAC which is useful basically anytime you need to rewrite a theorem in a precise location or with a theorem which makes the rewriting diverge. It can be used in particular for AC-rewriting. These two tactics, their use cases, and how they improve over existing tactics is described in details in the user manual. Note: This is really just ported from the HOL Light version of the library, unfortunately I don't have in HOL4 any code base as the one that I had in HOL Light in order to test this, so it is absolutely not guaranteed that it works as well as the HOL Light version. Regards, -- Vincent Aravantinos, PhD Analysis and Design of Dependable Systems fortiss GmbH <www.fortiss.org/en> Guerickestrasse 25 | 80805 Munich | Germany ------------------------------------------------------------------------------ Android is increasing in popularity, but the open development platform that developers love is also attractive to malware creators. Download this white paper to learn more about secure code signing practices that can help keep Android apps secure. http://pubads.g.doubleclick.net/gampad/clk?id=65839951&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
