# HG changeset patch
# User streckem
# Date 1035382142 -7200
# Node ID b95d12325b510c6458d7cb12cb4dab14af0bf89e
# Parent  eec2582923f634de53333e58a96d41b9c240b7c4
Added compiler

diff -r eec2582923f6 -r b95d12325b51 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/IsaMakefile	Wed Oct 23 16:09:02 2002 +0200
@@ -487,6 +487,16 @@
 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
 
 $(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \
+  MicroJava/Comp/AuxLemmas.thy \
+  MicroJava/Comp/CorrComp.thy \
+  MicroJava/Comp/CorrCompTp.thy \
+  MicroJava/Comp/DefsComp.thy \
+  MicroJava/Comp/Index.thy \
+  MicroJava/Comp/LemmasComp.thy \
+  MicroJava/Comp/NatCanonify.thy \
+  MicroJava/Comp/TranslComp.thy \
+  MicroJava/Comp/TranslCompTp.thy \
+  MicroJava/Comp/TypeInf.thy \
   MicroJava/J/Conform.thy MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \
   MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \
   MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/BV/Altern.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Altern.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -0,0 +1,67 @@
+
+theory Altern = BVSpec:
+
+
+constdefs
+  check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"
+  "check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr"
+
+  wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
+                exception_table,p_count] \<Rightarrow> bool"
+  "wt_instr_altern i G rT phi mxs mxr max_pc et pc \<equiv>
+  app i G mxs rT pc et (phi!pc) \<and>
+  check_type G mxs mxr (OK (phi!pc)) \<and>
+  (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
+
+  wt_method_altern :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
+                 exception_table,method_type] \<Rightarrow> bool"
+  "wt_method_altern G C pTs rT mxs mxl ins et phi \<equiv>
+  let max_pc = length ins in
+  0 < max_pc \<and> 
+  length phi = length ins \<and>
+  check_bounded ins et \<and> 
+  wt_start G C pTs mxl phi \<and>
+  (\<forall>pc. pc<max_pc \<longrightarrow> wt_instr_altern (ins!pc) G rT phi mxs (1+length pTs+mxl) max_pc et pc)"
+
+
+lemma wt_method_wt_method_altern : 
+  "wt_method G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method_altern G C pTs rT mxs mxl ins et phi"
+apply (simp add: wt_method_def wt_method_altern_def)
+apply (intro strip)
+apply clarify
+apply (drule spec, drule mp, assumption)
+apply (simp add: check_types_def wt_instr_def wt_instr_altern_def check_type_def)
+apply (auto  intro: imageI)
+done
+
+
+lemma check_type_check_types [rule_format]: 
+  "(\<forall>pc. pc < length phi \<longrightarrow> check_type G mxs mxr (OK (phi ! pc)))
+  \<longrightarrow> check_types G mxs mxr (map OK phi)"
+apply (induct phi)
+apply (simp add: check_types_def)
+apply (simp add: check_types_def)
+apply clarify
+apply (frule_tac x=0 in spec)
+apply (simp add: check_type_def)
+apply auto
+done
+
+lemma wt_method_altern_wt_method [rule_format]: 
+  "wt_method_altern G C pTs rT mxs mxl ins et phi \<longrightarrow> wt_method G C pTs rT mxs mxl ins et phi"
+apply (simp add: wt_method_def wt_method_altern_def)
+apply (intro strip)
+apply clarify
+apply (rule conjI)
+  (* show check_types *)
+apply (rule check_type_check_types)
+apply (simp add: wt_instr_altern_def)
+
+  (* show wt_instr *)
+apply (intro strip)
+apply (drule spec, drule mp, assumption)
+apply (simp add: wt_instr_def wt_instr_altern_def)
+done
+
+
+end
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -242,7 +242,7 @@
   qed
 qed
 
-
+declare raise_if_def [simp]
 text {*
   The requirement of lemma @{text uncaught_xcpt_correct} (that
   the exception is a valid reference on the heap) is always met
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -212,6 +212,11 @@
   "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
   by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons2)
 
+lemma sup_state_Cons:
+  "(G \<turnstile> (x#xt, a) <=s (y#yt, b)) = 
+   ((G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt,b)))"
+  by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def)
+
 
 theorem sup_loc_length:
   "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -6,7 +6,7 @@
 
 header {* \isaheader{Conformity Relations for Type Soundness Proof} *}
 
-theory Conform = State + WellType:
+theory Conform = State + WellType + Exceptions:
 
 types 'c env_ = "'c prog \<times> (vname \<leadsto> ty)"  -- "same as @{text env} of @{text WellType.thy}"
 
@@ -28,9 +28,14 @@
 
   hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50)
  "G|-h h [ok]    == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]"
+ 
+  xconf :: "aheap \<Rightarrow> val option \<Rightarrow> bool"
+  "xconf hp vo  == preallocated hp \<and> (\<forall> v. (vo = Some v) \<longrightarrow> (\<exists> xc. v = (Addr (XcptRef xc))))"
 
