src/HOL/Lambda/Commutation.thy
changeset 21404 eb85850d3eb7
parent 19363 667b5ea637dd
child 21669 c68717c16013
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -11,22 +11,25 @@
     1.4  subsection {* Basic definitions *}
     1.5  
     1.6  definition
     1.7 -  square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
     1.8 +  square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
     1.9    "square R S T U =
    1.10      (\<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U)))"
    1.11  
    1.12 -  commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
    1.13 +definition
    1.14 +  commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool" where
    1.15    "commute R S = square R S S R"
    1.16  
    1.17 -  diamond :: "('a \<times> 'a) set => bool"
    1.18 +definition
    1.19 +  diamond :: "('a \<times> 'a) set => bool" where
    1.20    "diamond R = commute R R"
    1.21  
    1.22 -  Church_Rosser :: "('a \<times> 'a) set => bool"
    1.23 +definition
    1.24 +  Church_Rosser :: "('a \<times> 'a) set => bool" where
    1.25    "Church_Rosser R =
    1.26      (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
    1.27  
    1.28  abbreviation
    1.29 -  confluent :: "('a \<times> 'a) set => bool"
    1.30 +  confluent :: "('a \<times> 'a) set => bool" where
    1.31    "confluent R == diamond (R^*)"
    1.32  
    1.33