author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45827  66c68453455c 
child 58889  5b7a9633cfa8 
permissions  rwrr 
11376  1 
(* Title: HOL/NanoJava/AxSem.thy 
41589  2 
Author: David von Oheimb, Technische Universitaet Muenchen 
11376  3 
*) 
4 

11560  5 
header "Axiomatic Semantics" 
11376  6 

16417  7 
theory AxSem imports State begin 
11376  8 

42463  9 
type_synonym assn = "state => bool" 
10 
type_synonym vassn = "val => assn" 

11 
type_synonym triple = "assn \<times> stmt \<times> assn" 

12 
type_synonym etriple = "assn \<times> expr \<times> vassn" 

11376  13 
translations 
35431  14 
(type) "assn" \<leftharpoondown> (type) "state => bool" 
15 
(type) "vassn" \<leftharpoondown> (type) "val => assn" 

16 
(type) "triple" \<leftharpoondown> (type) "assn \<times> stmt \<times> assn" 

17 
(type) "etriple" \<leftharpoondown> (type) "assn \<times> expr \<times> vassn" 

11376  18 

11476  19 

11560  20 
subsection "Hoare Logic Rules" 
21 

23755  22 
inductive 
23 
hoare :: "[triple set, triple set] => bool" ("_ \<turnstile>/ _" [61, 61] 60) 

24 
and ehoare :: "[triple set, etriple] => bool" ("_ \<turnstile>\<^sub>e/ _" [61, 61] 60) 

25 
and hoare1 :: "[triple set, assn,stmt,assn] => bool" 

26 
("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60) 

27 
and ehoare1 :: "[triple set, assn,expr,vassn]=> bool" 

28 
("_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60) 

29 
where 

11376  30 

23755  31 
"A \<turnstile> {P}c{Q} \<equiv> A \<turnstile> {(P,c,Q)}" 
32 
 "A \<turnstile>\<^sub>e {P}e{Q} \<equiv> A \<turnstile>\<^sub>e (P,e,Q)" 

11476  33 

23755  34 
 Skip: "A \<turnstile> {P} Skip {P}" 
35 

36 
 Comp: "[ A \<turnstile> {P} c1 {Q}; A \<turnstile> {Q} c2 {R} ] ==> A \<turnstile> {P} c1;;c2 {R}" 

11376  37 

23755  38 
 Cond: "[ A \<turnstile>\<^sub>e {P} e {Q}; 
39 
\<forall>v. A \<turnstile> {Q v} (if v \<noteq> Null then c1 else c2) {R} ] ==> 

40 
A \<turnstile> {P} If(e) c1 Else c2 {R}" 

11376  41 

23755  42 
 Loop: "A \<turnstile> {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==> 
43 
A \<turnstile> {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}" 

44 

45 
 LAcc: "A \<turnstile>\<^sub>e {\<lambda>s. P (s<x>) s} LAcc x {P}" 

11476  46 

23755  47 
 LAss: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. Q (lupd(x\<mapsto>v) s)} ==> 
48 
A \<turnstile> {P} x:==e {Q}" 

49 

50 
 FAcc: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. \<forall>a. v=Addr a > Q (get_field s a f) s} ==> 

51 
A \<turnstile>\<^sub>e {P} e..f {Q}" 

11376  52 

23755  53 
 FAss: "[ A \<turnstile>\<^sub>e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a > Q a s}; 
54 
\<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} ] ==> 

55 
A \<turnstile> {P} e1..f:==e2 {R}" 

11376  56 

23755  57 
 NewC: "A \<turnstile>\<^sub>e {\<lambda>s. \<forall>a. new_Addr s = Addr a > P (Addr a) (new_obj a C s)} 
11476  58 
new C {P}" 
11376  59 

23755  60 
 Cast: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. (case v of Null => True 
11476  61 
 Addr a => obj_class s a <=C C) > Q v s} ==> 
23755  62 
A \<turnstile>\<^sub>e {P} Cast C e {Q}" 
11376  63 

