On 27 May 2012, at 11:47, Rob Arthan wrote:

> 
>> .. or  generalise the above definitions to the notion of an equivalence 
>> relation on a subset:
> 
> let refl_on_def = new_definition
>   `ReflOn R P = !x:'a. P x ==> R x x`;;
> let symm_on_def = new_definition
>   `SymmOn R P = !x y:'a. P x /\ P y /\ R x y ==> R y x`;;
> let trans_on_def = new_definition 
>   `TransOn R P = !x y z:'a. P x /\ P y /\ P z /\ R x y /\ R y z ==> R x z`;;
> let equiv_rel_on_def = new_definition
>   `EquivRelOn R P = (ReflOn R P /\ SymmOn R P /\ TransOn R P)`;;
> 
> So you can write `EquivRelOn (\A B. (A, B) same_side l) l`. 

Oops! That  should read `EquivRelOn (\A B. (A, B) same_side l) (\A. ~(A IN 
l))`. 

Regards,

Rob.


------------------------------------------------------------------------------
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

Reply via email to