On 17/08/12 07:51, Bill Richter wrote:
> There's no reason for me to use these defs explicitly rather than
> IN_ELIM_THM, which uses them, but this definition bewilders me:
> let IN_ELIM_THM = prove
> (`(!P x. x IN GSPEC (\v. P (SETSPEC v)) <=> P (\p t. p /\ (x = t))) /\
> (!p x. x IN GSPEC (\v. ?y. SETSPEC v (p y) y) <=> p x) /\
> (!P x. GSPEC (\v. P (SETSPEC v)) x <=> P (\p t. p /\ (x = t))) /\
> (!p x. GSPEC (\v. ?y. SETSPEC v (p y) y) x <=> p x) /\
> (!p x. x IN (\y. p y) <=> p x)`,
> REPEAT STRIP_TAC THEN REWRITE_TAC[IN; GSPEC] THEN
> TRY(AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM]) THEN
> REWRITE_TAC[SETSPEC] THEN MESON_TAC[]);;
> I'd rather use BETA_THM instead, and I can do this by using lambda defs of
> INTER, UNION etc instead of the {...} defs in sets.ml.
The definitions of GSPEC and SETSPEC support the set-comprehension notation.
When the HOL Light parser sees
{ function on variables v1 v2.. vn | predicate on variables v1 v2 ... vn }
(e.g., { x + y | x ∈ P ∧ 10 < y })
it converts this to
GSPEC (λgv. ∃v1 v2 .. vn. SETSPEC gv (pred on v1 .. vn) (fn on v1 .. vn))
where gv is a completely fresh variable.
In the example, this would be
GSPEC (λgv. ∃x y. SETSPEC gv (x ∈ P ∧ 10 < y) (x + y))
This notation can be seen to have the right meaning if you expand the
definitions of GSPEC and SETSPEC, and get
GSPEC (λgv. ∃x y. (gv = x + y) ∧ x ∈ P ∧ 10 < y)
= (λgv. ∃x y. (gv = x + y) ∧ x ∈ P ∧ 10 < y)
which is the λ-expression you'd write to get the meaning of that comprehension.
The first clause of IN_ELIM_THM is the rewrite you'd want to apply.
Say you're trying to show that
11 ∈ { x + y | x ∈ P ∧ 10 < y }
then the first clause maps variable P to (λf. ∃x y. f (x ∈ P ∧ 10 < y) (x +
y)),
and then replaces the original term with
(λf. ∃x y. f (x ∈ P ∧ 10 < y) (x + y)) (λp t. p ∧ 11 = t)
which then β-reduces to
∃x y. x ∈ P ∧ 10 < y ∧ 11 = x + y
as desired.
Using a rewrite like IN_ELIM is better than simply rewriting with SETSPEC and
GSPEC's definition because doing that will destroy the structure of set
comprehensions that you don't want to simplify just yet.
E.g., try
REWRITE_CONV [GSPEC, SETSPEC] `{x + y | x IN P /\ 10 < y}`
and you'll get something pretty horrible out. But, if you do
REWRITE_CONV [IN_ELIM_THM] `{x + y | x IN P /\ 10 < y}`
it won't be disturbed because it doesn't have that external `x IN` at the front.
Michael
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
