Added List_Examples
authornipkow
Wed Nov 22 18:48:56 1995 +0100 (1995-11-22)
changeset 13637bdc4699ef4d
parent 1362 5fdd4da11d49
child 1364 8ea1a962ad72
Added List_Examples
src/HOL/Hoare/List_Examples.ML
src/HOL/Hoare/List_Examples.thy
src/HOL/Hoare/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hoare/List_Examples.ML	Wed Nov 22 18:48:56 1995 +0100
     1.3 @@ -0,0 +1,29 @@
     1.4 +goal thy
     1.5 +"{x=X} \
     1.6 +\ y := []; \
     1.7 +\ WHILE x ~= [] \
     1.8 +\ DO { rev(x)@y = rev(X)} \
     1.9 +\    y := hd x # y; x := tl x \
    1.10 +\ END \
    1.11 +\{y=rev(X)}";
    1.12 +by(hoare_tac 1);
    1.13 +by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
    1.14 +by(safe_tac HOL_cs);
    1.15 +by(Asm_full_simp_tac 1);
    1.16 +by(Asm_full_simp_tac 1);
    1.17 +qed "imperative_reverse";
    1.18 +
    1.19 +goal thy
    1.20 +"{x=X & y = Y} \
    1.21 +\ x := rev(x); \
    1.22 +\ WHILE x ~= [] \
    1.23 +\ DO { rev(x)@y = X@Y} \
    1.24 +\    y := hd x # y; x := tl x \
    1.25 +\ END \
    1.26 +\{y = X@Y}";
    1.27 +by(hoare_tac 1);
    1.28 +by(asm_full_simp_tac (!simpset addsimps [neq_Nil_conv]) 1);
    1.29 +by(safe_tac HOL_cs);
    1.30 +by(Asm_full_simp_tac 1);
    1.31 +by(Asm_full_simp_tac 1);
    1.32 +qed "imperative_append";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Hoare/List_Examples.thy	Wed Nov 22 18:48:56 1995 +0100
     2.3 @@ -0,0 +1,1 @@
     2.4 +List_Examples = Hoare + List
     3.1 --- a/src/HOL/Hoare/ROOT.ML	Tue Nov 21 17:59:45 1995 +0100
     3.2 +++ b/src/HOL/Hoare/ROOT.ML	Wed Nov 22 18:48:56 1995 +0100
     3.3 @@ -7,3 +7,4 @@
     3.4  HOL_build_completed;	(*Make examples fail if HOL did*)
     3.5  
     3.6  use_thy "Examples";
     3.7 +use_thy "List_Examples";