improved superclass entry for classes and definition status of is_class, class
authoroheimb
Wed Dec 06 19:10:36 2000 +0100 (2000-12-06)
changeset 1061378b1d6c3ee9c
parent 10612 779af7c58743
child 10614 d5c14e205c24
improved superclass entry for classes and definition status of is_class, class
corrected recursive definitions of "method" and "fields"
cleanup of many proofs, removed superfluous tactics and theorems
src/HOL/MicroJava/J/Conform.ML
src/HOL/MicroJava/J/Decl.ML
src/HOL/MicroJava/J/Decl.thy
src/HOL/MicroJava/J/Eval.ML
src/HOL/MicroJava/J/Example.ML
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JBasis.ML
src/HOL/MicroJava/J/JTypeSafe.ML
src/HOL/MicroJava/J/State.ML
src/HOL/MicroJava/J/TypeRel.ML
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellForm.ML
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.ML
src/HOL/MicroJava/J/WellType.thy
     1.1 --- a/src/HOL/MicroJava/J/Conform.ML	Wed Dec 06 19:09:34 2000 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Conform.ML	Wed Dec 06 19:10:36 2000 +0100
     1.3 @@ -6,71 +6,59 @@
     1.4  
     1.5  section "hext";
     1.6  
     1.7 -val hextI = prove_goalw thy [hext_def] "!!h. \
     1.8 -\ \\<forall>a C fs . h  a = Some (C,fs) -->  \
     1.9 -\     (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'" (K [Auto_tac ]);
    1.10 +Goalw [hext_def] 
    1.11 +" \\<forall>a C fs . h  a = Some (C,fs) -->  \
    1.12 +\     (\\<exists>fs'. h' a = Some (C,fs')) ==> h\\<le>|h'"; 
    1.13 +by Auto_tac;
    1.14 +qed "hextI";
    1.15  
    1.16 -val hext_objD = prove_goalw thy [hext_def] 
    1.17 -"!!h. [|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')" 
    1.18 -	(K [Force_tac 1]);
    1.19 +Goalw [hext_def] "[|h\\<le>|h'; h a = Some (C,fs) |] ==> \\<exists>fs'. h' a = Some (C,fs')";
    1.20 +by (Force_tac 1);
    1.21 +qed "hext_objD";
    1.22  
    1.23 -val hext_refl = prove_goal thy "h\\<le>|h" (K [
    1.24 -	rtac hextI 1,
    1.25 -	Fast_tac 1]);
    1.26 +Goal "h\\<le>|h";
    1.27 +by (rtac hextI 1);
    1.28 +by (Fast_tac 1);
    1.29 +qed "hext_refl";
    1.30  
    1.31 -val hext_new = prove_goal thy "!!h. h a = None ==> h\\<le>|h(a\\<mapsto>x)" (K [
    1.32 -	rtac hextI 1,
    1.33 -	safe_tac HOL_cs,
    1.34 -	 ALLGOALS (case_tac "aa = a"),
    1.35 -	   Auto_tac]);
    1.36 +Goal "h a = None ==> h\\<le>|h(a\\<mapsto>x)";
    1.37 +by (rtac hextI 1);
    1.38 +by Auto_tac;
    1.39 +qed "hext_new";
    1.40  
    1.41 -val hext_trans = prove_goal thy "!!h. [|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''" (K [
    1.42 -	rtac hextI 1,
    1.43 -	safe_tac HOL_cs,
    1.44 -	 fast_tac (HOL_cs addDs [hext_objD]) 1]);
    1.45 +Goal "[|h\\<le>|h'; h'\\<le>|h''|] ==> h\\<le>|h''";
    1.46 +by (rtac hextI 1);
    1.47 +by (fast_tac (HOL_cs addDs [hext_objD]) 1);
    1.48 +qed "hext_trans";
    1.49  
    1.50  Addsimps [hext_refl, hext_new];
    1.51  
    1.52 -val hext_upd_obj = prove_goal thy 
    1.53 -"!!h. h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
    1.54 -	rtac hextI 1,
    1.55 -	safe_tac HOL_cs,
    1.56 -	 ALLGOALS (case_tac "aa = a"),
    1.57 -	   Auto_tac]);
    1.58 +Goal "h a = Some (C,fs) ==> h\\<le>|h(a\\<mapsto>(C,fs'))";
    1.59 +by (rtac hextI 1);
    1.60 +by Auto_tac;
    1.61 +qed "hext_upd_obj";
    1.62  
    1.63  
    1.64  section "conf";
    1.65  
    1.66 -val conf_Null = prove_goalw thy [conf_def] 
    1.67 -"G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
    1.68 +Goalw [conf_def] "G,h\\<turnstile>Null::\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T"; 
    1.69 +by (Simp_tac 1);
    1.70 +qed "conf_Null";
    1.71  Addsimps [conf_Null];
    1.72  
    1.73 -val conf_litval = prove_goalw thy [conf_def] 
    1.74 -"typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T" (K [
    1.75 -	rtac val_.induct 1,
    1.76 -	    Auto_tac]) RS mp;
    1.77 -
    1.78 -Goalw [conf_def] "G,s\\<turnstile>Unit::\\<preceq>PrimT Void";
    1.79 -by( Simp_tac 1);
    1.80 -qed "conf_VoidI";
    1.81 -
    1.82 -Goalw [conf_def] "G,s\\<turnstile>Bool b::\\<preceq>PrimT Boolean";
    1.83 -by( Simp_tac 1);
    1.84 -qed "conf_BooleanI";
    1.85 +Goalw [conf_def] "typeof (\\<lambda>v. None) v = Some T --> G,h\\<turnstile>v::\\<preceq>T";
    1.86 +by (rtac val_.induct 1);
    1.87 +by Auto_tac;
    1.88 +qed_spec_mp "conf_litval";
    1.89 +Addsimps[conf_litval];
    1.90  
    1.91 -Goalw [conf_def] "G,s\\<turnstile>Intg i::\\<preceq>PrimT Integer";
    1.92 -by( Simp_tac 1);
    1.93 -qed "conf_IntegerI";
    1.94 -
    1.95 -Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
    1.96 +Goalw [conf_def] "[|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T";
    1.97 +by (Asm_full_simp_tac 1);
    1.98 +qed "conf_AddrI";
    1.99  
   1.100 -val conf_AddrI = prove_goalw thy [conf_def] 
   1.101 -"!!G. [|h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T|] ==> G,h\\<turnstile>Addr a::\\<preceq>T"
   1.102 -(K [Asm_full_simp_tac 1]);
   1.103 -
   1.104 -val conf_obj_AddrI = prove_goalw thy [conf_def]
   1.105 - "!!G. [|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D" 
   1.106 -(K [Asm_full_simp_tac 1]);
   1.107 +Goalw [conf_def] "[|h a = Some (C,fs); G\\<turnstile>C\\<preceq>C D|] ==> G,h\\<turnstile>Addr a::\\<preceq> Class D"; 
   1.108 +by (Asm_full_simp_tac 1);
   1.109 +qed "conf_obj_AddrI";
   1.110  
   1.111  Goalw [conf_def] "is_type G T --> G,h\\<turnstile>default_val T::\\<preceq>T";
   1.112  by (res_inst_tac [("y","T")] ty.exhaust 1);
   1.113 @@ -79,39 +67,25 @@
   1.114  by    (auto_tac (claset(), simpset() addsimps [widen.null]));
   1.115  qed_spec_mp "defval_conf";
   1.116  
   1.117 -val conf_upd_obj = prove_goalw thy [conf_def] 
   1.118 -"h a = Some (C,fs) --> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)" (fn _ => [
   1.119 -	rtac impI 1,
   1.120 -	rtac val_.induct 1,
   1.121 -	 ALLGOALS Simp_tac,
   1.122 -	case_tac "loc = a" 1,
   1.123 -	 ALLGOALS Asm_simp_tac]) RS mp;
   1.124 -
   1.125 -val conf_widen = prove_goalw thy [conf_def] 
   1.126 -"!!G. wf_prog wf_mb G ==> G,h\\<turnstile>x::\\<preceq>T --> G\\<turnstile>T\\<preceq>T' --> G,h\\<turnstile>x::\\<preceq>T'" (K [
   1.127 -	rtac val_.induct 1,
   1.128 -	    ALLGOALS Simp_tac,
   1.129 -	    ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
   1.130 -bind_thm ("conf_widen", conf_widen);
   1.131 +Goalw [conf_def] 
   1.132 +"h a = Some (C,fs) ==> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x::\\<preceq>T) = (G,h\\<turnstile>x::\\<preceq>T)";
   1.133 +by (rtac val_.induct 1);
   1.134 +by Auto_tac;
   1.135 +qed "conf_upd_obj";
   1.136  
   1.137 -val conf_hext' = prove_goalw thy [conf_def] 
   1.138 -	"!!h. h\\<le>|h' ==> (\\<forall>v T. G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T)" (K [
   1.139 -	REPEAT (rtac allI 1),
   1.140 -	rtac val_.induct 1,
   1.141 -	 ALLGOALS Simp_tac,
   1.142 -	safe_tac (HOL_cs addSDs [option_map_SomeD]),
   1.143 -	rewtac option_map_def,
   1.144 -	  dtac hext_objD 1,
   1.145 -	   Auto_tac]);
   1.146 -val conf_hext = conf_hext' RS spec RS spec RS mp;
   1.147 -bind_thm ("conf_hext", conf_hext);
   1.148 +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'";
   1.149 +by (rtac val_.induct 1);
   1.150 +by (auto_tac (claset() addIs [widen_trans], simpset()));
   1.151 +qed_spec_mp "conf_widen";
   1.152  
   1.153 -val new_locD = prove_goalw thy [conf_def] 
   1.154 -	"[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a" (fn prems => [
   1.155 -	cut_facts_tac prems 1,
   1.156 -	Full_simp_tac 1,
   1.157 -	safe_tac HOL_cs,
   1.158 -	Asm_full_simp_tac 1]);
   1.159 +Goalw [conf_def] "h\\<le>|h' ==> G,h\\<turnstile>v::\\<preceq>T --> G,h'\\<turnstile>v::\\<preceq>T";
   1.160 +by (rtac val_.induct 1);
   1.161 +by (auto_tac (claset() addDs [hext_objD], simpset()));
   1.162 +qed_spec_mp "conf_hext";
   1.163 +
   1.164 +Goalw [conf_def] "[|h a = None; G,h\\<turnstile>Addr t::\\<preceq>T|] ==> t\\<noteq>a";
   1.165 +by Auto_tac;
   1.166 +qed "new_locD";
   1.167  
   1.168  Goalw [conf_def]
   1.169   "G,h\\<turnstile>a'::\\<preceq>RefT T --> a' = Null |  \
   1.170 @@ -120,34 +94,28 @@
   1.171  by(Auto_tac);
   1.172  qed_spec_mp "conf_RefTD";
   1.173  
   1.174 -val conf_NullTD = prove_goal thy "!!G. G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null" (K [
   1.175 -	dtac conf_RefTD 1,
   1.176 -	Step_tac 1,
   1.177 -	 Auto_tac]);
   1.178 +Goal "G,h\\<turnstile>a'::\\<preceq>RefT NullT ==> a' = Null";
   1.179 +by (dtac conf_RefTD 1);
   1.180 +by Auto_tac;
   1.181 +qed "conf_NullTD";
   1.182  
   1.183 -val non_npD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
   1.184 -\ \\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t" (K [
   1.185 -	dtac conf_RefTD 1,
   1.186 -	Step_tac 1,
   1.187 -	 Auto_tac]);
   1.188 +Goal "[|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq>RefT t|] ==> \
   1.189 +\ \\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t";
   1.190 +by (dtac conf_RefTD 1);
   1.191 +by Auto_tac;
   1.192 +qed "non_npD";
   1.193  
   1.194 -val non_np_objD = prove_goal thy "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
   1.195 -\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>C'\\<preceq>C C)" 
   1.196 -	(K[fast_tac (claset() addDs [non_npD]) 1]);
   1.197 +Goal "!!G. [|a' \\<noteq> Null; G,h\\<turnstile>a'::\\<preceq> Class C; C \\<noteq> Object|] ==> \
   1.198 +\ (\\<exists>a C' fs. a' = Addr a \\<and>  h a = Some (C',fs) \\<and>  G\\<turnstile>C'\\<preceq>C C)";
   1.199 +by (fast_tac (claset() addDs [non_npD]) 1);
   1.200 +qed "non_np_objD";
   1.201  
   1.202 -Goal "a' \\<noteq> Null --> wf_prog wf_mb G --> G,h\\<turnstile>a'::\\<preceq>RefT t -->\
   1.203 +Goal "a' \\<noteq> Null ==> wf_prog wf_mb G ==> G,h\\<turnstile>a'::\\<preceq>RefT t -->\
   1.204  \ (\\<forall>C. t = ClassT C --> C \\<noteq> Object) --> \
   1.205  \ (\\<exists>a C fs. a' = Addr a \\<and>  h a = Some (C,fs) \\<and>  G\\<turnstile>Class C\\<preceq>RefT t)";
   1.206 -by(rtac impI 1);
   1.207 -by(rtac impI 1);
   1.208  by(res_inst_tac [("y","t")] ref_ty.exhaust 1);
   1.209 - by(Safe_tac);
   1.210 - by(dtac conf_NullTD 1);
   1.211 - by(contr_tac 1);
   1.212 -by(dtac non_np_objD 1);
   1.213 -  by(atac 1);
   1.214 - by(Fast_tac 1);
   1.215 -by(Fast_tac 1);
   1.216 + by (fast_tac (claset() addDs [conf_NullTD]) 1);
   1.217 +by (fast_tac (claset() addDs [non_np_objD]) 1);
   1.218  qed_spec_mp "non_np_objD'";
   1.219  
   1.220  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'";
   1.221 @@ -165,20 +133,18 @@
   1.222  
   1.223  section "lconf";
   1.224  
   1.225 -val lconfD = prove_goalw thy [lconf_def] 
   1.226 -   "!!X. [| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T"
   1.227 - (K [Force_tac 1]);
   1.228 +Goalw[lconf_def] "[| G,h\\<turnstile>vs[::\\<preceq>]Ts; Ts n = Some T |] ==> G,h\\<turnstile>(the (vs n))::\\<preceq>T";
   1.229 +by (Force_tac 1);
   1.230 +qed "lconfD";
   1.231  
   1.232 -val lconf_hext = prove_goalw thy [lconf_def] 
   1.233 -	"!!X. [| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L" (K [
   1.234 -		fast_tac (claset() addEs [conf_hext]) 1]);
   1.235 +Goalw [lconf_def] "[| G,h\\<turnstile>l[::\\<preceq>]L; h\\<le>|h' |] ==> G,h'\\<turnstile>l[::\\<preceq>]L";
   1.236 +by  (fast_tac (claset() addEs [conf_hext]) 1);
   1.237 +qed "lconf_hext";
   1.238  AddEs [lconf_hext];
   1.239  
   1.240  Goalw [lconf_def] "!!X. [| G,h\\<turnstile>l[::\\<preceq>]lT; \
   1.241  \ G,h\\<turnstile>v::\\<preceq>T; lT va = Some T |] ==> G,h\\<turnstile>l(va\\<mapsto>v)[::\\<preceq>]lT";
   1.242 -by( Clarify_tac 1);
   1.243 -by( case_tac "n = va" 1);
   1.244 - by Auto_tac;
   1.245 +by Auto_tac;
   1.246  qed "lconf_upd";
   1.247  
   1.248  Goal "\\<forall>x. P x --> R (dv x) x ==> (\\<forall>x. map_of fs f = Some x --> P x) --> \
   1.249 @@ -199,9 +165,9 @@
   1.250  qed "lconf_init_vars";
   1.251  AddSIs [lconf_init_vars];
   1.252  
   1.253 -val lconf_ext = prove_goalw thy [lconf_def] 
   1.254 -"!!X. [|G,s\\<turnstile>l[::\\<preceq>]L; G,s\\<turnstile>v::\\<preceq>T|] ==> G,s\\<turnstile>l(vn\\<mapsto>v)[::\\<preceq>]L(vn\\<mapsto>T)" 
   1.255 -	(K [Auto_tac]);
   1.256 +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)";
   1.257 +by Auto_tac;
   1.258 +qed "lconf_ext";
   1.259  
   1.260  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)";
   1.261  by( induct_tac "vns" 1);
   1.262 @@ -213,14 +179,15 @@
   1.263  
   1.264  section "oconf";
   1.265  
   1.266 -val oconf_hext = prove_goalw thy [oconf_def] 
   1.267 -"!!X. G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
   1.268 +Goalw [oconf_def] "G,h\\<turnstile>obj\\<surd> ==> h\\<le>|h' ==> G,h'\\<turnstile>obj\\<surd>"; 
   1.269 +by (Fast_tac 1);
   1.270 +qed "oconf_hext";
   1.271  
   1.272 -val oconf_obj = prove_goalw thy [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
   1.273 -\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and>  G,h\\<turnstile>v::\\<preceq>T))"(K [
   1.274 -	Auto_tac]);
   1.275 -
   1.276 -val oconf_objD = oconf_obj RS iffD1 RS spec RS spec RS mp;
   1.277 +Goalw [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
   1.278 +\ (\\<forall>T f. map_of(fields (G,C)) f = Some T --> (\\<exists>v. fs f = Some v \\<and>  G,h\\<turnstile>v::\\<preceq>T))";
   1.279 +by Auto_tac;
   1.280 +qed "oconf_obj";
   1.281 +bind_thm ("oconf_objD", oconf_obj RS iffD1 RS spec RS spec RS mp);
   1.282  
   1.283  
   1.284  section "hconf";
   1.285 @@ -236,19 +203,17 @@
   1.286  
   1.287  section "conforms";
   1.288  
   1.289 -val conforms_heapD = prove_goalw thy [conforms_def]
   1.290 -	"(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>"
   1.291 -	(fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
   1.292 +Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G\\<turnstile>h h\\<surd>";
   1.293 +by (Asm_full_simp_tac 1);
   1.294 +qed "conforms_heapD";
   1.295  
   1.296 -val conforms_localD = prove_goalw thy [conforms_def]
   1.297 -	 "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT" (fn prems => [
   1.298 -	cut_facts_tac prems 1, Asm_full_simp_tac 1]);
   1.299 +Goalw [conforms_def] "(h, l)::\\<preceq>(G, lT) ==> G,h\\<turnstile>l[::\\<preceq>]lT";
   1.300 +by (Asm_full_simp_tac 1);
   1.301 +qed "conforms_localD";
   1.302  
   1.303 -val conformsI = prove_goalw thy [conforms_def] 
   1.304 -"[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)" (fn prems => [
   1.305 -	cut_facts_tac prems 1,
   1.306 -	Simp_tac 1,
   1.307 -	Auto_tac]);
   1.308 +Goalw [conforms_def] "[|G\\<turnstile>h h\\<surd>; G,h\\<turnstile>l[::\\<preceq>]lT|] ==> (h, l)::\\<preceq>(G, lT)"; 
   1.309 +by Auto_tac;
   1.310 +qed "conformsI";
   1.311  
   1.312  Goal "[|(h,l)::\\<preceq>(G,lT); h\\<le>|h'; G\\<turnstile>h h'\\<surd> |] ==> (h',l)::\\<preceq>(G,lT)";
   1.313  by( fast_tac (HOL_cs addDs [conforms_localD] 
     2.1 --- a/src/HOL/MicroJava/J/Decl.ML	Wed Dec 06 19:09:34 2000 +0100
     2.2 +++ b/src/HOL/MicroJava/J/Decl.ML	Wed Dec 06 19:10:36 2000 +0100
     2.3 @@ -4,12 +4,8 @@
     2.4      Copyright   1999 Technische Universitaet Muenchen
     2.5  *)
     2.6  
     2.7 -val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
     2.8 -	rtac finite_map_of 1]);
     2.9 +Goal "finite {C. is_class G C}";
    2.10 +by (fold_goals_tac [dom_def]);
    2.11 +by (rtac finite_dom_map_of 1);
    2.12 +qed "finite_is_class";
    2.13  
    2.14 -val is_classI = prove_goalw thy [is_class_def]
    2.15 -"!!G. class G C = Some c ==> is_class G C" (K [Auto_tac]);
    2.16 -
    2.17 -val is_classD = prove_goalw thy [is_class_def]
    2.18 -"!!G. is_class G C ==> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
    2.19 -	not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
     3.1 --- a/src/HOL/MicroJava/J/Decl.thy	Wed Dec 06 19:09:34 2000 +0100
     3.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Wed Dec 06 19:10:36 2000 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4  	= "sig \\<times> ty \\<times> 'c"
     3.5  
     3.6  types	'c class		(* class *)
     3.7 -	= "cname option \\<times> fdecl list \\<times> 'c mdecl list"
     3.8 +	= "cname \\<times> fdecl list \\<times> 'c mdecl list"
     3.9  	(* superclass, fields, methods*)
    3.10  
    3.11  	'c cdecl		(* class declaration, cf. 8.1 *)
    3.12 @@ -32,23 +32,33 @@
    3.13  
    3.14  defs 
    3.15  
    3.16 - ObjectC_def "ObjectC == (Object, (None, [], []))"
    3.17 + ObjectC_def "ObjectC == (Object, (arbitrary, [], []))"
    3.18  
    3.19  
    3.20  types 'c prog = "'c cdecl list"
    3.21  
    3.22 +
    3.23 +translations
    3.24 +  "fdecl"   <= (type) "vname \\<times> ty"
    3.25 +  "sig"     <= (type) "mname \\<times> ty list"
    3.26 +  "mdecl c" <= (type) "sig \\<times> ty \\<times> c"
    3.27 +  "class c" <= (type) "cname \\<times> fdecl list \\<times> (c mdecl) list"
    3.28 +  "cdecl c" <= (type) "cname \\<times> (c class)"
    3.29 +  "prog  c" <= (type) "(c cdecl) list"
    3.30 +
    3.31  consts
    3.32  
    3.33    class		:: "'c prog => (cname \\<leadsto> 'c class)"
    3.34 +  is_class	:: "'c prog => cname => bool"
    3.35  
    3.36 -  is_class	:: "'c prog => cname => bool"
    3.37 -  is_type	:: "'c prog => ty    => bool"
    3.38 +translations
    3.39  
    3.40 -defs
    3.41 +  "class"        => "map_of"
    3.42 +  "is_class G C" == "class G C \\<noteq> None"
    3.43  
    3.44 -  class_def	"class        == map_of"
    3.45 +consts
    3.46  
    3.47 -  is_class_def	"is_class G C == class G C \\<noteq> None"
    3.48 +  is_type	:: "'c prog => ty    => bool"
    3.49  
    3.50  primrec
    3.51  "is_type G (PrimT pt) = True"
     4.1 --- a/src/HOL/MicroJava/J/Eval.ML	Wed Dec 06 19:09:34 2000 +0100
     4.2 +++ b/src/HOL/MicroJava/J/Eval.ML	Wed Dec 06 19:10:36 2000 +0100
     4.3 @@ -7,7 +7,7 @@
     4.4  Goal "[|new_Addr (heap s) = (a,x); \
     4.5  \      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> \
     4.6  \      G\\<turnstile>Norm s -NewC C\\<succ>Addr a-> s'";
     4.7 -by (hyp_subst_tac 1);
     4.8 +by (Asm_simp_tac 1);
     4.9  br eval_evals_exec.NewC 1;
    4.10  by Auto_tac;
    4.11  qed "NewCI";
    4.12 @@ -21,27 +21,32 @@
    4.13  by(ALLGOALS Asm_full_simp_tac);
    4.14  qed "eval_evals_exec_no_xcpt";
    4.15  
    4.16 -val eval_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None" (K [
    4.17 -	dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1,
    4.18 -	Fast_tac 1]);
    4.19 -val evals_no_xcpt = prove_goal thy "!!X. G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None" (K [
    4.20 -	dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1,
    4.21 -	Fast_tac 1]);
    4.22 +Goal "G\\<turnstile>(x,s) -e\\<succ>v-> (None,s') ==> x=None";
    4.23 +by (dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1);
    4.24 +by (Fast_tac 1);
    4.25 +qed "eval_no_xcpt";
    4.26  
    4.27 -val eval_evals_exec_xcpt = prove_goal thy 
    4.28 +Goal "G\\<turnstile>(x,s) -e[\\<succ>]v-> (None,s') ==> x=None";
    4.29 +by (dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1);
    4.30 +by (Fast_tac 1);
    4.31 +qed "evals_no_xcpt";
    4.32 +
    4.33 +Goal 
    4.34  "!!s s'. (G\\<turnstile>(x,s) -e \\<succ>  v -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
    4.35  \        (G\\<turnstile>(x,s) -es[\\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s) \\<and> \
    4.36 -\        (G\\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)"
    4.37 - (K [
    4.38 -	split_all_tac 1,
    4.39 -	rtac eval_evals_exec.induct 1,
    4.40 -	rewtac c_hupd_def,
    4.41 -	ALLGOALS Asm_full_simp_tac]);
    4.42 -val eval_xcpt = prove_goal thy 
    4.43 -"!!X. G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
    4.44 -	dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1,
    4.45 -	Fast_tac 1]);
    4.46 -val exec_xcpt = prove_goal thy 
    4.47 -"!!X. G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and>  s'=s" (K [
    4.48 -	dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
    4.49 -	Fast_tac 1]);
    4.50 +\        (G\\<turnstile>(x,s) -c       -> (x',s') --> x=Some xc --> x'=Some xc \\<and> s'=s)";
    4.51 +by (split_all_tac 1);
    4.52 +by (rtac eval_evals_exec.induct 1);
    4.53 +by (rewtac c_hupd_def);
    4.54 +by (ALLGOALS Asm_full_simp_tac);
    4.55 +qed "eval_evals_exec_xcpt";
    4.56 +
    4.57 +Goal "G\\<turnstile>(Some xc,s) -e\\<succ>v-> (x',s') ==> x'=Some xc \\<and>  s'=s";
    4.58 +by (dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1);
    4.59 +by (Fast_tac 1);
    4.60 +qed "eval_xcpt";  
    4.61 +
    4.62 +Goal "G\\<turnstile>(Some xc,s) -s0-> (x',s') ==> x'=Some xc \\<and>  s'=s";
    4.63 +by (dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1);
    4.64 +by (Fast_tac 1);
    4.65 +qed "exec_xcpt";
    4.66 \ No newline at end of file
     5.1 --- a/src/HOL/MicroJava/J/Example.ML	Wed Dec 06 19:09:34 2000 +0100
     5.2 +++ b/src/HOL/MicroJava/J/Example.ML	Wed Dec 06 19:10:36 2000 +0100
     5.3 @@ -1,35 +1,37 @@
     5.4 -
     5.5 -AddIs [widen.null];
     5.6  
     5.7  Addsimps [inj_cnam_, inj_vnam_];
     5.8  Addsimps [Base_not_Object,Ext_not_Object];
     5.9  Addsimps [Base_not_Object RS not_sym,Ext_not_Object RS not_sym];
    5.10  
    5.11 -val map_of_Cons = prove_goalw thy [get_def thy "map_of_list"] 
    5.12 -"map_of (p#ps) = (map_of ps)(fst p |-> snd p)" (K [Simp_tac 1]);
    5.13 -val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"] 
    5.14 -"map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]);
    5.15 -val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"] 
    5.16 -"!!X. x\\<noteq>k ==> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
    5.17 +bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps")));
    5.18 +Goal "map_of ((aa,bb)#ps) aa = Some bb";
    5.19 +by (Simp_tac 1);
    5.20 +qed "map_of_Cons1";
    5.21 +Goal "aa\\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa";
    5.22 +by (Asm_simp_tac 1);
    5.23 +qed "map_of_Cons2";
    5.24  Delsimps[map_of_Cons]; (* sic! *)
    5.25  Addsimps[map_of_Cons1, map_of_Cons2];
    5.26  
    5.27 -val class_tprg_Object = prove_goalw thy [class_def, ObjectC_def] 
    5.28 - 	"class tprg Object = Some (None, [], [])" 
    5.29 -	(K [Simp_tac 1]);
    5.30 -val class_tprg_Base = prove_goalw thy [class_def, ObjectC_def, BaseC_def, 
    5.31 - ExtC_def] "class tprg Base = Some (Some Object, \
    5.32 +Goalw [ObjectC_def] "class tprg Object = Some (arbitrary, [], [])";
    5.33 +by (Simp_tac 1);
    5.34 +qed "class_tprg_Object";
    5.35 +
    5.36 +Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg Base = Some (Object, \
    5.37  	\ [(vee, PrimT Boolean)], \
    5.38 -        \ [((foo, [Class Base]), Class Base, foo_Base)])" (K [
    5.39 -	Simp_tac 1]);
    5.40 -val class_tprg_Ext = prove_goalw thy [class_def, ObjectC_def, BaseC_def, 
    5.41 - ExtC_def] "class tprg Ext = Some (Some Base, \
    5.42 +        \ [((foo, [Class Base]), Class Base, foo_Base)])";
    5.43 +by (Simp_tac 1);
    5.44 +qed "class_tprg_Base";
    5.45 +
    5.46 +Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg Ext = Some (Base, \
    5.47  	\ [(vee, PrimT Integer)], \
    5.48 -        \ [((foo, [Class Base]), Class Ext, foo_Ext)])" (K [
    5.49 -	Simp_tac 1]);
    5.50 +        \ [((foo, [Class Base]), Class Ext, foo_Ext)])";
    5.51 +by (Simp_tac 1);
    5.52 +qed "class_tprg_Ext";
    5.53 +
    5.54  Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];
    5.55  
    5.56 -Goal "!!X. (Object,C) \\<in> (subcls1 tprg)^+ ==> R";
    5.57 +Goal "(Object,C) \\<in> (subcls1 tprg)^+ ==> R";
    5.58  by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
    5.59  qed "not_Object_subcls";
    5.60  AddSEs [not_Object_subcls];
    5.61 @@ -42,13 +44,13 @@
    5.62  qed "subcls_ObjectD";
    5.63  AddSDs[subcls_ObjectD];
    5.64  
    5.65 -Goal "!!X. (Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
    5.66 +Goal "(Base, Ext) \\<in> (subcls1 tprg)^+ ==> R";
    5.67  by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
    5.68  qed "not_Base_subcls_Ext";
    5.69  AddSEs [not_Base_subcls_Ext];
    5.70  
    5.71 -Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
    5.72 -by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm]));
    5.73 +Goalw [ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z ==> C=Object \\<or> C=Base \\<or> C=Ext";
    5.74 +by (auto_tac (claset(),simpset()addsplits[split_if_asm]addsimps[map_of_Cons]));
    5.75  qed "class_tprgD";
    5.76  
    5.77  Goal "(C,C) \\<in> (subcls1 tprg)^+ ==> R";
    5.78 @@ -66,13 +68,13 @@
    5.79  
    5.80  bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl);
    5.81  
    5.82 -Goalw [] "tprg\\<turnstile>Ext\\<preceq>C Base";
    5.83 +Goal "tprg\\<turnstile>Ext\\<preceq>C Base";
    5.84  br subcls_direct 1;
    5.85 -by (Simp_tac 1);
    5.86 +by Auto_tac;
    5.87  qed "Ext_subcls_Base";
    5.88  Addsimps [Ext_subcls_Base];
    5.89  
    5.90 -Goalw [] "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
    5.91 +Goal "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
    5.92  br widen.subcls 1;
    5.93  by (Simp_tac 1);
    5.94  qed "Ext_widen_Base";
    5.95 @@ -89,8 +91,6 @@
    5.96  val wf_subcls1_=acyclic_subcls1_ RS(finite_subcls1 RS finite_acyclic_wf_converse);
    5.97  
    5.98  
    5.99 -Addsimps[is_class_def];
   5.100 -
   5.101  val fields_rec_ = wf_subcls1_ RSN (1, fields_rec_lemma);
   5.102  
   5.103  Goal "fields (tprg, Object) = []";
     6.1 --- a/src/HOL/MicroJava/J/Example.thy	Wed Dec 06 19:09:34 2000 +0100
     6.2 +++ b/src/HOL/MicroJava/J/Example.thy	Wed Dec 06 19:10:36 2000 +0100
     6.3 @@ -75,13 +75,13 @@
     6.4  defs
     6.5  
     6.6    foo_Base_def "foo_Base == ([x],[],Skip,LAcc x)"
     6.7 -  BaseC_def "BaseC == (Base, (Some Object, 
     6.8 +  BaseC_def "BaseC == (Base, (Object, 
     6.9  			     [(vee, PrimT Boolean)], 
    6.10  			     [((foo,[Class Base]),Class Base,foo_Base)]))"
    6.11    foo_Ext_def "foo_Ext == ([x],[],Expr( {Ext}Cast Ext
    6.12  				       (LAcc x)..vee:=Lit (Intg #1)),
    6.13  				   Lit Null)"
    6.14 -  ExtC_def  "ExtC  == (Ext,  (Some Base  , 
    6.15 +  ExtC_def  "ExtC  == (Ext,  (Base  , 
    6.16  			     [(vee, PrimT Integer)], 
    6.17  			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
    6.18  
     7.1 --- a/src/HOL/MicroJava/J/JBasis.ML	Wed Dec 06 19:09:34 2000 +0100
     7.2 +++ b/src/HOL/MicroJava/J/JBasis.ML	Wed Dec 06 19:10:36 2000 +0100
     7.3 @@ -4,92 +4,21 @@
     7.4      Copyright   1999 TU Muenchen
     7.5  *)
     7.6  
     7.7 -val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE]));
     7.8 -
     7.9 -Goalw [image_def]
    7.10 -	"x \\<in> f``A ==> \\<exists>y. y \\<in> A \\<and>  x = f y";
    7.11 -by(Auto_tac);
    7.12 -qed "image_rev";
    7.13 -
    7.14 -fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
    7.15 -
    7.16 -val select_split = prove_goalw Product_Type.thy [split_def] 
    7.17 -	"(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
    7.18 -	 
    7.19 -
    7.20 -val split_beta = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
    7.21 -	(fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
    7.22 -val split_beta2 = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
    7.23 -	(fn _ => [Auto_tac]);
    7.24 -val splitE2 = prove_goal Product_Type.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [
    7.25 -	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
    7.26 -	rtac (split_beta RS subst) 1,
    7.27 -	rtac (hd prems) 1]);
    7.28 -val splitE2' = prove_goal Product_Type.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [
    7.29 -	REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
    7.30 -	res_inst_tac [("P1","P")] (split_beta RS subst) 1,
    7.31 -	rtac (hd prems) 1]);
    7.32 -	
    7.33 -
    7.34 -fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
    7.35 -
    7.36 -val BallE = prove_goal thy "[|Ball A P; x \\<notin> A ==> Q; P x ==> Q |] ==> Q"
    7.37 -	(fn prems => [rtac ballE 1, resolve_tac prems 1, 
    7.38 -			eresolve_tac prems 1, eresolve_tac prems 1]);
    7.39 -
    7.40 -val set_cs2 = set_cs delrules [ballE] addSEs [BallE];
    7.41 +(*###TO Product_Type*)
    7.42 +Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
    7.43 +by (rtac refl 1);
    7.44 +qed "select_split";
    7.45  
    7.46  Addsimps [Let_def];
    7.47  
    7.48 -(* To HOL.ML *)
    7.49 -
    7.50 -val ex1_some_eq_trivial = prove_goal HOL.thy "[| \\<exists>!x. P x; P y |] ==> Eps P = y" 
    7.51 -	(fn prems => [
    7.52 -	cut_facts_tac prems 1,
    7.53 -	rtac some_equality 1,
    7.54 -	 atac 1,
    7.55 -	etac ex1E 1,
    7.56 -	etac all_dupE 1,
    7.57 -	fast_tac HOL_cs 1]);
    7.58 -
    7.59 -
    7.60 -val ball_insert = prove_goalw equalities.thy [Ball_def]
    7.61 -	"Ball (insert x A) P = (P x \\<and> Ball A P)" (fn _ => [
    7.62 -	fast_tac set_cs 1]);
    7.63 -
    7.64 -fun option_case_tac i = EVERY [
    7.65 -	etac option_caseE i,
    7.66 -	 rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), 
    7.67 -	 rotate_tac ~2  i   , asm_full_simp_tac HOL_basic_ss i];
    7.68 -
    7.69 -val not_None_tac = EVERY' [dtac (not_None_eq RS iffD1),rotate_tac ~1,etac exE,
    7.70 -		rotate_tac ~1,asm_full_simp_tac 
    7.71 -	(simpset() delsimps [split_paired_All,split_paired_Ex])];
    7.72 -
    7.73 -Goal "{y. x = Some y} \\<subseteq> {the x}";
    7.74 -by Auto_tac;
    7.75 -qed "some_subset_the";
    7.76 -
    7.77 -fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
    7.78 -  asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
    7.79 -
    7.80 -val optionE = prove_goal thy 
    7.81 -       "[| opt = None ==> P;  !!x. opt = Some x ==> P |] ==> P" 
    7.82 -   (fn prems => [
    7.83 -	case_tac "opt = None" 1,
    7.84 -	 eresolve_tac prems 1,
    7.85 -	not_None_tac 1,
    7.86 -	eresolve_tac prems 1]);
    7.87 -
    7.88 -fun option_case_tac2 s i = EVERY [
    7.89 -	 case_tac s i,
    7.90 -	 rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), 
    7.91 -	 rotate_tac ~1  i   , asm_full_simp_tac HOL_basic_ss i];
    7.92 -
    7.93 -val option_map_SomeD = prove_goalw thy [option_map_def]
    7.94 -	"!!x. option_map f x = Some y ==> \\<exists>z. x = Some z \\<and> f z = y" (K [
    7.95 -	option_case_tac2 "x" 1,
    7.96 -	 Auto_tac]);
    7.97 +(* ### To HOL.ML *)
    7.98 +Goal "[| ?!x. P x; P y |] ==> Eps P = y"; 
    7.99 +by (rtac some_equality 1);
   7.100 +by  (atac 1);
   7.101 +by (etac ex1E 1);
   7.102 +by (etac all_dupE 1);
   7.103 +by (fast_tac HOL_cs 1);
   7.104 +qed "ex1_some_eq_trivial";
   7.105  
   7.106  
   7.107  section "unique";
   7.108 @@ -103,7 +32,7 @@
   7.109  by (Simp_tac 1);
   7.110  qed "unique_Nil";
   7.111  
   7.112 -Goalw [unique_def] "unique ((x,y)#l) = (unique l \\<and> (!y. (x,y) ~: set l))";
   7.113 +Goalw [unique_def] "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))";
   7.114  by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
   7.115  qed "unique_Cons";
   7.116  
   7.117 @@ -120,47 +49,14 @@
   7.118  by  (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq]));
   7.119  qed_spec_mp "unique_map_inj";
   7.120  
   7.121 -Goal "!!l. unique l ==> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
   7.122 -by(etac unique_map_inj 1);
   7.123 -by(rtac injI 1);
   7.124 -by Auto_tac;
   7.125 -qed "unique_map_Pair";
   7.126 -
   7.127 -Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N";
   7.128 -by(rtac set_ext 1);
   7.129 -by(simp_tac (simpset() addsimps image_def::premises()) 1);
   7.130 -qed "image_cong";
   7.131 -
   7.132 -val split_Pair_eq = prove_goal Product_Type.thy 
   7.133 -"!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [
   7.134 -	etac imageE 1,
   7.135 -	split_all_tac 1,
   7.136 -	auto_tac(claset_of Product_Type.thy,simpset_of Product_Type.thy)]);
   7.137 -
   7.138 -
   7.139  (* More about Maps *)
   7.140  
   7.141 -val override_SomeD = prove_goalw thy [override_def] "(s ++ t) k = Some x ==> \
   7.142 -\ t k = Some x |  t k = None \\<and>  s k = Some x" (fn prems => [
   7.143 -	cut_facts_tac prems 1,
   7.144 -	case_tac "\\<exists>x. t k = Some x" 1,
   7.145 -	 etac exE 1,
   7.146 -	 rotate_tac ~1 1,
   7.147 -	 Asm_full_simp_tac 1,
   7.148 -	asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1,
   7.149 -	 rotate_tac ~1 1,
   7.150 -	 Asm_full_simp_tac 1]);
   7.151 +(*###Addsimps [fun_upd_same, fun_upd_other];*)
   7.152  
   7.153 -Addsimps [fun_upd_same, fun_upd_other];
   7.154 -
   7.155 -Goal "unique xys --> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
   7.156 -by(induct_tac "xys" 1);
   7.157 - by(Simp_tac 1);
   7.158 -by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
   7.159 -qed_spec_mp "unique_map_of_Some_conv";
   7.160 -
   7.161 -val in_set_get = unique_map_of_Some_conv RS iffD2;
   7.162 -val get_in_set = unique_map_of_Some_conv RS iffD1;
   7.163 +Goal "unique l --> (k, x) : set l --> map_of l k = Some x";
   7.164 +by (induct_tac "l" 1);
   7.165 +by  Auto_tac;
   7.166 +qed_spec_mp "map_of_SomeI";
   7.167  
   7.168  Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)";
   7.169  by(induct_tac "l" 1);
   7.170 @@ -169,50 +65,14 @@
   7.171  by Auto_tac;
   7.172  bind_thm("Ball_set_table",result() RS mp);
   7.173  
   7.174 -val table_mono = prove_goal thy 
   7.175 -"unique l' --> (\\<forall>xy. (xy)\\<in>set l --> (xy)\\<in>set l') -->\
   7.176 -\ (\\<forall>k y. map_of l k = Some y --> map_of l' k = Some y)" (fn _ => [
   7.177 -	induct_tac "l" 1,
   7.178 -	 Auto_tac,
   7.179 - 	 fast_tac (HOL_cs addSIs [in_set_get]) 1])
   7.180 - RS mp RS mp RS spec RS spec RS mp;
   7.181 -
   7.182 -val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) --> \
   7.183 -\ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
   7.184 -	induct_tac "t" 1,	
   7.185 -	 ALLGOALS Simp_tac,
   7.186 -	case_tac1 "k = fst a" 1,
   7.187 -	 Auto_tac]) RS mp;
   7.188 -val table_map_Some = prove_goal thy 
   7.189 -"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
   7.190 -\map_of t (k, k') = Some x" (K [
   7.191 -	induct_tac "t" 1,	
   7.192 -	Auto_tac]) RS mp;
   7.193 -
   7.194 +Goal "map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \
   7.195 +\map_of t (k, k') = Some x";
   7.196 +by (induct_tac "t" 1);
   7.197 +by  Auto_tac;
   7.198 +qed_spec_mp "table_of_remap_SomeD";
   7.199  
   7.200 -val table_mapf_Some = prove_goal thy "!!f. \\<forall>x y. f x = f y --> x = y ==> \
   7.201 -\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) --> map_of t k = Some x" (K [
   7.202 -	induct_tac "t" 1,	
   7.203 -	Auto_tac]) RS mp;
   7.204 -val table_mapf_SomeD = prove_goal thy 
   7.205 -"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z --> (\\<exists>y. (k,y)\\<in>set t \\<and>  z = f y)"(K [
   7.206 -	induct_tac "t" 1,	
   7.207 -	Auto_tac]) RS mp;
   7.208 -
   7.209 -val table_mapf_Some2 = prove_goal thy 
   7.210 -"!!k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) ==> C = D \\<and> map_of t k = Some x" (K [
   7.211 -	forward_tac [table_mapf_SomeD] 1,
   7.212 -	Auto_tac,
   7.213 -	rtac table_mapf_Some 1,
   7.214 -	 atac 2,
   7.215 -	Fast_tac 1]);
   7.216 -
   7.217 -val finite_map_of = rewrite_rule [dom_def] finite_dom_map_of;
   7.218 -
   7.219 -Goal
   7.220 -"map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
   7.221 +(* ### To Map.ML *)
   7.222 +Goal "map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
   7.223  by (induct_tac "xs" 1);
   7.224 -auto();
   7.225 +by Auto_tac;
   7.226  qed "map_of_map";
   7.227 -
   7.228 -
     8.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Dec 06 19:09:34 2000 +0100
     8.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Wed Dec 06 19:10:36 2000 +0100
     8.3 @@ -7,29 +7,29 @@
     8.4  *)
     8.5  
     8.6  
     8.7 +
     8.8  Addsimps [split_beta];
     8.9  
    8.10  Goal "[|h a = None; (h, l)::\\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> \
    8.11  \ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)::\\<preceq>(G, lT)";
    8.12  by( etac conforms_upd_obj 1);
    8.13  by(  rewtac oconf_def);
    8.14 -by(  auto_tac (claset() addSDs [is_type_fields, map_of_SomeD], simpset()));
    8.15 +by(  auto_tac (claset() addSDs [fields_is_type], simpset()));
    8.16  qed "NewC_conforms";
    8.17 -
    8.18 + 
    8.19  Goalw [cast_ok_def]
    8.20   "[| wf_prog wf_mb G; G,h\\<turnstile>v::\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v|] \
    8.21  \ ==> G,h\\<turnstile>v::\\<preceq>Class D";
    8.22 -by( case_tac1 "v = Null" 1);
    8.23 +by( case_tac "v = Null" 1);
    8.24  by(  Asm_full_simp_tac 1);
    8.25  by(  dtac widen_RefT 1);
    8.26  by(  Clarify_tac 1);
    8.27 -by(  rtac widen.null 1);
    8.28  by( datac non_npD 1 1);
    8.29  by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def]));
    8.30  qed "Cast_conf";
    8.31  
    8.32  Goal "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\\<preceq>(G,lT); \
    8.33 -\    x' = None --> G,h\\<turnstile>a'::\\<preceq> Class C; np a' x' = None |] ==> \
    8.34 +\ x' = None --> G,h\\<turnstile>a'::\\<preceq> Class C; np a' x' = None |] ==> \
    8.35  \ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\\<preceq>ft";
    8.36  by( dtac np_NoneD 1);
    8.37  by( etac conjE 1);
    8.38 @@ -38,11 +38,8 @@
    8.39  by   Auto_tac;
    8.40  by( dtac (conforms_heapD RS hconfD) 1);
    8.41  by(  atac 1);
    8.42 -by( dtac widen_cfs_fields 1);
    8.43 -by(   atac 1);
    8.44 -by(  atac 1);
    8.45 -by( dtac oconf_objD 1);
    8.46 -by(  atac 1);
    8.47 +by( datac widen_cfs_fields 2 1);
    8.48 +by( datac oconf_objD 1 1);
    8.49  by Auto_tac;
    8.50  qed "FAcc_type_sound";
    8.51  
    8.52 @@ -62,12 +59,12 @@
    8.53  by( dtac non_np_objD 1);
    8.54  by(   atac 1);
    8.55  by(  SELECT_GOAL Auto_tac 1);
    8.56 -by( strip_tac1 1);
    8.57 +by( Clarify_tac 1);
    8.58  by( Full_simp_tac 1);
    8.59  by( EVERY [forward_tac [hext_objD] 1, atac 1]);
    8.60  by( etac exE 1);
    8.61  by( Asm_full_simp_tac 1);
    8.62 -by( strip_tac1 1);
    8.63 +by( Clarify_tac 1);
    8.64  by( rtac conjI 1);
    8.65  by(  fast_tac (HOL_cs addEs [hext_trans, hext_upd_obj]) 1);
    8.66  by( rtac conjI 1);
    8.67 @@ -85,7 +82,7 @@
    8.68  by( rtac (oconf_obj RS iffD2) 1);
    8.69  by( Simp_tac 1);
    8.70  by( strip_tac 1);
    8.71 -by( case_tac1 "(aaa, b) = (fn, fd)" 1);
    8.72 +by( case_tac "(aaa, b) = (fn, fd)" 1);
    8.73  by(  Asm_full_simp_tac 1);
    8.74  by(  fast_tac (HOL_cs addIs [conf_widen]) 1);
    8.75  by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1);
    8.76 @@ -105,8 +102,14 @@
    8.77  by( (etac conf_list_gext_widen THEN_ALL_NEW atac) 1);
    8.78  qed "Call_lemma2";
    8.79  
    8.80 +Goal "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> is_class G D \\<longrightarrow> is_class G C";
    8.81 +by (etac rtrancl_induct 1);
    8.82 +by  (dtac subcls1D 2);
    8.83 +by  Auto_tac;
    8.84 +qed_spec_mp "subcls_is_class2"; 
    8.85 +
    8.86  Goalw [wf_java_prog_def]
    8.87 - "[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); \
    8.88 + "[| wf_java_prog G; a' \\<noteq> Null; (h, l)::\\<preceq>(G, lT); class G C = Some y; \
    8.89  \    max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
    8.90  \    list_all2 (conf G h) pvs pTsa;\
    8.91  \    (md, rT, pns, lvars, blk, res) = \
    8.92 @@ -117,16 +120,14 @@
    8.93  \         xi\\<le>|h' \\<and> (h', xj)::\\<preceq>(G, lT) \\<and> (x' = None --> G,h'\\<turnstile>v::\\<preceq>T)); \
    8.94  \ G,xh\\<turnstile>a'::\\<preceq> Class C |] ==> \
    8.95  \ xc\\<le>|h' \\<and> (h', l)::\\<preceq>(G, lT) \\<and>  (x' = None --> G,h'\\<turnstile>v::\\<preceq>rTa)";
    8.96 -by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
    8.97 -by( dtac (max_spec2appl_meths RS appl_methsD) 1);
    8.98 +by( dtac max_spec2mheads 1);
    8.99  by( Clarify_tac 1);
   8.100  by( datac non_np_objD' 2 1);
   8.101 -by(  strip_tac1 1);
   8.102 -by(  Asm_full_simp_tac 1);
   8.103 +by(  Clarsimp_tac 1);
   8.104  by( Clarsimp_tac 1);
   8.105  by( EVERY'[forward_tac [hext_objD], atac] 1);
   8.106  by( Clarsimp_tac 1);
   8.107 -by( EVERY'[dtac Call_lemma, atac, atac] 1);
   8.108 +by( datac Call_lemma 3 1);
   8.109  by( clarsimp_tac (claset(),simpset() addsimps [wf_java_mdecl_def])1);
   8.110  by( thin_tac "method ?sig ?x = ?y" 1);
   8.111  by( EVERY'[dtac spec, etac impE] 1);
   8.112 @@ -142,7 +143,7 @@
   8.113  (*by( thin_tac "?E::\\<preceq>(G, pT')" 1);*)
   8.114  by( EVERY'[dtac spec, mp_tac] 1);
   8.115  by( thin_tac "?E\\<turnstile>res::?rT" 1);
   8.116 -by( strip_tac1 1);
   8.117 +by( Clarify_tac 1);
   8.118  by( rtac conjI 1);
   8.119  by(  fast_tac (HOL_cs addIs [hext_trans]) 1);
   8.120  by( rtac conjI 1);
   8.121 @@ -163,7 +164,8 @@
   8.122  Unify.search_bound := 40;
   8.123  Unify.trace_bound  := 40;
   8.124  Delsplits[split_if];
   8.125 -Delsimps[fun_upd_apply];(*###*)
   8.126 +Delsimps[fun_upd_apply];
   8.127 +Addsimps[fun_upd_same];
   8.128  val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
   8.129  	(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
   8.130  Goal
   8.131 @@ -194,10 +196,9 @@
   8.132  by( dtac new_AddrD 1);
   8.133  by( etac disjE 1);
   8.134  by(  Asm_simp_tac 2);
   8.135 -by( etac conjE 1);
   8.136 -by( Asm_simp_tac 1);
   8.137 +by( Clarsimp_tac 1);
   8.138  by( rtac conjI 1);
   8.139 -by(  fast_tac (HOL_cs addSEs [NewC_conforms]) 1);
   8.140 +by(  force_tac (claset() addSEs [NewC_conforms],simpset()) 1);
   8.141  by( rtac conf_obj_AddrI 1);
   8.142  by(  rtac rtrancl_refl 2);
   8.143  by( Simp_tac 1);
   8.144 @@ -228,7 +229,7 @@
   8.145  			REPEAT o (etac conjE), hyp_subst_tac] 3);
   8.146  
   8.147  (* for if *)
   8.148 -by( (case_tac1 "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
   8.149 +by( (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
   8.150  
   8.151  by forward_hyp_tac;
   8.152  
   8.153 @@ -266,7 +267,7 @@
   8.154  by( fast_tac (claset() addIs [hext_trans]) 3);
   8.155  
   8.156  (* 2 FAss *)
   8.157 -by( case_tac1 "x2 = None" 1);
   8.158 +by( case_tac "x2 = None" 1);
   8.159  by(  Asm_simp_tac 2);
   8.160  by(  fast_tac (claset() addIs [hext_trans]) 2);
   8.161  by( Asm_full_simp_tac 1);
   8.162 @@ -274,7 +275,7 @@
   8.163  by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
   8.164  
   8.165  by prune_params_tac;
   8.166 -(* Level 51 *)
   8.167 +(* Level 50 *)
   8.168  
   8.169  (* 1 Call *)
   8.170  by( case_tac "x" 1);
   8.171 @@ -287,14 +288,16 @@
   8.172  by( Clarify_tac 1);
   8.173  by( dtac evals_no_xcpt 1);
   8.174  by( Asm_full_simp_tac 1);
   8.175 -by( case_tac1 "a' = Null" 1);
   8.176 +by( case_tac "a' = Null" 1);
   8.177  by(  Asm_full_simp_tac 1);
   8.178  by(  dtac exec_xcpt 1);
   8.179  by(  Asm_full_simp_tac 1);
   8.180  by(  dtac eval_xcpt 1);
   8.181  by(  Asm_full_simp_tac 1);
   8.182  by(  fast_tac (HOL_cs addEs [hext_trans]) 1);
   8.183 -by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) 
   8.184 +by( datac ty_expr_is_type 1 1);
   8.185 +by(Clarsimp_tac 1);
   8.186 +by( (rtac (rewrite_rule [wf_java_prog_def] Call_type_sound) 
   8.187      THEN_ALL_NEW Asm_simp_tac) 1);
   8.188  qed "eval_evals_exec_type_sound";
   8.189  
   8.190 @@ -318,18 +321,15 @@
   8.191  \         s::\\<preceq>E; E\\<turnstile>e::Class C; method (G,C) sig \\<noteq> None|] ==> \
   8.192  \ method (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
   8.193  by( datac eval_type_sound 4 1);
   8.194 -by( not_None_tac 1);
   8.195 -by( split_all_tac 1);
   8.196 +by(Clarsimp_tac 1);
   8.197  by(rewtac wf_java_prog_def);
   8.198  by( forward_tac [widen_methd] 1);
   8.199  by(   atac 1);
   8.200 -by(  rtac (not_None_eq RS iffD1) 2);
   8.201  by(  Fast_tac 2);
   8.202 -by( etac conjE 1);
   8.203  by( dtac non_npD 1);
   8.204  by Auto_tac;
   8.205  qed "all_methods_understood";
   8.206  
   8.207  Delsimps [split_beta];
   8.208 -Addsimps[fun_upd_apply];(*###*)
   8.209 +Addsimps[fun_upd_apply];
   8.210  
     9.1 --- a/src/HOL/MicroJava/J/State.ML	Wed Dec 06 19:09:34 2000 +0100
     9.2 +++ b/src/HOL/MicroJava/J/State.ML	Wed Dec 06 19:10:36 2000 +0100
     9.3 @@ -4,65 +4,69 @@
     9.4      Copyright   1999 Technische Universitaet Muenchen
     9.5  *)
     9.6  
     9.7 -val obj_ty_def2 = prove_goalw thy [obj_ty_def] "obj_ty (C,fs) = Class C" 
     9.8 -	(K [Simp_tac 1]);
     9.9 -
    9.10 +Goalw [obj_ty_def] "obj_ty (C,fs) = Class C";
    9.11 +by (Simp_tac 1);
    9.12 +qed "obj_ty_def2";
    9.13  Addsimps [obj_ty_def2];
    9.14  
    9.15 -val new_AddrD = prove_goalw thy [new_Addr_def] 
    9.16 -"!!X. (a,x) = new_Addr h ==> h a = None \\<and>  x = None |  x = Some OutOfMemory" (K[
    9.17 -	asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
    9.18 -	rtac someI 1,
    9.19 -	rtac disjI2 1,
    9.20 -	res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1,
    9.21 -	 Auto_tac ]);
    9.22 -
    9.23 -val raise_if_True = prove_goalw thy [raise_if_def] 
    9.24 -	"raise_if True x y \\<noteq> None"
    9.25 -(K [split_tac [split_if] 1,Auto_tac]);
    9.26 -
    9.27 -val raise_if_False = prove_goalw thy [raise_if_def] 
    9.28 -	"raise_if False x y = y"
    9.29 -(K [Auto_tac]);
    9.30 -
    9.31 -val raise_if_Some = prove_goalw thy [raise_if_def] 
    9.32 -	"raise_if c x (Some y) \\<noteq> None" (K [Auto_tac]);
    9.33 -
    9.34 -val raise_if_Some2 = prove_goalw thy [raise_if_def] 
    9.35 -"raise_if c z (if x = None then Some y else x) \\<noteq> None" (K[
    9.36 -	induct_tac "x" 1,
    9.37 -	Auto_tac]);
    9.38 -val if_None_eq = prove_goal thy 
    9.39 -"(if x = None then None else x) = x" (K[
    9.40 -	induct_tac "x" 1,
    9.41 -	Auto_tac]);
    9.42 -
    9.43 -Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2,if_None_eq];
    9.44 -
    9.45 -val raise_if_SomeD = prove_goalw thy [raise_if_def] 
    9.46 -	"raise_if c x y = Some z --> c \\<and>  Some z = Some x |  y = Some z" 
    9.47 -(K [split_tac [split_if] 1,Auto_tac]) RS mp;
    9.48 -
    9.49 -val raise_if_NoneD = prove_goalw thy [raise_if_def] 
    9.50 -	"raise_if c x y = None --> \\<not> c \\<and>  y = None"
    9.51 -(K [split_tac [split_if] 1,Auto_tac]) RS mp;
    9.52 +Goalw [new_Addr_def] 
    9.53 +"(a,x) = new_Addr h ==> h a = None \\<and> x = None | x = Some OutOfMemory";
    9.54 +by(asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1);
    9.55 +by(rtac someI 1);
    9.56 +by(rtac disjI2 1);
    9.57 +by(res_inst_tac [("r","snd (?a,Some OutOfMemory)")] trans 1);
    9.58 +by Auto_tac;
    9.59 +qed "new_AddrD";
    9.60  
    9.61  
    9.62 -val np_NoneD = (prove_goalw thy [np_def, raise_if_def] 
    9.63 -	"np a' x' = None --> x' = None \\<and>  a' \\<noteq> Null" (fn _ => [
    9.64 -	split_tac [split_if] 1,
    9.65 -	Auto_tac ])) RS mp;
    9.66 -val np_None = (prove_goalw thy [np_def, raise_if_def] 
    9.67 -	"a' \\<noteq> Null --> np a' x' = x'" (fn _ => [
    9.68 -	split_tac [split_if] 1,
    9.69 -	Auto_tac ])) RS mp;
    9.70 -val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
    9.71 -	(fn _ => [Auto_tac ]);
    9.72 -val np_Null = prove_goalw thy [np_def, raise_if_def] 
    9.73 -	"np Null None = Some NullPointer" (fn _ => [
    9.74 -	Auto_tac ]);
    9.75 -val np_Addr = prove_goalw thy [np_def, raise_if_def] "np (Addr a) None = None" 
    9.76 -	(fn _ => [Auto_tac ]);
    9.77 +Goalw [raise_if_def] "raise_if True x y \\<noteq> None";
    9.78 +by Auto_tac;
    9.79 +qed "raise_if_True";
    9.80 +
    9.81 +Goalw [raise_if_def] "raise_if False x y = y";
    9.82 +by Auto_tac;
    9.83 +qed "raise_if_False";
    9.84 +
    9.85 +Goalw [raise_if_def] "raise_if c x (Some y) \\<noteq> None";
    9.86 +by Auto_tac;
    9.87 +qed "raise_if_Some";
    9.88 +
    9.89 +Goalw [raise_if_def] "raise_if c z (if x = None then Some y else x) \\<noteq> None";
    9.90 +by(induct_tac "x" 1);
    9.91 +by Auto_tac;
    9.92 +qed "raise_if_Some2";
    9.93 +
    9.94 +Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2];
    9.95 +
    9.96 +Goalw [raise_if_def] 
    9.97 +  "raise_if c x y = Some z \\<longrightarrow> c \\<and>  Some z = Some x |  y = Some z"; 
    9.98 +by Auto_tac;
    9.99 +qed_spec_mp "raise_if_SomeD";
   9.100 +
   9.101 +Goalw [raise_if_def] "raise_if c x y = None --> \\<not> c \\<and>  y = None";
   9.102 +by Auto_tac;
   9.103 +qed_spec_mp "raise_if_NoneD";
   9.104 +
   9.105 +Goalw [np_def, raise_if_def] "np a' x' = None --> x' = None \\<and>  a' \\<noteq> Null"; 
   9.106 +by Auto_tac;
   9.107 +qed_spec_mp "np_NoneD";
   9.108 +
   9.109 +Goalw [np_def, raise_if_def] "a' \\<noteq> Null --> np a' x' = x'";
   9.110 +by Auto_tac;
   9.111 +qed_spec_mp "np_None";
   9.112 +
   9.113 +Goalw [np_def, raise_if_def] "np a' (Some xc) = Some xc";
   9.114 +by Auto_tac;
   9.115 +qed "np_Some";
   9.116 +
   9.117 +Goalw [np_def, raise_if_def] "np Null None = Some NullPointer";
   9.118 +by Auto_tac;
   9.119 +qed "np_Null";
   9.120 +
   9.121 +Goalw [np_def, raise_if_def] "np (Addr a) None = None";
   9.122 +by Auto_tac;
   9.123 +qed "np_Addr";
   9.124 +
   9.125  Addsimps[np_None, np_Some,np_Null,np_Addr];
   9.126  
   9.127  Goalw [raise_if_def] "(np Null (raise_if c xc None)) = \
    10.1 --- a/src/HOL/MicroJava/J/TypeRel.ML	Wed Dec 06 19:09:34 2000 +0100
    10.2 +++ b/src/HOL/MicroJava/J/TypeRel.ML	Wed Dec 06 19:10:36 2000 +0100
    10.3 @@ -4,44 +4,43 @@
    10.4      Copyright   1999 Technische Universitaet Muenchen
    10.5  *)
    10.6  
    10.7 -val subcls1D = prove_goalw thy [subcls1_def] "!!G. G\\<turnstile>C\\<prec>C1D ==> \
    10.8 -\ \\<exists>fs ms. class G C = Some (Some D,fs,ms)" (K [Auto_tac]);
    10.9 +Goalw [subcls1_def] 
   10.10 +  "G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> C \\<noteq> Object \\<and> (\\<exists>fs ms. class G C = Some (D,fs,ms))";
   10.11 +by Auto_tac;
   10.12 +qed "subcls1D";
   10.13 +Goalw [subcls1_def] "\\<lbrakk>class G C = Some (D,rest); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C1D";
   10.14 +by Auto_tac;
   10.15 +qed "subcls1I";
   10.16  
   10.17 -val subcls1I = prove_goalw  thy [subcls1_def] 
   10.18 -"!!G. [| class G C = Some (Some D,rest) |] ==> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
   10.19 -
   10.20 -val subcls1_def2 = prove_goalw thy [subcls1_def,is_class_def]  "subcls1 G = \
   10.21 -\ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
   10.22 - (K [Auto_tac]);
   10.23 +Goalw [subcls1_def]  
   10.24 +"subcls1 G = (\\<Sigma>C\\<in>{C. is_class G C} . {D. C\\<noteq>Object \\<and> fst (the (class G C))=D})";
   10.25 +by Auto_tac;
   10.26 +qed "subcls1_def2";
   10.27  
   10.28  Goal "finite (subcls1 G)";
   10.29  by(stac subcls1_def2 1);
   10.30 -by( rtac finite_SigmaI 1);
   10.31 -by(  rtac finite_is_class 1);
   10.32 -by( rtac finite_subset 1);
   10.33 -by(  rtac some_subset_the 1);
   10.34 -by( Simp_tac 1);
   10.35 +by( rtac (finite_is_class RS finite_SigmaI) 1);
   10.36 +by(res_inst_tac [("B","{fst (the (class G C))}")] finite_subset 1);
   10.37 +by  Auto_tac;
   10.38  qed "finite_subcls1";
   10.39  
   10.40 -fun prove_typerel_lemma drules indrule s = prove_goal thy s (fn prems => [
   10.41 -	rtac (hd prems RS indrule) 1,
   10.42 -	auto_tac (claset() addDs drules, simpset())]);
   10.43  
   10.44 -fun prove_typerel s lemmata = prove_goal thy s (fn prems => [
   10.45 -	cut_facts_tac prems 1,
   10.46 -	auto_tac (claset() addDs lemmata, simpset())]);
   10.47 -
   10.48 -
   10.49 -Goalw [is_class_def] "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
   10.50 +Goal "(C,D) \\<in> (subcls1 G)^+ ==> is_class G C";
   10.51  by(etac trancl_trans_induct 1);
   10.52  by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
   10.53  qed "subcls_is_class";
   10.54  
   10.55 +Goal "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> is_class G D \\<longrightarrow> is_class G C";
   10.56 +by (etac rtrancl_induct 1);
   10.57 +by  (dtac subcls1D 2);
   10.58 +by  Auto_tac;
   10.59 +qed_spec_mp "subcls_is_class2"; 
   10.60 +
   10.61  (* A particular thm about wf;
   10.62     looks like it is an odd instance of something more general
   10.63  *)
   10.64  Goalw [wf_def] "wf{((A,x),(B,y)) . A=B \\<and> wf(R(A)) \\<and> (x,y)\\<in>R(A)}";
   10.65 -by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [split_paired_All]) 1);
   10.66 +by(full_simp_tac (simpset() delcongs [imp_cong]) 1);
   10.67  by(strip_tac 1);
   10.68  by(rename_tac "A x" 1);
   10.69  by(case_tac "wf(R A)" 1);
   10.70 @@ -68,30 +67,48 @@
   10.71   (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (fields.tcs)))))
   10.72   (K [auto_tac (claset() addIs [subcls1I], simpset())]);
   10.73  
   10.74 +Goalw [field_def] 
   10.75 +"field (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of (fields (G,C)) (fn, fd) = Some fT";
   10.76 +by (rtac table_of_remap_SomeD 1);
   10.77 +by (Asm_full_simp_tac 1);
   10.78 +qed "field_fields";
   10.79  
   10.80 -AddSIs   [widen.refl];
   10.81 +AddSIs   [widen.refl,widen.null];
   10.82  Addsimps [widen.refl];
   10.83  
   10.84 -val prove_widen_lemma = prove_typerel_lemma [] widen.elim;
   10.85 -
   10.86  Goal "(G\\<turnstile>PrimT pT\\<preceq>RefT rT) = False";
   10.87  br iffI 1;
   10.88  be widen.elim 1;
   10.89 -by(Auto_tac);
   10.90 +by Auto_tac;
   10.91  qed "widen_PrimT_RefT";
   10.92  AddIffs [widen_PrimT_RefT];
   10.93  
   10.94 -val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t" 
   10.95 -	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)"];
   10.96 -bind_thm ("widen_RefT", widen_RefT);
   10.97 +Goal "G\\<turnstile>S\\<preceq>T ==> S=RefT R --> (\\<exists>t. T=RefT t)";
   10.98 +by (etac widen.elim 1);
   10.99 +by Auto_tac;
  10.100 +qed "widen_RefT_lemma";
  10.101 +Goal "G\\<turnstile>RefT R\\<preceq>T ==> \\<exists>t. T=RefT t"; 
  10.102 +by (dtac widen_RefT_lemma 1);
  10.103 +by Auto_tac;
  10.104 +qed "widen_RefT";
  10.105  
  10.106 -val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t" 
  10.107 -	[prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)"];
  10.108 -bind_thm ("widen_RefT2", widen_RefT2);
  10.109 +Goal "G\\<turnstile>S\\<preceq>T ==> T=RefT R --> (\\<exists>t. S=RefT t)";
  10.110 +by (etac widen.elim 1);
  10.111 +by Auto_tac;
  10.112 +qed "widen_RefT2_lemma";
  10.113 +Goal "G\\<turnstile>S\\<preceq>RefT R ==> \\<exists>t. S=RefT t";
  10.114 +by (dtac widen_RefT2_lemma 1);
  10.115 +by Auto_tac;
  10.116 +qed "widen_RefT2";
  10.117  
  10.118 -val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D"
  10.119 - [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)"];
  10.120 -bind_thm ("widen_Class", widen_Class);
  10.121 +Goal "G\\<turnstile>S\\<preceq>T ==> S = Class C --> (\\<exists>D. T=Class D)";
  10.122 +by (etac widen.elim 1);
  10.123 +by Auto_tac;
  10.124 +qed "widen_Class_lemma";
  10.125 +Goal "G\\<turnstile>Class C\\<preceq>T ==> \\<exists>D. T=Class D";
  10.126 +by (dtac widen_Class_lemma 1);
  10.127 +by Auto_tac;
  10.128 +qed "widen_Class";
  10.129  
  10.130  Goal "(G\\<turnstile>Class C\\<preceq>RefT NullT) = False"; 
  10.131  br iffI 1;
  10.132 @@ -113,6 +130,5 @@
  10.133  by   Safe_tac;
  10.134  by(  ALLGOALS (forward_tac [widen_Class, widen_RefT]));
  10.135  by  Safe_tac;
  10.136 -by(  rtac widen.null 2);
  10.137  by(eatac rtrancl_trans 1 1);
  10.138  qed_spec_mp "widen_trans";
    11.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Dec 06 19:09:34 2000 +0100
    11.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Dec 06 19:10:36 2000 +0100
    11.3 @@ -34,7 +34,7 @@
    11.4  defs
    11.5  
    11.6    (* direct subclass, cf. 8.1.3 *)
    11.7 -  subcls1_def	"subcls1 G == {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
    11.8 + subcls1_def"subcls1 G \\<equiv> {(C,D). C\\<noteq>Object \\<and> (\\<exists>c. class G C=Some c \\<and> fst c=D)}"
    11.9    
   11.10  consts
   11.11  
   11.12 @@ -42,15 +42,15 @@
   11.13    field	:: "'c prog \\<times> cname => ( vname \\<leadsto> cname \\<times> ty)"
   11.14    fields	:: "'c prog \\<times> cname => ((vname \\<times> cname) \\<times>  ty) list"
   11.15  
   11.16 -constdefs       (* auxiliary relations for recursive definitions below *)
   11.17 +constdefs       (* auxiliary relation for recursive definitions below *)
   11.18  
   11.19    subcls1_rel	:: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
   11.20   "subcls1_rel == {((G,C),(G',C')). G = G' \\<and>  wf ((subcls1 G)^-1) \\<and>  G\\<turnstile>C'\\<prec>C1C}"
   11.21  
   11.22  (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
   11.23  recdef method "subcls1_rel"
   11.24 - "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => empty
   11.25 -                   | Some (sc,fs,ms) => (case sc of None => empty | Some D => 
   11.26 + "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
   11.27 +                   | Some (D,fs,ms) => (if C = Object then empty else 
   11.28                                             if is_class G D then method (G,D) 
   11.29                                                             else arbitrary) ++
   11.30                                             map_of (map (\\<lambda>(s,  m ). 
   11.31 @@ -59,9 +59,9 @@
   11.32  
   11.33  (* list of fields of a class, including inherited and hidden ones *)
   11.34  recdef fields  "subcls1_rel"
   11.35 - "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
   11.36 -                   | Some (sc,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
   11.37 -                                           (case sc of None => [] | Some D => 
   11.38 + "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None =>arbitrary
   11.39 +                   | Some (D,fs,ms) => map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
   11.40 +                                           (if C = Object then [] else 
   11.41                                             if is_class G D then fields (G,D) 
   11.42                                                             else arbitrary))
   11.43                    else arbitrary)"
    12.1 --- a/src/HOL/MicroJava/J/WellForm.ML	Wed Dec 06 19:09:34 2000 +0100
    12.2 +++ b/src/HOL/MicroJava/J/WellForm.ML	Wed Dec 06 19:10:36 2000 +0100
    12.3 @@ -4,58 +4,59 @@
    12.4      Copyright   1999 Technische Universitaet Muenchen
    12.5  *)
    12.6  
    12.7 -val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
    12.8 - "!!X. [|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)" (K [
    12.9 -	Asm_full_simp_tac 1,
   12.10 -	fast_tac (set_cs addDs [get_in_set]) 1]);
   12.11 +Goalw [wf_prog_def]
   12.12 + "[|class G C = Some c; wf_prog wf_mb G|] ==> wf_cdecl wf_mb G (C,c)";
   12.13 +by (Asm_full_simp_tac 1);
   12.14 +by (fast_tac (set_cs addDs [map_of_SomeD]) 1);
   12.15 +qed "class_wf";
   12.16  
   12.17 -val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
   12.18 -	"!!X. wf_prog wf_mb G ==> class G Object = Some (None, [], [])" (K [
   12.19 -	safe_tac set_cs,
   12.20 -	dtac in_set_get 1,
   12.21 -	 Auto_tac]);
   12.22 +Goalw [wf_prog_def, ObjectC_def]
   12.23 +	"wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])";
   12.24 +by (auto_tac (claset() addIs [map_of_SomeI], simpset()));
   12.25 +qed "class_Object";
   12.26  Addsimps [class_Object];
   12.27  
   12.28 -val is_class_Object = prove_goalw thy [is_class_def] 
   12.29 -	"!!X. wf_prog wf_mb G ==> is_class G Object" (K [Asm_simp_tac 1]);
   12.30 +Goal "wf_prog wf_mb G ==> is_class G Object";
   12.31 +by (Asm_simp_tac 1);
   12.32 +qed "is_class_Object";
   12.33  Addsimps [is_class_Object];
   12.34  
   12.35  Goal "[|G\\<turnstile>C\\<prec>C1D; wf_prog wf_mb G|] ==> D \\<noteq> C \\<and> \\<not>(D,C)\\<in>(subcls1 G)^+";
   12.36  by( forward_tac [r_into_trancl] 1);
   12.37  by( dtac subcls1D 1);
   12.38 -by( strip_tac1 1);
   12.39 +by(Clarify_tac 1);
   12.40  by( datac class_wf 1 1);
   12.41  by( rewtac wf_cdecl_def);
   12.42  by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
   12.43  				  delsimps [reflcl_trancl]) 1);
   12.44  qed "subcls1_wfD";
   12.45  
   12.46 -val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def] 
   12.47 -"!!X. [|wf_cdecl wf_mb G (C, sc, r); C \\<noteq> Object|] ==> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
   12.48 -	pair_tac "r" 1,
   12.49 -	asm_full_simp_tac (simpset() addsplits [option.split_asm]) 1]);
   12.50 +Goalw [wf_cdecl_def] 
   12.51 +"!!r. \\<lbrakk>wf_cdecl wf_mb G (C,D,r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> is_class G D";
   12.52 +by (auto_tac (claset(), simpset() addsplits [option.split_asm]));
   12.53 +qed "wf_cdecl_supD";
   12.54  
   12.55  Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> \\<not>(D,C)\\<in>(subcls1 G)^+";
   12.56  by(etac tranclE 1);
   12.57 -by(TRYALL(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
   12.58 +by(TRYALL(fast_tac (claset() addSDs [subcls1_wfD] addIs [trancl_trans])));
   12.59  qed "subcls_asym";
   12.60  
   12.61 -val subcls_irrefl = prove_goal thy "!!X. [|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D" (K [
   12.62 -	etac trancl_trans_induct 1,
   12.63 -	 fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
   12.64 -	fast_tac (HOL_cs addDs [subcls_asym]) 1]);
   12.65 +Goal "[|wf_prog wf_mb G; (C,D)\\<in>(subcls1 G)^+|] ==> C \\<noteq> D";
   12.66 +by (etac trancl_trans_induct 1);
   12.67 +by  (auto_tac (claset() addDs [subcls1_wfD,subcls_asym],simpset()));
   12.68 +qed "subcls_irrefl";
   12.69  
   12.70 -val acyclic_subcls1 = prove_goalw thy [acyclic_def] 
   12.71 -	"!!X. wf_prog wf_mb G ==> acyclic (subcls1 G)" (K [
   12.72 -	strip_tac1 1,
   12.73 -	fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
   12.74 +Goalw [acyclic_def] "wf_prog wf_mb G ==> acyclic (subcls1 G)";
   12.75 +by (fast_tac (claset() addDs [subcls_irrefl]) 1);
   12.76 +qed "acyclic_subcls1";
   12.77  
   12.78 -val wf_subcls1 = prove_goal thy "!!X. wf_prog wf_mb G ==> wf ((subcls1 G)^-1)" (K [
   12.79 -	rtac finite_acyclic_wf 1,
   12.80 -	 stac finite_converse 1,
   12.81 -	 rtac finite_subcls1 1,
   12.82 -	stac acyclic_converse 1,
   12.83 -	etac acyclic_subcls1 1]);
   12.84 +Goal "wf_prog wf_mb G ==> wf ((subcls1 G)^-1)";
   12.85 +by (rtac finite_acyclic_wf 1);
   12.86 +by ( stac finite_converse 1);
   12.87 +by ( rtac finite_subcls1 1);
   12.88 +by (stac acyclic_converse 1);
   12.89 +by (etac acyclic_subcls1 1);
   12.90 +qed "wf_subcls1";
   12.91  
   12.92  val major::prems = goal thy
   12.93    "[|wf_prog wf_mb G; !!C. \\<forall>D. (C,D)\\<in>(subcls1 G)^+ --> P D ==> P C|] ==> P C";
   12.94 @@ -68,8 +69,8 @@
   12.95  qed "subcls_induct";
   12.96  
   12.97  val prems = goal thy "[|is_class G C; wf_prog wf_mb G; P Object; \
   12.98 -\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
   12.99 -\   wf_cdecl wf_mb G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D|] ==> P C\
  12.100 +\!!C D fs ms. [|C \\<noteq> Object; is_class G C; class G C = Some (D,fs,ms) \\<and> \
  12.101 +\   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\
  12.102  \ |] ==> P C";
  12.103  by( cut_facts_tac prems 1);
  12.104  by( rtac impE 1);
  12.105 @@ -81,32 +82,30 @@
  12.106  by( rtac impI 1);
  12.107  by( case_tac "C = Object" 1);
  12.108  by(  Fast_tac 1);
  12.109 -by( ex_ftac is_classD 1);
  12.110 +by Safe_tac;
  12.111  by( forward_tac [class_wf] 1);
  12.112  by(  atac 1);
  12.113  by( forward_tac [wf_cdecl_supD] 1);
  12.114  by(  atac 1);
  12.115 -by( strip_tac1 1);
  12.116 +
  12.117 +by( subgoal_tac "G\\<turnstile>C\\<prec>C1a" 1);
  12.118 +by( etac subcls1I 2);
  12.119  by( rtac (hd (tl (tl (tl prems)))) 1);
  12.120 -by(   atac 1);
  12.121 -by(  atac 1);
  12.122 -by( subgoal_tac "G\\<turnstile>C\\<prec>C1D" 1);
  12.123 -by(  fast_tac (HOL_cs addIs [r_into_trancl]) 1);
  12.124 -by( etac subcls1I 1);
  12.125 +by Auto_tac;
  12.126  qed "subcls1_induct";
  12.127  
  12.128 -Goal "[|wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) --> is_class G D|] ==> method (G,C) = \
  12.129 -\ (case class G C of None => empty | Some (sc,fs,ms) => \
  12.130 -\ (case sc of None => empty | Some D => method (G,D)) ++ \
  12.131 +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) = \
  12.132 +\ (case class G C of None => arbitrary | Some (D,fs,ms) => \
  12.133 +\ (if C = Object then empty else method (G,D)) ++ \
  12.134  \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
  12.135  by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
  12.136  by( asm_simp_tac (simpset() addsplits[option.split]) 1);
  12.137 -auto();
  12.138 +by Auto_tac;
  12.139  qed "method_rec_lemma";
  12.140  
  12.141  Goal "wf_prog wf_mb G ==> method (G,C) = \
  12.142 -\ (case class G C of None => empty | Some (sc,fs,ms) => \
  12.143 -\ (case sc of None => empty | Some D => method (G,D)) ++ \
  12.144 +\ (case class G C of None => arbitrary | Some (D,fs,ms) => \
  12.145 +\ (if C = Object then empty else method (G,D)) ++ \
  12.146  \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
  12.147  by(rtac method_rec_lemma 1);
  12.148  by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def] 
  12.149 @@ -119,36 +118,40 @@
  12.150  by( Asm_full_simp_tac 1);
  12.151  qed "method_rec";
  12.152  
  12.153 -Goal "[|wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C --> is_class G C|] ==> fields (G,C) = \
  12.154 -\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
  12.155 -\ (case sc of None => [] | Some D => fields (G,D))";
  12.156 -by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
  12.157 +Goal "[|wf ((subcls1 G)^-1); class G C = Some (D,fs,ms); C \\<noteq> Object \\<longrightarrow> is_class G D|] ==> fields (G,C) = \
  12.158 +\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))";
  12.159 +by(rtac trans 1);
  12.160 +by(rtac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
  12.161  by( asm_simp_tac (simpset() addsplits[option.split]) 1);
  12.162  qed "fields_rec_lemma";
  12.163  
  12.164 -Goal "[|class G C = Some (sc,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
  12.165 -\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
  12.166 -\ (case sc of None => [] | Some D => fields (G,D))";
  12.167 +Goal "[|class G C = Some (D,fs,ms); wf_prog wf_mb G|] ==> fields (G,C) = \
  12.168 +\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))";
  12.169 +by(rtac trans 1);
  12.170  by(rtac fields_rec_lemma 1);
  12.171 -by(   asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
  12.172 +by(   asm_simp_tac (simpset() addsimps [wf_subcls1]) 1);
  12.173  ba  1;
  12.174 -by( option_case_tac2 "sc" 1);
  12.175 -by(  Asm_simp_tac 1);
  12.176 -by( case_tac "C = Object" 1);
  12.177 -by(  rotate_tac 2 1);
  12.178 -by(  Asm_full_simp_tac 1);
  12.179 +br refl 2;
  12.180  by( datac class_wf 1 1);
  12.181 -by( datac wf_cdecl_supD 1 1);
  12.182 -by( Asm_full_simp_tac 1);
  12.183 +by(rtac impI 1);
  12.184 +by( eatac wf_cdecl_supD 1 1);
  12.185  qed "fields_rec";
  12.186  
  12.187 -val method_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> method (G,Object) = empty"
  12.188 -	(K [stac method_rec 1,Auto_tac]);
  12.189 -val fields_Object = prove_goal thy "!!X. wf_prog wf_mb G ==> fields (G,Object) = []"(K [
  12.190 -	stac fields_rec 1,Auto_tac]);
  12.191 +Goal "wf_prog wf_mb G ==> method (G,Object) = empty";
  12.192 +by(stac method_rec 1);
  12.193 +by Auto_tac;
  12.194 +qed "method_Object";
  12.195 +
  12.196 +Goal "wf_prog wf_mb G ==> fields (G,Object) = []";
  12.197 +by(stac fields_rec 1);
  12.198 +by Auto_tac;
  12.199 +qed "fields_Object";
  12.200 +
  12.201  Addsimps [method_Object, fields_Object];
  12.202 -val field_Object = prove_goalw thy [field_def]
  12.203 - "!!X. wf_prog wf_mb G ==> field (G,Object) = empty" (K [Asm_simp_tac 1]);
  12.204 +
  12.205 +Goalw [field_def] "wf_prog wf_mb G ==> field (G,Object) = empty";
  12.206 +by(Asm_simp_tac 1);
  12.207 +qed "field_Object";
  12.208  Addsimps [field_Object];
  12.209  
  12.210  Goal "[|is_class G C; wf_prog wf_mb G|] ==> G\\<turnstile>C\\<preceq>C Object";
  12.211 @@ -159,17 +162,9 @@
  12.212  by(eatac rtrancl_into_rtrancl2 1 1);
  12.213  qed "subcls_C_Object";
  12.214  
  12.215 -val is_type_rTI = prove_goalw thy [wf_mhead_def]
  12.216 -	"!!sig. wf_mhead G sig rT ==> is_type G rT"
  12.217 -	(K [split_all_tac 1, Auto_tac]);
  12.218 -
  12.219 -Goal "[|(C',C)\\<in>(subcls1 G)^+; wf_prog wf_mb G|] ==> \
  12.220 -\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
  12.221 -by(etac trancl_trans_induct 1);
  12.222 -by( safe_tac (HOL_cs addSDs [subcls1D]));
  12.223 -by(stac fields_rec 1);
  12.224 -by(  Auto_tac);
  12.225 -qed_spec_mp "fields_mono";
  12.226 +Goalw [wf_mhead_def] "wf_mhead G sig rT ==> is_type G rT";
  12.227 +by Auto_tac;
  12.228 +qed "is_type_rTI";
  12.229  
  12.230  Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
  12.231  \ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>C\\<preceq>C fd";
  12.232 @@ -180,28 +175,22 @@
  12.233  by( stac fields_rec 1);
  12.234  by(   atac 1);
  12.235  by(  atac 1);
  12.236 -by( Simp_tac 1);
  12.237 +by( simp_tac (simpset() delsplits [split_if]) 1);
  12.238  by( rtac ballI 1);
  12.239  by( split_all_tac 1);
  12.240  by( Simp_tac 1);
  12.241  by( etac UnE 1);
  12.242 -by(  dtac split_Pair_eq 1);
  12.243 -by(  SELECT_GOAL (Auto_tac) 1);
  12.244 +by(  Force_tac 1);
  12.245  by( etac (r_into_rtrancl RS rtrancl_trans) 1);
  12.246 -by( etac BallE 1);
  12.247 -by(  contr_tac 1);
  12.248 -by( Asm_full_simp_tac 1);
  12.249 +by Auto_tac;
  12.250  qed "widen_fields_defpl'";
  12.251  
  12.252 -Goal "[|is_class G C; wf_prog wf_mb G; ((fn,fd),fT) \\<in> set (fields (G,C))|] ==> \
  12.253 +Goal "[|((fn,fd),fT) \\<in> set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==> \
  12.254  \ G\\<turnstile>C\\<preceq>C fd";
  12.255  by( datac widen_fields_defpl' 1 1);
  12.256 -(*###################*)
  12.257 -by( dtac bspec 1);
  12.258 -auto();
  12.259 +by (Fast_tac 1);
  12.260  qed "widen_fields_defpl";
  12.261  
  12.262 -
  12.263  Goal "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))";
  12.264  by( etac subcls1_induct 1);
  12.265  by(   atac 1);
  12.266 @@ -212,54 +201,53 @@
  12.267  by( stac fields_rec 1);
  12.268  by   Auto_tac;
  12.269  by( rotate_tac ~1 1);
  12.270 -by( ex_ftac is_classD 1);
  12.271  by( forward_tac [class_wf] 1);
  12.272  by  Auto_tac;
  12.273  by( asm_full_simp_tac (simpset() addsimps [wf_cdecl_def]) 1);
  12.274  by( etac unique_append 1);
  12.275 -by(  rtac unique_map_Pair 1);
  12.276 -by(  Step_tac 1);
  12.277 -by (EVERY1[dtac widen_fields_defpl, atac, atac]);
  12.278 -by( Asm_full_simp_tac 1);
  12.279 -by( dtac split_Pair_eq 1);
  12.280 -by( Asm_full_simp_tac 1);
  12.281 +by(  rtac unique_map_inj 1);
  12.282 +by(   Clarsimp_tac 1);
  12.283 +by  (rtac injI 1);
  12.284 +by(  Asm_full_simp_tac 1);
  12.285 +by(auto_tac (claset() addSDs [widen_fields_defpl], simpset()));
  12.286  qed "unique_fields";
  12.287  
  12.288 +Goal "[|wf_prog wf_mb G; (C',C)\\<in>(subcls1 G)^*|] ==> \
  12.289 +\ x \\<in> set (fields (G,C)) --> x \\<in> set (fields (G,C'))";
  12.290 +by(etac converse_rtrancl_induct 1);
  12.291 +by( safe_tac (HOL_cs addSDs [subcls1D]));
  12.292 +by(stac fields_rec 1);
  12.293 +by(  Auto_tac);
  12.294 +qed_spec_mp "fields_mono_lemma";
  12.295 +
  12.296  Goal
  12.297 -"[|wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft|] ==> \
  12.298 -\                          map_of (fields (G,C')) f = Some ft";
  12.299 -by( dtac rtranclD 1);
  12.300 -by( Auto_tac);
  12.301 -by( rtac table_mono 1);
  12.302 -by(   atac 3);
  12.303 -by(  rtac unique_fields 1);
  12.304 -by(   etac subcls_is_class 1);
  12.305 -by(  atac 1);
  12.306 -by( fast_tac (HOL_cs addEs [fields_mono]) 1);
  12.307 -qed "widen_fields_mono";
  12.308 -
  12.309 +"\\<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>\
  12.310 +\ \\<Longrightarrow> map_of (fields (G,D)) fn = Some f";
  12.311 +by (rtac map_of_SomeI 1);
  12.312 +by  (eatac unique_fields 1 1);
  12.313 +by (eatac fields_mono_lemma 1 1);
  12.314 +by (etac map_of_SomeD 1);
  12.315 +qed "fields_mono";
  12.316  
  12.317 -val cfs_fields_lemma = prove_goalw thy [field_def] 
  12.318 -"!!X. field (G,C) fn = Some (fd, fT) ==> map_of(fields (G,C)) (fn, fd) = Some fT"
  12.319 -(K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
  12.320 +Goal 
  12.321 +"[|field (G,C) fn = Some (fd, fT); G\\<turnstile>D\\<preceq>C C; wf_prog wf_mb G|]==> \
  12.322 +\ map_of (fields (G,D)) (fn, fd) = Some fT";
  12.323 +by (dtac field_fields 1);
  12.324 +by (dtac rtranclD 1);
  12.325 +by Safe_tac;
  12.326 +by (ftac subcls_is_class 1);
  12.327 +by (dtac trancl_into_rtrancl 1);
  12.328 +by (fast_tac (HOL_cs addDs [fields_mono]) 1);
  12.329 +qed "widen_cfs_fields";
  12.330  
  12.331 -val widen_cfs_fields = prove_goal thy "!!X. [|field (G,C) fn = Some (fd, fT);\
  12.332 -\  G\\<turnstile>C'\\<preceq>C C; wf_prog wf_mb G|] ==> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
  12.333 -fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
  12.334 -bind_thm ("widen_cfs_fields",widen_cfs_fields);
  12.335 -
  12.336 -
  12.337 -Goal "wf_prog wf_mb G ==> method (G,C) sig = Some (md,mh,m)\
  12.338 +Goal "wf_prog wf_mb G ==> is_class G C \\<Longrightarrow>  \
  12.339 +\    method (G,C) sig = Some (md,mh,m)\
  12.340  \  --> G\\<turnstile>C\\<preceq>C md \\<and> wf_mdecl wf_mb G md (sig,(mh,m))";
  12.341 -by( case_tac "is_class G C" 1);
  12.342 -by(  forw_inst_tac [("C","C")] method_rec 2);
  12.343 -by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
  12.344 -	delsimps [not_None_eq]) 2);
  12.345  by( etac subcls1_induct 1);
  12.346  by(   atac 1);
  12.347  by(  Force_tac 1);
  12.348  by( forw_inst_tac [("C","C")] method_rec 1);
  12.349 -by( strip_tac1 1);
  12.350 +by( Clarify_tac 1);
  12.351  by( rotate_tac ~1 1);
  12.352  by( Asm_full_simp_tac 1);
  12.353  by( dtac override_SomeD 1);
  12.354 @@ -270,11 +258,10 @@
  12.355  by(   atac 3);
  12.356  by(  rtac r_into_rtrancl 2);
  12.357  by(  fast_tac (HOL_cs addIs [subcls1I]) 2);
  12.358 -by( forward_tac [table_mapf_SomeD] 1);
  12.359 -by( strip_tac1 1);
  12.360 -by( Asm_full_simp_tac 1);
  12.361 +by (rotate_tac ~1 1);
  12.362 +by (ftac map_of_SomeD 1);
  12.363  by( rewtac wf_cdecl_def);
  12.364 -by( Asm_full_simp_tac 1);
  12.365 +by (Clarsimp_tac 1);
  12.366  qed_spec_mp "method_wf_mdecl";
  12.367  
  12.368  Goal "[|G\\<turnstile>T\\<preceq>C T'; wf_prog wf_mb G|] ==> \
  12.369 @@ -285,12 +272,12 @@
  12.370  by(  Fast_tac 1);
  12.371  by( etac conjE 1);
  12.372  by( etac trancl_trans_induct 1);
  12.373 -by(  strip_tac1 2);
  12.374 -by(  EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
  12.375 +by(  Clarify_tac 2);
  12.376 +by(  EVERY[smp_tac 3 2]);
  12.377  by(  fast_tac (HOL_cs addEs [widen_trans]) 2);
  12.378 -by( strip_tac1 1);
  12.379 +by( Clarify_tac 1);
  12.380  by( dtac subcls1D 1);
  12.381 -by( strip_tac1 1);
  12.382 +by( Clarify_tac 1);
  12.383  by( stac method_rec 1);
  12.384  by(  atac 1);
  12.385  by( rewtac override_def);
  12.386 @@ -304,13 +291,10 @@
  12.387  by(  atac 1);
  12.388  by( split_all_tac 1);
  12.389  by( rewtac wf_cdecl_def);
  12.390 -by( dtac table_mapf_Some2 1);
  12.391 -by( Clarsimp_tac 1);
  12.392 -by( dres_inst_tac [("xys1","ms")] get_in_set 1);
  12.393 +by( dtac map_of_SomeD 1);
  12.394  by Auto_tac;
  12.395  qed_spec_mp "subcls_widen_methd";
  12.396  
  12.397 -
  12.398  Goal
  12.399   "[| G\\<turnstile> C\\<preceq>C D; wf_prog wf_mb G; \
  12.400  \    method (G,D) sig = Some (md, rT, b) |] \
  12.401 @@ -319,12 +303,7 @@
  12.402               simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
  12.403  qed "subtype_widen_methd";
  12.404  
  12.405 -
  12.406 -Goal "wf_prog wf_mb G ==> \\<forall>D. method (G,C) sig = Some(D,mh,code) --> is_class G D \\<and> method (G,D) sig = Some(D,mh,code)";
  12.407 -by( case_tac "is_class G C" 1);
  12.408 -by(  forw_inst_tac [("C","C")] method_rec 2);
  12.409 -by(    asm_full_simp_tac (simpset() addsimps [is_class_def] 
  12.410 -	delsimps [not_None_eq]) 2);
  12.411 +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)";
  12.412  by (etac subcls1_induct 1);
  12.413    ba 1;
  12.414   by (Asm_full_simp_tac 1);
  12.415 @@ -340,26 +319,30 @@
  12.416   by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
  12.417  qed_spec_mp "method_in_md";
  12.418  
  12.419 -
  12.420  Goal "[|is_class G C; wf_prog wf_mb G|] ==> \
  12.421  \ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
  12.422  by( etac subcls1_induct 1);
  12.423  by(   atac 1);
  12.424  by(  Asm_simp_tac 1);
  12.425 -by( strip_tac1 1);
  12.426  by( stac fields_rec 1);
  12.427 -by(   atac 1);
  12.428 +by(   Fast_tac 1);
  12.429  by(  atac 1);
  12.430 -by( Asm_simp_tac 1);
  12.431 -by( safe_tac set_cs);
  12.432 -by(  Fast_tac 2);
  12.433 +by( Clarsimp_tac 1);
  12.434 +by( Safe_tac);
  12.435 +by(  Force_tac 2);
  12.436  by( dtac class_wf 1);
  12.437  by(  atac 1);
  12.438  by( rewtac wf_cdecl_def);
  12.439 -by( Asm_full_simp_tac 1);
  12.440 -by( strip_tac1 1);
  12.441 +by( Clarsimp_tac 1);
  12.442  by( EVERY[dtac bspec 1, atac 1]);
  12.443  by( rewtac wf_fdecl_def);
  12.444 -by( split_all_tac 1);
  12.445 -by( Asm_full_simp_tac 1);
  12.446 -bind_thm ("is_type_fields", result() RS bspec);
  12.447 +by Auto_tac;
  12.448 +qed_spec_mp "fields_is_type_lemma";
  12.449 +
  12.450 +Goal "[|map_of (fields (G,C)) fn = Some f; wf_prog wf_mb G; is_class G C|] ==> \
  12.451 +\ is_type G f";
  12.452 +by(dtac map_of_SomeD 1);
  12.453 +by(datac fields_is_type_lemma 2 1);
  12.454 +by(Auto_tac);
  12.455 +qed "fields_is_type";
  12.456 +
    13.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Wed Dec 06 19:09:34 2000 +0100
    13.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Dec 06 19:10:36 2000 +0100
    13.3 @@ -30,14 +30,12 @@
    13.4  
    13.5   wf_cdecl :: "'c wf_mb => 'c prog => 'c cdecl => bool"
    13.6  "wf_cdecl wf_mb G ==
    13.7 -   \\<lambda>(C,(sc,fs,ms)).
    13.8 -  (\\<forall>f\\<in>set fs. wf_fdecl G   f    ) \\<and>  unique fs \\<and>
    13.9 +   \\<lambda>(C,(D,fs,ms)).
   13.10 +  (\\<forall>f\\<in>set fs. wf_fdecl G         f) \\<and>  unique fs \\<and>
   13.11    (\\<forall>m\\<in>set ms. wf_mdecl wf_mb G C m) \\<and>  unique ms \\<and>
   13.12 -  (case sc of None => C = Object
   13.13 -         | Some D =>
   13.14 -             is_class G D \\<and>  \\<not>  G\\<turnstile>D\\<preceq>C C \\<and>
   13.15 -             (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
   13.16 -                 method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
   13.17 +  (C \\<noteq> Object \\<longrightarrow> is_class G D \\<and>  \\<not>G\\<turnstile>D\\<preceq>C C \\<and>
   13.18 +                   (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
   13.19 +                      method(G,D) sig = Some(D',rT',b') --> G\\<turnstile>rT\\<preceq>rT'))"
   13.20  
   13.21   wf_prog :: "'c wf_mb => 'c prog => bool"
   13.22  "wf_prog wf_mb G ==
    14.1 --- a/src/HOL/MicroJava/J/WellType.ML	Wed Dec 06 19:09:34 2000 +0100
    14.2 +++ b/src/HOL/MicroJava/J/WellType.ML	Wed Dec 06 19:10:36 2000 +0100
    14.3 @@ -13,18 +13,18 @@
    14.4  
    14.5  
    14.6  Goal
    14.7 -"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G|] ==> \
    14.8 -\ \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
    14.9 -\ 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)";
   14.10 +"[|method (G,C) sig = Some (md,rT,b); G\\<turnstile>T''\\<preceq>C C; wf_prog wf_mb G; \
   14.11 +\ class G C = Some y|] ==> \\<exists>T' rT' b. method (G,T'') sig = Some (T',rT',b) \\<and> \
   14.12 +\ 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)"; 
   14.13  by( datac widen_methd 2 1);
   14.14 -by( Clarsimp_tac 1);
   14.15 +by( Clarify_tac 1);
   14.16 +by( ftac subcls_is_class2 1);
   14.17 +by (Asm_simp_tac 1);
   14.18  by( dtac method_wf_mdecl 1);
   14.19 -by(  atac 1);
   14.20  by( rewtac wf_mdecl_def);
   14.21  by Auto_tac;
   14.22  qed "Call_lemma";
   14.23  
   14.24 -
   14.25  Goal "wf_prog wf_mb G ==> method (G,Object) sig = None";
   14.26  by (Asm_simp_tac 1);
   14.27  qed "method_Object";
   14.28 @@ -42,9 +42,32 @@
   14.29  by (Fast_tac 1);
   14.30  qed "appl_methsD";
   14.31  
   14.32 -val is_type_typeof = prove_goal thy 
   14.33 -	"(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and>  is_type G T)" (K [
   14.34 -	rtac val_.induct 1,
   14.35 -	    Fast_tac 5,
   14.36 -	   ALLGOALS Simp_tac]) RS mp;
   14.37 +bind_thm ("max_spec2mheads", insertI1 RSN (2,(equalityD2 RS subsetD)) RS 
   14.38 +                      max_spec2appl_meths RS appl_methsD);
   14.39 +
   14.40 +Goal "(\\<forall>a. v \\<noteq> Addr a) --> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)";
   14.41 +by (rtac val_.induct 1);
   14.42 +by (Fast_tac 5);
   14.43 +by Auto_tac;
   14.44 +qed_spec_mp "is_type_typeof";
   14.45  Addsimps [is_type_typeof];
   14.46 +
   14.47 +Goal "typeof (\\<lambda>a. None) v = Some T \\<longrightarrow> is_type G T";
   14.48 +by (rtac val_.induct 1);
   14.49 +by     Auto_tac;
   14.50 +qed_spec_mp "typeof_empty_is_type";
   14.51 +
   14.52 +Goal "wf_prog wf_mb G \\<Longrightarrow> ((G,L)\\<turnstile>e::T \\<longrightarrow> is_type G T) \\<and> \
   14.53 +\      ((G,L)\\<turnstile>es[::]Ts \\<longrightarrow> Ball (set Ts) (is_type G)) \\<and> ((G,L)\\<turnstile>c \\<surd> \\<longrightarrow> True)";
   14.54 +by (rtac ty_expr_ty_exprs_wt_stmt.induct 1);
   14.55 +by Auto_tac;
   14.56 +by (   etac typeof_empty_is_type 1);
   14.57 +by (  asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
   14.58 +by ( dtac field_fields 1);
   14.59 +by ( datac fields_is_type 1 1);
   14.60 +by (  Asm_simp_tac 1);
   14.61 +ba 1;
   14.62 +by (auto_tac (claset() addSDs [max_spec2mheads,method_wf_mdecl,is_type_rTI], simpset()addsimps[wf_mdecl_def]));
   14.63 +qed "wt_is_type";
   14.64 +
   14.65 +bind_thm ("ty_expr_is_type", permute_prems 0 1 (wt_is_type RS conjunct1 RS mp));
    15.1 --- a/src/HOL/MicroJava/J/WellType.thy	Wed Dec 06 19:09:34 2000 +0100
    15.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Wed Dec 06 19:10:36 2000 +0100
    15.3 @@ -95,7 +95,7 @@
    15.4           E\\<turnstile>NewC C::Class C"
    15.5  
    15.6    (* cf. 15.15 *)
    15.7 -  Cast  "[| E\\<turnstile>e::Class C;
    15.8 +  Cast  "[| E\\<turnstile>e::Class C; is_class (prg E) D;
    15.9              prg E\\<turnstile>C\\<preceq>? D |] ==>
   15.10           E\\<turnstile>Cast D e::Class D"
   15.11