src/HOL/Wellfounded_Relations.thy
author oheimb
Thu Feb 15 16:00:40 2001 +0100 (2001-02-15)
changeset 11136 e34e7f6d9b57
parent 11008 f7333f055ef6
child 11451 8abfb4f7bd02
permissions -rw-r--r--
moved inv_image to Relation
     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 
    13 Wellfounded_Relations = Finite +
    14 
    15 (* actually belongs to theory Finite *)
    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
    36    call. See Library/While_Combinator.thy for an application.
    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