src/HOL/Wellfounded_Relations.thy
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 10213 01c2744a3786
child 11008 f7333f055ef6
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Wellfounded_Relations
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     3
    Author:     Konrad Slind
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     4
    Copyright   1995 TU Munich
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     5
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     6
Derived WF relations: inverse image, lexicographic product, measure, ...
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     7
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     8
The simple relational product, in which (x',y')<(x,y) iff x'<x and y'<y, is a
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     9
subset of the lexicographic product, and therefore does not need to be defined
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    10
separately.
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    11
*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    12
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    13
Wellfounded_Relations = Finite +
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    14
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    15
(* actually belongs to theory Finite *)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    16
instance unit :: finite                  (finite_unit)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    17
instance "*" :: (finite,finite) finite   (finite_Prod)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    18
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    19
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    20
constdefs
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    21
 less_than :: "(nat*nat)set"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    22
"less_than == trancl pred_nat"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    23
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    24
 inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    25
"inv_image r f == {(x,y). (f(x), f(y)) : r}"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    26
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    27
 measure   :: "('a => nat) => ('a * 'a)set"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    28
"measure == inv_image less_than"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    29
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    30
 lex_prod  :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    31
               (infixr "<*lex*>" 80)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    32
"ra <*lex*> rb == {((a,b),(a',b')). (a,a') : ra | a=a' & (b,b') : rb}"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    33
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    34
 (* finite proper subset*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    35
 finite_psubset  :: "('a set * 'a set) set"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    36
"finite_psubset == {(A,B). A < B & finite B}"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    37
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    38
(* For rec_defs where the first n parameters stay unchanged in the recursive
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    39
   call. See While for an application.
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    40
*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    41
 same_fst :: "('a => bool) => ('a => ('b * 'b)set) => (('a*'b)*('a*'b))set"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    42
"same_fst P R == {((x',y'),(x,y)) . x'=x & P x & (y',y) : R x}"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    43
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    44
end