author | wenzelm |
Fri, 08 Apr 2011 14:20:57 +0200 | |
changeset 42287 | d98eb048a2e4 |
parent 39557 | fe5722fce758 |
child 44890 | 22f665a2e91c |
permissions | -rw-r--r-- |
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28819
diff
changeset
|
1 |
(* Title: HOL/Statespace/DistinctTreeProver.thy |
25171 | 2 |
Author: Norbert Schirmer, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*} |
|
6 |
||
7 |
theory DistinctTreeProver |
|
8 |
imports Main |
|
25174 | 9 |
uses ("distinct_tree_prover.ML") |
25171 | 10 |
begin |
11 |
||
12 |
text {* A state space manages a set of (abstract) names and assumes |
|
13 |
that the names are distinct. The names are stored as parameters of a |
|
14 |
locale and distinctness as an assumption. The most common request is |
|
15 |
to proof distinctness of two given names. We maintain the names in a |
|
16 |
balanced binary tree and formulate a predicate that all nodes in the |
|
17 |
tree have distinct names. This setup leads to logarithmic certificates. |
|
18 |
*} |
|
19 |
||
20 |
subsection {* The Binary Tree *} |
|
21 |
||
22 |
datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip |
|
23 |
||
24 |
||
25 |
text {* The boolean flag in the node marks the content of the node as |
|
26 |
deleted, without having to build a new tree. We prefer the boolean |
|
27 |
flag to an option type, so that the ML-layer can still use the node |
|
28 |
content to facilitate binary search in the tree. The ML code keeps the |
|
29 |
nodes sorted using the term order. We do not have to push ordering to |
|
30 |
the HOL level. *} |
|
31 |
||
32 |
subsection {* Distinctness of Nodes *} |
|
33 |
||
34 |
||
38838 | 35 |
primrec set_of :: "'a tree \<Rightarrow> 'a set" |
36 |
where |
|
37 |
"set_of Tip = {}" |
|
38 |
| "set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r" |
|
25171 | 39 |
|
38838 | 40 |
primrec all_distinct :: "'a tree \<Rightarrow> bool" |
41 |
where |
|
42 |
"all_distinct Tip = True" |
|
43 |
| "all_distinct (Node l x d r) = |
|
44 |
((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> |
|
45 |
set_of l \<inter> set_of r = {} \<and> |
|
46 |
all_distinct l \<and> all_distinct r)" |
|
25171 | 47 |
|
48 |
text {* Given a binary tree @{term "t"} for which |
|
49 |
@{const all_distinct} holds, given two different nodes contained in the tree, |
|
50 |
we want to write a ML function that generates a logarithmic |
|
51 |
certificate that the content of the nodes is distinct. We use the |
|
52 |
following lemmas to achieve this. *} |
|
53 |
||
54 |
lemma all_distinct_left: |
|
55 |
"all_distinct (Node l x b r) \<Longrightarrow> all_distinct l" |
|
56 |
by simp |
|
57 |
||
58 |
lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r" |
|
59 |
by simp |
|
60 |
||
61 |
lemma distinct_left: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of l \<rbrakk> \<Longrightarrow> x\<noteq>y" |
|
62 |
by auto |
|
63 |
||
64 |
lemma distinct_right: "\<lbrakk>all_distinct (Node l x False r); y \<in> set_of r \<rbrakk> \<Longrightarrow> x\<noteq>y" |
|
65 |
by auto |
|
66 |
||
67 |
lemma distinct_left_right: "\<lbrakk>all_distinct (Node l z b r); x \<in> set_of l; y \<in> set_of r\<rbrakk> |
|
68 |
\<Longrightarrow> x\<noteq>y" |
|
69 |
by auto |
|
70 |
||
71 |
lemma in_set_root: "x \<in> set_of (Node l x False r)" |
|
72 |
by simp |
|
73 |
||
74 |
lemma in_set_left: "y \<in> set_of l \<Longrightarrow> y \<in> set_of (Node l x False r)" |
|
75 |
by simp |
|
76 |
||
77 |
lemma in_set_right: "y \<in> set_of r \<Longrightarrow> y \<in> set_of (Node l x False r)" |
|
78 |
by simp |
|
79 |
||
80 |
lemma swap_neq: "x \<noteq> y \<Longrightarrow> y \<noteq> x" |
|
81 |
by blast |
|
82 |
||
83 |
lemma neq_to_eq_False: "x\<noteq>y \<Longrightarrow> (x=y)\<equiv>False" |
|
84 |
by simp |
|
85 |
||
86 |
subsection {* Containment of Trees *} |
|
87 |
||
88 |
text {* When deriving a state space from other ones, we create a new |
|
89 |
name tree which contains all the names of the parent state spaces and |
|
90 |
assumme the predicate @{const all_distinct}. We then prove that the new locale |
|
91 |
interprets all parent locales. Hence we have to show that the new |
|
92 |
distinctness assumption on all names implies the distinctness |
|
93 |
assumptions of the parent locales. This proof is implemented in ML. We |
|
94 |
do this efficiently by defining a kind of containment check of trees |
|
95 |
by 'subtraction'. We subtract the parent tree from the new tree. If this |
|
96 |
succeeds we know that @{const all_distinct} of the new tree implies |
|
97 |
@{const all_distinct} of the parent tree. The resulting certificate is |
|
98 |
of the order @{term "n * log(m)"} where @{term "n"} is the size of the |
|
99 |
(smaller) parent tree and @{term "m"} the size of the (bigger) new tree. |
|
100 |
*} |
|
101 |
||
102 |
||
38838 | 103 |
primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option" |
104 |
where |
|
105 |
"delete x Tip = None" |
|
106 |
| "delete x (Node l y d r) = (case delete x l of |
|
107 |
Some l' \<Rightarrow> |
|
108 |
(case delete x r of |
|
109 |
Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r') |
|
110 |
| None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r)) |
|
111 |
| None \<Rightarrow> |
|
112 |
(case (delete x r) of |
|
113 |
Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r') |
|
114 |
| None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r) |
|
115 |
else None))" |
|
25171 | 116 |
|
117 |
||
118 |
lemma delete_Some_set_of: "\<And>t'. delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t" |
|
119 |
proof (induct t) |
|
120 |
case Tip thus ?case by simp |
|
121 |
next |
|
122 |
case (Node l y d r) |
|
25364 | 123 |
have del: "delete x (Node l y d r) = Some t'" by fact |
25171 | 124 |
show ?case |
125 |
proof (cases "delete x l") |
|
126 |
case (Some l') |
|
127 |
note x_l_Some = this |
|
128 |
with Node.hyps |
|
129 |
have l'_l: "set_of l' \<subseteq> set_of l" |
|
130 |
by simp |
|
131 |
show ?thesis |
|
132 |
proof (cases "delete x r") |
|
133 |
case (Some r') |
|
134 |
with Node.hyps |
|
135 |
have "set_of r' \<subseteq> set_of r" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
136 |
by simp |
25171 | 137 |
with l'_l Some x_l_Some del |
138 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
139 |
by (auto split: split_if_asm) |
25171 | 140 |
next |
141 |
case None |
|
142 |
with l'_l Some x_l_Some del |
|
143 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
144 |
by (fastsimp split: split_if_asm) |
25171 | 145 |
qed |
146 |
next |
|
147 |
case None |
|
148 |
note x_l_None = this |
|
149 |
show ?thesis |
|
150 |
proof (cases "delete x r") |
|
151 |
case (Some r') |
|
152 |
with Node.hyps |
|
153 |
have "set_of r' \<subseteq> set_of r" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
154 |
by simp |
25171 | 155 |
with Some x_l_None del |
156 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
157 |
by (fastsimp split: split_if_asm) |
25171 | 158 |
next |
159 |
case None |
|
160 |
with x_l_None del |
|
161 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
162 |
by (fastsimp split: split_if_asm) |
25171 | 163 |
qed |
164 |
qed |
|
165 |
qed |
|
166 |
||
167 |
lemma delete_Some_all_distinct: |
|
168 |
"\<And>t'. \<lbrakk>delete x t = Some t'; all_distinct t\<rbrakk> \<Longrightarrow> all_distinct t'" |
|
169 |
proof (induct t) |
|
170 |
case Tip thus ?case by simp |
|
171 |
next |
|
172 |
case (Node l y d r) |
|
25364 | 173 |
have del: "delete x (Node l y d r) = Some t'" by fact |
174 |
have "all_distinct (Node l y d r)" by fact |
|
25171 | 175 |
then obtain |
176 |
dist_l: "all_distinct l" and |
|
177 |
dist_r: "all_distinct r" and |
|
178 |
d: "d \<or> (y \<notin> set_of l \<and> y \<notin> set_of r)" and |
|
179 |
dist_l_r: "set_of l \<inter> set_of r = {}" |
|
180 |
by auto |
|
181 |
show ?case |
|
182 |
proof (cases "delete x l") |
|
183 |
case (Some l') |
|
184 |
note x_l_Some = this |
|
185 |
from Node.hyps (1) [OF Some dist_l] |
|
186 |
have dist_l': "all_distinct l'" |
|
187 |
by simp |
|
188 |
from delete_Some_set_of [OF x_l_Some] |
|
189 |
have l'_l: "set_of l' \<subseteq> set_of l". |
|
190 |
show ?thesis |
|
191 |
proof (cases "delete x r") |
|
192 |
case (Some r') |
|
193 |
from Node.hyps (2) [OF Some dist_r] |
|
194 |
have dist_r': "all_distinct r'" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
195 |
by simp |
25171 | 196 |
from delete_Some_set_of [OF Some] |
197 |
have "set_of r' \<subseteq> set_of r". |
|
198 |
||
199 |
with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r |
|
200 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
201 |
by fastsimp |
25171 | 202 |
next |
203 |
case None |
|
204 |
with l'_l dist_l' x_l_Some del d dist_l_r dist_r |
|
205 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
206 |
by fastsimp |
25171 | 207 |
qed |
208 |
next |
|
209 |
case None |
|
210 |
note x_l_None = this |
|
211 |
show ?thesis |
|
212 |
proof (cases "delete x r") |
|
213 |
case (Some r') |
|
214 |
with Node.hyps (2) [OF Some dist_r] |
|
215 |
have dist_r': "all_distinct r'" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
216 |
by simp |
25171 | 217 |
from delete_Some_set_of [OF Some] |
218 |
have "set_of r' \<subseteq> set_of r". |
|
219 |
with Some dist_r' x_l_None del dist_l d dist_l_r |
|
220 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
221 |
by fastsimp |
25171 | 222 |
next |
223 |
case None |
|
224 |
with x_l_None del dist_l dist_r d dist_l_r |
|
225 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
226 |
by (fastsimp split: split_if_asm) |
25171 | 227 |
qed |
228 |
qed |
|
229 |
qed |
|
230 |
||
231 |
lemma delete_None_set_of_conv: "delete x t = None = (x \<notin> set_of t)" |
|
232 |
proof (induct t) |
|
233 |
case Tip thus ?case by simp |
|
234 |
next |
|
235 |
case (Node l y d r) |
|
236 |
thus ?case |
|
237 |
by (auto split: option.splits) |
|
238 |
qed |
|
239 |
||
240 |
lemma delete_Some_x_set_of: |
|
241 |
"\<And>t'. delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'" |
|
242 |
proof (induct t) |
|
243 |
case Tip thus ?case by simp |
|
244 |
next |
|
245 |
case (Node l y d r) |
|
25364 | 246 |
have del: "delete x (Node l y d r) = Some t'" by fact |
25171 | 247 |
show ?case |
248 |
proof (cases "delete x l") |
|
249 |
case (Some l') |
|
250 |
note x_l_Some = this |
|
251 |
from Node.hyps (1) [OF Some] |
|
252 |
obtain x_l: "x \<in> set_of l" "x \<notin> set_of l'" |
|
253 |
by simp |
|
254 |
show ?thesis |
|
255 |
proof (cases "delete x r") |
|
256 |
case (Some r') |
|
257 |
from Node.hyps (2) [OF Some] |
|
258 |
obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
259 |
by simp |
25171 | 260 |
from x_r x_l Some x_l_Some del |
261 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
262 |
by (clarsimp split: split_if_asm) |
25171 | 263 |
next |
264 |
case None |
|
265 |
then have "x \<notin> set_of r" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
266 |
by (simp add: delete_None_set_of_conv) |
25171 | 267 |
with x_l None x_l_Some del |
268 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
269 |
by (clarsimp split: split_if_asm) |
25171 | 270 |
qed |
271 |
next |
|
272 |
case None |
|
273 |
note x_l_None = this |
|
274 |
then have x_notin_l: "x \<notin> set_of l" |
|
275 |
by (simp add: delete_None_set_of_conv) |
|
276 |
show ?thesis |
|
277 |
proof (cases "delete x r") |
|
278 |
case (Some r') |
|
279 |
from Node.hyps (2) [OF Some] |
|
280 |
obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
281 |
by simp |
25171 | 282 |
from x_r x_notin_l Some x_l_None del |
283 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
284 |
by (clarsimp split: split_if_asm) |
25171 | 285 |
next |
286 |
case None |
|
287 |
then have "x \<notin> set_of r" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
288 |
by (simp add: delete_None_set_of_conv) |
25171 | 289 |
with None x_l_None x_notin_l del |
290 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
291 |
by (clarsimp split: split_if_asm) |
25171 | 292 |
qed |
293 |
qed |
|
294 |
qed |
|
295 |
||
296 |
||
38838 | 297 |
primrec subtract :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option" |
298 |
where |
|
299 |
"subtract Tip t = Some t" |
|
300 |
| "subtract (Node l x b r) t = |
|
301 |
(case delete x t of |
|
302 |
Some t' \<Rightarrow> (case subtract l t' of |
|
303 |
Some t'' \<Rightarrow> subtract r t'' |
|
304 |
| None \<Rightarrow> None) |
|
305 |
| None \<Rightarrow> None)" |
|
25171 | 306 |
|
307 |
lemma subtract_Some_set_of_res: |
|
308 |
"\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2" |
|
309 |
proof (induct t\<^isub>1) |
|
310 |
case Tip thus ?case by simp |
|
311 |
next |
|
312 |
case (Node l x b r) |
|
25364 | 313 |
have sub: "subtract (Node l x b r) t\<^isub>2 = Some t" by fact |
25171 | 314 |
show ?case |
315 |
proof (cases "delete x t\<^isub>2") |
|
316 |
case (Some t\<^isub>2') |
|
317 |
note del_x_Some = this |
|
318 |
from delete_Some_set_of [OF Some] |
|
319 |
have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" . |
|
320 |
show ?thesis |
|
321 |
proof (cases "subtract l t\<^isub>2'") |
|
322 |
case (Some t\<^isub>2'') |
|
323 |
note sub_l_Some = this |
|
324 |
from Node.hyps (1) [OF Some] |
|
325 |
have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" . |
|
326 |
show ?thesis |
|
327 |
proof (cases "subtract r t\<^isub>2''") |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
328 |
case (Some t\<^isub>2''') |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
329 |
from Node.hyps (2) [OF Some ] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
330 |
have "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''" . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
331 |
with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
332 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
333 |
by simp |
25171 | 334 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
335 |
case None |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
336 |
with del_x_Some sub_l_Some sub |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
337 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
338 |
by simp |
25171 | 339 |
qed |
340 |
next |
|
341 |
case None |
|
342 |
with del_x_Some sub |
|
343 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
344 |
by simp |
25171 | 345 |
qed |
346 |
next |
|
347 |
case None |
|
348 |
with sub show ?thesis by simp |
|
349 |
qed |
|
350 |
qed |
|
351 |
||
352 |
lemma subtract_Some_set_of: |
|
353 |
"\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<subseteq> set_of t\<^isub>2" |
|
354 |
proof (induct t\<^isub>1) |
|
355 |
case Tip thus ?case by simp |
|
356 |
next |
|
357 |
case (Node l x d r) |
|
25364 | 358 |
have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact |
25171 | 359 |
show ?case |
360 |
proof (cases "delete x t\<^isub>2") |
|
361 |
case (Some t\<^isub>2') |
|
362 |
note del_x_Some = this |
|
363 |
from delete_Some_set_of [OF Some] |
|
364 |
have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" . |
|
365 |
from delete_None_set_of_conv [of x t\<^isub>2] Some |
|
366 |
have x_t2: "x \<in> set_of t\<^isub>2" |
|
367 |
by simp |
|
368 |
show ?thesis |
|
369 |
proof (cases "subtract l t\<^isub>2'") |
|
370 |
case (Some t\<^isub>2'') |
|
371 |
note sub_l_Some = this |
|
372 |
from Node.hyps (1) [OF Some] |
|
373 |
have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" . |
|
374 |
from subtract_Some_set_of_res [OF Some] |
|
375 |
have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" . |
|
376 |
show ?thesis |
|
377 |
proof (cases "subtract r t\<^isub>2''") |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
378 |
case (Some t\<^isub>2''') |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
379 |
from Node.hyps (2) [OF Some ] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
380 |
have r_t\<^isub>2'': "set_of r \<subseteq> set_of t\<^isub>2''" . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
381 |
from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
382 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
383 |
by auto |
25171 | 384 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
385 |
case None |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
386 |
with del_x_Some sub_l_Some sub |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
387 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
388 |
by simp |
25171 | 389 |
qed |
390 |
next |
|
391 |
case None |
|
392 |
with del_x_Some sub |
|
393 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
394 |
by simp |
25171 | 395 |
qed |
396 |
next |
|
397 |
case None |
|
398 |
with sub show ?thesis by simp |
|
399 |
qed |
|
400 |
qed |
|
401 |
||
402 |
lemma subtract_Some_all_distinct_res: |
|
403 |
"\<And>t\<^isub>2 t. \<lbrakk>subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\<rbrakk> \<Longrightarrow> all_distinct t" |
|
404 |
proof (induct t\<^isub>1) |
|
405 |
case Tip thus ?case by simp |
|
406 |
next |
|
407 |
case (Node l x d r) |
|
25364 | 408 |
have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact |
409 |
have dist_t2: "all_distinct t\<^isub>2" by fact |
|
25171 | 410 |
show ?case |
411 |
proof (cases "delete x t\<^isub>2") |
|
412 |
case (Some t\<^isub>2') |
|
413 |
note del_x_Some = this |
|
414 |
from delete_Some_all_distinct [OF Some dist_t2] |
|
415 |
have dist_t2': "all_distinct t\<^isub>2'" . |
|
416 |
show ?thesis |
|
417 |
proof (cases "subtract l t\<^isub>2'") |
|
418 |
case (Some t\<^isub>2'') |
|
419 |
note sub_l_Some = this |
|
420 |
from Node.hyps (1) [OF Some dist_t2'] |
|
421 |
have dist_t2'': "all_distinct t\<^isub>2''" . |
|
422 |
show ?thesis |
|
423 |
proof (cases "subtract r t\<^isub>2''") |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
424 |
case (Some t\<^isub>2''') |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
425 |
from Node.hyps (2) [OF Some dist_t2''] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
426 |
have dist_t2''': "all_distinct t\<^isub>2'''" . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
427 |
from Some sub_l_Some del_x_Some sub |
25171 | 428 |
dist_t2''' |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
429 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
430 |
by simp |
25171 | 431 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
432 |
case None |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
433 |
with del_x_Some sub_l_Some sub |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
434 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
435 |
by simp |
25171 | 436 |
qed |
437 |
next |
|
438 |
case None |
|
439 |
with del_x_Some sub |
|
440 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
441 |
by simp |
25171 | 442 |
qed |
443 |
next |
|
444 |
case None |
|
445 |
with sub show ?thesis by simp |
|
446 |
qed |
|
447 |
qed |
|
448 |
||
449 |
||
450 |
lemma subtract_Some_dist_res: |
|
451 |
"\<And>t\<^isub>2 t. subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<inter> set_of t = {}" |
|
452 |
proof (induct t\<^isub>1) |
|
453 |
case Tip thus ?case by simp |
|
454 |
next |
|
455 |
case (Node l x d r) |
|
29291 | 456 |
have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact |
25171 | 457 |
show ?case |
458 |
proof (cases "delete x t\<^isub>2") |
|
459 |
case (Some t\<^isub>2') |
|
460 |
note del_x_Some = this |
|
461 |
from delete_Some_x_set_of [OF Some] |
|
462 |
obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'" |
|
463 |
by simp |
|
464 |
from delete_Some_set_of [OF Some] |
|
465 |
have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" . |
|
466 |
show ?thesis |
|
467 |
proof (cases "subtract l t\<^isub>2'") |
|
468 |
case (Some t\<^isub>2'') |
|
469 |
note sub_l_Some = this |
|
470 |
from Node.hyps (1) [OF Some ] |
|
471 |
have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}". |
|
472 |
from subtract_Some_set_of_res [OF Some] |
|
473 |
have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" . |
|
474 |
show ?thesis |
|
475 |
proof (cases "subtract r t\<^isub>2''") |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
476 |
case (Some t\<^isub>2''') |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
477 |
from Node.hyps (2) [OF Some] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
478 |
have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}" . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
479 |
from subtract_Some_set_of_res [OF Some] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
480 |
have t2'''_t2'': "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''". |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
481 |
|
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
482 |
from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2''' |
25171 | 483 |
t2''_t2' t2'_t2 x_not_t2' |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
484 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
485 |
by auto |
25171 | 486 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
487 |
case None |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
488 |
with del_x_Some sub_l_Some sub |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
489 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
490 |
by simp |
25171 | 491 |
qed |
492 |
next |
|
493 |
case None |
|
494 |
with del_x_Some sub |
|
495 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
496 |
by simp |
25171 | 497 |
qed |
498 |
next |
|
499 |
case None |
|
500 |
with sub show ?thesis by simp |
|
501 |
qed |
|
502 |
qed |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
503 |
|
25171 | 504 |
lemma subtract_Some_all_distinct: |
505 |
"\<And>t\<^isub>2 t. \<lbrakk>subtract t\<^isub>1 t\<^isub>2 = Some t; all_distinct t\<^isub>2\<rbrakk> \<Longrightarrow> all_distinct t\<^isub>1" |
|
506 |
proof (induct t\<^isub>1) |
|
507 |
case Tip thus ?case by simp |
|
508 |
next |
|
509 |
case (Node l x d r) |
|
25364 | 510 |
have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact |
511 |
have dist_t2: "all_distinct t\<^isub>2" by fact |
|
25171 | 512 |
show ?case |
513 |
proof (cases "delete x t\<^isub>2") |
|
514 |
case (Some t\<^isub>2') |
|
515 |
note del_x_Some = this |
|
516 |
from delete_Some_all_distinct [OF Some dist_t2 ] |
|
517 |
have dist_t2': "all_distinct t\<^isub>2'" . |
|
518 |
from delete_Some_set_of [OF Some] |
|
519 |
have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" . |
|
520 |
from delete_Some_x_set_of [OF Some] |
|
521 |
obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'" |
|
522 |
by simp |
|
523 |
||
524 |
show ?thesis |
|
525 |
proof (cases "subtract l t\<^isub>2'") |
|
526 |
case (Some t\<^isub>2'') |
|
527 |
note sub_l_Some = this |
|
528 |
from Node.hyps (1) [OF Some dist_t2' ] |
|
529 |
have dist_l: "all_distinct l" . |
|
530 |
from subtract_Some_all_distinct_res [OF Some dist_t2'] |
|
531 |
have dist_t2'': "all_distinct t\<^isub>2''" . |
|
532 |
from subtract_Some_set_of [OF Some] |
|
533 |
have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" . |
|
534 |
from subtract_Some_set_of_res [OF Some] |
|
535 |
have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" . |
|
536 |
from subtract_Some_dist_res [OF Some] |
|
537 |
have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}". |
|
538 |
show ?thesis |
|
539 |
proof (cases "subtract r t\<^isub>2''") |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
540 |
case (Some t\<^isub>2''') |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
541 |
from Node.hyps (2) [OF Some dist_t2''] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
542 |
have dist_r: "all_distinct r" . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
543 |
from subtract_Some_set_of [OF Some] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
544 |
have r_t2'': "set_of r \<subseteq> set_of t\<^isub>2''" . |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
545 |
from subtract_Some_dist_res [OF Some] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
546 |
have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}". |
25171 | 547 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
548 |
from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2' |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
549 |
t2''_t2' dist_l_t2'' dist_r_t2''' |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
550 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
551 |
by auto |
25171 | 552 |
next |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
553 |
case None |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
554 |
with del_x_Some sub_l_Some sub |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
555 |
show ?thesis |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
556 |
by simp |
25171 | 557 |
qed |
558 |
next |
|
559 |
case None |
|
560 |
with del_x_Some sub |
|
561 |
show ?thesis |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32740
diff
changeset
|
562 |
by simp |
25171 | 563 |
qed |
564 |
next |
|
565 |
case None |
|
566 |
with sub show ?thesis by simp |
|
567 |
qed |
|
568 |
qed |
|
569 |
||
570 |
||
571 |
lemma delete_left: |
|
572 |
assumes dist: "all_distinct (Node l y d r)" |
|
573 |
assumes del_l: "delete x l = Some l'" |
|
574 |
shows "delete x (Node l y d r) = Some (Node l' y d r)" |
|
575 |
proof - |
|
576 |
from delete_Some_x_set_of [OF del_l] |
|
577 |
obtain "x \<in> set_of l" |
|
578 |
by simp |
|
579 |
moreover with dist |
|
580 |
have "delete x r = None" |
|
581 |
by (cases "delete x r") (auto dest:delete_Some_x_set_of) |
|
582 |
||
583 |
ultimately |
|
584 |
show ?thesis |
|
585 |
using del_l dist |
|
586 |
by (auto split: option.splits) |
|
587 |
qed |
|
588 |
||
589 |
lemma delete_right: |
|
590 |
assumes dist: "all_distinct (Node l y d r)" |
|
591 |
assumes del_r: "delete x r = Some r'" |
|
592 |
shows "delete x (Node l y d r) = Some (Node l y d r')" |
|
593 |
proof - |
|
594 |
from delete_Some_x_set_of [OF del_r] |
|
595 |
obtain "x \<in> set_of r" |
|
596 |
by simp |
|
597 |
moreover with dist |
|
598 |
have "delete x l = None" |
|
599 |
by (cases "delete x l") (auto dest:delete_Some_x_set_of) |
|
600 |
||
601 |
ultimately |
|
602 |
show ?thesis |
|
603 |
using del_r dist |
|
604 |
by (auto split: option.splits) |
|
605 |
qed |
|
606 |
||
607 |
lemma delete_root: |
|
608 |
assumes dist: "all_distinct (Node l x False r)" |
|
609 |
shows "delete x (Node l x False r) = Some (Node l x True r)" |
|
610 |
proof - |
|
611 |
from dist have "delete x r = None" |
|
612 |
by (cases "delete x r") (auto dest:delete_Some_x_set_of) |
|
613 |
moreover |
|
614 |
from dist have "delete x l = None" |
|
615 |
by (cases "delete x l") (auto dest:delete_Some_x_set_of) |
|
616 |
ultimately show ?thesis |
|
617 |
using dist |
|
618 |
by (auto split: option.splits) |
|
619 |
qed |
|
620 |
||
621 |
lemma subtract_Node: |
|
622 |
assumes del: "delete x t = Some t'" |
|
623 |
assumes sub_l: "subtract l t' = Some t''" |
|
624 |
assumes sub_r: "subtract r t'' = Some t'''" |
|
625 |
shows "subtract (Node l x False r) t = Some t'''" |
|
626 |
using del sub_l sub_r |
|
627 |
by simp |
|
628 |
||
629 |
lemma subtract_Tip: "subtract Tip t = Some t" |
|
630 |
by simp |
|
631 |
||
632 |
text {* Now we have all the theorems in place that are needed for the |
|
633 |
certificate generating ML functions. *} |
|
634 |
||
25174 | 635 |
use "distinct_tree_prover.ML" |
25171 | 636 |
|
637 |
(* Uncomment for profiling or debugging *) |
|
638 |
(* |
|
639 |
ML {* |
|
640 |
(* |
|
641 |
val nums = (0 upto 10000); |
|
642 |
val nums' = (200 upto 3000); |
|
643 |
*) |
|
644 |
val nums = (0 upto 10000); |
|
645 |
val nums' = (0 upto 3000); |
|
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
39557
diff
changeset
|
646 |
val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums |
25171 | 647 |
|
35408 | 648 |
val consts = sort Term_Ord.fast_term_ord |
25171 | 649 |
(map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums) |
35408 | 650 |
val consts' = sort Term_Ord.fast_term_ord |
25171 | 651 |
(map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums') |
652 |
||
653 |
val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts |
|
654 |
||
655 |
||
656 |
val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts' |
|
657 |
||
658 |
||
659 |
val dist = |
|
660 |
HOLogic.Trueprop$ |
|
661 |
(Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t) |
|
662 |
||
663 |
val dist' = |
|
664 |
HOLogic.Trueprop$ |
|
665 |
(Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t') |
|
666 |
||
32740 | 667 |
val da = Unsynchronized.ref refl; |
25171 | 668 |
|
669 |
*} |
|
670 |
||
671 |
setup {* |
|
672 |
Theory.add_consts_i const_decls |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38838
diff
changeset
|
673 |
#> (fn thy => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy |
25171 | 674 |
in (da := thm; thy') end) |
675 |
*} |
|
676 |
||
677 |
||
678 |
ML {* |
|
32010 | 679 |
val ct' = cterm_of @{theory} t'; |
25171 | 680 |
*} |
681 |
||
682 |
ML {* |
|
683 |
timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);())) |
|
684 |
*} |
|
685 |
||
686 |
(* 590 s *) |
|
687 |
||
688 |
ML {* |
|
689 |
||
690 |
||
691 |
val p1 = |
|
692 |
the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t) |
|
693 |
val p2 = |
|
694 |
the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t) |
|
695 |
*} |
|
696 |
||
697 |
||
698 |
ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da ) |
|
699 |
p1 |
|
700 |
p2)*} |
|
701 |
||
702 |
||
703 |
ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *} |
|
704 |
||
705 |
||
706 |
||
707 |
||
708 |
ML {* |
|
32010 | 709 |
val cdist' = cterm_of @{theory} dist'; |
25171 | 710 |
DistinctTreeProver.distinct_implProver (!da) cdist'; |
711 |
*} |
|
712 |
||
713 |
*) |
|
714 |
||
715 |
end |