I suspect that the order of quantification in the goal is important, since
that controls how the induction predicate is instantiated. So try
!Gamma A. Gm Gamma A ==> !Gamma'. ....
since that makes it explicit for the machinery.
Konrad.
On Tue, Jan 15, 2019 at 1:30 AM Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> 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
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
