Note that any relation A satisfying !u v z. A u v /\ A u z ==> (u = z)
must be a subset of the identity relation. Specialise the above with x, y, y and you get A x y /\ A x y ==> x = y Michael On 30/05/14 02:39, David Sanan wrote: > Hi all, > I am trying to prove this simple property over the transition closure of a > relation Next, which is defined used Hol_reln, > ((TC (Next h l)) x y) > /\ ((TC (Next h l)) x x) > /\ (!u v z.((Next h l) u v) /\ ((Next h l) u z) ==> u=z) > ==> > (((TC (Next h l)) x)=((TC (Next h l)) y)) > For that I prove using METIS_TAC [TC_RULES] the following theorem > val EQ_TC_SETS = store_thm( > "EQ_TC_SETS", > ``((TC A) x y) > /\ ((TC A) x x) > /\ (!u v z.(A u v) /\ (A u z) ==> u=z) > ==> > (((TC A) x)=((TC A) y))``, > METIS_TAC [TC_RULES] > ); > So I would like to prove the property over Next relation using EQ_TC_SETS. I > know it is a simple thing (or I think so) but I don't find how to use this > theorem EQ_TC_SETS to substitute (Next h l) for A so I can solve (I think) > this. I have try RW_TAC and FULL_SIMP_TAC, but they leave the subgoal > untouched. > Many thanks in advance for any suggestion... > Cheers, > David. > ------------------------------------------------------------------------------ > Time is money. Stop wasting it! Get your web API in 5 minutes. > www.restlet.com/download > http://p.sf.net/sfu/restlet > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Time is money. Stop wasting it! Get your web API in 5 minutes. www.restlet.com/download http://p.sf.net/sfu/restlet
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
