|
28
|
1 |
theory MyTree
|
|
|
2 |
imports Main
|
|
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
datatype
|
|
|
6 |
'a tree = Tip |
|
|
|
7 |
Node " 'a tree" 'a " 'a tree"
|
|
|
8 |
|
|
|
9 |
fun mirror :: " 'a tree \<Rightarrow> 'a tree" where
|
|
|
10 |
"mirror Tip = Tip" |
|
|
|
11 |
"mirror (Node l a r) = Node (mirror r) a (mirror l)"
|
|
|
12 |
|
|
|
13 |
lemma "mirror(mirror t) = t"
|
|
|
14 |
apply(induction t)
|
|
|
15 |
apply(auto)
|
|
|
16 |
done
|
|
|
17 |
|
|
|
18 |
datatype 'a option = None | Some 'a
|
|
|
19 |
|
|
|
20 |
fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
|
|
|
21 |
"lookup [] x = None" |
|
|
|
22 |
"lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
|
|
|
23 |
|
|
|
24 |
definition sq :: "nat \<Rightarrow> nat" where
|
|
|
25 |
"sq n = n * n"
|
|
|
26 |
|
|
|
27 |
abbreviation sq' :: "nat \<Rightarrow> nat" where
|
|
|
28 |
"sq' n \<equiv> n * n"
|
|
|
29 |
|
|
|
30 |
fun div2 :: "nat \<Rightarrow> nat" where
|
|
|
31 |
"div2 0 = 0" |
|
|
|
32 |
"div2 (Suc 0) = 0" |
|
|
|
33 |
"div2 (Suc(Suc n)) = Suc(div2 n)"
|
|
|
34 |
|
|
|
35 |
lemma "div2(n) = n div 2"
|
|
|
36 |
apply(induction n rule: div2.induct)
|
|
|
37 |
apply(auto)
|
|
|
38 |
done
|
|
|
39 |
|
|
|
40 |
value "div2 8"
|
|
|
41 |
|
|
|
42 |
|