Hi Bill,
| I tried it and I get the same error message. I just posted my code
| (sorry I didn't see that you & Rob had written), and maybe I'll say
| the problems I'm having can probably all be circumvented, as in this
| case I replaced a {P | ... } definition by a boolean function. But it
| would be nice to do exactly what I want as an exercise to show that
| HOL Light is very flexible and can handle the set-theoretic
| constructions that come up naturally in math.
Yes, this may be the core problem: the default built-in miz3 prover
doesn't know much about sets, and may not know that, say, the formulas
S = {x | P x} and !x. x IN S <=> P x are equivalent, as you might have
expected. There is a standard HOL Light tactic called SET_TAC that
does some preprocessing of set operations and then calls MESON. It
would certainly be possible to change the default miz3 prover to do
something similar.
You are probably going to hit quite a few such restrictions as you are
using miz3 pretty heavily, and it may make sense for us to improve the
default miz3 prover as you hit these issues rather than have you work
around them. However, I am a bit short of time to work on it right now
so I can't promise to fix these shortcomings myself in the short term.
| Here's another thing I couldn't do. Let's define Line(A, B) to be the
| (unique if A <> B) line through the points A and B. Well, then I'd
| like to say in my miz3 code
|
| let a = Line(A, B);
|
| I can't get anything like that to work. You ought to be able to do
| that, right? I see that Freek in lagrange1.ml did this:
|
| set coset = \a. {b | b IN g /\ ?x. x IN h /\ b = a**x} [coset];
| !a. coset a = {b' | b' IN g /\ ?x. x IN h /\ b' = a**x} [13];
|
| So maybe it's set and not let, but that didn't work for me.
I don't know exactly what went wrong, but I can say that let is really
a (derived) HOL term construct and needs to conform to the syntax
"let x1 = e1 [and x2 = e2 and ... and xn = en] in E" as part of a
single term. By constrast, "set" is a Mizar and miz3 construct, and
that's what I would expect to work in this situation. (In the world of
standard HOL Light tactics, ABBREV_TAC plays a similar role.) I don't
know why you hit problems with it.
John.
------------------------------------------------------------------------------
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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
