| changeset 252 | a4dc62a46ee4 |
| parent 251 | f04b33ce250f |
| child 253 | 132634d24019 |
| 251:f04b33ce250f | 252:a4dc62a46ee4 |
|---|---|
1 (* Title: HOL/IOA/example/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 = Solve + Impl + Spec + |
|
10 |
|
11 consts |
|
12 |
|
13 hom :: "'m impl_state => 'm list" |
|
14 |
|
15 defs |
|
16 |
|
17 hom_def |
|
18 "hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)), |
|
19 sq(sen(s)), |
|
20 ttl(sq(sen(s))))" |
|
21 |
|
22 end |