author | nipkow |
Wed, 05 Nov 1997 09:08:35 +0100 | |
changeset 4137 | 2ce2e659c2b1 |
child 4712 | facfbbca7242 |
permissions | -rw-r--r-- |
4137
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
1 |
(* Title: HOL/Lex/AutoChopper1.thy |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
4 |
Copyright 1997 TUM |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
5 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
6 |
This is a version of theory AutoChopper base on a non-primrec definition of |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
7 |
`acc'. Advantage: does not need lazy evaluation for reasonable (quadratic?) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
8 |
performance. |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
9 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
10 |
Verification: |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
11 |
1. Via AutoChopper.acc using |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
12 |
Claim: acc A xs s [] [] [] = AutoChopper.acc xs s [] [] ([],xs) A |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
13 |
Generalization? |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
14 |
2. Directly. |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
15 |
Hope: acc is easier to verify than AutoChopper.acc because simpler. |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
16 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
17 |
No proofs yet. |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
18 |
*) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
19 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
20 |
AutoChopper1 = Auto + Chopper + WF_Rel + |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
21 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
22 |
consts |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
23 |
acc :: "(('a,'b)auto * 'a list * 'b * 'a list list * 'a list * 'a list) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
24 |
=> 'a list list * 'a list" |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
25 |
recdef acc "inv_image (less_than ** less_than) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
26 |
(%(A,ys,s,xss,zs,xs). (length xs + length ys + length zs, |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
27 |
length ys))" |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
28 |
simpset "simpset() addsimps (less_add_Suc2::add_ac) addsplits [expand_if]" |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
29 |
"acc(A,[],s,xss,zs,[]) = (xss, zs)" |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
30 |
"acc(A,[],s,xss,zs,x#xs) = acc(A,zs,start A, xss @ [x#xs],[],[])" |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
31 |
"acc(A,y#ys,s,xss,zs,xs) = |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
32 |
(let s' = next A s y; |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
33 |
zs' = (if fin A s' then [] else zs@[y]); |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
34 |
xs' = (if fin A s' then xs@zs@[y] else xs) |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
35 |
in acc(A,ys,s',xss,zs',xs'))" |
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
36 |
|
2ce2e659c2b1
Added an alternativ version of AutoChopper and a theory for the conversion of
nipkow
parents:
diff
changeset
|
37 |
end |