# HG changeset patch
# User oheimb
# Date 1000136122 -7200
# Node ID 6539627881e86e3be4aba3d07fa3e232fab85f0f
# Parent  66b62cbeaab35e24501b0b5dd2ee42e0ef9a4da8
simplified vnam/vname, introduced fname, improved comments

diff -r 66b62cbeaab3 -r 6539627881e8 src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Mon Sep 10 13:57:57 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Mon Sep 10 17:35:22 2001 +0200
@@ -38,7 +38,7 @@
 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 necess.**)
+             "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)"
 
 
@@ -77,7 +77,7 @@
 
   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))}
+                    s' = lupd(This\<mapsto>a)(lupd(Par\<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}"
 
@@ -86,13 +86,13 @@
                   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 *)
+  --{*\<Union>z instead of \<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) ||- 
                             (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==>
                       A ||- (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms"
 
-(* structural rules *)
+--{* structural rules *}
 
   Asm:  "   a \<in> A ==> A ||- {a}"
 
@@ -104,7 +104,7 @@
              \<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 *)
+  --{* 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. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
             A |-e {P} c {Q }"
diff -r 66b62cbeaab3 -r 6539627881e8 src/HOL/NanoJava/Decl.thy
--- a/src/HOL/NanoJava/Decl.thy	Mon Sep 10 13:57:57 2001 +0200
+++ b/src/HOL/NanoJava/Decl.thy	Mon Sep 10 17:35:22 2001 +0200
@@ -9,34 +9,37 @@
 theory Decl = Term:
 
 datatype ty
-  = NT           (* null type  *)
-  | Class cname  (* class type *)
+  = NT           --{* null type  *}
+  | Class cname  --{* class type *}
 
-types	fdecl		(* field declaration *)
-	= "vnam \<times> ty"
+text{* field declaration *}
+types	fdecl		
+	= "fname \<times> ty"
 
-record  methd		(* method declaration *)
+record  methd		
 	= par :: ty 
           res :: ty 
           lcl ::"(vname \<times> ty) list"
           bdy :: stmt
 
-types	mdecl    	(* method declaration *)
+text{* method declaration *}
+types	mdecl
         = "mname \<times> methd"
 
-record	class		(* class *)
+record	class
 	= super   :: cname
           fields  ::"fdecl list"
           methods ::"mdecl list"
 
-types	cdecl		(* class declaration *)
+text{* class declaration *}
+types	cdecl
 	= "cname \<times> class"
 
 types   prog
         = "cdecl list"
 
 translations
-  "fdecl" \<leftharpoondown> (type)"vname \<times> ty"
+  "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
   "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
   "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
   "cdecl" \<leftharpoondown> (type)"cname \<times> class"
@@ -44,8 +47,8 @@
 
 consts
 
-  Prog    :: prog	(* program as a global value *)
-  Object  :: cname	(* name of root class *)
+  Prog    :: prog	--{* program as a global value *}
+  Object  :: cname	--{* name of root class *}
 
 
 constdefs
diff -r 66b62cbeaab3 -r 6539627881e8 src/HOL/NanoJava/OpSem.thy
--- a/src/HOL/NanoJava/OpSem.thy	Mon Sep 10 13:57:57 2001 +0200
+++ b/src/HOL/NanoJava/OpSem.thy	Mon Sep 10 17:35:22 2001 +0200
@@ -54,7 +54,7 @@
             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(Par\<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;
diff -r 66b62cbeaab3 -r 6539627881e8 src/HOL/NanoJava/State.thy
--- a/src/HOL/NanoJava/State.thy	Mon Sep 10 13:57:57 2001 +0200
+++ b/src/HOL/NanoJava/State.thy	Mon Sep 10 17:35:22 2001 +0200
@@ -17,17 +17,17 @@
 typedecl loc 
 
 datatype val
-  = Null        (* null reference *)
-  | Addr loc    (* address, i.e. location of object *)
+  = Null        --{* null reference *}
+  | Addr loc    --{* address, i.e. location of object *}
 
 types	fields
-	= "(vnam \<leadsto> val)"
+	= "(fname \<leadsto> val)"
 
         obj = "cname \<times> fields"
 
 translations
 
-  "fields" \<leftharpoondown> (type)"vnam \<Rightarrow> val option"
+  "fields" \<leftharpoondown> (type)"fname => val option"
   "obj"    \<leftharpoondown> (type)"cname \<times> fields"
 
 constdefs
@@ -67,35 +67,33 @@
   get_local     :: "state => vname => val" ("_<_>" [99,0] 99)
  "get_local s x  \<equiv> the (locals s x)"
 
-(* local function: *)
+--{* local function: *}
   get_obj       :: "state => loc => obj"
  "get_obj s a \<equiv> the (heap s a)"
 
   obj_class     :: "state => loc => cname"
  "obj_class s a \<equiv> fst (get_obj s a)"
 
-  get_field     :: "state => loc => vnam => val"
+  get_field     :: "state => loc => fname => val"
  "get_field s a f \<equiv> the (snd (get_obj s a) f)"
 
+--{* local function: *}
+  hupd       :: "loc => obj => state => state"   ("hupd'(_|->_')" [10,10] 1000)
+ "hupd a obj s \<equiv> s (| heap   := ((heap   s)(a\<mapsto>obj))|)"
+
+  lupd       :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000)
+ "lupd x v s   \<equiv> s (| locals := ((locals s)(x\<mapsto>v  ))|)"
+
+syntax (xsymbols)
+  hupd       :: "loc => obj => state => state"   ("hupd'(_\<mapsto>_')" [10,10] 1000)
+  lupd       :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
+
 constdefs
 
-(* local function: *)
-  hupd       :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state"   ("hupd'(_|->_')" [10,10] 1000)
- "hupd a obj s \<equiv> s (| heap   := ((heap   s)(a\<mapsto>obj))|)"
-
-  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_|->_')" [10,10] 1000)
- "lupd x v s   \<equiv> s (| locals := ((locals s)(x\<mapsto>v  ))|)"
-
-syntax (xsymbols)
-  hupd       :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state"   ("hupd'(_\<mapsto>_')" [10,10] 1000)
-  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
-
-constdefs
-
-  new_obj    :: "loc \<Rightarrow> cname \<Rightarrow> state \<Rightarrow> state"
+  new_obj    :: "loc => cname => state => state"
  "new_obj a C   \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))"
 
