1 (* Title: HOL/BCV/Semilat.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 |
|
6 Semilattices |
|
7 *) |
|
8 |
|
9 Semilat = Main + |
|
10 |
|
11 types 'a ord = 'a => 'a => bool |
|
12 'a binop = 'a => 'a => 'a |
|
13 'a sl = "'a set * 'a ord * 'a binop" |
|
14 |
|
15 consts |
|
16 "@lesub" :: 'a => 'a ord => 'a => bool ("(_ /<='__ _)" [50, 1000, 51] 50) |
|
17 "@lesssub" :: 'a => 'a ord => 'a => bool ("(_ /<'__ _)" [50, 1000, 51] 50) |
|
18 defs |
|
19 lesub_def "x <=_r y == r x y" |
|
20 lesssub_def "x <_r y == x <=_r y & x ~= y" |
|
21 |
|
22 consts |
|
23 "@plussub" :: 'a => ('a => 'b => 'c) => 'b => 'c ("(_ /+'__ _)" [65, 1000, 66] 65) |
|
24 defs |
|
25 plussub_def "x +_f y == f x y" |
|
26 |
|
27 |
|
28 constdefs |
|
29 ord :: "('a*'a)set => 'a ord" |
|
30 "ord r == %x y. (x,y):r" |
|
31 |
|
32 order :: 'a ord => bool |
|
33 "order r == (!x. x <=_r x) & |
|
34 (!x y. x <=_r y & y <=_r x --> x=y) & |
|
35 (!x y z. x <=_r y & y <=_r z --> x <=_r z)" |
|
36 |
|
37 acc :: 'a ord => bool |
|
38 "acc r == wf{(y,x) . x <_r y}" |
|
39 |
|
40 top :: 'a ord => 'a => bool |
|
41 "top r T == !x. x <=_r T" |
|
42 |
|
43 closed :: 'a set => 'a binop => bool |
|
44 "closed A f == !x:A. !y:A. x +_f y : A" |
|
45 |
|
46 semilat :: "'a sl => bool" |
|
47 "semilat == %(A,r,f). order r & closed A f & |
|
48 (!x:A. !y:A. x <=_r x +_f y) & |
|
49 (!x:A. !y:A. y <=_r x +_f y) & |
|
50 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)" |
|
51 |
|
52 is_ub :: "('a*'a)set => 'a => 'a => 'a => bool" |
|
53 "is_ub r x y u == (x,u):r & (y,u):r" |
|
54 |
|
55 is_lub :: "('a*'a)set => 'a => 'a => 'a => bool" |
|
56 "is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)" |
|
57 |
|
58 some_lub :: "('a*'a)set => 'a => 'a => 'a" |
|
59 "some_lub r x y == SOME z. is_lub r x y z" |
|
60 |
|
61 end |
|