# HG changeset patch
# User kleing
# Date 1014734732 -3600
# Node ID a9fdcb71d25251eb6aec7bd44ece8bf104a437bb
# Parent  3aadb133632d2fcbdc5efc2112ad30c6a7ca2ab9
introduces SystemClasses and BVExample

diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/IsaMakefile	Tue Feb 26 15:45:32 2002 +0100
@@ -468,7 +468,7 @@
   MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \
   MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \
   MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
-  MicroJava/BV/Kildall_Lift.thy \
+  MicroJava/BV/Kildall_Lift.thy MicroJava/BV/BVExample.thy \
   MicroJava/document/root.bib MicroJava/document/root.tex \
   MicroJava/document/introduction.tex
 	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/BV/BVExample.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -0,0 +1,377 @@
+(*  Title:      HOL/MicroJava/BV/BVExample.thy
+    ID:         $Id$
+    Author:     Gerwin Klein
+*)
+
+header {* Example Welltypings *}
+
+theory BVExample = JVMListExample + Correct:
+
+section "Setup"
+text {*
+  Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
+  anonymous, we describe distinctness of names in the example by axioms:
+*}
+axioms 
+  distinct_classes: "list_nam \<noteq> test_nam"
+  distinct_fields:  "val_nam \<noteq> next_nam"
+
+text {* Shorthands for definitions we will have to use often in the
+proofs below: *}
+lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def
+lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
+                     OutOfMemoryC_def ClassCastC_def
+lemmas class_defs  = list_class_def test_class_def
+
+text {* These auxiliary proofs are for efficiency: class lookup,
+subclass relation, method and field lookup are computed only once:
+*}
+lemma class_Object [simp]:
+  "class E Object = Some (arbitrary, [],[])"
+  by (simp add: class_def system_defs E_def)
+
+lemma class_NullPointer [simp]:
+  "class E (Xcpt NullPointer) = Some (Object, [], [])"
+  by (simp add: class_def system_defs E_def)
+
+lemma class_OutOfMemory [simp]:
+  "class E (Xcpt OutOfMemory) = Some (Object, [], [])"
+  by (simp add: class_def system_defs E_def)
+
+lemma class_ClassCast [simp]:
+  "class E (Xcpt ClassCast) = Some (Object, [], [])"
+  by (simp add: class_def system_defs E_def)
+
+lemma class_list [simp]:
+  "class E list_name = Some list_class"
+  by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
+ 
+lemma class_test [simp]:
+  "class E test_name = Some test_class"
+  by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
+
+lemma E_classes [simp]:
+  "{C. is_class E C} = {list_name, test_name, Xcpt NullPointer, 
+                        Xcpt ClassCast, Xcpt OutOfMemory, Object}"
+  by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
+
+text {* The subclass releation spelled out: *}
+lemma subcls1:
+  "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
+                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
+  apply (simp add: subcls1_def2)
+  apply (simp add: name_defs class_defs system_defs E_def class_def)
+  apply (auto split: split_if_asm)
+  done
+
+text {* The subclass relation is acyclic; hence its converse is well founded: *}
+lemma notin_rtrancl:
+  "(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
+  by (auto elim: converse_rtranclE)  
+
+lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
+  apply (rule acyclicI)
+  apply (simp add: subcls1)
+  apply (auto dest!: tranclD)
+  apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
+  done
+
+lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
+  apply (rule finite_acyclic_wf_converse)
+  apply (simp add: subcls1)
+  apply (rule acyclic_subcls1_E)
+  done  
+
+text {* Method and field lookup: *}
+lemma method_Object [simp]:
+  "method (E, Object) = empty"
+  by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
+
+lemma method_append [simp]:
+  "method (E, list_name) (append_name, [Class list_name]) =
+  Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"
+  apply (insert class_list)
+  apply (unfold list_class_def)
+  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
+  apply simp
+  done
+
+lemma method_makelist [simp]:
+  "method (E, test_name) (makelist_name, []) = 
+  Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"
+  apply (insert class_test)
+  apply (unfold test_class_def)
+  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
+  apply simp
+  done
+
+lemma field_val [simp]:
+  "field (E, list_name) val_name = Some (list_name, PrimT Integer)"
+  apply (unfold field_def)
+  apply (insert class_list)
+  apply (unfold list_class_def)
+  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
+  apply simp
+  done
+
+lemma field_next [simp]:
+  "field (E, list_name) next_name = Some (list_name, Class list_name)"
+  apply (unfold field_def)
+  apply (insert class_list)
+  apply (unfold list_class_def)
+  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
+  apply (simp add: name_defs distinct_fields [symmetric])
+  done
+
+lemma [simp]: "fields (E, Object) = []"
+   by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])
+ 
+lemma [simp]: "fields (E, Xcpt NullPointer) = []"
+  by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])
+
+lemma [simp]: "fields (E, Xcpt ClassCast) = []"
+  by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])
+
+lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"
+  by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])
+
+lemma [simp]: "fields (E, test_name) = []"
+  apply (insert class_test)
+  apply (unfold test_class_def)
+  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
+  apply simp
+  done
+
+lemmas [simp] = is_class_def
+
+text {*
+  The next definition and three proof rules implement an algorithm to
+  enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} 
+  transforms a goal of the form
+  @{prop [display] "pc < n \<Longrightarrow> P pc"} 
+  into a series of goals
+  @{prop [display] "P 0"} 
+  @{prop [display] "P (Suc 0)"} 
+
+  @{text "\<dots>"}
+
+  @{prop [display] "P n"} 
+*}
+constdefs 
+  intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')")
+  "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
+
+lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
+  by (simp add: intervall_def)
+
+lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
+  apply (cases "x=n0")
+  apply (auto simp add: intervall_def) 
+  apply arith
+  done
+
+lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" 
+  by (unfold intervall_def) arith
+
+
+section "Program structure"
+
+text {*
+  The program is structurally wellformed:
+*}
+lemma wf_struct:
+  "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
+proof -
+  have "unique E" 
+    by (simp add: system_defs E_def class_defs name_defs distinct_classes)
+  moreover
+  have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def)
+  hence "wf_syscls E" by (rule wf_syscls)
+  moreover
+  have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)
+  moreover
+  have "wf_cdecl ?mb E NullPointerC" 
+    by (auto elim: notin_rtrancl 
+            simp add: wf_cdecl_def name_defs NullPointerC_def subcls1)
+  moreover
+  have "wf_cdecl ?mb E ClassCastC" 
+    by (auto elim: notin_rtrancl 
+            simp add: wf_cdecl_def name_defs ClassCastC_def subcls1)
+  moreover
+  have "wf_cdecl ?mb E OutOfMemoryC" 
+    by (auto elim: notin_rtrancl 
+            simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1)
+  moreover
+  have "wf_cdecl ?mb E (list_name, list_class)"
+    apply (auto elim!: notin_rtrancl 
+            simp add: wf_cdecl_def wf_fdecl_def list_class_def 
+                      wf_mdecl_def wf_mhead_def subcls1)
+    apply (auto simp add: name_defs distinct_classes distinct_fields)
+    done    
+  moreover
+  have "wf_cdecl ?mb E (test_name, test_class)" 
+    apply (auto elim!: notin_rtrancl 
+            simp add: wf_cdecl_def wf_fdecl_def test_class_def 
+                      wf_mdecl_def wf_mhead_def subcls1)
+    apply (auto simp add: name_defs distinct_classes distinct_fields)
+    done       
+  ultimately
+  show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
+qed
+
+section "Welltypings"
+text {*
+  We show welltypings of the methods @{term append_name} in class @{term list_name}, 
+  and @{term makelist_name} in class @{term test_name}:
+*}
+lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
+declare appInvoke [simp del]
+
+constdefs
+  phi_append :: method_type ("\<phi>\<^sub>a")
+  "\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [ 
+   (                                    [], [Class list_name, Class list_name]),
+   (                     [Class list_name], [Class list_name, Class list_name]),
+   (                     [Class list_name], [Class list_name, Class list_name]),
+   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
+   ([NT, Class list_name, Class list_name], [Class list_name, Class list_name]),
+   (                     [Class list_name], [Class list_name, Class list_name]),
+   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
+   (                          [PrimT Void], [Class list_name, Class list_name]),
+   (                        [Class Object], [Class list_name, Class list_name]),
+   (                                    [], [Class list_name, Class list_name]),
+   (                     [Class list_name], [Class list_name, Class list_name]),
+   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
+   (                                    [], [Class list_name, Class list_name]),
+   (                          [PrimT Void], [Class list_name, Class list_name])]"
+
+lemma wt_append [simp]:
+  "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
+             [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
+  apply (simp add: wt_method_def append_ins_def phi_append_def 
+                   wt_start_def wt_instr_def)
+  apply clarify
+  apply (elim pc_end pc_next pc_0)
+  apply simp
+  apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
+  apply simp
+  apply simp
+  apply (fastsimp simp add: sup_state_conv subcls1)
+  apply simp
+  apply (simp add: app_def xcpt_app_def)
+  apply simp
+  apply simp
+  apply simp
+  apply (simp add: match_exception_entry_def)
+  apply (simp add: match_exception_entry_def)
+  apply simp
+  apply simp
+  done
+
+text {* Some shorthands to make the welltyping of method @{term
+makelist_name} easier to read *} 
+syntax
+  list :: ty 
+  test :: ty
+translations
+  "list" == "Class list_name"
+  "test" == "Class test_name"
+
+constdefs
+  phi_makelist :: method_type ("\<phi>\<^sub>m")
+  "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ 
+    (                                   [], [OK test, Err    , Err    ]),
+    (                               [list], [OK test, Err    , Err    ]),
+    (                         [list, list], [OK test, Err    , Err    ]),
+    (                               [list], [OK list, Err    , Err    ]),
+    (                [PrimT Integer, list], [OK list, Err    , Err    ]),
+    (                                   [], [OK list, Err    , Err    ]),
+    (                               [list], [OK list, Err    , Err    ]),
+    (                         [list, list], [OK list, Err    , Err    ]),
+    (                               [list], [OK list, OK list, Err    ]),
+    (                [PrimT Integer, list], [OK list, OK list, Err    ]),
+    (                                   [], [OK list, OK list, Err    ]),
+    (                               [list], [OK list, OK list, Err    ]),
+    (                         [list, list], [OK list, OK list, Err    ]),
+    (                               [list], [OK list, OK list, OK list]),
+    (                [PrimT Integer, list], [OK list, OK list, OK list]),
+    (                                   [], [OK list, OK list, OK list]),
+    (                               [list], [OK list, OK list, OK list]),
+    (                         [list, list], [OK list, OK list, OK list]),
+    (                         [PrimT Void], [OK list, OK list, OK list]),
+    (                   [list, PrimT Void], [OK list, OK list, OK list]),
+    (             [list, list, PrimT Void], [OK list, OK list, OK list]),
+    (             [PrimT Void, PrimT Void], [OK list, OK list, OK list]),
+    ( [PrimT Void, PrimT Void, PrimT Void], [OK list, OK list, OK list])]"
+
+lemma wt_makelist [simp]:
+  "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
+  apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
+  apply (simp add: wt_start_def nat_number_of)
+  apply (simp add: wt_instr_def)
+  apply clarify
+  apply (elim pc_end pc_next pc_0)
+  apply (simp add: match_exception_entry_def)
+  apply simp
+  apply simp
+  apply simp
+  apply (simp add: match_exception_entry_def)
+  apply (simp add: match_exception_entry_def) 
+  apply simp
+  apply simp
+  apply simp
+  apply (simp add: match_exception_entry_def)
+  apply (simp add: match_exception_entry_def) 
+  apply simp
+  apply simp
+  apply simp
+  apply (simp add: match_exception_entry_def)
+  apply (simp add: match_exception_entry_def) 
+  apply simp
+  apply (simp add: app_def xcpt_app_def)
+  apply simp
+  apply simp
+  apply (simp add: app_def xcpt_app_def)
+  apply simp
+  apply simp
+  done
+
+text {* The whole program is welltyped: *}
+constdefs 
+  Phi :: prog_type ("\<Phi>")
+  "\<Phi> C sig \<equiv> if C = test_name \<and> sig = (makelist_name, []) then \<phi>\<^sub>m else
+              if C = list_name \<and> sig = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
+  
+lemma wf_prog:
+  "wt_jvm_prog E \<Phi>"
+  apply (unfold wt_jvm_prog_def)
+  apply (rule wf_mb'E [OF wf_struct])
+  apply (simp add: E_def)
+  apply clarify
+  apply (fold E_def)
+  apply (simp add: system_defs class_defs Phi_def)
+  apply auto
+  done
+
+
+section "Conformance"
+text {* Execution of the program will be typesafe, because its
+  start state conforms to the welltyping: *}
+
+lemma [simp]: "preallocated start_heap"
+  apply (unfold start_heap_def preallocated_def)
+  apply auto
+  apply (case_tac x)
+  apply auto
+  done
+
+lemma "E,\<Phi> \<turnstile>JVM start_state \<surd>"
+  apply (simp add: correct_state_def start_state_def test_class_def)
+  apply (simp add: hconf_def start_heap_def oconf_def lconf_def)
+  apply (simp add: Phi_def phi_makelist_def)
+  apply (simp add: correct_frame_def)
+  apply (simp add: make_list_ins_def)
+  apply (simp add: conf_def start_heap_def)
+  done
+
+end
\ No newline at end of file
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -114,6 +114,14 @@
   qed
 qed
 
+lemma match_et_imp_match:
+  "match_exception_table G X pc et = Some handler
+  \<Longrightarrow> match G X pc et = [X]"
+  apply (simp add: match_some_entry)
+  apply (induct et)
+  apply (auto split: split_if_asm)
+  done
+
 text {*
   We can prove separately that the recursive search for exception
   handlers (@{text find_handler}) in the frame stack results in 
@@ -356,7 +364,7 @@
         phi': "phi C sig ! handler = Some (ST', LT')" and
         less: "G \<turnstile> ([Class (Xcpt OutOfMemory)], LT) <=s (ST', LT')" and
         pc':  "handler < length ins"
-        by (simp add: xcpt_eff_def) blast
+        by (simp add: xcpt_eff_def match_et_imp_match) blast
       note phi'
       moreover
       { from xcp prehp
@@ -386,7 +394,7 @@
         phi': "phi C sig ! handler = Some (ST', LT')" and
         less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
         pc':  "handler < length ins"
-        by (simp add: xcpt_eff_def) blast
+        by (simp add: xcpt_eff_def match_et_imp_match) blast
       note phi'
       moreover
       { from xcp prehp
@@ -416,7 +424,7 @@
         phi': "phi C sig ! handler = Some (ST', LT')" and
         less: "G \<turnstile> ([Class (Xcpt NullPointer)], LT) <=s (ST', LT')" and
         pc':  "handler < length ins"
-        by (simp add: xcpt_eff_def) blast
+        by (simp add: xcpt_eff_def match_et_imp_match) blast
       note phi'
       moreover
       { from xcp prehp
@@ -446,7 +454,7 @@
         phi': "phi C sig ! handler = Some (ST', LT')" and
         less: "G \<turnstile> ([Class (Xcpt ClassCast)], LT) <=s (ST', LT')" and
         pc':  "handler < length ins"
-        by (simp add: xcpt_eff_def) blast
+        by (simp add: xcpt_eff_def match_et_imp_match) blast
       note phi'
       moreover
       { from xcp prehp
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -72,14 +72,24 @@
                             in 
                             if start_pc <= pc \<and> pc < end_pc then catch_type#es' else es')"
 
+consts
+  match :: "jvm_prog \<Rightarrow> cname \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list"
+primrec
+  "match G X pc [] = []"
+  "match G X pc (e#es) = 
+  (if match_exception_entry G X pc e then [X] else match G X pc es)"
+
+lemma match_some_entry:
+  "match G X pc et = (if \<exists>e \<in> set et. match_exception_entry G X pc e then [X] else [])"
+  by (induct et) auto
 
 consts
   xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table => cname list" 
 recdef xcpt_names "{}"
-  "xcpt_names (Getfield F C, G, pc, et) = [Xcpt NullPointer]" 
-  "xcpt_names (Putfield F C, G, pc, et) = [Xcpt NullPointer]"
-  "xcpt_names (New C, G, pc, et)        = [Xcpt OutOfMemory]"
-  "xcpt_names (Checkcast C, G, pc, et)  = [Xcpt ClassCast]"
+  "xcpt_names (Getfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et" 
+  "xcpt_names (Putfield F C, G, pc, et) = match G (Xcpt NullPointer) pc et" 
+  "xcpt_names (New C, G, pc, et)        = match G (Xcpt OutOfMemory) pc et"
+  "xcpt_names (Checkcast C, G, pc, et)  = match G (Xcpt ClassCast) pc et"
   "xcpt_names (Throw, G, pc, et)        = match_any G pc et"
   "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et" 
   "xcpt_names (i, G, pc, et)            = []" 
@@ -214,23 +224,26 @@
 lemma appGetField[simp]:
 "(app (Getfield F C) G maxs rT pc et (Some s)) = 
  (\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and>  
-  field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C) \<and> is_class G (Xcpt NullPointer))"
+  field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C) \<and> (\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). is_class G x))"
   by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)
 
 lemma appPutField[simp]:
 "(app (Putfield F C) G maxs rT pc et (Some s)) = 
  (\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and> 
-  field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> vT' \<and> is_class G (Xcpt NullPointer))"
+  field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> vT' \<and>
+  (\<forall>x \<in> set (match G (Xcpt NullPointer) pc et). is_class G x))"
   by (cases s, cases "2 <length (fst s)", auto dest!: 1 2)
 
 lemma appNew[simp]:
   "(app (New C) G maxs rT pc et (Some s)) = 
-  (\<exists>ST LT. s=(ST,LT) \<and> is_class G C \<and> length ST < maxs \<and> is_class G (Xcpt OutOfMemory))"
+  (\<exists>ST LT. s=(ST,LT) \<and> is_class G C \<and> length ST < maxs \<and>
+  (\<forall>x \<in> set (match G (Xcpt OutOfMemory) pc et). is_class G x))"
   by (cases s, simp)
 
 lemma appCheckcast[simp]: 
   "(app (Checkcast C) G maxs rT pc et (Some s)) =  
-  (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and> is_class G (Xcpt ClassCast))"
+  (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and>
+  (\<forall>x \<in> set (match G (Xcpt ClassCast) pc et). is_class G x))"
   by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)
 
 lemma appPop[simp]: 
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -151,7 +151,7 @@
                   "is_class G cname" and
               oT: "G\<turnstile> oT\<preceq> (Class cname)" and
               vT: "G\<turnstile> vT\<preceq> b" and
