#
24650ee6 |
|
31-Jan-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add some tools for working with function update (=+). The new directory provides a suitable home for any future theorems/tools wrt =+. To remove redundant updates you can do: > OVERRIDE_UPDATES_CONV ``:num -> 'a`` [] ``(3 =+ a) o (4 =+ b) o (3 =+ a)``; <<HOL message: inventing new type variable names: 'a>> val it = |- (3 =+ a) o (4 =+ b) o (3 =+ c) = (3 =+ a) o (4 =+ b): thm or > OVERRIDE_UPDATES_CONV ``:num -> 'a`` [] ``(3 =+ a) ((4 =+ b) ((3 =+ c) f))``; <<HOL message: inventing new type variable names: 'a>> val it = |- (3 =+ a) ((4 =+ b) ((3 =+ c) f)) = (3 =+ a) ((4 =+ b) f): thm This only works properly when you can evaluate equality on the update domain (there are no free variables), i.e. here we know that 3 <> 4. The second argument is a list of rewrites that can be used to evaluate this equality. To sort updates you can do: > SORT_NUM_UPDATES_CONV ``(4 =+ a) o (3 =+ b) o (2 =+ 1)``; val it = |- (4 =+ a) o (3 =+ b) o (2 =+ 1) = (2 =+ 1) o (3 =+ b) o (4 =+ a): thm This is a specialised version of SORT_UPDATES_MAPTO_CONV, i.e. SORT_NUM_UPDATES_CONV is SORT_UPDATES_MAPTO_CONV ``FST : num # 'a -> num`` numSyntax.less_tm [] The first argument maps the update pair (i.e. (l =+ r)) into some domain (over which we do the sorting); the second argument is an ordering on that domain; and the third argument is a list of evaluation rewrites. Support is provided for sorting ``:'a word -> 'b`` and for ``:enum -> 'a`` for some enumerated type, e.g. > Hol_datatype `enum = One | Two | Three`; <<HOL message: Defined type: "enum">> val it = (): unit > SORT_ENUM_UPDATES_CONV ``:enum`` ``(Two =+ a) o (One =+ b)``; <<HOL message: inventing new type variable names: 'a>> val it = |- (Two =+ a) o (One =+ b) = (One =+ b) o (Two =+ a): thm
|