HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Published 20 hours ago • verified publisher icon HOL-Theorem-Prover

Induct_on / using example

Open mn200 opened this issue 2 years ago • 2 comments 

Induct_on `RTC` using relationTheory.RTC_ALT_RIGHT_INDUCT

should work.

mn200 avatar Nov 17 '22 01:11 mn200

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: @.***>

konrad-slind avatar Nov 17 '22 07:11 konrad-slind

Yes, exactly.

Induct_on `RTC`

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

mn200 avatar Nov 17 '22 20:11 mn200