Hi, I think you should use HO_MATCH_MP_TAC (together with your induction theorem of “Gm”, of the form ``!Gm. X ==> P Gm``) in this case. I only use Induct and Induct_on on simple variables like your Γ Γ’ A.
—Chun
> Il giorno 15 gen 2019, alle ore 14:49, Alexander Cox <u6060...@anu.edu.au> ha
> scritto:
>
> I am having an issue using Induct_on on a Hol_reln called Gm.
>
> If I try to use it on a trivial goal it works, e.g.
>
> > g `!Γ A. Gm Γ A ==> Gm Γ A`;
> …
> > e (Induct_on `Gm`);
> OK..
> 1 subgoal:
> val it =
>
>
> (∀A. Gm {|A|} A) ∧ …
>
> but if I use on a useful goal such as:
>
> g `!Γ Γ' A. Gm Γ A ==> Gm (Γ' + Γ) A`;
> …
> e (Induct_on `Gm`);
> OK..
>
> Exception raised at BasicProvers.Induct_on:
> at BasicProvers.induct_on_type:
> Type: :(α formula -> num) -> α formula -> bool is not registered in the types
> database
>
> Any ideas where I’m going wrong? Is the latter the goal in the wrong form?
> Where should I look to figure this out?
>
> Thank you,
> Alex
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