-  conforms :: "state => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
- "s::<=E == prg E|-h heap s [ok] \<and> prg E,heap s|-locals s[::<=]localT E"
+  conforms :: "xstate => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
+ "s::<=E == prg E|-h heap (store s) [ok] \<and> 
+            prg E,heap (store s)|-locals (store s)[::<=]localT E \<and> 
+            xconf (heap (store s)) (abrupt s)"
 
 
 syntax (xsymbols)
@@ -247,6 +252,12 @@
 apply( auto simp add: length_Suc_conv)
 done
 
+lemma lconf_restr: "\<lbrakk>lT vn = None; G, h \<turnstile> l [::\<preceq>] lT(vn\<mapsto>T)\<rbrakk> \<Longrightarrow> G, h \<turnstile> l [::\<preceq>] lT"
+apply (unfold lconf_def)
+apply (intro strip)
+apply (case_tac "n = vn")
+apply auto
+done
 
 section "oconf"
 
@@ -277,29 +288,56 @@
 done
 
 
+section "xconf"
+
+lemma xconf_raise_if: "xconf h x \<Longrightarrow> xconf h (raise_if b xcn x)"
+by (simp add: xconf_def raise_if_def)
+
+
+
 section "conforms"
 
-lemma conforms_heapD: "(h, l)::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"
+lemma conforms_heapD: "(x, (h, l))::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"
 apply (unfold conforms_def)
 apply (simp)
 done
 
-lemma conforms_localD: "(h, l)::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT"
+lemma conforms_localD: "(x, (h, l))::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT"
+apply (unfold conforms_def)
+apply (simp)
+done
+
+lemma conforms_xcptD: "(x, (h, l))::\<preceq>(G, lT) ==> xconf h x"
 apply (unfold conforms_def)
 apply (simp)
 done
 
-lemma conformsI: "[|G\<turnstile>h h\<surd>; G,h\<turnstile>l[::\<preceq>]lT|] ==> (h, l)::\<preceq>(G, lT)"
+lemma conformsI: "[|G\<turnstile>h h\<surd>; G,h\<turnstile>l[::\<preceq>]lT; xconf h x|] ==> (x, (h, l))::\<preceq>(G, lT)"
 apply (unfold conforms_def)
 apply auto
 done
 
-lemma conforms_hext: "[|(h,l)::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] ==> (h',l)::\<preceq>(G,lT)"
-apply( fast dest: conforms_localD elim!: conformsI lconf_hext)
-done
+lemma conforms_restr: "\<lbrakk>lT vn = None; s ::\<preceq> (G, lT(vn\<mapsto>T)) \<rbrakk> \<Longrightarrow> s ::\<preceq> (G, lT)"
+by (simp add: conforms_def, fast intro: lconf_restr)
+
+lemma conforms_xcpt_change: "\<lbrakk> (x, (h,l))::\<preceq> (G, lT); xconf h x \<longrightarrow> xconf h x' \<rbrakk> \<Longrightarrow> (x', (h,l))::\<preceq> (G, lT)"
+by (simp add: conforms_def)
+
+
+lemma preallocated_hext: "\<lbrakk> preallocated h; h\<le>|h'\<rbrakk> \<Longrightarrow> preallocated h'"
+by (simp add: preallocated_def hext_def)
+
+lemma xconf_hext: "\<lbrakk> xconf h vo; h\<le>|h'\<rbrakk> \<Longrightarrow> xconf h' vo"
+by (simp add: xconf_def preallocated_def hext_def)
+
+lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] 
+  ==> (x,(h',l))::\<preceq>(G,lT)"
+by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)
+
 
 lemma conforms_upd_obj: 
-  "[|(h,l)::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] ==> (h(a\<mapsto>obj),l)::\<preceq>(G, lT)"
+  "[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] 
+  ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)"
 apply(rule conforms_hext)
 apply  auto
 apply(rule hconfI)
@@ -309,7 +347,8 @@
 done
 
 lemma conforms_upd_local: 
-"[|(h, l)::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] ==> (h, l(va\<mapsto>v))::\<preceq>(G, lT)"
+"[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] 
+  ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)"
 apply (unfold conforms_def)
 apply( auto elim: lconf_upd)
 done
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -8,6 +8,30 @@
 
 theory Eval = State + WellType:
 
