# HG changeset patch
# User oheimb
# Date 976126236 -3600
# Node ID 78b1d6c3ee9cfa8c1b6757e0395988f268c1480d
# Parent  779af7c5874354f9cc9dbe2b2d202e157f2a2c4b
improved superclass entry for classes and definition status of is_class, class
corrected recursive definitions of "method" and "fields"
cleanup of many proofs, removed superfluous tactics and theorems

diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/Conform.ML
--- a/src/HOL/MicroJava/J/Conform.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Conform.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -6,71 +6,59 @@
 
 section "hext";
 
-val hextI = prove_goalw thy [hext_def] "!!h. \
-\ \\<forall>a C fs . h  a = Some (C,fs) -->  \
-\     (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'" (K [Auto_tac ]);
+Goalw [hext_def] 
+" \\<forall>a C fs . h  a = Some (C,fs) -->  \
+\     (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'"; 
+by Auto_tac;
+qed "hextI";
 
-val hext_objD = prove_goalw thy [hext_def] 
-"!!h. [|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')" 
-	(K [Force_tac 1]);
+Goalw [hext_def] "[|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')";
+by (Force_tac 1);
+qed "hext_objD";
 
-val hext_refl = prove_goal thy "h\\<le>|h" (K [
-	rtac hextI 1,
-	Fast_tac 1]);
+Goal "h\\<le>|h";
+by (rtac hextI 1);
+by (Fast_tac 1);
+qed "hext_refl";
 
-val hext_new = prove_goal thy "!!h. h a = None ==> h\\<le>|h(a\\<mapsto>x)" (K [
-	rtac hextI 1,
-	safe_tac HOL_cs,
-	 ALLGOALS (case_tac "aa = a"),
-	   Auto_tac]);
+Goal "h a = None ==> h\\<le>|h(a\\<mapsto>x)";
+by (rtac hextI 1);
+by Auto_tac;
+qed "hext_new";
 
-val hext_trans = prove_goal thy "!!h. [|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''" (K [
-	rtac hextI 1,
-	safe_tac HOL_cs,
-	 fast_tac (HOL_cs addDs [hext_objD]) 1]);
+Goal "[|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''";
+by (rtac hextI 1);
+by (fast_tac (HOL_cs addDs [hext_objD]) 1);
+qed "hext_trans";
 
 Addsimps [hext_refl, hext_new];
 
-val hext_upd_obj = prove_goal thy 
-"!!h. h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
-	rtac hextI 1,
-	safe_tac HOL_cs,
-	 ALLGOALS (case_tac "aa = a"),
-	   Auto_tac]);
+Goal "h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))";
+by (rtac hextI 1);
+by Auto_tac;
+qed "hext_upd_obj";
 
 
 section "conf";
 
-val conf_Null = prove_goalw thy [conf_def] 
-"G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
+Goalw [conf_def] "G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T"; 
+by (Simp_tac 1);
+qed "conf_Null";
 Addsimps [conf_Null];
 
-val conf_litval = prove_goalw thy [conf_def] 
-"typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T" (K [
-	rtac val_.induct 1,
-	    Auto_tac]) RS mp;
-
-Goalw [conf_def] "G,s\\<turnstile>Unit::\\<preceq>PrimT Void";
-by( Simp_tac 1);
-qed "conf_VoidI";
-
-Goalw [conf_def] "G,s\\<turnstile>Bool b::\\<preceq>PrimT Boolean";
-by( Simp_tac 1);
-qed "conf_BooleanI";
+Goalw [conf_def] "typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T";
+by (rtac val_.induct 1);
+by Auto_tac;
+qed_spec_mp "conf_litval";
+Addsimps[conf_litval];
 
-Goalw [conf_def] "G,s\\<turnstile>Intg i::\\<preceq>PrimT Integer";
-by( Simp_tac 1);
-qed "conf_IntegerI";
-
-Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
+Goalw [conf_def] "[|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T";
+by (Asm_full_simp_tac 1);
+qed "conf_AddrI";
 
-val conf_AddrI = prove_goalw thy [conf_def] 
-"!!G. [|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T"
-(K [Asm_full_simp_tac 1]);
-
-val conf_obj_AddrI = prove_goalw thy [conf_def]
- "!!G. [|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D" 
-(K [Asm_full_simp_tac 1]);
+Goalw [conf_def] "[|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D"; 
+by (Asm_full_simp_tac 1);
+qed "conf_obj_AddrI";
 
 Goalw [conf_def] "is_type G T --> G,h\\<turnstile>default_val T::\\<preceq>T";
 by (res_inst_tac [("y","T")] ty.exhaust 1);
@@ -79,39 +67,25 @@
 by    (auto_tac (claset(), simpset() addsimps [widen.null]));
 qed_spec_mp "defval_conf";
 
-val conf_upd_obj = prove_goalw thy [conf_def] 
-"h a = Some (C,fs) --> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)" (fn _ => [
-	rtac impI 1,
-	rtac val_.induct 1,
-	 ALLGOALS Simp_tac,
-	case_tac "loc = a" 1,
-	 ALLGOALS Asm_simp_tac]) RS mp;
-
-val conf_widen = prove_goalw thy [conf_def] 
-"!!G. wf_prog wf_mb G ==> G,h\\<turnstile>x::\\<preceq>T --> G\\<turnstile>T\\<preceq>T' --> G,h\\<turnstile>x::\\<preceq>T'" (K [
-	rtac val_.induct 1,
-	    ALLGOALS Simp_tac,
-	    ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
-bind_thm ("conf_widen", conf_widen);
+Goalw [conf_def] 
+"h a = Some (C,fs) ==> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)";
+by (rtac val_.induct 1);
+by Auto_tac;
+qed "conf_upd_obj";
 
-val conf_hext' = prove_goalw thy [conf_def] 
-	"!!h. h\\<le>|h' ==> (\\<forall>v T. G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T)" (K [
-	REPEAT (rtac allI 1),
-	rtac val_.induct 1,
-	 ALLGOALS Simp_tac,
-	safe_tac (HOL_cs addSDs [option_map_SomeD]),
-	rewtac option_map_def,
-	  dtac hext_objD 1,
-	   Auto_tac]);
-val conf_hext = conf_hext' RS spec RS spec RS mp;
-bind_thm ("conf_hext", conf_hext);
+Goalw [conf_def] "wf_prog wf_mb G ==> G,h\\<turnstile>x::\\<preceq>T --> G\\<turnstile>T\\<preceq>T' --> G,h\\<turnstile>x::\\<preceq>T'";
+by (rtac val_.induct 1);
+by (auto_tac (claset() addIs [widen_trans], simpset()));
+qed_spec_mp "conf_widen";
 
-val new_locD = prove_goalw thy [conf_def] 
-	"[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a" (fn prems => [
-	cut_facts_tac prems 1,
-	Full_simp_tac 1,
-	safe_tac HOL_cs,
-	Asm_full_simp_tac 1]);
+Goalw [conf_def] "h\\<le>|h' ==> G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T";
+by (rtac val_.induct 1);
+by (auto_tac (claset() addDs [hext_objD], simpset()));
+qed_spec_mp "conf_hext";
+
+Goalw [conf_def] "[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a";
+by Auto_tac;
+qed "new_locD";
 
 Goalw [conf_def]
  "G,h\\<turnstile>a'::\\<preceq>RefT T --> a' = Null |  \
@@ -120,34 +94,28 @@
 by(Auto_tac);
 qed_spec_mp "conf_RefTD";
 
-val conf_NullTD = prove_goal thy "!!G. G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null" (K [
-	dtac conf_RefTD 1,
-	Step_tac 1,
-	 Auto_tac]);
+Goal "G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null";
+by (dtac conf_RefTD 1);
+by Auto_tac;
+qed "conf_NullTD";
 
-val non_npD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
-\ \\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t" (K [
-	dtac conf_RefTD 1,
-	Step_tac 1,
-	 Auto_tac]);
+Goal "[|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
+\ \\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t";
+by (dtac conf_RefTD 1);
+by Auto_tac;
+qed "non_npD";
 
-val non_np_objD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
-\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>C'\\<preceq>C C)" 
-	(K[fast_tac (claset() addDs [non_npD]) 1]);
+Goal "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
+\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>C'\\<preceq>C C)";
+by (fast_tac (claset() addDs [non_npD]) 1);
+qed "non_np_objD";
 
-Goal "a' \\<noteq> Null --> wf_prog wf_mb G --> G,h\\<turnstile>a'::\\<preceq>RefT t -->\
+Goal "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)";
-by(rtac impI 1);
-by(rtac impI 1);
 by(res_inst_tac [("y","t")] ref_ty.exhaust 1);
- by(Safe_tac);
- by(dtac conf_NullTD 1);
- by(contr_tac 1);
-by(dtac non_np_objD 1);
-  by(atac 1);
- by(Fast_tac 1);
-by(Fast_tac 1);
+ by (fast_tac (claset() addDs [conf_NullTD]) 1);
+by (fast_tac (claset() addDs [non_np_objD]) 1);
 qed_spec_mp "non_np_objD'";
 
 Goal "wf_prog wf_mb G ==> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' -->  list_all2 (conf G h) vs Ts'";
