author | nipkow |
Thu, 16 May 2019 19:43:21 +0200 | |
changeset 70273 | acc1749c2be9 |
parent 68440 | 6826718f732d |
child 70274 | 7daa65d45462 |
permissions | -rw-r--r-- |
61640 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
62130 | 3 |
section \<open>2-3 Tree Implementation of Maps\<close> |
61640 | 4 |
|
5 |
theory Tree23_Map |
|
6 |
imports |
|
7 |
Tree23_Set |
|
67965 | 8 |
Map_Specs |
61640 | 9 |
begin |
10 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
11 |
fun lookup :: "('a::linorder * 'b) tree23 \<Rightarrow> 'a \<Rightarrow> 'b option" where |
61640 | 12 |
"lookup Leaf x = None" | |
13 |
"lookup (Node2 l (a,b) r) x = (case cmp x a of |
|
14 |
LT \<Rightarrow> lookup l x | |
|
15 |
GT \<Rightarrow> lookup r x | |
|
16 |
EQ \<Rightarrow> Some b)" | |
|
17 |
"lookup (Node3 l (a1,b1) m (a2,b2) r) x = (case cmp x a1 of |
|
18 |
LT \<Rightarrow> lookup l x | |
|
19 |
EQ \<Rightarrow> Some b1 | |
|
20 |
GT \<Rightarrow> (case cmp x a2 of |
|
21 |
LT \<Rightarrow> lookup m x | |
|
22 |
EQ \<Rightarrow> Some b2 | |
|
23 |
GT \<Rightarrow> lookup r x))" |
|
24 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
25 |
fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>i" where |
61640 | 26 |
"upd x y Leaf = Up\<^sub>i Leaf (x,y) Leaf" | |
27 |
"upd x y (Node2 l ab r) = (case cmp x (fst ab) of |
|
28 |
LT \<Rightarrow> (case upd x y l of |
|
29 |
T\<^sub>i l' => T\<^sub>i (Node2 l' ab r) |
|
30 |
| Up\<^sub>i l1 ab' l2 => T\<^sub>i (Node3 l1 ab' l2 ab r)) | |
|
31 |
EQ \<Rightarrow> T\<^sub>i (Node2 l (x,y) r) | |
|
32 |
GT \<Rightarrow> (case upd x y r of |
|
33 |
T\<^sub>i r' => T\<^sub>i (Node2 l ab r') |
|
34 |
| Up\<^sub>i r1 ab' r2 => T\<^sub>i (Node3 l ab r1 ab' r2)))" | |
|
35 |
"upd x y (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of |
|
36 |
LT \<Rightarrow> (case upd x y l of |
|
37 |
T\<^sub>i l' => T\<^sub>i (Node3 l' ab1 m ab2 r) |
|
38 |
| Up\<^sub>i l1 ab' l2 => Up\<^sub>i (Node2 l1 ab' l2) ab1 (Node2 m ab2 r)) | |
|
39 |
EQ \<Rightarrow> T\<^sub>i (Node3 l (x,y) m ab2 r) | |
|
40 |
GT \<Rightarrow> (case cmp x (fst ab2) of |
|
41 |
LT \<Rightarrow> (case upd x y m of |
|
42 |
T\<^sub>i m' => T\<^sub>i (Node3 l ab1 m' ab2 r) |
|
43 |
| Up\<^sub>i m1 ab' m2 => Up\<^sub>i (Node2 l ab1 m1) ab' (Node2 m2 ab2 r)) | |
|
44 |
EQ \<Rightarrow> T\<^sub>i (Node3 l ab1 m (x,y) r) | |
|
45 |
GT \<Rightarrow> (case upd x y r of |
|
46 |
T\<^sub>i r' => T\<^sub>i (Node3 l ab1 m ab2 r') |
|
47 |
| Up\<^sub>i r1 ab' r2 => Up\<^sub>i (Node2 l ab1 m) ab2 (Node2 r1 ab' r2))))" |
|
48 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
49 |
definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where |
61640 | 50 |
"update a b t = tree\<^sub>i(upd a b t)" |
51 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
52 |
fun del :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) up\<^sub>d" where |
61640 | 53 |
"del x Leaf = T\<^sub>d Leaf" | |
54 |
"del x (Node2 Leaf ab1 Leaf) = (if x=fst ab1 then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf ab1 Leaf))" | |
|
55 |
"del x (Node3 Leaf ab1 Leaf ab2 Leaf) = T\<^sub>d(if x=fst ab1 then Node2 Leaf ab2 Leaf |
|
56 |
else if x=fst ab2 then Node2 Leaf ab1 Leaf else Node3 Leaf ab1 Leaf ab2 Leaf)" | |
|
57 |
"del x (Node2 l ab1 r) = (case cmp x (fst ab1) of |
|
58 |
LT \<Rightarrow> node21 (del x l) ab1 r | |
|
59 |
GT \<Rightarrow> node22 l ab1 (del x r) | |
|
68020 | 60 |
EQ \<Rightarrow> let (ab1',t) = split_min r in node22 l ab1' t)" | |
61640 | 61 |
"del x (Node3 l ab1 m ab2 r) = (case cmp x (fst ab1) of |
62 |
LT \<Rightarrow> node31 (del x l) ab1 m ab2 r | |
|
68020 | 63 |
EQ \<Rightarrow> let (ab1',m') = split_min m in node32 l ab1' m' ab2 r | |
61640 | 64 |
GT \<Rightarrow> (case cmp x (fst ab2) of |
65 |
LT \<Rightarrow> node32 l ab1 (del x m) ab2 r | |
|
68020 | 66 |
EQ \<Rightarrow> let (ab2',r') = split_min r in node33 l ab1 m ab2' r' | |
61640 | 67 |
GT \<Rightarrow> node33 l ab1 m ab2 (del x r)))" |
68 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
69 |
definition delete :: "'a::linorder \<Rightarrow> ('a*'b) tree23 \<Rightarrow> ('a*'b) tree23" where |
61640 | 70 |
"delete x t = tree\<^sub>d(del x t)" |
71 |
||
72 |
||
73 |
subsection \<open>Functional Correctness\<close> |
|
74 |
||
61790 | 75 |
lemma lookup_map_of: |
76 |
"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
|
61640 | 77 |
by (induction t) (auto simp: map_of_simps split: option.split) |
78 |
||
79 |
||
80 |
lemma inorder_upd: |
|
61789 | 81 |
"sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)" |
61640 | 82 |
by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits) |
83 |
||
68440 | 84 |
corollary inorder_update: |
61789 | 85 |
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)" |
61640 | 86 |
by(simp add: update_def inorder_upd) |
87 |
||
88 |
||
70273 | 89 |
lemma inorder_del: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
61640 | 90 |
inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" |
91 |
by(induction t rule: del.induct) |
|
68020 | 92 |
(auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) |
61640 | 93 |
|
70273 | 94 |
corollary inorder_delete: "\<lbrakk> complete t ; sorted1(inorder t) \<rbrakk> \<Longrightarrow> |
61640 | 95 |
inorder(delete x t) = del_list x (inorder t)" |
96 |
by(simp add: delete_def inorder_del) |
|
97 |
||
98 |
||
99 |
subsection \<open>Balancedness\<close> |
|
100 |
||
70273 | 101 |
lemma complete_upd: "complete t \<Longrightarrow> complete (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t" |
63636 | 102 |
by (induct t) (auto split!: if_split up\<^sub>i.split)(* 16 secs in 2015 *) |
61640 | 103 |
|
70273 | 104 |
corollary complete_update: "complete t \<Longrightarrow> complete (update x y t)" |
105 |
by (simp add: update_def complete_upd) |
|
61640 | 106 |
|
107 |
||
70273 | 108 |
lemma height_del: "complete t \<Longrightarrow> height(del x t) = height t" |
61640 | 109 |
by(induction x t rule: del.induct) |
68020 | 110 |
(auto simp add: heights max_def height_split_min split: prod.split) |
61640 | 111 |
|
70273 | 112 |
lemma complete_tree\<^sub>d_del: "complete t \<Longrightarrow> complete(tree\<^sub>d(del x t))" |
61640 | 113 |
by(induction x t rule: del.induct) |
70273 | 114 |
(auto simp: completes complete_split_min height_del height_split_min split: prod.split) |
61640 | 115 |
|
70273 | 116 |
corollary complete_delete: "complete t \<Longrightarrow> complete(delete x t)" |
117 |
by(simp add: delete_def complete_tree\<^sub>d_del) |
|
61640 | 118 |
|
119 |
||
120 |
subsection \<open>Overall Correctness\<close> |
|
121 |
||
68440 | 122 |
interpretation M: Map_by_Ordered |
68431 | 123 |
where empty = empty and lookup = lookup and update = update and delete = delete |
70273 | 124 |
and inorder = inorder and inv = complete |
61640 | 125 |
proof (standard, goal_cases) |
68431 | 126 |
case 1 thus ?case by(simp add: empty_def) |
127 |
next |
|
61790 | 128 |
case 2 thus ?case by(simp add: lookup_map_of) |
61640 | 129 |
next |
68440 | 130 |
case 3 thus ?case by(simp add: inorder_update) |
61640 | 131 |
next |
68440 | 132 |
case 4 thus ?case by(simp add: inorder_delete) |
68431 | 133 |
next |
134 |
case 5 thus ?case by(simp add: empty_def) |
|
61640 | 135 |
next |
70273 | 136 |
case 6 thus ?case by(simp add: complete_update) |
61640 | 137 |
next |
70273 | 138 |
case 7 thus ?case by(simp add: complete_delete) |
68431 | 139 |
qed |
61640 | 140 |
|
141 |
end |