# HG changeset patch
# User oheimb
# Date 963600431 -7200
# Node ID f495dba0cb07b23d7594942cbcb58c5755edf11e
# Parent  1791a62b33e714bc85b9ef807dabe7630a78c127
corrections (cast relation, Prog.ML -> Decl.ML)

diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Fri Jul 14 20:47:11 2000 +0200
@@ -108,8 +108,8 @@
 (**** CH ****)
 
 Goalw [cast_ok_def]
- "\\<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> \
-\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
+ "\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G C h v ; G\\<turnstile>Class C\\<preceq>T; is_class G C \\<rbrakk> \
+\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T";
 by (forward_tac [widen_Class] 1);
 by (Clarify_tac 1);
 be disjE 1;
@@ -135,7 +135,6 @@
 	addss (simpset() addsimps [map_eq_Cons,approx_val_def])) 1);
 qed "Checkcast_correct";
 
-
 Goal
 "\\<lbrakk> wt_jvm_prog G phi; \
 \  method (G,C) sig = Some (C,rT,maxl,ins); \
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/Decl.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Decl.ML	Fri Jul 14 20:47:11 2000 +0200
@@ -0,0 +1,15 @@
+(*  Title:      HOL/MicroJava/J/Decl.ML
+    ID:         $Id$
+    Author:     David von Oheimb
+    Copyright   1999 Technische Universitaet Muenchen
+*)
+
+val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
+	rtac finite_map_of 1]);
+
+val is_classI = prove_goalw thy [is_class_def]
+"\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]);
+
+val is_classD = prove_goalw thy [is_class_def]
+"\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
+	not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/Eval.thy
--- a/src/HOL/MicroJava/J/Eval.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -42,8 +42,8 @@
 
   (* cf. 15.15 *)
   Cast	"\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> (x1,s1);
-	  x2=raise_if (\\<not> cast_ok G T (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
-			        G\\<turnstile>Norm s0 -Cast T e\\<succ>v\\<rightarrow> (x2,s1)"
+	  x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
+			        G\\<turnstile>Norm s0 -Cast C e\\<succ>v\\<rightarrow> (x2,s1)"
 
   (* cf. 15.7.1 *)
   Lit				   "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/Example.ML
--- a/src/HOL/MicroJava/J/Example.ML	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.ML	Fri Jul 14 20:47:11 2000 +0200
@@ -260,4 +260,4 @@
 by  (Simp_tac 1);
 by (Simp_tac 1);
 by e;	(* XcptE *)
-qed "exec_test";
+bind_thm ("exec_test", simplify (simpset()) (result()));
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -80,8 +80,8 @@
   BaseC_def "BaseC \\<equiv> (Base, (Some Object, 
 			     [(vee, PrimT Boolean)], 
 			     [((foo,[Class Base]),Class Base,foo_Base)]))"
-  foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast (ClassT Ext)
-					(LAcc x)..vee:=Lit (Intg #1)),
+  foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast Ext
+				       (LAcc x)..vee:=Lit (Intg #1)),
 				   Lit Null)"
   ExtC_def  "ExtC  \\<equiv> (Ext,  (Some Base  , 
 			     [(vee, PrimT Integer)], 
@@ -113,5 +113,5 @@
   "s0" == " Norm    (empty          ,empty                        )"
   "s1" == " Norm    (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a)             )"
   "s2" == " Norm    (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
-  "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
+  "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
 end
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/JTypeSafe.ML
--- a/src/HOL/MicroJava/J/JTypeSafe.ML	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Fri Jul 14 20:47:11 2000 +0200
@@ -17,24 +17,15 @@
 qed "NewC_conforms";
 
 Goalw [cast_ok_def]
- "\\<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> \
-\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>RefT T'";
+ "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v\\<rbrakk> \
+\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>Class D";
 by( case_tac1 "v = Null" 1);
 by(  Asm_full_simp_tac 1);
 by(  dtac widen_RefT 1);
 by(  Clarify_tac 1);
-by(  forward_tac [cast_RefT] 1);
-by(  Clarify_tac 1);
 by(  rtac widen.null 1);
-by( Asm_full_simp_tac 1);
-by( forward_tac [cast_RefT2] 1);
-by( strip_tac1 1);
-by( dtac non_npD 1);
-by(  atac 1);
-by( rewrite_goals_tac [obj_ty_def]);
-by Auto_tac ;
-by(  ALLGOALS (rtac conf_AddrI));
-by     Auto_tac;
+by( datac non_npD 1 1);
+by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def]));
 qed "Cast_conf";
 
 Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
@@ -283,7 +274,7 @@
 by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
 
 by prune_params_tac;
-(* Level 45 *)
+(* Level 51 *)
 
 (* 1 Call *)
 by( case_tac "x" 1);
@@ -303,7 +294,8 @@
 by(  dtac eval_xcpt 1);
 by(  Asm_full_simp_tac 1);
 by(  fast_tac (HOL_cs addEs [hext_trans]) 1);
