--- a/src/HOL/IsaMakefile Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/IsaMakefile Fri Jul 14 16:32:51 2000 +0200
@@ -329,14 +329,15 @@
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \
- MicroJava/J/Conform.ML MicroJava/J/Conform.thy MicroJava/J/Decl.thy \
+ MicroJava/J/Conform.ML MicroJava/J/Conform.thy \
MicroJava/J/Eval.thy MicroJava/J/Eval.ML MicroJava/J/JBasis.ML \
MicroJava/J/JBasis.thy MicroJava/J/JTypeSafe.thy MicroJava/J/JTypeSafe.ML \
- MicroJava/J/Prog.thy MicroJava/J/Prog.ML MicroJava/J/State.ML \
- MicroJava/J/State.thy MicroJava/J/Term.thy MicroJava/J/Type.ML \
+ MicroJava/J/Decl.thy MicroJava/J/Decl.ML MicroJava/J/State.ML \
+ MicroJava/J/State.thy MicroJava/J/Term.thy \
MicroJava/J/Type.thy MicroJava/J/TypeRel.ML MicroJava/J/TypeRel.thy \
- MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML \
+ MicroJava/J/WellForm.thy MicroJava/J/WellForm.ML MicroJava/J/Value.thy \
MicroJava/J/WellType.ML MicroJava/J/WellType.thy \
+ MicroJava/J/Example.ML MicroJava/J/Example.thy \
MicroJava/JVM/Control.thy MicroJava/JVM/JVMExec.thy \
MicroJava/JVM/JVMState.thy MicroJava/JVM/LoadAndStore.thy \
MicroJava/JVM/Method.thy MicroJava/JVM/Object.thy MicroJava/JVM/Opstack.thy \
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Fri Jul 14 16:32:51 2000 +0200
@@ -108,10 +108,8 @@
(**** CH ****)
Goalw [cast_ok_def]
- "\\<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> \
+ "\\<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'";
-be disjE 1;
- by (Clarify_tac 1);
by (forward_tac [widen_Class] 1);
by (Clarify_tac 1);
be disjE 1;
--- a/src/HOL/MicroJava/J/Conform.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Fri Jul 14 16:32:51 2000 +0200
@@ -6,7 +6,9 @@
Conformity relations for type safety of Java
*)
-Conform = State +
+Conform = State + WellType +
+
+types 'c env_ = "'c prog \\<times> (vname \\<leadsto> ty)" (* same as env of WellType.thy *)
constdefs
@@ -26,7 +28,7 @@
hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_\\<turnstile>h _\\<surd>" [51,51] 50)
"G\\<turnstile>h h\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
- conforms :: "state \\<Rightarrow> java_mb env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
+ conforms :: "state \\<Rightarrow> java_mb env_ \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
"s\\<Colon>\\<preceq>E \\<equiv> prg E\\<turnstile>h heap s\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
end
--- a/src/HOL/MicroJava/J/Decl.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/Decl.thy Fri Jul 14 16:32:51 2000 +0200
@@ -3,7 +3,7 @@
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
-Class declarations
+Class declarations and programs
*)
Decl = Type +
@@ -34,4 +34,24 @@
ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
+
+types 'c prog = "'c cdecl list"
+
+consts
+
+ class :: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
+
+ is_class :: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
+ is_type :: "'c prog \\<Rightarrow> ty \\<Rightarrow> bool"
+
+defs
+
+ class_def "class \\<equiv> map_of"
+
+ is_class_def "is_class G C \\<equiv> class G C \\<noteq> None"
+
+primrec
+"is_type G (PrimT pt) = True"
+"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"
+
end
--- a/src/HOL/MicroJava/J/Eval.ML Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.ML Fri Jul 14 16:32:51 2000 +0200
@@ -4,6 +4,14 @@
Copyright 1999 Technische Universitaet Muenchen
*)
+Goal "\\<lbrakk>new_Addr (heap s) = (a,x); \
+\ s' = c_hupd (heap s(a\\<mapsto>(C,init_vars (fields (G,C))))) (x,s)\\<rbrakk> \\<Longrightarrow> \
+\ G\\<turnstile>Norm s -NewC C\\<succ>Addr a\\<rightarrow> s'";
+by (hyp_subst_tac 1);
+br eval_evals_exec.NewC 1;
+by Auto_tac;
+qed "NewCI";
+
Goal "\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ> v \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
\ (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
\ (G\\<turnstile>(x,s) -c \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None)";
--- a/src/HOL/MicroJava/J/Eval.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Fri Jul 14 16:32:51 2000 +0200
@@ -7,7 +7,7 @@
execution of Java expressions and statements
*)
-Eval = State +
+Eval = State + WellType +
consts
eval :: "java_mb prog \\<Rightarrow> (xstate \\<times> expr \\<times> val \\<times> xstate) set"
@@ -73,7 +73,7 @@
G\\<turnstile>(np a' x1,s1) -e2\\<succ>v \\<rightarrow> (x2,s2);
h = heap s2; (c,fs) = the (h a);
h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))\\<rbrakk> \\<Longrightarrow>
- G\\<turnstile>Norm s0 -{T}e1..fn\\<in>=e2\\<succ>v\\<rightarrow> c_hupd h' (x2,s2)"
+ G\\<turnstile>Norm s0 -{T}e1..fn:=e2\\<succ>v\\<rightarrow> c_hupd h' (x2,s2)"
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
Call "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a';
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Example.ML Fri Jul 14 16:32:51 2000 +0200
@@ -0,0 +1,263 @@
+open Example;
+
+AddIs [widen.null];
+
+Addsimps [inj_cnam_, inj_vnam_];
+Addsimps [Base_not_Object,Ext_not_Object];
+Addsimps [Base_not_Object RS not_sym,Ext_not_Object RS not_sym];
+
+val map_of_Cons = prove_goalw thy [get_def thy "map_of_list"]
+"map_of (p#ps) = (map_of ps)(fst p |-> snd p)" (K [Simp_tac 1]);
+val map_of_Cons1 = prove_goalw Map.thy [get_def thy "map_of_list"]
+"map_of ((x,y)#ps) x = Some y" (K [Simp_tac 1]);
+val map_of_Cons2 = prove_goalw Map.thy [get_def thy "map_of_list"]
+"\\<And>X. x\\<noteq>k \\<Longrightarrow> map_of ((k,y)#ps) x = map_of ps x" (K [Asm_simp_tac 1]);
+Delsimps[map_of_Cons]; (* sic! *)
+Addsimps[map_of_Cons1, map_of_Cons2];
+
+val class_tprg_Object = prove_goalw thy [class_def, ObjectC_def]
+ "class tprg Object = Some (None, [], [])"
+ (K [Simp_tac 1]);
+val class_tprg_Base = prove_goalw thy [class_def, ObjectC_def, BaseC_def,
+ ExtC_def] "class tprg Base = Some (Some Object, \
+ \ [(vee, PrimT Boolean)], \
+ \ [((foo, [Class Base]), Class Base, foo_Base)])" (K [
+ Simp_tac 1]);
+val class_tprg_Ext = prove_goalw thy [class_def, ObjectC_def, BaseC_def,
+ ExtC_def] "class tprg Ext = Some (Some Base, \
+ \ [(vee, PrimT Integer)], \
+ \ [((foo, [Class Base]), Class Ext, foo_Ext)])" (K [
+ Simp_tac 1]);
+Addsimps [class_tprg_Object, class_tprg_Base, class_tprg_Ext];
+
+Goal "\\<And>X. (Object,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
+by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
+qed "not_Object_subcls";
+AddSEs [not_Object_subcls];
+
+Goal "tprg\\<turnstile>Object\\<preceq>C C \\<Longrightarrow> C = Object";
+be rtrancl_induct 1;
+by Auto_tac;
+bd subcls1D 1;
+by Auto_tac;
+qed "subcls_ObjectD";
+AddSDs[subcls_ObjectD];
+
+Goal "\\<And>X. (Base, Ext) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
+by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
+qed "not_Base_subcls_Ext";
+AddSEs [not_Base_subcls_Ext];
+
+Goalw [class_def, ObjectC_def, BaseC_def, ExtC_def] "class tprg C = Some z \\<Longrightarrow> C=Object \\<or> C=Base \\<or> C=Ext";
+by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm]));
+qed "class_tprgD";
+
+Goal "(C,C) \\<in> (subcls1 tprg)^+ \\<Longrightarrow> R";
+by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset()));
+by (ftac class_tprgD 1);
+by (auto_tac (claset() addSDs [],simpset()));
+bd rtranclD 1;
+by Auto_tac;
+qed "not_class_subcls_class";
+AddSEs [not_class_subcls_class];
+
+goalw thy [ObjectC_def, BaseC_def, ExtC_def] "unique tprg";
+by (Simp_tac 1);
+qed "unique_classes";
+
+bind_thm ("subcls_direct", subcls1I RS r_into_rtrancl);
+
+Goalw [] "tprg\\<turnstile>Ext\\<preceq>C Base";
+br subcls_direct 1;
+by (Simp_tac 1);
+qed "Ext_subcls_Base";
+Addsimps [Ext_subcls_Base];
+
+Goalw [] "tprg\\<turnstile>Class Ext\\<preceq> Class Base";
+br widen.subcls 1;
+by (Simp_tac 1);
+qed "Ext_widen_Base";
+Addsimps [Ext_widen_Base];
+
+AddSIs ty_expr_ty_exprs_wt_stmt.intrs;
+
+
+Goal "acyclic (subcls1 tprg)";
+br acyclicI 1;
+by Safe_tac ;
+qed "acyclic_subcls1_";
+
+val wf_subcls1_=acyclic_subcls1_ RS(finite_subcls1 RS finite_acyclic_wf_converse);
+
+
+Addsimps[is_class_def];
+
+val fields_rec_ = wf_subcls1_ RSN (1, fields_rec_lemma);
+
+Goal "fields (tprg, Object) = []";
+by (stac fields_rec_ 1);
+by Auto_tac;
+qed "fields_Object";
+Addsimps [fields_Object];
+
+Goal "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]";
+by (stac fields_rec_ 1);
+by Auto_tac;
+qed "fields_Base";
+Addsimps [fields_Base];
+
+Goal "fields (tprg, Ext) = [((vee, Ext ), PrimT Integer)] @\
+ \ fields (tprg, Base)";
+br trans 1;
+br fields_rec_ 1;
+by Auto_tac;
+qed "fields_Ext";
+Addsimps [fields_Ext];
+
+val method_rec_ = wf_subcls1_ RS method_rec_lemma;
+
+Goal "method (tprg,Object) = map_of []";
+by (stac method_rec_ 1);
+by Auto_tac;
+qed "method_Object";
+Addsimps [method_Object];
+
+Goal "method (tprg, Base) = map_of \
+\ [((foo, [Class Base]), Base, (Class Base, foo_Base))]";
+br trans 1;
+br method_rec_ 1;
+by Auto_tac;
+qed "method_Base";
+Addsimps [method_Base];
+
+Goal "method (tprg, Ext) = (method (tprg, Base) \\<oplus> map_of \
+\ [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])";
+br trans 1;
+br method_rec_ 1;
+by Auto_tac;
+qed "method_Ext";
+Addsimps [method_Ext];
+
+Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Base_def]
+"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))";
+by Auto_tac;
+qed "wf_foo_Base";
+
+Goalw [wf_mdecl_def,wf_mhead_def,wf_java_mdecl_def,foo_Ext_def]
+"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))";
+by Auto_tac;
+br ty_expr_ty_exprs_wt_stmt.Cast 1;
+by (Simp_tac 2);
+br cast.subcls 2;
+by (rewtac field_def);
+by Auto_tac;
+qed "wf_foo_Ext";
+
+Goalw [wf_cdecl_def, wf_fdecl_def, ObjectC_def]
+"wf_cdecl wf_java_mdecl tprg ObjectC";
+by (Simp_tac 1);
+qed "wf_ObjectC";
+
+Goalw [wf_cdecl_def, wf_fdecl_def, BaseC_def]
+"wf_cdecl wf_java_mdecl tprg BaseC";
+by (Simp_tac 1);
+by (fold_goals_tac [BaseC_def]);
+br (wf_foo_Base RS conjI) 1;
+by Auto_tac;
+qed "wf_BaseC";
+
+Goalw [wf_cdecl_def, wf_fdecl_def, ExtC_def]
+"wf_cdecl wf_java_mdecl tprg ExtC";
+by (Simp_tac 1);
+by (fold_goals_tac [ExtC_def]);
+br (wf_foo_Ext RS conjI) 1;
+by Auto_tac;
+bd rtranclD 1;
+by Auto_tac;
+qed "wf_ExtC";
+
+Goalw [wf_prog_def,Let_def]
+"wf_prog wf_java_mdecl tprg";
+by(simp_tac (simpset() addsimps [wf_ObjectC,wf_BaseC,wf_ExtC,unique_classes])1);
+qed "wf_tprg";
+
+Goalw [appl_methds_def]
+"appl_methds tprg Base (foo, [NT]) = \
+\ {((Class Base, Class Base), [Class Base])}";
+by (Simp_tac 1);
+by (subgoal_tac "tprg\\<turnstile>NT\\<preceq> Class Base" 1);
+by (auto_tac (claset(), simpset() addsimps [map_of_Cons,foo_Base_def]));
+qed "appl_methds_foo_Base";
+
+Goalw [max_spec_def] "max_spec tprg Base (foo, [NT]) = \
+\ {((Class Base, Class Base), [Class Base])}";
+by (auto_tac (claset(), simpset() addsimps [appl_methds_foo_Base]));
+qed "max_spec_foo_Base";
+
+fun t thm = resolve_tac ty_expr_ty_exprs_wt_stmt.intrs 1 thm;
+Goalw [test_def] "(tprg, empty(e\\<mapsto>Class Base))\\<turnstile>\
+\ Expr(e\\<Colon>=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\<surd>";
+(* ?pTs' = [Class Base] *)
+by t; (* ;; *)
+by t; (* Expr *)
+by t; (* LAss *)
+by t; (* LAcc *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+by t; (* NewC *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+by t; (* Expr *)
+by t; (* Call *)
+by t; (* LAcc *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+by t; (* Cons *)
+by t; (* Lit *)
+by (Simp_tac 1);
+by t; (* Nil *)
+by (Simp_tac 1);
+br max_spec_foo_Base 1;
+qed "wt_test";
+
+fun e thm = resolve_tac (NewCI::eval_evals_exec.intrs) 1 thm;
+
+Delsplits[split_if];
+Addsimps[init_vars_def,c_hupd_def,cast_ok_def];
+Goalw [test_def]
+" \\<lbrakk>new_Addr (heap (snd s0)) = (a, None)\\<rbrakk> \\<Longrightarrow> \
+\ tprg\\<turnstile>s0 -test\\<rightarrow> ?s";
+(* ?s = s3 *)
+by e; (* ;; *)
+by e; (* Expr *)
+by e; (* LAss *)
+by e; (* NewC *)
+by (Force_tac 1);
+by (Force_tac 1);
+by (Simp_tac 1);
+be thin_rl 1;
+by e; (* Expr *)
+by e; (* Call *)
+by e; (* LAcc *)
+by (Force_tac 1);
+by e; (* Cons *)
+by e; (* Lit *)
+by e; (* Nil *)
+by (Simp_tac 1);
+by (force_tac (claset(), simpset() addsimps [foo_Ext_def]) 1);
+by (Simp_tac 1);
+by e; (* Expr *)
+by e; (* FAss *)
+by e;(* Cast *)
+by e;(* LAcc *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by e;(* XcptE *)
+by (Simp_tac 1);
+by (EVERY'[rtac (surjective_pairing RS sym RSN (2,trans)), stac Pair_eq,
+ Force_tac] 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by e; (* XcptE *)
+qed "exec_test";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Example.thy Fri Jul 14 16:32:51 2000 +0200
@@ -0,0 +1,117 @@
+(* Title: isabelle/Bali/Example.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1997 Technische Universitaet Muenchen
+
+The following example Bali program includes:
+ class declarations with inheritance, hiding of fields, and overriding of
+ methods (with refined result type),
+ instance creation, local assignment, sequential composition,
+ method call with dynamic binding, literal values,
+ expression statement, local access, type cast, field assignment (in part), skip
+
+class Base {
+ boolean vee;
+ Base foo(Base x) {return x;}
+}
+
+class Ext extends Base{
+ int vee;
+ Ext foo(Base x) {((Ext)x).vee=1; return null;}
+}
+
+class Example {
+ public static void main (String args[]) {
+ Base e;
+ e=new Ext();
+ try {e.foo(null); }
+ catch (NullPointerException x) {}
+ }
+}
+*)
+
+Example = Eval +
+
+datatype cnam_ = Base_ | Ext_
+datatype vnam_ = vee_ | x_ | e_
+
+consts
+
+ cnam_ :: "cnam_ \\<Rightarrow> cname"
+ vnam_ :: "vnam_ \\<Rightarrow> vnam"
+
+rules (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *)
+
+ inj_cnam_ "(cnam_ x = cnam_ y) = (x = y)"
+ inj_vnam_ "(vnam_ x = vnam_ y) = (x = y)"
+
+ surj_cnam_ "\\<exists>m. n = cnam_ m"
+ surj_vnam_ "\\<exists>m. n = vnam_ m"
+
+syntax
+
+ Base, Ext :: cname
+ vee, x, e :: vname
+
+translations
+
+ "Base" == "cnam_ Base_"
+ "Ext" == "cnam_ Ext_"
+ "vee" == "VName (vnam_ vee_)"
+ "x" == "VName (vnam_ x_)"
+ "e" == "VName (vnam_ e_)"
+
+rules
+ Base_not_Object "Base \\<noteq> Object"
+ Ext_not_Object "Ext \\<noteq> Object"
+
+consts
+
+ foo_Base :: java_mb
+ foo_Ext :: java_mb
+ BaseC, ExtC :: java_mb cdecl
+ test :: stmt
+ foo :: mname
+ a,b :: loc
+
+defs
+
+ foo_Base_def "foo_Base \\<equiv> ([x],[],Skip,LAcc x)"
+ 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)),
+ Lit Null)"
+ ExtC_def "ExtC \\<equiv> (Ext, (Some Base ,
+ [(vee, PrimT Integer)],
+ [((foo,[Class Base]),Class Ext,foo_Ext)]))"
+
+ test_def "test \\<equiv> Expr(e\\<Colon>=NewC Ext);;
+ Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
+
+
+
+
+
+
+
+
+syntax
+
+ NP :: xcpt
+ tprg :: java_mb prog
+ obj1, obj2 :: obj
+ s0,s1,s2,s3,s4:: state
+
+translations
+
+ "NP" == "NullPointer"
+ "tprg" == "[ObjectC, BaseC, ExtC]"
+ "obj1" <= "(Ext, empty((vee, Base)\\<mapsto>Bool False)
+ ((vee, Ext )\\<mapsto>Intg #0))"
+ "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))"
+end
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.ML Fri Jul 14 16:32:51 2000 +0200
@@ -6,19 +6,6 @@
Type safety proof
*)
-Goalw [conf_def] "G,s\\<turnstile>Unit\\<Colon>\\<preceq>PrimT Void";
-by( Simp_tac 1);
-qed "conf_VoidI";
-
-Goalw [conf_def] "G,s\\<turnstile>Bool b\\<Colon>\\<preceq>PrimT Boolean";
-by( Simp_tac 1);
-qed "conf_BooleanI";
-
-Goalw [conf_def] "G,s\\<turnstile>Intg i\\<Colon>\\<preceq>PrimT Integer";
-by( Simp_tac 1);
-qed "conf_IntegerI";
-
-Addsimps [conf_VoidI, conf_BooleanI, conf_IntegerI];
Addsimps [split_beta];
@@ -30,8 +17,8 @@
qed "NewC_conforms";
Goalw [cast_ok_def]
- "\\<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> \
-\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
+ "\\<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'";
by( case_tac1 "v = Null" 1);
by( Asm_full_simp_tac 1);
by( dtac widen_RefT 1);
@@ -39,15 +26,7 @@
by( forward_tac [cast_RefT] 1);
by( Clarify_tac 1);
by( rtac widen.null 1);
-by( case_tac1 "\\<exists>pt. T' = PrimT pt" 1);
-by( strip_tac1 1);
-by( dtac cast_PrimT2 1);
-by( etac conf_widen 1);
-by( atac 1);
-by( atac 1);
by( Asm_full_simp_tac 1);
-by( dtac (non_PrimT RS iffD1) 1);
-by( strip_tac1 1);
by( forward_tac [cast_RefT2] 1);
by( strip_tac1 1);
by( dtac non_npD 1);
--- a/src/HOL/MicroJava/J/Prog.thy Fri Jul 14 16:32:44 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* Title: HOL/MicroJava/J/Prog.thy
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-
-Java program = list of class declarations
-*)
-
-Prog = Decl +
-
-types 'c prog = "'c cdecl list"
-
-consts
-
- class :: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
-
- is_class :: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
- is_type :: "'c prog \\<Rightarrow> ty \\<Rightarrow> bool"
-
-defs
-
- class_def "class \\<equiv> map_of"
-
- is_class_def "is_class G C \\<equiv> class G C \\<noteq> None"
-
-primrec
-"is_type G (PrimT pt) = True"
-"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"
-
-end
--- a/src/HOL/MicroJava/J/State.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/State.thy Fri Jul 14 16:32:51 2000 +0200
@@ -6,38 +6,12 @@
State for evaluation of Java expressions and statements
*)
-State = WellType +
-
-consts
- the_Bool :: "val \\<Rightarrow> bool"
- the_Intg :: "val \\<Rightarrow> int"
- the_Addr :: "val \\<Rightarrow> loc"
-
- defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *)
- default_val :: "ty \\<Rightarrow> val" (* default value for all types *)
-
-primrec
- "the_Bool (Bool b) = b"
-
-primrec
- "the_Intg (Intg i) = i"
-
-primrec
- "the_Addr (Addr a) = a"
-
-primrec
- "defpval Void = Unit"
- "defpval Boolean = Bool False"
- "defpval Integer = Intg (#0)"
-
-primrec
- "default_val (PrimT pt) = defpval pt"
- "default_val (RefT r ) = Null"
+State = TypeRel + Value +
types fields_
= "(vname \\<times> cname \\<leadsto> val)" (* field name, defining class, value *)
-types obj = "cname \\<times> fields_" (* class instance with class name and fields *)
+ obj = "cname \\<times> fields_" (* class instance with class name and fields *)
constdefs
@@ -86,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> ty \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
- "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)"
+ 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"
end
--- a/src/HOL/MicroJava/J/Term.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Fri Jul 14 16:32:51 2000 +0200
@@ -6,33 +6,20 @@
Java expressions and statements
*)
-Term = Type +
-
-types loc (* locations, i.e. abstract references on objects *)
-arities loc :: term
-
-datatype val_ (* name non 'val' because of clash with ML token *)
- = Unit (* dummy result value of void methods *)
- | Null (* null reference *)
- | Bool bool (* Boolean value *)
- | Intg int (* integer value *) (* Name Intg instead of Int because
- of clash with HOL/Set.thy *)
- | Addr loc (* addresses, i.e. locations of objects *)
-types val = val_
-translations "val" <= (type) "val_"
+Term = Value +
datatype binop = Eq | Add (* function codes for binary operation *)
datatype expr
= NewC cname (* class instance creation *)
- | Cast ty expr (* type cast *)
+ | Cast ref_ty expr (* type cast *)
| Lit val (* literal value, also references *)
| BinOp binop expr expr (* binary operation *)
| LAcc vname (* local (incl. parameter) access *)
| LAss vname expr (* local assign *) ("_\\<Colon>=_" [ 90,90]90)
| FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90)
| FAss cname expr vname
- expr (* field ass. *)("{_}_.._\\<in>=_"[10,90,99,90]90)
+ expr (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
| Call expr mname (ty list) (expr list)(* method call*)
("_.._'({_}_')" [90,99,10,10] 90)
and stmt
--- a/src/HOL/MicroJava/J/Type.ML Fri Jul 14 16:32:44 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-(* Title: HOL/MicroJava/J/Type.ML
- ID: $Id$
- Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-Goal "(\\<forall>pt. T \\<noteq> PrimT pt) = (\\<exists>t. T = RefT t)";
-by(case_tac "T" 1);
-by Auto_tac;
-qed "non_PrimT";
--- a/src/HOL/MicroJava/J/TypeRel.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Jul 14 16:32:51 2000 +0200
@@ -6,7 +6,7 @@
The relations between Java types
*)
-TypeRel = Prog +
+TypeRel = Decl +
consts
subcls1 :: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (* subclass *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/J/Value.thy Fri Jul 14 16:32:51 2000 +0200
@@ -0,0 +1,51 @@
+(* Title: HOL/MicroJava/J/Term.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 1999 Technische Universitaet Muenchen
+
+Java values
+*)
+
+Value = Type +
+
+types loc (* locations, i.e. abstract references on objects *)
+arities loc :: term
+
+datatype val_ (* name non 'val' because of clash with ML token *)
+ = Unit (* dummy result value of void methods *)
+ | Null (* null reference *)
+ | Bool bool (* Boolean value *)
+ | Intg int (* integer value *) (* Name Intg instead of Int because
+ of clash with HOL/Set.thy *)
+ | Addr loc (* addresses, i.e. locations of objects *)
+types val = val_
+translations "val" <= (type) "val_"
+
+consts
+ the_Bool :: "val \\<Rightarrow> bool"
+ the_Intg :: "val \\<Rightarrow> int"
+ the_Addr :: "val \\<Rightarrow> loc"
+
+primrec
+ "the_Bool (Bool b) = b"
+
+primrec
+ "the_Intg (Intg i) = i"
+
+primrec
+ "the_Addr (Addr a) = a"
+
+consts
+ defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *)
+ default_val :: "ty \\<Rightarrow> val" (* default value for all types *)
+
+primrec
+ "defpval Void = Unit"
+ "defpval Boolean = Bool False"
+ "defpval Integer = Intg (#0)"
+
+primrec
+ "default_val (PrimT pt) = defpval pt"
+ "default_val (RefT r ) = Null"
+
+end
--- a/src/HOL/MicroJava/J/WellForm.ML Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/WellForm.ML Fri Jul 14 16:32:51 2000 +0200
@@ -95,36 +95,50 @@
by( etac subcls1I 1);
qed "subcls1_induct";
-Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
+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) = \
\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
by( stac (method_TC RS (wf_subcls1_rel RS (hd method.simps))) 1);
+by( asm_simp_tac (simpset() addsplits[option.split]) 1);
+auto();
+qed "method_rec_lemma";
+
+Goal "wf_prog wf_mb G \\<Longrightarrow> method (G,C) = \
+\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
+\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> method (G,D)) \\<oplus> \
+\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
+by(rtac method_rec_lemma 1);
by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
addsplits [option.split]) 1);
by( case_tac "C = Object" 1);
-by( Asm_full_simp_tac 1);
-by( dtac class_wf 1);
-by( atac 1);
-by( dtac wf_cdecl_supD 1);
-by( atac 1);
+by( Force_tac 1);
+by Safe_tac;
+by( datac class_wf 1 1);
+by( datac wf_cdecl_supD 1 1);
by( Asm_full_simp_tac 1);
qed "method_rec";
+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) = \
+\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
+\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
+by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
+by( asm_simp_tac (simpset() addsplits[option.split]) 1);
+qed "fields_rec_lemma";
+
Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
-by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.simps))) 1);
-by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
+by(rtac fields_rec_lemma 1);
+by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
+ba 1;
by( option_case_tac2 "sc" 1);
by( Asm_simp_tac 1);
by( case_tac "C = Object" 1);
by( rotate_tac 2 1);
by( Asm_full_simp_tac 1);
-by( dtac class_wf 1);
-by( atac 1);
-by( dtac wf_cdecl_supD 1);
-by( atac 1);
+by( datac class_wf 1 1);
+by( datac wf_cdecl_supD 1 1);
by( Asm_full_simp_tac 1);
qed "fields_rec";
@@ -211,12 +225,6 @@
by( Asm_full_simp_tac 1);
qed "unique_fields";
-(*####TO Trancl.ML*)
-Goal "(a,b):r^* ==> a=b | a~=b & (a,b):r^+";
-by(force_tac (claset(), simpset() addsimps [reflcl_trancl RS sym]
- delsimps [reflcl_trancl]) 1);
-qed "rtranclD";
-
Goal
"\\<lbrakk>wf_prog wf_mb G; G\\<turnstile>C'\\<preceq>C C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
\ map_of (fields (G,C')) f = Some ft";
--- a/src/HOL/MicroJava/J/WellType.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/WellType.thy Fri Jul 14 16:32:51 2000 +0200
@@ -96,8 +96,8 @@
(* cf. 15.15 *)
Cast "\\<lbrakk>E\\<turnstile>e\\<Colon>T;
- prg E\\<turnstile>T\\<preceq>? T'\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>Cast T' e\\<Colon>T'"
+ prg E\\<turnstile>T\\<preceq>? RefT rt\\<rbrakk> \\<Longrightarrow>
+ E\\<turnstile>Cast rt e\\<Colon>RefT rt"
(* cf. 15.7.1 *)
Lit "\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
@@ -129,7 +129,7 @@
FAss "\\<lbrakk>E\\<turnstile>{fd}a..fn\\<Colon>T;
E\\<turnstile>v \\<Colon>T';
prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
- E\\<turnstile>{fd}a..fn\\<in>=v\\<Colon>T'"
+ E\\<turnstile>{fd}a..fn:=v\\<Colon>T'"
(* cf. 15.11.1, 15.11.2, 15.11.3 *)
--- a/src/HOL/MicroJava/JVM/Object.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Object.thy Fri Jul 14 16:32:51 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 (Class C) hp oref) ClassCast;
+ xp' = raise_xcpt (\\<not> cast_ok G (ClassT C) hp oref) ClassCast;
stk' = if xp'=None then stk else tl stk
in
(xp' , stk' , pc+1))"