Your example can be handled with a bit of simplification. For
example, if you add
- open computeLib
- add_conv(``$COND:bool -> 'a -> 'a -> 'a``, 3, SIMP_CONV bool_ss [])
the_compset;
you get
- EVAL ``update (update not T T) F F``;
> val it = |- update (update not T T) F F = (\z. z) : thm
However, it may be best to exclude the update definition from
the_compset and write custom conversions for simplifying/evaluating
update terms.
You can exclude a definition with:
- computeLib.auto_import_definitions := false;
- Define `update f x y = \z. if z=x then y else (f z)`;
- computeLib.auto_import_definitions := true;
You'll then need something like:
- add_conv(``$update:('a -> 'b) -> 'a -> 'b -> 'a -> 'b``, 3,
SORT_UPDATE) the_compset;
- add_conv(``$update:('a -> 'b) -> 'a -> 'b -> 'a -> 'b``, 4,
EVAL_UPDATE) the_compset;
SORT_UPDATE will depend on the finite domain and you could use
CNV_CONV with some suitable rewrites. In your example, I would aim
for something like:
- EVAL ``update (update not T T) F F```;
> |- update (update not T T) F F = update (update not T T) F F
- EVAL ``update (update not F F) T T```;
> |- update (update not F F) T T = update (update not T T) F F
- EVAL ``(update (update not T T) F F) T```;
> |- (update (update not T T) F F) T = T
Some examples of rewrites for sorting updates can be found in $HOLDIR/
examples/ARM/v4T/updateScript.sml. These are used in arm_evalLib.sml.
Anthony Fox.
On 16 Nov 2007, at 16:01, Bingham, Jesse D wrote:
Thanks to Konrad and Michael for their responses to my previous
question.
Here's another one. I'm not sure if it is a question about EVAL or
a pretty printing question. If I EVAL a function that has a finite
domain (especially a small one), I would like the function to be
represented as a set of pairs. However, EVAL tends to give
unnecessarily complicated terms when dealing with functions. For
example,
Define `update f x y = \z. if z=x then y else (f z)`;
Define `not x = ~x`;
Now let's use update to morph not into the identity on bools.
EVAL ``update (update not T T) F F``;
I would like this to print the bool identity in some succinct
manner (something along the lines of [T |-> T, F |-> F])
Instead, EVAL gives the function as a nested if-then-else lambda
expression:
(\z. (if ~z then F else (if z then T else ~z)))
Things get worse if there are more updates. I tried using
finite_maps and |+ instead of update and got similar results,
modulo notation. How do I get EVAL to crunch a function with a
finite domains down to a set of pairs?
Thanks
-Jesse
----------------------------------------------------------------------
---
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2005.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
