changeset 3073 | 88366253a09a |
child 3898 | f6bf42312e9e |
3072:a31419014be5 | 3073:88366253a09a |
---|---|
1 (* Title: HOL/IOA/NTP/Correctness.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 The main correctness proof: Impl implements Spec |
|
7 *) |
|
8 |
|
9 Correctness = IOA + Impl + Spec + |
|
10 |
|
11 constdefs |
|
12 |
|
13 hom :: 'm impl_state => 'm list |
|
14 "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s) |
|
15 else ttl(sq(sen s)))" |
|
16 |
|
17 end |