src/HOL/Lambda/Commutation.thy
author nipkow
Wed Oct 11 10:09:56 1995 +0100 (1995-10-11)
changeset 1278 7e6189fc833c
child 1302 ddfdcc9ce667
permissions -rw-r--r--
Commutation replaces Confluence
     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   reflcl  :: "('a*'a)set => ('a*'a)set"               ("(_^=)" [100] 100)
    13   square  :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"
    14   commute :: "[('a*'a)set,('a*'a)set] => bool"
    15   confluent, diamond, Church_Rosser :: "('a*'a)set => bool"
    16 
    17 defs
    18   square_def
    19  "square R S T U == !x y.(x,y):R --> (!z.(x,z):S --> (? u. (y,u):T & (z,u):U))"
    20 
    21   commute_def "commute R S == square R S S R"
    22   diamond_def "diamond R   == commute R R"
    23 
    24   Church_Rosser_def "Church_Rosser(R) ==   
    25   !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
    26 
    27 translations
    28   "r^="   == "r Un id"
    29   "confluent R" == "diamond(R^*)"
    30 
    31 end