Inductive Set with Non-fixed Parameters

Question

When defining an inductive predicate I can choose which parameters are fixed and which not. For a contrived example consider:

inductive foo for P where
  "foo P True (Inl x) (Inl x)"

Is it somehow possible to turn this into an inductively defined set with one fixed and one non-fixed parameter?

inductive_set Foo for P where
  "(Inl x, Inl x) : Foo P True"

is rejected with the error message:

Argument types 'd, bool of Foo do not agree with types'd of declared parameter

I know that I can define a set based on the inductive predicate version (e.g., Foo P b = {(x, y). foo P b x x}), but then I always have to unfold it before I can apply induction or case-analysis (or have to introduce corresponding rules for Foo, which seems a bit redundant).

Answer 1

This is a limitation of inductive_set, all parameters must be declared as for; in particular, you cannot instantiate them. Currently, the only solution is as you have described: define the predicate first and then introduce corresponding rules for the set. Fortunately, you can use the attributes pred_to_set and to_set to do that automatically. In your example, this looks as follows:

 inductive foo for P where
   "foo P True (Inl x) (Inl x)"

 definition Foo where "Foo P b = {(x, y). foo P b x y}"

 lemma foo_Foo_eq [pred_set_conv]: "foo P b = (%x y. (x, y) : Foo P b)"
 by(simp add: Foo_def)

 lemmas Foo_intros [intro?] = foo.intros[to_set]
 lemmas Foo_induct [consumes 1, induct set: Foo] = foo.induct[to_set]
 lemmas Foo_cases [consumes 1, cases set: Foo] = foo.cases[to_set]
 lemmas Foo_simps = foo.simps[to_set]