Re: [isabelle] Fwd: problem with inductive definition



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
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.