Email Gateway (Aug 19 2022 at 16:39): Email Gateway (Aug 19 2022 at 16:39):From: Ghassen HELALI <helali@encs.concordia.ca>
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
Email Gateway (Aug 19 2022 at 16:39):From: Tobias Nipkow <nipkow@in.tum.de>
You want to defined a set, hence the keyword is "inductive_set", not "inductive".
Tobias
smime.p7s
Last updated: Apr 26 2024 at 04:17 UTC