author | wenzelm |
Thu, 15 Nov 2001 18:20:13 +0100 | |
changeset 12207 | 4dff931b852f |
parent 11454 | 7514e5e21cb8 |
child 12398 | 9c27f28c8f5a |
permissions | -rw-r--r-- |
10213 | 1 |
(* Title: HOL/Wellfounded_Relations |
2 |
ID: $Id$ |
|
3 |
Author: Konrad Slind |
|
4 |
Copyright 1995 TU Munich |
|
5 |
||
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. |
|
11 |
*) |
|
12 |
||
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11451
diff
changeset
|
13 |
Wellfounded_Relations = Finite + |
10213 | 14 |
|
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11136
diff
changeset
|
15 |
(* logically belongs in Finite.thy, but the theorems are proved in Finite.ML *) |
10213 | 16 |
instance unit :: finite (finite_unit) |
17 |
instance "*" :: (finite,finite) finite (finite_Prod) |
|
18 |
||
19 |
||
20 |
constdefs |
|
21 |
less_than :: "(nat*nat)set" |
|
22 |
"less_than == trancl pred_nat" |
|
23 |
||
24 |
measure :: "('a => nat) => ('a * 'a)set" |
|
25 |
"measure == inv_image less_than" |
|
26 |
||
27 |
lex_prod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" |
|
28 |
(infixr "<*lex*>" 80) |
|
29 |
"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}" |
|
30 |
||
31 |
(* finite proper subset*) |
|
32 |
finite_psubset :: "('a set * 'a set) set" |
|
33 |
"finite_psubset == {(A,B). A < B & finite B}" |
|
34 |
||
35 |
(* For rec_defs where the first n parameters stay unchanged in the recursive |
|
11008 | 36 |
call. See Library/While_Combinator.thy for an application. |
10213 | 37 |
*) |
38 |
same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set" |
|
39 |
"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}" |
|
40 |
||
41 |
end |