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