具有非固定參數的感應集合

Question

定義歸納謂詞時，我可以選擇哪些參數是固定的，哪些不是。對於一個人爲的例子考慮：

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

是它在某種程度上可能把它變成一個電感組定義與一個固定的和一個非固定的參數？

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

被拒絕，並顯示錯誤消息：

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

我知道，我可以根據感應謂詞版本定義了一組（例如，Foo P b = {(x, y). foo P b x x}），但後來我一直有前展開它我可以申請歸納或案例分析（或者必須爲Foo引入相應的規則，這似乎有點多餘）。

Answer 1

這是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]