-              xc: "is_class G (Xcpt NullPointer)"
+              xc: "Ball (set (match G (Xcpt NullPointer) pc et)) (is_class G)"
         by force
       moreover
       from s1 G
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -107,14 +107,14 @@
   apply clarsimp
   apply (erule disjE)
    apply (fastsimp dest: field_fields fields_is_type)
-  apply simp
+  apply (simp add: match_some_entry split: split_if_asm)
   apply (rule_tac x=1 in exI)
   apply fastsimp
 
   apply clarsimp
   apply (erule disjE)
    apply fastsimp
-  apply simp
+  apply (simp add: match_some_entry split: split_if_asm)
   apply (rule_tac x=1 in exI)
   apply fastsimp
 
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -165,14 +165,13 @@
 apply auto
 done
 
-lemma non_np_objD: "!!G. [|a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C; C \<noteq> Object|] ==>  
+lemma non_np_objD: "!!G. [|a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C|] ==>  
   (\<exists>a C' fs. a' = Addr a \<and>  h a = Some (C',fs) \<and>  G\<turnstile>C'\<preceq>C C)"
 apply (fast dest: non_npD)
 done
 
 lemma non_np_objD' [rule_format (no_asm)]: 
   "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t --> 
-  (\<forall>C. t = ClassT C --> C \<noteq> Object) -->  
   (\<exists>a C fs. a' = Addr a \<and>  h a = Some (C,fs) \<and>  G\<turnstile>Class C\<preceq>RefT t)"
 apply(rule_tac "y" = "t" in ref_ty.exhaust)
  apply (fast dest: conf_NullTD)
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -23,11 +23,6 @@
   'c prog  = "'c cdecl list"     -- "program"
 
 
-constdefs
-  ObjectC :: "'c cdecl" -- "decl of root class"
-  "ObjectC \<equiv> (Object, (arbitrary, [], []))"
-
-
 translations
   "fdecl"   <= (type) "vname \<times> ty"
   "sig"     <= (type) "mname \<times> ty list"
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -6,7 +6,7 @@
 
 header {* \isaheader{Example MicroJava Program} *}
 
-theory Example = Eval:
+theory Example = SystemClasses + Eval:
 
 text {* 
 The following example MicroJava program includes:
@@ -72,12 +72,17 @@
 axioms
   Base_not_Object: "Base \<noteq> Object"
   Ext_not_Object:  "Ext  \<noteq> Object"
-  e_not_This:      "e \<noteq> This"
+  Base_not_Xcpt:   "Base \<noteq> Xcpt z"
+  Ext_not_Xcpt:    "Ext  \<noteq> Xcpt z"
+  e_not_This:      "e \<noteq> This"  
 
 declare Base_not_Object [simp] Ext_not_Object [simp]
+declare Base_not_Xcpt [simp] Ext_not_Xcpt [simp]
 declare e_not_This [simp]
-declare Base_not_Object [THEN not_sym, simp]
-declare Ext_not_Object  [THEN not_sym, simp]
+declare Base_not_Object [symmetric, simp]
+declare Ext_not_Object  [symmetric, simp]
+declare Base_not_Xcpt [symmetric, simp]
+declare Ext_not_Xcpt  [symmetric, simp]
 
 consts
   foo_Base::  java_mb
@@ -119,7 +124,7 @@
 
 translations
   "NP"   == "NullPointer"
-  "tprg" == "[ObjectC, BaseC, ExtC]"
+  "tprg" == "[ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
   "obj1"    <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
          ((vee, Ext )\<mapsto>Intg 0))"
   "s0" == " Norm    (empty, empty)"
@@ -142,11 +147,26 @@
 apply (simp (no_asm))
 done
 
+lemma class_tprg_NP [simp]: "class tprg (Xcpt NP) = Some (Object, [], [])"
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_OM [simp]: "class tprg (Xcpt OutOfMemory) = Some (Object, [], [])"
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_CC [simp]: "class tprg (Xcpt ClassCast) = Some (Object, [], [])"
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
 lemma class_tprg_Base [simp]: 
 "class tprg Base = Some (Object,  
     [(vee, PrimT Boolean)],  
           [((foo, [Class Base]), Class Base, foo_Base)])"
-apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
 apply (simp (no_asm))
 done
 
@@ -174,8 +194,8 @@
 done
 
 lemma class_tprgD: 
-"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext"
-apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory"
+apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
 apply (auto split add: split_if_asm simp add: map_of_Cons)
 done
 
@@ -188,7 +208,7 @@
 done
 
 lemma unique_classes: "unique tprg"
-apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def)
+apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
 done
 
 lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
