search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
615 stars 133 forks source link

Induct_on / using example #1073

Open mn200 opened 1 year ago

mn200 commented 1 year ago 
Induct_on `RTC` using relationTheory.RTC_ALT_RIGHT_INDUCT

should work.

konrad-slind commented 1 year ago

How is this different/better than HO_MATCH_MP_TAC relationTheory.RTC_ALT_RIGHT_INDUCT? Is there some kind of normalization/search for an expression in the goal with RTC as its operator?

On Wed, Nov 16, 2022 at 7:38 PM Michael Norrish @.***> wrote:

Induct_on RTC using relationTheory.RTC_ALT_RIGHT_INDUCT

should work.

— Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/1073, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD4LHU2DHAM2CA4CLCTWIWEDBANCNFSM6AAAAAASC3FWM4 . You are receiving this because you are subscribed to this thread.Message ID: @.***>

mn200 commented 1 year ago

Yes, exactly. 

Induct_on `RTC`

does this already (using the default principle) but the form of the alt-right theorem defeats this machinery.