6 Soundness and completeness of vc |
6 Soundness and completeness of vc |
7 *) |
7 *) |
8 |
8 |
9 open VC; |
9 open VC; |
10 |
10 |
11 val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[fast_tac HOL_cs 1]); |
11 AddIs hoare.intrs; |
|
12 |
|
13 val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]); |
12 |
14 |
13 goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}"; |
15 goal VC.thy "!Q. (!s. vc c Q s) --> |- {wp c Q} astrip c {Q}"; |
14 by(acom.induct_tac "c" 1); |
16 by(acom.induct_tac "c" 1); |
15 by(ALLGOALS Simp_tac); |
17 by(ALLGOALS Simp_tac); |
16 by(fast_tac (HOL_cs addIs hoare.intrs) 1); |
18 by(Fast_tac 1); |
17 by(fast_tac (HOL_cs addIs hoare.intrs) 1); |
19 by(Fast_tac 1); |
18 by(fast_tac (HOL_cs addIs hoare.intrs) 1); |
20 by(Fast_tac 1); |
19 (* if *) |
21 (* if *) |
20 br allI 1; |
22 by(Deepen_tac 4 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 *) |
23 (* while *) |
32 by(safe_tac HOL_cs); |
24 by(safe_tac HOL_cs); |
33 by (resolve_tac hoare.intrs 1); |
25 by (resolve_tac hoare.intrs 1); |
34 br lemma 1; |
26 br lemma 1; |
35 brs hoare.intrs 1; |
27 brs hoare.intrs 1; |
36 brs hoare.intrs 1; |
28 brs hoare.intrs 1; |
37 by(fast_tac HOL_cs 2); |
29 by(ALLGOALS(fast_tac HOL_cs)); |
38 by(ALLGOALS(fast_tac HOL_cs)); |
|
39 qed "vc_sound"; |
30 qed "vc_sound"; |
40 |
31 |
41 goal VC.thy "!P Q. (!s. P s --> Q s) --> (!s. wp c P s --> wp c Q s)"; |
32 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); |
33 by(acom.induct_tac "c" 1); |
43 by(ALLGOALS Asm_simp_tac); |
34 by(ALLGOALS Asm_simp_tac); |