src/HOL/Induct/Comb.thy
 changeset 23746 a455e69c31cc parent 21404 eb85850d3eb7 child 35621 1c084dda4c3c
--- a/src/HOL/Induct/Comb.thy	Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/Induct/Comb.thy	Wed Jul 11 11:14:51 2007 +0200
@@ -34,47 +34,39 @@
(multi-step) reductions, @{text "--->"}.
*}

-consts
-  contract  :: "(comb*comb) set"
-
-abbreviation
-  contract_rel1 :: "[comb,comb] => bool"   (infixl "-1->" 50) where
-  "x -1-> y == (x,y) \<in> contract"
+inductive_set
+  contract :: "(comb*comb) set"
+  and contract_rel1 :: "[comb,comb] => bool"  (infixl "-1->" 50)
+  where
+    "x -1-> y == (x,y) \<in> contract"
+   | K:     "K##x##y -1-> x"
+   | S:     "S##x##y##z -1-> (x##z)##(y##z)"
+   | Ap1:   "x-1->y ==> x##z -1-> y##z"
+   | Ap2:   "x-1->y ==> z##x -1-> z##y"

abbreviation
contract_rel :: "[comb,comb] => bool"   (infixl "--->" 50) where
"x ---> y == (x,y) \<in> contract^*"

-inductive contract
-  intros
-    K:     "K##x##y -1-> x"
-    S:     "S##x##y##z -1-> (x##z)##(y##z)"
-    Ap1:   "x-1->y ==> x##z -1-> y##z"
-    Ap2:   "x-1->y ==> z##x -1-> z##y"
-
text {*
Inductive definition of parallel contractions, @{text "=1=>"} and
(multi-step) parallel reductions, @{text "===>"}.
*}

-consts
+inductive_set
parcontract :: "(comb*comb) set"
-
-abbreviation
-  parcontract_rel1 :: "[comb,comb] => bool"   (infixl "=1=>" 50) where
-  "x =1=> y == (x,y) \<in> parcontract"
+  and parcontract_rel1 :: "[comb,comb] => bool"  (infixl "=1=>" 50)
+  where
+    "x =1=> y == (x,y) \<in> parcontract"
+  | refl:  "x =1=> x"
+  | K:     "K##x##y =1=> x"
+  | S:     "S##x##y##z =1=> (x##z)##(y##z)"
+  | Ap:    "[| x=1=>y;  z=1=>w |] ==> x##z =1=> y##w"

abbreviation
parcontract_rel :: "[comb,comb] => bool"   (infixl "===>" 50) where
"x ===> y == (x,y) \<in> parcontract^*"

-inductive parcontract
-  intros
-    refl:  "x =1=> x"
-    K:     "K##x##y =1=> x"
-    S:     "S##x##y##z =1=> (x##z)##(y##z)"
-    Ap:    "[| x=1=>y;  z=1=>w |] ==> x##z =1=> y##w"
-
text {*
Misc definitions.
*}