# HG changeset patch
# User oheimb
# Date 979835936 -3600
# Node ID 5ffe7ed8899ad529661da4d2113c49ae82a168a4
# Parent  92305ae9f460b9e5963bd7aee89430910159ec0a
is_class and class now as defs (rather than translations); corrected Digest.thy

diff -r 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Jan 18 17:38:56 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,27 +48,27 @@
 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 *)
+(* ### 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"
+  "[| 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 C:  "(C,S,fs,mdecls) \\<in> set G"
 
-  assume m: "(sig,rT,code) \<in> set mdecls"
+  assume m: "(sig,rT,code) \\<in> set mdecls"
   moreover
   from wf
   have "class G Object = Some (arbitrary, [], [])"
@@ -76,25 +76,25 @@
   moreover
   from wf C
   have c: "class G C = Some (S,fs,mdecls)"
-    by (auto simp add: wf_prog_def intro: map_of_SomeI)
+    by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
   ultimately
-  have O: "C \<noteq> Object"
+  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)"
+  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)"
+  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 dest: method_rec [of _ _ C])
+    by (auto simp add: is_class_def dest: method_rec [of _ _ C])
 qed
 
 
diff -r 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/BV/JType.thy
--- a/src/HOL/MicroJava/BV/JType.thy	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy	Thu Jan 18 17:38:56 2001 +0100
@@ -21,7 +21,7 @@
                                     | ClassT D => OK (Class (some_lub ((subcls1 G)^* ) C D)))))"
 
   subtype :: "'c prog => ty => ty => bool"
-  "subtype G T1 T2 == G \<turnstile> T1 \<preceq> T2"
+  "subtype G T1 T2 == G \\<turnstile> T1 \\<preceq> T2"
 
   is_ty :: "'c prog => ty => bool"
   "is_ty G T == case T of PrimT P => True | RefT R =>
@@ -34,10 +34,10 @@
   esl :: "'c prog => ty esl"
   "esl G == (types G, subtype G, sup G)"
 
-lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
+lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)"
   by (auto elim: widen.elims)
 
-lemma PrimT_PrimT2: "(G \<turnstile> PrimT p \<preceq> xb) = (xb = PrimT p)"
+lemma PrimT_PrimT2: "(G \\<turnstile> PrimT p \\<preceq> xb) = (xb = PrimT p)"
   by (auto elim: widen.elims)
 
 lemma is_tyI:
@@ -62,11 +62,11 @@
   next
     fix R assume R: "T = RefT R"
     with wf
-    have "R = ClassT Object \<Longrightarrow> ?thesis" by simp
+    have "R = ClassT Object \\<Longrightarrow> ?thesis" by simp
     moreover    
     from R wf ty
-    have "R \<noteq> ClassT Object \<Longrightarrow> ?thesis"
-      by (auto simp add: is_ty_def subcls1_def 
+    have "R \\<noteq> ClassT Object \\<Longrightarrow> ?thesis"
+      by (auto simp add: is_ty_def subcls1_def is_class_def
                elim: converse_rtranclE
                split: ref_ty.splits)    
     ultimately    
@@ -163,7 +163,7 @@
 lemma sup_subtype_greater:
   "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
       is_type G t1; is_type G t2; sup G t1 t2 = OK s |] 
-  ==> subtype G t1 s \<and> subtype G t2 s"
+  ==> subtype G t1 s \\<and> subtype G t2 s"
 proof -
   assume wf_prog:       "wf_prog wf_mb G"
   assume single_valued: "single_valued (subcls1 G)" 
@@ -173,16 +173,16 @@
     assume is_class: "is_class G c1" "is_class G c2"
     with wf_prog 
     obtain 
-      "G \<turnstile> c1 \<preceq>C Object"
-      "G \<turnstile> c2 \<preceq>C Object"
+      "G \\<turnstile> c1 \\<preceq>C Object"
+      "G \\<turnstile> c2 \\<preceq>C Object"
       by (blast intro: subcls_C_Object)
     with wf_prog single_valued
     obtain u where
       "is_lub ((subcls1 G)^* ) c1 c2 u"      
       by (blast dest: single_valued_has_lubs)
     with acyclic
