--- 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 }"
--- 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
--- 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;
--- 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"
--- 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
--- 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>