# HG changeset patch # User kleing # Date 1008458297 -3600 # Node ID 360e3215f029365b795c9c6788abaa00e55d1a18 # Parent d09d0f160888a7f65cbf0ead5843e750f20d8b74 exception merge, cleanup, tuned diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/Conform.thy --- a/src/HOL/MicroJava/J/Conform.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Conform.thy Sun Dec 16 00:18:17 2001 +0100 @@ -8,14 +8,14 @@ theory Conform = State + WellType: -types 'c env_ = "'c prog \ (vname \ ty)" (* same as env of WellType.thy *) +types 'c env_ = "'c prog \ (vname \ ty)" -- "same as @{text env} of @{text WellType.thy}" constdefs hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) "h<=|h' == \a C fs. h a = Some(C,fs) --> (\fs'. h' a = Some(C,fs'))" - conf :: "'c prog => aheap => val => ty => bool" + conf :: "'c prog => aheap => val => ty => bool" ("_,_ |- _ ::<= _" [51,51,51,51] 50) "G,h|-v::<=T == \T'. typeof (option_map obj_ty o h) v = Some T' \ G\T'\T" @@ -29,7 +29,7 @@ hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50) "G|-h h [ok] == \a obj. h a = Some obj --> G,h|-obj [ok]" - 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 [ok] \ prg E,heap s|-locals s[::<=]localT E" @@ -112,7 +112,8 @@ apply (simp) done -lemma defval_conf [rule_format (no_asm)]: "is_type G T --> G,h\default_val T::\T" +lemma defval_conf [rule_format (no_asm)]: + "is_type G T --> G,h\default_val T::\T" apply (unfold conf_def) apply (rule_tac "y" = "T" in ty.exhaust) apply (erule ssubst) @@ -127,7 +128,8 @@ apply auto done -lemma conf_widen [rule_format (no_asm)]: "wf_prog wf_mb G ==> G,h\x::\T --> G\T\T' --> G,h\x::\T'" +lemma conf_widen [rule_format (no_asm)]: + "wf_prog wf_mb G ==> G,h\x::\T --> G\T\T' --> G,h\x::\T'" apply (unfold conf_def) apply (rule val.induct) apply (auto intro: widen_trans) @@ -168,7 +170,8 @@ apply (fast dest: non_npD) done -lemma non_np_objD' [rule_format (no_asm)]: "a' \ Null ==> wf_prog wf_mb G ==> G,h\a'::\RefT t --> +lemma non_np_objD' [rule_format (no_asm)]: + "a' \ Null ==> wf_prog wf_mb G ==> G,h\a'::\RefT t --> (\C. t = ClassT C --> C \ Object) --> (\a C fs. a' = Addr a \ h a = Some (C,fs) \ G\Class C\RefT t)" apply(rule_tac "y" = "t" in ref_ty.exhaust) @@ -176,7 +179,9 @@ apply (fast dest: non_np_objD) done -lemma conf_list_gext_widen [rule_format (no_asm)]: "wf_prog wf_mb G ==> \Ts Ts'. list_all2 (conf G h) vs Ts --> list_all2 (\T T'. G\T\T') Ts Ts' --> list_all2 (conf G h) vs Ts'" +lemma conf_list_gext_widen [rule_format (no_asm)]: + "wf_prog wf_mb G ==> \Ts Ts'. list_all2 (conf G h) vs Ts --> + list_all2 (\T T'. G\T\T') Ts Ts' --> list_all2 (conf G h) vs Ts'" apply(induct_tac "vs") apply(clarsimp) apply(clarsimp) @@ -208,7 +213,8 @@ apply auto done -lemma lconf_init_vars_lemma [rule_format (no_asm)]: "\x. P x --> R (dv x) x ==> (\x. map_of fs f = Some x --> P x) --> +lemma lconf_init_vars_lemma [rule_format (no_asm)]: + "\x. P x --> R (dv x) x ==> (\x. map_of fs f = Some x --> P x) --> (\T. map_of fs f = Some T --> (\v. map_of (map (\(f,ft). (f, dv ft)) fs) f = Some v \ R v T))" apply( induct_tac "fs") @@ -231,7 +237,9 @@ apply auto done -lemma lconf_ext_list [rule_format (no_asm)]: "G,h\l[::\]L ==> \vs Ts. nodups vns --> length Ts = length vns --> list_all2 (\v T. G,h\v::\T) vs Ts --> G,h\l(vns[\]vs)[::\]L(vns[\]Ts)" +lemma lconf_ext_list [rule_format (no_asm)]: + "G,h\l[::\]L ==> \vs Ts. nodups vns --> length Ts = length vns --> + list_all2 (\v T. G,h\v::\T) vs Ts --> G,h\l(vns[\]vs)[::\]L(vns[\]Ts)" apply (unfold lconf_def) apply( induct_tac "vns") apply( clarsimp) @@ -291,12 +299,14 @@ apply( fast dest: conforms_localD elim!: conformsI lconf_hext) done -lemma conforms_upd_obj: "[|(h,l)::\(G, lT); G,h(a\obj)\obj\; h\|h(a\obj)|] ==> (h(a\obj),l)::\(G, lT)" -apply( rule conforms_hext) -apply auto -apply( rule hconfI) -apply( drule conforms_heapD) -apply( tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *}) +lemma conforms_upd_obj: + "[|(h,l)::\(G, lT); G,h(a\obj)\obj\; h\|h(a\obj)|] ==> (h(a\obj),l)::\(G, lT)" +apply(rule conforms_hext) +apply auto +apply(rule hconfI) +apply(drule conforms_heapD) +apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"] + addDs [thm "hconfD"], simpset() delsimps [split_paired_All]) *}) done lemma conforms_upd_local: diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/Decl.thy --- a/src/HOL/MicroJava/J/Decl.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Decl.thy Sun Dec 16 00:18:17 2001 +0100 @@ -4,38 +4,28 @@ Copyright 1999 Technische Universitaet Muenchen *) -header "Class Declarations and whole Programs" +header "Class Declarations and Programs" theory Decl = Type: -types fdecl (* field declaration, cf. 8.3 (, 9.3) *) - = "vname \ ty" +types + fdecl = "vname \ ty" -- "field declaration, cf. 8.3 (, 9.3)" + + sig = "mname \ ty list" -- "signature of a method, cf. 8.4.2" + + 'c mdecl = "sig \ ty \ 'c" -- "method declaration in a class" + + 'c class = "cname \ fdecl list \ 'c mdecl list" + -- "class = superclass, fields, methods" + + 'c cdecl = "cname \ 'c class" -- "class declaration, cf. 8.1" + + 'c prog = "'c cdecl list" -- "program" -types sig (* signature of a method, cf. 8.4.2 *) - = "mname \ ty list" - - 'c mdecl (* method declaration in a class *) - = "sig \ ty \ 'c" - -types 'c class (* class *) - = "cname \ fdecl list \ 'c mdecl list" - (* superclass, fields, methods*) - - 'c cdecl (* class declaration, cf. 8.1 *) - = "cname \ 'c class" - -consts - - Object :: cname (* name of root class *) - ObjectC :: "'c cdecl" (* decl of root class *) - -defs - - ObjectC_def: "ObjectC == (Object, (arbitrary, [], []))" - - -types 'c prog = "'c cdecl list" +constdefs + ObjectC :: "'c cdecl" -- "decl of root class" + "ObjectC \ (Object, (arbitrary, [], []))" translations @@ -46,12 +36,14 @@ "cdecl c" <= (type) "cname \ (c class)" "prog c" <= (type) "(c cdecl) list" -constdefs - class :: "'c prog => (cname \ 'c class)" - "class \ map_of" - is_class :: "'c prog => cname => bool" - "is_class G C \ class G C \ None" +constdefs + class :: "'c prog => (cname \ 'c class)" + "class \ map_of" + + is_class :: "'c prog => cname => bool" + "is_class G C \ class G C \ None" + lemma finite_is_class: "finite {C. is_class G C}" apply (unfold is_class_def class_def) @@ -60,11 +52,9 @@ done consts - - is_type :: "'c prog => ty => bool" - + is_type :: "'c prog => ty => bool" primrec -"is_type G (PrimT pt) = True" -"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)" + "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 d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/Eval.thy --- a/src/HOL/MicroJava/J/Eval.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Eval.thy Sun Dec 16 00:18:17 2001 +0100 @@ -4,7 +4,7 @@ Copyright 1999 Technische Universitaet Muenchen *) -header "Operational Evaluation (big-step) Semantics" +header "Operational Evaluation (big step) Semantics" theory Eval = State + WellType: @@ -40,24 +40,24 @@ "G\s -c -> (x,s')" <= "(s, c, x, s') \ exec G" "G\s -c -> s' " == "(s, c, s') \ exec G" + inductive "eval G" "evals G" "exec G" intros -(* evaluation of expressions *) + (* evaluation of expressions *) - (* cf. 15.5 *) - XcptE:"G\(Some xc,s) -e\arbitrary-> (Some xc,s)" + XcptE:"G\(Some xc,s) -e\arbitrary-> (Some xc,s)" -- "cf. 15.5" - (* cf. 15.8.1 *) + -- "cf. 15.8.1" NewC: "[| h = heap s; (a,x) = new_Addr h; h'= h(a\(C,init_vars (fields (G,C)))) |] ==> G\Norm s -NewC C\Addr a-> c_hupd h' (x,s)" - (* cf. 15.15 *) + -- "cf. 15.15" Cast: "[| G\Norm s0 -e\v-> (x1,s1); x2 = raise_if (\ cast_ok G C (heap s1) v) ClassCast x1 |] ==> G\Norm s0 -Cast C e\v-> (x2,s1)" - (* cf. 15.7.1 *) + -- "cf. 15.7.1" Lit: "G\Norm s -Lit v\v-> Norm s" BinOp:"[| G\Norm s -e1\v1-> s1; @@ -66,29 +66,27 @@ | Add => Intg (the_Intg v1 + the_Intg v2)) |] ==> G\Norm s -BinOp bop e1 e2\v-> s2" - (* cf. 15.13.1, 15.2 *) + -- "cf. 15.13.1, 15.2" LAcc: "G\Norm s -LAcc v\the (locals s v)-> Norm s" - (* cf. 15.25.1 *) + -- "cf. 15.25.1" LAss: "[| G\Norm s -e\v-> (x,(h,l)); l' = (if x = None then l(va\v) else l) |] ==> G\Norm s -va::=e\v-> (x,(h,l'))" - - (* cf. 15.10.1, 15.2 *) + -- "cf. 15.10.1, 15.2" FAcc: "[| G\Norm s0 -e\a'-> (x1,s1); v = the (snd (the (heap s1 (the_Addr a'))) (fn,T)) |] ==> G\Norm s0 -{T}e..fn\v-> (np a' x1,s1)" - (* cf. 15.25.1 *) + -- "cf. 15.25.1" FAss: "[| G\ Norm s0 -e1\a'-> (x1,s1); a = the_Addr a'; 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)" - - (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *) + -- "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'; G\s1 -ps[\]pvs-> (x,(h,l)); dynT = fst (the (h a)); (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs)); @@ -96,48 +94,51 @@ G\ s3 -res\v -> (x4,s4) |] ==> G\Norm s0 -{C}e..mn({pTs}ps)\v-> (x4,(heap s4,l))" -(* evaluation of expression lists *) - (* cf. 15.5 *) + -- "evaluation of expression lists" + + -- "cf. 15.5" XcptEs:"G\(Some xc,s) -e[\]arbitrary-> (Some xc,s)" - (* cf. 15.11.??? *) + -- "cf. 15.11.???" Nil: "G\Norm s0 -[][\][]-> Norm s0" - (* cf. 15.6.4 *) + -- "cf. 15.6.4" Cons: "[| G\Norm s0 -e \ v -> s1; G\ s1 -es[\]vs-> s2 |] ==> G\Norm s0 -e#es[\]v#vs-> s2" -(* execution of statements *) - (* cf. 14.1 *) + -- "execution of statements" + + -- "cf. 14.1" XcptS:"G\(Some xc,s) -c-> (Some xc,s)" - (* cf. 14.5 *) + -- "cf. 14.5" Skip: "G\Norm s -Skip-> Norm s" - (* cf. 14.7 *) + -- "cf. 14.7" Expr: "[| G\Norm s0 -e\v-> s1 |] ==> G\Norm s0 -Expr e-> s1" - (* cf. 14.2 *) + -- "cf. 14.2" Comp: "[| G\Norm s0 -c1-> s1; G\ s1 -c2-> s2|] ==> G\Norm s0 -c1;; c2-> s2" - (* cf. 14.8.2 *) + -- "cf. 14.8.2" Cond: "[| G\Norm s0 -e\v-> s1; G\ s1 -(if the_Bool v then c1 else c2)-> s2|] ==> G\Norm s0 -If(e) c1 Else c2-> s2" - (* cf. 14.10, 14.10.1 *) + -- "cf. 14.10, 14.10.1" LoopF:"[| G\Norm s0 -e\v-> s1; \the_Bool v |] ==> G\Norm s0 -While(e) c-> s1" LoopT:"[| G\Norm s0 -e\v-> s1; the_Bool v; - G\s1 -c-> s2; G\s2 -While(e) c-> s3 |] ==> + G\s1 -c-> s2; G\s2 -While(e) c-> s3 |] ==> G\Norm s0 -While(e) c-> s3" + lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)] lemma NewCI: "[|new_Addr (heap s) = (a,x); diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/Example.thy --- a/src/HOL/MicroJava/J/Example.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Example.thy Sun Dec 16 00:18:17 2001 +0100 @@ -1,4 +1,4 @@ -(* Title: isabelle/Bali/Example.thy +(* Title: HOL/MicroJava/J/Example.thy ID: $Id$ Author: David von Oheimb Copyright 1999 Technische Universitaet Muenchen @@ -41,12 +41,12 @@ datatype vnam_ = vee_ | x_ | e_ consts - cnam_ :: "cnam_ => cname" vnam_ :: "vnam_ => vnam" -axioms (* cnam_ and vnam_ are intended to be isomorphic to cnam and vnam *) - +-- "@{text cnam_} and @{text vnam_} are intended to be isomorphic + to @{text cnam} and @{text vnam}" +axioms inj_cnam_: "(cnam_ x = cnam_ y) = (x = y)" inj_vnam_: "(vnam_ x = vnam_ y) = (x = y)" @@ -56,7 +56,6 @@ declare inj_cnam_ [simp] inj_vnam_ [simp] syntax - Base :: cname Ext :: cname vee :: vname @@ -64,15 +63,13 @@ e :: vname translations - "Base" == "cnam_ Base_" - "Ext" == "cnam_ Ext_" + "Ext" == "cnam_ Ext_" "vee" == "VName (vnam_ vee_)" - "x" == "VName (vnam_ x_)" - "e" == "VName (vnam_ e_)" + "x" == "VName (vnam_ x_)" + "e" == "VName (vnam_ e_)" axioms - Base_not_Object: "Base \ Object" Ext_not_Object: "Ext \ Object" e_not_This: "e \ This" @@ -83,28 +80,26 @@ declare Ext_not_Object [THEN not_sym, simp] consts - foo_Base:: java_mb foo_Ext :: java_mb BaseC :: "java_mb cdecl" ExtC :: "java_mb cdecl" - test :: stmt - foo :: mname - a :: loc + test :: stmt + foo :: mname + a :: loc b :: loc defs - foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)" BaseC_def:"BaseC == (Base, (Object, - [(vee, PrimT Boolean)], - [((foo,[Class Base]),Class Base,foo_Base)]))" + [(vee, PrimT Boolean)], + [((foo,[Class Base]),Class Base,foo_Base)]))" foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext - (LAcc x)..vee:=Lit (Intg 1)), - Lit Null)" + (LAcc x)..vee:=Lit (Intg Numeral1)), + Lit Null)" ExtC_def: "ExtC == (Ext, (Base , - [(vee, PrimT Integer)], - [((foo,[Class Base]),Class Ext,foo_Ext)]))" + [(vee, PrimT Integer)], + [((foo,[Class Base]),Class Ext,foo_Ext)]))" test_def:"test == Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))" @@ -112,22 +107,21 @@ syntax - NP :: xcpt - tprg ::"java_mb prog" - obj1 :: obj - obj2 :: obj - s0 :: state - s1 :: state - s2 :: state - s3 :: state - s4 :: state + NP :: xcpt + tprg ::"java_mb prog" + obj1 :: obj + obj2 :: obj + s0 :: state + s1 :: state + s2 :: state + s3 :: state + s4 :: state translations - "NP" == "NullPointer" "tprg" == "[ObjectC, BaseC, ExtC]" "obj1" <= "(Ext, empty((vee, Base)\Bool False) - ((vee, Ext )\Intg 0))" + ((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))" @@ -141,7 +135,7 @@ lemma map_of_Cons2 [simp]: "aa\k ==> map_of ((k,bb)#ps) aa = map_of ps aa" apply (simp (no_asm_simp)) done -declare map_of_Cons [simp del]; (* sic! *) +declare map_of_Cons [simp del] -- "sic!" lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])" apply (unfold ObjectC_def class_def) @@ -150,7 +144,7 @@ lemma class_tprg_Base [simp]: "class tprg Base = Some (Object, - [(vee, PrimT Boolean)], + [(vee, PrimT Boolean)], [((foo, [Class Base]), Class Base, foo_Base)])" apply (unfold ObjectC_def BaseC_def ExtC_def class_def) apply (simp (no_asm)) @@ -158,7 +152,7 @@ lemma class_tprg_Ext [simp]: "class tprg Ext = Some (Base, - [(vee, PrimT Integer)], + [(vee, PrimT Integer)], [((foo, [Class Base]), Class Ext, foo_Ext)])" apply (unfold ObjectC_def BaseC_def ExtC_def class_def) apply (simp (no_asm)) @@ -328,25 +322,25 @@ ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *} lemma wt_test: "(tprg, empty(e\Class Base))\ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\" -apply (tactic t) (* ;; *) -apply (tactic t) (* Expr *) -apply (tactic t) (* LAss *) -apply simp (* e \ This *) -apply (tactic t) (* LAcc *) +apply (tactic t) -- ";;" +apply (tactic t) -- "Expr" +apply (tactic t) -- "LAss" +apply simp -- {* @{text "e \ This"} *} +apply (tactic t) -- "LAcc" apply (simp (no_asm)) apply (simp (no_asm)) -apply (tactic t) (* NewC *) +apply (tactic t) -- "NewC" apply (simp (no_asm)) apply (simp (no_asm)) -apply (tactic t) (* Expr *) -apply (tactic t) (* Call *) -apply (tactic t) (* LAcc *) +apply (tactic t) -- "Expr" +apply (tactic t) -- "Call" +apply (tactic t) -- "LAcc" apply (simp (no_asm)) apply (simp (no_asm)) -apply (tactic t) (* Cons *) -apply (tactic t) (* Lit *) +apply (tactic t) -- "Cons" +apply (tactic t) -- "Lit" apply (simp (no_asm)) -apply (tactic t) (* Nil *) +apply (tactic t) -- "Nil" apply (simp (no_asm)) apply (rule max_spec_foo_Base) done @@ -359,38 +353,38 @@ " [|new_Addr (heap (snd s0)) = (a, None)|] ==> tprg\s0 -test-> ?s" apply (unfold test_def) -(* ?s = s3 *) -apply (tactic e) (* ;; *) -apply (tactic e) (* Expr *) -apply (tactic e) (* LAss *) -apply (tactic e) (* NewC *) +-- "?s = s3 " +apply (tactic e) -- ";;" +apply (tactic e) -- "Expr" +apply (tactic e) -- "LAss" +apply (tactic e) -- "NewC" apply force apply force apply (simp (no_asm)) apply (erule thin_rl) -apply (tactic e) (* Expr *) -apply (tactic e) (* Call *) -apply (tactic e) (* LAcc *) +apply (tactic e) -- "Expr" +apply (tactic e) -- "Call" +apply (tactic e) -- "LAcc" apply force -apply (tactic e) (* Cons *) -apply (tactic e) (* Lit *) -apply (tactic e) (* Nil *) +apply (tactic e) -- "Cons" +apply (tactic e) -- "Lit" +apply (tactic e) -- "Nil" apply (simp (no_asm)) apply (force simp add: foo_Ext_def) apply (simp (no_asm)) -apply (tactic e) (* Expr *) -apply (tactic e) (* FAss *) -apply (tactic e) (* Cast *) -apply (tactic e) (* LAcc *) +apply (tactic e) -- "Expr" +apply (tactic e) -- "FAss" +apply (tactic e) -- "Cast" +apply (tactic e) -- "LAcc" apply (simp (no_asm)) apply (simp (no_asm)) apply (simp (no_asm)) -apply (tactic e) (* XcptE *) +apply (tactic e) -- "XcptE" apply (simp (no_asm)) apply (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force) apply (simp (no_asm)) apply (simp (no_asm)) -apply (tactic e) (* XcptE *) +apply (tactic e) -- "XcptE" done end diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/JBasis.thy --- a/src/HOL/MicroJava/J/JBasis.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/JBasis.thy Sun Dec 16 00:18:17 2001 +0100 @@ -13,9 +13,8 @@ section "unique" constdefs - unique :: "('a \ 'b) list => bool" - "unique == nodups \ map fst" + "unique == nodups \ map fst" lemma fst_in_set_lemma [rule_format (no_asm)]: @@ -71,4 +70,3 @@ done end - diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/JTypeSafe.thy --- a/src/HOL/MicroJava/J/JTypeSafe.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sun Dec 16 00:18:17 2001 +0100 @@ -161,7 +161,7 @@ declare fun_upd_same [simp] ML{* val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac, - (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)])) + (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)])) *} ML{* Unify.search_bound := 40; @@ -181,15 +181,16 @@ apply( rule eval_evals_exec_induct) apply( unfold c_hupd_def) -(* several simplifications, XcptE, XcptEs, XcptS, Skip, Nil?? *) +-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??" apply( simp_all) apply( tactic "ALLGOALS strip_tac") -apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) *}) -apply( tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") +apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") + THEN_ALL_NEW Full_simp_tac) *}) +apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") -(* Level 7 *) +-- "Level 7" -(* 15 NewC *) +-- "15 NewC" apply( drule new_AddrD) apply( erule disjE) prefer 2 @@ -201,13 +202,13 @@ apply( rule_tac [2] rtrancl_refl) apply( simp (no_asm)) -(* for Cast *) +-- "for Cast" defer 1 -(* 14 Lit *) +-- "14 Lit" apply( erule conf_litval) -(* 13 BinOp *) +-- "13 BinOp" apply (tactic "forward_hyp_tac") apply (tactic "forward_hyp_tac") apply( rule conjI, erule (1) hext_trans) @@ -216,46 +217,48 @@ apply( drule eval_no_xcpt) apply( simp split add: binop.split) -(* 12 LAcc *) +-- "12 LAcc" apply( fast elim: conforms_localD [THEN lconfD]) -(* for FAss *) -apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*}) +-- "for FAss" +apply( tactic {* EVERY'[eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") + THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*}) -(* for if *) +-- "for if" apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8*}) apply (tactic "forward_hyp_tac") -(* 11+1 if *) +-- "11+1 if" prefer 8 apply( fast intro: hext_trans) prefer 8 apply( fast intro: hext_trans) -(* 10 Expr *) +-- "10 Expr" prefer 6 apply( fast) -(* 9 ??? *) +-- "9 ???" apply( simp_all) -(* 8 Cast *) +-- "8 Cast" prefer 8 apply (rule impI) apply (drule raise_if_NoneD) apply (clarsimp) apply (fast elim: Cast_conf) -(* 7 LAss *) +-- "7 LAss" apply (fold fun_upd_def) -apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") THEN_ALL_NEW Full_simp_tac) 1 *}) +apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") + THEN_ALL_NEW Full_simp_tac) 1 *}) apply( blast intro: conforms_upd_local conf_widen) -(* 6 FAcc *) +-- "6 FAcc" apply( fast elim!: FAcc_type_sound) -(* 5 While *) +-- "5 While" prefer 5 apply(erule_tac V = "?a \ ?b" in thin_rl) apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop) @@ -263,15 +266,15 @@ apply (tactic "forward_hyp_tac") -(* 4 Cons *) +-- "4 Cons" prefer 3 apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) -(* 3 ;; *) +-- "3 ;;" prefer 3 apply( fast intro: hext_trans) -(* 2 FAss *) +-- "2 FAss" apply( case_tac "x2 = None") prefer 2 apply( simp (no_asm_simp)) @@ -281,9 +284,9 @@ apply( erule FAss_type_sound, rule HOL.refl, assumption+) apply( tactic prune_params_tac) -(* Level 52 *) +-- "Level 52" -(* 1 Call *) +-- "1 Call" apply( case_tac "x") prefer 2 apply( clarsimp) diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/State.thy --- a/src/HOL/MicroJava/J/State.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/State.thy Sun Dec 16 00:18:17 2001 +0100 @@ -8,58 +8,57 @@ theory State = TypeRel + Value: -types fields_ - = "(vname \ cname \ val)" (* field name, defining class, value *) +types + fields_ = "(vname \ cname \ val)" -- "field name, defining class, value" - obj = "cname \ fields_" (* class instance with class name and fields *) + obj = "cname \ fields_" -- "class instance with class name and fields" constdefs - obj_ty :: "obj => ty" + obj_ty :: "obj => ty" "obj_ty obj == Class (fst obj)" - init_vars :: "('a \ ty) list => ('a \ val)" - "init_vars == map_of o map (\(n,T). (n,default_val T))" + init_vars :: "('a \ ty) list => ('a \ val)" + "init_vars == map_of o map (\(n,T). (n,default_val T))" -datatype xcpt (* exceptions *) - = NullPointer - | ClassCast - | OutOfMemory + +types aheap = "loc \ obj" -- {* "@{text heap}" used in a translation below *} + locals = "vname \ val" -- "simple state, i.e. variable contents" -types aheap = "loc \ obj" (** "heap" used in a translation below **) - locals = "vname \ val" + state = "aheap \ locals" -- "heap, local parameter including This" + xstate = "xcpt option \ state" -- "state including exception information" + - state (* simple state, i.e. variable contents *) - = "aheap \ locals" - (* heap, local parameter including This *) +text {* + System exceptions are allocated in all heaps, + and they don't carry any information other than their type: *} +axioms + system_xcpt_allocated: "(hp::aheap) (XcptRef x) = Some (Xcpt x, empty)" - xstate (* state including exception information *) - = "xcpt option \ state" syntax - heap :: "state => aheap" - locals :: "state => locals" - Norm :: "state => xstate" + heap :: "state => aheap" + locals :: "state => locals" + Norm :: "state => xstate" translations "heap" => "fst" "locals" => "snd" - "Norm s" == "(None,s)" + "Norm s" == "(None,s)" constdefs - - new_Addr :: "aheap => loc \ xcpt option" + new_Addr :: "aheap => loc \ xcpt option" "new_Addr h == SOME (a,x). (h a = None \ x = None) | x = Some OutOfMemory" - raise_if :: "bool => xcpt => xcpt option => xcpt option" + raise_if :: "bool => xcpt => xcpt option => xcpt option" "raise_if c x xo == if c \ (xo = None) then Some x else xo" - np :: "val => xcpt option => xcpt option" + np :: "val => xcpt option => xcpt option" "np v == raise_if (v = Null) NullPointer" - c_hupd :: "aheap => xstate => xstate" + 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 => cname => aheap => val => bool" + cast_ok :: "'c prog => cname => aheap => val => bool" "cast_ok G C h v == v = Null \ G\obj_ty (the (h (the_Addr v)))\ Class C" lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C" @@ -93,7 +92,8 @@ apply auto done -lemma raise_if_Some2 [simp]: "raise_if c z (if x = None then Some y else x) \ None" +lemma raise_if_Some2 [simp]: + "raise_if c z (if x = None then Some y else x) \ None" apply (unfold raise_if_def) apply(induct_tac "x") apply auto @@ -105,12 +105,14 @@ apply auto done -lemma raise_if_NoneD [rule_format (no_asm)]: "raise_if c x y = None --> \ c \ y = None" +lemma raise_if_NoneD [rule_format (no_asm)]: + "raise_if c x y = None --> \ c \ y = None" apply (unfold raise_if_def) apply auto done -lemma np_NoneD [rule_format (no_asm)]: "np a' x' = None --> x' = None \ a' \ Null" +lemma np_NoneD [rule_format (no_asm)]: + "np a' x' = None --> x' = None \ a' \ Null" apply (unfold np_def raise_if_def) apply auto done diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/Term.thy --- a/src/HOL/MicroJava/J/Term.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Term.thy Sun Dec 16 00:18:17 2001 +0100 @@ -8,25 +8,24 @@ theory Term = Value: -datatype binop = Eq | Add (* function codes for binary operation *) +datatype binop = Eq | Add -- "function codes for binary operation" datatype expr - = NewC cname (* class instance creation *) - | Cast cname 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) + = NewC cname -- "class instance creation" + | Cast cname expr -- "type cast" + | Lit val -- "literal value, also references" + | BinOp binop expr expr -- "binary operation" + | LAcc vname -- "local (incl. parameter) access" + | LAss vname expr ("_::=_" [90,90]90) -- "local assign" + | FAcc cname expr vname ("{_}_.._" [10,90,99]90) -- "field access" | FAss cname expr vname - expr (* field ass. *) ("{_}_.._:=_" [10,90,99,90]90) + expr ("{_}_.._:=_" [10,90,99,90]90) -- "field ass." | Call cname expr mname - "ty list" "expr list" (* method call*) ("{_}_.._'( {_}_')" - [10,90,99,10,10] 90) + "ty list" "expr list" ("{_}_.._'( {_}_')" [10,90,99,10,10] 90) -- "method call" datatype stmt - = Skip (* empty statement *) - | Expr expr (* expression statement *) + = Skip -- "empty statement" + | Expr expr -- "expression statement" | Comp stmt stmt ("_;; _" [61,60]60) | Cond expr stmt stmt ("If '(_') _ Else _" [80,79,79]70) | Loop expr stmt ("While '(_') _" [80,79]70) diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/Type.thy --- a/src/HOL/MicroJava/J/Type.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Type.thy Sun Dec 16 00:18:17 2001 +0100 @@ -8,29 +8,47 @@ theory Type = JBasis: -typedecl cname (* class name *) -typedecl vnam (* variable or field name *) -typedecl mname (* method name *) +typedecl cnam + + -- "exceptions" +datatype + xcpt + = NullPointer + | ClassCast + | OutOfMemory -datatype vname (* names for This pointer and local/field variables *) +-- "class names" +datatype cname + = Object + | Xcpt xcpt + | Cname cname + +typedecl vnam -- "variable or field name" +typedecl mname -- "method name" + +-- "names for @{text This} pointer and local/field variables" +datatype vname = This | VName vnam -datatype prim_ty (* primitive type, cf. 4.2 *) - = Void (* 'result type' of void methods *) +-- "primitive type, cf. 4.2" +datatype prim_ty + = Void -- "'result type' of void methods" | Boolean | Integer -datatype ref_ty (* reference type, cf. 4.3 *) - = NullT (* null type, cf. 4.1 *) - | ClassT cname (* class type *) +-- "reference type, cf. 4.3" +datatype ref_ty + = NullT -- "null type, cf. 4.1" + | ClassT cname -- "class type" -datatype ty (* any type, cf. 4.1 *) - = PrimT prim_ty (* primitive type *) - | RefT ref_ty (* reference type *) +-- "any type, cf. 4.1" +datatype ty + = PrimT prim_ty -- "primitive type" + | RefT ref_ty -- "reference type" syntax - NT :: " ty" + NT :: "ty" Class :: "cname => ty" translations diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/TypeRel.thy Sun Dec 16 00:18:17 2001 +0100 @@ -9,9 +9,9 @@ theory TypeRel = Decl: consts - subcls1 :: "'c prog => (cname \ cname) set" (* subclass *) - widen :: "'c prog => (ty \ ty ) set" (* widening *) - cast :: "'c prog => (cname \ cname) set" (* casting *) + subcls1 :: "'c prog => (cname \ cname) set" -- "subclass" + widen :: "'c prog => (ty \ ty ) set" -- "widening" + cast :: "'c prog => (cname \ cname) set" -- "casting" syntax (xsymbols) subcls1 :: "'c prog => [cname, cname] => bool" ("_ \ _ \C1 _" [71,71,71] 70) @@ -31,9 +31,8 @@ "G\S \ T" == "(S,T) \ widen G" "G\C \? D" == "(C,D) \ cast G" +-- "direct subclass, cf. 8.1.3" inductive "subcls1 G" intros - - (* direct subclass, cf. 8.1.3 *) subcls1I: "\class G C = Some (D,rest); C \ Object\ \ G\C\C1D" lemma subcls1D: @@ -91,7 +90,7 @@ field :: "'c prog \ cname => ( vname \ cname \ ty )" (* ###curry *) fields :: "'c prog \ cname => ((vname \ cname) \ ty) list" (* ###curry *) -(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *) +-- "methods of a class, with inheritance, overriding and hiding, cf. 8.4.6" defs method_def: "method \ \(G,C). class_rec (G,C) empty (\C fs ms ts. ts ++ map_of (map (\(s,m). (s,(C,m))) ms))" @@ -105,7 +104,7 @@ done -(* list of fields of a class, including inherited and hidden ones *) +-- "list of fields of a class, including inherited and hidden ones" defs fields_def: "fields \ \(G,C). class_rec (G,C) [] (\C fs ms ts. map (\(fn,ft). ((fn,C),ft)) fs @ ts)" @@ -129,14 +128,15 @@ done -inductive "widen G" intros (*widening, viz. method invocation conversion,cf. 5.3 - i.e. sort of syntactic subtyping *) - refl [intro!, simp]: "G\ T \ T" (* identity conv., cf. 5.1.1 *) +-- "widening, viz. method invocation conversion,cf. 5.3 i.e. sort of syntactic subtyping" +inductive "widen G" intros + refl [intro!, simp]: "G\ T \ T" -- "identity conv., cf. 5.1.1" subcls : "G\C\C D ==> G\Class C \ Class D" null [intro!]: "G\ NT \ RefT R" -inductive "cast G" intros (* casting conversion, cf. 5.5 / 5.1.5 *) - (* left out casts on primitve types *) +-- "casting conversion, cf. 5.5 / 5.1.5" +-- "left out casts on primitve types" +inductive "cast G" intros widen: "G\C\C D ==> G\C \? D" subcls: "G\D\C C ==> G\C \? D" @@ -173,45 +173,11 @@ apply (auto elim: widen.subcls) done -lemma widen_trans [rule_format (no_asm)]: "G\S\U ==> \T. G\U\T --> G\S\T" -apply (erule widen.induct) -apply safe -apply (frule widen_Class) -apply (frule_tac [2] widen_RefT) -apply safe -apply(erule (1) rtrancl_trans) -done - - -(*####theorem widen_trans: "\G\S\U; G\U\T\ \ G\S\T" +theorem widen_trans[trans]: "\G\S\U; G\U\T\ \ G\S\T" proof - - assume "G\S\U" - thus "\T. G\U\T \ G\S\T" ( *(is "PROP ?P S U")* ) - proof (induct ( *cases* ) (open) ( *?P S U* ) rule: widen.induct [consumes 1]) - case refl - fix T' assume "G\T\T'" thus "G\T\T'". - ( * fix T' show "PROP ?P T T".* ) - next - case subcls - fix T assume "G\Class D\T" - then obtain E where "T = Class E" by (blast dest: widen_Class) - from prems show "G\Class C\T" proof (auto elim: rtrancl_trans) qed - next - case null - fix RT assume "G\RefT R\RT" - then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT) - thus "G\NT\RT" by auto - qed -qed -*) - -theorem widen_trans: "\G\S\U; G\U\T\ \ G\S\T" -proof - - assume "G\S\U" - thus "\T. G\U\T \ G\S\T" + assume "G\S\U" thus "\T. G\U\T \ G\S\T" proof induct - case (refl T T') - thus "G\T\T'" . + case (refl T T') thus "G\T\T'" . next case (subcls C D T) then obtain E where "T = Class E" by (blast dest: widen_Class) diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/Value.thy --- a/src/HOL/MicroJava/J/Value.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/Value.thy Sun Dec 16 00:18:17 2001 +0100 @@ -8,15 +8,19 @@ theory Value = Type: -typedecl loc (* locations, i.e. abstract references on objects *) +typedecl loc_ -- "locations, i.e. abstract references on objects" + +datatype loc + = XcptRef xcpt -- "special locations for pre-allocated system exceptions" + | Loc loc_ -- "usual locations (references on objects)" datatype val - = 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 *) + = 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 " consts the_Bool :: "val => bool" @@ -33,8 +37,8 @@ "the_Addr (Addr a) = a" consts - defpval :: "prim_ty => val" (* default value for primitive types *) - default_val :: "ty => val" (* default value for all types *) + defpval :: "prim_ty => val" -- "default value for primitive types" + default_val :: "ty => val" -- "default value for all types" primrec "defpval Void = Unit" diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/WellForm.thy --- a/src/HOL/MicroJava/J/WellForm.thy Sun Dec 16 00:17:44 2001 +0100 +++ b/src/HOL/MicroJava/J/WellForm.thy Sun Dec 16 00:18:17 2001 +0100 @@ -57,7 +57,7 @@ done lemma class_Object [simp]: - "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])" + "wf_prog wf_mb G ==> class G Object = Some (arbitrary, [], [])" apply (unfold wf_prog_def ObjectC_def class_def) apply (auto intro: map_of_SomeI) done @@ -205,13 +205,15 @@ apply auto done -lemma widen_fields_defpl: "[|((fn,fd),fT) \ set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==> +lemma widen_fields_defpl: + "[|((fn,fd),fT) \ set (fields (G,C)); wf_prog wf_mb G; is_class G C|] ==> G\C\C fd" apply( drule (1) widen_fields_defpl') apply (fast) done -lemma unique_fields: "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))" +lemma unique_fields: + "[|is_class G C; wf_prog wf_mb G|] ==> unique (fields (G,C))" apply( erule subcls1_induct) apply( assumption) apply( safe dest!: wf_cdecl_supD) @@ -232,7 +234,8 @@ apply(auto dest!: widen_fields_defpl) done -lemma fields_mono_lemma [rule_format (no_asm)]: "[|wf_prog wf_mb G; (C',C)\(subcls1 G)^*|] ==> +lemma fields_mono_lemma [rule_format (no_asm)]: + "[|wf_prog wf_mb G; (C',C)\(subcls1 G)^*|] ==> x \ set (fields (G,C)) --> x \ set (fields (G,C'))" apply(erule converse_rtrancl_induct) apply( safe dest!: subcls1D) @@ -260,7 +263,8 @@ apply (fast dest: fields_mono) done -lemma method_wf_mdecl [rule_format (no_asm)]: "wf_prog wf_mb G ==> is_class G C \ +lemma method_wf_mdecl [rule_format (no_asm)]: + "wf_prog wf_mb G ==> is_class G C \ method (G,C) sig = Some (md,mh,m) --> G\C\C md \ wf_mdecl wf_mb G md (sig,(mh,m))" apply( erule subcls1_induct) @@ -322,10 +326,13 @@ "[| G\ C\C D; wf_prog wf_mb G; method (G,D) sig = Some (md, rT, b) |] ==> \