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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
