# HG changeset patch # User oheimb # Date 963585171 -7200 # Node ID 297dcbf64526488307d1a8ada6833cddf6260b70 # Parent 2f5f6824f88889817feee2752b295ebf766ea580 re-structuring MicroJava; added Example; corrected := syntax; simplfied cast diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/IsaMakefile --- 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 \ diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML --- 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] - "\\ wf_prog ok G; G,h\\v\\\\RefT rt; cast_ok G (Class C) h v ; G\\(Class C)\\T'; is_class G C \\ \ + "\\ wf_prog ok G; G,h\\v\\\\RefT rt; cast_ok G (ClassT C) h v ; G\\(Class C)\\T'; is_class G C \\ \ \ \\ G,h\\v\\\\T'"; -be disjE 1; - by (Clarify_tac 1); by (forward_tac [widen_Class] 1); by (Clarify_tac 1); be disjE 1; diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Conform.thy --- 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 \\ (vname \\ ty)" (* same as env of WellType.thy *) constdefs @@ -26,7 +28,7 @@ hconf :: "'c prog \\ aheap \\ bool" ("_\\h _\\" [51,51] 50) "G\\h h\\ \\ \\a obj. h a = Some obj \\ G,h\\obj\\" - conforms :: "state \\ java_mb env \\ bool" ("_\\\\_" [51,51] 50) + conforms :: "state \\ java_mb env_ \\ bool" ("_\\\\_" [51,51] 50) "s\\\\E \\ prg E\\h heap s\\ \\ prg E,heap s\\locals s[\\\\]localT E" end diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Decl.thy --- 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 \\ (Object, (None, [], []))" + +types 'c prog = "'c cdecl list" + +consts + + class :: "'c prog \\ (cname \\ 'c class)" + + is_class :: "'c prog \\ cname \\ bool" + is_type :: "'c prog \\ ty \\ bool" + +defs + + class_def "class \\ map_of" + + is_class_def "is_class G C \\ class G C \\ None" + +primrec +"is_type G (PrimT pt) = True" +"is_type G (RefT t) = (case t of NullT \\ True | ClassT C \\ is_class G C)" + end diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Eval.ML --- 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 "\\new_Addr (heap s) = (a,x); \ +\ s' = c_hupd (heap s(a\\(C,init_vars (fields (G,C))))) (x,s)\\ \\ \ +\ G\\Norm s -NewC C\\Addr a\\ s'"; +by (hyp_subst_tac 1); +br eval_evals_exec.NewC 1; +by Auto_tac; +qed "NewCI"; + Goal "\\s s'. (G\\(x,s) -e \\ v \\ (x',s') \\ x'=None \\ x=None) \\ \ \ (G\\(x,s) -es[\\]vs\\ (x',s') \\ x'=None \\ x=None) \\ \ \ (G\\(x,s) -c \\ (x',s') \\ x'=None \\ x=None)"; diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Eval.thy --- 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 \\ (xstate \\ expr \\ val \\ xstate) set" @@ -73,7 +73,7 @@ G\\(np a' x1,s1) -e2\\v \\ (x2,s2); h = heap s2; (c,fs) = the (h a); h' = h(a\\(c,(fs((fn,T)\\v))))\\ \\ - G\\Norm s0 -{T}e1..fn\\=e2\\v\\ c_hupd h' (x2,s2)" + G\\Norm s0 -{T}e1..fn:=e2\\v\\ 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 "\\G\\Norm s0 -e\\a'\\ s1; a = the_Addr a'; diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Example.ML --- /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"] +"\\X. x\\k \\ 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 "\\X. (Object,C) \\ (subcls1 tprg)^+ \\ R"; +by (auto_tac (claset() addSDs [tranclD,subcls1D],simpset())); +qed "not_Object_subcls"; +AddSEs [not_Object_subcls]; + +Goal "tprg\\Object\\C C \\ C = Object"; +be rtrancl_induct 1; +by Auto_tac; +bd subcls1D 1; +by Auto_tac; +qed "subcls_ObjectD"; +AddSDs[subcls_ObjectD]; + +Goal "\\X. (Base, Ext) \\ (subcls1 tprg)^+ \\ 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 \\ C=Object \\ C=Base \\ C=Ext"; +by (auto_tac (claset(),simpset()addsimps[]addsplits[split_if_asm])); +qed "class_tprgD"; + +Goal "(C,C) \\ (subcls1 tprg)^+ \\ 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\\Ext\\C Base"; +br subcls_direct 1; +by (Simp_tac 1); +qed "Ext_subcls_Base"; +Addsimps [Ext_subcls_Base]; + +Goalw [] "tprg\\Class Ext\\ 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) \\ 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\\NT\\ 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\\Class Base))\\\ +\ Expr(e\\=NewC Ext);; Expr(LAcc e..foo({?pTs'}[Lit Null]))\\"; +(* ?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] +" \\new_Addr (heap (snd s0)) = (a, None)\\ \\ \ +\ tprg\\s0 -test\\ ?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"; diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Example.thy --- /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_ \\ cname" + vnam_ :: "vnam_ \\ 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_ "\\m. n = cnam_ m" + surj_vnam_ "\\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 \\ Object" + Ext_not_Object "Ext \\ 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 \\ ([x],[],Skip,LAcc x)" + BaseC_def "BaseC \\ (Base, (Some Object, + [(vee, PrimT Boolean)], + [((foo,[Class Base]),Class Base,foo_Base)]))" + foo_Ext_def "foo_Ext \\ ([x],[],Expr( {Ext}Cast (ClassT Ext) + (LAcc x)..vee:=Lit (Intg #1)), + Lit Null)" + ExtC_def "ExtC \\ (Ext, (Some Base , + [(vee, PrimT Integer)], + [((foo,[Class Base]),Class Ext,foo_Ext)]))" + + test_def "test \\ Expr(e\\=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)\\Bool False) + ((vee, Ext )\\Intg #0))" + "s0" == " Norm (empty � ,empty � � )" + "s1" == " Norm (empty(a\\obj1),empty(e\\Addr a) � )" + "s2" == " Norm (empty(a\\obj1),empty(x\\Null)(This\\Addr a))" + "s3" == "(Some NP, empty(a\\obj1),empty(x\\Null)(This\\Addr a))" +end diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/JTypeSafe.ML --- 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\\Unit\\\\PrimT Void"; -by( Simp_tac 1); -qed "conf_VoidI"; - -Goalw [conf_def] "G,s\\Bool b\\\\PrimT Boolean"; -by( Simp_tac 1); -qed "conf_BooleanI"; - -Goalw [conf_def] "G,s\\Intg i\\\\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] - "\\ wf_prog wf_mb G; G,h\\v\\\\Tb; G\\Tb\\? T'; cast_ok G T' h v\\ \ -\ \\ G,h\\v\\\\T'"; + "\\ wf_prog wf_mb G; G,h\\v\\\\Tb; G\\Tb\\? RefT T'; cast_ok G T' h v\\ \ +\ \\ G,h\\v\\\\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 "\\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); diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Prog.thy --- 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 \\ (cname \\ 'c class)" - - is_class :: "'c prog \\ cname \\ bool" - is_type :: "'c prog \\ ty \\ bool" - -defs - - class_def "class \\ map_of" - - is_class_def "is_class G C \\ class G C \\ None" - -primrec -"is_type G (PrimT pt) = True" -"is_type G (RefT t) = (case t of NullT \\ True | ClassT C \\ is_class G C)" - -end diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/State.thy --- 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 \\ bool" - the_Intg :: "val \\ int" - the_Addr :: "val \\ loc" - - defpval :: "prim_ty \\ val" (* default value for primitive types *) - default_val :: "ty \\ 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 \\ cname \\ val)" (* field name, defining class, value *) -types obj = "cname \\ fields_" (* class instance with class name and fields *) + obj = "cname \\ fields_" (* class instance with class name and fields *) constdefs @@ -86,7 +60,7 @@ c_hupd :: "aheap \\ xstate \\ xstate" "c_hupd h'\\ \\(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))" - cast_ok :: "'c prog \\ ty \\ aheap \\ val \\ bool" - "cast_ok G T h v \\ ((\\pt. T = PrimT pt) | (v=Null) | G\\obj_ty (the (h (the_Addr v)))\\T)" + cast_ok :: "'c prog \\ ref_ty \\ aheap \\ val \\ bool" + "cast_ok G T h v \\ (v=Null) | G\\obj_ty (the (h (the_Addr v)))\\RefT T" end diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Term.thy --- 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 *) ("_\\=_" [ 90,90]90) | FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90) | FAss cname expr vname - expr (* field ass. *)("{_}_.._\\=_"[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 diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Type.ML --- 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 "(\\pt. T \\ PrimT pt) = (\\t. T = RefT t)"; -by(case_tac "T" 1); -by Auto_tac; -qed "non_PrimT"; diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/TypeRel.thy --- 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 \\ (cname \\ cname) set" (* subclass *) diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/Value.thy --- /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 \\ bool" + the_Intg :: "val \\ int" + the_Addr :: "val \\ loc" + +primrec + "the_Bool (Bool b) = b" + +primrec + "the_Intg (Intg i) = i" + +primrec + "the_Addr (Addr a) = a" + +consts + defpval :: "prim_ty \\ val" (* default value for primitive types *) + default_val :: "ty \\ 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 diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/WellForm.ML --- 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 \\ method (G,C) = \ +Goal "\\wf ((subcls1 G)^-1); \\D fs ms. class G C = Some (Some D,fs,ms) \\ is_class G D\\ \\ method (G,C) = \ \ (case class G C of None \\ empty | Some (sc,fs,ms) \\ \ \ (case sc of None \\ empty | Some D \\ method (G,D)) \\ \ \ map_of (map (\\(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 \\ method (G,C) = \ +\ (case class G C of None \\ empty | Some (sc,fs,ms) \\ \ +\ (case sc of None \\ empty | Some D \\ method (G,D)) \\ \ +\ map_of (map (\\(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 "\\wf ((subcls1 G)^-1); class G C = Some (sc,fs,ms); \\C. sc = Some C \\ is_class G C\\ \\ fields (G,C) = \ +\ map (\\(fn,ft). ((fn,C),ft)) fs @ \ +\ (case sc of None \\ [] | Some D \\ 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 "\\class G C = Some (sc,fs,ms); wf_prog wf_mb G\\ \\ fields (G,C) = \ \ map (\\(fn,ft). ((fn,C),ft)) fs @ \ \ (case sc of None \\ [] | Some D \\ 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 "\\wf_prog wf_mb G; G\\C'\\C C; map_of(fields (G,C )) f = Some ft\\ \\ \ \ map_of (fields (G,C')) f = Some ft"; diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/J/WellType.thy --- 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 "\\E\\e\\T; - prg E\\T\\? T'\\ \\ - E\\Cast T' e\\T'" + prg E\\T\\? RefT rt\\ \\ + E\\Cast rt e\\RefT rt" (* cf. 15.7.1 *) Lit "\\typeof (\\v. None) x = Some T\\ \\ @@ -129,7 +129,7 @@ FAss "\\E\\{fd}a..fn\\T; E\\v \\T'; prg E\\T'\\T\\ \\ - E\\{fd}a..fn\\=v\\T'" + E\\{fd}a..fn:=v\\T'" (* cf. 15.11.1, 15.11.2, 15.11.3 *) diff -r 2f5f6824f888 -r 297dcbf64526 src/HOL/MicroJava/JVM/Object.thy --- 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 (\\ cast_ok G (Class C) hp oref) ClassCast; + xp' = raise_xcpt (\\ cast_ok G (ClassT C) hp oref) ClassCast; stk' = if xp'=None then stk else tl stk in (xp' , stk' , pc+1))"