TFL/WF1.thy

Konrad Slind's TFL

(* Derived wellfounded relations, plus customized-for-TFL theorems from WF *)

WF1 = List +
consts
 inv_image  :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set"
 measure    :: "('a => nat) => ('a * 'a)set"
    "**"    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
   rprod    :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set"
   emptyr   :: "('a * 'b) set"
 pred_list  :: "('a list * 'a list) set"

defs
  inv_image_def "inv_image R f == {p. (f(fst p), f(snd p)) : R}"

  measure_def   "measure == inv_image (trancl pred_nat)"

  lex_prod_def  "ra**rb == {p. ? a a' b b'. 
                                p = ((a,b),(a',b')) & 
                               ((a,a') : ra | a=a' & (b,b') : rb)}"

  rprod_def     "rprod ra rb == {p. ? a a' b b'. 
                                p = ((a,b),(a',b')) & 
                               ((a,a') : ra & (b,b') : rb)}"

  emptyr_def    "emptyr == {}"
  pred_list_def "pred_list == {p. ? h. snd p = h#(fst p)}"
end