-  upd_obj    :: "loc \<Rightarrow> vnam \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
+  upd_obj    :: "loc => fname => val => state => state"
  "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s"
 
   new_Addr	:: "state => val"
diff -r 66b62cbeaab3 -r 6539627881e8 src/HOL/NanoJava/Term.thy
--- a/src/HOL/NanoJava/Term.thy	Mon Sep 10 13:57:57 2001 +0200
+++ b/src/HOL/NanoJava/Term.thy	Mon Sep 10 17:35:22 2001 +0200
@@ -8,32 +8,40 @@
 
 theory Term = Main:
 
-typedecl cname  (* class name *)
-typedecl vnam   (* variable or field name *)
-typedecl mname  (* method name *)
+typedecl cname  --{* class    name *}
+typedecl mname  --{* method   name *}
+typedecl fname  --{* field    name *}
+typedecl vname  --{* variable name *}
 
-datatype vname  (* variable for special names *)
-  = This        (* This pointer *)
-  | Param       (* method parameter *)
-  | Res         (* method result *)
-  | VName vnam 
+consts 
+  This :: vname --{* This pointer *}
+  Par  :: vname --{* method parameter *}
+  Res  :: vname --{* method result *}
+
+text {* Inequality axioms not required here *}
+(*
+axioms
+  This_neq_Par [simp]: "This \<noteq> Par"
+  Par_neq_Res  [simp]: "Par \<noteq> Res"
+  Res_neq_This [simp]: "Res \<noteq> This"
+*)
 
 datatype stmt
-  = Skip                   (* empty statement *)
+  = Skip                   --{* empty statement *}
   | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
   | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
   | 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 \<times> mname"   (* virtual method *)
-  | Impl "cname \<times> mname"   (* method implementation *)
+  | LAss vname expr        ("_ :== _"           [99,   95] 94) --{* local ass.*}
+  | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) --{* field ass.*}
+  | 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        *)
-  | LAcc vname                                   (* local access     *)
-  | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)
-  | Call cname expr mname expr                   (* method call      *)
-                     ("{_}_.._'(_')" [99,95,99,95] 95)
+  = NewC cname       ("new _"        [   99] 95) --{* object creation  *}
+  | Cast cname expr                              --{* type cast        *}
+  | LAcc vname                                   --{* local access     *}
+  | FAcc expr  fname ("_.._"         [95,99] 95) --{* field access     *}
+  | Call cname expr mname expr                   
+                     ("{_}_.._'(_')" [99,95,99,95] 95) --{* method call *}
 
 end
 
diff -r 66b62cbeaab3 -r 6539627881e8 src/HOL/NanoJava/TypeRel.thy
--- a/src/HOL/NanoJava/TypeRel.thy	Mon Sep 10 13:57:57 2001 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy	Mon Sep 10 17:35:22 2001 +0200
@@ -9,8 +9,8 @@
 theory TypeRel = Decl:
 
 consts
-  widen   :: "(ty    \<times> ty   ) set"  (* widening *)
-  subcls1 :: "(cname \<times> cname) set"  (* subclass *)
+  widen   :: "(ty    \<times> ty   ) set"  --{* widening *}
+  subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
 
 syntax (xsymbols)
   widen   :: "[ty   , ty   ] => bool" ("_ \<preceq> _"    [71,71] 70)
@@ -28,17 +28,17 @@
 
 consts
   method :: "cname => (mname \<leadsto> methd)"
-  field  :: "cname => (vnam  \<leadsto> ty)"
+  field  :: "cname => (fname \<leadsto> ty)"
 
 
 text {* The rest of this theory is not actually used. *}
 
+text{* direct subclass relation *}
 defs
-  (* direct subclass relation *)
  subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
-  
-inductive widen intros (*widening, viz. method invocation conversion,
-			           i.e. sort of syntactic subtyping *)
+
+text{* widening, viz. method invocation conversion *}
+inductive widen intros 
   refl   [intro!, simp]:           "T \<preceq> T"
   subcls         : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
   null   [intro!]:                "NT \<preceq> R"
@@ -121,7 +121,7 @@
 apply simp
 done
 
-(* methods of a class, with inheritance and hiding *)
+--{* methods of a class, with inheritance and hiding *}
 defs method_def: "method C \<equiv> class_rec C methods"
 
 lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
@@ -132,7 +132,7 @@
 done
 
 
-(* fields of a class, with inheritance and hiding *)
+--{* fields of a class, with inheritance and hiding *}
 defs field_def: "field C \<equiv> class_rec C fields"
 
 lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>