-    have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2 \<and>
-          G \<turnstile> c2 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
+    have "G \\<turnstile> c1 \\<preceq>C some_lub ((subcls1 G)^* ) c1 c2 \\<and>
+          G \\<turnstile> c2 \\<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
       by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
   } note this [simp]
       
@@ -206,11 +206,11 @@
 
   { fix c1 c2 D
     assume is_class: "is_class G c1" "is_class G c2"
-    assume le: "G \<turnstile> c1 \<preceq>C D" "G \<turnstile> c2 \<preceq>C D"
+    assume le: "G \\<turnstile> c1 \\<preceq>C D" "G \\<turnstile> c2 \\<preceq>C D"
     from wf_prog is_class
     obtain 
-      "G \<turnstile> c1 \<preceq>C Object"
-      "G \<turnstile> c2 \<preceq>C Object"
+      "G \\<turnstile> c1 \\<preceq>C Object"
+      "G \\<turnstile> c2 \\<preceq>C Object"
       by (blast intro: subcls_C_Object)
     with wf_prog single_valued
     obtain u where
@@ -221,15 +221,15 @@
       by (rule some_lub_conv)
     moreover
     from lub le
-    have "G \<turnstile> u \<preceq>C D" 
+    have "G \\<turnstile> u \\<preceq>C D" 
       by (simp add: is_lub_def is_ub_def)
     ultimately     
-    have "G \<turnstile> some_lub ((subcls1 G)\<^sup>*) c1 c2 \<preceq>C D"
+    have "G \\<turnstile> some_lub ((subcls1 G)\<^sup>*) c1 c2 \\<preceq>C D"
       by blast
   } note this [intro]
 
   have [dest!]:
-    "!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
+    "!!C T. G \\<turnstile> Class C \\<preceq> T ==> \\<exists>D. T=Class D \\<and> G \\<turnstile> C \\<preceq>C D"
     by (frule widen_Class, auto)
 
   assume "is_type G a" "is_type G b" "is_type G c"
@@ -262,16 +262,16 @@
 
   from wf_prog single_valued acyclic 
   have