+
+  -- "Auxiliary notions"
+
+constdefs
+  fits    :: "java_mb prog \<Rightarrow> state \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60)
+ "G,s\<turnstile>a' fits T  \<equiv> case T of PrimT T' \<Rightarrow> False | RefT T' \<Rightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T"
+
+constdefs
+  catch ::"java_mb prog \<Rightarrow> xstate \<Rightarrow> cname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60)
+ "G,s\<turnstile>catch C\<equiv>  case abrupt s of None \<Rightarrow> False | Some a \<Rightarrow> G,store s\<turnstile> a fits Class C"
+
+
+
+constdefs
+  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"        ("lupd'(_\<mapsto>_')"[10,10]1000)
+ "lupd vn v   \<equiv> \<lambda> (hp,loc). (hp, (loc(vn\<mapsto>v)))"
+
+constdefs
+  new_xcpt_var :: "vname \<Rightarrow> xstate \<Rightarrow> xstate"
+ "new_xcpt_var vn \<equiv>  \<lambda>(x,s). Norm (lupd(vn\<mapsto>the x) s)"
+
+
+  -- "Evaluation relations"
+
 consts
   eval  :: "java_mb prog => (xstate \<times> expr      \<times> val      \<times> xstate) set"
   evals :: "java_mb prog => (xstate \<times> expr list \<times> val list \<times> xstate) set"
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/J/Exceptions.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Exceptions.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -0,0 +1,65 @@
+(*  Title:      HOL/MicroJava/J/Exceptions.thy
+    ID:         $Id$
+    Author:     Gerwin Klein, Martin Strecker
+    Copyright   2002 Technische Universitaet Muenchen
+*)
+
+theory Exceptions = State:
+
+text {* a new, blank object with default values in all fields: *}
+constdefs
+  blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj"
+  "blank G C \<equiv> (C,init_vars (fields(G,C)))" 
+
+  start_heap :: "'c prog \<Rightarrow> aheap"
+  "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer))
+                        (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast))
+                        (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))"
+
+
+consts
+  cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname"
+
+translations
+  "cname_of hp v" == "fst (the (hp (the_Addr v)))"
+
+
+constdefs
+  preallocated :: "aheap \<Rightarrow> bool"
+  "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
+
+lemma preallocatedD:
+  "preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)"
+  by (unfold preallocated_def) fast
+
+lemma preallocatedE [elim?]:
+  "preallocated hp \<Longrightarrow> (\<And>fs. hp (XcptRef x) = Some (Xcpt x, fs) \<Longrightarrow> P hp) \<Longrightarrow> P hp"
+  by (fast dest: preallocatedD)
+
+lemma cname_of_xcp:
+  "raise_if b x None = Some xcp \<Longrightarrow> preallocated hp 
+  \<Longrightarrow> cname_of (hp::aheap) xcp = Xcpt x"
+proof -
+  assume "raise_if b x None = Some xcp"
+  hence "xcp = Addr (XcptRef x)"
+    by (simp add: raise_if_def split: split_if_asm)
+  moreover
+  assume "preallocated hp" 
+  then obtain fs where "hp (XcptRef x) = Some (Xcpt x, fs)" ..
+  ultimately
+  show ?thesis by simp
+qed
+
+lemma preallocated_start:
+  "preallocated (start_heap G)"
+  apply (unfold preallocated_def)
+  apply (unfold start_heap_def)
+  apply (rule allI)
+  apply (case_tac x)
+  apply (auto simp add: blank_def)
+  done
+
+
+
+end
+
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -62,10 +62,10 @@
   cname ("string")
   vnam ("string")
   mname ("string")
-  loc ("int")
+  loc_ ("int")
 
 consts_code
-  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
+  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
 
   "arbitrary" ("(raise ERROR)")
   "arbitrary" :: "val" ("{* Unit *}")
@@ -83,8 +83,8 @@
   "l4_nam" ("\"l4\"")
 
 ML {*
-fun new_addr p none hp =
-  let fun nr i = if p (hp i) then (i, none) else nr (i+1);
+fun new_addr p none loc hp =
+  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
   in nr 0 end;
 *}
 
@@ -114,14 +114,14 @@
 locs l2_name;
 locs l3_name;
 locs l4_name;
-snd (the (heap 0)) (val_name, "list");
-snd (the (heap 0)) (next_name, "list");
-snd (the (heap 1)) (val_name, "list");
-snd (the (heap 1)) (next_name, "list");
-snd (the (heap 2)) (val_name, "list");
-snd (the (heap 2)) (next_name, "list");
-snd (the (heap 3)) (val_name, "list");
-snd (the (heap 3)) (next_name, "list");
+snd (the (heap (Loc 0))) (val_name, "list");
+snd (the (heap (Loc 0))) (next_name, "list");
+snd (the (heap (Loc 1))) (val_name, "list");
+snd (the (heap (Loc 1))) (next_name, "list");
+snd (the (heap (Loc 2))) (val_name, "list");
+snd (the (heap (Loc 2))) (next_name, "list");
+snd (the (heap (Loc 3))) (val_name, "list");
+snd (the (heap (Loc 3))) (next_name, "list");
 
 *}
 
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -11,8 +11,8 @@
 declare split_beta [simp]
 
 lemma NewC_conforms: 
