src/HOL/Lambda/Commutation.thy
 changeset 19086 1b3780be6cc2 parent 18513 791b53bf4073 child 19363 667b5ea637dd
```     1.1 --- a/src/HOL/Lambda/Commutation.thy	Thu Feb 16 21:11:58 2006 +0100
1.2 +++ b/src/HOL/Lambda/Commutation.thy	Thu Feb 16 21:12:00 2006 +0100
1.3 @@ -10,25 +10,24 @@
1.4
1.5  subsection {* Basic definitions *}
1.6
1.7 -constdefs
1.8 +definition
1.9    square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
1.10 -  "square R S T U ==
1.11 -    \<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.12 +  "square R S T U =
1.13 +    (\<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.14
1.15    commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
1.16 -  "commute R S == square R S S R"
1.17 +  "commute R S = square R S S R"
1.18
1.19    diamond :: "('a \<times> 'a) set => bool"
1.20 -  "diamond R == commute R R"
1.21 +  "diamond R = commute R R"
1.22
1.23    Church_Rosser :: "('a \<times> 'a) set => bool"
1.24 -  "Church_Rosser R ==
1.25 -    \<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)"
1.26 +  "Church_Rosser R =
1.27 +    (\<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*))"
1.28
1.29 -syntax
1.30 +abbreviation (output)
1.31    confluent :: "('a \<times> 'a) set => bool"
1.32 -translations
1.33 -  "confluent R" == "diamond (R^*)"
1.34 +  "confluent R = diamond (R^*)"
1.35
1.36
1.37  subsection {* Basic lemmas *}
```