@@ -165,20 +133,18 @@
 
 section "lconf";
 
-val lconfD = prove_goalw thy [lconf_def] 
-   "!!X. [| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T"
- (K [Force_tac 1]);
+Goalw[lconf_def] "[| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T";
+by (Force_tac 1);
+qed "lconfD";
 
-val lconf_hext = prove_goalw thy [lconf_def] 
-	"!!X. [| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L" (K [
-		fast_tac (claset() addEs [conf_hext]) 1]);
+Goalw [lconf_def] "[| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L";
+by  (fast_tac (claset() addEs [conf_hext]) 1);
+qed "lconf_hext";
 AddEs [lconf_hext];
 
 Goalw [lconf_def] "!!X. [| G,h\\<turnstile>l[::\\<preceq>]lT; \
 \ G,h\\<turnstile>v::\\<preceq>T; lT va = Some T |] ==> G,h\\<turnstile>l(va\\<mapsto>v)[::\\<preceq>]lT";
-by( Clarify_tac 1);
-by( case_tac "n = va" 1);
- by Auto_tac;
+by Auto_tac;
 qed "lconf_upd";
 
 Goal "\\<forall>x. P x --> R (dv x) x ==> (\\<forall>x. map_of fs f = Some x --> P x) --> \
@@ -199,9 +165,9 @@
 qed "lconf_init_vars";
 AddSIs [lconf_init_vars];
 
-val lconf_ext = prove_goalw thy [lconf_def] 
-"!!X. [|G,s\\<turnstile>l[::\\<preceq>]L; G,s\\<turnstile>v::\\<preceq>T|] ==> G,s\\<turnstile>l(vn\\<mapsto>v)[::\\<preceq>]L(vn\\<mapsto>T)" 
-	(K [Auto_tac]);
+Goalw [lconf_def] "[|G,s\\<turnstile>l[::\\<preceq>]L; G,s\\<turnstile>v::\\<preceq>T|] ==> G,s\\<turnstile>l(vn\\<mapsto>v)[::\\<preceq>]L(vn\\<mapsto>T)";
+by Auto_tac;
+qed "lconf_ext";
 
 Goalw [lconf_def] "G,h\\<turnstile>l[::\\<preceq>]L ==> \\<forall>vs Ts. nodups vns --> length Ts = length vns --> list_all2 (\\<lambda>v T. G,h\\<turnstile>v::\\<preceq>T) vs Ts --> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[::\\<preceq>]L(vns[\\<mapsto>]Ts)";
 by( induct_tac "vns" 1);
@@ -213,14 +179,15 @@
 
 section "oconf";
 
-val oconf_hext = prove_goalw thy [oconf_def] 
-"!!X. G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
+Goalw [oconf_def] "G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>"; 
+by (Fast_tac 1);
+qed "oconf_hext";
 
-val oconf_obj = prove_goalw thy [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
-\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and>  G,h\\<turnstile>v::\\<preceq>T))"(K [
-	Auto_tac]);
-
-val oconf_objD = oconf_obj RS iffD1 RS spec RS spec RS mp;
+Goalw [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
+\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and>  G,h\\<turnstile>v::\\<preceq>T))";
+by Auto_tac;
+qed "oconf_obj";
+bind_thm ("oconf_objD", oconf_obj RS iffD1 RS spec RS spec RS mp);
 
 
 section "hconf";
@@ -236,19 +203,17 @@
 
 section "conforms";
 
-val conforms_heapD = prove_goalw thy [conforms_def]
-	"(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>"
-	(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
+Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>";
+by (Asm_full_simp_tac 1);
+qed "conforms_heapD";
 
-val conforms_localD = prove_goalw thy [conforms_def]
-	 "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT" (fn prems => [
-	cut_facts_tac prems 1, Asm_full_simp_tac 1]);
+Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT";
+by (Asm_full_simp_tac 1);
+qed "conforms_localD";
 
-val conformsI = prove_goalw thy [conforms_def] 
-"[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)" (fn prems => [
-	cut_facts_tac prems 1,
-	Simp_tac 1,
-	Auto_tac]);
+Goalw [conforms_def] "[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)"; 
+by Auto_tac;
+qed "conformsI";
 
 Goal "[|(h,l)::\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> |] ==> (h',l)::\\<preceq>(G,lT)";
 by( fast_tac (HOL_cs addDs [conforms_localD] 
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/Decl.ML
--- a/src/HOL/MicroJava/J/Decl.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Decl.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -4,12 +4,8 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
-	rtac finite_map_of 1]);
+Goal "finite {C. is_class G C}";
+by (fold_goals_tac [dom_def]);
+by (rtac finite_dom_map_of 1);
+qed "finite_is_class";
 
-val is_classI = prove_goalw thy [is_class_def]
-"!!G. class G C = Some c ==> is_class G C" (K [Auto_tac]);
-
-val is_classD = prove_goalw thy [is_class_def]
-"!!G. is_class G C ==> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
-	not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Wed Dec 06 19:10:36 2000 +0100
@@ -19,7 +19,7 @@
 	= "sig \\<times> ty \\<times> 'c"
 
 types	'c class		(* class *)
-	= "cname option \\<times> fdecl list \\<times> 'c mdecl list"
+	= "cname \\<times> fdecl list \\<times> 'c mdecl list"
 	(* superclass, fields, methods*)
 
 	'c cdecl		(* class declaration, cf. 8.1 *)
@@ -32,23 +32,33 @@
 
 defs 
 
- ObjectC_def "ObjectC == (Object, (None, [], []))"
+ ObjectC_def "ObjectC == (Object, (arbitrary, [], []))"
 
 
 types 'c prog = "'c cdecl list"
 
+
+translations
+  "fdecl"   <= (type) "vname \\<times> ty"
+  "sig"     <= (type) "mname \\<times> ty list"
+  "mdecl c" <= (type) "sig \\<times> ty \\<times> c"
+  "class c" <= (type) "cname \\<times> fdecl list \\<times> (c mdecl) list"
+  "cdecl c" <= (type) "cname \\<times> (c class)"
+  "prog  c" <= (type) "(c cdecl) list"
+
 consts
 
   class		:: "'c prog => (cname \\<leadsto> 'c class)"
+  is_class	:: "'c prog => cname => bool"
 
-  is_class	:: "'c prog => cname => bool"
-  is_type	:: "'c prog => ty    => bool"
+translations
 
-defs
+  "class"        => "map_of"
+  "is_class G C" == "class G C \\<noteq> None"
 
-  class_def	"class        == map_of"
+consts
 
-  is_class_def	"is_class G C == class G C \\<noteq> None"
+  is_type	:: "'c prog => ty    => bool"
 
 primrec
 "is_type G (PrimT pt) = True"
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/Eval.ML
--- a/src/HOL/MicroJava/J/Eval.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Eval.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -7,7 +7,7 @@
 Goal "[|new_Addr (heap s) = (a,x); \
 \      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
 \      G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> s'";
-by (hyp_subst_tac 1);
+by (Asm_simp_tac 1);
 br eval_evals_exec.NewC 1;
 by Auto_tac;
 qed "NewCI";
@@ -21,27 +21,32 @@
 by(ALLGOALS Asm_full_simp_tac);
 qed "eval_evals_exec_no_xcpt";
 
-val eval_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None" (K [
-	dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1,
-	Fast_tac 1]);
-val evals_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None" (K [
-	dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1,
-	Fast_tac 1]);
+Goal "G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None";
+by (dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1);
+by (Fast_tac 1);
+qed "eval_no_xcpt";
 
-val eval_evals_exec_xcpt = prove_goal thy 
+Goal "G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None";
+by (dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1);
+by (Fast_tac 1);
+qed "evals_no_xcpt";
+
+Goal 
 "!!s s'. (G\\<turnstile>(x,s) -e \\<succ>  v -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
 \        (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
-\        (G\\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)"
- (K [
-	split_all_tac 1,
-	rtac eval_evals_exec.induct 1,
-	rewtac c_hupd_def,
-	ALLGOALS Asm_full_simp_tac]);
-val eval_xcpt = prove_goal thy 
-"!!X. G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
-	dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1,
-	Fast_tac 1]);
-val exec_xcpt = prove_goal thy 
-"!!X. G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
-	dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
-	Fast_tac 1]);
+\        (G\\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)";
+by (split_all_tac 1);
+by (rtac eval_evals_exec.induct 1);
+by (rewtac c_hupd_def);
+by (ALLGOALS Asm_full_simp_tac);
+qed "eval_evals_exec_xcpt";
+
+Goal "G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and>  s'=s";
+by (dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1);
+by (Fast_tac 1);
+qed "eval_xcpt";  
+
+Goal "G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and>  s'=s";
+by (dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1);
+by (Fast_tac 1);
+qed "exec_xcpt";
\ No newline at end of file
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/Example.ML
--- a/src/HOL/MicroJava/J/Example.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Example.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -1,35 +1,37 @@
-
-AddIs [widen.null];
 
 Addsimps [inj_cnam_, inj_vnam_];
 Addsimps [Base_not_Object,Ext_not_Object];
 Addsimps [Base_not_Object RS not_sym,Ext_not_Object RS not_sym];
 
