src/CCL/wfd.thy
changeset 0 a5a9c433f639
child 227 5415c6ad0028
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CCL/wfd.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,34 @@
     1.4 +(*  Title: 	CCL/wf.thy
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Well-founded relations in CCL.
    1.10 +*)
    1.11 +
    1.12 +Wfd = Trancl + Type +
    1.13 +
    1.14 +consts
    1.15 +      (*** Predicates ***)
    1.16 +  Wfd        ::       "[i set] => o"
    1.17 +      (*** Relations ***)
    1.18 +  wf         ::       "[i set] => i set"
    1.19 +  wmap       ::       "[i=>i,i set] => i set"
    1.20 +  "**"       ::       "[i set,i set] => i set"      (infixl 70)
    1.21 +  NatPR      ::       "i set"
    1.22 +  ListPR     ::       "i set => i set"
    1.23 +
    1.24 +rules
    1.25 +
    1.26 +  Wfd_def
    1.27 +  "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a.a:P)"
    1.28 +
    1.29 +  wf_def         "wf(R) == {x.x:R & Wfd(R)}"
    1.30 +
    1.31 +  wmap_def       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
    1.32 +  lex_def
    1.33 +  "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
    1.34 +
    1.35 +  NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
    1.36 +  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"
    1.37 +end