# HG changeset patch
# User oheimb
# Date 981057193 -3600
# Node ID a50365d21144ff4f9baef25ca5be5c2edda9bde7
# Parent  a70b796d9af80d3cff43b1afb88f2a4a8ec1f874
converted to Isar, simplifying recursion on class hierarchy

diff -r a70b796d9af8 -r a50365d21144 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/IsaMakefile	Thu Feb 01 20:53:13 2001 +0100
@@ -87,7 +87,7 @@
   Lfp.thy List.ML List.thy Main.ML Main.thy Map.ML Map.thy Nat.ML \
   Nat.thy NatArith.ML NatArith.thy NatDef.ML NatDef.thy Numeral.thy \
   Option.ML Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy \
-  Product_Type.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
+  Product_Type_lemmas.ML Product_Type.thy ROOT.ML Recdef.thy Record.thy \
   Relation.ML Relation.thy Relation_Power.ML Relation_Power.thy \
   SVC_Oracle.ML SVC_Oracle.thy Set.ML Set.thy SetInterval.ML \
   SetInterval.thy String.thy Sum_Type.ML Sum_Type.thy \
@@ -96,7 +96,8 @@
   Tools/datatype_rep_proofs.ML Tools/induct_attrib.ML Tools/induct_method.ML \
   Tools/inductive_package.ML Tools/meson.ML Tools/numeral_syntax.ML \
   Tools/primrec_package.ML Tools/recdef_package.ML \
-  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML \
+  Tools/record_package.ML Tools/split_rule.ML \
+  Tools/svc_funcs.ML Tools/typedef_package.ML \
   Transitive_Closure.thy Transitive_Closure_lemmas.ML Wellfounded_Recursion.ML \
   Wellfounded_Recursion.thy Wellfounded_Relations.ML \
   Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \
@@ -420,15 +421,11 @@
 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
 
 $(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML MicroJava/Digest.thy \
-  MicroJava/J/Conform.ML MicroJava/J/Conform.thy \
-  MicroJava/J/Eval.thy MicroJava/J/Eval.ML MicroJava/J/JBasis.ML \
-  MicroJava/J/JBasis.thy MicroJava/J/JTypeSafe.thy MicroJava/J/JTypeSafe.ML \
-  MicroJava/J/Decl.thy MicroJava/J/Decl.ML MicroJava/J/State.ML \
-  MicroJava/J/State.thy MicroJava/J/Term.thy \
-  MicroJava/J/Type.thy MicroJava/J/TypeRel.ML MicroJava/J/TypeRel.thy \
-  MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML MicroJava/J/Value.thy \
-  MicroJava/J/WellType.ML MicroJava/J/WellType.thy \
-  MicroJava/J/Example.ML MicroJava/J/Example.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 \
+  MicroJava/J/WellForm.thy MicroJava/J/Value.thy \
+  MicroJava/J/WellType.thy MicroJava/J/Example.thy \
   MicroJava/JVM/JVMExec.thy MicroJava/JVM/JVMInstructions.thy\
   MicroJava/JVM/JVMState.thy MicroJava/JVM/JVMExecInstr.thy\
   MicroJava/BV/BVSpec.thy MicroJava/BV/Step.thy\
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -12,30 +12,30 @@
 constdefs
 wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool"
 "wt_instr i G rT phi mxs max_pc pc == 
-    app i G mxs rT (phi!pc) \\<and>
-   (\\<forall> pc' \\<in> set (succs i pc). pc' < max_pc \\<and> (G \\<turnstile> step i G (phi!pc) <=' phi!pc'))"
+    app i G mxs rT (phi!pc) \<and>
+   (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))"
 
 wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
 "wt_start G C pTs mxl phi == 
-    G \\<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
+    G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
 
 
 wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool"
 "wt_method G C pTs rT mxs mxl ins phi ==
 	let max_pc = length ins
         in
-	0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and> 
-	(\\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)"
+	0 < max_pc \<and> wt_start G C pTs mxl phi \<and> 
+	(\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)"
 
 wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
 "wt_jvm_prog G phi ==
-   wf_prog (\\<lambda>G C (sig,rT,(maxs,maxl,b)).
+   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)).
               wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G"
 
 
 
 lemma wt_jvm_progD:
-"wt_jvm_prog G phi ==> (\\<exists>wt. wf_prog wt G)"
+"wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
 by (unfold wt_jvm_prog_def, blast)
 
 lemma wt_jvm_prog_impl_wt_instr:
@@ -48,54 +48,17 @@
 lemma wt_jvm_prog_impl_wt_start:
 "[| wt_jvm_prog G phi; is_class G C;
     method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> 
- 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)"
+ 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
     simp, simp, simp add: wf_mdecl_def wt_method_def)
 
 text {* for most instructions wt\_instr collapses: *}
 lemma  
 "succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = 
- (app i G mxs rT (phi!pc) \\<and> pc+1 < max_pc \\<and> (G \\<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
+ (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
 by (simp add: wt_instr_def) 
 
 
-(* ### move to WellForm *)
-
-lemma methd:
-  "[| wf_prog wf_mb G; (C,S,fs,mdecls) \\<in> set G; (sig,rT,code) \\<in> set mdecls |]
-  ==> method (G,C) sig = Some(C,rT,code) \\<and> is_class G C"
-proof -
-  assume wf: "wf_prog wf_mb G" 
-  assume C:  "(C,S,fs,mdecls) \\<in> set G"
-
-  assume m: "(sig,rT,code) \\<in> set mdecls"
-  moreover
-  from wf
-  have "class G Object = Some (arbitrary, [], [])"
-    by simp 
-  moreover
-  from wf C
-  have c: "class G C = Some (S,fs,mdecls)"
-    by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
-  ultimately
-  have O: "C \\<noteq> Object"
-    by auto
-      
-  from wf C
-  have "unique mdecls"
-    by (unfold wf_prog_def wf_cdecl_def) auto
-
-  hence "unique (map (\\<lambda>(s,m). (s,C,m)) mdecls)"
-    by - (induct mdecls, auto)
-
-  with m
-  have "map_of (map (\\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
-    by (force intro: map_of_SomeI)
-
-  with wf C m c O
-  show ?thesis
-    by (auto simp add: is_class_def dest: method_rec [of _ _ C])
-qed
 
 
 end
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Conform.ML
--- a/src/HOL/MicroJava/J/Conform.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,236 +0,0 @@
-(*  Title:      HOL/MicroJava/J/Conform.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-section "hext";
-
-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";
-
-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";
-
-Goal "h\\<le>|h";
-by (rtac hextI 1);
-by (Fast_tac 1);
-qed "hext_refl";
-
-Goal "h a = None ==> h\\<le>|h(a\\<mapsto>x)";
-by (rtac hextI 1);
-by Auto_tac;
-qed "hext_new";
-
-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];
-
-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";
-
-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];
-
-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] "[|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";
-
-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);
-by  (etac ssubst 1);
-by  (res_inst_tac [("y","prim_ty")] prim_ty.exhaust 1);
-by    (auto_tac (claset(), simpset() addsimps [widen.null]));
-qed_spec_mp "defval_conf";
-
-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";
-
-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";
-
-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 |  \
-\ (\\<exists>a obj T'. a' = Addr a \\<and>  h a = Some obj \\<and>  obj_ty obj = T' \\<and>  G\\<turnstile>T'\\<preceq>RefT T)";
-by(induct_tac "a'" 1);
-by(Auto_tac);
-qed_spec_mp "conf_RefTD";
-
-Goal "G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null";
-by (dtac conf_RefTD 1);
-by Auto_tac;
-qed "conf_NullTD";
-
-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";
-
-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 -->\
-\ (\\<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(res_inst_tac [("y","t")] ref_ty.exhaust 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'";
-by(induct_tac "vs" 1);
- by(ALLGOALS Clarsimp_tac);
-by(forward_tac [list_all2_lengthD RS sym] 1);
-by(full_simp_tac (simpset()addsimps[length_Suc_conv]) 1);
-by(Safe_tac);
-by(forward_tac [list_all2_lengthD RS sym] 1);
-by(full_simp_tac (simpset()addsimps[length_Suc_conv]) 1);
-by(Clarify_tac 1);
-by(fast_tac (claset() addEs [conf_widen]) 1);
-qed_spec_mp "conf_list_gext_widen";
-
-
-section "lconf";
-
-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";
-
-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 Auto_tac;
-qed "lconf_upd";
-
-Goal "\\<forall>x. P x --> R (dv x) x ==> (\\<forall>x. map_of fs f = Some x --> P x) --> \
-\ (\\<forall>T. map_of fs f = Some T --> \
-\ (\\<exists>v. map_of (map (\\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \\<and>  R v T))";
-by( induct_tac "fs" 1);
-by Auto_tac;
-qed_spec_mp "lconf_init_vars_lemma";
-
-Goalw [lconf_def, init_vars_def] 
-"\\<forall>n. \\<forall>T. map_of fs n = Some T --> is_type G T ==> G,h\\<turnstile>init_vars fs[::\\<preceq>]map_of fs";
-by Auto_tac;
-by( rtac lconf_init_vars_lemma 1);
-by(   atac 3);
-by(  strip_tac 1);
-by(  etac defval_conf 1);
-by Auto_tac;
-qed "lconf_init_vars";
-AddSIs [lconf_init_vars];
-
-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);
-by(  ALLGOALS Clarsimp_tac);
-by( forward_tac [list_all2_lengthD] 1);
-by( auto_tac (claset(), simpset() addsimps [length_Suc_conv]));
-qed_spec_mp "lconf_ext_list";
-
-
-section "oconf";
-
-Goalw [oconf_def] "G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>"; 
-by (Fast_tac 1);
-qed "oconf_hext";
-
-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";
-
-Goalw [hconf_def] "[|G\\<turnstile>h h\\<surd>; h a = Some obj|] ==> G,h\\<turnstile>obj\\<surd>";
-by (Fast_tac 1);
-qed "hconfD";
-
-Goalw [hconf_def] "\\<forall>a obj. h a=Some obj --> G,h\\<turnstile>obj\\<surd> ==> G\\<turnstile>h h\\<surd>";
-by (Fast_tac 1);
-qed "hconfI";
-
-
-section "conforms";
-
-Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>";
-by (Asm_full_simp_tac 1);
-qed "conforms_heapD";
-
-Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT";
-by (Asm_full_simp_tac 1);
-qed "conforms_localD";
-
-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] 
-  addSEs [conformsI, lconf_hext]) 1);
-qed "conforms_hext";
-
-Goal "[|(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)";
-by( rtac conforms_hext 1);
-by   Auto_tac;
-by( rtac hconfI 1);
-by( dtac conforms_heapD 1);
-by( (auto_tac (HOL_cs addEs [oconf_hext] addDs [hconfD],
-		simpset()delsimps[split_paired_All])));
-qed "conforms_upd_obj";
-
-Goalw [conforms_def] 
-"[|(h, l)::\\<preceq>(G, lT); G,h\\<turnstile>v::\\<preceq>T; lT va = Some T|] ==> \
-\ (h, l(va\\<mapsto>v))::\\<preceq>(G, lT)";
-by( auto_tac (claset() addEs [lconf_upd], simpset()));
-qed "conforms_upd_local";
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -6,30 +6,30 @@
 Conformity relations for type safety of Java
 *)
 
-Conform = State + WellType +
+theory Conform = State + WellType:
 
-types	'c env_ = "'c prog \\<times> (vname \\<leadsto> ty)" (* same as env of WellType.thy *)
+types	'c env_ = "'c prog \<times> (vname \<leadsto> ty)" (* same as env of WellType.thy *)
 
 constdefs
 
-  hext :: "aheap => aheap => bool" ("_ \\<le>| _" [51,51] 50)
- "h\\<le>|h' == \\<forall>a C fs. h a = Some(C,fs) --> (\\<exists>fs'. h' a = Some(C,fs'))"
+  hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50)
+ "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
 
-  conf :: "'c prog => aheap => val => ty => bool"	("_,_ \\<turnstile> _ ::\\<preceq> _" [51,51,51,51] 50)
- "G,h\\<turnstile>v::\\<preceq>T == \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
+  conf :: "'c prog => aheap => val => ty => bool"	("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50)
+ "G,h\<turnstile>v::\<preceq>T == \<exists>T'. typeof (option_map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
 
-  lconf :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
-                                                ("_,_ \\<turnstile> _ [::\\<preceq>] _" [51,51,51,51] 50)
- "G,h\\<turnstile>vs[::\\<preceq>]Ts == \\<forall>n T. Ts n = Some T --> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v::\\<preceq>T)"
+  lconf :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
+                                                ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50)
+ "G,h\<turnstile>vs[::\<preceq>]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h\<turnstile>v::\<preceq>T)"
 
-  oconf :: "'c prog => aheap => obj => bool" ("_,_ \\<turnstile> _ \\<surd>" [51,51,51] 50)
- "G,h\\<turnstile>obj\\<surd> == G,h\\<turnstile>snd obj[::\\<preceq>]map_of (fields (G,fst obj))"
+  oconf :: "'c prog => aheap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
+ "G,h\<turnstile>obj\<surd> == G,h\<turnstile>snd obj[::\<preceq>]map_of (fields (G,fst obj))"
 
-  hconf :: "'c prog => aheap => bool" ("_ \\<turnstile>h _ \\<surd>" [51,51] 50)
- "G\\<turnstile>h h\\<surd>    == \\<forall>a obj. h a = Some obj --> G,h\\<turnstile>obj\\<surd>"
+  hconf :: "'c prog => aheap => bool" ("_ \<turnstile>h _ \<surd>" [51,51] 50)
+ "G\<turnstile>h h\<surd>    == \<forall>a obj. h a = Some obj --> G,h\<turnstile>obj\<surd>"
 
-  conforms :: "state => java_mb env_ => bool"	("_ ::\\<preceq> _" [51,51] 50)
- "s::\\<preceq>E == prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[::\\<preceq>]localT E"
+  conforms :: "state => java_mb env_ => bool"	("_ ::\<preceq> _" [51,51] 50)
+ "s::\<preceq>E == prg E\<turnstile>h heap s\<surd> \<and> prg E,heap s\<turnstile>locals s[::\<preceq>]localT E"
 
 
 syntax (HTML)
@@ -39,7 +39,7 @@
   conf     :: "'c prog => aheap => val => ty => bool"
               ("_,_ |- _ ::<= _"  [51,51,51,51] 50)
 
-  lconf    :: "'c prog => aheap => ('a \\<leadsto> val) => ('a \\<leadsto> ty) => bool"
+  lconf    :: "'c prog => aheap => ('a \<leadsto> val) => ('a \<leadsto> ty) => bool"
               ("_,_ |- _ [::<=] _" [51,51,51,51] 50)
 
   oconf    :: "'c prog => aheap => obj => bool"
@@ -51,4 +51,257 @@
   conforms :: "state => java_mb env_ => bool"
               ("_ ::<= _" [51,51] 50)
 
