--- a/src/HOL/NanoJava/AxSem.thy Wed Jul 11 11:27:46 2007 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Wed Jul 11 11:28:13 2007 +0200
@@ -18,116 +18,102 @@
"triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
"etriple" \<leftharpoondown> (type)"assn \<times> expr \<times> vassn"
-consts hoare :: "(triple set \<times> triple set) set"
-consts ehoare :: "(triple set \<times> etriple ) set"
-syntax (xsymbols)
- "@hoare" :: "[triple set, triple set ] => bool" ("_ |\<turnstile>/ _" [61,61] 60)
- "@hoare1" :: "[triple set, assn,stmt,assn] => bool"
- ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
-"@ehoare" :: "[triple set, etriple ] => bool" ("_ |\<turnstile>\<^sub>e/ _"[61,61]60)
-"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool"
- ("_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
-syntax
- "@hoare" :: "[triple set, triple set ] => bool" ("_ ||-/ _" [61,61] 60)
- "@hoare1" :: "[triple set, assn,stmt,assn] => bool"
- ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
-"@ehoare" :: "[triple set, etriple ] => bool" ("_ ||-e/ _"[61,61] 60)
-"@ehoare1" :: "[triple set, assn,expr,vassn]=> bool"
- ("_ |-e/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
-
-translations "A |\<turnstile> C" \<rightleftharpoons> "(A,C) \<in> hoare"
- "A \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
- "A |\<turnstile>\<^sub>e t" \<rightleftharpoons> "(A,t) \<in> ehoare"
- "A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (* shouldn't be necessary *)
- "A \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^sub>e (P,e,Q)"
-
subsection "Hoare Logic Rules"
-inductive hoare ehoare
-intros
-
- Skip: "A |- {P} Skip {P}"
-
- Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
+inductive
+ hoare :: "[triple set, triple set] => bool" ("_ |\<turnstile>/ _" [61, 61] 60)
+ and ehoare :: "[triple set, etriple] => bool" ("_ |\<turnstile>\<^sub>e/ _" [61, 61] 60)
+ and hoare1 :: "[triple set, assn,stmt,assn] => bool"
+ ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
+ and ehoare1 :: "[triple set, assn,expr,vassn]=> bool"
+ ("_ \<turnstile>\<^sub>e/ ({(1_)}/ (_)/ {(1_)})" [61, 3, 90, 3] 60)
+where
- Cond: "[| A |-e {P} e {Q};
- \<forall>v. A |- {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
- A |- {P} If(e) c1 Else c2 {R}"
+ "A \<turnstile> {P}c{Q} \<equiv> A |\<turnstile> {(P,c,Q)}"
+| "A \<turnstile>\<^sub>e {P}e{Q} \<equiv> A |\<turnstile>\<^sub>e (P,e,Q)"
- Loop: "A |- {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
- A |- {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
+| Skip: "A \<turnstile> {P} Skip {P}"
+
+| Comp: "[| A \<turnstile> {P} c1 {Q}; A \<turnstile> {Q} c2 {R} |] ==> A \<turnstile> {P} c1;;c2 {R}"
- LAcc: "A |-e {\<lambda>s. P (s<x>) s} LAcc x {P}"
+| Cond: "[| A \<turnstile>\<^sub>e {P} e {Q};
+ \<forall>v. A \<turnstile> {Q v} (if v \<noteq> Null then c1 else c2) {R} |] ==>
+ A \<turnstile> {P} If(e) c1 Else c2 {R}"
- LAss: "A |-e {P} e {\<lambda>v s. Q (lupd(x\<mapsto>v) s)} ==>
- A |- {P} x:==e {Q}"
+| Loop: "A \<turnstile> {\<lambda>s. P s \<and> s<x> \<noteq> Null} c {P} ==>
+ A \<turnstile> {P} While(x) c {\<lambda>s. P s \<and> s<x> = Null}"
+
+| LAcc: "A \<turnstile>\<^sub>e {\<lambda>s. P (s<x>) s} LAcc x {P}"
- FAcc: "A |-e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
- A |-e {P} e..f {Q}"
+| LAss: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. Q (lupd(x\<mapsto>v) s)} ==>
+ A \<turnstile> {P} x:==e {Q}"
+
+| FAcc: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. \<forall>a. v=Addr a --> Q (get_field s a f) s} ==>
+ A \<turnstile>\<^sub>e {P} e..f {Q}"
- FAss: "[| A |-e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
- \<forall>a. A |-e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
- A |- {P} e1..f:==e2 {R}"
+| FAss: "[| A \<turnstile>\<^sub>e {P} e1 {\<lambda>v s. \<forall>a. v=Addr a --> Q a s};
+ \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {\<lambda>v s. R (upd_obj a f v s)} |] ==>
+ A \<turnstile> {P} e1..f:==e2 {R}"
- NewC: "A |-e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
+| NewC: "A \<turnstile>\<^sub>e {\<lambda>s. \<forall>a. new_Addr s = Addr a --> P (Addr a) (new_obj a C s)}
new C {P}"
- Cast: "A |-e {P} e {\<lambda>v s. (case v of Null => True
+| Cast: "A \<turnstile>\<^sub>e {P} e {\<lambda>v s. (case v of Null => True
| Addr a => obj_class s a <=C C) --> Q v s} ==>
- A |-e {P} Cast C e {Q}"
+ A \<turnstile>\<^sub>e {P} Cast C e {Q}"
- Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
- \<forall>a p ls. A |- {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and>
+| Call: "[| A \<turnstile>\<^sub>e {P} e1 {Q}; \<forall>a. A \<turnstile>\<^sub>e {Q a} e2 {R a};
+ \<forall>a p ls. A \<turnstile> {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and>
s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s))}
Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
- A |-e {P} {C}e1..m(e2) {S}"
+ A \<turnstile>\<^sub>e {P} {C}e1..m(e2) {S}"
- Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and>
+| 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>
P s \<and> s' = init_locs D m s}
Impl (D,m) {Q} ==>
- A |- {P} Meth (C,m) {Q}"
+ A \<turnstile> {P} Meth (C,m) {Q}"
--{* @{text "\<Union>Z"} instead of @{text "\<forall>Z"} in the conclusion and\\
Z restricted to type state due to limitations of the inductive package *}
- Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||-
+| Impl: "\<forall>Z::state. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile>
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
- A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
+ A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
--{* structural rules *}
- Asm: " a \<in> A ==> A ||- {a}"
+| Asm: " a \<in> A ==> A |\<turnstile> {a}"
- ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
+| ConjI: " \<forall>c \<in> C. A |\<turnstile> {c} ==> A |\<turnstile> C"
- ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
+| ConjE: "[|A |\<turnstile> C; c \<in> C |] ==> A |\<turnstile> {c}"
--{* Z restricted to type state due to limitations of the inductive package *}
- Conseq:"[| \<forall>Z::state. A |- {P' Z} c {Q' Z};
+| Conseq:"[| \<forall>Z::state. A \<turnstile> {P' Z} c {Q' Z};
\<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
- A |- {P} c {Q }"
+ A \<turnstile> {P} c {Q }"
--{* Z restricted to type state due to limitations of the inductive package *}
- eConseq:"[| \<forall>Z::state. A |-e {P' Z} e {Q' Z};
+| eConseq:"[| \<forall>Z::state. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
\<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
- A |-e {P} e {Q }"
+ A \<turnstile>\<^sub>e {P} e {Q }"
subsection "Fully polymorphic variants, required for Example only"
axioms
- Conseq:"[| \<forall>Z. A |- {P' Z} c {Q' Z};
+ Conseq:"[| \<forall>Z. A \<turnstile> {P' Z} c {Q' Z};
\<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
- A |- {P} c {Q }"
+ A \<turnstile> {P} c {Q }"
- eConseq:"[| \<forall>Z. A |-e {P' Z} e {Q' Z};
+ eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
\<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
- A |-e {P} e {Q }"
+ A \<turnstile>\<^sub>e {P} e {Q }"
- Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) ||-
+ Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile>
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
- A ||- (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
+ A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
subsection "Derived Rules"