-val map_of_Cons = prove_goalw thy [get_def thy "map_of_list"] 
-"map_of (p#ps) = (map_of ps)(fst p |-> snd p)" (K [Simp_tac 1]);
-val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"] 
-"map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]);
-val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"] 
-"!!X. x\\<noteq>k ==> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
+bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps")));
+Goal "map_of ((aa,bb)#ps) aa = Some bb";
+by (Simp_tac 1);
+qed "map_of_Cons1";
+Goal "aa\\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa";
+by (Asm_simp_tac 1);
+qed "map_of_Cons2";
 Delsimps[map_of_Cons]; (* sic! *)
 Addsimps[map_of_Cons1, map_of_Cons2];
 
-val class_tprg_Object = prove_goalw thy [class_def, ObjectC_def] 
- 	"class tprg Object = Some (None, [], [])" 
-	(K [Simp_tac 1]);
-val class_tprg_Base = prove_goalw thy [class_def, ObjectC_def, BaseC_def, 
- ExtC_def] "class tprg Base = Some (Some Object, \
+Goalw [ObjectC_def] "class tprg Object = Some (arbitrary, [], [])";
+by (Simp_tac 1);
+qed "class_tprg_Object";
+
+Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg Base = Some (Object, \
 	\ [(vee, PrimT Boolean)], \
-        \ [((foo, [Class Base]), Class Base, foo_Base)])" (K [
-	Simp_tac 1]);
-val class_tprg_Ext = prove_goalw thy [class_def, ObjectC_def, BaseC_def, 
- ExtC_def] "class tprg Ext = Some (Some Base, \
+        \ [((foo, [Class Base]), Class Base, foo_Base)])";
+by (Simp_tac 1);
+qed "class_tprg_Base";
+
+Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg Ext = Some (Base, \
 	\ [(vee, PrimT Integer)], \
-        \ [((foo, [Class Base]), Class Ext, foo_Ext)])" (K [
-	Simp_tac 1]);
+        \ [((foo, [Class Base]), Class Ext, foo_Ext)])";
+by (Simp_tac 1);
+qed "class_tprg_Ext";
+
 Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];
 
-Goal "!!X. (Object,C) \\<in> (subcls1 tprg)^+ ==> R";
+Goal "(Object,C) \\<in> (subcls1 tprg)^+ ==> R";
 by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
 qed "not_Object_subcls";
 AddSEs [not_Object_subcls];
@@ -42,13 +44,13 @@
 qed "subcls_ObjectD";
 AddSDs[subcls_ObjectD];
 
-Goal "!!X. (Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
+Goal "(Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
 by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
 qed "not_Base_subcls_Ext";
 AddSEs [not_Base_subcls_Ext];
 
-Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
-by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm]));
+Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
+by (auto_tac (claset(),simpset()addsplits[split_if_asm]addsimps[map_of_Cons]));
 qed "class_tprgD";
 
 Goal "(C,C) \\<in> (subcls1 tprg)^+ ==> R";
@@ -66,13 +68,13 @@
 
 bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl);
 
-Goalw [] "tprg\\<turnstile>Ext\\<preceq>C Base";
+Goal "tprg\\<turnstile>Ext\\<preceq>C Base";
 br subcls_direct 1;
-by (Simp_tac 1);
+by Auto_tac;
 qed "Ext_subcls_Base";
 Addsimps [Ext_subcls_Base];
 
-Goalw [] "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
+Goal "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
 br widen.subcls 1;
 by (Simp_tac 1);
 qed "Ext_widen_Base";
@@ -89,8 +91,6 @@
 val wf_subcls1_=acyclic_subcls1_ RS(finite_subcls1 RS finite_acyclic_wf_converse);
 
 
-Addsimps[is_class_def];
-
 val fields_rec_ = wf_subcls1_ RSN (1, fields_rec_lemma);
 
 Goal "fields (tprg, Object) = []";
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Wed Dec 06 19:10:36 2000 +0100
@@ -75,13 +75,13 @@
 defs
 
   foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
-  BaseC_def "BaseC == (Base, (Some Object, 
+  BaseC_def "BaseC == (Base, (Object, 
 			     [(vee, PrimT Boolean)], 
 			     [((foo,[Class Base]),Class Base,foo_Base)]))"
   foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
 				       (LAcc x)..vee:=Lit (Intg #1)),
 				   Lit Null)"
-  ExtC_def  "ExtC  == (Ext,  (Some Base  , 
+  ExtC_def  "ExtC  == (Ext,  (Base  , 
 			     [(vee, PrimT Integer)], 
 			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
 
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/JBasis.ML
--- a/src/HOL/MicroJava/J/JBasis.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/JBasis.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -4,92 +4,21 @@
     Copyright   1999 TU Muenchen
 *)
 
-val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE]));
-
-Goalw [image_def]
-	"x \\<in> f``A ==> \\<exists>y. y \\<in> A \\<and>  x = f y";
-by(Auto_tac);
-qed "image_rev";
-
-fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
-
-val select_split = prove_goalw Product_Type.thy [split_def] 
-	"(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
-	 
-
-val split_beta = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
-	(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
-val split_beta2 = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
-	(fn _ => [Auto_tac]);
-val splitE2 = prove_goal Product_Type.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
-	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
-	rtac (split_beta RS subst) 1,
-	rtac (hd prems) 1]);
-val splitE2' = prove_goal Product_Type.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
-	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
-	res_inst_tac [("P1","P")] (split_beta RS subst) 1,
-	rtac (hd prems) 1]);
-	
-
-fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
-
-val BallE = prove_goal thy "[|Ball A P; x \\<notin> A ==> Q; P x ==> Q |] ==> Q"
-	(fn prems => [rtac ballE 1, resolve_tac prems 1, 
-			eresolve_tac prems 1, eresolve_tac prems 1]);
-
-val set_cs2 = set_cs delrules [ballE] addSEs [BallE];
+(*###TO Product_Type*)
+Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
+by (rtac refl 1);
+qed "select_split";
 
 Addsimps [Let_def];
 
-(* To HOL.ML *)
-
-val ex1_some_eq_trivial = prove_goal HOL.thy "[| \\<exists>!x. P x; P y |] ==> Eps P = y" 
-	(fn prems => [
-	cut_facts_tac prems 1,
-	rtac some_equality 1,
-	 atac 1,
-	etac ex1E 1,
-	etac all_dupE 1,
-	fast_tac HOL_cs 1]);
-
-
-val ball_insert = prove_goalw equalities.thy [Ball_def]
-	"Ball (insert x A) P = (P x \\<and> Ball A P)" (fn _ => [
-	fast_tac set_cs 1]);
-
-fun option_case_tac i = EVERY [
-	etac option_caseE i,
-	 rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), 
-	 rotate_tac ~2  i   , asm_full_simp_tac HOL_basic_ss i];
-
-val not_None_tac = EVERY' [dtac (not_None_eq RS iffD1),rotate_tac ~1,etac exE,
-		rotate_tac ~1,asm_full_simp_tac 
-	(simpset() delsimps [split_paired_All,split_paired_Ex])];
-
-Goal "{y. x = Some y} \\<subseteq> {the x}";
-by Auto_tac;
-qed "some_subset_the";
-
-fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
-  asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
-
-val optionE = prove_goal thy 
-       "[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" 
-   (fn prems => [
-	case_tac "opt = None" 1,
-	 eresolve_tac prems 1,
-	not_None_tac 1,
-	eresolve_tac prems 1]);
-
-fun option_case_tac2 s i = EVERY [
-	 case_tac s i,
-	 rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), 
-	 rotate_tac ~1  i   , asm_full_simp_tac HOL_basic_ss i];
-
-val option_map_SomeD = prove_goalw thy [option_map_def]
-	"!!x. option_map f x = Some y ==> \\<exists>z. x = Some z \\<and> f z = y" (K [
-	option_case_tac2 "x" 1,
-	 Auto_tac]);
+(* ### To HOL.ML *)
+Goal "[| ?!x. P x; P y |] ==> Eps P = y"; 
+by (rtac some_equality 1);
+by  (atac 1);
+by (etac ex1E 1);
+by (etac all_dupE 1);
+by (fast_tac HOL_cs 1);
+qed "ex1_some_eq_trivial";
 
 
 section "unique";
@@ -103,7 +32,7 @@
 by (Simp_tac 1);
 qed "unique_Nil";
 
-Goalw [unique_def] "unique ((x,y)#l) = (unique l \\<and> (!y. (x,y) ~: set l))";
+Goalw [unique_def] "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))";
 by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
 qed "unique_Cons";
 
@@ -120,47 +49,14 @@
 by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
 qed_spec_mp "unique_map_inj";
 
-Goal "!!l. unique l ==> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
-by(etac unique_map_inj 1);
-by(rtac injI 1);
-by Auto_tac;
-qed "unique_map_Pair";
-
-Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N";
-by(rtac set_ext 1);
-by(simp_tac (simpset() addsimps image_def::premises()) 1);
-qed "image_cong";
-
-val split_Pair_eq = prove_goal Product_Type.thy 
-"!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
-	etac imageE 1,
-	split_all_tac 1,
-	auto_tac(claset_of Product_Type.thy,simpset_of Product_Type.thy)]);
-
-
 (* More about Maps *)
 
