src/HOL/Wellfounded_Relations.thy
changeset 10213 01c2744a3786
child 11008 f7333f055ef6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Wellfounded_Relations.thy	Thu Oct 12 18:44:35 2000 +0200
     1.3 @@ -0,0 +1,44 @@
     1.4 +(*  Title:      HOL/Wellfounded_Relations
     1.5 +    ID:         $Id$
     1.6 +    Author:     Konrad Slind
     1.7 +    Copyright   1995 TU Munich
     1.8 +
     1.9 +Derived WF relations: inverse image, lexicographic product, measure, ...
    1.10 +
    1.11 +The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
    1.12 +subset of the lexicographic product, and therefore does not need to be defined
    1.13 +separately.
    1.14 +*)
    1.15 +
    1.16 +Wellfounded_Relations = Finite +
    1.17 +
    1.18 +(* actually belongs to theory Finite *)
    1.19 +instance unit :: finite                  (finite_unit)
    1.20 +instance "*" :: (finite,finite) finite   (finite_Prod)
    1.21 +
    1.22 +
    1.23 +constdefs
    1.24 + less_than :: "(nat*nat)set"
    1.25 +"less_than == trancl pred_nat"
    1.26 +
    1.27 + inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
    1.28 +"inv_image r f == {(x,y). (f(x), f(y)) : r}"
    1.29 +
    1.30 + measure   :: "('a => nat) => ('a * 'a)set"
    1.31 +"measure == inv_image less_than"
    1.32 +
    1.33 + lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
    1.34 +               (infixr "<*lex*>" 80)
    1.35 +"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
    1.36 +
    1.37 + (* finite proper subset*)
    1.38 + finite_psubset  :: "('a set * 'a set) set"
    1.39 +"finite_psubset == {(A,B). A < B & finite B}"
    1.40 +
    1.41 +(* For rec_defs where the first n parameters stay unchanged in the recursive
    1.42 +   call. See While for an application.
    1.43 +*)
    1.44 + same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
    1.45 +"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
    1.46 +
    1.47 +end