There’s no direct support for this in the system, though I’d certainly like to
extend Induct so that it supported this.
For the moment, you have to set things up by hand. E.g., arrange for the goal
to look like
!n. EVEN n ==> !m. (n = SUC m) ==> ~EVEN m
before then calling Induct_on `EVEN` (assuming EVEN has been defined
inductively, which I don’t think is actually the case in HOL4).
I’ve made a feature request on Github
(https://github.com/HOL-Theorem-Prover/HOL/issues/244), which may help remind
me to implement this very nice feature. (Not that it *has* to be me that
implements it…)
Michael
> On 13 Mar 2015, at 10:39 am, Piotr Trojanek <piotr.troja...@gmail.com> wrote:
>
> Dear HOL4 experts,
>
> Isabelle documentation ("Programming and Proving in Isabelle/HOL",
> section 4.4.6) shows how one can apply "advanced rule induction" to
> goals where an argument of some inductive predicate is not a variable,
> for example,
>
> "EVEN (SUC n) ==> ~ EVEN n".
>
> I could not find anything similar in HOL4 -- did I missed something?
>
> --
> Regards,
> Piotr Trojanek
>
> ------------------------------------------------------------------------------
> Dive into the World of Parallel Programming The Go Parallel Website, sponsored
> by Intel and developed in partnership with Slashdot Media, is your hub for all
> things parallel software development, from weekly thought leadership blogs to
> news, videos, case studies, tutorials and more. Take a look and join the
> conversation now. http://goparallel.sourceforge.net/
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
Dive into the World of Parallel Programming The Go Parallel Website, sponsored
by Intel and developed in partnership with Slashdot Media, is your hub for all
things parallel software development, from weekly thought leadership blogs to
news, videos, case studies, tutorials and more. Take a look and join the
conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