-val override_SomeD = prove_goalw thy [override_def] "(s ++ t) k = Some x ==> \
-\ t k = Some x |  t k = None \\<and>  s k = Some x" (fn prems => [
-	cut_facts_tac prems 1,
-	case_tac "\\<exists>x. t k = Some x" 1,
-	 etac exE 1,
-	 rotate_tac ~1 1,
-	 Asm_full_simp_tac 1,
-	asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1,
-	 rotate_tac ~1 1,
-	 Asm_full_simp_tac 1]);
+(*###Addsimps [fun_upd_same, fun_upd_other];*)
 
-Addsimps [fun_upd_same, fun_upd_other];
-
-Goal "unique xys --> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
-by(induct_tac "xys" 1);
- by(Simp_tac 1);
-by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
-qed_spec_mp "unique_map_of_Some_conv";
-
-val in_set_get = unique_map_of_Some_conv RS iffD2;
-val get_in_set = unique_map_of_Some_conv RS iffD1;
+Goal "unique l --> (k, x) : set l --> map_of l k = Some x";
+by (induct_tac "l" 1);
+by  Auto_tac;
+qed_spec_mp "map_of_SomeI";
 
 Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)";
 by(induct_tac "l" 1);
@@ -169,50 +65,14 @@
 by Auto_tac;
 bind_thm("Ball_set_table",result() RS mp);
 
-val table_mono = prove_goal thy 
-"unique l' --> (\\<forall>xy. (xy)\\<in>set l --> (xy)\\<in>set l') -->\
-\ (\\<forall>k y. map_of l k = Some y --> map_of l' k = Some y)" (fn _ => [
-	induct_tac "l" 1,
-	 Auto_tac,
- 	 fast_tac (HOL_cs addSIs [in_set_get]) 1])
- RS mp RS mp RS spec RS spec RS mp;
-
-val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) --> \
-\ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
-	induct_tac "t" 1,	
-	 ALLGOALS Simp_tac,
-	case_tac1 "k = fst a" 1,
-	 Auto_tac]) RS mp;
-val table_map_Some = prove_goal thy 
-"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
-\map_of t (k, k') = Some x" (K [
-	induct_tac "t" 1,	
-	Auto_tac]) RS mp;
-
+Goal "map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
+\map_of t (k, k') = Some x";
+by (induct_tac "t" 1);
+by  Auto_tac;
+qed_spec_mp "table_of_remap_SomeD";
 
-val table_mapf_Some = prove_goal thy "!!f. \\<forall>x y. f x = f y --> x = y ==> \
-\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) --> map_of t k = Some x" (K [
-	induct_tac "t" 1,	
-	Auto_tac]) RS mp;
-val table_mapf_SomeD = prove_goal thy 
-"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z --> (\\<exists>y. (k,y)\\<in>set t \\<and>  z = f y)"(K [
-	induct_tac "t" 1,	
-	Auto_tac]) RS mp;
-
-val table_mapf_Some2 = prove_goal thy 
-"!!k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) ==> C = D \\<and> map_of t k = Some x" (K [
-	forward_tac [table_mapf_SomeD] 1,
-	Auto_tac,
-	rtac table_mapf_Some 1,
-	 atac 2,
-	Fast_tac 1]);
-
-val finite_map_of = rewrite_rule [dom_def] finite_dom_map_of;
-
-Goal
-"map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
+(* ### To Map.ML *)
+Goal "map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
 by (induct_tac "xs" 1);
-auto();
+by Auto_tac;
 qed "map_of_map";
-
-
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -7,29 +7,29 @@
 *)
 
 
+
 Addsimps [split_beta];
 
 Goal "[|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)";
 by( etac conforms_upd_obj 1);
 by(  rewtac oconf_def);
-by(  auto_tac (claset() addSDs [is_type_fields, map_of_SomeD], simpset()));
+by(  auto_tac (claset() addSDs [fields_is_type], simpset()));
 qed "NewC_conforms";
-
+ 
 Goalw [cast_ok_def]
  "[| wf_prog wf_mb G; G,h\\<turnstile>v::\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v|] \
 \ ==> G,h\\<turnstile>v::\\<preceq>Class D";
-by( case_tac1 "v = Null" 1);
+by( case_tac "v = Null" 1);
 by(  Asm_full_simp_tac 1);
 by(  dtac widen_RefT 1);
 by(  Clarify_tac 1);
-by(  rtac widen.null 1);
 by( datac non_npD 1 1);
 by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def]));
 qed "Cast_conf";
 
 Goal "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\\<preceq>(G,lT); \
-\    x' = None --> G,h\\<turnstile>a'::\\<preceq> Class C; np a' x' = None |] ==> \
+\ 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";
 by( dtac np_NoneD 1);
 by( etac conjE 1);
@@ -38,11 +38,8 @@
 by   Auto_tac;
 by( dtac (conforms_heapD RS hconfD) 1);
 by(  atac 1);
-by( dtac widen_cfs_fields 1);
-by(   atac 1);
-by(  atac 1);
-by( dtac oconf_objD 1);
-by(  atac 1);
+by( datac widen_cfs_fields 2 1);
+by( datac oconf_objD 1 1);
 by Auto_tac;
 qed "FAcc_type_sound";
 
