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]);;
>
> If you can't do that in HOL4, that's evidence for my feeling that IN_ELIM_THM
> is hard to understand.
The tactic in HOL4 would be
SRW_TAC [][EXTENSION]
But it's complicated underneath the hood. The mechanism is different to the
way
HOL Light does it, but it's still complex, and perhaps "hard to understand".
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
