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 *}