Rob, I couldn't use some of your code. This code of yours is fine: let SameSideEquivalenceRelation_THM = thm `; thus Reflexive_Property /\ Symmetric_Property /\ Transitive_Property proof qed by SameSideReflexiveRelation_THM, SameSideSymmetricRelation_THM, SameSideTransitiveRelation_THM`;;
You can paste this in after evaluating my code from yesterday. But you gave me a definition similar to let equiv_rel_DEF = new_definition `EquivRel = (Reflexive_Property /\ Symmetric_Property /\ Transitive_Property)`;; I think your working code above ought to be identical to let SameSideEquivalenceRelation_THM = thm `; thus EquivRel; qed by SameSideReflexiveRelation_THM, SameSideSymmetricRelation_THM, SameSideTransitiveRelation_THM, equiv_rel_DEF`;; But it doesn't work! I get the error message After thus I get :: #1 :: 1: inference error and at the end I get ::#9 :: 9: syntax error mizar You actual code is 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) (\A. ~(A IN l))`. -- Best, Bill ------------------------------------------------------------------------------ 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
