author | wenzelm |
Tue, 28 Mar 2000 12:28:24 +0200 | |
changeset 8599 | 58b6f99dd5a9 |
parent 7626 | 5997f35954d7 |
permissions | -rw-r--r-- |
7626 | 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 |