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
```