1 (* Title: HOL/IMP/Hoare.ML |
1 (* Title: HOL/IMP/Hoare.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1995 TUM |
4 Copyright 1995 TUM |
5 |
5 |
6 Soundness of Hoare rules wrt denotational semantics |
6 Soundness (and part of) relative completeness of Hoare rules |
|
7 wrt denotational semantics |
7 *) |
8 *) |
8 |
9 |
9 open Hoare; |
10 open Hoare; |
10 |
11 |
11 goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q"; |
12 goalw Hoare.thy [hoare_valid_def] "!P c Q. ({{P}}c{{Q}}) --> |= {{P}}c{{Q}}"; |
12 by (rtac hoare.mutual_induct 1); |
13 by (rtac hoare.mutual_induct 1); |
13 by(ALLGOALS Asm_simp_tac); |
14 by(ALLGOALS Asm_simp_tac); |
14 by(fast_tac rel_cs 1); |
15 by(fast_tac rel_cs 1); |
15 by(fast_tac HOL_cs 1); |
16 by(fast_tac HOL_cs 1); |
16 by (rtac allI 1); |
17 by (rtac allI 1); |
22 by(eres_inst_tac [("x","a")] allE 1); |
23 by(eres_inst_tac [("x","a")] allE 1); |
23 by (safe_tac comp_cs); |
24 by (safe_tac comp_cs); |
24 by(ALLGOALS Asm_full_simp_tac); |
25 by(ALLGOALS Asm_full_simp_tac); |
25 qed "hoare_sound"; |
26 qed "hoare_sound"; |
26 |
27 |
27 (* |
28 goalw Hoare.thy [swp_def] "swp Skip Q = Q"; |
28 fun while_tac inv ss i = |
29 by(Simp_tac 1); |
29 EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i, |
30 br ext 1; |
30 asm_full_simp_tac ss (i+1)]; |
31 by(fast_tac HOL_cs 1); |
|
32 qed "swp_Skip"; |
31 |
33 |
32 fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss, |
34 goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[A a s/x]))"; |
33 TRY o (strip_tac THEN' atac)]; |
35 by(Simp_tac 1); |
|
36 br ext 1; |
|
37 by(fast_tac HOL_cs 1); |
|
38 qed "swp_Ass"; |
34 |
39 |
35 fun hoare_tac ss = |
40 goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)"; |
36 REPEAT(STATE(fn th => FIRST'[rtac hoare_seq, assign_tac ss] (nprems_of th))); |
41 by(Simp_tac 1); |
|
42 br ext 1; |
|
43 by(fast_tac comp_cs 1); |
|
44 qed "swp_Semi"; |
37 |
45 |
38 (* example *) |
46 goalw Hoare.thy [swp_def] |
39 val prems = goal Hoare.thy |
47 "swp (IF b THEN c ELSE d) Q = (%s. (B b s --> swp c Q s) & \ |
40 "[| u ~= y; u ~= z; y ~= z |] ==> \ |
48 \ (~B b s --> swp d Q s))"; |
41 \ {{%s.s(x)=i & s(y)=j}} \ |
49 by(Simp_tac 1); |
42 \ z := X x; (u := N 0; \ |
50 br ext 1; |
43 \ while noti(ROp op = (X u) (X y)) \ |
51 by(fast_tac comp_cs 1); |
44 \ do (u := Op1 Suc (X u); z := Op1 Suc (X z))) \ |
52 qed "swp_If"; |
45 \ {{%s. s(z)=i+j}}"; |
53 |
46 val ss = !simpset addsimps (eq_sym_conv::assign_def::prems); |
54 goalw Hoare.thy [swp_def] |
47 by(hoare_tac ss); |
55 "!!s. B b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s"; |
48 by(while_tac "%s.s z = i + s u & s y = j" ss 3); |
56 by(stac C_While_If 1); |
49 by(hoare_tac ss); |
57 by(Asm_simp_tac 1); |
50 result(); |
58 qed "swp_While_True"; |
51 *) |
59 |
|
60 goalw Hoare.thy [swp_def] "!!s. ~B b s ==> swp (WHILE b DO c) Q s = Q s"; |
|
61 by(stac C_While_If 1); |
|
62 by(Asm_simp_tac 1); |
|
63 by(fast_tac HOL_cs 1); |
|
64 qed "swp_While_False"; |
|
65 |
|
66 Addsimps [swp_Skip,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False]; |
|
67 |
|
68 Delsimps [C_while]; |
|
69 |
|
70 goalw Hoare.thy [hoare_valid_def,swp_def] |
|
71 "!!c. |= {{P}}c{{Q}} ==> !s. P s --> swp c Q s"; |
|
72 by(fast_tac HOL_cs 1); |
|
73 qed "swp_is_weakest"; |
|
74 |
|
75 goal Hoare.thy "!Q. {{swp c Q}} c {{Q}}"; |
|
76 by(com.induct_tac "c" 1); |
|
77 by(ALLGOALS Simp_tac); |
|
78 by(fast_tac (HOL_cs addIs [hoare.skip]) 1); |
|
79 by(fast_tac (HOL_cs addIs [hoare.ass]) 1); |
|
80 by(fast_tac (HOL_cs addIs [hoare.semi]) 1); |
|
81 by(safe_tac (HOL_cs addSIs [hoare.If])); |
|
82 br hoare.conseq 1; |
|
83 by(fast_tac HOL_cs 2); |
|
84 by(fast_tac HOL_cs 2); |
|
85 by(fast_tac HOL_cs 1); |
|
86 br hoare.conseq 1; |
|
87 by(fast_tac HOL_cs 2); |
|
88 by(fast_tac HOL_cs 2); |
|
89 by(fast_tac HOL_cs 1); |
|
90 br hoare.conseq 1; |
|
91 br hoare.While 2; |
|
92 be thin_rl 1; |
|
93 by(fast_tac HOL_cs 1); |
|
94 br hoare.conseq 1; |
|
95 be thin_rl 3; |
|
96 br allI 3; |
|
97 br impI 3; |
|
98 ba 3; |
|
99 by(fast_tac HOL_cs 2); |
|
100 by(safe_tac HOL_cs); |
|
101 by(rotate_tac ~1 1); |
|
102 by(Asm_full_simp_tac 1); |
|
103 by(rotate_tac ~1 1); |
|
104 by(Asm_full_simp_tac 1); |
|
105 bind_thm("swp_is_pre", result() RS spec); |
|
106 |
|
107 goal Hoare.thy "!!c. |= {{P}}c{{Q}} ==> {{P}}c{{Q}}"; |
|
108 br (swp_is_pre RSN (2,hoare.conseq)) 1; |
|
109 by(fast_tac HOL_cs 2); |
|
110 be swp_is_weakest 1; |
|
111 qed "hoare_relative_complete"; |