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 <
[email protected]> 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 <[email protected]>
>
>> 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 <
>> [email protected]> 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
>>> [email protected]
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>>
>>
>
>
> --
> Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
> Verification Group
> http://users.encs.concordia.ca/~vincent/
>
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
