在inductive_set中使用mono屬性

Question

我努力證明我的inductive_set滿足必要的單調性要求。有人能告訴我在這裏做錯了嗎？

theory Scratch imports Main begin 

consts foo :: "'a set ⇒ 'a set" 

lemma foo_mono [mono]: 
"x ⊆ y ⟶ foo x ⊆ foo y" 
sorry 

inductive_set blah :: "'a set" 
where 
    "x ∈ foo blah ⟹ x ∈ blah" 
monos foo_mono 

end 

Answer 1

如果你說出你的單調性引理這樣它的工作原理：

lemma foo_mono [mono_set]: 
"A ⊆ B ⟹ x ∈ foo A ⟶ x ∈ foo B" 

另外請注意，您應該使用mono_set屬性，而不是mono，如果你想引理被inductive_set自動使用。也就是說，使用mono_set使inductive_set命令中的monos子句不必要。