improved superclass entry for classes and definition status of is_class, class
corrected recursive definitions of "method" and "fields"
Beware: some proofs are incomplete (sorry, oops), preliminary comments with DvO:

--- a/src/HOL/MicroJava/BV/BVSpec.thy	Wed Dec 06 19:05:50 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Wed Dec 06 19:09:34 2000 +0100
@@ -38,17 +38,19 @@
 "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
 by (unfold wt_jvm_prog_def, blast)
 
-lemma wt_jvm_prog_impl_wt_instr:
-"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] 
+lemma wt_jvm_prog_impl_wt_instr: (* DvO: is_class G C eingefügt *)
+"[| wt_jvm_prog G phi; is_class G C;
+    method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] 
  ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc";
 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
-    simp, simp add: wf_mdecl_def wt_method_def)
+    simp, simp, simp add: wf_mdecl_def wt_method_def)
 
-lemma wt_jvm_prog_impl_wt_start:
-"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> 
+lemma wt_jvm_prog_impl_wt_start: (* DvO: is_class G C eingefügt *)
+"[| wt_jvm_prog G phi; is_class G C;
+    method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> 
  0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
-    simp, simp add: wf_mdecl_def wt_method_def)
+    simp, simp, simp add: wf_mdecl_def wt_method_def)
 
 text {* for most instructions wt\_instr collapses: *}
 lemma  

--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Dec 06 19:05:50 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Dec 06 19:09:34 2000 +0100
@@ -17,7 +17,7 @@
 lemmas [simp del] = split_paired_All
 
 lemma wt_jvm_prog_impl_wt_instr_cor:
-  "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); 
+  "[| wt_jvm_prog G phi;is_class G C; method (G,C) sig = Some (C,rT,maxs,maxl,ins); 
       G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
   ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
 apply (unfold correct_state_def Let_def correct_frame_def)
@@ -195,7 +195,7 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def defs1
-		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def 
+		   fun_upd_apply map_eq_Cons raise_xcpt_def init_vars_def 
        split: option.split)
 apply (force dest!: iffD1 [OF collapse_paired_All]
        intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap 
@@ -205,7 +205,7 @@
               hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
               correct_init_obj 
        simp add: NT_subtype_conv approx_val_def conf_def defs1
-         fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def 
+         fun_upd_apply map_eq_Cons raise_xcpt_def init_vars_def 
        split: option.split)
 done
 
@@ -214,8 +214,8 @@
 
 lemmas [simp del] = split_paired_Ex
 
-lemma Invoke_correct:
-"[| wt_jvm_prog G phi; 
+lemma Invoke_correct: (* DvO: is_class G C' eingefügt *)
+"[| wt_jvm_prog G phi; is_class G C';
   method (G,C) sig = Some (C,rT,maxs,maxl,ins); 
   ins ! pc = Invoke C' mn pTs; 
   wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; 
@@ -224,6 +224,7 @@
 ==> G,phi \<turnstile>JVM state'\<surd>" 
 proof -
   assume wtprog: "wt_jvm_prog G phi"
+  assume is_class: "is_class G C'"
   assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)"
   assume ins:    "ins ! pc = Invoke C' mn pTs"
   assume wti:    "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"
@@ -324,7 +325,7 @@
       by - (drule widen_Class, elim, rule that)
       
     with X
-    have "G \<turnstile> X' \<preceq>C C'" 
+    have X'_subcls: "G \<turnstile> X' \<preceq>C C'" 
       by simp
 
     with mC' wfprog
@@ -333,7 +334,7 @@
       by (auto dest: subtype_widen_methd intro: that)
 
     from X' D
-    have "G \<turnstile> D \<preceq>C X'" 
+    have D_subcls: "G \<turnstile> D \<preceq>C X'" 
       by simp
 
     with wfprog mX
@@ -346,10 +347,14 @@
     have rT': "G \<turnstile> rT' \<preceq> rT"
       by - (rule widen_trans)
     
-    from mD wfprog
+    from is_class X'_subcls D_subcls
+    have is_class_D: "is_class G D"
+    by (auto dest: subcls_is_class2)
+
+    with mD wfprog
     obtain mD'': 
       "method (G, D'') (mn, pTs) = Some (D'', rT', mxs', mxl', ins')"
-      "is_class G D''" 
+      "is_class G D''"
       by (auto dest: method_in_md)
       
     from loc obj_ty
@@ -385,7 +390,7 @@
         by (simp add: approx_loc_def approx_val_Err 
                       list_all2_def set_replicate_conv_if)
 
-      from wfprog mD
+      from wfprog mD is_class_D
       have "G \<turnstile> Class D \<preceq> Class D''"
         by (auto dest: method_wf_mdecl)
       with obj_ty loc
@@ -460,6 +465,8 @@
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm)
 apply (frule wt_jvm_prog_impl_wt_instr)
+sorry
+(*
 apply (assumption, erule Suc_lessD)
 apply (unfold wt_jvm_prog_def)
 apply (fastsimp
@@ -468,6 +475,7 @@
   intro: conf_widen
   simp: approx_val_def append_eq_conv_conj map_eq_Cons defs1)
 done
+*)
 
 lemmas [simp] = map_append
 
