CODEWITHSUNDEEP
isabelletheorem-proving
Charlie Parker
Charlie Parker

Reputation: 5201

How do I add the additional type variables in my specification of an inductive type in Isabelle?

I defined an inductive type like this:

inductive I :: "tau ⇒ bool" where
rule0: "I C0" |
rule1: "I x" |
rule2: "Q x ⟹ I x" |
rule3: "Q x ⟹ I x'" |
rule4: "Q x ⟹ I (C1 x)" |
rule5: "Q (C1 x) ⟹ I x" |
rule6: "Q (C1 x) ⟹ I x'" |
rule7: "Q x ⟹ I (C2 x' x'')"

which I thought would be enough but Isabelle complains/warns me with:

Additional type variable(s) in specification of "I": 'a, 'b

I don't understand what this means. I know that it's saying that I should put somewhere that inductive predicate accepts any two type (as shown by the type variables 'a and 'b). But that isn't what I wanted to do. I just want the input to always be of type tau which is:

datatype tau = 
C0 |
C1 tau |
C2 tau tau

obviously these definitions are made up, not really meant to prove anything. I'm just curious to inspect the theorems (in particular induction) that it generates with these defintions.

1) How do I have it stop complaining about my variables being arbitrary types and have them always be type tau?

As an addition, I became really curious what the complaint means and how to fix it with the 'a and 'b syntax it is suggestion. Although that was not what I initially intended, I am curious to see a more general definition of my made up inductive predicate and see what iduct theorems it will generate.

2) how do I define my inductive predicate with the arbitrary types Isabelle wants? where do I put 'a and 'b in the definition? If I don't what happens?

Upvotes: 0

Views: 208

Answers (1)

Charlie Parker
Charlie Parker

Reputation: 5201

To restrict the type in my rules I can decorate the types in the inductive definition of I:

inductive I :: "tau ⇒ bool"  where
rule0: "I C0" |
rule1: "I x" |
rule2: "Q x ⟹ I x" |
rule3: "Q (x::tau) ⟹ I x'" |
rule4: "Q x ⟹ I (C1 x)" |
rule5: "Q (C1 x) ⟹ I x" |
rule6: "Q (C1 x) ⟹ I x'" |
rule7: "Q (x::tau) ⟹ I (C2 x' x'')"

now the theorems like this:

thm I.induct

⟦I ?x; ?P C0; ⋀x. ?P x; ⋀Q x. Q x ⟹ ?P x; ⋀Q x x'. Q x ⟹ ?P x'; ⋀Q x. Q x ⟹ ?P (C1 x); ⋀Q x. Q (C1 x) ⟹ ?P x; ⋀Q x x'. Q (C1 x) ⟹ ?P x'; ⋀Q x x' x''. Q x ⟹ ?P (C2 x' x'')⟧ ⟹ ?P ?x

Thanks Manuel Eberl!

Upvotes: 1

Related Questions