equal
deleted
inserted
replaced
13 Based on Lex/Prefix |
13 Based on Lex/Prefix |
14 *) |
14 *) |
15 |
15 |
16 header {*The Prefix Ordering on Lists*} |
16 header {*The Prefix Ordering on Lists*} |
17 |
17 |
18 theory ListOrder imports Main begin |
18 theory ListOrder |
|
19 imports Main |
|
20 begin |
19 |
21 |
20 inductive_set |
22 inductive_set |
21 genPrefix :: "('a * 'a)set => ('a list * 'a list)set" |
23 genPrefix :: "('a * 'a)set => ('a list * 'a list)set" |
22 for r :: "('a * 'a)set" |
24 for r :: "('a * 'a)set" |
23 where |
25 where |
26 | prepend: "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==> |
28 | prepend: "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==> |
27 (x#xs, y#ys) : genPrefix(r)" |
29 (x#xs, y#ys) : genPrefix(r)" |
28 |
30 |
29 | append: "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" |
31 | append: "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" |
30 |
32 |
31 instance list :: (type)ord .. |
33 instantiation list :: (type) ord |
32 |
34 begin |
33 defs |
35 |
34 prefix_def: "xs <= zs == (xs,zs) : genPrefix Id" |
36 definition |
35 |
37 prefix_def: "xs <= zs \<longleftrightarrow> (xs, zs) : genPrefix Id" |
36 strict_prefix_def: "xs < zs == xs <= zs & xs ~= (zs::'a list)" |
38 |
37 |
39 definition |
|
40 strict_prefix_def: "xs < zs \<longleftrightarrow> xs \<le> zs \<and> \<not> zs \<le> (xs :: 'a list)" |
|
41 |
|
42 instance .. |
38 |
43 |
39 (*Constants for the <= and >= relations, used below in translations*) |
44 (*Constants for the <= and >= relations, used below in translations*) |
|
45 |
|
46 end |
|
47 |
40 constdefs |
48 constdefs |
41 Le :: "(nat*nat) set" |
49 Le :: "(nat*nat) set" |
42 "Le == {(x,y). x <= y}" |
50 "Le == {(x,y). x <= y}" |
43 |
51 |
44 Ge :: "(nat*nat) set" |
52 Ge :: "(nat*nat) set" |
266 lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys" |
274 lemma prefix_antisym: "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys" |
267 apply (unfold prefix_def) |
275 apply (unfold prefix_def) |
268 apply (blast intro: genPrefix_antisym) |
276 apply (blast intro: genPrefix_antisym) |
269 done |
277 done |
270 |
278 |
271 lemma prefix_less_le: "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)" |
279 lemma prefix_less_le_not_le: "!!xs::'a list. (xs < zs) = (xs <= zs & \<not> zs \<le> xs)" |
272 by (unfold strict_prefix_def, auto) |
280 by (unfold strict_prefix_def, auto) |
273 |
281 |
274 instance list :: (type) order |
282 instance list :: (type) order |
275 by (intro_classes, |
283 by (intro_classes, |
276 (assumption | rule prefix_refl prefix_trans prefix_antisym |
284 (assumption | rule prefix_refl prefix_trans prefix_antisym |
277 prefix_less_le)+) |
285 prefix_less_le_not_le)+) |
278 |
286 |
279 (*Monotonicity of "set" operator WRT prefix*) |
287 (*Monotonicity of "set" operator WRT prefix*) |
280 lemma set_mono: "xs <= ys ==> set xs <= set ys" |
288 lemma set_mono: "xs <= ys ==> set xs <= set ys" |
281 apply (unfold prefix_def) |
289 apply (unfold prefix_def) |
282 apply (erule genPrefix.induct, auto) |
290 apply (erule genPrefix.induct, auto) |