src/HOL/Induct/Comb.thy
changeset 19736 d8d0f8f51d69
parent 16588 8de758143786
child 21210 c17fd2df4e9e
--- a/src/HOL/Induct/Comb.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Comb.thy	Sat May 27 17:42:02 2006 +0200
@@ -23,7 +23,11 @@
 
 datatype comb = K
               | S
-              | "##" comb comb (infixl 90)
+              | Ap comb comb (infixl "##" 90)
+
+const_syntax (xsymbols)
+  Ap  (infixl "\<bullet>" 90)
+
 
 text {*
   Inductive definition of contractions, @{text "-1->"} and
@@ -32,15 +36,12 @@
 
 consts
   contract  :: "(comb*comb) set"
-  "-1->"    :: "[comb,comb] => bool"   (infixl 50)
-  "--->"    :: "[comb,comb] => bool"   (infixl 50)
 
-translations
-  "x -1-> y" == "(x,y) \<in> contract"
-  "x ---> y" == "(x,y) \<in> contract^*"
-
-syntax (xsymbols)
-  "op ##" :: "[comb,comb] => comb"  (infixl "\<bullet>" 90)
+abbreviation
+  contract_rel1 :: "[comb,comb] => bool"   (infixl "-1->" 50)
+  "x -1-> y == (x,y) \<in> contract"
+  contract_rel :: "[comb,comb] => bool"   (infixl "--->" 50)
+  "x ---> y == (x,y) \<in> contract^*"
 
 inductive contract
   intros
@@ -56,12 +57,12 @@
 
 consts
   parcontract :: "(comb*comb) set"
-  "=1=>"      :: "[comb,comb] => bool"   (infixl 50)
-  "===>"      :: "[comb,comb] => bool"   (infixl 50)
 
-translations
-  "x =1=> y" == "(x,y) \<in> parcontract"
-  "x ===> y" == "(x,y) \<in> parcontract^*"
+abbreviation
+  parcontract_rel1 :: "[comb,comb] => bool"   (infixl "=1=>" 50)
+  "x =1=> y == (x,y) \<in> parcontract"
+  parcontract_rel :: "[comb,comb] => bool"   (infixl "===>" 50)
+  "x ===> y == (x,y) \<in> parcontract^*"
 
 inductive parcontract
   intros
@@ -74,15 +75,15 @@
   Misc definitions.
 *}
 
-constdefs
+definition
   I :: comb
-  "I == S##K##K"
+  "I = S##K##K"
 
   diamond   :: "('a * 'a)set => bool"	
     --{*confluence; Lambda/Commutation treats this more abstractly*}
-  "diamond(r) == \<forall>x y. (x,y) \<in> r --> 
+  "diamond(r) = (\<forall>x y. (x,y) \<in> r --> 
                   (\<forall>y'. (x,y') \<in> r --> 
-                    (\<exists>z. (y,z) \<in> r & (y',z) \<in> r))"
+                    (\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))"
 
 
 subsection {*Reflexive/Transitive closure preserves Church-Rosser property*}