equal
deleted
inserted
replaced
1 Correctness = Solve + Impl + Spec + "Lemmas" + |
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 + |
2 |
10 |
3 consts |
11 consts |
4 |
12 |
5 hom :: "'m impl_state => 'm list" |
13 hom :: "'m impl_state => 'm list" |
6 |
14 |
7 |
15 defs |
8 rules |
|
9 |
16 |
10 hom_def |
17 hom_def |
11 "hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)), \ |
18 "hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)), \ |
12 \ sq(sen(s)), \ |
19 \ sq(sen(s)), \ |
13 \ ttl(sq(sen(s))))" |
20 \ ttl(sq(sen(s))))" |