14052
|
1 |
(* Title: ZF/UNITY/Monotonicity.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
|
|
4 |
Copyright 2002 University of Cambridge
|
|
5 |
|
|
6 |
Monotonicity of an operator (meta-function) with respect to arbitrary set relations.
|
|
7 |
*)
|
|
8 |
|
|
9 |
Monotonicity = GenPrefix + MultisetSum +
|
|
10 |
constdefs
|
|
11 |
mono1 :: [i, i, i, i, i=>i] => o
|
|
12 |
"mono1(A, r, B, s, f) ==
|
|
13 |
(ALL x:A. ALL y:A. <x, y>:r --> <f(x), f(y)>:s) & (ALL x:A. f(x):B)"
|
|
14 |
|
|
15 |
(* monotonicity of a 2-place meta-function f *)
|
|
16 |
|
|
17 |
mono2 :: [i, i, i, i, i, i, [i,i]=>i] => o
|
|
18 |
"mono2(A, r, B, s, C, t, f) == (ALL x:A. ALL y:A. ALL u:B. ALL v:B.
|
|
19 |
<x, y>:r & <u,v>:s --> <f(x, u), f(y,v)>:t) &
|
|
20 |
(ALL x:A. ALL y:B. f(x,y):C)"
|
|
21 |
|
|
22 |
(* Internalized relations on sets and multisets *)
|
|
23 |
|
|
24 |
SetLe :: i =>i
|
|
25 |
"SetLe(A) == {<x, y>:Pow(A)*Pow(A). x <= y}"
|
|
26 |
|
|
27 |
MultLe :: [i,i] =>i
|
|
28 |
"MultLe(A, r) == multirel(A, r - id(A)) Un id(Mult(A))"
|
|
29 |
|
|
30 |
end |