re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
authoroheimb
Fri Jul 14 16:32:51 2000 +0200 (2000-07-14)
changeset 9346297dcbf64526
parent 9345 2f5f6824f888
child 9347 1791a62b33e7
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
src/HOL/IsaMakefile
src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Decl.thy
src/HOL/MicroJava/J/Eval.ML
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/Example.ML
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JTypeSafe.ML
src/HOL/MicroJava/J/Prog.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/Term.thy
src/HOL/MicroJava/J/Type.ML
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/Value.thy
src/HOL/MicroJava/J/WellForm.ML
src/HOL/MicroJava/J/WellType.thy
src/HOL/MicroJava/JVM/Object.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Jul 14 16:32:44 2000 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jul 14 16:32:51 2000 +0200
     1.3 @@ -329,14 +329,15 @@
     1.4  HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
     1.5  
     1.6  $(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \
     1.7 -  MicroJava/J/Conform.ML MicroJava/J/Conform.thy MicroJava/J/Decl.thy \
     1.8 +  MicroJava/J/Conform.ML MicroJava/J/Conform.thy \
     1.9    MicroJava/J/Eval.thy MicroJava/J/Eval.ML MicroJava/J/JBasis.ML \
    1.10    MicroJava/J/JBasis.thy MicroJava/J/JTypeSafe.thy MicroJava/J/JTypeSafe.ML \
    1.11 -  MicroJava/J/Prog.thy MicroJava/J/Prog.ML MicroJava/J/State.ML \
    1.12 -  MicroJava/J/State.thy MicroJava/J/Term.thy MicroJava/J/Type.ML \
    1.13 +  MicroJava/J/Decl.thy MicroJava/J/Decl.ML MicroJava/J/State.ML \
    1.14 +  MicroJava/J/State.thy MicroJava/J/Term.thy \
    1.15    MicroJava/J/Type.thy MicroJava/J/TypeRel.ML MicroJava/J/TypeRel.thy \
    1.16 -  MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML \
    1.17 +  MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML MicroJava/J/Value.thy \
    1.18    MicroJava/J/WellType.ML MicroJava/J/WellType.thy \
    1.19 +  MicroJava/J/Example.ML MicroJava/J/Example.thy \
    1.20    MicroJava/JVM/Control.thy MicroJava/JVM/JVMExec.thy \
    1.21    MicroJava/JVM/JVMState.thy MicroJava/JVM/LoadAndStore.thy \
    1.22    MicroJava/JVM/Method.thy MicroJava/JVM/Object.thy MicroJava/JVM/Opstack.thy \
     2.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Fri Jul 14 16:32:44 2000 +0200
     2.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Fri Jul 14 16:32:51 2000 +0200
     2.3 @@ -108,10 +108,8 @@
     2.4  (**** CH ****)
     2.5  
     2.6  Goalw [cast_ok_def]
     2.7 - "\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G (Class C) h v ; G\\<turnstile>(Class C)\\<preceq>T'; is_class G C \\<rbrakk> \
     2.8 + "\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G (ClassT C) h v ; G\\<turnstile>(Class C)\\<preceq>T'; is_class G C \\<rbrakk> \
     2.9  \ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
    2.10 -be disjE 1;
    2.11 - by (Clarify_tac 1);
    2.12  by (forward_tac [widen_Class] 1);
    2.13  by (Clarify_tac 1);
    2.14  be disjE 1;
     3.1 --- a/src/HOL/MicroJava/J/Conform.thy	Fri Jul 14 16:32:44 2000 +0200
     3.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Fri Jul 14 16:32:51 2000 +0200
     3.3 @@ -6,7 +6,9 @@
     3.4  Conformity relations for type safety of Java
     3.5  *)
     3.6  
     3.7 -Conform = State +
     3.8 +Conform = State + WellType +
     3.9 +
    3.10 +types	'c env_ = "'c prog \\<times> (vname \\<leadsto> ty)" (* same as env of WellType.thy *)
    3.11  
    3.12  constdefs
    3.13  
    3.14 @@ -26,7 +28,7 @@
    3.15    hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool"             ("_\\<turnstile>h _\\<surd>"      [51,51]       50)
    3.16   "G\\<turnstile>h h\\<surd>    \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
    3.17  
    3.18 -  conforms :: "state \\<Rightarrow> java_mb env \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
    3.19 +  conforms :: "state \\<Rightarrow> java_mb env_ \\<Rightarrow> bool"	 ("_\\<Colon>\\<preceq>_"       [51,51]       50)
    3.20   "s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
    3.21  
    3.22  end
     4.1 --- a/src/HOL/MicroJava/J/Decl.thy	Fri Jul 14 16:32:44 2000 +0200
     4.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Fri Jul 14 16:32:51 2000 +0200
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     David von Oheimb
     4.5      Copyright   1997 Technische Universitaet Muenchen
     4.6  
     4.7 -Class declarations
     4.8 +Class declarations and programs
     4.9  *)
    4.10  
    4.11  Decl = Type +
    4.12 @@ -34,4 +34,24 @@
    4.13  
    4.14   ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
    4.15  
    4.16 +
    4.17 +types 'c prog = "'c cdecl list"
    4.18 +
    4.19 +consts
    4.20 +
    4.21 +  class		:: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
    4.22 +
    4.23 +  is_class	:: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
    4.24 +  is_type	:: "'c prog \\<Rightarrow> ty    \\<Rightarrow> bool"
    4.25 +
    4.26 +defs
    4.27 +
    4.28 +  class_def	"class        \\<equiv> map_of"
    4.29 +
    4.30 +  is_class_def	"is_class G C \\<equiv> class G C \\<noteq> None"
    4.31 +
    4.32 +primrec
    4.33 +"is_type G (PrimT pt) = True"
    4.34 +"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"
    4.35 +
    4.36  end
     5.1 --- a/src/HOL/MicroJava/J/Eval.ML	Fri Jul 14 16:32:44 2000 +0200
     5.2 +++ b/src/HOL/MicroJava/J/Eval.ML	Fri Jul 14 16:32:51 2000 +0200
     5.3 @@ -4,6 +4,14 @@
     5.4      Copyright   1999 Technische Universitaet Muenchen
     5.5  *)
     5.6  
     5.7 +Goal "\\<lbrakk>new_Addr (heap s) = (a,x); \
     5.8 +\      s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)\\<rbrakk> \\<Longrightarrow> \
     5.9 +\      G\\<turnstile>Norm s -NewC C\\<succ>Addr a\\<rightarrow> s'";
    5.10 +by (hyp_subst_tac 1);
    5.11 +br eval_evals_exec.NewC 1;
    5.12 +by Auto_tac;
    5.13 +qed "NewCI";
    5.14 +
    5.15  Goal "\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ>  v \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
    5.16  \             (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
    5.17  \             (G\\<turnstile>(x,s) -c       \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None)";
     6.1 --- a/src/HOL/MicroJava/J/Eval.thy	Fri Jul 14 16:32:44 2000 +0200
     6.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Fri Jul 14 16:32:51 2000 +0200
     6.3 @@ -7,7 +7,7 @@
     6.4  execution of Java expressions and statements
     6.5  *)
     6.6  
     6.7 -Eval = State + 
     6.8 +Eval = State + WellType +
     6.9  
    6.10  consts
    6.11    eval  :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr      \\<times> val      \\<times> xstate) set"
    6.12 @@ -73,7 +73,7 @@
    6.13  	  G\\<turnstile>(np a' x1,s1) -e2\\<succ>v \\<rightarrow> (x2,s2);
    6.14  	  h = heap s2; (c,fs) = the (h a);
    6.15  	  h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))\\<rbrakk> \\<Longrightarrow>
    6.16 -			  G\\<turnstile>Norm s0 -{T}e1..fn\\<in>=e2\\<succ>v\\<rightarrow> c_hupd h' (x2,s2)"
    6.17 +			  G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v\\<rightarrow> c_hupd h' (x2,s2)"
    6.18  
    6.19    (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
    6.20    Call	"\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a';
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/MicroJava/J/Example.ML	Fri Jul 14 16:32:51 2000 +0200
     7.3 @@ -0,0 +1,263 @@
     7.4 +open Example;
     7.5 +
     7.6 +AddIs [widen.null];
     7.7 +
     7.8 +Addsimps [inj_cnam_, inj_vnam_];
     7.9 +Addsimps [Base_not_Object,Ext_not_Object];
    7.10 +Addsimps [Base_not_Object RS not_sym,Ext_not_Object RS not_sym];
    7.11 +
    7.12 +val map_of_Cons = prove_goalw thy [get_def thy "map_of_list"] 
    7.13 +"map_of (p#ps) = (map_of ps)(fst p |-> snd p)" (K [Simp_tac 1]);
    7.14 +val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"] 
    7.15 +"map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]);
    7.16 +val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"] 
    7.17 +"\\<And>X. x\\<noteq>k \\<Longrightarrow> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
    7.18 +Delsimps[map_of_Cons]; (* sic! *)
    7.19 +Addsimps[map_of_Cons1, map_of_Cons2];
    7.20 +
    7.21 +val class_tprg_Object = prove_goalw thy [class_def, ObjectC_def] 
    7.22 + 	"class tprg Object = Some (None, [], [])" 
    7.23 +	(K [Simp_tac 1]);
    7.24 +val class_tprg_Base = prove_goalw thy [class_def, ObjectC_def, BaseC_def, 
    7.25 + ExtC_def] "class tprg Base = Some (Some Object, \
    7.26 +	\ [(vee, PrimT Boolean)], \
    7.27 +        \ [((foo, [Class Base]), Class Base, foo_Base)])" (K [
    7.28 +	Simp_tac 1]);
    7.29 +val class_tprg_Ext = prove_goalw thy [class_def, ObjectC_def, BaseC_def, 
    7.30 + ExtC_def] "class tprg Ext = Some (Some Base, \
    7.31 +	\ [(vee, PrimT Integer)], \
    7.32 +        \ [((foo, [Class Base]), Class Ext, foo_Ext)])" (K [
    7.33 +	Simp_tac 1]);
    7.34 +Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];
    7.35 +
    7.36 +Goal "\\<And>X. (Object,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
    7.37 +by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
    7.38 +qed "not_Object_subcls";
    7.39 +AddSEs [not_Object_subcls];
    7.40 +
    7.41 +Goal "tprg\\<turnstile>Object\\<preceq>C C \\<Longrightarrow> C = Object";
    7.42 +be rtrancl_induct 1;
    7.43 +by  Auto_tac;
    7.44 +bd subcls1D 1;
    7.45 +by Auto_tac;
    7.46 +qed "subcls_ObjectD";
    7.47 +AddSDs[subcls_ObjectD];
    7.48 +
    7.49 +Goal "\\<And>X. (Base, Ext) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
    7.50 +by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
    7.51 +qed "not_Base_subcls_Ext";
    7.52 +AddSEs [not_Base_subcls_Ext];
    7.53 +
    7.54 +Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z \\<Longrightarrow> C=Object \\<or> C=Base \\<or> C=Ext";
    7.55 +by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm]));
    7.56 +qed "class_tprgD";
    7.57 +
    7.58 +Goal "(C,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
    7.59 +by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
    7.60 +by (ftac class_tprgD 1);
    7.61 +by (auto_tac (claset() addSDs [],simpset()));
    7.62 +bd rtranclD 1;
    7.63 +by Auto_tac;
    7.64 +qed "not_class_subcls_class";
    7.65 +AddSEs [not_class_subcls_class];
    7.66 +
    7.67 +goalw thy [ObjectC_def, BaseC_def, ExtC_def] "unique tprg";
    7.68 +by (Simp_tac 1);
    7.69 +qed "unique_classes";
    7.70 +
    7.71 +bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl);
    7.72 +
    7.73 +Goalw [] "tprg\\<turnstile>Ext\\<preceq>C Base";
    7.74 +br subcls_direct 1;
    7.75 +by (Simp_tac 1);
    7.76 +qed "Ext_subcls_Base";
    7.77 +Addsimps [Ext_subcls_Base];
    7.78 +
    7.79 +Goalw [] "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
    7.80 +br widen.subcls 1;
    7.81 +by (Simp_tac 1);
    7.82 +qed "Ext_widen_Base";
    7.83 +Addsimps [Ext_widen_Base];
    7.84 +
    7.85 +AddSIs ty_expr_ty_exprs_wt_stmt.intrs;
    7.86 +
    7.87 +
    7.88 +Goal "acyclic (subcls1 tprg)";
    7.89 +br acyclicI 1;
    7.90 +by Safe_tac ;
    7.91 +qed "acyclic_subcls1_";
    7.92 +
    7.93 +val wf_subcls1_=acyclic_subcls1_ RS(finite_subcls1 RS finite_acyclic_wf_converse);
    7.94 +
    7.95 +
    7.96 +Addsimps[is_class_def];
    7.97 +
    7.98 +val fields_rec_ = wf_subcls1_ RSN (1, fields_rec_lemma);
    7.99 +
   7.100 +Goal "fields (tprg, Object) = []";
   7.101 +by (stac fields_rec_ 1);
   7.102 +by   Auto_tac;
   7.103 +qed "fields_Object";
   7.104 +Addsimps [fields_Object];
   7.105 +
   7.106 +Goal "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]";
   7.107 +by (stac fields_rec_ 1);
   7.108 +by   Auto_tac;
   7.109 +qed "fields_Base";
   7.110 +Addsimps [fields_Base];
   7.111 +
   7.112 +Goal "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @\
   7.113 +                                    \ fields (tprg, Base)";
   7.114 +br trans 1;
   7.115 +br  fields_rec_ 1;
   7.116 +by   Auto_tac;
   7.117 +qed "fields_Ext";
   7.118 +Addsimps [fields_Ext];
   7.119 +
   7.120 +val method_rec_ = wf_subcls1_ RS method_rec_lemma;
   7.121 +
   7.122 +Goal "method (tprg,Object) = map_of []";
   7.123 +by (stac method_rec_ 1);
   7.124 +by  Auto_tac;
   7.125 +qed "method_Object";
   7.126 +Addsimps [method_Object];
   7.127 +
   7.128 +Goal "method (tprg, Base) = map_of \
   7.129 +\ [((foo, [Class Base]), Base, (Class Base, foo_Base))]";
   7.130 +br trans 1;
   7.131 +br  method_rec_ 1;
   7.132 +by  Auto_tac;
   7.133 +qed "method_Base";
   7.134 +Addsimps [method_Base];
   7.135 +
   7.136 +Goal "method (tprg, Ext) = (method (tprg, Base) \\<oplus> map_of \
   7.137 +\ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])";
   7.138 +br trans 1;
   7.139 +br  method_rec_ 1;
   7.140 +by  Auto_tac;
   7.141 +qed "method_Ext";
   7.142 +Addsimps [method_Ext];
   7.143 +
   7.144 +Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Base_def] 
   7.145 +"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))";
   7.146 +by Auto_tac;
   7.147 +qed "wf_foo_Base";
   7.148 +
   7.149 +Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Ext_def] 
   7.150 +"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))";
   7.151 +by Auto_tac;
   7.152 +br  ty_expr_ty_exprs_wt_stmt.Cast 1;
   7.153 +by   (Simp_tac 2);
   7.154 +br   cast.subcls 2;
   7.155 +by   (rewtac field_def);
   7.156 +by   Auto_tac;
   7.157 +qed "wf_foo_Ext";
   7.158 +
   7.159 +Goalw [wf_cdecl_def, wf_fdecl_def, ObjectC_def] 
   7.160 +"wf_cdecl wf_java_mdecl tprg ObjectC";
   7.161 +by (Simp_tac 1);
   7.162 +qed "wf_ObjectC";
   7.163 +
   7.164 +Goalw [wf_cdecl_def, wf_fdecl_def, BaseC_def] 
   7.165 +"wf_cdecl wf_java_mdecl tprg BaseC";
   7.166 +by (Simp_tac 1);
   7.167 +by (fold_goals_tac [BaseC_def]);
   7.168 +br (wf_foo_Base RS conjI) 1;
   7.169 +by Auto_tac;
   7.170 +qed "wf_BaseC";
   7.171 +
   7.172 +Goalw [wf_cdecl_def, wf_fdecl_def, ExtC_def] 
   7.173 +"wf_cdecl wf_java_mdecl tprg ExtC";
   7.174 +by (Simp_tac 1);
   7.175 +by (fold_goals_tac [ExtC_def]);
   7.176 +br (wf_foo_Ext RS conjI) 1;
   7.177 +by Auto_tac;
   7.178 +bd rtranclD 1;
   7.179 +by Auto_tac;
   7.180 +qed "wf_ExtC";
   7.181 +
   7.182 +Goalw [wf_prog_def,Let_def] 
   7.183 +"wf_prog wf_java_mdecl tprg";
   7.184 +by(simp_tac (simpset() addsimps [wf_ObjectC,wf_BaseC,wf_ExtC,unique_classes])1);
   7.185 +qed "wf_tprg";
   7.186 +
   7.187 +Goalw [appl_methds_def] 
   7.188 +"appl_methds tprg Base (foo, [NT]) = \
   7.189 +\ {((Class Base, Class Base), [Class Base])}";
   7.190 +by (Simp_tac 1);
   7.191 +by (subgoal_tac "tprg\\<turnstile>NT\\<preceq> Class Base" 1);
   7.192 +by  (auto_tac (claset(), simpset() addsimps [map_of_Cons,foo_Base_def]));
   7.193 +qed "appl_methds_foo_Base";
   7.194 +
   7.195 +Goalw [max_spec_def] "max_spec tprg Base (foo, [NT]) = \
   7.196 +\ {((Class Base, Class Base), [Class Base])}";
   7.197 +by (auto_tac (claset(), simpset() addsimps [appl_methds_foo_Base]));
   7.198 +qed "max_spec_foo_Base";
   7.199 +
   7.200 +fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
   7.201 +Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\ 
   7.202 +\ Expr(e\\<Colon>=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
   7.203 +(* ?pTs' = [Class Base] *)
   7.204 +by t;		(* ;; *)
   7.205 +by  t;		(* Expr *)
   7.206 +by  t;		(* LAss *)
   7.207 +by    t;	(* LAcc *)
   7.208 +by     (Simp_tac 1);
   7.209 +by    (Simp_tac 1);
   7.210 +by   t;	(* NewC *)
   7.211 +by   (Simp_tac 1);
   7.212 +by  (Simp_tac 1);
   7.213 +by t;	(* Expr *)
   7.214 +by t;	(* Call *)
   7.215 +by   t;	(* LAcc *)
   7.216 +by    (Simp_tac 1);
   7.217 +by   (Simp_tac 1);
   7.218 +by  t;	(* Cons *)
   7.219 +by   t;	(* Lit *)
   7.220 +by   (Simp_tac 1);
   7.221 +by  t;	(* Nil *)
   7.222 +by (Simp_tac 1);
   7.223 +br max_spec_foo_Base 1;
   7.224 +qed "wt_test";
   7.225 +
   7.226 +fun e thm = resolve_tac (NewCI::eval_evals_exec.intrs) 1 thm;
   7.227 +
   7.228 +Delsplits[split_if];
   7.229 +Addsimps[init_vars_def,c_hupd_def,cast_ok_def];
   7.230 +Goalw [test_def] 
   7.231 +" \\<lbrakk>new_Addr (heap (snd s0)) = (a, None)\\<rbrakk> \\<Longrightarrow> \
   7.232 +\ tprg\\<turnstile>s0 -test\\<rightarrow> ?s";
   7.233 +(* ?s = s3 *)
   7.234 +by e;		(* ;; *)
   7.235 +by  e;		(* Expr *)
   7.236 +by  e;		(* LAss *)
   7.237 +by   e;	(* NewC *)
   7.238 +by    (Force_tac 1);
   7.239 +by   (Force_tac 1);
   7.240 +by  (Simp_tac 1);
   7.241 +be thin_rl 1;
   7.242 +by e;	(* Expr *)
   7.243 +by e;	(* Call *)
   7.244 +by       e;	(* LAcc *)
   7.245 +by      (Force_tac 1);
   7.246 +by     e;	(* Cons *)
   7.247 +by      e;	(* Lit *)
   7.248 +by     e;	(* Nil *)
   7.249 +by    (Simp_tac 1);
   7.250 +by   (force_tac (claset(), simpset() addsimps [foo_Ext_def]) 1);
   7.251 +by  (Simp_tac 1);
   7.252 +by  e;	(* Expr *)
   7.253 +by  e;	(* FAss *)
   7.254 +by       e;(* Cast *)
   7.255 +by        e;(* LAcc *)
   7.256 +by       (Simp_tac 1);
   7.257 +by      (Simp_tac 1);
   7.258 +by     (Simp_tac 1);
   7.259 +by     e;(* XcptE *)
   7.260 +by    (Simp_tac 1);
   7.261 +by   (EVERY'[rtac (surjective_pairing RS sym RSN (2,trans)), stac Pair_eq,
   7.262 +             Force_tac] 1);
   7.263 +by  (Simp_tac 1);
   7.264 +by (Simp_tac 1);
   7.265 +by e;	(* XcptE *)
   7.266 +qed "exec_test";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/MicroJava/J/Example.thy	Fri Jul 14 16:32:51 2000 +0200
     8.3 @@ -0,0 +1,117 @@
     8.4 +(*  Title:      isabelle/Bali/Example.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     David von Oheimb
     8.7 +    Copyright   1997 Technische Universitaet Muenchen
     8.8 +
     8.9 +The following example Bali program includes:
    8.10 + class declarations with inheritance, hiding of fields, and overriding of
    8.11 +  methods (with refined result type), 
    8.12 + instance creation, local assignment, sequential composition,
    8.13 + method call with dynamic binding, literal values,
    8.14 + expression statement, local access, type cast, field assignment (in part), skip
    8.15 +
    8.16 +class Base {
    8.17 +  boolean vee;
    8.18 +  Base foo(Base x) {return x;}
    8.19 +}
    8.20 +
    8.21 +class Ext extends Base{
    8.22 +  int vee;
    8.23 +  Ext foo(Base x) {((Ext)x).vee=1; return null;}
    8.24 +}
    8.25 +
    8.26 +class Example {
    8.27 +  public static void main (String args[]) {
    8.28 +    Base e;
    8.29 +    e=new Ext();
    8.30 +    try {e.foo(null); }
    8.31 +    catch (NullPointerException x) {}
    8.32 +  }
    8.33 +}
    8.34 +*)
    8.35 +
    8.36 +Example = Eval + 
    8.37 +
    8.38 +datatype cnam_ = Base_ | Ext_
    8.39 +datatype vnam_ = vee_ | x_ | e_
    8.40 +
    8.41 +consts
    8.42 +
    8.43 +  cnam_ :: "cnam_ \\<Rightarrow> cname"
    8.44 +  vnam_ :: "vnam_ \\<Rightarrow> vnam"
    8.45 +
    8.46 +rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
    8.47 +
    8.48 +  inj_cnam_  "(cnam_ x = cnam_ y) = (x = y)"
    8.49 +  inj_vnam_  "(vnam_ x = vnam_ y) = (x = y)"
    8.50 +
    8.51 +  surj_cnam_ "\\<exists>m. n = cnam_ m"
    8.52 +  surj_vnam_ "\\<exists>m. n = vnam_ m"
    8.53 +
    8.54 +syntax
    8.55 +
    8.56 +  Base,  Ext	:: cname
    8.57 +  vee, x, e	:: vname
    8.58 +
    8.59 +translations
    8.60 +
    8.61 +  "Base" == "cnam_ Base_"
    8.62 +  "Ext"	 == "cnam_ Ext_"
    8.63 +  "vee"  == "VName (vnam_ vee_)"
    8.64 +  "x"	 == "VName (vnam_ x_)"
    8.65 +  "e"	 == "VName (vnam_ e_)"
    8.66 +
    8.67 +rules
    8.68 +  Base_not_Object "Base \\<noteq> Object"
    8.69 +  Ext_not_Object  "Ext  \\<noteq> Object"
    8.70 +
    8.71 +consts
    8.72 +
    8.73 +  foo_Base       :: java_mb
    8.74 +  foo_Ext        :: java_mb
    8.75 +  BaseC, ExtC    :: java_mb cdecl
    8.76 +  test		 :: stmt
    8.77 +  foo	         :: mname
    8.78 +  a,b		 :: loc
    8.79 +
    8.80 +defs
    8.81 +
    8.82 +  foo_Base_def "foo_Base \\<equiv> ([x],[],Skip,LAcc x)"
    8.83 +  BaseC_def "BaseC \\<equiv> (Base, (Some Object, 
    8.84 +			     [(vee, PrimT Boolean)], 
    8.85 +			     [((foo,[Class Base]),Class Base,foo_Base)]))"
    8.86 +  foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast (ClassT Ext)
    8.87 +					(LAcc x)..vee:=Lit (Intg #1)),
    8.88 +				   Lit Null)"
    8.89 +  ExtC_def  "ExtC  \\<equiv> (Ext,  (Some Base  , 
    8.90 +			     [(vee, PrimT Integer)], 
    8.91 +			     [((foo,[Class Base]),Class Ext,foo_Ext)]))"
    8.92 +
    8.93 +  test_def "test \\<equiv> Expr(e\\<Colon>=NewC Ext);; 
    8.94 +		    Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
    8.95 +
    8.96 +
    8.97 +
    8.98 +
    8.99 +
   8.100 +
   8.101 +
   8.102 +
   8.103 +syntax
   8.104 +
   8.105 +  NP		:: xcpt
   8.106 +  tprg 	 	:: java_mb prog
   8.107 +  obj1, obj2	:: obj
   8.108 +  s0,s1,s2,s3,s4:: state
   8.109 +
   8.110 +translations
   8.111 +
   8.112 +  "NP"      == "NullPointer"
   8.113 +  "tprg" == "[ObjectC, BaseC, ExtC]"
   8.114 +  "obj1"    <= "(Ext, empty((vee, Base)\\<mapsto>Bool False)
   8.115 +			   ((vee, Ext )\\<mapsto>Intg #0))"
   8.116 +  "s0" == " Norm    (empty          ,empty                        )"
   8.117 +  "s1" == " Norm    (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a)             )"
   8.118 +  "s2" == " Norm    (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
   8.119 +  "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
   8.120 +end
     9.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML	Fri Jul 14 16:32:44 2000 +0200
     9.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Fri Jul 14 16:32:51 2000 +0200
     9.3 @@ -6,19 +6,6 @@
     9.4  Type safety proof
     9.5  *)
     9.6  
     9.7 -Goalw [conf_def] "G,s\\<turnstile>Unit\\<Colon>\\<preceq>PrimT Void";
     9.8 -by( Simp_tac 1);
     9.9 -qed "conf_VoidI";
    9.10 -
    9.11 -Goalw [conf_def] "G,s\\<turnstile>Bool b\\<Colon>\\<preceq>PrimT Boolean";
    9.12 -by( Simp_tac 1);
    9.13 -qed "conf_BooleanI";
    9.14 -
    9.15 -Goalw [conf_def] "G,s\\<turnstile>Intg i\\<Colon>\\<preceq>PrimT Integer";
    9.16 -by( Simp_tac 1);
    9.17 -qed "conf_IntegerI";
    9.18 -
    9.19 -Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
    9.20  
    9.21  Addsimps [split_beta];
    9.22  
    9.23 @@ -30,8 +17,8 @@
    9.24  qed "NewC_conforms";
    9.25  
    9.26  Goalw [cast_ok_def]
    9.27 - "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<preceq>? T'; cast_ok G T' h v\\<rbrakk> \
    9.28 -\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
    9.29 + "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<preceq>? RefT T'; cast_ok G T' h v\\<rbrakk> \
    9.30 +\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>RefT T'";
    9.31  by( case_tac1 "v = Null" 1);
    9.32  by(  Asm_full_simp_tac 1);
    9.33  by(  dtac widen_RefT 1);
    9.34 @@ -39,15 +26,7 @@
    9.35  by(  forward_tac [cast_RefT] 1);
    9.36  by(  Clarify_tac 1);
    9.37  by(  rtac widen.null 1);
    9.38 -by( case_tac1 "\\<exists>pt. T' = PrimT pt" 1);
    9.39 -by(  strip_tac1 1);
    9.40 -by(  dtac cast_PrimT2 1);
    9.41 -by(  etac conf_widen 1);
    9.42 -by(   atac 1);
    9.43 -by(  atac 1);
    9.44  by( Asm_full_simp_tac 1);
    9.45 -by( dtac (non_PrimT RS iffD1) 1);
    9.46 -by( strip_tac1 1);
    9.47  by( forward_tac [cast_RefT2] 1);
    9.48  by( strip_tac1 1);
    9.49  by( dtac non_npD 1);
    10.1 --- a/src/HOL/MicroJava/J/Prog.thy	Fri Jul 14 16:32:44 2000 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,30 +0,0 @@
    10.4 -(*  Title:      HOL/MicroJava/J/Prog.thy
    10.5 -    ID:         $Id$
    10.6 -    Author:     David von Oheimb
    10.7 -    Copyright   1999 Technische Universitaet Muenchen
    10.8 -
    10.9 -Java program = list of class declarations
   10.10 -*)
   10.11 -
   10.12 -Prog = Decl +
   10.13 -
   10.14 -types 'c prog = "'c cdecl list"
   10.15 -
   10.16 -consts
   10.17 -
   10.18 -  class		:: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
   10.19 -
   10.20 -  is_class	:: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
   10.21 -  is_type	:: "'c prog \\<Rightarrow> ty    \\<Rightarrow> bool"
   10.22 -
   10.23 -defs
   10.24 -
   10.25 -  class_def	"class        \\<equiv> map_of"
   10.26 -
   10.27 -  is_class_def	"is_class G C \\<equiv> class G C \\<noteq> None"
   10.28 -
   10.29 -primrec
   10.30 -"is_type G (PrimT pt) = True"
   10.31 -"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"
   10.32 -
   10.33 -end
    11.1 --- a/src/HOL/MicroJava/J/State.thy	Fri Jul 14 16:32:44 2000 +0200
    11.2 +++ b/src/HOL/MicroJava/J/State.thy	Fri Jul 14 16:32:51 2000 +0200
    11.3 @@ -6,38 +6,12 @@
    11.4  State for evaluation of Java expressions and statements
    11.5  *)
    11.6  
    11.7 -State = WellType +
    11.8 -
    11.9 -consts
   11.10 -  the_Bool	:: "val \\<Rightarrow> bool"
   11.11 -  the_Intg	:: "val \\<Rightarrow> int"
   11.12 -  the_Addr	:: "val \\<Rightarrow> loc"
   11.13 -
   11.14 -  defpval	:: "prim_ty \\<Rightarrow> val"	(* default value for primitive types *)
   11.15 -  default_val	:: "ty \\<Rightarrow> val"		(* default value for all types *)
   11.16 -
   11.17 -primrec
   11.18 - "the_Bool (Bool b) = b"
   11.19 -
   11.20 -primrec
   11.21 - "the_Intg (Intg i) = i"
   11.22 -
   11.23 -primrec
   11.24 - "the_Addr (Addr a) = a"
   11.25 -
   11.26 -primrec
   11.27 -	"defpval Void    = Unit"
   11.28 -	"defpval Boolean = Bool False"
   11.29 -	"defpval Integer = Intg (#0)"
   11.30 -
   11.31 -primrec
   11.32 -	"default_val (PrimT pt) = defpval pt"
   11.33 -	"default_val (RefT  r ) = Null"
   11.34 +State = TypeRel + Value +
   11.35  
   11.36  types	fields_
   11.37  	= "(vname \\<times> cname \\<leadsto> val)" (* field name, defining class, value *)
   11.38  
   11.39 -types obj = "cname \\<times> fields_"	(* class instance with class name and fields *)
   11.40 +        obj = "cname \\<times> fields_"	(* class instance with class name and fields *)
   11.41  
   11.42  constdefs
   11.43  
   11.44 @@ -86,7 +60,7 @@
   11.45    c_hupd	:: "aheap \\<Rightarrow> xstate \\<Rightarrow> xstate"
   11.46   "c_hupd h'\\<equiv> \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
   11.47  
   11.48 -  cast_ok	:: "'c prog \\<Rightarrow> ty \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
   11.49 - "cast_ok G T h v \\<equiv> ((\\<exists>pt. T = PrimT pt) | (v=Null) | G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq>T)"
   11.50 +  cast_ok	:: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
   11.51 + "cast_ok G T h v \\<equiv> (v=Null) | G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq>RefT T"
   11.52  
   11.53  end
    12.1 --- a/src/HOL/MicroJava/J/Term.thy	Fri Jul 14 16:32:44 2000 +0200
    12.2 +++ b/src/HOL/MicroJava/J/Term.thy	Fri Jul 14 16:32:51 2000 +0200
    12.3 @@ -6,33 +6,20 @@
    12.4  Java expressions and statements
    12.5  *)
    12.6  
    12.7 -Term = Type + 
    12.8 -
    12.9 -types   loc		(* locations, i.e. abstract references on objects *)
   12.10 -arities loc :: term
   12.11 -
   12.12 -datatype val_		(* name non 'val' because of clash with ML token *)
   12.13 -	= Unit		(* dummy result value of void methods *)
   12.14 -	| Null		(* null reference *)
   12.15 -	| Bool bool	(* Boolean value *)
   12.16 -	| Intg int	(* integer value *) (* Name Intg instead of Int because
   12.17 -					       of clash with HOL/Set.thy *)
   12.18 -	| Addr loc	(* addresses, i.e. locations of objects *)
   12.19 -types	val = val_
   12.20 -translations "val" <= (type) "val_"
   12.21 +Term = Value + 
   12.22  
   12.23  datatype binop = Eq | Add	   (* function codes for binary operation *)
   12.24  
   12.25  datatype expr
   12.26  	= NewC	cname		   (* class instance creation *)
   12.27 -	| Cast	ty expr		   (* type cast *)
   12.28 +	| Cast	ref_ty expr	   (* type cast *)
   12.29  	| Lit	val		   (* literal value, also references *)
   12.30          | BinOp binop  expr expr   (* binary operation *)
   12.31  	| LAcc vname		   (* local (incl. parameter) access *)
   12.32  	| LAss vname expr          (* local assign *) ("_\\<Colon>=_"  [      90,90]90)
   12.33  	| FAcc cname expr vname    (* field access *) ("{_}_.._"[10,90,99   ]90)
   12.34  	| FAss cname expr vname 
   12.35 -	                  expr     (* field ass. *)("{_}_.._\\<in>=_"[10,90,99,90]90)
   12.36 +	                  expr     (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
   12.37  	| Call expr mname (ty list) (expr list)(* method call*)
   12.38                                      ("_.._'({_}_')" [90,99,10,10] 90)
   12.39  and stmt
    13.1 --- a/src/HOL/MicroJava/J/Type.ML	Fri Jul 14 16:32:44 2000 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,10 +0,0 @@
    13.4 -(*  Title:      HOL/MicroJava/J/Type.ML
    13.5 -    ID:         $Id$
    13.6 -    Author:     David von Oheimb
    13.7 -    Copyright   1999 Technische Universitaet Muenchen
    13.8 -*)
    13.9 -
   13.10 -Goal "(\\<forall>pt. T \\<noteq> PrimT pt) = (\\<exists>t. T = RefT t)";
   13.11 -by(case_tac "T" 1);
   13.12 -by Auto_tac;
   13.13 -qed "non_PrimT";
    14.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 14 16:32:44 2000 +0200
    14.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 14 16:32:51 2000 +0200
    14.3 @@ -6,7 +6,7 @@
    14.4  The relations between Java types
    14.5  *)
    14.6  
    14.7 -TypeRel = Prog +
    14.8 +TypeRel = Decl +
    14.9  
   14.10  consts
   14.11    subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (*        subclass *)
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/MicroJava/J/Value.thy	Fri Jul 14 16:32:51 2000 +0200
    15.3 @@ -0,0 +1,51 @@
    15.4 +(*  Title:      HOL/MicroJava/J/Term.thy
    15.5 +    ID:         $Id$
    15.6 +    Author:     David von Oheimb
    15.7 +    Copyright   1999 Technische Universitaet Muenchen
    15.8 +
    15.9 +Java values
   15.10 +*)
   15.11 +
   15.12 +Value = Type +
   15.13 +
   15.14 +types   loc		(* locations, i.e. abstract references on objects *)
   15.15 +arities loc :: term
   15.16 +
   15.17 +datatype val_		(* name non 'val' because of clash with ML token *)
   15.18 +	= Unit		(* dummy result value of void methods *)
   15.19 +	| Null		(* null reference *)
   15.20 +	| Bool bool	(* Boolean value *)
   15.21 +	| Intg int	(* integer value *) (* Name Intg instead of Int because
   15.22 +					       of clash with HOL/Set.thy *)
   15.23 +	| Addr loc	(* addresses, i.e. locations of objects *)
   15.24 +types	val = val_
   15.25 +translations "val" <= (type) "val_"
   15.26 +
   15.27 +consts
   15.28 +  the_Bool	:: "val \\<Rightarrow> bool"
   15.29 +  the_Intg	:: "val \\<Rightarrow> int"
   15.30 +  the_Addr	:: "val \\<Rightarrow> loc"
   15.31 +
   15.32 +primrec
   15.33 + "the_Bool (Bool b) = b"
   15.34 +
   15.35 +primrec
   15.36 + "the_Intg (Intg i) = i"
   15.37 +
   15.38 +primrec
   15.39 + "the_Addr (Addr a) = a"
   15.40 +
   15.41 +consts
   15.42 +  defpval	:: "prim_ty \\<Rightarrow> val"	(* default value for primitive types *)
   15.43 +  default_val	:: "ty \\<Rightarrow> val"		(* default value for all types *)
   15.44 +
   15.45 +primrec
   15.46 +	"defpval Void    = Unit"
   15.47 +	"defpval Boolean = Bool False"
   15.48 +	"defpval Integer = Intg (#0)"
   15.49 +
   15.50 +primrec
   15.51 +	"default_val (PrimT pt) = defpval pt"
   15.52 +	"default_val (RefT  r ) = Null"
   15.53 +
   15.54 +end
    16.1 --- a/src/HOL/MicroJava/J/WellForm.ML	Fri Jul 14 16:32:44 2000 +0200
    16.2 +++ b/src/HOL/MicroJava/J/WellForm.ML	Fri Jul 14 16:32:51 2000 +0200
    16.3 @@ -95,36 +95,50 @@
    16.4  by( etac subcls1I 1);
    16.5  qed "subcls1_induct";
    16.6  
    16.7 -Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
    16.8 +Goal "\\<lbrakk>wf ((subcls1 G)^-1); \\<forall>D fs ms. class G C = Some (Some D,fs,ms) \\<longrightarrow> is_class G D\\<rbrakk> \\<Longrightarrow> method (G,C) = \
    16.9  \ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
   16.10  \ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
   16.11  \ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
   16.12  by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
   16.13 +by( asm_simp_tac (simpset() addsplits[option.split]) 1);
   16.14 +auto();
   16.15 +qed "method_rec_lemma";
   16.16 +
   16.17 +Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
   16.18 +\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
   16.19 +\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
   16.20 +\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
   16.21 +by(rtac method_rec_lemma 1);
   16.22  by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def] 
   16.23  		addsplits [option.split]) 1);
   16.24  by( case_tac "C = Object" 1);
   16.25 -by(  Asm_full_simp_tac 1);
   16.26 -by( dtac class_wf 1);
   16.27 -by(  atac 1);
   16.28 -by( dtac wf_cdecl_supD 1);
   16.29 -by(  atac 1);
   16.30 +by(  Force_tac 1);
   16.31 +by Safe_tac;
   16.32 +by( datac class_wf 1 1);
   16.33 +by( datac wf_cdecl_supD 1 1);
   16.34  by( Asm_full_simp_tac 1);
   16.35  qed "method_rec";
   16.36  
   16.37 +Goal "\\<lbrakk>wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\<forall>C. sc = Some C \\<longrightarrow> is_class G C\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
   16.38 +\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
   16.39 +\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
   16.40 +by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
   16.41 +by( asm_simp_tac (simpset() addsplits[option.split]) 1);
   16.42 +qed "fields_rec_lemma";
   16.43 +
   16.44  Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
   16.45  \ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
   16.46  \ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
   16.47 -by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
   16.48 -by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
   16.49 +by(rtac fields_rec_lemma 1);
   16.50 +by(   asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
   16.51 +ba  1;
   16.52  by( option_case_tac2 "sc" 1);
   16.53  by(  Asm_simp_tac 1);
   16.54  by( case_tac "C = Object" 1);
   16.55  by(  rotate_tac 2 1);
   16.56  by(  Asm_full_simp_tac 1);
   16.57 -by( dtac class_wf 1);
   16.58 -by(  atac 1);
   16.59 -by( dtac wf_cdecl_supD 1);
   16.60 -by(  atac 1);
   16.61 +by( datac class_wf 1 1);
   16.62 +by( datac wf_cdecl_supD 1 1);
   16.63  by( Asm_full_simp_tac 1);
   16.64  qed "fields_rec";
   16.65  
   16.66 @@ -211,12 +225,6 @@
   16.67  by( Asm_full_simp_tac 1);
   16.68  qed "unique_fields";
   16.69  
   16.70 -(*####TO Trancl.ML*)
   16.71 -Goal "(a,b):r^* ==> a=b | a~=b & (a,b):r^+";
   16.72 -by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym] 
   16.73 -				  delsimps [reflcl_trancl]) 1);
   16.74 -qed "rtranclD";
   16.75 -
   16.76  Goal
   16.77  "\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
   16.78  \                          map_of (fields (G,C')) f = Some ft";
    17.1 --- a/src/HOL/MicroJava/J/WellType.thy	Fri Jul 14 16:32:44 2000 +0200
    17.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Fri Jul 14 16:32:51 2000 +0200
    17.3 @@ -96,8 +96,8 @@
    17.4  
    17.5    (* cf. 15.15 *)
    17.6    Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>T;
    17.7 -	  prg E\\<turnstile>T\\<preceq>? T'\\<rbrakk> \\<Longrightarrow>
    17.8 -						 E\\<turnstile>Cast T' e\\<Colon>T'"
    17.9 +	  prg E\\<turnstile>T\\<preceq>? RefT rt\\<rbrakk> \\<Longrightarrow>
   17.10 +						 E\\<turnstile>Cast rt e\\<Colon>RefT rt"
   17.11  
   17.12    (* cf. 15.7.1 *)
   17.13    Lit	"\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
   17.14 @@ -129,7 +129,7 @@
   17.15    FAss  "\\<lbrakk>E\\<turnstile>{fd}a..fn\\<Colon>T;
   17.16  	  E\\<turnstile>v       \\<Colon>T';
   17.17  	  prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
   17.18 -					 	 E\\<turnstile>{fd}a..fn\\<in>=v\\<Colon>T'"
   17.19 +					 	 E\\<turnstile>{fd}a..fn:=v\\<Colon>T'"
   17.20  
   17.21  
   17.22    (* cf. 15.11.1, 15.11.2, 15.11.3 *)
    18.1 --- a/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 16:32:44 2000 +0200
    18.2 +++ b/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 16:32:51 2000 +0200
    18.3 @@ -65,7 +65,7 @@
    18.4  primrec
    18.5    "exec_ch (Checkcast C) G hp stk pc =
    18.6  	(let oref	= hd stk;
    18.7 -	     xp'	= raise_xcpt (\\<not> cast_ok G (Class C) hp oref) ClassCast;
    18.8 +	     xp'	= raise_xcpt (\\<not> cast_ok G (ClassT C) hp oref) ClassCast;
    18.9  	     stk'	= if xp'=None then stk else tl stk
   18.10  	 in
   18.11  	 (xp' , stk' , pc+1))"