author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
6008 | 1 |
(* Title: HOL/IOA/example/Correctness.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
6008 | 5 |
|
12218 | 6 |
Correctness Proof. |
6008 | 7 |
*) |
8 |
||
9 |
Correctness = SimCorrectness + Spec + Impl + |
|
10 |
||
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
12218
diff
changeset
|
11 |
default type |
6008 | 12 |
|
13 |
consts |
|
14 |
||
15 |
sim_relation :: "((nat * bool) * (nat set * bool)) set" |
|
16 |
||
17 |
defs |
|
18 |
||
19 |
sim_relation_def |
|
20 |
"sim_relation == {qua. let c = fst qua; a = snd qua ; |
|
21 |
k = fst c; b = snd c; |
|
22 |
used = fst a; c = snd a |
|
23 |
in |
|
24 |
(! l:used. l < k) & b=c }" |
|
25 |
||
26 |
end |