-"[|h a = None; (h, l)::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==>  
-  (h(a\<mapsto>(C,(init_vars (fields (G,C))))), l)::\<preceq>(G, lT)"
+"[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==>  
+  (x,(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l))::\<preceq>(G, lT)"
 apply( erule conforms_upd_obj)
 apply(  unfold oconf_def)
 apply(  auto dest!: fields_is_type)
@@ -30,8 +30,10 @@
 apply( auto intro!: conf_AddrI simp add: obj_ty_def)
 done
 
+
+
 lemma FAcc_type_sound: 
-"[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\<preceq>(G,lT);  
+"[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (x,(h,l))::\<preceq>(G,lT);  
   x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==>  
   G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft"
 apply( drule np_NoneD)
@@ -52,9 +54,9 @@
     (G, lT)\<turnstile>aa::Class C;  
     field (G,C) fn = Some (fd, ft); h''\<le>|h';  
     x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h;  
-    (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==>  
+    Norm (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==>  
   h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and>   
-  (h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and>   
+  Norm(h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and>   
   G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'"
 apply( drule np_NoneD)
 apply( erule conjE)
@@ -90,6 +92,8 @@
 apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD)
 done
 
+
+
 lemma Call_lemma2: "[| wf_prog wf_mb G; list_all2 (conf G h) pvs pTs;  
    list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT;  
   length pTs' = length pns; distinct pns;  
@@ -106,17 +110,18 @@
 done
 
 lemma Call_type_sound: 
- "[| wf_java_prog G; a' \<noteq> Null; (h, l)::\<preceq>(G, lT); class G C = Some y;  
+ "[| wf_java_prog G; a' \<noteq> Null; Norm (h, l)::\<preceq>(G, lT); class G C = Some y;  
      max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>|xh; xh\<le>|h;  
      list_all2 (conf G h) pvs pTsa; 
      (md, rT, pns, lvars, blk, res) =  
                the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); 
-  \<forall>lT. (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->  
-  (G, lT)\<turnstile>blk\<surd> -->  h\<le>|xi \<and>  (xi, xl)::\<preceq>(G, lT);  
-  \<forall>lT. (xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->  
-          xi\<le>|h' \<and> (h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));  
-  G,xh\<turnstile>a'::\<preceq> Class C |] ==>  
-  xc\<le>|h' \<and> (h', l)::\<preceq>(G, lT) \<and>  (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
+  \<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) -->  
+  (G, lT)\<turnstile>blk\<surd> -->  h\<le>|xi \<and>  (xcptb, xi, xl)::\<preceq>(G, lT);  
+  \<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T -->  
+          xi\<le>|h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T));  
+  G,xh\<turnstile>a'::\<preceq> Class C
+  |] ==>  
+  xc\<le>|h' \<and> (x',(h', l))::\<preceq>(G, lT) \<and>  (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)"
 apply( drule max_spec2mheads)
 apply( clarify)
 apply( drule (2) non_np_objD')
@@ -126,14 +131,15 @@
 apply( drule (3) Call_lemma)
 apply( clarsimp simp add: wf_java_mdecl_def)
 apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl)
-apply( drule spec, erule impE)
-apply(  erule_tac [2] notE impE, tactic "assume_tac 2")
+apply( drule spec, erule impE,  erule_tac [2] notE impE, tactic "assume_tac 2")
 apply(  rule conformsI)
 apply(   erule conforms_heapD)
 apply(  rule lconf_ext)
 apply(   force elim!: Call_lemma2)
 apply(  erule conf_hext, erule (1) conf_obj_AddrI)
-apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl)
+apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) 
+apply (simp add: conforms_def)
+
 apply( erule conjE)
 apply( drule spec, erule (1) impE)
 apply( drule spec, erule (1) impE)
@@ -149,11 +155,16 @@
 apply(   tactic "assume_tac 2")
 prefer 2
 apply(  fast elim!: widen_trans)
-apply( erule conforms_hext)
+apply (rule conforms_xcpt_change)
+apply( rule conforms_hext) apply assumption
+(* apply( erule conforms_hext)*)
 apply(  erule (1) hext_trans)
 apply( erule conforms_heapD)
+apply (simp add: conforms_def)
 done
 
+
+
 declare split_if [split del]
 declare fun_upd_apply [simp del]
 declare fun_upd_same [simp]
@@ -165,17 +176,19 @@
 Unify.search_bound := 40;
 Unify.trace_bound  := 40
 *}
+
+
 theorem eval_evals_exec_type_sound: 
 "wf_java_prog G ==>  
   (G\<turnstile>(x,(h,l)) -e  \<succ>v  -> (x', (h',l')) -->  
-      (\<forall>lT.   (h ,l )::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e  :: T -->  
-      h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v  ::\<preceq> T )))) \<and>  
+      (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e  :: T -->  
+      h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v  ::\<preceq> T )))) \<and>  
   (G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) -->  
