Hi David,
I think you could prove your goal with METIS_TAC[EQ_TC_SETS]. (Or even
METIS_TAC[TC_RULES].)
Alternatively, you could do STRIP_TAC THEN MATCH_MP EQ_TC_SETS and
simplification would probably take it from there.
Ramana
On Thu, May 29, 2014 at 5:39 PM, David Sanan <david.sa...@nus.edu.sg> 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
>
------------------------------------------------------------------------------
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
