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