# HG changeset patch
# User kleing
# Date 952606614 -3600
# Node ID e5b618f6824e04955f9de6ae488eff420adc01bd
# Parent  130109a9b8c16096a3824e8663c21be569822e49
tuned for completeness of LBV

diff -r 130109a9b8c1 -r e5b618f6824e src/HOL/MicroJava/BV/LBVCorrect.ML
--- 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);
diff -r 130109a9b8c1 -r e5b618f6824e src/HOL/MicroJava/BV/LBVCorrect.thy
--- 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
diff -r 130109a9b8c1 -r e5b618f6824e src/HOL/MicroJava/BV/LBVSpec.thy
--- 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))"