@@ -62,12 +59,12 @@
 by( dtac non_np_objD 1);
 by(   atac 1);
 by(  SELECT_GOAL Auto_tac 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
 by( Full_simp_tac 1);
 by( EVERY [forward_tac [hext_objD] 1, atac 1]);
 by( etac exE 1);
 by( Asm_full_simp_tac 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
 by( rtac conjI 1);
 by(  fast_tac (HOL_cs addEs [hext_trans, hext_upd_obj]) 1);
 by( rtac conjI 1);
@@ -85,7 +82,7 @@
 by( rtac (oconf_obj RS iffD2) 1);
 by( Simp_tac 1);
 by( strip_tac 1);
-by( case_tac1 "(aaa, b) = (fn, fd)" 1);
+by( case_tac "(aaa, b) = (fn, fd)" 1);
 by(  Asm_full_simp_tac 1);
 by(  fast_tac (HOL_cs addIs [conf_widen]) 1);
 by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1);
@@ -105,8 +102,14 @@
 by( (etac conf_list_gext_widen THEN_ALL_NEW atac) 1);
 qed "Call_lemma2";
 
+Goal "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> is_class G D \\<longrightarrow> is_class G C";
+by (etac rtrancl_induct 1);
+by  (dtac subcls1D 2);
+by  Auto_tac;
+qed_spec_mp "subcls_is_class2"; 
+
 Goalw [wf_java_prog_def]
- "[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); \
+ "[| wf_java_prog G; a' \\<noteq> Null; (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) = \
@@ -117,16 +120,14 @@
 \         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)";
-by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
-by( dtac (max_spec2appl_meths RS appl_methsD) 1);
+by( dtac max_spec2mheads 1);
 by( Clarify_tac 1);
 by( datac non_np_objD' 2 1);
-by(  strip_tac1 1);
-by(  Asm_full_simp_tac 1);
+by(  Clarsimp_tac 1);
 by( Clarsimp_tac 1);
 by( EVERY'[forward_tac [hext_objD], atac] 1);
 by( Clarsimp_tac 1);
-by( EVERY'[dtac Call_lemma, atac, atac] 1);
+by( datac Call_lemma 3 1);
 by( clarsimp_tac (claset(),simpset() addsimps [wf_java_mdecl_def])1);
 by( thin_tac "method ?sig ?x = ?y" 1);
 by( EVERY'[dtac spec, etac impE] 1);
@@ -142,7 +143,7 @@
 (*by( thin_tac "?E::\\<preceq>(G, pT')" 1);*)
 by( EVERY'[dtac spec, mp_tac] 1);
 by( thin_tac "?E\\<turnstile>res::?rT" 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
 by( rtac conjI 1);
 by(  fast_tac (HOL_cs addIs [hext_trans]) 1);
 by( rtac conjI 1);
@@ -163,7 +164,8 @@
 Unify.search_bound := 40;
 Unify.trace_bound  := 40;
 Delsplits[split_if];
-Delsimps[fun_upd_apply];(*###*)
+Delsimps[fun_upd_apply];
+Addsimps[fun_upd_same];
 val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
 	(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
 Goal
@@ -194,10 +196,9 @@
 by( dtac new_AddrD 1);
 by( etac disjE 1);
 by(  Asm_simp_tac 2);
-by( etac conjE 1);
-by( Asm_simp_tac 1);
+by( Clarsimp_tac 1);
 by( rtac conjI 1);
-by(  fast_tac (HOL_cs addSEs [NewC_conforms]) 1);
+by(  force_tac (claset() addSEs [NewC_conforms],simpset()) 1);
 by( rtac conf_obj_AddrI 1);
 by(  rtac rtrancl_refl 2);
 by( Simp_tac 1);
@@ -228,7 +229,7 @@
 			REPEAT o (etac conjE), hyp_subst_tac] 3);
 
 (* for if *)
-by( (case_tac1 "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
+by( (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
 
 by forward_hyp_tac;
 
@@ -266,7 +267,7 @@
 by( fast_tac (claset() addIs [hext_trans]) 3);
 
 (* 2 FAss *)
-by( case_tac1 "x2 = None" 1);
+by( case_tac "x2 = None" 1);
 by(  Asm_simp_tac 2);
 by(  fast_tac (claset() addIs [hext_trans]) 2);
 by( Asm_full_simp_tac 1);
@@ -274,7 +275,7 @@
 by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
 
 by prune_params_tac;
-(* Level 51 *)
+(* Level 50 *)
 
 (* 1 Call *)
 by( case_tac "x" 1);
@@ -287,14 +288,16 @@
 by( Clarify_tac 1);
 by( dtac evals_no_xcpt 1);
 by( Asm_full_simp_tac 1);
-by( case_tac1 "a' = Null" 1);
+by( case_tac "a' = Null" 1);
 by(  Asm_full_simp_tac 1);
 by(  dtac exec_xcpt 1);
 by(  Asm_full_simp_tac 1);
 by(  dtac eval_xcpt 1);
 by(  Asm_full_simp_tac 1);
 by(  fast_tac (HOL_cs addEs [hext_trans]) 1);
-by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) 
+by( datac ty_expr_is_type 1 1);
+by(Clarsimp_tac 1);
+by( (rtac (rewrite_rule [wf_java_prog_def] Call_type_sound) 
     THEN_ALL_NEW Asm_simp_tac) 1);
 qed "eval_evals_exec_type_sound";
 
@@ -318,18 +321,15 @@
 \         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";
 by( datac eval_type_sound 4 1);
-by( not_None_tac 1);
-by( split_all_tac 1);
+by(Clarsimp_tac 1);
 by(rewtac wf_java_prog_def);
 by( forward_tac [widen_methd] 1);
 by(   atac 1);
-by(  rtac (not_None_eq RS iffD1) 2);
 by(  Fast_tac 2);
-by( etac conjE 1);
 by( dtac non_npD 1);
 by Auto_tac;
 qed "all_methods_understood";
 
 Delsimps [split_beta];
-Addsimps[fun_upd_apply];(*###*)
+Addsimps[fun_upd_apply];
 
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/State.ML
--- a/src/HOL/MicroJava/J/State.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/State.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -4,65 +4,69 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-val obj_ty_def2 = prove_goalw thy [obj_ty_def] "obj_ty (C,fs) = Class C" 
-	(K [Simp_tac 1]);
-
+Goalw [obj_ty_def] "obj_ty (C,fs) = Class C";
+by (Simp_tac 1);
+qed "obj_ty_def2";
 Addsimps [obj_ty_def2];
 
-val new_AddrD = prove_goalw thy [new_Addr_def] 
-"!!X. (a,x) = new_Addr h ==> h a = None \\<and>  x = None |  x = Some OutOfMemory" (K[
-	asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
-	rtac someI 1,
-	rtac disjI2 1,
-	res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1,
-	 Auto_tac ]);
-
-val raise_if_True = prove_goalw thy [raise_if_def] 
-	"raise_if True x y \\<noteq> None"
-(K [split_tac [split_if] 1,Auto_tac]);
-
-val raise_if_False = prove_goalw thy [raise_if_def] 
-	"raise_if False x y = y"
-(K [Auto_tac]);
-
-val raise_if_Some = prove_goalw thy [raise_if_def] 
-	"raise_if c x (Some y) \\<noteq> None" (K [Auto_tac]);
-
-val raise_if_Some2 = prove_goalw thy [raise_if_def] 
-"raise_if c z (if x = None then Some y else x) \\<noteq> None" (K[
-	induct_tac "x" 1,
-	Auto_tac]);
-val if_None_eq = prove_goal thy 
-"(if x = None then None else x) = x" (K[
-	induct_tac "x" 1,
-	Auto_tac]);
-
-Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2,if_None_eq];
-
-val raise_if_SomeD = prove_goalw thy [raise_if_def] 
-	"raise_if c x y = Some z --> c \\<and>  Some z = Some x |  y = Some z" 
-(K [split_tac [split_if] 1,Auto_tac]) RS mp;
-
-val raise_if_NoneD = prove_goalw thy [raise_if_def] 
-	"raise_if c x y = None --> \\<not> c \\<and>  y = None"
-(K [split_tac [split_if] 1,Auto_tac]) RS mp;
+Goalw [new_Addr_def] 
+"(a,x) = new_Addr h ==> h a = None \\<and> x = None | x = Some OutOfMemory";
+by(asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1);
+by(rtac someI 1);
+by(rtac disjI2 1);
+by(res_inst_tac [("r","snd (?a,Some OutOfMemory)")] trans 1);
+by Auto_tac;
+qed "new_AddrD";
 
 
-val np_NoneD = (prove_goalw thy [np_def, raise_if_def] 
-	"np a' x' = None --> x' = None \\<and>  a' \\<noteq> Null" (fn _ => [
-	split_tac [split_if] 1,
-	Auto_tac ])) RS mp;
-val np_None = (prove_goalw thy [np_def, raise_if_def] 
-	"a' \\<noteq> Null --> np a' x' = x'" (fn _ => [
-	split_tac [split_if] 1,
-	Auto_tac ])) RS mp;
-val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
-	(fn _ => [Auto_tac ]);
-val np_Null = prove_goalw thy [np_def, raise_if_def] 
-	"np Null None = Some NullPointer" (fn _ => [
-	Auto_tac ]);
-val np_Addr = prove_goalw thy [np_def, raise_if_def] "np (Addr a) None = None" 
-	(fn _ => [Auto_tac ]);
+Goalw [raise_if_def] "raise_if True x y \\<noteq> None";
+by Auto_tac;
+qed "raise_if_True";
+
+Goalw [raise_if_def] "raise_if False x y = y";
+by Auto_tac;
+qed "raise_if_False";
+
+Goalw [raise_if_def] "raise_if c x (Some y) \\<noteq> None";
+by Auto_tac;
+qed "raise_if_Some";
+
+Goalw [raise_if_def] "raise_if c z (if x = None then Some y else x) \\<noteq> None";
+by(induct_tac "x" 1);
+by Auto_tac;
+qed "raise_if_Some2";
+
+Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2];
+
+Goalw [raise_if_def] 
+  "raise_if c x y = Some z \\<longrightarrow> c \\<and>  Some z = Some x |  y = Some z"; 
+by Auto_tac;
+qed_spec_mp "raise_if_SomeD";
+
+Goalw [raise_if_def] "raise_if c x y = None --> \\<not> c \\<and>  y = None";
+by Auto_tac;
+qed_spec_mp "raise_if_NoneD";
+
+Goalw [np_def, raise_if_def] "np a' x' = None --> x' = None \\<and>  a' \\<noteq> Null"; 
+by Auto_tac;
+qed_spec_mp "np_NoneD";
+
+Goalw [np_def, raise_if_def] "a' \\<noteq> Null --> np a' x' = x'";
+by Auto_tac;
+qed_spec_mp "np_None";
+
+Goalw [np_def, raise_if_def] "np a' (Some xc) = Some xc";
+by Auto_tac;
+qed "np_Some";
+
+Goalw [np_def, raise_if_def] "np Null None = Some NullPointer";
+by Auto_tac;
+qed "np_Null";
+
+Goalw [np_def, raise_if_def] "np (Addr a) None = None";
+by Auto_tac;
+qed "np_Addr";
+
 Addsimps[np_None, np_Some,np_Null,np_Addr];
 
 Goalw [raise_if_def] "(np Null (raise_if c xc None)) = \
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -4,44 +4,43 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-val subcls1D = prove_goalw thy [subcls1_def] "!!G. G\\<turnstile>C\\<prec>C1D ==> \
-\ \\<exists>fs ms. class G C = Some (Some D,fs,ms)" (K [Auto_tac]);
+Goalw [subcls1_def] 
+  "G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> C \\<noteq> Object \\<and> (\\<exists>fs ms. class G C = Some (D,fs,ms))";
+by Auto_tac;
+qed "subcls1D";
+Goalw [subcls1_def] "\\<lbrakk>class G C = Some (D,rest); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C1D";
+by Auto_tac;
+qed "subcls1I";
 
-val subcls1I = prove_goalw  thy [subcls1_def] 
-"!!G. [| class G C = Some (Some D,rest) |] ==> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
-
-val subcls1_def2 = prove_goalw thy [subcls1_def,is_class_def]  "subcls1 G = \
-\ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
- (K [Auto_tac]);
+Goalw [subcls1_def]  
+"subcls1 G = (\\<Sigma>C\\<in>{C. is_class G C} . {D. C\\<noteq>Object \\<and> fst (the (class G C))=D})";
+by Auto_tac;
+qed "subcls1_def2";
 
 Goal "finite (subcls1 G)";
 by(stac subcls1_def2 1);
-by( rtac finite_SigmaI 1);
-by(  rtac finite_is_class 1);
-by( rtac finite_subset 1);
-by(  rtac some_subset_the 1);
-by( Simp_tac 1);
+by( rtac (finite_is_class RS finite_SigmaI) 1);
+by(res_inst_tac [("B","{fst (the (class G C))}")] finite_subset 1);
+by  Auto_tac;
 qed "finite_subcls1";
 
-fun prove_typerel_lemma drules indrule s = prove_goal thy s (fn prems => [
-	rtac (hd prems RS indrule) 1,
-	auto_tac (claset() addDs drules, simpset())]);
 
-fun prove_typerel s lemmata = prove_goal thy s (fn prems => [
-	cut_facts_tac prems 1,
-	auto_tac (claset() addDs lemmata, simpset())]);
-
-
-Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
+Goal "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
 by(etac trancl_trans_induct 1);
 by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
 qed "subcls_is_class";
 
+Goal "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> is_class G D \\<longrightarrow> is_class G C";
+by (etac rtrancl_induct 1);
+by  (dtac subcls1D 2);
+by  Auto_tac;
+qed_spec_mp "subcls_is_class2"; 
+
 (* A particular thm about wf;
    looks like it is an odd instance of something more general
 *)
 Goalw [wf_def] "wf{((A,x),(B,y)) . A=B \\<and> wf(R(A)) \\<and> (x,y)\\<in>R(A)}";
-by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [split_paired_All]) 1);
+by(full_simp_tac (simpset() delcongs [imp_cong]) 1);
 by(strip_tac 1);
 by(rename_tac "A x" 1);
 by(case_tac "wf(R A)" 1);
@@ -68,30 +67,48 @@
  (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (fields.tcs)))))
  (K [auto_tac (claset() addIs [subcls1I], simpset())]);
 
+Goalw [field_def] 
+"field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT";
+by (rtac table_of_remap_SomeD 1);
+by (Asm_full_simp_tac 1);
+qed "field_fields";
 
-AddSIs   [widen.refl];
+AddSIs   [widen.refl,widen.null];
 Addsimps [widen.refl];
 
-val prove_widen_lemma = prove_typerel_lemma [] widen.elim;
-
 Goal "(G\\<turnstile>PrimT pT\\<preceq>RefT rT) = False";
 br iffI 1;
 be widen.elim 1;
-by(Auto_tac);
+by Auto_tac;
 qed "widen_PrimT_RefT";
 AddIffs [widen_PrimT_RefT];
 
-val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t" 
-	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)"];
-bind_thm ("widen_RefT", widen_RefT);
+Goal "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)";
+by (etac widen.elim 1);
+by Auto_tac;
+qed "widen_RefT_lemma";
+Goal "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t"; 
+by (dtac widen_RefT_lemma 1);
+by Auto_tac;
+qed "widen_RefT";
 
-val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t" 
-	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)"];
-bind_thm ("widen_RefT2", widen_RefT2);
+Goal "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)";
+by (etac widen.elim 1);
+by Auto_tac;
+qed "widen_RefT2_lemma";
+Goal "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t";
+by (dtac widen_RefT2_lemma 1);
+by Auto_tac;
+qed "widen_RefT2";
 
-val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D"
- [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)"];
-bind_thm ("widen_Class", widen_Class);
+Goal "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)";
+by (etac widen.elim 1);
+by Auto_tac;
+qed "widen_Class_lemma";
+Goal "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D";
+by (dtac widen_Class_lemma 1);
+by Auto_tac;
+qed "widen_Class";
 
 Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False"; 
 br iffI 1;
@@ -113,6 +130,5 @@
 by   Safe_tac;
 by(  ALLGOALS (forward_tac [widen_Class, widen_RefT]));
 by  Safe_tac;
-by(  rtac widen.null 2);
 by(eatac rtrancl_trans 1 1);
 qed_spec_mp "widen_trans";
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Dec 06 19:10:36 2000 +0100
@@ -34,7 +34,7 @@
 defs
 
   (* direct subclass, cf. 8.1.3 *)
-  subcls1_def	"subcls1 G == {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
+ subcls1_def"subcls1 G \\<equiv> {(C,D). C\\<noteq>Object \\<and> (\\<exists>c. class G C=Some c \\<and> fst c=D)}"
   
 consts
 
@@ -42,15 +42,15 @@
   field	:: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
   fields	:: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times>  ty) list"
 
-constdefs       (* auxiliary relations for recursive definitions below *)
+constdefs       (* auxiliary relation for recursive definitions below *)
 
   subcls1_rel	:: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
  "subcls1_rel == {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
 
 (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
 recdef method "subcls1_rel"
- "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
-                   | Some (sc,fs,ms) => (case sc of None => empty | Some D => 
+ "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
+                   | Some (D,fs,ms) => (if C = Object then empty else 
                                            if is_class G D then method (G,D) 
                                                            else arbitrary) ++
                                            map_of (map (\\<lambda>(s,  m ). 
@@ -59,9 +59,9 @@
 
 (* list of fields of a class, including inherited and hidden ones *)
 recdef fields  "subcls1_rel"
- "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
-                   | Some (sc,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
-                                           (case sc of None => [] | Some D => 
+ "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
+                   | Some (D,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
+                                           (if C = Object then [] else 
                                            if is_class G D then fields (G,D) 
                                                            else arbitrary))
                   else arbitrary)"
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/WellForm.ML
--- a/src/HOL/MicroJava/J/WellForm.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellForm.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -4,58 +4,59 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
- "!!X. [|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)" (K [
-	Asm_full_simp_tac 1,
-	fast_tac (set_cs addDs [get_in_set]) 1]);
+Goalw [wf_prog_def]
+ "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)";
+by (Asm_full_simp_tac 1);
+by (fast_tac (set_cs addDs [map_of_SomeD]) 1);
+qed "class_wf";
 
-val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
-	"!!X. wf_prog wf_mb G ==> class G Object = Some (None, [], [])" (K [
-	safe_tac set_cs,
-	dtac in_set_get 1,
-	 Auto_tac]);
+Goalw [wf_prog_def, ObjectC_def]
+	"wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])";
+by (auto_tac (claset() addIs [map_of_SomeI], simpset()));
+qed "class_Object";
 Addsimps [class_Object];
 
-val is_class_Object = prove_goalw thy [is_class_def] 
-	"!!X. wf_prog wf_mb G ==> is_class G Object" (K [Asm_simp_tac 1]);
+Goal "wf_prog wf_mb G ==> is_class G Object";
+by (Asm_simp_tac 1);
+qed "is_class_Object";
 Addsimps [is_class_Object];
 
 Goal "[|G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G|] ==> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
 by( forward_tac [r_into_trancl] 1);
 by( dtac subcls1D 1);
-by( strip_tac1 1);
+by(Clarify_tac 1);
 by( datac class_wf 1 1);
 by( rewtac wf_cdecl_def);
 by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
 				  delsimps [reflcl_trancl]) 1);
 qed "subcls1_wfD";
 
-val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] 
-"!!X. [|wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object|] ==> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
-	pair_tac "r" 1,
-	asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]);
+Goalw [wf_cdecl_def] 
+"!!r. \\<lbrakk>wf_cdecl wf_mb G (C,D,r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> is_class G D";
+by (auto_tac (claset(), simpset() addsplits [option.split_asm]));
+qed "wf_cdecl_supD";
 
 Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> \\<not>(D,C)\\<in>(subcls1 G)^+";
 by(etac tranclE 1);
-by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
+by(TRYALL(fast_tac (claset() addSDs [subcls1_wfD] addIs [trancl_trans])));
 qed "subcls_asym";
 
-val subcls_irrefl = prove_goal thy "!!X. [|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D" (K [
-	etac trancl_trans_induct 1,
-	 fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
-	fast_tac (HOL_cs addDs [subcls_asym]) 1]);
+Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D";
+by (etac trancl_trans_induct 1);
+by  (auto_tac (claset() addDs [subcls1_wfD,subcls_asym],simpset()));
+qed "subcls_irrefl";
 
-val acyclic_subcls1 = prove_goalw thy [acyclic_def] 
-	"!!X. wf_prog wf_mb G ==> acyclic (subcls1 G)" (K [
-	strip_tac1 1,
-	fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
+Goalw [acyclic_def] "wf_prog wf_mb G ==> acyclic (subcls1 G)";
+by (fast_tac (claset() addDs [subcls_irrefl]) 1);
+qed "acyclic_subcls1";
 
-val wf_subcls1 = prove_goal thy "!!X. wf_prog wf_mb G ==> wf ((subcls1 G)^-1)" (K [
-	rtac finite_acyclic_wf 1,
-	 stac finite_converse 1,
-	 rtac finite_subcls1 1,
-	stac acyclic_converse 1,
-	etac acyclic_subcls1 1]);
+Goal "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)";
+by (rtac finite_acyclic_wf 1);
+by ( stac finite_converse 1);
+by ( rtac finite_subcls1 1);
+by (stac acyclic_converse 1);
+by (etac acyclic_subcls1 1);
+qed "wf_subcls1";
 
 val major::prems = goal thy
   "[|wf_prog wf_mb G; !!C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C";
@@ -68,8 +69,8 @@
 qed "subcls_induct";
 
 val prems = goal thy "[|is_class G C; wf_prog wf_mb G; P Object; \
-\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
-\   wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D|] ==> P C\
+\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \\<and> \
+\   wf_cdecl wf_mb G (C,D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D|] ==> P C\
 \ |] ==> P C";
 by( cut_facts_tac prems 1);
 by( rtac impE 1);
@@ -81,32 +82,30 @@
 by( rtac impI 1);
 by( case_tac "C = Object" 1);
 by(  Fast_tac 1);
-by( ex_ftac is_classD 1);
+by Safe_tac;
 by( forward_tac [class_wf] 1);
 by(  atac 1);
 by( forward_tac [wf_cdecl_supD] 1);
 by(  atac 1);
-by( strip_tac1 1);
+
+by( subgoal_tac "G\\<turnstile>C\\<prec>C1a" 1);
+by( etac subcls1I 2);
 by( rtac (hd (tl (tl (tl prems)))) 1);
-by(   atac 1);
-by(  atac 1);
-by( subgoal_tac "G\\<turnstile>C\\<prec>C1D" 1);
-by(  fast_tac (HOL_cs addIs [r_into_trancl]) 1);
-by( etac subcls1I 1);
+by Auto_tac;
 qed "subcls1_induct";
 
-Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) --> is_class G D|] ==> method (G,C) = \
-\ (case class G C of None => empty | Some (sc,fs,ms) => \
-\ (case sc of None => empty | Some D => method (G,D)) ++ \
+Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (D,fs,ms) \\<longrightarrow> C \\<noteq> Object --> is_class G D|] ==> method (G,C) = \
+\ (case class G C of None => arbitrary | Some (D,fs,ms) => \
+\ (if C = Object then empty else method (G,D)) ++ \
 \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
 by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
 by( asm_simp_tac (simpset() addsplits[option.split]) 1);
-auto();
+by Auto_tac;
 qed "method_rec_lemma";
 
 Goal "wf_prog wf_mb G ==> method (G,C) = \
-\ (case class G C of None => empty | Some (sc,fs,ms) => \
-\ (case sc of None => empty | Some D => method (G,D)) ++ \
+\ (case class G C of None => arbitrary | Some (D,fs,ms) => \
+\ (if C = Object then empty else method (G,D)) ++ \
 \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
 by(rtac method_rec_lemma 1);
 by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def] 
