936
|
1 |
(* Title: HOL/IMP/Hoare.ML
|
938
|
2 |
ID: $Id$
|
936
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 1995 TUM
|
|
5 |
|
|
6 |
Derivation of Hoare rules
|
|
7 |
*)
|
|
8 |
|
|
9 |
open Hoare;
|
|
10 |
|
|
11 |
Unify.trace_bound := 30;
|
|
12 |
Unify.search_bound := 30;
|
|
13 |
|
|
14 |
goalw Hoare.thy [spec_def]
|
|
15 |
"!!P.[| !s. P' s --> P s; {{P}}c{{Q}}; !s. Q s --> Q' s |] \
|
|
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}}";
|
1266
|
26 |
by(Asm_full_simp_tac 1);
|
936
|
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}}";
|
1266
|
37 |
by(Simp_tac 1);
|
936
|
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;
|
|
45 |
br allI 1;
|
|
46 |
br impI 1;
|
|
47 |
be induct2 1;
|
|
48 |
br Gamma_mono 1;
|
|
49 |
by (rewrite_goals_tac [Gamma_def]);
|
|
50 |
by(eres_inst_tac [("x","a")] allE 1);
|
|
51 |
by (safe_tac comp_cs);
|
1266
|
52 |
by(ALLGOALS Asm_full_simp_tac);
|
936
|
53 |
qed"hoare_while";
|
|
54 |
|
|
55 |
fun while_tac inv ss i =
|
|
56 |
EVERY[res_inst_tac[("P",inv)] hoare_conseq i, atac i, rtac hoare_while i,
|
|
57 |
asm_full_simp_tac ss (i+1)];
|
|
58 |
|
|
59 |
fun assign_tac ss = EVERY'[rtac hoare_assign, simp_tac ss,
|
|
60 |
TRY o (strip_tac THEN' atac)];
|
|
61 |
|
|
62 |
fun hoare_tac ss =
|
|
63 |
REPEAT(STATE(fn th => FIRST'[rtac hoare_seq, assign_tac ss] (nprems_of th)));
|
|
64 |
|
|
65 |
(* example *)
|
|
66 |
val prems = goal Hoare.thy
|
|
67 |
"[| u ~= y; u ~= z; y ~= z |] ==> \
|
|
68 |
\ {{%s.s(x)=i & s(y)=j}} \
|
|
69 |
\ z := X x; (u := N 0; \
|
|
70 |
\ while noti(ROp op = (X u) (X y)) \
|
|
71 |
\ do (u := Op1 Suc (X u); z := Op1 Suc (X z))) \
|
|
72 |
\ {{%s. s(z)=i+j}}";
|
1266
|
73 |
val ss = !simpset addsimps (eq_sym_conv::assign_def::prems);
|
936
|
74 |
by(hoare_tac ss);
|
|
75 |
by(while_tac "%s.s z = i + s u & s y = j" ss 3);
|
|
76 |
by(hoare_tac ss);
|
|
77 |
result();
|