-      (\<forall>lT.   (h ,l )::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->  
-      h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and>  
+      (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts -->  
+      h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and>  
   (G\<turnstile>(x,(h,l)) -c       -> (x', (h',l')) -->  
-      (\<forall>lT.   (h ,l )::\<preceq>(G,lT) -->       (G,lT)\<turnstile>c  \<surd> -->  
-      h\<le>|h' \<and> (h',l')::\<preceq>(G,lT)))"
+      (\<forall>lT.   (x,(h ,l ))::\<preceq>(G,lT) -->       (G,lT)\<turnstile>c  \<surd> -->  
+      h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT)))"
 apply( rule eval_evals_exec_induct)
 apply( unfold c_hupd_def)
 
@@ -187,12 +200,14 @@
 apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
 
 -- "Level 7"
-
 -- "15 NewC"
+apply (drule sym)
 apply( drule new_AddrD)
 apply( erule disjE)
 prefer 2
 apply(  simp (no_asm_simp))
+apply (rule conforms_xcpt_change, assumption) 
+apply (simp (no_asm_simp) add: xconf_def)
 apply( clarsimp)
 apply( rule conjI)
 apply(  force elim!: NewC_conforms)
@@ -216,6 +231,7 @@
 apply( simp split add: binop.split)
 
 -- "12 LAcc"
+apply simp
 apply( fast elim: conforms_localD [THEN lconfD])
 
 -- "for FAss"
@@ -234,7 +250,7 @@
 apply(  fast intro: hext_trans)
 
 -- "10 Expr"
-prefer 6
+prefer 7
 apply( fast)
 
 -- "9 ???"
@@ -242,18 +258,28 @@
 
 -- "8 Cast"
 prefer 8
-apply (rule impI)
-apply (drule raise_if_NoneD)
-apply (clarsimp)
-apply (fast elim: Cast_conf)
+apply (rule conjI)
+  apply (fast intro: conforms_xcpt_change xconf_raise_if)
+
+  apply clarify
+  apply (drule raise_if_NoneD)
+  apply (clarsimp)
+  apply (rule Cast_conf)
+  apply assumption+
 
 -- "7 LAss"
 apply (fold fun_upd_def)
 apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") 
                  THEN_ALL_NEW Full_simp_tac) 1 *})
+apply (intro strip)
+apply (case_tac E)
+apply (simp)
 apply( blast intro: conforms_upd_local conf_widen)
 
 -- "6 FAcc"
+apply (rule conjI) 
+  apply (simp add: np_def)
+  apply (fast intro: conforms_xcpt_change xconf_raise_if)
 apply( fast elim!: FAcc_type_sound)
 
 -- "5 While"
@@ -264,22 +290,34 @@
 
 apply (tactic "forward_hyp_tac")
 
--- "4 Cons"
-prefer 3
+-- "4 Cond"
+prefer 4
+apply (case_tac "the_Bool v")
+apply simp
+apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
+apply simp
 apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
 
 -- "3 ;;"
 prefer 3
-apply( fast intro: hext_trans)
+apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
+
 
 -- "2 FAss"
-apply( case_tac "x2 = None")
-prefer 2
-apply(  simp (no_asm_simp))
-apply(  fast intro: hext_trans)
-apply( simp)
-apply( drule eval_no_xcpt)
-apply( erule FAss_type_sound, rule HOL.refl, assumption+)
+apply (subgoal_tac "(np a' x1, ab, ba) ::\<preceq> (G, lT)")
+  prefer 2
+  apply (simp add: np_def)
+  apply (fast intro: conforms_xcpt_change xconf_raise_if)
+apply( case_tac "x2")
+  -- "x2 = None"
+  apply (simp)
+  apply (tactic forward_hyp_tac, clarify)
+  apply( drule eval_no_xcpt)
+  apply( erule FAss_type_sound, rule HOL.refl, assumption+)
+  -- "x2 = Some a"
+  apply (  simp (no_asm_simp))
+  apply(  fast intro: hext_trans)
+
 
 apply( tactic prune_params_tac)
 -- "Level 52"
@@ -302,15 +340,21 @@
 apply(  simp)
 apply(  drule eval_xcpt)
 apply(  simp)
-apply(  fast elim: hext_trans)
-apply( drule (1) ty_expr_is_type)
+apply (rule conjI)
+  apply(  fast elim: hext_trans)
+  apply (rule conforms_xcpt_change, assumption) apply (simp (no_asm_simp) add: xconf_def)
+apply(clarsimp)
+
+apply( drule ty_expr_is_type, simp)
 apply(clarsimp)
 apply(unfold is_class_def)
 apply(clarsimp)
+
 apply(rule Call_type_sound);
 prefer 11
 apply blast
 apply (simp (no_asm_simp))+ 
+
 done
 ML{*
 Unify.search_bound := 20;
@@ -318,8 +362,8 @@
 *}
 
 lemma eval_type_sound: "!!E s s'.  
