src/HOL/BCV/Semilat.thy

Completely new version of BCV

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

Semilattices
*)

Semilat = Main +

types 'a ord    = 'a => 'a => bool
      'a binop  = 'a => 'a => 'a
      'a sl     = "'a set * 'a ord * 'a binop"

consts
 "@lesub"   :: 'a => 'a ord => 'a => bool ("(_ /<='__ _)" [50, 1000, 51] 50)
 "@lesssub" :: 'a => 'a ord => 'a => bool ("(_ /<'__ _)" [50, 1000, 51] 50)
defs
lesub_def   "x <=_r y == r x y"
lesssub_def "x <_r y  == x <=_r y & x ~= y"

consts
 "@plussub" :: 'a => ('a => 'b => 'c) => 'b => 'c ("(_ /+'__ _)" [65, 1000, 66] 65)
defs
plussub_def   "x +_f y == f x y"


constdefs
 ord :: "('a*'a)set => 'a ord"
"ord r == %x y. (x,y):r"

 order :: 'a ord => bool
"order r == (!x. x <=_r x) &
            (!x y. x <=_r y & y <=_r x --> x=y) &
            (!x y z. x <=_r y & y <=_r z --> x <=_r z)"

 acc :: 'a ord => bool
"acc r == wf{(y,x) . x <_r y}"

 top :: 'a ord => 'a => bool
"top r T == !x. x <=_r T"

 closed :: 'a set => 'a binop => bool
"closed A f == !x:A. !y:A. x +_f y : A"

 semilat :: "'a sl => bool"
"semilat == %(A,r,f). order r & closed A f &
                (!x:A. !y:A. x <=_r x +_f y)  &
                (!x:A. !y:A. y <=_r x +_f y)  &
                (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"

 is_ub :: "('a*'a)set => 'a => 'a => 'a => bool"
"is_ub r x y u == (x,u):r & (y,u):r"

 is_lub :: "('a*'a)set => 'a => 'a => 'a => bool"
"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"

 some_lub :: "('a*'a)set => 'a => 'a => 'a"
"some_lub r x y == SOME z. is_lub r x y z"

end