@@ -278,6 +298,30 @@
 apply (simp (no_asm))
 done
 
+lemma wf_NP:
+"wf_cdecl wf_java_mdecl tprg NullPointerC"
+apply (unfold wf_cdecl_def wf_fdecl_def NullPointerC_def)
+apply (simp add: class_def)
+apply (fold NullPointerC_def class_def)
+apply auto
+done
+
+lemma wf_OM:
+"wf_cdecl wf_java_mdecl tprg OutOfMemoryC"
+apply (unfold wf_cdecl_def wf_fdecl_def OutOfMemoryC_def)
+apply (simp add: class_def)
+apply (fold OutOfMemoryC_def class_def)
+apply auto
+done
+
+lemma wf_CC:
+"wf_cdecl wf_java_mdecl tprg ClassCastC"
+apply (unfold wf_cdecl_def wf_fdecl_def ClassCastC_def)
+apply (simp add: class_def)
+apply (fold ClassCastC_def class_def)
+apply auto
+done
+
 lemma wf_BaseC: 
 "wf_cdecl wf_java_mdecl tprg BaseC"
 apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def)
@@ -298,10 +342,14 @@
 apply auto
 done
 
+lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def)
+
 lemma wf_tprg: 
 "wf_prog wf_java_mdecl tprg"
 apply (unfold wf_prog_def Let_def)
