equal
deleted
inserted
replaced
|
1 (* Title: HOL/BCV/Err.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 |
|
6 The error type |
|
7 *) |
|
8 |
|
9 Err = Semilat + |
|
10 |
|
11 datatype 'a err = Err | OK 'a |
|
12 |
|
13 types 'a ebinop = 'a => 'a => 'a err |
|
14 'a esl = "'a set * 'a ord * 'a ebinop" |
|
15 |
|
16 constdefs |
|
17 lift :: ('a => 'b err) => ('a err => 'b err) |
|
18 "lift f e == case e of Err => Err | OK x => f x" |
|
19 |
|
20 lift2 :: ('a => 'b => 'c err) => 'a err => 'b err => 'c err |
|
21 "lift2 f e1 e2 == |
|
22 case e1 of Err => Err |
|
23 | OK x => (case e2 of Err => Err | OK y => f x y)" |
|
24 |
|
25 le :: 'a ord => 'a err ord |
|
26 "le r e1 e2 == |
|
27 case e2 of Err => True | |
|
28 OK y => (case e1 of Err => False | OK x => x <=_r y)" |
|
29 |
|
30 sup :: ('a => 'b => 'c) => ('a err => 'b err => 'c err) |
|
31 "sup f == lift2(%x y. OK(x +_f y))" |
|
32 |
|
33 err :: 'a set => 'a err set |
|
34 "err A == insert Err {x . ? y:A. x = OK y}" |
|
35 |
|
36 esl :: 'a sl => 'a esl |
|
37 "esl == %(A,r,f). (A,r, %x y. OK(f x y))" |
|
38 |
|
39 sl :: 'a esl => 'a err sl |
|
40 "sl == %(A,r,f). (err A, le r, lift2 f)" |
|
41 |
|
42 syntax |
|
43 err_semilat :: 'a esl => bool |
|
44 translations |
|
45 "err_semilat L" == "semilat(Err.sl L)" |
|
46 |
|
47 end |