src/ZF/ex/Commutation.thy
author paulson
Sat Feb 03 12:41:38 2001 +0100 (2001-02-03)
changeset 11042 bb566dd3f927
child 11316 b4e71bd751e4
permissions -rw-r--r--
commutation theory, ported by Sidi Ehmety
     1 (*  Title:      HOL/Lambda/Commutation.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Sidi Ould Ehmety
     4     Copyright   1995  TU Muenchen
     5 
     6 Commutation theory for proving the Church Rosser theorem
     7 	ported from Isabelle/HOL  by Sidi Ould Ehmety
     8 *)
     9 
    10 Commutation = Main +    
    11 
    12 constdefs
    13   square  :: [i, i, i, i] => o
    14    "square(r,s,t,u) ==
    15    (ALL a b. <a,b>:r --> (ALL c. <a, c>:s
    16                           --> (EX x. <b,x>:t & <c,x>:u)))"
    17 
    18    commute :: [i, i] => o       
    19    "commute(r,s) == square(r,s,s,r)"
    20 
    21   diamond :: i=>o
    22   "diamond(r)   == commute(r, r)"
    23 
    24   strip :: i=>o  
    25   "strip(r) == commute(r^*, r)"
    26 
    27   Church_Rosser :: i => o     
    28   "Church_Rosser(r) == (ALL x y. <x,y>: (r Un converse(r))^* -->
    29 			(EX z. <x,z>:r^* & <y,z>:r^*))"
    30   confluent :: i=>o    
    31   "confluent(r) == diamond(r^*)"
    32 end