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
clasohm@1476
     1
(*  Title:      HOL/Lambda/Commutation.thy
nipkow@1278
     2
    ID:         $Id$
clasohm@1476
     3
    Author:     Tobias Nipkow
nipkow@1278
     4
    Copyright   1995  TU Muenchen
nipkow@1278
     5
nipkow@1278
     6
Abstract commutation and confluence notions.
nipkow@1278
     7
*)
nipkow@1278
     8
nipkow@1278
     9
Commutation = Trancl +
nipkow@1278
    10
nipkow@1278
    11
consts
nipkow@1278
    12
  square  :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"
nipkow@1278
    13
  commute :: "[('a*'a)set,('a*'a)set] => bool"
nipkow@1278
    14
  confluent, diamond, Church_Rosser :: "('a*'a)set => bool"
nipkow@1278
    15
nipkow@1278
    16
defs
nipkow@1278
    17
  square_def
nipkow@1278
    18
 "square R S T U == !x y.(x,y):R --> (!z.(x,z):S --> (? u. (y,u):T & (z,u):U))"
nipkow@1278
    19
nipkow@1278
    20
  commute_def "commute R S == square R S S R"
nipkow@1278
    21
  diamond_def "diamond R   == commute R R"
nipkow@1278
    22
nipkow@1278
    23
  Church_Rosser_def "Church_Rosser(R) ==   
nipkow@1278
    24
  !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
nipkow@1278
    25
nipkow@1278
    26
translations
nipkow@1278
    27
  "confluent R" == "diamond(R^*)"
nipkow@1278
    28
nipkow@1278
    29
end