@@ -119,36 +118,40 @@
 by( Asm_full_simp_tac 1);
 qed "method_rec";
 
-Goal "[|wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C --> is_class G C|] ==> fields (G,C) = \
-\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
-\ (case sc of None => [] | Some D => fields (G,D))";
-by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
+Goal "[|wf ((subcls1 G)^-1); class G C = Some (D,fs,ms); C \\<noteq> Object \\<longrightarrow> is_class G D|] ==> fields (G,C) = \
+\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))";
+by(rtac trans 1);
+by(rtac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
 by( asm_simp_tac (simpset() addsplits[option.split]) 1);
 qed "fields_rec_lemma";
 
-Goal "[|class G C = Some (sc,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
-\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
-\ (case sc of None => [] | Some D => fields (G,D))";
+Goal "[|class G C = Some (D,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
+\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))";
+by(rtac trans 1);
 by(rtac fields_rec_lemma 1);
-by(   asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
+by(   asm_simp_tac (simpset() addsimps [wf_subcls1]) 1);
 ba  1;
-by( option_case_tac2 "sc" 1);
-by(  Asm_simp_tac 1);
-by( case_tac "C = Object" 1);
-by(  rotate_tac 2 1);
-by(  Asm_full_simp_tac 1);
+br refl 2;
 by( datac class_wf 1 1);
-by( datac wf_cdecl_supD 1 1);
-by( Asm_full_simp_tac 1);
+by(rtac impI 1);
+by( eatac wf_cdecl_supD 1 1);
 qed "fields_rec";
 
-val method_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> method (G,Object) = empty"
-	(K [stac method_rec 1,Auto_tac]);
-val fields_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> fields (G,Object) = []"(K [
-	stac fields_rec 1,Auto_tac]);
+Goal "wf_prog wf_mb G ==> method (G,Object) = empty";
+by(stac method_rec 1);
+by Auto_tac;
+qed "method_Object";
+
+Goal "wf_prog wf_mb G ==> fields (G,Object) = []";
+by(stac fields_rec 1);
+by Auto_tac;
+qed "fields_Object";
+
 Addsimps [method_Object, fields_Object];
