Re: [Hol-info] How to define PAT_X_ASSUM to PAT_ASSUM in K11 final release (and before) and do nothing in K12 (and later version)?

One thing you could try is to use Globals.version, e.g., val PAT_X_ASSUM = if Globals.version < 12 then PAT_ASSUM else PAT_X_ASSUM; On 25 March 2017 at 07:32, Chun Tian (binghe) wrote: > Hi, > > Currently I’m doing several projects in HOL4, and fortunately > Kananaskis-11

Re: [Hol-info] How to prove ``R = R'`` (two relations are equal) given the corresponding universally qualified form?

I think I get it ... > REWRITE_RULE [FUN_EQ_THM] (ASSUME ``R = R'``); <> val it = [.] |- R = R': thm > REWRITE_RULE [FUN_EQ_THM] (ASSUME ``(R:'a -> 'a -> bool) = R'``); val it = [.] |- ∀x x'. R x x' ⇔ R' x x': thm > Il giorno 24 mar 2017, alle ore 21:50, Thomas Tuerk

Re: [Hol-info] How to prove ``R = R'`` (two relations are equal) given the corresponding universally qualified form?

Hi Thomas, Sorry, I found and tried FUN_EQ_THM, but failed to see the path to benefit from it ... > Il giorno 24 mar 2017, alle ore 21:50, Thomas Tuerk > ha scritto: > > Hi Chun, > > use functional extensionality. There are many ways to do it, one is using > the

Re: [Hol-info] How to prove ``R = R'`` (two relations are equal) given the corresponding universally qualified form?

Hi Chun, use functional extensionality. There are many ways to do it, one is using the theorem boolTheory.FUN_EQ_THM. Best Thomas On 24.03.2017 21:42, Chun Tian (binghe) wrote: > Hi again, > > If I have a theorem saying two (2-ary) relations are the same: > > |- R = R’ > > Then I can easily

[Hol-info] How to prove ``R = R'`` (two relations are equal) given the corresponding universally qualified form?

Hi again, If I have a theorem saying two (2-ary) relations are the same: |- R = R’ Then I can easily prove the following theorem using REWRITE_TAC: |- !x y. R x y = R’ x y But if I had the second one first, how to prove the previous one? Regards, Chun Tian signature.asc Description:

[Hol-info] How to define PAT_X_ASSUM to PAT_ASSUM in K11 final release (and before) and do nothing in K12 (and later version)?

Hi, Currently I’m doing several projects in HOL4, and fortunately Kananaskis-11 was finally released early this month, and for now I only use K-11 final release and not chasing and rebuild HOL from Git master any more. On the other side, I finally learnt to use PAT_X_ASSUM to “pop” any