| author | kleing |
| Sun, 07 Jan 2001 18:43:13 +0100 | |
| changeset 10812 | ead84e90bfeb |
| parent 10811 | 98f52cb93d93 |
| child 10813 | d466b42ad7a9 |
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sat Jan 06 21:31:37 2001 +0100 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sun Jan 07 18:43:13 2001 +0100 @@ -11,28 +11,30 @@ theory BVSpecTypeSafe = Correct: -lemmas defs1 = sup_state_def correct_state_def correct_frame_def +lemmas defs1 = sup_state_conv correct_state_def correct_frame_def wt_instr_def step_def lemmas [simp del] = split_paired_All lemma wt_jvm_prog_impl_wt_instr_cor: "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" apply (unfold correct_state_def Let_def correct_frame_def) apply simp apply (blast intro: wt_jvm_prog_impl_wt_instr) done +lemmas [iff] = not_Err_eq + lemma Load_correct: "[| wf_prog wt G; method (G,C) sig = Some (C,rT,maxs,maxl,ins); ins!pc = Load idx; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 map_eq_Cons) apply (rule conjI) apply (rule approx_loc_imp_approx_val_sup) @@ -47,8 +49,8 @@ ins!pc = Store idx; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 map_eq_Cons) apply (rule conjI) apply (blast intro: approx_stk_imp_approx_stk_sup) @@ -58,7 +60,7 @@ lemma conf_Intg_Integer [iff]: - "G,h \\<turnstile> Intg i ::\\<preceq> PrimT Integer" + "G,h \<turnstile> Intg i ::\<preceq> PrimT Integer" by (simp add: conf_def) @@ -68,17 +70,17 @@ ins!pc = Bipush i; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons) apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup) done lemma NT_subtype_conv: - "G \\<turnstile> NT \\<preceq> T = (T=NT \\<or> (\\<exists>C. T = Class C))" + "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))" proof - - have "!!T T'. G \\<turnstile> T' \\<preceq> T ==> T' = NT --> (T=NT | (\\<exists>C. T = Class C))" + have "!!T T'. G \<turnstile> T' \<preceq> T ==> T' = NT --> (T=NT | (\<exists>C. T = Class C))" apply (erule widen.induct) apply auto apply (case_tac R) @@ -96,8 +98,8 @@ ins!pc = Aconst_null; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 map_eq_Cons) apply (rule conjI) apply (force simp add: approx_val_Null NT_subtype_conv) @@ -107,9 +109,9 @@ lemma Cast_conf2: - "[| wf_prog ok G; G,h\\<turnstile>v::\\<preceq>RefT rt; cast_ok G C h v; - G\\<turnstile>Class C\\<preceq>T; is_class G C|] - ==> G,h\\<turnstile>v::\\<preceq>T" + "[| wf_prog ok G; G,h\<turnstile>v::\<preceq>RefT rt; cast_ok G C h v; + G\<turnstile>Class C\<preceq>T; is_class G C|] + ==> G,h\<turnstile>v::\<preceq>T" apply (unfold cast_ok_def) apply (frule widen_Class) apply (elim exE disjE) @@ -126,8 +128,8 @@ ins!pc = Checkcast D; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def) apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2) @@ -140,8 +142,8 @@ ins!pc = Getfield F D; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split) apply (frule conf_widen) @@ -162,8 +164,8 @@ ins!pc = Putfield F D; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split) apply (clarsimp simp add: approx_val_def) apply (frule conf_widen) @@ -183,7 +185,7 @@ done lemma collapse_paired_All: - "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)" + "(\<forall>x y. P(x,y)) = (\<forall>z. P z)" by fast lemma New_correct: @@ -192,8 +194,8 @@ ins!pc = New cl_idx; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def defs1 fun_upd_apply map_eq_Cons raise_xcpt_def init_vars_def split: option.split) @@ -220,15 +222,15 @@ ins ! pc = Invoke C' mn pTs; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" proof - assume wtprog: "wt_jvm_prog G phi" assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins)" assume ins: "ins ! pc = Invoke C' mn pTs" assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc" assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)" - assume approx: "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd>" + assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>" from wtprog obtain wfmb where @@ -237,7 +239,7 @@ from ins method approx obtain s where - heap_ok: "G\\<turnstile>h hp\\<surd>" and + heap_ok: "G\<turnstile>h hp\<surd>" and phi_pc: "phi C sig!pc = Some s" and is_class_C: "is_class G C" and frame: "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and @@ -249,11 +251,11 @@ s: "s = (rev apTs @ X # ST, LT)" and l: "length apTs = length pTs" and is_class: "is_class G C'" and - X: "G\\<turnstile> X \\<preceq> Class C'" and - w: "\\<forall>x\\<in>set (zip apTs pTs). x \\<in> widen G" and + X: "G\<turnstile> X \<preceq> Class C'" and + w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and pc: "Suc pc < length ins" and - step: "G \\<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" + step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc" by (simp add: wt_instr_def del: not_None_eq) (elim exE conjE, rule that) from step @@ -284,13 +286,13 @@ by - (drule approx_stk_append_lemma, simp, elim, simp) from oX - have "\\<exists>T'. typeof (option_map obj_ty \\<circ> hp) oX = Some T' \\<and> G \\<turnstile> T' \\<preceq> X" + have "\<exists>T'. typeof (option_map obj_ty \<circ> hp) oX = Some T' \<and> G \<turnstile> T' \<preceq> X" by (clarsimp simp add: approx_val_def conf_def) with X_Ref obtain T' where - oX_Ref: "typeof (option_map obj_ty \\<circ> hp) oX = Some (RefT T')" - "G \\<turnstile> RefT T' \\<preceq> X" + oX_Ref: "typeof (option_map obj_ty \<circ> hp) oX = Some (RefT T')" + "G \<turnstile> RefT T' \<preceq> X" apply (elim, simp) apply (frule widen_RefT2) by (elim, simp) @@ -317,7 +319,7 @@ by (auto simp add: obj_ty_def) with X_Ref oX_Ref loc - obtain D: "G \\<turnstile> Class D \\<preceq> X" + obtain D: "G \<turnstile> Class D \<preceq> X" by simp with X_Ref @@ -326,26 +328,26 @@ by - (drule widen_Class, elim, rule that) with X - have X'_subcls: "G \\<turnstile> X' \\<preceq>C C'" + have X'_subcls: "G \<turnstile> X' \<preceq>C C'" by simp with mC' wfprog obtain D0 rT0 maxs0 maxl0 ins0 where - mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0)" "G\\<turnstile>rT0\\<preceq>rT" + mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxs0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT" by (auto dest: subtype_widen_methd intro: that) from X' D - have D_subcls: "G \\<turnstile> D \\<preceq>C X'" + have D_subcls: "G \<turnstile> D \<preceq>C X'" by simp with wfprog mX obtain D'' rT' mxs' mxl' ins' where mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxs', mxl', ins')" - "G \\<turnstile> rT' \\<preceq> rT0" + "G \<turnstile> rT' \<preceq> rT0" by (auto dest: subtype_widen_methd intro: that) from mX mD - have rT': "G \\<turnstile> rT' \\<preceq> rT" + have rT': "G \<turnstile> rT' \<preceq> rT" by - (rule widen_trans) from is_class X'_subcls D_subcls @@ -371,35 +373,35 @@ by (simp add: raise_xcpt_def) from wtprog mD'' - have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \\<and> ins' \\<noteq> []" + have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []" by (auto dest: wt_jvm_prog_impl_wt_start) then obtain LT0 where LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)" - by (clarsimp simp add: wt_start_def sup_state_def) + by (clarsimp simp add: wt_start_def sup_state_conv) have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f" proof - from start LT0 have sup_loc: - "G \\<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0" - (is "G \\<turnstile> ?LT <=l LT0") - by (simp add: wt_start_def sup_state_def) + "G \<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0" + (is "G \<turnstile> ?LT <=l LT0") + by (simp add: wt_start_def sup_state_conv) have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)" by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if) from wfprog mD is_class_D - have "G \\<turnstile> Class D \\<preceq> Class D''" + have "G \<turnstile> Class D \<preceq> Class D''" by (auto dest: method_wf_mdecl) with obj_ty loc have a: "approx_val G hp (Addr ref) (OK (Class D''))" by (simp add: approx_val_def conf_def) from w l - have "\\<forall>x\\<in>set (zip (rev apTs) (rev pTs)). x \\<in> widen G" + have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G" by (auto simp add: zip_rev) with wfprog l l_o opTs have "approx_loc G hp opTs (map OK (rev pTs))" @@ -426,15 +428,15 @@ have c_f': "correct_frame G hp (tl ST', LT') maxl ins ?f'" proof - from s s' mC' step l - have "G \\<turnstile> LT <=l LT'" - by (simp add: step_def sup_state_def) + have "G \<turnstile> LT <=l LT'" + by (simp add: step_def sup_state_conv) with wfprog a_loc have a: "approx_loc G hp loc LT'" by (rule approx_loc_imp_approx_loc_sup) moreover from s s' mC' step l - have "G \\<turnstile> map OK ST <=l map OK (tl ST')" - by (auto simp add: step_def sup_state_def map_eq_Cons) + have "G \<turnstile> map OK ST <=l map OK (tl ST')" + by (auto simp add: step_def sup_state_conv map_eq_Cons) with wfprog a_stk' have "approx_stk G hp stk' (tl ST')" by (rule approx_stk_imp_approx_stk_sup) @@ -450,7 +452,7 @@ } with Null_ok oX_Ref - show "G,phi \\<turnstile>JVM state'\\<surd>" + show "G,phi \<turnstile>JVM state'\<surd>" by - (cases oX, auto) qed @@ -462,8 +464,8 @@ ins ! pc = Return; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm iff del: not_None_eq) apply (frule wt_jvm_prog_impl_wt_instr) apply (assumption, assumption, erule Suc_lessD) @@ -483,8 +485,8 @@ ins ! pc = Goto branch; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1) apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) @@ -497,8 +499,8 @@ ins ! pc = Ifcmpeq branch; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1) apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) @@ -510,8 +512,8 @@ ins ! pc = Pop; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1) apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup) @@ -523,8 +525,8 @@ ins ! pc = Dup; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 map_eq_Cons) apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup @@ -538,8 +540,8 @@ ins ! pc = Dup_x1; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 map_eq_Cons) apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup @@ -553,8 +555,8 @@ ins ! pc = Dup_x2; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 map_eq_Cons) apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup @@ -568,8 +570,8 @@ ins ! pc = Swap; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 map_eq_Cons) apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup @@ -583,8 +585,8 @@ ins ! pc = IAdd; wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc; Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def) apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup @@ -598,8 +600,8 @@ "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); - G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> |] -==> G,phi \\<turnstile>JVM state'\\<surd>" + G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] +==> G,phi \<turnstile>JVM state'\<surd>" apply (frule wt_jvm_prog_impl_wt_instr_cor) apply assumption+ apply (cases "ins!pc") @@ -632,14 +634,14 @@ (** Main **) lemma correct_state_impl_Some_method: - "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> - ==> \\<exists>meth. method (G,C) sig = Some(C,meth)" + "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> + ==> \<exists>meth. method (G,C) sig = Some(C,meth)" by (auto simp add: correct_state_def Let_def) lemma BV_correct_1 [rule_format]: -"!!state. [| wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>|] - ==> exec (G,state) = Some state' --> G,phi \\<turnstile>JVM state'\\<surd>" +"!!state. [| wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>|] + ==> exec (G,state) = Some state' --> G,phi \<turnstile>JVM state'\<surd>" apply (simp only: split_tupled_all) apply (rename_tac xp hp frs) apply (case_tac xp) @@ -655,12 +657,12 @@ lemma L0: - "[| xp=None; frs\\<noteq>[] |] ==> (\\<exists>state'. exec (G,xp,hp,frs) = Some state')" + "[| xp=None; frs\<noteq>[] |] ==> (\<exists>state'. exec (G,xp,hp,frs) = Some state')" by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex) lemma L1: - "[|wt_jvm_prog G phi; G,phi \\<turnstile>JVM (xp,hp,frs)\\<surd>; xp=None; frs\\<noteq>[]|] - ==> \\<exists>state'. exec(G,xp,hp,frs) = Some state' \\<and> G,phi \\<turnstile>JVM state'\\<surd>" + "[|wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]|] + ==> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>" apply (drule L0) apply assumption apply (fast intro: BV_correct_1) @@ -668,7 +670,7 @@ theorem BV_correct [rule_format]: -"[| wt_jvm_prog G phi; G \\<turnstile> s -jvm-> t |] ==> G,phi \\<turnstile>JVM s\\<surd> --> G,phi \\<turnstile>JVM t\\<surd>" +"[| wt_jvm_prog G phi; G \<turnstile> s -jvm-> t |] ==> G,phi \<turnstile>JVM s\<surd> --> G,phi \<turnstile>JVM t\<surd>" apply (unfold exec_all_def) apply (erule rtrancl_induct) apply simp @@ -678,8 +680,8 @@ theorem BV_correct_initial: "[| wt_jvm_prog G phi; - G \\<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \\<turnstile>JVM s0 \\<surd>|] -==> approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \\<and> + G \<turnstile> s0 -jvm-> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>|] +==> approx_stk G hp stk (fst (the (((phi C) sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi C) sig) ! pc)))" apply (drule BV_correct) apply assumption+
--- a/src/HOL/MicroJava/BV/Convert.thy Sat Jan 06 21:31:37 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,497 +0,0 @@ -(* Title: HOL/MicroJava/BV/Convert.thy - ID: $Id$ - Author: Cornelia Pusch and Gerwin Klein - Copyright 1999 Technische Universitaet Muenchen -*) - -header "Lifted Type Relations" - -theory Convert = Err + JVMExec: - -text "The supertype relation lifted to type err, type lists and state types." - -types - locvars_type = "ty err list" - opstack_type = "ty list" - state_type = "opstack_type \<times> locvars_type" - method_type = "state_type option list" - class_type = "sig => method_type" - prog_type = "cname => class_type" - -consts - strict :: "('a => 'b err) => ('a err => 'b err)" -primrec - "strict f Err = Err" - "strict f (OK x) = f x" - - -constdefs - (* lifts a relation to err with Err as top element *) - lift_top :: "('a => 'b => bool) => ('a err => 'b err => bool)" - "lift_top P a' a == case a of - Err => True - | OK t => (case a' of Err => False | OK t' => P t' t)" - - (* lifts a relation to option with None as bottom element *) - lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)" - "lift_bottom P a' a == - case a' of - None => True - | Some t' => (case a of None => False | Some t => P t' t)" - - sup_ty_opt :: "['code prog,ty err,ty err] => bool" - ("_ \<turnstile> _ <=o _" [71,71] 70) - "sup_ty_opt G == lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')" - - sup_loc :: "['code prog,locvars_type,locvars_type] => bool" - ("_ \<turnstile> _ <=l _" [71,71] 70) - "G \<turnstile> LT <=l LT' == list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'" - - sup_state :: "['code prog,state_type,state_type] => bool" - ("_ \<turnstile> _ <=s _" [71,71] 70) - "G \<turnstile> s <=s s' == - (G \<turnstile> map OK (fst s) <=l map OK (fst s')) \<and> G \<turnstile> snd s <=l snd s'" - - sup_state_opt :: "['code prog,state_type option,state_type option] => bool" - ("_ \<turnstile> _ <=' _" [71,71] 70) - "sup_state_opt G == lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')" - -syntax (HTML) - sup_ty_opt :: "['code prog,ty err,ty err] => bool" - ("_ |- _ <=o _") - sup_loc :: "['code prog,locvars_type,locvars_type] => bool" - ("_ |- _ <=l _" [71,71] 70) - sup_state :: "['code prog,state_type,state_type] => bool" - ("_ |- _ <=s _" [71,71] 70) - sup_state_opt :: "['code prog,state_type option,state_type option] => bool" - ("_ |- _ <=' _" [71,71] 70) - - -lemmas [iff] = not_Err_eq not_OK_eq - -lemma lift_top_refl [simp]: - "[| !!x. P x x |] ==> lift_top P x x" - by (simp add: lift_top_def split: err.splits) - -lemma lift_top_trans [trans]: - "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] - ==> lift_top P x z" -proof - - assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z" - assume a: "lift_top P x y" - assume b: "lift_top P y z" - - { assume "z = Err" - hence ?thesis by (simp add: lift_top_def) - } note z_none = this - - { assume "x = Err" - with a b - have ?thesis - by (simp add: lift_top_def split: err.splits) - } note x_none = this - - { fix r t - assume x: "x = OK r" and z: "z = OK t" - with a b - obtain s where y: "y = OK s" - by (simp add: lift_top_def split: err.splits) - - from a x y - have "P r s" by (simp add: lift_top_def) - also - from b y z - have "P s t" by (simp add: lift_top_def) - finally - have "P r t" . - - with x z - have ?thesis by (simp add: lift_top_def) - } - - with x_none z_none - show ?thesis by blast -qed - -lemma lift_top_Err_any [simp]: - "lift_top P Err any = (any = Err)" - by (simp add: lift_top_def split: err.splits) - -lemma lift_top_OK_OK [simp]: - "lift_top P (OK a) (OK b) = P a b" - by (simp add: lift_top_def split: err.splits) - -lemma lift_top_any_OK [simp]: - "lift_top P any (OK b) = (\<exists>a. any = OK a \<and> P a b)" - by (simp add: lift_top_def split: err.splits) - -lemma lift_top_OK_any: - "lift_top P (OK a) any = (any = Err \<or> (\<exists>b. any = OK b \<and> P a b))" - by (simp add: lift_top_def split: err.splits) - - -lemma lift_bottom_refl [simp]: - "[| !!x. P x x |] ==> lift_bottom P x x" - by (simp add: lift_bottom_def split: option.splits) - -lemma lift_bottom_trans [trans]: - "[| !!x y z. [| P x y; P y z |] ==> P x z; - lift_bottom P x y; lift_bottom P y z |] - ==> lift_bottom P x z" -proof - - assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z" - assume a: "lift_bottom P x y" - assume b: "lift_bottom P y z" - - { assume "x = None" - hence ?thesis by (simp add: lift_bottom_def) - } note z_none = this - - { assume "z = None" - with a b - have ?thesis - by (simp add: lift_bottom_def split: option.splits) - } note x_none = this - - { fix r t - assume x: "x = Some r" and z: "z = Some t" - with a b - obtain s where y: "y = Some s" - by (simp add: lift_bottom_def split: option.splits) - - from a x y - have "P r s" by (simp add: lift_bottom_def) - also - from b y z - have "P s t" by (simp add: lift_bottom_def) - finally - have "P r t" . - - with x z - have ?thesis by (simp add: lift_bottom_def) - } - - with x_none z_none - show ?thesis by blast -qed - -lemma lift_bottom_any_None [simp]: - "lift_bottom P any None = (any = None)" - by (simp add: lift_bottom_def split: option.splits) - -lemma lift_bottom_Some_Some [simp]: - "lift_bottom P (Some a) (Some b) = P a b" - by (simp add: lift_bottom_def split: option.splits) - -lemma lift_bottom_any_Some [simp]: - "lift_bottom P (Some a) any = (\<exists>b. any = Some b \<and> P a b)" - by (simp add: lift_bottom_def split: option.splits) - -lemma lift_bottom_Some_any: - "lift_bottom P any (Some b) = (any = None \<or> (\<exists>a. any = Some a \<and> P a b))" - by (simp add: lift_bottom_def split: option.splits) - - - -theorem sup_ty_opt_refl [simp]: - "G \<turnstile> t <=o t" - by (simp add: sup_ty_opt_def) - -theorem sup_loc_refl [simp]: - "G \<turnstile> t <=l t" - by (induct t, auto simp add: sup_loc_def) - -theorem sup_state_refl [simp]: - "G \<turnstile> s <=s s" - by (simp add: sup_state_def) - -theorem sup_state_opt_refl [simp]: - "G \<turnstile> s <=' s" - by (simp add: sup_state_opt_def) - - -theorem anyConvErr [simp]: - "(G \<turnstile> Err <=o any) = (any = Err)" - by (simp add: sup_ty_opt_def) - -theorem OKanyConvOK [simp]: - "(G \<turnstile> (OK ty') <=o (OK ty)) = (G \<turnstile> ty' \<preceq> ty)" - by (simp add: sup_ty_opt_def) - -theorem sup_ty_opt_OK: - "G \<turnstile> a <=o (OK b) ==> \<exists> x. a = OK x" - by (clarsimp simp add: sup_ty_opt_def) - -lemma widen_PrimT_conv1 [simp]: - "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x" - by (auto elim: widen.elims) - -theorem sup_PTS_eq: - "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))" - by (auto simp add: sup_ty_opt_def lift_top_OK_any) - - - -theorem sup_loc_Nil [iff]: - "(G \<turnstile> [] <=l XT) = (XT=[])" - by (simp add: sup_loc_def) - -theorem sup_loc_Cons [iff]: - "(G \<turnstile> (Y#YT) <=l XT) = (\<exists>X XT'. XT=X#XT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT <=l XT'))" - by (simp add: sup_loc_def list_all2_Cons1) - -theorem sup_loc_Cons2: - "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))" - by (simp add: sup_loc_def list_all2_Cons2) - - -theorem sup_loc_length: - "G \<turnstile> a <=l b ==> length a = length b" -proof - - assume G: "G \<turnstile> a <=l b" - have "\<forall> b. (G \<turnstile> a <=l b) --> length a = length b" - by (induct a, auto) - with G - show ?thesis by blast -qed - -theorem sup_loc_nth: - "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)" -proof - - assume a: "G \<turnstile> a <=l b" "n < length a" - have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))" - (is "?P a") - proof (induct a) - show "?P []" by simp - - fix x xs assume IH: "?P xs" - - show "?P (x#xs)" - proof (intro strip) - fix n b - assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)" - with IH - show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)" - by - (cases n, auto) - qed - qed - with a - show ?thesis by blast -qed - - -theorem all_nth_sup_loc: - "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) - --> (G \<turnstile> a <=l b)" (is "?P a") -proof (induct a) - show "?P []" by simp - - fix l ls assume IH: "?P ls" - - show "?P (l#ls)" - proof (intro strip) - fix b - assume f: "\<forall>n. n < length (l # ls) --> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))" - assume l: "length (l#ls) = length b" - - then obtain b' bs where b: "b = b'#bs" - by - (cases b, simp, simp add: neq_Nil_conv, rule that) - - with f - have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))" - by auto - - with f b l IH - show "G \<turnstile> (l # ls) <=l b" - by auto - qed -qed - - -theorem sup_loc_append: - "length a = length b ==> - (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))" -proof - - assume l: "length a = length b" - - have "\<forall>b. length a = length b --> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> - (G \<turnstile> x <=l y))" (is "?P a") - proof (induct a) - show "?P []" by simp - - fix l ls assume IH: "?P ls" - show "?P (l#ls)" - proof (intro strip) - fix b - assume "length (l#ls) = length (b::ty err list)" - with IH - show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))" - by - (cases b, auto) - qed - qed - with l - show ?thesis by blast -qed - -theorem sup_loc_rev [simp]: - "(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" -proof - - have "\<forall>b. (G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" (is "\<forall>b. ?Q a b" is "?P a") - proof (induct a) - show "?P []" by simp - - fix l ls assume IH: "?P ls" - - { - fix b - have "?Q (l#ls) b" - proof (cases (open) b) - case Nil - thus ?thesis by (auto dest: sup_loc_length) - next - case Cons - show ?thesis - proof - assume "G \<turnstile> (l # ls) <=l b" - thus "G \<turnstile> rev (l # ls) <=l rev b" - by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append) - next - assume "G \<turnstile> rev (l # ls) <=l rev b" - hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])" - by (simp add: Cons) - - hence "length (rev ls) = length (rev list)" - by (auto dest: sup_loc_length) - - from this G - obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a" - by (simp add: sup_loc_append) - - thus "G \<turnstile> (l # ls) <=l b" - by (simp add: Cons IH) - qed - qed - } - thus "?P (l#ls)" by blast - qed - - thus ?thesis by blast -qed - - -theorem sup_loc_update [rule_format]: - "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) --> - (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x") -proof (induct x) - show "?P []" by simp - - fix l ls assume IH: "?P ls" - show "?P (l#ls)" - proof (intro strip) - fix n y - assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y" - with IH - show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]" - by - (cases n, auto simp add: sup_loc_Cons2 list_all2_Cons1) - qed -qed - - -theorem sup_state_length [simp]: - "G \<turnstile> s2 <=s s1 ==> - length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)" - by (auto dest: sup_loc_length simp add: sup_state_def); - -theorem sup_state_append_snd: - "length a = length b ==> - (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))" - by (auto simp add: sup_state_def sup_loc_append) - -theorem sup_state_append_fst: - "length a = length b ==> - (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))" - by (auto simp add: sup_state_def sup_loc_append) - -theorem sup_state_Cons1: - "(G \<turnstile> (x#xt, a) <=s (yt, b)) = - (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))" - by (auto simp add: sup_state_def map_eq_Cons) - -theorem sup_state_Cons2: - "(G \<turnstile> (xt, a) <=s (y#yt, b)) = - (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))" - by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2) - -theorem sup_state_ignore_fst: - "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)" - by (simp add: sup_state_def) - -theorem sup_state_rev_fst: - "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))" -proof - - have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map) - show ?thesis by (simp add: m sup_state_def) -qed - - -lemma sup_state_opt_None_any [iff]: - "(G \<turnstile> None <=' any) = True" - by (simp add: sup_state_opt_def lift_bottom_def) - -lemma sup_state_opt_any_None [iff]: - "(G \<turnstile> any <=' None) = (any = None)" - by (simp add: sup_state_opt_def) - -lemma sup_state_opt_Some_Some [iff]: - "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)" - by (simp add: sup_state_opt_def del: split_paired_Ex) - -lemma sup_state_opt_any_Some [iff]: - "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)" - by (simp add: sup_state_opt_def) - -lemma sup_state_opt_Some_any: - "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))" - by (simp add: sup_state_opt_def lift_bottom_Some_any) - - -theorem sup_ty_opt_trans [trans]: - "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c" - by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def) - -theorem sup_loc_trans [trans]: - "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c" -proof - - assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c" - - hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))" - proof (intro strip) - fix n - assume n: "n < length a" - with G - have "G \<turnstile> (a!n) <=o (b!n)" - by - (rule sup_loc_nth) - also - from n G - have "G \<turnstile> ... <=o (c!n)" - by - (rule sup_loc_nth, auto dest: sup_loc_length) - finally - show "G \<turnstile> (a!n) <=o (c!n)" . - qed - - with G - show ?thesis - by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) -qed - - -theorem sup_state_trans [trans]: - "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c" - by (auto intro: sup_loc_trans simp add: sup_state_def) - -theorem sup_state_opt_trans [trans]: - "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c" - by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def) - - -end
--- a/src/HOL/MicroJava/BV/Correct.thy Sat Jan 06 21:31:37 2001 +0100 +++ b/src/HOL/MicroJava/BV/Correct.thy Sun Jan 07 18:43:13 2001 +0100 @@ -166,7 +166,7 @@ lemma approx_loc_imp_approx_loc_sup [rule_format]: "wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' --> approx_loc G hp lvars lt'" -apply (unfold sup_loc_def approx_loc_def list_all2_def) +apply (unfold Listn.le_def lesub_def sup_loc_def approx_loc_def list_all2_def) apply (auto simp add: all_set_conv_all_nth) apply (auto elim: approx_val_imp_approx_val_sup) done
--- a/src/HOL/MicroJava/BV/Err.thy Sat Jan 06 21:31:37 2001 +0100 +++ b/src/HOL/MicroJava/BV/Err.thy Sun Jan 07 18:43:13 2001 +0100 @@ -54,6 +54,13 @@ "err_semilat L" == "semilat(Err.sl L)" +consts + strict :: "('a => 'b err) => ('a err => 'b err)" +primrec + "strict f Err = Err" + "strict f (OK x) = f x" + + lemma not_Err_eq: "(x \<noteq> Err) = (\<exists>a. x = OK a)" by (cases x) auto @@ -63,6 +70,7 @@ by (cases x) auto + lemma unfold_lesub_err: "e1 <=_(le r) e2 == le r e1 e2" by (simp add: lesub_def)
--- a/src/HOL/MicroJava/BV/JType.thy Sat Jan 06 21:31:37 2001 +0100 +++ b/src/HOL/MicroJava/BV/JType.thy Sun Jan 07 18:43:13 2001 +0100 @@ -1,12 +1,10 @@ (* Title: HOL/BCV/JType.thy ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow, Gerwin Klein Copyright 2000 TUM - -The type system of the JVM *) -header "JVM Type System as Semilattice" +header "Java Type System as Semilattice" theory JType = WellForm + Err: @@ -201,10 +199,11 @@ (cases s, auto intro: widen.null split: ty.splits ref_ty.splits if_splits) } note this [intro] - + have "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y" by (auto simp add: lesub_def plussub_def le_def lift2_def split: err.split) + moreover { fix c1 c2 @@ -285,8 +284,6 @@ "wf_prog wf_mb G ==> single_valued (subcls1 G)" by (unfold wf_prog_def unique_def single_valued_def subcls1_def) auto -ML_setup {* bind_thm ("acyclic_subcls1", acyclic_subcls1) *} - theorem err_semilat_JType_esl: "wf_prog wf_mb G ==> err_semilat (esl G)" by (frule acyclic_subcls1, frule single_valued_subcls1, rule err_semilat_JType_esl_lemma)
--- a/src/HOL/MicroJava/BV/JVM.thy Sat Jan 06 21:31:37 2001 +0100 +++ b/src/HOL/MicroJava/BV/JVM.thy Sun Jan 07 18:43:13 2001 +0100 @@ -7,30 +7,7 @@ header "Kildall for the JVM" -theory JVM = Kildall + JType + Opt + Product + DFA_err + StepMono + BVSpec: - -types state = "state_type option err" - -constdefs - stk_esl :: "'c prog => nat => ty list esl" -"stk_esl S maxs == upto_esl maxs (JType.esl S)" - - reg_sl :: "'c prog => nat => ty err list sl" -"reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))" - - sl :: "'c prog => nat => nat => state sl" -"sl S maxs maxr == - Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))" - - states :: "'c prog => nat => nat => state set" -"states S maxs maxr == fst(sl S maxs maxr)" - - le :: "'c prog => nat => nat => state ord" -"le S maxs maxr == fst(snd(sl S maxs maxr))" - - sup :: "'c prog => nat => nat => state binop" -"sup S maxs maxr == snd(snd(sl S maxs maxr))" - +theory JVM = Kildall + JVMType + Opt + Product + DFA_err + StepMono + BVSpec: constdefs exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> state" @@ -38,7 +15,7 @@ kiljvm :: "jvm_prog => nat => nat => ty => instr list => state list => state list" "kiljvm G maxs maxr rT bs == - kildall (sl G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)" + kildall (JVMType.sl G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)" wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool" "wt_kil G C pTs rT mxs mxl ins == @@ -52,102 +29,6 @@ "wt_jvm_prog_kildall G == wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)). wt_kil G C (snd sig) rT maxs maxl b) G" -lemma JVM_states_unfold: - "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*> - list maxr (err(types S))))" - apply (unfold states_def JVM.sl_def Opt.esl_def Err.sl_def - stk_esl_def reg_sl_def Product.esl_def - Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) - by simp - - -lemma JVM_le_unfold: - "le S m n == - Err.le(Opt.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))" - apply (unfold JVM.le_def JVM.sl_def Opt.esl_def Err.sl_def - stk_esl_def reg_sl_def Product.esl_def - Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) - by simp - - -lemma Err_convert: - "Err.le (subtype G) a b = G \<turnstile> a <=o b" - by (auto simp add: Err.le_def sup_ty_opt_def lift_top_def lesub_def subtype_def - split: err.split) - -lemma loc_convert: - "Listn.le (Err.le (subtype G)) a b = G \<turnstile> a <=l b" - by (unfold Listn.le_def lesub_def sup_loc_def list_all2_def) - (simp add: Err_convert) - -lemma zip_map [rule_format]: - "\<forall>a. length a = length b --> zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)" - apply (induct b) - apply simp - apply clarsimp - apply (case_tac aa) - apply simp+ - done - -lemma stk_convert: - "Listn.le (subtype G) a b = G \<turnstile> map OK a <=l map OK b" -proof - assume "Listn.le (subtype G) a b" - - hence le: "list_all2 (subtype G) a b" - by (unfold Listn.le_def lesub_def) - - { fix x' y' - assume "length a = length b" - "(x',y') \<in> set (zip (map OK a) (map OK b))" - then - obtain x y where OK: - "x' = OK x" "y' = OK y" "(x,y) \<in> set (zip a b)" - by (auto simp add: zip_map) - with le - have "subtype G x y" - by (simp add: list_all2_def Ball_def) - with OK - have "G \<turnstile> x' <=o y'" - by (simp add: subtype_def) - } - - with le - show "G \<turnstile> map OK a <=l map OK b" - by (auto simp add: sup_loc_def list_all2_def) -next - assume "G \<turnstile> map OK a <=l map OK b" - - thus "Listn.le (subtype G) a b" - apply (unfold sup_loc_def list_all2_def Listn.le_def lesub_def) - apply (clarsimp simp add: zip_map subtype_def) - apply (drule bspec, assumption) - apply auto - done -qed - - -lemma state_conv: - "Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G))) a b = G \<turnstile> a <=s b" - by (unfold Product.le_def lesub_def sup_state_def) - (simp add: split_beta stk_convert loc_convert) - -lemma state_opt_conv: - "Opt.le (Product.le (Listn.le (subtype G)) (Listn.le (Err.le (subtype G)))) a b = G \<turnstile> a <=' b" - by (unfold Opt.le_def lesub_def sup_state_opt_def lift_bottom_def) - (auto simp add: state_conv split: option.split) - -lemma JVM_le_convert: - "le G m n (OK t1) (OK t2) = G \<turnstile> t1 <=' t2" - by (simp add: JVM_le_unfold Err.le_def lesub_def state_opt_conv) - -lemma JVM_le_Err_conv: - "le G m n = Err.le (sup_state_opt G)" - apply (simp add: expand_fun_eq) - apply (unfold Err.le_def JVM_le_unfold lesub_def) - apply (clarsimp split: err.splits) - apply (simp add: state_opt_conv) - done lemma special_ex_swap_lemma [iff]: "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)" @@ -208,7 +89,7 @@ theorem exec_mono: "wf_prog wf_mb G ==> - mono (JVM.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)" + mono (JVMType.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)" apply (unfold mono_def) apply clarify apply (unfold lesub_def) @@ -227,8 +108,8 @@ done theorem semilat_JVM_slI: - "[| wf_prog wf_mb G |] ==> semilat(sl G maxs maxr)" - apply (unfold JVM.sl_def stk_esl_def reg_sl_def) + "[| wf_prog wf_mb G |] ==> semilat (JVMType.sl G maxs maxr)" + apply (unfold JVMType.sl_def stk_esl_def reg_sl_def) apply (rule semilat_opt) apply (rule err_semilat_Product_esl) apply (rule err_semilat_upto_esl) @@ -239,16 +120,14 @@ done lemma sl_triple_conv: - "sl G maxs maxr == - (states G maxs maxr, le G maxs maxr, sup G maxs maxr)" - by (simp (no_asm) add: states_def JVM.le_def JVM.sup_def) + "JVMType.sl G maxs maxr == + (states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)" + by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def) -ML_setup {* bind_thm ("wf_subcls1", wf_subcls1); *} - theorem is_bcv_kiljvm: "[| wf_prog wf_mb G; bounded (\<lambda>pc. succs (bs!pc) pc) (size bs) |] ==> - is_bcv (JVM.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc) + is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc) (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)" apply (unfold kiljvm_def sl_triple_conv) apply (rule is_bcv_kildall) @@ -295,7 +174,7 @@ from wf bounded have bcv: - "is_bcv (le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc) + "is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc) (size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)" by (rule is_bcv_kiljvm) @@ -328,14 +207,14 @@ with bcv success result have "\<exists>ts\<in>list (length bs) (states G maxs maxr). - ?start <=[le G maxs maxr] ts \<and> - welltyping (JVM.le G maxs maxr) Err (JVM.exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts" + ?start <=[JVMType.le G maxs maxr] ts \<and> + welltyping (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts" by (unfold is_bcv_def) auto then obtain phi' where l: "phi' \<in> list (length bs) (states G maxs maxr)" and - s: "?start <=[le G maxs maxr] phi'" and - w: "welltyping (le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'" + s: "?start <=[JVMType.le G maxs maxr] phi'" and + w: "welltyping (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'" by blast hence dynamic: @@ -343,7 +222,7 @@ by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv) from s - have le: "le G maxs maxr (?start ! 0) (phi'!0)" + have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)" by (drule_tac p=0 in le_listD) (simp add: lesub_def)+ from l @@ -356,7 +235,7 @@ with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0" - by clarsimp + by (clarsimp simp add: not_Err_eq) from l bounded have "bounded (\<lambda>pc. succs (bs ! pc) pc) (length phi')" @@ -434,7 +313,7 @@ from wf bounded have is_bcv: - "is_bcv (JVM.le G maxs ?maxr) Err (exec G maxs rT bs) ?succs + "is_bcv (JVMType.le G maxs ?maxr) Err (exec G maxs rT bs) ?succs (size bs) (states G maxs ?maxr) (kiljvm G maxs ?maxr rT bs)" by (rule is_bcv_kiljvm)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/MicroJava/BV/JVMType.thy Sun Jan 07 18:43:13 2001 +0100 @@ -0,0 +1,465 @@ +(* Title: HOL/BCV/JVM.thy + ID: $Id$ + Author: Gerwin Klein + Copyright 2000 TUM + +*) + +header "JVM Type System" + +theory JVMType = Opt + Product + Listn + JType: + +types + locvars_type = "ty err list" + opstack_type = "ty list" + state_type = "opstack_type \<times> locvars_type" + state = "state_type option err" (* for Kildall *) + method_type = "state_type option list" (* for BVSpec *) + class_type = "sig => method_type" + prog_type = "cname => class_type" + + +constdefs + stk_esl :: "'c prog => nat => ty list esl" + "stk_esl S maxs == upto_esl maxs (JType.esl S)" + + reg_sl :: "'c prog => nat => ty err list sl" + "reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))" + + sl :: "'c prog => nat => nat => state sl" + "sl S maxs maxr == + Err.sl(Opt.esl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))" + +constdefs + states :: "'c prog => nat => nat => state set" + "states S maxs maxr == fst(sl S maxs maxr)" + + le :: "'c prog => nat => nat => state ord" + "le S maxs maxr == fst(snd(sl S maxs maxr))" + + sup :: "'c prog => nat => nat => state binop" + "sup S maxs maxr == snd(snd(sl S maxs maxr))" + + +constdefs + sup_ty_opt :: "['code prog,ty err,ty err] => bool" + ("_ \<turnstile> _ <=o _" [71,71] 70) + "sup_ty_opt G == Err.le (subtype G)" + + sup_loc :: "['code prog,locvars_type,locvars_type] => bool" + ("_ \<turnstile> _ <=l _" [71,71] 70) + "sup_loc G == Listn.le (sup_ty_opt G)" + + sup_state :: "['code prog,state_type,state_type] => bool" + ("_ \<turnstile> _ <=s _" [71,71] 70) + "sup_state G == Product.le (Listn.le (subtype G)) (sup_loc G)" + + sup_state_opt :: "['code prog,state_type option,state_type option] => bool" + ("_ \<turnstile> _ <=' _" [71,71] 70) + "sup_state_opt G == Opt.le (sup_state G)" + + +syntax (HTML) + sup_ty_opt :: "['code prog,ty err,ty err] => bool" + ("_ |- _ <=o _") + sup_loc :: "['code prog,locvars_type,locvars_type] => bool" + ("_ |- _ <=l _" [71,71] 70) + sup_state :: "['code prog,state_type,state_type] => bool" + ("_ |- _ <=s _" [71,71] 70) + sup_state_opt :: "['code prog,state_type option,state_type option] => bool" + ("_ |- _ <=' _" [71,71] 70) + + +lemma JVM_states_unfold: + "states S maxs maxr == err(opt((Union {list n (types S) |n. n <= maxs}) <*> + list maxr (err(types S))))" + apply (unfold states_def sl_def Opt.esl_def Err.sl_def + stk_esl_def reg_sl_def Product.esl_def + Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) + by simp + + +lemma JVM_le_unfold: + "le S m n == + Err.le(Opt.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))" + apply (unfold le_def sl_def Opt.esl_def Err.sl_def + stk_esl_def reg_sl_def Product.esl_def + Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) + by simp + +lemma JVM_le_convert: + "le G m n (OK t1) (OK t2) = G \<turnstile> t1 <=' t2" + by (simp add: JVM_le_unfold Err.le_def lesub_def sup_state_opt_def + sup_state_def sup_loc_def sup_ty_opt_def) + +lemma JVM_le_Err_conv: + "le G m n = Err.le (sup_state_opt G)" + by (unfold sup_state_opt_def sup_state_def sup_loc_def + sup_ty_opt_def JVM_le_unfold) simp + +lemma zip_map [rule_format]: + "\<forall>a. length a = length b --> zip (map f a) (map g b) = map (\<lambda>(x,y). (f x, g y)) (zip a b)" + apply (induct b) + apply simp + apply clarsimp + apply (case_tac aa) + apply simp+ + done + +lemma [simp]: "Err.le r (OK a) (OK b) = r a b" + by (simp add: Err.le_def lesub_def) + +lemma stk_convert: + "Listn.le (subtype G) a b = G \<turnstile> map OK a <=l map OK b" +proof + assume "Listn.le (subtype G) a b" + + hence le: "list_all2 (subtype G) a b" + by (unfold Listn.le_def lesub_def) + + { fix x' y' + assume "length a = length b" + "(x',y') \<in> set (zip (map OK a) (map OK b))" + then + obtain x y where OK: + "x' = OK x" "y' = OK y" "(x,y) \<in> set (zip a b)" + by (auto simp add: zip_map) + with le + have "subtype G x y" + by (simp add: list_all2_def Ball_def) + with OK + have "G \<turnstile> x' <=o y'" + by (simp add: sup_ty_opt_def) + } + + with le + show "G \<turnstile> map OK a <=l map OK b" + by (unfold sup_loc_def Listn.le_def lesub_def list_all2_def) auto +next + assume "G \<turnstile> map OK a <=l map OK b" + + thus "Listn.le (subtype G) a b" + apply (unfold sup_loc_def list_all2_def Listn.le_def lesub_def) + apply (clarsimp simp add: zip_map) + apply (drule bspec, assumption) + apply (auto simp add: sup_ty_opt_def subtype_def) + done +qed + + +lemma sup_state_conv: + "(G \<turnstile> s1 <=s s2) == (G \<turnstile> map OK (fst s1) <=l map OK (fst s2)) \<and> (G \<turnstile> snd s1 <=l snd s2)" + by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def split_beta) + + +lemma subtype_refl [simp]: + "subtype G t t" + by (simp add: subtype_def) + +theorem sup_ty_opt_refl [simp]: + "G \<turnstile> t <=o t" + by (simp add: sup_ty_opt_def Err.le_def lesub_def split: err.split) + +lemma le_list_refl2 [simp]: + "(\<And>xs. r xs xs) \<Longrightarrow> Listn.le r xs xs" + by (induct xs, auto simp add: Listn.le_def lesub_def) + +theorem sup_loc_refl [simp]: + "G \<turnstile> t <=l t" + by (simp add: sup_loc_def) + +theorem sup_state_refl [simp]: + "G \<turnstile> s <=s s" + by (auto simp add: sup_state_def Product.le_def lesub_def) + +theorem sup_state_opt_refl [simp]: + "G \<turnstile> s <=' s" + by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split) + + +theorem anyConvErr [simp]: + "(G \<turnstile> Err <=o any) = (any = Err)" + by (simp add: sup_ty_opt_def Err.le_def split: err.split) + +theorem OKanyConvOK [simp]: + "(G \<turnstile> (OK ty') <=o (OK ty)) = (G \<turnstile> ty' \<preceq> ty)" + by (simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def) + +theorem sup_ty_opt_OK: + "G \<turnstile> a <=o (OK b) ==> \<exists> x. a = OK x" + by (clarsimp simp add: sup_ty_opt_def Err.le_def split: err.splits) + +lemma widen_PrimT_conv1 [simp]: + "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x" + by (auto elim: widen.elims) + +theorem sup_PTS_eq: + "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))" + by (auto simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def + split: err.splits) + +theorem sup_loc_Nil [iff]: + "(G \<turnstile> [] <=l XT) = (XT=[])" + by (simp add: sup_loc_def Listn.le_def) + +theorem sup_loc_Cons [iff]: + "(G \<turnstile> (Y#YT) <=l XT) = (\<exists>X XT'. XT=X#XT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT <=l XT'))" + by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons1) + +theorem sup_loc_Cons2: + "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))" + by (simp add: sup_loc_def Listn.le_def lesub_def list_all2_Cons2) + + +theorem sup_loc_length: + "G \<turnstile> a <=l b ==> length a = length b" +proof - + assume G: "G \<turnstile> a <=l b" + have "\<forall>b. (G \<turnstile> a <=l b) --> length a = length b" + by (induct a, auto) + with G + show ?thesis by blast +qed + +theorem sup_loc_nth: + "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)" +proof - + assume a: "G \<turnstile> a <=l b" "n < length a" + have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))" + (is "?P a") + proof (induct a) + show "?P []" by simp + + fix x xs assume IH: "?P xs" + + show "?P (x#xs)" + proof (intro strip) + fix n b + assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)" + with IH + show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)" + by - (cases n, auto) + qed + qed + with a + show ?thesis by blast +qed + +theorem all_nth_sup_loc: + "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) + --> (G \<turnstile> a <=l b)" (is "?P a") +proof (induct a) + show "?P []" by simp + + fix l ls assume IH: "?P ls" + + show "?P (l#ls)" + proof (intro strip) + fix b + assume f: "\<forall>n. n < length (l # ls) --> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))" + assume l: "length (l#ls) = length b" + + then obtain b' bs where b: "b = b'#bs" + by - (cases b, simp, simp add: neq_Nil_conv, rule that) + + with f + have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))" + by auto + + with f b l IH + show "G \<turnstile> (l # ls) <=l b" + by auto + qed +qed + + +theorem sup_loc_append: + "length a = length b ==> + (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))" +proof - + assume l: "length a = length b" + + have "\<forall>b. length a = length b --> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> + (G \<turnstile> x <=l y))" (is "?P a") + proof (induct a) + show "?P []" by simp + + fix l ls assume IH: "?P ls" + show "?P (l#ls)" + proof (intro strip) + fix b + assume "length (l#ls) = length (b::ty err list)" + with IH + show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))" + by - (cases b, auto) + qed + qed + with l + show ?thesis by blast +qed + +theorem sup_loc_rev [simp]: + "(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" +proof - + have "\<forall>b. (G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" (is "\<forall>b. ?Q a b" is "?P a") + proof (induct a) + show "?P []" by simp + + fix l ls assume IH: "?P ls" + + { + fix b + have "?Q (l#ls) b" + proof (cases (open) b) + case Nil + thus ?thesis by (auto dest: sup_loc_length) + next + case Cons + show ?thesis + proof + assume "G \<turnstile> (l # ls) <=l b" + thus "G \<turnstile> rev (l # ls) <=l rev b" + by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append) + next + assume "G \<turnstile> rev (l # ls) <=l rev b" + hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])" + by (simp add: Cons) + + hence "length (rev ls) = length (rev list)" + by (auto dest: sup_loc_length) + + from this G + obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a" + by (simp add: sup_loc_append) + + thus "G \<turnstile> (l # ls) <=l b" + by (simp add: Cons IH) + qed + qed + } + thus "?P (l#ls)" by blast + qed + + thus ?thesis by blast +qed + + +theorem sup_loc_update [rule_format]: + "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) --> + (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x") +proof (induct x) + show "?P []" by simp + + fix l ls assume IH: "?P ls" + show "?P (l#ls)" + proof (intro strip) + fix n y + assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y" + with IH + show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]" + by - (cases n, auto simp add: sup_loc_Cons2 list_all2_Cons1) + qed +qed + + +theorem sup_state_length [simp]: + "G \<turnstile> s2 <=s s1 ==> + length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)" + by (auto dest: sup_loc_length simp add: sup_state_def stk_convert lesub_def Product.le_def); + +theorem sup_state_append_snd: + "length a = length b ==> + (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))" + by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append) + +theorem sup_state_append_fst: + "length a = length b ==> + (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))" + by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def sup_loc_append) + +theorem sup_state_Cons1: + "(G \<turnstile> (x#xt, a) <=s (yt, b)) = + (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))" + by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons) + +theorem sup_state_Cons2: + "(G \<turnstile> (xt, a) <=s (y#yt, b)) = + (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))" + by (auto simp add: sup_state_def stk_convert lesub_def Product.le_def map_eq_Cons sup_loc_Cons2) + +theorem sup_state_ignore_fst: + "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)" + by (simp add: sup_state_def lesub_def Product.le_def) + +theorem sup_state_rev_fst: + "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))" +proof - + have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map) + show ?thesis by (simp add: m sup_state_def stk_convert lesub_def Product.le_def) +qed + + +lemma sup_state_opt_None_any [iff]: + "(G \<turnstile> None <=' any) = True" + by (simp add: sup_state_opt_def Opt.le_def split: option.split) + +lemma sup_state_opt_any_None [iff]: + "(G \<turnstile> any <=' None) = (any = None)" + by (simp add: sup_state_opt_def Opt.le_def split: option.split) + +lemma sup_state_opt_Some_Some [iff]: + "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)" + by (simp add: sup_state_opt_def Opt.le_def lesub_def del: split_paired_Ex) + +lemma sup_state_opt_any_Some [iff]: + "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)" + by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split) + +lemma sup_state_opt_Some_any: + "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))" + by (simp add: sup_state_opt_def Opt.le_def lesub_def split: option.split) + + +theorem sup_ty_opt_trans [trans]: + "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c" + by (auto intro: widen_trans + simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def + split: err.splits) + +theorem sup_loc_trans [trans]: + "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c" +proof - + assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c" + + hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))" + proof (intro strip) + fix n + assume n: "n < length a" + with G + have "G \<turnstile> (a!n) <=o (b!n)" + by - (rule sup_loc_nth) + also + from n G + have "G \<turnstile> ... <=o (c!n)" + by - (rule sup_loc_nth, auto dest: sup_loc_length) + finally + show "G \<turnstile> (a!n) <=o (c!n)" . + qed + + with G + show ?thesis + by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) +qed + + +theorem sup_state_trans [trans]: + "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c" + by (auto intro: sup_loc_trans simp add: sup_state_def stk_convert Product.le_def lesub_def) + +theorem sup_state_opt_trans [trans]: + "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c" + by (auto intro: sup_state_trans + simp add: sup_state_opt_def Opt.le_def lesub_def + split: option.splits) + +end
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Sat Jan 06 21:31:37 2001 +0100 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Sun Jan 07 18:43:13 2001 +0100 @@ -313,4 +313,4 @@ by blast qed -end \ No newline at end of file +end
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Sat Jan 06 21:31:37 2001 +0100 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy Sun Jan 07 18:43:13 2001 +0100 @@ -62,6 +62,8 @@ wf_prog (\<lambda>G C (sig,rT,maxs,maxl,b). wtl_method G C (snd sig) rT maxs maxl b (cert C sig)) G" +lemmas [iff] = not_Err_eq + lemma wtl_inst_OK: "(wtl_inst i G rT s cert maxs max_pc pc = OK s') = @@ -78,7 +80,7 @@ "wtl_inst_list (i#is) G rT cert maxs max_pc pc s \<noteq> Err = (\<exists>s'. wtl_cert i G rT s cert maxs max_pc pc = OK s' \<and> wtl_inst_list is G rT cert maxs max_pc (pc+1) s' \<noteq> Err)" -by (auto simp del: split_paired_Ex) + by (auto simp del: split_paired_Ex) lemma wtl_append: "\<forall> s pc. (wtl_inst_list (a@b) G rT cert mxs mpc pc s = OK s') =
--- a/src/HOL/MicroJava/BV/Step.thy Sat Jan 06 21:31:37 2001 +0100 +++ b/src/HOL/MicroJava/BV/Step.thy Sun Jan 07 18:43:13 2001 +0100 @@ -7,7 +7,7 @@ header {* Effect of instructions on the state type *} -theory Step = Convert: +theory Step = JVMType + JVMExec: text "Effect of instruction on the state type:"
--- a/src/HOL/MicroJava/BV/StepMono.thy Sat Jan 06 21:31:37 2001 +0100 +++ b/src/HOL/MicroJava/BV/StepMono.thy Sun Jan 07 18:43:13 2001 +0100 @@ -20,12 +20,12 @@ show "?P []" by simp case Cons - show "?P (a#list)" - proof (clarsimp simp add: list_all2_Cons1 sup_loc_def) + show "?P (a#list)" + proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def) fix z zs n assume * : "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs" - "n < Suc (length zs)" "(z # zs) ! n = OK t" + "n < Suc (length list)" "(z # zs) ! n = OK t" show "(\<exists>t. (a # list) ! n = OK t) \<and> G \<turnstile>(a # list) ! n <=o OK t" proof (cases n) @@ -34,9 +34,9 @@ next case Suc with Cons * - show ?thesis by (simp add: sup_loc_def) + show ?thesis by (simp add: sup_loc_def Listn.le_def lesub_def) qed - qed + qed qed @@ -116,6 +116,7 @@ qed qed +lemmas [iff] = not_Err_eq lemma app_mono: "[|G \<turnstile> s <=' s'; app i G m rT s'|] ==> app i G m rT s" @@ -125,27 +126,22 @@ assume G: "G \<turnstile> s2 <=s s1" assume app: "app i G m rT (Some s1)" - (* - from G - have l: "length (fst s2) = length (fst s1)" - by simp - *) - have "app i G m rT (Some s2)" proof (cases (open) i) case Load from G Load app - have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def) + have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_conv) with G Load app - show ?thesis by clarsimp (drule sup_loc_some, simp+) + show ?thesis + by clarsimp (drule sup_loc_some, simp+) next case Store with G app show ?thesis by - (cases s2, auto simp add: map_eq_Cons sup_loc_Cons2 - sup_loc_length sup_state_def) + sup_loc_length sup_state_conv) next case Bipush with G app @@ -283,7 +279,7 @@ from G' have "G \<turnstile> map OK apTs' <=l map OK apTs" - by (simp add: sup_state_def) + by (simp add: sup_state_conv) also from l w have "G \<turnstile> map OK apTs <=l map OK list" @@ -345,19 +341,19 @@ y': "nat < length b2" "b2 ! nat = OK y'" by clarsimp from G s - have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_def) + have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_conv) with y y' have "G \<turnstile> y \<preceq> y'" by - (drule sup_loc_some, simp+) with Load G y y' s step app1 app2 - show ?thesis by (clarsimp simp add: sup_state_def) + show ?thesis by (clarsimp simp add: sup_state_conv) next case Store with G s step app1 app2 show ?thesis - by (clarsimp simp add: sup_state_def sup_loc_update) + by (clarsimp simp add: sup_state_conv sup_loc_update) next case Bipush with G s step app1 app2 @@ -421,7 +417,7 @@ with Invoke G s step app1 app2 s1 s2 l l' show ?thesis - by (clarsimp simp add: sup_state_def) + by (clarsimp simp add: sup_state_conv) next case Return with G step @@ -478,6 +474,7 @@ by (cases s1, cases s2, auto dest: step_mono_Some) lemmas [simp del] = step_def +lemmas [iff del] = not_Err_eq end