Bill,
On 27 Dec 2013, at 18:47, Bill Richter wrote:
> ...
> Now this last part surprised me. I didn't know that numerals are
> combinations, and I would have guessed they were constants. So let me
> practice my is_*/dest_* skills:
>
> dest_comb `1`;;
>
> val it : term * term = (`NUMERAL`, `BIT1 _0`)
>
Good point. In my earlier post giving a rule of thumb for recognising when
dest_comb is applicable, I forgot that
(unlike ProofPower-HOL), numeric literals in HOL4 and HOL Light print as if
they are atomic but are actually
nested applications representing an encoding of the number as a string of 0s
and 1s.
> And I think this must be largely defined by this code in nums.ml:
>
> (* -------------------------------------------------------------------------
> *)
> (* Syntax operations on numerals.
> *)
> (* -------------------------------------------------------------------------
> *)
>
> let mk_numeral =
> let Z = mk_const("_0",[])
> and BIT0 = mk_const("BIT0",[])
> and BIT1 = mk_const("BIT1",[])
The definitions should make it clear how these things work:
# ZERO_DEF;;
val it : thm = |- _0 = mk_num IND_0
# NUMERAL;;
val it : thm = |- !n. NUMERAL n = n
# BIT0_DEF;;
val it : thm = |- BIT0 0 = 0 /\ (!n. BIT0 (SUC n) = SUC (SUC (BIT0 n)))
# BIT1_DEF;;
val it : thm = |- !n. BIT1 n = SUC (BIT0 n)
IND_0 is the representative of zero in the type ind that provides the
representation
type for the natural numbers. NUMERAL is just an alias for the identity function
that provokes the pretty-printer into recognising the term as a numeric literal.
BIT0 is \n.2n and BIT1 is \n.2n+1. Hence a string of BIT0s and BIT1 applied to
_0 gives the binary representation of a number in reverse order:
# `NUMERAL(BIT1(BIT1(BIT0(BIT1 _0))))`;;
val it : term = `11`
N.b., the above is specific to HOL Light. HOL4 uses a different representation
based on BIT1 and BIT2 = \n.2n + 2.
> Rob, thanks for explaining some HOL Light to me. Can you (or Michael)
> explain better the HOL4 GSPEC? You say that
>
> It's great that HOL4 isn't grabbing a fresh variable, but I don't get it. I
> suppose HOL4 could check that there's only one free variable, y, in the 2
> "sides" of the set comprehension, and then make an abstraction using the
> ordered pair. But now GSPEC has to translate this ordered pair abstraction
> into the set we want. Let's look at a more general case
>
> {F x y z | R x y z}
>
> for a function F and a predicate R.
Here is the equivalent of HOL4's GSPEC defined in HOL Light:
let HOL4_GSPEC = new_definition `HOL4_GSPEC f v = ?x. f x = (v, T)`;;
The following proof shows that this can be used to represent a set comprehension
without introducing any extra bound variables:
g `{f x | R x} = HOL4_GSPEC (\x.(f x, R x))`;;
e(REWRITE_TAC[SETSPEC; GSPEC; EXTENSION; HOL4_GSPEC; IN; PAIR_EQ]);;
e(MESON_TAC[]);;
let thm1 = top_thm();;
> HOL Light does what I think is the obvious thing, turning this into
>
> λa. ∃ x y z. a = F x y z ∧ R x y z
>
> That's the only abstraction I can think of.
The HOL4 design sees two abstractions here: `\(x, y, z). f x y z` and `\(x, y,
z). R x y z`
and combines them together into one abstraction `\(x, y, z). (f x y z, R x y
z)`.
This contains all the information needed to construct the set comprehension and
the
HOL4 formulation of GSPEC captures that construction.
Regards,
Rob.
------------------------------------------------------------------------------
Rapidly troubleshoot problems before they affect your business. Most IT
organizations don't have a clear picture of how application performance
affects their revenue. With AppDynamics, you get 100% visibility into your
Java,.NET, & PHP application. Start your 15-day FREE TRIAL of AppDynamics Pro!
http://pubads.g.doubleclick.net/gampad/clk?id=84349831&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
