28 |
28 |
29 consts |
29 consts |
30 acc :: "[('a,'s)da, 's, 'a list list*'a list, 'a list, 'a list, 'a list] |
30 acc :: "[('a,'s)da, 's, 'a list list*'a list, 'a list, 'a list, 'a list] |
31 => 'a list list * 'a list" |
31 => 'a list list * 'a list" |
32 primrec acc List.list |
32 primrec acc List.list |
33 "acc A s r [] ys zs = (if ys=[] then r else (ys#fst(r),snd(r)))" |
33 "acc A s r ps [] zs = (if ps=[] then r else (ps#fst(r),snd(r)))" |
34 "acc A s r (x#xs) ys zs = |
34 "acc A s r ps (x#xs) zs = |
35 (let t = next A x s |
35 (let t = next A x s |
36 in if fin A t |
36 in if fin A t |
37 then acc A t (acc A (start A) ([],xs) xs [] []) |
37 then acc A t (acc A (start A) ([],xs) [] xs []) |
38 xs (zs@[x]) (zs@[x]) |
38 (zs@[x]) xs (zs@[x]) |
39 else acc A t r xs ys (zs@[x]))" |
39 else acc A t r ps xs (zs@[x]))" |
40 |
40 |
41 constdefs |
41 constdefs |
42 auto_chopper :: ('a,'s)da => 'a chopper |
42 auto_chopper :: ('a,'s)da => 'a chopper |
43 "auto_chopper A xs == acc A (start A) ([],xs) xs [] []" |
43 "auto_chopper A xs == acc A (start A) ([],xs) [] xs []" |
44 |
44 |
45 (* acc_prefix is an auxiliary notion for the proof *) |
45 (* acc_prefix is an auxiliary notion for the proof *) |
46 constdefs |
46 constdefs |
47 acc_prefix :: ('a,'s)da => 'a list => 's => bool |
47 acc_prefix :: ('a,'s)da => 'a list => 's => bool |
48 "acc_prefix A xs s == ? us. us <= xs & us~=[] & fin A (delta A us s)" |
48 "acc_prefix A xs s == ? us. us <= xs & us~=[] & fin A (delta A us s)" |