src/HOL/WF_Rel.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8703 816d8f6513be
child 9361 8b09c29453ac
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     1
(*  Title:      HOL/WF_Rel
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     2
    ID:         $Id$
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     3
    Author:     Konrad Slind
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     4
    Copyright   1995 TU Munich
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     5
3296
2ee6c397003d Deleted rprod: lex_prod is (usually?) enough
paulson
parents: 3237
diff changeset
     6
Derived WF relations: inverse image, lexicographic product, measure, ...
2ee6c397003d Deleted rprod: lex_prod is (usually?) enough
paulson
parents: 3237
diff changeset
     7
2ee6c397003d Deleted rprod: lex_prod is (usually?) enough
paulson
parents: 3237
diff changeset
     8
The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
2ee6c397003d Deleted rprod: lex_prod is (usually?) enough
paulson
parents: 3237
diff changeset
     9
subset of the lexicographic product, and therefore does not need to be defined
2ee6c397003d Deleted rprod: lex_prod is (usually?) enough
paulson
parents: 3237
diff changeset
    10
separately.
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    11
*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    12
3222
726a9b069947 Distributed Psubset stuff to basic set theory files, incl Finite.
nipkow
parents: 3193
diff changeset
    13
WF_Rel = Finite +
8262
08ad0a986db2 added instance declaration for finite product
oheimb
parents: 3296
diff changeset
    14
08ad0a986db2 added instance declaration for finite product
oheimb
parents: 3296
diff changeset
    15
(* actually belongs to Finite.thy *)
08ad0a986db2 added instance declaration for finite product
oheimb
parents: 3296
diff changeset
    16
instance "*" :: (finite,finite) finite   (finite_Prod) 
08ad0a986db2 added instance declaration for finite product
oheimb
parents: 3296
diff changeset
    17
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    18
consts
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3222
diff changeset
    19
  less_than :: "(nat*nat)set"
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3222
diff changeset
    20
  inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3222
diff changeset
    21
  measure   :: "('a => nat) => ('a * 'a)set"
8703
816d8f6513be Times -> <*>
nipkow
parents: 8262
diff changeset
    22
  lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
816d8f6513be Times -> <*>
nipkow
parents: 8262
diff changeset
    23
               (infixr "<*lex*>" 80)
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3222
diff changeset
    24
  finite_psubset  :: "('a set * 'a set) set"
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3222
diff changeset
    25
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    26
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    27
defs
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3222
diff changeset
    28
  less_than_def "less_than == trancl pred_nat"
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3222
diff changeset
    29
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    30
  inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}"
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    31
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3222
diff changeset
    32
  measure_def   "measure == inv_image less_than"
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    33
8703
816d8f6513be Times -> <*>
nipkow
parents: 8262
diff changeset
    34
  lex_prod_def  "ra <*lex*> rb == {((a,b),(a',b')) | a a' b b'.
816d8f6513be Times -> <*>
nipkow
parents: 8262
diff changeset
    35
                                   ((a,a') : ra | a=a' & (b,b') : rb)}"
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    36
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    37
  (* finite proper subset*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    38
  finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}"
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    39
end