author | wenzelm |
Sat, 28 Nov 2020 15:15:53 +0100 | |
changeset 72755 | 8dffbe01a3e1 |
parent 71818 | 986d5abbe77c |
permissions | -rw-r--r-- |
61232 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
section "AVL Tree Implementation of Maps" |
|
4 |
||
5 |
theory AVL_Map |
|
6 |
imports |
|
7 |
AVL_Set |
|
8 |
Lookup2 |
|
9 |
begin |
|
10 |
||
71818 | 11 |
fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree_ht \<Rightarrow> ('a*'b) tree_ht" where |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68440
diff
changeset
|
12 |
"update x y Leaf = Node Leaf ((x,y), 1) Leaf" | |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68440
diff
changeset
|
13 |
"update x y (Node l ((a,b), h) r) = (case cmp x a of |
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68440
diff
changeset
|
14 |
EQ \<Rightarrow> Node l ((x,y), h) r | |
61581 | 15 |
LT \<Rightarrow> balL (update x y l) (a,b) r | |
16 |
GT \<Rightarrow> balR l (a,b) (update x y r))" |
|
61232 | 17 |
|
71818 | 18 |
fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree_ht \<Rightarrow> ('a*'b) tree_ht" where |
61232 | 19 |
"delete _ Leaf = Leaf" | |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68440
diff
changeset
|
20 |
"delete x (Node l ((a,b), h) r) = (case cmp x a of |
71636 | 21 |
EQ \<Rightarrow> if l = Leaf then r |
22 |
else let (l', ab') = split_max l in balR l' ab' r | |
|
61581 | 23 |
LT \<Rightarrow> balR (delete x l) (a,b) r | |
24 |
GT \<Rightarrow> balL l (a,b) (delete x r))" |
|
61232 | 25 |
|
26 |
||
68422 | 27 |
subsection \<open>Functional Correctness\<close> |
61232 | 28 |
|
68440 | 29 |
theorem inorder_update: |
61232 | 30 |
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
61581 | 31 |
by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR) |
61232 | 32 |
|
33 |
||
68440 | 34 |
theorem inorder_delete: |
61232 | 35 |
"sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
36 |
by(induction t) |
|
61581 | 37 |
(auto simp: del_list_simps inorder_balL inorder_balR |
71636 | 38 |
inorder_split_maxD split: prod.splits) |
61232 | 39 |
|
68422 | 40 |
|
41 |
subsection \<open>AVL invariants\<close> |
|
42 |
||
43 |
||
44 |
subsubsection \<open>Insertion maintains AVL balance\<close> |
|
45 |
||
46 |
theorem avl_update: |
|
47 |
assumes "avl t" |
|
48 |
shows "avl(update x y t)" |
|
49 |
"(height (update x y t) = height t \<or> height (update x y t) = height t + 1)" |
|
50 |
using assms |
|
51 |
proof (induction x y t rule: update.induct) |
|
52 |
case eq2: (2 x y l a b h r) |
|
53 |
case 1 |
|
54 |
show ?case |
|
55 |
proof(cases "x = a") |
|
56 |
case True with eq2 1 show ?thesis by simp |
|
57 |
next |
|
58 |
case False |
|
59 |
with eq2 1 show ?thesis |
|
60 |
proof(cases "x<a") |
|
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
61 |
case True with eq2 1 show ?thesis by (auto intro!: avl_balL) |
68422 | 62 |
next |
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
63 |
case False with eq2 1 \<open>x\<noteq>a\<close> show ?thesis by (auto intro!: avl_balR) |
68422 | 64 |
qed |
65 |
qed |
|
66 |
case 2 |
|
67 |
show ?case |
|
68 |
proof(cases "x = a") |
|
69 |
case True with eq2 1 show ?thesis by simp |
|
70 |
next |
|
71 |
case False |
|
72 |
show ?thesis |
|
73 |
proof(cases "x<a") |
|
74 |
case True |
|
75 |
show ?thesis |
|
76 |
proof(cases "height (update x y l) = height r + 2") |
|
77 |
case False with eq2 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2) |
|
78 |
next |
|
79 |
case True |
|
80 |
hence "(height (balL (update x y l) (a,b) r) = height r + 2) \<or> |
|
81 |
(height (balL (update x y l) (a,b) r) = height r + 3)" (is "?A \<or> ?B") |
|
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
82 |
using eq2 2 \<open>x<a\<close> height_balL[OF _ _ True] by simp |
68422 | 83 |
thus ?thesis |
84 |
proof |
|
85 |
assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto) |
|
86 |
next |
|
87 |
assume ?B with True 1 eq2(2) \<open>x < a\<close> show ?thesis by (simp) arith |
|
88 |
qed |
|
89 |
qed |
|
90 |
next |
|
91 |
case False |
|
92 |
show ?thesis |
|
93 |
proof(cases "height (update x y r) = height l + 2") |
|
94 |
case False with eq2 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2) |
|
95 |
next |
|
96 |
case True |
|
97 |
hence "(height (balR l (a,b) (update x y r)) = height l + 2) \<or> |
|
98 |
(height (balR l (a,b) (update x y r)) = height l + 3)" (is "?A \<or> ?B") |
|
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
99 |
using eq2 2 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> height_balR[OF _ _ True] by simp |
68422 | 100 |
thus ?thesis |
101 |
proof |
|
102 |
assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto) |
|
103 |
next |
|
104 |
assume ?B with True 1 eq2(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith |
|
105 |
qed |
|
106 |
qed |
|
107 |
qed |
|
108 |
qed |
|
109 |
qed simp_all |
|
110 |
||
111 |
||
112 |
subsubsection \<open>Deletion maintains AVL balance\<close> |
|
113 |
||
114 |
theorem avl_delete: |
|
115 |
assumes "avl t" |
|
116 |
shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1" |
|
117 |
using assms |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
68440
diff
changeset
|
118 |
proof (induct t rule: tree2_induct) |
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
119 |
case (Node l ab h r) |
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
120 |
obtain a b where [simp]: "ab = (a,b)" by fastforce |
68422 | 121 |
case 1 |
122 |
show ?case |
|
123 |
proof(cases "x = a") |
|
71636 | 124 |
case True with Node 1 show ?thesis |
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
125 |
using avl_split_max[of l] by (auto intro!: avl_balR split: prod.split) |
68422 | 126 |
next |
127 |
case False |
|
128 |
show ?thesis |
|
129 |
proof(cases "x<a") |
|
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
130 |
case True with Node 1 show ?thesis by (auto intro!: avl_balR) |
68422 | 131 |
next |
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
132 |
case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto intro!: avl_balL) |
68422 | 133 |
qed |
134 |
qed |
|
135 |
case 2 |
|
136 |
show ?case |
|
137 |
proof(cases "x = a") |
|
71636 | 138 |
case True then show ?thesis using 1 avl_split_max[of l] |
139 |
by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split) |
|
68422 | 140 |
next |
141 |
case False |
|
142 |
show ?thesis |
|
143 |
proof(cases "x<a") |
|
144 |
case True |
|
145 |
show ?thesis |
|
146 |
proof(cases "height r = height (delete x l) + 2") |
|
147 |
case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def) |
|
148 |
next |
|
149 |
case True |
|
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
150 |
thus ?thesis using height_balR[OF _ _ True, of ab] 2 Node(1,2) \<open>x < a\<close> by simp linarith |
68422 | 151 |
qed |
152 |
next |
|
153 |
case False |
|
154 |
show ?thesis |
|
155 |
proof(cases "height l = height (delete x r) + 2") |
|
156 |
case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def) |
|
157 |
next |
|
71806
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
158 |
case True |
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
159 |
thus ?thesis |
884c6c0bc99a
use abs(h l - h r) instead of 3 cases, tuned proofs
nipkow
parents:
71636
diff
changeset
|
160 |
using height_balL[OF _ _ True, of ab] 2 Node(3,4) \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> by auto |
68422 | 161 |
qed |
162 |
qed |
|
163 |
qed |
|
164 |
qed simp_all |
|
165 |
||
166 |
||
68440 | 167 |
interpretation M: Map_by_Ordered |
68431 | 168 |
where empty = empty and lookup = lookup and update = update and delete = delete |
68422 | 169 |
and inorder = inorder and inv = avl |
61232 | 170 |
proof (standard, goal_cases) |
68431 | 171 |
case 1 show ?case by (simp add: empty_def) |
61232 | 172 |
next |
61790 | 173 |
case 2 thus ?case by(simp add: lookup_map_of) |
61232 | 174 |
next |
68440 | 175 |
case 3 thus ?case by(simp add: inorder_update) |
61232 | 176 |
next |
68440 | 177 |
case 4 thus ?case by(simp add: inorder_delete) |
68422 | 178 |
next |
68431 | 179 |
case 5 show ?case by (simp add: empty_def) |
68422 | 180 |
next |
181 |
case 6 thus ?case by(simp add: avl_update(1)) |
|
182 |
next |
|
183 |
case 7 thus ?case by(simp add: avl_delete(1)) |
|
184 |
qed |
|
61232 | 185 |
|
186 |
end |