diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Lambda/Commutation.thy --- a/src/HOL/Lambda/Commutation.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Lambda/Commutation.thy Fri Nov 17 02:20:03 2006 +0100 @@ -11,22 +11,25 @@ subsection {* Basic definitions *} definition - square :: "[('a \ 'a) set, ('a \ 'a) set, ('a \ 'a) set, ('a \ 'a) set] => bool" + square :: "[('a \ 'a) set, ('a \ 'a) set, ('a \ 'a) set, ('a \ 'a) set] => bool" where "square R S T U = (\x y. (x, y) \ R --> (\z. (x, z) \ S --> (\u. (y, u) \ T \ (z, u) \ U)))" - commute :: "[('a \ 'a) set, ('a \ 'a) set] => bool" +definition + commute :: "[('a \ 'a) set, ('a \ 'a) set] => bool" where "commute R S = square R S S R" - diamond :: "('a \ 'a) set => bool" +definition + diamond :: "('a \ 'a) set => bool" where "diamond R = commute R R" - Church_Rosser :: "('a \ 'a) set => bool" +definition + Church_Rosser :: "('a \ 'a) set => bool" where "Church_Rosser R = (\x y. (x, y) \ (R \ R^-1)^* --> (\z. (x, z) \ R^* \ (y, z) \ R^*))" abbreviation - confluent :: "('a \ 'a) set => bool" + confluent :: "('a \ 'a) set => bool" where "confluent R == diamond (R^*)"