author | paulson |
Thu, 26 Sep 1996 12:47:47 +0200 | |
changeset 2031 | 03a843f0f447 |
parent 1973 | 8c94c9a5be10 |
child 2055 | cc274e47f607 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/IMP/VC.ML |
1447 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
1447 | 4 |
Copyright 1996 TUM |
5 |
||
6 |
Soundness and completeness of vc |
|
7 |
*) |
|
8 |
||
9 |
open VC; |
|
10 |
||
1973 | 11 |
AddIs hoare.intrs; |
12 |
||
13 |
val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]); |
|
1447 | 14 |
|
1486 | 15 |
goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}"; |
2031 | 16 |
by (acom.induct_tac "c" 1); |
1447 | 17 |
by(ALLGOALS Simp_tac); |
1973 | 18 |
by(Fast_tac 1); |
19 |
by(Fast_tac 1); |
|
20 |
by(Fast_tac 1); |
|
1447 | 21 |
(* if *) |
1973 | 22 |
by(Deepen_tac 4 1); |
1447 | 23 |
(* while *) |
2031 | 24 |
by (safe_tac HOL_cs); |
1465 | 25 |
by (resolve_tac hoare.intrs 1); |
1447 | 26 |
br lemma 1; |
27 |
brs hoare.intrs 1; |
|
28 |
brs hoare.intrs 1; |
|
1973 | 29 |
by(ALLGOALS(fast_tac HOL_cs)); |
1447 | 30 |
qed "vc_sound"; |
31 |
||
32 |
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)"; |
|
2031 | 33 |
by (acom.induct_tac "c" 1); |
1447 | 34 |
by(ALLGOALS Asm_simp_tac); |
2031 | 35 |
by (EVERY1[rtac allI, rtac allI, rtac impI]); |
36 |
by (EVERY1[etac allE, etac allE, etac mp]); |
|
37 |
by (EVERY1[etac allE, etac allE, etac mp, atac]); |
|
1486 | 38 |
qed_spec_mp "wp_mono"; |
1447 | 39 |
|
40 |
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"; |
|
2031 | 41 |
by (acom.induct_tac "c" 1); |
1447 | 42 |
by(ALLGOALS Asm_simp_tac); |
2031 | 43 |
by (safe_tac HOL_cs); |
44 |
by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]); |
|
45 |
by (fast_tac (HOL_cs addEs [wp_mono]) 1); |
|
1486 | 46 |
qed_spec_mp "vc_mono"; |
1447 | 47 |
|
48 |
goal VC.thy |
|
1743 | 49 |
"!!P c Q. |- {P}c{Q} ==> \ |
1940
9bd1c8826f5c
Swaped two conditions in the completeness statement.
nipkow
parents:
1743
diff
changeset
|
50 |
\ (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> wp ac Q s))"; |
1743 | 51 |
by (etac hoare.induct 1); |
1447 | 52 |
by(res_inst_tac [("x","Askip")] exI 1); |
53 |
by(Simp_tac 1); |
|
54 |
by(res_inst_tac [("x","Aass x a")] exI 1); |
|
55 |
by(Simp_tac 1); |
|
56 |
by(SELECT_GOAL(safe_tac HOL_cs)1); |
|
57 |
by(res_inst_tac [("x","Asemi ac aca")] exI 1); |
|
58 |
by(Asm_simp_tac 1); |
|
59 |
by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); |
|
60 |
by(SELECT_GOAL(safe_tac HOL_cs)1); |
|
61 |
by(res_inst_tac [("x","Aif b ac aca")] exI 1); |
|
62 |
by(Asm_simp_tac 1); |
|
63 |
by(SELECT_GOAL(safe_tac HOL_cs)1); |
|
1743 | 64 |
by(res_inst_tac [("x","Awhile b Pa ac")] exI 1); |
1447 | 65 |
by(Asm_simp_tac 1); |
1743 | 66 |
by (safe_tac HOL_cs); |
2031 | 67 |
by (res_inst_tac [("x","ac")] exI 1); |
68 |
by (Asm_simp_tac 1); |
|
69 |
by (fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); |
|
1743 | 70 |
qed "vc_complete"; |
1451 | 71 |
|
72 |
goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)"; |
|
2031 | 73 |
by (acom.induct_tac "c" 1); |
74 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def]))); |
|
1451 | 75 |
qed "vcwp_vc_wp"; |