author | oheimb |
Mon, 15 Oct 2001 17:02:57 +0200 | |
changeset 11772 | cf618fe8facd |
parent 11565 | ab004c0ecc63 |
child 12934 | 6003b4f916c0 |
permissions | -rw-r--r-- |
11376 | 1 |
(* Title: HOL/NanoJava/AxSem.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 2001 Technische Universitaet Muenchen |
|
5 |
*) |
|
6 |
||
11560 | 7 |
header "Axiomatic Semantics" |
11376 | 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" |
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11508
diff
changeset
|
41 |
"A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (* shouldn't be necessary *) |
11486 | 42 |
"A \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^sub>e (P,e,Q)" |
11376 | 43 |
|
11476 | 44 |
|
11560 | 45 |
subsection "Hoare Logic Rules" |
46 |
||
11476 | 47 |
inductive hoare ehoare |
11376 | 48 |
intros |
49 |
||
50 |
Skip: "A |- {P} Skip {P}" |
|
51 |
||
52 |
Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}" |
|
53 |
||
11476 | 54 |
Cond: "[| A |-e {P} e {Q}; |
55 |
\<forall>v. A |- {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==> |
|
56 |
A |- {P} If(e) c1 Else c2 {R}" |
|
57 |
||
58 |
Loop: "A |- {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==> |
|
59 |
A |- {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}" |
|
11376 | 60 |
|
11476 | 61 |
LAcc: "A |-e {\<lambda>s. P (s<x>) s} LAcc x {P}" |
11376 | 62 |
|
11476 | 63 |
LAss: "A |-e {P} e {\<lambda>v s. Q (lupd(x\<mapsto>v) s)} ==> |
64 |
A |- {P} x:==e {Q}" |
|
65 |
||
66 |
FAcc: "A |-e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==> |
|
67 |
A |-e {P} e..f {Q}" |
|
11376 | 68 |
|
11476 | 69 |
FAss: "[| A |-e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s}; |
70 |
\<forall>a. A |-e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==> |
|
71 |
A |- {P} e1..f:==e2 {R}" |
|
11376 | 72 |
|
11476 | 73 |
NewC: "A |-e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)} |
74 |
new C {P}" |
|
11376 | 75 |
|
11476 | 76 |
Cast: "A |-e {P} e {\<lambda>v s. (case v of Null => True |
77 |
| Addr a => obj_class s a <=C C) --> Q v s} ==> |
|
78 |
A |-e {P} Cast C e {Q}" |
|
11376 | 79 |
|
11476 | 80 |
Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a}; |
11565 | 81 |
\<forall>a p ls. A |- {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and> |
11772 | 82 |
s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s))} |
11565 | 83 |
Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==> |
11476 | 84 |
A |-e {P} {C}e1..m(e2) {S}" |
11376 | 85 |
|
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset
|
86 |
Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> |
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset
|
87 |
P s \<and> s' = init_locs D m s} |
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset
|
88 |
Impl (D,m) {Q} ==> |
11507 | 89 |
A |- {P} Meth (C,m) {Q}" |
11376 | 90 |
|
11565 | 91 |
--{* @{text "\<Union>Z"} instead of @{text "\<forall>Z"} in the conclusion and\\ |
92 |
Z restricted to type state due to limitations of the inductive package *} |
|
93 |
Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- |
|
94 |
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> |
|
95 |
A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" |
|
11376 | 96 |
|
11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11508
diff
changeset
|
97 |
--{* structural rules *} |
11376 | 98 |
|
11476 | 99 |
Asm: " a \<in> A ==> A ||- {a}" |
100 |
||
101 |
ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C" |
|
102 |
||
103 |
ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}" |
|
104 |
||
11565 | 105 |
--{* Z restricted to type state due to limitations of the inductive package *} |
106 |
Conseq:"[| \<forall>Z::state. A |- {P' Z} c {Q' Z}; |
|
107 |
\<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> |
|
11376 | 108 |
A |- {P} c {Q }" |
109 |
||
11565 | 110 |
--{* Z restricted to type state due to limitations of the inductive package *} |
111 |
eConseq:"[| \<forall>Z::state. A |-e {P' Z} e {Q' Z}; |
|
112 |
\<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> |
|
113 |
A |-e {P} e {Q }" |
|
114 |
||
115 |
||
116 |
subsection "Fully polymorphic variants" |
|
11376 | 117 |
|
11565 | 118 |
axioms |
119 |
Conseq:"[| \<forall>Z. A |- {P' Z} c {Q' Z}; |
|
120 |
\<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==> |
|
121 |
A |- {P} c {Q }" |
|
122 |
||
123 |
eConseq:"[| \<forall>Z. A |-e {P' Z} e {Q' Z}; |
|
124 |
\<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==> |
|
125 |
A |-e {P} e {Q }" |
|
126 |
||
127 |
Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||- |
|
128 |
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> |
|
129 |
A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" |
|
11376 | 130 |
|
131 |
subsection "Derived Rules" |
|
132 |
||
133 |
lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}" |
|
11476 | 134 |
apply (rule hoare_ehoare.Conseq) |
135 |
apply (rule allI, assumption) |
|
136 |
apply fast |
|
137 |
done |
|
138 |
||
139 |
lemma Conseq2: "\<lbrakk>A \<turnstile> {P} c {Q'}; \<forall>t. Q' t \<longrightarrow> Q t\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}" |
|
140 |
apply (rule hoare_ehoare.Conseq) |
|
141 |
apply (rule allI, assumption) |
|
142 |
apply fast |
|
143 |
done |
|
144 |
||
11486 | 145 |
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 | 146 |
apply (rule hoare_ehoare.eConseq) |
147 |
apply (rule allI, assumption) |
|
148 |
apply fast |
|
149 |
done |
|
150 |
||
11486 | 151 |
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 | 152 |
apply (rule hoare_ehoare.eConseq) |
11376 | 153 |
apply (rule allI, assumption) |
154 |
apply fast |
|
155 |
done |
|
156 |
||
157 |
lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C" |
|
11476 | 158 |
apply (rule hoare_ehoare.ConjI) |
11376 | 159 |
apply clarify |
11476 | 160 |
apply (drule hoare_ehoare.ConjE) |
11376 | 161 |
apply fast |
162 |
apply assumption |
|
163 |
done |
|
164 |
||
11565 | 165 |
lemma Thin_lemma: |
166 |
"(A' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and> |
|
167 |
(A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}))" |
|
168 |
apply (rule hoare_ehoare.induct) |
|
169 |
apply (tactic "ALLGOALS(EVERY'[Clarify_tac, REPEAT o smp_tac 1])") |
|
170 |
apply (blast intro: hoare_ehoare.Skip) |
|
171 |
apply (blast intro: hoare_ehoare.Comp) |
|
172 |
apply (blast intro: hoare_ehoare.Cond) |
|
173 |
apply (blast intro: hoare_ehoare.Loop) |
|
174 |
apply (blast intro: hoare_ehoare.LAcc) |
|
175 |
apply (blast intro: hoare_ehoare.LAss) |
|
176 |
apply (blast intro: hoare_ehoare.FAcc) |
|
177 |
apply (blast intro: hoare_ehoare.FAss) |
|
178 |
apply (blast intro: hoare_ehoare.NewC) |
|
179 |
apply (blast intro: hoare_ehoare.Cast) |
|
180 |
apply (erule hoare_ehoare.Call) |
|
181 |
apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption) |
|
182 |
apply blast |
|
183 |
apply (blast intro!: hoare_ehoare.Meth) |
|
184 |
apply (blast intro!: hoare_ehoare.Impl) |
|
185 |
apply (blast intro!: hoare_ehoare.Asm) |
|
186 |
apply (blast intro: hoare_ehoare.ConjI) |
|
187 |
apply (blast intro: hoare_ehoare.ConjE) |
|
188 |
apply (rule hoare_ehoare.Conseq) |
|
189 |
apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+) |
|
190 |
apply (rule hoare_ehoare.eConseq) |
|
191 |
apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+) |
|
192 |
done |
|
193 |
||
194 |
lemma cThin: "\<lbrakk>A' |\<turnstile> C; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A |\<turnstile> C" |
|
195 |
by (erule (1) conjunct1 [OF Thin_lemma, rule_format]) |
|
196 |
||
197 |
lemma eThin: "\<lbrakk>A' \<turnstile>\<^sub>e {P} e {Q}; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}" |
|
198 |
by (erule (1) conjunct2 [OF Thin_lemma, rule_format]) |
|
199 |
||
200 |
||
201 |
lemma Union: "A |\<turnstile> (\<Union>Z. C Z) = (\<forall>Z. A |\<turnstile> C Z)" |
|
11476 | 202 |
by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE) |
11376 | 203 |
|
11565 | 204 |
lemma Impl1': |
205 |
"\<lbrakk>\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> |
|
206 |
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms; |
|
11508 | 207 |
Cm \<in> Ms\<rbrakk> \<Longrightarrow> |
11565 | 208 |
A \<turnstile> {P Z Cm} Impl Cm {Q Z Cm}" |
209 |
apply (drule Impl) |
|
11376 | 210 |
apply (erule Weaken) |
211 |
apply (auto del: image_eqI intro: rev_image_eqI) |
|
212 |
done |
|
213 |
||
11565 | 214 |
lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard] |
215 |
||
11376 | 216 |
end |