src/HOL/IMP/Com.thy
 author clasohm Fri, 24 Mar 1995 12:30:35 +0100 changeset 972 e61b058d58d2 parent 965 24eef3860714 child 977 5d57287e5e1e permissions -rw-r--r--
changed syntax of tuples from <..., ...> to (..., ...)
```
(*  Title: 	HOL/IMP/Com.thy
ID:         \$Id\$
Author: 	Heiko Loetzbeyer & Robert Sandner, TUM

Arithmetic expressions, Boolean expressions, Commands

And their Operational semantics
*)

Com = Arith +

(** Arithmetic expressions **)
types loc
state = "loc => nat"
n2n = "nat => nat"
n2n2n = "nat => nat => nat"

arities loc :: term

datatype
aexp = N (nat)
| X (loc)
| Op1 (n2n, aexp)
| Op2 (n2n2n, aexp, aexp)

(** Evaluation of arithmetic expressions **)
consts  evala    :: "(aexp*state*nat)set"
"@evala"  :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _"  [0,0,50] 50)
translations
"<ae,sig> -a-> n" == "(ae,sig,n) : evala"
inductive "evala"
intrs
N   "<N(n),s> -a-> n"
X  	"<X(x),s> -a-> s(x)"
Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] \
\           ==> <Op2 f e0 e1,s> -a-> f n0 n1"

types n2n2b = "[nat,nat] => bool"

(** Boolean expressions **)

datatype
bexp = true
| false
| ROp  (n2n2b, aexp, aexp)
| noti (bexp)
| andi (bexp,bexp)	(infixl 60)
| ori  (bexp,bexp)	(infixl 60)

(** Evaluation of boolean expressions **)
consts evalb	:: "(bexp*state*bool)set"
"@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _"  [0,0,50] 50)

translations
"<be,sig> -b-> b" == "(be,sig,b) : evalb"

inductive "evalb"
intrs (*avoid clash with ML constructors true, false*)
tru   "<true,s> -b-> True"
fls   "<false,s> -b-> False"
ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \
\	   ==> <ROp f a0 a1,s> -b-> f n0 n1"
noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
\          ==> <b0 andi b1,s> -b-> (w0 & w1)"
ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
\	    ==> <b0 ori b1,s> -b-> (w0 | w1)"

(** Commands **)

datatype
com = skip
| ":="   (loc,aexp)	 (infixl  60)
| semic  (com,com)	 ("_; _"  [60, 60] 10)
| whileC (bexp,com)	 ("while _ do _"  60)
| ifC    (bexp, com, com)	 ("ifc _ then _ else _"  60)

(** Execution of commands **)
consts  evalc    :: "(com*state*state)set"
"@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50)
"assign" :: "[state,nat,loc] => state"  ("_[_'/_]"       [95,0,0] 95)

translations
"<ce,sig> -c-> s" == "(ce,sig,s) : evalc"

rules
assign_def	"s[m/x] == (%y. if y=x then m else s y)"

inductive "evalc"
intrs
skip    "<skip,s> -c-> s"

assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"

semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \
\            ==> <c0 ; c1, s> -c-> s1"

ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \
\            ==> <ifc b then c0 else c1, s> -c-> s1"

ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \
\             ==> <ifc b then c0 else c1, s> -c-> s1"

whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"

whileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; \
\                  <while b do c, s2> -c-> s1 |] \
\               ==> <while b do c, s> -c-> s1 "

end
```