theory demo imports Main begin
section ‹Inductive predicates for lists›
datatype 'a list = Nil (“[]”) | Cons 'a “'a list” (“_ # _”)
- fun length
-
“'a list ⇒ nat” where
"length [] = 0" | "length (x # xs) = 1 + length xs"
- inductive ζ
-
“'a list ⇒ nat ⇒ bool” where
Nil: “ζ [] 0” | Cons: “ζ xs l ⟹ ζ (x # xs) (1 + l)”
(* Not the answer? *) lemma “ζ xs 42”
oops