-apply(simp add: wf_ObjectC wf_BaseC wf_ExtC unique_classes)
+apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes)
+apply (rule wf_syscls)
+apply (simp add: SystemClasses_def)
 done
 
 lemma appl_methds_foo_Base: 
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -1,11 +1,11 @@
-(*  Title:      HOL/MicroJava/JVM/JVMListExample.thy
+(*  Title:      HOL/MicroJava/J/JListExample.thy
     ID:         $Id$
     Author:     Stefan Berghofer
 *)
 
 header {* \isaheader{Example for generating executable code from Java semantics} *}
 
-theory JListExample = Eval:
+theory JListExample = Eval + SystemClasses:
 
 ML {* Syntax.ambiguity_level := 100000 *}
 
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -60,8 +60,7 @@
 apply( erule conjE)
 apply( simp)
 apply( drule non_np_objD)
-apply(   assumption)
-apply(  force)
+apply(  assumption)
 apply( clarify)
 apply( simp (no_asm_use))
 apply( frule (1) hext_objD)
@@ -121,7 +120,6 @@
 apply( drule max_spec2mheads)
 apply( clarify)
 apply( drule (2) non_np_objD')
-apply(  clarsimp)
 apply( clarsimp)
 apply( frule (1) hext_objD)
 apply( clarsimp)
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/J/SystemClasses.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/SystemClasses.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -0,0 +1,32 @@
+(*  Title:      HOL/MicroJava/J/SystemClasses.thy
+    ID:         $Id$
+    Author:     Gerwin Klein
+    Copyright   2002 Technische Universitaet Muenchen
+*)
+
+header {* \isaheader{System Classes} *}
+
+theory SystemClasses = Decl:
+
+text {*
+  This theory provides definitions for the @{text Object} class,
+  and the system exceptions.
+*}
+
+constdefs
+  ObjectC :: "'c cdecl"
+  "ObjectC \<equiv> (Object, (arbitrary,[],[]))"
+
+  NullPointerC :: "'c cdecl"
+  "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
+
+  ClassCastC :: "'c cdecl"
+  "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))"
+
+  OutOfMemoryC :: "'c cdecl"
+  "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))"
+
+  SystemClasses :: "'c cdecl list"
+  "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]"
+
+end
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/Type.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -21,7 +21,7 @@
 datatype cname  
   = Object 
   | Xcpt xcpt 
-  | Cname cname 
+  | Cname cnam 
 
 typedecl vnam   -- "variable or field name"
 typedecl mname  -- "method name"
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -6,7 +6,7 @@
 
 header {* \isaheader{Well-formedness of Java programs} *}
 
-theory WellForm = TypeRel:
+theory WellForm = TypeRel + SystemClasses:
 
 text {*
 for static checks on expressions and statements, see WellType.
@@ -45,9 +45,12 @@
                    (\<forall>(sig,rT,b)\<in>set ms. \<forall>D' rT' b'.
                       method(G,D) sig = Some(D',rT',b') --> G\<turnstile>rT\<preceq>rT'))"
 
+ wf_syscls :: "'c prog => bool"
+"wf_syscls G == let cs = set G in Object \<in> fst ` cs \<and> (\<forall>x. Xcpt x \<in> fst ` cs)"
+
  wf_prog :: "'c wf_mb => 'c prog => bool"
-"wf_prog wf_mb G ==
-   let cs = set G in ObjectC \<in> cs \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
+"wf_prog wf_mb G == 
+   let cs = set G in wf_syscls G \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
 
 lemma class_wf: 
  "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)"
@@ -57,9 +60,9 @@
 done
 
 lemma class_Object [simp]: 
-  "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
-apply (unfold wf_prog_def ObjectC_def class_def)
-apply (auto intro: map_of_SomeI)
+  "wf_prog wf_mb G ==> \<exists>X fs ms. class G Object = Some (X,fs,ms)"
+apply (unfold wf_prog_def wf_syscls_def class_def)
+apply (auto simp: map_of_SomeI)
 done
 
 lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object"
@@ -158,20 +161,12 @@
 
 lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
 
-lemma method_Object [simp]: "wf_prog wf_mb G ==> method (G,Object) = empty"
-apply(subst method_rec)
-apply auto
-done
-
-lemma fields_Object [simp]: "wf_prog wf_mb G ==> fields (G,Object) = []"
-apply(subst fields_rec)
-apply auto
-done
-
-lemma field_Object [simp]: "wf_prog wf_mb G ==> field (G,Object) = empty"
-apply (unfold field_def)
-apply(simp (no_asm_simp))
-done
+lemma method_Object [simp]:
+  "method (G, Object) sig = Some (D, mh, code) \<Longrightarrow> wf_prog wf_mb G \<Longrightarrow> D = Object"  
+  apply (frule class_Object, clarify)
+  apply (drule method_rec, assumption)
+  apply (auto dest: map_of_SomeD)
+  done
 
 lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object"
 apply(erule subcls1_induct)
@@ -190,7 +185,10 @@
   \<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd"
 apply( erule subcls1_induct)
 apply(   assumption)
-apply(  simp (no_asm_simp))
+apply(  frule class_Object)
+apply(  clarify)
+apply(  frule fields_rec, assumption)
+apply(  fastsimp)
 apply( tactic "safe_tac HOL_cs")
 apply( subst fields_rec)
 apply(   assumption)
@@ -216,8 +214,16 @@
   "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
 apply( erule subcls1_induct)
 apply(   assumption)
-apply(  safe dest!: wf_cdecl_supD)
-apply(  simp (no_asm_simp))
+apply(  frule class_Object)
+apply(  clarify)
+apply(  frule fields_rec, assumption)
+apply(  drule class_wf, assumption)
+apply(  simp add: wf_cdecl_def)
+apply(  rule unique_map_inj)
+apply(   simp)
+apply(  rule injI)
+apply(  simp)
+apply( safe dest!: wf_cdecl_supD)
 apply( drule subcls1_wfD)
 apply(  assumption)
 apply( subst fields_rec)
@@ -269,7 +275,16 @@
    --> G\<turnstile>C\<preceq>C md \<and> wf_mdecl wf_mb G md (sig,(mh,m))"
 apply( erule subcls1_induct)
 apply(   assumption)
-apply(  force)
+apply(  clarify) 
+apply(  frule class_Object)
+apply(  clarify)
+apply(  frule method_rec, assumption)
+apply(  drule class_wf, assumption)
+apply(  simp add: wf_cdecl_def)
+apply(  drule map_of_SomeD)
+apply(  subgoal_tac "md = Object")
+apply(   fastsimp)
+apply(  fastsimp)
 apply( clarify)
 apply( frule_tac C = C in method_rec)
 apply(  assumption)
@@ -334,7 +349,10 @@
   "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) 
   --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
 apply (erule (1) subcls1_induct)
- apply (simp)
+ apply clarify
+ apply (frule method_Object, assumption)
+ apply hypsubst
+ apply simp
 apply (erule conjE)
 apply (subst method_rec)
   apply (assumption)
@@ -377,7 +395,12 @@
   "[|is_class G C; wf_prog wf_mb G|] ==>  
   \<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
 apply( erule (1) subcls1_induct)
-apply(  simp (no_asm_simp))
+apply(  frule class_Object)
+apply(  clarify)
+apply(  frule fields_rec, assumption)
+apply(  drule class_wf, assumption)
+apply(  simp add: wf_cdecl_def wf_fdecl_def)
+apply(  fastsimp)
 apply( subst fields_rec)
 apply(   fast)
 apply(  assumption)
@@ -405,24 +428,52 @@
   "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
   ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
 proof -
-  assume wf: "wf_prog wf_mb G" 
-  assume C:  "(C,S,fs,mdecls) \<in> set G"
-
-  assume m: "(sig,rT,code) \<in> set mdecls"
+  assume wf: "wf_prog wf_mb G" and C:  "(C,S,fs,mdecls) \<in> set G" and
+         m: "(sig,rT,code) \<in> set mdecls"
   moreover
-  from wf have "class G Object = Some (arbitrary, [], [])" by simp 
-  moreover
-  from wf C have c: "class G C = Some (S,fs,mdecls)"
+  from wf C have "class G C = Some (S,fs,mdecls)"
     by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
+  moreover
+  from wf C 
+  have "unique mdecls" by (unfold wf_prog_def wf_cdecl_def) auto
+  hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)  
+  with m 
+  have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
+    by (force intro: map_of_SomeI)
   ultimately
-  have O: "C \<noteq> Object" by auto      
-
-  from wf C have "unique mdecls" by (unfold wf_prog_def wf_cdecl_def) auto
-  hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)" by (induct mdecls, auto)
-  with m have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
-    by (force intro: map_of_SomeI)
-  with wf C m c O
   show ?thesis by (auto simp add: is_class_def dest: method_rec)
 qed
 
+
+lemma wf_mb'E:
+  "\<lbrakk> wf_prog wf_mb G; \<And>C S fs ms m.\<lbrakk>(C,S,fs,ms) \<in> set G; m \<in> set ms\<rbrakk> \<Longrightarrow> wf_mb' G C m \<rbrakk>
+  \<Longrightarrow> wf_prog wf_mb' G"
+  apply (simp add: wf_prog_def)
+  apply auto
+  apply (simp add: wf_cdecl_def wf_mdecl_def)
+  apply safe
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply clarify apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply (drule bspec, assumption) apply simp
+  apply clarify apply (drule bspec, assumption)+ apply simp
+  done
+
+
+lemma fst_mono: "A \<subseteq> B \<Longrightarrow> fst ` A \<subseteq> fst ` B" by fast
+
+lemma wf_syscls:
+  "set SystemClasses \<subseteq> set G \<Longrightarrow> wf_syscls G"
+  apply (drule fst_mono)
+  apply (simp add: SystemClasses_def wf_syscls_def)
+  apply (simp add: ObjectC_def) 
+  apply (rule allI, case_tac x)
+  apply (auto simp add: NullPointerC_def ClassCastC_def OutOfMemoryC_def)
+  done
+
 end
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Feb 26 15:45:32 2002 +0100
@@ -5,49 +5,56 @@
 
 header {* \isaheader{Example for generating executable code from JVM semantics} *}
 
-theory JVMListExample = JVMExec:
+theory JVMListExample = SystemClasses + JVMExec:
 
 consts
-  list_name :: cname
-  test_name :: cname
+  list_nam :: cnam
+  test_nam :: cnam
   append_name :: mname
   makelist_name :: mname
   val_nam :: vnam
   next_nam :: vnam
+  test_name_loc :: loc_
 
 constdefs
+  list_name :: cname
+  "list_name == Cname list_nam"
+  
+  test_name :: cname
+  "test_name == Cname test_nam"
+
   val_name :: vname
   "val_name == VName val_nam"
 
   next_name :: vname
   "next_name == VName next_nam"
 
-  list_class :: "jvm_method class"
-  "list_class ==
-    (Object,
-     [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
-     [((append_name, [RefT (ClassT list_name)]), PrimT Integer,
-      (0, 0,
+  append_ins :: bytecode
+  "append_ins == 
        [Load 0,
         Getfield next_name list_name,
         Dup,
         LitPush Null,
         Ifcmpeq 4,
-        Load 1,
-        Invoke list_name append_name [RefT (ClassT list_name)],
+        Load 1,       
+        Invoke list_name append_name [Class list_name],
         Return,
         Pop,
         Load 0,
         Load 1,
         Putfield next_name list_name,
         LitPush Unit,
-        Return],[]))])"
+        Return]"
 
-  test_class :: "jvm_method class"
-  "test_class ==
-    (Object, [],
-     [((makelist_name, []), PrimT Integer,
-      (0, 3,
+  list_class :: "jvm_method class"
+  "list_class ==
+    (Object,
+     [(val_name, PrimT Integer), (next_name, Class list_name)],
+     [((append_name, [Class list_name]), PrimT Void,
+        (3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])"
+
+  make_list_ins :: bytecode
+  "make_list_ins ==
        [New list_name,
         Dup,
         Store 0,
@@ -65,22 +72,33 @@
         Putfield val_name list_name,
         Load 0,
         Load 1,
-        Invoke list_name append_name [RefT (ClassT list_name)],
+        Invoke list_name append_name [Class list_name],
         Load 0,
         Load 2,
-        Invoke list_name append_name [RefT (ClassT list_name)],
+        Invoke list_name append_name [Class list_name],
         LitPush Unit,
-        Return],[]))])"
+        Return]"
+
+  test_class :: "jvm_method class"
+  "test_class ==
+    (Object, [],
+     [((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])"
 
-  example_prg :: jvm_prog
-  "example_prg == [ObjectC, (list_name, list_class), (test_name, test_class)]"
+  E :: jvm_prog
+  "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
+
+  start_heap :: aheap
+  "start_heap == empty (XcptRef NullPointer \<mapsto> (Xcpt NullPointer, empty))
+                       (XcptRef ClassCast \<mapsto> (Xcpt ClassCast, empty))
+                       (XcptRef OutOfMemory \<mapsto> (Xcpt OutOfMemory, empty))
+                       (Loc test_name_loc \<mapsto> (test_name, empty))"
 
   start_state :: jvm_state
   "start_state ==
-    (None, empty, [([], Unit # Unit # Unit # [], test_name, (makelist_name, []), 0)])"
+    (None, start_heap, [([], [Addr (Loc test_name_loc), arbitrary, arbitrary], test_name, (makelist_name, []), 0)])"
 
 types_code
-  cname ("string")
+  cnam ("string")
   vnam ("string")
   mname ("string")
   loc_ ("int")
@@ -92,11 +110,12 @@
 
   "arbitrary" ("(raise ERROR)")
   "arbitrary" :: "val" ("{* Unit *}")
-  "arbitrary" :: "cname" ("\"\"")
+  "arbitrary" :: "cname" ("Object")
 
-  "Object" ("\"Object\"")
-  "list_name" ("\"list\"")
-  "test_name" ("\"test\"")
+  "test_name_loc" ("0")
+
+  "list_nam" ("\"list\"")
+  "test_nam" ("\"test\"")
   "append_name" ("\"append\"")
   "makelist_name" ("\"makelist\"")
   "val_nam" ("\"val\"")
@@ -110,62 +129,62 @@
 
 subsection {* Single step execution *}
 
-generate_code
-  test = "exec (example_prg, start_state)"
+generate_code 
+  test = "exec (E, start_state)"
 
 ML {* test *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
-ML {* exec (example_prg, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
+ML {* exec (E, the it) *}
 
 end
\ No newline at end of file
diff -r 3aadb133632d -r a9fdcb71d252 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Tue Feb 26 13:47:19 2002 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Tue Feb 26 15:45:32 2002 +0100
@@ -10,8 +10,9 @@
 use_thy "Example";
 use_thy "JListExample";
 use_thy "JVMListExample";
+use_thy "JVM";
 use_thy "BVSpecTypeSafe";
-use_thy "JVM";
+use_thy "BVExample";
 
 (* momentarily broken:
 use_thy "LBVSpec";