23755  64 
 Call: "[ A \<turnstile>\<^sub>e {P} e1 {Q}; \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {R a}; 
65 
\<forall>a p ls. A \<turnstile> {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and> 

11772  66 
s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s))} 
11565  67 
Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} ] ==> 
23755  68 
A \<turnstile>\<^sub>e {P} {C}e1..m(e2) {S}" 
11376  69 

23755  70 
 Meth: "\<forall>D. A \<turnstile> {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> 
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

71 
P s \<and> s' = init_locs D m s} 
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11486
diff
changeset

72 
Impl (D,m) {Q} ==> 
23755  73 
A \<turnstile> {P} Meth (C,m) {Q}" 
11376  74 

11565  75 
{* @{text "\<Union>Z"} instead of @{text "\<forall>Z"} in the conclusion and\\ 
76 
Z restricted to type state due to limitations of the inductive package *} 

23755  77 
 Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) \<turnstile> 
11565  78 
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> 
23755  79 
A \<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" 
11376  80 

11558
6539627881e8
simplified vnam/vname, introduced fname, improved comments
oheimb
parents:
11508
diff
changeset

81 
{* structural rules *} 
11376  82 

23755  83 
 Asm: " a \<in> A ==> A \<turnstile> {a}" 
11476  84 

23755  85 
 ConjI: " \<forall>c \<in> C. A \<turnstile> {c} ==> A \<turnstile> C" 
11476  86 

23755  87 
 ConjE: "[A \<turnstile> C; c \<in> C ] ==> A \<turnstile> {c}" 
11476  88 

11565  89 
{* Z restricted to type state due to limitations of the inductive package *} 
23755  90 
 Conseq:"[ \<forall>Z::state. A \<turnstile> {P' Z} c {Q' Z}; 
11565  91 
\<forall>s t. (\<forall>Z. P' Z s > Q' Z t) > (P s > Q t) ] ==> 
23755  92 
A \<turnstile> {P} c {Q }" 
11376  93 

11565  94 
{* Z restricted to type state due to limitations of the inductive package *} 
23755  95 
 eConseq:"[ \<forall>Z::state. A \<turnstile>\<^sub>e {P' Z} e {Q' Z}; 
11565  96 
\<forall>s v t. (\<forall>Z. P' Z s > Q' Z v t) > (P s > Q v t) ] ==> 
23755  97 
A \<turnstile>\<^sub>e {P} e {Q }" 
11565  98 

99 

12934
6003b4f916c0
Clarification wrt. use of polymorphic variants of Hoare logic rules
oheimb
parents:
11772
diff
changeset

100 
subsection "Fully polymorphic variants, required for Example only" 
11376  101 

45827  102 
axiomatization where 
23755  103 
Conseq:"[ \<forall>Z. A \<turnstile> {P' Z} c {Q' Z}; 
11565  104 
\<forall>s t. (\<forall>Z. P' Z s > Q' Z t) > (P s > Q t) ] ==> 
23755  105 
A \<turnstile> {P} c {Q }" 
11565  106 

45827  107 
axiomatization where 
108 
eConseq:"[ \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z}; 

11565  109 
\<forall>s v t. (\<forall>Z. P' Z s > Q' Z v t) > (P s > Q v t) ] ==> 
23755  110 
A \<turnstile>\<^sub>e {P} e {Q }" 
11565  111 

45827  112 
axiomatization where 
113 
Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) \<turnstile> 

11565  114 
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==> 
23755  115 
A \<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms" 
11376  116 

117 
subsection "Derived Rules" 

118 

119 
lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}" 

11476  120 
apply (rule hoare_ehoare.Conseq) 
121 
apply (rule allI, assumption) 

122 
apply fast 

123 
done 

124 

125 
lemma Conseq2: "\<lbrakk>A \<turnstile> {P} c {Q'}; \<forall>t. Q' t \<longrightarrow> Q t\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}" 

126 
apply (rule hoare_ehoare.Conseq) 

