forked from nipkow/fds_ss20
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ex02.thy
81 lines (54 loc) · 2.06 KB
/
ex02.thy
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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
theory ex02
imports Main
begin
fun list_sum :: "nat list \<Rightarrow> nat" where
"list_sum [] = 0" |
"list_sum (x # xs) = x + list_sum xs"
value "list_sum [1,2,3]"
thm fold.simps
definition list_sum'::"nat list \<Rightarrow> nat" where
"list_sum' xs \<equiv> fold (+) xs (0::nat)"
value "list_sum' [1,2,3]"
thm list_sum'_def
lemma lemma_aux: "fold (+) xs a = list_sum xs + a"
apply(induction xs arbitrary: a)
apply auto
done
lemma "list_sum xs = list_sum' xs"
apply (auto simp: list_sum'_def lemma_aux)
done
datatype 'a ltree = Leaf 'a | Node "'a ltree" "'a ltree"
fun inorder::"'a ltree \<Rightarrow> 'a list" where
"inorder (Leaf x) = [x]" |
"inorder (Node l r) = inorder l @ inorder r"
value "inorder (Node (Node (Leaf (1::nat)) (Leaf 2)) (Leaf 3))"
term "fold f (inorder t) s"
value "fold (+) (inorder (Node (Node (Leaf (1::nat)) (Leaf 2)) (Leaf 3))) 0"
fun fold_ltree:: "('a \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> 'a ltree \<Rightarrow> 's \<Rightarrow> 's" where
"fold_ltree f (Leaf x) s = f x s" |
"fold_ltree f (Node l r) s = fold_ltree f r (fold_ltree f l s)"
value "fold_ltree (+) (Node (Node (Leaf (1::nat)) (Leaf 2)) (Leaf 3)) 0"
lemma "fold f (inorder t) s = fold_ltree f t s"
apply(induction t arbitrary: s)
apply auto
done
fun mirror:: "'a ltree \<Rightarrow> 'a ltree" where
"mirror (Leaf x) = Leaf x" |
"mirror (Node l r) = (Node (mirror r) (mirror l))"
value "inorder (mirror (Node (Node (Leaf (1::nat)) (Leaf 2)) (Leaf 3)))"
lemma "inorder (mirror t) = rev (inorder t)"
apply(induction t)
apply auto
done
term "map f xs"
fun shuffles:: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
"shuffles xs [] = [xs]" |
"shuffles [] ys = [ys]" |
"shuffles (x#xs) (y#ys) = map (\<lambda>xs. x # xs) (shuffles xs (y#ys)) @
map (\<lambda>ys. y # ys) (shuffles (x#xs) ys)"
thm shuffles.induct
lemma "zs \<in> set (shuffles xs ys) \<Longrightarrow> length zs = length xs + length ys"
apply(induction xs ys arbitrary: zs rule: shuffles.induct)
apply auto
done
end