Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Argument types problem

Email Gateway (Aug 19 2022 at 16:43):

From: Ghassen HELALI <helali@encs.concordia.ca>
Dear fellows,
I am about to definie an inductive set to compute the ste of reachable
states as following:

inductive_set
Reachable :: "[('action,'state)ts, 'state set] ⇒ 'state set" where
init: "s ∈ Init ==> s ∈ (Reachable Ts Init)"
| nextStep : "==> [| s ∈ (Reachable Ts Init); (mk_trans s a t) ∈
(trans_of Ts) |] ==> t ∈ (Reachable Ts Init)"

But it was not accepted and I got the following error message:
Argument types ('action, 'state) ts, 'state set of Reachable do not agree
with types of declared parameters

Any helps how to sort out this error please.

--gh

Email Gateway (Aug 19 2022 at 16:44):

From: Makarius <makarius@sketis.net>
The error message is a bit implicit, meaning that the free parameters Ts
and Init should be declared like this:

inductive_set
Reachable :: "[('action,'state)ts, 'state set] ⇒ 'state set"
for Ts :: "('action,'state)ts" and Init :: "'state set"

Also note that camel case is not used in Isabelle sources, so nextStep
should be next_step.

Moreover, there is no need to put extra parentheses around applications
such as (Reachable Ts Init): it binds tightly without that.

Makarius

http://stop-ttip.org 998,638 people so far

Last updated: Apr 25 2024 at 08:20 UTC