src/HOL/Trancl.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 6906 46652582f831
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1301
diff changeset
     1
(*  Title:      HOL/Trancl.thy
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1475
7f5a4cd08209 expanded tabs; renamed subtype to typedef;
clasohm
parents: 1301
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents: 972
diff changeset
     6
Relfexive and Transitive closure of a relation
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     7
1642
21db0cf9a1a4 Using new "Times" infix
paulson
parents: 1558
diff changeset
     8
rtrancl is reflexive/transitive closure;
21db0cf9a1a4 Using new "Times" infix
paulson
parents: 1558
diff changeset
     9
trancl  is transitive closure
21db0cf9a1a4 Using new "Times" infix
paulson
parents: 1558
diff changeset
    10
reflcl  is reflexive closure
1916
43521f79f016 Changed precedences to remove ambiguities in r^+ notation
paulson
parents: 1642
diff changeset
    11
43521f79f016 Changed precedences to remove ambiguities in r^+ notation
paulson
parents: 1642
diff changeset
    12
These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
43521f79f016 Changed precedences to remove ambiguities in r^+ notation
paulson
parents: 1642
diff changeset
    13
      atomic.
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    14
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    15
1128
64b30e3cc6d4 Trancl is now based on Relation which used to be in Integ.
nipkow
parents: 972
diff changeset
    16
Trancl = Lfp + Relation + 
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    17
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    18
constdefs
3499
ce1664057431 Reduced priority of postfix ^* etc operators such that they are the same as
nipkow
parents: 1916
diff changeset
    19
  rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
5608
a82a038a3e7a id <-> Id
nipkow
parents: 3499
diff changeset
    20
  "r^*  ==  lfp(%s. Id Un (r O s))"
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    21
3499
ce1664057431 Reduced priority of postfix ^* etc operators such that they are the same as
nipkow
parents: 1916
diff changeset
    22
  trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    23
  "r^+  ==  r O rtrancl(r)"
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    24
1301
42782316d510 Added various thms and tactics.
nipkow
parents: 1287
diff changeset
    25
syntax
6906
46652582f831 _reflcl;
wenzelm
parents: 5608
diff changeset
    26
  "_reflcl"  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    27
1301
42782316d510 Added various thms and tactics.
nipkow
parents: 1287
diff changeset
    28
translations
5608
a82a038a3e7a id <-> Id
nipkow
parents: 3499
diff changeset
    29
  "r^=" == "r Un Id"
1558
9c6ebfab4e05 added constdefs section
clasohm
parents: 1475
diff changeset
    30
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
    31
end