simplified vnam/vname, introduced fname, improved comments
authoroheimb
Mon Sep 10 17:35:22 2001 +0200 (2001-09-10)
changeset 115586539627881e8
parent 11557 66b62cbeaab3
child 11559 65d98faa2182
simplified vnam/vname, introduced fname, improved comments
src/HOL/NanoJava/AxSem.thy
src/HOL/NanoJava/Decl.thy
src/HOL/NanoJava/OpSem.thy
src/HOL/NanoJava/State.thy
src/HOL/NanoJava/Term.thy
src/HOL/NanoJava/TypeRel.thy
     1.1 --- a/src/HOL/NanoJava/AxSem.thy	Mon Sep 10 13:57:57 2001 +0200
     1.2 +++ b/src/HOL/NanoJava/AxSem.thy	Mon Sep 10 17:35:22 2001 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  translations "A |\<turnstile> C"        \<rightleftharpoons> "(A,C) \<in> hoare"
     1.5               "A  \<turnstile> {P}c{Q}"  \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
     1.6               "A |\<turnstile>\<^sub>e t"       \<rightleftharpoons> "(A,t) \<in> ehoare"
     1.7 -             "A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (** shouldn't be necess.**)
     1.8 +             "A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (* shouldn't be necessary *)
     1.9               "A  \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^sub>e (P,e,Q)"
    1.10  
    1.11  
    1.12 @@ -77,7 +77,7 @@
    1.13  
    1.14    Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
    1.15      \<forall>a p l. A |- {\<lambda>s'. \<exists>s. R a p s \<and> l = s \<and> 
    1.16 -                    s' = lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(reset_locs s))}
    1.17 +                    s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(reset_locs s))}
    1.18                    Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs l s)} |] ==>
    1.19               A |-e {P} {C}e1..m(e2) {S}"
    1.20  
    1.21 @@ -86,13 +86,13 @@
    1.22                    Impl (D,m) {Q} ==>
    1.23               A |- {P} Meth (C,m) {Q}"
    1.24  
    1.25 -  (*\<Union>z instead of \<forall>z in the conclusion and
    1.26 -      z restricted to type state due to limitations of the inductive package *)
    1.27 +  --{*\<Union>z instead of \<forall>z in the conclusion and
    1.28 +      z restricted to type state due to limitations of the inductive package *}
    1.29    Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||- 
    1.30                              (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==>
    1.31                        A ||- (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms"
    1.32  
    1.33 -(* structural rules *)
    1.34 +--{* structural rules *}
    1.35  
    1.36    Asm:  "   a \<in> A ==> A ||- {a}"
    1.37  
    1.38 @@ -104,7 +104,7 @@
    1.39               \<forall>s t. (\<forall>z. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
    1.40              A |- {P} c {Q }"
    1.41  
    1.42 -  (* z restricted to type state due to limitations of the inductive package *)
    1.43 +  --{* z restricted to type state due to limitations of the inductive package *}
    1.44   eConseq:"[| \<forall>z::state. A |-e {P' z} c {Q' z};
    1.45               \<forall>s v t. (\<forall>z. P' z s --> Q' z v t) --> (P s --> Q v t) |] ==>
    1.46              A |-e {P} c {Q }"
     2.1 --- a/src/HOL/NanoJava/Decl.thy	Mon Sep 10 13:57:57 2001 +0200
     2.2 +++ b/src/HOL/NanoJava/Decl.thy	Mon Sep 10 17:35:22 2001 +0200
     2.3 @@ -9,34 +9,37 @@
     2.4  theory Decl = Term:
     2.5  
     2.6  datatype ty
     2.7 -  = NT           (* null type  *)
     2.8 -  | Class cname  (* class type *)
     2.9 +  = NT           --{* null type  *}
    2.10 +  | Class cname  --{* class type *}
    2.11  
    2.12 -types	fdecl		(* field declaration *)
    2.13 -	= "vnam \<times> ty"
    2.14 +text{* field declaration *}
    2.15 +types	fdecl		
    2.16 +	= "fname \<times> ty"
    2.17  
    2.18 -record  methd		(* method declaration *)
    2.19 +record  methd		
    2.20  	= par :: ty 
    2.21            res :: ty 
    2.22            lcl ::"(vname \<times> ty) list"
    2.23            bdy :: stmt
    2.24  
    2.25 -types	mdecl    	(* method declaration *)
    2.26 +text{* method declaration *}
    2.27 +types	mdecl
    2.28          = "mname \<times> methd"
    2.29  
    2.30 -record	class		(* class *)
    2.31 +record	class
    2.32  	= super   :: cname
    2.33            fields  ::"fdecl list"
    2.34            methods ::"mdecl list"
    2.35  
    2.36 -types	cdecl		(* class declaration *)
    2.37 +text{* class declaration *}
    2.38 +types	cdecl
    2.39  	= "cname \<times> class"
    2.40  
    2.41  types   prog
    2.42          = "cdecl list"
    2.43  
    2.44  translations
    2.45 -  "fdecl" \<leftharpoondown> (type)"vname \<times> ty"
    2.46 +  "fdecl" \<leftharpoondown> (type)"fname \<times> ty"
    2.47    "mdecl" \<leftharpoondown> (type)"mname \<times> ty \<times> ty \<times> stmt"
    2.48    "class" \<leftharpoondown> (type)"cname \<times> fdecl list \<times> mdecl list"
    2.49    "cdecl" \<leftharpoondown> (type)"cname \<times> class"
    2.50 @@ -44,8 +47,8 @@
    2.51  
    2.52  consts
    2.53  
    2.54 -  Prog    :: prog	(* program as a global value *)
    2.55 -  Object  :: cname	(* name of root class *)
    2.56 +  Prog    :: prog	--{* program as a global value *}
    2.57 +  Object  :: cname	--{* name of root class *}
    2.58  
    2.59  
    2.60  constdefs
     3.1 --- a/src/HOL/NanoJava/OpSem.thy	Mon Sep 10 13:57:57 2001 +0200
     3.2 +++ b/src/HOL/NanoJava/OpSem.thy	Mon Sep 10 17:35:22 2001 +0200
     3.3 @@ -54,7 +54,7 @@
     3.4              s -Cast C e>v-n-> s'"
     3.5  
     3.6    Call: "[| s0 -e1>a-n-> s1; s1 -e2>p-n-> s2; 
     3.7 -            lupd(This\<mapsto>a)(lupd(Param\<mapsto>p)(reset_locs s2)) -Meth (C,m)-n-> s3
     3.8 +            lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(reset_locs s2)) -Meth (C,m)-n-> s3
     3.9       |] ==> s0 -{C}e1..m(e2)>s3<Res>-n-> set_locs s2 s3"
    3.10  
    3.11    Meth: "[| s<This> = Addr a; D = obj_class s a; D\<preceq>C C;
     4.1 --- a/src/HOL/NanoJava/State.thy	Mon Sep 10 13:57:57 2001 +0200
     4.2 +++ b/src/HOL/NanoJava/State.thy	Mon Sep 10 17:35:22 2001 +0200
     4.3 @@ -17,17 +17,17 @@
     4.4  typedecl loc 
     4.5  
     4.6  datatype val
     4.7 -  = Null        (* null reference *)
     4.8 -  | Addr loc    (* address, i.e. location of object *)
     4.9 +  = Null        --{* null reference *}
    4.10 +  | Addr loc    --{* address, i.e. location of object *}
    4.11  
    4.12  types	fields
    4.13 -	= "(vnam \<leadsto> val)"
    4.14 +	= "(fname \<leadsto> val)"
    4.15  
    4.16          obj = "cname \<times> fields"
    4.17  
    4.18  translations
    4.19  
    4.20 -  "fields" \<leftharpoondown> (type)"vnam \<Rightarrow> val option"
    4.21 +  "fields" \<leftharpoondown> (type)"fname => val option"
    4.22    "obj"    \<leftharpoondown> (type)"cname \<times> fields"
    4.23  
    4.24  constdefs
    4.25 @@ -67,35 +67,33 @@
    4.26    get_local     :: "state => vname => val" ("_<_>" [99,0] 99)
    4.27   "get_local s x  \<equiv> the (locals s x)"
    4.28  
    4.29 -(* local function: *)
    4.30 +--{* local function: *}
    4.31    get_obj       :: "state => loc => obj"
    4.32   "get_obj s a \<equiv> the (heap s a)"
    4.33  
    4.34    obj_class     :: "state => loc => cname"
    4.35   "obj_class s a \<equiv> fst (get_obj s a)"
    4.36  
    4.37 -  get_field     :: "state => loc => vnam => val"
    4.38 +  get_field     :: "state => loc => fname => val"
    4.39   "get_field s a f \<equiv> the (snd (get_obj s a) f)"
    4.40  
    4.41 +--{* local function: *}
    4.42 +  hupd       :: "loc => obj => state => state"   ("hupd'(_|->_')" [10,10] 1000)
    4.43 + "hupd a obj s \<equiv> s (| heap   := ((heap   s)(a\<mapsto>obj))|)"
    4.44 +
    4.45 +  lupd       :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000)
    4.46 + "lupd x v s   \<equiv> s (| locals := ((locals s)(x\<mapsto>v  ))|)"
    4.47 +
    4.48 +syntax (xsymbols)
    4.49 +  hupd       :: "loc => obj => state => state"   ("hupd'(_\<mapsto>_')" [10,10] 1000)
    4.50 +  lupd       :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
    4.51 +
    4.52  constdefs
    4.53  
    4.54 -(* local function: *)
    4.55 -  hupd       :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state"   ("hupd'(_|->_')" [10,10] 1000)
    4.56 - "hupd a obj s \<equiv> s (| heap   := ((heap   s)(a\<mapsto>obj))|)"
    4.57 -
    4.58 -  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_|->_')" [10,10] 1000)
    4.59 - "lupd x v s   \<equiv> s (| locals := ((locals s)(x\<mapsto>v  ))|)"
    4.60 -
    4.61 -syntax (xsymbols)
    4.62 -  hupd       :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state"   ("hupd'(_\<mapsto>_')" [10,10] 1000)
    4.63 -  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
    4.64 -
    4.65 -constdefs
    4.66 -
    4.67 -  new_obj    :: "loc \<Rightarrow> cname \<Rightarrow> state \<Rightarrow> state"
    4.68 +  new_obj    :: "loc => cname => state => state"
    4.69   "new_obj a C   \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))"
    4.70  
    4.71 -  upd_obj    :: "loc \<Rightarrow> vnam \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
    4.72 +  upd_obj    :: "loc => fname => val => state => state"
    4.73   "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s"
    4.74  
    4.75    new_Addr	:: "state => val"
     5.1 --- a/src/HOL/NanoJava/Term.thy	Mon Sep 10 13:57:57 2001 +0200
     5.2 +++ b/src/HOL/NanoJava/Term.thy	Mon Sep 10 17:35:22 2001 +0200
     5.3 @@ -8,32 +8,40 @@
     5.4  
     5.5  theory Term = Main:
     5.6  
     5.7 -typedecl cname  (* class name *)
     5.8 -typedecl vnam   (* variable or field name *)
     5.9 -typedecl mname  (* method name *)
    5.10 +typedecl cname  --{* class    name *}
    5.11 +typedecl mname  --{* method   name *}
    5.12 +typedecl fname  --{* field    name *}
    5.13 +typedecl vname  --{* variable name *}
    5.14  
    5.15 -datatype vname  (* variable for special names *)
    5.16 -  = This        (* This pointer *)
    5.17 -  | Param       (* method parameter *)
    5.18 -  | Res         (* method result *)
    5.19 -  | VName vnam 
    5.20 +consts 
    5.21 +  This :: vname --{* This pointer *}
    5.22 +  Par  :: vname --{* method parameter *}
    5.23 +  Res  :: vname --{* method result *}
    5.24 +
    5.25 +text {* Inequality axioms not required here *}
    5.26 +(*
    5.27 +axioms
    5.28 +  This_neq_Par [simp]: "This \<noteq> Par"
    5.29 +  Par_neq_Res  [simp]: "Par \<noteq> Res"
    5.30 +  Res_neq_This [simp]: "Res \<noteq> This"
    5.31 +*)
    5.32  
    5.33  datatype stmt
    5.34 -  = Skip                   (* empty statement *)
    5.35 +  = Skip                   --{* empty statement *}
    5.36    | Comp       stmt stmt   ("_;; _"             [91,90   ] 90)
    5.37    | Cond expr  stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
    5.38    | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
    5.39 -  | LAss vname expr        ("_ :== _"           [99,   95] 94) (* local ass. *)
    5.40 -  | FAss expr  vnam expr   ("_.._:==_"          [95,99,95] 94) (* field ass. *)
    5.41 -  | Meth "cname \<times> mname"   (* virtual method *)
    5.42 -  | Impl "cname \<times> mname"   (* method implementation *)
    5.43 +  | LAss vname expr        ("_ :== _"           [99,   95] 94) --{* local ass.*}
    5.44 +  | FAss expr  fname expr  ("_.._:==_"          [95,99,95] 94) --{* field ass.*}
    5.45 +  | Meth "cname \<times> mname"   --{* virtual method *}
    5.46 +  | Impl "cname \<times> mname"   --{* method implementation *}
    5.47  and expr
    5.48 -  = NewC cname       ("new _"        [   99] 95) (* object creation  *)
    5.49 -  | Cast cname expr                              (* type cast        *)
    5.50 -  | LAcc vname                                   (* local access     *)
    5.51 -  | FAcc expr  vnam  ("_.._"         [95,99] 95) (* field access     *)
    5.52 -  | Call cname expr mname expr                   (* method call      *)
    5.53 -                     ("{_}_.._'(_')" [99,95,99,95] 95)
    5.54 +  = NewC cname       ("new _"        [   99] 95) --{* object creation  *}
    5.55 +  | Cast cname expr                              --{* type cast        *}
    5.56 +  | LAcc vname                                   --{* local access     *}
    5.57 +  | FAcc expr  fname ("_.._"         [95,99] 95) --{* field access     *}
    5.58 +  | Call cname expr mname expr                   
    5.59 +                     ("{_}_.._'(_')" [99,95,99,95] 95) --{* method call *}
    5.60  
    5.61  end
    5.62  
     6.1 --- a/src/HOL/NanoJava/TypeRel.thy	Mon Sep 10 13:57:57 2001 +0200
     6.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Mon Sep 10 17:35:22 2001 +0200
     6.3 @@ -9,8 +9,8 @@
     6.4  theory TypeRel = Decl:
     6.5  
     6.6  consts
     6.7 -  widen   :: "(ty    \<times> ty   ) set"  (* widening *)
     6.8 -  subcls1 :: "(cname \<times> cname) set"  (* subclass *)
     6.9 +  widen   :: "(ty    \<times> ty   ) set"  --{* widening *}
    6.10 +  subcls1 :: "(cname \<times> cname) set"  --{* subclass *}
    6.11  
    6.12  syntax (xsymbols)
    6.13    widen   :: "[ty   , ty   ] => bool" ("_ \<preceq> _"    [71,71] 70)
    6.14 @@ -28,17 +28,17 @@
    6.15  
    6.16  consts
    6.17    method :: "cname => (mname \<leadsto> methd)"
    6.18 -  field  :: "cname => (vnam  \<leadsto> ty)"
    6.19 +  field  :: "cname => (fname \<leadsto> ty)"
    6.20  
    6.21  
    6.22  text {* The rest of this theory is not actually used. *}
    6.23  
    6.24 +text{* direct subclass relation *}
    6.25  defs
    6.26 -  (* direct subclass relation *)
    6.27   subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
    6.28 -  
    6.29 -inductive widen intros (*widening, viz. method invocation conversion,
    6.30 -			           i.e. sort of syntactic subtyping *)
    6.31 +
    6.32 +text{* widening, viz. method invocation conversion *}
    6.33 +inductive widen intros 
    6.34    refl   [intro!, simp]:           "T \<preceq> T"
    6.35    subcls         : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
    6.36    null   [intro!]:                "NT \<preceq> R"
    6.37 @@ -121,7 +121,7 @@
    6.38  apply simp
    6.39  done
    6.40  
    6.41 -(* methods of a class, with inheritance and hiding *)
    6.42 +--{* methods of a class, with inheritance and hiding *}
    6.43  defs method_def: "method C \<equiv> class_rec C methods"
    6.44  
    6.45  lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
    6.46 @@ -132,7 +132,7 @@
    6.47  done
    6.48  
    6.49  
    6.50 -(* fields of a class, with inheritance and hiding *)
    6.51 +--{* fields of a class, with inheritance and hiding *}
    6.52  defs field_def: "field C \<equiv> class_rec C fields"
    6.53  
    6.54  lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>