# HG changeset patch
# User oheimb
# Date 999179250 -7200
# Node ID 4b32a46ffd2923fc7d76a4d600a74a750d165488
# Parent  244a02a2968bd9ce6b48e15e8979a48d7fcd4399
removed imname, uncurried Meth

diff -r 244a02a2968b -r 4b32a46ffd29 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Wed Aug 29 21:17:24 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Thu Aug 30 15:47:30 2001 +0200
@@ -78,13 +78,13 @@
   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)(reset_locs s))}
-                  Meth C m {\<lambda>s. S (s<Res>) (set_locs l 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>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 |- {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 *)
diff -r 244a02a2968b -r 4b32a46ffd29 src/HOL/NanoJava/Equivalence.thy
--- a/src/HOL/NanoJava/Equivalence.thy	Wed Aug 29 21:17:24 2001 +0200
+++ b/src/HOL/NanoJava/Equivalence.thy	Thu Aug 30 15:47:30 2001 +0200
@@ -249,6 +249,7 @@
 apply (drule (1) eval_eval_max)
 apply blast
 
+apply (simp only: split_paired_all)
 apply (rule hoare_ehoare.Meth)
 apply (rule allI)
 apply (drule spec, drule spec, erule hoare_ehoare.Conseq)
diff -r 244a02a2968b -r 4b32a46ffd29 src/HOL/NanoJava/OpSem.thy
--- a/src/HOL/NanoJava/OpSem.thy	Wed Aug 29 21:17:24 2001 +0200
+++ b/src/HOL/NanoJava/OpSem.thy	Thu Aug 30 15:47:30 2001 +0200
@@ -54,12 +54,12 @@
             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)(reset_locs 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; 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'"
+            s -Meth (C,m)-n-> s'"
 
   Impl: "   s -body M-n-> s' ==>
             s -Impl M-Suc n-> s'"
@@ -72,8 +72,8 @@
 				  "s -While(x) c      -n\<rightarrow> t"
 				  "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   M-n\<rightarrow> t"
+inductive_cases Meth_elim_cases:  "s -Meth Cm-n\<rightarrow> t"
+inductive_cases Impl_elim_cases:  "s -Impl Cm-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"
diff -r 244a02a2968b -r 4b32a46ffd29 src/HOL/NanoJava/State.thy
--- a/src/HOL/NanoJava/State.thy	Wed Aug 29 21:17:24 2001 +0200
+++ b/src/HOL/NanoJava/State.thy	Thu Aug 30 15:47:30 2001 +0200
@@ -10,7 +10,7 @@
 
 constdefs
 
-  body :: "imname => stmt"
+  body :: "cname \<times> mname => stmt"
  "body \<equiv> \<lambda>(C,m). bdy (the (method C m))"
 
 text {* locations, i.e.\ abstract references to objects *}
diff -r 244a02a2968b -r 4b32a46ffd29 src/HOL/NanoJava/Term.thy
--- a/src/HOL/NanoJava/Term.thy	Wed Aug 29 21:17:24 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy	Thu Aug 30 15:47:30 2001 +0200
@@ -11,7 +11,6 @@
 typedecl cname  (* class name *)
 typedecl vnam   (* variable or field name *)
 typedecl mname  (* method name *)
-types   imname = "cname \<times> mname"
 
 datatype vname  (* variable for special names *)
   = This        (* This pointer *)
@@ -26,8 +25,8 @@
   | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
   | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
   | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
-  | Meth cname mname       (* virtual method *)
-  | Impl      imname       (* method implementation *)
+  | Meth "cname \<times> mname"   (* virtual method *)
+  | Impl "cname \<times> mname"   (* method implementation *)
 and expr
   = NewC cname       ("new _"        [   99] 95) (* object creation  *)
   | Cast cname expr                              (* type cast        *)
diff -r 244a02a2968b -r 4b32a46ffd29 src/HOL/NanoJava/document/root.bib
--- a/src/HOL/NanoJava/document/root.bib	Wed Aug 29 21:17:24 2001 +0200
+++ b/src/HOL/NanoJava/document/root.bib	Thu Aug 30 15:47:30 2001 +0200
@@ -30,6 +30,8 @@
         title = {Hoare Logic for {J}ava in {Isabelle/HOL}},
         journal = {Concurrency: Practice and Experience},
         year = {2001},
+        volume = 598,
+        pages = {??--??+43},
         url = {http://www4.in.tum.de/papers/DvO-CPE01.html},
         abstract = {
 This article presents a Hoare-style calculus for a substantial subset