+
+section "hext"
+
+lemma hextI: 
+" \<forall>a C fs . h  a = Some (C,fs) -->   
+      (\<exists>fs'. h' a = Some (C,fs')) ==> h\<le>|h'"
+apply (unfold hext_def)
+apply auto
+done
+
+lemma hext_objD: "[|h\<le>|h'; h a = Some (C,fs) |] ==> \<exists>fs'. h' a = Some (C,fs')"
+apply (unfold hext_def)
+apply (force)
+done
+
+lemma hext_refl [simp]: "h\<le>|h"
+apply (rule hextI)
+apply (fast)
+done
+
+lemma hext_new [simp]: "h a = None ==> h\<le>|h(a\<mapsto>x)"
+apply (rule hextI)
+apply auto
+done
+
+lemma hext_trans: "[|h\<le>|h'; h'\<le>|h''|] ==> h\<le>|h''"
+apply (rule hextI)
+apply (fast dest: hext_objD)
+done
+
+lemma hext_upd_obj: "h a = Some (C,fs) ==> h\<le>|h(a\<mapsto>(C,fs'))"
+apply (rule hextI)
+apply auto
+done
+
+
+section "conf"
+
+lemma conf_Null [simp]: "G,h\<turnstile>Null::\<preceq>T = G\<turnstile>RefT NullT\<preceq>T"
+apply (unfold conf_def)
+apply (simp (no_asm))
+done
+
+lemma conf_litval [rule_format (no_asm), simp]: 
+  "typeof (\<lambda>v. None) v = Some T --> G,h\<turnstile>v::\<preceq>T"
+apply (unfold conf_def)
+apply (rule val.induct)
+apply auto
+done
+
+lemma conf_AddrI: "[|h a = Some obj; G\<turnstile>obj_ty obj\<preceq>T|] ==> G,h\<turnstile>Addr a::\<preceq>T"
+apply (unfold conf_def)
+apply (simp)
+done
+
+lemma conf_obj_AddrI: "[|h a = Some (C,fs); G\<turnstile>C\<preceq>C D|] ==> G,h\<turnstile>Addr a::\<preceq> Class D"
+apply (unfold conf_def)
+apply (simp)
+done
+
+lemma defval_conf [rule_format (no_asm)]: "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
+apply (unfold conf_def)
+apply (rule_tac "y" = "T" in ty.exhaust)
+apply  (erule ssubst)
+apply  (rule_tac "y" = "prim_ty" in prim_ty.exhaust)
+apply    (auto simp add: widen.null)
+done
+
+lemma conf_upd_obj: 
+"h a = Some (C,fs) ==> (G,h(a\<mapsto>(C,fs'))\<turnstile>x::\<preceq>T) = (G,h\<turnstile>x::\<preceq>T)"
+apply (unfold conf_def)
+apply (rule val.induct)
+apply auto
+done
+
+lemma conf_widen [rule_format (no_asm)]: "wf_prog wf_mb G ==> G,h\<turnstile>x::\<preceq>T --> G\<turnstile>T\<preceq>T' --> G,h\<turnstile>x::\<preceq>T'"
+apply (unfold conf_def)
+apply (rule val.induct)
+apply (auto intro: widen_trans)
+done
+
+lemma conf_hext [rule_format (no_asm)]: "h\<le>|h' ==> G,h\<turnstile>v::\<preceq>T --> G,h'\<turnstile>v::\<preceq>T"
+apply (unfold conf_def)
+apply (rule val.induct)
+apply (auto dest: hext_objD)
+done
+
+lemma new_locD: "[|h a = None; G,h\<turnstile>Addr t::\<preceq>T|] ==> t\<noteq>a"
+apply (unfold conf_def)
+apply auto
+done
+
+lemma conf_RefTD [rule_format (no_asm)]: 
+ "G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null |   
+  (\<exists>a obj T'. a' = Addr a \<and>  h a = Some obj \<and>  obj_ty obj = T' \<and>  G\<turnstile>T'\<preceq>RefT T)"
+apply (unfold conf_def)
+apply(induct_tac "a'")
+apply(auto)
+done
+
+lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null"
+apply (drule conf_RefTD)
+apply auto
+done
+
+lemma non_npD: "[|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"
+apply (drule conf_RefTD)
+apply auto
+done
+
+lemma non_np_objD: "!!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)"
+apply (fast dest: non_npD)
+done
+
+lemma non_np_objD' [rule_format (no_asm)]: "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t --> 
+  (\<forall>C. t = ClassT C --> C \<noteq> Object) -->  
+  (\<exists>a C fs. a' = Addr a \<and>  h a = Some (C,fs) \<and>  G\<turnstile>Class C\<preceq>RefT t)"
+apply(rule_tac "y" = "t" in ref_ty.exhaust)
+ apply (fast dest: conf_NullTD)
+apply (fast dest: non_np_objD)
+done
+
+lemma conf_list_gext_widen [rule_format (no_asm)]: "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'"
+apply(induct_tac "vs")
+ apply(clarsimp)
+apply(clarsimp)
+apply(frule list_all2_lengthD [THEN sym])
+apply(simp (no_asm_use) add: length_Suc_conv)
+apply(safe)
+apply(frule list_all2_lengthD [THEN sym])
+apply(simp (no_asm_use) add: length_Suc_conv)
+apply(clarify)
+apply(fast elim: conf_widen)
+done
+
+
+section "lconf"
+
+lemma lconfD: "[| G,h\<turnstile>vs[::\<preceq>]Ts; Ts n = Some T |] ==> G,h\<turnstile>(the (vs n))::\<preceq>T"
+apply (unfold lconf_def)
+apply (force)
+done
+
+lemma lconf_hext [elim]: "[| G,h\<turnstile>l[::\<preceq>]L; h\<le>|h' |] ==> G,h'\<turnstile>l[::\<preceq>]L"
+apply (unfold lconf_def)
+apply  (fast elim: conf_hext)
+done
+
+lemma lconf_upd: "!!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"
+apply (unfold lconf_def)
+apply auto
+done
+
+lemma lconf_init_vars_lemma [rule_format (no_asm)]: "\<forall>x. P x --> R (dv x) x ==> (\<forall>x. map_of fs f = Some x --> P x) -->  
+  (\<forall>T. map_of fs f = Some T -->  
+  (\<exists>v. map_of (map (\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \<and>  R v T))"
+apply( induct_tac "fs")
+apply auto
+done
+
+lemma lconf_init_vars [intro!]: 
+"\<forall>n. \<forall>T. map_of fs n = Some T --> is_type G T ==> G,h\<turnstile>init_vars fs[::\<preceq>]map_of fs"
+apply (unfold lconf_def init_vars_def)
+apply auto
+apply( rule lconf_init_vars_lemma)
+apply(   erule_tac [3] asm_rl)
+apply(  intro strip)
+apply(  erule defval_conf)
+apply auto
+done
+
+lemma lconf_ext: "[|G,s\<turnstile>l[::\<preceq>]L; G,s\<turnstile>v::\<preceq>T|] ==> G,s\<turnstile>l(vn\<mapsto>v)[::\<preceq>]L(vn\<mapsto>T)"
+apply (unfold lconf_def)
+apply auto
+done
+
+lemma lconf_ext_list [rule_format (no_asm)]: "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)"
+apply (unfold lconf_def)
+apply( induct_tac "vns")
+apply(  clarsimp)
+apply( clarsimp)
+apply( frule list_all2_lengthD)
+apply( auto simp add: length_Suc_conv)
+done
+
+
+section "oconf"
+
+lemma oconf_hext: "G,h\<turnstile>obj\<surd> ==> h\<le>|h' ==> G,h'\<turnstile>obj\<surd>"
+apply (unfold oconf_def)
+apply (fast)
+done
+
+lemma oconf_obj: "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))"
+apply (unfold oconf_def lconf_def)
+apply auto
+done
+
+lemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp]
+
+
+section "hconf"
+
+lemma hconfD: "[|G\<turnstile>h h\<surd>; h a = Some obj|] ==> G,h\<turnstile>obj\<surd>"
+apply (unfold hconf_def)
+apply (fast)
+done
+
+lemma hconfI: "\<forall>a obj. h a=Some obj --> G,h\<turnstile>obj\<surd> ==> G\<turnstile>h h\<surd>"
+apply (unfold hconf_def)
+apply (fast)
+done
+
+
+section "conforms"
+
+lemma conforms_heapD: "(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"
+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)"
+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_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)"
+apply( rule conforms_hext)
+apply   auto
+apply( rule hconfI)
+apply( drule conforms_heapD)
+apply( tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *})
+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)"
+apply (unfold conforms_def)
+apply( auto elim: lconf_upd)
+done
+
 end
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Decl.ML
--- a/src/HOL/MicroJava/J/Decl.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  Title:      HOL/MicroJava/J/Decl.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-Goalw [is_class_def, class_def] "finite {C. is_class G C}";
-by (fold_goals_tac [dom_def]);
-by (rtac finite_dom_map_of 1);
-qed "finite_is_class";
-
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -6,52 +6,58 @@
 Class declarations and programs
 *)
 
-Decl = Type +
+theory Decl = Type:
 
 types	fdecl		(* field declaration, cf. 8.3 (, 9.3) *)
-	= "vname \\<times> ty"
+	= "vname \<times> ty"
 
 
 types	sig		(* signature of a method, cf. 8.4.2 *)
-	= "mname \\<times> ty list"
+	= "mname \<times> ty list"
 
 	'c mdecl		(* method declaration in a class *)
-	= "sig \\<times> ty \\<times> 'c"
+	= "sig \<times> ty \<times> 'c"
 
 types	'c class		(* class *)
-	= "cname \\<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 *)
-	= "cname \\<times> 'c class"
+	= "cname \<times> 'c class"
 
 consts
 
   Object  :: cname	(* name of root class *)
-  ObjectC :: 'c cdecl	(* decl of root class *)
+  ObjectC :: "'c cdecl"	(* decl of root class *)
 
 defs 
 
- ObjectC_def "ObjectC == (Object, (arbitrary, [], []))"
+ 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)"
+  "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"
 
 constdefs
 
-  class		:: "'c prog => (cname \\<leadsto> 'c class)"
-  "class        \\<equiv> map_of"
+  class		:: "'c prog => (cname \<leadsto> 'c class)"
+  "class        \<equiv> map_of"
   is_class	:: "'c prog => cname => bool"
- "is_class G C  \\<equiv> class G C \\<noteq> None"
+ "is_class G C  \<equiv> class G C \<noteq> None"
+
+lemma finite_is_class: "finite {C. is_class G C}"
+apply (unfold is_class_def class_def)
+apply (fold dom_def)
+apply (rule finite_dom_map_of)
+done
 
 consts
 
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Eval.ML
--- a/src/HOL/MicroJava/J/Eval.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-(*  Title:      HOL/MicroJava/J/Eval.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-val eval_evals_exec_induct = complete_split_rule eval_evals_exec.induct;
-
-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 (Asm_simp_tac 1);
-br eval_evals_exec.NewC 1;
-by Auto_tac;
-qed "NewCI";
-
-Goal "!!s s'. (G\\<turnstile>(x,s) -e \\<succ>  v -> (x',s') --> x'=None --> x=None) \\<and> \
-\             (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x'=None --> x=None) \\<and> \
-\             (G\\<turnstile>(x,s) -c       -> (x',s') --> x'=None --> x=None)";
-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_no_xcpt";
-
-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";
-
-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)";
-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 a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -7,20 +7,21 @@
 execution of Java expressions and statements
 *)
 
-Eval = State + WellType +
+theory Eval = State + WellType:
+
 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"
-  exec  :: "java_mb prog => (xstate \\<times> stmt                 \\<times> xstate) set"
+  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"
+  exec  :: "java_mb prog => (xstate \<times> stmt                 \<times> xstate) set"
 
 syntax
   eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
-          ("_ \\<turnstile> _ -_\\<succ>_-> _" [51,82,60,82,82] 81)
+          ("_ \<turnstile> _ -_\<succ>_-> _" [51,82,60,82,82] 81)
   evals:: "[java_mb prog,xstate,expr list,
                         val list,xstate] => bool "
-          ("_ \\<turnstile> _ -_[\\<succ>]_-> _" [51,82,60,51,82] 81)
+          ("_ \<turnstile> _ -_[\<succ>]_-> _" [51,82,60,51,82] 81)
   exec :: "[java_mb prog,xstate,stmt,    xstate] => bool "
-          ("_ \\<turnstile> _ -_-> _" [51,82,60,82] 81)
+          ("_ \<turnstile> _ -_-> _" [51,82,60,82] 81)
 
 syntax (HTML)
   eval :: "[java_mb prog,xstate,expr,val,xstate] => bool "
@@ -33,112 +34,159 @@
 
 
 translations
-  "G\\<turnstile>s -e \\<succ> v-> (x,s')" <= "(s, e, v, x, s') \\<in> eval  G"
-  "G\\<turnstile>s -e \\<succ> v->    s' " == "(s, e, v,    s') \\<in> eval  G"
-  "G\\<turnstile>s -e[\\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \\<in> evals G"
-  "G\\<turnstile>s -e[\\<succ>]v->    s' " == "(s, e, v,    s') \\<in> evals G"
-  "G\\<turnstile>s -c    -> (x,s')" <= "(s, c, x, s') \\<in> exec G"
-  "G\\<turnstile>s -c    ->    s' " == "(s, c,    s') \\<in> exec G"
+  "G\<turnstile>s -e \<succ> v-> (x,s')" <= "(s, e, v, x, s') \<in> eval  G"
+  "G\<turnstile>s -e \<succ> v->    s' " == "(s, e, v,    s') \<in> eval  G"
+  "G\<turnstile>s -e[\<succ>]v-> (x,s')" <= "(s, e, v, x, s') \<in> evals G"
+  "G\<turnstile>s -e[\<succ>]v->    s' " == "(s, e, v,    s') \<in> evals G"
+  "G\<turnstile>s -c    -> (x,s')" <= "(s, c, x, s') \<in> exec G"
+  "G\<turnstile>s -c    ->    s' " == "(s, c,    s') \<in> exec G"
 
-inductive "eval G" "evals G" "exec G" intrs
+inductive "eval G" "evals G" "exec G" intros
 
 (* evaluation of expressions *)
 
   (* cf. 15.5 *)
-  XcptE "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary-> (Some xc,s)"
+  XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)"
 
   (* cf. 15.8.1 *)
-  NewC  "[| h = heap s; (a,x) = new_Addr h;
-            h'= h(a\\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
-         G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> c_hupd h' (x,s)"
+  NewC: "[| h = heap s; (a,x) = new_Addr h;
+            h'= h(a\<mapsto>(C,init_vars (fields (G,C)))) |] ==>
+         G\<turnstile>Norm s -NewC C\<succ>Addr a-> c_hupd h' (x,s)"
 
   (* cf. 15.15 *)
-  Cast  "[| G\\<turnstile>Norm s0 -e\\<succ>v-> (x1,s1);
-            x2 = raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
-         G\\<turnstile>Norm s0 -Cast C e\\<succ>v-> (x2,s1)"
+  Cast: "[| G\<turnstile>Norm s0 -e\<succ>v-> (x1,s1);
+            x2 = raise_if (\<not> cast_ok G C (heap s1) v) ClassCast x1 |] ==>
+         G\<turnstile>Norm s0 -Cast C e\<succ>v-> (x2,s1)"
 
   (* cf. 15.7.1 *)
-  Lit   "G\\<turnstile>Norm s -Lit v\\<succ>v-> Norm s"
+  Lit:  "G\<turnstile>Norm s -Lit v\<succ>v-> Norm s"
 
-  BinOp "[| G\\<turnstile>Norm s -e1\\<succ>v1-> s1;
-            G\\<turnstile>s1     -e2\\<succ>v2-> s2;
+  BinOp:"[| G\<turnstile>Norm s -e1\<succ>v1-> s1;
+            G\<turnstile>s1     -e2\<succ>v2-> s2;
             v = (case bop of Eq  => Bool (v1 = v2)
                            | Add => Intg (the_Intg v1 + the_Intg v2)) |] ==>
-         G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v-> s2"
+         G\<turnstile>Norm s -BinOp bop e1 e2\<succ>v-> s2"
 
   (* cf. 15.13.1, 15.2 *)
-  LAcc  "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)-> Norm s"
+  LAcc: "G\<turnstile>Norm s -LAcc v\<succ>the (locals s v)-> Norm s"
 
   (* cf. 15.25.1 *)
-  LAss  "[| G\\<turnstile>Norm s -e\\<succ>v-> (x,(h,l));
-            l' = (if x = None then l(va\\<mapsto>v) else l) |] ==>
-         G\\<turnstile>Norm s -va::=e\\<succ>v-> (x,(h,l'))"
+  LAss: "[| G\<turnstile>Norm s -e\<succ>v-> (x,(h,l));
+            l' = (if x = None then l(va\<mapsto>v) else l) |] ==>
+         G\<turnstile>Norm s -va::=e\<succ>v-> (x,(h,l'))"
 
 
   (* cf. 15.10.1, 15.2 *)
-  FAcc  "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> (x1,s1); 
+  FAcc: "[| G\<turnstile>Norm s0 -e\<succ>a'-> (x1,s1); 
             v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==>
-         G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v-> (np a' x1,s1)"
+         G\<turnstile>Norm s0 -{T}e..fn\<succ>v-> (np a' x1,s1)"
 
   (* cf. 15.25.1 *)
-  FAss  "[| G\\<turnstile>     Norm s0  -e1\\<succ>a'-> (x1,s1); a = the_Addr a';
-            G\\<turnstile>(np a' x1,s1) -e2\\<succ>v -> (x2,s2);
+  FAss: "[| G\<turnstile>     Norm s0  -e1\<succ>a'-> (x1,s1); a = the_Addr a';
+            G\<turnstile>(np a' x1,s1) -e2\<succ>v -> (x2,s2);
             h  = heap s2; (c,fs) = the (h a);
-            h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v)))) |] ==>
-         G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v-> c_hupd h' (x2,s2)"
+            h' = h(a\<mapsto>(c,(fs((fn,T)\<mapsto>v)))) |] ==>
+         G\<turnstile>Norm s0 -{T}e1..fn:=e2\<succ>v-> c_hupd h' (x2,s2)"
 
   (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
-  Call  "[| G\\<turnstile>Norm s0 -e\\<succ>a'-> s1; a = the_Addr a';
-            G\\<turnstile>s1 -ps[\\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
+  Call: "[| G\<turnstile>Norm s0 -e\<succ>a'-> s1; a = the_Addr a';
+            G\<turnstile>s1 -ps[\<succ>]pvs-> (x,(h,l)); dynT = fst (the (h a));
             (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs));
-            G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk-> s3;
-            G\\<turnstile> s3 -res\\<succ>v -> (x4,s4) |] ==>
-         G\\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\\<succ>v-> (x4,(heap s4,l))"
+            G\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\<mapsto>]pvs)(This\<mapsto>a'))) -blk-> s3;
+            G\<turnstile> s3 -res\<succ>v -> (x4,s4) |] ==>
+         G\<turnstile>Norm s0 -{C}e..mn({pTs}ps)\<succ>v-> (x4,(heap s4,l))"
 
 
 (* evaluation of expression lists *)
 
   (* cf. 15.5 *)
-  XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary-> (Some xc,s)"
+  XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
 
   (* cf. 15.11.??? *)
-  Nil   "G\\<turnstile>Norm s0 -[][\\<succ>][]-> Norm s0"
+  Nil:  "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
 
   (* cf. 15.6.4 *)
-  Cons  "[| G\\<turnstile>Norm s0 -e  \\<succ> v -> s1;
-            G\\<turnstile>     s1 -es[\\<succ>]vs-> s2 |] ==>
-         G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs-> s2"
+  Cons: "[| G\<turnstile>Norm s0 -e  \<succ> v -> s1;
+            G\<turnstile>     s1 -es[\<succ>]vs-> s2 |] ==>
+         G\<turnstile>Norm s0 -e#es[\<succ>]v#vs-> s2"
 
 (* execution of statements *)
 
   (* cf. 14.1 *)
