src/HOL/Lambda/Commutation.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1476 608483c2122a
child 3439 54785105178c
permissions -rw-r--r--
Dep. on Provers/nat_transitive
     1 (*  Title:      HOL/Lambda/Commutation.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1995  TU Muenchen
     5 
     6 Abstract commutation and confluence notions.
     7 *)
     8 
     9 Commutation = Trancl +
    10 
    11 consts
    12   square  :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"
    13   commute :: "[('a*'a)set,('a*'a)set] => bool"
    14   confluent, diamond, Church_Rosser :: "('a*'a)set => bool"
    15 
    16 defs
    17   square_def
    18  "square R S T U == !x y.(x,y):R --> (!z.(x,z):S --> (? u. (y,u):T & (z,u):U))"
    19 
    20   commute_def "commute R S == square R S S R"
    21   diamond_def "diamond R   == commute R R"
    22 
    23   Church_Rosser_def "Church_Rosser(R) ==   
    24   !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
    25 
    26 translations
    27   "confluent R" == "diamond(R^*)"
    28 
    29 end