src/HOL/Hoare/List_Examples.ML
author wenzelm
Fri, 29 May 1998 13:50:21 +0200
changeset 4987 257aeccdefc3
parent 4724 3d2375efb80e
child 5069 3ea049f7979d
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1363
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
     1
goal thy
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
     2
"{x=X} \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
     3
\ y := []; \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
     4
\ WHILE x ~= [] \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
     5
\ DO { rev(x)@y = rev(X)} \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
     6
\    y := hd x # y; x := tl x \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
     7
\ END \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
     8
\{y=rev(X)}";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1875
diff changeset
     9
by (hoare_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 2031
diff changeset
    10
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4089
diff changeset
    11
by Safe_tac;
2031
03a843f0f447 Ran expandshort
paulson
parents: 1875
diff changeset
    12
by (Asm_full_simp_tac 1);
1363
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    13
qed "imperative_reverse";
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    14
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    15
goal thy
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    16
"{x=X & y = Y} \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    17
\ x := rev(x); \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    18
\ WHILE x ~= [] \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    19
\ DO { rev(x)@y = X@Y} \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    20
\    y := hd x # y; x := tl x \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    21
\ END \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    22
\{y = X@Y}";
2031
03a843f0f447 Ran expandshort
paulson
parents: 1875
diff changeset
    23
by (hoare_tac 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 2031
diff changeset
    24
by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
4153
e534c4c32d54 Ran expandshort, especially to introduce Safe_tac
paulson
parents: 4089
diff changeset
    25
by Safe_tac;
2031
03a843f0f447 Ran expandshort
paulson
parents: 1875
diff changeset
    26
by (Asm_full_simp_tac 1);
1363
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    27
qed "imperative_append";