1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
theory Verification imports
Notraits
begin
fun height_of_node :: "AVLNode option \<Rightarrow> nat" where
"height_of_node None = 0"
| "height_of_node (Some (mkAVLNode _ l r)) =
max (height_of_node l) (height_of_node r) + 1"
fun is_ok :: "'a result \<Rightarrow> bool" where
"is_ok (Ok _) = True"
| "is_ok _ = False"
lemma[simp]: "is_ok (cmp a b)"
by simp
(* nicer induction rule for type AVLNode option *)
lemma AVLNode_option_induct:
assumes "\<And>v l r. (\<And>x. x \<in> set_option l \<Longrightarrow> P (Some x))
\<Longrightarrow> (\<And>x. x \<in> set_option r \<Longrightarrow> P (Some x))
\<Longrightarrow> P (Some (mkAVLNode v l r))"
and "P None"
shows "P AVLNodeOption"
proof (cases AVLNodeOption)
case None
then show ?thesis using assms by simp
next
case (Some a)
then show ?thesis
apply (induction a arbitrary: AVLNodeOption)
using Some assms(1) by blast
qed
lemma right_is_smaller: "height_of_node r < height_of_node (Some (mkAVLNode v l r))"
by (cases l) auto
lemma left_is_smaller: "height_of_node l < height_of_node (Some (mkAVLNode v l r))"
by (cases r) auto
(* the loop in find always terminates (important for using \<open>obtain\<close> further down *)
termination aVLTreeSet_find_loop
proof (relation "measure (\<lambda>(v, t). height_of_node t)")
show "wf (measure (\<lambda>(v, t). height_of_node t))" by simp
next
fix value1 current_tree and x2 :: "AVLNode"
assume "current_tree = Some x2"
then show "((value1, right x2), value1, current_tree) \<in> measure (\<lambda>(v, t). height_of_node t)"
using right_is_smaller in_measure
by (metis AVLNode.collapse case_prod_conv)
next
fix value1 current_tree and x2 :: "AVLNode"
assume "current_tree = Some x2"
then show "((value1, left x2), value1, current_tree) \<in> measure (\<lambda>(v, t). height_of_node t)"
using left_is_smaller in_measure
by (metis AVLNode.collapse case_prod_conv)
qed
value "cmp (u32 1) (u32 1)"
value "left (mkAVLNode (u32 0) None (Some (mkAVLNode (u32 0) None None)))"
lemma find_loop_ok: "is_ok (aVLTreeSet_find_loop v n)"
proof (induction n arbitrary: v rule: AVLNode_option_induct)
case (1 u l r)
obtain ordering where order: "Ok ordering = cmp u v"
by force
then show ?case
proof (cases ordering)
case Ordering_Less
hence "is_ok (aVLTreeSet_find_loop v r)"
using 1 by (simp add: option.split_sel_asm)
then obtain b r' where a: "Ok (b, r') = aVLTreeSet_find_loop v r"
by (auto elim: is_ok.elims)
hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) =
Ok (b, Some (mkAVLNode u l r'))"
using Ordering_Less order apply simp
by (smt (verit) AVLNode.expand AVLNode.record_simps(12) AVLNode.record_simps(13) AVLNode.record_simps(14) AVLNode.sel(1) AVLNode.sel(2) AVLNode.sel(3) case_prod_conv result.simps(4))
then show ?thesis by simp
next
case Ordering_Equal
hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) = Ok (True, Some (mkAVLNode u l r))"
using 1 order by simp
then show ?thesis by simp
next
case Ordering_Greater
hence "is_ok (aVLTreeSet_find_loop v l)"
using 1 by (simp add: option.split_sel_asm)
then obtain b l' where a: "Ok (b, l') = aVLTreeSet_find_loop v l"
by (auto elim: is_ok.elims)
hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) =
Ok (b, Some (mkAVLNode u l' r))"
using Ordering_Greater order apply simp
by (smt (verit, ccfv_threshold) AVLNode.expand AVLNode.record_simps(6) AVLNode.record_simps(7) AVLNode.record_simps(8) AVLNode.sel(1) AVLNode.sel(2) AVLNode.sel(3) case_prod_conv result.simps(4))
then show ?thesis by simp
qed
next
case 2
then show ?case by simp
qed
(* find never produces an error *)
lemma find_ok: "\<exists>res. aVLTreeSet_find t v = Ok res"
proof -
obtain b as where "Ok (b, as) = aVLTreeSet_find_loop v (root t)"
using find_loop_ok by (metis is_ok.elims(2) old.prod.exhaust)
then have "aVLTreeSet_find t v = Ok (b, \<lparr> root = as \<rparr>)"
apply simp unfolding bind_def
by (metis old.prod.case result.simps(4))
thus ?thesis
by simp
qed
end
|
