# HG changeset patch
# User kleing
# Date 950633471 -3600
# Node ID 6acc80f7f36f8a664edef0c4a825592b5b769921
# Parent  c587f5ac4a982b80d633824b5b1b84e975a3dc0d
lightweight bytecode verifier with correctness proof

diff -r c587f5ac4a98 -r 6acc80f7f36f src/HOL/MicroJava/BV/LBVCorrect.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/LBVCorrect.ML	Tue Feb 15 17:51:11 2000 +0100
@@ -0,0 +1,294 @@
+(*  Title:      HOL/MicroJava/BV/BVLcorrect.ML
+    ID:         $Id$
+    Author:     Gerwin Klein
+    Copyright   1999 Technische Universitaet Muenchen
+*)
+
+
+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";
+by (induct_tac "n" 1);
+by Auto_tac;
+by (res_inst_tac [("x","x#l")] exI 1);
+by (Simp_tac 1);
+qed "exists_list";
+
+
+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)";
+by (induct_tac "is" 1);
+ by (asm_full_simp_tac (simpset() addsimps [fits_partial_def, exists_list]) 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("x","ab")] allE 1);
+by (eres_inst_tac [("x","ba")] allE 1);
+by (eres_inst_tac [("x","Suc pc")] allE 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (exhaust_tac "cert ! pc" 1);
+ by (res_inst_tac [("x","phi[pc:=(aa, b)]")] exI 1);
+ by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
+ by (Clarify_tac 1);
+ by (exhaust_tac "ac" 1);
+  by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (Clarify_tac 1);
+ by (eres_inst_tac [("x","lista")] allE 1);
+ by (eres_inst_tac [("x","bb")] allE 1);
+ by (eres_inst_tac [("x","i")] allE 1);
+ by (Asm_full_simp_tac 1);
+ by (datac wtl_inst_option_unique 1 1);
+ by (Asm_full_simp_tac 1);
+ by (smp_tac 2 1);
+ be impE 1;
+  by (Force_tac 1);
+ ba 1;
+by (res_inst_tac [("x","phi[pc:=ac]")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [fits_partial_def]) 1);
+by (Clarify_tac 1);
+by (exhaust_tac "ad" 1);
+ by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("x","lista")] allE 1);
+by (eres_inst_tac [("x","bc")] allE 1);
+by (eres_inst_tac [("x","i")] allE 1);
+by (Asm_full_simp_tac 1);
+by (datac wtl_inst_option_unique 1 1);
+by (Asm_full_simp_tac 1);
+by (smp_tac 2 1);
+be impE 1;
+ by (Force_tac 1);
+ba 1;
+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";
+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 (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";
+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 (Clarify_tac 1);
+by (eres_inst_tac [("x","aa")] allE 1);
+by (eres_inst_tac [("x","ys")] allE 1);
+by (eres_inst_tac [("x","y")] allE 1);
+by (Asm_full_simp_tac 1);
+qed "fits_lemma1";
+
+
+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); \
+\     wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a)); \
+\     fits phi (a@i#b) G rT s0 s3 cert \\<rbrakk> \\<Longrightarrow> \
+\ b \\<noteq> [] \\<longrightarrow> G \\<turnstile> s2 <=s (phi ! (Suc (length a)))";
+by (forward_tac [wtl_append] 1);
+  ba 1;
+ ba 1;
+by (exhaust_tac "b=[]" 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 (exhaust_tac "cert!(Suc (length a))" 1);
+ by (asm_full_simp_tac (simpset() addsimps [fits_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);
+ by (Asm_full_simp_tac 1);
+ by (pair_tac "s2" 1);
+ by (smp_tac 2 1);
+ be impE 1;
+  by (Force_tac 1);
+ by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [fits_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);
+by (Asm_full_simp_tac 1);
+by (pair_tac "s2" 1);
+by (smp_tac 2 1);
+by (Clarify_tac 1);
+be impE 1;
+ by (Force_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [wtl_inst_option_def]) 1);
+qed "wtl_suc_pc";
+
+
+Goalw[fits_def] "\\<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 (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);
+be impE 1;
+ by (pair_tac "s2" 1);
+ by (Force_tac 1);
+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))
+fun GOALS t g1 g2 = EVERY (map t (ls g1 g2));
+
+Goal "is=(i1@i#i2) \\<longrightarrow> wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length is) 0 \\<longrightarrow> \
+\     wtl_inst_list i1 G rT s0 s1 cert (length is) 0 \\<longrightarrow> \
+\     wtl_inst_option i G rT s1 s2 cert (length is) (length i1) \\<longrightarrow> \
+\     wtl_inst_list i2 G rT s2 s3 cert (length is) (Suc (length i1)) \\<longrightarrow> \
+\     fits phi (i1@i#i2) G rT s0 s3 cert \\<longrightarrow> \
+\       wt_instr i G rT phi (length is) (length i1)";
+by (Clarify_tac 1);
+by (forward_tac [wtl_suc_pc] 1);
+by (TRYALL atac);
+by (forward_tac [fits_lemma1] 1);
+ ba 1;
+by (exhaust_tac "cert!(length i1)" 1);
+ by (forward_tac [fits_lemma2] 1);
+     by (TRYALL atac);
+ by (exhaust_tac "i" 1);
+        by (exhaust_tac "check_object" 4);
+        by (exhaust_tac "manipulate_object" 3);
+         by (exhaust_tac "create_object" 2);
+         by (exhaust_tac "load_and_store" 1);
+            by (GOALS (force_tac (claset(), 
+                simpset() addsimps [wt_instr_def,wtl_inst_option_def])) 1 8);
+    by (exhaust_tac "meth_inv" 1);
+    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 (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);
+   by (exhaust_tac "op_stack" 1);
+       by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 
+                  THEN_MAYBE' Force_tac) 1 7);
+by (forw_inst_tac [("x","length i1")] spec 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (exhaust_tac "i" 1);
+       by (exhaust_tac "check_object" 4);
+       by (exhaust_tac "manipulate_object" 3);
+        by (exhaust_tac "create_object" 2);
+        by (exhaust_tac "load_and_store" 1);
+           by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 
+                      THEN' Force_tac) 1 8);
+   by (exhaust_tac "meth_inv" 1);
+   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 (exhaust_tac "branch" 3);
+   by (exhaust_tac "op_stack" 2);
+       by (exhaust_tac "meth_ret" 1);
+       by (GOALS (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 
+                  THEN_MAYBE' Force_tac) 1 8);
+qed "wtl_lemma";
+
+Goal "\\<lbrakk>wtl_inst_list is G rT s0 s2 cert (length is) 0; \
+\     fits phi is G rT s0 s2 cert\\<rbrakk> \
+\ \\<Longrightarrow> \\<forall>pc. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
+by (Clarify_tac 1);
+by (forward_tac [wtl_partial] 1);
+ba 1;
+by (Clarify_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 (cut_inst_tac [("is","a@y#ys"),("i1.0","a"),("i2.0","ys"),("i","y"),("G","G"),("rT","rT"),("s0.0","s0"),("cert","cert"),("phi","phi"),("s1.0","(aa,ba)"),("s2.0","(ab,b)"),("s3.0","s2")] wtl_lemma 1);
+by (asm_full_simp_tac (simpset() addsimps [nth_append]) 1);
+qed "wtl_fits_wt";
+
+
+Goal "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";
+by (forward_tac [exists_phi] 1);
+by (Clarify_tac 1);
+by (forward_tac [wtl_fits_wt] 1);
+ba 1;
+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";
+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 (eres_inst_tac [("x","[]")] allE 1);
+by (eres_inst_tac [("x","ys")] allE 1);
+by (eres_inst_tac [("x","y")] allE 1);
+by (Asm_full_simp_tac 1);
+be impE 1;
+by (Force_tac 1);
+by (exhaust_tac "cert ! 0" 1);
+by (auto_tac (claset(), simpset() addsimps [wtl_inst_option_def]));
+qed "fits_first";
+
+
+Goal "wtl_method G C pTs rT mxl ins cert \\<Longrightarrow> \\<exists> phi. wt_method G C pTs rT mxl ins phi";
+by (asm_full_simp_tac (simpset() addsimps [wtl_method_def, wt_method_def, wt_start_def]) 1);
+by (Clarify_tac 1);
+by (forward_tac [exists_phi] 1);
+by (Clarify_tac 1);
+by (forward_tac [wtl_fits_wt] 1);
+ba 1;
+by (res_inst_tac [("x","phi")] exI 1);
+by (auto_tac (claset(), simpset() addsimps [fits_first]));
+qed "wtl_method_correct";
+
+Goal "(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'";
+by (induct_tac "l" 1);
+by Auto_tac;
+qed_spec_mp "unique_set";
+
+Goal "(a,b,c,d)\\<in>set l \\<longrightarrow> unique l \\<longrightarrow> (\\<epsilon> (a',b',c',d'). (a',b',c',d') \\<in> set l \\<and> a'=a) = (a,b,c,d)";
+by (auto_tac (claset(), simpset() addsimps [unique_set]));
+qed_spec_mp "unique_epsilon";
+
+Goalw[wtl_jvm_prog_def,wt_jvm_prog_def] "wtl_jvm_prog G cert ==> \\<exists> Phi. wt_jvm_prog G Phi";
+by (asm_full_simp_tac (simpset() addsimps [wf_prog_def, wf_cdecl_def, wf_mdecl_def]) 1);
+by (res_inst_tac [("x",
+  "\\<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\
+\        \\<epsilon> phi. wt_method G C (snd sig) rT maxl b phi")] exI 1);
+by Safe_tac;
+by (GOALS Force_tac 1 3);
+by (GOALS Force_tac 2 3);
+by (eres_inst_tac [("x","(a, aa, ab, b)")] BallE 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("x","((ac, ba), ad, ae, bb)")] BallE 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+bd wtl_method_correct 1;
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [unique_epsilon]) 1);
+br selectI 1;
+ba 1;
+qed "wtl_correct";
+
diff -r c587f5ac4a98 -r 6acc80f7f36f src/HOL/MicroJava/BV/LBVCorrect.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Feb 15 17:51:11 2000 +0100
@@ -0,0 +1,28 @@
+(*  Title:      HOL/MicroJava/BV/BVLcorrect.thy
+    ID:         $Id$
+    Author:     Gerwin Klein
+    Copyright   1999 Technische Universitaet Muenchen
+
+    Correctness of the lightweight bytecode verifier
+*)
+
+LBVCorrect = LBVSpec +
+
+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_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)))"
+  
+  
+end
diff -r c587f5ac4a98 -r 6acc80f7f36f src/HOL/MicroJava/BV/LBVSpec.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/LBVSpec.ML	Tue Feb 15 17:51:11 2000 +0100
@@ -0,0 +1,122 @@
+(*  Title:      HOL/MicroJava/BV/BVLightSpec.ML
+    ID:         $Id$
+    Author:     Gerwin Klein
+    Copyright   1999 Technische Universitaet Muenchen
+*)
+
+Goal "\\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\\<rbrakk> \\<Longrightarrow> a = x \\<and> b = y \\<and> c = z";
+by Auto_tac;
+qed "rev_eq";
+
+
+Goal "\\<lbrakk>wtl_inst i G rT s0 s1 cert max_pc pc; \
+\      wtl_inst i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'";
+by (exhaust_tac "i" 1);
+by (exhaust_tac "branch" 8);
+by (exhaust_tac "op_stack" 7);
+by (exhaust_tac "meth_ret" 6);
+by (exhaust_tac "meth_inv" 5);
+by (exhaust_tac "check_object" 4);
+by (exhaust_tac "manipulate_object" 3);
+by (exhaust_tac "create_object" 2);
+by (exhaust_tac "load_and_store" 1);
+by Auto_tac;
+by (ALLGOALS (dtac rev_eq));
+by (TRYALL atac);
+by (ALLGOALS Asm_full_simp_tac);
+qed "wtl_inst_unique";
+
+
+Goal "\\<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 (exhaust_tac "cert!pc" 1);
+by (auto_tac (claset(), simpset() addsimps [wtl_inst_unique, wtl_inst_option_def]));
+qed "wtl_inst_option_unique";
+
+Goal "\\<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'";
+by (induct_tac "is" 1);
+ by Auto_tac;
+by (datac wtl_inst_option_unique 1 1);
+by (Asm_full_simp_tac 1);
+qed "wtl_inst_list_unique";
+
+Goal "\\<forall> pc' pc s. \
+\       wtl_inst_list is G rT s s' cert mpc pc \\<longrightarrow> \
+\       pc' < length is \\<longrightarrow> \
+\       (\\<exists> a b s1. a @ b = is \\<and> length a = pc' \\<and> \
+\                  wtl_inst_list a G rT s  s1 cert mpc pc \\<and> \
+\                  wtl_inst_list b G rT s1 s' cert mpc (pc+length a))";
+by(induct_tac "is" 1);
+ by Auto_tac;
+by (exhaust_tac "pc'" 1);
+ by (dres_inst_tac [("x","pc'")] spec 1);
+ by (smp_tac 3 1);
+ by (res_inst_tac [("x","[]")] exI 1);
+ by (Asm_full_simp_tac 1);
+ by (exhaust_tac "cert!pc" 1);
+  by (Force_tac 1);
+ by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
+by (dres_inst_tac [("x","nat")] spec 1);
+by (smp_tac 3 1);
+by Safe_tac;
+ by (res_inst_tac [("x","a#list")] exI 1);
+ by (Asm_full_simp_tac 1);
+by (res_inst_tac [("x","a#ac")] exI 1);
+by (Force_tac 1);
+qed_spec_mp "wtl_partial";
+
+
+Goal "\\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \\<longrightarrow> \
+\       wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \\<longrightarrow> \
+\       wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc (pc + length a)) \\<longrightarrow> \
+\         wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc";
+by (induct_tac "a" 1);
+ by (Clarify_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (pair_tac "s2" 1);
+ by (Force_tac 1);
+(* ---- 
+ by (exhaust_tac "cert!Suc pc" 1);
+  by (exhaust_tac "cert!pc" 1);
+   by (Force_tac 1);
+ by (res_inst_tac [("x","fst aa")] exI 1);
+ by (res_inst_tac [("x","snd aa")] exI 1);
+  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
+ by (exhaust_tac "cert!pc" 1);
+  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
+ by (Asm_full_simp_tac 1);
+  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
+ 
+
+  by (exhaust_tac "cert!pc" 1);
+   by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
+   by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
+   by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
+
+
+ by (res_inst_tac [("x","x")] exI 1);
+ by (res_inst_tac [("x","y")] exI 1);
+ by (exhaust_tac "cert!pc" 1);
+  by (exhaust_tac "cert!Suc pc" 1);
+   by (Force_tac 1);
+  by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
+ ------- *)
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("x","ab")] allE 1);
+by (eres_inst_tac [("x","baa")] allE 1);
+by (eres_inst_tac [("x","Suc pc")] allE 1);
+by (Force_tac 1);
+bind_thm ("wtl_append_lemma", result() RS spec RS spec);
+
+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); \
+\      wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow> \
+\      wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0";
+by (cut_inst_tac [("a","a"),("G","G"),("rT","rT"),("xa","s0"),("s1.0","s1"),("cert","cert"),("x","0"),("i","i"),("b","b"),("s2.0","s2"),("s3.0","s3")] wtl_append_lemma 1);
+by (Asm_full_simp_tac 1);
+qed "wtl_append";
+
+
diff -r c587f5ac4a98 -r 6acc80f7f36f src/HOL/MicroJava/BV/LBVSpec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Tue Feb 15 17:51:11 2000 +0100
@@ -0,0 +1,228 @@
+(*  Title:      HOL/MicroJava/BV/BVLightSpec.thy
+    ID:         $Id$
+    Author:     Gerwin Klein
+    Copyright   1999 Technische Universitaet Muenchen
+
+Specification of a lightweight bytecode verifier
+*)
+
+LBVSpec = Convert + BVSpec +
+
+types
+  certificate       = "state_type option list" 
+  class_certificate = "sig \\<Rightarrow> certificate"
+  prog_certificate  = "cname \\<Rightarrow> class_certificate"
+
+consts
+ wtl_LS :: "[load_and_store,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
+primrec
+"wtl_LS (Load idx) s s' 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_LS (Store idx) s s' 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_LS (Bipush i) s s' max_pc pc =
+	(let (ST,LT) = s
+	 in
+	 pc+1 < max_pc \\<and>
+	 ((PrimT Integer) # ST , LT) = s')"
+
+"wtl_LS (Aconst_null) s s' max_pc pc =
+	(let (ST,LT) = s
+	 in
+	 pc+1 < max_pc \\<and>
+	 (NT # ST , LT) = s')"
+
+consts
+ wtl_MO	:: "[manipulate_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wtl_MO (Getfield F C) G s s' 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_MO (Putfield F C) G s s' 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'))"
+
+
+consts 
+ wtl_CO	:: "[create_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wtl_CO (New C) G s s' max_pc pc =
+	(let (ST,LT) = s
+	 in
+	 pc+1 < max_pc \\<and>
+	 is_class G C \\<and>
+	 ((Class C) # ST , LT) = s')"
+
+consts
+ wtl_CH	:: "[check_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wtl_CH (Checkcast C) G s s' 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'))"
+
+consts 
+ wtl_OS	:: "[op_stack,state_type,state_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wtl_OS Pop s s' max_pc pc =
+	(let (ST,LT) = s
+	 in
+	 \\<exists>ts ST'. pc+1 < max_pc \\<and>
+		ST = ts # ST' \\<and> 	 
+		(ST' , LT) = s')"
+
+"wtl_OS Dup s s' 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_OS Dup_x1 s s' 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_OS Dup_x2 s s' 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_OS Swap s s' 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'))"
+
+consts 
+ wtl_BR	:: "[branch,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wtl_BR (Ifcmpeq branch) G 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>  (G \\<turnstile> ts \\<preceq> ts' \\<or> G \\<turnstile> ts' \\<preceq> ts) \\<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_BR (Goto branch) G 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'))"
+   
+   (* (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" 
+primrec
+"wtl_MI (Invoke mn fpTs) G s s' max_pc pc =
+	(let (ST,LT) = s
+	 in
+         pc+1 < max_pc \\<and>
+         (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # 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')))"
+
+consts
+ wtl_MR	:: "[meth_ret,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+primrec
+  "wtl_MR 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'))"
+(*   
+  (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_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+ primrec
+ "wtl_inst (LS ins) G rT s s' cert max_pc pc = wtl_LS ins s s' max_pc pc"
+ "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 (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"
+
+
+constdefs
+wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+"wtl_inst_option i G rT s0 s1 cert max_pc pc \\<equiv>
+     (case cert!pc of 
+          None     \\<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
+        | Some s0' \\<Rightarrow> (G \\<turnstile> s0 <=s s0') \\<and>
+                      wtl_inst i G rT s0' s1 cert max_pc pc)"
+  
+consts
+ wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+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))"
+
+constdefs
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \\<Rightarrow> bool" 
+ "wtl_method G C pTs rT mxl ins cert \\<equiv> 
+	let max_pc = length ins 
+        in 
+	0 < max_pc \\<and>  
+        (\\<exists>s2. wtl_inst_list ins G rT 
+                            ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))
+                            s2 cert max_pc 0)"
+
+ wtl_jvm_prog :: "[jvm_prog,prog_certificate] \\<Rightarrow> bool" 
+ "wtl_jvm_prog G cert \\<equiv> 
+    wf_prog (\\<lambda>G C (sig,rT,maxl,b). 
+               wtl_method G C (snd sig) rT maxl b (cert C sig)) G" 
+
+end