| changeset 7626 | 5997f35954d7 |
| 7625:94b2a50e69a5 | 7626:5997f35954d7 |
|---|---|
1 (* Title: HOL/BCV/Types0.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1999 TUM |
|
5 |
|
6 Types for the register machine |
|
7 *) |
|
8 |
|
9 Types0 = SemiLattice + |
|
10 |
|
11 datatype typ = Atyp | Btyp | Ctyp | Top |
|
12 |
|
13 instance typ :: ord |
|
14 instance typ :: plus |
|
15 |
|
16 defs |
|
17 le_typ "t1 <= t2 == (t1=t2) | (t1=Atyp & t2=Btyp) | (t2=Top)" |
|
18 less_typ "(t1::typ) < t2 == t1 <= t2 & t1 ~= t2" |
|
19 plus_typ "t1 + t2 == if t1<=t2 then t2 else if t2 <= t1 then t1 else Top" |
|
20 |
|
21 end |