Michael's comments below have been quite interesting to me as part of
understanding set comprehensions better, so thanks Michael! I have
comments and questions below:
On Thu, Aug 16, 2012 at 11:40 PM, Michael Norrish <
[email protected]> wrote:
> 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
Well, maybe not so bad. I did:
# REWRITE_CONV [GSPEC;SETSPEC] `{x + y | x IN P /\ 10 < y}`;;
val it : thm =
|- {x + y | x IN P /\ 10 < y} =
(\GEN%PVAR%219. ?x y. (x IN P /\ 10 < y) /\ GEN%PVAR%219 = x + y)
with a result that is a little simpler than what Michael suggested above,
except for the ugly printing of the generated variable. Renaming gives a
right side of:
\v. ?x y. (x IN P /\ 10 < y) /\ v = x + y
>
> 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.
>
It appears to me that Michael is trying to make a point here that I'm not
grasping, and that maybe his code snippet is not successful in
demonstrating. I have done:
# let tt = `{x + y | x IN P /\ 10 < y} = {x + y | x IN P /\ 10 < y}`;;
val tt : term = `{x + y | x IN P /\ 10 < y} = {x + y | x IN P /\ 10 < y}`
# let rhs = (rand (concl (REWRITE_CONV [IN_ELIM_THM] tt)));;
val rhs : term = `{x + y | x IN P /\ 10 < y}`
# aconv tt rhs;;
val it : bool = true
This says to me that the rewrite with IN_ELIM_THM did not do anything at
all, which is probably not the intended point. Michael, could you clarify
this for us?
Cheers,
Cris
>
> 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
>
------------------------------------------------------------------------------
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
