|
1138
|
1 |
(* Title: HOL/IOA/example/Correctness.thy
|
|
1050
|
2 |
ID: $Id$
|
|
1138
|
3 |
Author: Tobias Nipkow & Konrad Slind
|
|
1050
|
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 |
|
|
1138
|
13 |
reduce :: "'a list => 'a list"
|
|
1050
|
14 |
|
|
1138
|
15 |
abs :: "'c"
|
|
|
16 |
system_ioa :: "('m action, bool * 'm impl_state)ioa"
|
|
|
17 |
system_fin_ioa :: "('m action, bool * 'm impl_state)ioa"
|
|
|
18 |
|
|
1050
|
19 |
primrec
|
|
|
20 |
reduce List.list
|
|
|
21 |
reduce_Nil "reduce [] = []"
|
|
|
22 |
reduce_Cons "reduce(x#xs) = \
|
|
|
23 |
\ (case xs of \
|
|
|
24 |
\ [] => [x] \
|
|
|
25 |
\ | y#ys => (if (x=y) \
|
|
|
26 |
\ then reduce xs \
|
|
|
27 |
\ else (x#(reduce xs))))"
|
|
|
28 |
|
|
1138
|
29 |
|
|
|
30 |
defs
|
|
|
31 |
|
|
|
32 |
system_def
|
|
|
33 |
"system_ioa == (env_ioa || impl_ioa)"
|
|
|
34 |
|
|
|
35 |
system_fin_def
|
|
|
36 |
"system_fin_ioa == (env_ioa || impl_fin_ioa)"
|
|
|
37 |
|
|
|
38 |
abs_def "abs == \
|
|
|
39 |
\ (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), \
|
|
|
40 |
\ (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
|
|
|
41 |
|
|
|
42 |
rules
|
|
|
43 |
|
|
|
44 |
sys_IOA "IOA system_ioa"
|
|
|
45 |
sys_fin_IOA "IOA system_fin_ioa"
|
|
|
46 |
|
|
1050
|
47 |
end
|
|
|
48 |
|
|
|
49 |
|
|
|
50 |
|