nipkow@10213: (*  Title:      HOL/Transitive_Closure.thy
nipkow@10213:     ID:         $Id$
nipkow@10213:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
nipkow@10213:     Copyright   1992  University of Cambridge
nipkow@10213: 
nipkow@10213: Relfexive and Transitive closure of a relation
nipkow@10213: 
nipkow@10213: rtrancl is reflexive/transitive closure;
nipkow@10213: trancl  is transitive closure
nipkow@10213: reflcl  is reflexive closure
nipkow@10213: 
nipkow@10213: These postfix operators have MAXIMUM PRIORITY, forcing their operands to be
nipkow@10213:       atomic.
nipkow@10213: *)
nipkow@10213: 
nipkow@10213: Transitive_Closure = Lfp + Relation + 
nipkow@10213: 
nipkow@10213: constdefs
nipkow@10213:   rtrancl :: "('a * 'a)set => ('a * 'a)set"   ("(_^*)" [1000] 999)
nipkow@10213:   "r^*  ==  lfp(%s. Id Un (r O s))"
nipkow@10213: 
nipkow@10213:   trancl  :: "('a * 'a)set => ('a * 'a)set"   ("(_^+)" [1000] 999)
nipkow@10213:   "r^+  ==  r O rtrancl(r)"
nipkow@10213: 
nipkow@10213: syntax
nipkow@10213:   "_reflcl"  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [1000] 999)
nipkow@10213: 
nipkow@10213: translations
nipkow@10213:   "r^=" == "r Un Id"
nipkow@10213: 
nipkow@10213: end