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