author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8703  816d8f6513be 
child 9361  8b09c29453ac 
permissions  rwrr 
3193  1 
(* Title: HOL/WF_Rel 
2 
ID: $Id$ 

3 
Author: Konrad Slind 

4 
Copyright 1995 TU Munich 

5 

3296  6 
Derived WF relations: inverse image, lexicographic product, measure, ... 
7 

8 
The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a 

9 
subset of the lexicographic product, and therefore does not need to be defined 

10 
separately. 

3193  11 
*) 
12 

3222
726a9b069947
Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents:
3193
diff
changeset

13 
WF_Rel = Finite + 
8262  14 

15 
(* actually belongs to Finite.thy *) 

16 
instance "*" :: (finite,finite) finite (finite_Prod) 

17 

3193  18 
consts 
3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset

19 
less_than :: "(nat*nat)set" 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset

20 
inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset

21 
measure :: "('a => nat) => ('a * 'a)set" 
8703  22 
lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" 
23 
(infixr "<*lex*>" 80) 

3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset

24 
finite_psubset :: "('a set * 'a set) set" 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset

25 

3193  26 

27 
defs 

3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset

28 
less_than_def "less_than == trancl pred_nat" 
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset

29 

3193  30 
inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}" 
31 

3237
4da86d44de33
Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents:
3222
diff
changeset

32 
measure_def "measure == inv_image less_than" 
3193  33 

8703  34 
lex_prod_def "ra <*lex*> rb == {((a,b),(a',b'))  a a' b b'. 
35 
((a,a') : ra  a=a' & (b,b') : rb)}" 

3193  36 

37 
(* finite proper subset*) 

38 
finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}" 

39 
end 