# HG changeset patch
# User oheimb
# Date 992714802 -7200
# Node ID bf98ad1c22c6415ed2718fe991abae368214dd81
# Parent  a6730c90e75365e801ef8bd5f7150c72fc3cfbe0
added NanoJava

diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jun 13 16:30:12 2001 +0200
+++ b/src/HOL/IsaMakefile	Sat Jun 16 20:06:42 2001 +0200
@@ -31,6 +31,7 @@
   HOL-MicroJava \
   HOL-MiniML \
   HOL-Modelcheck \
+  HOL-NanoJava \
   HOL-NumberTheory \
   HOL-Prolog \
   HOL-Subst \
@@ -460,6 +461,15 @@
   MicroJava/document/root.bib MicroJava/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/HOL MicroJava
 
+## HOL-NanoJava
+
+HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
+
+$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
+  NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
+  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
+  NanoJava/document/root.bib NanoJava/document/root.tex
+	@$(ISATOOL) usedir $(OUT)/HOL NanoJava
 
 ## HOL-CTL
 
@@ -581,7 +591,7 @@
 ## clean
 
 clean:
-	@rm -f $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
+	@rm -f  $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/TLA \
 		$(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
 		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
 		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
@@ -589,8 +599,8 @@
 		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
 		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
 		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
-		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
-		$(LOG)/HOL-CTL.gz $(LOG)/HOL-MicroJava.gz \
+		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-CTL.gz \
+		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
 		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
 		$(LOG)/HOL-Lattice $(LOG)/HOL-Real-ex.gz \
 		$(LOG)/HOL-Real-HahnBanach.gz $(LOG)/TLA-Inc.gz \
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/AxSem.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/AxSem.thy	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,122 @@
+(*  Title:      HOL/NanoJava/AxSem.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   2001 Technische Universitaet Muenchen
+*)
+
+header "Axiomatic Semantics (Hoare Logic)"
+
+theory AxSem = State:
+
+types assn   = "state => bool"
+      triple = "assn \<times> stmt \<times> assn"
+translations
+  "assn"   \<leftharpoondown> (type)"state => bool"
+  "triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
+
+consts   hoare   :: "(triple set \<times> triple set) set"
+syntax (xsymbols)
+ "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ |\<turnstile>/ _" [61,61]    60)
+ "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
+                                   ("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
+syntax
+ "@hoare"  :: "[triple set,  triple set    ] => bool" ("_ ||-/ _" [61,61] 60)
+ "@hoare1" :: "[triple set,  assn,stmt,assn] => bool" 
+                                  ("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
+
+translations "A |\<turnstile> C"       \<rightleftharpoons> "(A,C) \<in> hoare"
+             "A  \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
+
+inductive hoare
+intros
+
+  Skip:  "A |- {P} Skip {P}"
+
+  Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
+
+  Cond: "[| A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c1 {Q}; 
+            A |- {\<lambda>s. P s \<and> s<e> = Null} c2 {Q}  |] ==>
+            A |- {P} If(e) c1 Else c2 {Q}"
+
+  Loop: "A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c {P} ==>
+         A |- {P} While(e) c {\<lambda>s. P s \<and> s<e> = Null}"
+
+  NewC: "A |- {\<lambda>s.\<forall>a. new_Addr s=Addr a--> P (lupd(x|->Addr a)(new_obj a C s))}
+              x:=new C {P}"
+
+  Cast: "A |- {\<lambda>s.(case s<y> of Null=> True | Addr a=> obj_class s a <=C C) -->
+              P (lupd(x|->s<y>) s)} x:=(C)y {P}"
+
+  FAcc: "A |- {\<lambda>s.\<forall>a. s<y>=Addr a-->P(lupd(x|->get_field s a f) s)} x:=y..f{P}"
+
+  FAss: "A |- {\<lambda>s. \<forall>a. s<y>=Addr a --> P (upd_obj a f (s<x>) s)} y..f:=x {P}"
+
+  Call: "\<forall>l. A |- {\<lambda>s'. \<exists>s. P s \<and> l = s \<and> 
+                    s' = lupd(This|->s<y>)(lupd(Param|->s<p>)(init_locs C m s))}
+                  Meth C m {\<lambda>s. Q (lupd(x|->s<Res>)(set_locs l s))} ==>
+             A |- {P} x:={C}y..m(p) {Q}"
+
+  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} ==>
+             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 paackage *)
+  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)"
+
+(* structural rules *)
+
+  (* z restricted to type state due to limitations of the inductive paackage *)
+  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) |] ==>
+            A |- {P} c {Q }"
+
+  Asm:  "   a \<in> A ==> A ||- {a}"
+
+  ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
+
+  ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}";
+
+
+subsection "Derived Rules"
+
+lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
+apply (rule hoare.Conseq)
+apply  (rule allI, assumption)
+apply fast
+done
+
+lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
+apply (rule hoare.ConjI)
+apply clarify
+apply (drule hoare.ConjE)
+apply  fast
+apply assumption
+done
+
+lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
+by (auto intro: hoare.ConjI hoare.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])
+apply (drule hoare.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    \<turnstile> {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
+
+end
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/Decl.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/Decl.thy	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,68 @@
+(*  Title:      HOL/NanoJava/Decl.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   2001 Technische Universitaet Muenchen
+*)
+
+header "Types, class Declarations, and whole programs"
+
+theory Decl = Term:
+
+datatype ty
+  = NT           (* null type  *)
+  | Class cname  (* class type *)
+
+types	fdecl		(* field declaration *)
+	= "vnam \<times> ty"
+
+
+record  methd		(* method declaration *)
+	= par :: ty 
+          res :: ty 
+          lcl ::"(vname \<times> ty) list"
+          bdy :: stmt
+
+types	mdecl    	(* method declaration *)
+        = "mname \<times> methd"
+
+record	class		(* class *)
+	= super   :: cname
+          fields  ::"fdecl list"
+          methods ::"mdecl list"
+
+types	cdecl		(* class declaration *)
+	= "cname \<times> class"
+
+types   prog
+        = "cdecl list"
+
+translations
+  "fdecl" \<leftharpoondown> (type)"vname \<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"
+  "prog " \<leftharpoondown> (type)"cdecl list"
+
+consts
+
+  Prog    :: prog	(* program as a global value *)
+
+consts
+
+  Object  :: cname	(* name of root class *)
+
+
+constdefs
+  class	     :: "cname \<leadsto> class"
+ "class      \<equiv> map_of Prog"
+
+  is_class   :: "cname => bool"
+ "is_class C \<equiv> class C \<noteq> None"
+
+lemma finite_is_class: "finite {C. is_class C}"
+apply (unfold is_class_def class_def)
+apply (fold dom_def)
+apply (rule finite_dom_map_of)
+done
+
+end
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/Equivalence.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/Equivalence.thy	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,237 @@
+(*  Title:      HOL/NanoJava/Equivalence.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   2001 Technische Universitaet Muenchen
+*)
+
+header "Equivalence of Operational and Axiomatic Semantics"
+
+theory Equivalence = OpSem + AxSem:
+
+subsection "Validity"
+
+constdefs
+  valid   :: "[assn,stmt,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
+ "|= {P} c {Q} \<equiv> \<forall>s t. P s --> (\<exists>n. s -c-n-> t) --> Q t"
+
+ nvalid   :: "[nat,       triple    ] => bool" ("|=_: _"  [61,61] 60)
+ "|=n: t \<equiv> let (P,c,Q) = t in \<forall>s t. s -c-n-> t --> P s --> Q t"
+
+ nvalids  :: "[nat,       triple set] => bool" ("||=_: _" [61,61] 60)
+ "||=n: T \<equiv> \<forall>t\<in>T. |=n: t"
+
+ cnvalids :: "[triple set,triple set] => bool" ("_ ||=/ _"[61,61] 60)
+ "A ||= C \<equiv> \<forall>n. ||=n: A --> ||=n: C"
+
+syntax (xsymbols)
+  valid   :: "[assn,stmt,assn] => bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" [3,90,3] 60)
+ nvalid   :: "[nat,       triple    ] => bool" ("\<Turnstile>_: _"   [61,61] 60)
+ nvalids  :: "[nat,       triple set] => bool" ("|\<Turnstile>_: _"  [61,61] 60)
+ cnvalids :: "[triple set,triple set] => bool" ("_ |\<Turnstile>/ _" [61,61] 60)
+
+syntax
+  nvalid1::"[nat,        assn,stmt,assn] => bool" ( "|=_:.{(1_)}/ (_)/ {(1_)}"
+                                                         [61,3,90,3] 60)
+ cnvalid1::"[triple set, assn,stmt,assn] => bool" ("_ ||=.{(1_)}/ (_)/ {(1_)}"
+                                                         [61,3,90,3] 60)
+syntax (xsymbols)
+  nvalid1::"[nat,        assn,stmt,assn] => bool" (  "\<Turnstile>_:.{(1_)}/ (_)/ {(1_)}"
+                                                         [61,3,90,3] 60)
+ cnvalid1::"[triple set, assn,stmt,assn] => bool" ( "_ |\<Turnstile>.{(1_)}/ (_)/ {(1_)}"
+                                                         [61,3,90,3] 60)
+translations
+ " \<Turnstile>n:.{P} c {Q}" \<rightleftharpoons> " \<Turnstile>n:  (P,c,Q)"
+ "A |\<Turnstile>.{P} c {Q}" \<rightleftharpoons> "A |\<Turnstile> {(P,c,Q)}"
+
+lemma nvalid1_def2: "\<Turnstile>n:.{P} c {Q} \<equiv> \<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t"
+by (simp add: nvalid_def Let_def)
+
+lemma cnvalid1_def2: 
+  "A |\<Turnstile>.{P} c {Q} \<equiv> \<forall>n. |\<Turnstile>n: A \<longrightarrow> (\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)"
+by(simp add: nvalid1_def2 nvalids_def cnvalids_def)
+
+lemma valid_def2: "\<Turnstile> {P} c {Q} = (\<forall>n. \<Turnstile>n:.{P} c {Q})"
+apply (simp add: valid_def nvalid1_def2)
+apply blast
+done
+
+
+subsection "Soundness"
+
+declare exec_elim_cases [elim!]
+
+lemma Impl_nvalid_0: "\<Turnstile>0:.{P} Impl C m {Q}"
+by (clarsimp simp add: nvalid1_def2)
+
+lemma Impl_nvalid_Suc: "\<Turnstile>n:.{P} body C m {Q} \<Longrightarrow> \<Turnstile>Suc n:.{P} Impl C m {Q}"
+by (clarsimp simp add: nvalid1_def2)
+
+lemma nvalid_SucD: "\<And>t. \<Turnstile>Suc n:t \<Longrightarrow> \<Turnstile>n:t"
+by (force simp add: split_paired_all nvalid1_def2 intro: exec_mono)
+
+lemma nvalids_SucD: "Ball A (nvalid (Suc n)) \<Longrightarrow>  Ball A (nvalid n)"
+by (fast intro: nvalid_SucD)
+
+lemma Loop_sound_lemma [rule_format (no_asm)]: 
+"\<lbrakk>\<forall>s t. s -c-n\<rightarrow> t \<longrightarrow> P s \<and> s<e> \<noteq> Null \<longrightarrow> P t; s -c0-n0\<rightarrow> t\<rbrakk> \<Longrightarrow> 
+  P s \<longrightarrow> c0 = While (e) c \<longrightarrow> n0 = n \<longrightarrow> P t \<and> t<e> = Null"
+apply (erule exec.induct)
+apply clarsimp+
+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)"
+by blast
+
+lemma hoare_sound_main: "A |\<turnstile> C \<Longrightarrow> A |\<Turnstile> C"
+apply (erule hoare.induct)
+apply (simp_all only: cnvalid1_def2)
+apply clarsimp
+apply clarsimp
+apply (clarsimp split add: split_if_asm)
+apply (clarsimp,tactic "smp_tac 1 1",erule(2) Loop_sound_lemma,(rule HOL.refl)+)
+apply clarsimp
+apply clarsimp
+apply clarsimp
+apply clarsimp
+apply (clarsimp del: Meth_elim_cases) (* Call *)
+apply (clarsimp del: Impl_elim_cases) (* Meth *)
+defer
+apply blast (* Conseq *)
+apply (simp_all (no_asm_use) only: cnvalids_def nvalids_def)
+apply blast
+apply blast
+apply blast
+(* Impl *)
+apply (erule thin_rl)
+apply (rule allI)
+apply (induct_tac "n")
+apply  (clarify intro!: Impl_nvalid_0)
+apply (clarify  intro!: Impl_nvalid_Suc)
+apply (drule nvalids_SucD)
+apply (erule (1) impE)
+apply (drule (4) Impl_sound_lemma)
+done
+
+theorem hoare_sound: "{} \<turnstile> {P} c {Q} \<Longrightarrow> \<Turnstile> {P} c {Q}"
+apply (simp only: valid_def2)
+apply (drule hoare_sound_main)
+apply (unfold cnvalids_def nvalids_def)
+apply fast
+done
+
+
+subsection "(Relative) Completeness"
+
+constdefs MGT    :: "stmt => state => triple"
+         "MGT c z \<equiv> (\<lambda> s. z = s, c, %t. \<exists>n. z -c-n-> t)"
+
+lemma MGF_implies_complete:
+ "\<forall>z. {} |\<turnstile> {MGT c z} \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
+apply (simp only: valid_def2)
+apply (unfold MGT_def)
+apply (erule hoare.Conseq)
+apply (clarsimp simp add: nvalid1_def2)
+done
+
+
+declare exec.intros[intro!]
+
+lemma MGF_Loop: "\<forall>z. A \<turnstile> {op = z} c {\<lambda>t. \<exists>n. z -c-n\<rightarrow> t} \<Longrightarrow> 
+  A \<turnstile> {op = z} While (e) c {\<lambda>t. \<exists>n. z -While (e) c-n\<rightarrow> t}"
+apply (rule_tac P' = "\<lambda>z s. (z,s) \<in> ({(s,t). \<exists>n. s<e> \<noteq> Null \<and> s -c-n\<rightarrow> t})^*"
+       in hoare.Conseq)
+apply  (rule allI)
+apply  (rule hoare.Loop)
+apply  (erule hoare.Conseq)
+apply  clarsimp
+apply  (blast intro:rtrancl_into_rtrancl)
+apply (erule thin_rl)
+apply clarsimp
+apply (erule_tac x = z in allE)
+apply clarsimp
+apply (erule converse_rtrancl_induct)
+apply  blast
+apply clarsimp
+apply (drule (1) exec_max2)
+apply (blast del: exec_elim_cases)
+done
+
+lemma MGF_lemma[rule_format]:
+ "(\<forall>C m z. A |\<turnstile> {MGT (Impl C m) z}) \<longrightarrow> (\<forall>z. A |\<turnstile> {MGT c z})"
+apply (simp add: MGT_def)
+apply (induct_tac c)
+apply (tactic "ALLGOALS Clarify_tac")
+
+apply (rule Conseq1 [OF hoare.Skip])
+apply blast
+
+apply (rule hoare.Comp)
+apply  (erule spec)
+apply (erule hoare.Conseq)
+apply (erule thin_rl, erule thin_rl)
+apply clarsimp
+apply (drule (1) exec_max2)
+apply blast
+
+apply (rule hoare.Cond)
+apply  (erule hoare.Conseq)
+apply  (erule thin_rl, erule thin_rl)
+apply  force
+apply (erule hoare.Conseq)
+apply (erule thin_rl, erule thin_rl)
+apply force
+
+apply (erule MGF_Loop)
+
+apply (rule Conseq1 [OF hoare.NewC])
+apply blast
+
+apply (rule Conseq1 [OF hoare.Cast])
+apply blast
+
+apply (rule Conseq1 [OF hoare.FAcc])
+apply blast
+
+apply (rule Conseq1 [OF hoare.FAss])
+apply blast
+
+apply (rule hoare.Call)
+apply (rule allI)
+apply (rule hoare.Meth)
+apply (rule allI)
+apply (drule spec, drule spec, erule hoare.Conseq)
+apply blast
+
+apply (rule hoare.Meth)
+apply (rule allI)
+apply (drule spec, drule spec, erule hoare.Conseq)
+apply blast
+
+apply blast
+done
+
+lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl C m) z}"
+apply (unfold MGT_def)
+apply (rule Impl1)
+apply  (rule_tac [2] UNIV_I)
+apply clarsimp
+apply (rule hoare.ConjI)
+apply clarsimp
+apply (rule ssubst [OF Impl_body_eq])
+apply (fold MGT_def)
+apply (rule MGF_lemma)
+apply (rule hoare.Asm)
+apply force
+done
+
+theorem hoare_relative_complete: "\<Turnstile> {P} c {Q} \<Longrightarrow> {} \<turnstile> {P} c {Q}"
+apply (rule MGF_implies_complete)
+apply  (erule_tac [2] asm_rl)
+apply (rule allI)
+apply (rule MGF_lemma)
+apply (rule MGF_Impl)
+done
+
+end
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/OpSem.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/OpSem.thy	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,89 @@
+(*  Title:      HOL/NanoJava/OpSem.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   2001 Technische Universitaet Muenchen
+*)
+
+header "Operational Evaluation Semantics"
+
+theory OpSem = State:
+
+consts
+  exec :: "(state \<times> stmt \<times> nat \<times> state) set"
+syntax (xsymbols)
+  exec :: "[state,  stmt,  nat,  state] => bool" ("_ -_-_\<rightarrow> _" [98,90,99,98] 89)
+syntax
+  exec :: "[state,  stmt,  nat,  state] => bool" ("_ -_-_-> _" [98,90,99,98] 89)
+translations
+  "s -c-n-> s'" == "(s, c, n, s') \<in> exec"
+
+inductive exec intros
+
+  Skip: "   s -Skip-n-> s"
+
+  Comp: "[| s0 -c1-n-> s1; s1 -c2-n-> s2 |] ==>
+            s0 -c1;; c2-n-> s2"
+
+  Cond: "[| s -(if s<e> \<noteq> Null then c1 else c2)-n-> s' |] ==>
+            s -If(e) c1 Else c2-n-> s'"
+
+  LoopF:"   s0<e> = Null ==>
+            s0 -While(e) c-n-> s0"
+  LoopT:"[| s0<e> \<noteq> Null; s0 -c-n-> s1; s1 -While(e) c-n-> s2 |] ==>
+            s0 -While(e) c-n-> s2"
+
+  NewC: "   new_Addr s = Addr a ==>
+            s -x:=new C-n-> lupd(x\<mapsto>Addr a)(new_obj a C s)"
+
+  Cast: "  (case s<y> of Null => True | Addr a => obj_class s a \<preceq>C C) ==>
+            s -x:=(C)y-n-> lupd(x\<mapsto>s<y>) s"
+
+  FAcc: "   s<y> = Addr a ==>
+            s -x:=y..f-n-> lupd(x\<mapsto>get_field s a f) s"
+
+  FAss: "   s<y> = Addr a ==>
+            s -y..f:=x-n-> upd_obj a f (s<x>) s"
+
+  Call: "lupd(This\<mapsto>s<y>)(lupd(Param\<mapsto>s<p>)(init_locs C m s))-Meth C m -n-> s'==>
+            s -x:={C}y..m(p)-n-> lupd(x\<mapsto>s'<Res>)(set_locs s s')"
+
+  Meth: "[| s<This> = Addr a; obj_class s a\<preceq>C C;
+            s -Impl (obj_class s a) m-n-> s' |] ==>
+            s -Meth C m-n-> s'"
+
+  Impl: "   s -body C m-    n-> s' ==>
+            s -Impl C m-Suc n-> s'"
+
+inductive_cases exec_elim_cases':
+	"s -Skip            -n-> t"
+	"s -c1;; c2         -n-> t"
+	"s -If(e) c1 Else c2-n-> t"
+	"s -While(e) c      -n-> t"
+	"s -x:=new C        -n-> t"
+	"s -x:=(C)y         -n-> t"
+	"s -x:=y..f         -n-> t"
+	"s -y..f:=x         -n-> t"
+	"s -x:={C}y..m(p)   -n-> t"
+inductive_cases Meth_elim_cases: "s -Meth C m -n-> t"
+inductive_cases Impl_elim_cases: "s -Impl C m -n-> t"
+lemmas exec_elim_cases = exec_elim_cases' Meth_elim_cases Impl_elim_cases
+
+lemma exec_mono [rule_format]: "s -c-n\<rightarrow> t \<Longrightarrow> \<forall>m. n \<le> m \<longrightarrow> s -c-m\<rightarrow> t"
+apply (erule exec.induct)
+prefer 12 (* Impl *)
+apply clarify
+apply (rename_tac n)
+apply (case_tac n)
+apply (blast intro:exec.intros)+
+done
+
+lemma exec_max2: "\<lbrakk>s1 -c1-    n1   \<rightarrow> t1 ; s2 -c2-        n2\<rightarrow> t2\<rbrakk> \<Longrightarrow> 
+                   s1 -c1-max n1 n2\<rightarrow> t1 \<and> s2 -c2-max n1 n2\<rightarrow> t2"
+by (fast intro: exec_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)"
+apply (rule ext)
+apply (fast elim: exec_elim_cases intro: exec.Impl)
+done
+
+end
\ No newline at end of file
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/ROOT.ML	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,1 @@
+use_thy "Equivalence";
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/State.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/State.thy	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,111 @@
+(*  Title:      HOL/NanoJava/State.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   2001 Technische Universitaet Muenchen
+*)
+
+header "Program State"
+
+theory State = TypeRel:
+
+constdefs
+
+  body :: "cname => mname => stmt"
+ "body C m \<equiv> bdy (the (method C m))"
+
+text {* locations, i.e.\ abstract references to objects *}
+typedecl loc 
+arities  loc :: "term"
+
+datatype val
+  = Null        (* null reference *)
+  | Addr loc    (* address, i.e. location of object *)
+
+types	fields
+	= "(vnam \<leadsto> val)"
+
+        obj = "cname \<times> fields"
+
+translations
+
+  "fields" \<leftharpoondown> (type)"vnam \<Rightarrow> val option"
+  "obj"    \<leftharpoondown> (type)"cname \<times> fields"
+
+constdefs
+
+  init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)"
+ "init_vars m == option_map (\<lambda>T. Null) o m"
+  
+text {* private *}
+types	heap   = "loc   \<leadsto> obj"
+        locals = "vname \<leadsto> val"	
+
+text {* private *}
+record  state
+	= heap   :: heap
+          locals :: locals
+
+translations
+
+  "heap"   \<leftharpoondown> (type)"loc   => obj option"
+  "locals" \<leftharpoondown> (type)"vname => val option"
+  "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
+
+constdefs
+
+  init_locs     :: "cname => mname => state => state"
+ "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.*}
+constdefs
+  set_locs  :: "state => state => state"
+ "set_locs s s' \<equiv> s' (| locals := locals s |)"
+
+  get_local     :: "state => vname => val" ("_<_>" [99,0] 99)
+ "get_local s x  \<equiv> the (locals s x)"
+
+(* 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 s a f \<equiv> the (snd (get_obj s a) f)"
+
+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 a C   \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))"
+
+  upd_obj    :: "loc \<Rightarrow> vnam \<Rightarrow> val \<Rightarrow> state \<Rightarrow> 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"
+ "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null"
+
+lemma new_AddrD: 
+"new_Addr s = v \<Longrightarrow> (\<exists>a. v = Addr a \<and> heap s a = None) | v = Null"
+apply (unfold new_Addr_def)
+apply (erule subst)
+apply (rule someI)
+apply (rule disjI2)
+apply (rule HOL.refl)
+done
+
+end
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/Term.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/Term.thy	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,46 @@
+(*  Title:      HOL/NanoJava/Term.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   2001 Technische Universitaet Muenchen
+*)
+
+header "Statements and expression emulations"
+
+theory Term = Main:
+
+typedecl cname  (* class name *)
+typedecl vnam   (* variable or field name *)
+typedecl mname  (* method name *)
+arities  cname :: "term"
+         vnam  :: "term"
+         mname :: "term"
+
+datatype vname  (* variable for special names *)
+  = This        (* This pointer *)
+  | Param       (* method parameter *)
+  | Res         (* method result *)
+  | VName vnam 
+
+datatype stmt
+  = Skip                   (* empty statement *)
+  | Comp       stmt stmt   ("_;; _"             [91,90]    90)
+  | Cond vname stmt stmt   ("If '(_') _ Else _" [99,91,91] 91)
+  | Loop vname stmt        ("While '(_') _"     [99,91   ] 91)
+
+  | NewC vname cname       ("_:=new _"  [99,   99] 95) (* object creation  *)
+  | Cast vname cname vname ("_:='(_')_" [99,99,99] 95) (* assignment, cast *)
+  | FAcc vname vname vnam  ("_:=_.._"   [99,99,99] 95) (* field access     *)
+  | FAss vname vnam  vname ("_.._:=_"   [99,99,99] 95) (* field assigment  *)
+  | Call vname cname vname mname vname                 (* method call      *)
+                           ("_:={_}_.._'(_')" [99,99,99,99,99] 95)
+  | Meth cname mname       (* virtual method *)
+  | Impl cname mname       (* method implementation *)
+
+(*###TO Product_Type_lemmas.ML*)
+lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
+apply (rule_tac x = "(a,b)" in image_eqI)
+apply  auto
+done
+
+end
+
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/TypeRel.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/TypeRel.thy	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,145 @@
+(*  Title:      HOL/NanoJava/TypeRel.thy
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   2001 Technische Universitaet Muenchen
+*)
+
+header "Type relations"
+
+theory TypeRel = Decl:
+
+consts
+  widen   :: "(ty    \<times> ty   ) set"  (* widening *)
+  subcls1 :: "(cname \<times> cname) set"  (* subclass *)
+
+syntax (xsymbols)
+  widen   :: "[ty   , ty   ] => bool" ("_ \<preceq> _"    [71,71] 70)
+  subcls1 :: "[cname, cname] => bool" ("_ \<prec>C1 _"  [71,71] 70)
+  subcls  :: "[cname, cname] => bool" ("_ \<preceq>C _"   [71,71] 70)
+syntax
+  widen   :: "[ty   , ty   ] => bool" ("_ <= _"   [71,71] 70)
+  subcls1 :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
+  subcls  :: "[cname, cname] => bool" ("_ <=C _"  [71,71] 70)
+
+translations
+  "C \<prec>C1 D" == "(C,D) \<in> subcls1"
+  "C \<preceq>C  D" == "(C,D) \<in> subcls1^*"
+  "S \<preceq>   T" == "(S,T) \<in> widen"
+
+consts
+  method :: "cname => (mname \<leadsto> methd)"
+  field  :: "cname => (vnam  \<leadsto> ty)"
+
+
+text {* The rest of this theory is not actually used. *}
+
+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 *)
+  refl   [intro!, simp]:           "T \<preceq> T"
+  subcls         : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
+  null   [intro!]:                "NT \<preceq> R"
+
+lemma subcls1D: 
+  "C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>c. class C = Some c \<and> super c=D)"
+apply (unfold subcls1_def)
+apply auto
+done
+
+lemma subcls1I: "\<lbrakk>class C = Some m; super m = D; C \<noteq> Object\<rbrakk> \<Longrightarrow> C\<prec>C1D"
+apply (unfold subcls1_def)
+apply auto
+done
+
+lemma subcls1_def2: 
+"subcls1 = (\<Sigma>C\<in>{C. is_class C} . {D. C\<noteq>Object \<and> super (the (class C)) = D})"
+apply (unfold subcls1_def is_class_def)
+apply auto
+done
+
+lemma finite_subcls1: "finite subcls1"
+apply(subst subcls1_def2)
+apply(rule finite_SigmaI [OF finite_is_class])
+apply(rule_tac B = "{super (the (class C))}" in finite_subset)
+apply  auto
+done
+
+constdefs
+
+  ws_prog  :: "bool"
+ "ws_prog \<equiv> \<forall>(C,c)\<in>set Prog. C\<noteq>Object \<longrightarrow> 
+                              is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
+
+lemma ws_progD: "\<lbrakk>class C = Some c; C\<noteq>Object; ws_prog\<rbrakk> \<Longrightarrow>  
+  is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
+apply (unfold ws_prog_def class_def)
+apply (drule_tac map_of_SomeD)
+apply auto
+done
+
+lemma subcls1_irrefl_lemma1: "ws_prog \<Longrightarrow> subcls1^-1 \<inter> subcls1^+ = {}"
+by (fast dest: subcls1D ws_progD)
+
+(* context (theory "Transitive_Closure") *)
+lemma irrefl_tranclI': "r^-1 Int r^+ = {} ==> !x. (x, x) ~: r^+"
+apply (rule allI)
+apply (erule irrefl_tranclI)
+done
+
+lemmas subcls1_irrefl_lemma2 = subcls1_irrefl_lemma1 [THEN irrefl_tranclI']
+
+lemma subcls1_irrefl: "\<lbrakk>(x, y) \<in> subcls1; ws_prog\<rbrakk> \<Longrightarrow> x \<noteq> y"
+apply (rule irrefl_trancl_rD)
+apply (rule subcls1_irrefl_lemma2)
+apply auto
+done
+
+lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
+
+lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)"
+by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
+
+
+consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<leadsto> 'b)"
+
+recdef class_rec "subcls1\<inverse>"
+      "class_rec C = (\<lambda>f. case class C of None   \<Rightarrow> arbitrary 
+                                        | Some m \<Rightarrow> if wf (subcls1\<inverse>) 
+       then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m)
+       else arbitrary)"
+(hints intro: subcls1I)
+
+lemma class_rec: "\<lbrakk>class C = Some m;  ws_prog\<rbrakk> \<Longrightarrow>
+ class_rec C f = (if C = Object then empty else class_rec (super m) f) ++ 
+                 map_of (f m)";
+apply (drule wf_subcls1)
+apply (rule class_rec.simps [THEN trans [THEN fun_cong]])
+apply  assumption
+apply simp
+done
+
+(* 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>
+method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
+apply (unfold method_def)
+apply (erule (1) class_rec [THEN trans]);
+apply simp
+done
+
+
+(* 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>
+field C = (if C=Object then empty else field (super m)) ++ map_of (fields m)"
+apply (unfold field_def)
+apply (erule (1) class_rec [THEN trans]);
+apply simp
+done
+
+end
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/document/root.bib	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,58 @@
+@inproceedings{NipkowOP00,
+        author={Tobias Nipkow and Oheimb, David von and Cornelia Pusch},
+        title={{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
+        booktitle = {Foundations of Secure Computation},
+        series= {NATO Science Series F: Computer and Systems Sciences},
+        volume = {175},
+        year = {2000},
+        publisher = {IOS Press},
+        editor = {Friedrich L. Bauer and Ralf Steinbr{\"u}ggen},
+        abstract = {This paper introduces the subset $micro$Java of Java,
+essentially by omitting everything but classes.
+The type system and semantics of this language
+(and a corresponding abstract Machine $micro$JVM)
+are formalized in the theorem prover Isabelle/HOL.
+Type safety both of $micro$Java and the $micro$JVM
+are mechanically verified.
+
+To make the paper self-contained, it starts with
+introductions to Isabelle/HOL and the art of
+embedding languages in theorem provers.},
+        CRClassification = {D.3.1, F.3.2},
+        CRGenTerms = {Languages, Reliability, Theory, Verification},
+        url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
+        pages = {117--144}
+}
+
+
+@article{DvO-CPE01,
+        author = {David von Oheimb},
+        title = {Hoare Logic for {J}ava in {Isabelle/HOL}},
+        journal = {Concurrency: Practice and Experience},
+        year = {2001},
+        url = {http://www4.in.tum.de/papers/DvO-CPE01.html},
+        abstract = {
+This article presents a Hoare-style calculus for a substantial subset 
+of Java Card, which we call Java_light. In particular, the language 
+includes side-effecting expressions, mutual recursion, dynamic method 
+binding, full exception handling, and static class initialization.
+
+The Hoare logic of partial correctness is proved not only sound (w.r.t.
+our operational semantics of Java_light, described in detail elsewhere)
+but even complete. It is the first logic for an object-oriented 
+language that is provably complete.
+The completeness proof uses a refinement of the Most General Formula 
+approach. The proof of soundness gives new insights into the role of 
+type safety. Further by-products of this work are a new general 
+methodology for handling side-effecting expressions and their results, 
+the discovery of the strongest possible rule of consequence, and a 
+flexible Call rule for mutual recursion. 
+We also give a small but non-trivial application example.
+
+All definitions and proofs have been done formally with the interactive 
+theorem prover Isabelle/HOL. This guarantees not only rigorous definitions, 
+but also gives maximal confidence in the results obtained.},
+        CRClassification = {D.2.4, D.3.1, F.3.1},
+        CRGenTerms = {Languages, Verification, Theory},
+        note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear}
+}
diff -r a6730c90e753 -r bf98ad1c22c6 src/HOL/NanoJava/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/document/root.tex	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,57 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{latexsym,isabelle,isabellesym,latexsym,pdfsetup}
+
+\urlstyle{tt}
+\pagestyle{myheadings}
+
+\addtolength{\hoffset}{-1,5cm}
+\addtolength{\textwidth}{4cm}
+\addtolength{\voffset}{-2cm}
+\addtolength{\textheight}{4cm}
+
+%subsection instead of section to make the toc readable
+\renewcommand{\thesubsection}{\arabic{subsection}}
+\renewcommand{\isamarkupheader}[1]{\newpage\markright{Theory~\isabellecontext}\subsection{#1}}
+\renewcommand{\isamarkupsection}[1]{\subsubsection{#1}}
+
+%remove spaces from the isabelle environment (trivlist makes them too large)
+\renewenvironment{isabelle}
+{\begin{isabellebody}}
+{\end{isabellebody}}
+
+\newcommand{\nJava}{\it NanoJava}
+
+%remove clutter from the toc
+\setcounter{secnumdepth}{3}
+\setcounter{tocdepth}{2}
+
+\begin{document}
+
+\title{\nJava}
+\author{David von Oheimb \\ Tobias Nipkow}
+\maketitle
+
+\begin{abstract}\noindent
+  These theories define {\nJava}, a very small fragment of the programming 
+  language Java (with essentially just classes) derived from the one given 
+  in \cite{NipkowOP00}.
+  For {\nJava}, an operational semantics is given as well as a Hoare logic,
+  which is proved both sound and (relatively) complete. The Hoare logic
+  implements a new approach for handling auxiliary variables.
+  A more complex Hoare logic covering a much larger subset of Java is described
+  in \cite{DvO-CPE01}.\\
+See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/}.
+\end{abstract}
+
+\tableofcontents
+\parindent 0pt \parskip 0.5ex
+
+\newpage
+\input{session}
+
+\newpage
+\nocite{*}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}