--- 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); \
--- /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]);
--- 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"
--- 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()));
--- 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
--- 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'. \
--- 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]);
--- 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];
--- 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
--- 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 *)
--- 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"];
-
--- 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
--- 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>
--- 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))"