2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 *) |
5 *) |
6 |
6 |
7 MaxPrefix = List_Prefix + |
7 theory MaxPrefix = List_Prefix: |
8 |
8 |
9 constdefs |
9 constdefs |
10 is_maxpref :: ('a list => bool) => 'a list => 'a list => bool |
10 is_maxpref :: "('a list => bool) => 'a list => 'a list => bool" |
11 "is_maxpref P xs ys == |
11 "is_maxpref P xs ys == |
12 xs <= ys & (xs=[] | P xs) & (!zs. zs <= ys & P zs --> zs <= xs)" |
12 xs <= ys & (xs=[] | P xs) & (!zs. zs <= ys & P zs --> zs <= xs)" |
13 |
13 |
14 types 'a splitter = "'a list => 'a list * 'a list" |
14 types 'a splitter = "'a list => 'a list * 'a list" |
|
15 |
15 constdefs |
16 constdefs |
16 is_maxsplitter :: "('a list => bool) => 'a splitter => bool" |
17 is_maxsplitter :: "('a list => bool) => 'a splitter => bool" |
17 "is_maxsplitter P f == |
18 "is_maxsplitter P f == |
18 (!xs ps qs. f xs = (ps,qs) = (xs=ps@qs & is_maxpref P ps xs))" |
19 (!xs ps qs. f xs = (ps,qs) = (xs=ps@qs & is_maxpref P ps xs))" |
19 |
20 |
21 maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => 'a splitter" |
22 maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => 'a splitter" |
22 primrec |
23 primrec |
23 "maxsplit P res ps [] = (if P ps then (ps,[]) else res)" |
24 "maxsplit P res ps [] = (if P ps then (ps,[]) else res)" |
24 "maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res) |
25 "maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res) |
25 (ps@[q]) qs" |
26 (ps@[q]) qs" |
|
27 |
|
28 declare split_if[split del] |
|
29 |
|
30 lemma maxsplit_lemma: "!!(ps::'a list) res. |
|
31 (maxsplit P res ps qs = (xs,ys)) = |
|
32 (if EX us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) |
|
33 else (xs,ys)=res)" |
|
34 apply(unfold is_maxpref_def) |
|
35 apply (induct "qs") |
|
36 apply (simp split: split_if) |
|
37 apply blast |
|
38 apply simp |
|
39 apply (erule thin_rl) |
|
40 apply clarify |
|
41 apply (case_tac "EX us. us <= list & P (ps @ a # us)") |
|
42 apply (subgoal_tac "EX us. us <= a # list & P (ps @ us)") |
|
43 apply simp |
|
44 apply (blast intro: prefix_Cons[THEN iffD2]) |
|
45 apply (subgoal_tac "~P(ps@[a])") |
|
46 prefer 2 apply blast |
|
47 apply (simp (no_asm_simp)) |
|
48 apply (case_tac "EX us. us <= a#list & P (ps @ us)") |
|
49 apply simp |
|
50 apply clarify |
|
51 apply (case_tac "us") |
|
52 apply (rule iffI) |
|
53 apply (simp add: prefix_Cons prefix_append) |
|
54 apply blast |
|
55 apply (simp add: prefix_Cons prefix_append) |
|
56 apply clarify |
|
57 apply (erule disjE) |
|
58 apply (fast dest: order_antisym) |
|
59 apply clarify |
|
60 apply (erule disjE) |
|
61 apply clarify |
|
62 apply simp |
|
63 apply (erule disjE) |
|
64 apply clarify |
|
65 apply simp |
|
66 apply blast |
|
67 apply simp |
|
68 apply (subgoal_tac "~P(ps)") |
|
69 apply (simp (no_asm_simp)) |
|
70 apply fastsimp |
|
71 done |
|
72 |
|
73 declare split_if[split add] |
|
74 |
|
75 lemma is_maxpref_Nil[simp]: |
|
76 "~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])" |
|
77 apply(unfold is_maxpref_def) |
|
78 apply blast |
|
79 done |
|
80 |
|
81 lemma is_maxsplitter_maxsplit: |
|
82 "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)" |
|
83 apply(unfold is_maxsplitter_def) |
|
84 apply (simp add: maxsplit_lemma) |
|
85 apply (fastsimp) |
|
86 done |
|
87 |
|
88 lemmas maxsplit_eq = is_maxsplitter_maxsplit[simplified is_maxsplitter_def] |
|
89 |
26 end |
90 end |