32 inductive "evala" |
32 inductive "evala" |
33 intrs |
33 intrs |
34 N "<N(n),s> -a-> n" |
34 N "<N(n),s> -a-> n" |
35 X "<X(x),s> -a-> s(x)" |
35 X "<X(x),s> -a-> s(x)" |
36 Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)" |
36 Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)" |
37 Op2 "[| <e0,s> -a-> n0; <e1,s> -a-> n1 |] \ |
37 Op2 "[| <e0,s> -a-> n0; <e1,s> -a-> n1 |] |
38 \ ==> <Op2 f e0 e1,s> -a-> f n0 n1" |
38 ==> <Op2 f e0 e1,s> -a-> f n0 n1" |
39 |
39 |
40 types n2n2b = "[nat,nat] => bool" |
40 types n2n2b = "[nat,nat] => bool" |
41 |
41 |
42 (** Boolean expressions **) |
42 (** Boolean expressions **) |
43 |
43 |
58 |
58 |
59 inductive "evalb" |
59 inductive "evalb" |
60 intrs (*avoid clash with ML constructors true, false*) |
60 intrs (*avoid clash with ML constructors true, false*) |
61 tru "<true,s> -b-> True" |
61 tru "<true,s> -b-> True" |
62 fls "<false,s> -b-> False" |
62 fls "<false,s> -b-> False" |
63 ROp "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \ |
63 ROp "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] |
64 \ ==> <ROp f a0 a1,s> -b-> f n0 n1" |
64 ==> <ROp f a0 a1,s> -b-> f n0 n1" |
65 noti "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)" |
65 noti "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)" |
66 andi "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \ |
66 andi "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] |
67 \ ==> <b0 andi b1,s> -b-> (w0 & w1)" |
67 ==> <b0 andi b1,s> -b-> (w0 & w1)" |
68 ori "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \ |
68 ori "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] |
69 \ ==> <b0 ori b1,s> -b-> (w0 | w1)" |
69 ==> <b0 ori b1,s> -b-> (w0 | w1)" |
70 |
70 |
71 (** Commands **) |
71 (** Commands **) |
72 |
72 |
73 datatype |
73 datatype |
74 com = skip |
74 com = skip |
92 intrs |
92 intrs |
93 skip "<skip,s> -c-> s" |
93 skip "<skip,s> -c-> s" |
94 |
94 |
95 assign "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]" |
95 assign "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]" |
96 |
96 |
97 semi "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \ |
97 semi "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] |
98 \ ==> <c0 ; c1, s> -c-> s1" |
98 ==> <c0 ; c1, s> -c-> s1" |
99 |
99 |
100 ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \ |
100 ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] |
101 \ ==> <ifc b then c0 else c1, s> -c-> s1" |
101 ==> <ifc b then c0 else c1, s> -c-> s1" |
102 |
102 |
103 ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \ |
103 ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] |
104 \ ==> <ifc b then c0 else c1, s> -c-> s1" |
104 ==> <ifc b then c0 else c1, s> -c-> s1" |
105 |
105 |
106 whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s" |
106 whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s" |
107 |
107 |
108 whileTrue "[| <b,s> -b-> True; <c,s> -c-> s2; \ |
108 whileTrue "[| <b,s> -b-> True; <c,s> -c-> s2; |
109 \ <while b do c, s2> -c-> s1 |] \ |
109 <while b do c, s2> -c-> s1 |] |
110 \ ==> <while b do c, s> -c-> s1 " |
110 ==> <while b do c, s> -c-> s1 " |
111 |
111 |
112 end |
112 end |