blob: 8024ce925a88ab7ebea58a35fa737ddbd273b50b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
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
|
