src/HOL/Hoare/List_Examples.ML
author wenzelm
Mon Nov 03 12:13:18 1997 +0100 (1997-11-03)
changeset 4089 96fba19bcbe2
parent 2031 03a843f0f447
child 4153 e534c4c32d54
permissions -rw-r--r--
isatool fixclasimp;
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);
wenzelm@4089
    11
by (safe_tac (claset()));
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);
wenzelm@4089
    26
by (safe_tac (claset()));
paulson@2031
    27
by (Asm_full_simp_tac 1);
paulson@2031
    28
by (Asm_full_simp_tac 1);
nipkow@1363
    29
qed "imperative_append";