-val field_Object = prove_goalw thy [field_def]
- "!!X. wf_prog wf_mb G ==> field (G,Object) = empty" (K [Asm_simp_tac 1]);
+
+Goalw [field_def] "wf_prog wf_mb G ==> field (G,Object) = empty";
+by(Asm_simp_tac 1);
+qed "field_Object";
 Addsimps [field_Object];
 
 Goal "[|is_class G C; wf_prog wf_mb G|] ==> G\\<turnstile>C\\<preceq>C Object";
@@ -159,17 +162,9 @@
 by(eatac rtrancl_into_rtrancl2 1 1);
 qed "subcls_C_Object";
 
-val is_type_rTI = prove_goalw thy [wf_mhead_def]
-	"!!sig. wf_mhead G sig rT ==> is_type G rT"
-	(K [split_all_tac 1, Auto_tac]);
-
-Goal "[|(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G|] ==> \
-\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
-by(etac trancl_trans_induct 1);
-by( safe_tac (HOL_cs addSDs [subcls1D]));
-by(stac fields_rec 1);
-by(  Auto_tac);
-qed_spec_mp "fields_mono";
+Goalw [wf_mhead_def] "wf_mhead G sig rT ==> is_type G rT";
+by Auto_tac;
+qed "is_type_rTI";
 
 Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
 \ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>C\\<preceq>C fd";
@@ -180,28 +175,22 @@
 by( stac fields_rec 1);
 by(   atac 1);
 by(  atac 1);
-by( Simp_tac 1);
+by( simp_tac (simpset() delsplits [split_if]) 1);
 by( rtac ballI 1);
 by( split_all_tac 1);
 by( Simp_tac 1);
 by( etac UnE 1);
-by(  dtac split_Pair_eq 1);
-by(  SELECT_GOAL (Auto_tac) 1);
+by(  Force_tac 1);
 by( etac (r_into_rtrancl RS rtrancl_trans) 1);
-by( etac BallE 1);
-by(  contr_tac 1);
-by( Asm_full_simp_tac 1);
+by Auto_tac;
 qed "widen_fields_defpl'";
 
