--- a/src/HOL/MicroJava/BV/LBVCorrect.ML Thu Mar 09 13:55:39 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.ML Thu Mar 09 13:56:54 2000 +0100
@@ -5,12 +5,7 @@
*)
-Goalw[fits_def,fits_partial_def] "fits_partial phi 0 is G rT s0 s2 cert = fits phi is G rT s0 s2 cert";
-by (Simp_tac 1);
-qed "fits_eq_fits_partial";
-
-
-Goal "\\<exists> l. n = length l";
+Goal "\\<exists> l. n < length l";
by (induct_tac "n" 1);
by Auto_tac;
by (res_inst_tac [("x","x#l")] exI 1);
@@ -19,7 +14,7 @@
Goal "\\<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)";
+\ \\<longrightarrow> (\\<exists> phi. pc + length is < length phi \\<and> fits_partial phi pc is G rT s0 s2 cert)";
by (induct_tac "is" 1);
by (asm_full_simp_tac (simpset() addsimps [fits_partial_def, exists_list]) 1);
by (Clarify_tac 1);
@@ -68,21 +63,21 @@
bind_thm ("exists_phi_partial", result() RS spec RS spec);
-Goal "wtl_inst_list is G rT s0 s2 cert (length is) 0 \\<Longrightarrow> \\<exists> phi. fits phi is G rT s0 s2 cert";
+Goal "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";
by (cut_inst_tac [("is","is"),("G","G"),("rT","rT"),("s2.0","s2"),("x","0"),("xa","s0"),("cert","cert")] exists_phi_partial 1);
-by (asm_full_simp_tac (simpset() addsimps [fits_eq_fits_partial]) 1);
+by (asm_full_simp_tac (simpset() addsimps [fits_def]) 1);
by (Force_tac 1);
qed "exists_phi";
Goal "\\<lbrakk>wtl_inst_list is G rT s0 s3 cert (length is) 0; \
-\fits phi is G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow> \
-\ \\<forall> pc t. pc < length is \\<longrightarrow> (cert ! pc) = Some t \\<longrightarrow> (phi ! pc) = t";
+\ fits phi is G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow> \
+\ \\<forall> pc t. pc < length is \\<longrightarrow> (cert ! pc) = Some t \\<longrightarrow> (phi ! pc) = t";
by (Clarify_tac 1);
by (forward_tac [wtl_partial] 1);
ba 1;
by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [fits_def,neq_Nil_conv]) 1);
+by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def ,neq_Nil_conv]) 1);
by (Clarify_tac 1);
by (eres_inst_tac [("x","aa")] allE 1);
by (eres_inst_tac [("x","ys")] allE 1);
@@ -106,7 +101,7 @@
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
by (exhaust_tac "cert!(Suc (length a))" 1);
- by (asm_full_simp_tac (simpset() addsimps [fits_def]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def]) 1);
by (eres_inst_tac [("x","a@[i]")] allE 1);
by (eres_inst_tac [("x","ys")] allE 1);
by (eres_inst_tac [("x","y")] allE 1);
@@ -116,7 +111,7 @@
be impE 1;
by (Force_tac 1);
by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [fits_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def]) 1);
by (eres_inst_tac [("x","a@[i]")] allE 1);
by (eres_inst_tac [("x","ys")] allE 1);
by (eres_inst_tac [("x","y")] allE 1);
@@ -130,15 +125,19 @@
qed "wtl_suc_pc";
-Goalw[fits_def] "\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; \
+Goal "\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; \
\ wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); \
\ fits phi (a@i#b) G rT s0 s3 cert; cert!(length a) = None; \
\ wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \
\ \\<Longrightarrow> phi!(length a) = s1";
+by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def]) 1);
by (eres_inst_tac [("x","a")] allE 1);
by (eres_inst_tac [("x","b")] allE 1);
by (eres_inst_tac [("x","i")] allE 1);
-by (eres_inst_tac [("x","s1")] allE 1);
+by (Asm_full_simp_tac 1);
+by (pair_tac "s1" 1);
+by (eres_inst_tac [("x","x")] allE 1);
+by (eres_inst_tac [("x","y")] allE 1);
by (Asm_full_simp_tac 1);
be impE 1;
by (pair_tac "s2" 1);
@@ -146,7 +145,6 @@
ba 1;
qed "fits_lemma2";
-
fun ls g1 g2 = if g1 > g2 then ls g2 g1
else if g1 = g2 then [g1]
else g2::(ls g1 (g2-1))
@@ -177,7 +175,9 @@
by (thin_tac "\\<forall>pc t.\
\ pc < length (i1 @ i # i2) \\<longrightarrow> \
\ cert ! pc = Some t \\<longrightarrow> phi ! pc = t" 1);
- by (force_tac (claset(), simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
+ by (pair_tac "s1" 1);
+ by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
+ by (Force_tac 1);
by (exhaust_tac "meth_ret" 1);
by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
by (exhaust_tac "branch" 2);
@@ -230,14 +230,12 @@
by (Force_tac 1);
qed "wtl_inst_list_correct";
-Goalw[fits_def] "\\<lbrakk>is \\<noteq> []; wtl_inst_list is G rT s0 s2 cert (length is) 0; \
-\ fits phi is G rT s0 s2 cert\\<rbrakk> \\<Longrightarrow> G \\<turnstile> s0 <=s phi ! 0";
+Goal "\\<lbrakk>is \\<noteq> []; wtl_inst_list is G rT s0 s2 cert (length is) 0; \
+\ fits phi is G rT s0 s2 cert\\<rbrakk> \\<Longrightarrow> G \\<turnstile> s0 <=s phi ! 0";
by (forw_inst_tac [("pc'","0")] wtl_partial 1);
by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [fits_def, fits_partial_def, neq_Nil_conv]) 1);
+by (Clarsimp_tac 1);
by (eres_inst_tac [("x","[]")] allE 1);
by (eres_inst_tac [("x","ys")] allE 1);
by (eres_inst_tac [("x","y")] allE 1);
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Mar 09 13:55:39 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Thu Mar 09 13:56:54 2000 +0100
@@ -10,19 +10,14 @@
constdefs
fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
-"fits phi is G rT s0 s2 cert \\<equiv> (\\<forall> a b i s1. (a@(i#b) = is) \\<longrightarrow>
- wtl_inst_list a G rT s0 s1 cert (length is) 0 \\<longrightarrow>
- wtl_inst_list (i#b) G rT s1 s2 cert (length is) (length a) \\<longrightarrow>
- ((cert!(length a) = None \\<longrightarrow> phi!(length a) = s1) \\<and>
- (\\<forall> t. cert!(length a) = Some t \\<longrightarrow> phi!(length a) = t)))"
-
+"fits phi is G rT s0 s2 cert \\<equiv> fits_partial phi 0 is G rT s0 s2 cert"
fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
"fits_partial phi pc is G rT s0 s2 cert \\<equiv> (\\<forall> a b i s1. (a@(i#b) = is) \\<longrightarrow>
wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \\<longrightarrow>
wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \\<longrightarrow>
- ((cert!(pc+length a) = None \\<longrightarrow> phi!(pc+length a) = s1) \\<and>
- (\\<forall> t. cert!(pc+length a) = Some t \\<longrightarrow> phi!(pc+length a) = t)))"
+ ((cert!(pc+length a) = None \\<longrightarrow> phi!(pc+length a) = s1) \\<and>
+ (\\<forall> t. cert!(pc+length a) = Some t \\<longrightarrow> phi!(pc+length a) = t)))"
end
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Thu Mar 09 13:55:39 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Thu Mar 09 13:56:54 2000 +0100
@@ -6,7 +6,7 @@
Specification of a lightweight bytecode verifier
*)
-LBVSpec = Convert + BVSpec +
+LBVSpec = BVSpec +
types
certificate = "state_type option list"
@@ -53,9 +53,9 @@
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'))"
+ ST = oT # ST' \\<and>
+ G \\<turnstile> oT \\<preceq> (Class C) \\<and>
+ (T # ST' , LT) = s'))"
"wtl_MO (Putfield F C) G s s' max_pc pc =
(let (ST,LT) = s
@@ -66,7 +66,7 @@
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> vT \\<preceq> T \\<and>
(ST' , LT) = s'))"
@@ -136,7 +136,9 @@
(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> (G \\<turnstile> ts \\<preceq> ts' \\<or> G \\<turnstile> ts' \\<preceq> ts) \\<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)))))"
@@ -147,22 +149,22 @@
(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'))"
-
- (* (pc+1 < max_pc \\<longrightarrow> ((cert ! (pc+1)) \\<noteq> None \\<and> s' = the (cert ! (pc+1)))) \\<and>
- (\\<not> pc+1 < max_pc \\<longrightarrow> s = s'))" *)
consts
- wtl_MI :: "[meth_inv,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
+ wtl_MI :: "[meth_inv,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
primrec
-"wtl_MI (Invoke mn fpTs) G s s' max_pc pc =
+"wtl_MI (Invoke mn fpTs) G s s' cert max_pc pc =
(let (ST,LT) = s
in
pc+1 < max_pc \\<and>
- (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and>
+ (\\<exists>apTs X ST'. ST = (rev apTs) @ (X # ST') \\<and>
length apTs = length fpTs \\<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')))"
+ (\\<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')))))))"
consts
wtl_MR :: "[meth_ret,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
@@ -172,9 +174,6 @@
in
(\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT)) \\<and>
(cert ! (pc+1) = Some s'))"
-(*
- (pc+1 < max_pc \\<longrightarrow> ((cert ! (pc+1)) \\<noteq> None \\<and> s' = the (cert ! (pc+1)))) \\<and>
- (\\<not> pc+1 < max_pc \\<longrightarrow> s' = s))" *)
consts
@@ -184,7 +183,7 @@
"wtl_inst (CO ins) G rT s s' cert max_pc pc = wtl_CO ins G s s' max_pc pc"
"wtl_inst (MO ins) G rT s s' cert max_pc pc = wtl_MO ins G s s' max_pc pc"
"wtl_inst (CH ins) G rT s s' cert max_pc pc = wtl_CH ins G s s' max_pc pc"
- "wtl_inst (MI ins) G rT s s' cert max_pc pc = wtl_MI ins G s s' max_pc pc"
+ "wtl_inst (MI ins) G rT s s' cert max_pc pc = wtl_MI ins G s s' cert max_pc pc"
"wtl_inst (MR ins) G rT s s' cert max_pc pc = wtl_MR ins G rT s s' cert max_pc pc"
"wtl_inst (OS ins) G rT s s' cert max_pc pc = wtl_OS ins s s' max_pc pc"
"wtl_inst (BR ins) G rT s s' cert max_pc pc = wtl_BR ins G s s' cert max_pc pc"
@@ -203,9 +202,6 @@
primrec
"wtl_inst_list [] G rT s0 s2 cert max_pc pc = (s0 = s2)"
- (* None \\<Rightarrow> (s0 = s2)
- | Some s0' \\<Rightarrow> (s0' = s2))" *)
-
"wtl_inst_list (instr#is) G rT s0 s2 cert max_pc pc =
(\\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \\<and>
wtl_inst_list is G rT s1 s2 cert max_pc (pc+1))"