110 G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2" |
110 G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2" |
111 |
111 |
112 (* execution of statements *) |
112 (* execution of statements *) |
113 |
113 |
114 (* cf. 14.1 *) |
114 (* cf. 14.1 *) |
115 XcptS "G\\<turnstile>(Some xc,s) -s0-> (Some xc,s)" |
115 XcptS "G\\<turnstile>(Some xc,s) -c-> (Some xc,s)" |
116 |
116 |
117 (* cf. 14.5 *) |
117 (* cf. 14.5 *) |
118 Skip "G\\<turnstile>Norm s -Skip-> Norm s" |
118 Skip "G\\<turnstile>Norm s -Skip-> Norm s" |
119 |
119 |
120 (* cf. 14.7 *) |
120 (* cf. 14.7 *) |
121 Expr "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1 |] ==> |
121 Expr "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1 |] ==> |
122 G\\<turnstile>Norm s0 -Expr e-> s1" |
122 G\\<turnstile>Norm s0 -Expr e-> s1" |
123 |
123 |
124 (* cf. 14.2 *) |
124 (* cf. 14.2 *) |
125 Comp "[| G\\<turnstile>Norm s0 -s-> s1; |
125 Comp "[| G\\<turnstile>Norm s0 -c1-> s1; |
126 G\\<turnstile> s1 -t -> s2|] ==> |
126 G\\<turnstile> s1 -c2-> s2|] ==> |
127 G\\<turnstile>Norm s0 -s;; t-> s2" |
127 G\\<turnstile>Norm s0 -c1;; c2-> s2" |
128 |
128 |
129 (* cf. 14.8.2 *) |
129 (* cf. 14.8.2 *) |
130 Cond "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; |
130 Cond "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; |
131 G\\<turnstile> s1 -(if the_Bool v then s else t)-> s2|] ==> |
131 G\\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==> |
132 G\\<turnstile>Norm s0 -If(e) s Else t-> s2" |
132 G\\<turnstile>Norm s0 -If(e) c1 Else c2-> s2" |
133 |
133 |
134 (* cf. 14.10, 14.10.1 *) |
134 (* cf. 14.10, 14.10.1 *) |
135 Loop "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; |
135 LoopF "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; \\<not>the_Bool v |] ==> |
136 if the_Bool v then G\\<turnstile>s1 -s-> s2 \\<and> G\\<turnstile>s2 -While(e) s-> s3 |
136 G\\<turnstile>Norm s0 -While(e) c-> s1" |
137 else s3 = s1 |] ==> |
137 LoopT "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; the_Bool v; |
138 G\\<turnstile>Norm s0 -While(e) s-> s3" |
138 G\\<turnstile>s1 -c-> s2; G\\<turnstile>s2 -While(e) c-> s3 |] ==> |
|
139 G\\<turnstile>Norm s0 -While(e) c-> s3" |
139 |
140 |
140 monos |
141 monos |
141 if_def2 |
142 if_def2 |
142 |
143 |
143 end |
144 end |