66 and aval'_const is aval' |
66 and aval'_const is aval' |
67 proof qed (auto simp: iter'_pfp_above) |
67 proof qed (auto simp: iter'_pfp_above) |
68 |
68 |
69 text{* Straight line code: *} |
69 text{* Straight line code: *} |
70 definition "test1_const = |
70 definition "test1_const = |
71 ''y'' ::= N 7; |
71 ''y'' ::= N 7;; |
72 ''z'' ::= Plus (V ''y'') (N 2); |
72 ''z'' ::= Plus (V ''y'') (N 2);; |
73 ''y'' ::= Plus (V ''x'') (N 0)" |
73 ''y'' ::= Plus (V ''x'') (N 0)" |
74 |
74 |
75 text{* Conditional: *} |
75 text{* Conditional: *} |
76 definition "test2_const = |
76 definition "test2_const = |
77 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5" |
77 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5" |
78 |
78 |
79 text{* Conditional, test is ignored: *} |
79 text{* Conditional, test is ignored: *} |
80 definition "test3_const = |
80 definition "test3_const = |
81 ''x'' ::= N 42; |
81 ''x'' ::= N 42;; |
82 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6" |
82 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6" |
83 |
83 |
84 text{* While: *} |
84 text{* While: *} |
85 definition "test4_const = |
85 definition "test4_const = |
86 ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0" |
86 ''x'' ::= N 0;; WHILE Bc True DO ''x'' ::= N 0" |
87 |
87 |
88 text{* While, test is ignored: *} |
88 text{* While, test is ignored: *} |
89 definition "test5_const = |
89 definition "test5_const = |
90 ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1" |
90 ''x'' ::= N 0;; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1" |
91 |
91 |
92 text{* Iteration is needed: *} |
92 text{* Iteration is needed: *} |
93 definition "test6_const = |
93 definition "test6_const = |
94 ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2; |
94 ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 2;; |
95 WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')" |
95 WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'')" |
96 |
96 |
97 text{* More iteration would be needed: *} |
97 text{* More iteration would be needed: *} |
98 definition "test7_const = |
98 definition "test7_const = |
99 ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3; |
99 ''x'' ::= N 0;; ''y'' ::= N 0;; ''z'' ::= N 0;; ''u'' ::= N 3;; |
100 WHILE Less (V ''x'') (N 1) |
100 WHILE Less (V ''x'') (N 1) |
101 DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')" |
101 DO (''x'' ::= V ''y'';; ''y'' ::= V ''z'';; ''z'' ::= V ''u'')" |
102 |
102 |
103 value [code] "list (AI_const test1_const Top)" |
103 value [code] "list (AI_const test1_const Top)" |
104 value [code] "list (AI_const test2_const Top)" |
104 value [code] "list (AI_const test2_const Top)" |
105 value [code] "list (AI_const test3_const Top)" |
105 value [code] "list (AI_const test3_const Top)" |
106 value [code] "list (AI_const test4_const Top)" |
106 value [code] "list (AI_const test4_const Top)" |