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 ------------------------------------------------------------------------------ Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft MVPs and experts. ON SALE this month only -- learn more at: http://p.sf.net/sfu/learnnow-d2d _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
