Hi Konrad and Chun, When I change the goal to ∀A Γ. Gm Γ A ⇒ ∀Γ'. Gm Γ' A, I still get errors with both Induct_on and HO_MATCH_MP_TAC (“not registered in the types database”, “at HolKernel.ho_match_term: at ??.failwith: term_pmatch” respectively).
It appears (to me) that Gm_ind wants Γ and A to always be the same, and I don’t know why. Gm_ind ends with …⇒ ∀a0 a1. Gm a0 a1 ⇒ Gm' a0 a1. Thank you, Alex On 15 Jan 2019, at 19:07, Konrad Slind wrote: 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<mailto: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<mailto: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<mailto:hol-info@lists.sourceforge.net> > https://lists.sourceforge.net/lists/listinfo/hol-info _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto: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
