src/HOL/Trancl.thy

added rev_contrapos

(*  Title: 	HOL/Trancl.thy
    ID:         $Id$
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

Relfexive and Transitive closure of a relation

rtrancl is refl&transitive closure;
trancl is transitive closure
reflcl is reflexive closure
*)

Trancl = Lfp + Relation + 
consts
    rtrancl :: "('a * 'a)set => ('a * 'a)set"	("(_^*)" [100] 100)
    trancl  :: "('a * 'a)set => ('a * 'a)set"	("(_^+)" [100] 100)  
syntax
    reflcl  :: "('a*'a)set => ('a*'a)set"       ("(_^=)" [100] 100)
defs   
  rtrancl_def	"r^*  ==  lfp(%s. id Un (r O s))"
  trancl_def	"r^+  ==  r O rtrancl(r)"
translations
                "r^=" == "r Un id"
end