1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
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
theorem len_pred: "ζ xs (length xs)"
proof (induction rule: length.induct)
case 1
then show ?case apply simp ..
next
fix x xs assume "ζ xs (length xs)"
then show "ζ (x # xs) (length (x # xs))"
using ζ.simps by auto
qed
end
|
