--- a/src/HOL/MicroJava/BV/BVSpec.ML Mon Aug 07 10:29:54 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: HOL/MicroJava/BV/BVSpec.ML
- ID: $Id$
- Author: Cornelia Pusch
- Copyright 1999 Technische Universitaet Muenchen
-*)
-
-Goalw [wt_jvm_prog_def] "wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)";
-by(Blast_tac 1);
-qed "wt_jvm_progD";
-
-
-Goalw [wt_jvm_prog_def]
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ pc < length ins \\<rbrakk> \
-\\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
-by(forward_tac [rotate_prems 2 method_wf_mdecl] 1);
- by (Asm_full_simp_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
-qed "wt_jvm_prog_impl_wt_instr";
-
-Goalw [wt_jvm_prog_def]
-"\\<lbrakk> wt_jvm_prog G phi; \
-\ method (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow> \
-\ 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)";
-by(forward_tac [rotate_prems 2 method_wf_mdecl] 1);
- by (Asm_full_simp_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [wf_mdecl_def,wt_method_def]) 1);
-qed "wt_jvm_prog_impl_wt_start";
--- a/src/HOL/MicroJava/BV/BVSpec.thy Mon Aug 07 10:29:54 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Mon Aug 07 14:32:56 2000 +0200
@@ -6,173 +6,58 @@
Specification of bytecode verifier
*)
-BVSpec = Convert +
+theory BVSpec = Step :
types
- method_type = "state_type list"
- class_type = "sig \\<Rightarrow> method_type"
- prog_type = "cname \\<Rightarrow> class_type"
-
-consts
-wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool"
-
-primrec
-"wt_instr (Load idx) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- idx < length LT \\<and>
- (\\<exists>ts. (LT ! idx) = Some ts \\<and>
- G \\<turnstile> (ts # ST , LT) <=s phi ! (pc+1)))"
-
-"wt_instr (Store idx) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- idx < length LT \\<and>
- (\\<exists>ts ST'. ST = ts # ST' \\<and>
- G \\<turnstile> (ST' , LT[idx:=Some ts]) <=s phi ! (pc+1)))"
-
-"wt_instr (Bipush i) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- G \\<turnstile> ((PrimT Integer) # ST , LT) <=s phi ! (pc+1))"
-
-"wt_instr (Aconst_null) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- G \\<turnstile> (NT # ST , LT) <=s phi ! (pc+1))"
-
-"wt_instr (Getfield F C) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- is_class G C \\<and>
- (\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and>
- ST = oT # ST' \\<and>
- G \\<turnstile> oT \\<preceq> (Class C) \\<and>
- G \\<turnstile> (T # ST' , LT) <=s phi ! (pc+1)))"
-
-"wt_instr (Putfield F C) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- is_class G C \\<and>
- (\\<exists>T vT oT ST'.
- field (G,C) F = Some(C,T) \\<and>
- ST = vT # oT # ST' \\<and>
- G \\<turnstile> oT \\<preceq> (Class C) \\<and>
- G \\<turnstile> vT \\<preceq> T \\<and>
- G \\<turnstile> (ST' , LT) <=s phi ! (pc+1)))"
-
-"wt_instr (New C) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- is_class G C \\<and>
- G \\<turnstile> ((Class C) # ST , LT) <=s phi ! (pc+1))"
-
-"wt_instr (Checkcast C) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- is_class G C \\<and>
- (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
- G \\<turnstile> (Class C # ST' , LT) <=s phi ! (pc+1)))"
-
-"wt_instr Pop G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- \\<exists>ts ST'. pc+1 < max_pc \\<and>
- ST = ts # ST' \\<and>
- G \\<turnstile> (ST' , LT) <=s phi ! (pc+1))"
-
-"wt_instr Dup G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ts ST'. ST = ts # ST' \\<and>
- G \\<turnstile> (ts # ts # ST' , LT) <=s phi ! (pc+1)))"
-
-"wt_instr Dup_x1 G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and>
- G \\<turnstile> (ts1 # ts2 # ts1 # ST' , LT) <=s phi ! (pc+1)))"
-
-"wt_instr Dup_x2 G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and>
- G \\<turnstile> (ts1 # ts2 # ts3 # ts1 # ST' , LT) <=s phi ! (pc+1)))"
-
-"wt_instr Swap G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
- G \\<turnstile> (ts # ts' # ST' , LT) <=s phi ! (pc+1)))"
-
-"wt_instr IAdd G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\<and>
- G \\<turnstile> ((PrimT Integer) # ST' , LT) <=s phi ! (pc+1)))"
-
-"wt_instr (Ifcmpeq branch) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and>
- (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>
- ((\\<exists>p. ts = PrimT p \\<and> ts' = PrimT p) \\<or>
- (\\<exists>r r'. ts = RefT r \\<and> ts' = RefT r')) \\<and>
- G \\<turnstile> (ST' , LT) <=s phi ! (pc+1) \\<and>
- G \\<turnstile> (ST' , LT) <=s phi ! (nat(int pc+branch))))"
-
-"wt_instr (Goto branch) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- (nat(int pc+branch)) < max_pc \\<and>
- G \\<turnstile> (ST , LT) <=s phi ! (nat(int pc+branch)))"
-
-"wt_instr (Invoke mn fpTs) G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- pc+1 < max_pc \\<and>
- (\\<exists>apTs X ST'. ST = (rev apTs) @ (X # ST') \\<and>
- length apTs = length fpTs \\<and>
- (X = NT \\<or> (\\<exists>C. X = Class C \\<and>
- (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
- (\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
- G \\<turnstile> (rT # ST' , LT) <=s phi ! (pc+1))))))"
-
-"wt_instr Return G rT phi max_pc pc =
- (let (ST,LT) = phi ! pc
- in
- (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))"
-
+ method_type = "state_type list"
+ class_type = "sig \\<Rightarrow> method_type"
+ prog_type = "cname \\<Rightarrow> class_type"
constdefs
- wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
- "wt_start G C pTs mxl phi \\<equiv>
+wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \\<Rightarrow> bool"
+"wt_instr i G rT phi max_pc pc \\<equiv>
+ app (i, G, rT, phi!pc) \\<and>
+ (\\<forall> pc' \\<in> (succs i pc). pc' < max_pc \\<and> (G \\<turnstile> the (step (i, G, phi!pc)) <=s phi!pc'))"
+
+wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
+"wt_start G C pTs mxl phi \\<equiv>
G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0"
- wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
- "wt_method G C pTs rT mxl ins phi \\<equiv>
+wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
+"wt_method G C pTs rT mxl ins phi \\<equiv>
let max_pc = length ins
in
length ins < length phi \\<and> 0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and>
(\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
- wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool"
+wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool"
"wt_jvm_prog G phi \\<equiv>
wf_prog (\\<lambda>G C (sig,rT,maxl,b).
wt_method G C (snd sig) rT maxl b (phi C sig)) G"
+lemma wt_jvm_progD:
+"wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)"
+by (unfold wt_jvm_prog_def, blast)
+
+lemma wt_jvm_prog_impl_wt_instr:
+"\\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \\<rbrakk>
+ \\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
+by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
+ simp, simp add: wf_mdecl_def wt_method_def)
+
+lemma wt_jvm_prog_impl_wt_start:
+"\\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow>
+ 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)"
+by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
+ simp, simp add: wf_mdecl_def wt_method_def)
+
+lemma [simp]:
+"succs i pc = {pc+1} \\<Longrightarrow> wt_instr i G rT phi max_pc pc =
+ (app (i, G, rT, phi!pc) \\<and> pc+1 < max_pc \\<and>
+ (G \\<turnstile> the (step (i, G, phi!pc)) <=s phi!(pc+1)))"
+by (simp add: wt_instr_def)
+
end
+
+
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Aug 07 10:29:54 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML Mon Aug 07 14:32:56 2000 +0200
@@ -5,7 +5,7 @@
*)
val defs1 = exec.simps@[split_def,sup_state_def,correct_state_def,
- correct_frame_def];
+ correct_frame_def, thm "wt_instr_def"];
Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
"\\<lbrakk> wt_jvm_prog G phi; \
@@ -13,15 +13,16 @@
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
by (Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [wt_jvm_prog_impl_wt_instr]) 1);
+by(blast_tac (claset() addIs [thm "wt_jvm_prog_impl_wt_instr"]) 1);
qed "wt_jvm_prog_impl_wt_instr_cor";
-Delsimps [split_paired_All];
+Delsimps [split_paired_All];
(******* LS *******)
+
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -30,11 +31,13 @@
\ 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> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
+by (case_tac "phi C sig!pc" 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
qed "Load_correct";
+
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -47,6 +50,7 @@
addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
qed "Store_correct";
+
Goalw [conf_def] "G,h \\<turnstile> Intg i \\<Colon>\\<preceq> PrimT Integer";
by(Simp_tac 1);
qed "conf_Intg_Integer";
@@ -60,6 +64,7 @@
\ 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> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
+by (case_tac "phi C sig ! pc" 1);
by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_val_def,sup_PTS_eq,map_eq_Cons]@defs1)) 1);
qed "Bipush_correct";
@@ -84,12 +89,12 @@
\ 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> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
+by (case_tac "phi C sig ! pc" 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,map_eq_Cons]@defs1)) 1);
qed "Aconst_null_correct";
-
Goalw [cast_ok_def]
"\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G C h v ; G\\<turnstile>Class C\\<preceq>T; is_class G C \\<rbrakk> \
\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T";
@@ -118,7 +123,6 @@
addss (simpset() addsimps [map_eq_Cons,approx_val_def])) 1);
qed "Checkcast_correct";
-
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -138,16 +142,16 @@
ba 1;
bd conf_RefTD 1;
by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
br conjI 1;
bd widen_cfs_fields 1;
ba 1;
ba 1;
- by(fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1);
+ by (fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1);
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]) 1);
+qed "Getfield_correct";
-qed "Getfield_correct";
Goal
@@ -174,7 +178,6 @@
correct_frames_imp_correct_frames_field_update,conf_widen] addss (simpset())) 1);
qed "Putfield_correct";
-
Goal "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)";
by(Fast_tac 1);
qed "collapse_paired_All";
@@ -187,6 +190,7 @@
\ 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> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
+by (case_tac "phi C sig ! pc" 1);
by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,
approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
@@ -198,88 +202,105 @@
qed "New_correct";
+
+Delsimps (thms "app.simps");
+
(****** Method Invocation ******)
Goal
"\\<lbrakk> wt_jvm_prog G phi; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
-\ ins ! pc = Invoke mn pTs; \
+\ ins ! pc = Invoke C' mn pTs; \
\ wt_instr (ins!pc) G rT (phi C sig) (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> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_progD] 1);
+by(case_tac "phi C sig ! pc" 1);
+by(forward_tac [thm "wt_jvm_progD"] 1);
by(etac exE 1);
by(asm_full_simp_tac (simpset() addsimps defs1) 1);
by(Clarify_tac 1);
-by(case_tac "X\\<noteq>NT" 1);
- by (asm_full_simp_tac (simpset()addsimps[raise_xcpt_def]@defs1
- addsplits [option.split]) 1);
- by (Clarify_tac 1);
- by (asm_full_simp_tac (simpset() addsimps defs1) 1);
- bd approx_stk_append_lemma 1;
- by (Clarify_tac 1);
- by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
- bd conf_RefTD 1;
- by (Clarify_tac 1);
- by(rename_tac "oloc oT ofs T'" 1);
- by (asm_full_simp_tac (simpset() addsimps defs1) 1);
- bd subtype_widen_methd 1;
- ba 1;
+by(asm_full_simp_tac (simpset() addsimps [raise_xcpt_def] addsplits [option.split]) 1);
+by(Clarify_tac 1);
+bd approx_stk_append_lemma 1;
+by(clarsimp_tac (claset(), simpset() addsimps [approx_val_def]) 1);
+
+by (subgoal_tac "\\<exists> D'. X = Class D'" 1);
+ bd widen_RefT2 2;
+ by (Clarsimp_tac 2);
+ bd conf_RefTD 2;
+ by (Clarsimp_tac 2);
+ bd widen_Class 2;
+ by (Clarsimp_tac 2);
+
+by (Clarsimp_tac 1);
+bd conf_RefTD 1;
+by (Clarify_tac 1);
+by(rename_tac "oloc oT ofs T'" 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by (subgoal_tac "G\\<turnstile>oT\\<preceq>C C'" 1);
+ bd widen.subcls 2;
+ bd widen.subcls 2;
+ by (((dtac widen_trans) THEN' atac THEN' Blast_tac) 2);
+bd subtype_widen_methd 1;
ba 1;
- be exE 1;
- by(rename_tac "oT'" 1);
- by (Clarify_tac 1);
- by(subgoal_tac "G \\<turnstile> oT \\<preceq>C oT'" 1);
- by(forw_inst_tac [("C","oT")](standard(rotate_prems 1 method_wf_mdecl)) 2);
- ba 2;
- by(Blast_tac 2);
- by (asm_full_simp_tac (simpset() addsimps defs1) 1);
- by(forward_tac [method_in_md] 1);
+ ba 1;
+by (Clarify_tac 1);
+bd subtype_widen_methd 1;
ba 1;
- back();
- back();
- by (Clarify_tac 1);
- by (asm_full_simp_tac (simpset() addsimps defs1) 1);
- by (forward_tac [wt_jvm_prog_impl_wt_start] 1);
- ba 1;
- back();
- by (asm_full_simp_tac (simpset() addsimps [wt_start_def,sup_state_def]) 1);
- by (Clarify_tac 1);
+ ba 1;
+be exE 1;
+by(rename_tac "oT'" 1);
+by (Clarify_tac 1);
+by(subgoal_tac "G \\<turnstile> oT \\<preceq>C oT'" 1);
+ by(forw_inst_tac [("C","oT")] method_wf_mdecl 2);
+ ba 2;
+ by (Blast_tac 2);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by(forward_tac [method_in_md] 1);
+ ba 1;
+ back();
+ back();
+ back();
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps defs1) 1);
+by (forward_tac [thm "wt_jvm_prog_impl_wt_start"] 1);
+ ba 1;
+ back();
+by (asm_full_simp_tac (simpset() addsimps [thm "wt_start_def",sup_state_def]) 1);
+by (Clarify_tac 1);
(** approx_loc **)
+br conjI 1;
+ br approx_loc_imp_approx_loc_sup 1;
+ ba 1;
+ by (Fast_tac 2);
+ by (asm_full_simp_tac (simpset() addsimps [split_def,approx_val_def,approx_loc_append]) 1);
br conjI 1;
- br approx_loc_imp_approx_loc_sup 1;
+ br conf_widen 1;
ba 1;
by (Fast_tac 2);
- by (asm_full_simp_tac (simpset() addsimps [split_def,approx_val_def,approx_loc_append]) 1);
- br conjI 1;
- br conf_widen 1;
- ba 1;
- by (Fast_tac 2);
- by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
- br conjI 1;
- by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)]
- addss (simpset() addsimps [split_def,approx_val_def])) 1);
- by (asm_simp_tac (simpset() addsimps [list_all2_def,split_def,approx_loc_def,approx_val_None,set_replicate_conv_if]) 1);
-
+ by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
br conjI 1;
- by (asm_simp_tac (simpset() addsimps [min_def]) 1);
- br exI 1;
- br exI 1;
- br conjI 1;
- by(Blast_tac 1);
- by (fast_tac (claset()
- addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
- addss (simpset()addsimps [map_eq_Cons])) 1);
-by (Asm_full_simp_tac 1);
-bd approx_stk_append_lemma 1;
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [approx_val_def, raise_xcpt_def]) 1);
-bd conf_NullTD 1;
-by (Asm_simp_tac 1);
+ by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)]
+ addss (simpset() addsimps [split_def,approx_val_def])) 1);
+ by (asm_simp_tac (simpset() addsimps [list_all2_def,split_def,approx_loc_def,approx_val_None,set_replicate_conv_if]) 1);
+
+br conjI 1;
+ by (asm_simp_tac (simpset() addsimps [min_def]) 1);
+br exI 1;
+br exI 1;
+br conjI 1;
+ by(Blast_tac 1);
+by (Clarsimp_tac 1);
+
+by (fast_tac (claset()
+ addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
+ addss (simpset()addsimps [map_eq_Cons])) 1);
qed "Invoke_correct";
+Addsimps (thms "app.simps");
+
Delsimps [map_append];
Goal
@@ -295,9 +316,10 @@
by (asm_full_simp_tac (simpset() addsimps [map_eq_Cons]@defs1) 1);
by (Clarify_tac 1);
by (asm_full_simp_tac (simpset() addsimps defs1) 1);
-by (forward_tac [wt_jvm_prog_impl_wt_instr] 1);
+by (forward_tac [thm "wt_jvm_prog_impl_wt_instr"] 1);
by(EVERY1[atac, etac Suc_lessD]);
-by(rewtac wt_jvm_prog_def);
+by(rewtac (thm "wt_jvm_prog_def"));
+by (case_tac "phi ab (ac, b) ! k" 1);
by (fast_tac (claset()
addDs [subcls_widen_methd]
addEs [rotate_prems 1 widen_trans]
@@ -307,6 +329,7 @@
Addsimps [map_append];
+
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -329,7 +352,7 @@
\ G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
-qed "Ifiacmpeq_correct";
+qed "Ifcmpeq_correct";
Goal
@@ -357,6 +380,7 @@
qed "Dup_correct";
+
Goal
"\\<lbrakk> wf_prog wt G; \
\ method (G,C) sig = Some (C,rT,maxl,ins); \
@@ -407,6 +431,7 @@
qed "IAdd_correct";
+
(** instr correct **)
Goal
@@ -421,11 +446,11 @@
by(case_tac "ins!pc" 1);
by(fast_tac (claset() addIs [Invoke_correct]) 9);
by(fast_tac (claset() addIs [Return_correct]) 9);
-by(rewtac wt_jvm_prog_def);
+by(rewtac (thm "wt_jvm_prog_def"));
by (ALLGOALS (fast_tac (claset() addIs
[Load_correct,Store_correct,Bipush_correct,Aconst_null_correct,
Checkcast_correct,Getfield_correct,Putfield_correct,New_correct,
- Goto_correct,Ifiacmpeq_correct,Pop_correct,Dup_correct,
+ Goto_correct,Ifcmpeq_correct,Pop_correct,Dup_correct,
Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct])));
qed "instr_correct";
--- a/src/HOL/MicroJava/BV/Correct.thy Mon Aug 07 10:29:54 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy Mon Aug 07 14:32:56 2000 +0200
@@ -34,7 +34,7 @@
in
(\\<exists>rT maxl ins.
method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and>
- (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = (Invoke mn pTs) \\<and>
+ (\\<exists>C' mn pTs k. pc = k+1 \\<and> ins!k = (Invoke C' mn pTs) \\<and>
(mn,pTs) = sig0 \\<and>
(\\<exists>apTs D ST'.
fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Mon Aug 07 10:29:54 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Mon Aug 07 14:32:56 2000 +0200
@@ -6,10 +6,12 @@
header {* Completeness of the LBV *}
-theory LBVComplete = LBVSpec:;
+theory LBVComplete = BVSpec + LBVSpec:
+
-ML_setup {* bind_thm ("widen_RefT", widen_RefT) *};
-ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *};
+ML_setup {* bind_thm ("widen_RefT", widen_RefT) *}
+ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *}
+
constdefs
is_approx :: "['a option list, 'a list] \\<Rightarrow> bool"
@@ -18,14 +20,14 @@
contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
"contains_dead ins cert phi pc \\<equiv>
- (((\\<exists> branch. ins!pc = (Goto branch)) \\<or> ins!pc = Return) \\<or>
- (\\<exists>m l. ins!pc = Invoke m l)) \\<longrightarrow> Suc pc < length phi \\<longrightarrow>
- cert ! (Suc pc) = Some (phi ! Suc pc)"
+ Suc pc \\<notin> succs (ins!pc) pc \\<and> Suc pc < length phi \\<longrightarrow>
+ cert ! (Suc pc) = Some (phi ! Suc pc)"
contains_targets :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
- "contains_targets ins cert phi pc \\<equiv>
- \\<forall> branch. (ins!pc = (Goto branch) \\<or> ins!pc = (Ifcmpeq branch)) \\<longrightarrow>
- (let pc' = nat (int pc+branch) in pc' < length phi \\<longrightarrow> cert!pc' = Some (phi!pc'))"
+ "contains_targets ins cert phi pc \\<equiv> (
+ \\<forall> pc' \\<in> succs (ins!pc) pc. pc' \\<noteq> Suc pc \\<and> pc' < length phi \\<longrightarrow>
+ cert!pc' = Some (phi!pc'))"
+
fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
"fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and>
@@ -34,28 +36,21 @@
contains_targets ins cert phi pc)"
is_target :: "[instr list, p_count] \\<Rightarrow> bool"
- "is_target ins pc \\<equiv>
- \\<exists> pc' branch. pc' < length ins \\<and>
- (ins ! pc' = (Ifcmpeq branch) \\<or> ins ! pc' = (Goto branch)) \\<and>
- pc = (nat(int pc'+branch))"
-
+ "is_target ins pc \\<equiv> \\<exists> pc'. pc' < length ins \\<and> pc \\<in> succs (ins!pc') pc'"
+
maybe_dead :: "[instr list, p_count] \\<Rightarrow> bool"
- "maybe_dead ins pc \\<equiv>
- \\<exists> pc'. pc = pc'+1 \\<and> ((\\<exists> branch. ins!pc' = (Goto branch)) \\<or>
- ins!pc' = Return \\<or>
- (\\<exists>m l. ins!pc' = Invoke m l))"
-
+ "maybe_dead ins pc \\<equiv> \\<exists> pc'. pc = pc'+1 \\<and> pc \\<notin> succs (ins!pc') pc'"
mdot :: "[instr list, p_count] \\<Rightarrow> bool"
- "mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc";
+ "mdot ins pc \\<equiv> maybe_dead ins pc \\<or> is_target ins pc"
consts
- option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list";
+ option_filter_n :: "['a list, nat \\<Rightarrow> bool, nat] \\<Rightarrow> 'a option list"
primrec
"option_filter_n [] P n = []"
"option_filter_n (h#t) P n = (if (P n) then Some h # option_filter_n t P (n+1)
- else None # option_filter_n t P (n+1))";
+ else None # option_filter_n t P (n+1))"
constdefs
option_filter :: "['a list, nat \\<Rightarrow> bool] \\<Rightarrow> 'a option list"
@@ -68,678 +63,267 @@
"make_Cert G Phi \\<equiv> \\<lambda> C sig.
let (C,x,y,mdecls) = \\<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \\<in> set G \\<and> Cl = C in
let (sig,rT,maxl,b) = \\<epsilon> (sg,rT,maxl,b). (sg,rT,maxl,b) \\<in> set mdecls \\<and> sg = sig in
- make_cert b (Phi C sig)";
+ make_cert b (Phi C sig)"
-lemma length_ofn: "\\<forall>n. length (option_filter_n l P n) = length l";
- by (induct l) auto;
+lemma length_ofn: "\\<forall>n. length (option_filter_n l P n) = length l"
+ by (induct l) auto
lemma is_approx_option_filter_n:
-"\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a");
-proof (induct a);
- show "?P []"; by (auto simp add: is_approx_def);
+"\\<forall>n. is_approx (option_filter_n a P n) a" (is "?P a")
+proof (induct a)
+ show "?P []" by (auto simp add: is_approx_def)
- fix l ls;
- assume Cons: "?P ls";
+ fix l ls
+ assume Cons: "?P ls"
- show "?P (l#ls)";
- proof (unfold is_approx_def, intro allI conjI impI);
- fix n;
- show "length (option_filter_n (l # ls) P n) = length (l # ls)";
- by (simp only: length_ofn);
+ show "?P (l#ls)"
+ proof (unfold is_approx_def, intro allI conjI impI)
+ fix n
+ show "length (option_filter_n (l # ls) P n) = length (l # ls)"
+ by (simp only: length_ofn)
- fix m;
- assume "m < length (option_filter_n (l # ls) P n)";
- hence m: "m < Suc (length ls)"; by (simp only: length_ofn) simp;
+ fix m
+ assume "m < length (option_filter_n (l # ls) P n)"
+ hence m: "m < Suc (length ls)" by (simp only: length_ofn) simp
show "option_filter_n (l # ls) P n ! m = None \\<or>
- option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)";
- proof (cases "m");
- assume "m = 0";
- with m; show ?thesis; by simp;
- next;
- fix m'; assume Suc: "m = Suc m'";
- from Cons;
- show ?thesis;
- proof (unfold is_approx_def, elim allE impE conjE);
- from m Suc;
- show "m' < length (option_filter_n ls P (Suc n))"; by (simp add: length_ofn);
+ option_filter_n (l # ls) P n ! m = Some ((l # ls) ! m)"
+ proof (cases "m")
+ assume "m = 0"
+ with m show ?thesis by simp
+ next
+ fix m' assume Suc: "m = Suc m'"
+ from Cons
+ show ?thesis
+ proof (unfold is_approx_def, elim allE impE conjE)
+ from m Suc
+ show "m' < length (option_filter_n ls P (Suc n))" by (simp add: length_ofn)
assume "option_filter_n ls P (Suc n) ! m' = None \\<or>
- option_filter_n ls P (Suc n) ! m' = Some (ls ! m')";
- with m Suc;
- show ?thesis; by auto;
- qed;
- qed;
- qed;
-qed;
-
-lemma is_approx_option_filter: "is_approx (option_filter l P) l";
- by (simp add: option_filter_def is_approx_option_filter_n);
-
-lemma option_filter_Some:
-"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)";
-proof -;
-
- assume 1: "n < length l" "P n";
-
- have "\\<forall>n n'. n < length l \\<longrightarrow> P (n+n') \\<longrightarrow> option_filter_n l P n' ! n = Some (l!n)"
- (is "?P l");
- proof (induct l);
- show "?P []"; by simp;
-
- fix l ls; assume Cons: "?P ls";
- show "?P (l#ls)";
- proof (intro);
- fix n n';
- assume l: "n < length (l # ls)";
- assume P: "P (n + n')";
- show "option_filter_n (l # ls) P n' ! n = Some ((l # ls) ! n)";
- proof (cases "n");
- assume "n=0";
- with P; show ?thesis; by simp;
- next;
- fix m; assume "n = Suc m";
- with l P Cons;
- show ?thesis; by simp;
- qed;
- qed;
- qed;
-
- with 1;
- show ?thesis; by (auto simp add: option_filter_def);
-qed;
-
-lemma option_filter_contains_dead:
-"contains_dead ins (option_filter phi (mdot ins)) phi pc";
- by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def);
-
-lemma option_filter_contains_targets:
-"pc < length ins \\<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc";
-proof (simp add: contains_targets_def, intro allI impI conjI);
-
- fix branch;
- assume 1: "ins ! pc = Goto branch"
- "nat (int pc + branch) < length phi"
- "pc < length ins";
-
- show "option_filter phi (mdot ins) ! nat (int pc + branch) = Some (phi ! nat (int pc + branch))";
- proof (rule option_filter_Some);
- from 1; show "nat (int pc + branch) < length phi"; by simp;
- from 1;
- have "is_target ins (nat (int pc + branch))"; by (auto simp add: is_target_def);
- thus "mdot ins (nat (int pc + branch))"; by (simp add: mdot_def);
- qed;
-
-next;
- fix branch;
- assume 2: "ins ! pc = Ifcmpeq branch"
- "nat (int pc + branch) < length phi"
- "pc < length ins";
-
- show "option_filter phi (mdot ins) ! nat (int pc + branch) = Some (phi ! nat (int pc + branch))";
- proof (rule option_filter_Some);
- from 2; show "nat (int pc + branch) < length phi"; by simp;
- from 2;
- have "is_target ins (nat (int pc + branch))"; by (auto simp add: is_target_def);
- thus "mdot ins (nat (int pc + branch))"; by (simp add: mdot_def);
- qed;
-
-qed;
-
-
-lemma fits_make_cert:
- "length ins < length phi \\<Longrightarrow> fits ins (make_cert ins phi) phi";
-proof -;
- assume l: "length ins < length phi";
-
- thus "fits ins (make_cert ins phi) phi";
- proof (unfold fits_def make_cert_def, intro conjI allI impI);
- show "is_approx (option_filter phi (mdot ins)) phi"; by (rule is_approx_option_filter);
- show "length ins < length phi"; .;
-
- fix pc;
- show "contains_dead ins (option_filter phi (mdot ins)) phi pc"; by (rule option_filter_contains_dead);
-
- assume "pc < length ins";
- thus "contains_targets ins (option_filter phi (mdot ins)) phi pc"; by (rule option_filter_contains_targets);
- qed;
-qed;
-
-
-
-lemma append_length_n: "\\<forall>n. n \\<le> length x \\<longrightarrow> (\\<exists>a b. x = a@b \\<and> length a = n)" (is "?P x");
-proof (induct "?P" "x");
- show "?P []"; by simp;
-
- fix l ls; assume Cons: "?P ls";
-
- show "?P (l#ls)";
- proof (intro allI impI);
- fix n;
- assume l: "n \\<le> length (l # ls)";
-
- show "\\<exists>a b. l # ls = a @ b \\<and> length a = n";
- proof (cases n);
- assume "n=0"; thus ?thesis; by simp;
- next;
- fix "n'"; assume s: "n = Suc n'";
- with l;
- have "n' \\<le> length ls"; by simp;
- hence "\\<exists>a b. ls = a @ b \\<and> length a = n'"; by (rule Cons [rulify]);
- thus ?thesis;
- proof elim;
- fix a b;
- assume "ls = a @ b" "length a = n'";
- with s;
- have "l # ls = (l#a) @ b \\<and> length (l#a) = n"; by simp;
- thus ?thesis; by blast;
- qed;
- qed;
- qed;
-qed;
-
-
-
-lemma rev_append_cons:
-"\\<lbrakk>n < length x\\<rbrakk> \\<Longrightarrow> \\<exists>a b c. x = (rev a) @ b # c \\<and> length a = n";
-proof -;
- assume n: "n < length x";
- hence "n \\<le> length x"; by simp;
- hence "\\<exists>a b. x = a @ b \\<and> length a = n"; by (rule append_length_n [rulify]);
- thus ?thesis;
- proof elim;
- fix r d; assume x: "x = r@d" "length r = n";
- with n;
- have "\\<exists>b c. d = b#c"; by (simp add: neq_Nil_conv);
-
- thus ?thesis;
- proof elim;
- fix b c;
- assume "d = b#c";
- with x;
- have "x = (rev (rev r)) @ b # c \\<and> length (rev r) = n"; by simp;
- thus ?thesis; by blast;
- qed;
- qed;
-qed;
-
-lemma widen_NT: "G \\<turnstile> b \\<preceq> NT \\<Longrightarrow> b = NT";
-proof (cases b);
- case RefT;
- thus "G\\<turnstile>b\\<preceq>NT \\<Longrightarrow> b = NT"; by - (cases ref_ty, auto);
-qed auto;
-
-lemma widen_Class: "G \\<turnstile> b \\<preceq> Class C \\<Longrightarrow> \\<exists>r. b = RefT r";
-by (cases b) auto;
-
-lemma all_widen_is_sup_loc:
-"\\<forall>b. length a = length b \\<longrightarrow> (\\<forall>x\\<in>set (zip a b). x \\<in> widen G) = (G \\<turnstile> (map Some a) <=l (map Some b))"
- (is "\\<forall>b. length a = length b \\<longrightarrow> ?Q a b" is "?P a");
-proof (induct "a");
- show "?P []"; by simp;
-
- fix l ls; assume Cons: "?P ls";
-
- show "?P (l#ls)";
- proof (intro allI impI);
- fix b;
- assume "length (l # ls) = length (b::ty list)";
- with Cons;
- show "?Q (l # ls) b"; by - (cases b, auto);
- qed;
-qed;
-
-lemma method_inv_pseudo_mono:
-"\\<lbrakk>fits ins cert phi; i = ins!pc; i = Invoke mname list; pc < length ins;
- wf_prog wf_mb G; G \\<turnstile> (x, y) <=s s1; wtl_inst (ins!pc) G rT s1 s1' cert mpc pc\\<rbrakk>
- \\<Longrightarrow> \\<exists>s2'. wtl_inst i G rT (x, y) s2' cert mpc pc \\<and> \
- ((G \\<turnstile> s2' <=s s1') \\<or> (\\<exists> s. cert ! (Suc pc) = Some s \\<and> (G \\<turnstile> s2' <=s s)))";
-proof -
- assume fits: "fits ins cert phi" and
- i: "i = ins ! pc" "i = Invoke mname list" and
- pc: "pc < length ins" and
- wfp: "wf_prog wf_mb G" and
- "wtl_inst (ins!pc) G rT s1 s1' cert mpc pc" and
- lt: "G \\<turnstile> (x, y) <=s s1";
-
- thus ?thesis
- proof (clarsimp_tac simp del: split_paired_Ex)
- fix apTs X ST' y' s;
-
- assume G: "G \\<turnstile> (x, y) <=s (rev apTs @ X # ST', y')";
- assume lapTs: "length apTs = length list";
- assume "cert ! Suc pc = Some s";
- assume wtl: "s = s1' \\<and> X = NT \\<or>
- G \\<turnstile> s1' <=s s \\<and>
- (\\<exists>C. X = Class C \\<and>
- (\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G) \\<and>
- (\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and>
- (rT # ST', y') = s1'))" (is "?NT \\<or> ?ClassC");
-
- from G;
- have "\\<exists>a b c. x = rev a @ b # c \\<and> length a = length apTs";
- by - (rule rev_append_cons, simp add: sup_state_length_fst);
-
- thus "\\<exists>s2'. (\\<exists>apTs X ST'.
- x = rev apTs @ X # ST' \\<and>
- length apTs = length list \\<and>
- (s = s2' \\<and> X = NT \\<or>
- G \\<turnstile> s2' <=s s \\<and>
- (\\<exists>C. X = Class C \\<and>
- (\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G) \\<and>
- (\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and>
- (rT # ST', y) = s2')))) \\<and>
- (G \\<turnstile> s2' <=s s1' \\<or> G \\<turnstile> s2' <=s s)" (is "\\<exists>s2'. ?P s2'");
- proof elim;
- fix a b c;
- assume rac: "x = rev a @ b # c";
- with G;
- have x: "G \\<turnstile> (rev a @ b # c, y) <=s (rev apTs @ X # ST', y')"; by simp;
-
- assume l: "length a = length apTs";
- hence "length (rev a) = length (rev apTs)"; by simp;
-
- with x;
- have "G \\<turnstile> (rev a, y) <=s (rev apTs, y') \\<and> G \\<turnstile> (b # c, y) <=s (X # ST', y')";
- by - (rule sup_state_append_fst [elimify], blast+);
-
- hence x2: "G \\<turnstile> (a, y) <=s (apTs, y') \\<and> G \\<turnstile> b\\<preceq>X \\<and> G \\<turnstile> (c, y) <=s (ST', y')";
- by (simp add: sup_state_rev_fst sup_state_Cons1);
-
- show ?thesis
- proof (cases "X = NT");
- case True;
- with x2;
- have "b = NT"; by (clarsimp_tac simp add: widen_NT);
-
- with rac l lapTs;
- have "?P s"; by auto;
- thus ?thesis; by blast;
-
- next;
- case False;
-
- with wtl;
- have "\\<exists>C. X = Class C"; by clarsimp_tac;
- with x2;
- have "\\<exists>r. b = RefT r"; by (auto simp add: widen_Class);
-
- thus ?thesis;
- proof elim;
- fix r;
- assume b: "b = RefT r";
- show ?thesis;
- proof (cases r);
- case NullT;
- with b rac x2 l lapTs wtl False;
- have "?P s"; by auto;
- thus ?thesis; by blast;
- next;
- case ClassT;
-
- from False wtl;
- have wtlC: "?ClassC"; by simp;
-
- with b ClassT;
- show ?thesis;
- proof (elim exE conjE);
- fix C D rT body;
- assume ClassC: "X = Class C";
- assume zip: "\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G";
- assume s1': "(rT # ST', y') = s1'";
- assume s: "G \\<turnstile> s1' <=s s";
- assume method: "method (G, C) (mname, list) = Some (D, rT, body)";
-
- from ClassC b ClassT x2;
- have "G \\<turnstile> cname \\<preceq>C C"; by simp;
- with method wfp;
- have "\\<exists>D' rT' b'. method (G, cname) (mname, list) = Some (D', rT', b') \\<and> G \\<turnstile> rT'\\<preceq>rT";
- by - (rule subcls_widen_methd, blast);
-
- thus ?thesis;
- proof elim;
- fix D' rT' body';
- assume method': "method (G, cname) (mname, list) = Some (D', rT', body')" "G\\<turnstile>rT'\\<preceq>rT";
-
- have "?P (rT'#c,y)" (is "(\\<exists> apTs X ST'. ?A apTs X ST') \\<and> ?B");
- proof (intro conjI);
- from s1' method' x2;
- show "?B"; by (auto simp add: sup_state_Cons1);
-
- from b ClassT rac l lapTs method';
- have "?A a (Class cname) c";
- proof (simp, intro conjI);
-
- from method' x2;
- have s': "G \\<turnstile> (rT' # c, y) <=s (rT # ST', y')";
- by (auto simp add: sup_state_Cons1);
- from s s1';
- have "G \\<turnstile> (rT # ST', y') <=s s"; by simp;
- with s';
- show "G \\<turnstile> (rT' # c, y) <=s s"; by (rule sup_state_trans);
-
- from x2;
- have 1: "G \\<turnstile> map Some a <=l map Some apTs"; by (simp add: sup_state_def);
- from lapTs zip;
- have "G \\<turnstile> map Some apTs <=l map Some list"; by (simp add: all_widen_is_sup_loc);
- with 1;
- have "G \\<turnstile> map Some a <=l map Some list"; by (rule sup_loc_trans);
- with l lapTs;
- show "\\<forall>x\\<in>set (zip a list). x \\<in> widen G"; by (simp add: all_widen_is_sup_loc);
-
- qed;
- thus "\\<exists> apTs X ST'. ?A apTs X ST'"; by blast;
- qed;
- thus ?thesis; by blast;
- qed
- qed
- qed
- qed
+ option_filter_n ls P (Suc n) ! m' = Some (ls ! m')"
+ with m Suc
+ show ?thesis by auto
qed
qed
qed
qed
-lemma sup_loc_some:
-"\\<forall> y n. (G \\<turnstile> b <=l y) \\<longrightarrow> n < length y \\<longrightarrow> y!n = Some t \\<longrightarrow> (\\<exists>t. b!n = Some t \\<and> (G \\<turnstile> (b!n) <=o (y!n)))" (is "?P b");
-proof (induct "?P" b);
- show "?P []"; by simp;
+lemma is_approx_option_filter: "is_approx (option_filter l P) l"
+ by (simp add: option_filter_def is_approx_option_filter_n)
+
+lemma option_filter_Some:
+"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)"
+proof -
+
+ assume 1: "n < length l" "P n"
+
+ have "\\<forall>n n'. n < length l \\<longrightarrow> P (n+n') \\<longrightarrow> option_filter_n l P n' ! n = Some (l!n)"
+ (is "?P l")
+ proof (induct l)
+ show "?P []" by simp
- case Cons;
- show "?P (a#list)";
- proof (clarsimp_tac simp add: list_all2_Cons1 sup_loc_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 = Some t";
+ fix l ls assume Cons: "?P ls"
+ show "?P (l#ls)"
+ proof (intro)
+ fix n n'
+ assume l: "n < length (l # ls)"
+ assume P: "P (n + n')"
+ show "option_filter_n (l # ls) P n' ! n = Some ((l # ls) ! n)"
+ proof (cases "n")
+ assume "n=0"
+ with P show ?thesis by simp
+ next
+ fix m assume "n = Suc m"
+ with l P Cons
+ show ?thesis by simp
+ qed
+ qed
+ qed
+
+ with 1
+ show ?thesis by (auto simp add: option_filter_def)
+qed
+
+lemma option_filter_contains_dead:
+"contains_dead ins (option_filter phi (mdot ins)) phi pc"
+ by (auto intro: option_filter_Some simp add: contains_dead_def mdot_def maybe_dead_def)
- show "(\\<exists>t. (a # list) ! n = Some t) \\<and> G \\<turnstile>(a # list) ! n <=o Some t";
- proof (cases n);
- case 0;
- with *; show ?thesis; by (simp add: sup_ty_opt_some);
- next;
- case Suc;
- with Cons *;
- show ?thesis; by (simp add: sup_loc_def);
- qed;
- qed;
-qed;
+lemma option_filter_contains_targets:
+"pc < length ins \\<Longrightarrow> contains_targets ins (option_filter phi (mdot ins)) phi pc"
+proof (unfold contains_targets_def, clarsimp)
+
+ fix pc'
+ assume "pc < length ins"
+ "pc' \\<in> succs (ins ! pc) pc"
+ "pc' \\<noteq> Suc pc" and
+ pc': "pc' < length phi"
+
+ hence "is_target ins pc'" by (auto simp add: is_target_def)
+
+ with pc'
+ show "option_filter phi (mdot ins) ! pc' = Some (phi ! pc')"
+ by (auto intro: option_filter_Some simp add: mdot_def)
+qed
+
+
+lemma fits_make_cert:
+ "length ins < length phi \\<Longrightarrow> fits ins (make_cert ins phi) phi"
+proof -
+ assume l: "length ins < length phi"
-lemma mono_load:
-"\\<lbrakk>G \\<turnstile> (a, b) <=s (x, y); n < length y; y!n = Some t\\<rbrakk> \\<Longrightarrow> \\<exists>ts. b!n = Some ts \\<and> G \\<turnstile> (ts#a, b) <=s (t#x, y)";
-proof (clarsimp_tac simp add: sup_state_def);
- assume "G \\<turnstile> b <=l y" "n < length y" "y!n = Some t";
- thus "\\<exists>ts. b ! n = Some ts \\<and> G\\<turnstile>ts\\<preceq>t";
- by (rule sup_loc_some [rulify, elimify], clarsimp_tac);
-qed;
-
-lemma mono_store:
-"\\<lbrakk>G \\<turnstile> (a, b) <=s (ts # ST', y); n < length y\\<rbrakk> \\<Longrightarrow>
- \\<exists> t a'. a = t#a' \\<and> G \\<turnstile> (a', b[n := Some t]) <=s (ST', y[n := Some ts])";
-proof (clarsimp_tac simp add: sup_state_def sup_loc_Cons2);
- fix Y YT';
- assume * : "n < length y" "G \\<turnstile> b <=l y" "G \\<turnstile>Y <=o Some ts" "G \\<turnstile> YT' <=l map Some ST'";
- assume "map Some a = Y # YT'";
- hence "map Some (tl a) = YT' \\<and> Some (hd a) = Y \\<and> (\\<exists>y yt. a = y # yt)";
- by (rule map_hd_tl);
- with *;
- show "\\<exists>t a'. a = t # a' \\<and> G \\<turnstile> map Some a' <=l map Some ST' \\<and> G \\<turnstile> b[n := Some t] <=l y[n := Some ts]";
- by (clarsimp_tac simp add: sup_loc_update);
-qed;
+ thus "fits ins (make_cert ins phi) phi"
+ proof (unfold fits_def make_cert_def, intro conjI allI impI)
+ show "is_approx (option_filter phi (mdot ins)) phi"
+ by (rule is_approx_option_filter)
+
+ show "length ins < length phi" .
+
+ fix pc
+ show "contains_dead ins (option_filter phi (mdot ins)) phi pc"
+ by (rule option_filter_contains_dead)
+
+ assume "pc < length ins"
+ thus "contains_targets ins (option_filter phi (mdot ins)) phi pc"
+ by (rule option_filter_contains_targets)
+ qed
+qed
+
+lemma fitsD:
+"\\<lbrakk>fits ins cert phi; pc' \\<in> succs (ins!pc) pc; pc' \\<noteq> Suc pc; pc < length ins; pc' < length ins\\<rbrakk>
+ \\<Longrightarrow> cert!pc' = Some (phi!pc')"
+by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
+
+lemma fitsD2:
+"\\<lbrakk>fits ins cert phi; Suc pc \\<notin> succs (ins!pc) pc; pc < length ins\\<rbrakk>
+ \\<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)"
+by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
-lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)";
-proof;
- show "xb = PrimT p \\<Longrightarrow> G \\<turnstile> xb \\<preceq> PrimT p"; by blast;
- show "G\\<turnstile> xb \\<preceq> PrimT p \\<Longrightarrow> xb = PrimT p";
- proof (cases xb);
- fix prim;
- assume "xb = PrimT prim" "G\\<turnstile>xb\\<preceq>PrimT p";
- thus ?thesis; by simp;
- next;
- fix ref;
- assume "G\\<turnstile>xb\\<preceq>PrimT p" "xb = RefT ref";
- thus ?thesis; by simp (rule widen_RefT [elimify], auto);
- qed;
-qed;
+lemmas [trans] = sup_state_trans
-
-lemma wtl_inst_pseudo_mono:
+lemma wtl_inst_mono:
"\\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; wf_prog wf_mb G;
G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
- \\<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
-proof (simp only:);
- assume 1 : "wtl_inst (ins ! pc) G rT s1 s1' cert mpc pc" "G \\<turnstile> s2 <=s s1" "pc < length ins";
- assume 2 : "fits ins cert phi" "wf_prog wf_mb G" "i = ins!pc";
+ \\<exists> s2'. wtl_inst (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
+proof -
+ assume pc: "pc < length ins" "i = ins!pc"
+ assume wtl: "wtl_inst i G rT s1 s1' cert mpc pc"
+ assume fits: "fits ins cert phi"
+ assume G: "G \\<turnstile> s2 <=s s1"
+
+ let "?step s" = "step (i, G, s)"
- have 3: "\\<exists> a b. s2 = (a,b)"; by simp;
-
- show ?thesis;
- proof (cases "ins ! pc", insert 1, insert 3);
+ from wtl G
+ have app: "app (i, G, rT, s2)" by (auto simp add: wtl_inst_def app_mono)
+
+ from wtl G
+ have step: "succs i pc \\<noteq> {} \\<Longrightarrow> G \\<turnstile> the (?step s2) <=s the (?step s1)"
+ by - (drule step_mono, auto simp add: wtl_inst_def)
+
+ with app
+ have some: "succs i pc \\<noteq> {} \\<Longrightarrow> ?step s2 \\<noteq> None" by (simp add: app_step_some)
- case Load
- with 1 3
- show ?thesis; by (elim, clarsimp_tac) (rule mono_load [elimify], auto simp add: sup_state_length_snd);
- next
- case Store;
- with 1 3;
- show ?thesis; by (elim, clarsimp_tac) (rule mono_store [elimify], auto simp add: sup_state_length_snd);
- next
- case Getfield;
- with 1 3;
- show ?thesis;
- proof (elim, clarsimp_tac simp add: sup_state_Cons2);
- fix oT x;
- assume "G \\<turnstile> x \\<preceq> oT" "G \\<turnstile> oT \\<preceq> Class cname";
- show "G \\<turnstile> x \\<preceq> Class cname"; by (rule widen_trans);
- qed;
- next
- case Putfield;
- with 1 3;
- show ?thesis;
- proof (elim, clarsimp_tac simp add: sup_state_Cons2);
- fix x xa vT oT T;
- assume "G \\<turnstile> x \\<preceq> vT" "G \\<turnstile> vT \\<preceq> T";
- hence * : "G \\<turnstile> x \\<preceq> T"; by (rule widen_trans);
+ {
+ fix pc'
+ assume 0: "pc' \\<in> succs i pc" "pc' \\<noteq> pc+1"
+ hence "succs i pc \\<noteq> {}" by auto
+ hence "G \\<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
+ also
+ from wtl 0
+ have "G \\<turnstile> the (?step s1) <=s the (cert!pc')"
+ by (auto simp add: wtl_inst_def)
+ finally
+ have "G\\<turnstile> the (?step s2) <=s the (cert!pc')" .
+ } note cert = this
+
+ have "\\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \\<and> G \\<turnstile> s2' <=s s1'"
+ proof (cases "pc+1 \\<in> succs i pc")
+ case True
+ with wtl
+ have s1': "s1' = the (?step s1)" by (simp add: wtl_inst_def)
- assume "G \\<turnstile> xa \\<preceq> oT" "G \\<turnstile> oT \\<preceq> Class cname";
- hence "G \\<turnstile> xa \\<preceq> Class cname"; by (rule widen_trans);
-
- with *
- show "(G \\<turnstile> xa \\<preceq> Class cname) \\<and> (G \\<turnstile> x \\<preceq> T)"; by blast;
+ have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \\<and> G \\<turnstile> (the (?step s2)) <=s s1'"
+ (is "?wtl \\<and> ?G")
+ proof
+ from True s1'
+ show ?G by (auto intro: step)
+
+ from True app wtl
+ show ?wtl
+ by (clarsimp intro: cert simp add: wtl_inst_def)
qed
- next
- case Checkcast;
- with 1 3;
- show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons2) (rule widen_RefT2);
- next
- case Invoke;
- with 1 2 3;
- show ?thesis; by elim (rule method_inv_pseudo_mono [elimify], simp+);
- next
- case Return;
- with 1 3;
- show ?thesis;
- proof (elim, clarsimp_tac simp add: sup_state_Cons2 simp del: split_paired_Ex);
- fix x T;
- assume "G\\<turnstile>x\\<preceq>T" "G\\<turnstile>T\\<preceq>rT";
- thus "G\\<turnstile>x\\<preceq>rT"; by (rule widen_trans);
- qed
- next
- case Goto;
- with 1 3;
- show ?thesis;
- proof (elim, clarsimp_tac simp del: split_paired_Ex);
- fix a b x y;
- assume "G \\<turnstile> (a, b) <=s s1" "G \\<turnstile> s1 <=s (x, y)";
- thus "G \\<turnstile> (a, b) <=s (x, y)"; by (rule sup_state_trans);
- qed
+ thus ?thesis by blast
next
- case Ifcmpeq;
- with 1 3;
- show ?thesis
- proof (elim, clarsimp_tac simp add: sup_state_Cons2, intro conjI);
- fix xt' b ST' y c d;
- assume "G \\<turnstile> (xt', b) <=s (ST', y)" "G \\<turnstile> (ST', y) <=s (c, d)";
- thus "G \\<turnstile> (xt', b) <=s (c, d)"; by (rule sup_state_trans);
- next;
- fix ts ts' x xa;
- assume * :
- "(\\<exists>p. ts = PrimT p \\<and> ts' = PrimT p) \\<or> (\\<exists>r. ts = RefT r) \\<and> (\\<exists>r'. ts' = RefT r')";
-
- assume x: "G\\<turnstile>x\\<preceq>ts" "G\\<turnstile>xa\\<preceq>ts'";
-
- show "(\\<exists>p. x = PrimT p \\<and> xa = PrimT p) \\<or> (\\<exists>r. x = RefT r) \\<and> (\\<exists>r'. xa = RefT r')";
- proof (cases x);
- case PrimT;
- with * x;
- show ?thesis; by (auto simp add: PrimT_PrimT);
- next;
- case RefT;
- hence 1: "\\<exists>r. x = RefT r"; by blast;
-
- have "\\<exists>r'. xa = RefT r'";
- proof (cases xa);
- case PrimT;
- with RefT * x;
- have "False"; by auto (rule widen_RefT [elimify], auto);
- thus ?thesis; by blast;
- qed blast;
+ case False
+ with wtl
+ have "s1' = the (cert ! Suc pc)" by (simp add: wtl_inst_def)
- with 1
- show ?thesis by blast
- qed
- qed
- qed (elim, clarsimp_tac simp add: sup_state_Cons1 sup_state_Cons2 PrimT_PrimT)+
-qed
-
-lemma wtl_inst_last_mono:
-"\\<lbrakk>wtl_inst i G rT s1 s1' cert (Suc pc) pc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow>
- \\<exists>s2'. wtl_inst i G rT s2 s2' cert (Suc pc) pc \\<and> (G \\<turnstile> s2' <=s s1')";
-proof -;
- assume * : "wtl_inst i G rT s1 s1' cert (Suc pc) pc" "G \\<turnstile> s2 <=s s1";
+ with False app wtl
+ have "wtl_inst i G rT s2 s1' cert mpc pc \\<and> G \\<turnstile> s1' <=s s1'"
+ by (clarsimp intro: cert simp add: wtl_inst_def)
+
+ thus ?thesis by blast
+ qed
- show ?thesis
- proof (cases i, insert *)
- case Return with *
- show ?thesis
- by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2)
- (rule widen_trans, blast+);
- next
- case Goto with *
- show ?thesis
- by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2)
- (rule sup_state_trans, blast+);
- qed auto
+ with pc show ?thesis by simp
qed
-
-
-lemma wtl_option_last_mono:
-"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; mpc = Suc pc; G \\<turnstile> s2 <=s s1\\<rbrakk> \\<Longrightarrow>
- \\<exists>s2'. wtl_inst_option i G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')";
-proof (simp only: );
- assume G: "G \\<turnstile> s2 <=s s1";
- assume w: "wtl_inst_option i G rT s1 s1' cert (Suc pc) pc";
-
- show "\\<exists>s2'. wtl_inst_option i G rT s2 s2' cert (Suc pc) pc \\<and> (G \\<turnstile> s2' <=s s1')";
- proof (cases "cert!pc");
- case None;
- with G w;
- show ?thesis; by (simp add: wtl_inst_option_def wtl_inst_last_mono del: split_paired_Ex);
- next;
- case Some;
- with G w;
- have o: "G \\<turnstile> s1 <=s a \\<and> wtl_inst i G rT a s1' cert (Suc pc) pc";
- by (simp add: wtl_inst_option_def);
- hence w' : "wtl_inst i G rT a s1' cert (Suc pc) pc"; ..;
-
- from o G;
- have G' : "G \\<turnstile> s2 <=s a"; by - (rule sup_state_trans, blast+);
-
- from o;
- have "\\<exists>s2'. wtl_inst i G rT a s2' cert (Suc pc) pc \\<and> G \\<turnstile> s2' <=s s1'";
- by elim (rule wtl_inst_last_mono, auto);
-
- with Some w G';
- show ?thesis; by (auto simp add: wtl_inst_option_def);
- qed;
-qed;
-
+
+
lemma wt_instr_imp_wtl_inst:
"\\<lbrakk>wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
pc < length ins; length ins = max_pc\\<rbrakk> \\<Longrightarrow>
\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
proof -
- assume * : "wt_instr (ins!pc) G rT phi max_pc pc" "fits ins cert phi"
- "pc < length ins" "length ins = max_pc"
+ assume wt: "wt_instr (ins!pc) G rT phi max_pc pc"
+ assume fits: "fits ins cert phi"
+ assume pc: "pc < length ins" "length ins = max_pc"
+
+ from wt
+ have app: "app (ins!pc, G, rT, phi!pc)" by (simp add: wt_instr_def);
+
+ from wt pc
+ have pc': "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> pc' < length ins"
+ by (simp add: wt_instr_def)
- have xy: "\\<exists> x y. phi!pc = (x,y)" by simp
+ let ?s' = "the (step (ins!pc,G, phi!pc))"
+
+ from wt
+ have G: "!!pc'. pc' \\<in> succs (ins!pc) pc \\<Longrightarrow> G \\<turnstile> ?s' <=s phi ! pc'"
+ by (simp add: wt_instr_def)
+
+ from wt fits pc
+ have cert: "!!pc'. \\<lbrakk>pc' \\<in> succs (ins!pc) pc; pc' < max_pc; pc' \\<noteq> pc+1\\<rbrakk>
+ \\<Longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> ?s' <=s the (cert!pc')"
+ by (auto dest: fitsD simp add: wt_instr_def simp del: split_paired_Ex)
show ?thesis
- proof (cases "ins!pc", insert *, insert xy);
- case Return with * xy
- show ?thesis
- by (elim, clarsimp_tac simp add: fits_def contains_dead_def simp del: split_paired_Ex);
- next
- case Goto with * xy
- show ?thesis;
- by (clarsimp_tac simp add: fits_def contains_dead_def contains_targets_def simp del: split_paired_Ex);
- next
- case Ifcmpeq with * xy
- show ?thesis;
- by (clarsimp_tac simp add: fits_def contains_dead_def contains_targets_def simp del: split_paired_Ex);
- next
- case Invoke with * xy
- show ?thesis
- proof (elim, clarsimp_tac simp del: split_paired_Ex)
- fix y apTs X ST';
- assume pc : "Suc pc < length ins";
- assume phi : "phi ! pc = (rev apTs @ X # ST', y)" "length apTs = length list";
- assume ** :
- "X = NT \\<or> (\\<exists>C. X = Class C \\<and>
- (\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G) \\<and>
- (\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and> G \\<turnstile> (rT # ST', y) <=s phi ! Suc pc))"
- (is "?NT \\<or> ?CL");
-
- from Invoke pc *;
- have cert: "cert ! Suc pc = Some (phi ! Suc pc)"; by (clarsimp_tac simp add: fits_def contains_dead_def);
+ proof (cases "pc+1 \\<in> succs (ins!pc) pc")
+ case True
+
+ have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \\<and> G \\<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \\<and> ?G")
+ proof
+ from True
+ show "G \\<turnstile> ?s' <=s phi ! Suc pc" by (simp add: G)
+
+ from True fits app pc cert pc'
+ show "?wtl"
+ by (auto simp add: wtl_inst_def)
+ qed
- show "\\<exists>s. (\\<exists>apTsa Xa ST'a.
- rev apTs @ X # ST' = rev apTsa @ Xa # ST'a \\<and>
- length apTsa = length list \\<and>
- (\\<exists>s''. cert ! Suc pc = Some s'' \\<and>
- (s'' = s \\<and> Xa = NT \\<or>
- G \\<turnstile> s <=s s'' \\<and>
- (\\<exists>C. Xa = Class C \\<and>
- (\\<forall>x\\<in>set (zip apTsa list). x \\<in> widen G) \\<and>
- (\\<exists>D rT. (\\<exists>b. method (G, C) (mname, list) = Some (D, rT, b)) \\<and> (rT # ST'a, y) = s))))) \\<and>
- G \\<turnstile> s <=s phi ! Suc pc" (is "\\<exists>s. ?P s");
- proof (cases "X=NT");
- case True
- with cert phi **
- have "?P (phi ! Suc pc)" by (force simp del: split_paired_Ex)
- thus ?thesis by blast
- next
- case False
- with **
+ thus ?thesis by blast
+
+ next
+ let ?s'' = "the (cert ! Suc pc)"
- have "?CL" by simp
+ case False
+ with fits app pc cert pc'
+ have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \\<and> G \\<turnstile> ?s'' <=s phi ! Suc pc"
+ by (auto dest: fitsD2 simp add: wtl_inst_def)
- thus ?thesis
- proof (elim exE conjE);
- fix C D rT b;
- assume "X = Class C" "\\<forall>x\\<in>set (zip apTs list). x \\<in> widen G"
- "G \\<turnstile> (rT # ST', y) <=s phi ! Suc pc"
- "method (G, C) (mname, list) = Some (D, rT, b)";
- with cert phi;
- have "?P (rT #ST', y)" by (force simp del: split_paired_Ex)
- thus ?thesis by blast
- qed
- qed
- qed
- qed (elim, force)+
+ thus ?thesis by blast
+ qed
qed
@@ -764,51 +348,49 @@
case Some;
from fits;
- have "pc < length phi"; by (clarsimp_tac simp add: fits_def);
+ have "pc < length phi"; by (clarsimp simp add: fits_def);
with fits Some;
have "cert ! pc = Some (phi!pc)"; by (auto simp add: fits_def is_approx_def);
with *;
show ?thesis; by (simp add: wtl_inst_option_def);
- qed;
-qed;
+ qed
+qed
-lemma wtl_option_pseudo_mono:
+lemma wtl_option_mono:
"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins;
wf_prog wf_mb G; G \\<turnstile> s2 <=s s1; i = ins!pc\\<rbrakk> \\<Longrightarrow>
- \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and>
- (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
-proof -;
+ \\<exists> s2'. wtl_inst_option (ins!pc) G rT s2 s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
+proof -
assume wtl: "wtl_inst_option i G rT s1 s1' cert mpc pc" and
fits: "fits ins cert phi" "pc < length ins"
- "wf_prog wf_mb G" "G \\<turnstile> s2 <=s s1" "i = ins!pc";
+ "wf_prog wf_mb G" "G \\<turnstile> s2 <=s s1" "i = ins!pc"
- show ?thesis;
- proof (cases "cert!pc");
- case None;
+ show ?thesis
+ proof (cases "cert!pc")
+ case None
with wtl fits;
show ?thesis;
- by - (rule wtl_inst_pseudo_mono [elimify], (simp add: wtl_inst_option_def)+);
- next;
- case Some;
+ by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+);
+ next
+ case Some
with wtl fits;
- have G: "G \\<turnstile> s2 <=s a";
- by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+);
+ have G: "G \\<turnstile> s2 <=s a"
+ by - (rule sup_state_trans, (simp add: wtl_inst_option_def)+)
- from Some wtl;
- have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def);
+ from Some wtl
+ have "wtl_inst i G rT a s1' cert mpc pc"; by (simp add: wtl_inst_option_def)
- with G fits;
- have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and>
- (G \\<turnstile> s2' <=s s1' \\<or> (\\<exists>s. cert!(Suc pc) = Some s \\<and> G \\<turnstile> s2' <=s s))";
- by - (rule wtl_inst_pseudo_mono, (simp add: wtl_inst_option_def)+);
+ with G fits
+ have "\\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \\<and> (G \\<turnstile> s2' <=s s1')"
+ by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+);
with Some G;
show ?thesis; by (simp add: wtl_inst_option_def);
qed
-qed;
+qed
(* main induction over instruction list *)
@@ -854,7 +436,7 @@
with Nil 1 2 5;
have "\\<exists>s'. wtl_inst_option a G rT s s' cert (Suc (length l)) pc";
- by elim (rule wtl_option_pseudo_mono [elimify], force+);
+ by elim (rule wtl_option_mono [elimify], force+);
with Nil 2;
show ?thesis; by auto;
@@ -875,15 +457,15 @@
by - (rule wt_instr_imp_wtl_option [elimify], assumption+, simp+);
hence "\\<exists>s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\<and>
- (G \\<turnstile> s1 <=s (phi ! (Suc pc)) \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))";
+ (G \\<turnstile> s1 <=s (phi ! (Suc pc)))" (* \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))"; *)
proof elim;
fix s1';
assume "wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc" and
a :"G \\<turnstile> s1' <=s phi ! Suc pc";
with 1 2 5;
have "\\<exists>s1. wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc \\<and>
- ((G \\<turnstile> s1 <=s s1') \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))";
- by - (rule wtl_option_pseudo_mono [elimify], simp+);
+ ((G \\<turnstile> s1 <=s s1'))" (* \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s))"; *)
+ by - (rule wtl_option_mono [elimify], simp+);
with a;
show ?thesis;
@@ -892,51 +474,23 @@
assume "G \\<turnstile> s1 <=s s1'" "G \\<turnstile> s1' <=s phi ! Suc pc";
show "G \\<turnstile> s1 <=s phi ! Suc pc"; by (rule sup_state_trans);
qed auto;
- qed;
+ qed
- thus ?thesis;
+ thus ?thesis
proof (elim exE conjE);
fix s1;
assume wto: "wtl_inst_option a G rT s s1 cert (Suc (pc + length list)) pc";
- assume Gs1: "G \\<turnstile> s1 <=s phi ! Suc pc \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s)";
+ assume Gs1: "G \\<turnstile> s1 <=s phi ! Suc pc" (* \\<or> (\\<exists>s. cert ! Suc pc = Some s \\<and> G \\<turnstile> s1 <=s s)"; *)
- have "\\<exists>s'. wtl_inst_list list G rT s1 s' cert ((Suc pc)+length list) (Suc pc)";
- proof (cases "G \\<turnstile> s1 <=s phi ! Suc pc");
- case True;
- with Gs1;
- have "G \\<turnstile> s1 <=s phi ! Suc pc"; by simp;
- with *;
- show ?thesis; by blast;
- next;
- case False;
- with Gs1;
- have "\\<exists>c. cert ! Suc pc = Some c \\<and> G \\<turnstile> s1 <=s c"; by simp;
- thus ?thesis;
- proof elim;
- from 1 2 Cons Cons2;
- have "Suc pc < length phi"; by (clarsimp_tac simp add: fits_def is_approx_def);
+ with *
+ have "\\<exists>s'. wtl_inst_list list G rT s1 s' cert ((Suc pc)+length list) (Suc pc)"; by blast
- with 1;
- have cert: "cert ! (Suc pc) = None \\<or> cert ! (Suc pc) = Some (phi ! Suc pc)";
- by (clarsimp_tac simp add: fits_def is_approx_def);
-
- fix c;
- assume "cert ! Suc pc = Some c";
- with cert;
- have c: "c = phi ! Suc pc"; by simp;
- assume "G \\<turnstile> s1 <=s c";
- with c;
- have "G \\<turnstile> s1 <=s phi ! Suc pc"; by simp;
- with *;
- show ?thesis; by blast;
- qed;
- qed;
with wto;
show ?thesis; by (auto simp del: split_paired_Ex);
- qed;
- qed;
- qed;
-qed;
+ qed
+ qed
+ qed
+qed
lemma fits_imp_wtl_method_complete:
@@ -991,12 +545,12 @@
from 1;
show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))";
- proof (rule bspec [elimify], clarsimp_tac);
+ proof (rule bspec [elimify], clarsimp);
assume ub : "unique b";
assume m: "\\<forall>(sig,rT,mb)\\<in>set b. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G a (snd sig) rT maxl b (Phi a sig)) mb";
from m b;
show ?thesis;
- proof (rule bspec [elimify], clarsimp_tac);
+ proof (rule bspec [elimify], clarsimp);
assume "wt_method G a ba ad ae bb (Phi a (ac, ba))";
with wfprog uG ub b 1;
show ?thesis;
@@ -1004,6 +558,7 @@
qed;
qed;
qed;
-qed;
+qed
-end;
+
+end
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Mon Aug 07 10:29:54 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Mon Aug 07 14:32:56 2000 +0200
@@ -6,7 +6,7 @@
header {* Correctness of the LBV *}
-theory LBVCorrect = LBVSpec:;
+theory LBVCorrect = BVSpec + LBVSpec:
constdefs
fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
@@ -17,7 +17,7 @@
(\\<forall> t. cert!(pc+length a) = Some t \\<longrightarrow> phi!(pc+length a) = t)))"
fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
-"fits phi is G rT s0 s2 cert \\<equiv> fits_partial phi 0 is G rT s0 s2 cert";
+"fits phi is G rT s0 s2 cert \\<equiv> fits_partial phi 0 is G rT s0 s2 cert"
lemma fitsD:
"fits phi is G rT s0 s2 cert \\<Longrightarrow>
@@ -25,123 +25,126 @@
wtl_inst_list a G rT s0 s1 cert (0+length is) 0 \\<Longrightarrow>
wtl_inst_list (i#b) G rT s1 s2 cert (0+length is) (0+length a) \\<Longrightarrow>
((cert!(0+length a) = None \\<longrightarrow> phi!(0+length a) = s1) \\<and>
- (\\<forall> t. cert!(0+length a) = Some t \\<longrightarrow> phi!(0+length a) = t))";
-by (unfold fits_def fits_partial_def) blast;
+ (\\<forall> t. cert!(0+length a) = Some t \\<longrightarrow> phi!(0+length a) = t))"
+by (unfold fits_def fits_partial_def) blast
-lemma exists_list: "\\<exists>l. n < length l" (is "?Q n");
-proof (induct "n");
- fix n; assume "?Q n";
- thus "?Q (Suc n)";
- proof elim;
- fix l; assume "n < length (l::'a list)";
- hence "Suc n < length (a#l)"; by simp;
- thus ?thesis; ..;
- qed;
-qed auto;
+lemma exists_list: "\\<exists>l. n < length l" (is "?Q n")
+proof (induct "n")
+ fix n; assume "?Q n"
+ thus "?Q (Suc n)"
+ proof elim
+ fix l assume "n < length (l::'a list)"
+ hence "Suc n < length (a#l)" by simp
+ thus ?thesis ..
+ qed
+qed auto
lemma exists_phi:
"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow>
- \\<exists> phi. fits phi is G rT s0 s2 cert \\<and> length is < length phi";
-proof -;
- assume all: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
+ \\<exists> phi. fits phi is G rT s0 s2 cert \\<and> length is < length phi"
+proof -
+ assume all: "wtl_inst_list is G rT s0 s2 cert (length is) 0"
have "\\<forall> s0 pc. wtl_inst_list is G rT s0 s2 cert (pc+length is) pc
\\<longrightarrow> (\\<exists> phi. pc + length is < length phi \\<and> fits_partial phi pc is G rT s0 s2 cert)"
- (is "?P is");
- proof (induct "?P" "is");
- case Nil;
- show "?P []"; by (simp add: fits_partial_def exists_list);
- case Cons;
- show "?P (a#list)";
- proof (intro allI impI);
- fix s0 pc;
- assume wtl: "wtl_inst_list (a # list) G rT s0 s2 cert (pc + length (a # list)) pc";
- thus "\\<exists>phi. pc + length (a # list) < length phi \\<and>
- fits_partial phi pc (a # list) G rT s0 s2 cert";
- obtain s1 where
- opt: "wtl_inst_option a G rT s0 s1 cert (Suc pc + length list) pc" and
- wtlSuc: "wtl_inst_list list G rT s1 s2 cert (Suc pc + length list) (Suc pc)";
- by auto;
- with Cons;
- show ?thesis;
- obtain phi where fits: "fits_partial phi (Suc pc) list G rT s1 s2 cert"
- and length: "(Suc pc) + length list < length phi"; by blast;
- let "?A phi pc x s1'" =
- "(cert ! (pc + length (x::instr list)) = None \\<longrightarrow> phi ! (pc + length x) = s1') \\<and>
- (\\<forall>t. cert ! (pc + length x) = Some t \\<longrightarrow> phi ! (pc + length x) = t)";
- show ?thesis;
- proof (cases "cert!pc");
- case None;
- have "fits_partial (phi[pc:= s0]) pc (a # list) G rT s0 s2 cert";
- proof (unfold fits_partial_def, intro allI impI);
- fix x i y s1';
- assume * :
- "x @ i # y = a # list"
- "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc"
- "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)";
- show "?A (phi[pc:= s0]) pc x s1'";
- proof (cases "x");
- assume "x = []";
- with * length None;
- show ?thesis; by simp;
- next;
- fix b l; assume Cons: "x = b#l";
- with fits *;
- have "?A (phi[pc:= s0]) (Suc pc) l s1'";
- proof (unfold fits_partial_def, elim allE impE);
- from * Cons;
- show "l @ i # y = list"; by simp;
- from Cons opt *;
- show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)";
- by (simp, elim) (drule wtl_inst_option_unique, assumption, simp);
- qed simp+;
- with Cons length;
- show ?thesis; by auto;
- qed;
- qed;
- with length;
- show ?thesis; by intro auto;
- next;
- fix c; assume Some: "cert!pc = Some c";
- have "fits_partial (phi[pc:= c]) pc (a # list) G rT s0 s2 cert";
- proof (unfold fits_partial_def, intro allI impI);
- fix x i y s1';
- assume * :
- "x @ i # y = a # list"
- "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc"
- "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)";
- show "?A (phi[pc:= c]) pc x s1'";
- proof (cases "x");
- assume "x = []";
- with length Some;
- show ?thesis; by simp;
- next;
- fix b l; assume Cons: "x = b#l";
- with fits *;
- have "?A (phi[pc:= c]) (Suc pc) l s1'";
- proof (unfold fits_partial_def, elim allE impE);
- from * Cons;
- show "l @ i # y = list"; by simp;
- from Cons opt *;
- show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)";
- by (simp, elim) (drule wtl_inst_option_unique, assumption, simp);
- qed simp+;
- with Cons length;
- show ?thesis; by auto;
- qed;
- qed;
- with length;
- show ?thesis; by intro auto;
- qed;
- qed;
- qed;
- qed;
- qed;
- with all;
- show ?thesis;
- proof (elim exE allE impE conjE);
- show "wtl_inst_list is G rT s0 s2 cert (0+length is) 0"; by simp;
- qed (auto simp add: fits_def);
-qed;
+ (is "?P is")
+ proof (induct "?P" "is")
+ case Nil
+ show "?P []" by (simp add: fits_partial_def exists_list)
+ case Cons
+ show "?P (a#list)"
+ proof (intro allI impI)
+ fix s0 pc
+ assume wtl: "wtl_inst_list (a # list) G rT s0 s2 cert (pc + length (a # list)) pc"
+
+ from this
+ obtain s1 where
+ opt: "wtl_inst_option a G rT s0 s1 cert (Suc pc + length list) pc" and
+ wtlSuc: "wtl_inst_list list G rT s1 s2 cert (Suc pc + length list) (Suc pc)"
+ by auto
+
+ with Cons
+ obtain phi where
+ fits: "fits_partial phi (Suc pc) list G rT s1 s2 cert" and
+ length: "(Suc pc) + length list < length phi"
+ by blast
+
+ let "?A phi pc x s1'" =
+ "(cert ! (pc + length (x::instr list)) = None \\<longrightarrow> phi ! (pc + length x) = s1') \\<and>
+ (\\<forall>t. cert ! (pc + length x) = Some t \\<longrightarrow> phi ! (pc + length x) = t)"
+
+ show "\\<exists>phi. pc + length (a # list) < length phi \\<and>
+ fits_partial phi pc (a # list) G rT s0 s2 cert"
+ proof (cases "cert!pc")
+ case None
+ have "fits_partial (phi[pc:= s0]) pc (a # list) G rT s0 s2 cert"
+ proof (unfold fits_partial_def, intro allI impI)
+ fix x i y s1'
+ assume * :
+ "x @ i # y = a # list"
+ "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc"
+ "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)"
+ show "?A (phi[pc:= s0]) pc x s1'"
+ proof (cases "x")
+ assume "x = []"
+ with * length None
+ show ?thesis by simp
+ next
+ fix b l assume Cons: "x = b#l"
+ with fits *
+ have "?A (phi[pc:= s0]) (Suc pc) l s1'"
+ proof (unfold fits_partial_def, elim allE impE)
+ from * Cons
+ show "l @ i # y = list" by simp
+ from Cons opt *
+ show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)"
+ by (simp, elim) (drule wtl_inst_option_unique, assumption, simp)
+ qed simp+
+ with Cons length
+ show ?thesis by auto
+ qed
+ qed
+ with length
+ show ?thesis by intro auto
+ next
+ fix c assume Some: "cert!pc = Some c"
+ have "fits_partial (phi[pc:= c]) pc (a # list) G rT s0 s2 cert"
+ proof (unfold fits_partial_def, intro allI impI)
+ fix x i y s1'
+ assume * :
+ "x @ i # y = a # list"
+ "wtl_inst_list x G rT s0 s1' cert (pc + length (a # list)) pc"
+ "wtl_inst_list (i # y) G rT s1' s2 cert (pc + length (a # list)) (pc + length x)"
+ show "?A (phi[pc:= c]) pc x s1'"
+ proof (cases "x")
+ assume "x = []"
+ with length Some
+ show ?thesis by simp
+ next
+ fix b l assume Cons: "x = b#l"
+ with fits *
+ have "?A (phi[pc:= c]) (Suc pc) l s1'"
+ proof (unfold fits_partial_def, elim allE impE)
+ from * Cons
+ show "l @ i # y = list" by simp
+ from Cons opt *
+ show "wtl_inst_list l G rT s1 s1' cert (Suc pc + length list) (Suc pc)"
+ by (simp, elim) (drule wtl_inst_option_unique, assumption, simp)
+ qed simp+
+ with Cons length
+ show ?thesis by auto
+ qed
+ qed
+ with length
+ show ?thesis by intro auto
+ qed
+ qed
+ qed
+ with all
+ show ?thesis
+ proof (elim exE allE impE conjE)
+ show "wtl_inst_list is G rT s0 s2 cert (0+length is) 0" by simp
+ qed (auto simp add: fits_def)
+qed
lemma fits_lemma1:
@@ -205,38 +208,38 @@
"wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)"
and w: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))";
hence a: "wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0"; by (rule wtl_append);
- assume "b \\<noteq> []";
- thus "G \\<turnstile> s2 <=s phi ! Suc (length a)";
- obtain b' bs where Cons: "b = b' # bs"; by (simp add: neq_Nil_conv) (elim exE, rule that);
- hence "(a@[i]) @ b' # bs = a @ i # b"; by simp;
- with f;
- show ?thesis;
- proof (rule fitsD [elimify]);
- from Cons w;
- show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))";
- by simp;
- from a;
- show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0"; by simp;
+ assume "b \\<noteq> []"
- assume cert:
- "(cert ! (0 + length (a @ [i])) = None \\<longrightarrow> phi ! (0 + length (a @ [i])) = s2) \\<and>
- (\\<forall>t. cert ! (0 + length (a @ [i])) = Some t \\<longrightarrow> phi ! (0 + length (a @ [i])) = t)";
- show ?thesis;
- proof (cases "cert ! Suc (length a)");
- assume "cert ! Suc (length a) = None";
- with cert;
- have "s2 = phi ! Suc (length a)"; by simp;
- thus ?thesis; by simp;
- next;
- fix t; assume "cert ! Suc (length a) = Some t";
- with cert;
- have "phi ! Suc (length a) = t"; by (simp del: split_paired_All);
- with cert Cons w;
- show ?thesis; by (auto simp add: wtl_inst_option_def);
- qed;
- qed;
- qed;
-qed;
+ from this
+ obtain b' bs where Cons: "b = b' # bs"; by (simp add: neq_Nil_conv) (elim exE, rule that);
+ hence "(a@[i]) @ b' # bs = a @ i # b"; by simp;
+ with f
+ show "G \\<turnstile> s2 <=s phi ! Suc (length a)";
+ proof (rule fitsD [elimify]);
+ from Cons w;
+ show "wtl_inst_list (b' # bs) G rT s2 s3 cert (0 + length (a @ i # b)) (0 + length (a @ [i]))";
+ by simp;
+ from a;
+ show "wtl_inst_list (a @ [i]) G rT s0 s2 cert (0 + length (a @ i # b)) 0"; by simp;
+
+ assume cert:
+ "(cert ! (0 + length (a @ [i])) = None \\<longrightarrow> phi ! (0 + length (a @ [i])) = s2) \\<and>
+ (\\<forall>t. cert ! (0 + length (a @ [i])) = Some t \\<longrightarrow> phi ! (0 + length (a @ [i])) = t)";
+ show ?thesis;
+ proof (cases "cert ! Suc (length a)");
+ assume "cert ! Suc (length a) = None";
+ with cert;
+ have "s2 = phi ! Suc (length a)"; by simp;
+ thus ?thesis; by simp;
+ next;
+ fix t; assume "cert ! Suc (length a) = Some t";
+ with cert;
+ have "phi ! Suc (length a) = t"; by (simp del: split_paired_All);
+ with cert Cons w;
+ show ?thesis; by (auto simp add: wtl_inst_option_def)
+ qed
+ qed
+qed
lemma wtl_lemma:
"\\<lbrakk>wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0;
@@ -270,17 +273,10 @@
have suc: "i2 \\<noteq> [] \\<Longrightarrow> G \\<turnstile> s2 <=s phi ! Suc (length i1)";
by (rule wtl_suc_pc [rulify]);
+ with wo
show ?thesis;
- proof (cases i, insert suc, insert wo);
- case Invoke with suc wo
- show ?thesis
- by - (cases "cert ! (length i1)",
- clarsimp_tac simp add: c2 wtl_inst_option_def split_beta,
- intro exI conjI, blast, simp, force,
- clarsimp_tac simp add: c1 wtl_inst_option_def,
- intro exI conjI, blast, simp, force)
- qed (clarsimp_tac simp add: c1 c2 c3 wtl_inst_option_def split_beta split: option.split_asm)+
-qed;
+ by (auto simp add: c1 c2 c3 wt_instr_def wtl_inst_def wtl_inst_option_def split: option.split_asm)
+qed
lemma wtl_fits_wt:
@@ -292,49 +288,55 @@
fix pc;
assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0"
and pc: "pc < length is";
+
+ from this
+ obtain i1 i2' s1 where
+ l: "i1 @ i2' = is" "length i1 = pc" and
+ w1: "wtl_inst_list i1 G rT s0 s1 cert (length is) 0" and
+ w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)";
+ by (rule wtl_partial [rulify, elimify]) (elim, rule that);
- thus "wt_instr (is ! pc) G rT phi (length is) pc";
- obtain i1 i2' s1 where l: "i1 @ i2' = is" "length i1 = pc" and
- w1: "wtl_inst_list i1 G rT s0 s1 cert (length is) 0" and
- w2: "wtl_inst_list i2' G rT s1 s3 cert (length is) (0 + length i1)";
- by (rule wtl_partial [rulify, elimify]) (elim, rule that);
- from l pc;
- have "i2' \\<noteq> []"; by auto;
- thus ?thesis;
- obtain i i2 where c: "i2' = i#i2"; by (simp add: neq_Nil_conv) (elim, rule that);
- with w2 l;
- show ?thesis;
- obtain s2 where w3:
- "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)"
- "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))"; by auto;
+ from l pc;
+ have "i2' \\<noteq> []"; by auto;
+
+ from this
+ obtain i i2 where c: "i2' = i#i2"
+ by (simp add: neq_Nil_conv) (elim, rule that)
+
+ with w2 l
+ obtain s2
+ where w3:
+ "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)"
+ "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))"
+ by auto
- from w1 l c;
- have w4: "wtl_inst_list i1 G rT s0 s1 cert (length (i1 @ i # i2)) 0"; by simp;
+ from w1 l c
+ have w4: "wtl_inst_list i1 G rT s0 s1 cert (length (i1 @ i # i2)) 0" by simp
+
+ from l c fits
+ have "fits phi (i1@i#i2) G rT s0 s3 cert" by simp
+ with w4 w3
+ have "wt_instr i G rT phi (length (i1@i#i2)) (length i1)" by (rule wtl_lemma)
- from l c fits;
- have "fits phi (i1@i#i2) G rT s0 s3 cert"; by simp;
- with w4 w3;
- have "wt_instr i G rT phi (length (i1@i#i2)) (length i1)"; by (rule wtl_lemma);
- with l c;
- show ?thesis; by (auto simp add: nth_append);
- qed;
- qed;
- qed;
-qed;
+ with l c
+ show "wt_instr (is ! pc) G rT phi (length is) pc"
+ by (auto simp add: nth_append)
+qed
lemma wtl_inst_list_correct:
"wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow>
\\<exists> phi. \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
proof -;
assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
- thus ?thesis;
- obtain phi where "fits phi is G rT s0 s2 cert";
- by (rule exists_phi [elimify]) blast;
- with wtl;
- show ?thesis;
- by (rule wtl_fits_wt [elimify]) blast;
- qed;
-qed;
+
+ from this
+ obtain phi where "fits phi is G rT s0 s2 cert";
+ by (rule exists_phi [elimify]) blast
+
+ with wtl
+ show ?thesis
+ by (rule wtl_fits_wt [elimify]) blast;
+qed
lemma fits_first:
"\\<lbrakk>is \\<noteq> [];wtl_inst_list is G rT s0 s2 cert (length is) 0;
@@ -342,58 +344,64 @@
proof -;
assume wtl: "wtl_inst_list is G rT s0 s2 cert (length is) 0";
assume fits: "fits phi is G rT s0 s2 cert";
- assume "is \\<noteq> []";
- thus ?thesis;
- obtain y ys where cons: "is = y#ys"; by (simp add: neq_Nil_conv) (elim, rule that);
- from fits;
- show ?thesis;
- proof (rule fitsD [elimify]);
- from cons; show "[]@y#ys = is"; by simp;
- from cons wtl;
- show "wtl_inst_list (y#ys) G rT s0 s2 cert (0 + length is) (0 + length [])";
- by simp;
+ assume "is \\<noteq> []"
+
+ from this
+ obtain y ys where cons: "is = y#ys"
+ by (simp add: neq_Nil_conv) (elim, rule that)
- assume cert:
- "(cert ! (0 + length []) = None \\<longrightarrow> phi ! (0 + length []) = s0) \\<and>
- (\\<forall>t. cert ! (0 + length []) = Some t \\<longrightarrow> phi ! (0 + length []) = t)";
+ from fits
+ show ?thesis
+ proof (rule fitsD [elimify])
+ from cons show "[]@y#ys = is" by simp
+
+ from cons wtl
+ show "wtl_inst_list (y#ys) G rT s0 s2 cert (0 + length is) (0 + length [])"
+ by simp
- show ?thesis;
- proof (cases "cert!0");
- assume "cert!0 = None";
- with cert;
- show ?thesis; by simp;
- next;
- fix t; assume "cert!0 = Some t";
- with cert;
- have "phi!0 = t"; by (simp del: split_paired_All);
- with cert cons wtl;
- show ?thesis; by (auto simp add: wtl_inst_option_def);
- qed;
- qed simp;
- qed;
-qed;
+ assume cert:
+ "(cert ! (0 + length []) = None \\<longrightarrow> phi ! (0 + length []) = s0) \\<and>
+ (\\<forall>t. cert ! (0 + length []) = Some t \\<longrightarrow> phi ! (0 + length []) = t)"
+
+ show ?thesis
+ proof (cases "cert!0")
+ assume "cert!0 = None"
+ with cert
+ show ?thesis by simp
+ next
+ fix t; assume "cert!0 = Some t"
+ with cert
+ have "phi!0 = t"; by (simp del: split_paired_All);
+ with cert cons wtl;
+ show ?thesis; by (auto simp add: wtl_inst_option_def);
+ qed
+ qed simp
+qed
lemma wtl_method_correct:
-"wtl_method G C pTs rT mxl ins cert \\<Longrightarrow> \\<exists> phi. wt_method G C pTs rT mxl ins phi";
-proof (unfold wtl_method_def, simp del: split_paired_Ex, elim exE conjE);
- let "?s0" = "([], Some (Class C) # map Some pTs @ replicate mxl None)";
- fix s2;
- assume neqNil: "ins \\<noteq> []";
- assume wtl: "wtl_inst_list ins G rT ?s0 s2 cert (length ins) 0";
- thus ?thesis;
- obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \\<and> length ins < length phi";
- by (rule exists_phi [elimify]) blast;
- with wtl;
- have allpc:
- "\\<forall>pc. pc < length ins \\<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc";
- by elim (rule wtl_fits_wt [elimify]);
- from neqNil wtl fits;
- have "wt_start G C pTs mxl phi";
- by (elim conjE, unfold wt_start_def) (rule fits_first);
- with neqNil allpc fits;
- show ?thesis; by (auto simp add: wt_method_def);
- qed;
-qed;
+"wtl_method G C pTs rT mxl ins cert \\<Longrightarrow> \\<exists> phi. wt_method G C pTs rT mxl ins phi"
+proof (unfold wtl_method_def, simp del: split_paired_Ex, elim exE conjE)
+ let "?s0" = "([], Some (Class C) # map Some pTs @ replicate mxl None)"
+ fix s2
+ assume neqNil: "ins \\<noteq> []"
+ assume wtl: "wtl_inst_list ins G rT ?s0 s2 cert (length ins) 0"
+
+ from this
+ obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \\<and> length ins < length phi"
+ by (rule exists_phi [elimify]) blast;
+
+ with wtl
+ have allpc:
+ "\\<forall>pc. pc < length ins \\<longrightarrow> wt_instr (ins ! pc) G rT phi (length ins) pc"
+ by elim (rule wtl_fits_wt [elimify])
+
+ from neqNil wtl fits
+ have "wt_start G C pTs mxl phi"
+ by (elim conjE, unfold wt_start_def) (rule fits_first)
+
+ with neqNil allpc fits
+ show ?thesis by (auto simp add: wt_method_def)
+qed
lemma unique_set:
"(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (a',b',c',d') \\<in> set l \\<longrightarrow> a = a' \\<longrightarrow> b=b' \\<and> c=c' \\<and> d=d'";
@@ -405,7 +413,7 @@
theorem wtl_correct:
"wtl_jvm_prog G cert ==> \\<exists> Phi. wt_jvm_prog G Phi";
-proof (clarsimp_tac simp add: wt_jvm_prog_def wf_prog_def, intro conjI);
+proof (clarsimp simp add: wt_jvm_prog_def wf_prog_def, intro conjI);
assume wtl_prog: "wtl_jvm_prog G cert";
thus "ObjectC \\<in> set G"; by (simp add: wtl_jvm_prog_def wf_prog_def);
@@ -442,8 +450,8 @@
(\\<epsilon>(sg,rT,maxl,b). (sg, rT, maxl, b) \\<in> set mdecls \\<and> sg = sig))
(\\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \\<in> set G \\<and> Cl = a))) mb) m";
by - (drule bspec, assumption,
- clarsimp_tac elim: wtl_method_correct [elimify],
- clarsimp_tac intro: selectI simp add: unique_epsilon);
+ clarsimp elim: wtl_method_correct [elimify],
+ clarsimp intro: selectI simp add: unique_epsilon);
qed;
qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def);
qed;
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Mon Aug 07 10:29:54 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Mon Aug 07 14:32:56 2000 +0200
@@ -7,162 +7,33 @@
header {* Specification of the LBV *}
-theory LBVSpec = BVSpec:
+theory LBVSpec = Step :
types
certificate = "state_type option list"
class_certificate = "sig \\<Rightarrow> certificate"
prog_certificate = "cname \\<Rightarrow> class_certificate"
-
-consts
+constdefs
wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
-primrec
-"wtl_inst (Load idx) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- idx < length LT \\<and>
- (\\<exists>ts. (LT ! idx) = Some ts \\<and>
- (ts # ST , LT) = s'))"
-
-"wtl_inst (Store idx) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- idx < length LT \\<and>
- (\\<exists>ts ST'. ST = ts # ST' \\<and>
- (ST' , LT[idx:=Some ts]) = s'))"
-
-"wtl_inst (Bipush i) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- ((PrimT Integer) # ST , LT) = s')"
-
-"wtl_inst (Aconst_null) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- (NT # ST , LT) = s')"
-
-"wtl_inst (Getfield F C) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- is_class G C \\<and>
- (\\<exists>T oT ST'. field (G,C) F = Some(C,T) \\<and>
- ST = oT # ST' \\<and>
- G \\<turnstile> oT \\<preceq> (Class C) \\<and>
- (T # ST' , LT) = s'))"
-
-"wtl_inst (Putfield F C) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- is_class G C \\<and>
- (\\<exists>T vT oT ST'.
- field (G,C) F = Some(C,T) \\<and>
- ST = vT # oT # ST' \\<and>
- G \\<turnstile> oT \\<preceq> (Class C) \\<and>
- G \\<turnstile> vT \\<preceq> T \\<and>
- (ST' , LT) = s'))"
-
-"wtl_inst (New C) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- is_class G C \\<and>
- ((Class C) # ST , LT) = s')"
-
-"wtl_inst (Checkcast C) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- is_class G C \\<and>
- (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
- (Class C # ST' , LT) = s'))"
-
-"wtl_inst Pop G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- \\<exists>ts ST'. pc+1 < max_pc \\<and>
- ST = ts # ST' \\<and>
- (ST' , LT) = s')"
+"wtl_inst i G rT s s' cert max_pc pc \\<equiv> app (i,G,rT,s) \\<and>
+ (let s'' = the (step (i,G,s)) in
+ (\\<forall> pc' \\<in> (succs i pc). pc' < max_pc \\<and>
+ ((pc' \\<noteq> pc+1) \\<longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> s'' <=s the (cert!pc'))) \\<and>
+ (if (pc+1) \\<in> (succs i pc) then
+ s' = s''
+ else
+ cert ! (pc+1) = Some s'))"
-"wtl_inst Dup G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ts ST'. ST = ts # ST' \\<and>
- (ts # ts # ST' , LT) = s'))"
-
-"wtl_inst Dup_x1 G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and>
- (ts1 # ts2 # ts1 # ST' , LT) = s'))"
-
-"wtl_inst Dup_x2 G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and>
- (ts1 # ts2 # ts3 # ts1 # ST' , LT) = s'))"
-
-"wtl_inst Swap G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and>
- (ts # ts' # ST' , LT) = s'))"
-
-"wtl_inst IAdd G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- (\\<exists>ST'. ST = (PrimT Integer) # (PrimT Integer) # ST' \\<and>
- ((PrimT Integer) # ST' , LT) = s'))"
-
+lemma [simp]:
+"succs i pc = {pc+1} \\<Longrightarrow>
+ wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> pc+1 < max_pc \\<and> (s' = the (step (i,G,s))))"
+by (unfold wtl_inst_def, auto)
-"wtl_inst (Ifcmpeq branch) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and>
- (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>
- ((\\<exists>p. ts = PrimT p \\<and> ts' = PrimT p) \\<or>
- (\\<exists>r r'. ts = RefT r \\<and> ts' = RefT r')) \\<and>
- ((ST' , LT) = s') \\<and>
- cert ! (nat(int pc+branch)) \\<noteq> None \\<and>
- G \\<turnstile> (ST' , LT) <=s the (cert ! (nat(int pc+branch)))))"
-
-"wtl_inst (Goto branch) G rT s s' cert max_pc pc =
- ((let (ST,LT) = s
- in
- (nat(int pc+branch)) < max_pc \\<and> cert ! (nat(int pc+branch)) \\<noteq> None \\<and>
- G \\<turnstile> (ST , LT) <=s the (cert ! (nat(int pc+branch)))) \\<and>
- (cert ! (pc+1) = Some s'))"
-
-"wtl_inst (Invoke mn fpTs) G rT s s' cert max_pc pc =
- (let (ST,LT) = s
- in
- pc+1 < max_pc \\<and>
- (\\<exists>apTs X ST'. ST = (rev apTs) @ (X # ST') \\<and>
- length apTs = length fpTs \\<and>
- (\\<exists>s''. cert ! (pc+1) = Some s'' \\<and>
- ((s'' = s' \\<and> X = NT) \\<or>
- ((G \\<turnstile> s' <=s s'') \\<and> (\\<exists>C. X = Class C \\<and>
- (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
- (\\<exists>D rT b. method (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
- (rT # ST' , LT) = s')))))))"
-
-"wtl_inst Return G rT s s' cert max_pc pc =
- ((let (ST,LT) = s
- in
- (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT)) \\<and>
- (cert ! (pc+1) = Some s'))"
+lemma [simp]:
+"succs i pc = {} \\<Longrightarrow> wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> cert!(pc+1) = Some s')"
+by (unfold wtl_inst_def, auto)
constdefs
@@ -205,24 +76,13 @@
lemma wtl_inst_unique:
"wtl_inst i G rT s0 s1 cert max_pc pc \\<longrightarrow>
wtl_inst i G rT s0 s1' cert max_pc pc \\<longrightarrow> s1 = s1'" (is "?P i")
-proof (induct i)
-case Invoke
- have "\\<exists>x y. s0 = (x,y)" by (simp)
- thus "wtl_inst (Invoke mname list) G rT s0 s1 cert max_pc pc \\<longrightarrow>
- wtl_inst (Invoke mname list) G rT s0 s1' cert max_pc pc \\<longrightarrow>
- s1 = s1'"
- proof elim
- apply_end(clarsimp_tac, drule rev_eq, assumption+)
- qed auto
-qed auto
-
+by (unfold wtl_inst_def, auto)
lemma wtl_inst_option_unique:
"\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc;
wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'"
by (cases "cert!pc") (auto simp add: wtl_inst_unique wtl_inst_option_def)
-
lemma wtl_inst_list_unique:
"\\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \\<longrightarrow>
wtl_inst_list is G rT s0 s1' cert max_pc pc \\<longrightarrow> s1=s1'" (is "?P is")
@@ -239,14 +99,13 @@
assume a: "?l (a#list) s0 s1 pc"
assume b: "?l (a#list) s0 s1' pc"
with a
- show "s1 = s1'"
- obtain s s' where "?o s0 s" "?o s0 s'"
- and l: "?l list s s1 (Suc pc)"
- and l': "?l list s' s1' (Suc pc)" by auto
- have "s=s'" by(rule wtl_inst_option_unique)
- with l l' Cons
- show ?thesis by blast
- qed
+ obtain s s' where "?o s0 s" "?o s0 s'"
+ and l: "?l list s s1 (Suc pc)"
+ and l': "?l list s' s1' (Suc pc)" by auto
+
+ have "s=s'" by(rule wtl_inst_option_unique)
+ with l l' Cons
+ show "s1 = s1'" by blast
qed
qed
@@ -279,25 +138,21 @@
thus ?thesis by blast
next
case Suc
- with wtl
- show ?thesis
- obtain s0 where wtlSuc: "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)"
- and wtlOpt: "wtl_inst_option a G rT s s0 cert mpc pc" by auto
- from Cons
- show ?thesis
- obtain a' b s1'
- where "a' @ b = list" "length a' = nat"
- and w:"wtl_inst_list a' G rT s0 s1' cert mpc (Suc pc)"
- and "wtl_inst_list b G rT s1' s' cert mpc (Suc pc + length a')"
- proof (elim allE impE)
- from length Suc show "nat < length list" by simp
- from wtlSuc show "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" .
- qed (elim exE conjE, auto)
- with Suc wtlOpt
- have "?E (a#a') b s1'" by (auto simp del: split_paired_Ex)
- thus ?thesis by blast
- qed
- qed
+ with wtl
+ obtain s0 where wtlSuc: "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)"
+ and wtlOpt: "wtl_inst_option a G rT s s0 cert mpc pc" by auto
+ from Cons
+ obtain a' b s1'
+ where "a' @ b = list" "length a' = nat"
+ and w:"wtl_inst_list a' G rT s0 s1' cert mpc (Suc pc)"
+ and "wtl_inst_list b G rT s1' s' cert mpc (Suc pc + length a')"
+ proof (elim allE impE)
+ from length Suc show "nat < length list" by simp
+ from wtlSuc show "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" .
+ qed (elim exE conjE, auto)
+ with Suc wtlOpt
+ have "?E (a#a') b s1'" by (auto simp del: split_paired_Ex)
+ thus ?thesis by blast
qed
qed
qed
@@ -311,36 +166,36 @@
"wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0"
"wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)"
-have
-"\\<forall> pc s0.
- wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \\<longrightarrow>
- wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \\<longrightarrow>
- wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x")
-proof (induct "?P" "x")
- case Nil
- show "?P []" by simp
-next
- case Cons
- show "?P (a#list)"
- proof intro
- fix pc s0
- assume y:
- "wtl_inst_list y G rT s1 s2 cert (pc + length ((a # list) @ y)) (pc + length (a # list))"
- assume al:
- "wtl_inst_list (a # list) G rT s0 s1 cert (pc + length ((a # list) @ y)) pc"
- thus "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc"
+ have
+ "\\<forall> pc s0.
+ wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \\<longrightarrow>
+ wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \\<longrightarrow>
+ wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x")
+ proof (induct "?P" "x")
+ case Nil
+ show "?P []" by simp
+ next
+ case Cons
+ show "?P (a#list)"
+ proof intro
+ fix pc s0
+ assume y:
+ "wtl_inst_list y G rT s1 s2 cert (pc + length ((a # list) @ y)) (pc + length (a # list))"
+ assume al:
+ "wtl_inst_list (a # list) G rT s0 s1 cert (pc + length ((a # list) @ y)) pc"
+ from this
obtain s' where
- a: "wtl_inst_option a G rT s0 s' cert (Suc pc + length (list@y)) pc" and
- l: "wtl_inst_list list G rT s' s1 cert (Suc pc + length (list@y)) (Suc pc)" by auto
+ a: "wtl_inst_option a G rT s0 s' cert (Suc pc + length (list@y)) pc" and
+ l: "wtl_inst_list list G rT s' s1 cert (Suc pc + length (list@y)) (Suc pc)" by auto
with y Cons
have "wtl_inst_list (list @ y) G rT s' s2 cert (Suc pc + length (list @ y)) (Suc pc)"
by (elim allE impE) (assumption, simp+)
with a
- show ?thesis by (auto simp del: split_paired_Ex)
+ show "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc"
+ by (auto simp del: split_paired_Ex)
qed
qed
-qed
-
+
with w
show ?thesis
proof (elim allE impE)
@@ -390,18 +245,18 @@
assume y: "?y s0 pc"
assume z: "?z s0 pc"
assume "?x s0 pc"
- thus "?p s0 pc"
- obtain s0' where opt: "wtl_inst_option a G rT s0 s0' cert (pc + length ((a # list) @ i # b)) pc"
- and list: "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)"
- by (auto simp del: split_paired_Ex)
- with y z Cons
- have "wtl_inst_list (list @ [i]) G rT s0' s2 cert (Suc pc + length (list @ i # b)) (Suc pc)"
- proof (elim allE impE)
- from list show "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" .
- qed auto
- with opt
- show ?thesis by (auto simp del: split_paired_Ex)
- qed
+ from this
+ obtain s0' where opt: "wtl_inst_option a G rT s0 s0' cert (pc + length ((a # list) @ i # b)) pc"
+ and list: "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)"
+ by (auto simp del: split_paired_Ex)
+ with y z Cons
+ have "wtl_inst_list (list @ [i]) G rT s0' s2 cert (Suc pc + length (list @ i # b)) (Suc pc)"
+ proof (elim allE impE)
+ from list show "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" .
+ qed auto
+ with opt
+ show "?p s0 pc"
+ by (auto simp del: split_paired_Ex)
qed
qed
with a i b
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Step.thy Mon Aug 07 14:32:56 2000 +0200
@@ -0,0 +1,718 @@
+(* Title: HOL/MicroJava/BV/Step.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2000 Technische Universitaet Muenchen
+*)
+
+header {* Effect of instructions on the state type *}
+
+
+theory Step = Convert :
+
+
+(* effect of instruction on the state type *)
+consts
+step :: "instr \\<times> jvm_prog \\<times> state_type \\<Rightarrow> state_type option"
+
+recdef step "{}"
+"step (Load idx, G, (ST, LT)) = Some (the (LT ! idx) # ST, LT)"
+"step (Store idx, G, (ts#ST, LT)) = Some (ST, LT[idx:= Some ts])"
+"step (Bipush i, G, (ST, LT)) = Some (PrimT Integer # ST, LT)"
+"step (Aconst_null, G, (ST, LT)) = Some (NT#ST,LT)"
+"step (Getfield F C, G, (oT#ST, LT)) = Some (snd (the (field (G,C) F)) # ST, LT)"
+"step (Putfield F C, G, (vT#oT#ST, LT)) = Some (ST,LT)"
+"step (New C, G, (ST,LT)) = Some (Class C # ST, LT)"
+"step (Checkcast C, G, (RefT rt#ST,LT)) = Some (Class C # ST,LT)"
+"step (Pop, G, (ts#ST,LT)) = Some (ST,LT)"
+"step (Dup, G, (ts#ST,LT)) = Some (ts#ts#ST,LT)"
+"step (Dup_x1, G, (ts1#ts2#ST,LT)) = Some (ts1#ts2#ts1#ST,LT)"
+"step (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = Some (ts1#ts2#ts3#ts1#ST,LT)"
+"step (Swap, G, (ts1#ts2#ST,LT)) = Some (ts2#ts1#ST,LT)"
+"step (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT))
+ = Some (PrimT Integer#ST,LT)"
+"step (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = Some (ST,LT)"
+"step (Goto b, G, s) = Some s"
+"step (Return, G, (T#ST,LT)) = None" (* Return has no successor instruction in the same method *)
+"step (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST in
+ Some (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))"
+
+"step (i,G,s) = None"
+
+
+(* conditions under which step is applicable *)
+consts
+app :: "instr \\<times> jvm_prog \\<times> ty \\<times> state_type \\<Rightarrow> bool"
+
+recdef app "{}"
+"app (Load idx, G, rT, s) = (idx < length (snd s) \\<and> (snd s) ! idx \\<noteq> None)"
+"app (Store idx, G, rT, (ts#ST, LT)) = (idx < length LT)"
+"app (Bipush i, G, rT, s) = True"
+"app (Aconst_null, G, rT, s) = True"
+"app (Getfield F C, G, rT, (oT#ST, LT)) = (is_class G C \\<and>
+ field (G,C) F \\<noteq> None \\<and>
+ fst (the (field (G,C) F)) = C \\<and>
+ G \\<turnstile> oT \\<preceq> (Class C))"
+"app (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \\<and>
+ field (G,C) F \\<noteq> None \\<and>
+ fst (the (field (G,C) F)) = C \\<and>
+ G \\<turnstile> oT \\<preceq> (Class C) \\<and>
+ G \\<turnstile> vT \\<preceq> (snd (the (field (G,C) F))))"
+"app (New C, G, rT, s) = (is_class G C)"
+"app (Checkcast C, G, rT, (RefT rt#ST,LT)) = (is_class G C)"
+"app (Pop, G, rT, (ts#ST,LT)) = True"
+"app (Dup, G, rT, (ts#ST,LT)) = True"
+"app (Dup_x1, G, rT, (ts1#ts2#ST,LT)) = True"
+"app (Dup_x2, G, rT, (ts1#ts2#ts3#ST,LT)) = True"
+"app (Swap, G, rT, (ts1#ts2#ST,LT)) = True"
+"app (IAdd, G, rT, (PrimT Integer#PrimT Integer#ST,LT))
+ = True"
+"app (Ifcmpeq b, G, rT, (ts1#ts2#ST,LT)) = ((\\<exists> p. ts1 = PrimT p \\<and> ts1 = PrimT p) \\<or>
+ (\\<exists>r r'. ts1 = RefT r \\<and> ts2 = RefT r'))"
+"app (Goto b, G, rT, s) = True"
+"app (Return, G, rT, (T#ST,LT)) = (G \\<turnstile> T \\<preceq> rT)"
+app_invoke:
+"app (Invoke C mn fpTs, G, rT, s) = (length fpTs < length (fst s) \\<and>
+ (let
+ apTs = rev (take (length fpTs) (fst s));
+ X = hd (drop (length fpTs) (fst s))
+ in
+ G \\<turnstile> X \\<preceq> Class C \\<and>
+ (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
+ method (G,C) (mn,fpTs) \\<noteq> None
+ ))"
+
+"app (i,G,rT,s) = False"
+
+
+(* p_count of successor instructions *)
+consts
+succs :: "instr \\<Rightarrow> p_count \\<Rightarrow> p_count set"
+
+primrec
+"succs (Load idx) pc = {pc+1}"
+"succs (Store idx) pc = {pc+1}"
+"succs (Bipush i) pc = {pc+1}"
+"succs (Aconst_null) pc = {pc+1}"
+"succs (Getfield F C) pc = {pc+1}"
+"succs (Putfield F C) pc = {pc+1}"
+"succs (New C) pc = {pc+1}"
+"succs (Checkcast C) pc = {pc+1}"
+"succs Pop pc = {pc+1}"
+"succs Dup pc = {pc+1}"
+"succs Dup_x1 pc = {pc+1}"
+"succs Dup_x2 pc = {pc+1}"
+"succs Swap pc = {pc+1}"
+"succs IAdd pc = {pc+1}"
+"succs (Ifcmpeq b) pc = {pc+1, nat (int pc + b)}"
+"succs (Goto b) pc = {nat (int pc + b)}"
+"succs Return pc = {}"
+"succs (Invoke C mn fpTs) pc = {pc+1}"
+
+
+lemma 1: "2 < length a \\<Longrightarrow> (\\<exists>l l' l'' ls. a = l#l'#l''#ls)"
+proof (cases a)
+ fix x xs assume "a = x#xs" "2 < length a"
+ thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
+qed auto
+
+lemma 2: "\\<not>(2 < length a) \\<Longrightarrow> a = [] \\<or> (\\<exists> l. a = [l]) \\<or> (\\<exists> l l'. a = [l,l'])"
+proof -;
+ assume "\\<not>(2 < length a)"
+ hence "length a < (Suc 2)" by simp
+ hence * : "length a = 0 \\<or> length a = 1 \\<or> length a = 2" by (auto simp add: less_Suc_eq)
+
+ {
+ fix x
+ assume "length x = 1"
+ hence "\\<exists> l. x = [l]" by - (cases x, auto)
+ } note 0 = this
+
+ have "length a = 2 \\<Longrightarrow> \\<exists>l l'. a = [l,l']" by (cases a, auto dest: 0)
+ with * show ?thesis by (auto dest: 0)
+qed
+
+lemma appStore[simp]:
+"app (Store idx, G, rT, s) = (\\<exists> ts ST LT. s = (ts#ST,LT) \\<and> idx < length LT)" (is "?app s = ?P s")
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appGetField[simp]:
+"app (Getfield F C, G, rT, s) = (\\<exists> oT ST LT. s = (oT#ST, LT) \\<and> is_class G C \\<and>
+ fst (the (field (G,C) F)) = C \\<and>
+ field (G,C) F \\<noteq> None \\<and> G \\<turnstile> oT \\<preceq> (Class C))" (is "?app s = ?P s")
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appPutField[simp]:
+"app (Putfield F C, G, rT, s) = (\\<exists> vT oT ST LT. s = (vT#oT#ST, LT) \\<and> is_class G C \\<and>
+ field (G,C) F \\<noteq> None \\<and> fst (the (field (G,C) F)) = C \\<and>
+ G \\<turnstile> oT \\<preceq> (Class C) \\<and>
+ G \\<turnstile> vT \\<preceq> (snd (the (field (G,C) F))))" (is "?app s = ?P s")
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appCheckcast[simp]:
+"app (Checkcast C, G, rT, s) = (\\<exists>rT ST LT. s = (RefT rT#ST,LT) \\<and> is_class G C)" (is "?app s = ?P s")
+by (cases s, cases "fst s", simp, cases "hd (fst s)", auto)
+
+lemma appPop[simp]:
+"app (Pop, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))" (is "?app s = ?P s")
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appDup[simp]:
+"app (Dup, G, rT, s) = (\\<exists>ts ST LT. s = (ts#ST,LT))" (is "?app s = ?P s")
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appDup_x1[simp]:
+"app (Dup_x1, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" (is "?app s = ?P s")
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appDup_x2[simp]:
+"app (Dup_x2, G, rT, s) = (\\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"(is "?app s = ?P s")
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appSwap[simp]:
+"app (Swap, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" (is "?app s = ?P s")
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appIAdd[simp]:
+"app (IAdd, G, rT, s) = (\\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))" (is "?app s = ?P s")
+proof (cases s)
+ case Pair
+ have "?app (a,b) = ?P (a,b)"
+ proof (cases "a")
+ fix t ts assume a: "a = t#ts"
+ show ?thesis
+ proof (cases t)
+ fix p assume p: "t = PrimT p"
+ show ?thesis
+ proof (cases p)
+ assume ip: "p = Integer"
+ show ?thesis
+ proof (cases ts)
+ fix t' ts' assume t': "ts = t' # ts'"
+ show ?thesis
+ proof (cases t')
+ fix p' assume "t' = PrimT p'"
+ with t' ip p a
+ show ?thesis by - (cases p', auto)
+ qed (auto simp add: a p ip t')
+ qed (auto simp add: a p ip)
+ qed (auto simp add: a p)
+ qed (auto simp add: a)
+ qed auto
+ with Pair show ?thesis by simp
+qed
+
+
+lemma appIfcmpeq[simp]:
+"app (Ifcmpeq b, G, rT, s) = (\\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \\<and>
+ ((\\<exists> p. ts1 = PrimT p \\<and> ts1 = PrimT p) \\<or>
+ (\\<exists>r r'. ts1 = RefT r \\<and> ts2 = RefT r')))"
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appReturn[simp]:
+"app (Return, G, rT, s) = (\\<exists>T ST LT. s = (T#ST,LT) \\<and> (G \\<turnstile> T \\<preceq> rT))"
+by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+
+
+lemma appInvoke[simp]:
+"app (Invoke C mn fpTs, G, rT, s) = (\\<exists>apTs X ST LT.
+ s = ((rev apTs) @ (X # ST), LT) \\<and>
+ length apTs = length fpTs \\<and>
+ G \\<turnstile> X \\<preceq> Class C \\<and>
+ (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
+ method (G,C) (mn,fpTs) \\<noteq> None)" (is "?app s = ?P s")
+proof (cases s)
+ case Pair
+ have "?app (a,b) \\<Longrightarrow> ?P (a,b)"
+ proof -
+ assume app: "?app (a,b)"
+ hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \\<and> length fpTs < length a"
+ (is "?a \\<and> ?l") by auto
+ hence "?a \\<and> 0 < length (drop (length fpTs) a)" (is "?a \\<and> ?l") by auto
+ hence "?a \\<and> ?l \\<and> length (rev (take (length fpTs) a)) = length fpTs" by (auto simp add: min_def)
+ hence "\\<exists>apTs ST. a = rev apTs @ ST \\<and> length apTs = length fpTs \\<and> 0 < length ST" by blast
+ hence "\\<exists>apTs ST. a = rev apTs @ ST \\<and> length apTs = length fpTs \\<and> ST \\<noteq> []" by blast
+ hence "\\<exists>apTs ST. a = rev apTs @ ST \\<and> length apTs = length fpTs \\<and> (\\<exists>X ST'. ST = X#ST')" by (simp add: neq_Nil_conv)
+ hence "\\<exists>apTs X ST. a = rev apTs @ X # ST \\<and> length apTs = length fpTs" by blast
+ with app
+ show ?thesis by auto blast
+ qed
+ with Pair have "?app s \\<Longrightarrow> ?P s" by simp
+ thus ?thesis by auto
+qed
+
+lemmas [simp del] = app_invoke
+lemmas [trans] = sup_loc_trans
+
+ML_setup {* bind_thm ("widen_RefT", widen_RefT) *}
+ML_setup {* bind_thm ("widen_RefT2", widen_RefT2) *}
+
+
+
+lemma app_step_some:
+"\\<lbrakk>app (i,G,rT,s); succs i pc \\<noteq> {} \\<rbrakk> \\<Longrightarrow> step (i,G,s) \\<noteq> None";
+by (cases s, cases i, auto)
+
+lemma sup_state_length:
+"G \\<turnstile> s2 <=s s1 \\<Longrightarrow> length (fst s2) = length (fst s1) \\<and> length (snd s2) = length (snd s1)"
+ by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd)
+
+lemma PrimT_PrimT: "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)"
+proof
+ show "xb = PrimT p \\<Longrightarrow> G \\<turnstile> xb \\<preceq> PrimT p" by blast
+
+ show "G\\<turnstile> xb \\<preceq> PrimT p \\<Longrightarrow> xb = PrimT p"
+ proof (cases xb)
+ fix prim
+ assume "xb = PrimT prim" "G\\<turnstile>xb\\<preceq>PrimT p"
+ thus ?thesis by simp
+ next
+ fix ref
+ assume "G\\<turnstile>xb\\<preceq>PrimT p" "xb = RefT ref"
+ thus ?thesis by simp (rule widen_RefT [elimify], auto)
+ qed
+qed
+
+lemma sup_loc_some [rulify]:
+"\\<forall> y n. (G \\<turnstile> b <=l y) \\<longrightarrow> n < length y \\<longrightarrow> y!n = Some t \\<longrightarrow> (\\<exists>t. b!n = Some t \\<and> (G \\<turnstile> (b!n) <=o (y!n)))" (is "?P b")
+proof (induct "?P" b)
+ show "?P []" by simp
+
+ case Cons
+ show "?P (a#list)"
+ proof (clarsimp simp add: list_all2_Cons1 sup_loc_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 = Some t"
+
+ show "(\\<exists>t. (a # list) ! n = Some t) \\<and> G \\<turnstile>(a # list) ! n <=o Some t"
+ proof (cases n)
+ case 0
+ with * show ?thesis by (simp add: sup_ty_opt_some)
+ next
+ case Suc
+ with Cons *
+ show ?thesis by (simp add: sup_loc_def)
+ qed
+ qed
+qed
+
+
+lemma all_widen_is_sup_loc:
+"\\<forall>b. length a = length b \\<longrightarrow> (\\<forall>x\\<in>set (zip a b). x \\<in> widen G) = (G \\<turnstile> (map Some a) <=l (map Some b))"
+ (is "\\<forall>b. length a = length b \\<longrightarrow> ?Q a b" is "?P a")
+proof (induct "a")
+ show "?P []" by simp
+
+ fix l ls assume Cons: "?P ls"
+
+ show "?P (l#ls)"
+ proof (intro allI impI)
+ fix b
+ assume "length (l # ls) = length (b::ty list)"
+ with Cons
+ show "?Q (l # ls) b" by - (cases b, auto)
+ qed
+qed
+
+
+lemma append_length_n: "\\<forall>n. n \\<le> length x \\<longrightarrow> (\\<exists>a b. x = a@b \\<and> length a = n)" (is "?P x")
+proof (induct "?P" "x")
+ show "?P []" by simp
+
+ fix l ls assume Cons: "?P ls"
+
+ show "?P (l#ls)"
+ proof (intro allI impI)
+ fix n
+ assume l: "n \\<le> length (l # ls)"
+
+ show "\\<exists>a b. l # ls = a @ b \\<and> length a = n"
+ proof (cases n)
+ assume "n=0" thus ?thesis by simp
+ next
+ fix "n'" assume s: "n = Suc n'"
+ with l
+ have "n' \\<le> length ls" by simp
+ hence "\\<exists>a b. ls = a @ b \\<and> length a = n'" by (rule Cons [rulify])
+ thus ?thesis
+ proof elim
+ fix a b
+ assume "ls = a @ b" "length a = n'"
+ with s
+ have "l # ls = (l#a) @ b \\<and> length (l#a) = n" by simp
+ thus ?thesis by blast
+ qed
+ qed
+ qed
+qed
+
+
+
+lemma rev_append_cons:
+"\\<lbrakk>n < length x\\<rbrakk> \\<Longrightarrow> \\<exists>a b c. x = (rev a) @ b # c \\<and> length a = n"
+proof -
+ assume n: "n < length x"
+ hence "n \\<le> length x" by simp
+ hence "\\<exists>a b. x = a @ b \\<and> length a = n" by (rule append_length_n [rulify])
+ thus ?thesis
+ proof elim
+ fix r d assume x: "x = r@d" "length r = n"
+ with n
+ have "\\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
+
+ thus ?thesis
+ proof elim
+ fix b c
+ assume "d = b#c"
+ with x
+ have "x = (rev (rev r)) @ b # c \\<and> length (rev r) = n" by simp
+ thus ?thesis by blast
+ qed
+ qed
+qed
+
+
+lemma app_mono:
+"\\<lbrakk>G \\<turnstile> s2 <=s s1; app (i, G, rT, s1)\\<rbrakk> \\<Longrightarrow> app (i, G, rT, s2)";
+proof -
+ assume G: "G \\<turnstile> s2 <=s s1"
+ assume app: "app (i, G, rT, s1)"
+
+ show ?thesis
+ proof (cases i)
+ case Load
+
+ from G
+ have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length)
+
+ from G Load app
+ have "G \\<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
+
+ with G Load app l
+ show ?thesis by clarsimp (drule sup_loc_some, simp+)
+ next
+ case Store
+ with G app
+ show ?thesis
+ by - (cases s2,
+ auto dest: map_hd_tl simp add: sup_loc_Cons2 sup_loc_length sup_state_def)
+ next
+ case Bipush
+ thus ?thesis by simp
+ next
+ case Aconst_null
+ thus ?thesis by simp
+ next
+ case New
+ with app
+ show ?thesis by simp
+ next
+ case Getfield
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
+ next
+ case Putfield
+
+ with app
+ obtain vT oT ST LT b
+ where s1: "s1 = (vT # oT # ST, LT)" and
+ "field (G, cname) vname = Some (cname, b)"
+ "is_class G cname" and
+ oT: "G\\<turnstile> oT\\<preceq> (Class cname)" and
+ vT: "G\\<turnstile> vT\\<preceq> b"
+ by simp (elim exE conjE, simp, rule that)
+ moreover
+ from s1 G
+ obtain vT' oT' ST' LT'
+ where s2: "s2 = (vT' # oT' # ST', LT')" and
+ oT': "G\\<turnstile> oT' \\<preceq> oT" and
+ vT': "G\\<turnstile> vT' \\<preceq> vT"
+ by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
+ moreover
+ from vT' vT
+ have "G \\<turnstile> vT' \\<preceq> b" by (rule widen_trans)
+ moreover
+ from oT' oT
+ have "G\\<turnstile> oT' \\<preceq> (Class cname)" by (rule widen_trans)
+ ultimately
+ show ?thesis
+ by (auto simp add: Putfield)
+ next
+ case Checkcast
+ with app G
+ show ?thesis
+ by - (cases s2, auto intro: widen_RefT2 simp add: sup_state_Cons2)
+ next
+ case Return
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
+ next
+ case Pop
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case Dup
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case Dup_x1
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case Dup_x2
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case Swap
+ with app G
+ show ?thesis
+ by - (cases s2, clarsimp simp add: sup_state_Cons2)
+ next
+ case IAdd
+ with app G
+ show ?thesis
+ by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT)
+ next
+ case Goto
+ with app
+ show ?thesis by simp
+ next
+ case Ifcmpeq
+ with app G
+ show ?thesis
+ by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2)
+ next
+ case Invoke
+
+ with app
+ obtain apTs X ST LT where
+ s1: "s1 = (rev apTs @ X # ST, LT)" and
+ l: "length apTs = length list" and
+ C: "G \\<turnstile> X \\<preceq> Class cname" and
+ w: "\\<forall>x \\<in> set (zip apTs list). x \\<in> widen G" and
+ m: "method (G, cname) (mname, list) \\<noteq> None"
+ by (simp del: not_None_eq, elim exE conjE) (rule that)
+
+ obtain apTs' X' ST' LT' where
+ s2: "s2 = (rev apTs' @ X' # ST', LT')" and
+ l': "length apTs' = length list"
+ proof -
+ from l s1 G
+ have "length list < length (fst s2)"
+ by (simp add: sup_state_length)
+ hence "\\<exists>a b c. (fst s2) = rev a @ b # c \\<and> length a = length list"
+ by (rule rev_append_cons [rulify])
+ thus ?thesis
+ by - (cases s2, elim exE conjE, simp, rule that)
+ qed
+
+ from l l'
+ have "length (rev apTs') = length (rev apTs)" by simp
+
+ from this s1 s2 G
+ obtain
+ G': "G \\<turnstile> (apTs',LT') <=s (apTs,LT)"
+ "G \\<turnstile> X' \\<preceq> X" "G \\<turnstile> (ST',LT') <=s (ST,LT)"
+ by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1);
+
+ with C
+ have C': "G \\<turnstile> X' \\<preceq> Class cname"
+ by - (rule widen_trans, auto)
+
+ from G'
+ have "G \\<turnstile> map Some apTs' <=l map Some apTs"
+ by (simp add: sup_state_def)
+ also
+ from l w
+ have "G \\<turnstile> map Some apTs <=l map Some list"
+ by (simp add: all_widen_is_sup_loc)
+ finally
+ have "G \\<turnstile> map Some apTs' <=l map Some list" .
+
+ with l'
+ have w': "\\<forall>x \\<in> set (zip apTs' list). x \\<in> widen G"
+ by (simp add: all_widen_is_sup_loc)
+
+ from Invoke s2 l' w' C' m
+ show ?thesis
+ by simp blast
+ qed
+qed
+
+
+lemma step_mono:
+"\\<lbrakk>succs i pc \\<noteq> {}; app (i,G,rT,s2); G \\<turnstile> s1 <=s s2\\<rbrakk> \\<Longrightarrow>
+ G \\<turnstile> the (step (i,G,s1)) <=s the (step (i,G,s2))"
+proof (cases s1, cases s2)
+ fix a1 b1 a2 b2
+ assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
+ assume succs: "succs i pc \\<noteq> {}"
+ assume app2: "app (i,G,rT,s2)"
+ assume G: "G \\<turnstile> s1 <=s s2"
+
+ from G app2
+ have app1: "app (i,G,rT,s1)" by (rule app_mono)
+
+ from app1 app2 succs
+ obtain a1' b1' a2' b2'
+ where step: "step (i,G,s1) = Some (a1',b1')" "step (i,G,s2) = Some (a2',b2')";
+ by (auto dest: app_step_some);
+
+ have "G \\<turnstile> (a1',b1') <=s (a2',b2')"
+ proof (cases i)
+ case Load
+
+ with s app1
+ obtain y where
+ y: "nat < length b1" "b1 ! nat = Some y" by clarsimp
+
+ from Load s app2
+ obtain y' where
+ y': "nat < length b2" "b2 ! nat = Some y'" by clarsimp
+
+ from G s
+ have "G \\<turnstile> b1 <=l b2" by (simp add: sup_state_def)
+
+ 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)
+ next
+ case Store
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_def sup_loc_update)
+ next
+ case Bipush
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case New
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Aconst_null
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Getfield
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Putfield
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Checkcast
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Invoke
+
+ with s app1
+ obtain a X ST where
+ s1: "s1 = (a @ X # ST, b1)" and
+ l: "length a = length list"
+ by (simp, elim exE conjE, simp)
+
+ from Invoke s app2
+ obtain a' X' ST' where
+ s2: "s2 = (a' @ X' # ST', b2)" and
+ l': "length a' = length list"
+ by (simp, elim exE conjE, simp)
+
+ from l l'
+ have lr: "length a = length a'" by simp
+
+ from lr G s s1 s2
+ have "G \\<turnstile> (ST, b1) <=s (ST', b2)"
+ by (simp add: sup_state_append_fst sup_state_Cons1)
+
+ moreover
+
+ from Invoke G s step app1 app2
+ have "b1 = b1' \\<and> b2 = b2'" by simp
+
+ ultimately
+
+ have "G \\<turnstile> (ST, b1') <=s (ST', b2')" by simp
+
+ with Invoke G s step app1 app2 s1 s2 l l'
+ show ?thesis
+ by (clarsimp simp add: sup_state_def)
+ next
+ case Return
+ with succs have "False" by simp
+ thus ?thesis by blast
+ next
+ case Pop
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Dup
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Dup_x1
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Dup_x2
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Swap
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case IAdd
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ next
+ case Goto
+ with G s step app1 app2
+ show ?thesis by simp
+ next
+ case Ifcmpeq
+ with G s step app1 app2
+ show ?thesis
+ by (clarsimp simp add: sup_state_Cons1)
+ qed
+
+ with step
+ show ?thesis by auto
+qed
+
+
+
+end