[isabelle] inductive_set with non-fixed parameters

Dear all,

I would like to inductively define a set as follows:

locale transition_system =
  fixes en :: "'state => 'transition set"
  fixes ex :: "'transition => 'state => 'state"

  inductive_set paths :: "'state => 'transition list set" where
    "[] : paths p" | "a : en p ==> w : paths (ex a p) ==> a # w : paths p"


I get the error "Argument types ['state] of paths do not agree with types
[] of declared parameters" (added brackets for clarity). However, I cannot
declare this parameter using a for clause, since it is not fixed ("ex a p"
vs. "p").

I was under the impression that the inductive_set command simply uses
inductive to define a predicate and then composes this predicate with
Collect to obtain the set representation. However, it seems that
inductive_set is strictly weaker than inductive.

As of now, I am working around this by doing what I thought inductive_set
was doing by hand. However, this results in quite a lot of boilerplate
since all the introduction, elimination and induction rules have to be
transferred by hand. Is there a reason why the inductive_set command cannot
do this for me?


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