Hi Ramana,
- regarding your example: no, it is not the intended behavior. I'll have
a look asap.
- regarding the infinite loop: do you mean that it goes most of the time
into an infinite loop? This is not normal either... Could you provide me
with such examples?
The examples provided in the manual are a good starting point to grasp a
lil bit better the intended behaviour. Dunno if that helps though.
Unfortunately, on a daily basis, I use only the HOL Light version of it
and could not test on real-life use cases the HOL4 version :-(
Cheers,
V.
On 10.02.2014 18:23, Ramana Kumar wrote:
Hi Vincent,
I have just now started trying to use your new tactic, and I am having
some trouble. When I call IMP_REWRITE_TAC[] on some simple goal like
``p /\ q ==> q /\ p``, it raises an exception (Unchanged). Is this the
intended behaviour? That seems pretty annoying.
Also, I have not yet found a non-trivial example on which it does not
appear to go into an infinite loop. But I haven't looked far yet.
Cheers,
Ramana
On Tue, Jul 30, 2013 at 1:33 PM, Vincent Aravantinos
<vincent.aravanti...@gmail.com <mailto:vincent.aravanti...@gmail.com>>
wrote:
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
<mailto: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
<mailto: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 <http://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/
<http://users.encs.concordia.ca/%7Evincent/>
------------------------------------------------------------------------------
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
<mailto: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/
<http://users.encs.concordia.ca/%7Evincent/>
--
Dr Vincent Aravantinos
Analysis and Design of Dependable Systems
fortiss GmbH <www.fortiss.org/en>
T +49 (0)89 360 35 22 33 | Fx +49 (0)89 360 35 22 50
Guerickestrasse 25 | 80805 Munich | Germany
------------------------------------------------------------------------------
Android™ apps run on BlackBerry®10
Introducing the new BlackBerry 10.2.1 Runtime for Android apps.
Now with support for Jelly Bean, Bluetooth, Mapview and more.
Get your Android app in front of a whole new audience. Start now.
http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