-  [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); s::\<preceq>E; E\<turnstile>e::T |]  
-  ==> s'::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)"
+  [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T |]  
+  ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)"
 apply( simp (no_asm_simp) only: split_tupled_all)
 apply (drule eval_evals_exec_type_sound 
              [THEN conjunct1, THEN mp, THEN spec, THEN mp])
@@ -327,8 +371,8 @@
 done
 
 lemma exec_type_sound: "!!E s s'.  
-  [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); s::\<preceq>E; E\<turnstile>s0\<surd> |]  
-  ==> s'::\<preceq>E"
+  [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd> |]  
+  ==> (x',s')::\<preceq>E"
 apply( simp (no_asm_simp) only: split_tupled_all)
 apply (drule eval_evals_exec_type_sound 
              [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp])
@@ -337,7 +381,7 @@
 
 theorem all_methods_understood: 
 "[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; 
-          s::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>  
+          (x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==>  
   method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
 apply( drule (4) eval_type_sound)
 apply(clarsimp)
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -25,26 +25,33 @@
       locals = "vname \<leadsto> val"  -- "simple state, i.e. variable contents"
 
       state  = "aheap \<times> locals"      -- "heap, local parameter including This"
-      xstate = "xcpt option \<times> state" -- "state including exception information"
+      xstate = "val option \<times> state" -- "state including exception information"
 
 syntax
   heap    :: "state => aheap"
   locals  :: "state => locals"
   Norm    :: "state => xstate"
+  abrupt  :: "xstate \<Rightarrow> val option"
+  store   :: "xstate \<Rightarrow> state"
+  lookup_obj   :: "state \<Rightarrow> val \<Rightarrow> obj"
 
 translations
   "heap"   => "fst"
   "locals" => "snd"
   "Norm s" == "(None,s)"
+  "abrupt"     => "fst"
+  "store"      => "snd"
+ "lookup_obj s a'"  == "the (heap s (the_Addr a'))"
+
 
 constdefs
-  new_Addr  :: "aheap => loc \<times> xcpt option"
- "new_Addr h == SOME (a,x). (h a = None \<and>  x = None) |  x = Some OutOfMemory"
+  raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option"
+  "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
 
-  raise_if  :: "bool => xcpt => xcpt option => xcpt option"
- "raise_if c x xo == if c \<and>  (xo = None) then Some x else xo"
+  new_Addr  :: "aheap => loc \<times> val option"
+  "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"
 
-  np    :: "val => xcpt option => xcpt option"
+  np    :: "val => val option => val option"
  "np v == raise_if (v = Null) NullPointer"
 
   c_hupd  :: "aheap => xstate => xstate"
@@ -58,17 +65,18 @@
 apply (simp (no_asm))
 done
 
-lemma new_AddrD: 
-"(a,x) = new_Addr h ==> h a = None \<and> x = None | x = Some OutOfMemory"
+
+lemma new_AddrD: "new_Addr hp = (ref, xcp) \<Longrightarrow>
+  hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))"
+apply (drule sym)
 apply (unfold new_Addr_def)
 apply(simp add: Pair_fst_snd_eq Eps_split)
 apply(rule someI)
 apply(rule disjI2)
-apply(rule_tac "r" = "snd (?a,Some OutOfMemory)" in trans)
+apply(rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans)
 apply auto
 done
 
-
 lemma raise_if_True [simp]: "raise_if True x y \<noteq> None"
 apply (unfold raise_if_def)
 apply auto
@@ -92,7 +100,7 @@
 done
 
 lemma raise_if_SomeD [rule_format (no_asm)]: 
-  "raise_if c x y = Some z \<longrightarrow> c \<and>  Some z = Some x |  y = Some z"
+  "raise_if c x y = Some z \<longrightarrow> c \<and>  Some z = Some (Addr (XcptRef x)) |  y = Some z"
 apply (unfold raise_if_def)
 apply auto
 done
@@ -119,7 +127,7 @@
 apply auto
 done
 
-lemma np_Null [simp]: "np Null None = Some NullPointer"
+lemma np_Null [simp]: "np Null None = Some (Addr (XcptRef NullPointer))"
 apply (unfold np_def raise_if_def)
 apply auto
 done
@@ -130,7 +138,7 @@
 done
 
 lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) =  
-  Some (if c then xc else NullPointer)"
+  Some (Addr (XcptRef (if c then  xc else NullPointer)))"
 apply (unfold raise_if_def)
 apply (simp (no_asm))
 done
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -170,6 +170,18 @@
 
 lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
 
+lemma field_rec: "\<lbrakk>class G C = Some (D, fs, ms); wf_prog wf_mb G\<rbrakk>
+\<Longrightarrow> field (G, C) =
+   (if C = Object then empty else field (G, D)) ++
+   map_of (map (\<lambda>(s, f). (s, C, f)) fs)"
+apply (simp only: field_def)
+apply (frule fields_rec, assumption)
+apply (rule HOL.trans)
+apply (simp add: o_def)
+apply (simp (no_asm_use) 
+  add: split_beta split_def o_def map_compose [THEN sym] del: map_compose)
+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)
@@ -177,6 +189,19 @@
   apply (auto dest: map_of_SomeD)
   done
 