-  XcptS "G\\<turnstile>(Some xc,s) -c-> (Some xc,s)"
+  XcptS:"G\<turnstile>(Some xc,s) -c-> (Some xc,s)"
 
   (* cf. 14.5 *)
-  Skip  "G\\<turnstile>Norm s -Skip-> Norm s"
+  Skip: "G\<turnstile>Norm s -Skip-> Norm s"
 
   (* cf. 14.7 *)
-  Expr  "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1 |] ==>
-         G\\<turnstile>Norm s0 -Expr e-> s1"
+  Expr: "[| G\<turnstile>Norm s0 -e\<succ>v-> s1 |] ==>
+         G\<turnstile>Norm s0 -Expr e-> s1"
 
   (* cf. 14.2 *)
-  Comp  "[| G\\<turnstile>Norm s0 -c1-> s1;
-            G\\<turnstile>     s1 -c2-> s2|] ==>
-         G\\<turnstile>Norm s0 -c1;; c2-> s2"
+  Comp: "[| G\<turnstile>Norm s0 -c1-> s1;
+            G\<turnstile>     s1 -c2-> s2|] ==>
+         G\<turnstile>Norm s0 -c1;; c2-> s2"
 
   (* cf. 14.8.2 *)
-  Cond  "[| G\\<turnstile>Norm s0  -e\\<succ>v-> s1;
-            G\\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==>
-         G\\<turnstile>Norm s0 -If(e) c1 Else c2-> s2"
+  Cond: "[| G\<turnstile>Norm s0  -e\<succ>v-> s1;
+            G\<turnstile> s1 -(if the_Bool v then c1 else c2)-> s2|] ==>
+         G\<turnstile>Norm s0 -If(e) c1 Else c2-> s2"
 
   (* cf. 14.10, 14.10.1 *)
-  LoopF "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1; \\<not>the_Bool v |] ==>
-         G\\<turnstile>Norm s0 -While(e) c-> s1"
-  LoopT "[| G\\<turnstile>Norm s0 -e\\<succ>v-> s1;  the_Bool v;
-	    G\\<turnstile>s1 -c-> s2; G\\<turnstile>s2 -While(e) c-> s3 |] ==>
-         G\\<turnstile>Norm s0 -While(e) c-> s3"
+  LoopF:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; \<not>the_Bool v |] ==>
+         G\<turnstile>Norm s0 -While(e) c-> s1"
+  LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1;  the_Bool v;
+	    G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==>
+         G\<turnstile>Norm s0 -While(e) c-> s3"
+
+lemmas eval_evals_exec_induct = eval_evals_exec.induct [complete_split]
+
+lemma NewCI: "[|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'"
+apply (simp (no_asm_simp))
+apply (rule eval_evals_exec.NewC)
+apply auto
+done
+
+lemma eval_evals_exec_no_xcpt: 
+ "!!s s'. (G\<turnstile>(x,s) -e \<succ>  v -> (x',s') --> x'=None --> x=None) \<and>  
+          (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x'=None --> x=None) \<and>  
+          (G\<turnstile>(x,s) -c       -> (x',s') --> x'=None --> x=None)"
+apply(simp (no_asm_simp) only: split_tupled_all)
+apply(rule eval_evals_exec_induct)
+apply(unfold c_hupd_def)
+apply(simp_all)
+done
 
-monos
-  if_def2
+lemma eval_no_xcpt: "G\<turnstile>(x,s) -e\<succ>v-> (None,s') ==> x=None"
+apply (drule eval_evals_exec_no_xcpt [THEN conjunct1, THEN mp])
+apply (fast)
+done
+
+lemma evals_no_xcpt: "G\<turnstile>(x,s) -e[\<succ>]v-> (None,s') ==> x=None"
+apply (drule eval_evals_exec_no_xcpt [THEN conjunct2, THEN conjunct1, THEN mp])
+apply (fast)
+done
 
-end
+lemma eval_evals_exec_xcpt: 
+"!!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)"
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply (rule eval_evals_exec_induct)
+apply (unfold c_hupd_def)
+apply (simp_all)
+done
+
+lemma eval_xcpt: "G\<turnstile>(Some xc,s) -e\<succ>v-> (x',s') ==> x'=Some xc \<and>  s'=s"
+apply (drule eval_evals_exec_xcpt [THEN conjunct1, THEN mp])
+apply (fast)
+done
+
+lemma exec_xcpt: "G\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \<and>  s'=s"
+apply (drule eval_evals_exec_xcpt [THEN conjunct2, THEN conjunct2, THEN mp])
+apply (fast)
+done
+
+end
\ No newline at end of file
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Example.ML
--- a/src/HOL/MicroJava/J/Example.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-
-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];
-
-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];
-
-Goalw [ObjectC_def,class_def] "class tprg Object = Some (arbitrary, [], [])";
-by (Simp_tac 1);
-qed "class_tprg_Object";
-
-Goalw [ObjectC_def, BaseC_def, ExtC_def, class_def] 
-"class tprg Base = Some (Object, \
-	\ [(vee, PrimT Boolean)], \
-        \ [((foo, [Class Base]), Class Base, foo_Base)])";
-by (Simp_tac 1);
-qed "class_tprg_Base";
-
-Goalw [ObjectC_def, BaseC_def, ExtC_def, class_def] 
-"class tprg Ext = Some (Base, \
-	\ [(vee, PrimT Integer)], \
-        \ [((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 "(Object,C) \\<in> (subcls1 tprg)^+ ==> R";
-by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
-qed "not_Object_subcls";
-AddSEs [not_Object_subcls];
-
-Goal "tprg\\<turnstile>Object\\<preceq>C C ==> C = Object";
-be rtrancl_induct 1;
-by  Auto_tac;
-bd subcls1D 1;
-by Auto_tac;
-qed "subcls_ObjectD";
-AddSDs[subcls_ObjectD];
-
-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 [ObjectC_def, BaseC_def, ExtC_def, class_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";
-by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
-by (ftac class_tprgD 1);
-by (auto_tac (claset() addSDs [],simpset()));
-bd (thm"rtranclD") 1;
-by Auto_tac;
-qed "not_class_subcls_class";
-AddSEs [not_class_subcls_class];
-
-goalw thy [ObjectC_def, BaseC_def, ExtC_def] "unique tprg";
-by (Simp_tac 1);
-qed "unique_classes";
-
-bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl);
-
-Goal "tprg\\<turnstile>Ext\\<preceq>C Base";
-br subcls_direct 1;
-by Auto_tac;
-qed "Ext_subcls_Base";
-Addsimps [Ext_subcls_Base];
-
-Goal "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
-br widen.subcls 1;
-by (Simp_tac 1);
-qed "Ext_widen_Base";
-Addsimps [Ext_widen_Base];
-
-AddSIs ty_expr_ty_exprs_wt_stmt.intrs;
-
-
-Goal "acyclic (subcls1 tprg)";
-br acyclicI 1;
-by Safe_tac ;
-qed "acyclic_subcls1_";
-
-val wf_subcls1_=acyclic_subcls1_ RS(finite_subcls1 RS finite_acyclic_wf_converse);
-
-
-val fields_rec_ = wf_subcls1_ RSN (1, fields_rec_lemma);
-
-Goal "fields (tprg, Object) = []";
-by (stac fields_rec_ 1);
-by   Auto_tac;
-qed "fields_Object";
-Addsimps [fields_Object];
-
-Addsimps [is_class_def];
-
-Goal "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]";
-by (stac fields_rec_ 1);
-by   Auto_tac;
-qed "fields_Base";
-Addsimps [fields_Base];
-
-Goal "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @\
-                                    \ fields (tprg, Base)";
-br trans 1;
-br  fields_rec_ 1;
-by   Auto_tac;
-qed "fields_Ext";
-Addsimps [fields_Ext];
-
-val method_rec_ = wf_subcls1_ RS method_rec_lemma;
-
-Goal "method (tprg,Object) = map_of []";
-by (stac method_rec_ 1);
-by  Auto_tac;
-qed "method_Object";
-Addsimps [method_Object];
-
-Goal "method (tprg, Base) = map_of \
-\ [((foo, [Class Base]), Base, (Class Base, foo_Base))]";
-br trans 1;
-br  method_rec_ 1;
-by  Auto_tac;
-qed "method_Base";
-Addsimps [method_Base];
-
-Goal "method (tprg, Ext) = (method (tprg, Base) ++ map_of \
-\ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])";
-br trans 1;
-br  method_rec_ 1;
-by  Auto_tac;
-qed "method_Ext";
-Addsimps [method_Ext];
-
-Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Base_def] 
-"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))";
-by Auto_tac;
-qed "wf_foo_Base";
-
-Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Ext_def] 
-"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))";
-by Auto_tac;
-br  ty_expr_ty_exprs_wt_stmt.Cast 1;
-by   (Simp_tac 2);
-br   cast.subcls 2;
-by   (rewtac field_def);
-by   Auto_tac;
-qed "wf_foo_Ext";
-
-Goalw [wf_cdecl_def, wf_fdecl_def, ObjectC_def] 
-"wf_cdecl wf_java_mdecl tprg ObjectC";
-by (Simp_tac 1);
-qed "wf_ObjectC";
-
-Goalw [wf_cdecl_def, wf_fdecl_def, BaseC_def] 
-"wf_cdecl wf_java_mdecl tprg BaseC";
-by (Simp_tac 1);
-by (fold_goals_tac [BaseC_def]);
-br (wf_foo_Base RS conjI) 1;
-by Auto_tac;
-qed "wf_BaseC";
-
-Goalw [wf_cdecl_def, wf_fdecl_def, ExtC_def] 
-"wf_cdecl wf_java_mdecl tprg ExtC";
-by (Simp_tac 1);
-by (fold_goals_tac [ExtC_def]);
-br (wf_foo_Ext RS conjI) 1;
-by Auto_tac;
-bd (thm"rtranclD") 1;
-by Auto_tac;
-qed "wf_ExtC";
-
-Goalw [wf_prog_def,Let_def] 
-"wf_prog wf_java_mdecl tprg";
-by(simp_tac (simpset() addsimps [wf_ObjectC,wf_BaseC,wf_ExtC,unique_classes])1);
-qed "wf_tprg";
-
-Goalw [appl_methds_def] 
-"appl_methds tprg Base (foo, [NT]) = \
-\ {((Class Base, Class Base), [Class Base])}";
-by (Simp_tac 1);
-by (subgoal_tac "tprg\\<turnstile>NT\\<preceq> Class Base" 1);
-by  (auto_tac (claset(), simpset() addsimps [map_of_Cons,foo_Base_def]));
-qed "appl_methds_foo_Base";
-
-Goalw [max_spec_def] "max_spec tprg Base (foo, [NT]) = \
-\ {((Class Base, Class Base), [Class Base])}";
-by (auto_tac (claset(), simpset() addsimps [appl_methds_foo_Base]));
-qed "max_spec_foo_Base";
-
-fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
-Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\ 
-\ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
-(* ?pTs' = [Class Base] *)
-by t;		(* ;; *)
-by  t;		(* Expr *)
-by  t;		(* LAss *)
-by    t;	(* LAcc *)
-by     (Simp_tac 1);
-by    (Simp_tac 1);
-by   t;	(* NewC *)
-by   (Simp_tac 1);
-by  (Simp_tac 1);
-by t;	(* Expr *)
-by t;	(* Call *)
-by   t;	(* LAcc *)
-by    (Simp_tac 1);
-by   (Simp_tac 1);
-by  t;	(* Cons *)
-by   t;	(* Lit *)
-by   (Simp_tac 1);
-by  t;	(* Nil *)
-by (Simp_tac 1);
-br max_spec_foo_Base 1;
-qed "wt_test";
-
-fun e thm = resolve_tac (NewCI::eval_evals_exec.intrs) 1 thm;
-
-Delsplits[split_if];
-Addsimps[init_vars_def,c_hupd_def,cast_ok_def];
-Goalw [test_def] 
-" [|new_Addr (heap (snd s0)) = (a, None)|] ==> \
-\ tprg\\<turnstile>s0 -test-> ?s";
-(* ?s = s3 *)
-by e;		(* ;; *)
-by  e;		(* Expr *)
-by  e;		(* LAss *)
-by   e;	(* NewC *)
-by    (Force_tac 1);
-by   (Force_tac 1);
-by  (Simp_tac 1);
-be thin_rl 1;
-by e;	(* Expr *)
-by e;	(* Call *)
-by       e;	(* LAcc *)
-by      (Force_tac 1);
-by     e;	(* Cons *)
-by      e;	(* Lit *)
-by     e;	(* Nil *)
-by    (Simp_tac 1);
-by   (force_tac (claset(), simpset() addsimps [foo_Ext_def]) 1);
-by  (Simp_tac 1);
-by  e;	(* Expr *)
-by  e;	(* FAss *)
-by       e;(* Cast *)
-by        e;(* LAcc *)
-by       (Simp_tac 1);
-by      (Simp_tac 1);
-by     (Simp_tac 1);
-by     e;(* XcptE *)
-by    (Simp_tac 1);
-by   (EVERY'[rtac (surjective_pairing RS sym RSN (2,trans)), stac Pair_eq,
-             Force_tac] 1);
-by  (Simp_tac 1);
-by (Simp_tac 1);
-by e;	(* XcptE *)
-bind_thm ("exec_test", simplify (simpset()) (result()));
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -28,7 +28,7 @@
 }
 *)
 
-Example = Eval + 
+theory Example = Eval:
 
 datatype cnam_ = Base_ | Ext_
 datatype vnam_ = vee_ | x_ | e_
@@ -38,18 +38,23 @@
   cnam_ :: "cnam_ => cname"
   vnam_ :: "vnam_ => vnam"
 
-rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
+axioms (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
+
+  inj_cnam_:  "(cnam_ x = cnam_ y) = (x = y)"
+  inj_vnam_:  "(vnam_ x = vnam_ y) = (x = y)"
 
-  inj_cnam_  "(cnam_ x = cnam_ y) = (x = y)"
-  inj_vnam_  "(vnam_ x = vnam_ y) = (x = y)"
+  surj_cnam_: "\<exists>m. n = cnam_ m"
+  surj_vnam_: "\<exists>m. n = vnam_ m"
 
-  surj_cnam_ "\\<exists>m. n = cnam_ m"
-  surj_vnam_ "\\<exists>m. n = vnam_ m"
+declare inj_cnam_ [simp] inj_vnam_ [simp]
 
 syntax
 
-  Base,  Ext	:: cname
-  vee, x, e	:: vname
+  Base :: cname
+  Ext  :: cname
+  vee  :: vname
+  x    :: vname
+  e    :: vname
 
 translations
 
@@ -59,51 +64,323 @@
   "x"	 == "VName (vnam_ x_)"
   "e"	 == "VName (vnam_ e_)"
 
-rules
-  Base_not_Object "Base \\<noteq> Object"
-  Ext_not_Object  "Ext  \\<noteq> Object"
+axioms
+
+  Base_not_Object: "Base \<noteq> Object"
+  Ext_not_Object:  "Ext  \<noteq> Object"
+
+declare Base_not_Object [simp] Ext_not_Object [simp]
+declare Base_not_Object [THEN not_sym, simp] 
+declare Ext_not_Object  [THEN not_sym, simp]
 
 consts
 
-  foo_Base       :: java_mb
-  foo_Ext        :: java_mb
-  BaseC, ExtC    :: java_mb cdecl
-  test		 :: stmt
-  foo	         :: mname
-  a,b		 :: loc
+  foo_Base::  java_mb
+  foo_Ext ::  java_mb
+  BaseC   :: "java_mb cdecl"
+  ExtC    :: "java_mb cdecl"
+  test	  ::  stmt
+  foo	  ::  mname
+  a	  ::  loc
+  b       ::  loc
 
 defs
 
-  foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
-  BaseC_def "BaseC == (Base, (Object, 
+  foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
+  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
+  foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
 				       (LAcc x)..vee:=Lit (Intg #1)),
 				   Lit Null)"
-  ExtC_def  "ExtC  == (Ext,  (Base  , 
+  ExtC_def: "ExtC  == (Ext,  (Base  , 
 			     [(vee, PrimT Integer)], 
 			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
 
-  test_def "test == Expr(e::=NewC Ext);; 
+  test_def:"test == Expr(e::=NewC Ext);; 
                     Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
 
 
 syntax
 
-  NP		:: xcpt
-  tprg 	 	:: java_mb prog
-  obj1, obj2	:: obj
-  s0,s1,s2,s3,s4:: state
+  NP	:: xcpt
+  tprg 	::"java_mb prog"
+  obj1	:: obj
+  obj2	:: obj
+  s0 	:: state
+  s1 	:: state
+  s2 	:: state
+  s3 	:: state
+  s4 	:: state
 
 translations
 
   "NP"   == "NullPointer"
   "tprg" == "[ObjectC, BaseC, ExtC]"
-  "obj1"    <= "(Ext, empty((vee, Base)\\<mapsto>Bool False)
-			   ((vee, Ext )\\<mapsto>Intg #0))"
+  "obj1"    <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
+			   ((vee, Ext )\<mapsto>Intg #0))"
   "s0" == " Norm    (empty, empty)"
-  "s1" == " Norm    (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
-  "s2" == " Norm    (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
-  "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
+  "s1" == " Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+  "s2" == " Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
+  "s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+
+
+ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
+lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"
+apply (simp (no_asm))
+done
+lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa"
+apply (simp (no_asm_simp))
+done
+declare map_of_Cons [simp del]; (* sic! *)
+
+lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])"
+apply (unfold ObjectC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_Base [simp]: 
+"class tprg Base = Some (Object,  
+	  [(vee, PrimT Boolean)],  
+          [((foo, [Class Base]), Class Base, foo_Base)])"
+apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma class_tprg_Ext [simp]: 
+"class tprg Ext = Some (Base,  
+	  [(vee, PrimT Integer)],  
+          [((foo, [Class Base]), Class Ext, foo_Ext)])"
+apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (simp (no_asm))
+done
+
+lemma not_Object_subcls [elim!]: "(Object,C) \<in> (subcls1 tprg)^+ ==> R"
+apply (auto dest!: tranclD subcls1D)
+done
+
+lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
+apply (erule rtrancl_induct)
+apply  auto
+apply (drule subcls1D)
+apply auto
+done
+
+lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ ==> R"
+apply (auto dest!: tranclD subcls1D)
+done
+
+lemma class_tprgD: 
+"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext"
+apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
+apply (auto split add: split_if_asm simp add: map_of_Cons)
+done
+
+lemma not_class_subcls_class [elim!]: "(C,C) \<in> (subcls1 tprg)^+ ==> R"
+apply (auto dest!: tranclD subcls1D)
+apply (frule class_tprgD)
+apply (auto dest!:)
+apply (drule rtranclD)
+apply auto
+done
+
+lemma unique_classes: "unique tprg"
+apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def)
+done
+
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
+
+lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
+apply (rule subcls_direct)
+apply auto
+done
+
+lemma Ext_widen_Base [simp]: "tprg\<turnstile>Class Ext\<preceq> Class Base"
+apply (rule widen.subcls)
+apply (simp (no_asm))
+done
+
+declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
+
+lemma acyclic_subcls1_: "acyclic (subcls1 tprg)"
+apply (rule acyclicI)
+apply safe
+done
+
+lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]]
+
+lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma]
+
+lemma fields_Object [simp]: "fields (tprg, Object) = []"
+apply (subst fields_rec_)
+apply   auto
+done
+
+declare is_class_def [simp]
+
+lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"
+apply (subst fields_rec_)
+apply   auto
+done
+
+lemma fields_Ext [simp]: 
+  "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)"
+apply (rule trans)
+apply  (rule fields_rec_)
+apply   auto
+done
+
+lemmas method_rec_ = wf_subcls1_ [THEN [2] method_rec_lemma]
+
+lemma method_Object [simp]: "method (tprg,Object) = map_of []"
+apply (subst method_rec_)
+apply  auto
+done
+
+lemma method_Base [simp]: "method (tprg, Base) = map_of  
+  [((foo, [Class Base]), Base, (Class Base, foo_Base))]"
+apply (rule trans)
+apply  (rule method_rec_)
+apply  auto
+done
+
+lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of  
+  [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"
+apply (rule trans)
+apply  (rule method_rec_)
+apply  auto
+done
+
+lemma wf_foo_Base: 
+"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))"
+apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Base_def)
+apply auto
+done
+
+lemma wf_foo_Ext: 
+"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))"
+apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Ext_def)
+apply auto
+apply  (rule ty_expr_ty_exprs_wt_stmt.Cast)
+prefer 2
+apply   (simp)
+apply   (rule_tac [2] cast.subcls)
+apply   (unfold field_def)
+apply   auto
+done
+
+lemma wf_ObjectC: 
+"wf_cdecl wf_java_mdecl tprg ObjectC"
+apply (unfold wf_cdecl_def wf_fdecl_def ObjectC_def)
+apply (simp (no_asm))
+done
+
+lemma wf_BaseC: 
+"wf_cdecl wf_java_mdecl tprg BaseC"
+apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def)
+apply (simp (no_asm))
+apply (fold BaseC_def)
+apply (rule wf_foo_Base [THEN conjI])
+apply auto
+done
+
+lemma wf_ExtC: 
+"wf_cdecl wf_java_mdecl tprg ExtC"
+apply (unfold wf_cdecl_def wf_fdecl_def ExtC_def)
+apply (simp (no_asm))
+apply (fold ExtC_def)
+apply (rule wf_foo_Ext [THEN conjI])
+apply auto
+apply (drule rtranclD)
+apply auto
+done
+
+lemma wf_tprg: 
+"wf_prog wf_java_mdecl tprg"
+apply (unfold wf_prog_def Let_def)
+apply(simp add: wf_ObjectC wf_BaseC wf_ExtC unique_classes)
+done
+
+lemma appl_methds_foo_Base: 
+"appl_methds tprg Base (foo, [NT]) =  
+  {((Class Base, Class Base), [Class Base])}"
+apply (unfold appl_methds_def)
+apply (simp (no_asm))
+apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
+apply  (auto simp add: map_of_Cons foo_Base_def)
+done
+
+lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) =  
+  {((Class Base, Class Base), [Class Base])}"
+apply (unfold max_spec_def)
+apply (auto simp add: appl_methds_foo_Base)
+done
+
+ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *}
+lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
+  Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
+apply (tactic t) (* ;; *)
+apply  (tactic t) (* Expr *)
+apply  (tactic t) (* LAss *)
+apply    (tactic t) (* LAcc *)
+apply     (simp (no_asm))
+apply    (simp (no_asm))
+apply   (tactic t) (* NewC *)
+apply   (simp (no_asm))
+apply  (simp (no_asm))
+apply (tactic t) (* Expr *)
+apply (tactic t) (* Call *)
+apply   (tactic t) (* LAcc *)
+apply    (simp (no_asm))
+apply   (simp (no_asm))
+apply  (tactic t) (* Cons *)
+apply   (tactic t) (* Lit *)
+apply   (simp (no_asm))
+apply  (tactic t) (* Nil *)
+apply (simp (no_asm))
+apply (rule max_spec_foo_Base)
+done
+
+ML {* fun e t = resolve_tac (thm "NewCI"::thms "eval_evals_exec.intros") 1 t *}
+
+declare split_if [split del]
+declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
+lemma exec_test: 
+" [|new_Addr (heap (snd s0)) = (a, None)|] ==>  
+  tprg\<turnstile>s0 -test-> ?s"
+apply (unfold test_def)
+(* ?s = s3 *)
+apply (tactic e) (* ;; *)
+apply  (tactic e) (* Expr *)
+apply  (tactic e) (* LAss *)
+apply   (tactic e) (* NewC *)
+apply    force
+apply   force
+apply  (simp (no_asm))
+apply (erule thin_rl)
+apply (tactic e) (* Expr *)
+apply (tactic e) (* Call *)
+apply       (tactic e) (* LAcc *)
+apply      force
+apply     (tactic e) (* Cons *)
+apply      (tactic e) (* Lit *)
+apply     (tactic e) (* Nil *)
+apply    (simp (no_asm))
+apply   (force simp add: foo_Ext_def)
+apply  (simp (no_asm))
+apply  (tactic e) (* Expr *)
+apply  (tactic e) (* FAss *)
+apply       (tactic e) (* Cast *)
+apply        (tactic e) (* LAcc *)
+apply       (simp (no_asm))
+apply      (simp (no_asm))
+apply     (simp (no_asm))
+apply     (tactic e) (* XcptE *)
+apply    (simp (no_asm))
+apply   (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
+apply  (simp (no_asm))
+apply (simp (no_asm))
+apply (tactic e) (* XcptE *)
+done
+
 end
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/JBasis.ML
--- a/src/HOL/MicroJava/J/JBasis.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(*  Title:      HOL/MicroJava/J/JBasis.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 TU Muenchen
-*)
-
-(*###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];
-
-bind_thm ("if_def2", read_instantiate [("P","\\<lambda>x. x")] split_if);
-
-(* ### 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";
-
-Goal "(x, y) : set xys --> x : fst ` set xys";
-by (induct_tac "xys" 1);
-by  Auto_tac;
-qed_spec_mp "fst_in_set_lemma";
-
-Goalw [unique_def] "unique []";
-by (Simp_tac 1);
-qed "unique_Nil";
-
-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";
-
-Addsimps [unique_Nil,unique_Cons];
-
-Goal "unique l' ==> unique l --> \
-\ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')";
-by (induct_tac "l" 1);
-by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
-qed_spec_mp "unique_append";
-
-Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)";
-by (induct_tac "l" 1);
-by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
-qed_spec_mp "unique_map_inj";
-
-(* More about Maps *)
-
-(*###Addsimps [fun_upd_same, fun_upd_other];*)
-
-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);
-by(ALLGOALS Simp_tac);
-by Safe_tac;
-by Auto_tac;
-bind_thm("Ball_set_table",result() 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";
-
-(* ### 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);
-by Auto_tac;
-qed "map_of_map";
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -6,11 +6,69 @@
 Some auxiliary definitions.
 *)
 
-JBasis = Main + 
+theory JBasis = Main: 
 
+lemmas [simp] = Let_def
+
+section "unique"
+ 
 constdefs
 
   unique  :: "('a \\<times> 'b) list => bool"
  "unique  == nodups \\<circ> map fst"
 
+
+lemma fst_in_set_lemma [rule_format (no_asm)]: 
+      "(x, y) : set xys --> x : fst ` set xys"
+apply (induct_tac "xys")
+apply  auto
+done
+
+lemma unique_Nil [simp]: "unique []"
+apply (unfold unique_def)
+apply (simp (no_asm))
+done
+
+lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
+apply (unfold unique_def)
+apply (auto dest: fst_in_set_lemma)
+done
+
+lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l --> 
+ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
+apply (induct_tac "l")
+apply  (auto dest: fst_in_set_lemma)
+done
+
+lemma unique_map_inj [rule_format (no_asm)]: 
+  "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
+apply (induct_tac "l")
+apply  (auto dest: fst_in_set_lemma simp add: inj_eq)
+done
+
+section "More about Maps"
+
+lemma map_of_SomeI [rule_format (no_asm)]: 
+  "unique l --> (k, x) : set l --> map_of l k = Some x"
+apply (induct_tac "l")
+apply  auto
+done
+
+lemma Ball_set_table_: 
+  "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)"
+apply(induct_tac "l")
+apply(simp_all (no_asm))
+apply safe
+apply auto
+done
+lemmas Ball_set_table = Ball_set_table_ [THEN mp];
+
+lemma table_of_remap_SomeD [rule_format (no_asm)]: 
+"map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> 
+ map_of t (k, k') = Some x"
+apply (induct_tac "t")
+apply  auto
+done
+
 end
+
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,330 +0,0 @@
-(*  Title:      HOL/MicroJava/J/JTypeSafe.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-
-Type safety proof
-*)
-
-
-
-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 [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_tac "v = Null" 1);
-by(  Asm_full_simp_tac 1);
-by(  dtac widen_RefT 1);
-by(  Clarify_tac 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 |] ==> \
-\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\\<preceq>ft";
-by( dtac np_NoneD 1);
-by( etac conjE 1);
-by( mp_tac 1);
-by( dtac non_np_objD 1);
-by   Auto_tac;
-by( dtac (conforms_heapD RS hconfD) 1);
-by(  atac 1);
-by( datac widen_cfs_fields 2 1);
-by( datac oconf_objD 1 1);
-by Auto_tac;
-qed "FAcc_type_sound";
-
-Goal
- "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); \
-\   (G, lT)\\<turnstile>v::T'; G\\<turnstile>T'\\<preceq>ft; \
-\   (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|] ==> \
-\ 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>  \
-\ G,h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x))))\\<turnstile>x::\\<preceq>T'";
-by( dtac np_NoneD 1);
-by( etac conjE 1);
-by( Asm_full_simp_tac 1);
-by( dtac non_np_objD 1);
-by(   atac 1);
-by(  SELECT_GOAL Auto_tac 1);
-by( Clarify_tac 1);
-by( Full_simp_tac 1);
-by( EVERY [ftac hext_objD 1, atac 1]);
-by( etac exE 1);
-by( Asm_full_simp_tac 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);
-by(  fast_tac (HOL_cs addEs [conf_upd_obj RS iffD2]) 2);
-
-by( rtac conforms_upd_obj 1);
-by   Auto_tac;
-by(  rtac hextI 2);
-by(  Force_tac 2);
-by( rtac oconf_hext 1);
-by(  etac hext_upd_obj 2);
-by( dtac widen_cfs_fields 1);
-by(   atac 1);
-by(  atac 1);
-by( rtac (oconf_obj RS iffD2) 1);
-by( Simp_tac 1);
-by( strip_tac 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);
-qed "FAss_type_sound";
-
-Goalw [wf_mhead_def] "[| 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; nodups pns; \
-\ Ball (set lvars) (split (\\<lambda>vn. is_type G)) \
-\ |] ==> G,h\\<turnstile>init_vars lvars(pns[\\<mapsto>]pvs)[::\\<preceq>]map_of lvars(pns[\\<mapsto>]pTs')";
-by( Clarsimp_tac 1);
-by( rtac lconf_ext_list 1);
-by(    rtac (Ball_set_table RS lconf_init_vars) 1);
-by(    Force_tac 1);
-by(   atac 1);
-by(  atac 1);
-by( (etac conf_list_gext_widen THEN_ALL_NEW atac) 1);
-qed "Call_lemma2";
-
-Goalw [wf_java_prog_def]
- "[| 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) = \
-\              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)";
-by( dtac max_spec2mheads 1);
-by( Clarify_tac 1);
-by( datac non_np_objD' 2 1);
-by(  Clarsimp_tac 1);
-by( Clarsimp_tac 1);
-by( EVERY'[ftac hext_objD, atac] 1);
-by( Clarsimp_tac 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);
-by(  mp_tac 2);
-by(  rtac conformsI 1);
-by(   etac conforms_heapD 1);
-by(  rtac lconf_ext 1);
-by(   force_tac (claset() addSEs [Call_lemma2],simpset()) 1);
-by(  EVERY'[etac conf_hext, etac conf_obj_AddrI, atac] 1);
-by( thin_tac "?E\\<turnstile>?blk\\<surd>" 1);
-by( etac conjE 1);
-by( EVERY'[dtac spec, mp_tac] 1);
-(*by( thin_tac "?E::\\<preceq>(G, pT')" 1);*)
-by( EVERY'[dtac spec, mp_tac] 1);
-by( thin_tac "?E\\<turnstile>res::?rT" 1);
-by( Clarify_tac 1);
-by( rtac conjI 1);
-by(  fast_tac (HOL_cs addIs [hext_trans]) 1);
-by( rtac conjI 1);
-by(  rtac impI 2);
-by(  mp_tac 2);
-by(  forward_tac [conf_widen] 2);
-by(    atac 4);
-by(   atac 2);
-by(  fast_tac (HOL_cs addSEs [widen_trans]) 2);
-by( etac conforms_hext 1);
-by(  etac hext_trans 1);
-by(  atac 1);
-by( etac conforms_heapD 1);
-qed "Call_type_sound";
-
-
-
-Unify.search_bound := 40;
-Unify.trace_bound  := 40;
-Delsplits[split_if];
-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
-"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> \
-\ (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> \
-\ (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)))";
-by( rtac eval_evals_exec_induct 1);
-by( rewtac c_hupd_def);
-
-(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
-by( ALLGOALS Asm_full_simp_tac);
-by( ALLGOALS strip_tac);
-by( ALLGOALS (eresolve_tac ty_expr_ty_exprs_wt_stmt.elims 
-		THEN_ALL_NEW Full_simp_tac));
-by( ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac]));
-by( rewtac wf_java_prog_def);
-
-(* Level 7 *)
-
-(* 15 NewC *)
-by( dtac new_AddrD 1);
-by( etac disjE 1);
-by(  Asm_simp_tac 2);
-by( Clarsimp_tac 1);
-by( rtac conjI 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);
-
-(* for Cast *)
-by( defer_tac 1);
-
-(* 14 Lit *)
-by( etac conf_litval 1);
-
-(* 13 BinOp *)
-by forward_hyp_tac;
-by forward_hyp_tac;
-by( EVERY'[rtac conjI, eatac hext_trans 1] 1);
-by( etac conjI 1);
-by( Clarsimp_tac 1);
-by( dtac eval_no_xcpt 1);
-by( asm_full_simp_tac (simpset() addsplits [binop.split]) 1);
-
-(* 12 LAcc *)
-by( fast_tac (claset() addEs [conforms_localD RS lconfD]) 1);
-
-(* for FAss *)
-by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac, 
-			REPEAT o (etac conjE), hyp_subst_tac] 3);
-
-(* for if *)
-by( (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
-
-by forward_hyp_tac;
-
-(* 11+1 if *)
-by(  fast_tac (HOL_cs addIs [hext_trans]) 8);
-by( fast_tac (HOL_cs addIs [hext_trans]) 8);
-
-(* 10 Expr *)
-by( Fast_tac 6);
-
-(* 9 ??? *)
-by( ALLGOALS Asm_full_simp_tac);
-
-(* 8 Cast *)
-by( EVERY'[rtac impI, dtac raise_if_NoneD, Clarsimp_tac, 
-           fast_tac (claset() addEs [Cast_conf])] 8);
-
-(* 7 LAss *)
-by( asm_simp_tac (simpset() addsplits [split_if]) 1);
-by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac] 1);
-by( blast_tac (claset() addIs [conforms_upd_local, conf_widen]) 1);
-
-(* 6 FAcc *)
-by( fast_tac (claset() addSEs [FAcc_type_sound]) 1);
-
-(* 5 While *)
-by(thin_tac "?a \\<longrightarrow> ?b" 5);
-by(datac ty_expr_ty_exprs_wt_stmt.Loop 1 5);
-by(force_tac (claset() addEs [hext_trans], simpset()) 5);
-
-by forward_hyp_tac;
-
-(* 4 Cons *)
-by( fast_tac (claset() addDs [evals_no_xcpt] addIs [conf_hext,hext_trans]) 3);
-
-(* 3 ;; *)
-by( fast_tac (claset() addIs [hext_trans]) 3);
-
-(* 2 FAss *)
-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);
-by( dtac eval_no_xcpt 1);
-by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
-
-by prune_params_tac;
-(* Level 52 *)
-
-(* 1 Call *)
-by( case_tac "x" 1);
-by(  Clarsimp_tac 2);
-by(  dtac exec_xcpt 2);
-by(  Asm_full_simp_tac 2);
-by(  dtac eval_xcpt 2);
-by(  Asm_full_simp_tac 2);
-by(  fast_tac (HOL_cs addEs [hext_trans]) 2);
-by( Clarify_tac 1);
-by( dtac evals_no_xcpt 1);
-by( Asm_full_simp_tac 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( datac ty_expr_is_type 1 1);
-by(Clarsimp_tac 1);
-by(rewtac is_class_def);
-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";
-
-Goal "!!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)";
-by( split_all_tac 1);
-bd (eval_evals_exec_type_sound RS conjunct1 RS mp RS spec RS mp) 1;
-by Auto_tac;
-qed "eval_type_sound";
-
-Goal "!!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";
-by( split_all_tac 1);
-bd (eval_evals_exec_type_sound RS conjunct2 RS conjunct2 RS mp RS spec RS mp) 1;
-by   Auto_tac;
-qed "exec_type_sound";
-
-Goal "[|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|] ==> \
-\ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
-by( datac eval_type_sound 4 1);
-by(Clarsimp_tac 1);
-by(rewtac wf_java_prog_def);
-by( forward_tac [widen_methd] 1);
-by(   atac 1);
-by(  Fast_tac 2);
-by( dtac non_npD 1);
-by Auto_tac;
-qed "all_methods_understood";
-
-Delsimps [split_beta];
-Addsimps[fun_upd_apply];
-
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -3,7 +3,357 @@
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
 
-Type Safety of Java
+Type Safety Proof for MicroJava
 *)
 
-JTypeSafe = Eval + Conform
+theory JTypeSafe = Eval + Conform:
+
+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)"
+apply( erule conforms_upd_obj)
+apply(  unfold oconf_def)
+apply(  auto dest!: fields_is_type)
+done
+ 
+lemma Cast_conf: 
+ "[| 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" 
+apply (unfold cast_ok_def)
+apply( case_tac "v = Null")
+apply(  simp)
+apply(  drule widen_RefT)
+apply(  clarify)
+apply( drule (1) non_npD)
+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);  
+  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)
+apply( erule conjE)
+apply( erule (1) notE impE)
+apply( drule non_np_objD)
+apply   auto
+apply( drule conforms_heapD [THEN hconfD])
+apply(  assumption)
+apply( drule (2) widen_cfs_fields)
+apply( drule (1) oconf_objD)
+apply auto
+done
+
+lemma FAss_type_sound: 
+ "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a);  
+    (G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft;  
+    (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|] ==>  
+  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>   
+  G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'"
+apply( drule np_NoneD)
+apply( erule conjE)
+apply( simp)
+apply( drule non_np_objD)
+apply(   assumption)
+apply(  force)
+apply( clarify)
+apply( simp (no_asm_use))
+apply( frule (1) hext_objD)
+apply( erule exE)
+apply( simp)
+apply( clarify)
+apply( rule conjI)
+apply(  fast elim: hext_trans hext_upd_obj)
+apply( rule conjI)
+prefer 2
+apply(  fast elim: conf_upd_obj [THEN iffD2])
+
+apply( rule conforms_upd_obj)
+apply   auto
+apply(  rule_tac [2] hextI)
+prefer 2
+apply(  force)
+apply( rule oconf_hext)
+apply(  erule_tac [2] hext_upd_obj)
+apply( drule (2) widen_cfs_fields)
+apply( rule oconf_obj [THEN iffD2])
+apply( simp (no_asm))
+apply( intro strip)
+apply( case_tac "(aaa, b) = (fn, fd)")
+apply(  simp)
+apply(  fast intro: conf_widen)
+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; nodups pns;  
+  Ball (set lvars) (split (\<lambda>vn. is_type G))  
+  |] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')"
+apply (unfold wf_mhead_def)
+apply( clarsimp)
+apply( rule lconf_ext_list)
+apply(    rule Ball_set_table [THEN lconf_init_vars])
+apply(    force)
+apply(   assumption)
+apply(  assumption)
+apply( erule (2) conf_list_gext_widen)
+done
+
+lemma Call_type_sound: 
+ "[| 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) =  
+               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)"
+apply (unfold wf_java_prog_def)
+apply( drule max_spec2mheads)
+apply( clarify)
+apply( drule (2) non_np_objD')
+apply(  clarsimp)
+apply( clarsimp)
+apply( frule (1) hext_objD)
+apply( clarsimp)
+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(  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 conjE)
+apply( drule spec, erule (1) impE)
+apply( drule spec, erule (1) impE)
+apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl)
+apply( clarify)
+apply( rule conjI)
+apply(  fast intro: hext_trans)
+apply( rule conjI)
+apply(  rule_tac [2] impI)
+apply(  erule_tac [2] notE impE, tactic "assume_tac 2")
+apply(  frule_tac [2] conf_widen)
+apply(    tactic "assume_tac 4")
+apply(   tactic "assume_tac 2")
+prefer 2
+apply(  fast elim!: widen_trans)
+apply( erule conforms_hext)
+apply(  erule (1) hext_trans)
+apply( erule conforms_heapD)
+done
+
+declare split_if [split del]
+declare fun_upd_apply [simp del]
+declare fun_upd_same [simp]
+ML{*
+val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
+	(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]))
+*}
+ML{*
+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>  
+  (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>  
+  (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)))"
+apply( rule eval_evals_exec_induct)
+apply( unfold c_hupd_def)
+
+(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *)
+apply( simp_all)
+apply( tactic "ALLGOALS strip_tac")
+apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) *})
+apply( tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
+apply( unfold wf_java_prog_def)
+
+(* Level 7 *)
+
+(* 15 NewC *)
+apply( drule new_AddrD)
+apply( erule disjE)
+prefer 2
+apply(  simp (no_asm_simp))
+apply( clarsimp)
+apply( rule conjI)
+apply(  force elim!: NewC_conforms)
+apply( rule conf_obj_AddrI)
+apply(  rule_tac [2] rtrancl_refl)
+apply( simp (no_asm))
+
+(* for Cast *)
+defer 1
+
+(* 14 Lit *)
+apply( erule conf_litval)
+
+(* 13 BinOp *)
+apply (tactic "forward_hyp_tac")
+apply (tactic "forward_hyp_tac")
+apply( rule conjI, erule (1) hext_trans)
+apply( erule conjI)
+apply( clarsimp)
+apply( drule eval_no_xcpt)
+apply( simp split add: binop.split)
+
+(* 12 LAcc *)
+apply( fast elim: conforms_localD [THEN lconfD])
+
+(* for FAss *)
+apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
+
+(* for if *)
+apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*})
+
+apply (tactic "forward_hyp_tac")
+
+(* 11+1 if *)
+prefer 8
+apply(  fast intro: hext_trans)
+prefer 8
+apply(  fast intro: hext_trans)
+
+(* 10 Expr *)
+prefer 6
+apply( fast)
+
+(* 9 ??? *)
+apply( simp_all)
+
+(* 8 Cast *)
+prefer 8
+apply (rule impI)
+apply (drule raise_if_NoneD)
+apply (clarsimp)
+apply (fast elim: Cast_conf)
+
+(* 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( blast intro: conforms_upd_local conf_widen)
+
+(* 6 FAcc *)
+apply( fast elim!: FAcc_type_sound)
+
+(* 5 While *)
+prefer 5
+apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl)
+apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop)
+apply(force elim: hext_trans)
+
+apply (tactic "forward_hyp_tac")
+
+(* 4 Cons *)
+prefer 3
+apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans)
+
+(* 3 ;; *)
+prefer 3
+apply( fast intro: 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, simp (no_asm) (*###rule refl*), assumption+)
+
+apply( tactic prune_params_tac)
+(* Level 52 *)
+
+(* 1 Call *)
+apply( case_tac "x")
+prefer 2
+apply(  clarsimp)
+apply(  drule exec_xcpt)
+apply(  simp)
+apply(  drule_tac eval_xcpt)
+apply(  simp)
+apply(  fast elim: hext_trans)
+apply( clarify)
+apply( drule evals_no_xcpt)
+apply( simp)
+apply( case_tac "a' = Null")
+apply(  simp)
+apply(  drule exec_xcpt)
+apply(  simp)
+apply(  drule eval_xcpt)
+apply(  simp)
+apply(  fast elim: hext_trans)
+apply( drule (1) ty_expr_is_type)
+apply(clarsimp)
+apply(unfold is_class_def)
+apply(clarsimp)
+apply(rule Call_type_sound [unfolded wf_java_prog_def]);
+prefer 11
+apply blast
+apply (simp (no_asm_simp))+
+done
+ML{*
+Unify.search_bound := 20;
+Unify.trace_bound  := 20
+*}
+
+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)"
+apply( simp (no_asm_simp) only: split_tupled_all)
+apply (drule eval_evals_exec_type_sound 
+             [THEN conjunct1, THEN mp, THEN spec, THEN mp])
+apply auto
+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"
+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])
+apply   auto
+done
+
+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|] ==>  
+  method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None"
+apply( drule (4) eval_type_sound)
+apply(clarsimp)
+apply(unfold wf_java_prog_def)
+apply( frule widen_methd)
+apply(   assumption)
+prefer 2
+apply(  fast)
+apply( drule non_npD)
+apply auto
+done
+
+declare split_beta [simp del]
+declare fun_upd_apply [simp]
+
+end
+
+
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/State.ML
--- a/src/HOL/MicroJava/J/State.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,81 +0,0 @@
-(*  Title:      HOL/MicroJava/J/State.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-Goalw [obj_ty_def] "obj_ty (C,fs) = Class C";
-by (Simp_tac 1);
-qed "obj_ty_def2";
-Addsimps [obj_ty_def2];
-
-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";
-
-
-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)) = \
-\ Some (if c then xc else NullPointer)";
-by (Simp_tac 1);
-qed "np_raise_if";
-Addsimps[np_raise_if];
-
-
-
-
-
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/State.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -6,34 +6,34 @@
 State for evaluation of Java expressions and statements
 *)
 
