1 header {* Tactic-Style Reasoning for Binary Tree Operations *} |
|
2 theory BinaryTree_TacticStyle = Main: |
|
3 |
|
4 text {* This example theory illustrates automated proofs of correctness |
|
5 for binary tree operations using tactic-style reasoning. |
|
6 The current proofs for remove operation are by Tobias Nipkow, |
|
7 some modifications and the remaining tree operations are |
|
8 by Viktor Kuncak. *} |
|
9 |
|
10 (*============================================================*) |
|
11 section {* Definition of a sorted binary tree *} |
|
12 (*============================================================*) |
|
13 |
|
14 datatype tree = Tip | Nd tree nat tree |
|
15 |
|
16 consts set_of :: "tree => nat set" |
|
17 -- {* The set of nodes stored in a tree. *} |
|
18 primrec |
|
19 "set_of Tip = {}" |
|
20 "set_of(Nd l x r) = set_of l Un set_of r Un {x}" |
|
21 |
|
22 consts sorted :: "tree => bool" |
|
23 -- {* Tree is sorted *} |
|
24 primrec |
|
25 "sorted Tip = True" |
|
26 "sorted(Nd l y r) = |
|
27 (sorted l & sorted r & (ALL x:set_of l. x < y) & (ALL z:set_of r. y < z))" |
|
28 |
|
29 (*============================================================*) |
|
30 section {* Tree Membership *} |
|
31 (*============================================================*) |
|
32 |
|
33 consts |
|
34 memb :: "nat => tree => bool" |
|
35 primrec |
|
36 "memb e Tip = False" |
|
37 "memb e (Nd t1 x t2) = |
|
38 (if e < x then memb e t1 |
|
39 else if x < e then memb e t2 |
|
40 else True)" |
|
41 |
|
42 lemma member_set: "sorted t --> memb e t = (e : set_of t)" |
|
43 by (induct t, auto) |
|
44 |
|
45 (*============================================================*) |
|
46 section {* Insertion operation *} |
|
47 (*============================================================*) |
|
48 |
|
49 consts binsert :: "nat => tree => tree" |
|
50 -- {* Insert a node into sorted tree. *} |
|
51 primrec |
|
52 "binsert x Tip = (Nd Tip x Tip)" |
|
53 "binsert x (Nd t1 y t2) = (if x < y then |
|
54 (Nd (binsert x t1) y t2) |
|
55 else |
|
56 (if y < x then |
|
57 (Nd t1 y (binsert x t2)) |
|
58 else (Nd t1 y t2)))" |
|
59 |
|
60 theorem set_of_binsert [simp]: "set_of (binsert x t) = set_of t Un {x}" |
|
61 by (induct_tac t, auto) |
|
62 |
|
63 theorem binsert_sorted: "sorted t --> sorted (binsert x t)" |
|
64 by (induct_tac t, auto simp add: set_of_binsert) |
|
65 |
|
66 corollary binsert_spec: (* summary specification of binsert *) |
|
67 "sorted t ==> |
|
68 sorted (binsert x t) & |
|
69 set_of (binsert x t) = set_of t Un {x}" |
|
70 by (simp add: binsert_sorted) |
|
71 |
|
72 (*============================================================*) |
|
73 section {* Remove operation *} |
|
74 (*============================================================*) |
|
75 |
|
76 consts |
|
77 remove:: "nat => tree => tree" -- {* remove a node from sorted tree *} |
|
78 -- {* auxiliary operations: *} |
|
79 rm :: "tree => nat" -- {* find the rightmost element in the tree *} |
|
80 rem :: "tree => tree" -- {* find the tree without the rightmost element *} |
|
81 primrec |
|
82 "rm(Nd l x r) = (if r = Tip then x else rm r)" |
|
83 primrec |
|
84 "rem(Nd l x r) = (if r=Tip then l else Nd l x (rem r))" |
|
85 primrec |
|
86 "remove x Tip = Tip" |
|
87 "remove x (Nd l y r) = |
|
88 (if x < y then Nd (remove x l) y r else |
|
89 if y < x then Nd l y (remove x r) else |
|
90 if l = Tip then r |
|
91 else Nd (rem l) (rm l) r)" |
|
92 |
|
93 lemma rm_in_set_of: "t ~= Tip ==> rm t : set_of t" |
|
94 by (induct t) auto |
|
95 |
|
96 lemma set_of_rem: "t ~= Tip ==> set_of t = set_of(rem t) Un {rm t}" |
|
97 by (induct t) auto |
|
98 |
|
99 lemma [simp]: "[| t ~= Tip; sorted t |] ==> sorted(rem t)" |
|
100 by (induct t) (auto simp add:set_of_rem) |
|
101 |
|
102 lemma sorted_rem: "[| t ~= Tip; x \<in> set_of(rem t); sorted t |] ==> x < rm t" |
|
103 by (induct t) (auto simp add:set_of_rem split:if_splits) |
|
104 |
|
105 theorem set_of_remove [simp]: "sorted t ==> set_of(remove x t) = set_of t - {x}" |
|
106 apply(induct t) |
|
107 apply simp |
|
108 apply simp |
|
109 apply(rule conjI) |
|
110 apply fastsimp |
|
111 apply(rule impI) |
|
112 apply(rule conjI) |
|
113 apply fastsimp |
|
114 apply(fastsimp simp:set_of_rem) |
|
115 done |
|
116 |
|
117 theorem remove_sorted: "sorted t ==> sorted(remove x t)" |
|
118 by (induct t) (auto intro: less_trans rm_in_set_of sorted_rem) |
|
119 |
|
120 corollary remove_spec: -- {* summary specification of remove *} |
|
121 "sorted t ==> |
|
122 sorted (remove x t) & |
|
123 set_of (remove x t) = set_of t - {x}" |
|
124 by (simp add: remove_sorted) |
|
125 |
|
126 text {* Finally, note that rem and rm can be computed |
|
127 using a single tree traversal given by remrm. *} |
|
128 |
|
129 consts remrm :: "tree => tree * nat" |
|
130 primrec |
|
131 "remrm(Nd l x r) = (if r=Tip then (l,x) else |
|
132 let (r',y) = remrm r in (Nd l x r',y))" |
|
133 |
|
134 lemma "t ~= Tip ==> remrm t = (rem t, rm t)" |
|
135 by (induct t) (auto simp:Let_def) |
|
136 |
|
137 text {* We can test this implementation by generating code. *} |
|
138 generate_code ("BinaryTree_TacticStyle_Code.ML") |
|
139 test = "memb 4 (remove (3::nat) (binsert 4 (binsert 3 Tip)))" |
|
140 |
|
141 end |
|