17 lines
401 B
Plaintext
17 lines
401 B
Plaintext
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[intro!]: "ζ [] 0" |
|
||
Cons[intro]: "ζ xs l ⟹ ζ (x # xs) (1 + l)"
|
||
|
||
(* Not the answer? *)
|
||
lemma "ζ xs 42"
|
||
oops
|