비 고정 매개 변수가있는 유도 세트

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]