|
1050
|
1 |
(* Title: HOL/IOA/ABP/Correctness.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow & Olaf Mueller
|
|
|
4 |
Copyright 1994 TU Muenchen
|
|
|
5 |
|
|
|
6 |
The main correctness proof: System_fin implements System
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Correctness = Solve + Env + Impl + Impl_finite +
|
|
|
10 |
|
|
|
11 |
consts
|
|
|
12 |
|
|
|
13 |
reduce :: "'a list => 'a list"
|
|
|
14 |
|
|
|
15 |
primrec
|
|
|
16 |
reduce List.list
|
|
|
17 |
reduce_Nil "reduce [] = []"
|
|
|
18 |
reduce_Cons "reduce(x#xs) = \
|
|
|
19 |
\ (case xs of \
|
|
|
20 |
\ [] => [x] \
|
|
|
21 |
\ | y#ys => (if (x=y) \
|
|
|
22 |
\ then reduce xs \
|
|
|
23 |
\ else (x#(reduce xs))))"
|
|
|
24 |
|
|
|
25 |
end
|
|
|
26 |
|
|
|
27 |
|
|
|
28 |
|