-Goal "[|is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))|] ==> \
+Goal "[|((fn,fd),fT) \\<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==> \
 \ G\\<turnstile>C\\<preceq>C fd";
 by( datac widen_fields_defpl' 1 1);
-(*###################*)
-by( dtac bspec 1);
-auto();
+by (Fast_tac 1);
 qed "widen_fields_defpl";
 
-
 Goal "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))";
 by( etac subcls1_induct 1);
 by(   atac 1);
@@ -212,54 +201,53 @@
 by( stac fields_rec 1);
 by   Auto_tac;
 by( rotate_tac ~1 1);
-by( ex_ftac is_classD 1);
 by( forward_tac [class_wf] 1);
 by  Auto_tac;
 by( asm_full_simp_tac (simpset() addsimps [wf_cdecl_def]) 1);
 by( etac unique_append 1);
-by(  rtac unique_map_Pair 1);
-by(  Step_tac 1);
-by (EVERY1[dtac widen_fields_defpl, atac, atac]);
-by( Asm_full_simp_tac 1);
-by( dtac split_Pair_eq 1);
-by( Asm_full_simp_tac 1);
+by(  rtac unique_map_inj 1);
+by(   Clarsimp_tac 1);
+by  (rtac injI 1);
+by(  Asm_full_simp_tac 1);
+by(auto_tac (claset() addSDs [widen_fields_defpl], simpset()));
 qed "unique_fields";
 
+Goal "[|wf_prog wf_mb G; (C',C)\\<in>(subcls1 G)^*|] ==> \
+\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
+by(etac converse_rtrancl_induct 1);
+by( safe_tac (HOL_cs addSDs [subcls1D]));
+by(stac fields_rec 1);
+by(  Auto_tac);
+qed_spec_mp "fields_mono_lemma";
+
 Goal
-"[|wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft|] ==> \
-\                          map_of (fields (G,C')) f = Some ft";
-by( dtac rtranclD 1);
-by( Auto_tac);
-by( rtac table_mono 1);
-by(   atac 3);
-by(  rtac unique_fields 1);
-by(   etac subcls_is_class 1);
-by(  atac 1);
-by( fast_tac (HOL_cs addEs [fields_mono]) 1);
-qed "widen_fields_mono";
-
+"\\<lbrakk>map_of (fields (G,C)) fn = Some f; G\\<turnstile>D\\<preceq>C C; is_class G D; wf_prog wf_mb G\\<rbrakk>\
+\ \\<Longrightarrow> map_of (fields (G,D)) fn = Some f";
+by (rtac map_of_SomeI 1);
+by  (eatac unique_fields 1 1);
+by (eatac fields_mono_lemma 1 1);
+by (etac map_of_SomeD 1);
+qed "fields_mono";
 
-val cfs_fields_lemma = prove_goalw thy [field_def] 
-"!!X. field (G,C) fn = Some (fd, fT) ==> map_of(fields (G,C)) (fn, fd) = Some fT"
-(K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
+Goal 
+"[|field (G,C) fn = Some (fd, fT); G\\<turnstile>D\\<preceq>C C; wf_prog wf_mb G|]==> \
+\ map_of (fields (G,D)) (fn, fd) = Some fT";
+by (dtac field_fields 1);
+by (dtac rtranclD 1);
+by Safe_tac;
+by (ftac subcls_is_class 1);
+by (dtac trancl_into_rtrancl 1);
+by (fast_tac (HOL_cs addDs [fields_mono]) 1);
+qed "widen_cfs_fields";
 
-val widen_cfs_fields = prove_goal thy "!!X. [|field (G,C) fn = Some (fd, fT);\
-\  G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G|] ==> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
-fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
-bind_thm ("widen_cfs_fields",widen_cfs_fields);
-
-
-Goal "wf_prog wf_mb G ==> method (G,C) sig = Some (md,mh,m)\
+Goal "wf_prog wf_mb G ==> is_class G C \\<Longrightarrow>  \
+\    method (G,C) sig = Some (md,mh,m)\
 \  --> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
-by( case_tac "is_class G C" 1);
-by(  forw_inst_tac [("C","C")] method_rec 2);
-by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
-	delsimps [not_None_eq]) 2);
 by( etac subcls1_induct 1);
 by(   atac 1);
 by(  Force_tac 1);
 by( forw_inst_tac [("C","C")] method_rec 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
 by( rotate_tac ~1 1);
 by( Asm_full_simp_tac 1);
 by( dtac override_SomeD 1);
@@ -270,11 +258,10 @@
 by(   atac 3);
 by(  rtac r_into_rtrancl 2);
 by(  fast_tac (HOL_cs addIs [subcls1I]) 2);
-by( forward_tac [table_mapf_SomeD] 1);
-by( strip_tac1 1);
-by( Asm_full_simp_tac 1);
+by (rotate_tac ~1 1);
+by (ftac map_of_SomeD 1);
 by( rewtac wf_cdecl_def);
-by( Asm_full_simp_tac 1);
+by (Clarsimp_tac 1);
 qed_spec_mp "method_wf_mdecl";
 
 Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
@@ -285,12 +272,12 @@
 by(  Fast_tac 1);
 by( etac conjE 1);
 by( etac trancl_trans_induct 1);
-by(  strip_tac1 2);
-by(  EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
+by(  Clarify_tac 2);
+by(  EVERY[smp_tac 3 2]);
 by(  fast_tac (HOL_cs addEs [widen_trans]) 2);
-by( strip_tac1 1);
+by( Clarify_tac 1);
 by( dtac subcls1D 1);
-by( strip_tac1 1);
+by( Clarify_tac 1);
 by( stac method_rec 1);
 by(  atac 1);
 by( rewtac override_def);
@@ -304,13 +291,10 @@
 by(  atac 1);
 by( split_all_tac 1);
 by( rewtac wf_cdecl_def);
-by( dtac table_mapf_Some2 1);
-by( Clarsimp_tac 1);
-by( dres_inst_tac [("xys1","ms")] get_in_set 1);
+by( dtac map_of_SomeD 1);
 by Auto_tac;
 qed_spec_mp "subcls_widen_methd";
 
-
 Goal
  "[| G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
 \    method (G,D) sig = Some (md, rT, b) |] \
@@ -319,12 +303,7 @@
              simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
 qed "subtype_widen_methd";
 
-
-Goal "wf_prog wf_mb G ==> \\<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
-by( case_tac "is_class G C" 1);
-by(  forw_inst_tac [("C","C")] method_rec 2);
-by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
-	delsimps [not_None_eq]) 2);
+Goal "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)";
 by (etac subcls1_induct 1);
   ba 1;
  by (Asm_full_simp_tac 1);
@@ -340,26 +319,30 @@
  by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
 qed_spec_mp "method_in_md";
 
-
 Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
 \ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
 by( etac subcls1_induct 1);
 by(   atac 1);
 by(  Asm_simp_tac 1);
-by( strip_tac1 1);
 by( stac fields_rec 1);
-by(   atac 1);
+by(   Fast_tac 1);
 by(  atac 1);
-by( Asm_simp_tac 1);
-by( safe_tac set_cs);
-by(  Fast_tac 2);
+by( Clarsimp_tac 1);
+by( Safe_tac);
+by(  Force_tac 2);
 by( dtac class_wf 1);
 by(  atac 1);
 by( rewtac wf_cdecl_def);
-by( Asm_full_simp_tac 1);
-by( strip_tac1 1);
+by( Clarsimp_tac 1);
 by( EVERY[dtac bspec 1, atac 1]);
 by( rewtac wf_fdecl_def);
-by( split_all_tac 1);
-by( Asm_full_simp_tac 1);
-bind_thm ("is_type_fields", result() RS bspec);
+by Auto_tac;
+qed_spec_mp "fields_is_type_lemma";
+
+Goal "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==> \
+\ is_type G f";
+by(dtac map_of_SomeD 1);
+by(datac fields_is_type_lemma 2 1);
+by(Auto_tac);
+qed "fields_is_type";
+
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Dec 06 19:10:36 2000 +0100
@@ -30,14 +30,12 @@
 
  wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
 "wf_cdecl wf_mb G ==
-   \\<lambda>(C,(sc,fs,ms)).
-  (\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
+   \\<lambda>(C,(D,fs,ms)).
+  (\\<forall>f\\<in>set fs. wf_fdecl G         f) \\<and>  unique fs \\<and>
   (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
-  (case sc of None => C = Object
-         | Some D =>
-             is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
-             (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
-                 method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
+  (C \\<noteq> Object \\<longrightarrow> is_class G D \\<and>  \\<not>G\\<turnstile>D\\<preceq>C C \\<and>
+                   (\\<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_prog :: "'c wf_mb => 'c prog => bool"
 "wf_prog wf_mb G ==
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/WellType.ML
--- a/src/HOL/MicroJava/J/WellType.ML	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML	Wed Dec 06 19:10:36 2000 +0100
@@ -13,18 +13,18 @@
 
 
 Goal
-"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G|] ==> \
-\ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
-\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)";
+"[|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> \
+\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>T''\\<preceq>C T' \\<and> wf_mhead G sig rT' \\<and> wf_mb G T' (sig,rT',b)"; 
 by( datac widen_methd 2 1);
-by( Clarsimp_tac 1);
+by( Clarify_tac 1);
+by( ftac subcls_is_class2 1);
+by (Asm_simp_tac 1);
 by( dtac method_wf_mdecl 1);
-by(  atac 1);
 by( rewtac wf_mdecl_def);
 by Auto_tac;
 qed "Call_lemma";
 
-
 Goal "wf_prog wf_mb G ==> method (G,Object) sig = None";
 by (Asm_simp_tac 1);
 qed "method_Object";
@@ -42,9 +42,32 @@
 by (Fast_tac 1);
 qed "appl_methsD";
 
-val is_type_typeof = prove_goal thy 
-	"(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and>  is_type G T)" (K [
-	rtac val_.induct 1,
-	    Fast_tac 5,
-	   ALLGOALS Simp_tac]) RS mp;
+bind_thm ("max_spec2mheads", insertI1 RSN (2,(equalityD2 RS subsetD)) RS 
+                      max_spec2appl_meths RS appl_methsD);
+
+Goal "(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)";
+by (rtac val_.induct 1);
+by (Fast_tac 5);
+by Auto_tac;
+qed_spec_mp "is_type_typeof";
 Addsimps [is_type_typeof];
+
+Goal "typeof (\\<lambda>a. None) v = Some T \\<longrightarrow> is_type G T";
+by (rtac val_.induct 1);
+by     Auto_tac;
+qed_spec_mp "typeof_empty_is_type";
+
+Goal "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)";
+by (rtac ty_expr_ty_exprs_wt_stmt.induct 1);
+by Auto_tac;
+by (   etac typeof_empty_is_type 1);
+by (  asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
+by ( dtac field_fields 1);
+by ( datac fields_is_type 1 1);
+by (  Asm_simp_tac 1);
+ba 1;
+by (auto_tac (claset() addSDs [max_spec2mheads,method_wf_mdecl,is_type_rTI], simpset()addsimps[wf_mdecl_def]));
+qed "wt_is_type";
+
+bind_thm ("ty_expr_is_type", permute_prems 0 1 (wt_is_type RS conjunct1 RS mp));
diff -r 779af7c58743 -r 78b1d6c3ee9c src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Wed Dec 06 19:09:34 2000 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Wed Dec 06 19:10:36 2000 +0100
@@ -95,7 +95,7 @@
          E\\<turnstile>NewC C::Class C"
 
   (* cf. 15.15 *)
-  Cast  "[| E\\<turnstile>e::Class C;
+  Cast  "[| E\\<turnstile>e::Class C; is_class (prg E) D;
             prg E\\<turnstile>C\\<preceq>? D |] ==>
          E\\<turnstile>Cast D e::Class D"