Re: [isabelle] Inductive Set Definitions

Dear Cristiano,

> In the previous versions of Isabelle i used the "induct" construct to do
> that, but with the later version its counterpart "induct_set" does not
> allow this.

I have no clear idea what your problem really is.  In principial the
inductive_set command should do the job, as in the following (slightly
pointless) example:

inductive_set foo :: "'a set \<Rightarrow> 'a set set"
  for A :: "'a set" where
  "A \<in> foo A"
  | "B \<in> foo A \<Longrightarrow> A \<union> B \<in> foo A"

Could you post a self-contained theory snippet which illustrates your



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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