-by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) THEN_ALL_NEW Asm_simp_tac) 1);
+by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) 
+    THEN_ALL_NEW Asm_simp_tac) 1);
 qed "eval_evals_exec_type_sound";
 
 Goal "\\<And>E s s'. \
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/Prog.ML
--- a/src/HOL/MicroJava/J/Prog.ML	Fri Jul 14 17:49:56 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      HOL/MicroJava/J/Prog.ML
-    ID:         $Id$
-    Author:     David von Oheimb
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
-	rtac finite_map_of 1]);
-
-val is_classI = prove_goalw thy [is_class_def]
-"\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]);
-
-val is_classD = prove_goalw thy [is_class_def]
-"\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
-	not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/State.ML
--- a/src/HOL/MicroJava/J/State.ML	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/State.ML	Fri Jul 14 20:47:11 2000 +0200
@@ -65,6 +65,11 @@
 	(fn _ => [Auto_tac ]);
 Addsimps[np_None, np_Some,np_Null,np_Addr];
 
+Goalw [raise_if_def] "(np Null (raise_if c xc None)) = \
+\ Some (if c then xc else NullPointer)";
+by (Simp_tac 1);
+qed "np_raise_if";
+Addsimps[np_raise_if];
 
 
 
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -60,7 +60,7 @@
   c_hupd	:: "aheap \\<Rightarrow> xstate \\<Rightarrow> xstate"
  "c_hupd h'\\<equiv> \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
 
-  cast_ok	:: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
- "cast_ok G T h v \\<equiv> (v=Null) | G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq>RefT T"
+  cast_ok	:: "'c prog \\<Rightarrow> cname \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
+ "cast_ok G C h v \\<equiv> v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C"
 
 end
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/Term.thy
--- a/src/HOL/MicroJava/J/Term.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -12,7 +12,7 @@
 
 datatype expr
 	= NewC	cname		   (* class instance creation *)
-	| Cast	ref_ty expr	   (* type cast *)
+	| Cast	cname expr	   (* type cast *)
 	| Lit	val		   (* literal value, also references *)
         | BinOp binop  expr expr   (* binary operation *)
 	| LAcc vname		   (* local (incl. parameter) access *)
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/TypeRel.ML
--- a/src/HOL/MicroJava/J/TypeRel.ML	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.ML	Fri Jul 14 20:47:11 2000 +0200
@@ -113,18 +113,3 @@
 by(  rtac widen.null 2);
 by(eatac rtrancl_trans 1 1);
 qed_spec_mp "widen_trans";
-
-
-val prove_cast_lemma = prove_typerel_lemma [] cast.elim;
-
-val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>? T \\<Longrightarrow> \\<exists>t. T=RefT t" 
-	[prove_typerel_lemma [widen_RefT] cast.elim 
-	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
-
-val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
-	[prove_typerel_lemma [widen_RefT2] cast.elim 
-	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
-
-val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<preceq>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt" 
- [prove_cast_lemma "G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
-
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -9,21 +9,21 @@
 TypeRel = Decl +
 
 consts
-  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (*        subclass *)
-  widen,				 	    (*        widening *)
-  cast		:: "'c prog \\<Rightarrow> (ty \\<times> ty) set"	    (*        casting *)
+  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* subclass *)
+  widen 	:: "'c prog \\<Rightarrow> (ty    \\<times> ty   ) set"  (* widening *)
+  cast		:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* casting *)
 
 syntax
   subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
   subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
-  widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
-  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
+  widen		:: "'c prog \\<Rightarrow> [ty   , ty   ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
+  cast		:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
 
 translations
   	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
 	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
 	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
-	"G\\<turnstile>S \\<preceq>?  T" == "(S,T) \\<in> cast    G"
+	"G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
 
 defs
 
@@ -65,12 +65,13 @@
 
 inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
 			     i.e. sort of syntactic subtyping *)
-  refl	              "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
+  refl	             "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
   subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
-  null	              "G\\<turnstile>     NT \\<preceq> RefT R"
+  null	             "G\\<turnstile>     NT \\<preceq> RefT R"
 
 inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
-  widen	 "G\\<turnstile>S\\<preceq>T   \\<Longrightarrow> G\\<turnstile>      S \\<preceq>? T"
-  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<preceq>? Class C"
+                         (* left out casts on primitve types    *)
+  widen	 "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
+  subcls "G\\<turnstile>D\\<preceq>C C \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
 
 end
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/J/WellType.thy
--- a/src/HOL/MicroJava/J/WellType.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -95,9 +95,9 @@
 						 E\\<turnstile>NewC C\\<Colon>Class C"
 
   (* cf. 15.15 *)
-  Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>T;
-	  prg E\\<turnstile>T\\<preceq>? RefT rt\\<rbrakk> \\<Longrightarrow>
-						 E\\<turnstile>Cast rt e\\<Colon>RefT rt"
+  Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>Class C;
+	  prg E\\<turnstile>C\\<preceq>? D\\<rbrakk> \\<Longrightarrow>
+						 E\\<turnstile>Cast D e\\<Colon>Class D"
 
   (* cf. 15.7.1 *)
   Lit	"\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
diff -r 1791a62b33e7 -r f495dba0cb07 src/HOL/MicroJava/JVM/Object.thy
--- a/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 17:49:56 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 20:47:11 2000 +0200
@@ -65,7 +65,7 @@
 primrec
   "exec_ch (Checkcast C) G hp stk pc =
 	(let oref	= hd stk;
-	     xp'	= raise_xcpt (\\<not> cast_ok G (ClassT C) hp oref) ClassCast;
+	     xp'	= raise_xcpt (\\<not> cast_ok G C hp oref) ClassCast;
 	     stk'	= if xp'=None then stk else tl stk
 	 in
 	 (xp' , stk' , pc+1))"