src/HOL/Wellfounded_Relations.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10213 01c2744a3786
child 11136 e34e7f6d9b57
permissions -rw-r--r--
improved theory reference in comment
nipkow@10213
     1
(*  Title:      HOL/Wellfounded_Relations
nipkow@10213
     2
    ID:         $Id$
nipkow@10213
     3
    Author:     Konrad Slind
nipkow@10213
     4
    Copyright   1995 TU Munich
nipkow@10213
     5
nipkow@10213
     6
Derived WF relations: inverse image, lexicographic product, measure, ...
nipkow@10213
     7
nipkow@10213
     8
The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
nipkow@10213
     9
subset of the lexicographic product, and therefore does not need to be defined
nipkow@10213
    10
separately.
nipkow@10213
    11
*)
nipkow@10213
    12
nipkow@10213
    13
Wellfounded_Relations = Finite +
nipkow@10213
    14
nipkow@10213
    15
(* actually belongs to theory Finite *)
nipkow@10213
    16
instance unit :: finite                  (finite_unit)
nipkow@10213
    17
instance "*" :: (finite,finite) finite   (finite_Prod)
nipkow@10213
    18
nipkow@10213
    19
nipkow@10213
    20
constdefs
nipkow@10213
    21
 less_than :: "(nat*nat)set"
nipkow@10213
    22
"less_than == trancl pred_nat"
nipkow@10213
    23
nipkow@10213
    24
 inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
nipkow@10213
    25
"inv_image r f == {(x,y). (f(x), f(y)) : r}"
nipkow@10213
    26
nipkow@10213
    27
 measure   :: "('a => nat) => ('a * 'a)set"
nipkow@10213
    28
"measure == inv_image less_than"
nipkow@10213
    29
nipkow@10213
    30
 lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
nipkow@10213
    31
               (infixr "<*lex*>" 80)
nipkow@10213
    32
"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
nipkow@10213
    33
nipkow@10213
    34
 (* finite proper subset*)
nipkow@10213
    35
 finite_psubset  :: "('a set * 'a set) set"
nipkow@10213
    36
"finite_psubset == {(A,B). A < B & finite B}"
nipkow@10213
    37
nipkow@10213
    38
(* For rec_defs where the first n parameters stay unchanged in the recursive
oheimb@11008
    39
   call. See Library/While_Combinator.thy for an application.
nipkow@10213
    40
*)
nipkow@10213
    41
 same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
nipkow@10213
    42
"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
nipkow@10213
    43
nipkow@10213
    44
end