src/HOL/Lambda/Confluence.thy

Put in direct proof of C-R w/o detour via cd.

(*  Title: 	HOL/Lambda/Confluence.thy
    ID:         $Id$
    Author: 	Tobias Nipkow
    Copyright   1995  TU Muenchen

Abstract confluence notions.
*)

Confluence = Trancl +

consts
  confluent, confluent1, confluent2, diamond, Church_Rosser ::
  "('a*'a)set => bool"

defs
  diamond_def
  "diamond(R) == !x y.(x,y):R --> (!z.(x,z):R --> (EX u. (y,u):R & (z,u):R))" 

  confluent_def "confluent(R) == diamond(R^*)"

  Church_Rosser_def "Church_Rosser(R) ==   
  !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
end