src/HOL/BCV/Err.thy

final tuning;

(*  Title:      HOL/BCV/Err.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000 TUM

The error type
*)

Err = Semilat +

datatype 'a err = Err | OK 'a

types 'a ebinop = 'a => 'a => 'a err
      'a esl =    "'a set * 'a ord * 'a ebinop"

constdefs
 lift :: ('a => 'b err) => ('a err => 'b err)
"lift f e == case e of Err => Err | OK x => f x"

 lift2 :: ('a => 'b => 'c err) => 'a err => 'b err => 'c err
"lift2 f e1 e2 ==
 case e1 of Err  => Err
          | OK x => (case e2 of Err => Err | OK y => f x y)"

 le :: 'a ord => 'a err ord
"le r e1 e2 ==
        case e2 of Err => True |
                   OK y => (case e1 of Err => False | OK x => x <=_r y)"

 sup :: ('a => 'b => 'c) => ('a err => 'b err => 'c err)
"sup f == lift2(%x y. OK(x +_f y))"

 err :: 'a set => 'a err set
"err A == insert Err {x . ? y:A. x = OK y}"

 esl :: 'a sl => 'a esl
"esl == %(A,r,f). (A,r, %x y. OK(f x y))"

 sl :: 'a esl => 'a err sl
"sl == %(A,r,f). (err A, le r, lift2 f)"

syntax
 err_semilat :: 'a esl => bool
translations
"err_semilat L" == "semilat(Err.sl L)"

end