1 (* |
1 (* |
2 Author: Tobias Nipkow, Daniel Stüwe |
2 Author: Tobias Nipkow, Daniel Stüwe |
3 Based on the AFP entry AVL. |
3 Based on the AFP entry AVL. |
4 *) |
4 *) |
5 |
5 |
6 section "AVL Tree Implementation of Sets" |
6 subsection \<open>Invariant\<close> |
7 |
7 |
8 theory AVL_Set |
8 theory AVL_Set |
9 imports |
9 imports |
10 Cmp |
10 AVL_Set_Code |
11 Isin2 |
|
12 "HOL-Number_Theory.Fib" |
11 "HOL-Number_Theory.Fib" |
13 begin |
12 begin |
14 |
|
15 type_synonym 'a avl_tree = "('a*nat) tree" |
|
16 |
|
17 definition empty :: "'a avl_tree" where |
|
18 "empty = Leaf" |
|
19 |
|
20 text \<open>Invariant:\<close> |
|
21 |
13 |
22 fun avl :: "'a avl_tree \<Rightarrow> bool" where |
14 fun avl :: "'a avl_tree \<Rightarrow> bool" where |
23 "avl Leaf = True" | |
15 "avl Leaf = True" | |
24 "avl (Node l (a,n) r) = |
16 "avl (Node l (a,n) r) = |
25 ((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> |
17 ((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> |
26 n = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" |
18 n = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" |
27 |
|
28 fun ht :: "'a avl_tree \<Rightarrow> nat" where |
|
29 "ht Leaf = 0" | |
|
30 "ht (Node l (a,n) r) = n" |
|
31 |
|
32 definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
|
33 "node l a r = Node l (a, max (ht l) (ht r) + 1) r" |
|
34 |
|
35 definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
|
36 "balL AB b C = |
|
37 (if ht AB = ht C + 2 then |
|
38 case AB of |
|
39 Node A (a, _) B \<Rightarrow> |
|
40 if ht A \<ge> ht B then node A a (node B b C) |
|
41 else |
|
42 case B of |
|
43 Node B\<^sub>1 (ab, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) ab (node B\<^sub>2 b C) |
|
44 else node AB b C)" |
|
45 |
|
46 definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
|
47 "balR A a BC = |
|
48 (if ht BC = ht A + 2 then |
|
49 case BC of |
|
50 Node B (b, _) C \<Rightarrow> |
|
51 if ht B \<le> ht C then node (node A a B) b C |
|
52 else |
|
53 case B of |
|
54 Node B\<^sub>1 (ab, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) ab (node B\<^sub>2 b C) |
|
55 else node A a BC)" |
|
56 |
|
57 fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
|
58 "insert x Leaf = Node Leaf (x, 1) Leaf" | |
|
59 "insert x (Node l (a, n) r) = (case cmp x a of |
|
60 EQ \<Rightarrow> Node l (a, n) r | |
|
61 LT \<Rightarrow> balL (insert x l) a r | |
|
62 GT \<Rightarrow> balR l a (insert x r))" |
|
63 |
|
64 fun split_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where |
|
65 "split_max (Node l (a, _) r) = |
|
66 (if r = Leaf then (l,a) else let (r',a') = split_max r in (balL l a r', a'))" |
|
67 |
|
68 lemmas split_max_induct = split_max.induct[case_names Node Leaf] |
|
69 |
|
70 fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
|
71 "delete _ Leaf = Leaf" | |
|
72 "delete x (Node l (a, n) r) = |
|
73 (case cmp x a of |
|
74 EQ \<Rightarrow> if l = Leaf then r |
|
75 else let (l', a') = split_max l in balR l' a' r | |
|
76 LT \<Rightarrow> balR (delete x l) a r | |
|
77 GT \<Rightarrow> balL l a (delete x r))" |
|
78 |
|
79 |
|
80 subsection \<open>Functional Correctness Proofs\<close> |
|
81 |
|
82 text\<open>Very different from the AFP/AVL proofs\<close> |
|
83 |
|
84 |
|
85 subsubsection "Proofs for insert" |
|
86 |
|
87 lemma inorder_balL: |
|
88 "inorder (balL l a r) = inorder l @ a # inorder r" |
|
89 by (auto simp: node_def balL_def split:tree.splits) |
|
90 |
|
91 lemma inorder_balR: |
|
92 "inorder (balR l a r) = inorder l @ a # inorder r" |
|
93 by (auto simp: node_def balR_def split:tree.splits) |
|
94 |
|
95 theorem inorder_insert: |
|
96 "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
|
97 by (induct t) |
|
98 (auto simp: ins_list_simps inorder_balL inorder_balR) |
|
99 |
|
100 |
|
101 subsubsection "Proofs for delete" |
|
102 |
|
103 lemma inorder_split_maxD: |
|
104 "\<lbrakk> split_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> |
|
105 inorder t' @ [a] = inorder t" |
|
106 by(induction t arbitrary: t' rule: split_max.induct) |
|
107 (auto simp: inorder_balL split: if_splits prod.splits tree.split) |
|
108 |
|
109 theorem inorder_delete: |
|
110 "sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
|
111 by(induction t) |
|
112 (auto simp: del_list_simps inorder_balL inorder_balR inorder_split_maxD split: prod.splits) |
|
113 |
|
114 |
|
115 subsection \<open>AVL invariants\<close> |
|
116 |
|
117 text\<open>Essentially the AFP/AVL proofs\<close> |
|
118 |
19 |
119 |
20 |
120 subsubsection \<open>Insertion maintains AVL balance\<close> |
21 subsubsection \<open>Insertion maintains AVL balance\<close> |
121 |
22 |
122 declare Let_def [simp] |
23 declare Let_def [simp] |