--- a/src/HOL/NanoJava/AxSem.thy Thu Aug 09 19:33:22 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Thu Aug 09 20:48:57 2001 +0200
@@ -77,19 +77,20 @@
Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
\<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and>
- s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s))}
+ s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(reset_locs s))}
Meth C m {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==>
A |-e {P} {C}e1..m(e2) {S}"
- 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}
- Impl D m {Q} ==>
+ Meth: "\<forall>D. A |- {\<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}"
(*\<Union>z instead of \<forall>z in the conclusion and
z restricted to type state due to limitations of the inductive package *)
- Impl: "A\<union> (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||-
- (\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
- A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
+ Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) ||-
+ (\<lambda>M. (P z M, body M, Q z M))`Ms ==>
+ A ||- (\<lambda>M. (P z M, Impl M, Q z M))`Ms"
(* structural rules *)
@@ -99,14 +100,13 @@
ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}"
- (* z restricted to type state due to limitations of the inductive package *)
Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
- \<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
+ \<forall>s t. (\<forall>z. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
A |- {P} c {Q }"
(* z restricted to type state due to limitations of the inductive package *)
eConseq:"[| \<forall>z::state. A |-e {P' z} c {Q' z};
- \<forall>s v t. (\<forall>z::state. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
+ \<forall>s v t. (\<forall>z. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
A |-e {P} c {Q }"
@@ -147,22 +147,12 @@
lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
by (auto intro: hoare_ehoare.ConjI hoare_ehoare.ConjE)
-lemma Impl':
- "\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||-
- (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
- A ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
-apply (drule Union[THEN iffD2])
+lemma Impl1:
+ "\<lbrakk>\<forall>z::state. A\<union> (\<Union>z. (\<lambda>M. (P z M, Impl M, Q z M))`Ms) |\<turnstile>
+ (\<lambda>M. (P z M, body M, Q z M))`Ms;
+ M \<in> Ms\<rbrakk> \<Longrightarrow>
+ A \<turnstile> {P z M} Impl M {Q z M}"
apply (drule hoare_ehoare.Impl)
-apply (drule Union[THEN iffD1])
-apply (erule spec)
-done
-
-lemma Impl1:
- "\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||-
- (\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms;
- (C,m)\<in> ms\<rbrakk> \<Longrightarrow>
- A |- {P z C m} Impl C m {Q (z::state) C m}"
-apply (drule Impl')
apply (erule Weaken)
apply (auto del: image_eqI intro: rev_image_eqI)
done
--- a/src/HOL/NanoJava/Equivalence.thy Thu Aug 09 19:33:22 2001 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy Thu Aug 09 20:48:57 2001 +0200
@@ -68,10 +68,10 @@
declare exec_elim_cases [elim!] eval_elim_cases [elim!]
-lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl C m,Q)"
+lemma Impl_nvalid_0: "\<Turnstile>0: (P,Impl M,Q)"
by (clarsimp simp add: nvalid_def2)
-lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body C m,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl C m,Q)"
+lemma Impl_nvalid_Suc: "\<Turnstile>n: (P,body M,Q) \<Longrightarrow> \<Turnstile>Suc n: (P,Impl M,Q)"
by (clarsimp simp add: nvalid_def2)
lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
@@ -88,8 +88,8 @@
done
lemma Impl_sound_lemma:
-"\<lbrakk>\<forall>n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (\<Union>z. split (f z) ` ms) (nvalid n);
- (C, m) \<in> ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z C m)"
+"\<lbrakk>\<forall>z n. Ball (A \<union> B) (nvalid n) \<longrightarrow> Ball (f z ` Ms) (nvalid n);
+M\<in>Ms; Ball A (nvalid na); Ball B (nvalid na)\<rbrakk> \<Longrightarrow> nvalid na (f z M)"
by blast
lemma all_conjunct2: "\<forall>l. P' l \<and> P l \<Longrightarrow> \<forall>l. P l"
@@ -124,7 +124,7 @@
apply (tactic "smp_tac 1 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
apply (tactic "smp_tac 2 1", tactic "smp_tac 3 1", tactic "smp_tac 0 1")
apply (tactic "smp_tac 4 1", tactic "smp_tac 2 1", fast)
-apply (clarsimp del: Impl_elim_cases) (* Meth *)
+apply (force del: Impl_elim_cases) (* Meth *)
defer
prefer 4 apply blast (* Conseq *)
prefer 4 apply blast (* eConseq *)
@@ -134,12 +134,16 @@
apply blast
(* Impl *)
apply (rule allI)
+apply (rule_tac x=z in spec)
apply (induct_tac "n")
apply (clarify intro!: Impl_nvalid_0)
apply (clarify intro!: Impl_nvalid_Suc)
apply (drule nvalids_SucD)
+apply (simp only: all_simps)
apply (erule (1) impE)
-apply (drule (4) Impl_sound_lemma)
+apply (drule (2) Impl_sound_lemma)
+apply blast
+apply assumption
done
theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
@@ -204,7 +208,7 @@
apply (blast del: exec_elim_cases)
done
-lemma MGF_lemma: "\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z} \<Longrightarrow>
+lemma MGF_lemma: "\<forall>M z. A |\<turnstile> {MGT (Impl M) z} \<Longrightarrow>
(\<forall>z. A |\<turnstile> {MGT c z}) \<and> (\<forall>z. A |\<turnstile>\<^sub>e MGT\<^sub>e e z)"
apply (simp add: MGT_def MGTe_def)
apply (rule stmt_expr.induct)
@@ -250,7 +254,7 @@
apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
apply blast
-apply blast
+apply (simp add: split_paired_all)
apply (rule eConseq1 [OF hoare_ehoare.NewC])
apply blast
@@ -281,7 +285,7 @@
apply (fast del: Impl_elim_cases)
done
-lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
+lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl M) z}"
apply (unfold MGT_def)
apply (rule Impl1)
apply (rule_tac [2] UNIV_I)
--- a/src/HOL/NanoJava/OpSem.thy Thu Aug 09 19:33:22 2001 +0200
+++ b/src/HOL/NanoJava/OpSem.thy Thu Aug 09 20:48:57 2001 +0200
@@ -54,15 +54,15 @@
s -Cast C e>v-n-> s'"
Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2;
- lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(init_locs C m s2)) -Meth C m-n-> s3
+ lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(reset_locs s2)) -Meth C m-n-> s3
|] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
- Meth: "[| s<This> = Addr a; obj_class s a\<preceq>C C;
- s -Impl (obj_class s a) m-n-> s' |] ==>
+ Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
+ init_locs D m s -Impl (D,m)-n-> s' |] ==>
s -Meth C m-n-> s'"
- Impl: " s -body C m-n-> s' ==>
- s -Impl C m-Suc n-> s'"
+ Impl: " s -body M-n-> s' ==>
+ s -Impl M-Suc n-> s'"
inductive_cases exec_elim_cases':
@@ -73,7 +73,7 @@
"s -x:==e -n\<rightarrow> t"
"s -e1..f:==e2 -n\<rightarrow> t"
inductive_cases Meth_elim_cases: "s -Meth C m-n\<rightarrow> t"
-inductive_cases Impl_elim_cases: "s -Impl C m-n\<rightarrow> t"
+inductive_cases Impl_elim_cases: "s -Impl M-n\<rightarrow> t"
lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
inductive_cases eval_elim_cases:
"s -new C \<succ>v-n\<rightarrow> t"
@@ -115,7 +115,7 @@
apply (drule (1) eval_eval_max, erule thin_rl)
by (fast intro: exec_mono eval_mono le_maxI1 le_maxI2)
-lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl C m-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body C m-n\<rightarrow> t)"
+lemma Impl_body_eq: "(\<lambda>t. \<exists>n. z -Impl M-n\<rightarrow> t) = (\<lambda>t. \<exists>n. z -body M-n\<rightarrow> t)"
apply (rule ext)
apply (fast elim: exec_elim_cases intro: exec_eval.Impl)
done
--- a/src/HOL/NanoJava/State.thy Thu Aug 09 19:33:22 2001 +0200
+++ b/src/HOL/NanoJava/State.thy Thu Aug 09 20:48:57 2001 +0200
@@ -10,8 +10,8 @@
constdefs
- body :: "cname => mname => stmt"
- "body C m \<equiv> bdy (the (method C m))"
+ body :: "imname => stmt"
+ "body \<equiv> \<lambda>(C,m). bdy (the (method C m))"
text {* locations, i.e.\ abstract references to objects *}
typedecl loc
@@ -53,8 +53,11 @@
constdefs
+ reset_locs :: "state => state"
+ "reset_locs s \<equiv> s (| locals := empty |)"
+
init_locs :: "cname => mname => state => state"
- "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m))))|)"
+ "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m)))) |)"
text {* The first parameter of @{term set_locs} is of type @{typ state}
rather than @{typ locals} in order to keep @{typ locals} private.*}
--- a/src/HOL/NanoJava/Term.thy Thu Aug 09 19:33:22 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy Thu Aug 09 20:48:57 2001 +0200
@@ -14,6 +14,7 @@
arities cname :: "term"
vnam :: "term"
mname :: "term"
+types imname = "cname \<times> mname"
datatype vname (* variable for special names *)
= This (* This pointer *)
@@ -29,7 +30,7 @@
| LAss vname expr ("_ :== _" [99, 95] 94) (* local ass. *)
| FAss expr vnam expr ("_.._:==_" [95,99,95] 94) (* field ass. *)
| Meth cname mname (* virtual method *)
- | Impl cname mname (* method implementation *)
+ | Impl imname (* method implementation *)
and expr
= NewC cname ("new _" [ 99] 95) (* object creation *)
| Cast cname expr (* type cast *)