+
+lemma fields_Object [simp]: "\<lbrakk> ((vn, C), T) \<in> set (fields (G, Object)); wf_prog wf_mb G \<rbrakk>
+  \<Longrightarrow> C = Object"
+apply (frule class_Object)
+apply clarify
+apply (subgoal_tac "fields (G, Object) = map (\<lambda>(fn,ft). ((fn,Object),ft)) fs")
+apply (simp add: image_iff split_beta)
+apply auto
+apply (rule trans)
+apply (rule fields_rec, assumption+)
+apply simp
+done
+
 lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object"
 apply(erule subcls1_induct)
 apply(  assumption)
@@ -312,6 +337,19 @@
 apply( fast intro: subcls1I)
 done
 
+
+lemma wf_prog_wf_mhead: "\<lbrakk> wf_prog wf_mb G; (C, D, fds, mths) \<in> set G;
+  ((mn, pTs), rT, jmb) \<in> set mths \<rbrakk>
+  \<Longrightarrow> wf_mhead G (mn, pTs) rT"
+apply (simp add: wf_prog_def wf_cdecl_def)
+apply (erule conjE)+
+apply (drule bspec, assumption)
+apply simp
+apply (erule conjE)+
+apply (drule bspec, assumption)
+apply (simp add: wf_mdecl_def)
+done
+
 lemma subcls_widen_methd [rule_format (no_asm)]: 
   "[|G\<turnstile>T\<preceq>C T'; wf_prog wf_mb G|] ==>  
    \<forall>D rT b. method (G,T') sig = Some (D,rT ,b) --> 
@@ -377,6 +415,55 @@
  apply (simp add: override_def map_of_map split add: option.split)
 done
 
+
+lemma fields_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
+  \<Longrightarrow> \<forall> vn D T. (((vn,D),T) \<in> set (fields (G,C))
+  \<longrightarrow> (is_class G D \<and> ((vn,D),T) \<in> set (fields (G,D))))"
+apply (erule (1) subcls1_induct)
+
+apply clarify
+apply (frule fields_Object, assumption+)
+apply (simp only: is_class_Object) apply simp
+
+apply clarify
+apply (frule fields_rec)
+apply assumption
+
+apply (case_tac "Da=C")
+apply blast			(* case Da=C *)
+
+apply (subgoal_tac "((vn, Da), T) \<in> set (fields (G, D))") apply blast
+apply (erule thin_rl)
+apply (rotate_tac 1)
+apply (erule thin_rl, erule thin_rl, erule thin_rl, 
+      erule thin_rl, erule thin_rl, erule thin_rl)
+apply auto
+done
+
+lemma field_in_fd [rule_format (no_asm)]: "\<lbrakk> wf_prog wf_mb G; is_class G C\<rbrakk>
+  \<Longrightarrow> \<forall> vn D T. (field (G,C) vn = Some(D,T) 
+  \<longrightarrow> is_class G D \<and> field (G,D) vn = Some(D,T))"
+apply (erule (1) subcls1_induct)
+
+apply clarify
+apply (frule field_fields)
+apply (drule map_of_SomeD)
+apply (drule fields_Object, assumption+)
+apply simp
+
+apply clarify
+apply (subgoal_tac "((field (G, D)) ++ map_of (map (\<lambda>(s, f). (s, C, f)) fs)) vn = Some (Da, T)")
+apply (simp (no_asm_use) only:  override_Some_iff)
+apply (erule disjE)
+apply (simp (no_asm_use) add: map_of_map) apply blast
+apply blast
+apply (rule trans [THEN sym], rule sym, assumption)
+apply (rule_tac x=vn in fun_cong)
+apply (rule trans, rule field_rec, assumption+)
+apply (simp (no_asm_use)) apply blast
+done
+
+
 lemma widen_methd: 
 "[| method (G,C) sig = Some (md,rT,b); wf_prog wf_mb G; G\<turnstile>T''\<preceq>C C|] 
   ==> \<exists>md' rT' b'. method (G,T'') sig = Some (md',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
@@ -384,6 +471,15 @@
 apply   auto
 done
 
+lemma widen_field: "\<lbrakk> (field (G,C) fn) = Some (fd, fT); wf_prog wf_mb G; is_class G C \<rbrakk>
+  \<Longrightarrow> G\<turnstile>C\<preceq>C fd"
+apply (rule widen_fields_defpl)
+apply (simp add: field_def)
+apply (rule map_of_SomeD)
+apply (rule table_of_remap_SomeD) 
+apply assumption+
+done
+
 lemma Call_lemma: 
 "[|method (G,C) sig = Some (md,rT,b); G\<turnstile>T''\<preceq>C C; wf_prog wf_mb G;  
   class G C = Some y|] ==> \<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \<and>  
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Wed Oct 23 16:09:02 2002 +0200
@@ -96,15 +96,21 @@
 apply     auto
 done
 
