src/HOL/Hoare/List_Examples.ML
author berghofe
Tue, 25 Jun 1996 13:11:29 +0200
changeset 1824 44254696843a
parent 1363 7bdc4699ef4d
child 1875 54c0462f8fb2
permissions -rw-r--r--
Changed argument order of nat_rec.
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)}";
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
     9
by(hoare_tac 1);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    10
by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    11
by(safe_tac HOL_cs);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    12
by(Asm_full_simp_tac 1);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    13
by(Asm_full_simp_tac 1);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    14
qed "imperative_reverse";
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    15
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    16
goal thy
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    17
"{x=X & y = Y} \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    18
\ x := rev(x); \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    19
\ WHILE x ~= [] \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    20
\ DO { rev(x)@y = X@Y} \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    21
\    y := hd x # y; x := tl x \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    22
\ END \
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    23
\{y = X@Y}";
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    24
by(hoare_tac 1);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    25
by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    26
by(safe_tac HOL_cs);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    27
by(Asm_full_simp_tac 1);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    28
by(Asm_full_simp_tac 1);
7bdc4699ef4d Added List_Examples
nipkow
parents:
diff changeset
    29
qed "imperative_append";