-State = TypeRel + Value +
+theory State = TypeRel + Value:
 
 types	fields_
-	= "(vname \\<times> cname \\<leadsto> val)" (* field name, defining class, value *)
+	= "(vname \<times> cname \<leadsto> val)" (* field name, defining class, value *)
 
-        obj = "cname \\<times> fields_"	(* class instance with class name and fields *)
+        obj = "cname \<times> fields_"	(* class instance with class name and fields *)
 
 constdefs
   obj_ty	:: "obj => ty"
  "obj_ty obj  == Class (fst obj)"
 
-  init_vars	:: "('a \\<times> ty) list => ('a \\<leadsto> val)"
- "init_vars	== map_of o map (\\<lambda>(n,T). (n,default_val T))"
+  init_vars	:: "('a \<times> ty) list => ('a \<leadsto> val)"
+ "init_vars	== map_of o map (\<lambda>(n,T). (n,default_val T))"
   
 datatype xcpt		(* exceptions *)
 	= NullPointer
 	| ClassCast
 	| OutOfMemory
 
-types	aheap  = "loc \\<leadsto> obj" (* "heap" used in a translation below *)
-        locals = "vname \\<leadsto> val"	
+types	aheap  = "loc \<leadsto> obj" (* "heap" used in a translation below *)
+        locals = "vname \<leadsto> val"	
 
         state		(* simple state, i.e. variable contents *)
-	= "aheap \\<times> locals"
+	= "aheap \<times> locals"
 	(* heap, local parameter including This *)
 
 	xstate		(* state including exception information *)
-	 = "xcpt option \\<times> state"
+	 = "xcpt option \<times> state"
 
 syntax
   heap		:: "state => aheap"
@@ -47,19 +47,98 @@
 
 constdefs
 
-  new_Addr	:: "aheap => loc \\<times> xcpt option"
- "new_Addr h == SOME (a,x). (h a = None \\<and>  x = None) |  x = Some OutOfMemory"
+  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 => xcpt => xcpt option => xcpt option"
- "raise_if c x xo == if c \\<and>  (xo = None) then Some x else xo"
+ "raise_if c x xo == if c \<and>  (xo = None) then Some x else xo"
 
   np		:: "val => xcpt option => xcpt option"
  "np v == raise_if (v = Null) NullPointer"
 
   c_hupd	:: "aheap => xstate => xstate"
- "c_hupd h'== \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
+ "c_hupd h'== \<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
 
   cast_ok	:: "'c prog => cname => aheap => val => bool"
- "cast_ok G C h v == v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C"
+ "cast_ok G C h v == v = Null \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C"
+
+lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C"
+apply (unfold obj_ty_def)
+apply (simp (no_asm))
+done
+
+lemma new_AddrD: 
+"(a,x) = new_Addr h ==> h a = None \<and> x = None | x = Some OutOfMemory"
+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 auto
+done
+
+
+lemma raise_if_True [simp]: "raise_if True x y \<noteq> None"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma raise_if_False [simp]: "raise_if False x y = y"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma raise_if_Some [simp]: "raise_if c x (Some y) \<noteq> None"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma raise_if_Some2 [simp]: "raise_if c z (if x = None then Some y else x) \<noteq> None"
+apply (unfold raise_if_def)
+apply(induct_tac "x")
+apply auto
+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"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma raise_if_NoneD [rule_format (no_asm)]: "raise_if c x y = None --> \<not> c \<and>  y = None"
+apply (unfold raise_if_def)
+apply auto
+done
+
+lemma np_NoneD [rule_format (no_asm)]: "np a' x' = None --> x' = None \<and>  a' \<noteq> Null"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_None [rule_format (no_asm), simp]: "a' \<noteq> Null --> np a' x' = x'"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_Some [simp]: "np a' (Some xc) = Some xc"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_Null [simp]: "np Null None = Some NullPointer"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_Addr [simp]: "np (Addr a) None = None"
+apply (unfold np_def raise_if_def)
+apply auto
+done
+
+lemma np_raise_if [simp]: "(np Null (raise_if c xc None)) =  
+  Some (if c then xc else NullPointer)"
+apply (unfold raise_if_def)
+apply (simp (no_asm))
+done
 
 end
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Term.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -6,7 +6,7 @@
 Java expressions and statements
 *)
 
