This looks great, Vincent.
Are you interested in working on a version for HOL4?
On Thu, Jul 11, 2013 at 11:08 AM, Vincent Aravantinos <
vincent.aravanti...@gmail.com> wrote:
> Hi list,
>
> I developed a new tactic that 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).
>
> This is a follow-up of the discussion I started a few months ago (
> http://sourceforge.net/mailarchive/message.php?msg_id=30133516), the
> major difference being that it solves the problem raised by Michael Norrish
> (i.e., it could not work under the scope of a quantifier) in a systematic
> and (in my opinion) elegant way.
>
> This change entails that the tactic is much more modular and thus can be
> chained very smoothly. Many preprocessing options also allows it to be a
> (sometimes more powerful) replacement for REWRITE_TAC, SIMP_TAC and even
> MATCH_MP_TAC. Please look at the (draft) manual for more info.
>
> The code is available at: https://github.com/aravantv/impconv (HOL Light
> only for now)
> To install, type:
> # needs "target_rewrite.ml";;
> The pdf manual is available in the directory "manual".
>
> The development of this tactic required quite some work that might be
> useful in other context. This is undocumented for now but is described in a
> paper which is currently under review.
>
> Regards,
> --
> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
> Verification Group
> http://users.encs.concordia.ca/~vincent/
>
>
> ------------------------------------------------------------------------------
> See everything from the browser to the database with AppDynamics
> Get end-to-end visibility with application monitoring from AppDynamics
> Isolate bottlenecks and diagnose root cause in seconds.
> Start your free trial of AppDynamics Pro today!
> http://pubads.g.doubleclick.net/gampad/clk?id=48808831&iu=/4140/ostg.clktrk
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Get your SQL database under version control now!
Version control is standard for application code, but databases havent
caught up. So what steps can you take to put your SQL databases under
version control? Why should you start doing it? Read more to find out.
http://pubads.g.doubleclick.net/gampad/clk?id=49501711&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
