1 (* Title: HOL/IMP/Com.thy |
1 (* Title: HOL/IMP/Com.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
3 Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM |
4 Copyright 1994 TUM |
4 Copyright 1994 TUM |
5 |
5 |
6 Arithmetic expressions, Boolean expressions, Commands |
6 Semantics of arithmetic and boolean expressions |
7 |
7 Syntax of commands |
8 And their Operational semantics |
|
9 *) |
8 *) |
10 |
9 |
11 Com = Arith + |
10 Com = Arith + |
12 |
11 |
13 (** Arithmetic expressions **) |
12 types |
14 types loc |
13 val |
15 state = "loc => nat" |
14 loc |
16 n2n = "nat => nat" |
15 state = "loc => val" |
17 n2n2n = "nat => nat => nat" |
16 aexp = "state => val" |
|
17 bexp = state => bool |
18 |
18 |
19 arities loc :: term |
19 arities loc,val :: term |
20 |
20 |
21 datatype |
21 datatype |
22 aexp = N nat |
22 com = SKIP |
23 | X loc |
|
24 | Op1 n2n aexp |
|
25 | Op2 n2n2n aexp aexp |
|
26 |
|
27 (** Evaluation of arithmetic expressions **) |
|
28 consts evala :: "(aexp*state*nat)set" |
|
29 "@evala" :: [aexp,state,nat] => bool ("<_,_>/ -a-> _" [0,0,50] 50) |
|
30 translations |
|
31 "<ae,sig> -a-> n" == "(ae,sig,n) : evala" |
|
32 inductive "evala" |
|
33 intrs |
|
34 N "<N(n),s> -a-> n" |
|
35 X "<X(x),s> -a-> s(x)" |
|
36 Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)" |
|
37 Op2 "[| <e0,s> -a-> n0; <e1,s> -a-> n1 |] |
|
38 ==> <Op2 f e0 e1,s> -a-> f n0 n1" |
|
39 |
|
40 types n2n2b = "[nat,nat] => bool" |
|
41 |
|
42 (** Boolean expressions **) |
|
43 |
|
44 datatype |
|
45 bexp = true |
|
46 | false |
|
47 | ROp n2n2b aexp aexp |
|
48 | noti bexp |
|
49 | andi bexp bexp (infixl 60) |
|
50 | ori bexp bexp (infixl 60) |
|
51 |
|
52 (** Evaluation of boolean expressions **) |
|
53 consts evalb :: "(bexp*state*bool)set" |
|
54 "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _" [0,0,50] 50) |
|
55 |
|
56 translations |
|
57 "<be,sig> -b-> b" == "(be,sig,b) : evalb" |
|
58 |
|
59 inductive "evalb" |
|
60 intrs (*avoid clash with ML constructors true, false*) |
|
61 tru "<true,s> -b-> True" |
|
62 fls "<false,s> -b-> False" |
|
63 ROp "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] |
|
64 ==> <ROp f a0 a1,s> -b-> f n0 n1" |
|
65 noti "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)" |
|
66 andi "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] |
|
67 ==> <b0 andi b1,s> -b-> (w0 & w1)" |
|
68 ori "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] |
|
69 ==> <b0 ori b1,s> -b-> (w0 | w1)" |
|
70 |
|
71 (** Commands **) |
|
72 |
|
73 datatype |
|
74 com = Skip |
|
75 | ":=" loc aexp (infixl 60) |
23 | ":=" loc aexp (infixl 60) |
76 | Semi com com ("_; _" [60, 60] 10) |
24 | Semi com com ("_; _" [60, 60] 10) |
77 | Cond bexp com com ("IF _ THEN _ ELSE _" 60) |
25 | Cond bexp com com ("IF _ THEN _ ELSE _" 60) |
78 | While bexp com ("WHILE _ DO _" 60) |
26 | While bexp com ("WHILE _ DO _" 60) |
79 |
27 |
80 (** Execution of commands **) |
|
81 consts evalc :: "(com*state*state)set" |
|
82 "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50) |
|
83 "assign" :: [state,nat,loc] => state ("_[_'/_]" [95,0,0] 95) |
|
84 |
|
85 translations |
|
86 "<ce,sig> -c-> s" == "(ce,sig,s) : evalc" |
|
87 |
|
88 defs |
|
89 assign_def "s[m/x] == (%y. if y=x then m else s y)" |
|
90 |
|
91 inductive "evalc" |
|
92 intrs |
|
93 skip "<Skip,s> -c-> s" |
|
94 |
|
95 assign "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]" |
|
96 |
|
97 semi "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] |
|
98 ==> <c0 ; c1, s> -c-> s1" |
|
99 |
|
100 IfTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] |
|
101 ==> <IF b THEN c0 ELSE c1, s> -c-> s1" |
|
102 |
|
103 IfFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] |
|
104 ==> <IF b THEN c0 ELSE c1, s> -c-> s1" |
|
105 |
|
106 WhileFalse "<b, s> -b-> False ==> <WHILE b DO c,s> -c-> s" |
|
107 |
|
108 WhileTrue "[| <b,s> -b-> True; <c,s> -c-> s2; |
|
109 <WHILE b DO c, s2> -c-> s1 |] |
|
110 ==> <WHILE b DO c, s> -c-> s1" |
|
111 |
|
112 end |
28 end |