+lemma typeof_default_val: "\<exists>T. (typeof dt (default_val ty) = Some T) \<and> G\<turnstile> T \<preceq> ty"
+apply (case_tac ty)
+apply (case_tac prim_ty)
+apply auto
+done
+
 types
   java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
 -- "method body with parameter names, local variables, block, result expression."
 -- "local variables might include This, which is hidden anyway"
 
 consts
-  ty_expr :: "java_mb env => (expr      \<times> ty     ) set"
-  ty_exprs:: "java_mb env => (expr list \<times> ty list) set"
-  wt_stmt :: "java_mb env =>  stmt                 set"
+  ty_expr :: "(java_mb env \<times> expr      \<times> ty     ) set"
+  ty_exprs:: "(java_mb env \<times> expr list \<times> ty list) set"
+  wt_stmt :: "(java_mb env \<times> stmt               ) set"
 
 syntax (xsymbols)
   ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
@@ -118,11 +124,11 @@
 
 
 translations
-  "E\<turnstile>e :: T" == "(e,T) \<in> ty_expr  E"
-  "E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E"
-  "E\<turnstile>c \<surd>"    == "c     \<in> wt_stmt  E"
+  "E\<turnstile>e :: T" == "(E,e,T) \<in> ty_expr"
+  "E\<turnstile>e[::]T" == "(E,e,T) \<in> ty_exprs"
+  "E\<turnstile>c \<surd>"    == "(E,c)   \<in> wt_stmt"
   
-inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intros
+inductive "ty_expr" "ty_exprs" "wt_stmt" intros
   
   NewC: "[| is_class (prg E) C |] ==>
          E\<turnstile>NewC C::Class C"  -- "cf. 15.8"
@@ -150,7 +156,7 @@
   -- "cf. 15.25, 15.25.1"
   LAss: "[| v ~= This;
             E\<turnstile>LAcc v::T;
-      E\<turnstile>e::T';
+            E\<turnstile>e::T';
             prg E\<turnstile>T'\<preceq>T |] ==>
          E\<turnstile>v::=e::T'"
 
@@ -204,6 +210,7 @@
            E\<turnstile>s\<surd> |] ==>
         E\<turnstile>While(e) s\<surd>"
 
+
 constdefs
 
  wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
@@ -222,9 +229,22 @@
 translations
   "wf_java_prog" == "wf_prog wf_java_mdecl"
 
+lemma wf_java_prog_wf_java_mdecl: "\<lbrakk> 
+  wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths \<rbrakk>
+  \<Longrightarrow> wf_java_mdecl G C jmdcl"
+apply (simp add: wf_prog_def) 
+apply (simp add: wf_cdecl_def)
+apply (erule conjE)+
+apply (drule bspec, assumption)
+apply simp
+apply (erule conjE)+
+apply (drule bspec, assumption)
+apply (simp add: wf_mdecl_def split_beta)
+done
 
-lemma wt_is_type: "wf_prog wf_mb G \<Longrightarrow> ((G,L)\<turnstile>e::T \<longrightarrow> is_type G T) \<and>  
-       ((G,L)\<turnstile>es[::]Ts \<longrightarrow> Ball (set Ts) (is_type G)) \<and> ((G,L)\<turnstile>c \<surd> \<longrightarrow> True)"
+lemma wt_is_type: "(E\<turnstile>e::T \<longrightarrow> wf_prog wf_mb (prg E) \<longrightarrow> is_type (prg E) T) \<and>  
+       (E\<turnstile>es[::]Ts \<longrightarrow> wf_prog wf_mb (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and> 
+       (E\<turnstile>c \<surd> \<longrightarrow> True)"
 apply (rule ty_expr_ty_exprs_wt_stmt.induct)
 apply auto
 apply (   erule typeof_empty_is_type)
@@ -237,6 +257,6 @@
             simp add: wf_mdecl_def)
 done
 
-lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, COMP swap_prems_rl]
+lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, rule_format]
 
 end
diff -r eec2582923f6 -r b95d12325b51 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Mon Oct 21 17:23:23 2002 +0200
+++ b/src/HOL/MicroJava/ROOT.ML	Wed Oct 23 16:09:02 2002 +0200
@@ -3,6 +3,7 @@
 add_path "J";
 add_path "JVM";
 add_path "BV";
+add_path "Comp";
 
 no_document use_thy "While_Combinator";
 
@@ -14,3 +15,6 @@
 use_thy "LBVJVM";
 use_thy "BVNoTypeError";
 use_thy "BVExample";
+
+use_thy "CorrComp";
+use_thy "CorrCompTp";