corrections (cast relation, Prog.ML -> Decl.ML)
authoroheimb
Fri Jul 14 20:47:11 2000 +0200 (2000-07-14)
changeset 9348f495dba0cb07
parent 9347 1791a62b33e7
child 9349 d43669fb423d
corrections (cast relation, Prog.ML -> Decl.ML)
src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
src/HOL/MicroJava/J/Decl.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.ML
src/HOL/MicroJava/J/State.ML
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/Term.thy
src/HOL/MicroJava/J/TypeRel.ML
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellType.thy
src/HOL/MicroJava/JVM/Object.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Fri Jul 14 17:49:56 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Fri Jul 14 20:47:11 2000 +0200
     1.3 @@ -108,8 +108,8 @@
     1.4  (**** CH ****)
     1.5  
     1.6  Goalw [cast_ok_def]
     1.7 - "\\<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> \
     1.8 -\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
     1.9 + "\\<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> \
    1.10 +\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T";
    1.11  by (forward_tac [widen_Class] 1);
    1.12  by (Clarify_tac 1);
    1.13  be disjE 1;
    1.14 @@ -135,7 +135,6 @@
    1.15  	addss (simpset() addsimps [map_eq_Cons,approx_val_def])) 1);
    1.16  qed "Checkcast_correct";
    1.17  
    1.18 -
    1.19  Goal
    1.20  "\\<lbrakk> wt_jvm_prog G phi; \
    1.21  \  method (G,C) sig = Some (C,rT,maxl,ins); \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/MicroJava/J/Decl.ML	Fri Jul 14 20:47:11 2000 +0200
     2.3 @@ -0,0 +1,15 @@
     2.4 +(*  Title:      HOL/MicroJava/J/Decl.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     David von Oheimb
     2.7 +    Copyright   1999 Technische Universitaet Muenchen
     2.8 +*)
     2.9 +
    2.10 +val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
    2.11 +	rtac finite_map_of 1]);
    2.12 +
    2.13 +val is_classI = prove_goalw thy [is_class_def]
    2.14 +"\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]);
    2.15 +
    2.16 +val is_classD = prove_goalw thy [is_class_def]
    2.17 +"\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
    2.18 +	not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
     3.1 --- a/src/HOL/MicroJava/J/Eval.thy	Fri Jul 14 17:49:56 2000 +0200
     3.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Fri Jul 14 20:47:11 2000 +0200
     3.3 @@ -42,8 +42,8 @@
     3.4  
     3.5    (* cf. 15.15 *)
     3.6    Cast	"\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> (x1,s1);
     3.7 -	  x2=raise_if (\\<not> cast_ok G T (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
     3.8 -			        G\\<turnstile>Norm s0 -Cast T e\\<succ>v\\<rightarrow> (x2,s1)"
     3.9 +	  x2=raise_if (\\<not> cast_ok G C (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
    3.10 +			        G\\<turnstile>Norm s0 -Cast C e\\<succ>v\\<rightarrow> (x2,s1)"
    3.11  
    3.12    (* cf. 15.7.1 *)
    3.13    Lit				   "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
     4.1 --- a/src/HOL/MicroJava/J/Example.ML	Fri Jul 14 17:49:56 2000 +0200
     4.2 +++ b/src/HOL/MicroJava/J/Example.ML	Fri Jul 14 20:47:11 2000 +0200
     4.3 @@ -260,4 +260,4 @@
     4.4  by  (Simp_tac 1);
     4.5  by (Simp_tac 1);
     4.6  by e;	(* XcptE *)
     4.7 -qed "exec_test";
     4.8 +bind_thm ("exec_test", simplify (simpset()) (result()));
     5.1 --- a/src/HOL/MicroJava/J/Example.thy	Fri Jul 14 17:49:56 2000 +0200
     5.2 +++ b/src/HOL/MicroJava/J/Example.thy	Fri Jul 14 20:47:11 2000 +0200
     5.3 @@ -80,8 +80,8 @@
     5.4    BaseC_def "BaseC \\<equiv> (Base, (Some Object, 
     5.5  			     [(vee, PrimT Boolean)], 
     5.6  			     [((foo,[Class Base]),Class Base,foo_Base)]))"
     5.7 -  foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast (ClassT Ext)
     5.8 -					(LAcc x)..vee:=Lit (Intg #1)),
     5.9 +  foo_Ext_def "foo_Ext \\<equiv> ([x],[],Expr( {Ext}Cast Ext
    5.10 +				       (LAcc x)..vee:=Lit (Intg #1)),
    5.11  				   Lit Null)"
    5.12    ExtC_def  "ExtC  \\<equiv> (Ext,  (Some Base  , 
    5.13  			     [(vee, PrimT Integer)], 
    5.14 @@ -113,5 +113,5 @@
    5.15    "s0" == " Norm    (empty          ,empty                        )"
    5.16    "s1" == " Norm    (empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a)             )"
    5.17    "s2" == " Norm    (empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
    5.18 -  "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(x\\<mapsto>Null)(This\\<mapsto>Addr a))"
    5.19 +  "s3" == "(Some NP, empty(a\\<mapsto>obj1),empty(e\\<mapsto>Addr a))"
    5.20  end
     6.1 --- a/src/HOL/MicroJava/J/JTypeSafe.ML	Fri Jul 14 17:49:56 2000 +0200
     6.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML	Fri Jul 14 20:47:11 2000 +0200
     6.3 @@ -17,24 +17,15 @@
     6.4  qed "NewC_conforms";
     6.5  
     6.6  Goalw [cast_ok_def]
     6.7 - "\\<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> \
     6.8 -\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>RefT T'";
     6.9 + "\\<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> \
    6.10 +\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>Class D";
    6.11  by( case_tac1 "v = Null" 1);
    6.12  by(  Asm_full_simp_tac 1);
    6.13  by(  dtac widen_RefT 1);
    6.14  by(  Clarify_tac 1);
    6.15 -by(  forward_tac [cast_RefT] 1);
    6.16 -by(  Clarify_tac 1);
    6.17  by(  rtac widen.null 1);
    6.18 -by( Asm_full_simp_tac 1);
    6.19 -by( forward_tac [cast_RefT2] 1);
    6.20 -by( strip_tac1 1);
    6.21 -by( dtac non_npD 1);
    6.22 -by(  atac 1);
    6.23 -by( rewrite_goals_tac [obj_ty_def]);
    6.24 -by Auto_tac ;
    6.25 -by(  ALLGOALS (rtac conf_AddrI));
    6.26 -by     Auto_tac;
    6.27 +by( datac non_npD 1 1);
    6.28 +by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def]));
    6.29  qed "Cast_conf";
    6.30  
    6.31  Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
    6.32 @@ -283,7 +274,7 @@
    6.33  by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
    6.34  
    6.35  by prune_params_tac;
    6.36 -(* Level 45 *)
    6.37 +(* Level 51 *)
    6.38  
    6.39  (* 1 Call *)
    6.40  by( case_tac "x" 1);
    6.41 @@ -303,7 +294,8 @@
    6.42  by(  dtac eval_xcpt 1);
    6.43  by(  Asm_full_simp_tac 1);
    6.44  by(  fast_tac (HOL_cs addEs [hext_trans]) 1);
    6.45 -by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) THEN_ALL_NEW Asm_simp_tac) 1);
    6.46 +by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) 
    6.47 +    THEN_ALL_NEW Asm_simp_tac) 1);
    6.48  qed "eval_evals_exec_type_sound";
    6.49  
    6.50  Goal "\\<And>E s s'. \
     7.1 --- a/src/HOL/MicroJava/J/Prog.ML	Fri Jul 14 17:49:56 2000 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,15 +0,0 @@
     7.4 -(*  Title:      HOL/MicroJava/J/Prog.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     David von Oheimb
     7.7 -    Copyright   1999 Technische Universitaet Muenchen
     7.8 -*)
     7.9 -
    7.10 -val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
    7.11 -	rtac finite_map_of 1]);
    7.12 -
    7.13 -val is_classI = prove_goalw thy [is_class_def]
    7.14 -"\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]);
    7.15 -
    7.16 -val is_classD = prove_goalw thy [is_class_def]
    7.17 -"\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
    7.18 -	not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
     8.1 --- a/src/HOL/MicroJava/J/State.ML	Fri Jul 14 17:49:56 2000 +0200
     8.2 +++ b/src/HOL/MicroJava/J/State.ML	Fri Jul 14 20:47:11 2000 +0200
     8.3 @@ -65,6 +65,11 @@
     8.4  	(fn _ => [Auto_tac ]);
     8.5  Addsimps[np_None, np_Some,np_Null,np_Addr];
     8.6  
     8.7 +Goalw [raise_if_def] "(np Null (raise_if c xc None)) = \
     8.8 +\ Some (if c then xc else NullPointer)";
     8.9 +by (Simp_tac 1);
    8.10 +qed "np_raise_if";
    8.11 +Addsimps[np_raise_if];
    8.12  
    8.13  
    8.14  
     9.1 --- a/src/HOL/MicroJava/J/State.thy	Fri Jul 14 17:49:56 2000 +0200
     9.2 +++ b/src/HOL/MicroJava/J/State.thy	Fri Jul 14 20:47:11 2000 +0200
     9.3 @@ -60,7 +60,7 @@
     9.4    c_hupd	:: "aheap \\<Rightarrow> xstate \\<Rightarrow> xstate"
     9.5   "c_hupd h'\\<equiv> \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
     9.6  
     9.7 -  cast_ok	:: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
     9.8 - "cast_ok G T h v \\<equiv> (v=Null) | G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq>RefT T"
     9.9 +  cast_ok	:: "'c prog \\<Rightarrow> cname \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
    9.10 + "cast_ok G C h v \\<equiv> v = Null \\<or> G\\<turnstile>obj_ty (the (h (the_Addr v)))\\<preceq> Class C"
    9.11  
    9.12  end
    10.1 --- a/src/HOL/MicroJava/J/Term.thy	Fri Jul 14 17:49:56 2000 +0200
    10.2 +++ b/src/HOL/MicroJava/J/Term.thy	Fri Jul 14 20:47:11 2000 +0200
    10.3 @@ -12,7 +12,7 @@
    10.4  
    10.5  datatype expr
    10.6  	= NewC	cname		   (* class instance creation *)
    10.7 -	| Cast	ref_ty expr	   (* type cast *)
    10.8 +	| Cast	cname expr	   (* type cast *)
    10.9  	| Lit	val		   (* literal value, also references *)
   10.10          | BinOp binop  expr expr   (* binary operation *)
   10.11  	| LAcc vname		   (* local (incl. parameter) access *)
    11.1 --- a/src/HOL/MicroJava/J/TypeRel.ML	Fri Jul 14 17:49:56 2000 +0200
    11.2 +++ b/src/HOL/MicroJava/J/TypeRel.ML	Fri Jul 14 20:47:11 2000 +0200
    11.3 @@ -113,18 +113,3 @@
    11.4  by(  rtac widen.null 2);
    11.5  by(eatac rtrancl_trans 1 1);
    11.6  qed_spec_mp "widen_trans";
    11.7 -
    11.8 -
    11.9 -val prove_cast_lemma = prove_typerel_lemma [] cast.elim;
   11.10 -
   11.11 -val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>? T \\<Longrightarrow> \\<exists>t. T=RefT t" 
   11.12 -	[prove_typerel_lemma [widen_RefT] cast.elim 
   11.13 -	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
   11.14 -
   11.15 -val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t" 
   11.16 -	[prove_typerel_lemma [widen_RefT2] cast.elim 
   11.17 -	"G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
   11.18 -
   11.19 -val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<preceq>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt" 
   11.20 - [prove_cast_lemma "G\\<turnstile>S\\<preceq>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
   11.21 -
    12.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 14 17:49:56 2000 +0200
    12.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Jul 14 20:47:11 2000 +0200
    12.3 @@ -9,21 +9,21 @@
    12.4  TypeRel = Decl +
    12.5  
    12.6  consts
    12.7 -  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (*        subclass *)
    12.8 -  widen,				 	    (*        widening *)
    12.9 -  cast		:: "'c prog \\<Rightarrow> (ty \\<times> ty) set"	    (*        casting *)
   12.10 +  subcls1	:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* subclass *)
   12.11 +  widen 	:: "'c prog \\<Rightarrow> (ty    \\<times> ty   ) set"  (* widening *)
   12.12 +  cast		:: "'c prog \\<Rightarrow> (cname \\<times> cname) set"  (* casting *)
   12.13  
   12.14  syntax
   12.15    subcls1	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_"	 [71,71,71] 70)
   12.16    subcls	:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>C _"	 [71,71,71] 70)
   12.17 -  widen		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
   12.18 -  cast		:: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool"       ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
   12.19 +  widen		:: "'c prog \\<Rightarrow> [ty   , ty   ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_"  [71,71,71] 70)
   12.20 +  cast		:: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>? _"[71,71,71] 70)
   12.21  
   12.22  translations
   12.23    	"G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
   12.24  	"G\\<turnstile>C \\<preceq>C  D" == "(C,D) \\<in> (subcls1 G)^*"
   12.25  	"G\\<turnstile>S \\<preceq>   T" == "(S,T) \\<in> widen   G"
   12.26 -	"G\\<turnstile>S \\<preceq>?  T" == "(S,T) \\<in> cast    G"
   12.27 +	"G\\<turnstile>C \\<preceq>?  D" == "(C,D) \\<in> cast    G"
   12.28  
   12.29  defs
   12.30  
   12.31 @@ -65,12 +65,13 @@
   12.32  
   12.33  inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
   12.34  			     i.e. sort of syntactic subtyping *)
   12.35 -  refl	              "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
   12.36 +  refl	             "G\\<turnstile>      T \\<preceq> T" 	 (* identity conv., cf. 5.1.1 *)
   12.37    subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
   12.38 -  null	              "G\\<turnstile>     NT \\<preceq> RefT R"
   12.39 +  null	             "G\\<turnstile>     NT \\<preceq> RefT R"
   12.40  
   12.41  inductive "cast G" intrs (* casting conversion, cf. 5.5 / 5.1.5 *)
   12.42 -  widen	 "G\\<turnstile>S\\<preceq>T   \\<Longrightarrow> G\\<turnstile>      S \\<preceq>? T"
   12.43 -  subcls "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>Class D \\<preceq>? Class C"
   12.44 +                         (* left out casts on primitve types    *)
   12.45 +  widen	 "G\\<turnstile>C\\<preceq>C D \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
   12.46 +  subcls "G\\<turnstile>D\\<preceq>C C \\<Longrightarrow> G\\<turnstile>C \\<preceq>? D"
   12.47  
   12.48  end
    13.1 --- a/src/HOL/MicroJava/J/WellType.thy	Fri Jul 14 17:49:56 2000 +0200
    13.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Fri Jul 14 20:47:11 2000 +0200
    13.3 @@ -95,9 +95,9 @@
    13.4  						 E\\<turnstile>NewC C\\<Colon>Class C"
    13.5  
    13.6    (* cf. 15.15 *)
    13.7 -  Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>T;
    13.8 -	  prg E\\<turnstile>T\\<preceq>? RefT rt\\<rbrakk> \\<Longrightarrow>
    13.9 -						 E\\<turnstile>Cast rt e\\<Colon>RefT rt"
   13.10 +  Cast	"\\<lbrakk>E\\<turnstile>e\\<Colon>Class C;
   13.11 +	  prg E\\<turnstile>C\\<preceq>? D\\<rbrakk> \\<Longrightarrow>
   13.12 +						 E\\<turnstile>Cast D e\\<Colon>Class D"
   13.13  
   13.14    (* cf. 15.7.1 *)
   13.15    Lit	"\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
    14.1 --- a/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 17:49:56 2000 +0200
    14.2 +++ b/src/HOL/MicroJava/JVM/Object.thy	Fri Jul 14 20:47:11 2000 +0200
    14.3 @@ -65,7 +65,7 @@
    14.4  primrec
    14.5    "exec_ch (Checkcast C) G hp stk pc =
    14.6  	(let oref	= hd stk;
    14.7 -	     xp'	= raise_xcpt (\\<not> cast_ok G (ClassT C) hp oref) ClassCast;
    14.8 +	     xp'	= raise_xcpt (\\<not> cast_ok G C hp oref) ClassCast;
    14.9  	     stk'	= if xp'=None then stk else tl stk
   14.10  	 in
   14.11  	 (xp' , stk' , pc+1))"