Hi Ramana,
I will make a few performance improvements on the HOL Light version in the
coming weeks hopefully, and then I plan indeed to translate it to HOL4.
V.
2013/7/30 Ramana Kumar ramana.ku...@cl.cam.ac.uk
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=48808831iu=/4140/ostg.clktrk
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
--
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=49501711iu=/4140/ostg.clktrk___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