127 
apply (rule allI, assumption) 

128 
apply fast 

129 
done 

130 

11486  131 
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  132 
apply (rule hoare_ehoare.eConseq) 
133 
apply (rule allI, assumption) 

134 
apply fast 

135 
done 

136 

11486  137 
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  138 
apply (rule hoare_ehoare.eConseq) 
11376  139 
apply (rule allI, assumption) 
140 
apply fast 

141 
done 

142 

143 
lemma Weaken: "\<lbrakk>A \<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A \<turnstile> C" 

11476  144 
apply (rule hoare_ehoare.ConjI) 
11376  145 
apply clarify 
11476  146 
apply (drule hoare_ehoare.ConjE) 
11376  147 
apply fast 
148 
apply assumption 

149 
done 

150 

11565  151 
lemma Thin_lemma: 
152 
"(A' \<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile> C )) \<and> 

153 
(A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}))" 

154 
apply (rule hoare_ehoare.induct) 

42793  155 
apply (tactic "ALLGOALS(EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])") 
11565  156 
apply (blast intro: hoare_ehoare.Skip) 
157 
apply (blast intro: hoare_ehoare.Comp) 

158 
apply (blast intro: hoare_ehoare.Cond) 

159 
apply (blast intro: hoare_ehoare.Loop) 

160 
apply (blast intro: hoare_ehoare.LAcc) 

161 
apply (blast intro: hoare_ehoare.LAss) 

162 
apply (blast intro: hoare_ehoare.FAcc) 

163 
apply (blast intro: hoare_ehoare.FAss) 

164 
apply (blast intro: hoare_ehoare.NewC) 

165 
apply (blast intro: hoare_ehoare.Cast) 

166 
apply (erule hoare_ehoare.Call) 

167 
apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption) 

168 
apply blast 

169 
apply (blast intro!: hoare_ehoare.Meth) 

170 
apply (blast intro!: hoare_ehoare.Impl) 

171 
apply (blast intro!: hoare_ehoare.Asm) 

172 
apply (blast intro: hoare_ehoare.ConjI) 

173 
apply (blast intro: hoare_ehoare.ConjE) 

174 
apply (rule hoare_ehoare.Conseq) 

175 
apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+) 

176 
apply (rule hoare_ehoare.eConseq) 

177 
apply (rule, drule spec, erule conjE, tactic "smp_tac 1 1", assumption+) 

178 
done 

179 

180 
lemma cThin: "\<lbrakk>A' \<turnstile> C; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A \<turnstile> C" 

181 
by (erule (1) conjunct1 [OF Thin_lemma, rule_format]) 

182 

183 
lemma eThin: "\<lbrakk>A' \<turnstile>\<^sub>e {P} e {Q}; A' \<subseteq> A\<rbrakk> \<Longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}" 

184 
by (erule (1) conjunct2 [OF Thin_lemma, rule_format]) 

185 

186 

187 
lemma Union: "A \<turnstile> (\<Union>Z. C Z) = (\<forall>Z. A \<turnstile> C Z)" 

11476  188 
by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE) 
11376  189 

11565  190 
lemma Impl1': 
12934
6003b4f916c0
Clarification wrt. use of polymorphic variants of Hoare logic rules
oheimb
parents:
11772
diff
changeset

191 
"\<lbrakk>\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) \<turnstile> 
11565  192 
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms; 
11508  193 
Cm \<in> Ms\<rbrakk> \<Longrightarrow> 
11565  194 
A \<turnstile> {P Z Cm} Impl Cm {Q Z Cm}" 
12934
6003b4f916c0
Clarification wrt. use of polymorphic variants of Hoare logic rules
oheimb
parents:
11772
diff
changeset

195 
apply (drule AxSem.Impl) 
11376  196 
apply (erule Weaken) 
197 
apply (auto del: image_eqI intro: rev_image_eqI) 

198 
done 

199 

45605  200 
lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified] for Cm 
11565  201 

11376  202 
end 