-Term = Value +
+theory Term = Value:
 
 datatype binop = Eq | Add    (* function codes for binary operation *)
 
@@ -21,7 +21,7 @@
   | FAss cname expr vname 
                     expr     (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90)
   | Call cname expr mname 
-    (ty list) (expr list)    (* method call*) ("{_}_.._'( {_}_')"
+    "ty list" "expr list"    (* method call*) ("{_}_.._'( {_}_')"
                                                             [10,90,99,10,10] 90)
 
 datatype stmt
@@ -32,3 +32,4 @@
   | Loop expr stmt       ("While '(_') _"     [80,79]70)
 
 end
+
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Type.thy
--- a/src/HOL/MicroJava/J/Type.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Type.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -6,13 +6,14 @@
 Java types
 *)
 
-Type = JBasis +
+theory Type = JBasis:
 
-types cname   (* class name *)
-      vnam    (* variable or field name *)
-      mname   (* method name *)
-
-arities cname, vnam, mname :: term
+typedecl cname  (* class name *)
+typedecl vnam   (* variable or field name *)
+typedecl mname  (* method name *)
+arities  cname :: "term"
+         vnam  :: "term"
+         mname :: "term"
 
 datatype vname    (* names for This pointer and local/field variables *)
   = This
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-(*  Title:      HOL/MicroJava/J/TypeRel.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-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";
-
-Goalw [subcls1_def, is_class_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_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";
-
-
-Goalw [is_class_def] "(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";
-
-Goalw [is_class_def] "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]) 1);
-by(strip_tac 1);
-by(rename_tac "A x" 1);
-by(case_tac "wf(R A)" 1);
-by (eres_inst_tac [("a","x")] wf_induct 1);
-by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
-by (Fast_tac 1);
-by(rewrite_goals_tac [wf_def]);
-by(Blast_tac 1);
-qed "wf_rel_lemma";
-
-
-(* Proving the termination conditions *)
-
-goalw thy [subcls1_rel_def] "wf subcls1_rel";
-by(rtac (wf_rel_lemma RS wf_subset) 1);
-by(Force_tac 1);
-qed "wf_subcls1_rel";
-
-val method_TC = prove_goalw_cterm [subcls1_rel_def]
- (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (method.tcs)))))
- (K [auto_tac (claset() addIs [subcls1I], simpset())]);
-
-val fields_TC = prove_goalw_cterm [subcls1_rel_def]
- (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,widen.null];
-Addsimps [widen.refl];
-
-Goal "(G\\<turnstile>PrimT pT\\<preceq>RefT rT) = False";
-br iffI 1;
-be widen.elim 1;
-by Auto_tac;
-qed "widen_PrimT_RefT";
-AddIffs [widen_PrimT_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";
-
-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";
-
-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;
-be widen.elim 1;
-by(Auto_tac);
-qed "widen_Class_NullT";
-AddIffs [widen_Class_NullT];
-
-Goal "(G\\<turnstile>Class C\\<preceq> Class D) = (G\\<turnstile>C\\<preceq>C D)";
-br iffI 1;
-be widen.elim 1;
-by(Auto_tac);
-bes widen.intrs 1;
-qed "widen_Class_Class";
-AddIffs [widen_Class_Class];
-
-Goal "G\\<turnstile>S\\<preceq>U ==> \\<forall>T. G\\<turnstile>U\\<preceq>T --> G\\<turnstile>S\\<preceq>T";
-by( etac widen.induct 1);
-by   Safe_tac;
-by(  ALLGOALS (forward_tac [widen_Class, widen_RefT]));
-by  Safe_tac;
-by(eatac rtrancl_trans 1 1);
-qed_spec_mp "widen_trans";
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -6,18 +6,18 @@
 The relations between Java types
 *)
 
-TypeRel = Decl +
+theory TypeRel = Decl:
 
 consts
-  subcls1 :: "'c prog => (cname \\<times> cname) set"  (* subclass *)
-  widen   :: "'c prog => (ty    \\<times> ty   ) set"  (* widening *)
-  cast    :: "'c prog => (cname \\<times> cname) set"  (* casting *)
+  subcls1 :: "'c prog => (cname \<times> cname) set"  (* subclass *)
+  widen   :: "'c prog => (ty    \<times> ty   ) set"  (* widening *)
+  cast    :: "'c prog => (cname \<times> cname) set"  (* casting *)
 
 syntax
-  subcls1 :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<prec>C1 _" [71,71,71] 70)
-  subcls  :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>C _" [71,71,71] 70)
-  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \\<turnstile> _ \\<preceq> _" [71,71,71] 70)
-  cast    :: "'c prog => [cname, cname] => bool" ("_ \\<turnstile> _ \\<preceq>? _" [71,71,71] 70)
+  subcls1 :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<prec>C1 _" [71,71,71] 70)
+  subcls  :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>C _" [71,71,71] 70)
+  widen   :: "'c prog => [ty   , ty   ] => bool" ("_ \<turnstile> _ \<preceq> _" [71,71,71] 70)
+  cast    :: "'c prog => [cname, cname] => bool" ("_ \<turnstile> _ \<preceq>? _" [71,71,71] 70)
 
 syntax (HTML)
   subcls1 :: "'c prog => [cname, cname] => bool" ("_ |- _ <=C1 _" [71,71,71] 70)
@@ -26,58 +26,215 @@
   cast    :: "'c prog => [cname, cname] => bool" ("_ |- _ <=? _" [71,71,71] 70)
 
 translations
-  "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
-  "G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
-  "G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
-  "G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
+  "G\<turnstile>C \<prec>C1 D" == "(C,D) \<in> subcls1 G"
+  "G\<turnstile>C \<preceq>C  D" == "(C,D) \<in> (subcls1 G)^*"
+  "G\<turnstile>S \<preceq>   T" == "(S,T) \<in> widen   G"
+  "G\<turnstile>C \<preceq>?  D" == "(C,D) \<in> cast    G"
 
 defs
 
   (* direct subclass, cf. 8.1.3 *)
- subcls1_def"subcls1 G \\<equiv> {(C,D). C\\<noteq>Object \\<and> (\\<exists>c. class G C=Some c \\<and> fst c=D)}"
+ subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class G C=Some c \<and> fst c=D)}"
   
+lemma subcls1D: 
+  "G\<turnstile>C\<prec>C1D \<Longrightarrow> C \<noteq> Object \<and> (\<exists>fs ms. class G C = Some (D,fs,ms))"
+apply (unfold subcls1_def)
+apply auto
+done
+
+lemma subcls1I: "\<lbrakk>class G C = Some (D,rest); C \<noteq> Object\<rbrakk> \<Longrightarrow> G\<turnstile>C\<prec>C1D"
+apply (unfold subcls1_def)
+apply auto
+done
+
+lemma subcls1_def2: 
+"subcls1 G = (\<Sigma>C\<in>{C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
+apply (unfold subcls1_def is_class_def)
+apply auto
+done
+
+lemma finite_subcls1: "finite (subcls1 G)"
+apply(subst subcls1_def2)
+apply(rule finite_SigmaI [OF finite_is_class])
+apply(rule_tac B = "{fst (the (class G C))}" in finite_subset)
+apply  auto
+done
+
+lemma subcls_is_class: "(C,D) \<in> (subcls1 G)^+ ==> is_class G C"
+apply (unfold is_class_def)
+apply(erule trancl_trans_induct)
+apply (auto dest!: subcls1D)
+done
+
+lemma subcls_is_class2 [rule_format (no_asm)]: "G\<turnstile>C\<preceq>C D \<Longrightarrow> is_class G D \<longrightarrow> is_class G C"
+apply (unfold is_class_def)
+apply (erule rtrancl_induct)
+apply  (drule_tac [2] subcls1D)
+apply  auto
+done
+
+consts class_rec ::"'c prog \<times> cname \<Rightarrow> 
+        'a \<Rightarrow> (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
+recdef class_rec "same_fst (\<lambda>G. wf ((subcls1 G)^-1)) (\<lambda>G. (subcls1 G)^-1)"
+      "class_rec (G,C) = (\<lambda>t f. case class G C of None \<Rightarrow> arbitrary 
+                         | Some (D,fs,ms) \<Rightarrow> if wf ((subcls1 G)^-1) then 
+      f C fs ms (if C = Object then t else class_rec (G,D) t f) else arbitrary)"
+recdef_tc class_rec_tc: class_rec
+  apply (unfold same_fst_def)
+  apply (auto intro: subcls1I)
+  done
+
+lemma class_rec_lemma: "\<lbrakk> wf ((subcls1 G)^-1); class G C = Some (D,fs,ms)\<rbrakk> \<Longrightarrow>
+ class_rec (G,C) t f = f C fs ms (if C=Object then t else class_rec (G,D) t f)";
+  apply (rule class_rec_tc [THEN class_rec.simps 
+              [THEN trans [THEN fun_cong [THEN fun_cong]]]])
+  apply (rule ext, rule ext)
+  apply auto
+  done
+
 consts
 
-  method	:: "'c prog \\<times> cname => ( sig   \\<leadsto> cname \\<times> ty \\<times> 'c)"
-  field	:: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
-  fields	:: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times>  ty) list"
-
-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}"
+  method :: "'c prog \<times> cname => ( sig   \<leadsto> cname \<times> ty \<times> 'c)" (* ###curry *)
+  field  :: "'c prog \<times> cname => ( vname \<leadsto> cname \<times> ty     )" (* ###curry *)
+  fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
 
 (* 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 =>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 ). 
-                                                        (s,(C,m))) ms))
-                  else arbitrary)"
+defs method_def: "method \<equiv> \<lambda>(G,C). class_rec (G,C) empty (\<lambda>C fs ms ts.
+                           ts ++ map_of (map (\<lambda>(s,m). (s,(C,m))) ms))"
+
+lemma method_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
+  method (G,C) = (if C = Object then empty else method (G,D)) ++  
+  map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
+apply (unfold method_def)
+apply (simp split del: split_if)
+apply (erule (1) class_rec_lemma [THEN trans]);
+apply auto
+done
+
 
 (* 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 (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)"
-defs
+defs fields_def: "fields \<equiv> \<lambda>(G,C). class_rec (G,C) []    (\<lambda>C fs ms ts.
+                           map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ ts)"
+
+lemma fields_rec_lemma: "[|class G C = Some (D,fs,ms); wf ((subcls1 G)^-1)|] ==>
+ fields (G,C) = 
+  map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
+apply (unfold fields_def)
+apply (simp split del: split_if)
+apply (erule (1) class_rec_lemma [THEN trans]);
+apply auto
+done
+
+
+defs field_def: "field == map_of o (map (\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+
+lemma field_fields: 
+"field (G,C) fn = Some (fd, fT) \<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT"
+apply (unfold field_def)
+apply (rule table_of_remap_SomeD)
+apply simp
+done
+
+
+inductive "widen G" intros (*widening, viz. method invocation conversion,cf. 5.3
+			     i.e. sort of syntactic subtyping *)
+  refl   [intro!, simp]:       "G\<turnstile>      T \<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
+  subcls         : "G\<turnstile>C\<preceq>C D ==> G\<turnstile>Class C \<preceq> Class D"
+  null   [intro!]:             "G\<turnstile>     NT \<preceq> RefT R"
 
-  field_def "field == map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
+inductive "cast G" intros (* casting conversion, cf. 5.5 / 5.1.5 *)
+                          (* left out casts on primitve types    *)
+  widen:  "G\<turnstile>C\<preceq>C D ==> G\<turnstile>C \<preceq>? D"
+  subcls: "G\<turnstile>D\<preceq>C C ==> G\<turnstile>C \<preceq>? D"
+
+lemma widen_PrimT_RefT [iff]: "(G\<turnstile>PrimT pT\<preceq>RefT rT) = False"
+apply (rule iffI)
+apply (erule widen.elims)
+apply auto
+done
+
+lemma widen_RefT: "G\<turnstile>RefT R\<preceq>T ==> \<exists>t. T=RefT t"
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply auto
+done
+
+lemma widen_RefT2: "G\<turnstile>S\<preceq>RefT R ==> \<exists>t. S=RefT t"
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply auto
+done
+
+lemma widen_Class: "G\<turnstile>Class C\<preceq>T ==> \<exists>D. T=Class D"
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply auto
+done
+
+lemma widen_Class_NullT [iff]: "(G\<turnstile>Class C\<preceq>NT) = False"
+apply (rule iffI)
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply auto
+done
 
-inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
-			     i.e. sort of syntactic subtyping *)
-  refl	             "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
-  subcls "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>Class C \\<preceq> Class D"
-  null	             "G\\<turnstile>     NT \\<preceq> RefT R"
+lemma widen_Class_Class [iff]: "(G\<turnstile>Class C\<preceq> Class D) = (G\<turnstile>C\<preceq>C D)"
+apply (rule iffI)
+apply (ind_cases "G\<turnstile>S\<preceq>T")
+apply (auto elim: widen.subcls)
+done
+
+lemma widen_trans [rule_format (no_asm)]: "G\<turnstile>S\<preceq>U ==> \<forall>T. G\<turnstile>U\<preceq>T --> G\<turnstile>S\<preceq>T"
+apply (erule widen.induct)
+apply   safe
+apply  (frule widen_Class)
+apply  (frule_tac [2] widen_RefT)
+apply  safe
+apply(erule (1) rtrancl_trans)
+done
+
+ML {* InductAttrib.print_global_rules(the_context()) *}
+ML {* set show_tags *}
 
-inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
-                         (* left out casts on primitve types    *)
-  widen	 "G\\<turnstile>C\\<preceq>C D ==> G\\<turnstile>C \\<preceq>? D"
-  subcls "G\\<turnstile>D\\<preceq>C C ==> G\\<turnstile>C \\<preceq>? D"
+(*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
+proof -
+  assume "G\<turnstile>S\<preceq>U"
+  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
+  proof (induct (*cases*) (open) (*?P S U*) rule: widen.induct [consumes 1])
+    case refl
+    fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
+      (* fix T' show "PROP ?P T T".*)
+  next
+    case subcls
+    fix T assume "G\<turnstile>Class D\<preceq>T"
+    then obtain E where "T = Class E" by (blast dest: widen_Class)
+    from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
+  next
+    case null
+    fix RT assume "G\<turnstile>RefT R\<preceq>RT"
+    then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
+    thus "G\<turnstile>NT\<preceq>RT" by auto
+  qed
+qed
+*)
+
+theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
+proof -
+  assume "G\<turnstile>S\<preceq>U"
+  thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
+  proof (induct (*cases*) (open) (*?P S U*)) (* rule: widen.induct *)
+    case refl
+    fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
+      (* fix T' show "PROP ?P T T".*)
+  next
+    case subcls
+    fix T assume "G\<turnstile>Class D\<preceq>T"
+    then obtain E where "T = Class E" by (blast dest: widen_Class)
+    from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
+  next
+    case null
+    fix RT assume "G\<turnstile>RefT R\<preceq>RT"
+    then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
+    thus "G\<turnstile>NT\<preceq>RT" by auto
+  qed
+qed
+
+
 
 end
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/Value.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/J/Term.thy
+(*  Title:      HOL/MicroJava/J/Value.thy
     ID:         $Id$
     Author:     David von Oheimb
     Copyright   1999 Technische Universitaet Muenchen
@@ -6,12 +6,12 @@
 Java values
 *)
 
-Value = Type +
+theory Value = Type:
 
-types   loc     (* locations, i.e. abstract references on objects *)
-arities loc :: term
+typedecl loc (* locations, i.e. abstract references on objects *)
+arities loc :: "term"
 
-datatype val_   (* name non 'val' because of clash with ML token *)
+datatype val
   = Unit        (* dummy result value of void methods *)
   | Null        (* null reference *)
   | Bool bool   (* Boolean value *)
@@ -19,9 +19,6 @@
                    of clash with HOL/Set.thy *)
   | Addr loc    (* addresses, i.e. locations of objects *)
 
-types	val = val_
-translations "val" <= (type) "val_"
-
 consts
   the_Bool :: "val => bool"
   the_Intg :: "val => int"
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/WellForm.ML
--- a/src/HOL/MicroJava/J/WellForm.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,349 +0,0 @@
-(*  Title:      HOL/MicroJava/J/WellForm.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-Goalw [wf_prog_def, class_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";
-
-Goalw [wf_prog_def, ObjectC_def, class_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];
-
-Goalw [is_class_def] "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(Clarify_tac 1);
-by( datac class_wf 1 1);
-by( rewtac wf_cdecl_def);
-by(force_tac (claset(), simpset() addsimps [thm"reflcl_trancl" RS sym] 
-				  delsimps [thm"reflcl_trancl"]) 1);
-qed "subcls1_wfD";
-
-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 (claset() addSDs [subcls1_wfD] addIs [trancl_trans])));
-qed "subcls_asym";
-
-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";
-
-Goalw [acyclic_def] "wf_prog wf_mb G ==> acyclic (subcls1 G)";
-by (fast_tac (claset() addDs [subcls_irrefl]) 1);
-qed "acyclic_subcls1";
-
-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";
-by(cut_facts_tac [major RS wf_subcls1] 1);
-by(dtac wf_trancl 1);
-by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
-by(eres_inst_tac [("a","C")] wf_induct 1);
-by(resolve_tac prems 1);
-by(Auto_tac);
-qed "subcls_induct";
-
-val prems = goalw thy [is_class_def] "[|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 (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);
-by(   atac 2);
-by(  atac 2);
-by( etac thin_rl 1);
-by( rtac subcls_induct 1);
-by(  atac 1);
-by( rtac impI 1);
-by( case_tac "C = Object" 1);
-by(  Fast_tac 1);
-by Safe_tac;
-by( ftac class_wf 1);
-by(  atac 1);
-by( ftac wf_cdecl_supD 1);
-by(  atac 1);
-
-by( subgoal_tac "G\\<turnstile>C\\<prec>C1a" 1);
-by( etac subcls1I 2);
-by( rtac (hd (tl (tl (tl prems)))) 1);
-by (rewtac is_class_def);
-by Auto_tac;
-qed "subcls1_induct";
-
-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);
-by Auto_tac;
-qed "method_rec_lemma";
-
-Goal "wf_prog wf_mb G ==> 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(rtac method_rec_lemma 1);
-by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def] 
-		addsplits [option.split]) 1);
-by( case_tac "C = Object" 1);
-by(  Force_tac 1);
-by Safe_tac;
-by( datac class_wf 1 1);
-by( datac wf_cdecl_supD 1 1);
-by( Asm_full_simp_tac 1);
-qed "method_rec";
-
-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 (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]) 1);
-ba  1;
-br refl 2;
-by( datac class_wf 1 1);
-by(rtac impI 1);
-by( eatac wf_cdecl_supD 1 1);
-qed "fields_rec";
-
-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];
-
-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";
-by(etac subcls1_induct 1);
-by(  atac 1);
-by( Fast_tac 1);
-by(auto_tac (HOL_cs addSDs [wf_cdecl_supD], simpset()));
-by(eatac rtrancl_into_rtrancl2 1 1);
-qed "subcls_C_Object";
-
-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";
-by( etac subcls1_induct 1);
-by(   atac 1);
-by(  Asm_simp_tac 1);
-by( safe_tac HOL_cs);
-by( stac fields_rec 1);
-by(   atac 1);
-by(  atac 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(  Force_tac 1);
-by( etac (r_into_rtrancl RS rtrancl_trans) 1);
-by Auto_tac;
-qed "widen_fields_defpl'";
-
-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 (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);
-by(  safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
-by(  Asm_simp_tac 1);
-by( dtac subcls1_wfD 1);
-by(  atac 1);
-by( stac fields_rec 1);
-by   Auto_tac;
-by( rotate_tac ~1 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_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
-"\\<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";
-
-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 (thm"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";
-
-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( etac subcls1_induct 1);
-by(   atac 1);
-by(  Force_tac 1);
-by( forw_inst_tac [("C","C")] method_rec 1);
-by( Clarify_tac 1);
-by( rotate_tac ~1 1);
-by( Asm_full_simp_tac 1);
-by( dtac override_SomeD 1);
-by( etac disjE 1);
-by(  thin_tac "?P --> ?Q" 1);
-by(  Clarify_tac 2);
-by(  rtac rtrancl_trans 2);
-by(   atac 3);
-by(  rtac r_into_rtrancl 2);
-by(  fast_tac (HOL_cs addIs [subcls1I]) 2);
-by (rotate_tac ~1 1);
-by (ftac map_of_SomeD 1);
-by( rewtac wf_cdecl_def);
-by (Clarsimp_tac 1);
-qed_spec_mp "method_wf_mdecl";
-
-Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
-\  \\<forall>D rT b. method (G,T') sig = Some (D,rT ,b) -->\
-\ (\\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
-by( dtac (thm"rtranclD") 1);
-by( etac disjE 1);
-by(  Fast_tac 1);
-by( etac conjE 1);
-by( etac trancl_trans_induct 1);
-by(  Clarify_tac 2);
-by(  EVERY[smp_tac 3 2]);
-by(  fast_tac (HOL_cs addEs [widen_trans]) 2);
-by( Clarify_tac 1);
-by( dtac subcls1D 1);
-by( Clarify_tac 1);
-by( stac method_rec 1);
-by(  atac 1);
-by( rewtac override_def);
-by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
-by( case_tac "\\<exists>z. map_of(map (\\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z" 1);
-by(  etac exE 1);
-by(  asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 2);
-by(  ALLGOALS (rotate_tac ~1 THEN' forward_tac[ssubst] THEN' (fn n=>atac(n+1))));
-by(  ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex])));
-by( dtac class_wf 1);
-by(  atac 1);
-by( split_all_tac 1);
-by( rewtac wf_cdecl_def);
-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) |] \
-\ ==> \\<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
-by(auto_tac (claset() addDs [subcls_widen_methd,method_wf_mdecl],
-             simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
-qed "subtype_widen_methd";
-
-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);
-by (stac method_rec 1);
- ba 1;
-by (Clarify_tac 1);
-by (eres_inst_tac [("x","Da")] allE 1);
-by (Clarsimp_tac 1);
- by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
- by (Clarify_tac 1);
- by (stac method_rec 1);
-  ba 1;
- 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( stac fields_rec 1);
-by(   Fast_tac 1);
-by(  atac 1);
-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( Clarsimp_tac 1);
-by( EVERY[dtac bspec 1, atac 1]);
-by( rewtac wf_fdecl_def);
-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 a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -14,31 +14,410 @@
 * for uniformity, Object is assumed to be declared like any other class
 *)
 
-WellForm = TypeRel +
+theory WellForm = TypeRel:
 
-types 'c wf_mb = 'c prog => cname => 'c mdecl => bool
+types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
 
 constdefs
  wf_fdecl :: "'c prog => fdecl => bool"
-"wf_fdecl G == \\<lambda>(fn,ft). is_type G ft"
+"wf_fdecl G == \<lambda>(fn,ft). is_type G ft"
 
  wf_mhead :: "'c prog => sig => ty => bool"
-"wf_mhead G == \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
+"wf_mhead G == \<lambda>(mn,pTs) rT. (\<forall>T\<in>set pTs. is_type G T) \<and> is_type G rT"
 
  wf_mdecl :: "'c wf_mb => 'c wf_mb"
-"wf_mdecl wf_mb G C == \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wf_mb G C (sig,rT,mb)"
+"wf_mdecl wf_mb G C == \<lambda>(sig,rT,mb). wf_mhead G sig rT \<and> wf_mb G C (sig,rT,mb)"
 
  wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
 "wf_cdecl wf_mb G ==
