Stream: Beginner Questions

Topic: Conclusion of introduction rule inductive predicate

Yiming Xu (Oct 20 2024 at 07:10):

I am defining a inductive set.

I wrote:

inductive_set urav_seq ::
 "'a set ⇒ 'm set ⇒ ('m ⇒ 'a list ⇒ bool) ⇒ ('a list set)"
 for W :: "'a set" and Op :: "'m set" and R ::"'m ⇒ 'a list ⇒ bool"
 where
 "x ∈ W ⟹ [x] ∈ unrav_seq W Op R"

Isabelle complains

Ill-formed introduction rule ""
W x ⟹ [x] ∈ unrav_seq {x. W x} Op R
Conclusion of introduction rule must be an inductive predicate

I am confused. What is wrong here? Sorry if it turns of to be my stupidness.

Mathias Fleury (Oct 20 2024 at 07:12):

urav

unrav

Mathias Fleury (Oct 20 2024 at 07:13):

Look at the color of the constants ;-)

Yiming Xu (Oct 20 2024 at 07:13):

Thank you! That is indeed my stupid...

Yiming Xu (Oct 20 2024 at 07:13):

Mathias Fleury said:

Look at the color of the constants ;-)

Thanks that is helpful!

Yiming Xu (Oct 20 2024 at 07:14):

The distinction between black/green and black/blue is easier to spot. Here it should be blue but was green. I see.

Last updated: Dec 21 2024 at 16:20 UTC