@@ -595,9 +603,12 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
 ==> G,phi \<turnstile>JVM state'\<surd>"
 apply (frule wt_jvm_prog_impl_wt_instr_cor)
+sorry
+(*
 apply assumption+
 apply (cases "ins!pc")
 prefer 9
+
 apply (blast intro: Invoke_correct)
 prefer 9
 apply (blast intro: Return_correct)
@@ -608,7 +619,7 @@
   Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
   Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
 done
-
+*)
 
 (** Main **)
 

--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Dec 06 19:05:50 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Wed Dec 06 19:09:34 2000 +0100
@@ -244,7 +244,7 @@
   G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>"
 apply (unfold oconf_def lconf_def)
 apply (simp add: map_of_map)
-apply (force intro: defval_conf dest: map_of_SomeD is_type_fields)
+apply (force intro: defval_conf dest: map_of_SomeD fields_is_type)
 done
 
 

--- a/src/HOL/MicroJava/BV/JType.thy	Wed Dec 06 19:05:50 2000 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Wed Dec 06 19:09:34 2000 +0100
@@ -68,7 +68,7 @@
     moreover    
     from R wf ty
     have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
-      by (auto simp add: is_ty_def subcls1_def is_class_def class_def 
+      by (auto simp add: is_ty_def subcls1_def 
                elim: converse_rtranclE
                split: ref_ty.splits)    
     ultimately    

--- a/src/HOL/MicroJava/BV/JVM.thy	Wed Dec 06 19:05:50 2000 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Wed Dec 06 19:09:34 2000 +0100
@@ -179,7 +179,7 @@
  apply (drule method_wf_mdecl, assumption)
  apply (simp add: wf_mdecl_def wf_mhead_def)
 
- apply (drule is_type_fields)
+ apply (drule fields_is_type)
  apply assumption
  apply (subgoal_tac "((vname, cname), vT) \<in> set (fields (S, cname))")
  apply assumption

--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Dec 06 19:05:50 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Dec 06 19:09:34 2000 +0100
@@ -427,17 +427,15 @@
   assume wfprog: 
     "wf_prog (\<lambda>G C (sig,rT,mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) G"
 
-  thus ?thesis 
+  thus ?thesis (* DvO: braucht ewig :-( *)
   proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto)
     fix a aa ab b ac ba ad ae af bb 
-    assume 1 : "\<forall>(C,sc,fs,ms)\<in>set G.
-             Ball (set fs) (wf_fdecl G) \<and>
-             unique fs \<and>
+    assume 1 : "\<forall>(C,D,fs,ms)\<in>set G.
+             Ball (set fs) (wf_fdecl G) \<and> unique fs \<and>
              (\<forall>(sig,rT,mb)\<in>set ms. wf_mhead G sig rT \<and> 
                (\<lambda>(mxs,mxl,b). wt_method G C (snd sig) rT mxs mxl b (Phi C sig)) mb) \<and>
              unique ms \<and>
-             (case sc of None => C = Object
-              | Some D =>
+             (C \<noteq> Object \<longrightarrow>
                   is_class G D \<and>
                   (D, C) \<notin> (subcls1 G)^* \<and>
                   (\<forall>(sig,rT,b)\<in>set ms. 
@@ -456,15 +454,18 @@
       from m b
       show ?thesis
       proof (rule bspec [elim_format], clarsimp)
-        assume "wt_method G a ba ad ae af bb (Phi a (ac, ba))"         
+        assume "wt_method G a ba ad ae af bb (Phi a (ac, ba))"
         with wfprog uG ub b 1
         show ?thesis
           by - (rule wtl_method_complete [elim_format], assumption+, 
                 simp add: make_Cert_def unique_epsilon unique_epsilon')
       qed 
+oops
+(*
     qed
   qed
 qed
+*)
 
 lemmas [simp] = split_paired_Ex
 

--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Dec 06 19:05:50 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Dec 06 19:09:34 2000 +0100
@@ -282,6 +282,7 @@
 
 theorem wtl_correct:
 "wtl_jvm_prog G cert ==> \<exists> Phi. wt_jvm_prog G Phi"
+(*
 proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI)
 
   assume wtl_prog: "wtl_jvm_prog G cert"
@@ -300,6 +301,10 @@
       in SOME phi. wt_method G C (snd sig) rT maxs maxl b phi"
     from wtl_prog
     show "?Q ?Phi"
+*)
+sorry
+(*
+DvO: hier beginnt die Maschine wie blöd zu swappen
     proof (unfold wf_cdecl_def, intro)
       fix x a b aa ba ab bb m
       assume 1: "x \<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \<in> set bb"
@@ -328,6 +333,6 @@
     qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
   qed
 qed
-    
+*)    
 
 end

--- a/src/HOL/MicroJava/BV/StepMono.thy	Wed Dec 06 19:05:50 2000 +0100
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Wed Dec 06 19:09:34 2000 +0100
@@ -174,7 +174,7 @@
                   "is_class G cname" and
               oT: "G\<turnstile> oT\<preceq> (Class cname)" and
               vT: "G\<turnstile> vT\<preceq> b"
-        by simp (elim exE conjE, rule that) 
+        by force
       moreover
       from s1 G
       obtain vT' oT' ST' LT'