1

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).

4

1 回答 1

4

这是一个限制inductive_set，所有参数必须声明为for；特别是，您不能实例化它们。目前，唯一的解决方案是如您所描述的：首先定义谓词，然后为集合引入相应的规则。幸运的是，您可以使用属性pred_to_set并to_set自动执行此操作。在您的示例中，如下所示：

 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]
于 2013-05-17T08:37:01.397 回答