TFL/WF1.thy
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
paulson@2112
     1
(* Derived wellfounded relations, plus customized-for-TFL theorems from WF *)
paulson@2112
     2
paulson@2112
     3
WF1 = List +
paulson@2112
     4
consts
paulson@2112
     5
 inv_image  :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
paulson@2112
     6
 measure    :: "('a => nat) => ('a * 'a)set"
paulson@2112
     7
    "**"    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
paulson@2112
     8
   rprod    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
paulson@2112
     9
   emptyr   :: "('a * 'b) set"
paulson@2112
    10
 pred_list  :: "('a list * 'a list) set"
paulson@2112
    11
paulson@2112
    12
defs
paulson@2112
    13
  inv_image_def "inv_image R f == {p. (f(fst p), f(snd p)) : R}"
paulson@2112
    14
paulson@2112
    15
  measure_def   "measure == inv_image (trancl pred_nat)"
paulson@2112
    16
paulson@2112
    17
  lex_prod_def  "ra**rb == {p. ? a a' b b'. 
paulson@2112
    18
                                p = ((a,b),(a',b')) & 
paulson@2112
    19
                               ((a,a') : ra | a=a' & (b,b') : rb)}"
paulson@2112
    20
paulson@2112
    21
  rprod_def     "rprod ra rb == {p. ? a a' b b'. 
paulson@2112
    22
                                p = ((a,b),(a',b')) & 
paulson@2112
    23
                               ((a,a') : ra & (b,b') : rb)}"
paulson@2112
    24
paulson@2112
    25
  emptyr_def    "emptyr == {}"
paulson@2112
    26
  pred_list_def "pred_list == {p. ? h. snd p = h#(fst p)}"
paulson@2112
    27
end