author | wenzelm |
Sat, 14 Nov 2009 18:45:24 +0100 | |
changeset 33687 | 3222fa052846 |
parent 32960 | 69916a850301 |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32235
diff
changeset
|
1 |
(* Title: HOL/UNITY/ListOrder.thy |
6708 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1998 University of Cambridge |
|
4 |
||
13798 | 5 |
Lists are partially ordered by Charpentier's Generalized Prefix Relation |
6 |
(xs,ys) : genPrefix(r) |
|
7 |
if ys = xs' @ zs where length xs = length xs' |
|
8 |
and corresponding elements of xs, xs' are pairwise related by r |
|
9 |
||
10 |
Also overloads <= and < for lists! |
|
6708 | 11 |
*) |
12 |
||
13798 | 13 |
header {*The Prefix Ordering on Lists*} |
14 |
||
27682 | 15 |
theory ListOrder |
16 |
imports Main |
|
17 |
begin |
|
13798 | 18 |
|
23767 | 19 |
inductive_set |
13798 | 20 |
genPrefix :: "('a * 'a)set => ('a list * 'a list)set" |
23767 | 21 |
for r :: "('a * 'a)set" |
22 |
where |
|
13798 | 23 |
Nil: "([],[]) : genPrefix(r)" |
24 |
||
23767 | 25 |
| prepend: "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32235
diff
changeset
|
26 |
(x#xs, y#ys) : genPrefix(r)" |
13798 | 27 |
|
23767 | 28 |
| append: "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" |
13798 | 29 |
|
27682 | 30 |
instantiation list :: (type) ord |
31 |
begin |
|
13798 | 32 |
|
27682 | 33 |
definition |
34 |
prefix_def: "xs <= zs \<longleftrightarrow> (xs, zs) : genPrefix Id" |
|
13798 | 35 |
|
27682 | 36 |
definition |
37 |
strict_prefix_def: "xs < zs \<longleftrightarrow> xs \<le> zs \<and> \<not> zs \<le> (xs :: 'a list)" |
|
38 |
||
39 |
instance .. |
|
13798 | 40 |
|
41 |
(*Constants for the <= and >= relations, used below in translations*) |
|
27682 | 42 |
|
43 |
end |
|
44 |
||
13798 | 45 |
constdefs |
46 |
Le :: "(nat*nat) set" |
|
47 |
"Le == {(x,y). x <= y}" |
|
48 |
||
49 |
Ge :: "(nat*nat) set" |
|
50 |
"Ge == {(x,y). y <= x}" |
|
51 |
||
23767 | 52 |
abbreviation |
53 |
pfixLe :: "[nat list, nat list] => bool" (infixl "pfixLe" 50) where |
|
54 |
"xs pfixLe ys == (xs,ys) : genPrefix Le" |
|
13798 | 55 |
|
23767 | 56 |
abbreviation |
57 |
pfixGe :: "[nat list, nat list] => bool" (infixl "pfixGe" 50) where |
|
58 |
"xs pfixGe ys == (xs,ys) : genPrefix Ge" |
|
13798 | 59 |
|
60 |
||
61 |
subsection{*preliminary lemmas*} |
|
62 |
||
63 |
lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r" |
|
64 |
by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto) |
|
65 |
||
66 |
lemma genPrefix_length_le: "(xs,ys) : genPrefix r ==> length xs <= length ys" |
|
67 |
by (erule genPrefix.induct, auto) |
|
68 |
||
69 |
lemma cdlemma: |
|
70 |
"[| (xs', ys'): genPrefix r |] |
|
71 |
==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))" |
|
72 |
apply (erule genPrefix.induct, blast, blast) |
|
73 |
apply (force intro: genPrefix.append) |
|
74 |
done |
|
75 |
||
76 |
(*As usual converting it to an elimination rule is tiresome*) |
|
77 |
lemma cons_genPrefixE [elim!]: |
|
78 |
"[| (x#xs, zs): genPrefix r; |
|
79 |
!!y ys. [| zs = y#ys; (x,y) : r; (xs, ys) : genPrefix r |] ==> P |
|
80 |
|] ==> P" |
|
81 |
by (drule cdlemma, simp, blast) |
|
82 |
||
83 |
lemma Cons_genPrefix_Cons [iff]: |
|
84 |
"((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)" |
|
85 |
by (blast intro: genPrefix.prepend) |
|
86 |
||
87 |
||
88 |
subsection{*genPrefix is a partial order*} |
|
89 |
||
30198 | 90 |
lemma refl_genPrefix: "refl r ==> refl (genPrefix r)" |
91 |
apply (unfold refl_on_def, auto) |
|
13798 | 92 |
apply (induct_tac "x") |
93 |
prefer 2 apply (blast intro: genPrefix.prepend) |
|
94 |
apply (blast intro: genPrefix.Nil) |
|
95 |
done |
|
96 |
||
30198 | 97 |
lemma genPrefix_refl [simp]: "refl r ==> (l,l) : genPrefix r" |
98 |
by (erule refl_onD [OF refl_genPrefix UNIV_I]) |
|
13798 | 99 |
|
100 |
lemma genPrefix_mono: "r<=s ==> genPrefix r <= genPrefix s" |
|
101 |
apply clarify |
|
102 |
apply (erule genPrefix.induct) |
|
103 |
apply (auto intro: genPrefix.append) |
|
104 |
done |
|
105 |
||
106 |
||
107 |
(** Transitivity **) |
|
108 |
||
109 |
(*A lemma for proving genPrefix_trans_O*) |
|
110 |
lemma append_genPrefix [rule_format]: |
|
111 |
"ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r" |
|
112 |
by (induct_tac "xs", auto) |
|
113 |
||
114 |
(*Lemma proving transitivity and more*) |
|
115 |
lemma genPrefix_trans_O [rule_format]: |
|
116 |
"(x, y) : genPrefix r |
|
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
30198
diff
changeset
|
117 |
==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (r O s)" |
13798 | 118 |
apply (erule genPrefix.induct) |
119 |
prefer 3 apply (blast dest: append_genPrefix) |
|
120 |
prefer 2 apply (blast intro: genPrefix.prepend, blast) |
|
121 |
done |
|
122 |
||
123 |
lemma genPrefix_trans [rule_format]: |
|
124 |
"[| (x,y) : genPrefix r; (y,z) : genPrefix r; trans r |] |
|
125 |
==> (x,z) : genPrefix r" |
|
126 |
apply (rule trans_O_subset [THEN genPrefix_mono, THEN subsetD]) |
|
127 |
apply assumption |
|
128 |
apply (blast intro: genPrefix_trans_O) |
|
129 |
done |
|
130 |
||
131 |
lemma prefix_genPrefix_trans [rule_format]: |
|
132 |
"[| x<=y; (y,z) : genPrefix r |] ==> (x, z) : genPrefix r" |
|
133 |
apply (unfold prefix_def) |
|
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
30198
diff
changeset
|
134 |
apply (drule genPrefix_trans_O, assumption) |
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
30198
diff
changeset
|
135 |
apply simp |
13798 | 136 |
done |
137 |
||
138 |
lemma genPrefix_prefix_trans [rule_format]: |
|
139 |
"[| (x,y) : genPrefix r; y<=z |] ==> (x,z) : genPrefix r" |
|
140 |
apply (unfold prefix_def) |
|
32235
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
30198
diff
changeset
|
141 |
apply (drule genPrefix_trans_O, assumption) |
8f9b8d14fc9f
"more standard" argument order of relation composition (op O)
krauss
parents:
30198
diff
changeset
|
142 |
apply simp |
13798 | 143 |
done |
144 |
||
145 |
lemma trans_genPrefix: "trans r ==> trans (genPrefix r)" |
|
146 |
by (blast intro: transI genPrefix_trans) |
|
147 |
||
148 |
||
149 |
(** Antisymmetry **) |
|
150 |
||
151 |
lemma genPrefix_antisym [rule_format]: |
|
152 |
"[| (xs,ys) : genPrefix r; antisym r |] |
|
153 |
==> (ys,xs) : genPrefix r --> xs = ys" |
|
154 |
apply (erule genPrefix.induct) |
|
155 |
txt{*Base case*} |
|
156 |
apply blast |
|
157 |
txt{*prepend case*} |
|
158 |
apply (simp add: antisym_def) |
|
159 |
txt{*append case is the hardest*} |
|
160 |
apply clarify |
|
161 |
apply (subgoal_tac "length zs = 0", force) |
|
162 |
apply (drule genPrefix_length_le)+ |
|
163 |
apply (simp del: length_0_conv) |
|
164 |
done |
|
165 |
||
166 |
lemma antisym_genPrefix: "antisym r ==> antisym (genPrefix r)" |
|
167 |
by (blast intro: antisymI genPrefix_antisym) |
|
168 |
||
169 |
||
170 |
subsection{*recursion equations*} |
|
171 |
||
172 |
lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])" |
|
173 |
apply (induct_tac "xs") |
|
174 |
prefer 2 apply blast |
|
175 |
apply simp |
|
176 |
done |
|
177 |
||
178 |
lemma same_genPrefix_genPrefix [simp]: |
|
30198 | 179 |
"refl r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)" |
180 |
apply (unfold refl_on_def) |
|
13798 | 181 |
apply (induct_tac "xs") |
182 |
apply (simp_all (no_asm_simp)) |
|
183 |
done |
|
184 |
||
185 |
lemma genPrefix_Cons: |
|
186 |
"((xs, y#ys) : genPrefix r) = |
|
187 |
(xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))" |
|
188 |
by (case_tac "xs", auto) |
|
189 |
||
190 |
lemma genPrefix_take_append: |
|
30198 | 191 |
"[| refl r; (xs,ys) : genPrefix r |] |
13798 | 192 |
==> (xs@zs, take (length xs) ys @ zs) : genPrefix r" |
193 |
apply (erule genPrefix.induct) |
|
194 |
apply (frule_tac [3] genPrefix_length_le) |
|
195 |
apply (simp_all (no_asm_simp) add: diff_is_0_eq [THEN iffD2]) |
|
196 |
done |
|
197 |
||
198 |
lemma genPrefix_append_both: |
|
30198 | 199 |
"[| refl r; (xs,ys) : genPrefix r; length xs = length ys |] |
13798 | 200 |
==> (xs@zs, ys @ zs) : genPrefix r" |
201 |
apply (drule genPrefix_take_append, assumption) |
|
202 |
apply (simp add: take_all) |
|
203 |
done |
|
204 |
||
205 |
||
206 |
(*NOT suitable for rewriting since [y] has the form y#ys*) |
|
207 |
lemma append_cons_eq: "xs @ y # ys = (xs @ [y]) @ ys" |
|
208 |
by auto |
|
209 |
||
210 |
lemma aolemma: |
|
30198 | 211 |
"[| (xs,ys) : genPrefix r; refl r |] |
13798 | 212 |
==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r" |
213 |
apply (erule genPrefix.induct) |
|
214 |
apply blast |
|
215 |
apply simp |
|
216 |
txt{*Append case is hardest*} |
|
217 |
apply simp |
|
218 |
apply (frule genPrefix_length_le [THEN le_imp_less_or_eq]) |
|
219 |
apply (erule disjE) |
|
220 |
apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append) |
|
221 |
apply (blast intro: genPrefix.append, auto) |
|
15481 | 222 |
apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append) |
13798 | 223 |
done |
224 |
||
225 |
lemma append_one_genPrefix: |
|
30198 | 226 |
"[| (xs,ys) : genPrefix r; length xs < length ys; refl r |] |
13798 | 227 |
==> (xs @ [ys ! length xs], ys) : genPrefix r" |
228 |
by (blast intro: aolemma [THEN mp]) |
|
229 |
||
230 |
||
231 |
(** Proving the equivalence with Charpentier's definition **) |
|
232 |
||
233 |
lemma genPrefix_imp_nth [rule_format]: |
|
234 |
"ALL i ys. i < length xs |
|
235 |
--> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r" |
|
236 |
apply (induct_tac "xs", auto) |
|
237 |
apply (case_tac "i", auto) |
|
238 |
done |
|
239 |
||
240 |
lemma nth_imp_genPrefix [rule_format]: |
|
241 |
"ALL ys. length xs <= length ys |
|
242 |
--> (ALL i. i < length xs --> (xs ! i, ys ! i) : r) |
|
243 |
--> (xs, ys) : genPrefix r" |
|
244 |
apply (induct_tac "xs") |
|
245 |
apply (simp_all (no_asm_simp) add: less_Suc_eq_0_disj all_conj_distrib) |
|
246 |
apply clarify |
|
247 |
apply (case_tac "ys") |
|
248 |
apply (force+) |
|
249 |
done |
|
250 |
||
251 |
lemma genPrefix_iff_nth: |
|
252 |
"((xs,ys) : genPrefix r) = |
|
253 |
(length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))" |
|
254 |
apply (blast intro: genPrefix_length_le genPrefix_imp_nth nth_imp_genPrefix) |
|
255 |
done |
|
256 |
||
257 |
||
258 |
subsection{*The type of lists is partially ordered*} |
|
259 |
||
30198 | 260 |
declare refl_Id [iff] |
13798 | 261 |
antisym_Id [iff] |
262 |
trans_Id [iff] |
|
263 |
||
264 |
lemma prefix_refl [iff]: "xs <= (xs::'a list)" |
|
265 |
by (simp add: prefix_def) |
|
266 |
||
267 |
lemma prefix_trans: "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs" |
|
268 |
apply (unfold prefix_def) |
|
269 |
apply (blast intro: genPrefix_trans) |
|
270 |
done |
|
271 |
||
272 |
lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys" |
|
273 |
apply (unfold prefix_def) |
|
274 |
apply (blast intro: genPrefix_antisym) |
|
275 |
done |
|
276 |
||
27682 | 277 |
lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \<not> zs \<le> xs)" |
13798 | 278 |
by (unfold strict_prefix_def, auto) |
6708 | 279 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
6810
diff
changeset
|
280 |
instance list :: (type) order |
13798 | 281 |
by (intro_classes, |
282 |
(assumption | rule prefix_refl prefix_trans prefix_antisym |
|
27682 | 283 |
prefix_less_le_not_le)+) |
13798 | 284 |
|
285 |
(*Monotonicity of "set" operator WRT prefix*) |
|
286 |
lemma set_mono: "xs <= ys ==> set xs <= set ys" |
|
287 |
apply (unfold prefix_def) |
|
288 |
apply (erule genPrefix.induct, auto) |
|
289 |
done |
|
290 |
||
291 |
||
292 |
(** recursion equations **) |
|
293 |
||
294 |
lemma Nil_prefix [iff]: "[] <= xs" |
|
295 |
apply (unfold prefix_def) |
|
296 |
apply (simp add: Nil_genPrefix) |
|
297 |
done |
|
298 |
||
299 |
lemma prefix_Nil [simp]: "(xs <= []) = (xs = [])" |
|
300 |
apply (unfold prefix_def) |
|
301 |
apply (simp add: genPrefix_Nil) |
|
302 |
done |
|
303 |
||
304 |
lemma Cons_prefix_Cons [simp]: "(x#xs <= y#ys) = (x=y & xs<=ys)" |
|
305 |
by (simp add: prefix_def) |
|
306 |
||
307 |
lemma same_prefix_prefix [simp]: "(xs@ys <= xs@zs) = (ys <= zs)" |
|
308 |
by (simp add: prefix_def) |
|
309 |
||
310 |
lemma append_prefix [iff]: "(xs@ys <= xs) = (ys <= [])" |
|
311 |
by (insert same_prefix_prefix [of xs ys "[]"], simp) |
|
312 |
||
313 |
lemma prefix_appendI [simp]: "xs <= ys ==> xs <= ys@zs" |
|
314 |
apply (unfold prefix_def) |
|
315 |
apply (erule genPrefix.append) |
|
316 |
done |
|
317 |
||
318 |
lemma prefix_Cons: |
|
319 |
"(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))" |
|
320 |
by (simp add: prefix_def genPrefix_Cons) |
|
321 |
||
322 |
lemma append_one_prefix: |
|
323 |
"[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys" |
|
324 |
apply (unfold prefix_def) |
|
325 |
apply (simp add: append_one_genPrefix) |
|
326 |
done |
|
327 |
||
328 |
lemma prefix_length_le: "xs <= ys ==> length xs <= length ys" |
|
329 |
apply (unfold prefix_def) |
|
330 |
apply (erule genPrefix_length_le) |
|
331 |
done |
|
332 |
||
333 |
lemma splemma: "xs<=ys ==> xs~=ys --> length xs < length ys" |
|
334 |
apply (unfold prefix_def) |
|
335 |
apply (erule genPrefix.induct, auto) |
|
336 |
done |
|
337 |
||
338 |
lemma strict_prefix_length_less: "xs < ys ==> length xs < length ys" |
|
339 |
apply (unfold strict_prefix_def) |
|
340 |
apply (blast intro: splemma [THEN mp]) |
|
341 |
done |
|
342 |
||
343 |
lemma mono_length: "mono length" |
|
344 |
by (blast intro: monoI prefix_length_le) |
|
345 |
||
346 |
(*Equivalence to the definition used in Lex/Prefix.thy*) |
|
347 |
lemma prefix_iff: "(xs <= zs) = (EX ys. zs = xs@ys)" |
|
348 |
apply (unfold prefix_def) |
|
349 |
apply (auto simp add: genPrefix_iff_nth nth_append) |
|
350 |
apply (rule_tac x = "drop (length xs) zs" in exI) |
|
351 |
apply (rule nth_equalityI) |
|
352 |
apply (simp_all (no_asm_simp) add: nth_append) |
|
353 |
done |
|
354 |
||
355 |
lemma prefix_snoc [simp]: "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)" |
|
356 |
apply (simp add: prefix_iff) |
|
357 |
apply (rule iffI) |
|
358 |
apply (erule exE) |
|
359 |
apply (rename_tac "zs") |
|
360 |
apply (rule_tac xs = zs in rev_exhaust) |
|
361 |
apply simp |
|
362 |
apply clarify |
|
363 |
apply (simp del: append_assoc add: append_assoc [symmetric], force) |
|
364 |
done |
|
365 |
||
366 |
lemma prefix_append_iff: |
|
367 |
"(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))" |
|
368 |
apply (rule_tac xs = zs in rev_induct) |
|
369 |
apply force |
|
370 |
apply (simp del: append_assoc add: append_assoc [symmetric], force) |
|
371 |
done |
|
372 |
||
373 |
(*Although the prefix ordering is not linear, the prefixes of a list |
|
374 |
are linearly ordered.*) |
|
375 |
lemma common_prefix_linear [rule_format]: |
|
376 |
"!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs" |
|
377 |
by (rule_tac xs = zs in rev_induct, auto) |
|
378 |
||
379 |
||
380 |
subsection{*pfixLe, pfixGe: properties inherited from the translations*} |
|
381 |
||
382 |
(** pfixLe **) |
|
383 |
||
30198 | 384 |
lemma refl_Le [iff]: "refl Le" |
385 |
by (unfold refl_on_def Le_def, auto) |
|
13798 | 386 |
|
387 |
lemma antisym_Le [iff]: "antisym Le" |
|
388 |
by (unfold antisym_def Le_def, auto) |
|
389 |
||
390 |
lemma trans_Le [iff]: "trans Le" |
|
391 |
by (unfold trans_def Le_def, auto) |
|
392 |
||
393 |
lemma pfixLe_refl [iff]: "x pfixLe x" |
|
394 |
by simp |
|
395 |
||
396 |
lemma pfixLe_trans: "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z" |
|
397 |
by (blast intro: genPrefix_trans) |
|
398 |
||
399 |
lemma pfixLe_antisym: "[| x pfixLe y; y pfixLe x |] ==> x = y" |
|
400 |
by (blast intro: genPrefix_antisym) |
|
401 |
||
402 |
lemma prefix_imp_pfixLe: "xs<=ys ==> xs pfixLe ys" |
|
403 |
apply (unfold prefix_def Le_def) |
|
404 |
apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD]) |
|
405 |
done |
|
406 |
||
30198 | 407 |
lemma refl_Ge [iff]: "refl Ge" |
408 |
by (unfold refl_on_def Ge_def, auto) |
|
13798 | 409 |
|
410 |
lemma antisym_Ge [iff]: "antisym Ge" |
|
411 |
by (unfold antisym_def Ge_def, auto) |
|
412 |
||
413 |
lemma trans_Ge [iff]: "trans Ge" |
|
414 |
by (unfold trans_def Ge_def, auto) |
|
415 |
||
416 |
lemma pfixGe_refl [iff]: "x pfixGe x" |
|
417 |
by simp |
|
418 |
||
419 |
lemma pfixGe_trans: "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z" |
|
420 |
by (blast intro: genPrefix_trans) |
|
421 |
||
422 |
lemma pfixGe_antisym: "[| x pfixGe y; y pfixGe x |] ==> x = y" |
|
423 |
by (blast intro: genPrefix_antisym) |
|
424 |
||
425 |
lemma prefix_imp_pfixGe: "xs<=ys ==> xs pfixGe ys" |
|
426 |
apply (unfold prefix_def Ge_def) |
|
427 |
apply (blast intro: genPrefix_mono [THEN [2] rev_subsetD]) |
|
428 |
done |
|
6708 | 429 |
|
430 |
end |