author | paulson |
Mon, 19 Aug 1996 11:17:20 +0200 | |
changeset 1910 | 6d572f96fb76 |
parent 1747 | f20c9abe4b50 |
child 1973 | 8c94c9a5be10 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/IMP/Hoare.ML |
938 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Tobias Nipkow |
936 | 4 |
Copyright 1995 TUM |
5 |
||
1481 | 6 |
Soundness (and part of) relative completeness of Hoare rules |
7 |
wrt denotational semantics |
|
936 | 8 |
*) |
9 |
||
10 |
open Hoare; |
|
11 |
||
1730 | 12 |
goalw Hoare.thy [hoare_valid_def] "!!P c Q. |- {P}c{Q} ==> |= {P}c{Q}"; |
13 |
by (etac hoare.induct 1); |
|
1447 | 14 |
by(ALLGOALS Asm_simp_tac); |
15 |
by(fast_tac rel_cs 1); |
|
1910 | 16 |
by (Fast_tac 1); |
1465 | 17 |
by (rtac allI 1); |
18 |
by (rtac allI 1); |
|
19 |
by (rtac impI 1); |
|
20 |
by (etac induct2 1); |
|
1447 | 21 |
br Gamma_mono 1; |
1747
f20c9abe4b50
Had to rename params because variable names in an induction rule changed.
nipkow
parents:
1730
diff
changeset
|
22 |
by(prune_params_tac); |
f20c9abe4b50
Had to rename params because variable names in an induction rule changed.
nipkow
parents:
1730
diff
changeset
|
23 |
by(rename_tac "s t" 1); |
1465 | 24 |
by (rewtac Gamma_def); |
1747
f20c9abe4b50
Had to rename params because variable names in an induction rule changed.
nipkow
parents:
1730
diff
changeset
|
25 |
by(eres_inst_tac [("x","s")] allE 1); |
1910 | 26 |
by (Step_tac 1); |
1447 | 27 |
by(ALLGOALS Asm_full_simp_tac); |
1730 | 28 |
qed "hoare_sound"; |
936 | 29 |
|
1696 | 30 |
goalw Hoare.thy [swp_def] "swp SKIP Q = Q"; |
1481 | 31 |
by(Simp_tac 1); |
32 |
br ext 1; |
|
1910 | 33 |
by (Fast_tac 1); |
1696 | 34 |
qed "swp_SKIP"; |
1481 | 35 |
|
1696 | 36 |
goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))"; |
1481 | 37 |
by(Simp_tac 1); |
38 |
qed "swp_Ass"; |
|
39 |
||
40 |
goalw Hoare.thy [swp_def] "swp (c;d) Q = swp c (swp d Q)"; |
|
41 |
by(Simp_tac 1); |
|
42 |
br ext 1; |
|
1910 | 43 |
by (Fast_tac 1); |
1481 | 44 |
qed "swp_Semi"; |
936 | 45 |
|
1481 | 46 |
goalw Hoare.thy [swp_def] |
1696 | 47 |
"swp (IF b THEN c ELSE d) Q = (%s. (b s --> swp c Q s) & \ |
48 |
\ (~b s --> swp d Q s))"; |
|
1481 | 49 |
by(Simp_tac 1); |
50 |
br ext 1; |
|
1910 | 51 |
by (Fast_tac 1); |
1481 | 52 |
qed "swp_If"; |
936 | 53 |
|
1481 | 54 |
goalw Hoare.thy [swp_def] |
1696 | 55 |
"!!s. b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s"; |
1481 | 56 |
by(stac C_While_If 1); |
57 |
by(Asm_simp_tac 1); |
|
58 |
qed "swp_While_True"; |
|
59 |
||
1696 | 60 |
goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s"; |
1481 | 61 |
by(stac C_While_If 1); |
62 |
by(Asm_simp_tac 1); |
|
1910 | 63 |
by (Fast_tac 1); |
1481 | 64 |
qed "swp_While_False"; |
65 |
||
1696 | 66 |
Addsimps [swp_SKIP,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False]; |
1481 | 67 |
|
1910 | 68 |
(*Not suitable for rewriting: LOOPS!*) |
69 |
goal Hoare.thy "swp (WHILE b DO c) Q s = \ |
|
70 |
\ (if b s then swp (c;WHILE b DO c) Q s else Q s)"; |
|
71 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); |
|
72 |
qed "swp_While_if"; |
|
73 |
||
74 |
||
1481 | 75 |
Delsimps [C_while]; |
936 | 76 |
|
1910 | 77 |
AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If]; |
78 |
||
1486 | 79 |
goal Hoare.thy "!Q. |- {swp c Q} c {Q}"; |
1481 | 80 |
by(com.induct_tac "c" 1); |
81 |
by(ALLGOALS Simp_tac); |
|
1910 | 82 |
by (REPEAT_FIRST Fast_tac); |
83 |
by (deepen_tac (!claset addIs [hoare.conseq]) 0 1); |
|
84 |
by (Step_tac 1); |
|
1481 | 85 |
br hoare.conseq 1; |
86 |
be thin_rl 1; |
|
1910 | 87 |
by (Fast_tac 1); |
1696 | 88 |
br hoare.While 1; |
1481 | 89 |
br hoare.conseq 1; |
90 |
be thin_rl 3; |
|
91 |
br allI 3; |
|
92 |
br impI 3; |
|
93 |
ba 3; |
|
1910 | 94 |
by (Fast_tac 2); |
1481 | 95 |
by(safe_tac HOL_cs); |
96 |
by(rotate_tac ~1 1); |
|
97 |
by(Asm_full_simp_tac 1); |
|
98 |
by(rotate_tac ~1 1); |
|
99 |
by(Asm_full_simp_tac 1); |
|
1486 | 100 |
qed_spec_mp "swp_is_pre"; |
1481 | 101 |
|
1486 | 102 |
goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}"; |
1481 | 103 |
br (swp_is_pre RSN (2,hoare.conseq)) 1; |
1910 | 104 |
by (Fast_tac 2); |
1696 | 105 |
by(rewrite_goals_tac [hoare_valid_def,swp_def]); |
1910 | 106 |
by (Fast_tac 1); |
1481 | 107 |
qed "hoare_relative_complete"; |