| author | wenzelm |
| Thu, 15 Nov 2001 23:25:46 +0100 | |
| changeset 12218 | 6597093b77e7 |
| parent 5192 | 704dd3a6d47d |
| child 14981 | e73f8140af78 |
| permissions | -rw-r--r-- |
| mueller@3072 | 1 |
(* Title: HOLCF/IOA/ABP/Correctness.thy |
| mueller@3072 | 2 |
ID: $Id$ |
| wenzelm@12218 | 3 |
Author: Olaf Müller |
| wenzelm@12218 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
| mueller@3072 | 5 |
|
| wenzelm@12218 | 6 |
The main correctness proof: System_fin implements System. |
| mueller@3072 | 7 |
*) |
| mueller@3072 | 8 |
|
| mueller@3072 | 9 |
Correctness = IOA + Env + Impl + Impl_finite + |
| mueller@3072 | 10 |
|
| mueller@3072 | 11 |
consts |
| mueller@3072 | 12 |
|
| mueller@3072 | 13 |
reduce :: 'a list => 'a list |
| mueller@3072 | 14 |
|
| mueller@3072 | 15 |
abs :: 'c |
| mueller@3072 | 16 |
system_ioa :: "('m action, bool * 'm impl_state)ioa"
|
| mueller@3072 | 17 |
system_fin_ioa :: "('m action, bool * 'm impl_state)ioa"
|
| mueller@3072 | 18 |
|
| mueller@3072 | 19 |
primrec |
| mueller@3072 | 20 |
reduce_Nil "reduce [] = []" |
| mueller@3072 | 21 |
reduce_Cons "reduce(x#xs) = |
| mueller@3072 | 22 |
(case xs of |
| mueller@3072 | 23 |
[] => [x] |
| mueller@3072 | 24 |
| y#ys => (if (x=y) |
| mueller@3072 | 25 |
then reduce xs |
| mueller@3072 | 26 |
else (x#(reduce xs))))" |
| mueller@3072 | 27 |
|
| mueller@3072 | 28 |
|
| mueller@3072 | 29 |
defs |
| mueller@3072 | 30 |
|
| mueller@3072 | 31 |
system_def |
| mueller@3072 | 32 |
"system_ioa == (env_ioa || impl_ioa)" |
| mueller@3072 | 33 |
|
| mueller@3072 | 34 |
system_fin_def |
| mueller@3072 | 35 |
"system_fin_ioa == (env_ioa || impl_fin_ioa)" |
| mueller@3072 | 36 |
|
| mueller@3072 | 37 |
abs_def "abs == |
| mueller@3072 | 38 |
(%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), |
| mueller@3072 | 39 |
(reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))" |
| mueller@3072 | 40 |
|
| mueller@3072 | 41 |
rules |
| mueller@3072 | 42 |
|
| mueller@3072 | 43 |
sys_IOA "IOA system_ioa" |
| mueller@3072 | 44 |
sys_fin_IOA "IOA system_fin_ioa" |
| mueller@3072 | 45 |
|
| mueller@3072 | 46 |
end |
| mueller@3072 | 47 |
|
| mueller@3072 | 48 |