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
