# HG changeset patch # User nipkow # Date 943602419 -3600 # Node ID 6fc37b5c5e9827b982af772aa265256272b81ffb # Parent 325b8e754523f68c1603035cef046ed64ebdb5d9 Various little changes like cmethd -> method and cfield -> field. diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/BV/BVSpec.ML --- a/src/HOL/MicroJava/BV/BVSpec.ML Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/BV/BVSpec.ML Fri Nov 26 08:46:59 1999 +0100 @@ -11,19 +11,19 @@ Goalw [wt_jvm_prog_def] "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \ +\ method (G,C) sig = Some (C,rT,maxl,ins); \ \ pc < length ins \\ \ \\\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; -by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1); +by(forward_tac [rotate_prems 2 method_wf_mdecl] 1); by (Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1); qed "wt_jvm_prog_impl_wt_instr"; Goalw [wt_jvm_prog_def] "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) sig = Some (C,rT,maxl,ins) \\ \\ \ +\ method (G,C) sig = Some (C,rT,maxl,ins) \\ \\ \ \ 0 < (length ins) \\ wt_start G C (snd sig) maxl (phi C sig)"; -by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1); +by(forward_tac [rotate_prems 2 method_wf_mdecl] 1); by (Asm_full_simp_tac 1); by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1); qed "wt_jvm_prog_impl_wt_start"; diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/BV/BVSpec.thy --- a/src/HOL/MicroJava/BV/BVSpec.thy Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Fri Nov 26 08:46:59 1999 +0100 @@ -52,7 +52,7 @@ in pc+1 < max_pc \\ is_class G C \\ - (\\T oT ST'. cfield (G,C) F = Some(C,T) \\ + (\\T oT ST'. field (G,C) F = Some(C,T) \\ ST = oT # ST' \\ G \\ oT \\ (Class C) \\ G \\ (T # ST' , LT) <=s phi ! (pc+1)))" @@ -63,7 +63,7 @@ pc+1 < max_pc \\ is_class G C \\ (\\T vT oT ST'. - cfield (G,C) F = Some(C,T) \\ + field (G,C) F = Some(C,T) \\ ST = vT # oT # ST' \\ G \\ oT \\ (Class C) \\ G \\ vT \\ T \\ @@ -155,7 +155,7 @@ (\\apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\ length apTs = length fpTs \\ (\\(aT,fT)\\set(zip apTs fpTs). G \\ aT \\ fT) \\ - (\\D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\ + (\\D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\ G \\ (rT # ST' , LT) <=s phi ! (pc+1))))" consts diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Fri Nov 26 08:46:59 1999 +0100 @@ -9,7 +9,7 @@ Goalw [correct_state_def,Let_def,correct_frame_def,split_def] "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \ +\ method (G,C) sig = Some (C,rT,maxl,ins); \ \ G,phi \\JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\ \\ \ \\\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; by (Asm_full_simp_tac 1); @@ -24,7 +24,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = LS(Load idx); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ @@ -38,7 +38,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = LS(Store idx); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ @@ -56,7 +56,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = LS(Bipush i); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ @@ -80,7 +80,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = LS Aconst_null; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ @@ -93,7 +93,7 @@ Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = LS ls_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ @@ -127,14 +127,14 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = CH (Checkcast D); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ \\\ G,phi \\JVM (xp',hp',frs')\\"; by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons, - xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); + raise_xcpt_def]@defs1 addsplits [option.split]) 1); by (fast_tac (claset() addDs [approx_stk_Cons_lemma] addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2] addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,approx_val_def])) 1); @@ -143,7 +143,7 @@ Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = CH ch_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ @@ -160,13 +160,13 @@ (******* MO *******) Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = MO (Getfield F D); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ \\\ G,phi \\JVM (xp',hp',frs')\\"; -by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); +by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); by (Clarify_tac 1); @@ -199,13 +199,13 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = MO (Putfield F D); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ \\\ G,phi \\JVM (xp',hp',frs')\\"; -by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1); +by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1); by (Clarify_tac 1); @@ -228,7 +228,7 @@ Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = MO mo_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ @@ -250,7 +250,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = CO(New cl_idx); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ @@ -262,13 +262,13 @@ hconf_imp_hconf_newref,correct_frames_imp_correct_frames_newref, rewrite_rule [split_def] correct_init_obj] addss (simpset() addsimps [NT_subtype_conv,approx_stk_Cons,approx_val_def,conf_def, - fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,xcpt_update_def,raise_xcpt_def,init_vars_def]@defs1 + fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,raise_xcpt_def,init_vars_def]@defs1 addsplits [option.split])) 1); qed "New_correct"; Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = CO co_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ @@ -286,7 +286,7 @@ Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins ! pc = MI(Invoke mn pTs); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ @@ -294,7 +294,7 @@ \\\ G,phi \\JVM (xp',hp',frs')\\"; by(forward_tac [wt_jvm_progD] 1); by(etac exE 1); -by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1 +by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1 addsplits [option.split]) 1); by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps []@defs1) 1); @@ -315,11 +315,11 @@ by(rename_tac "oT'" 1); by (Clarify_tac 1); by(subgoal_tac "G \\ Class oT \\ Class oT'" 1); - by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 cmethd_wf_mdecl)) 2); + by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 method_wf_mdecl)) 2); ba 2; by(Blast_tac 2); by (asm_full_simp_tac (simpset() addsimps []@defs1) 1); -by(forward_tac [cmethd_in_md] 1); +by(forward_tac [method_in_md] 1); ba 1; back(); back(); @@ -365,7 +365,7 @@ Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = MI mi_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ @@ -394,7 +394,7 @@ Delsimps [map_append]; Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins ! pc = MR Return; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ @@ -423,7 +423,7 @@ Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = MR mr; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ @@ -438,7 +438,7 @@ (****** BR ******) Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins ! pc = BR(Goto branch); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ @@ -451,7 +451,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = BR(Ifcmpeq branch); \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ @@ -464,7 +464,7 @@ Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = BR br_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ @@ -482,7 +482,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins ! pc = OS Pop; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ @@ -495,7 +495,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins ! pc = OS Dup; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ @@ -509,7 +509,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins ! pc = OS Dup_x1; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ @@ -522,7 +522,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins ! pc = OS Dup_x2; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ @@ -535,7 +535,7 @@ Goal "\\ wf_prog wt G; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins ! pc = OS Swap; \ \ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \ @@ -548,7 +548,7 @@ Goal "\\ wt_jvm_prog G phi; \ -\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \ +\ method (G,C) ml = Some (C,rT,maxl,ins); \ \ ins!pc = OS os_com; \ \ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \ \ G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \\ \ @@ -565,10 +565,10 @@ Goalw [correct_state_def,Let_def] "G,phi \\JVM (None, hp, (stk,loc,C,ml,pc)#frs)\\ \ -\ \\ \\meth. cmethd (G,C) ml = Some(C,meth)"; +\ \\ \\meth. method (G,C) ml = Some(C,meth)"; by(Asm_full_simp_tac 1); by(Blast_tac 1); -qed "correct_state_impl_Some_cmethd"; +qed "correct_state_impl_Some_method"; Goal "\\state. \\ wt_jvm_prog G phi; G,phi \\JVM state\\\\ \ @@ -580,7 +580,7 @@ by (asm_full_simp_tac (simpset() addsimps exec.rules) 1); by(split_all_tac 1); by(hyp_subst_tac 1); - by(forward_tac [correct_state_impl_Some_cmethd] 1); + by(forward_tac [correct_state_impl_Some_method] 1); by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct, BR_correct], simpset() addsplits [instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1); by (exhaust_tac "frs" 1); diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/BV/Correct.thy --- a/src/HOL/MicroJava/BV/Correct.thy Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Fri Nov 26 08:46:59 1999 +0100 @@ -34,14 +34,14 @@ (ST,LT) = (phi C ml) ! pc in (\\rT maxl ins. - cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\ + method (G,C) ml = Some(C,rT,(maxl,ins)) \\ (\\mn pTs k. pc = k+1 \\ ins!k = MI(Invoke mn pTs) \\ (mn,pTs) = ml0 \\ (\\apTs D ST'. fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\ length apTs = length pTs \\ (\\D' rT' maxl' ins'. - cmethd (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\ + method (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\ G \\ rT0 \\ rT') \\ correct_frame G hp (tl ST, LT) maxl ins f \\ correct_frames G hp phi rT C ml frs))))" @@ -57,7 +57,7 @@ | (f#fs) \\ (let (stk,loc,C,ml,pc) = f in \\rT maxl ins. - cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\ + method (G,C) ml = Some(C,rT,(maxl,ins)) \\ G\\h hp\\ \\ correct_frame G hp ((phi C ml) ! pc) maxl ins f \\ correct_frames G hp phi rT C ml fs)) diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/J/Eval.thy --- a/src/HOL/MicroJava/J/Eval.thy Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/J/Eval.thy Fri Nov 26 08:46:59 1999 +0100 @@ -72,7 +72,7 @@ (* 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 (cmethd (G,dynT) (mn,pTs)); + (md,rT,pns,lvars,blk,res) = the (method (G,dynT) (mn,pTs)); G\\(np a' x,(h,(init_vars lvars)(pns[\\]pvs)(This\\a'))) -blk\\ s3; G\\ s3 -res\\v \\ (x4,s4)\\ \\ G\\Norm s0 -e..mn({pTs}ps)\\v\\ (x4,(heap s4,l))" diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/J/JTypeSafe.ML --- a/src/HOL/MicroJava/J/JTypeSafe.ML Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML Fri Nov 26 08:46:59 1999 +0100 @@ -44,7 +44,7 @@ by Auto_tac; qed "Cast_conf"; -Goal "\\ wf_prog wtm G; cfield (G,C) fn = Some (fd, ft); (h,l)\\\\(G,lT); \ +Goal "\\ wf_prog wtm G; field (G,C) fn = Some (fd, ft); (h,l)\\\\(G,lT); \ \ x' = None \\ G,h\\a'\\\\Class C; np a' x' = None \\ \\ \ \ G,h\\the (snd (the (h (the_Addr a'))) (fn, fd))\\\\ft"; by( dtac np_NoneD 1); @@ -66,7 +66,7 @@ "\\ wf_prog wtm G; a = the_Addr a'; (c, fs) = the (h a); \ \ (G, lT)\\v\\T'; G\\T'\\ft; \ \ (G, lT)\\aa\\Class C; \ -\ cfield (G,C) fn = Some (fd, ft); h''\\|h'; \ +\ field (G,C) fn = Some (fd, ft); h''\\|h'; \ \ x' = None \\ G,h'\\a'\\\\Class C; h'\\|h; \ \ (h, l)\\\\(G, lT); G,h\\x\\\\T'; np a' x' = None\\ \\ \ \ h''\\|h(a\\(c,(fs((fn,fd)\\x)))) \\ \ @@ -126,7 +126,7 @@ \ max_spec G T (mn,pTsa) = {((mda,rTa),pTs')}; xc\\|xh; xh\\|h; \ \ list_all2 (conf G h) pvs pTsa;\ \ (md, rT, pns, lvars, blk, res) = \ -\ the (cmethd (G,fst (the (h (the_Addr a')))) (mn, pTs'));\ +\ the (method (G,fst (the (h (the_Addr a')))) (mn, pTs'));\ \ \\lT. (h, init_vars lvars(pns[\\]pvs)(This\\a'))\\\\(G, lT) \\ \ \ (G, lT)\\blk\\ \\ h\\|xi \\ (xi, xl)\\\\(G, lT); \ \ \\lT. (xi, xl)\\\\(G, lT) \\ (\\T. (G, lT)\\res\\T \\ \ @@ -146,7 +146,7 @@ by( Clarsimp_tac 1); by( EVERY'[dtac Call_lemma, atac, atac] 1); by( clarsimp_tac (claset(),simpset() addsimps [wt_java_mdecl_def])1); -by( thin_tac "cmethd ?sig ?x = ?y" 1); +by( thin_tac "method ?sig ?x = ?y" 1); by( EVERY'[dtac spec, etac impE] 1); by( mp_tac 2); by( rtac conformsI 1); @@ -326,7 +326,7 @@ Goal "\\G=prg E; wf_java_prog G; G\\(x,s) -e\\a'\\ Norm s'; a' \\ Null;\ \ s\\\\E; E\\e\\RefT T; m_head G T sig \\ None\\ \\ \ -\ cmethd (G,fst (the (heap s' (the_Addr a')))) sig \\ None"; +\ method (G,fst (the (heap s' (the_Addr a')))) sig \\ None"; by( dtac eval_type_sound 1); by( atac 1); by( atac 1); diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/J/TypeRel.ML --- a/src/HOL/MicroJava/J/TypeRel.ML Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/J/TypeRel.ML Fri Nov 26 08:46:59 1999 +0100 @@ -76,8 +76,8 @@ by(Force_tac 1); val wf_subcls1_rel = result(); -val cmethd_TC = prove_goalw_cterm [subcls1_rel_def] - (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (cmethd.tcs))))) +val method_TC = prove_goalw_cterm [subcls1_rel_def] + (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (method.tcs))))) (K [auto_tac (claset() addIs [subcls1I], simpset())]); val fields_TC = prove_goalw_cterm [subcls1_rel_def] diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/J/TypeRel.thy Fri Nov 26 08:46:59 1999 +0100 @@ -32,8 +32,8 @@ consts - cmethd :: "'c prog \\ cname \\ ( sig \\ cname \\ ty \\ 'c)" - cfield :: "'c prog \\ cname \\ ( vname \\ cname \\ ty)" + method :: "'c prog \\ cname \\ ( sig \\ cname \\ ty \\ 'c)" + field :: "'c prog \\ cname \\ ( vname \\ cname \\ ty)" fields :: "'c prog \\ cname \\ ((vname \\ cname) \\ ty) list" constdefs (* auxiliary relations for recursive definitions below *) @@ -42,10 +42,10 @@ "subcls1_rel \\ {((G,C),(G',C')). G = G' \\ wf ((subcls1 G)^-1) \\ G\\C'\\C1C}" (* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *) -recdef cmethd "subcls1_rel" - "cmethd (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\ empty +recdef method "subcls1_rel" + "method (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\ empty | Some (sc,fs,ms) \\ (case sc of None \\ empty | Some D \\ - if is_class G D then cmethd (G,D) + if is_class G D then method (G,D) else arbitrary) \\ map_of (map (\\(s, m ). (s,(C,m))) ms)) @@ -61,7 +61,7 @@ else arbitrary)" defs - cfield_def "cfield \\ map_of o (map (\\((fn,fd),ft). (fn,(fd,ft)))) o fields" + field_def "field \\ map_of o (map (\\((fn,fd),ft). (fn,(fd,ft)))) o fields" inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3 i.e. sort of syntactic subtyping *) diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/J/WellForm.ML --- a/src/HOL/MicroJava/J/WellForm.ML Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/J/WellForm.ML Fri Nov 26 08:46:59 1999 +0100 @@ -111,11 +111,11 @@ by( etac subcls1I 1); qed "subcls1_induct"; -Goal "wf_prog wtm G \\ cmethd (G,C) = \ +Goal "wf_prog wtm G \\ method (G,C) = \ \ (case class G C of None \\ empty | Some (sc,fs,ms) \\ \ -\ (case sc of None \\ empty | Some D \\ cmethd (G,D)) \\ \ +\ (case sc of None \\ empty | Some D \\ method (G,D)) \\ \ \ map_of (map (\\(s,m). (s,(C,m))) ms))"; -by( stac (cmethd_TC RS (wf_subcls1_rel RS (hd cmethd.rules))) 1); +by( stac (method_TC RS (wf_subcls1_rel RS (hd method.rules))) 1); by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def] addsplits [option.split]) 1); by( case_tac "C = Object" 1); @@ -125,7 +125,7 @@ by( dtac wf_cdecl_supD 1); by( atac 1); by( Asm_full_simp_tac 1); -val cmethd_rec = result(); +val method_rec = result(); Goal "\\class G C = Some (sc,fs,ms); wf_prog wtm G\\ \\ fields (G,C) = \ \ map (\\(fn,ft). ((fn,C),ft)) fs @ \ @@ -144,14 +144,14 @@ by( Asm_full_simp_tac 1); val fields_rec = result(); -val cmethd_Object = prove_goal thy "\\X. wf_prog wtm G \\ cmethd (G,Object) = empty" - (K [stac cmethd_rec 1,Auto_tac]); +val method_Object = prove_goal thy "\\X. wf_prog wtm G \\ method (G,Object) = empty" + (K [stac method_rec 1,Auto_tac]); val fields_Object = prove_goal thy "\\X. wf_prog wtm G \\ fields (G,Object) = []"(K [ stac fields_rec 1,Auto_tac]); -Addsimps [cmethd_Object, fields_Object]; -val cfield_Object = prove_goalw thy [cfield_def] - "\\X. wf_prog wtm G \\ cfield (G,Object) = empty" (K [Asm_simp_tac 1]); -Addsimps [cfield_Object]; +Addsimps [method_Object, fields_Object]; +val field_Object = prove_goalw thy [field_def] + "\\X. wf_prog wtm G \\ field (G,Object) = empty" (K [Asm_simp_tac 1]); +Addsimps [field_Object]; val subcls_C_Object = prove_goal thy "\\X. \\is_class G C; wf_prog wtm G \\ \\ C \\ Object \\ G\\C\\C Object" (K [ @@ -264,24 +264,24 @@ val widen_fields_mono = result(); -val cfs_fields_lemma = prove_goalw thy [cfield_def] -"\\X. cfield (G,C) fn = Some (fd, fT) \\ map_of(fields (G,C)) (fn, fd) = Some fT" +val cfs_fields_lemma = prove_goalw thy [field_def] +"\\X. field (G,C) fn = Some (fd, fT) \\ map_of(fields (G,C)) (fn, fd) = Some fT" (K [rtac table_map_Some 1, Asm_full_simp_tac 1]); -val widen_cfs_fields = prove_goal thy "\\X. \\cfield (G,C) fn = Some (fd, fT);\ +val widen_cfs_fields = prove_goal thy "\\X. \\field (G,C) fn = Some (fd, fT);\ \ G\\Class C'\\Class C; wf_prog wtm G\\ \\ map_of (fields (G,C')) (fn, fd) = Some fT" (K[ fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]); -Goal "wf_prog wtm G \\ cmethd (G,C) sig = Some (md,mh,m)\ +Goal "wf_prog wtm G \\ method (G,C) sig = Some (md,mh,m)\ \ \\ G\\Class C\\Class md \\ wf_mdecl wtm G md (sig,(mh,m))"; by( case_tac "is_class G C" 1); -by( forw_inst_tac [("C","C")] cmethd_rec 2); +by( forw_inst_tac [("C","C")] method_rec 2); by( asm_full_simp_tac (simpset() addsimps [is_class_def] delsimps [not_None_eq]) 2); by( etac subcls1_induct 1); by( atac 1); by( Force_tac 1); -by( forw_inst_tac [("C","C")] cmethd_rec 1); +by( forw_inst_tac [("C","C")] method_rec 1); by( strip_tac1 1); by( rotate_tac ~1 1); by( Asm_full_simp_tac 1); @@ -300,11 +300,11 @@ by( Asm_full_simp_tac 1); by( rewtac wf_cdecl_def); by( Asm_full_simp_tac 1); -val cmethd_wf_mdecl = result() RS mp; +val method_wf_mdecl = result() RS mp; Goal "\\G\\T\\C T'; wf_prog wt G\\ \\ \ -\ \\D rT b. cmethd (G,T') sig = Some (D,rT ,b) \\\ -\ (\\D' rT' b'. cmethd (G,T) sig = Some (D',rT',b') \\ G\\rT'\\rT)"; +\ \\D rT b. method (G,T') sig = Some (D,rT ,b) \\\ +\ (\\D' rT' b'. method (G,T) sig = Some (D',rT',b') \\ G\\rT'\\rT)"; by( etac trancl_trans_induct 1); by( strip_tac1 2); by( EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]); @@ -312,7 +312,7 @@ by( strip_tac1 1); by( dtac subcls1D 1); by( strip_tac1 1); -by( stac cmethd_rec 1); +by( stac method_rec 1); by( atac 1); by( rewtac override_def); by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1); @@ -334,33 +334,33 @@ Goal "\\ G\\Class C\\Class D; wf_prog wt G; \ -\ cmethd (G,D) sig = Some (md, rT, b) \\ \ -\ \\ \\mD' rT' b'. cmethd (G,C) sig= Some(mD',rT',b') \\ G\\rT'\\rT"; +\ method (G,D) sig = Some (md, rT, b) \\ \ +\ \\ \\mD' rT' b'. method (G,C) sig= Some(mD',rT',b') \\ G\\rT'\\rT"; by(auto_tac (claset() addSDs [widen_Class_Class] - addDs [subcls_widen_methd,cmethd_wf_mdecl], + addDs [subcls_widen_methd,method_wf_mdecl], simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def])); qed "subtype_widen_methd"; -Goal "wf_prog wt G \\ \\D. cmethd (G,C) sig = Some(D,mh,code) \\ is_class G D \\ cmethd (G,D) sig = Some(D,mh,code)"; +Goal "wf_prog wt G \\ \\D. method (G,C) sig = Some(D,mh,code) \\ is_class G D \\ method (G,D) sig = Some(D,mh,code)"; by( case_tac "is_class G C" 1); -by( forw_inst_tac [("C","C")] cmethd_rec 2); +by( forw_inst_tac [("C","C")] method_rec 2); by( asm_full_simp_tac (simpset() addsimps [is_class_def] delsimps [not_None_eq]) 2); by (etac subcls1_induct 1); ba 1; by (Asm_full_simp_tac 1); -by (stac cmethd_rec 1); +by (stac method_rec 1); ba 1; by (Clarify_tac 1); by (eres_inst_tac [("x","Da")] allE 1); by (Clarsimp_tac 1); by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1); by (Clarify_tac 1); - by (stac cmethd_rec 1); + by (stac method_rec 1); ba 1; by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1); -qed_spec_mp "cmethd_in_md"; +qed_spec_mp "method_in_md"; writeln"OK"; diff -r 325b8e754523 -r 6fc37b5c5e98 src/HOL/MicroJava/J/WellForm.thy --- a/src/HOL/MicroJava/J/WellForm.thy Thu Nov 25 12:30:57 1999 +0100 +++ b/src/HOL/MicroJava/J/WellForm.thy Fri Nov 26 08:46:59 1999 +0100 @@ -38,7 +38,7 @@ | Some D \\ is_class G D \\ \\ G\\D\\C C \\ (\\(sig,rT,b)\\set ms. \\D' rT' b'. - cmethd(G,D) sig = Some(D',rT',b') \\ G\\rT\\rT'))" + method(G,D) sig = Some(D',rT',b') \\ G\\rT\\rT'))" wf_prog :: "'c wtm \\ 'c prog \\ bool" "wf_prog wtm G \\