9791
|
1 |
(* Title: HOL/BCV/Product.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2000 TUM
|
|
5 |
|
|
6 |
Products as semilattices
|
|
7 |
*)
|
|
8 |
|
|
9 |
Product = Err +
|
|
10 |
|
|
11 |
constdefs
|
|
12 |
le :: "'a ord => 'b ord => ('a * 'b) ord"
|
|
13 |
"le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'"
|
|
14 |
|
|
15 |
sup :: "'a ebinop => 'b ebinop => ('a * 'b)ebinop"
|
|
16 |
"sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
|
|
17 |
|
|
18 |
esl :: "'a esl => 'b esl => ('a * 'b ) esl"
|
|
19 |
"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
|
|
20 |
|
|
21 |
syntax "@lesubprod" :: "'a*'b => 'a ord => 'b ord => 'b => bool"
|
|
22 |
("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
|
|
23 |
translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
|
|
24 |
|
|
25 |
end
|