--- a/src/HOL/IMP/Transition.thy Fri May 08 13:54:45 1998 +0200
+++ b/src/HOL/IMP/Transition.thy Fri May 08 15:45:01 1998 +0200
@@ -8,25 +8,32 @@
Transition = Natural + RelPow +
-consts evalc1 :: "((com*state)*(com*state))set"
- "@evalc1" :: "[(com*state),(com*state)] => bool"
- ("_ -1-> _" [81,81] 100)
- "@evalcn" :: "[(com*state),(com*state)] => nat => bool"
- ("_ -_-> _" [81,81] 100)
- "@evalc*" :: "[(com*state),(com*state)] => bool"
- ("_ -*-> _" [81,81] 100)
+consts evalc1 :: "((com*state)*(com*state))set"
+
+syntax
+ "@evalc1" :: "[(com*state),(com*state)] => bool"
+ ("_ -1-> _" [81,81] 100)
+ "@evalcn" :: "[(com*state),(com*state)] => nat => bool"
+ ("_ -_-> _" [81,81] 100)
+ "@evalc*" :: "[(com*state),(com*state)] => bool"
+ ("_ -*-> _" [81,81] 100)
translations
- "cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
- "cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
- "cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
+ "cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
+ "cs0 -1-> (c1,s1)" <= "cs0 -1-> (_args c1 s1)"
+
+ "cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
+ "cs0 -n-> (c1,s1)" <= "cs0 -n-> (_args c1 s1)"
+
+ "cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
+ "cs0 -*-> (c1,s1)" <= "cs0 -*-> (_args c1 s1)"
inductive evalc1
intrs
Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
- Semi1 "(SKIP;c,s) -1-> (c,s)"
+ Semi1 "(SKIP;c,s) -1-> (c,s)"
Semi2 "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"