src/HOL/IMP/Com.thy
changeset 1481 03f096efa26d
parent 1476 608483c2122a
child 1696 e84bff5c519b
     1.1 --- a/src/HOL/IMP/Com.thy	Tue Feb 06 12:44:31 1996 +0100
     1.2 +++ b/src/HOL/IMP/Com.thy	Wed Feb 07 12:22:32 1996 +0100
     1.3 @@ -71,11 +71,11 @@
     1.4  (** Commands **)
     1.5  
     1.6  datatype
     1.7 -  com = skip
     1.8 -      | ":="   loc aexp          (infixl  60)
     1.9 -      | semic  com com           ("_; _"  [60, 60] 10)
    1.10 -      | whileC bexp com          ("while _ do _"  60)
    1.11 -      | ifC    bexp com com      ("ifc _ then _ else _"  60)
    1.12 +  com = Skip
    1.13 +      | ":="  loc aexp         (infixl  60)
    1.14 +      | Semi  com com          ("_; _"  [60, 60] 10)
    1.15 +      | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
    1.16 +      | While bexp com         ("WHILE _ DO _"  60)
    1.17  
    1.18  (** Execution of commands **)
    1.19  consts  evalc    :: "(com*state*state)set"
    1.20 @@ -85,28 +85,28 @@
    1.21  translations
    1.22         "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
    1.23  
    1.24 -rules 
    1.25 -        assign_def      "s[m/x] == (%y. if y=x then m else s y)"
    1.26 +defs 
    1.27 +  assign_def   "s[m/x] == (%y. if y=x then m else s y)"
    1.28  
    1.29  inductive "evalc"
    1.30    intrs
    1.31 -    skip    "<skip,s> -c-> s"
    1.32 +    skip    "<Skip,s> -c-> s"
    1.33  
    1.34      assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
    1.35  
    1.36      semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
    1.37              ==> <c0 ; c1, s> -c-> s1"
    1.38  
    1.39 -    ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
    1.40 -            ==> <ifc b then c0 else c1, s> -c-> s1"
    1.41 +    IfTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
    1.42 +            ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
    1.43  
    1.44 -    ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
    1.45 -             ==> <ifc b then c0 else c1, s> -c-> s1"
    1.46 +    IfFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
    1.47 +             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
    1.48  
    1.49 -    whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
    1.50 +    WhileFalse "<b, s> -b-> False ==> <WHILE b DO c,s> -c-> s"
    1.51  
    1.52 -    whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
    1.53 -                  <while b do c, s2> -c-> s1 |] 
    1.54 -               ==> <while b do c, s> -c-> s1 "
    1.55 +    WhileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
    1.56 +                  <WHILE b DO c, s2> -c-> s1 |] 
    1.57 +               ==> <WHILE b DO c, s> -c-> s1"
    1.58   
    1.59  end