*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Fwd: problem with inductive definition*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 14 Nov 2014 16:02:05 +0100*In-reply-to*: <CAHjcyTMUw7VpMBbbVTXsmeQHjJPSn369e8w-587p35zG42d8aQ@mail.gmail.com>*References*: <CAHjcyTNTjkYS6PzY7_Un-Mx=Mhkm-EjhSBvLizZB4s_YdoTODQ@mail.gmail.com> <CAHjcyTMUw7VpMBbbVTXsmeQHjJPSn369e8w-587p35zG42d8aQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

You want to defined a set, hence the keyword is "inductive_set", not "inductive". Tobias On 14/11/2014 15:51, Ghassen HELALI wrote:

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

**Attachment:
smime.p7s**

**References**:**[isabelle] Fwd: problem with inductive definition***From:*Ghassen HELALI

- Previous by Date: [isabelle] Fwd: problem with inductive definition
- Next by Date: Re: [isabelle] Sublocale, subclass and execution.
- Previous by Thread: [isabelle] Fwd: problem with inductive definition
- Next by Thread: [isabelle] Problem copying logical relation from TAPL
- 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