-   \\<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>
-  (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'))"
+   \<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>
+  (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 ==
-   let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wf_mb G c) \\<and> unique G"
+   let cs = set G in ObjectC \<in> cs \<and> (\<forall>c\<in>cs. wf_cdecl wf_mb G c) \<and> unique G"
+
+lemma class_wf: 
+ "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)"
+apply (unfold wf_prog_def class_def)
+apply (simp)
+apply (fast dest: map_of_SomeD)
+done
+
+lemma class_Object [simp]: 
+	"wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])"
+apply (unfold wf_prog_def ObjectC_def class_def)
+apply (auto intro: map_of_SomeI)
+done
+
+lemma is_class_Object [simp]: "wf_prog wf_mb G ==> is_class G Object"
+apply (unfold is_class_def)
+apply (simp (no_asm_simp))
+done
+
+lemma subcls1_wfD: "[|G\<turnstile>C\<prec>C1D; wf_prog wf_mb G|] ==> D \<noteq> C \<and> \<not>(D,C)\<in>(subcls1 G)^+"
+apply( frule r_into_trancl)
+apply( drule subcls1D)
+apply(clarify)
+apply( drule (1) class_wf)
+apply( unfold wf_cdecl_def)
+apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
+done
+
+lemma wf_cdecl_supD: 
+"!!r. \<lbrakk>wf_cdecl wf_mb G (C,D,r); C \<noteq> Object\<rbrakk> \<Longrightarrow> is_class G D"
+apply (unfold wf_cdecl_def)
+apply (auto split add: option.split_asm)
+done
+
+lemma subcls_asym: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> \<not>(D,C)\<in>(subcls1 G)^+"
+apply(erule tranclE)
+apply(fast dest!: subcls1_wfD )
+apply(fast dest!: subcls1_wfD intro: trancl_trans)
+done
+
+lemma subcls_irrefl: "[|wf_prog wf_mb G; (C,D)\<in>(subcls1 G)^+|] ==> C \<noteq> D"
+apply (erule trancl_trans_induct)
+apply  (auto dest: subcls1_wfD subcls_asym)
+done
+
+lemma acyclic_subcls1: "wf_prog wf_mb G ==> acyclic (subcls1 G)"
+apply (unfold acyclic_def)
+apply (fast dest: subcls_irrefl)
+done
+
+lemma wf_subcls1: "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)"
+apply (rule finite_acyclic_wf)
+apply ( subst finite_converse)
+apply ( rule finite_subcls1)
+apply (subst acyclic_converse)
+apply (erule acyclic_subcls1)
+done
+
+lemma subcls_induct: 
+"[|wf_prog wf_mb G; !!C. \<forall>D. (C,D)\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C"
+(is "?A \<Longrightarrow> PROP ?P \<Longrightarrow> _")
+proof -
+  assume p: "PROP ?P"
+  assume ?A thus ?thesis apply -
+apply(drule wf_subcls1)
+apply(drule wf_trancl)
+apply(simp only: trancl_converse)
+apply(erule_tac a = C in wf_induct)
+apply(rule p)
+apply(auto)
+done
+qed
+
+lemma subcls1_induct:
+"[|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 (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"
+(is "?A \<Longrightarrow> ?B \<Longrightarrow> ?C \<Longrightarrow> PROP ?P \<Longrightarrow> _")
+proof -
+  assume p: "PROP ?P"
+  assume ?A ?B ?C thus ?thesis apply -
+apply(unfold is_class_def)
+apply( rule impE)
+prefer 2
+apply(   assumption)
+prefer 2
+apply(  assumption)
+apply( erule thin_rl)
+apply( rule subcls_induct)
+apply(  assumption)
+apply( rule impI)
+apply( case_tac "C = Object")
+apply(  fast)
+apply safe
+apply( frule (1) class_wf)
+apply( frule (1) wf_cdecl_supD)
+
+apply( subgoal_tac "G\<turnstile>C\<prec>C1a")
+apply( erule_tac [2] subcls1I)
+apply(  rule p)
+apply (unfold is_class_def)
+apply auto
+done
+qed
+
+lemmas method_rec = wf_subcls1 [THEN [2] method_rec_lemma];
+
+lemmas fields_rec = wf_subcls1 [THEN [2] fields_rec_lemma];
+
+lemma method_Object [simp]: "wf_prog wf_mb G ==> method (G,Object) = empty"
+apply(subst method_rec)
+apply auto
+done
+
+lemma fields_Object [simp]: "wf_prog wf_mb G ==> fields (G,Object) = []"
+apply(subst fields_rec)
+apply auto
+done
+
+lemma field_Object [simp]: "wf_prog wf_mb G ==> field (G,Object) = empty"
+apply (unfold field_def)
+apply(simp (no_asm_simp))
+done
+
+lemma subcls_C_Object: "[|is_class G C; wf_prog wf_mb G|] ==> G\<turnstile>C\<preceq>C Object"
+apply(erule subcls1_induct)
+apply(  assumption)
+apply( fast)
+apply(auto dest!: wf_cdecl_supD)
+apply(erule (1) rtrancl_into_rtrancl2)
+done
+
+lemma is_type_rTI: "wf_mhead G sig rT ==> is_type G rT"
+apply (unfold wf_mhead_def)
+apply auto
+done
+
+lemma widen_fields_defpl': "[|is_class G C; wf_prog wf_mb G|] ==>  
+  \<forall>((fn,fd),fT)\<in>set (fields (G,C)). G\<turnstile>C\<preceq>C fd"
+apply( erule subcls1_induct)
+apply(   assumption)
+apply(  simp (no_asm_simp))
+apply( tactic "safe_tac HOL_cs")
+apply( subst fields_rec)
+apply(   assumption)
+apply(  assumption)
+apply( simp (no_asm) split del: split_if)
+apply( rule ballI)
+apply( simp (no_asm_simp) only: split_tupled_all)
+apply( simp (no_asm))
+apply( erule UnE)
+apply(  force)
+apply( erule r_into_rtrancl [THEN rtrancl_trans])
+apply auto
+done
+
+lemma widen_fields_defpl: "[|((fn,fd),fT) \<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==>  
+  G\<turnstile>C\<preceq>C fd"
+apply( drule (1) widen_fields_defpl')
+apply (fast)
+done
+
+lemma unique_fields: "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))"
+apply( erule subcls1_induct)
+apply(   assumption)
+apply(  safe dest!: wf_cdecl_supD)
+apply(  simp (no_asm_simp))
+apply( drule subcls1_wfD)
+apply(  assumption)
+apply( subst fields_rec)
+apply   auto
+apply( rotate_tac -1)
+apply( frule class_wf)
+apply  auto
+apply( simp add: wf_cdecl_def)
+apply( erule unique_append)
+apply(  rule unique_map_inj)
+apply(   clarsimp)
+apply  (rule injI)
+apply(  simp)
+apply(auto dest!: widen_fields_defpl)
+done
+
+lemma fields_mono_lemma [rule_format (no_asm)]: "[|wf_prog wf_mb G; (C',C)\<in>(subcls1 G)^*|] ==>  
+  x \<in> set (fields (G,C)) --> x \<in> set (fields (G,C'))"
+apply(erule converse_rtrancl_induct)
+apply( safe dest!: subcls1D)
+apply(subst fields_rec)
+apply(  auto)
+done
+
+lemma 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"
+apply (rule map_of_SomeI)
+apply  (erule (1) unique_fields)
+apply (erule (1) fields_mono_lemma)
+apply (erule map_of_SomeD)
+done
+
+lemma widen_cfs_fields: 
+"[|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"
+apply (drule field_fields)
+apply (drule rtranclD)
+apply safe
+apply (frule subcls_is_class)
+apply (drule trancl_into_rtrancl)
+apply (fast dest: fields_mono)
+done
+
+lemma method_wf_mdecl [rule_format (no_asm)]: "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))"
+apply( erule subcls1_induct)
+apply(   assumption)
+apply(  force)
+apply( clarify)
+apply( frule_tac C = C in method_rec)
+apply(  assumption)
+apply( rotate_tac -1)
+apply( simp)
+apply( drule override_SomeD)
+apply( erule disjE)
+apply(  erule_tac V = "?P --> ?Q" in thin_rl)
+apply (frule map_of_SomeD)
+apply (clarsimp simp add: wf_cdecl_def)
+apply( clarify)
+apply( rule rtrancl_trans)
+prefer 2
+apply(  assumption)
+apply( rule r_into_rtrancl)
+apply( fast intro: subcls1I)
+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) --> 
+  (\<exists>D' rT' b'. method (G,T) sig = Some (D',rT',b') \<and> G\<turnstile>rT'\<preceq>rT)"
+apply( drule rtranclD)
+apply( erule disjE)
+apply(  fast)
+apply( erule conjE)
+apply( erule trancl_trans_induct)
+prefer 2
+apply(  clarify)
+apply(  drule spec, drule spec, drule spec, erule (1) impE)
+apply(  fast elim: widen_trans)
+apply( clarify)
+apply( drule subcls1D)
+apply( clarify)
+apply( subst method_rec)
+apply(  assumption)
+apply( unfold override_def)
+apply( simp (no_asm_simp) del: split_paired_Ex)
+apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
+apply(  erule exE)
+apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
+prefer 2
+apply(  rotate_tac -1, frule ssubst, erule_tac [2] asm_rl)
+apply(  tactic "asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1")
+apply(  simp_all (no_asm_simp) del: split_paired_Ex)
+apply( drule (1) class_wf)
+apply( simp (no_asm_simp) only: split_tupled_all)
+apply( unfold wf_cdecl_def)
+apply( drule map_of_SomeD)
+apply auto
+done
+
+lemma subtype_widen_methd: 
+ "[| G\<turnstile> C\<preceq>C D; wf_prog wf_mb G;  
+     method (G,D) sig = Some (md, rT, b) |]  
+  ==> \<exists>mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \<and> G\<turnstile>rT'\<preceq>rT"
+apply(auto dest: subcls_widen_methd method_wf_mdecl simp add: wf_mdecl_def wf_mhead_def split_def)
+done
+
+lemma method_in_md [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \<Longrightarrow> \<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \<and> method (G,D) sig = Some(D,mh,code)"
+apply (erule (1) subcls1_induct)
+ apply (simp)
+apply (erule conjE)
+apply (subst method_rec)
+  apply (assumption)
+ apply (assumption)
+apply (clarify)
+apply (erule_tac "x" = "Da" in allE)
+apply (clarsimp)
+ apply (simp add: map_of_map)
+ apply (clarify)
+ apply (subst method_rec)
+   apply (assumption)
+  apply (assumption)
+ apply (simp add: override_def map_of_map split add: option.split)
+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"
+apply( drule subcls_widen_methd)
+apply   auto
+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>  
+  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)"
+apply( drule (2) widen_methd)
+apply( clarify)
+apply( frule subcls_is_class2)
+apply (unfold is_class_def)
+apply (simp (no_asm_simp))
+apply( drule method_wf_mdecl)
+apply( unfold wf_mdecl_def)
+apply( unfold is_class_def)
+apply auto
+done
+
+
+lemma fields_is_type_lemma [rule_format (no_asm)]: "[|is_class G C; wf_prog wf_mb G|] ==>  
+  \<forall>f\<in>set (fields (G,C)). is_type G (snd f)"
+apply( erule (1) subcls1_induct)
+apply(  simp (no_asm_simp))
+apply( subst fields_rec)
+apply(   fast)
+apply(  assumption)
+apply( clarsimp)
+apply( safe)
+prefer 2
+apply(  force)
+apply( drule (1) class_wf)
+apply( unfold wf_cdecl_def)
+apply( clarsimp)
+apply( drule (1) bspec)
+apply( unfold wf_fdecl_def)
+apply auto
+done
+
+lemma fields_is_type: "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==>  
+  is_type G f"
+apply(drule map_of_SomeD)
+apply(drule (2) fields_is_type_lemma)
+apply(auto)
+done
+
+lemma methd:
+  "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls |]
+  ==> method (G,C) sig = Some(C,rT,code) \<and> is_class G C"
+proof -
+  assume wf: "wf_prog wf_mb G" 
+  assume C:  "(C,S,fs,mdecls) \<in> set G"
+
+  assume m: "(sig,rT,code) \<in> set mdecls"
+  moreover
+  from wf
+  have "class G Object = Some (arbitrary, [], [])"
+    by simp 
+  moreover
+  from wf C
+  have c: "class G C = Some (S,fs,mdecls)"
+    by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
+  ultimately
+  have O: "C \<noteq> Object"
+    by auto
+      
+  from wf C
+  have "unique mdecls"
+    by (unfold wf_prog_def wf_cdecl_def) auto
+
+  hence "unique (map (\<lambda>(s,m). (s,C,m)) mdecls)"
+    by - (induct mdecls, auto)
+
+  with m
+  have "map_of (map (\<lambda>(s,m). (s,C,m)) mdecls) sig = Some (C,rT,code)"
+    by (force intro: map_of_SomeI)
+
+  with wf C m c O
+  show ?thesis
+    by (auto simp add: is_class_def dest: method_rec)
+qed
 
 end
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/WellType.ML
--- a/src/HOL/MicroJava/J/WellType.ML	Thu Feb 01 20:51:48 2001 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(*  Title:      HOL/MicroJava/J/WellType.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-Goal
-"[| 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";
-by( dtac subcls_widen_methd 1);
-by   Auto_tac;
-qed "widen_methd";
-
-
-Goal
-"[|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( Clarify_tac 1);
-by( ftac subcls_is_class2 1);
-by (rewtac is_class_def);
-by (Asm_simp_tac 1);
-by( dtac method_wf_mdecl 1);
-by( rewtac wf_mdecl_def);
-by( rewtac is_class_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";
-Addsimps [method_Object];
-
-Goalw [max_spec_def] 
-  "x \\<in> max_spec G C sig ==> x \\<in> appl_methds G C sig";
-by (Fast_tac 1);
-qed"max_spec2appl_meths";
-
-Goalw [appl_methds_def] 
-"((md,rT),pTs')\\<in>appl_methds G C (mn, pTs) ==> \
-\ \\<exists>D b. md = Class D \\<and> method (G,C) (mn, pTs') = Some (D,rT,b) \
-\ \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'";
-by (Fast_tac 1);
-qed "appl_methsD";
-
-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 a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy	Thu Feb 01 20:53:13 2001 +0100
@@ -15,41 +15,59 @@
 
 *)
 
-WellType = Term + WellForm +
+theory WellType = Term + WellForm:
 
 types	lenv (* local variables, including method parameters and This *)
-	= "vname \\<leadsto> ty"
+	= "vname \<leadsto> ty"
         'c env
-	= "'c prog \\<times> lenv"
+	= "'c prog \<times> lenv"
 
 syntax
   prg    :: "'c env => 'c prog"
-  localT :: "'c env => (vname \\<leadsto> ty)"
+  localT :: "'c env => (vname \<leadsto> ty)"
 
 translations	
   "prg"    => "fst"
   "localT" => "snd"
 
 consts
-  more_spec :: "'c prog => (ty \\<times> 'x) \\<times> ty list =>
-                (ty \\<times> 'x) \\<times> ty list => bool"
-  appl_methds :: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
-  max_spec :: "'c prog =>  cname => sig => ((ty \\<times> ty) \\<times> ty list) set"
+  more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list =>
+                (ty \<times> 'x) \<times> ty list => bool"
+  appl_methds :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
+  max_spec :: "'c prog =>  cname => sig => ((ty \<times> ty) \<times> ty list) set"
 
 defs
-  more_spec_def "more_spec G == \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
-		                            list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
+  more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and>
+		                            list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
   
   (* applicable methods, cf. 15.11.2.1 *)
-  appl_methds_def "appl_methds G C == \\<lambda>(mn, pTs).
+  appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs).
 		                 {((Class md,rT),pTs') |md rT mb pTs'.
-		                  method (G,C)  (mn, pTs') = Some (md,rT,mb) \\<and>
-		                  list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
+		                  method (G,C)  (mn, pTs') = Some (md,rT,mb) \<and>
+		                  list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}"
 
   (* maximally specific methods, cf. 15.11.2.2 *)
-  max_spec_def "max_spec G C sig == {m. m \\<in>appl_methds G C sig \\<and> 
-                                      (\\<forall>m'\\<in>appl_methds G C sig.
-                                        more_spec G m' m --> m' = m)}"
+  max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
+                                       (\<forall>m'\<in>appl_methds G C sig.
+                                         more_spec G m' m --> m' = m)}"
+
+lemma max_spec2appl_meths: 
+  "x \<in> max_spec G C sig ==> x \<in> appl_methds G C sig"
+apply (unfold max_spec_def)
+apply (fast)
+done
+
+lemma appl_methsD: 
+"((md,rT),pTs')\<in>appl_methds G C (mn, pTs) ==>  
+  \<exists>D b. md = Class D \<and> method (G,C) (mn, pTs') = Some (D,rT,b)  
+  \<and> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'"
+apply (unfold appl_methds_def)
+apply (fast)
+done
+
+lemmas max_spec2mheads = insertI1 [THEN [2] equalityD2 [THEN subsetD], 
+                         THEN max_spec2appl_meths, THEN appl_methsD]
+
 
 consts
   typeof :: "(loc => ty option) => val => ty option"
@@ -61,19 +79,30 @@
 	"typeof dt (Intg i) = Some (PrimT Integer)"
 	"typeof dt (Addr a) = dt a"
 
+lemma is_type_typeof [rule_format (no_asm), simp]: "(\<forall>a. v \<noteq> Addr a) --> (\<exists>T. typeof t v = Some T \<and> is_type G T)"
+apply (rule val.induct)
+apply     auto
+done
+
+lemma typeof_empty_is_type [rule_format (no_asm)]: 
+  "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
+apply (rule val.induct)
+apply     auto
+done
+
 types
-	java_mb = "vname list \\<times> (vname \\<times> ty) list \\<times> stmt \\<times> expr"
+	java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr"
 	(* method body with parameter names, local variables, block, result expression *)
 
 consts
-  ty_expr :: "java_mb env => (expr      \\<times> ty     ) set"
-  ty_exprs:: "java_mb env => (expr list \\<times> ty list) set"
+  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"
 
 syntax
-  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ \\<turnstile> _ :: _"   [51,51,51]50)
-  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \\<turnstile> _ [::] _" [51,51,51]50)
-  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ \\<turnstile> _ \\<surd>"      [51,51   ]50)
+  ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ \<turnstile> _ :: _"   [51,51,51]50)
+  ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50)
+  wt_stmt :: "java_mb env =>  stmt                => bool" ("_ \<turnstile> _ \<surd>"      [51,51   ]50)
 
 syntax (HTML)
   ty_expr :: "java_mb env => [expr     , ty     ] => bool" ("_ |- _ :: _"   [51,51,51]50)
@@ -82,107 +111,123 @@
 
 
 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,T) \<in> ty_expr  E"
+	"E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E"
+	"E\<turnstile>c \<surd>"    == "c     \<in> wt_stmt  E"
   
-inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intrs
+inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intros
 
 (* well-typed expressions *)
 
   (* cf. 15.8 *)
-  NewC	"[| is_class (prg E) C |] ==>
-         E\\<turnstile>NewC C::Class C"
+  NewC:	"[| is_class (prg E) C |] ==>
+         E\<turnstile>NewC C::Class C"
 
   (* cf. 15.15 *)
-  Cast  "[| E\\<turnstile>e::Class C; is_class (prg E) D;
-            prg E\\<turnstile>C\\<preceq>? D |] ==>
-         E\\<turnstile>Cast D e::Class D"
+  Cast:	"[| E\<turnstile>e::Class C; is_class (prg E) D;
+            prg E\<turnstile>C\<preceq>? D |] ==>
+         E\<turnstile>Cast D e::Class D"
 
   (* cf. 15.7.1 *)
-  Lit	  "[| typeof (\\<lambda>v. None) x = Some T |] ==>
-         E\\<turnstile>Lit x::T"
+  Lit:	  "[| typeof (\<lambda>v. None) x = Some T |] ==>
+         E\<turnstile>Lit x::T"
 
   
   (* cf. 15.13.1 *)
-  LAcc  "[| localT E v = Some T; is_type (prg E) T |] ==>
-         E\\<turnstile>LAcc v::T"
+  LAcc:	"[| localT E v = Some T; is_type (prg E) T |] ==>
+         E\<turnstile>LAcc v::T"
 
-  BinOp "[| E\\<turnstile>e1::T;
-            E\\<turnstile>e2::T;
+  BinOp:"[| E\<turnstile>e1::T;
+            E\<turnstile>e2::T;
             if bop = Eq then T' = PrimT Boolean
-                        else T' = T \\<and> T = PrimT Integer|] ==>
-         E\\<turnstile>BinOp bop e1 e2::T'"
+                        else T' = T \<and> T = PrimT Integer|] ==>
+         E\<turnstile>BinOp bop e1 e2::T'"
 
   (* cf. 15.25, 15.25.1 *)
-  LAss  "[| E\\<turnstile>LAcc v::T;
-	          E\\<turnstile>e::T';
-            prg E\\<turnstile>T'\\<preceq>T |] ==>
-         E\\<turnstile>v::=e::T'"
+  LAss: "[| E\<turnstile>LAcc v::T;
+	          E\<turnstile>e::T';
+            prg E\<turnstile>T'\<preceq>T |] ==>
+         E\<turnstile>v::=e::T'"
 
   (* cf. 15.10.1 *)
-  FAcc  "[| E\\<turnstile>a::Class C; 
+  FAcc: "[| E\<turnstile>a::Class C; 
             field (prg E,C) fn = Some (fd,fT) |] ==>
-         E\\<turnstile>{fd}a..fn::fT"
+         E\<turnstile>{fd}a..fn::fT"
 
   (* cf. 15.25, 15.25.1 *)
-  FAss  "[| E\\<turnstile>{fd}a..fn::T;
-            E\\<turnstile>v        ::T';
-            prg E\\<turnstile>T'\\<preceq>T |] ==>
-         E\\<turnstile>{fd}a..fn:=v::T'"
+  FAss: "[| E\<turnstile>{fd}a..fn::T;
+            E\<turnstile>v        ::T';
+            prg E\<turnstile>T'\<preceq>T |] ==>
+         E\<turnstile>{fd}a..fn:=v::T'"
 
 
   (* cf. 15.11.1, 15.11.2, 15.11.3 *)
-  Call  "[| E\\<turnstile>a::Class C;
-            E\\<turnstile>ps[::]pTs;
+  Call: "[| E\<turnstile>a::Class C;
+            E\<turnstile>ps[::]pTs;
             max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} |] ==>
-         E\\<turnstile>{C}a..mn({pTs'}ps)::rT"
+         E\<turnstile>{C}a..mn({pTs'}ps)::rT"
 
 (* well-typed expression lists *)
 
   (* cf. 15.11.??? *)
-  Nil  "E\\<turnstile>[][::][]"
+  Nil: "E\<turnstile>[][::][]"
 
   (* cf. 15.11.??? *)
-  Cons "[| E\\<turnstile>e::T;
-           E\\<turnstile>es[::]Ts |] ==>
-        E\\<turnstile>e#es[::]T#Ts"
+  Cons:"[| E\<turnstile>e::T;
+           E\<turnstile>es[::]Ts |] ==>
+        E\<turnstile>e#es[::]T#Ts"
 
 (* well-typed statements *)
 
-  Skip "E\\<turnstile>Skip\\<surd>"
+  Skip:"E\<turnstile>Skip\<surd>"
 
-  Expr "[| E\\<turnstile>e::T |] ==>
-        E\\<turnstile>Expr e\\<surd>"
+  Expr:"[| E\<turnstile>e::T |] ==>
+        E\<turnstile>Expr e\<surd>"
 
-  Comp "[| E\\<turnstile>s1\\<surd>; 
-           E\\<turnstile>s2\\<surd> |] ==>
-        E\\<turnstile>s1;; s2\\<surd>"
+  Comp:"[| E\<turnstile>s1\<surd>; 
+           E\<turnstile>s2\<surd> |] ==>
+        E\<turnstile>s1;; s2\<surd>"
 
   (* cf. 14.8 *)
-  Cond "[| E\\<turnstile>e::PrimT Boolean;
-           E\\<turnstile>s1\\<surd>;
-           E\\<turnstile>s2\\<surd> |] ==>
-         E\\<turnstile>If(e) s1 Else s2\\<surd>"
+  Cond:"[| E\<turnstile>e::PrimT Boolean;
+           E\<turnstile>s1\<surd>;
+           E\<turnstile>s2\<surd> |] ==>
+         E\<turnstile>If(e) s1 Else s2\<surd>"
 
   (* cf. 14.10 *)
-  Loop "[| E\\<turnstile>e::PrimT Boolean;
-           E\\<turnstile>s\\<surd> |] ==>
-        E\\<turnstile>While(e) s\\<surd>"
+  Loop:"[| E\<turnstile>e::PrimT Boolean;
+           E\<turnstile>s\<surd> |] ==>
+        E\<turnstile>While(e) s\<surd>"
 
 constdefs
 
- wf_java_mdecl :: java_mb prog => cname => java_mb mdecl => bool
-"wf_java_mdecl G C == \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
-	length pTs = length pns \\<and>
-	nodups pns \\<and>
-	unique lvars \\<and>
-	(\\<forall>pn\\<in>set pns. map_of lvars pn = None) \\<and>
-	(\\<forall>(vn,T)\\<in>set lvars. is_type G T) &
-	(let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
-	 E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res::T \\<and> G\\<turnstile>T\\<preceq>rT))"
+ wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool"
+"wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
+	length pTs = length pns \<and>
+	nodups pns \<and>
+	unique lvars \<and>
+	(\<forall>pn\<in>set pns. map_of lvars pn = None) \<and>
+	(\<forall>(vn,T)\<in>set lvars. is_type G T) &
+	(let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in
+	 E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))"
 
- wf_java_prog :: java_mb prog => bool
+ wf_java_prog :: "java_mb prog => bool"
 "wf_java_prog G == wf_prog wf_java_mdecl G"
 
+
+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)"
+apply (rule ty_expr_ty_exprs_wt_stmt.induct)
+apply auto
+apply (   erule typeof_empty_is_type)
+apply (  simp split add: split_if_asm)
+apply ( drule field_fields)
+apply ( drule (1) fields_is_type)
+apply (  simp (no_asm_simp))
+apply  (assumption)
+apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI simp add: wf_mdecl_def)
+done
+
+lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, COMP swap_prems_rl]
+
 end
diff -r a70b796d9af8 -r a50365d21144 src/HOL/MicroJava/ROOT.ML
--- a/src/HOL/MicroJava/ROOT.ML	Thu Feb 01 20:51:48 2001 +0100
+++ b/src/HOL/MicroJava/ROOT.ML	Thu Feb 01 20:53:13 2001 +0100
@@ -1,9 +1,6 @@
 
 goals_limit := 1;
 
-Unify.search_bound := 40;
-Unify.trace_bound  := 40;
-
 add_path "J";
 add_path "JVM";
 add_path "BV";