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
     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;
    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;
    27 by (Asm_full_simp_tac 1);
    28 by (Asm_full_simp_tac 1);
    29 qed "imperative_append";