61793
|
1 |
(*
|
|
2 |
Author: Tobias Nipkow
|
62130
|
3 |
|
|
4 |
Added trivial cases to function `adjust' to obviate invariants.
|
61793
|
5 |
*)
|
|
6 |
|
62130
|
7 |
section \<open>AA Tree Implementation of Sets\<close>
|
61793
|
8 |
|
|
9 |
theory AA_Set
|
|
10 |
imports
|
|
11 |
Isin2
|
|
12 |
Cmp
|
|
13 |
begin
|
|
14 |
|
|
15 |
type_synonym 'a aa_tree = "('a,nat) tree"
|
|
16 |
|
|
17 |
fun lvl :: "'a aa_tree \<Rightarrow> nat" where
|
|
18 |
"lvl Leaf = 0" |
|
|
19 |
"lvl (Node lv _ _ _) = lv"
|
62130
|
20 |
(*
|
61793
|
21 |
fun invar :: "'a aa_tree \<Rightarrow> bool" where
|
|
22 |
"invar Leaf = True" |
|
|
23 |
"invar (Node h l a r) =
|
|
24 |
(invar l \<and> invar r \<and>
|
|
25 |
h = lvl l + 1 \<and> (h = lvl r + 1 \<or> (\<exists>lr b rr. r = Node h lr b rr \<and> h = lvl rr + 1)))"
|
62130
|
26 |
*)
|
61793
|
27 |
fun skew :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
|
|
28 |
"skew (Node lva (Node lvb t1 b t2) a t3) =
|
|
29 |
(if lva = lvb then Node lva t1 b (Node lva t2 a t3) else Node lva (Node lvb t1 b t2) a t3)" |
|
|
30 |
"skew t = t"
|
|
31 |
|
|
32 |
fun split :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
|
|
33 |
"split (Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4))) =
|
|
34 |
(if lva = lvb \<and> lvb = lvc (* lva = lvc suffices *)
|
|
35 |
then Node (lva+1) (Node lva t1 a t2) b (Node lva t3 c t4)
|
|
36 |
else Node lva t1 a (Node lvb t2 b (Node lvc t3 c t4)))" |
|
|
37 |
"split t = t"
|
|
38 |
|
|
39 |
hide_const (open) insert
|
|
40 |
|
|
41 |
fun insert :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
|
|
42 |
"insert x Leaf = Node 1 Leaf x Leaf" |
|
|
43 |
"insert x (Node lv t1 a t2) =
|
|
44 |
(case cmp x a of
|
|
45 |
LT \<Rightarrow> split (skew (Node lv (insert x t1) a t2)) |
|
|
46 |
GT \<Rightarrow> split (skew (Node lv t1 a (insert x t2))) |
|
|
47 |
EQ \<Rightarrow> Node lv t1 x t2)"
|
|
48 |
|
|
49 |
(* wrong in paper! *)
|
|
50 |
fun del_max :: "'a aa_tree \<Rightarrow> 'a aa_tree * 'a" where
|
|
51 |
"del_max (Node lv l a Leaf) = (l,a)" |
|
|
52 |
"del_max (Node lv l a r) = (let (r',b) = del_max r in (Node lv l a r', b))"
|
|
53 |
|
|
54 |
fun sngl :: "'a aa_tree \<Rightarrow> bool" where
|
|
55 |
"sngl Leaf = False" |
|
|
56 |
"sngl (Node _ _ _ Leaf) = True" |
|
|
57 |
"sngl (Node lva _ _ (Node lvb _ _ _)) = (lva > lvb)"
|
|
58 |
|
|
59 |
definition adjust :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
|
|
60 |
"adjust t =
|
|
61 |
(case t of
|
|
62 |
Node lv l x r \<Rightarrow>
|
|
63 |
(if lvl l >= lv-1 \<and> lvl r >= lv-1 then t else
|
|
64 |
if lvl r < lv-1 \<and> sngl l then skew (Node (lv-1) l x r) else
|
|
65 |
if lvl r < lv-1
|
|
66 |
then case l of
|
|
67 |
Node lva t1 a (Node lvb t2 b t3)
|
|
68 |
\<Rightarrow> Node (lvb+1) (Node lva t1 a t2) b (Node (lv-1) t3 x r) |
|
|
69 |
_ \<Rightarrow> t (* unreachable *)
|
|
70 |
else
|
|
71 |
if lvl r < lv then split (Node (lv-1) l x r)
|
|
72 |
else
|
|
73 |
case r of
|
|
74 |
Leaf \<Rightarrow> Leaf (* unreachable *) |
|
|
75 |
Node _ t1 b t4 \<Rightarrow>
|
|
76 |
(case t1 of
|
|
77 |
Node lva t2 a t3
|
|
78 |
\<Rightarrow> Node (lva+1) (Node (lv-1) l x t2) a
|
|
79 |
(split (Node (if sngl t1 then lva-1 else lva) t3 b t4))
|
|
80 |
| _ \<Rightarrow> t (* unreachable *))))"
|
|
81 |
|
|
82 |
fun delete :: "'a::cmp \<Rightarrow> 'a aa_tree \<Rightarrow> 'a aa_tree" where
|
|
83 |
"delete _ Leaf = Leaf" |
|
|
84 |
"delete x (Node lv l a r) =
|
|
85 |
(case cmp x a of
|
|
86 |
LT \<Rightarrow> adjust (Node lv (delete x l) a r) |
|
|
87 |
GT \<Rightarrow> adjust (Node lv l a (delete x r)) |
|
|
88 |
EQ \<Rightarrow> (if l = Leaf then r
|
|
89 |
else let (l',b) = del_max l in adjust (Node lv l' b r)))"
|
|
90 |
|
|
91 |
|
|
92 |
subsection "Functional Correctness"
|
|
93 |
|
|
94 |
subsubsection "Proofs for insert"
|
|
95 |
|
|
96 |
lemma inorder_split: "inorder(split t) = inorder t"
|
|
97 |
by(cases t rule: split.cases) (auto)
|
|
98 |
|
|
99 |
lemma inorder_skew: "inorder(skew t) = inorder t"
|
|
100 |
by(cases t rule: skew.cases) (auto)
|
|
101 |
|
|
102 |
lemma inorder_insert:
|
|
103 |
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
|
|
104 |
by(induction t) (auto simp: ins_list_simps inorder_split inorder_skew)
|
|
105 |
|
|
106 |
subsubsection "Proofs for delete"
|
|
107 |
|
|
108 |
lemma del_maxD:
|
62130
|
109 |
"\<lbrakk> del_max t = (t',x); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> inorder t' @ [x] = inorder t"
|
61793
|
110 |
by(induction t arbitrary: t' rule: del_max.induct)
|
|
111 |
(auto simp: sorted_lems split: prod.splits)
|
|
112 |
|
|
113 |
lemma inorder_adjust: "t \<noteq> Leaf \<Longrightarrow> inorder(adjust t) = inorder t"
|
|
114 |
by(induction t)
|
|
115 |
(auto simp: adjust_def inorder_skew inorder_split split: tree.splits)
|
|
116 |
|
|
117 |
lemma inorder_delete:
|
|
118 |
"sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
|
|
119 |
by(induction t)
|
|
120 |
(auto simp: del_list_simps inorder_adjust del_maxD split: prod.splits)
|
|
121 |
|
|
122 |
|
|
123 |
subsection "Overall correctness"
|
|
124 |
|
|
125 |
interpretation Set_by_Ordered
|
|
126 |
where empty = Leaf and isin = isin and insert = insert and delete = delete
|
|
127 |
and inorder = inorder and inv = "\<lambda>_. True"
|
|
128 |
proof (standard, goal_cases)
|
|
129 |
case 1 show ?case by simp
|
|
130 |
next
|
|
131 |
case 2 thus ?case by(simp add: isin_set)
|
|
132 |
next
|
|
133 |
case 3 thus ?case by(simp add: inorder_insert)
|
|
134 |
next
|
|
135 |
case 4 thus ?case by(simp add: inorder_delete)
|
|
136 |
qed auto
|
|
137 |
|
|
138 |
end |