src/HOL/Hoare/List_Examples.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4724 3d2375efb80e
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
nipkow@1363
     1
goal thy
nipkow@1363
     2
"{x=X} \
nipkow@1363
     3
\ y := []; \
nipkow@1363
     4
\ WHILE x ~= [] \
nipkow@1363
     5
\ DO { rev(x)@y = rev(X)} \
nipkow@1363
     6
\    y := hd x # y; x := tl x \
nipkow@1363
     7
\ END \
nipkow@1363
     8
\{y=rev(X)}";
paulson@2031
     9
by (hoare_tac 1);
wenzelm@4089
    10
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
paulson@4153
    11
by Safe_tac;
paulson@2031
    12
by (Asm_full_simp_tac 1);
paulson@2031
    13
by (Asm_full_simp_tac 1);
nipkow@1363
    14
qed "imperative_reverse";
nipkow@1363
    15
nipkow@1363
    16
goal thy
nipkow@1363
    17
"{x=X & y = Y} \
nipkow@1363
    18
\ x := rev(x); \
nipkow@1363
    19
\ WHILE x ~= [] \
nipkow@1363
    20
\ DO { rev(x)@y = X@Y} \
nipkow@1363
    21
\    y := hd x # y; x := tl x \
nipkow@1363
    22
\ END \
nipkow@1363
    23
\{y = X@Y}";
paulson@2031
    24
by (hoare_tac 1);
wenzelm@4089
    25
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
paulson@4153
    26
by Safe_tac;
paulson@2031
    27
by (Asm_full_simp_tac 1);
paulson@2031
    28
by (Asm_full_simp_tac 1);
nipkow@1363
    29
qed "imperative_append";