src/HOL/Hoare/List_Examples.ML
author wenzelm
Thu, 20 Mar 1997 10:47:18 +0100
changeset 2816 647d557e9a40
parent 2031 03a843f0f447
child 4089 96fba19bcbe2
permissions -rw-r--r--
replaced ex.ML by ex/ROOT.ml, ex/ex.ML;

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

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