src/HOL/WF_Rel.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3296 2ee6c397003d
child 8262 08ad0a986db2
permissions -rw-r--r--
tidying
paulson@3193
     1
(*  Title:      HOL/WF_Rel
paulson@3193
     2
    ID:         $Id$
paulson@3193
     3
    Author:     Konrad Slind
paulson@3193
     4
    Copyright   1995 TU Munich
paulson@3193
     5
paulson@3296
     6
Derived WF relations: inverse image, lexicographic product, measure, ...
paulson@3296
     7
paulson@3296
     8
The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
paulson@3296
     9
subset of the lexicographic product, and therefore does not need to be defined
paulson@3296
    10
separately.
paulson@3193
    11
*)
paulson@3193
    12
nipkow@3222
    13
WF_Rel = Finite +
paulson@3193
    14
consts
paulson@3237
    15
  less_than :: "(nat*nat)set"
paulson@3237
    16
  inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
paulson@3237
    17
  measure   :: "('a => nat) => ('a * 'a)set"
paulson@3237
    18
  "**"      :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
paulson@3237
    19
  finite_psubset  :: "('a set * 'a set) set"
paulson@3237
    20
paulson@3193
    21
paulson@3193
    22
defs
paulson@3237
    23
  less_than_def "less_than == trancl pred_nat"
paulson@3237
    24
paulson@3193
    25
  inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}"
paulson@3193
    26
paulson@3237
    27
  measure_def   "measure == inv_image less_than"
paulson@3193
    28
paulson@3193
    29
  lex_prod_def  "ra**rb == {p. ? a a' b b'. 
paulson@3193
    30
                                p = ((a,b),(a',b')) & 
paulson@3193
    31
                               ((a,a') : ra | a=a' & (b,b') : rb)}"
paulson@3193
    32
paulson@3193
    33
  (* finite proper subset*)
paulson@3193
    34
  finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}"
paulson@3193
    35
end