-    "(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \<and> 
-     (\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
+    "(\\<forall>x\\<in>err (types G). \\<forall>y\\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \\<and> 
+     (\\<forall>x\\<in>err (types G). \\<forall>y\\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
     by (auto simp add: lesub_def plussub_def le_def lift2_def sup_subtype_greater split: err.split)
 
   moreover    
 
   from wf_prog single_valued acyclic 
   have
-    "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G). 
-    x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
+    "\\<forall>x\\<in>err (types G). \\<forall>y\\<in>err (types G). \\<forall>z\\<in>err (types G). 
+    x <=_(le (subtype G)) z \\<and> y <=_(le (subtype G)) z \\<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
     by (unfold lift2_def plussub_def lesub_def le_def)
        (auto intro: sup_subtype_smallest sup_exists split: err.split)
 
diff -r 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/Digest.thy
--- a/src/HOL/MicroJava/Digest.thy	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/Digest.thy	Thu Jan 18 17:38:56 2001 +0100
@@ -41,22 +41,15 @@
 @{thm [display] Store_correct [no_vars]}
 \medskip
 
-{\bf lemma} @{text conf_Intg_Integer}:\\
-@{thm [display] conf_Intg_Integer [no_vars]}
-\medskip
-
-{\bf lemma} @{text Bipush_correct}:\\
-@{thm [display] Bipush_correct [no_vars]}
-\medskip
+%removed {\bf lemma} {text conf_Intg_Integer}:\\
+%removed {\bf lemma} {text Bipush_correct}:\\
 
 {\bf lemma} @{text NT_subtype_conv}:\\
 @{thm [display] NT_subtype_conv [no_vars]}
 \medskip
 
-{\bf lemma} @{text Aconst_null_correct}:\\
-@{thm [display] Aconst_null_correct [no_vars]}
-\medskip
-
+%removed {\bf lemma} {text Aconst_null_correct}:\\
+  
 {\bf lemma} @{text Cast_conf2}:\\
 @{thm [display] Cast_conf2 [no_vars]}
 \medskip
@@ -153,17 +146,11 @@
 
 subsubsection {* Theory Conform *}
 text {*
-{\bf theorem} @{text conf_VoidI}:\\
-@{thm [display] conf_VoidI [no_vars]}
-\medskip
+%removed {\bf theorem} {text conf_VoidI}:\\
+  
+%removed {\bf theorem} {text conf_BooleanI}:\\
 
-{\bf theorem} @{text conf_BooleanI}:\\
-@{thm [display] conf_BooleanI [no_vars]}
-\medskip
-
-{\bf theorem} @{text conf_IntegerI}:\\
-@{thm [display] conf_IntegerI [no_vars]}
-\medskip
+%removed {\bf theorem} {text conf_IntegerI}:\\
 
 {\bf theorem} @{text defval_conf}:\\
 @{thm [display] defval_conf [no_vars]}
@@ -237,54 +224,30 @@
 @{thm [display] not_Some_eq [no_vars]}
 \medskip
 
-{\bf lemma} @{text lift_top_refl}:\\
-@{thm [display] lift_top_refl [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_top_refl}:\\
 
-{\bf lemma} @{text lift_top_trans}:\\
-@{thm [display] lift_top_trans [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_top_trans}:\\
 
-{\bf lemma} @{text lift_top_Err_any}:\\
-@{thm [display] lift_top_Err_any [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_top_Err_any}:\\
 
-{\bf lemma} @{text lift_top_OK_OK}:\\
-@{thm [display] lift_top_OK_OK [no_vars]}
-\medskip
-
-{\bf lemma} @{text lift_top_any_OK}:\\
-@{thm [display] lift_top_any_OK [no_vars]}
-\medskip
-
-{\bf lemma} @{text lift_top_OK_any}:\\
-@{thm [display] lift_top_OK_any [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_top_OK_OK}:\\
+  
+%removed {\bf lemma} @{text lift_top_any_OK}:\\
+  
+%removed {\bf lemma} @{text lift_top_OK_any}:\\
 
-{\bf lemma} @{text lift_bottom_refl}:\\
-@{thm [display] lift_bottom_refl [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_refl}:\\
 
-{\bf lemma} @{text lift_bottom_trans}:\\
-@{thm [display] lift_bottom_trans [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_trans}:\\
 
-{\bf lemma} @{text lift_bottom_any_None}:\\
-@{thm [display] lift_bottom_any_None [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_any_None}:\\
 
-{\bf lemma} @{text lift_bottom_Some_Some}:\\
-@{thm [display] lift_bottom_Some_Some [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_Some_Some}:\\
 
-{\bf lemma} @{text lift_bottom_any_Some}:\\
-@{thm [display] lift_bottom_any_Some [no_vars]}
-\medskip
+%removed {\bf lemma} @{text lift_bottom_any_Some}:\\
 
-{\bf lemma} @{text lift_bottom_Some_any}:\\
-@{thm [display] lift_bottom_Some_any [no_vars]}
-\medskip
-
+%removed {\bf lemma} @{text lift_bottom_Some_any}:\\
+  
 {\bf theorem} @{text sup_ty_opt_refl}:\\
 @{thm [display] sup_ty_opt_refl [no_vars]}
 \medskip
@@ -683,14 +646,10 @@
 
 subsubsection {* Theory JBasis *}
 text {*
-{\bf theorem} @{text image_rev}:\\
-@{thm [display] image_rev [no_vars]}
-\medskip
-
-{\bf theorem} @{text some_subset_the}:\\
-@{thm [display] some_subset_the [no_vars]}
-\medskip
-
+%removed {\bf theorem} {text image_rev}:\\
+  
+%removed {\bf theorem} {text some_subset_the}:\\
+  
 {\bf theorem} @{text fst_in_set_lemma}:\\
 @{thm [display] fst_in_set_lemma [no_vars]}
 \medskip
@@ -711,18 +670,14 @@
 @{thm [display] unique_map_inj [no_vars]}
 \medskip
 
-{\bf theorem} @{text unique_map_Pair}:\\
-@{thm [display] unique_map_Pair [no_vars]}
-\medskip
-
+%removed {\bf theorem} {text unique_map_Pair}:\\
+  
 {\bf theorem} @{text image_cong}:\\
 @{thm [display] image_cong [no_vars]}
 \medskip
 
-{\bf theorem} @{text unique_map_of_Some_conv}:\\
-@{thm [display] unique_map_of_Some_conv [no_vars]}
-\medskip
-
+%removed {\bf theorem} {text unique_map_of_Some_conv}:\\
+  
 {\bf theorem} @{text Ball_set_table}:\\
 @{thm [display] Ball_set_table [no_vars]}
 \medskip
@@ -859,15 +814,10 @@
 @{thm [display] wtl_method_complete [no_vars]}
 \medskip
 
-{\bf lemma} @{text unique_set}:\\
-@{thm [display] unique_set [no_vars]}
-\medskip
+%removed {\bf lemma} {text unique_set}:\\
 
-{\bf lemma} @{text unique_epsilon}:\\
-@{thm [display] unique_epsilon [no_vars]}
-\medskip
+%removed {\bf lemma} {text unique_epsilon}:\\
 
-{\bf theorem} @{text wtl_complete}:\\
 @{thm [display] wtl_complete [no_vars]}
 \medskip
 
@@ -915,14 +865,6 @@
 @{thm [display] wtl_method_correct [no_vars]}
 \medskip
 
-{\bf lemma} @{text unique_set}:\\
-@{thm [display] unique_set [no_vars]}
-\medskip
-
-{\bf lemma} @{text unique_epsilon}:\\
-@{thm [display] unique_epsilon [no_vars]}
-\medskip
-
 {\bf theorem} @{text wtl_correct}:\\
 @{thm [display] wtl_correct [no_vars]}
 \medskip
@@ -995,13 +937,9 @@
 @{thm [display] appStore [no_vars]}
 \medskip
 
-{\bf lemma} @{text appBipush}:\\
-@{thm [display] appBipush [no_vars]}
-\medskip
+%removed {\bf lemma} {text appBipush}:\\
 
-{\bf lemma} @{text appAconst}:\\
-@{thm [display] appAconst [no_vars]}
-\medskip
+%removed {\bf lemma} {text appAconst}:\\
 
 {\bf lemma} @{text appGetField}:\\
 @{thm [display] appGetField [no_vars]}
@@ -1107,10 +1045,7 @@
 
 subsubsection {* Theory Store *}
 text {*
-{\bf theorem} @{text newref_None}:\\
-@{thm [display] newref_None [no_vars]}
-\medskip
-
+%removed {\bf theorem} {text newref_None}:\\
 *}
 
 subsubsection {* Theory Term *}
@@ -1230,9 +1165,7 @@
 @{thm [display] unique_fields [no_vars]}
 \medskip
 
-{\bf theorem} @{text widen_fields_mono}:\\
-@{thm [display] widen_fields_mono [no_vars]}
-\medskip
+%removed {\bf theorem} {text widen_fields_mono}:\\
 
 {\bf theorem} @{text widen_cfs_fields}:\\
 @{thm [display] widen_cfs_fields [no_vars]}
@@ -1254,9 +1187,7 @@
 @{thm [display] method_in_md [no_vars]}
 \medskip
 
-{\bf theorem} @{text is_type_fields}:\\
-@{thm [display] is_type_fields [no_vars]}
-\medskip
+%removed {\bf theorem} {text is_type_fields}:\\
 
 *}
 
diff -r 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/J/Decl.ML
--- a/src/HOL/MicroJava/J/Decl.ML	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.ML	Thu Jan 18 17:38:56 2001 +0100
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-Goal "finite {C. is_class G C}";
+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 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Thu Jan 18 17:38:56 2001 +0100
@@ -46,15 +46,12 @@
   "cdecl c" <= (type) "cname \\<times> (c class)"
   "prog  c" <= (type) "(c cdecl) list"
 
-consts
+constdefs
 
   class		:: "'c prog => (cname \\<leadsto> 'c class)"
+  "class        \\<equiv> map_of"
   is_class	:: "'c prog => cname => bool"
-
-translations
-
-  "class"        => "map_of"
-  "is_class G C" == "class G C \\<noteq> None"
+ "is_class G C  \\<equiv> class G C \\<noteq> None"
 
 consts
 
diff -r 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/J/Example.ML
--- a/src/HOL/MicroJava/J/Example.ML	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.ML	Thu Jan 18 17:38:56 2001 +0100
@@ -13,17 +13,19 @@
 Delsimps[map_of_Cons]; (* sic! *)
 Addsimps[map_of_Cons1, map_of_Cons2];
 
-Goalw [ObjectC_def] "class tprg Object = Some (arbitrary, [], [])";
+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 tprg Base = Some (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 tprg Ext = Some (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);
@@ -49,7 +51,8 @@
 qed "not_Base_subcls_Ext";
 AddSEs [not_Base_subcls_Ext];
 
-Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=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";
 
@@ -99,6 +102,8 @@
 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;
diff -r 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Thu Jan 18 17:38:56 2001 +0100
@@ -61,7 +61,7 @@
 by(  SELECT_GOAL Auto_tac 1);
 by( Clarify_tac 1);
 by( Full_simp_tac 1);
-by( EVERY [forward_tac [hext_objD] 1, atac 1]);
+by( EVERY [ftac hext_objD 1, atac 1]);
 by( etac exE 1);
 by( Asm_full_simp_tac 1);
 by( Clarify_tac 1);
@@ -102,12 +102,6 @@
 by( (etac conf_list_gext_widen THEN_ALL_NEW atac) 1);
 qed "Call_lemma2";
 
-Goal "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> is_class G D \\<longrightarrow> is_class G C";
-by (etac rtrancl_induct 1);
-by  (dtac subcls1D 2);
-by  Auto_tac;
-qed_spec_mp "subcls_is_class2"; 
-
 Goalw [wf_java_prog_def]
  "[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); class G C = Some y; \
 \    max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
@@ -125,7 +119,7 @@
 by( datac non_np_objD' 2 1);
 by(  Clarsimp_tac 1);
 by( Clarsimp_tac 1);
-by( EVERY'[forward_tac [hext_objD], atac] 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);
@@ -276,7 +270,7 @@
 by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
 
 by prune_params_tac;
-(* Level 50 *)
+(* Level 52 *)
 
 (* 1 Call *)
 by( case_tac "x" 1);
@@ -298,6 +292,8 @@
 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";
diff -r 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Thu Jan 18 17:38:56 2001 +0100
@@ -12,7 +12,7 @@
 by Auto_tac;
 qed "subcls1I";
 
-Goalw [subcls1_def]  
+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";
@@ -25,12 +25,12 @@
 qed "finite_subcls1";
 
 
-Goal "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
+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";
 
-Goal "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> is_class G D \\<longrightarrow> is_class G C";
+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;
diff -r 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/J/WellForm.ML
--- a/src/HOL/MicroJava/J/WellForm.ML	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.ML	Thu Jan 18 17:38:56 2001 +0100
@@ -4,19 +4,19 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-Goalw [wf_prog_def]
+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]
+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];
 
-Goal "wf_prog wf_mb G ==> is_class G 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];
@@ -68,7 +68,7 @@
 by(Auto_tac);
 qed "subcls_induct";
 
-val prems = goal thy "[|is_class G C; wf_prog wf_mb G; P Object; \
+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";
@@ -83,14 +83,15 @@
 by( case_tac "C = Object" 1);
 by(  Fast_tac 1);
 by Safe_tac;
-by( forward_tac [class_wf] 1);
+by( ftac class_wf 1);
 by(  atac 1);
-by( forward_tac [wf_cdecl_supD] 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";
 
diff -r 92305ae9f460 -r 5ffe7ed8899a src/HOL/MicroJava/J/WellType.ML
--- a/src/HOL/MicroJava/J/WellType.ML	Tue Jan 16 21:54:43 2001 +0100
+++ b/src/HOL/MicroJava/J/WellType.ML	Thu Jan 18 17:38:56 2001 +0100
@@ -19,9 +19,11 @@
 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";