*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Fwd: problem with inductive definition*From*: Ghassen HELALI <helali at encs.concordia.ca>*Date*: Fri, 14 Nov 2014 09:51:12 -0500*In-reply-to*: <CAHjcyTNTjkYS6PzY7_Un-Mx=Mhkm-EjhSBvLizZB4s_YdoTODQ@mail.gmail.com>*References*: <CAHjcyTNTjkYS6PzY7_Un-Mx=Mhkm-EjhSBvLizZB4s_YdoTODQ@mail.gmail.com>*Sender*: gastongh05 at gmail.com

Dear fellows I am new to Isabelle/HOL and I was trying to define something in an inductive way as follows: inductive Reachable :: "[('action,'state)ts, 'state set] ⇒ 'state set" where here: "s ∈ I ==> s ∈ Reachable S I" | onemore : "[| s ∈ (Reachable S I); mk_trans s a t ∈ trans_of S |] ==> t ∈ (Reachable S I)" But I got an error message: ill-formed introduction rule "here" s ∈ I ==> s ∈ Reachable S I Conclusion of introduction must be an inductive predicate Any helps will be very appreciated Regards --gh

**Follow-Ups**:**Re: [isabelle] Fwd: problem with inductive definition***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...
- Next by Date: Re: [isabelle] Fwd: problem with inductive definition
- Previous by Thread: Re: [isabelle] Problems with BNF_LFP_Rec_Sugar.add_primrec...
- Next by Thread: Re: [isabelle] Fwd: problem with inductive definition
- Cl-isabelle-users November 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list