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 Derivation of Hoare rules |
6 Soundness of Hoare rules wrt denotational semantics |
7 *) |
7 *) |
8 |
8 |
9 open Hoare; |
9 open Hoare; |
10 |
10 |
11 Unify.trace_bound := 30; |
11 goalw Hoare.thy [spec_def] "!P c Q. ({{P}}c{{Q}}) --> spec P c Q"; |
12 Unify.search_bound := 30; |
12 br hoare.mutual_induct 1; |
13 |
13 by(ALLGOALS Asm_simp_tac); |
14 goalw Hoare.thy [spec_def] |
14 by(fast_tac rel_cs 1); |
15 "!!P.[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] \ |
15 by(fast_tac HOL_cs 1); |
16 \ ==> {{P'}}c{{Q'}}"; |
|
17 by(fast_tac HOL_cs 1); |
|
18 bind_thm("hoare_conseq", impI RSN (3,allI RSN (3,impI RS allI RS result()))); |
|
19 |
|
20 goalw Hoare.thy (spec_def::C_simps) "{{P}} skip {{P}}"; |
|
21 by(fast_tac comp_cs 1); |
|
22 qed"hoare_skip"; |
|
23 |
|
24 goalw Hoare.thy (spec_def::C_simps) |
|
25 "!!P. [| !s. P s --> Q(s[A a s/x]) |] ==> {{P}} x := a {{Q}}"; |
|
26 by(Asm_full_simp_tac 1); |
|
27 qed"hoare_assign"; |
|
28 |
|
29 goalw Hoare.thy (spec_def::C_simps) |
|
30 "!!P. [| {{P}} c {{Q}}; {{Q}} d {{R}} |] ==> {{P}} c;d {{R}}"; |
|
31 by(fast_tac comp_cs 1); |
|
32 qed"hoare_seq"; |
|
33 |
|
34 goalw Hoare.thy (spec_def::C_simps) |
|
35 "!!P. [| {{%s. P s & B b s}} c {{Q}}; {{%s. P s & ~B b s}} d {{Q}} |] ==> \ |
|
36 \ {{P}} ifc b then c else d {{Q}}"; |
|
37 by(Simp_tac 1); |
|
38 by(fast_tac comp_cs 1); |
|
39 qed"hoare_if"; |
|
40 |
|
41 goalw Hoare.thy (spec_def::C_simps) |
|
42 "!!P. [| {{%s. P s & B b s}} c {{P}} |] ==> \ |
|
43 \ {{P}} while b do c {{%s. P s & ~B b s}}"; |
|
44 br allI 1; |
16 br allI 1; |
45 br allI 1; |
17 br allI 1; |
46 br impI 1; |
18 br impI 1; |
47 be induct2 1; |
19 be induct2 1; |
48 br Gamma_mono 1; |
20 br Gamma_mono 1; |
49 by (rewrite_goals_tac [Gamma_def]); |
21 by (rewrite_goals_tac [Gamma_def]); |
50 by(eres_inst_tac [("x","a")] allE 1); |
22 by(eres_inst_tac [("x","a")] allE 1); |
51 by (safe_tac comp_cs); |
23 by (safe_tac comp_cs); |
52 by(ALLGOALS Asm_full_simp_tac); |
24 by(ALLGOALS Asm_full_simp_tac); |
53 qed"hoare_while"; |
25 qed "hoare_sound"; |
54 |
26 |
|
27 (* |
55 fun while_tac inv ss i = |
28 fun while_tac inv ss i = |
56 EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i, |
29 EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i, |
57 asm_full_simp_tac ss (i+1)]; |
30 asm_full_simp_tac ss (i+1)]; |
58 |
31 |
59 fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss, |
32 fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss, |