src/CCL/Wfd.thy
 changeset 0 a5a9c433f639 child 227 5415c6ad0028
equal inserted replaced
-1:000000000000 0:a5a9c433f639
`       `
`     1 (*  Title: 	CCL/wf.thy`
`       `
`     2     ID:         \$Id\$`
`       `
`     3     Author: 	Martin Coen, Cambridge University Computer Laboratory`
`       `
`     4     Copyright   1993  University of Cambridge`
`       `
`     5 `
`       `
`     6 Well-founded relations in CCL.`
`       `
`     7 *)`
`       `
`     8 `
`       `
`     9 Wfd = Trancl + Type +`
`       `
`    10 `
`       `
`    11 consts`
`       `
`    12       (*** Predicates ***)`
`       `
`    13   Wfd        ::       "[i set] => o"`
`       `
`    14       (*** Relations ***)`
`       `
`    15   wf         ::       "[i set] => i set"`
`       `
`    16   wmap       ::       "[i=>i,i set] => i set"`
`       `
`    17   "**"       ::       "[i set,i set] => i set"      (infixl 70)`
`       `
`    18   NatPR      ::       "i set"`
`       `
`    19   ListPR     ::       "i set => i set"`
`       `
`    20 `
`       `
`    21 rules`
`       `
`    22 `
`       `
`    23   Wfd_def`
`       `
`    24   "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a.a:P)"`
`       `
`    25 `
`       `
`    26   wf_def         "wf(R) == {x.x:R & Wfd(R)}"`
`       `
`    27 `
`       `
`    28   wmap_def       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"`
`       `
`    29   lex_def`
`       `
`    30   "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"`
`       `
`    31 `
`       `
`    32   NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"`
`       `
`    33   ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h.t>}"`
`       `
`    34 end`