On 15/08/12 14:41, Bill Richter wrote:
> A counterexample to what you wrote:
> If you never use that [{ n + 1 | n > 6 }] notation, then it's
> certainly fine to just view { x | P x } as a fancy way of writing
> (λx. P x).
> I'll give 3 reasons below to indicate this isn't true for me (I love
> your λ, BTW, and I suppose you can use it in HOL4). Let me first say
> that I think you understand this, as Konrad just posted something of
> this sort:
> each basic set operation (union, intersection, complement,
> powerset, difference, etc) is defined via a set abstraction. These
> definitions tend to be annoying to reason with, so for each
> definition, a theorem with the name IN_<operation> is proved.
In essence, Konrad's point is that it's annoying to prove, for example:
{ x | x ∈ P ∧ x ∈ Q} = λx. P x ∧ Q x
Your examples (deleted) demonstrate that fact; you didn't manage to prove the
equivalences. Nonetheless they're true, and if you tried harder (perhaps
feeding the definitions of GSPEC and SET_SPEC into your justifications), you
might manage them.
My claim ("{x|..} is a fancy way of writing (λx. ..)") is true (by definition,
even). However, working with one notation may well turn out to be
pragmatically
easier.
One exercise you might like to try is completely giving up on set-notation.
Write everything as predicates. If you need notions like intersection, define
predicate versions of these as well. Don't use IN, just use application of a
predicate to the argument.
E.g.,
inter P Q = λx. P x ∧ Q x
union P Q = λx. P x ∨ Q x
image f P = λx. ∃y. P y ∧ x = f y
etc.
You may find the notation unsatisfying, but semantically you will be in exactly
the same place.
Michael
PS: Yes, HOL4 supports Unicode tokens for things like ∪, ∈, ∩, ∀, ∃ and λ etc.
Scroll to the bottom of
http://hol.sourceforge.net/kananaskis-7-helpdocs/help/src-sml/htmlsigs/pred_setTheory.html
to see what this looks like for our pred_setTheory.
------------------------------------------------------------------------------
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
