equal
deleted
inserted
replaced
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 |
|