|
1363
|
1 |
goal thy
|
|
|
2 |
"{x=X} \
|
|
|
3 |
\ y := []; \
|
|
|
4 |
\ WHILE x ~= [] \
|
|
|
5 |
\ DO { rev(x)@y = rev(X)} \
|
|
|
6 |
\ y := hd x # y; x := tl x \
|
|
|
7 |
\ END \
|
|
|
8 |
\{y=rev(X)}";
|
|
|
9 |
by(hoare_tac 1);
|
|
|
10 |
by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
|
|
|
11 |
by(safe_tac HOL_cs);
|
|
|
12 |
by(Asm_full_simp_tac 1);
|
|
|
13 |
by(Asm_full_simp_tac 1);
|
|
|
14 |
qed "imperative_reverse";
|
|
|
15 |
|
|
|
16 |
goal thy
|
|
|
17 |
"{x=X & y = Y} \
|
|
|
18 |
\ x := rev(x); \
|
|
|
19 |
\ WHILE x ~= [] \
|
|
|
20 |
\ DO { rev(x)@y = X@Y} \
|
|
|
21 |
\ y := hd x # y; x := tl x \
|
|
|
22 |
\ END \
|
|
|
23 |
\{y = X@Y}";
|
|
|
24 |
by(hoare_tac 1);
|
|
|
25 |
by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
|
|
|
26 |
by(safe_tac HOL_cs);
|
|
|
27 |
by(Asm_full_simp_tac 1);
|
|
|
28 |
by(Asm_full_simp_tac 1);
|
|
|
29 |
qed "imperative_append";
|