Dear Antony,
Thank you so much for such a wonderful explanation.
Regards
--- On Tue, 1/29/13, Anthony Fox <[email protected]> wrote:
From: Anthony Fox <[email protected]>
Subject: Re: [Hol-info] HOL4's ARM model- Output Simplification.
To: "hamed nemati" <[email protected]>
Cc: "hol-info" <[email protected]>
Date: Tuesday, January 29, 2013, 3:20 PM
On 29 Jan 2013, at 09:57, hamed nemati <[email protected]> wrote:
> Dear Antony,
>
> Thank you very much for this wonderful explanation! Is there any example of
> such simplification inside the HOL4's ARM model?
>
> Regards,
> Hamed
Hi Hamed,
You can find examples of using “conversions” and “rules” throughout the HOL
distribution. These are often used to perform some sort of “simplification”.
Typically these routines are defined in files with the name *Lib.sml. The ARM
tools (e.g. arm_stepLib) are probably not particularly illustrative though.
You’d be better off reading through some HOL4 documentation, e.g.
http://hol.sourceforge.net/kananaskis-8-helpdocs/help/Docfiles/HTML/bossLib.SIMP_CONV.html
As a very brief primer:
A “conversion” is any SML function with type
: Term.term -> Thm.thm
satisfying the requirement that
cnv ``x``
produces a theorem of the form
|- x = y
For example, the simplifier "SIMP_CONV simpset rwts" is such a conversion:
> SIMP_CONV (srw_ss()) [] ``12w * a + 4w * a: word32``;
val it =
|- 12w * a + 4w * a = 16w * a: thm
Most conversions are suffixed with “_CONV” (but some aren’t, e.g. EVAL).
Conversions can be sequenced using the THENC operator; for example:
> (SIMP_CONV (srw_ss()) [] THENC wordsLib.WORD_MUL_LSL_CONV) ``12w * a + 4w *
> a: word32``;
val it =
|- 12w * a + 4w * a = a ≪ 4: thm
Therefore, the most common way to define new “custom” conversions is to use
existing conversions as building blocks (combining them together with operators
such as THENC, ORELSEC, REPEATC, DEPTH_CONV, RATOR_CONV, ...).
A “rule” is any SML function with type
: Thm.thm -> Thm.thm
Most, but not all, rules are suffixed with “_RULE”. Rules can be built from
conversions using Conv.CONV_RULE. For example:
> Conv.CONV_RULE (Conv.DEPTH_CONV wordsLib.WORD_MUL_LSL_CONV)
(ASSUME ``b = 16w * a : word32``)
val it = [.] |- b = a ≪ 4: thm
Here DEPTH_CONV ensures that the conversion is tried at all positions
(bottom-up).
If you wish to introduce your own definitions then you can use Define. For
example:
val LSL4_def = Define `LSL4 a = (a << 4) : word32`
These definitions can then be used as “rewrites”. For example:
(SIMP_CONV (srw_ss()) []
THENC wordsLib.WORD_MUL_LSL_CONV
THENC REWRITE_CONV [GSYM LSL4_def]) ``12w * a + 4w * a : word32``
val it = |- 12w * a + 4w * a = LSL4 a:
The rule GSYM reverses an equality — so here it ensures that the rewrite
theorem LSL4_def is applied right-to-left.
Thus, given a term or theorem, it’s possible to introduce your own definitions
through the use of conversions and rules.
Regards,
Anthony
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_jan
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
