src/HOL/Transitive_Closure.thy
author wenzelm
Fri, 26 Jan 2001 00:15:36 +0100
changeset 10980 0a45f2efaaec
parent 10827 a7ac8e1e024b
child 10996 74e970389def
permissions -rw-r--r--
Transitive_Closure turned into new-style theory;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Transitive_Closure.thy
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     5
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     6
Relfexive and Transitive closure of a relation
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     7
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     8
rtrancl is reflexive/transitive closure;
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
     9
trancl  is transitive closure
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    10
reflcl  is reflexive closure
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    11
10331
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    12
These postfix operators have MAXIMUM PRIORITY, forcing their operands
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    13
to be atomic.
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    14
*)
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    15
10980
0a45f2efaaec Transitive_Closure turned into new-style theory;
wenzelm
parents: 10827
diff changeset
    16
theory Transitive_Closure = Lfp + Relation
0a45f2efaaec Transitive_Closure turned into new-style theory;
wenzelm
parents: 10827
diff changeset
    17
files ("Transitive_Closure_lemmas.ML"):
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    18
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    19
constdefs
10331
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    20
  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    21
  "r^* == lfp (%s. Id Un (r O s))"
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    22
10331
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    23
  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    24
  "r^+ ==  r O rtrancl r"
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    25
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    26
syntax
10331
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    27
  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    28
translations
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    29
  "r^=" == "r Un Id"
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    30
10827
a7ac8e1e024b syntax (xsymbols);
wenzelm
parents: 10565
diff changeset
    31
syntax (xsymbols)
10331
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    32
  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    33
  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    34
  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
7411e4659d4a more "xsymbols" syntax;
wenzelm
parents: 10213
diff changeset
    35
10980
0a45f2efaaec Transitive_Closure turned into new-style theory;
wenzelm
parents: 10827
diff changeset
    36
use "Transitive_Closure_lemmas.ML"
0a45f2efaaec Transitive_Closure turned into new-style theory;
wenzelm
parents: 10827
diff changeset
    37
10213
01c2744a3786 *** empty log message ***
nipkow
parents:
diff changeset
    38
end