author | wenzelm |
Sat, 28 Nov 2020 15:15:53 +0100 | |
changeset 72755 | 8dffbe01a3e1 |
parent 68440 | 6826718f732d |
permissions | -rw-r--r-- |
61640 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
3 |
section \<open>Unbalanced Tree Implementation of Map\<close> |
61640 | 4 |
|
5 |
theory Tree_Map |
|
6 |
imports |
|
7 |
Tree_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:
61790
diff
changeset
|
11 |
fun lookup :: "('a::linorder*'b) tree \<Rightarrow> 'a \<Rightarrow> 'b option" where |
61640 | 12 |
"lookup Leaf x = None" | |
13 |
"lookup (Node l (a,b) r) x = |
|
14 |
(case cmp x a of LT \<Rightarrow> lookup l x | GT \<Rightarrow> lookup r x | EQ \<Rightarrow> Some b)" |
|
15 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
16 |
fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where |
61640 | 17 |
"update x y Leaf = Node Leaf (x,y) Leaf" | |
18 |
"update x y (Node l (a,b) r) = (case cmp x a of |
|
19 |
LT \<Rightarrow> Node (update x y l) (a,b) r | |
|
20 |
EQ \<Rightarrow> Node l (x,y) r | |
|
21 |
GT \<Rightarrow> Node l (a,b) (update x y r))" |
|
22 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
61790
diff
changeset
|
23 |
fun delete :: "'a::linorder \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where |
61640 | 24 |
"delete x Leaf = Leaf" | |
25 |
"delete x (Node l (a,b) r) = (case cmp x a of |
|
26 |
LT \<Rightarrow> Node (delete x l) (a,b) r | |
|
27 |
GT \<Rightarrow> Node l (a,b) (delete x r) | |
|
68020 | 28 |
EQ \<Rightarrow> if r = Leaf then l else let (ab',r') = split_min r in Node l ab' r')" |
61640 | 29 |
|
30 |
||
31 |
subsection "Functional Correctness Proofs" |
|
32 |
||
61790 | 33 |
lemma lookup_map_of: |
61640 | 34 |
"sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x" |
35 |
by (induction t) (auto simp: map_of_simps split: option.split) |
|
36 |
||
68440 | 37 |
lemma inorder_update: |
61640 | 38 |
"sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)" |
39 |
by(induction t) (auto simp: upd_list_simps) |
|
40 |
||
68440 | 41 |
lemma inorder_delete: |
61640 | 42 |
"sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
68020 | 43 |
by(induction t) (auto simp: del_list_simps split_minD split: prod.splits) |
61640 | 44 |
|
68440 | 45 |
interpretation M: Map_by_Ordered |
68431 | 46 |
where empty = empty and lookup = lookup and update = update and delete = delete |
61686 | 47 |
and inorder = inorder and inv = "\<lambda>_. True" |
61640 | 48 |
proof (standard, goal_cases) |
68431 | 49 |
case 1 show ?case by (simp add: empty_def) |
61640 | 50 |
next |
61790 | 51 |
case 2 thus ?case by(simp add: lookup_map_of) |
61640 | 52 |
next |
68440 | 53 |
case 3 thus ?case by(simp add: inorder_update) |
61640 | 54 |
next |
68440 | 55 |
case 4 thus ?case by(simp add: inorder_delete) |
61686 | 56 |
qed auto |
61640 | 57 |
|
58 |
end |