nipkow@1363: goal thy
nipkow@1363: "{x=X} \
nipkow@1363: \ y := []; \
nipkow@1363: \ WHILE x ~= [] \
nipkow@1363: \ DO { rev(x)@y = rev(X)} \
nipkow@1363: \    y := hd x # y; x := tl x \
nipkow@1363: \ END \
nipkow@1363: \{y=rev(X)}";
paulson@2031: by (hoare_tac 1);
paulson@2031: by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
paulson@2031: by (safe_tac (!claset));
paulson@2031: by (Asm_full_simp_tac 1);
paulson@2031: by (Asm_full_simp_tac 1);
nipkow@1363: qed "imperative_reverse";
nipkow@1363: 
nipkow@1363: goal thy
nipkow@1363: "{x=X & y = Y} \
nipkow@1363: \ x := rev(x); \
nipkow@1363: \ WHILE x ~= [] \
nipkow@1363: \ DO { rev(x)@y = X@Y} \
nipkow@1363: \    y := hd x # y; x := tl x \
nipkow@1363: \ END \
nipkow@1363: \{y = X@Y}";
paulson@2031: by (hoare_tac 1);
paulson@2031: by (asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
paulson@2031: by (safe_tac (!claset));
paulson@2031: by (Asm_full_simp_tac 1);
paulson@2031: by (Asm_full_simp_tac 1);
nipkow@1363: qed "imperative_append";