--- a/src/HOL/Lambda/Commutation.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Commutation.thy Thu Feb 16 21:12:00 2006 +0100
@@ -10,25 +10,24 @@
subsection {* Basic definitions *}
-constdefs
+definition
square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
- "square R S T U ==
- \<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U))"
+ "square R S T U =
+ (\<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U)))"
commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
- "commute R S == square R S S R"
+ "commute R S = square R S S R"
diamond :: "('a \<times> 'a) set => bool"
- "diamond R == commute R R"
+ "diamond R = commute R R"
Church_Rosser :: "('a \<times> 'a) set => bool"
- "Church_Rosser R ==
- \<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)"
+ "Church_Rosser R =
+ (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
-syntax
+abbreviation (output)
confluent :: "('a \<times> 'a) set => bool"
-translations
- "confluent R" == "diamond (R^*)"
+ "confluent R = diamond (R^*)"
subsection {* Basic lemmas *}