Michael> cd help/src-sml /bin/hol < DOT
Great, thanks. I don't know how I missed the last few lines of DOT when
I looked around.
--
Ian Zimmerman
gpg public key: 1024D/C6FF61AD
fingerprint: 66DC D68F 5C1B 4D71 2EE5 BD03 8A00 786C C6FF 61AD
http://www.gravatar.com/avatar/c66875cda51109f76c63
On 16/08/2012, at 14:57, Bill Richter wrote:
> So I didn't solve your exercise, which maybe would have required me to
> understand your GSPEC and SET_SPEC, but I see the result should be true.
> Still, I don't admit I was wrong, as your phrase "fancy way of writing" isn't
> precise. What I m
Hi list,
is there a good reason for not using Ocaml modules in HOL Light?
This would yield a better name management, and shorter and more readable
proofs.
For instance, instead of having:
# REAL_ADD_SYM;;
val it : thm = |- !x y. x + y = y + x
# REAL_ADD_LID;;
val it : thm = |- !x. &0 + x = x
#
Thanks, Michael, you're right, I don't want every lambda to be displayed as
{...}. But the main thing I learned from you is that there's no reason for me
to not rewrite the parts of sets.ml that I use (IN_SING etc) to use lambda
rather {...}, as the lambdas are actually equal to {...} defs. It
Hi Vincent,
That's a good question. I think it's mainly down to history. HOL Light was
originally implemented in Caml Light, and was ported to OCaml when it was
already quite a substantial system. Caml Light didn't have a module system,
and modules were not added in the port (except for the inf
Michael, here's a 1-line HOL Light proof of your exercise { x | x ∈ P ∧ x ∈ Q}
= λx. P x ∧ Q x:
let IntersectionAbstractionIsLambda = prove
(`!P Q :A->bool. {x | x IN P /\ x IN Q} = \x. x IN P /\ x IN Q`,
REWRITE_TAC[IN_ELIM_THM; EXTENSION]);;
If you can't do that in HOL4, that's evidence for
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
On 17/08/12 14:11, Bill Richter wrote:
> Michael, here's a 1-line HOL Light proof of your exercise
> { x | x ∈ P ∧ x ∈ Q} = λx. P x ∧ Q x:
>
> let IntersectionAbstractionIsLambda = prove (
> `!P Q :A->bool. {x | x IN P /\ x IN Q} = \x. x IN P /\ x IN Q`,
> REWRITE_TAC[IN_ELIM_THM; EXTENSION]);;
