[isabelle] Fwd: problem with inductive definition
I am new to Isabelle/HOL and I was trying to define something in an
inductive way as follows:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and