On 19/11/12 11:01, Michael Norrish wrote:
> Ignoring abbreviations, you could use
> fun simpterm q =
> ASSUM_LIST (fn ths => Q_TAC (ASSUME_TAC o SIMP_CONV (srw_ss()) ths) q)
> This simplifies the term corresponding to assumption q and gives you back the
> resulting assumption.
Err, this sh
On 19/11/12 03:46, Ramana Kumar wrote:
> Thanks for those.
> I just used
> IMP_RES_THEN (assume_tac o SIMP_RULE(srw_ss())[])
> (METIS_PROVE[]``Abbrev(x=y)==>(x.out = y.out)``)
> which worked great for getting an equation for the x.out of every x, but I'm
> not
> sure if I can get it for just one
Thanks for those.
I just used
IMP_RES_THEN (assume_tac o SIMP_RULE(srw_ss())[])
(METIS_PROVE[]``Abbrev(x=y)==>(x.out = y.out)``)
which worked great for getting an equation for the x.out of every x, but
I'm not sure if I can get it for just one of them...
There's probably a way along these lines.
