inductive_set의 모노 속성 사용

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" 

또한 당신이 보조 정리가 inductive_set에 의해 자동으로 사용하려는 경우, 대신 mono의 mono_set 속성을 사용해야 있습니다. 즉, mono_set을 사용하면 inductive_set 명령의 monos 절이 필요하지 않습니다.