equal
deleted
inserted
replaced
|
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"; |