# HG changeset patch
# User oheimb
# Date 997382937 -7200
# Node ID 0e66e0114d9a8962e3ac6cf1c0a54bb3da6f7c0d
# Parent  fa8d12b789e12a5ce595962ddb4ffa45935f570c
corrected initialization of locals, streamlined Impl

diff -r fa8d12b789e1 -r 0e66e0114d9a src/HOL/NanoJava/AxSem.thy
--- 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
diff -r fa8d12b789e1 -r 0e66e0114d9a src/HOL/NanoJava/Equivalence.thy
--- 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)
diff -r fa8d12b789e1 -r 0e66e0114d9a src/HOL/NanoJava/OpSem.thy
--- 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
diff -r fa8d12b789e1 -r 0e66e0114d9a src/HOL/NanoJava/State.thy
--- 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.*}
diff -r fa8d12b789e1 -r 0e66e0114d9a src/HOL/NanoJava/Term.thy
--- 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        *)