11376
|
1 |
(* Title: HOL/NanoJava/AxSem.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 2001 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
header "Axiomatic Semantics (Hoare Logic)"
|
|
8 |
|
|
9 |
theory AxSem = State:
|
|
10 |
|
|
11 |
types assn = "state => bool"
|
11486
|
12 |
vassn = "val => assn"
|
11476
|
13 |
triple = "assn \<times> stmt \<times> assn"
|
|
14 |
etriple = "assn \<times> expr \<times> vassn"
|
11376
|
15 |
translations
|
|
16 |
"assn" \<leftharpoondown> (type)"state => bool"
|
11476
|
17 |
"vassn" \<leftharpoondown> (type)"val => assn"
|
|
18 |
"triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
|
|
19 |
"etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
|
11376
|
20 |
|
11476
|
21 |
consts hoare :: "(triple set \<times> triple set) set"
|
|
22 |
consts ehoare :: "(triple set \<times> etriple ) set"
|
11376
|
23 |
syntax (xsymbols)
|
|
24 |
"@hoare" :: "[triple set, triple set ] => bool" ("_ |\<turnstile>/ _" [61,61] 60)
|
|
25 |
"@hoare1" :: "[triple set, assn,stmt,assn] => bool"
|
|
26 |
("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
|
11486
|
27 |
"@ehoare" :: "[triple set, etriple ] => bool" ("_ |\<turnstile>\<^sub>e/ _"[61,61]60)
|
11476
|
28 |
"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool"
|
11486
|
29 |
("_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
|
11376
|
30 |
syntax
|
|
31 |
"@hoare" :: "[triple set, triple set ] => bool" ("_ ||-/ _" [61,61] 60)
|
|
32 |
"@hoare1" :: "[triple set, assn,stmt,assn] => bool"
|
|
33 |
("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
|
11476
|
34 |
"@ehoare" :: "[triple set, etriple ] => bool" ("_ ||-e/ _"[61,61] 60)
|
|
35 |
"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool"
|
|
36 |
("_ |-e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
|
11376
|
37 |
|
11476
|
38 |
translations "A |\<turnstile> C" \<rightleftharpoons> "(A,C) \<in> hoare"
|
|
39 |
"A \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
|
11486
|
40 |
"A |\<turnstile>\<^sub>e t" \<rightleftharpoons> "(A,t) \<in> ehoare"
|
|
41 |
"A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (** shouldn't be necess.**)
|
|
42 |
"A \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^sub>e (P,e,Q)"
|
11376
|
43 |
|
11476
|
44 |
|
|
45 |
inductive hoare ehoare
|
11376
|
46 |
intros
|
|
47 |
|
|
48 |
Skip: "A |- {P} Skip {P}"
|
|
49 |
|
|
50 |
Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
|
|
51 |
|
11476
|
52 |
Cond: "[| A |-e {P} e {Q};
|
|
53 |
\<forall>v. A |- {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
|
|
54 |
A |- {P} If(e) c1 Else c2 {R}"
|
|
55 |
|
|
56 |
Loop: "A |- {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
|
|
57 |
A |- {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
|
11376
|
58 |
|
11476
|
59 |
LAcc: "A |-e {\<lambda>s. P (s<x>) s} LAcc x {P}"
|
11376
|
60 |
|
11476
|
61 |
LAss: "A |-e {P} e {\<lambda>v s. Q (lupd(x\<mapsto>v) s)} ==>
|
|
62 |
A |- {P} x:==e {Q}"
|
|
63 |
|
|
64 |
FAcc: "A |-e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
|
|
65 |
A |-e {P} e..f {Q}"
|
11376
|
66 |
|
11476
|
67 |
FAss: "[| A |-e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
|
|
68 |
\<forall>a. A |-e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
|
|
69 |
A |- {P} e1..f:==e2 {R}"
|
11376
|
70 |
|
11476
|
71 |
NewC: "A |-e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
|
|
72 |
new C {P}"
|
11376
|
73 |
|
11476
|
74 |
Cast: "A |-e {P} e {\<lambda>v s. (case v of Null => True
|
|
75 |
| Addr a => obj_class s a <=C C) --> Q v s} ==>
|
|
76 |
A |-e {P} Cast C e {Q}"
|
11376
|
77 |
|
11476
|
78 |
Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
|
|
79 |
\<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and>
|
|
80 |
s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s))}
|
|
81 |
Meth C m {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==>
|
|
82 |
A |-e {P} {C}e1..m(e2) {S}"
|
11376
|
83 |
|
|
84 |
Meth: "\<forall>D. A |- {\<lambda>s. \<exists>a. s<This> = Addr a \<and> D=obj_class s a \<and> D <=C C \<and> P s}
|
|
85 |
Impl D m {Q} ==>
|
|
86 |
A |- {P} Meth C m {Q}"
|
|
87 |
|
|
88 |
(*\<Union>z instead of \<forall>z in the conclusion and
|
11476
|
89 |
z restricted to type state due to limitations of the inductive package *)
|
11376
|
90 |
Impl: "A\<union> (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||-
|
|
91 |
(\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
|
|
92 |
A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
|
|
93 |
|
|
94 |
(* structural rules *)
|
|
95 |
|
11476
|
96 |
Asm: " a \<in> A ==> A ||- {a}"
|
|
97 |
|
|
98 |
ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
|
|
99 |
|
|
100 |
ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
|
|
101 |
|
|
102 |
(* z restricted to type state due to limitations of the inductive package *)
|
11376
|
103 |
Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
|
|
104 |
\<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
|
|
105 |
A |- {P} c {Q }"
|
|
106 |
|
11476
|
107 |
(* z restricted to type state due to limitations of the inductive package *)
|
|
108 |
eConseq:"[| \<forall>z::state. A |-e {P' z} c {Q' z};
|
|
109 |
\<forall>s v t. (\<forall>z::state. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
|
|
110 |
A |-e {P} c {Q }"
|
11376
|
111 |
|
|
112 |
|
|
113 |
subsection "Derived Rules"
|
|
114 |
|
|
115 |
lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
|
11476
|
116 |
apply (rule hoare_ehoare.Conseq)
|
|
117 |
apply (rule allI, assumption)
|
|
118 |
apply fast
|
|
119 |
done
|
|
120 |
|
|
121 |
lemma Conseq2: "\<lbrakk>A \<turnstile> {P} c {Q'}; \<forall>t. Q' t \<longrightarrow> Q t\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
|
|
122 |
apply (rule hoare_ehoare.Conseq)
|
|
123 |
apply (rule allI, assumption)
|
|
124 |
apply fast
|
|
125 |
done
|
|
126 |
|
11486
|
127 |
lemma eConseq1: "\<lbrakk>A \<turnstile>\<^sub>e {P'} e {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}"
|
11476
|
128 |
apply (rule hoare_ehoare.eConseq)
|
|
129 |
apply (rule allI, assumption)
|
|
130 |
apply fast
|
|
131 |
done
|
|
132 |
|
11486
|
133 |
lemma eConseq2: "\<lbrakk>A \<turnstile>\<^sub>e {P} e {Q'}; \<forall>v t. Q' v t \<longrightarrow> Q v t\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}"
|
11476
|
134 |
apply (rule hoare_ehoare.eConseq)
|
11376
|
135 |
apply (rule allI, assumption)
|
|
136 |
apply fast
|
|
137 |
done
|
|
138 |
|
|
139 |
lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
|
11476
|
140 |
apply (rule hoare_ehoare.ConjI)
|
11376
|
141 |
apply clarify
|
11476
|
142 |
apply (drule hoare_ehoare.ConjE)
|
11376
|
143 |
apply fast
|
|
144 |
apply assumption
|
|
145 |
done
|
|
146 |
|
|
147 |
lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
|
11476
|
148 |
by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
|
11376
|
149 |
|
|
150 |
lemma Impl':
|
11449
|
151 |
"\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||-
|
11376
|
152 |
(\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
|
11449
|
153 |
A ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
|
11376
|
154 |
apply (drule Union[THEN iffD2])
|
11476
|
155 |
apply (drule hoare_ehoare.Impl)
|
11376
|
156 |
apply (drule Union[THEN iffD1])
|
|
157 |
apply (erule spec)
|
|
158 |
done
|
|
159 |
|
|
160 |
lemma Impl1:
|
11449
|
161 |
"\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||-
|
11376
|
162 |
(\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms;
|
11449
|
163 |
(C,m)\<in> ms\<rbrakk> \<Longrightarrow>
|
|
164 |
A |- {P z C m} Impl C m {Q (z::state) C m}"
|
11376
|
165 |
apply (drule Impl')
|
|
166 |
apply (erule Weaken)
|
|
167 |
apply (auto del: image_eqI intro: rev_image_eqI)
|
|
168 |
done
|
|
169 |
|
|
170 |
end
|