1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/MicroJava/BV/BVSpec.ML Thu Nov 11 12:23:45 1999 +0100
1.3 @@ -0,0 +1,31 @@
1.4 +(* Title: HOL/MicroJava/BV/BVSpec.ML
1.5 + ID: $Id$
1.6 + Author: Cornelia Pusch
1.7 + Copyright 1999 Technische Universitaet Muenchen
1.8 +*)
1.9 +
1.10 +Addsimps [wt_MR_def];
1.11 +
1.12 +Goalw [wt_jvm_prog_def] "wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)";
1.13 +by(Blast_tac 1);
1.14 +qed "wt_jvm_progD";
1.15 +
1.16 +
1.17 +Goalw [wt_jvm_prog_def]
1.18 +"\\<lbrakk> wt_jvm_prog G phi; \
1.19 +\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
1.20 +\ pc < length ins \\<rbrakk> \
1.21 +\\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
1.22 +by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1);
1.23 + by (Asm_full_simp_tac 1);
1.24 +by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
1.25 +qed "wt_jvm_prog_impl_wt_instr";
1.26 +
1.27 +Goalw [wt_jvm_prog_def]
1.28 +"\\<lbrakk> wt_jvm_prog G phi; \
1.29 +\ cmethd (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow> \
1.30 +\ 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)";
1.31 +by(forward_tac [rotate_prems 2 cmethd_wf_mdecl] 1);
1.32 + by (Asm_full_simp_tac 1);
1.33 +by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
1.34 +qed "wt_jvm_prog_impl_wt_start";
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/MicroJava/BV/BVSpec.thy Thu Nov 11 12:23:45 1999 +0100
2.3 @@ -0,0 +1,201 @@
2.4 +(* Title: HOL/MicroJava/BV/BVSpec.thy
2.5 + ID: $Id$
2.6 + Author: Cornelia Pusch
2.7 + Copyright 1999 Technische Universitaet Muenchen
2.8 +
2.9 +Specification of bytecode verifier
2.10 +*)
2.11 +
2.12 +BVSpec = Convert +
2.13 +
2.14 +types
2.15 + method_type = "state_type list"
2.16 + class_type = "sig \\<Rightarrow> method_type"
2.17 + prog_type = "cname \\<Rightarrow> class_type"
2.18 +
2.19 +consts
2.20 + wt_LS :: "[load_and_store,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
2.21 +primrec
2.22 +"wt_LS (Load idx) G phi max_pc pc =
2.23 + (let (ST,LT) = phi ! pc
2.24 + in
2.25 + pc+1 < max_pc \\<and>
2.26 + idx < length LT \\<and>
2.27 + (\\<exists>ts. (LT ! idx) = Some ts \\<and>
2.28 + G \\<turnstile> phi ! (pc+1) >>>= (ts # ST , LT)))"
2.29 +
2.30 +"wt_LS (Store idx) G phi max_pc pc =
2.31 + (let (ST,LT) = phi ! pc
2.32 + in
2.33 + pc+1 < max_pc \\<and>
2.34 + idx < length LT \\<and>
2.35 + (\\<exists>ts ST'. ST = ts # ST' \\<and>
2.36 + G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT[idx:=Some ts])))"
2.37 +
2.38 +"wt_LS (Bipush i) G phi max_pc pc =
2.39 + (let (ST,LT) = phi ! pc
2.40 + in
2.41 + pc+1 < max_pc \\<and>
2.42 + G \\<turnstile> phi ! (pc+1) >>>= ((PrimT Integer) # ST , LT))"
2.43 +
2.44 +"wt_LS (Aconst_null) G phi max_pc pc =
2.45 + (let (ST,LT) = phi ! pc
2.46 + in
2.47 + pc+1 < max_pc \\<and>
2.48 + G \\<turnstile> phi ! (pc+1) >>>= (NT # ST , LT))"
2.49 +
2.50 +consts
2.51 + wt_MO :: "[manipulate_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
2.52 +primrec
2.53 +"wt_MO (Getfield F C) G phi max_pc pc =
2.54 + (let (ST,LT) = phi ! pc
2.55 + in
2.56 + pc+1 < max_pc \\<and>
2.57 + is_class G C \\<and>
2.58 + (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
2.59 + ST = oT # ST' \\<and>
2.60 + G \\<turnstile> oT \\<preceq> (Class C) \\<and>
2.61 + G \\<turnstile> phi ! (pc+1) >>>= (T # ST' , LT)))"
2.62 +
2.63 +"wt_MO (Putfield F C) G phi max_pc pc =
2.64 + (let (ST,LT) = phi ! pc
2.65 + in
2.66 + pc+1 < max_pc \\<and>
2.67 + is_class G C \\<and>
2.68 + (\\<exists>T vT oT ST'.
2.69 + cfield (G,C) F = Some(C,T) \\<and>
2.70 + ST = vT # oT # ST' \\<and>
2.71 + G \\<turnstile> oT \\<preceq> (Class C) \\<and>
2.72 + G \\<turnstile> vT \\<preceq> T \\<and>
2.73 + G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT)))"
2.74 +
2.75 +
2.76 +consts
2.77 + wt_CO :: "[create_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
2.78 +primrec
2.79 +"wt_CO (New C) G phi max_pc pc =
2.80 + (let (ST,LT) = phi ! pc
2.81 + in
2.82 + pc+1 < max_pc \\<and>
2.83 + is_class G C \\<and>
2.84 + G \\<turnstile> phi ! (pc+1) >>>= ((Class C) # ST , LT))"
2.85 +
2.86 +consts
2.87 + wt_CH :: "[check_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
2.88 +primrec
2.89 +"wt_CH (Checkcast C) G phi max_pc pc =
2.90 + (let (ST,LT) = phi ! pc
2.91 + in
2.92 + pc+1 < max_pc \\<and>
2.93 + is_class G C \\<and>
2.94 + (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
2.95 + G \\<turnstile> phi ! (pc+1) >>>= (Class C # ST' , LT)))"
2.96 +
2.97 +consts
2.98 + wt_OS :: "[op_stack,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
2.99 +primrec
2.100 +"wt_OS Pop G phi max_pc pc =
2.101 + (let (ST,LT) = phi ! pc
2.102 + in
2.103 + \\<exists>ts ST'. pc+1 < max_pc \\<and>
2.104 + ST = ts # ST' \\<and>
2.105 + G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT))"
2.106 +
2.107 +"wt_OS Dup G phi max_pc pc =
2.108 + (let (ST,LT) = phi ! pc
2.109 + in
2.110 + pc+1 < max_pc \\<and>
2.111 + (\\<exists>ts ST'. ST = ts # ST' \\<and>
2.112 + G \\<turnstile> phi ! (pc+1) >>>= (ts # ts # ST' , LT)))"
2.113 +
2.114 +"wt_OS Dup_x1 G phi max_pc pc =
2.115 + (let (ST,LT) = phi ! pc
2.116 + in
2.117 + pc+1 < max_pc \\<and>
2.118 + (\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and>
2.119 + G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts1 # ST' , LT)))"
2.120 +
2.121 +"wt_OS Dup_x2 G phi max_pc pc =
2.122 + (let (ST,LT) = phi ! pc
2.123 + in
2.124 + pc+1 < max_pc \\<and>
2.125 + (\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and>
2.126 + G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts3 # ts1 # ST' , LT)))"
2.127 +
2.128 +"wt_OS Swap G phi max_pc pc =
2.129 + (let (ST,LT) = phi ! pc
2.130 + in
2.131 + pc+1 < max_pc \\<and>
2.132 + (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
2.133 + G \\<turnstile> phi ! (pc+1) >>>= (ts # ts' # ST' , LT)))"
2.134 +
2.135 +consts
2.136 + wt_BR :: "[branch,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
2.137 +primrec
2.138 +"wt_BR (Ifcmpeq branch) G phi max_pc pc =
2.139 + (let (ST,LT) = phi ! pc
2.140 + in
2.141 + pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and>
2.142 + (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and> ts = ts' \\<and>
2.143 + G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT) \\<and>
2.144 + G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST' , LT)))"
2.145 +"wt_BR (Goto branch) G phi max_pc pc =
2.146 + (let (ST,LT) = phi ! pc
2.147 + in
2.148 + (nat(int pc+branch)) < max_pc \\<and>
2.149 + G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST , LT))"
2.150 +
2.151 +consts
2.152 + wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
2.153 +primrec
2.154 +"wt_MI (Invokevirtual mn fpTs) G phi max_pc pc =
2.155 + (let (ST,LT) = phi ! pc
2.156 + in
2.157 + pc+1 < max_pc \\<and>
2.158 + (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and>
2.159 + length apTs = length fpTs \\<and>
2.160 + (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
2.161 + (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
2.162 + G \\<turnstile> phi ! (pc+1) >>>= (rT # ST' , LT))))"
2.163 +
2.164 +constdefs
2.165 + wt_MR :: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
2.166 +"wt_MR G rT phi pc \\<equiv>
2.167 + (let (ST,LT) = phi ! pc
2.168 + in
2.169 + (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))"
2.170 +
2.171 +
2.172 +constdefs
2.173 + wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool"
2.174 + "wt_instr instr G rT phi max_pc pc \\<equiv>
2.175 + case instr of
2.176 + LS ins \\<Rightarrow> wt_LS ins G phi max_pc pc
2.177 + | CO ins \\<Rightarrow> wt_CO ins G phi max_pc pc
2.178 + | MO ins \\<Rightarrow> wt_MO ins G phi max_pc pc
2.179 + | CH ins \\<Rightarrow> wt_CH ins G phi max_pc pc
2.180 + | MI ins \\<Rightarrow> wt_MI ins G phi max_pc pc
2.181 + | MR \\<Rightarrow> wt_MR G rT phi pc
2.182 + | OS ins \\<Rightarrow> wt_OS ins G phi max_pc pc
2.183 + | BR ins \\<Rightarrow> wt_BR ins G phi max_pc pc"
2.184 +
2.185 +
2.186 +constdefs
2.187 + wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
2.188 + "wt_start G C pTs mxl phi \\<equiv>
2.189 + G \\<turnstile> phi!0 >>>= ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))"
2.190 +
2.191 +
2.192 + wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
2.193 + "wt_method G cn pTs rT mxl ins phi \\<equiv>
2.194 + let max_pc = length ins
2.195 + in
2.196 + 0 < max_pc \\<and> wt_start G cn pTs mxl phi \\<and>
2.197 + (\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
2.198 +
2.199 + wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool"
2.200 +"wt_jvm_prog G phi \\<equiv>
2.201 + wf_prog (\\<lambda>G C (sig,rT,maxl,b).
2.202 + wt_method G C (snd sig) rT maxl b (phi C sig)) G"
2.203 +
2.204 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Thu Nov 11 12:23:45 1999 +0100
3.3 @@ -0,0 +1,625 @@
3.4 +(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.ML
3.5 + ID: $Id$
3.6 + Author: Cornelia Pusch
3.7 + Copyright 1999 Technische Universitaet Muenchen
3.8 +*)
3.9 +
3.10 +val defs1 = exec.rules@[split_def,sup_state_def,correct_state_def,
3.11 + correct_frame_def,wt_instr_def];
3.12 +
3.13 +Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
3.14 +"\\<lbrakk> wt_jvm_prog G phi; \
3.15 +\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
3.16 +\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
3.17 +\\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
3.18 +by (Asm_full_simp_tac 1);
3.19 +by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1);
3.20 +qed "wt_jvm_prog_impl_wt_instr_cor";
3.21 +
3.22 +
3.23 +Delsimps [split_paired_All];
3.24 +
3.25 +
3.26 +(******* LS *******)
3.27 +
3.28 +Goal
3.29 +"\\<lbrakk> wf_prog wt G; \
3.30 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.31 +\ ins!pc = LS(Load idx); \
3.32 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.33 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.34 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.35 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.36 +by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
3.37 + approx_loc_imp_approx_loc_sup]
3.38 + addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.39 +qed "Load_correct";
3.40 +
3.41 +
3.42 +Goal
3.43 +"\\<lbrakk> wf_prog wt G; \
3.44 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.45 +\ ins!pc = LS(Store idx); \
3.46 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.47 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.48 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.49 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.50 +by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.51 + addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)]
3.52 + addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.53 +qed "Store_correct";
3.54 +
3.55 +Goalw [conf_def] "G,h \\<turnstile> Intg i \\<Colon>\\<preceq> PrimT Integer";
3.56 +by(Simp_tac 1);
3.57 +qed "conf_Intg_Integer";
3.58 +AddIffs [conf_Intg_Integer];
3.59 +
3.60 +Goal
3.61 +"\\<lbrakk> wf_prog wt G; \
3.62 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.63 +\ ins!pc = LS(Bipush i); \
3.64 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.65 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.66 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.67 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.68 +by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
3.69 + addss (simpset() addsimps [approx_val_def,sup_PTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
3.70 +qed "Bipush_correct";
3.71 +
3.72 +Goal "G \\<turnstile> T' \\<preceq> T \\<Longrightarrow> T' = NT \\<longrightarrow> (T=NT | (\\<exists>C. T = Class C))";
3.73 +be widen.induct 1;
3.74 +by(Auto_tac);
3.75 +by(rename_tac "R" 1);
3.76 +by(exhaust_tac "R" 1);
3.77 +by(Auto_tac);
3.78 +val lemma = result();
3.79 +
3.80 +Goal "G \\<turnstile> NT \\<preceq> T = (T=NT | (\\<exists>C. T = Class C))";
3.81 +by(force_tac (claset() addIs widen.intrs addDs [lemma],simpset()) 1);
3.82 +qed "NT_subtype_conv";
3.83 +
3.84 +Goal
3.85 +"\\<lbrakk> wf_prog wt G; \
3.86 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.87 +\ ins!pc = LS Aconst_null; \
3.88 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.89 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.90 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.91 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.92 +by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
3.93 + addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
3.94 +qed "Aconst_null_correct";
3.95 +
3.96 +
3.97 +Goal
3.98 +"\\<lbrakk> wt_jvm_prog G phi; \
3.99 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.100 +\ ins!pc = LS ls_com; \
3.101 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.102 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.103 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.104 +by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.105 + ba 1;
3.106 + ba 1;
3.107 +by(rewtac wt_jvm_prog_def);
3.108 +by (exhaust_tac "ls_com" 1);
3.109 +by (ALLGOALS (fast_tac (claset() addIs [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct])));
3.110 +qed "LS_correct";
3.111 +
3.112 +
3.113 +(**** CH ****)
3.114 +
3.115 +Goalw [cast_ok_def]
3.116 + "\\<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> \
3.117 +\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
3.118 +be disjE 1;
3.119 + by (Clarify_tac 1);
3.120 +by (forward_tac [widen_Class] 1);
3.121 +by (Clarify_tac 1);
3.122 +be disjE 1;
3.123 + by (asm_full_simp_tac (simpset() addsimps [widen.null]) 1);
3.124 +by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
3.125 +by (Clarify_tac 1);
3.126 +by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1);
3.127 +by (exhaust_tac "v" 1);
3.128 +by (ALLGOALS (fast_tac (claset() addIs [widen_trans] addss (simpset() addsimps [widen.null]))));
3.129 +qed "Cast_conf2";
3.130 +
3.131 +Goal
3.132 +"\\<lbrakk> wf_prog wt G; \
3.133 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.134 +\ ins!pc = CH (Checkcast D); \
3.135 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.136 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.137 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.138 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.139 +by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,
3.140 + xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.141 +by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.142 + addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2]
3.143 + addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,approx_val_def])) 1);
3.144 +qed "Checkcast_correct";
3.145 +
3.146 +
3.147 +Goal
3.148 +"\\<lbrakk> wt_jvm_prog G phi; \
3.149 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.150 +\ ins!pc = CH ch_com; \
3.151 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.152 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.153 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.154 +by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.155 + ba 1;
3.156 + ba 1;
3.157 +by(rewtac wt_jvm_prog_def);
3.158 +by (exhaust_tac "ch_com" 1);
3.159 +by (ALLGOALS (fast_tac (claset() addIs [Checkcast_correct])));
3.160 +qed "CH_correct";
3.161 +
3.162 +
3.163 +(******* MO *******)
3.164 +Goal
3.165 +"\\<lbrakk> wf_prog wt G; \
3.166 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.167 +\ ins!pc = MO (Getfield F D); \
3.168 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.169 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.170 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.171 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.172 +by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.173 +by (Clarify_tac 1);
3.174 +by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
3.175 +by (Clarify_tac 1);
3.176 +bd approx_stk_Cons_lemma 1;
3.177 +by (Clarify_tac 1);
3.178 +by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
3.179 +
3.180 +by (forward_tac [conf_widen] 1);
3.181 + ba 1;
3.182 + ba 1;
3.183 +bd conf_RefTD 1;
3.184 +by (Clarify_tac 1);
3.185 +by (asm_full_simp_tac (simpset() addsimps []) 1);
3.186 +
3.187 +(* approx_stk *)
3.188 +br conjI 1;
3.189 +by (asm_full_simp_tac (simpset() addsimps [approx_stk_Cons]) 1);
3.190 +br conjI 1;
3.191 +by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup]) 1);
3.192 +by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
3.193 +bd widen_cfs_fields 1;
3.194 + ba 1;
3.195 + ba 1;
3.196 +by (fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1);
3.197 +
3.198 +(* approx_loc *)
3.199 +by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
3.200 +qed "Getfield_correct";
3.201 +
3.202 +
3.203 +Goal
3.204 +"\\<lbrakk> wf_prog wt G; \
3.205 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.206 +\ ins!pc = MO (Putfield F D); \
3.207 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.208 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.209 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.210 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.211 +by (asm_full_simp_tac (simpset() addsimps [xcpt_update_def,raise_xcpt_def]@defs1 addsplits [option.split]) 1);
3.212 +by (Clarify_tac 1);
3.213 +by (asm_full_simp_tac (simpset() addsimps [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
3.214 +by (Clarify_tac 1);
3.215 +bd approx_stk_Cons_lemma 1;
3.216 +by (Clarify_tac 1);
3.217 +bd approx_stk_Cons_lemma 1;
3.218 +by (Clarify_tac 1);
3.219 +by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
3.220 +
3.221 +by (forward_tac [conf_widen] 1);
3.222 + ba 2;
3.223 + ba 1;
3.224 +by (fast_tac (claset() addDs [conf_RefTD,widen_cfs_fields]
3.225 + addIs [sup_heap_update_value,approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
3.226 + approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
3.227 + hconf_imp_hconf_field_update,
3.228 + correct_frames_imp_correct_frames_field_update,conf_widen] addss (simpset())) 1);
3.229 +qed "Putfield_correct";
3.230 +
3.231 +
3.232 +Goal
3.233 +"\\<lbrakk> wt_jvm_prog G phi; \
3.234 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.235 +\ ins!pc = MO mo_com; \
3.236 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.237 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.238 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.239 +by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.240 + ba 1;
3.241 + ba 1;
3.242 +by(rewtac wt_jvm_prog_def);
3.243 +by (exhaust_tac "mo_com" 1);
3.244 +by (ALLGOALS (fast_tac (claset() addIs [Getfield_correct,Putfield_correct])));
3.245 +qed "MO_correct";
3.246 +
3.247 +
3.248 +(****** CO ******)
3.249 +
3.250 +Goal "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)";
3.251 +by(Fast_tac 1);
3.252 +qed "collapse_paired_All";
3.253 +
3.254 +Goal
3.255 +"\\<lbrakk> wf_prog wt G; \
3.256 +\ cmethd (G,C) sig = Some (C,rT,maxl,ins); \
3.257 +\ ins!pc = CO(New cl_idx); \
3.258 +\ wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
3.259 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
3.260 +\ correct_state G phi (None, hp, (stk,loc,C,sig,pc)#frs) \\<rbrakk> \
3.261 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.262 +by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,
3.263 + approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
3.264 + approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
3.265 + hconf_imp_hconf_newref,correct_frames_imp_correct_frames_newref,
3.266 + rewrite_rule [split_def] correct_init_obj]
3.267 + addss (simpset() addsimps [NT_subtype_conv,approx_stk_Cons,approx_val_def,conf_def,
3.268 + fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,xcpt_update_def,raise_xcpt_def,init_vars_def]@defs1
3.269 + addsplits [option.split])) 1);
3.270 +qed "New_correct";
3.271 +
3.272 +Goal
3.273 +"\\<lbrakk> wt_jvm_prog G phi; \
3.274 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.275 +\ ins!pc = CO co_com; \
3.276 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.277 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.278 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.279 +by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.280 + ba 1;
3.281 + ba 1;
3.282 +by(rewtac wt_jvm_prog_def);
3.283 +by (exhaust_tac "co_com" 1);
3.284 +by (ALLGOALS (fast_tac (claset() addIs [New_correct])));
3.285 +qed "CO_correct";
3.286 +
3.287 +
3.288 +(****** MI ******)
3.289 +
3.290 +Goal
3.291 +"\\<lbrakk> wt_jvm_prog G phi; \
3.292 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.293 +\ ins ! pc = MI(Invokevirtual mn pTs); \
3.294 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.295 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.296 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.297 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.298 +by(forward_tac [wt_jvm_progD] 1);
3.299 +by(etac exE 1);
3.300 +by (asm_full_simp_tac (simpset()addsimps[xcpt_update_def,raise_xcpt_def]@defs1
3.301 + addsplits [option.split]) 1);
3.302 +by (Clarify_tac 1);
3.303 +by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
3.304 +bd approx_stk_append_lemma 1;
3.305 +by (Clarify_tac 1);
3.306 +bd approx_stk_Cons_lemma 1;
3.307 +by (asm_full_simp_tac (simpset() addsimps []) 1);
3.308 +by (Clarify_tac 1);
3.309 +by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
3.310 +bd conf_RefTD 1;
3.311 +by (Clarify_tac 1);
3.312 +by(rename_tac "oloc oT ofs T'" 1);
3.313 +by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
3.314 +bd subtype_widen_methd 1;
3.315 + ba 1;
3.316 + ba 1;
3.317 +be exE 1;
3.318 +by(rename_tac "oT'" 1);
3.319 +by (Clarify_tac 1);
3.320 +by(subgoal_tac "G \\<turnstile> Class oT \\<preceq> Class oT'" 1);
3.321 + by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 cmethd_wf_mdecl)) 2);
3.322 + ba 2;
3.323 + by(Blast_tac 2);
3.324 +by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
3.325 +by(forward_tac [cmethd_in_md] 1);
3.326 + ba 1;
3.327 + back();
3.328 + back();
3.329 +by (Clarify_tac 1);
3.330 +by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
3.331 +by (forward_tac [wt_jvm_prog_impl_wt_start] 1);
3.332 + ba 1;
3.333 + back();
3.334 +by (asm_full_simp_tac (simpset() addsimps [wt_start_def,sup_state_def]) 1);
3.335 +by (Clarify_tac 1);
3.336 +
3.337 +(** approx_stk **)
3.338 +br conjI 1;
3.339 + by (asm_full_simp_tac (simpset() addsimps [sup_loc_Nil,approx_stk_Nil]) 1);
3.340 +
3.341 +
3.342 +(** approx_loc **)
3.343 +br conjI 1;
3.344 + br approx_loc_imp_approx_loc_sup 1;
3.345 + ba 1;
3.346 + by (Fast_tac 2);
3.347 + by (asm_full_simp_tac (simpset() addsimps [split_def,approx_loc_Cons,approx_val_def,approx_loc_append]) 1);
3.348 + br conjI 1;
3.349 + br conf_widen 1;
3.350 + ba 1;
3.351 + by (Fast_tac 2);
3.352 + by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
3.353 + br conjI 1;
3.354 + by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)]
3.355 + addss (simpset() addsimps [split_def,approx_loc_Cons,approx_val_def])) 1);
3.356 + by (asm_simp_tac (simpset() addsimps [split_def,approx_loc_def,zip_replicate,approx_val_None,set_replicate_conv_if]) 1);
3.357 +
3.358 +br conjI 1;
3.359 + by (asm_simp_tac (simpset() addsimps [min_def]) 1);
3.360 +br exI 1;
3.361 +br exI 1;
3.362 +br conjI 1;
3.363 + by(Blast_tac 1);
3.364 +by (fast_tac (claset()
3.365 + addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
3.366 + addss (simpset()addsimps [map_eq_Cons,sup_loc_Cons])) 1);
3.367 +qed "Invokevirtual_correct";
3.368 +
3.369 +Goal
3.370 +"\\<lbrakk> wt_jvm_prog G phi; \
3.371 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.372 +\ ins!pc = MI mi_com; \
3.373 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.374 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.375 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.376 +by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.377 + ba 1;
3.378 + ba 1;
3.379 +by (exhaust_tac "mi_com" 1);
3.380 +by (ALLGOALS (fast_tac (claset() addIs [Invokevirtual_correct])));
3.381 +qed "MI_correct";
3.382 +
3.383 +(****** MR ******)
3.384 +
3.385 +Goal
3.386 + "\\<forall>zs. (xs@ys = zs) = (xs = take (length xs) zs \\<and> ys = drop (length xs) zs)";
3.387 +by(induct_tac "xs" 1);
3.388 +by(Simp_tac 1);
3.389 +by(Asm_full_simp_tac 1);
3.390 +by(Clarify_tac 1);
3.391 +by(exhaust_tac "zs" 1);
3.392 +by(Auto_tac);
3.393 +qed_spec_mp "append_eq_conv_conj";
3.394 +
3.395 +
3.396 +
3.397 +Delsimps [map_append];
3.398 +Goal
3.399 +"\\<lbrakk> wt_jvm_prog G phi; \
3.400 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.401 +\ ins ! pc = MR; \
3.402 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.403 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.404 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.405 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.406 +by (asm_full_simp_tac (simpset() addsimps defs1) 1);
3.407 +by (Clarify_tac 1);
3.408 +by (asm_full_simp_tac (simpset() addsimps defs1) 1);
3.409 +by (exhaust_tac "frs" 1);
3.410 + by (asm_full_simp_tac (simpset() addsimps defs1) 1);
3.411 +by (Clarify_tac 1);
3.412 +by (asm_full_simp_tac (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1) 1);
3.413 +by (Clarify_tac 1);
3.414 +by (asm_full_simp_tac (simpset() addsimps defs1) 1);
3.415 +by (forward_tac [wt_jvm_prog_impl_wt_instr] 1);
3.416 + by(EVERY1[atac, etac Suc_lessD]);
3.417 +by(rewtac wt_jvm_prog_def);
3.418 +by (fast_tac (claset()
3.419 + addDs [approx_stk_Cons_lemma,subcls_widen_methd]
3.420 + addEs [rotate_prems 1 widen_trans]
3.421 + addIs [conf_widen]
3.422 + addss (simpset()
3.423 + addsimps [approx_val_def,append_eq_conv_conj,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
3.424 +qed "Return_correct";
3.425 +Addsimps [map_append];
3.426 +
3.427 +Goal
3.428 +"\\<lbrakk> wt_jvm_prog G phi; \
3.429 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.430 +\ ins!pc = MR; \
3.431 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.432 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.433 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.434 +by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.435 + ba 1;
3.436 + ba 1;
3.437 +by (ALLGOALS (fast_tac (claset() addIs [Return_correct])));
3.438 +qed "MR_correct";
3.439 +
3.440 +(****** BR ******)
3.441 +Goal
3.442 +"\\<lbrakk> wf_prog wt G; \
3.443 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.444 +\ ins ! pc = BR(Goto branch); \
3.445 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.446 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.447 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.448 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.449 +by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]
3.450 + addss (simpset() addsimps defs1)) 1);
3.451 +qed "Goto_correct";
3.452 +
3.453 +
3.454 +Goal
3.455 +"\\<lbrakk> wf_prog wt G; \
3.456 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.457 +\ ins!pc = BR(Ifcmpeq branch); \
3.458 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.459 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.460 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.461 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.462 +by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.463 + addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
3.464 +qed "Ifiacmpeq_correct";
3.465 +
3.466 +
3.467 +Goal
3.468 +"\\<lbrakk> wt_jvm_prog G phi; \
3.469 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.470 +\ ins!pc = BR br_com; \
3.471 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.472 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.473 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.474 +by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.475 + ba 1;
3.476 + ba 1;
3.477 +by(rewtac wt_jvm_prog_def);
3.478 +by (exhaust_tac "br_com" 1);
3.479 +by (ALLGOALS (fast_tac (claset() addIs [Goto_correct,Ifiacmpeq_correct])));
3.480 +qed "BR_correct";
3.481 +
3.482 +
3.483 +(****** OS ******)
3.484 +
3.485 +Goal
3.486 +"\\<lbrakk> wf_prog wt G; \
3.487 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.488 +\ ins ! pc = OS Pop; \
3.489 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.490 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.491 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.492 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.493 +by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.494 + addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
3.495 +qed "Pop_correct";
3.496 +
3.497 +
3.498 +Goal
3.499 +"\\<lbrakk> wf_prog wt G; \
3.500 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.501 +\ ins ! pc = OS Dup; \
3.502 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.503 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.504 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.505 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.506 +by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.507 + addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
3.508 + addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.509 +qed "Dup_correct";
3.510 +
3.511 +
3.512 +Goal
3.513 +"\\<lbrakk> wf_prog wt G; \
3.514 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.515 +\ ins ! pc = OS Dup_x1; \
3.516 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.517 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.518 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.519 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.520 +by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.521 + addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
3.522 + addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.523 +qed "Dup_x1_correct";
3.524 +
3.525 +Goal
3.526 +"\\<lbrakk> wf_prog wt G; \
3.527 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.528 +\ ins ! pc = OS Dup_x2; \
3.529 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.530 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.531 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.532 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.533 +by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.534 + addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
3.535 + addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.536 +qed "Dup_x2_correct";
3.537 +
3.538 +Goal
3.539 +"\\<lbrakk> wf_prog wt G; \
3.540 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.541 +\ ins ! pc = OS Swap; \
3.542 +\ wt_instr (ins!pc) G rT (phi C ml) (length ins) pc; \
3.543 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs); \
3.544 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.545 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.546 +by (fast_tac (claset() addDs [approx_stk_Cons_lemma]
3.547 + addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
3.548 + addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
3.549 +qed "Swap_correct";
3.550 +
3.551 +Goal
3.552 +"\\<lbrakk> wt_jvm_prog G phi; \
3.553 +\ cmethd (G,C) ml = Some (C,rT,maxl,ins); \
3.554 +\ ins!pc = OS os_com; \
3.555 +\ Some (xp',hp',frs') = exec (G, None, hp, (stk,loc,C,ml,pc)#frs) ; \
3.556 +\ correct_state G phi (None, hp, (stk,loc,C,ml,pc)#frs) \\<rbrakk> \
3.557 +\\\<Longrightarrow> correct_state G phi (xp',hp',frs')";
3.558 +by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
3.559 + ba 1;
3.560 + ba 1;
3.561 +by(rewtac wt_jvm_prog_def);
3.562 +by (exhaust_tac "os_com" 1);
3.563 +by (ALLGOALS (fast_tac (claset() addIs [Pop_correct,Dup_correct,Dup_x1_correct,Dup_x2_correct,Swap_correct])));
3.564 +qed "OS_correct";
3.565 +
3.566 +(** Main **)
3.567 +
3.568 +Goalw [correct_state_def,Let_def]
3.569 + "correct_state G phi (None,hp,(stk,loc,C,sig,pc)#fs) \
3.570 +\ \\<Longrightarrow> \\<exists>meth. cmethd (G,C) sig = Some(C,meth)";
3.571 +by(Asm_full_simp_tac 1);
3.572 +by(Blast_tac 1);
3.573 +qed "correct_state_impl_Some_cmethd";
3.574 +
3.575 +Goal
3.576 +"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; correct_state G phi state\\<rbrakk> \
3.577 +\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> correct_state G phi state'";
3.578 +by(split_all_tac 1);
3.579 +by(rename_tac "xp hp frs" 1);
3.580 +by (exhaust_tac "xp" 1);
3.581 + by (exhaust_tac "frs" 1);
3.582 + by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
3.583 + by(split_all_tac 1);
3.584 + by(hyp_subst_tac 1);
3.585 + by(forward_tac [correct_state_impl_Some_cmethd] 1);
3.586 + by (force_tac (claset() addIs [LS_correct,CO_correct,MO_correct,CH_correct,MI_correct,MR_correct,OS_correct,
3.587 + BR_correct], simpset() addsplits [instr.split,instr.split_asm] addsimps exec.rules@[split_def]) 1);
3.588 +by (exhaust_tac "frs" 1);
3.589 + by (asm_full_simp_tac (simpset() addsimps exec.rules) 1);
3.590 +by (force_tac (claset(), simpset() addsimps exec.rules@[correct_state_def]) 1);
3.591 +qed_spec_mp "BV_correct_1";
3.592 +
3.593 +
3.594 +(*******)
3.595 +Goal
3.596 +"xp=None \\<longrightarrow> frs\\<noteq>[] \\<longrightarrow> (\\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs'))";
3.597 +by (fast_tac (claset() addIs [BV_correct_1]
3.598 + addss (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1)) 1);
3.599 +qed_spec_mp "exec_lemma";
3.600 +
3.601 +Goal
3.602 +"\\<lbrakk> wt_jvm_prog G phi; \
3.603 +\ correct_state G phi (xp,hp,frs); xp=None; frs\\<noteq>[] \\<rbrakk> \
3.604 +\ \\<Longrightarrow> \\<exists>xp' hp' frs'. exec (G,xp,hp,frs) = Some (xp',hp',frs') \\<and> correct_state G phi (xp',hp',frs')";
3.605 +by (dres_inst_tac [("G","G"),("hp","hp")] exec_lemma 1);
3.606 +ba 1;
3.607 +by (fast_tac (claset() addIs [BV_correct_1]) 1);
3.608 +qed "L1";
3.609 +(*******)
3.610 +
3.611 +Goalw [exec_all_def]
3.612 +"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \
3.613 +\ \\<Longrightarrow> correct_state G phi s \\<longrightarrow> correct_state G phi t";
3.614 +be rtrancl_induct 1;
3.615 + by (Simp_tac 1);
3.616 +by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1);
3.617 +qed_spec_mp "BV_correct";
3.618 +
3.619 +
3.620 +Goal
3.621 +"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,cn,ml,pc)#frs); correct_state G phi s0 \\<rbrakk> \
3.622 +\ \\<Longrightarrow> approx_stk G hp stk (fst (((phi cn) ml) ! pc)) \\<and> approx_loc G hp loc (snd (((phi cn) ml) ! pc)) ";
3.623 +bd BV_correct 1;
3.624 +ba 1;
3.625 +ba 1;
3.626 +by (asm_full_simp_tac (simpset() addsimps [correct_state_def,correct_frame_def,split_def]
3.627 + addsplits [option.split_asm]) 1);
3.628 +qed_spec_mp "BV_correct_initial";
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Nov 11 12:23:45 1999 +0100
4.3 @@ -0,0 +1,10 @@
4.4 +(* Title: HOL/MicroJava/BV/BVSpecTypeSafe.thy
4.5 + ID: $Id$
4.6 + Author: Cornelia Pusch
4.7 + Copyright 1999 Technische Universitaet Muenchen
4.8 +
4.9 +Proof that the specification of the bytecode verifier only admits type safe
4.10 +programs.
4.11 +*)
4.12 +
4.13 +BVSpecTypeSafe = Correct
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/MicroJava/BV/Convert.ML Thu Nov 11 12:23:45 1999 +0100
5.3 @@ -0,0 +1,41 @@
5.4 +(* Title: HOL/MicroJava/BV/Convert.ML
5.5 + ID: $Id$
5.6 + Author: Cornelia Pusch
5.7 + Copyright 1999 Technische Universitaet Muenchen
5.8 +*)
5.9 +
5.10 +val widen_PrimT_conv1 =
5.11 + prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)"
5.12 + [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"];
5.13 +Addsimps [widen_PrimT_conv1];
5.14 +
5.15 +Goalw [sup_ty_opt_def] "(G \\<turnstile> any >= None) = (any = None)";
5.16 +by(simp_tac (simpset() addsplits [option.split]) 1);
5.17 +qed "anyConvNone";
5.18 +Addsimps [anyConvNone];
5.19 +
5.20 +Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty >= Some ty') = (G \\<turnstile> ty' \\<preceq> ty)";
5.21 +by(Simp_tac 1);
5.22 +qed "SomeanyConvSome";
5.23 +Addsimps [SomeanyConvSome];
5.24 +
5.25 +Goal
5.26 +"(G \\<turnstile> X >= Some(PrimT Integer)) = (X=None \\<or> (X=Some(PrimT Integer)))";
5.27 +by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1);
5.28 +qed "sup_PTS_eq";
5.29 +
5.30 +
5.31 +
5.32 +Goal
5.33 +"CFS \\<turnstile> XT >>= [] = (XT=[])";
5.34 +by (case_tac "XT=[]" 1);
5.35 +by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
5.36 +by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
5.37 +qed "sup_loc_Nil";
5.38 +
5.39 +Goal
5.40 +"CFS \\<turnstile> XT >>= (Y#YT) = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> X>=Y \\<and> CFS \\<turnstile> XT'>>=YT)";
5.41 +by (case_tac "XT=[]" 1);
5.42 +by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
5.43 +by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
5.44 +qed "sup_loc_Cons";
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/MicroJava/BV/Convert.thy Thu Nov 11 12:23:45 1999 +0100
6.3 @@ -0,0 +1,33 @@
6.4 +(* Title: HOL/MicroJava/BV/Convert.thy
6.5 + ID: $Id$
6.6 + Author: Cornelia Pusch
6.7 + Copyright 1999 Technische Universitaet Muenchen
6.8 +
6.9 +The supertype relation lifted to type options, type lists and state types.
6.10 +*)
6.11 +
6.12 +Convert = JVMExec +
6.13 +
6.14 +types
6.15 + locvars_type = ty option list
6.16 + opstack_type = ty list
6.17 + state_type = "opstack_type \\<times> locvars_type"
6.18 +
6.19 +constdefs
6.20 +
6.21 + sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ >= _")
6.22 + "G \\<turnstile> a >= a' \\<equiv>
6.23 + case a of
6.24 + None \\<Rightarrow> True
6.25 + | Some t \\<Rightarrow> case a' of
6.26 + None \\<Rightarrow> False
6.27 + | Some t' \\<Rightarrow> G \\<turnstile> t' \\<preceq> t"
6.28 +
6.29 + sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ >>= _" [71,71] 70)
6.30 + "G \\<turnstile> LT >>= LT' \\<equiv> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t >= t')"
6.31 +
6.32 +
6.33 + sup_state :: "['code prog,state_type,state_type] \\<Rightarrow> bool" ("_ \\<turnstile> _ >>>= _" [71,71] 70)
6.34 + "G \\<turnstile> s >>>= s' \\<equiv> G \\<turnstile> map Some (fst s) >>= map Some (fst s') \\<and> G \\<turnstile> snd s >>= snd s'"
6.35 +
6.36 +end
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/MicroJava/BV/Correct.ML Thu Nov 11 12:23:45 1999 +0100
7.3 @@ -0,0 +1,281 @@
7.4 +(* Title: HOL/MicroJava/BV/Correct.ML
7.5 + ID: $Id$
7.6 + Author: Cornelia Pusch
7.7 + Copyright 1999 Technische Universitaet Muenchen
7.8 +*)
7.9 +
7.10 +(** sup_heap **)
7.11 +
7.12 +Goalw [hext_def]
7.13 + "hp x = None \\<longrightarrow> hp \\<le>| (hp((newref hp) \\<mapsto> obj))";
7.14 +by (asm_full_simp_tac (simpset() addsimps []) 1);
7.15 +by (Clarify_tac 1);
7.16 +bd newref_None 1;
7.17 +back();
7.18 +by (asm_full_simp_tac (simpset() addsimps []) 1);
7.19 +qed_spec_mp "sup_heap_newref";
7.20 +
7.21 +
7.22 +Goalw [hext_def]
7.23 +"hp a = Some (cn,od') \\<longrightarrow> hp \\<le>| (hp(a \\<mapsto> (cn,od)))";
7.24 +by (asm_full_simp_tac (simpset() addsimps []) 1);
7.25 +qed_spec_mp "sup_heap_update_value";
7.26 +
7.27 +
7.28 +(** approx_val **)
7.29 +
7.30 +Goalw [approx_val_def]
7.31 +"approx_val G hp x None";
7.32 +by (Asm_full_simp_tac 1);
7.33 +qed_spec_mp "approx_val_None";
7.34 +
7.35 +
7.36 +Goalw [approx_val_def]
7.37 +"approx_val G hp Null (Some(RefT x))";
7.38 +by(Simp_tac 1);
7.39 +by (fast_tac (claset() addIs widen.intrs) 1);
7.40 +qed_spec_mp "approx_val_Null";
7.41 +
7.42 +
7.43 +Goal
7.44 +"\\<lbrakk> wf_prog wt G \\<rbrakk> \
7.45 +\\\<Longrightarrow> approx_val G hp v (Some T) \\<longrightarrow> G\\<turnstile> T\\<preceq>T' \\<longrightarrow> approx_val G hp v (Some T')";
7.46 +by (exhaust_tac "T" 1);
7.47 + by (Asm_simp_tac 1);
7.48 +by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
7.49 +qed_spec_mp "approx_val_imp_approx_val_assConvertible";
7.50 +
7.51 +
7.52 +Goal
7.53 +"approx_val G hp val at \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_val G hp' val at";
7.54 +by (asm_full_simp_tac (simpset() setloop (split_tac [option.split])
7.55 + addsimps [approx_val_def]) 1);
7.56 +by(blast_tac (claset() addIs [conf_hext]) 1);
7.57 +qed_spec_mp "approx_val_imp_approx_val_sup_heap";
7.58 +
7.59 +Goal
7.60 +"\\<lbrakk> hp a = Some obj' ; G,hp\\<turnstile> v\\<Colon>\\<preceq>T ; obj_ty obj = obj_ty obj' \\<rbrakk> \
7.61 +\\\<Longrightarrow>G,(hp(a\\<mapsto>obj))\\<turnstile> v\\<Colon>\\<preceq>T";
7.62 +by (exhaust_tac "v" 1);
7.63 +by (auto_tac (claset() , simpset() addsimps [obj_ty_def,conf_def] addsplits [option.split]));
7.64 +qed_spec_mp "approx_val_imp_approx_val_heap_update";
7.65 +
7.66 +
7.67 +Goal
7.68 +"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us' >= us \\<longrightarrow> approx_val G h val us'";
7.69 +by (asm_simp_tac (simpset() addsimps [sup_PTS_eq,approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
7.70 +by(blast_tac (claset() addIs [conf_widen]) 1);
7.71 +qed_spec_mp "approx_val_imp_approx_val_sup";
7.72 +
7.73 +
7.74 +Goal
7.75 +"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> at >= LT ! idx \\<rbrakk> \
7.76 +\\\<Longrightarrow> approx_val G hp val at";
7.77 +by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset() addsimps
7.78 + [split_def,approx_loc_def,all_set_conv_all_nth])) 1);
7.79 +qed "approx_loc_imp_approx_val_sup";
7.80 +
7.81 +
7.82 +(** approx_loc **)
7.83 +
7.84 +Goal
7.85 +"approx_loc G hp (s#xs) (l#ls) = \
7.86 +\ ((length xs = length ls) \\<and> (approx_val G hp s l) \\<and> (approx_loc G hp xs ls))";
7.87 +by (fast_tac (claset() addss (simpset() addsimps [approx_loc_def])) 1);
7.88 +qed "approx_loc_Cons";
7.89 +
7.90 +
7.91 +Goalw [approx_stk_def,approx_loc_def]
7.92 +"\\<lbrakk> wf_prog wt G \\<rbrakk> \
7.93 +\\\<Longrightarrow> (\\<forall>tt'\\<in>set (zip tys_n ts). tt' \\<in> widen G) \\<longrightarrow> \
7.94 +\ length tys_n = length ts \\<longrightarrow> approx_stk G hp s tys_n \\<longrightarrow> approx_loc G hp s (map Some ts)";
7.95 +by (force_tac (claset() addIs [approx_val_imp_approx_val_assConvertible], simpset()
7.96 + addsimps [all_set_conv_all_nth,split_def]) 1);
7.97 +qed_spec_mp "assConv_approx_stk_imp_approx_loc";
7.98 +
7.99 +
7.100 +Goalw [approx_loc_def]
7.101 +"\\<forall> lvars. approx_loc G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_loc G hp' lvars lt";
7.102 +by (exhaust_tac "lt" 1);
7.103 + by (Asm_simp_tac 1);
7.104 +by (force_tac (claset() addIs [approx_val_imp_approx_val_sup_heap],
7.105 + simpset() addsimps [neq_Nil_conv]) 1);
7.106 +qed_spec_mp "approx_loc_imp_approx_loc_sup_heap";
7.107 +
7.108 +
7.109 +Goalw [sup_loc_def,approx_loc_def]
7.110 +"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt' >>= lt \\<longrightarrow> approx_loc G hp lvars lt'";
7.111 +by (auto_tac (claset() , simpset() addsimps [all_set_conv_all_nth,split_def]));
7.112 +by (auto_tac (claset() addEs [approx_val_imp_approx_val_sup] , simpset()));
7.113 +qed_spec_mp "approx_loc_imp_approx_loc_sup";
7.114 +
7.115 +
7.116 +Goalw [approx_loc_def]
7.117 +"\\<forall>loc idx x X. (approx_loc G hp loc LT) \\<longrightarrow> (approx_val G hp x X) \
7.118 +\ \\<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))";
7.119 +by (fast_tac (claset() addDs [set_update_subset RS subsetD]
7.120 + addss (simpset() addsimps [zip_update])) 1);
7.121 +qed_spec_mp "approx_loc_imp_approx_loc_subst";
7.122 +
7.123 +
7.124 +Goal
7.125 +"\\<forall>L1 l2 L2. length l1=length L1 \
7.126 +\ \\<longrightarrow> approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \\<and> approx_loc G hp l2 L2)";
7.127 +by (induct_tac "l1" 1);
7.128 + by (fast_tac (claset() addDs [] addss (simpset() addsimps [approx_loc_def])) 1);
7.129 +br allI 1;
7.130 +by (exhaust_tac "L1" 1);
7.131 + by (asm_full_simp_tac (simpset() addsimps []) 1);
7.132 +by (asm_full_simp_tac (simpset() addsimps []) 1);
7.133 +by (Clarify_tac 1);
7.134 +by (asm_full_simp_tac (simpset() addsimps [approx_loc_Cons]) 1);
7.135 +by (case_tac "length l2 = length L2" 1);
7.136 + by (asm_full_simp_tac (simpset() addsimps []) 1);
7.137 +by (asm_full_simp_tac (simpset() addsimps [approx_loc_def]) 1);
7.138 +qed_spec_mp "approx_loc_append";
7.139 +
7.140 +
7.141 +(** approx_stk **)
7.142 +
7.143 +Goalw [approx_stk_def,approx_loc_def]
7.144 +"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t";
7.145 +by (fast_tac (claset() addss (simpset() addsimps [zip_rev,rev_map RS sym])) 1);
7.146 +qed_spec_mp "approx_stk_rev_lem";
7.147 +
7.148 +Goal
7.149 +"approx_stk G hp (rev s) t = approx_stk G hp s (rev t)";
7.150 +by (fast_tac (claset() addIs [approx_stk_rev_lem RS subst] addss (simpset())) 1);
7.151 +qed_spec_mp "approx_stk_rev";
7.152 +
7.153 +Goalw [approx_stk_def]
7.154 +"\\<forall> lvars. approx_stk G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_stk G hp' lvars lt";
7.155 +by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup_heap]) 1);
7.156 +qed_spec_mp "approx_stk_imp_approx_stk_sup_heap";
7.157 +
7.158 +
7.159 +Goalw [approx_stk_def]
7.160 +"wf_prog wt G \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st') >>= (map Some st) \\<longrightarrow> approx_stk G hp lvars st'";
7.161 +by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
7.162 +qed_spec_mp "approx_stk_imp_approx_stk_sup";
7.163 +
7.164 +Goalw [approx_stk_def,approx_loc_def]
7.165 +"approx_stk G hp [] []";
7.166 +by (asm_full_simp_tac (simpset() addsimps []) 1);
7.167 +qed "approx_stk_Nil";
7.168 +
7.169 +
7.170 +Goalw [approx_stk_def,approx_loc_def]
7.171 +"approx_stk G hp (x # stk) (S#ST) = (approx_stk G hp stk ST \\<and> approx_val G hp x (Some S))";
7.172 +by (fast_tac (claset() addss (simpset())) 1);
7.173 +qed "approx_stk_Cons";
7.174 +
7.175 +Goal
7.176 +"\\<lbrakk> approx_stk G hp stk (S#ST') \\<rbrakk> \
7.177 +\ \\<Longrightarrow> \\<exists>s stk'. stk = s#stk' \\<and> approx_stk G hp stk' ST' \\<and> approx_val G hp s (Some S)";
7.178 +by (exhaust_tac "stk" 1);
7.179 + by (fast_tac (claset() addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
7.180 +by (fast_tac (claset() addss (simpset() addsimps [approx_stk_Cons])) 1);
7.181 +qed "approx_stk_Cons_lemma";
7.182 +
7.183 +Goal
7.184 +"\\<forall>ST' stk. approx_stk G hp stk (S@ST') \
7.185 +\ \\<longrightarrow> (\\<exists>s stk'. stk = s@stk' \\<and> length s = length S \\<and> length stk' = length ST' \\<and> \
7.186 +\ approx_stk G hp s S \\<and> approx_stk G hp stk' ST')";
7.187 +by (induct_tac "S" 1);
7.188 + by (fast_tac (claset() addDs [] addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
7.189 +by (Clarify_tac 1);
7.190 +by (asm_full_simp_tac (simpset() addsimps []) 1);
7.191 +bd approx_stk_Cons_lemma 1;
7.192 +by (Clarify_tac 1);
7.193 +by (eres_inst_tac [("x","ST'")] allE 1);
7.194 +by (eres_inst_tac [("x","stk'")] allE 1);
7.195 +by (Clarify_tac 1);
7.196 +by (res_inst_tac [("x","s#sa")] exI 1);
7.197 +by (res_inst_tac [("x","stk'a")] exI 1);
7.198 +by (asm_full_simp_tac (simpset() addsimps [approx_stk_Cons]) 1);
7.199 +qed_spec_mp "approx_stk_append_lemma";
7.200 +
7.201 +
7.202 +(** oconf **)
7.203 +
7.204 +Goalw [oconf_def,lconf_def]
7.205 +"\\<lbrakk> is_class G C; wf_prog wt G \\<rbrakk> \\<Longrightarrow> \
7.206 +\G,h\\<turnstile> (C, map_of (map (\\<lambda>(f,fT).(f,default_val fT)) (fields(G,C))))\\<surd>";
7.207 +by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
7.208 +by (force_tac (claset() addIs [defval_conf]
7.209 + addDs [map_of_SomeD,is_type_fields],simpset()) 1);
7.210 +qed "correct_init_obj";
7.211 +
7.212 +
7.213 +Goalw [oconf_def,lconf_def]
7.214 +"\\<lbrakk> map_of (fields (G, oT)) FD = Some T ; G,hp\\<turnstile>v\\<Colon>\\<preceq>T ; \
7.215 +\ G,hp\\<turnstile>(oT,fs)\\<surd> \\<rbrakk> \
7.216 +\\\<Longrightarrow> G,hp\\<turnstile>(oT, fs(FD\\<mapsto>v))\\<surd>";
7.217 +by (asm_full_simp_tac (simpset() addsplits [ty.split]) 1);
7.218 +qed_spec_mp "oconf_imp_oconf_field_update";
7.219 +
7.220 +
7.221 +Goalw [oconf_def,lconf_def]
7.222 +"hp x = None \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj'\\<surd> \
7.223 +\ \\<longrightarrow> G,(hp(newref hp\\<mapsto>obj'))\\<turnstile>obj\\<surd>";
7.224 +by (Asm_full_simp_tac 1);
7.225 +by (fast_tac (claset() addIs [conf_hext,sup_heap_newref]) 1);
7.226 +qed_spec_mp "oconf_imp_oconf_heap_newref";
7.227 +
7.228 +Goalw [oconf_def,lconf_def]
7.229 +"hp a = Some obj' \\<longrightarrow> obj_ty obj' = obj_ty obj'' \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \
7.230 +\ \\<longrightarrow> G,hp(a\\<mapsto>obj'')\\<turnstile>obj\\<surd>";
7.231 +by (Asm_full_simp_tac 1);
7.232 +by (fast_tac (claset() addIs [approx_val_imp_approx_val_heap_update] addss (simpset())) 1);
7.233 +qed_spec_mp "oconf_imp_oconf_heap_update";
7.234 +
7.235 +
7.236 +(** hconf **)
7.237 +
7.238 +
7.239 +Goal "hp x = None \\<longrightarrow> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G,hp(newref hp\\<mapsto>obj)\\<turnstile>\\<surd>";
7.240 +by (asm_full_simp_tac (simpset() addsplits [split_split]
7.241 + addsimps [hconf_def]) 1);
7.242 + by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1);
7.243 +qed_spec_mp "hconf_imp_hconf_newref";
7.244 +
7.245 +
7.246 +Goal "map_of (fields (G, oT)) (F, D) = Some T \\<and> hp oloc = Some(oT,fs) \\<and> \
7.247 +\ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G,hp\\<turnstile>\\<surd> \\<longrightarrow> G,hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<turnstile>\\<surd>";
7.248 +by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1);
7.249 +by (fast_tac (claset() addIs
7.250 + [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update]
7.251 + addss (simpset() addsimps [obj_ty_def])) 1);
7.252 +qed_spec_mp "hconf_imp_hconf_field_update";
7.253 +
7.254 +
7.255 +(** correct_frames **)
7.256 +
7.257 +Delsimps [fun_upd_apply];
7.258 +Goal
7.259 +"\\<forall>rT C ml. correct_frames G hp phi rT C ml frs \\<longrightarrow> \
7.260 +\ hp a = Some (cn,od) \\<longrightarrow> map_of (fields (G, cn)) fl = Some fd \\<longrightarrow> \
7.261 +\ G,hp\\<turnstile>v\\<Colon>\\<preceq>fd \
7.262 +\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (cn, od(fl\\<mapsto>v)))) phi rT C ml frs";
7.263 +by (induct_tac "frs" 1);
7.264 + by (Asm_full_simp_tac 1);
7.265 +by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);
7.266 +by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
7.267 + approx_loc_imp_approx_loc_sup_heap,
7.268 + sup_heap_update_value] addss (simpset())) 1);
7.269 +qed_spec_mp "correct_frames_imp_correct_frames_field_update";
7.270 +
7.271 +
7.272 +Goal
7.273 +"\\<forall>rT C ml. hp x = None \\<longrightarrow> correct_frames G hp phi rT C ml frs \\<and> \
7.274 +\ oconf G hp obj \
7.275 +\ \\<longrightarrow> correct_frames G (hp(newref hp \\<mapsto> obj)) phi rT C ml frs";
7.276 +by (induct_tac "frs" 1);
7.277 +by (asm_full_simp_tac (simpset() addsimps []) 1);
7.278 +by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);
7.279 +by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
7.280 + approx_loc_imp_approx_loc_sup_heap,
7.281 + hconf_imp_hconf_newref,
7.282 + sup_heap_newref] addss (simpset())) 1);
7.283 +qed_spec_mp "correct_frames_imp_correct_frames_newref";
7.284 +
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/MicroJava/BV/Correct.thy Thu Nov 11 12:23:45 1999 +0100
8.3 @@ -0,0 +1,65 @@
8.4 +(* Title: HOL/MicroJava/BV/Correct.thy
8.5 + ID: $Id$
8.6 + Author: Cornelia Pusch
8.7 + Copyright 1999 Technische Universitaet Muenchen
8.8 +
8.9 +The invariant for the type safety proof.
8.10 +*)
8.11 +
8.12 +Correct = BVSpec +
8.13 +
8.14 +constdefs
8.15 + approx_val :: "[jvm_prog,aheap,val,ty option] \\<Rightarrow> bool"
8.16 +"approx_val G h v any \\<equiv> case any of None \\<Rightarrow> True | Some T \\<Rightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T"
8.17 +
8.18 + approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \\<Rightarrow> bool"
8.19 +"approx_loc G hp loc LT \\<equiv>
8.20 + length loc=length LT \\<and> (\\<forall>(val,any)\\<in>set (zip loc LT). approx_val G hp val any)"
8.21 +
8.22 + approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \\<Rightarrow> bool"
8.23 +"approx_stk G hp stk ST \\<equiv> approx_loc G hp stk (map Some ST)"
8.24 +
8.25 + correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \\<Rightarrow> frame \\<Rightarrow> bool"
8.26 +"correct_frame G hp \\<equiv> \\<lambda>(ST,LT) maxl ins (stk,loc,C,ml,pc).
8.27 + approx_stk G hp stk ST \\<and> approx_loc G hp loc LT \\<and>
8.28 + pc < length ins \\<and> length loc=length(snd ml)+maxl+1"
8.29 +
8.30 +consts
8.31 + correct_frames :: "[jvm_prog,aheap,prog_type,ty,cname,sig,frame list] \\<Rightarrow> bool"
8.32 +primrec
8.33 +"correct_frames G hp phi rT0 C0 ml0 [] = False"
8.34 +
8.35 +"correct_frames G hp phi rT0 C0 ml0 (f#frs) =
8.36 + (let (stk,loc,C,ml,pc) = f;
8.37 + (ST,LT) = (phi C ml) ! pc
8.38 + in
8.39 + (\\<exists>rT maxl ins.
8.40 + cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
8.41 + (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invokevirtual mn pTs) \\<and>
8.42 + (mn,pTs) = ml0 \\<and>
8.43 + (\\<exists>apTs D ST'.
8.44 + fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\<and>
8.45 + length apTs = length pTs \\<and>
8.46 + (\\<exists>D' rT' maxl' ins'.
8.47 + cmethd (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\<and>
8.48 + G \\<turnstile> rT0 \\<preceq> rT') \\<and>
8.49 + correct_frame G hp (tl ST, LT) maxl ins f \\<and>
8.50 + correct_frames G hp phi rT C ml frs))))"
8.51 +
8.52 +
8.53 +constdefs
8.54 + correct_state :: "[jvm_prog,prog_type,jvm_state] \\<Rightarrow> bool"
8.55 +"correct_state G phi \\<equiv> \\<lambda>(xp,hp,frs).
8.56 + case xp of
8.57 + None \\<Rightarrow> (case frs of
8.58 + [] \\<Rightarrow> True
8.59 + | (f#fs) \\<Rightarrow> (let (stk,loc,C,ml,pc) = f
8.60 + in
8.61 + \\<exists>rT maxl ins.
8.62 + cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
8.63 + G,hp\\<turnstile>\\<surd> \\<and>
8.64 + correct_frame G hp ((phi C ml) ! pc) maxl ins f \\<and>
8.65 + correct_frames G hp phi rT C ml fs))
8.66 + | Some x \\<Rightarrow> True"
8.67 +
8.68 +end
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/MicroJava/J/Conform.ML Thu Nov 11 12:23:45 1999 +0100
9.3 @@ -0,0 +1,256 @@
9.4 +(* Title: HOL/MicroJava/J/Conform.ML
9.5 + ID: $Id$
9.6 + Author: David von Oheimb
9.7 + Copyright 1999 Technische Universitaet Muenchen
9.8 +*)
9.9 +
9.10 +section "hext";
9.11 +
9.12 +val hextI = prove_goalw thy [hext_def] "\\<And>h. \
9.13 +\ \\<forall>a C fs . h a = Some (C,fs) \\<longrightarrow> \
9.14 +\ (\\<exists>fs'. h' a = Some (C,fs')) \\<Longrightarrow> h\\<le>|h'" (K [Auto_tac ]);
9.15 +
9.16 +val hext_objD = prove_goalw thy [hext_def]
9.17 +"\\<And>h. \\<lbrakk>h\\<le>|h'; h a = Some (C,fs) \\<rbrakk> \\<Longrightarrow> \\<exists>fs'. h' a = Some (C,fs')"
9.18 + (K [Force_tac 1]);
9.19 +
9.20 +val hext_refl = prove_goal thy "h\\<le>|h" (K [
9.21 + rtac hextI 1,
9.22 + Fast_tac 1]);
9.23 +
9.24 +val hext_new = prove_goal thy "\\<And>h. h a = None \\<Longrightarrow> h\\<le>|h(a\\<mapsto>x)" (K [
9.25 + rtac hextI 1,
9.26 + safe_tac HOL_cs,
9.27 + ALLGOALS (case_tac "aa = a"),
9.28 + Auto_tac]);
9.29 +
9.30 +val hext_trans = prove_goal thy "\\<And>h. \\<lbrakk>h\\<le>|h'; h'\\<le>|h''\\<rbrakk> \\<Longrightarrow> h\\<le>|h''" (K [
9.31 + rtac hextI 1,
9.32 + safe_tac HOL_cs,
9.33 + fast_tac (HOL_cs addDs [hext_objD]) 1]);
9.34 +
9.35 +Addsimps [hext_refl, hext_new];
9.36 +
9.37 +val hext_upd_obj = prove_goal thy
9.38 +"\\<And>h. h a = Some (C,fs) \\<Longrightarrow> h\\<le>|h(a\\<mapsto>(C,fs'))" (K [
9.39 + rtac hextI 1,
9.40 + safe_tac HOL_cs,
9.41 + ALLGOALS (case_tac "aa = a"),
9.42 + Auto_tac]);
9.43 +
9.44 +
9.45 +section "conf";
9.46 +
9.47 +val conf_Null = prove_goalw thy [conf_def]
9.48 +"G,h\\<turnstile>Null\\<Colon>\\<preceq>T = G\\<turnstile>RefT NullT\\<preceq>T" (K [Simp_tac 1]);
9.49 +Addsimps [conf_Null];
9.50 +
9.51 +val conf_litval = prove_goalw thy [conf_def]
9.52 +"typeof (\\<lambda>v. None) v = Some T \\<longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T" (K [
9.53 + rtac val_.induct 1,
9.54 + Auto_tac]) RS mp;
9.55 +
9.56 +val conf_AddrI = prove_goalw thy [conf_def]
9.57 +"\\<And>G. \\<lbrakk>h a = Some obj; G\\<turnstile>obj_ty obj\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq>T"
9.58 +(K [Asm_full_simp_tac 1]);
9.59 +
9.60 +val conf_obj_AddrI = prove_goalw thy [conf_def]
9.61 + "\\<And>G. \\<lbrakk>h a = Some (C,fs); G\\<turnstile>Class C\\<preceq>Class D\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>Addr a\\<Colon>\\<preceq>Class D"
9.62 +(K [Asm_full_simp_tac 1]);
9.63 +
9.64 +Goalw [conf_def] "is_type G T \\<longrightarrow> G,h\\<turnstile>default_val T\\<Colon>\\<preceq>T";
9.65 +by (Simp_tac 1);
9.66 +by (res_inst_tac [("y","T")] ty.exhaust 1);
9.67 +by (etac ssubst 1);
9.68 +by (res_inst_tac [("y","prim_ty")] prim_ty.exhaust 1);
9.69 +by (auto_tac (claset(), simpset() addsimps [widen.null]));
9.70 +qed_spec_mp "defval_conf";
9.71 +
9.72 +val conf_upd_obj = prove_goalw thy [conf_def]
9.73 +"h a = Some (C,fs) \\<longrightarrow> (G,h(a\\<mapsto>(C,fs'))\\<turnstile>x\\<Colon>\\<preceq>T) = (G,h\\<turnstile>x\\<Colon>\\<preceq>T)" (fn _ => [
9.74 + rtac impI 1,
9.75 + rtac val_.induct 1,
9.76 + ALLGOALS Simp_tac,
9.77 + case_tac "loc = a" 1,
9.78 + ALLGOALS Asm_simp_tac]) RS mp;
9.79 +
9.80 +val conf_widen = prove_goalw thy [conf_def]
9.81 +"\\<And>G. wf_prog wtm G \\<Longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T \\<longrightarrow> G\\<turnstile>T\\<preceq>T' \\<longrightarrow> G,h\\<turnstile>x\\<Colon>\\<preceq>T'" (K [
9.82 + rtac val_.induct 1,
9.83 + ALLGOALS Simp_tac,
9.84 + ALLGOALS (fast_tac (HOL_cs addIs [widen_trans]))]) RS mp RS mp;
9.85 +
9.86 +val conf_hext' = prove_goalw thy [conf_def]
9.87 + "\\<And>h. h\\<le>|h' \\<Longrightarrow> (\\<forall>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)" (K [
9.88 + REPEAT (rtac allI 1),
9.89 + rtac val_.induct 1,
9.90 + ALLGOALS Simp_tac,
9.91 + safe_tac (HOL_cs addSDs [option_map_SomeD]),
9.92 + rewtac option_map_def,
9.93 + dtac hext_objD 1,
9.94 + Auto_tac]);
9.95 +val conf_hext = conf_hext' RS spec RS spec RS mp;
9.96 +
9.97 +val new_locD = prove_goalw thy [conf_def]
9.98 + "\\<lbrakk>h a = None; G,h\\<turnstile>Addr t\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> t\\<noteq>a" (fn prems => [
9.99 + cut_facts_tac prems 1,
9.100 + Full_simp_tac 1,
9.101 + safe_tac HOL_cs,
9.102 + Asm_full_simp_tac 1]);
9.103 +
9.104 +val conf_RefTD = prove_goalw thy [conf_def] "G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<longrightarrow> a' = Null | \
9.105 +\ (\\<exists>a obj T'. a' = Addr a \\<and> h a = Some obj \\<and> obj_ty obj = T' \\<and> G\\<turnstile>T'\\<preceq>RefT T)" (K [
9.106 + induct_tac "a'" 1,
9.107 + Auto_tac,
9.108 + REPEAT (etac widen_PrimT_RefT 1)]) RS mp;
9.109 +
9.110 +val conf_NullTD = prove_goal thy "\\<And>G. G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT NullT \\<Longrightarrow> a' = Null" (K [
9.111 + dtac conf_RefTD 1,
9.112 + Step_tac 1,
9.113 + Auto_tac,
9.114 + etac widen_Class_NullT 1]);
9.115 +
9.116 +val non_npD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t\\<rbrakk> \\<Longrightarrow> \
9.117 +\ \\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t" (K [
9.118 + dtac conf_RefTD 1,
9.119 + Step_tac 1,
9.120 + Auto_tac]);
9.121 +
9.122 +val non_np_objD = prove_goal thy "\\<And>G. \\<lbrakk>a' \\<noteq> Null; G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \
9.123 +\ (\\<exists>a C' fs. a' = Addr a \\<and> h a = Some (C',fs) \\<and> G\\<turnstile>Class C'\\<preceq>Class C)"
9.124 + (K[fast_tac (HOL_cs addDs [non_npD]) 1]);
9.125 +
9.126 +Goal "a' \\<noteq> Null \\<longrightarrow> wf_prog wtm G \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>RefT t \\<longrightarrow>\
9.127 +\ (\\<forall>C. t = ClassT C \\<longrightarrow> C \\<noteq> Object) \\<longrightarrow> \
9.128 +\ (\\<exists>a C fs. a' = Addr a \\<and> h a = Some (C,fs) \\<and> G\\<turnstile>Class C\\<preceq>RefT t)";
9.129 +by (rtac impI 1);
9.130 +by (rtac impI 1);
9.131 +by (res_inst_tac [("y","t")] ref_ty.exhaust 1);
9.132 +by (safe_tac HOL_cs);
9.133 +by (dtac conf_NullTD 1);
9.134 +by (contr_tac 1);
9.135 +by (etac non_np_objD 1);
9.136 +by (atac 1);
9.137 +by (Fast_tac 1);
9.138 +qed_spec_mp "non_np_objD'";
9.139 +
9.140 +Goal "wf_prog wtm G \\<Longrightarrow> \\<forall>Ts Ts'. list_all2 (conf G h) vs Ts \\<longrightarrow> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') Ts Ts' \\<longrightarrow> list_all2 (conf G h) vs Ts'";
9.141 +by( induct_tac "vs" 1);
9.142 +by( ALLGOALS Clarsimp_tac);
9.143 +by( ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
9.144 +by( ALLGOALS (full_simp_tac (simpset()addsimps[length_Suc_conv])));
9.145 +by( Safe_tac);
9.146 +by( rotate_tac ~1 1);
9.147 +by( ALLGOALS (forward_tac [list_all2_lengthD RS sym]));
9.148 +by( ALLGOALS (full_simp_tac (simpset()addsimps[length_Suc_conv])));
9.149 +by( ALLGOALS Clarify_tac);
9.150 +by( fast_tac (claset() addEs [conf_widen]) 1);
9.151 +qed_spec_mp "conf_list_gext_widen";
9.152 +
9.153 +
9.154 +section "lconf";
9.155 +
9.156 +val lconfD = prove_goalw thy [lconf_def]
9.157 + "\\<And>X. \\<lbrakk> G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts; Ts n = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>(the (vs n))\\<Colon>\\<preceq>T"
9.158 + (K [Force_tac 1]);
9.159 +
9.160 +val lconf_hext = prove_goalw thy [lconf_def]
9.161 + "\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]L; h\\<le>|h' \\<rbrakk> \\<Longrightarrow> G,h'\\<turnstile>l[\\<Colon>\\<preceq>]L" (K [
9.162 + fast_tac (claset() addEs [conf_hext]) 1]);
9.163 +AddEs [lconf_hext];
9.164 +
9.165 +Goalw [lconf_def] "\\<And>X. \\<lbrakk> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT; \
9.166 +\ G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>l(va\\<mapsto>v)[\\<Colon>\\<preceq>]lT";
9.167 +by( Clarify_tac 1);
9.168 +by( case_tac "n = va" 1);
9.169 + by Auto_tac;
9.170 +qed "lconf_upd";
9.171 +
9.172 +Goal "\\<forall>x. P x \\<longrightarrow> R (dv x) x \\<Longrightarrow> (\\<forall>x. map_of fs f = Some x \\<longrightarrow> P x) \\<longrightarrow> \
9.173 +\ (\\<forall>T. map_of fs f = Some T \\<longrightarrow> \
9.174 +\ (\\<exists>v. map_of (map (\\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \\<and> R v T))";
9.175 +by( induct_tac "fs" 1);
9.176 +by Auto_tac;
9.177 +qed_spec_mp "lconf_init_vars_lemma";
9.178 +
9.179 +Goalw [lconf_def, init_vars_def]
9.180 +"\\<forall>n. \\<forall>T. map_of fs n = Some T \\<longrightarrow> is_type G T \\<Longrightarrow> G,h\\<turnstile>init_vars fs[\\<Colon>\\<preceq>]map_of fs";
9.181 +by Auto_tac;
9.182 +by( rtac lconf_init_vars_lemma 1);
9.183 +by( atac 3);
9.184 +by( strip_tac 1);
9.185 +by( etac defval_conf 1);
9.186 +by Auto_tac;
9.187 +qed "lconf_init_vars";
9.188 +AddSIs [lconf_init_vars];
9.189 +
9.190 +val lconf_ext = prove_goalw thy [lconf_def]
9.191 +"\\<And>X. \\<lbrakk>G,s\\<turnstile>l[\\<Colon>\\<preceq>]L; G,s\\<turnstile>v\\<Colon>\\<preceq>T\\<rbrakk> \\<Longrightarrow> G,s\\<turnstile>l(vn\\<mapsto>v)[\\<Colon>\\<preceq>]L(vn\\<mapsto>T)"
9.192 + (K [Auto_tac]);
9.193 +
9.194 +Goalw [lconf_def] "G,h\\<turnstile>l[\\<Colon>\\<preceq>]L \\<Longrightarrow> \\<forall>vs Ts. nodups vns \\<longrightarrow> length Ts = length vns \\<longrightarrow> list_all2 (\\<lambda>v T. G,h\\<turnstile>v\\<Colon>\\<preceq>T) vs Ts \\<longrightarrow> G,h\\<turnstile>l(vns[\\<mapsto>]vs)[\\<Colon>\\<preceq>]L(vns[\\<mapsto>]Ts)";
9.195 +by( induct_tac "vns" 1);
9.196 +by( ALLGOALS Clarsimp_tac);
9.197 +by( forward_tac [list_all2_lengthD] 1);
9.198 +by( auto_tac (claset(), simpset() addsimps [length_Suc_conv]));
9.199 +qed_spec_mp "lconf_ext_list";
9.200 +
9.201 +
9.202 +section "oconf";
9.203 +
9.204 +val oconf_hext = prove_goalw thy [oconf_def]
9.205 +"\\<And>X. G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> h\\<le>|h' \\<Longrightarrow> G,h'\\<turnstile>obj\\<surd>" (K [Fast_tac 1]);
9.206 +
9.207 +val oconf_obj = prove_goalw thy [oconf_def,lconf_def] "G,h\\<turnstile>(C,fs)\\<surd> = \
9.208 +\ (\\<forall>T f. map_of(fields (G,C)) f = Some T \\<longrightarrow> (\\<exists>v. fs f = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T))"(K [
9.209 + Auto_tac]);
9.210 +
9.211 +val oconf_objD = oconf_obj RS iffD1 RS spec RS spec RS mp;
9.212 +
9.213 +
9.214 +section "hconf";
9.215 +
9.216 +Goalw [hconf_def] "\\<lbrakk>G,h\\<turnstile>\\<surd>; h a = Some obj\\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>obj\\<surd>";
9.217 +by (Fast_tac 1);
9.218 +qed "hconfD";
9.219 +
9.220 +Goalw [hconf_def] "\\<forall>a obj. h a=Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd> \\<Longrightarrow> G,h\\<turnstile>\\<surd>";
9.221 +by (Fast_tac 1);
9.222 +qed "hconfI";
9.223 +
9.224 +
9.225 +section "conforms";
9.226 +
9.227 +val conforms_heapD = prove_goalw thy [conforms_def]
9.228 + "(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>\\<surd>"
9.229 + (fn prems => [cut_facts_tac prems 1, Asm_full_simp_tac 1]);
9.230 +
9.231 +val conforms_localD = prove_goalw thy [conforms_def]
9.232 + "(h, l)\\<Colon>\\<preceq>(G, lT) \\<Longrightarrow> G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT" (fn prems => [
9.233 + cut_facts_tac prems 1, Asm_full_simp_tac 1]);
9.234 +
9.235 +val conformsI = prove_goalw thy [conforms_def]
9.236 +"\\<lbrakk>G,h\\<turnstile>\\<surd>; G,h\\<turnstile>l[\\<Colon>\\<preceq>]lT\\<rbrakk> \\<Longrightarrow> (h, l)\\<Colon>\\<preceq>(G, lT)" (fn prems => [
9.237 + cut_facts_tac prems 1,
9.238 + Simp_tac 1,
9.239 + Auto_tac]);
9.240 +
9.241 +Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G,lT); h\\<le>|h'; G,h'\\<turnstile>\\<surd> \\<rbrakk> \\<Longrightarrow> (h',l)\\<Colon>\\<preceq>(G,lT)";
9.242 +by( fast_tac (HOL_cs addDs [conforms_localD]
9.243 + addSEs [conformsI, lconf_hext]) 1);
9.244 +qed "conforms_hext";
9.245 +
9.246 +Goal "\\<lbrakk>(h,l)\\<Colon>\\<preceq>(G, lT); G,h(a\\<mapsto>obj)\\<turnstile>obj\\<surd>; h\\<le>|h(a\\<mapsto>obj)\\<rbrakk> \\<Longrightarrow> (h(a\\<mapsto>obj),l)\\<Colon>\\<preceq>(G, lT)";
9.247 +by( rtac conforms_hext 1);
9.248 +by Auto_tac;
9.249 +by( rtac hconfI 1);
9.250 +by( dtac conforms_heapD 1);
9.251 +by( (auto_tac (HOL_cs addEs [oconf_hext] addDs [hconfD],
9.252 + simpset()delsimps[split_paired_All])));
9.253 +qed "conforms_upd_obj";
9.254 +
9.255 +Goalw [conforms_def]
9.256 +"\\<lbrakk>(h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>v\\<Colon>\\<preceq>T; lT va = Some T\\<rbrakk> \\<Longrightarrow> \
9.257 +\ (h, l(va\\<mapsto>v))\\<Colon>\\<preceq>(G, lT)";
9.258 +by( auto_tac (claset() addEs [lconf_upd], simpset()));
9.259 +qed "conforms_upd_local";
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/MicroJava/J/Conform.thy Thu Nov 11 12:23:45 1999 +0100
10.3 @@ -0,0 +1,32 @@
10.4 +(* Title: HOL/MicroJava/J/Conform.thy
10.5 + ID: $Id$
10.6 + Author: David von Oheimb
10.7 + Copyright 1999 Technische Universitaet Muenchen
10.8 +
10.9 +Conformity relations for type safety of Java
10.10 +*)
10.11 +
10.12 +Conform = State +
10.13 +
10.14 +constdefs
10.15 +
10.16 + hext :: "aheap \\<Rightarrow> aheap \\<Rightarrow> bool" ( "_\\<le>|_" [51,51] 50)
10.17 + "h\\<le>|h' \\<equiv> \\<forall>a C fs. h a = Some(C,fs) \\<longrightarrow> (\\<exists>fs'. h' a = Some(C,fs'))"
10.18 +
10.19 + conf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> ty \\<Rightarrow> bool" ( "_,_\\<turnstile>_\\<Colon>\\<preceq>_" [51,51,51,51] 50)
10.20 + "G,h\\<turnstile>v\\<Colon>\\<preceq>T \\<equiv> \\<exists>T'. typeof (option_map obj_ty o h) v = Some T' \\<and> G\\<turnstile>T'\\<preceq>T"
10.21 +
10.22 + lconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> ('a \\<leadsto> val) \\<Rightarrow> ('a \\<leadsto> ty) \\<Rightarrow> bool"
10.23 + ("_,_\\<turnstile>_[\\<Colon>\\<preceq>]_" [51,51,51,51] 50)
10.24 + "G,h\\<turnstile>vs[\\<Colon>\\<preceq>]Ts \\<equiv> \\<forall>n T. Ts n = Some T \\<longrightarrow> (\\<exists>v. vs n = Some v \\<and> G,h\\<turnstile>v\\<Colon>\\<preceq>T)"
10.25 +
10.26 + oconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> obj \\<Rightarrow> bool" ("_,_\\<turnstile>_\\<surd>" [51,51,51] 50)
10.27 + "G,h\\<turnstile>obj\\<surd> \\<equiv> G,h\\<turnstile>snd obj[\\<Colon>\\<preceq>]map_of (fields (G,fst obj))"
10.28 +
10.29 + hconf :: "'c prog \\<Rightarrow> aheap \\<Rightarrow> bool" ("_,_\\<turnstile>\\<surd>" [51,51] 50)
10.30 + "G,h\\<turnstile>\\<surd> \\<equiv> \\<forall>a obj. h a = Some obj \\<longrightarrow> G,h\\<turnstile>obj\\<surd>"
10.31 +
10.32 + conforms :: "state \\<Rightarrow> javam env \\<Rightarrow> bool" ("_\\<Colon>\\<preceq>_" [51,51] 50)
10.33 + "s\\<Colon>\\<preceq>E \\<equiv> prg E,heap s\\<turnstile>\\<surd> \\<and> prg E,heap s\\<turnstile>locals s[\\<Colon>\\<preceq>]localT E"
10.34 +
10.35 +end
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/MicroJava/J/Decl.thy Thu Nov 11 12:23:45 1999 +0100
11.3 @@ -0,0 +1,37 @@
11.4 +(* Title: HOL/MicroJava/J/Decl.thy
11.5 + ID: $Id$
11.6 + Author: David von Oheimb
11.7 + Copyright 1997 Technische Universitaet Muenchen
11.8 +
11.9 +Class declarations
11.10 +*)
11.11 +
11.12 +Decl = Type +
11.13 +
11.14 +types fdecl (* field declaration, cf. 8.3 (, 9.3) *)
11.15 + = "vname \\<times> ty"
11.16 +
11.17 +
11.18 +types sig (* signature of a method, cf. 8.4.2 *)
11.19 + = "mname \\<times> ty list"
11.20 +
11.21 + 'c mdecl (* method declaration in a class *)
11.22 + = "sig \\<times> ty \\<times> 'c"
11.23 +
11.24 +types 'c class (* class *)
11.25 + = "cname option \\<times> fdecl list \\<times> 'c mdecl list"
11.26 + (* superclass, fields, methods*)
11.27 +
11.28 + 'c cdecl (* class declaration, cf. 8.1 *)
11.29 + = "cname \\<times> 'c class"
11.30 +
11.31 +consts
11.32 +
11.33 + Object :: cname (* name of root class *)
11.34 + ObjectC :: 'c cdecl (* decl of root class *)
11.35 +
11.36 +defs
11.37 +
11.38 + ObjectC_def "ObjectC \\<equiv> (Object, (None, [], []))"
11.39 +
11.40 +end
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/HOL/MicroJava/J/Eval.ML Thu Nov 11 12:23:45 1999 +0100
12.3 @@ -0,0 +1,39 @@
12.4 +(* Title: HOL/MicroJava/J/Eval.ML
12.5 + ID: $Id$
12.6 + Author: David von Oheimb
12.7 + Copyright 1999 Technische Universitaet Muenchen
12.8 +*)
12.9 +
12.10 +Goal "\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ> v \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
12.11 +\ (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None) \\<and> \
12.12 +\ (G\\<turnstile>(x,s) -c \\<rightarrow> (x',s') \\<longrightarrow> x'=None \\<longrightarrow> x=None)";
12.13 +by(split_all_tac 1);
12.14 +by(rtac eval_evals_exec.induct 1);
12.15 +by(rewtac c_hupd_def);
12.16 +by(ALLGOALS Asm_full_simp_tac);
12.17 +qed "eval_evals_exec_no_xcpt";
12.18 +
12.19 +val eval_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e\\<succ>v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
12.20 + dtac (eval_evals_exec_no_xcpt RS conjunct1 RS mp) 1,
12.21 + Fast_tac 1]);
12.22 +val evals_no_xcpt = prove_goal thy "\\<And>X. G\\<turnstile>(x,s) -e[\\<succ>]v\\<rightarrow> (None,s') \\<Longrightarrow> x=None" (K [
12.23 + dtac (eval_evals_exec_no_xcpt RS conjunct2 RS conjunct1 RS mp) 1,
12.24 + Fast_tac 1]);
12.25 +
12.26 +val eval_evals_exec_xcpt = prove_goal thy
12.27 +"\\<And>s s'. (G\\<turnstile>(x,s) -e \\<succ> v \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
12.28 +\ (G\\<turnstile>(x,s) -es[\\<succ>]vs\\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s) \\<and> \
12.29 +\ (G\\<turnstile>(x,s) -c \\<rightarrow> (x',s') \\<longrightarrow> x=Some xc \\<longrightarrow> x'=Some xc \\<and> s'=s)"
12.30 + (K [
12.31 + split_all_tac 1,
12.32 + rtac eval_evals_exec.induct 1,
12.33 + rewtac c_hupd_def,
12.34 + ALLGOALS Asm_full_simp_tac]);
12.35 +val eval_xcpt = prove_goal thy
12.36 +"\\<And>X. G\\<turnstile>(Some xc,s) -e\\<succ>v\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and> s'=s" (K [
12.37 + dtac (eval_evals_exec_xcpt RS conjunct1 RS mp) 1,
12.38 + Fast_tac 1]);
12.39 +val exec_xcpt = prove_goal thy
12.40 +"\\<And>X. G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (x',s') \\<Longrightarrow> x'=Some xc \\<and> s'=s" (K [
12.41 + dtac (eval_evals_exec_xcpt RS conjunct2 RS conjunct2 RS mp) 1,
12.42 + Fast_tac 1]);
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/HOL/MicroJava/J/Eval.thy Thu Nov 11 12:23:45 1999 +0100
13.3 @@ -0,0 +1,121 @@
13.4 +(* Title: HOL/MicroJava/J/Eval.thy
13.5 + ID: $Id$
13.6 + Author: David von Oheimb
13.7 + Copyright 1999 Technische Universitaet Muenchen
13.8 +
13.9 +Operational evaluation (big-step) semantics of the
13.10 +execution of Java expressions and statements
13.11 +*)
13.12 +
13.13 +Eval = State +
13.14 +
13.15 +consts
13.16 + eval :: "javam prog \\<Rightarrow> (xstate \\<times> expr \\<times> val \\<times> xstate) set"
13.17 + evals :: "javam prog \\<Rightarrow> (xstate \\<times> expr list \\<times> val list \\<times> xstate) set"
13.18 + exec :: "javam prog \\<Rightarrow> (xstate \\<times> stmt \\<times> xstate) set"
13.19 +
13.20 +syntax
13.21 + eval :: "[javam prog,xstate,expr,val,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<succ>_\\<rightarrow> _"[51,82,82,82,82]81)
13.22 + evals:: "[javam prog,xstate,expr list,
13.23 + val list,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_[\\<succ>]_\\<rightarrow> _"[51,82,51,51,82]81)
13.24 + exec :: "[javam prog,xstate,stmt, xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _" [51,82,82, 82]81)
13.25 +
13.26 +translations
13.27 + "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" == "(s, e, v, _args x s') \\<in> eval G"
13.28 + "G\\<turnstile>s -e \\<succ> v\\<rightarrow> s' " == "(s, e, v, s') \\<in> eval G"
13.29 + "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" == "(s, e, v, _args x s') \\<in> evals G"
13.30 + "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> s' " == "(s, e, v, s') \\<in> evals G"
13.31 + "G\\<turnstile>s -c \\<rightarrow> (x,s')" == "(s, c, _args x s') \\<in> exec G"
13.32 + "G\\<turnstile>s -c \\<rightarrow> s' " == "(s, c, s') \\<in> exec G"
13.33 +
13.34 +inductive "eval G" "evals G" "exec G" intrs
13.35 +
13.36 +(* evaluation of expressions *)
13.37 +
13.38 + (* cf. 15.5 *)
13.39 + XcptE "G\\<turnstile>(Some xc,s) -e\\<succ>arbitrary\\<rightarrow> (Some xc,s)"
13.40 +
13.41 + (* cf. 15.8.1 *)
13.42 + NewC "\\<lbrakk>h = heap s; (a,x) = new_Addr h;
13.43 + h'= h(a\\<mapsto>(C,init_vars (fields (G,C))))\\<rbrakk> \\<Longrightarrow>
13.44 + G\\<turnstile>Norm s -NewC C\\<succ>Addr a\\<rightarrow> c_hupd h' (x,s)"
13.45 +
13.46 + (* cf. 15.15 *)
13.47 + Cast "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> (x1,s1);
13.48 + x2=raise_if (\\<not> cast_ok G T (heap s1) v) ClassCast x1\\<rbrakk> \\<Longrightarrow>
13.49 + G\\<turnstile>Norm s0 -Cast T e\\<succ>v\\<rightarrow> (x2,s1)"
13.50 +
13.51 + (* cf. 15.7.1 *)
13.52 + Lit "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
13.53 +
13.54 + (* cf. 15.13.1, 15.2 *)
13.55 + LAcc "G\\<turnstile>Norm s -LAcc v\\<succ>the (locals s v)\\<rightarrow> Norm s"
13.56 +
13.57 + (* cf. 15.25.1 *)
13.58 + LAss "\\<lbrakk>G\\<turnstile>Norm s -e\\<succ>v\\<rightarrow> (x,(h,l));
13.59 + l' = (if x = None then l(va\\<mapsto>v) else l)\\<rbrakk> \\<Longrightarrow>
13.60 + G\\<turnstile>Norm s -va\\<Colon>=e\\<succ>v\\<rightarrow> (x,(h,l'))"
13.61 +
13.62 +
13.63 + (* cf. 15.10.1, 15.2 *)
13.64 + FAcc "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> (x1,s1);
13.65 + v = the (snd (the (heap s1 (the_Addr a'))) (fn,T))\\<rbrakk> \\<Longrightarrow>
13.66 + G\\<turnstile>Norm s0 -{T}e..fn\\<succ>v\\<rightarrow> (np a' x1,s1)"
13.67 +
13.68 + (* cf. 15.25.1 *)
13.69 + FAss "\\<lbrakk>G\\<turnstile> Norm s0 -e1\\<succ>a'\\<rightarrow> (x1,s1); a = the_Addr a';
13.70 + G\\<turnstile>(np a' x1,s1) -e2\\<succ>v \\<rightarrow> (x2,s2);
13.71 + h = heap s2; (c,fs) = the (h a);
13.72 + h' = h(a\\<mapsto>(c,(fs((fn,T)\\<mapsto>v))))\\<rbrakk> \\<Longrightarrow>
13.73 + G\\<turnstile>Norm s0 -{T}e1..fn\\<in>=e2\\<succ>v\\<rightarrow> c_hupd h' (x2,s2)"
13.74 +
13.75 + (* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)
13.76 + Call "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>a'\\<rightarrow> s1; a = the_Addr a';
13.77 + G\\<turnstile>s1 -ps[\\<succ>]pvs\\<rightarrow> (x,(h,l)); dynT = fst (the (h a));
13.78 + (md,rT,pns,lvars,blk,res) = the (cmethd (G,dynT) (mn,pTs));
13.79 + G\\<turnstile>(np a' x,(h,(init_vars lvars)(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))) -blk\\<rightarrow> s3;
13.80 + G\\<turnstile> s3 -res\\<succ>v \\<rightarrow> (x4,s4)\\<rbrakk> \\<Longrightarrow>
13.81 + G\\<turnstile>Norm s0 -e..mn({pTs}ps)\\<succ>v\\<rightarrow> (x4,(heap s4,l))"
13.82 +
13.83 +
13.84 +(* evaluation of expression lists *)
13.85 +
13.86 + (* cf. 15.5 *)
13.87 + XcptEs "G\\<turnstile>(Some xc,s) -e[\\<succ>]arbitrary\\<rightarrow> (Some xc,s)"
13.88 +
13.89 + (* cf. 15.11.??? *)
13.90 + Nil
13.91 + "G\\<turnstile>Norm s0 -[][\\<succ>][]\\<rightarrow> Norm s0"
13.92 +
13.93 + (* cf. 15.6.4 *)
13.94 + Cons "\\<lbrakk>G\\<turnstile>Norm s0 -e \\<succ> v \\<rightarrow> s1;
13.95 + G\\<turnstile> s1 -es[\\<succ>]vs\\<rightarrow> s2\\<rbrakk> \\<Longrightarrow>
13.96 + G\\<turnstile>Norm s0 -e#es[\\<succ>]v#vs\\<rightarrow> s2"
13.97 +
13.98 +(* execution of statements *)
13.99 +
13.100 + (* cf. 14.1 *)
13.101 + XcptS "G\\<turnstile>(Some xc,s) -s0\\<rightarrow> (Some xc,s)"
13.102 +
13.103 + (* cf. 14.5 *)
13.104 + Skip "G\\<turnstile>Norm s -Skip\\<rightarrow> Norm s"
13.105 +
13.106 + (* cf. 14.7 *)
13.107 + Expr "\\<lbrakk>G\\<turnstile>Norm s0 -e\\<succ>v\\<rightarrow> s1\\<rbrakk> \\<Longrightarrow>
13.108 + G\\<turnstile>Norm s0 -Expr e\\<rightarrow> s1"
13.109 +
13.110 + (* cf. 14.2 *)
13.111 + Comp "\\<lbrakk>G\\<turnstile>Norm s0 -s \\<rightarrow> s1;
13.112 + G\\<turnstile> s1 -t \\<rightarrow> s2\\<rbrakk> \\<Longrightarrow>
13.113 + G\\<turnstile>Norm s0 -(s;; t)\\<rightarrow> s2"
13.114 +
13.115 + (* cf. 14.8.2 *)
13.116 + Cond "\\<lbrakk>G\\<turnstile>Norm s0 -e \\<succ>v\\<rightarrow> s1;
13.117 + G\\<turnstile> s1 -(if the_Bool v then s else t)\\<rightarrow> s2\\<rbrakk> \\<Longrightarrow>
13.118 + G\\<turnstile>Norm s0 -(If(e) s Else t)\\<rightarrow> s2"
13.119 +
13.120 + (* cf. 14.10, 14.10.1 *)
13.121 + Loop "\\<lbrakk>G\\<turnstile>Norm s0 -(If(e) (s;; While(e) s) Else Skip)\\<rightarrow> s1\\<rbrakk> \\<Longrightarrow>
13.122 + G\\<turnstile>Norm s0 -(While(e) s)\\<rightarrow> s1"
13.123 +
13.124 +end
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/HOL/MicroJava/J/JBasis.ML Thu Nov 11 12:23:45 1999 +0100
14.3 @@ -0,0 +1,230 @@
14.4 +(* Title: HOL/MicroJava/J/JBasis.ML
14.5 + ID: $Id$
14.6 + Author: David von Oheimb
14.7 + Copyright 1999 TU Muenchen
14.8 +*)
14.9 +
14.10 +val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE]));
14.11 +
14.12 +Goalw [image_def]
14.13 + "x \\<in> f``A \\<Longrightarrow> \\<exists>y. y \\<in> A \\<and> x = f y";
14.14 +by(Auto_tac);
14.15 +qed "image_rev";
14.16 +
14.17 +fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)];
14.18 +
14.19 +val select_split = prove_goalw Prod.thy [split_def]
14.20 + "(\\<epsilon>(x,y). P x y) = (\\<epsilon>xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
14.21 +
14.22 +
14.23 +val split_beta = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)"
14.24 + (fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]);
14.25 +val split_beta2 = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z"
14.26 + (fn _ => [Auto_tac]);
14.27 +val splitE2 = prove_goal Prod.thy "\\<lbrakk>Q (split P z); \\<And>x y. \\<lbrakk>z = (x, y); Q (P x y)\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
14.28 + REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
14.29 + rtac (split_beta RS subst) 1,
14.30 + rtac (hd prems) 1]);
14.31 +val splitE2' = prove_goal Prod.thy "\\<lbrakk>((\\<lambda>(x,y). P x y) z) w; \\<And>x y. \\<lbrakk>z = (x, y); (P x y) w\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> R" (fn prems => [
14.32 + REPEAT (resolve_tac (prems@[surjective_pairing]) 1),
14.33 + res_inst_tac [("P1","P")] (split_beta RS subst) 1,
14.34 + rtac (hd prems) 1]);
14.35 +
14.36 +
14.37 +fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac;
14.38 +
14.39 +val BallE = prove_goal thy "\\<lbrakk>Ball A P; x \\<notin> A \\<Longrightarrow> Q; P x \\<Longrightarrow> Q \\<rbrakk> \\<Longrightarrow> Q"
14.40 + (fn prems => [rtac ballE 1, resolve_tac prems 1,
14.41 + eresolve_tac prems 1, eresolve_tac prems 1]);
14.42 +
14.43 +val set_cs2 = set_cs delrules [ballE] addSEs [BallE];
14.44 +
14.45 +Addsimps [Let_def];
14.46 +Addsimps [surjective_pairing RS sym];
14.47 +
14.48 +(* To HOL.ML *)
14.49 +
14.50 +val ex1_Eps_eq = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y"
14.51 + (fn prems => [
14.52 + cut_facts_tac prems 1,
14.53 + rtac select_equality 1,
14.54 + atac 1,
14.55 + etac ex1E 1,
14.56 + etac all_dupE 1,
14.57 + fast_tac HOL_cs 1]);
14.58 +
14.59 +
14.60 +val ball_insert = prove_goalw equalities.thy [Ball_def]
14.61 + "Ball (insert x A) P = (P x \\<and> Ball A P)" (fn _ => [
14.62 + fast_tac set_cs 1]);
14.63 +
14.64 +fun option_case_tac i = EVERY [
14.65 + etac option_caseE i,
14.66 + rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
14.67 + rotate_tac ~2 i , asm_full_simp_tac HOL_basic_ss i];
14.68 +
14.69 +val not_None_tac = EVERY' [dtac (not_None_eq RS iffD1),rotate_tac ~1,etac exE,
14.70 + rotate_tac ~1,asm_full_simp_tac
14.71 + (simpset() delsimps [split_paired_All,split_paired_Ex])];
14.72 +
14.73 +fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
14.74 + asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
14.75 +
14.76 +val optionE = prove_goal thy
14.77 + "\\<lbrakk> opt = None \\<Longrightarrow> P; \\<And>x. opt = Some x \\<Longrightarrow> P \\<rbrakk> \\<Longrightarrow> P"
14.78 + (fn prems => [
14.79 + case_tac "opt = None" 1,
14.80 + eresolve_tac prems 1,
14.81 + not_None_tac 1,
14.82 + eresolve_tac prems 1]);
14.83 +
14.84 +fun option_case_tac2 s i = EVERY [
14.85 + exhaust_tac s i,
14.86 + rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
14.87 + rotate_tac ~1 i , asm_full_simp_tac HOL_basic_ss i];
14.88 +
14.89 +val option_map_SomeD = prove_goalw thy [option_map_def]
14.90 + "\\<And>x. option_map f x = Some y \\<Longrightarrow> \\<exists>z. x = Some z \\<and> f z = y" (K [
14.91 + option_case_tac2 "x" 1,
14.92 + Auto_tac]);
14.93 +
14.94 +
14.95 +section "unique";
14.96 +
14.97 +Goal "(x, y) : set l --> x : fst `` set l";
14.98 +by (induct_tac "l" 1);
14.99 +by Auto_tac;
14.100 +qed_spec_mp "fst_in_set_lemma";
14.101 +
14.102 +Goalw [unique_def] "unique []";
14.103 +by (Simp_tac 1);
14.104 +qed "unique_Nil";
14.105 +
14.106 +Goalw [unique_def] "unique ((x,y)#l) = (unique l \\<and> (!y. (x,y) ~: set l))";
14.107 +by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
14.108 +qed "unique_Cons";
14.109 +
14.110 +Addsimps [unique_Nil,unique_Cons];
14.111 +
14.112 +Goal "unique l' ==> unique l --> \
14.113 +\ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')";
14.114 +by (induct_tac "l" 1);
14.115 +by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
14.116 +qed_spec_mp "unique_append";
14.117 +
14.118 +Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)";
14.119 +by (induct_tac "l" 1);
14.120 +by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
14.121 +qed_spec_mp "unique_map_inj";
14.122 +
14.123 +Goal "\\<And>l. unique l \\<Longrightarrow> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
14.124 +by(etac unique_map_inj 1);
14.125 +by(rtac injI 1);
14.126 +by Auto_tac;
14.127 +qed "unique_map_Pair";
14.128 +
14.129 +Goal "\\<lbrakk>M = N; \\<And>x. x\\<in>N \\<Longrightarrow> f x = g x\\<rbrakk> \\<Longrightarrow> f``M = g``N";
14.130 +by(rtac set_ext 1);
14.131 +by(simp_tac (simpset() addsimps image_def::premises()) 1);
14.132 +qed "image_cong";
14.133 +
14.134 +val split_Pair_eq = prove_goal Prod.thy
14.135 +"\\<And>X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A \\<Longrightarrow> y = Y" (K [
14.136 + etac imageE 1,
14.137 + split_all_tac 1,
14.138 + auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
14.139 +
14.140 +
14.141 +section "list_all2";
14.142 +
14.143 +val list_all2_lengthD = prove_goalw thy [list_all2_def]
14.144 + "\\<And>X. list_all2 P as bs \\<Longrightarrow> length as = length bs" (K [Auto_tac]);
14.145 +
14.146 +val list_all2_Nil = prove_goalw thy [list_all2_def]
14.147 + "list_all2 P [] []" (K [Auto_tac]);
14.148 +Addsimps[list_all2_Nil];
14.149 +AddSIs[list_all2_Nil];
14.150 +
14.151 +val list_all2_Cons = prove_goalw thy [list_all2_def]
14.152 + "\\<And>X. list_all2 P (a#as) (b#bs) = (P a b \\<and> list_all2 P as bs)" (K [Auto_tac]);
14.153 +AddIffs[list_all2_Cons];
14.154 +
14.155 +
14.156 +(* More about Maps *)
14.157 +
14.158 +val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x \\<Longrightarrow> \
14.159 +\ t k = Some x | t k = None \\<and> s k = Some x" (fn prems => [
14.160 + cut_facts_tac prems 1,
14.161 + case_tac "\\<exists>x. t k = Some x" 1,
14.162 + etac exE 1,
14.163 + rotate_tac ~1 1,
14.164 + Asm_full_simp_tac 1,
14.165 + asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1,
14.166 + rotate_tac ~1 1,
14.167 + Asm_full_simp_tac 1]);
14.168 +
14.169 +Addsimps [fun_upd_same, fun_upd_other];
14.170 +
14.171 +Goal "unique xys \\<longrightarrow> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
14.172 +by(induct_tac "xys" 1);
14.173 + by(Simp_tac 1);
14.174 +by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
14.175 +qed_spec_mp "unique_map_of_Some_conv";
14.176 +
14.177 +val in_set_get = unique_map_of_Some_conv RS iffD2;
14.178 +val get_in_set = unique_map_of_Some_conv RS iffD1;
14.179 +
14.180 +Goal "(\\<forall>(x,y)\\<in>set l. P x y) \\<longrightarrow> (\\<forall>x. \\<forall>y. map_of l x = Some y \\<longrightarrow> P x y)";
14.181 +by(induct_tac "l" 1);
14.182 +by(ALLGOALS Simp_tac);
14.183 +by Safe_tac;
14.184 +by Auto_tac;
14.185 +bind_thm("Ball_set_table",result() RS mp);
14.186 +
14.187 +val table_mono = prove_goal thy
14.188 +"unique l' \\<longrightarrow> (\\<forall>xy. (xy)\\<in>set l \\<longrightarrow> (xy)\\<in>set l') \\<longrightarrow>\
14.189 +\ (\\<forall>k y. map_of l k = Some y \\<longrightarrow> map_of l' k = Some y)" (fn _ => [
14.190 + induct_tac "l" 1,
14.191 + Auto_tac,
14.192 + fast_tac (HOL_cs addSIs [in_set_get]) 1])
14.193 + RS mp RS mp RS spec RS spec RS mp;
14.194 +
14.195 +val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) \\<longrightarrow> \
14.196 +\ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
14.197 + induct_tac "t" 1,
14.198 + ALLGOALS Simp_tac,
14.199 + case_tac1 "k = fst a" 1,
14.200 + Auto_tac]) RS mp;
14.201 +val table_map_Some = prove_goal thy
14.202 +"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \\<longrightarrow> \
14.203 +\map_of t (k, k') = Some x" (K [
14.204 + induct_tac "t" 1,
14.205 + Auto_tac]) RS mp;
14.206 +
14.207 +
14.208 +val table_mapf_Some = prove_goal thy "\\<And>f. \\<forall>x y. f x = f y \\<longrightarrow> x = y \\<Longrightarrow> \
14.209 +\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) \\<longrightarrow> map_of t k = Some x" (K [
14.210 + induct_tac "t" 1,
14.211 + Auto_tac]) RS mp;
14.212 +val table_mapf_SomeD = prove_goal thy
14.213 +"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z \\<longrightarrow> (\\<exists>y. (k,y)\\<in>set t \\<and> z = f y)"(K [
14.214 + induct_tac "t" 1,
14.215 + Auto_tac]) RS mp;
14.216 +
14.217 +val table_mapf_Some2 = prove_goal thy
14.218 +"\\<And>k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) \\<Longrightarrow> C = D \\<and> map_of t k = Some x" (K [
14.219 + forward_tac [table_mapf_SomeD] 1,
14.220 + Auto_tac,
14.221 + rtac table_mapf_Some 1,
14.222 + atac 2,
14.223 + Fast_tac 1]);
14.224 +
14.225 +val finite_map_of = rewrite_rule [dom_def] finite_dom_map_of;
14.226 +
14.227 +Goal
14.228 +"map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
14.229 +by (induct_tac "xs" 1);
14.230 +auto();
14.231 +qed "map_of_map";
14.232 +
14.233 +
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/HOL/MicroJava/J/JBasis.thy Thu Nov 11 12:23:45 1999 +0100
15.3 @@ -0,0 +1,19 @@
15.4 +(* Title: HOL/MicroJava/J/JBasis.thy
15.5 + ID: $Id$
15.6 + Author: David von Oheimb
15.7 + Copyright 1999 TU Muenchen
15.8 +
15.9 +Some auxiliary definitions.
15.10 +*)
15.11 +
15.12 +JBasis = Main +
15.13 +
15.14 +constdefs
15.15 +
15.16 + unique :: "('a \\<times> 'b) list \\<Rightarrow> bool"
15.17 + "unique \\<equiv> nodups \\<circ> map fst"
15.18 +
15.19 + list_all2 :: "('a \\<Rightarrow> 'b \\<Rightarrow> bool) \\<Rightarrow> ('a list \\<Rightarrow> 'b list \\<Rightarrow> bool)"
15.20 + "list_all2 P xs ys \\<equiv> length xs = length ys \\<and> (\\<forall> (x,y)\\<in>set (zip xs ys). P x y)"
15.21 +
15.22 +end
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML Thu Nov 11 12:23:45 1999 +0100
16.3 @@ -0,0 +1,349 @@
16.4 +(* Title: HOL/MicroJava/J/JTypeSafe.ML
16.5 + ID: $Id$
16.6 + Author: David von Oheimb
16.7 + Copyright 1999 Technische Universitaet Muenchen
16.8 +
16.9 +Type safety proof
16.10 +*)
16.11 +
16.12 +Addsimps [split_beta];
16.13 +
16.14 +Goal "\\<lbrakk>h a = None; (h, l)\\<Colon>\\<preceq>(G, lT); wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> \
16.15 +\ (h(a\\<mapsto>(C,(init_vars (fields (G,C))))), l)\\<Colon>\\<preceq>(G, lT)";
16.16 +by( etac conforms_upd_obj 1);
16.17 +by( rewtac oconf_def);
16.18 +by( auto_tac (claset() addSDs [is_type_fields, map_of_SomeD], simpset()));
16.19 +qed "NewC_conforms";
16.20 +
16.21 +Goalw [cast_ok_def]
16.22 + "\\<lbrakk> wf_prog wtm G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<Rightarrow>? T'; cast_ok G T' h v\\<rbrakk> \
16.23 +\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T'";
16.24 +by( case_tac1 "v = Null" 1);
16.25 +by( Asm_full_simp_tac 1);
16.26 +by( dtac widen_RefT 1);
16.27 +by( Clarify_tac 1);
16.28 +by( forward_tac [cast_RefT] 1);
16.29 +by( Clarify_tac 1);
16.30 +by( rtac widen.null 1);
16.31 +by( case_tac1 "\\<exists>pt. T' = PrimT pt" 1);
16.32 +by( strip_tac1 1);
16.33 +by( dtac cast_PrimT2 1);
16.34 +by( etac conf_widen 1);
16.35 +by( atac 1);
16.36 +by( atac 1);
16.37 +by( Asm_full_simp_tac 1);
16.38 +by( dtac (non_PrimT RS iffD1) 1);
16.39 +by( strip_tac1 1);
16.40 +by( forward_tac [cast_RefT2] 1);
16.41 +by( strip_tac1 1);
16.42 +by( dtac non_npD 1);
16.43 +by( atac 1);
16.44 +by( rewrite_goals_tac [the_Addr_def,obj_ty_def]);
16.45 +by Auto_tac ;
16.46 +by( ALLGOALS (rtac conf_AddrI));
16.47 +by Auto_tac;
16.48 +qed "Cast_conf";
16.49 +
16.50 +Goal "\\<lbrakk> wf_prog wtm G; cfield (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \
16.51 +\ x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq>Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \
16.52 +\ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft";
16.53 +by( dtac np_NoneD 1);
16.54 +by( etac conjE 1);
16.55 +by( mp_tac 1);
16.56 +by( dtac non_np_objD 1);
16.57 +by Auto_tac;
16.58 +by( dtac (conforms_heapD RS hconfD) 1);
16.59 +by( atac 1);
16.60 +by( dtac widen_cfs_fields 1);
16.61 +by( atac 1);
16.62 +by( atac 1);
16.63 +by( dtac oconf_objD 1);
16.64 +by( atac 1);
16.65 +by Auto_tac;
16.66 +val FAcc_type_sound = result();
16.67 +
16.68 +Goal
16.69 + "\\<lbrakk> wf_prog wtm G; a = the_Addr a'; (c, fs) = the (h a); \
16.70 +\ (G, lT)\\<turnstile>v\\<Colon>T'; G\\<turnstile>T'\\<preceq>ft; \
16.71 +\ (G, lT)\\<turnstile>aa\\<Colon>Class C; \
16.72 +\ cfield (G,C) fn = Some (fd, ft); h''\\<le>|h'; \
16.73 +\ x' = None \\<longrightarrow> G,h'\\<turnstile>a'\\<Colon>\\<preceq>Class C; h'\\<le>|h; \
16.74 +\ (h, l)\\<Colon>\\<preceq>(G, lT); G,h\\<turnstile>x\\<Colon>\\<preceq>T'; np a' x' = None\\<rbrakk> \\<Longrightarrow> \
16.75 +\ h''\\<le>|h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))) \\<and> \
16.76 +\ (h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x)))), l)\\<Colon>\\<preceq>(G, lT) \\<and> \
16.77 +\ G,h(a\\<mapsto>(c,(fs((fn,fd)\\<mapsto>x))))\\<turnstile>x\\<Colon>\\<preceq>T'";
16.78 +by( dtac np_NoneD 1);
16.79 +by( etac conjE 1);
16.80 +by( Asm_full_simp_tac 1);
16.81 +by( dtac non_np_objD 1);
16.82 +by( atac 1);
16.83 +by( SELECT_GOAL Auto_tac 1);
16.84 +by( strip_tac1 1);
16.85 +by( Full_simp_tac 1);
16.86 +by( EVERY [forward_tac [hext_objD] 1, atac 1]);
16.87 +by( etac exE 1);
16.88 +by( Asm_full_simp_tac 1);
16.89 +by( strip_tac1 1);
16.90 +by( rtac conjI 1);
16.91 +by( fast_tac (HOL_cs addEs [hext_trans, hext_upd_obj]) 1);
16.92 +by( rtac conjI 1);
16.93 +by( fast_tac (HOL_cs addEs [conf_upd_obj RS iffD2]) 2);
16.94 +
16.95 +by( rtac conforms_upd_obj 1);
16.96 +by Auto_tac;
16.97 +by( rtac hextI 2);
16.98 +by( Force_tac 2);
16.99 +by( rtac oconf_hext 1);
16.100 +by( etac hext_upd_obj 2);
16.101 +by( dtac widen_cfs_fields 1);
16.102 +by( atac 1);
16.103 +by( atac 1);
16.104 +by( rtac (oconf_obj RS iffD2) 1);
16.105 +by( Simp_tac 1);
16.106 +by( strip_tac 1);
16.107 +by( case_tac1 "(aaa, b) = (fn, fd)" 1);
16.108 +by( Asm_full_simp_tac 1);
16.109 +by( fast_tac (HOL_cs addIs [conf_widen]) 1);
16.110 +by( fast_tac (HOL_cs addDs [conforms_heapD RS hconfD, oconf_objD]) 1);
16.111 +val FAss_type_sound = result();
16.112 +
16.113 +Goalw [wf_mhead_def] "\\<lbrakk> wf_prog wtm G; list_all2 (conf G h) pvs pTs; \
16.114 + \ list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; \
16.115 +\ length pTs' = length pns; nodups pns; \
16.116 +\ Ball (set lvars) (split (\\<lambda>vn. is_type G)) \
16.117 +\ \\<rbrakk> \\<Longrightarrow> G,h\\<turnstile>init_vars lvars(pns[\\<mapsto>]pvs)[\\<Colon>\\<preceq>]map_of lvars(pns[\\<mapsto>]pTs')";
16.118 +by( Clarsimp_tac 1);
16.119 +by( rtac lconf_ext_list 1);
16.120 +by( rtac (Ball_set_table RS lconf_init_vars) 1);
16.121 +by( Force_tac 1);
16.122 +by( atac 1);
16.123 +by( atac 1);
16.124 +by( (etac conf_list_gext_widen THEN_ALL_NEW atac) 1);
16.125 +qed "Call_lemma2";
16.126 +
16.127 +Goalw [wf_java_prog_def]
16.128 + "\\<lbrakk> wf_java_prog G; a' \\<noteq> Null; (h, l)\\<Colon>\\<preceq>(G, lT); \
16.129 +\ max_spec G T (mn,pTsa) = {((mda,rTa),pTs')}; xc\\<le>|xh; xh\\<le>|h; \
16.130 +\ list_all2 (conf G h) pvs pTsa;\
16.131 +\ (md, rT, pns, lvars, blk, res) = \
16.132 +\ the (cmethd (G,fst (the (h (the_Addr a')))) (mn, pTs'));\
16.133 +\ \\<forall>lT. (h, init_vars lvars(pns[\\<mapsto>]pvs)(This\\<mapsto>a'))\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> \
16.134 +\ (G, lT)\\<turnstile>blk\\<surd> \\<longrightarrow> h\\<le>|xi \\<and> (xi, xl)\\<Colon>\\<preceq>(G, lT); \
16.135 +\ \\<forall>lT. (xi, xl)\\<Colon>\\<preceq>(G, lT) \\<longrightarrow> (\\<forall>T. (G, lT)\\<turnstile>res\\<Colon>T \\<longrightarrow> \
16.136 +\ xi\\<le>|h' \\<and> (h', xj)\\<Colon>\\<preceq>(G, lT) \\<and> (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>T)); \
16.137 +\ G,xh\\<turnstile>a'\\<Colon>\\<preceq>RefT T \\<rbrakk> \\<Longrightarrow> \
16.138 +\ xc\\<le>|h' \\<and> (h', l)\\<Colon>\\<preceq>(G, lT) \\<and> (x' = None \\<longrightarrow> G,h'\\<turnstile>v\\<Colon>\\<preceq>rTa)";
16.139 +by( dtac (insertI1 RSN (2,(equalityD2 RS subsetD))) 1);
16.140 +by( dtac (max_spec2appl_meths RS appl_methsD) 1);
16.141 +by( etac conjE 1);
16.142 +by( dtac non_np_objD' 1);
16.143 +by( atac 1);
16.144 +by( atac 1);
16.145 +by( strip_tac1 1);
16.146 +by( Asm_full_simp_tac 1);
16.147 +by( Clarsimp_tac 1);
16.148 +by( EVERY'[forward_tac [hext_objD], atac] 1);
16.149 +by( Clarsimp_tac 1);
16.150 +by( EVERY'[dtac Call_lemma, atac, atac] 1);
16.151 +by( clarsimp_tac (claset(),simpset() addsimps [wt_java_mdecl_def])1);
16.152 +by( thin_tac "cmethd ?sig ?x = ?y" 1);
16.153 +by( EVERY'[dtac spec, etac impE] 1);
16.154 +by( mp_tac 2);
16.155 +by( rtac conformsI 1);
16.156 +by( etac conforms_heapD 1);
16.157 +by( rtac lconf_ext 1);
16.158 +by( force_tac (claset() addSEs [Call_lemma2],simpset()) 1);
16.159 +by( EVERY'[etac conf_hext, etac conf_obj_AddrI, atac] 1);
16.160 +by( thin_tac "?E\\<turnstile>?blk\\<surd>" 1);
16.161 +by( etac conjE 1);
16.162 +by( EVERY'[dtac spec, mp_tac] 1);
16.163 +(*by( thin_tac "?E\\<Colon>\\<preceq>(G, pT')" 1);*)
16.164 +by( EVERY'[dtac spec, mp_tac] 1);
16.165 +by( thin_tac "?E\\<turnstile>res\\<Colon>?rT" 1);
16.166 +by( strip_tac1 1);
16.167 +by( rtac conjI 1);
16.168 +by( fast_tac (HOL_cs addIs [hext_trans]) 1);
16.169 +by( rtac conjI 1);
16.170 +by( rtac impI 2);
16.171 +by( mp_tac 2);
16.172 +by( forward_tac [conf_widen] 2);
16.173 +by( atac 4);
16.174 +by( atac 2);
16.175 +by( fast_tac (HOL_cs addSEs [widen_trans]) 2);
16.176 +by( etac conforms_hext 1);
16.177 +by( etac hext_trans 1);
16.178 +by( atac 1);
16.179 +by( etac conforms_heapD 1);
16.180 +qed "Call_type_sound";
16.181 +
16.182 +
16.183 +
16.184 +Unify.search_bound := 40;
16.185 +Unify.trace_bound := 40;
16.186 +Delsplits[split_if];
16.187 +Delsimps[fun_upd_apply];(*###*)
16.188 +Goal
16.189 +"wf_java_prog G \\<Longrightarrow> \
16.190 +\ (G\\<turnstile>(x,(h,l)) -e \\<succ>v \\<rightarrow> (x', (h',l')) \\<longrightarrow> \
16.191 +\ (\\<forall>lT. (h ,l )\\<Colon>\\<preceq>(G,lT) \\<longrightarrow> (\\<forall>T . (G,lT)\\<turnstile>e \\<Colon> T \\<longrightarrow> \
16.192 +\ h\\<le>|h' \\<and> (h',l')\\<Colon>\\<preceq>(G,lT) \\<and> (x'=None \\<longrightarrow> G,h'\\<turnstile>v \\<Colon>\\<preceq> T )))) \\<and> \
16.193 +\ (G\\<turnstile>(x,(h,l)) -es[\\<succ>]vs\\<rightarrow> (x', (h',l')) \\<longrightarrow> \
16.194 +\ (\\<forall>lT. (h ,l )\\<Colon>\\<preceq>(G,lT) \\<longrightarrow> (\\<forall>Ts. (G,lT)\\<turnstile>es[\\<Colon>]Ts \\<longrightarrow> \
16.195 +\ h\\<le>|h' \\<and> (h',l')\\<Colon>\\<preceq>(G,lT) \\<and> (x'=None \\<longrightarrow> list_all2 (\\<lambda>v T. G,h'\\<turnstile>v\\<Colon>\\<preceq>T) vs Ts)))) \\<and> \
16.196 +\ (G\\<turnstile>(x,(h,l)) -c \\<rightarrow> (x', (h',l')) \\<longrightarrow> \
16.197 +\ (\\<forall>lT. (h ,l )\\<Colon>\\<preceq>(G,lT) \\<longrightarrow> (G,lT)\\<turnstile>c \\<surd> \\<longrightarrow> \
16.198 +\ h\\<le>|h' \\<and> (h',l')\\<Colon>\\<preceq>(G,lT)))";
16.199 +by( rtac eval_evals_exec.induct 1);
16.200 +by( rewtac c_hupd_def);
16.201 +
16.202 +(* several simplifications, XcptE, XcptEs, XcptS, Skip *)
16.203 +by( ALLGOALS Asm_full_simp_tac);
16.204 +by( ALLGOALS strip_tac);
16.205 +by( ALLGOALS (eresolve_tac ty_expr_ty_exprs_wt_stmt.elims
16.206 + THEN_ALL_NEW Full_simp_tac));
16.207 +by( ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac]));
16.208 +by( rewtac wf_java_prog_def);
16.209 +
16.210 +(* Level 7 *)
16.211 +
16.212 +(* 14 NewC *)
16.213 +by( dtac new_AddrD 1);
16.214 +by( etac disjE 1);
16.215 +by( Asm_simp_tac 2);
16.216 +by( etac conjE 1);
16.217 +by( Asm_simp_tac 1);
16.218 +by( rtac conjI 1);
16.219 +by( fast_tac (HOL_cs addSEs [NewC_conforms]) 1);
16.220 +by( rtac conf_obj_AddrI 1);
16.221 +by( rtac widen.refl 2);
16.222 +by( Asm_simp_tac 2);
16.223 +by( Simp_tac 1);
16.224 +
16.225 +(* for Cast *)
16.226 +by( defer_tac 1);
16.227 +
16.228 +(* 13 Lit *)
16.229 +by( etac conf_litval 1);
16.230 +
16.231 +(* 12 LAcc *)
16.232 +by( fast_tac (claset() addEs [conforms_localD RS lconfD]) 1);
16.233 +
16.234 +(* 11 Nil *)
16.235 +by( Simp_tac 5);
16.236 +
16.237 +(* for FAss *)
16.238 +by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac,
16.239 + REPEAT o (etac conjE), hyp_subst_tac] 3);
16.240 +
16.241 +(* for if *)
16.242 +by( (case_tac1 "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 8);
16.243 +
16.244 +val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac,
16.245 + (mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)]));
16.246 +by forward_hyp_tac;
16.247 +
16.248 +(* 10+1 if *)
16.249 +by( fast_tac (HOL_cs addIs [hext_trans]) 8);
16.250 +by( fast_tac (HOL_cs addIs [hext_trans]) 8);
16.251 +
16.252 +(* 9 Expr *)
16.253 +by( Fast_tac 6);
16.254 +
16.255 +by( ALLGOALS Asm_full_simp_tac);
16.256 +
16.257 +(* 8 Cast *)
16.258 +by( EVERY'[rtac impI, dtac raise_if_NoneD, Clarsimp_tac,
16.259 + fast_tac (claset() addEs [Cast_conf])] 8);
16.260 +
16.261 +(* 7 LAss *)
16.262 +by( asm_simp_tac (simpset() addsplits [expand_if]) 1);
16.263 +by( EVERY'[eresolve_tac ty_expr_ty_exprs_wt_stmt.elims THEN_ALL_NEW Full_simp_tac] 1);
16.264 +by( blast_tac (claset() addIs [conforms_upd_local, conf_widen]) 1);
16.265 +
16.266 +(* 6 FAcc *)
16.267 +by( fast_tac (claset() addSEs [FAcc_type_sound]) 1);
16.268 +
16.269 +(* 5 While *)
16.270 +by( fast_tac (claset() addIs [ty_expr_ty_exprs_wt_stmt.Cond, ty_expr_ty_exprs_wt_stmt.Comp, ty_expr_ty_exprs_wt_stmt.Skip]
16.271 + addEs [ty_expr_ty_exprs_wt_stmt.Loop]) 5);
16.272 +
16.273 +by forward_hyp_tac;
16.274 +
16.275 +(* 4 Cons *)
16.276 +by( fast_tac (claset() addDs [evals_no_xcpt] addIs [conf_hext,hext_trans]) 3);
16.277 +
16.278 +(* 3 ;; *)
16.279 +by( fast_tac (claset() addIs [hext_trans]) 3);
16.280 +
16.281 +(* 2 FAss *)
16.282 +by( case_tac1 "x2 = None" 1);
16.283 +by( Asm_simp_tac 2);
16.284 +by( fast_tac (claset() addIs [hext_trans]) 2);
16.285 +by( Asm_full_simp_tac 1);
16.286 +by( dtac eval_no_xcpt 1);
16.287 +by( SELECT_GOAL (etac FAss_type_sound 1 THEN rtac refl 1 THEN ALLGOALS atac) 1);
16.288 +
16.289 +by prune_params_tac;
16.290 +(* Level 45 *)
16.291 +
16.292 +(* 1 Call *)
16.293 +by( case_tac1 "x = None" 1);
16.294 +by( dtac (not_None_eq RS iffD1) 2);
16.295 +by( Clarsimp_tac 2);
16.296 +by( dtac exec_xcpt 2);
16.297 +by( Asm_full_simp_tac 2);
16.298 +by( dtac eval_xcpt 2);
16.299 +by( Asm_full_simp_tac 2);
16.300 +by( fast_tac (HOL_cs addEs [hext_trans]) 2);
16.301 +by( Clarify_tac 1);
16.302 +by( dtac evals_no_xcpt 1);
16.303 +by( Asm_full_simp_tac 1);
16.304 +by( case_tac1 "a' = Null" 1);
16.305 +by( Asm_full_simp_tac 1);
16.306 +by( dtac exec_xcpt 1);
16.307 +by( Asm_full_simp_tac 1);
16.308 +by( dtac eval_xcpt 1);
16.309 +by( Asm_full_simp_tac 1);
16.310 +by( fast_tac (HOL_cs addEs [hext_trans]) 1);
16.311 +by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) THEN_ALL_NEW Asm_simp_tac) 1);
16.312 +qed "eval_evals_exec_type_sound";
16.313 +
16.314 +Goal "\\<And>E s s'. \
16.315 +\ \\<lbrakk> G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>v \\<rightarrow> (x',s'); s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>T \\<rbrakk> \
16.316 +\ \\<Longrightarrow> s'\\<Colon>\\<preceq>E \\<and> (x'=None \\<longrightarrow> G,heap s'\\<turnstile>v\\<Colon>\\<preceq>T)";
16.317 +by( split_all_tac 1);
16.318 +bd (eval_evals_exec_type_sound RS conjunct1 RS mp RS spec RS mp) 1;
16.319 +by Auto_tac;
16.320 +qed "eval_type_sound";
16.321 +
16.322 +Goal "\\<And>E s s'. \
16.323 +\ \\<lbrakk> G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -s0\\<rightarrow> (x',s'); s\\<Colon>\\<preceq>E; E\\<turnstile>s0\\<surd> \\<rbrakk> \
16.324 +\ \\<Longrightarrow> s'\\<Colon>\\<preceq>E";
16.325 +by( split_all_tac 1);
16.326 +bd (eval_evals_exec_type_sound RS conjunct2 RS conjunct2 RS mp RS spec RS mp) 1;
16.327 +by Auto_tac;
16.328 +qed "exec_type_sound";
16.329 +
16.330 +Goal "\\<lbrakk>G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>a'\\<rightarrow> Norm s'; a' \\<noteq> Null;\
16.331 +\ s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>RefT T; m_head G T sig \\<noteq> None\\<rbrakk> \\<Longrightarrow> \
16.332 +\ cmethd (G,fst (the (heap s' (the_Addr a')))) sig \\<noteq> None";
16.333 +by( dtac eval_type_sound 1);
16.334 +by( atac 1);
16.335 +by( atac 1);
16.336 +by( atac 1);
16.337 +by( atac 1);
16.338 +by( not_None_tac 1);
16.339 +by( split_all_tac 1);
16.340 +by(rewtac wf_java_prog_def);
16.341 +by( forward_tac [widen_methd] 1);
16.342 +by( atac 1);
16.343 +by( rtac (not_None_eq RS iffD1) 2);
16.344 +by( Fast_tac 2);
16.345 +by( etac conjE 1);
16.346 +by( dtac non_npD 1);
16.347 +by Auto_tac;
16.348 +qed "all_methods_understood";
16.349 +
16.350 +Delsimps [split_beta];
16.351 +Addsimps[fun_upd_apply];(*###*)
16.352 +
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Nov 11 12:23:45 1999 +0100
17.3 @@ -0,0 +1,9 @@
17.4 +(* Title: HOL/MicroJava/J/JTypeSafe.thy
17.5 + ID: $Id$
17.6 + Author: David von Oheimb
17.7 + Copyright 1999 Technische Universitaet Muenchen
17.8 +
17.9 +Type Safety of Java
17.10 +*)
17.11 +
17.12 +JTypeSafe = Eval + Conform
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/HOL/MicroJava/J/Prog.ML Thu Nov 11 12:23:45 1999 +0100
18.3 @@ -0,0 +1,15 @@
18.4 +(* Title: HOL/MicroJava/J/Prog.ML
18.5 + ID: $Id$
18.6 + Author: David von Oheimb
18.7 + Copyright 1999 Technische Universitaet Muenchen
18.8 +*)
18.9 +
18.10 +val finite_is_class = prove_goalw thy [is_class_def,class_def,o_def] "finite {C. is_class G C}" (K [
18.11 + rtac finite_map_of 1]);
18.12 +
18.13 +val is_classI = prove_goalw thy [is_class_def]
18.14 +"\\<And>G. class G C = Some c \\<Longrightarrow> is_class G C" (K [Auto_tac]);
18.15 +
18.16 +val is_classD = prove_goalw thy [is_class_def]
18.17 +"\\<And>G. is_class G C \\<Longrightarrow> \\<exists>sc fs ms. class G C = Some (sc,fs,ms)" (K [
18.18 + not_None_tac 1, pair_tac "y" 1, pair_tac "ya" 1, Auto_tac]);
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/HOL/MicroJava/J/Prog.thy Thu Nov 11 12:23:45 1999 +0100
19.3 @@ -0,0 +1,30 @@
19.4 +(* Title: HOL/MicroJava/J/Prog.thy
19.5 + ID: $Id$
19.6 + Author: David von Oheimb
19.7 + Copyright 1999 Technische Universitaet Muenchen
19.8 +
19.9 +Java program = list of class declarations
19.10 +*)
19.11 +
19.12 +Prog = Decl +
19.13 +
19.14 +types 'c prog = "'c cdecl list"
19.15 +
19.16 +consts
19.17 +
19.18 + class :: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"
19.19 +
19.20 + is_class :: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
19.21 + is_type :: "'c prog \\<Rightarrow> ty \\<Rightarrow> bool"
19.22 +
19.23 +defs
19.24 +
19.25 + class_def "class \\<equiv> map_of"
19.26 +
19.27 + is_class_def "is_class G C \\<equiv> class G C \\<noteq> None"
19.28 +
19.29 +primrec
19.30 +"is_type G (PrimT pt) = True"
19.31 +"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"
19.32 +
19.33 +end
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/HOL/MicroJava/J/State.ML Thu Nov 11 12:23:45 1999 +0100
20.3 @@ -0,0 +1,77 @@
20.4 +(* Title: HOL/MicroJava/J/State.ML
20.5 + ID: $Id$
20.6 + Author: David von Oheimb
20.7 + Copyright 1999 Technische Universitaet Muenchen
20.8 +*)
20.9 +
20.10 +val the_Addr_Addr = prove_goalw thy [the_Addr_def]
20.11 + "the_Addr (Addr a) = a" (K [Auto_tac]);
20.12 +
20.13 +Addsimps [the_Addr_Addr];
20.14 +
20.15 +val obj_ty_def2 = prove_goalw thy [obj_ty_def] "obj_ty (C,fs) = Class C"
20.16 + (K [Simp_tac 1]);
20.17 +
20.18 +Addsimps [obj_ty_def2];
20.19 +
20.20 +val new_AddrD = prove_goalw thy [new_Addr_def]
20.21 +"\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and> x = None | x = Some OutOfMemory" (K[
20.22 + asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1,
20.23 + rtac selectI 1,
20.24 + rtac disjI2 1,
20.25 + res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1,
20.26 + Auto_tac ]);
20.27 +
20.28 +val raise_if_True = prove_goalw thy [raise_if_def]
20.29 + "raise_if True x y \\<noteq> None"
20.30 +(K [split_tac [expand_if] 1,Auto_tac]);
20.31 +
20.32 +val raise_if_False = prove_goalw thy [raise_if_def]
20.33 + "raise_if False x y = y"
20.34 +(K [Auto_tac]);
20.35 +
20.36 +val raise_if_Some = prove_goalw thy [raise_if_def]
20.37 + "raise_if c x (Some y) \\<noteq> None" (K [Auto_tac]);
20.38 +
20.39 +val raise_if_Some2 = prove_goalw thy [raise_if_def]
20.40 +"raise_if c z (if x = None then Some y else x) \\<noteq> None" (K[
20.41 + induct_tac "x" 1,
20.42 + Auto_tac]);
20.43 +val if_None_eq = prove_goal thy
20.44 +"(if x = None then None else x) = x" (K[
20.45 + induct_tac "x" 1,
20.46 + Auto_tac]);
20.47 +
20.48 +Addsimps [raise_if_True,raise_if_False,raise_if_Some,raise_if_Some2,if_None_eq];
20.49 +
20.50 +val raise_if_SomeD = prove_goalw thy [raise_if_def]
20.51 + "raise_if c x y = Some z \\<longrightarrow> c \\<and> Some z = Some x | y = Some z"
20.52 +(K [split_tac [expand_if] 1,Auto_tac]) RS mp;
20.53 +
20.54 +val raise_if_NoneD = prove_goalw thy [raise_if_def]
20.55 + "raise_if c x y = None \\<longrightarrow> \\<not> c \\<and> y = None"
20.56 +(K [split_tac [expand_if] 1,Auto_tac]) RS mp;
20.57 +
20.58 +
20.59 +val np_NoneD = (prove_goalw thy [np_def, raise_if_def]
20.60 + "np a' x' = None \\<longrightarrow> x' = None \\<and> a' \\<noteq> Null" (fn _ => [
20.61 + split_tac [expand_if] 1,
20.62 + Auto_tac ])) RS mp;
20.63 +val np_None = (prove_goalw thy [np_def, raise_if_def]
20.64 + "a' \\<noteq> Null \\<longrightarrow> np a' x' = x'" (fn _ => [
20.65 + split_tac [expand_if] 1,
20.66 + Auto_tac ])) RS mp;
20.67 +val np_Some = prove_goalw thy [np_def, raise_if_def] "np a' (Some xc) = Some xc"
20.68 + (fn _ => [Auto_tac ]);
20.69 +val np_Null = prove_goalw thy [np_def, raise_if_def]
20.70 + "np Null None = Some NullPointer" (fn _ => [
20.71 + Auto_tac ]);
20.72 +val np_Addr = prove_goalw thy [np_def, raise_if_def] "np (Addr a) None = None"
20.73 + (fn _ => [Auto_tac ]);
20.74 +Addsimps[np_None, np_Some,np_Null,np_Addr];
20.75 +
20.76 +
20.77 +
20.78 +
20.79 +
20.80 +
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/HOL/MicroJava/J/State.thy Thu Nov 11 12:23:45 1999 +0100
21.3 @@ -0,0 +1,91 @@
21.4 +(* Title: HOL/MicroJava/J/State.thy
21.5 + ID: $Id$
21.6 + Author: David von Oheimb
21.7 + Copyright 1999 Technische Universitaet Muenchen
21.8 +
21.9 +State for evaluation of Java expressions and statements
21.10 +*)
21.11 +
21.12 +State = WellType +
21.13 +
21.14 +constdefs
21.15 +
21.16 + the_Bool :: "val \\<Rightarrow> bool"
21.17 + "the_Bool v \\<equiv> \\<epsilon>b. v = Bool b"
21.18 +
21.19 + the_Int :: "val \\<Rightarrow> int"
21.20 + "the_Int v \\<equiv> \\<epsilon>i. v = Intg i"
21.21 +
21.22 + the_Addr :: "val \\<Rightarrow> loc"
21.23 + "the_Addr v \\<equiv> \\<epsilon>a. v = Addr a"
21.24 +
21.25 +consts
21.26 +
21.27 + defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *)
21.28 + default_val :: "ty \\<Rightarrow> val" (* default value for all types *)
21.29 +
21.30 +primrec
21.31 + "defpval Void = Unit"
21.32 + "defpval Boolean = Bool False"
21.33 + "defpval Integer = Intg (#0)"
21.34 +
21.35 +primrec
21.36 + "default_val (PrimT pt) = defpval pt"
21.37 + "default_val (RefT r ) = Null"
21.38 +
21.39 +types fields_
21.40 + = "(vname \\<times> cname \\<leadsto> val)" (* field name, defining class, value *)
21.41 +
21.42 +types obj = "cname \\<times> fields_" (* class instance with class name and fields *)
21.43 +
21.44 +constdefs
21.45 +
21.46 + obj_ty :: "obj \\<Rightarrow> ty"
21.47 + "obj_ty obj \\<equiv> Class (fst obj)"
21.48 +
21.49 + init_vars :: "('a \\<times> ty) list \\<Rightarrow> ('a \\<leadsto> val)"
21.50 + "init_vars \\<equiv> map_of o map (\\<lambda>(n,T). (n,default_val T))"
21.51 +
21.52 +datatype xcpt (* exceptions *)
21.53 + = NullPointer
21.54 + | ClassCast
21.55 + | OutOfMemory
21.56 +
21.57 +types aheap = "loc \\<leadsto> obj" (* "heap" used in a translation below *)
21.58 + locals = "vname \\<leadsto> val"
21.59 +
21.60 + state (* simple state, i.e. variable contents *)
21.61 + = "aheap \\<times> locals"
21.62 + (* heap, local parameter including This *)
21.63 +
21.64 + xstate (* state including exception information *)
21.65 + = "xcpt option \\<times> state"
21.66 +
21.67 +syntax
21.68 + heap :: "state \\<Rightarrow> aheap"
21.69 + locals :: "state \\<Rightarrow> locals"
21.70 + Norm :: "state \\<Rightarrow> xstate"
21.71 +
21.72 +translations
21.73 + "heap" => "fst"
21.74 + "locals" => "snd"
21.75 + "Norm s" == "(None,s)"
21.76 +
21.77 +constdefs
21.78 +
21.79 + new_Addr :: "aheap \\<Rightarrow> loc \\<times> xcpt option"
21.80 + "new_Addr h \\<equiv> \\<epsilon>(a,x). (h a = None \\<and> x = None) | x = Some OutOfMemory"
21.81 +
21.82 + raise_if :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option \\<Rightarrow> xcpt option"
21.83 + "raise_if c x xo \\<equiv> if c \\<and> (xo = None) then Some x else xo"
21.84 +
21.85 + np :: "val \\<Rightarrow> xcpt option \\<Rightarrow> xcpt option"
21.86 + "np v \\<equiv> raise_if (v = Null) NullPointer"
21.87 +
21.88 + c_hupd :: "aheap \\<Rightarrow> xstate \\<Rightarrow> xstate"
21.89 + "c_hupd h'\\<equiv> \\<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
21.90 +
21.91 + cast_ok :: "'c prog \\<Rightarrow> ty \\<Rightarrow> aheap \\<Rightarrow> val \\<Rightarrow> bool"
21.92 + "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)"
21.93 +
21.94 +end
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/src/HOL/MicroJava/J/Term.thy Thu Nov 11 12:23:45 1999 +0100
22.3 @@ -0,0 +1,41 @@
22.4 +(* Title: HOL/MicroJava/J/Term.thy
22.5 + ID: $Id$
22.6 + Author: David von Oheimb
22.7 + Copyright 1999 Technische Universitaet Muenchen
22.8 +
22.9 +Java expressions and statements
22.10 +*)
22.11 +
22.12 +Term = Type +
22.13 +
22.14 +types loc (* locations, i.e. abstract references on objects *)
22.15 +arities loc :: term
22.16 +
22.17 +datatype val_ (* name non 'val' because of clash with ML token *)
22.18 + = Unit (* dummy result value of void methods *)
22.19 + | Null (* null reference *)
22.20 + | Bool bool (* Boolean value *)
22.21 + | Intg int (* integer value *) (* Name Intg instead of Int because
22.22 + of clash with HOL/Set.thy *)
22.23 + | Addr loc (* addresses, i.e. locations of objects *)
22.24 +types val = val_
22.25 +translations "val" <= (type) "val_"
22.26 +
22.27 +datatype expr
22.28 + = NewC cname (* class instance creation *)
22.29 + | Cast ty expr (* type cast *)
22.30 + | Lit val (* literal value, also references *)
22.31 + | LAcc vname (* local (incl. parameter) access *)
22.32 + | LAss vname expr (* local assign *) ("_\\<Colon>=_" [ 90,90]90)
22.33 + | FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90)
22.34 + | FAss cname expr vname
22.35 + expr (* field ass. *)("{_}_.._\\<in>=_"[10,90,99,90]90)
22.36 + | Call expr mname (ty list) (expr list)(* method call*)
22.37 + ("_.._'({_}_')" [90,99,10,10] 90)
22.38 +and stmt
22.39 + = Skip (* empty statement *)
22.40 + | Expr expr (* expression statement *)
22.41 + | Comp stmt stmt ("_;; _" [ 61,60]60)
22.42 + | Cond expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
22.43 + | Loop expr stmt ("While'(_') _" [ 80,79]70)
22.44 +end
23.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
23.2 +++ b/src/HOL/MicroJava/J/Type.ML Thu Nov 11 12:23:45 1999 +0100
23.3 @@ -0,0 +1,10 @@
23.4 +(* Title: HOL/MicroJava/J/Type.ML
23.5 + ID: $Id$
23.6 + Author: David von Oheimb
23.7 + Copyright 1999 Technische Universitaet Muenchen
23.8 +*)
23.9 +
23.10 +Goal "(\\<forall>pt. T \\<noteq> PrimT pt) = (\\<exists>t. T = RefT t)";
23.11 +by(exhaust_tac "T" 1);
23.12 +by Auto_tac;
23.13 +qed "non_PrimT";
24.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
24.2 +++ b/src/HOL/MicroJava/J/Type.thy Thu Nov 11 12:23:45 1999 +0100
24.3 @@ -0,0 +1,39 @@
24.4 +(* Title: HOL/MicroJava/J/Type.thy
24.5 + ID: $Id$
24.6 + Author: David von Oheimb
24.7 + Copyright 1999 Technische Universitaet Muenchen
24.8 +
24.9 +Java types
24.10 +*)
24.11 +
24.12 +Type = JBasis +
24.13 +
24.14 +types cname (* class name *)
24.15 + vnam (* variable or field name *)
24.16 + mname (* method name *)
24.17 +arities cname, vnam, mname :: term
24.18 +
24.19 +datatype vname (* names for This pointer and local/field variables *)
24.20 + = This
24.21 + | VName vnam
24.22 +
24.23 +datatype prim_ty (* primitive type, cf. 4.2 *)
24.24 + = Void (* 'result type' of void methods *)
24.25 + | Boolean
24.26 + | Integer
24.27 +
24.28 +datatype ref_ty (* reference type, cf. 4.3 *)
24.29 + = NullT (* null type, cf. 4.1 *)
24.30 + | ClassT cname (* class type *)
24.31 +and ty (* any type, cf. 4.1 *)
24.32 + = PrimT prim_ty (* primitive type *)
24.33 + | RefT ref_ty (* reference type *)
24.34 +
24.35 +syntax
24.36 + NT :: " ty"
24.37 + Class :: "cname \\<Rightarrow> ty"
24.38 +translations
24.39 + "NT" == "RefT NullT"
24.40 + "Class C" == "RefT (ClassT C)"
24.41 +
24.42 +end
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/src/HOL/MicroJava/J/TypeRel.ML Thu Nov 11 12:23:45 1999 +0100
25.3 @@ -0,0 +1,143 @@
25.4 +(* Title: HOL/MicroJava/J/TypeRel.ML
25.5 + ID: $Id$
25.6 + Author: David von Oheimb
25.7 + Copyright 1999 Technische Universitaet Muenchen
25.8 +*)
25.9 +
25.10 +val subcls1D = prove_goalw thy [subcls1_def] "\\<And>G. G\\<turnstile>C\\<prec>C1D \\<Longrightarrow> \
25.11 +\ \\<exists>fs ms. class G C = Some (Some D,fs,ms)" (K [Auto_tac]);
25.12 +
25.13 +val subcls1I = prove_goalw thy [subcls1_def]
25.14 +"\\<And>G. \\<lbrakk> class G C = Some (Some D,rest) \\<rbrakk> \\<Longrightarrow> G\\<turnstile>C\\<prec>C1D" (K [Auto_tac]);
25.15 +
25.16 +val subcls1_def2 = prove_goalw thy [subcls1_def,is_class_def] "subcls1 G = \
25.17 +\ (SIGMA C:{C. is_class G C} . {D. fst (the (class G C)) = Some D})"
25.18 + (K [Auto_tac]);
25.19 +
25.20 +context Option.thy;
25.21 +Goal "{y. x = Some y} \\<subseteq> {the x}";
25.22 +by Auto_tac;
25.23 +val some_subset_the = result();
25.24 +context thy;
25.25 +
25.26 +Goal "finite (subcls1 G)";
25.27 +by(stac subcls1_def2 1);
25.28 +by( rtac finite_SigmaI 1);
25.29 +by( rtac finite_is_class 1);
25.30 +by( rtac finite_subset 1);
25.31 +by( rtac some_subset_the 1);
25.32 +by( Simp_tac 1);
25.33 +qed "finite_subcls1";
25.34 +
25.35 +fun prove_typerel_lemma drules indrule s = prove_goal thy s (fn prems => [
25.36 + rtac (hd prems RS indrule) 1,
25.37 + auto_tac (claset() addDs drules, simpset())]);
25.38 +
25.39 +fun prove_typerel s lemmata = prove_goal thy s (fn prems => [
25.40 + cut_facts_tac prems 1,
25.41 + auto_tac (claset() addDs lemmata, simpset())]);
25.42 +
25.43 +
25.44 +(*#### patch for Isabelle98-1*)
25.45 +val major::prems = goal Trancl.thy
25.46 + "\\<lbrakk> (x,y) \\<in> r^+; \
25.47 +\ \\<And>x y. (x,y) \\<in> r \\<Longrightarrow> P x y; \
25.48 +\ \\<And>x y z. \\<lbrakk> (x,y) \\<in> r^+; P x y; (y,z) \\<in> r^+; P y z \\<rbrakk> \\<Longrightarrow> P x z \
25.49 +\ \\<rbrakk> \\<Longrightarrow> P x y";
25.50 +by(blast_tac (claset() addIs ([r_into_trancl,major RS trancl_induct]@prems))1);
25.51 +qed "trancl_trans_induct";
25.52 +
25.53 +Goalw [is_class_def] "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> is_class G C";
25.54 +by(etac trancl_trans_induct 1);
25.55 +by (auto_tac (HOL_cs addSDs [subcls1D],simpset()));
25.56 +qed "subcls_is_class";
25.57 +
25.58 +
25.59 +(* A particular thm about wf;
25.60 + looks like it is an odd instance of something more general
25.61 +*)
25.62 +Goalw [wf_def] "wf{((A,x),(B,y)) . A=B \\<and> wf(R(A)) \\<and> (x,y)\\<in>R(A)}";
25.63 +by(full_simp_tac (simpset() delcongs [imp_cong] addsimps [split_paired_All]) 1);
25.64 +by(strip_tac 1);
25.65 +by(rename_tac "A x" 1);
25.66 +by(case_tac "wf(R A)" 1);
25.67 +by (eres_inst_tac [("a","x")] wf_induct 1);
25.68 +by (EVERY1[etac allE, etac allE, etac mp, rtac allI, rtac allI]);
25.69 +by (Fast_tac 1);
25.70 +by(rewrite_goals_tac [wf_def]);
25.71 +by(Blast_tac 1);
25.72 +val wf_rel_lemma = result();
25.73 +
25.74 +
25.75 +(* Proving the termination conditions *)
25.76 +
25.77 +goalw thy [subcls1_rel_def] "wf subcls1_rel";
25.78 +by(rtac (wf_rel_lemma RS wf_subset) 1);
25.79 +by(Force_tac 1);
25.80 +val wf_subcls1_rel = result();
25.81 +
25.82 +val cmethd_TC = prove_goalw_cterm [subcls1_rel_def]
25.83 + (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (cmethd.tcs)))))
25.84 + (K [auto_tac (claset() addIs [subcls1I], simpset())]);
25.85 +
25.86 +val fields_TC = prove_goalw_cterm [subcls1_rel_def]
25.87 + (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd (tl (fields.tcs)))))
25.88 + (K [auto_tac (claset() addIs [subcls1I], simpset())]);
25.89 +
25.90 +
25.91 +AddSIs [widen.refl];
25.92 +Addsimps [widen.refl];
25.93 +
25.94 +val prove_widen_lemma = prove_typerel_lemma [] widen.elim;
25.95 +
25.96 +val widen_PrimT_RefT = prove_typerel "G\\<turnstile>PrimT x\\<preceq>RefT tname \\<Longrightarrow> R"
25.97 + [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = RefT tname \\<longrightarrow> R"];
25.98 +
25.99 +
25.100 +val widen_RefT = prove_typerel "G\\<turnstile>RefT R\\<preceq>T \\<Longrightarrow> \\<exists>t. T=RefT t"
25.101 + [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
25.102 +
25.103 +val widen_RefT2 = prove_typerel "G\\<turnstile>S\\<preceq>RefT R \\<Longrightarrow> \\<exists>t. S=RefT t"
25.104 + [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
25.105 +
25.106 +val widen_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>T \\<Longrightarrow> \\<exists>D. T=Class D"
25.107 + [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> (\\<exists>D. T=Class D)"];
25.108 +
25.109 +val widen_Class_RefT = prove_typerel
25.110 + "G\\<turnstile>Class C\\<preceq>RefT t \\<Longrightarrow> (\\<exists>tname. t=ClassT tname)"
25.111 + [prove_widen_lemma
25.112 + "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT t \\<longrightarrow> (\\<exists>tname. t=ClassT tname)"];
25.113 +
25.114 +val widen_Class_NullT = prove_typerel "G\\<turnstile>Class C\\<preceq>RefT NullT \\<Longrightarrow> R"
25.115 + [prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S=Class C \\<longrightarrow> T=RefT NullT \\<longrightarrow> R"];
25.116 +
25.117 +val widen_Class_Class = prove_typerel "G\\<turnstile>Class C\\<preceq>Class cm \\<Longrightarrow> C=cm | G\\<turnstile>C\\<prec>C cm"
25.118 +[ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = Class C \\<longrightarrow> T = Class cm \\<longrightarrow> C=cm | G\\<turnstile>C\\<prec>C cm"];
25.119 +
25.120 +Goal "\\<lbrakk>G\\<turnstile>S\\<preceq>U; \\<forall>C. is_class G C \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object;\
25.121 +\\\<forall>C. G\\<turnstile>Object\\<prec>C C \\<longrightarrow> False \\<rbrakk> \\<Longrightarrow> \\<forall>T. G\\<turnstile>U\\<preceq>T \\<longrightarrow> G\\<turnstile>S\\<preceq>T";
25.122 +by( etac widen.induct 1);
25.123 +by Safe_tac;
25.124 +by( ALLGOALS (forward_tac [widen_Class, widen_RefT]));
25.125 +by Safe_tac;
25.126 +by( rtac widen.null 2);
25.127 +by( forward_tac [widen_Class_Class] 1);
25.128 +by Safe_tac;
25.129 +by( ALLGOALS(EVERY'[etac thin_rl,etac thin_rl,
25.130 + fast_tac (claset() addIs [widen.subcls,trancl_trans])]));
25.131 +qed_spec_mp "widen_trans_lemma";
25.132 +
25.133 +
25.134 +val prove_cast_lemma = prove_typerel_lemma [] cast.elim;
25.135 +
25.136 +val cast_RefT = prove_typerel "G\\<turnstile>RefT R\\<Rightarrow>? T \\<Longrightarrow> \\<exists>t. T=RefT t"
25.137 + [prove_typerel_lemma [widen_RefT] cast.elim
25.138 + "G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> S=RefT R \\<longrightarrow> (\\<exists>t. T=RefT t)"];
25.139 +
25.140 +val cast_RefT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? RefT R \\<Longrightarrow> \\<exists>t. S=RefT t"
25.141 + [prove_typerel_lemma [widen_RefT2] cast.elim
25.142 + "G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=RefT R \\<longrightarrow> (\\<exists>t. S=RefT t)"];
25.143 +
25.144 +val cast_PrimT2 = prove_typerel "G\\<turnstile>S\\<Rightarrow>? PrimT pt \\<Longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"
25.145 + [prove_cast_lemma "G\\<turnstile>S\\<Rightarrow>? T \\<Longrightarrow> T=PrimT pt \\<longrightarrow> G\\<turnstile>S\\<preceq>PrimT pt"];
25.146 +
26.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
26.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Nov 11 12:23:45 1999 +0100
26.3 @@ -0,0 +1,76 @@
26.4 +(* Title: HOL/MicroJava/J/TypeRel.thy
26.5 + ID: $Id$
26.6 + Author: David von Oheimb
26.7 + Copyright 1999 Technische Universitaet Muenchen
26.8 +
26.9 +The relations between Java types
26.10 +*)
26.11 +
26.12 +TypeRel = Prog +
26.13 +
26.14 +consts
26.15 + subcls1 :: "'c prog \\<Rightarrow> (cname \\<times> cname) set" (* subclass *)
26.16 + widen, (* widening *)
26.17 + cast :: "'c prog \\<Rightarrow> (ty \\<times> ty) set" (* casting *)
26.18 +
26.19 +syntax
26.20 + subcls1 :: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C1_" [71,71,71] 70)
26.21 + subcls :: "'c prog \\<Rightarrow> [cname, cname] \\<Rightarrow> bool" ("_\\<turnstile>_\\<prec>C _" [71,71,71] 70)
26.22 + widen :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<preceq>_" [71,71,71] 70)
26.23 + cast :: "'c prog \\<Rightarrow> [ty, ty] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Rightarrow>? _"[71,71,71] 70)
26.24 +
26.25 +translations
26.26 + "G\\<turnstile>C \\<prec>C1 D" == "(C,D) \\<in> subcls1 G"
26.27 + "G\\<turnstile>C \\<prec>C D" == "(C,D) \\<in> (subcls1 G)^+"
26.28 + "G\\<turnstile>S \\<preceq> T" == "(S,T) \\<in> widen G"
26.29 + "G\\<turnstile>S \\<Rightarrow>? T" == "(S,T) \\<in> cast G"
26.30 +
26.31 +defs
26.32 +
26.33 + (* direct subclass, cf. 8.1.3 *)
26.34 + subcls1_def "subcls1 G \\<equiv> {(C,D). \\<exists>c. class G C = Some c \\<and> fst c = Some D}"
26.35 +
26.36 +consts
26.37 +
26.38 + cmethd :: "'c prog \\<times> cname \\<Rightarrow> ( sig \\<leadsto> cname \\<times> ty \\<times> 'c)"
26.39 + cfield :: "'c prog \\<times> cname \\<Rightarrow> ( vname \\<leadsto> cname \\<times> ty)"
26.40 + fields :: "'c prog \\<times> cname \\<Rightarrow> ((vname \\<times> cname) \\<times> ty) list"
26.41 +
26.42 +constdefs (* auxiliary relations for recursive definitions below *)
26.43 +
26.44 + subcls1_rel :: "(('c prog \\<times> cname) \\<times> ('c prog \\<times> cname)) set"
26.45 + "subcls1_rel \\<equiv> {((G,C),(G',C')). G = G' \\<and> wf ((subcls1 G)^-1) \\<and> G\\<turnstile>C'\\<prec>C1C}"
26.46 +
26.47 +(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
26.48 +recdef cmethd "subcls1_rel"
26.49 + "cmethd (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> empty
26.50 + | Some (sc,fs,ms) \\<Rightarrow> (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow>
26.51 + if is_class G D then cmethd (G,D)
26.52 + else arbitrary) \\<oplus>
26.53 + map_of (map (\\<lambda>(s, m ).
26.54 + (s,(C,m))) ms))
26.55 + else arbitrary)"
26.56 +
26.57 +(* list of fields of a class, including inherited and hidden ones *)
26.58 +recdef fields "subcls1_rel"
26.59 + "fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None \\<Rightarrow> arbitrary
26.60 + | Some (sc,fs,ms) \\<Rightarrow> map (\\<lambda>(fn,ft). ((fn,C),ft)) fs@
26.61 + (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow>
26.62 + if is_class G D then fields (G,D)
26.63 + else arbitrary))
26.64 + else arbitrary)"
26.65 +defs
26.66 +
26.67 + cfield_def "cfield \\<equiv> map_of o (map (\\<lambda>((fn,fd),ft). (fn,(fd,ft)))) o fields"
26.68 +
26.69 +inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
26.70 + i.e. sort of syntactic subtyping *)
26.71 + refl "G\\<turnstile> T \\<preceq> T" (* identity conv., cf. 5.1.1 *)
26.72 + subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class C \\<preceq> Class D"
26.73 + null "G\\<turnstile> NT \\<preceq> RefT R"
26.74 +
26.75 +inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
26.76 + widen "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> G\\<turnstile> S \\<Rightarrow>? T"
26.77 + subcls "G\\<turnstile>C\\<prec>C D \\<Longrightarrow> G\\<turnstile>Class D \\<Rightarrow>? Class C"
26.78 +
26.79 +end
27.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
27.2 +++ b/src/HOL/MicroJava/J/WellForm.ML Thu Nov 11 12:23:45 1999 +0100
27.3 @@ -0,0 +1,388 @@
27.4 +(* Title: HOL/MicroJava/J/WellForm.ML
27.5 + ID: $Id$
27.6 + Author: David von Oheimb
27.7 + Copyright 1999 Technische Universitaet Muenchen
27.8 +*)
27.9 +
27.10 +val class_wf = prove_goalw thy [wf_prog_def, Let_def, class_def]
27.11 + "\\<And>X. \\<lbrakk>class G C = Some c; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> wf_cdecl wtm G (C,c)" (K [
27.12 + Asm_full_simp_tac 1,
27.13 + fast_tac (set_cs addDs [get_in_set]) 1]);
27.14 +
27.15 +val class_Object = prove_goalw thy [wf_prog_def, Let_def, ObjectC_def,class_def]
27.16 + "\\<And>X. wf_prog wtm G \\<Longrightarrow> class G Object = Some (None, [], [])" (K [
27.17 + safe_tac set_cs,
27.18 + dtac in_set_get 1,
27.19 + Auto_tac]);
27.20 +Addsimps [class_Object];
27.21 +
27.22 +val is_class_Object = prove_goalw thy [is_class_def]
27.23 + "\\<And>X. wf_prog wtm G \\<Longrightarrow> is_class G Object" (K [Asm_simp_tac 1]);
27.24 +Addsimps [is_class_Object];
27.25 +
27.26 +Goal "\\<lbrakk>G\\<turnstile>C\\<prec>C1D; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> D \\<noteq> C \\<and> \\<not> G\\<turnstile>D\\<prec>C C";
27.27 +by( forward_tac [r_into_trancl] 1);
27.28 +by( dtac subcls1D 1);
27.29 +by( strip_tac1 1);
27.30 +by( dtac class_wf 1);
27.31 +by( atac 1);
27.32 +by( rewtac wf_cdecl_def);
27.33 +by( Clarsimp_tac 1);
27.34 +qed "subcls1_wfD";
27.35 +
27.36 +val wf_cdecl_supD = prove_goalw thy [wf_cdecl_def]
27.37 +"\\<And>X. \\<lbrakk>wf_cdecl wtm G (C, sc, r); C \\<noteq> Object\\<rbrakk> \\<Longrightarrow> \\<exists>D. sc = Some D \\<and> is_class G D" (K [
27.38 + pair_tac "r" 1,
27.39 + Asm_full_simp_tac 1,
27.40 + strip_tac1 1,
27.41 + option_case_tac 1,
27.42 + Fast_tac 1]);
27.43 +
27.44 +local
27.45 +val lemma = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C=Object \\<longrightarrow> R" (K [
27.46 + etac trancl_trans_induct 1,
27.47 + atac 2,
27.48 + rewtac subcls1_def,
27.49 + Auto_tac]);
27.50 +in
27.51 +val subcls_Object = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>Object\\<prec>C C\\<rbrakk> \\<Longrightarrow> R" (K [
27.52 + etac (lemma RS mp) 1,
27.53 + Auto_tac]);
27.54 +end;
27.55 +
27.56 +Goal "\\<lbrakk>wf_prog wt G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> \\<not> G\\<turnstile>D\\<prec>C C";
27.57 +by(etac tranclE 1);
27.58 +by(ALLGOALS(fast_tac (HOL_cs addSDs [subcls1_wfD] addIs [trancl_trans])));
27.59 +qed "subcls_asym";
27.60 +
27.61 +val subcls_irrefl = prove_goal thy "\\<And>X. \\<lbrakk>wf_prog wtm G; G\\<turnstile>C\\<prec>C D\\<rbrakk> \\<Longrightarrow> C \\<noteq> D" (K [
27.62 + etac trancl_trans_induct 1,
27.63 + fast_tac (HOL_cs addDs [subcls1_wfD]) 1,
27.64 + fast_tac (HOL_cs addDs [subcls_asym]) 1]);
27.65 +
27.66 +val acyclic_subcls1 = prove_goalw thy [acyclic_def]
27.67 + "\\<And>X. wf_prog wt G \\<Longrightarrow> acyclic (subcls1 G)" (K [
27.68 + strip_tac1 1,
27.69 + fast_tac (HOL_cs addDs [subcls_irrefl]) 1]);
27.70 +
27.71 +val wf_subcls1 = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> wf ((subcls1 G)^-1)" (K [
27.72 + rtac finite_acyclic_wf 1,
27.73 + stac finite_converse 1,
27.74 + rtac finite_subcls1 1,
27.75 + stac acyclic_converse 1,
27.76 + etac acyclic_subcls1 1]);
27.77 +
27.78 +
27.79 +val major::prems = goal thy
27.80 + "\\<lbrakk>wf_prog wt G; \\<And>C. \\<forall>D. G\\<turnstile>C\\<prec>C D \\<longrightarrow> P D \\<Longrightarrow> P C\\<rbrakk> \\<Longrightarrow> P C";
27.81 +by(cut_facts_tac [major RS wf_subcls1] 1);
27.82 +by(dtac wf_trancl 1);
27.83 +by(asm_full_simp_tac (HOL_ss addsimps [trancl_converse]) 1);
27.84 +by(eres_inst_tac [("a","C")] wf_induct 1);
27.85 +by(resolve_tac prems 1);
27.86 +by(Auto_tac);
27.87 +qed "subcls_induct";
27.88 +
27.89 +val prems = goal thy "\\<lbrakk>is_class G C; wf_prog wtm G; P Object; \
27.90 +\\\<And>C D fs ms. \\<lbrakk>C \\<noteq> Object; is_class G C; class G C = Some (Some D,fs,ms) \\<and> \
27.91 +\ wf_cdecl wtm G (C, Some D,fs,ms) \\<and> G\\<turnstile>C\\<prec>C1D \\<and> is_class G D \\<and> P D\\<rbrakk> \\<Longrightarrow> P C\
27.92 +\ \\<rbrakk> \\<Longrightarrow> P C";
27.93 +by( cut_facts_tac prems 1);
27.94 +by( rtac impE 1);
27.95 +by( atac 2);
27.96 +by( atac 2);
27.97 +by( etac thin_rl 1);
27.98 +by( rtac subcls_induct 1);
27.99 +by( atac 1);
27.100 +by( rtac impI 1);
27.101 +by( case_tac "C = Object" 1);
27.102 +by( Fast_tac 1);
27.103 +by( ex_ftac is_classD 1);
27.104 +by( forward_tac [class_wf] 1);
27.105 +by( atac 1);
27.106 +by( forward_tac [wf_cdecl_supD] 1);
27.107 +by( atac 1);
27.108 +by( strip_tac1 1);
27.109 +by( rtac (hd (tl (tl (tl prems)))) 1);
27.110 +by( atac 1);
27.111 +by( atac 1);
27.112 +by( subgoal_tac "G\\<turnstile>C\\<prec>C1D" 1);
27.113 +by( fast_tac (HOL_cs addIs [r_into_trancl]) 1);
27.114 +by( etac subcls1I 1);
27.115 +qed "subcls1_induct";
27.116 +
27.117 +Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) = \
27.118 +\ (case class G C of None \\<Rightarrow> empty | Some (sc,fs,ms) \\<Rightarrow> \
27.119 +\ (case sc of None \\<Rightarrow> empty | Some D \\<Rightarrow> cmethd (G,D)) \\<oplus> \
27.120 +\ map_of (map (\\<lambda>(s,m). (s,(C,m))) ms))";
27.121 +by( stac (cmethd_TC RS (wf_subcls1_rel RS (hd cmethd.rules))) 1);
27.122 +by( clarsimp_tac (claset(), simpset() addsimps [wf_subcls1,empty_def]
27.123 + addsplits [option.split]) 1);
27.124 +by( case_tac "C = Object" 1);
27.125 +by( Asm_full_simp_tac 1);
27.126 +by( dtac class_wf 1);
27.127 +by( atac 1);
27.128 +by( dtac wf_cdecl_supD 1);
27.129 +by( atac 1);
27.130 +by( Asm_full_simp_tac 1);
27.131 +val cmethd_rec = result();
27.132 +
27.133 +Goal "\\<lbrakk>class G C = Some (sc,fs,ms); wf_prog wtm G\\<rbrakk> \\<Longrightarrow> fields (G,C) = \
27.134 +\ map (\\<lambda>(fn,ft). ((fn,C),ft)) fs @ \
27.135 +\ (case sc of None \\<Rightarrow> [] | Some D \\<Rightarrow> fields (G,D))";
27.136 +by( stac (fields_TC RS (wf_subcls1_rel RS (hd fields.rules))) 1);
27.137 +by( asm_simp_tac (simpset() addsimps [wf_subcls1,empty_def]) 1);
27.138 +by( option_case_tac2 "sc" 1);
27.139 +by( Asm_simp_tac 1);
27.140 +by( case_tac "C = Object" 1);
27.141 +by( rotate_tac 2 1);
27.142 +by( Asm_full_simp_tac 1);
27.143 +by( dtac class_wf 1);
27.144 +by( atac 1);
27.145 +by( dtac wf_cdecl_supD 1);
27.146 +by( atac 1);
27.147 +by( Asm_full_simp_tac 1);
27.148 +val fields_rec = result();
27.149 +
27.150 +val cmethd_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> cmethd (G,Object) = empty"
27.151 + (K [stac cmethd_rec 1,Auto_tac]);
27.152 +val fields_Object = prove_goal thy "\\<And>X. wf_prog wtm G \\<Longrightarrow> fields (G,Object) = []"(K [
27.153 + stac fields_rec 1,Auto_tac]);
27.154 +Addsimps [cmethd_Object, fields_Object];
27.155 +val cfield_Object = prove_goalw thy [cfield_def]
27.156 + "\\<And>X. wf_prog wtm G \\<Longrightarrow> cfield (G,Object) = empty" (K [Asm_simp_tac 1]);
27.157 +Addsimps [cfield_Object];
27.158 +
27.159 +val subcls_C_Object = prove_goal thy
27.160 + "\\<And>X. \\<lbrakk>is_class G C; wf_prog wtm G \\<rbrakk> \\<Longrightarrow> C \\<noteq> Object \\<longrightarrow> G\\<turnstile>C\\<prec>C Object" (K [
27.161 + etac subcls1_induct 1,
27.162 + atac 1,
27.163 + Fast_tac 1,
27.164 + safe_tac (HOL_cs addSDs [wf_cdecl_supD] addss (simpset())),
27.165 + fast_tac (HOL_cs addIs [r_into_trancl]) 1,
27.166 + rtac trancl_trans 1,
27.167 + atac 2,
27.168 + rtac r_into_trancl 1,
27.169 + rtac subcls1I 1,
27.170 + ALLGOALS Asm_simp_tac]) RS mp;
27.171 +
27.172 +val is_type_rTI = prove_goalw thy [wf_mhead_def]
27.173 + "\\<And>sig. wf_mhead G sig rT \\<Longrightarrow> is_type G rT"
27.174 + (K [split_all_tac 1, Auto_tac]);
27.175 +
27.176 +val widen_Class_Object = prove_goal thy
27.177 + "\\<lbrakk>wf_prog wtm G; is_class G C\\<rbrakk> \\<Longrightarrow> G\\<turnstile>Class C\\<preceq>Class Object" (fn prems => [
27.178 + cut_facts_tac prems 1,
27.179 + case_tac "C=Object" 1,
27.180 + hyp_subst_tac 1,
27.181 + Asm_simp_tac 1,
27.182 + rtac widen.subcls 1,
27.183 + fast_tac (HOL_cs addEs [subcls_C_Object]) 1]);
27.184 +
27.185 +val widen_trans = prove_goal thy "\\<lbrakk>wf_prog wtm G; G\\<turnstile>S\\<preceq>U; G\\<turnstile>U\\<preceq>T\\<rbrakk> \\<Longrightarrow> G\\<turnstile>S\\<preceq>T"
27.186 +(fn prems=> [cut_facts_tac prems 1,
27.187 + fast_tac (HOL_cs addEs [widen_trans_lemma, widen_Class_Object,
27.188 + subcls_Object]) 1]);
27.189 +
27.190 +val fields_mono = prove_goal thy
27.191 +"\\<And>X. \\<lbrakk>G\\<turnstile>C'\\<prec>C C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
27.192 +\ x \\<in> set (fields (G,C)) \\<longrightarrow> x \\<in> set (fields (G,C'))" (K [
27.193 + etac trancl_trans_induct 1,
27.194 + safe_tac (HOL_cs addSDs [subcls1D]),
27.195 + stac fields_rec 1,
27.196 + Auto_tac]) RS mp;
27.197 +
27.198 +Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
27.199 +\ \\<forall>((fn,fd),fT)\\<in>set (fields (G,C)). G\\<turnstile>Class C\\<preceq>Class fd";
27.200 +by( etac subcls1_induct 1);
27.201 +by( atac 1);
27.202 +by( Asm_simp_tac 1);
27.203 +by( safe_tac HOL_cs);
27.204 +by( stac fields_rec 1);
27.205 +by( atac 1);
27.206 +by( atac 1);
27.207 +by( Simp_tac 1);
27.208 +by( rtac ballI 1);
27.209 +by( split_all_tac 1);
27.210 +by( Simp_tac 1);
27.211 +by( etac UnE 1);
27.212 +by( dtac split_Pair_eq 1);
27.213 +by( SELECT_GOAL (Auto_tac) 1);
27.214 +by( rtac widen_trans 1);
27.215 +by( atac 1);
27.216 +by( etac (r_into_trancl RS widen.subcls) 1);
27.217 +by( etac BallE 1);
27.218 +by( contr_tac 1);
27.219 +by( Asm_full_simp_tac 1);
27.220 +val widen_fields_defpl' = result();
27.221 +
27.222 +Goal "\\<lbrakk>is_class G C; wf_prog wtm G; ((fn,fd),fT) \\<in> set (fields (G,C))\\<rbrakk> \\<Longrightarrow> \
27.223 +\ G\\<turnstile>Class C\\<preceq>Class fd";
27.224 +by( dtac widen_fields_defpl' 1);
27.225 +by( atac 1);
27.226 +(*###################*)
27.227 +by( dtac bspec 1);
27.228 +auto();
27.229 +val widen_fields_defpl = result();
27.230 +
27.231 +
27.232 +Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> unique (fields (G,C))";
27.233 +by( etac subcls1_induct 1);
27.234 +by( atac 1);
27.235 +by( safe_tac (HOL_cs addSDs [wf_cdecl_supD]));
27.236 +by( Asm_simp_tac 1);
27.237 +by( dtac subcls1_wfD 1);
27.238 +by( atac 1);
27.239 +by( stac fields_rec 1);
27.240 +by Auto_tac;
27.241 +by( rotate_tac ~1 1);
27.242 +by( ex_ftac is_classD 1);
27.243 +by( forward_tac [class_wf] 1);
27.244 +by Auto_tac;
27.245 +by( asm_full_simp_tac (simpset() addsimps [wf_cdecl_def]) 1);
27.246 +by( etac unique_append 1);
27.247 +by( rtac unique_map_Pair 1);
27.248 +by( Step_tac 1);
27.249 +by (EVERY1[dtac widen_fields_defpl, atac, atac]);
27.250 +by( Asm_full_simp_tac 1);
27.251 +by( dtac split_Pair_eq 1);
27.252 +by( fast_tac (HOL_cs addSDs [widen_Class_Class]) 1);
27.253 +val unique_fields = result();
27.254 +
27.255 +Goal
27.256 +"\\<lbrakk>wf_prog wtm G; G\\<turnstile>Class C'\\<preceq>Class C; map_of(fields (G,C )) f = Some ft\\<rbrakk> \\<Longrightarrow> \
27.257 +\ map_of (fields (G,C')) f = Some ft";
27.258 +by( dtac widen_Class_Class 1);
27.259 +by( etac disjE 1);
27.260 +by( Asm_simp_tac 1);
27.261 +by( rtac table_mono 1);
27.262 +by( atac 3);
27.263 +by( rtac unique_fields 1);
27.264 +by( etac subcls_is_class 1);
27.265 +by( atac 1);
27.266 +by( fast_tac (HOL_cs addEs [fields_mono]) 1);
27.267 +val widen_fields_mono = result();
27.268 +
27.269 +
27.270 +val cfs_fields_lemma = prove_goalw thy [cfield_def]
27.271 +"\\<And>X. cfield (G,C) fn = Some (fd, fT) \\<Longrightarrow> map_of(fields (G,C)) (fn, fd) = Some fT"
27.272 +(K [rtac table_map_Some 1, Asm_full_simp_tac 1]);
27.273 +
27.274 +val widen_cfs_fields = prove_goal thy "\\<And>X. \\<lbrakk>cfield (G,C) fn = Some (fd, fT);\
27.275 +\ G\\<turnstile>Class C'\\<preceq>Class C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> map_of (fields (G,C')) (fn, fd) = Some fT" (K[
27.276 +fast_tac (HOL_cs addIs [widen_fields_mono, cfs_fields_lemma]) 1]);
27.277 +
27.278 +Goal "wf_prog wtm G \\<Longrightarrow> cmethd (G,C) sig = Some (md,mh,m)\
27.279 +\ \\<longrightarrow> G\\<turnstile>Class C\\<preceq>Class md \\<and> wf_mdecl wtm G md (sig,(mh,m))";
27.280 +by( case_tac "is_class G C" 1);
27.281 +by( forw_inst_tac [("C","C")] cmethd_rec 2);
27.282 +by( asm_full_simp_tac (simpset() addsimps [is_class_def]
27.283 + delsimps [not_None_eq]) 2);
27.284 +by( etac subcls1_induct 1);
27.285 +by( atac 1);
27.286 +by( Force_tac 1);
27.287 +by( forw_inst_tac [("C","C")] cmethd_rec 1);
27.288 +by( strip_tac1 1);
27.289 +by( rotate_tac ~1 1);
27.290 +by( Asm_full_simp_tac 1);
27.291 +by( dtac override_SomeD 1);
27.292 +by( etac disjE 1);
27.293 +by( thin_tac "?P \\<longrightarrow> ?Q" 1);
27.294 +by( Clarify_tac 2);
27.295 +by( rtac widen_trans 2);
27.296 +by( atac 2);
27.297 +by( atac 3);
27.298 +by( rtac widen.subcls 2);
27.299 +by( rtac r_into_trancl 2);
27.300 +by( fast_tac (HOL_cs addIs [subcls1I]) 2);
27.301 +by( forward_tac [table_mapf_SomeD] 1);
27.302 +by( strip_tac1 1);
27.303 +by( Asm_full_simp_tac 1);
27.304 +by( rewtac wf_cdecl_def);
27.305 +by( Asm_full_simp_tac 1);
27.306 +val cmethd_wf_mdecl = result() RS mp;
27.307 +
27.308 +Goal "\\<lbrakk>G\\<turnstile>T\\<prec>C T'; wf_prog wt G\\<rbrakk> \\<Longrightarrow> \
27.309 +\ \\<forall>D rT b. cmethd (G,T') sig = Some (D,rT ,b) \\<longrightarrow>\
27.310 +\ (\\<exists>D' rT' b'. cmethd (G,T) sig = Some (D',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT)";
27.311 +by( etac trancl_trans_induct 1);
27.312 +by( strip_tac1 2);
27.313 +by( EVERY[dtac spec 2, dtac spec 2, dtac spec 2, mp_tac 2]);
27.314 +by( fast_tac (HOL_cs addEs [widen_trans]) 2);
27.315 +by( strip_tac1 1);
27.316 +by( dtac subcls1D 1);
27.317 +by( strip_tac1 1);
27.318 +by( stac cmethd_rec 1);
27.319 +by( atac 1);
27.320 +by( rewtac override_def);
27.321 +by( asm_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
27.322 +by( case_tac "\\<exists>z. map_of(map (\\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z" 1);
27.323 +by( etac exE 1);
27.324 +by( asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 2);
27.325 +by( ALLGOALS (rotate_tac ~1 THEN' forward_tac[ssubst] THEN' (fn n=>atac(n+1))));
27.326 +by( ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex])));
27.327 +by( dtac class_wf 1);
27.328 +by( atac 1);
27.329 +by( split_all_tac 1);
27.330 +by( rewtac wf_cdecl_def);
27.331 +by( dtac table_mapf_Some2 1);
27.332 +by( Clarsimp_tac 1);
27.333 +by( dres_inst_tac [("xys1","ms")] get_in_set 1);
27.334 +by Auto_tac;
27.335 +qed_spec_mp "subcls_widen_methd";
27.336 +
27.337 +
27.338 +Goal
27.339 + "\\<lbrakk> G\\<turnstile>Class C\\<preceq>Class D; wf_prog wt G; \
27.340 +\ cmethd (G,D) sig = Some (md, rT, b) \\<rbrakk> \
27.341 +\ \\<Longrightarrow> \\<exists>mD' rT' b'. cmethd (G,C) sig= Some(mD',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
27.342 +by(auto_tac (claset() addSDs [widen_Class_Class]
27.343 + addDs [subcls_widen_methd,cmethd_wf_mdecl],
27.344 + simpset() addsimps [wf_mdecl_def,wf_mhead_def,split_def]));
27.345 +qed "subtype_widen_methd";
27.346 +
27.347 +
27.348 +Goal "wf_prog wt G \\<Longrightarrow> \\<forall>D. cmethd (G,C) sig = Some(D,mh,code) \\<longrightarrow> is_class G D \\<and> cmethd (G,D) sig = Some(D,mh,code)";
27.349 +by( case_tac "is_class G C" 1);
27.350 +by( forw_inst_tac [("C","C")] cmethd_rec 2);
27.351 +by( asm_full_simp_tac (simpset() addsimps [is_class_def]
27.352 + delsimps [not_None_eq]) 2);
27.353 +by (etac subcls1_induct 1);
27.354 + ba 1;
27.355 + by (Asm_full_simp_tac 1);
27.356 +by (stac cmethd_rec 1);
27.357 + ba 1;
27.358 +by (Clarify_tac 1);
27.359 +by (eres_inst_tac [("x","Da")] allE 1);
27.360 +by (Clarsimp_tac 1);
27.361 + by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
27.362 + by (Clarify_tac 1);
27.363 + by (stac cmethd_rec 1);
27.364 + ba 1;
27.365 + by (asm_full_simp_tac (simpset() addsimps [override_def,map_of_map] addsplits [option.split]) 1);
27.366 +qed_spec_mp "cmethd_in_md";
27.367 +
27.368 +writeln"OK";
27.369 +
27.370 +Goal "\\<lbrakk>is_class G C; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
27.371 +\ \\<forall>f\\<in>set (fields (G,C)). is_type G (snd f)";
27.372 +by( etac subcls1_induct 1);
27.373 +by( atac 1);
27.374 +by( Asm_simp_tac 1);
27.375 +by( strip_tac1 1);
27.376 +by( stac fields_rec 1);
27.377 +by( atac 1);
27.378 +by( atac 1);
27.379 +by( Asm_simp_tac 1);
27.380 +by( safe_tac set_cs);
27.381 +by( Fast_tac 2);
27.382 +by( dtac class_wf 1);
27.383 +by( atac 1);
27.384 +by( rewtac wf_cdecl_def);
27.385 +by( Asm_full_simp_tac 1);
27.386 +by( strip_tac1 1);
27.387 +by( EVERY[dtac bspec 1, atac 1]);
27.388 +by( rewtac wf_fdecl_def);
27.389 +by( split_all_tac 1);
27.390 +by( Asm_full_simp_tac 1);
27.391 +val is_type_fields = result() RS bspec;
28.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
28.2 +++ b/src/HOL/MicroJava/J/WellForm.thy Thu Nov 11 12:23:45 1999 +0100
28.3 @@ -0,0 +1,47 @@
28.4 +(* Title: HOL/MicroJava/J/WellForm.thy
28.5 + ID: $Id$
28.6 + Author: David von Oheimb
28.7 + Copyright 1999 Technische Universitaet Muenchen
28.8 +
28.9 +Well-formedness of Java programs
28.10 +for static checks on expressions and statements, see WellType.thy
28.11 +
28.12 +improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
28.13 +* a method implementing or overwriting another method may have a result type
28.14 + that widens to the result type of the other method (instead of identical type)
28.15 +
28.16 +simplifications:
28.17 +* for uniformity, Object is assumed to be declared like any other class
28.18 +*)
28.19 +
28.20 +WellForm = TypeRel +
28.21 +
28.22 +types 'c wtm = 'c prog => cname => 'c mdecl => bool
28.23 +
28.24 +constdefs
28.25 +
28.26 + wf_fdecl :: "'c prog \\<Rightarrow> fdecl \\<Rightarrow> bool"
28.27 +"wf_fdecl G \\<equiv> \\<lambda>(fn,ft). is_type G ft"
28.28 +
28.29 + wf_mhead :: "'c prog \\<Rightarrow> sig \\<Rightarrow> ty \\<Rightarrow> bool"
28.30 +"wf_mhead G \\<equiv> \\<lambda>(mn,pTs) rT. (\\<forall>T\\<in>set pTs. is_type G T) \\<and> is_type G rT"
28.31 +
28.32 + wf_mdecl :: "'c wtm \\<Rightarrow> 'c wtm"
28.33 +"wf_mdecl wtm G C \\<equiv> \\<lambda>(sig,rT,mb). wf_mhead G sig rT \\<and> wtm G C (sig,rT,mb)"
28.34 +
28.35 + wf_cdecl :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> 'c cdecl \\<Rightarrow> bool"
28.36 +"wf_cdecl wtm G \\<equiv>
28.37 + \\<lambda>(C,(sc,fs,ms)).
28.38 + (\\<forall>f\\<in>set fs. wf_fdecl G f ) \\<and> unique fs \\<and>
28.39 + (\\<forall>m\\<in>set ms. wf_mdecl wtm G C m) \\<and> unique ms \\<and>
28.40 + (case sc of None \\<Rightarrow> C = Object
28.41 + | Some D \\<Rightarrow>
28.42 + is_class G D \\<and> \\<not> G\\<turnstile>D\\<prec>C C \\<and>
28.43 + (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'.
28.44 + cmethd(G,D) sig = Some(D',rT',b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
28.45 +
28.46 + wf_prog :: "'c wtm \\<Rightarrow> 'c prog \\<Rightarrow> bool"
28.47 +"wf_prog wtm G \\<equiv>
28.48 + let cs = set G in ObjectC \\<in> cs \\<and> (\\<forall>c\\<in>cs. wf_cdecl wtm G c) \\<and> unique G"
28.49 +
28.50 +end
29.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
29.2 +++ b/src/HOL/MicroJava/J/WellType.ML Thu Nov 11 12:23:45 1999 +0100
29.3 @@ -0,0 +1,61 @@
29.4 +(* Title: HOL/MicroJava/J/WellType.ML
29.5 + ID: $Id$
29.6 + Author: David von Oheimb
29.7 + Copyright 1999 Technische Universitaet Muenchen
29.8 +*)
29.9 +
29.10 +Goalw [m_head_def]
29.11 +"\\<lbrakk> m_head G T sig = Some (md,rT); wf_prog wtm G; G\\<turnstile>Class T''\\<preceq>RefT T\\<rbrakk> \\<Longrightarrow> \
29.12 +\\\<exists>md' rT' b'. cmethd (G,T'') sig = Some (md',rT',b') \\<and> G\\<turnstile>rT'\\<preceq>rT";
29.13 +by( forward_tac [widen_Class_RefT] 1);
29.14 +by( etac exE 1);
29.15 +by( hyp_subst_tac 1);
29.16 +by( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
29.17 +by( rewtac option_map_def);
29.18 +by( strip_tac1 1);
29.19 +by( split_all_tac 1);
29.20 +by( dtac widen_Class_Class 1);
29.21 +by( etac disjE 1);
29.22 +by( hyp_subst_tac 1);
29.23 +by( asm_full_simp_tac (simpset() delsimps [split_paired_Ex]) 1);
29.24 +by( dtac subcls_widen_methd 1);
29.25 +by Auto_tac;
29.26 +qed "widen_methd";
29.27 +
29.28 +
29.29 +Goal
29.30 +"\\<lbrakk>m_head G T sig = Some (md,rT); G\\<turnstile>Class T''\\<preceq>RefT T; wf_prog wtm G\\<rbrakk> \\<Longrightarrow> \
29.31 +\ \\<exists>T' rT' b. cmethd (G,T'') sig = Some (T',rT',b) \\<and> \
29.32 +\ G\\<turnstile>rT'\\<preceq>rT \\<and> G\\<turnstile>Class T''\\<preceq>Class T' \\<and> wf_mhead G sig rT' \\<and> wtm G T' (sig,rT',b)";
29.33 +by( dtac widen_methd 1);
29.34 +by( atac 1);
29.35 +by( atac 1);
29.36 +by( Clarsimp_tac 1);
29.37 +by( dtac cmethd_wf_mdecl 1);
29.38 +by( atac 1);
29.39 +by( rewtac wf_mdecl_def);
29.40 +by Auto_tac;
29.41 +val Call_lemma = result();
29.42 +
29.43 +
29.44 +val m_head_Object = prove_goalw thy [m_head_def]
29.45 +"\\<And>x. wf_prog wtm G \\<Longrightarrow> m_head G (ClassT Object) sig = None" (K [Asm_simp_tac 1]);
29.46 +
29.47 +Addsimps [m_head_Object];
29.48 +
29.49 +val max_spec2appl_meths = prove_goalw thy [max_spec_def]
29.50 + "x \\<in> max_spec G rT sig \\<longrightarrow> x \\<in> appl_methds G rT sig"
29.51 + (fn _ => [Fast_tac 1]) RS mp;
29.52 +
29.53 +val appl_methsD = prove_goalw thy [appl_methds_def]
29.54 +"(mh,pTs')\\<in>appl_methds G rT (mn, pTs) \\<longrightarrow> \
29.55 +\ m_head G rT (mn, pTs') = Some mh \\<and> list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
29.56 + (K [Fast_tac 1]) RS mp;
29.57 +
29.58 +val is_type_typeof = prove_goal thy
29.59 + "(\\<forall>a. v \\<noteq> Addr a) \\<longrightarrow> (\\<exists>T. typeof t v = Some T \\<and> is_type G T)" (K [
29.60 + rtac val_.induct 1,
29.61 + Fast_tac 5,
29.62 + ALLGOALS Simp_tac]) RS mp;
29.63 +
29.64 +Addsimps [is_type_typeof];
30.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
30.2 +++ b/src/HOL/MicroJava/J/WellType.thy Thu Nov 11 12:23:45 1999 +0100
30.3 @@ -0,0 +1,184 @@
30.4 +(* Title: HOL/MicroJava/J/WellType.thy
30.5 + ID: $Id$
30.6 + Author: David von Oheimb
30.7 + Copyright 1999 Technische Universitaet Muenchen
30.8 +
30.9 +Well-typedness of Java programs
30.10 +
30.11 +the formulation of well-typedness of method calls given below (as well as
30.12 +the Java Specification 1.0) is a little too restrictive: Is does not allow
30.13 +methods of class Object to be called upon references of interface type.
30.14 +
30.15 +simplifications:
30.16 +* the type rules include all static checks on expressions and statements, e.g.
30.17 + definedness of names (of parameters, locals, fields, methods)
30.18 +
30.19 +*)
30.20 +
30.21 +WellType = Term + WellForm +
30.22 +
30.23 +types lenv (* local variables, including method parameters and This *)
30.24 + = "vname \\<leadsto> ty"
30.25 + 'c env
30.26 + = "'c prog \\<times> lenv"
30.27 +
30.28 +syntax
30.29 +
30.30 + prg :: "'c env \\<Rightarrow> 'c prog"
30.31 + localT :: "'c env \\<Rightarrow> (vname \\<leadsto> ty)"
30.32 +
30.33 +translations
30.34 +
30.35 + "prg" => "fst"
30.36 + "localT" => "snd"
30.37 +
30.38 +consts
30.39 +
30.40 + more_spec :: "'c prog \\<Rightarrow> (ty \\<times> 'x) \\<times> ty list \\<Rightarrow>
30.41 + (ty \\<times> 'x) \\<times> ty list \\<Rightarrow> bool"
30.42 + m_head :: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> sig \\<Rightarrow> (ty \\<times> ty) option"
30.43 + appl_methds :: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
30.44 + max_spec :: "'c prog \\<Rightarrow> ref_ty \\<Rightarrow> sig \\<Rightarrow> ((ty \\<times> ty) \\<times> ty list) set"
30.45 +
30.46 +defs
30.47 +
30.48 + m_head_def "m_head G t sig \\<equiv> case t of NullT \\<Rightarrow> None | ClassT C \\<Rightarrow>
30.49 + option_map (\\<lambda>(md,(rT,mb)). (Class md,rT)) (cmethd (G,C) sig)"
30.50 +
30.51 + more_spec_def "more_spec G \\<equiv> \\<lambda>((d,h),pTs). \\<lambda>((d',h'),pTs'). G\\<turnstile>d\\<preceq>d' \\<and>
30.52 + list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'"
30.53 +
30.54 + (* applicable methods, cf. 15.11.2.1 *)
30.55 + appl_methds_def "appl_methds G T \\<equiv> \\<lambda>(mn, pTs). {(mh,pTs') |mh pTs'.
30.56 + m_head G T (mn, pTs') = Some mh \\<and>
30.57 + list_all2 (\\<lambda>T T'. G\\<turnstile>T\\<preceq>T') pTs pTs'}"
30.58 +
30.59 + (* maximally specific methods, cf. 15.11.2.2 *)
30.60 + max_spec_def "max_spec G rT sig \\<equiv> {m. m \\<in>appl_methds G rT sig \\<and>
30.61 + (\\<forall>m'\\<in>appl_methds G rT sig.
30.62 + more_spec G m' m \\<longrightarrow> m' = m)}"
30.63 +consts
30.64 +
30.65 + typeof :: "(loc \\<Rightarrow> ty option) \\<Rightarrow> val \\<Rightarrow> ty option"
30.66 +
30.67 +primrec
30.68 + "typeof dt Unit = Some (PrimT Void)"
30.69 + "typeof dt Null = Some NT"
30.70 + "typeof dt (Bool b) = Some (PrimT Boolean)"
30.71 + "typeof dt (Intg i) = Some (PrimT Integer)"
30.72 + "typeof dt (Addr a) = dt a"
30.73 +
30.74 +types
30.75 + javam = "vname list \\<times> (vname \\<times> ty) list \\<times> stmt \\<times> expr"
30.76 + (* method body with parameter names, local variables, block, result expression *)
30.77 +
30.78 +consts
30.79 +
30.80 + ty_expr :: "javam env \\<Rightarrow> (expr \\<times> ty ) set"
30.81 + ty_exprs:: "javam env \\<Rightarrow> (expr list \\<times> ty list) set"
30.82 + wt_stmt :: "javam env \\<Rightarrow> stmt set"
30.83 +
30.84 +syntax
30.85 +
30.86 +ty_expr :: "javam env \\<Rightarrow> [expr , ty ] \\<Rightarrow> bool" ("_\\<turnstile>_\\<Colon>_" [51,51,51]50)
30.87 +ty_exprs:: "javam env \\<Rightarrow> [expr list, ty list] \\<Rightarrow> bool" ("_\\<turnstile>_[\\<Colon>]_"[51,51,51]50)
30.88 +wt_stmt :: "javam env \\<Rightarrow> stmt \\<Rightarrow> bool" ("_\\<turnstile>_ \\<surd>" [51,51 ]50)
30.89 +
30.90 +translations
30.91 + "E\\<turnstile>e \\<Colon> T" == "(e,T) \\<in> ty_expr E"
30.92 + "E\\<turnstile>e[\\<Colon>]T" == "(e,T) \\<in> ty_exprs E"
30.93 + "E\\<turnstile>c \\<surd>" == "c \\<in> wt_stmt E"
30.94 +
30.95 +inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intrs
30.96 +
30.97 +(* well-typed expressions *)
30.98 +
30.99 + (* cf. 15.8 *)
30.100 + NewC "\\<lbrakk>is_class (prg E) C\\<rbrakk> \\<Longrightarrow>
30.101 + E\\<turnstile>NewC C\\<Colon>Class C"
30.102 +
30.103 + (* cf. 15.15 *)
30.104 + Cast "\\<lbrakk>E\\<turnstile>e\\<Colon>T;
30.105 + prg E\\<turnstile>T\\<Rightarrow>? T'\\<rbrakk> \\<Longrightarrow>
30.106 + E\\<turnstile>Cast T' e\\<Colon>T'"
30.107 +
30.108 + (* cf. 15.7.1 *)
30.109 + Lit "\\<lbrakk>typeof (\\<lambda>v. None) x = Some T\\<rbrakk> \\<Longrightarrow>
30.110 + E\\<turnstile>Lit x\\<Colon>T"
30.111 +
30.112 + (* cf. 15.13.1 *)
30.113 + LAcc "\\<lbrakk>localT E v = Some T; is_type (prg E) T\\<rbrakk> \\<Longrightarrow>
30.114 + E\\<turnstile>LAcc v\\<Colon>T"
30.115 +
30.116 + (* cf. 15.25, 15.25.1 *)
30.117 + LAss "\\<lbrakk>E\\<turnstile>LAcc v\\<Colon>T;
30.118 + E\\<turnstile>e\\<Colon>T';
30.119 + prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
30.120 + E\\<turnstile>v\\<Colon>=e\\<Colon>T'"
30.121 +
30.122 + (* cf. 15.10.1 *)
30.123 + FAcc "\\<lbrakk>E\\<turnstile>a\\<Colon>Class C;
30.124 + cfield (prg E,C) fn = Some (fd,fT)\\<rbrakk> \\<Longrightarrow>
30.125 + E\\<turnstile>{fd}a..fn\\<Colon>fT"
30.126 +
30.127 + (* cf. 15.25, 15.25.1 *)
30.128 + FAss "\\<lbrakk>E\\<turnstile>{fd}a..fn\\<Colon>T;
30.129 + E\\<turnstile>v \\<Colon>T';
30.130 + prg E\\<turnstile>T'\\<preceq>T\\<rbrakk> \\<Longrightarrow>
30.131 + E\\<turnstile>{fd}a..fn\\<in>=v\\<Colon>T'"
30.132 +
30.133 +
30.134 + (* cf. 15.11.1, 15.11.2, 15.11.3 *)
30.135 + Call "\\<lbrakk>E\\<turnstile>a\\<Colon>RefT t;
30.136 + E\\<turnstile>ps[\\<Colon>]pTs;
30.137 + max_spec (prg E) t (mn, pTs) = {((md,rT),pTs')}\\<rbrakk> \\<Longrightarrow>
30.138 + E\\<turnstile>a..mn({pTs'}ps)\\<Colon>rT"
30.139 +
30.140 +(* well-typed expression lists *)
30.141 +
30.142 + (* cf. 15.11.??? *)
30.143 + Nil "E\\<turnstile>[][\\<Colon>][]"
30.144 +
30.145 + (* cf. 15.11.??? *)
30.146 + Cons "\\<lbrakk>E\\<turnstile>e\\<Colon>T;
30.147 + E\\<turnstile>es[\\<Colon>]Ts\\<rbrakk> \\<Longrightarrow>
30.148 + E\\<turnstile>e#es[\\<Colon>]T#Ts"
30.149 +
30.150 +(* well-typed statements *)
30.151 +
30.152 + Skip "E\\<turnstile>Skip\\<surd>"
30.153 +
30.154 + Expr "\\<lbrakk>E\\<turnstile>e\\<Colon>T\\<rbrakk> \\<Longrightarrow>
30.155 + E\\<turnstile>Expr e\\<surd>"
30.156 +
30.157 + Comp "\\<lbrakk>E\\<turnstile>s1\\<surd>;
30.158 + E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
30.159 + E\\<turnstile>s1;; s2\\<surd>"
30.160 +
30.161 + (* cf. 14.8 *)
30.162 + Cond "\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
30.163 + E\\<turnstile>s1\\<surd>;
30.164 + E\\<turnstile>s2\\<surd>\\<rbrakk> \\<Longrightarrow>
30.165 + E\\<turnstile>If(e) s1 Else s2\\<surd>"
30.166 +
30.167 + (* cf. 14.10 *)
30.168 + Loop "\\<lbrakk>E\\<turnstile>e\\<Colon>PrimT Boolean;
30.169 + E\\<turnstile>s\\<surd>\\<rbrakk> \\<Longrightarrow>
30.170 + E\\<turnstile>While(e) s\\<surd>"
30.171 +
30.172 +constdefs
30.173 +
30.174 + wt_java_mdecl :: javam prog => cname => javam mdecl => bool
30.175 +"wt_java_mdecl G C \\<equiv> \\<lambda>((mn,pTs),rT,(pns,lvars,blk,res)).
30.176 + length pTs = length pns \\<and>
30.177 + nodups pns \\<and>
30.178 + unique lvars \\<and>
30.179 + (\\<forall>pn\\<in>set pns. map_of lvars pn = None) \\<and>
30.180 + (\\<forall>(vn,T)\\<in>set lvars. is_type G T) &
30.181 + (let E = (G,map_of lvars(pns[\\<mapsto>]pTs)(This\\<mapsto>Class C)) in
30.182 + E\\<turnstile>blk\\<surd> \\<and> (\\<exists>T. E\\<turnstile>res\\<Colon>T \\<and> G\\<turnstile>T\\<preceq>rT))"
30.183 +
30.184 + wf_java_prog :: javam prog => bool
30.185 +"wf_java_prog G \\<equiv> wf_prog wt_java_mdecl G"
30.186 +
30.187 +end
31.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
31.2 +++ b/src/HOL/MicroJava/JVM/Control.thy Thu Nov 11 12:23:45 1999 +0100
31.3 @@ -0,0 +1,26 @@
31.4 +(* Title: HOL/MicroJava/JVM/Control.thy
31.5 + ID: $Id$
31.6 + Author: Cornelia Pusch
31.7 + Copyright 1999 Technische Universitaet Muenchen
31.8 +
31.9 +(Un)conditional branch instructions
31.10 +*)
31.11 +
31.12 +Control = JVMState +
31.13 +
31.14 +datatype branch = Goto int
31.15 + | Ifcmpeq int (** Branch if int/ref comparison succeeds **)
31.16 +
31.17 +
31.18 +consts
31.19 + exec_br :: "[branch,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)"
31.20 +
31.21 +primrec
31.22 + "exec_br (Ifcmpeq i) stk pc =
31.23 + (let (val1,val2) = (hd stk, hd (tl stk));
31.24 + pc' = if val1 = val2 then nat(int pc+i) else pc+1
31.25 + in
31.26 + (tl (tl stk),pc'))"
31.27 + "exec_br (Goto i) stk pc = (stk, nat(int pc+i))"
31.28 +
31.29 +end
32.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
32.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy Thu Nov 11 12:23:45 1999 +0100
32.3 @@ -0,0 +1,72 @@
32.4 +(* Title: HOL/MicroJava/JVM/JVMExec.thy
32.5 + ID: $Id$
32.6 + Author: Cornelia Pusch
32.7 + Copyright 1999 Technische Universitaet Muenchen
32.8 +
32.9 +Execution of the JVM
32.10 +*)
32.11 +
32.12 +JVMExec = LoadAndStore + Object + Method + Opstack + Control +
32.13 +
32.14 +datatype
32.15 + instr = LS load_and_store
32.16 + | CO create_object
32.17 + | MO manipulate_object
32.18 + | CH check_object
32.19 + | MI meth_inv
32.20 + | MR
32.21 + | OS op_stack
32.22 + | BR branch
32.23 +
32.24 +types
32.25 + bytecode = instr list
32.26 + jvm_prog = "(nat \\<times> bytecode)prog"
32.27 +
32.28 +consts
32.29 + exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option"
32.30 +
32.31 +(** exec is not recursive. recdef is just used because for pattern matching **)
32.32 +recdef exec "{}"
32.33 + "exec (G, xp, hp, []) = None"
32.34 +
32.35 + "exec (G, None, hp, (stk,loc,cn,ml,pc)#frs) =
32.36 + Some (case snd(snd(snd(the(cmethd (G,cn) ml)))) ! pc of
32.37 + LS ins \\<Rightarrow> (let (stk',loc',pc') = exec_las ins stk loc pc
32.38 + in
32.39 + (None,hp,(stk',loc',cn,ml,pc')#frs))
32.40 +
32.41 + | CO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_co ins G hp stk pc
32.42 + in
32.43 + (xp',hp',(stk',loc,cn,ml,pc')#frs))
32.44 +
32.45 + | MO ins \\<Rightarrow> (let (xp',hp',stk',pc') = exec_mo ins hp stk pc
32.46 + in
32.47 + (xp',hp',(stk',loc,cn,ml,pc')#frs))
32.48 +
32.49 + | CH ins \\<Rightarrow> (let (xp',stk',pc') = exec_ch ins G hp stk pc
32.50 + in
32.51 + (xp',hp,(stk',loc,cn,ml,pc')#frs))
32.52 +
32.53 + | MI ins \\<Rightarrow> (let (xp',frs',stk',pc') = exec_mi ins G hp stk pc
32.54 + in
32.55 + (xp',hp,frs'@(stk',loc,cn,ml,pc')#frs))
32.56 +
32.57 + | MR \\<Rightarrow> (let frs' = exec_mr stk frs in
32.58 + (None,hp,frs'))
32.59 +
32.60 + | OS ins \\<Rightarrow> (let (stk',pc') = exec_os ins stk pc
32.61 + in
32.62 + (None,hp,(stk',loc,cn,ml,pc')#frs))
32.63 +
32.64 + | BR ins \\<Rightarrow> (let (stk',pc') = exec_br ins stk pc
32.65 + in
32.66 + (None,hp,(stk',loc,cn,ml,pc')#frs)))"
32.67 +
32.68 + "exec (G, Some xp, hp, f#frs) = Some (Some xp, hp, [])"
32.69 +
32.70 +
32.71 +constdefs
32.72 + exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool" ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60)
32.73 + "G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
32.74 +
32.75 +end
33.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
33.2 +++ b/src/HOL/MicroJava/JVM/JVMState.thy Thu Nov 11 12:23:45 1999 +0100
33.3 @@ -0,0 +1,61 @@
33.4 +(* Title: HOL/MicroJava/JVM/JVMState.thy
33.5 + ID: $Id$
33.6 + Author: Cornelia Pusch
33.7 + Copyright 1999 Technische Universitaet Muenchen
33.8 +
33.9 +State of the JVM
33.10 +*)
33.11 +
33.12 +JVMState = Store +
33.13 +
33.14 +
33.15 +(** frame stack **)
33.16 +
33.17 +types
33.18 + opstack = "val list"
33.19 + locvars = "val list"
33.20 + p_count = nat
33.21 +
33.22 + frame = "opstack \\<times>
33.23 + locvars \\<times>
33.24 + cname \\<times>
33.25 + sig \\<times>
33.26 + p_count"
33.27 +
33.28 + (* operand stack *)
33.29 + (* local variables *)
33.30 + (* name of def. class defined *)
33.31 + (* meth name+param_desc *)
33.32 + (* program counter within frame *)
33.33 +
33.34 +
33.35 +(** exceptions **)
33.36 +
33.37 +constdefs
33.38 + raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option"
33.39 +"raise_xcpt c x \\<equiv> (if c then Some x else None)"
33.40 +
33.41 + heap_update :: "[xcpt option,aheap,aheap] \\<Rightarrow> aheap"
33.42 +"heap_update xp hp' hp \\<equiv> if xp=None then hp' else hp"
33.43 +
33.44 + stk_update :: "[xcpt option,opstack,opstack] \\<Rightarrow> opstack"
33.45 +"stk_update xp stk' stk \\<equiv> if xp=None then stk' else stk"
33.46 +
33.47 + xcpt_update :: "[xcpt option,'a,'a] \\<Rightarrow> 'a"
33.48 +"xcpt_update xp y' y \\<equiv> if xp=None then y' else y"
33.49 +
33.50 +(** runtime state **)
33.51 +
33.52 +types
33.53 + jvm_state = "xcpt option \\<times>
33.54 + aheap \\<times>
33.55 + frame list"
33.56 +
33.57 +
33.58 +
33.59 +(** dynamic method lookup **)
33.60 +
33.61 +constdefs
33.62 + dyn_class :: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname"
33.63 +"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(cmethd(G,C) sig))"
33.64 +end
34.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
34.2 +++ b/src/HOL/MicroJava/JVM/LoadAndStore.thy Thu Nov 11 12:23:45 1999 +0100
34.3 @@ -0,0 +1,32 @@
34.4 +(* Title: HOL/MicroJava/JVM/LoadAndStore.thy
34.5 + ID: $Id$
34.6 + Author: Cornelia Pusch
34.7 + Copyright 1999 Technische Universitaet Muenchen
34.8 +
34.9 +Load and store instructions
34.10 +*)
34.11 +
34.12 +LoadAndStore = JVMState +
34.13 +
34.14 +(** load and store instructions transfer values between local variables
34.15 + and operand stack. Values must all be of the same size (or tagged) **)
34.16 +
34.17 +datatype load_and_store =
34.18 + Load nat (* load from local variable *)
34.19 +| Store nat (* store into local variable *)
34.20 +| Bipush int (* push int *)
34.21 +| Aconst_null (* push null *)
34.22 +
34.23 +
34.24 +consts
34.25 + exec_las :: "[load_and_store,opstack,locvars,p_count] \\<Rightarrow> (opstack \\<times> locvars \\<times> p_count)"
34.26 +primrec
34.27 + "exec_las (Load idx) stk vars pc = ((vars ! idx) # stk , vars , pc+1)"
34.28 +
34.29 + "exec_las (Store idx) stk vars pc = (tl stk , vars[idx:=hd stk] , pc+1)"
34.30 +
34.31 + "exec_las (Bipush ival) stk vars pc = (Intg ival # stk , vars , pc+1)"
34.32 +
34.33 + "exec_las Aconst_null stk vars pc = (Null # stk , vars , pc+1)"
34.34 +
34.35 +end
35.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
35.2 +++ b/src/HOL/MicroJava/JVM/Method.ML Thu Nov 11 12:23:45 1999 +0100
35.3 @@ -0,0 +1,7 @@
35.4 +(* Title: HOL/MicroJava/JVM/Method.ML
35.5 + ID: $Id$
35.6 + Author: Cornelia Pusch
35.7 + Copyright 1999 Technische Universitaet Muenchen
35.8 +*)
35.9 +
35.10 +Addsimps [exec_mr_def];
36.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
36.2 +++ b/src/HOL/MicroJava/JVM/Method.thy Thu Nov 11 12:23:45 1999 +0100
36.3 @@ -0,0 +1,41 @@
36.4 +(* Title: HOL/MicroJava/JVM/Method.thy
36.5 + ID: $Id$
36.6 + Author: Cornelia Pusch
36.7 + Copyright 1999 Technische Universitaet Muenchen
36.8 +
36.9 +Method invocation
36.10 +*)
36.11 +
36.12 +Method = JVMState +
36.13 +
36.14 +(** method invocation and return instructions **)
36.15 +
36.16 +datatype
36.17 + meth_inv =
36.18 + Invokevirtual mname (ty list) (** inv. instance meth of an object **)
36.19 +
36.20 +consts
36.21 + exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count]
36.22 + \\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)"
36.23 +primrec
36.24 + "exec_mi (Invokevirtual mn ps) G hp stk pc =
36.25 + (let n = length ps;
36.26 + argsoref = take (n+1) stk;
36.27 + oref = last argsoref;
36.28 + xp' = raise_xcpt (oref=Null) NullPointer;
36.29 + dynT = fst(hp \\<And> (the_Addr oref));
36.30 + (dc,mh,mxl,c)= the (cmethd (G,dynT) (mn,ps));
36.31 + frs' = xcpt_update xp' [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] []
36.32 + in
36.33 + (xp' , frs' , drop (n+1) stk , pc+1))"
36.34 +
36.35 +
36.36 +constdefs
36.37 + exec_mr :: "[opstack,frame list] \\<Rightarrow> frame list"
36.38 +"exec_mr stk0 frs \\<equiv>
36.39 + (let val = hd stk0;
36.40 + (stk,loc,cn,met,pc) = hd frs
36.41 + in
36.42 + (val#stk,loc,cn,met,pc)#tl frs)"
36.43 +
36.44 +end
37.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
37.2 +++ b/src/HOL/MicroJava/JVM/Object.thy Thu Nov 11 12:23:45 1999 +0100
37.3 @@ -0,0 +1,73 @@
37.4 +(* Title: HOL/MicroJava/JVM/Object.thy
37.5 + ID: $Id$
37.6 + Author: Cornelia Pusch
37.7 + Copyright 1999 Technische Universitaet Muenchen
37.8 +
37.9 +Get and putfield instructions
37.10 +*)
37.11 +
37.12 +Object = JVMState +
37.13 +
37.14 +datatype
37.15 + create_object = New cname
37.16 +
37.17 +consts
37.18 + exec_co :: "[create_object,'code prog,aheap,opstack,p_count] \\<Rightarrow>
37.19 + (xcpt option \\<times> aheap \\<times> opstack \\<times> p_count)"
37.20 +
37.21 +
37.22 +primrec
37.23 + "exec_co (New C) G hp stk pc =
37.24 + (let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory;
37.25 + oref = newref hp;
37.26 + fs = init_vars (fields(G,C));
37.27 + hp' = xcpt_update xp' (hp(oref \\<mapsto> (C,fs))) hp;
37.28 + stk' = xcpt_update xp' ((Addr oref)#stk) stk
37.29 + in (xp' , hp' , stk' , pc+1))"
37.30 +
37.31 +
37.32 +datatype
37.33 + manipulate_object =
37.34 + Getfield vname cname (* Fetch field from object *)
37.35 + | Putfield vname cname (* Set field in object *)
37.36 +
37.37 +consts
37.38 + exec_mo :: "[manipulate_object,aheap,opstack,p_count] \\<Rightarrow>
37.39 + (xcpt option \\<times> aheap \\<times> opstack \\<times> p_count)"
37.40 +
37.41 +primrec
37.42 + "exec_mo (Getfield F C) hp stk pc =
37.43 + (let oref = hd stk;
37.44 + xp' = raise_xcpt (oref=Null) NullPointer;
37.45 + (oc,fs) = hp \\<And> (the_Addr oref);
37.46 + stk' = xcpt_update xp' ((fs\\<And>(F,C))#(tl stk)) (tl stk)
37.47 + in
37.48 + (xp' , hp , stk' , pc+1))"
37.49 +
37.50 + "exec_mo (Putfield F C) hp stk pc =
37.51 + (let (fval,oref)= (hd stk, hd(tl stk));
37.52 + xp' = raise_xcpt (oref=Null) NullPointer;
37.53 + a = the_Addr oref;
37.54 + (oc,fs) = hp \\<And> a;
37.55 + hp' = xcpt_update xp' (hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval)))) hp
37.56 + in
37.57 + (xp' , hp' , tl (tl stk), pc+1))"
37.58 +
37.59 +
37.60 +datatype
37.61 + check_object =
37.62 + Checkcast cname (* Check whether object is of given type *)
37.63 +
37.64 +consts
37.65 + exec_ch :: "[check_object,'code prog,aheap,opstack,p_count]
37.66 + \\<Rightarrow> (xcpt option \\<times> opstack \\<times> p_count)"
37.67 +
37.68 +primrec
37.69 + "exec_ch (Checkcast C) G hp stk pc =
37.70 + (let oref = hd stk;
37.71 + xp' = raise_xcpt (\\<not> cast_ok G (Class C) hp oref) ClassCast;
37.72 + stk' = xcpt_update xp' stk (tl stk)
37.73 + in
37.74 + (xp' , stk' , pc+1))"
37.75 +
37.76 +end
38.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
38.2 +++ b/src/HOL/MicroJava/JVM/Opstack.thy Thu Nov 11 12:23:45 1999 +0100
38.3 @@ -0,0 +1,38 @@
38.4 +(* Title: HOL/MicroJava/JVM/Opstack.thy
38.5 + ID: $Id$
38.6 + Author: Cornelia Pusch
38.7 + Copyright 1999 Technische Universitaet Muenchen
38.8 +
38.9 +Manipulation of operand stack
38.10 +*)
38.11 +
38.12 +Opstack = JVMState +
38.13 +
38.14 +(** instructions for the direct manipulation of the operand stack **)
38.15 +
38.16 +datatype
38.17 + op_stack =
38.18 + Pop
38.19 + | Dup
38.20 + | Dup_x1
38.21 + | Dup_x2
38.22 + | Swap
38.23 +
38.24 +consts
38.25 + exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)"
38.26 +
38.27 +primrec
38.28 + "exec_os Pop stk pc = (tl stk , pc+1)"
38.29 +
38.30 + "exec_os Dup stk pc = (hd stk # stk , pc+1)"
38.31 +
38.32 + "exec_os Dup_x1 stk pc = (hd stk # hd (tl stk) # hd stk # (tl (tl stk)) , pc+1)"
38.33 +
38.34 + "exec_os Dup_x2 stk pc = (hd stk # hd (tl stk) # (hd (tl (tl stk))) # hd stk # (tl (tl (tl stk))) , pc+1)"
38.35 +
38.36 + "exec_os Swap stk pc =
38.37 + (let (val1,val2) = (hd stk,hd (tl stk))
38.38 + in
38.39 + (val2#val1#(tl (tl stk)) , pc+1))"
38.40 +
38.41 +end
39.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
39.2 +++ b/src/HOL/MicroJava/JVM/Store.ML Thu Nov 11 12:23:45 1999 +0100
39.3 @@ -0,0 +1,10 @@
39.4 +(* Title: HOL/MicroJava/JVM/Store.thy
39.5 + ID: $Id$
39.6 + Author: Cornelia Pusch
39.7 + Copyright 1999 Technische Universitaet Muenchen
39.8 +*)
39.9 +
39.10 +Goalw [newref_def]
39.11 + "hp x = None \\<longrightarrow> hp (newref hp) = None";
39.12 +by (fast_tac (claset() addIs [selectI2EX] addss (simpset())) 1);
39.13 +qed_spec_mp "newref_None";
40.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
40.2 +++ b/src/HOL/MicroJava/JVM/Store.thy Thu Nov 11 12:23:45 1999 +0100
40.3 @@ -0,0 +1,23 @@
40.4 +(* Title: HOL/MicroJava/JVM/Store.thy
40.5 + ID: $Id$
40.6 + Author: Cornelia Pusch
40.7 + Copyright 1999 Technische Universitaet Muenchen
40.8 +
40.9 +The store.
40.10 +
40.11 +The JVM builds on many notions already defined in Java.
40.12 +Conform provides notions for the type safety proof of the Bytecode Verifier.
40.13 +*)
40.14 +
40.15 +Store = Conform +
40.16 +
40.17 +syntax
40.18 + value :: "['a \\<leadsto> 'b,'a] \\<Rightarrow> 'b" ("_ \\<And> _")
40.19 +translations
40.20 + "t \\<And> x" == "the (t x)"
40.21 +
40.22 +constdefs
40.23 + newref :: "('a \\<leadsto> 'b) \\<Rightarrow> 'a"
40.24 + "newref s \\<equiv> \\<epsilon>v. s v = None"
40.25 +
40.26 +end
41.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
41.2 +++ b/src/HOL/MicroJava/ROOT.ML Thu Nov 11 12:23:45 1999 +0100
41.3 @@ -0,0 +1,12 @@
41.4 +goals_limit:=1;
41.5 +
41.6 +Unify.search_bound := 40;
41.7 +Unify.trace_bound := 40;
41.8 +
41.9 +add_path "J";
41.10 +add_path "JVM";
41.11 +add_path "BV";
41.12 +
41.13 +
41.14 +use_thy "JTypeSafe";
41.15 +use_thy "BVSpecTypeSafe";