author | nipkow |
Fri, 23 Aug 1996 13:12:51 +0200 | |
changeset 1940 | 9bd1c8826f5c |
parent 1743 | f7feaacd33d3 |
child 1973 | 8c94c9a5be10 |
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 |
||
11 |
val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[fast_tac HOL_cs 1]); |
|
12 |
||
1486 | 13 |
goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}"; |
1447 | 14 |
by(acom.induct_tac "c" 1); |
15 |
by(ALLGOALS Simp_tac); |
|
16 |
by(fast_tac (HOL_cs addIs hoare.intrs) 1); |
|
17 |
by(fast_tac (HOL_cs addIs hoare.intrs) 1); |
|
18 |
by(fast_tac (HOL_cs addIs hoare.intrs) 1); |
|
19 |
(* if *) |
|
20 |
br allI 1; |
|
21 |
br impI 1; |
|
22 |
brs hoare.intrs 1; |
|
23 |
brs hoare.intrs 1; |
|
24 |
by(fast_tac HOL_cs 2); |
|
25 |
by(fast_tac HOL_cs 1); |
|
26 |
by(fast_tac HOL_cs 1); |
|
27 |
brs hoare.intrs 1; |
|
28 |
by(fast_tac HOL_cs 2); |
|
29 |
by(fast_tac HOL_cs 1); |
|
30 |
by(fast_tac HOL_cs 1); |
|
31 |
(* while *) |
|
32 |
by(safe_tac HOL_cs); |
|
1465 | 33 |
by (resolve_tac hoare.intrs 1); |
1447 | 34 |
br lemma 1; |
35 |
brs hoare.intrs 1; |
|
36 |
brs hoare.intrs 1; |
|
37 |
by(fast_tac HOL_cs 2); |
|
38 |
by(ALLGOALS(fast_tac HOL_cs)); |
|
39 |
qed "vc_sound"; |
|
40 |
||
41 |
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)"; |
|
42 |
by(acom.induct_tac "c" 1); |
|
43 |
by(ALLGOALS Asm_simp_tac); |
|
44 |
by(EVERY1[rtac allI, rtac allI, rtac impI]); |
|
45 |
by(EVERY1[etac allE, etac allE, etac mp]); |
|
46 |
by(EVERY1[etac allE, etac allE, etac mp, atac]); |
|
1486 | 47 |
qed_spec_mp "wp_mono"; |
1447 | 48 |
|
49 |
goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"; |
|
50 |
by(acom.induct_tac "c" 1); |
|
51 |
by(ALLGOALS Asm_simp_tac); |
|
52 |
by(safe_tac HOL_cs); |
|
53 |
by(EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]); |
|
54 |
by(fast_tac (HOL_cs addEs [wp_mono]) 1); |
|
1486 | 55 |
qed_spec_mp "vc_mono"; |
1447 | 56 |
|
57 |
goal VC.thy |
|
1743 | 58 |
"!!P c Q. |- {P}c{Q} ==> \ |
1940
9bd1c8826f5c
Swaped two conditions in the completeness statement.
nipkow
parents:
1743
diff
changeset
|
59 |
\ (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> wp ac Q s))"; |
1743 | 60 |
by (etac hoare.induct 1); |
1447 | 61 |
by(res_inst_tac [("x","Askip")] exI 1); |
62 |
by(Simp_tac 1); |
|
63 |
by(res_inst_tac [("x","Aass x a")] exI 1); |
|
64 |
by(Simp_tac 1); |
|
65 |
by(SELECT_GOAL(safe_tac HOL_cs)1); |
|
66 |
by(res_inst_tac [("x","Asemi ac aca")] exI 1); |
|
67 |
by(Asm_simp_tac 1); |
|
68 |
by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); |
|
69 |
by(SELECT_GOAL(safe_tac HOL_cs)1); |
|
70 |
by(res_inst_tac [("x","Aif b ac aca")] exI 1); |
|
71 |
by(Asm_simp_tac 1); |
|
72 |
by(SELECT_GOAL(safe_tac HOL_cs)1); |
|
1743 | 73 |
by(res_inst_tac [("x","Awhile b Pa ac")] exI 1); |
1447 | 74 |
by(Asm_simp_tac 1); |
1743 | 75 |
by (safe_tac HOL_cs); |
1447 | 76 |
by(res_inst_tac [("x","ac")] exI 1); |
77 |
by(Asm_simp_tac 1); |
|
78 |
by(fast_tac (HOL_cs addSEs [wp_mono,vc_mono]) 1); |
|
1743 | 79 |
qed "vc_complete"; |
1451 | 80 |
|
81 |
goal VC.thy "!Q. vcwp c Q = (vc c Q, wp c Q)"; |
|
82 |
by(acom.induct_tac "c" 1); |
|
83 |
by(ALLGOALS (asm_simp_tac (!simpset addsimps [Let_def]))); |
|
84 |
qed "vcwp_vc_wp"; |