# HG changeset patch
# User kleing
# Date 959789162 -7200
# Node ID d1bd2144ab5db5e496272d4e07cc45084a28625c
# Parent  0cfc347f8d19e75cf0c488be39755bbc1cdc736c
switched to Isar proofs

diff -r 0cfc347f8d19 -r d1bd2144ab5d src/HOL/MicroJava/BV/LBVComplete.ML
--- a/src/HOL/MicroJava/BV/LBVComplete.ML	Wed May 31 14:30:28 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,597 +0,0 @@
-Goal "\\<forall> n. length (option_filter_n l P n) = length l";
-by (induct_tac "l" 1);
-by Auto_tac;
-qed_spec_mp "length_option_filter_n";
-
-Goalw[is_approx_def] "\\<forall> n. is_approx (option_filter_n a P n) a";
-by (induct_tac "a" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "P n" 1);
- by (Clarsimp_tac 1);
- by (case_tac "na" 1);
-  by (Clarsimp_tac 1);
- by (clarsimp_tac (claset(), simpset() addsimps [length_option_filter_n]) 1);
- by (Force_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "na" 1);
- by (Clarsimp_tac 1);
-by (force_tac (claset(), simpset() addsimps [length_option_filter_n]) 1);
-qed_spec_mp "is_approx_option_filter_n";
-
-Goalw[option_filter_def] "is_approx (option_filter l P) l";
-by (simp_tac (simpset() addsimps [is_approx_option_filter_n]) 1);
-qed "is_approx_option_filter";
-
-
-Goal "\\<forall>n n'. n < length l \\<longrightarrow> P (n+n') \\<longrightarrow> option_filter_n l P n' ! n = Some (l!n)";
-by (induct_tac "l" 1);
- by (Simp_tac 1);
-by (Clarify_tac 1);
-by (case_tac "n" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "option_filter_n_Some";
-
-Goalw [option_filter_def]
-"\\<lbrakk>n < length l; P n\\<rbrakk> \\<Longrightarrow> option_filter l P ! n = Some (l!n)";
-br option_filter_n_Some 1;
- ba 1;
-by (Asm_simp_tac 1);
-qed "option_filter_Some";
-
-Goal "\\<lbrakk>length ins < length phi;  pc < length ins\\<rbrakk> \\<Longrightarrow> \
-\      contains_dead ins (option_filter phi (mdot ins)) phi pc";
-by (asm_full_simp_tac (simpset() addsimps [contains_dead_def]) 1);
-br conjI 1;
-br conjI 2;
-by (ALLGOALS (Clarsimp_tac 
-        THEN' (rtac option_filter_Some) 
-        THEN' Asm_simp_tac 
-        THEN' (clarsimp_tac (claset(), simpset() addsimps [mdot_def,maybe_dead_def]))));
-qed "option_filter_contains_dead";
-
-Goal "\\<lbrakk>length ins < length phi;  pc < length ins\\<rbrakk> \\<Longrightarrow> \
-\      contains_targets ins (option_filter phi (mdot ins)) phi pc"; 
-by (asm_full_simp_tac (simpset() addsimps [contains_targets_def]) 1);
-by (Clarsimp_tac 1);
-br conjI 1;
-by (ALLGOALS (Clarsimp_tac 
-        THEN' (rtac option_filter_Some) 
-        THEN' Asm_simp_tac 
-        THEN' (asm_full_simp_tac (simpset() addsimps [mdot_def,is_target_def]))
-        THEN' Force_tac));
-qed "option_filter_contains_targets";
-
-Goalw[fits_def, make_cert_def] "length ins < length phi \\<Longrightarrow> fits ins (make_cert ins phi) phi";
-by (Clarsimp_tac 1);
-br conjI 1;
- br is_approx_option_filter 1;
-by (Clarsimp_tac 1);
-br conjI 1;
- br option_filter_contains_dead 1;
-  ba 1;
- ba 1;
-br option_filter_contains_targets 1;
- ba 1;
-ba 1;
-qed "fits_make_cert";
-
-
-Goal "\\<exists>a'. a = rev a'"; 
-by (induct_tac "a" 1); 
- by (Simp_tac 1);
-by (Clarsimp_tac 1);
-by (res_inst_tac [("x","a'@[a]")] exI 1);
-by (Simp_tac 1);
-qed "rev_surj";
-
-Goal "\\<forall>n. n \\<le> length x \\<longrightarrow> (\\<exists>a b. x = a@b \\<and> length a = n)";
-by (induct_tac "x" 1);
- by (Simp_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "n" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (smp_tac 1 1);
-by (Clarsimp_tac 1);
-by (res_inst_tac [("x","a#aa")] exI 1);
-by (Simp_tac 1);
-qed_spec_mp "append_length_n";
-
-Goal "\\<lbrakk>n < length x\\<rbrakk> \\<Longrightarrow> \\<exists>a b c. x = (rev a) @ b # c \\<and> length a = n";
-by (subgoal_tac "n \\<le> length x" 1);
- by (Asm_full_simp_tac 2);
-by (forward_tac [append_length_n] 1);
-by (Clarsimp_tac 1);
-by (cut_inst_tac [("xs","b")] neq_Nil_conv 1);
-by (Clarsimp_tac 1);
-by (cut_inst_tac [("a","a")] rev_surj 1);
-by (Clarsimp_tac 1);
-by (res_inst_tac [("x","a'")] exI 1);
-by (Clarsimp_tac 1);
-qed "rev_append_cons";
-
-
-Goal "G \\<turnstile> b \\<preceq> NT \\<Longrightarrow> b = NT";
-by (case_tac "b" 1);
- by (case_tac "ref_ty" 2);
-by Auto_tac;
-qed "widen_NT";
-
-Goal "G \\<turnstile> b \\<preceq> Class C \\<Longrightarrow> \\<exists>r. b = RefT r";
-by (case_tac "b" 1);
-by Auto_tac;
-qed "widen_Class";
-
-
-Goal "\\<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))";
-by (induct_tac "a" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "b" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "all_widen_is_sup_loc";
-
-Goal "\\<lbrakk>fits ins cert phi; i = ins!pc; i = MI meth_inv; pc < length ins; \
- \     wf_prog wf_mb G; \
-\      G \\<turnstile> (x, y) <=s s1; wtl_inst i 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)))"; 
-by (case_tac "meth_inv" 1); 
-by (Clarsimp_tac 1);
-by (cut_inst_tac [("x","x"),("n","length apTs")] rev_append_cons 1);
- by (asm_full_simp_tac (simpset() addsimps [sup_state_length_fst]) 1);
-by (Clarify_tac 1);
-by (subgoal_tac "length (rev aa) = length (rev apTs)" 1);
- by (Asm_full_simp_tac 2);
-by (dres_inst_tac [("G","G"),("x","ba#c"),("i","y"),("j","ya"),("y","X#ST'")] sup_state_append_fst 1);
-back();
-back();
-by (clarsimp_tac (claset(), simpset() addsimps [sup_state_rev_fst,sup_state_Cons1]) 1);
-by (case_tac "X = NT" 1);
- by (Clarsimp_tac 1);
- by (res_inst_tac [("x","a")] exI 1);
- by (res_inst_tac [("x","b")] exI 1);
- by (Asm_full_simp_tac 1);
- by (res_inst_tac [("x","aa")] exI 1);
- by (asm_full_simp_tac (simpset() addsimps [widen_NT]) 1);
-by (Asm_full_simp_tac 1);
-by (strip_tac1 1);
-by (forward_tac [widen_Class] 1);
-by (Clarsimp_tac 1);
-by (case_tac "r" 1);
- by (Clarsimp_tac 1);
- by (res_inst_tac [("x","a")] exI 1);
- by (res_inst_tac [("x","b")] exI 1);
- by (Clarsimp_tac 1);
- by (res_inst_tac [("x","aa")] exI 1);
- by (clarsimp_tac (claset(), simpset() addsimps [fits_def]) 1);
-by (Clarsimp_tac 1);
-bd subcls_widen_methd 1;
-  ba 1;
- ba 1;
-by (Clarify_tac 1);
-by (res_inst_tac [("x","rT'#c")] exI 1);
-by (res_inst_tac [("x","y")] exI 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "\\<exists>a b. cert ! Suc pc = Some (a, b) \\<and> G \\<turnstile> (rT' # c, y) <=s (a, b)" 1);
- by (Clarsimp_tac 1);
- by (res_inst_tac [("x","aa")] exI 1);
- by (Asm_full_simp_tac 1);
- by (clarsimp_tac (claset(), simpset() addsimps [sup_state_def, all_widen_is_sup_loc]) 1);
- br sup_loc_trans 1;
-  ba 1;
- ba 1;
-by (Clarsimp_tac 1);
-by (subgoal_tac "G \\<turnstile> (rT' # c, y) <=s (rT # ST', ya)" 1);
- br sup_state_trans 1;
-  ba 1;
- ba 1;
-by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1);
-qed "method_inv_pseudo_mono";
-
-
-
-Goalw[sup_loc_def] "\\<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)))";
-by (induct_tac "b" 1);
- by (Simp_tac 1);
-by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
-by (case_tac "n" 1);
- by (asm_full_simp_tac (simpset() addsimps [sup_ty_opt_some]) 1);
-by (smp_tac 1 1);
-by (Asm_full_simp_tac 1);
-qed_spec_mp "sup_loc_some";
-
-
-Goalw[sup_state_def]
-"\\<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)";
-by (Clarsimp_tac 1);
-by (datac sup_loc_some 2 1);
-by (Clarsimp_tac 1);
-qed "mono_load";
-
-
-Goalw[sup_state_def] 
-"\\<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])";
-by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_Cons2]) 1);
-by (forward_tac [map_hd_tl] 1);
-by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_update]) 1);
-qed "mono_store"; 
-
-Goal "(G \\<turnstile> xb \\<preceq> PrimT p) = (xb = PrimT p)";
-by Safe_tac;
-by (case_tac "xb" 1);
-by Auto_tac;
-bd widen_RefT 1;
-by Auto_tac;
-qed "PrimT_PrimT";
-
-Goal "\\<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))"; 
-by (cut_inst_tac [("z","s2")] surj_pair 1); 
-by (Clarify_tac 1); 
-by (case_tac "ins!pc" 1); 
-       by (case_tac "load_and_store" 1); 
-          by (Clarsimp_tac 1); 
-          by (datac mono_load 2 1); 
-          by (clarsimp_tac (claset(), simpset() addsimps [sup_state_length_snd]) 1);
-         by (clarsimp_tac (claset(), simpset() addsimps [sup_state_length_snd]) 1);
-         by (datac mono_store 1 1);
-         by (Clarsimp_tac 1);
-        by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1); 
-       by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1); 
-      by (case_tac "create_object" 1); 
-      by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons1]) 1); 
-     by (case_tac "manipulate_object" 1); 
-      by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-      be widen_trans 1; 
-      ba 1; 
-     by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-     br conjI 1; 
-      be widen_trans 1; 
-      ba 1; 
-     be widen_trans 1; 
-     ba 1; 
-    by (case_tac "check_object" 1); 
-    by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-    be widen_RefT2 1; 
-    br method_inv_pseudo_mono 1;
-          ba 1;
-         by (Asm_full_simp_tac 1);
-        ba 1;
-       ba 1;
-      ba 1;
-     ba 1;
-    ba 1;   
-   by (case_tac "meth_ret" 1);
-   by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-   br conjI 1;
-    be widen_trans 1;
-    ba 1;
-   by (cut_inst_tac [("z","s1'")] surj_pair 1);
-   by (strip_tac1 1);
-   by (Clarsimp_tac 1);
-  by (case_tac "op_stack" 1);
-     by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-    by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-   by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-  by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
- by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-by (case_tac "branch" 1);
- by (Clarsimp_tac 1);
- bd sup_state_trans 1;
-  ba 1;
- by (Clarsimp_tac 1);
- by (cut_inst_tac [("z","s1'")] surj_pair 1);
- by (Clarify_tac 1);
- by (Clarsimp_tac 1);
-by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1); 
-br conjI 1;
- br sup_state_trans 2;
-  ba 2;
- ba 2;
-by (Clarsimp_tac 1);
-by (case_tac "xa" 1);
- by (clarsimp_tac (claset(), simpset() addsimps [PrimT_PrimT]) 1);
-by (Clarsimp_tac 1);
-by (case_tac "xb" 1);
-by Auto_tac;
-bd widen_RefT 1;
-by Auto_tac;
-qed "wtl_inst_pseudo_mono";
-
-
-Goal "\\<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')";
-by (case_tac "i" 1);
-by (case_tac "branch" 8);
-by (case_tac "op_stack" 7);
-by (case_tac "meth_ret" 6);
-by (case_tac "meth_inv" 5);
-by (case_tac "check_object" 4);
-by (case_tac "manipulate_object" 3);
-by (case_tac "create_object" 2);
-by (case_tac "load_and_store" 1);
-by (TRYALL Asm_full_simp_tac);
- by (pair_tac "s1'" 1);
- by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
- br widen_trans 1;
-  ba 1;
- ba 1;
-by (pair_tac "s1'" 1);
-by (clarsimp_tac (claset(), simpset() addsimps [sup_state_Cons2]) 1);
-br sup_state_trans 1;
- ba 1;
-ba 1;
-qed "wtl_inst_last_mono";
-
-Goalw [wtl_inst_option_def] 
-"\\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; Suc pc = mpc; 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')";
-by (case_tac "cert!pc" 1);
- by (Clarsimp_tac 1);
- bd wtl_inst_last_mono 1;
-  ba 1;
- by (Asm_full_simp_tac 1);
-by (Clarsimp_tac 1);
-bd sup_state_trans 1;
- ba 1;
-by (Asm_full_simp_tac 1);
-by (dres_inst_tac [("s2.0","(a,b)")] wtl_inst_last_mono 1);
- by (Simp_tac 1);
-by (Asm_full_simp_tac 1);
-qed "wtl_option_last_mono";
-
-Goalw [wt_instr_def] 
-     "\\<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";  
-by (cut_inst_tac [("z","phi!pc")] surj_pair 1);
-by (strip_tac1 1);
-by (case_tac "ins!pc" 1);
-by (case_tac "op_stack" 7);
-by (case_tac "check_object" 4);
-by (case_tac "manipulate_object" 3);
-by (case_tac "create_object" 2);
-by (case_tac "load_and_store" 1);
-               by (TRYALL (Asm_full_simp_tac THEN_MAYBE' Force_tac));
-  by (case_tac "meth_inv" 1);
-  by (cut_inst_tac [("z","phi!(Suc pc)")] surj_pair 1);
-  by (strip_tac1 1);
-  by (Clarsimp_tac 1);
-  by (case_tac "X = NT" 1);
-   by (clarsimp_tac (claset(),simpset() addsimps [fits_def, contains_dead_def]) 1);
-   by (smp_tac 1 1);
-   by (Clarsimp_tac 1);
-   by (Force_tac 1);
-  by (Asm_full_simp_tac 1);
-  by (strip_tac1 1);
-  by (res_inst_tac [("x","rT#ST'")] exI 1);
-  by (res_inst_tac [("x","y")] exI 1);
-  by (Asm_full_simp_tac 1);
-  by (res_inst_tac [("x","apTs")] exI 1);
-  by (clarsimp_tac (claset(),simpset() addsimps [fits_def, contains_dead_def]) 1);
- by (case_tac "meth_ret" 1);
- by (asm_full_simp_tac (simpset() addsimps [fits_def, contains_dead_def]) 1);
- by (cut_inst_tac [("z","phi!Suc pc")] surj_pair 1);
- by (strip_tac1 1);
- by (Clarsimp_tac 1);
-by (case_tac "branch" 1);
- by (asm_full_simp_tac (simpset() addsimps [fits_def, contains_dead_def, contains_targets_def]) 1);
- by (cut_inst_tac [("z","phi!Suc pc")] surj_pair 1);
- by (Force_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [fits_def, contains_targets_def]) 1);
-by (Force_tac 1);
-qed "wt_instr_imp_wtl_inst";
-
-Goalw [wtl_inst_option_def] 
-     "\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc; \
-\      max_pc = length ins\\<rbrakk> \\<Longrightarrow> \ 
-\     \\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
-by (case_tac "cert!pc" 1);
- by (Clarsimp_tac 1);
- bd wt_instr_imp_wtl_inst 1;
-    ba 1;
-   ba 1;
-  br refl 1;
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (forward_tac [wt_instr_imp_wtl_inst] 1);
-   ba 1;
-  ba 1;
- by (Clarsimp_tac 1);
-by (clarsimp_tac (claset(), simpset() addsimps [fits_def, is_approx_def]) 1);
-by (eres_inst_tac [("x","pc")] allE 1);
-by (Clarsimp_tac 1);
-by Auto_tac;
-qed "wt_inst_imp_wtl_option";
-
-Goal "\\<lbrakk>wtl_inst_list ins G rT s0 s' cert max_pc pc; \ 
-\     ins \\<noteq> []; G \\<turnstile> s <=s s0; \ 
-\     s \\<noteq> s0 \\<longrightarrow> cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> \ 
-\     wtl_inst_list ins G rT s s' cert max_pc pc";  
-by (case_tac "ins" 1); 
- by (Clarify_tac 1);
-by (Clarify_tac 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (case_tac "list = []" 1);
- by (Asm_full_simp_tac 1);
- by (case_tac "s = s0" 1);
-  by (Force_tac 1);
- by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
-by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
-qed "wtl_inst_list_s";
-
-
-Goal "\\<lbrakk>wtl_inst_list ins G rT s0 s' cert max_pc pc; \ 
-\     ins \\<noteq> []; G \\<turnstile> s <=s s0; cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> \ 
-\     wtl_inst_list ins G rT s s' cert max_pc pc"; 
-by (case_tac "ins" 1); 
- by (Clarify_tac 1);
-by (force_tac (claset(), simpset() addsimps [wtl_inst_option_def]) 1);
-qed "wtl_inst_list_cert";
-
-
-Goalw [wtl_inst_option_def]
-"\\<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))";
-by (case_tac "cert!pc" 1);
- by (Asm_full_simp_tac 1);
- by (datac wtl_inst_pseudo_mono 4 1);
-  by (Clarsimp_tac 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-br conjI 1;
- br sup_state_trans 1;
-  ba 1;
- ba 1;
-by (thin_tac "G \\<turnstile> s1 <=s (a, b)" 1);
-by (thin_tac "G \\<turnstile> s2 <=s s1" 1);
-by (subgoal_tac "G \\<turnstile> (a,b) <=s (a,b)" 1);
- by (datac wtl_inst_pseudo_mono 4 1);
-  by (Asm_full_simp_tac 1);
- by (Asm_full_simp_tac 1);
-by (Simp_tac 1);
-qed "wtl_option_pseudo_mono";
-
-Goal "((l @ a # list) ! length l) = a";
-by (induct_tac "l" 1);
-by Auto_tac;
-qed "append_cons_length_nth";
-
-Goal "\\<forall> pc. (\\<forall>pc'. pc' < length ins \\<longrightarrow> wt_instr (ins ! pc') G rT phi (pc+length ins) (pc+pc')) \\<longrightarrow>   \
-\           wf_prog wf_mb G \\<longrightarrow> \
-\           fits all_ins cert phi \\<longrightarrow> (\\<exists> l. pc = length l \\<and> l@ins=all_ins) \\<longrightarrow> pc < length all_ins \\<longrightarrow>\
-\           (\\<forall> s. (G \\<turnstile> s <=s (phi!pc)) \\<longrightarrow> \
-\           (\\<exists>s'. wtl_inst_list ins G rT s s' cert (pc+length ins) pc))";
-by (induct_tac "ins" 1);
- by (Simp_tac 1);
-by (Clarify_tac 1);
-by (eres_inst_tac [("x","Suc (length l)")] allE 1); 
-be impE 1; 
- by (Clarsimp_tac 1);
- by (eres_inst_tac [("x","Suc pc'")] allE 1);
- by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-be impE 1;
- by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("x","0")] allE 1);
-by (Asm_full_simp_tac 1);
-by (forw_inst_tac [("G","G"),("rT","rT"),("pc","length l"),
-                   ("max_pc","Suc (length l + length list)")] wt_inst_imp_wtl_option 1);
-   by (Simp_tac 1);
-  by (asm_full_simp_tac (simpset() addsimps [nth_append]) 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [nth_append]) 1);
-by (Clarify_tac 1);
-by (case_tac "list = []" 1);
- by (Clarsimp_tac 1);
- bd wtl_option_last_mono 1;
-   br refl 1;
-  ba 1;
- by (Clarsimp_tac 1);
- by (dres_inst_tac [("a","(ac,bb)")] sup_state_trans 1);
-  ba 1;
- by (Force_tac 1);
-by (Clarsimp_tac 1);
-bd wtl_option_pseudo_mono 1;
-     ba 1;
-    by (Simp_tac 1);
-   ba 1;
-  ba 1;
- by (simp_tac (simpset() addsimps [append_cons_length_nth]) 1);
-by (clarsimp_tac (claset(), simpset() addsimps [append_cons_length_nth]) 1);
-by (case_tac "cert ! Suc (length l)" 1);
- by (Clarsimp_tac 1);
- by (dres_inst_tac [("a","(ac,bb)")] sup_state_trans 1);
-  ba 1;
- by (Force_tac 1);
-by (Clarsimp_tac 1);
-by (subgoal_tac "G \\<turnstile> (ac, bb) <=s phi ! Suc (length l)" 1);
- by (thin_tac "G \\<turnstile> (ab, ba) <=s phi ! Suc (length l)" 1);
- by (smp_tac 2 1);
- by (Force_tac 1);
-be disjE 1;
- br sup_state_trans 1;
-  ba 1;
- ba 1;
-by (clarsimp_tac (claset(), simpset() addsimps [fits_def, is_approx_def]) 1);
-by (eres_inst_tac [("x","Suc (length l)")] allE 1);
-be impE 1;
- by (case_tac "length list" 1);
-  by (Clarsimp_tac 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "wt_imp_wtl_inst_list"; 
-
-
-
-Goalw[wt_method_def, wtl_method_def]
- "\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert";
-by (Clarsimp_tac 1);
-by (cut_inst_tac [("pc","0")] wt_imp_wtl_inst_list 1);    
-      by (Force_tac 1);
-     ba 1;
-    ba 1;
-   by (Simp_tac 1);
-  by (Simp_tac 1);
- by (clarsimp_tac (claset(), simpset() addsimps [wt_start_def]) 1);
- ba 1;
-by (Asm_full_simp_tac 1);
-qed "fits_imp_wtl_method_complete";
-
-Goal "\\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)";
-by (subgoal_tac "fits ins (make_cert ins phi) phi" 1);
- br fits_make_cert 2;
- by (asm_full_simp_tac (simpset() addsimps [wt_method_def]) 2);
-br fits_imp_wtl_method_complete 1;
-  ba 1;
- ba 1;
-ba 1;
-qed "wtl_method_complete";
-
-Goalw[wt_jvm_prog_def, wfprg_def] "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wfprg G";
-by Auto_tac;
-qed "wt_imp_wfprg";
-
-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";
-
-Goal "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)";
-by (forward_tac [wt_imp_wfprg] 1);
-by (asm_full_simp_tac (simpset() addsimps [wt_jvm_prog_def, 
-    wtl_jvm_prog_def, wf_prog_def, wf_cdecl_def, wf_mdecl_def]) 1);
-by Auto_tac;
-bd bspec 1;
- ba 1;
-by (Clarsimp_tac 1);
-bd bspec 1;
-back();
- ba 1;
-by (clarsimp_tac (claset(), simpset() addsimps [make_Cert_def, wfprg_def]) 1);
-bd wtl_method_complete 1;
- ba 1;
-by (asm_full_simp_tac (simpset() addsimps [unique_epsilon]) 1);
-qed "wtl_complete";
-
-
-
-
- 
diff -r 0cfc347f8d19 -r d1bd2144ab5d src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed May 31 14:30:28 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Wed May 31 18:06:02 2000 +0200
@@ -6,19 +6,16 @@
 Proof of completeness for the lightweight bytecode verifier
 *)
 
-LBVComplete= LBVSpec +
+theory LBVComplete = LBVSpec:;
+
+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"
   "is_approx a b \\<equiv> length a = length b \\<and> (\\<forall> n. n < length a \\<longrightarrow>
                    (a!n = None \\<or> a!n = Some (b!n)))"
   
-  fits :: "[instr list, certificate, method_type] \\<Rightarrow> bool"
-  "fits ins cert phi \\<equiv> is_approx cert phi \\<and> length ins < length phi \\<and>
-                            (\\<forall> pc. pc < length ins \\<longrightarrow>
-                                   contains_dead ins cert phi pc \\<and> 
-                                   contains_targets ins cert phi pc)"
-
   contains_dead :: "[instr list, certificate, method_type, p_count] \\<Rightarrow> bool"
   "contains_dead ins cert phi pc \\<equiv>
     (((\\<exists> branch. ins!pc = BR (Goto branch)) \\<or> ins!pc = MR Return) \\<or>
@@ -30,6 +27,12 @@
     \\<forall> branch. (ins!pc = BR (Goto branch) \\<or> ins!pc = BR (Ifcmpeq branch)) \\<longrightarrow>
         (let pc' = nat (int pc+branch) in 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>
+                            (\\<forall> pc. pc < length ins \\<longrightarrow>
+                                   contains_dead ins cert phi pc \\<and> 
+                                   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> 
@@ -44,15 +47,15 @@
 
 
   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" 
@@ -65,10 +68,1108 @@
   "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)";
   
 constdefs
   wfprg :: "jvm_prog \\<Rightarrow> bool"
-  "wfprg G \\<equiv> \\<exists>wf_mb. wf_prog wf_mb G"
+  "wfprg G \\<equiv> \\<exists>wf_mb. wf_prog wf_mb G";
+
+
+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);
+
+  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);
+    
+    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);
+
+        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 = BR (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 = BR (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 rev_surj: "\\<exists>a'. a = rev a'";
+proof (induct "a"); 
+  show "\\<exists>a'. [] = rev a'"; by simp;
+
+  fix l ls; assume "\\<exists>a''. ls = rev a''";  
+  thus "\\<exists>a'. l # ls = rev a'"; 
+  proof (elim exE);
+    fix a''; assume "ls = rev a''";
+    hence "l#ls = rev (a''@[l])"; by simp;
+    thus ?thesis; by blast;
+  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 bc: "\\<exists>b c. d = b#c"; by (simp add: neq_Nil_conv);
+    
+    have "\\<exists>a. r = rev a"; by (rule rev_surj);    
+    with bc;
+    show ?thesis;
+    proof elim;
+      fix a b c; 
+      assume "r = rev a" "d = b#c";
+      with x;
+      have "x = (rev a) @ b # c \\<and> length a = 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 = MI meth_inv; 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 (cases meth_inv); 
+  case Invoke; 
+  assume fits: "fits ins cert phi" and
+         i: "i = ins ! pc" "i = MI meth_inv" 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";
+ 
+  with Invoke; 
+  show ?thesis; (* (is "\\<exists>s2'. ?wtl s2' \\<and> (?lt s2' s1' \\<or> ?cert s2')" is "\\<exists>s2'. ?P s2'"); *)
+  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;
+      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;
+
+  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";
+
+    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 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;
+
+
+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); print_cases;
+    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 wtl_inst_pseudo_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";
+
+  have 3: "\\<exists> a b. s2 = (a,b)"; by simp;
+
+  show ?thesis; 
+  proof (cases "ins ! pc");
+
+    case LS;
+    show ?thesis;
+    proof (cases "load_and_store");
+      case Load;
+      with LS 1 3;
+      show ?thesis; by (elim, clarsimp_tac) (rule mono_load [elimify], auto simp add: sup_state_length_snd);
+    next;
+      case Store;
+      with LS 1 3; 
+      show ?thesis; by (elim, clarsimp_tac) (rule mono_store [elimify], auto simp add: sup_state_length_snd);
+    next;
+      case Bipush;
+      with LS 1 3;
+      show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons1);
+    next;
+      case Aconst_null;
+      with LS 1 3;
+      show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons1);
+    qed;
+
+  next;
+    case CO;
+    show ?thesis;
+    proof (cases create_object);
+      case New;
+      with CO 1 3;
+      show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons1);
+    qed;
+
+  next;
+    case MO;
+    show ?thesis;
+    proof (cases manipulate_object);
+      case Getfield;
+      with MO 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 MO 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);
+        
+        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;
+      qed;
+    qed;
+
+  next;
+    case CH;
+    show ?thesis;
+    proof (cases check_object);
+      case Checkcast;
+      with CH 1 3;
+      show ?thesis; by (elim, clarsimp_tac simp add: sup_state_Cons2) (rule widen_RefT2);
+    qed;
+
+  next;
+    case MI;
+    with 1 2 3;
+    show ?thesis; by elim (rule method_inv_pseudo_mono [elimify], simp+); 
 
-end
+  next;
+    case MR;
+    show ?thesis;
+    proof (cases meth_ret);
+      case Return;
+      with MR 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;
+    qed;
+
+  next;
+    case OS;
+    with 1 3;
+    show ?thesis; 
+      by - (cases op_stack, (elim, clarsimp_tac simp add: sup_state_Cons2)+);
+
+  next;
+    case BR;
+    show ?thesis;
+    proof (cases branch);
+      case Goto;
+      with BR 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;
+    next;
+      case Ifcmpeq;
+      with BR 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;
+
+          with 1;
+          show ?thesis; by blast;
+        qed;
+      qed;
+    qed;
+  qed;
+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";
+  
+  show ?thesis;
+  proof (cases i);
+    case LS; with *;
+    show ?thesis; by - (cases load_and_store, simp+);
+  next;
+    case CO; with *;
+    show ?thesis; by - (cases create_object, simp);
+  next;
+    case MO; with *;
+    show ?thesis; by - (cases manipulate_object, simp+);
+  next;
+    case CH; with *;
+    show ?thesis; by - (cases check_object, simp);
+  next;
+    case MI; with *;
+    show ?thesis; by - (cases meth_inv, simp);
+  next;
+    case OS; with *;
+    show ?thesis; by - (cases op_stack, simp+); 
+  next;
+    case MR; 
+    show ?thesis;
+    proof (cases meth_ret);
+      case Return; with MR *;
+      show ?thesis; 
+        by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2)
+           (rule widen_trans, blast+);
+    qed;
+  next;
+    case BR;
+    show ?thesis;
+    proof (cases branch);
+      case Ifcmpeq; with BR *;
+      show ?thesis; by simp;
+    next;
+      case Goto; with BR *;
+      show ?thesis;  
+      by (clarsimp_tac simp del: split_paired_Ex simp add: sup_state_Cons2)
+         (rule sup_state_trans, blast+);
+    qed;
+  qed;
+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";
+
+  have xy: "\\<exists> x y. phi!pc = (x,y)"; by simp;
+
+  show ?thesis;
+  proof (cases "ins!pc");
+    case LS; with * xy;
+    show ?thesis; 
+      by - (cases load_and_store, (elim, force simp add: wt_instr_def)+); 
+  next;
+    case CO; with * xy;
+    show ?thesis;
+      by - (cases create_object, (elim, force simp add: wt_instr_def)+); 
+  next;
+    case MO; with * xy;
+    show ?thesis;
+      by - (cases manipulate_object, (elim, force simp add: wt_instr_def)+);
+  next; 
+    case CH; with * xy;
+    show ?thesis;
+      by - (cases check_object, (elim, force simp add: wt_instr_def)+);
+  next;
+    case OS; with * xy;
+    show ?thesis;
+      by - (cases op_stack, (elim, force simp add: wt_instr_def)+);
+  next;
+    case MR; with * xy;
+    show ?thesis;
+    by - (cases meth_ret, elim, 
+      clarsimp_tac simp add: wt_instr_def fits_def contains_dead_def simp del: split_paired_Ex);
+  next;
+    case BR; with * xy;
+    show ?thesis; 
+      by - (cases branch,
+           (clarsimp_tac simp add: wt_instr_def fits_def contains_dead_def contains_targets_def 
+                         simp del: split_paired_Ex)+);
+  next;
+    case MI;
+    show ?thesis;
+    proof (cases meth_inv);
+      case Invoke;
+      with MI * xy;
+      show ?thesis; 
+      proof (elim, clarsimp_tac simp add: wt_instr_def 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 MI Invoke pc *;
+        have cert: "cert ! Suc pc = Some (phi ! Suc pc)"; by (clarsimp_tac simp add: fits_def contains_dead_def); 
+
+
+        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 **;
+
+          have "?CL"; by simp;
+
+          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;
+  qed;
+qed;
+
+  
+lemma wt_instr_imp_wtl_option:
+"\\<lbrakk>fits ins cert phi; pc < length ins; wt_instr (ins!pc) G rT phi max_pc pc;  max_pc = length ins\\<rbrakk> \\<Longrightarrow> 
+ \\<exists> s. wtl_inst_option (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
+proof -;
+  assume fits : "fits ins cert phi" "pc < length ins" 
+         and "wt_instr (ins!pc) G rT phi max_pc pc" 
+             "max_pc = length ins";
+
+  hence * : "\\<exists> s. wtl_inst (ins!pc) G rT (phi!pc) s cert max_pc pc \\<and> G \\<turnstile> s <=s phi ! Suc pc";
+    by - (rule wt_instr_imp_wtl_inst, simp+);
+  
+  show ?thesis;
+  proof (cases "cert ! pc");
+    case None;
+    with *;
+    show ?thesis; by (simp add: wtl_inst_option_def);
+
+  next;
+    case Some;
+
+    from fits; 
+    have "pc < length phi"; by (clarsimp_tac 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;
+
+(* not needed 
+lemma wtl_inst_list_s:
+"\\<lbrakk>wtl_inst_list ins G rT s0 s' cert max_pc pc; ins \\<noteq> []; G \\<turnstile> s <=s s0; s \\<noteq> s0 \\<longrightarrow> cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> 
+  wtl_inst_list ins G rT s s' cert max_pc pc";  
+proof -;
+  assume * : "wtl_inst_list ins G rT s0 s' cert max_pc pc" 
+             "ins \\<noteq> []" "G \\<turnstile> s <=s s0" 
+             "s \\<noteq> s0 \\<longrightarrow> cert ! pc = Some s0";
+
+  show ?thesis;
+  proof (cases ins);
+    case Nil;
+    with *;
+    show ?thesis; by simp;
+  next;
+    case Cons;
+
+    show ?thesis; 
+    proof (cases "list = []");
+      case True;
+      with Cons *;
+      show ?thesis; by - (cases "s = s0", (simp add: wtl_inst_option_def)+);
+    next;
+      case False;
+      with Cons *;
+      show ?thesis; by (force simp add: wtl_inst_option_def);
+    qed; 
+  qed;
+qed;
+
+
+lemma wtl_inst_list_cert:
+"\\<lbrakk>wtl_inst_list ins G rT s0 s' cert max_pc pc; ins \\<noteq> []; G \\<turnstile> s <=s s0; cert ! pc = Some s0\\<rbrakk> \\<Longrightarrow> 
+  wtl_inst_list ins G rT s s' cert max_pc pc";
+by (cases ins) (force simp add: wtl_inst_option_def)+;
+*)
+
+lemma wtl_option_pseudo_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 -;
+  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";
+
+  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;
+    with wtl fits;
+
+    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);
+
+    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 Some G;
+    show ?thesis; by (simp add: wtl_inst_option_def);
+  qed;
+qed;
+
+lemma append_cons_length_nth: "((l @ a # list) ! length l) = a"; 
+  by (induct l, auto);
+
+
+(* main induction over instruction list *)
+theorem wt_imp_wtl_inst_list:
+"\\<forall> pc. (\\<forall>pc'. pc' < length ins \\<longrightarrow> wt_instr (ins ! pc') G rT phi (pc+length ins) (pc+pc')) \\<longrightarrow>   
+       wf_prog wf_mb G \\<longrightarrow> 
+       fits all_ins cert phi \\<longrightarrow> (\\<exists> l. pc = length l \\<and> all_ins=l@ins) \\<longrightarrow> pc < length all_ins \\<longrightarrow>
+       (\\<forall> s. (G \\<turnstile> s <=s (phi!pc)) \\<longrightarrow> 
+       (\\<exists>s'. wtl_inst_list ins G rT s s' cert (pc+length ins) pc))" 
+(is "\\<forall>pc. ?C pc ins" is "?P ins");
+proof (induct "?P" "ins");
+  case Nil;
+  show "?P []"; by simp;
+next;
+  case Cons;
+
+  show "?P (a#list)";
+  proof (intro allI impI, elim exE conjE);
+    fix pc s l;
+    assume 1: "wf_prog wf_mb G" "fits all_ins cert phi";
+    assume 2: "pc < length all_ins" "G \\<turnstile> s <=s phi ! pc"
+              "all_ins = l @ a # list" "pc = length l";
+
+    from Cons;
+    have IH: "?C (Suc pc) list"; by blast;
+
+    assume 3: "\\<forall>pc'. pc' < length (a # list) \\<longrightarrow>
+               wt_instr ((a # list) ! pc') G rT phi (pc + length (a # list)) (pc + pc')";
+    hence 4: "\\<forall>pc'. pc' < length list \\<longrightarrow>
+              wt_instr (list ! pc') G rT phi (Suc pc + length list) (Suc pc + pc')"; by auto;    
+
+    from 2; 
+    have 5: "a = all_ins ! pc"; by (simp add: append_cons_length_nth);
+
+
+    show "\\<exists>s'. wtl_inst_list (a # list) G rT s s' cert (pc + length (a # list)) pc"; 
+    proof (cases list);
+      case Nil;
+
+      with 1 2 3 5; 
+      have "\\<exists>s'. wtl_inst_option a G rT (phi ! pc) s' cert (Suc (length l)) pc";
+        by - (rule wt_instr_imp_wtl_option [elimify], force+);
+
+      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+); 
+
+      with Nil 2;
+      show ?thesis; by auto;
+    next;
+      fix i' ins'; 
+      assume Cons2: "list = i' # ins'";
+
+      with IH 1 2 3;
+      have * : "\\<forall> s. (G \\<turnstile> s <=s (phi!(Suc pc))) \\<longrightarrow> 
+                     (\\<exists>s'. wtl_inst_list list G rT s s' cert ((Suc pc)+length list) (Suc pc))";
+        by (elim impE) force+;
+
+      from 3;
+      have "wt_instr a G rT phi (pc + length (a # list)) pc"; by auto;
+      
+      with 1 2 5;
+      have "\\<exists>s1'. wtl_inst_option a G rT (phi!pc) s1' cert (Suc (pc + length list)) pc \\<and> G \\<turnstile> s1' <=s phi ! Suc pc";
+        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))";
+      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+);
+
+        with a;
+        show ?thesis;
+        proof (elim, intro);
+          fix s1;
+          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;
+
+      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)";
+        
+        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 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;
+
+
+lemma fits_imp_wtl_method_complete:
+"\\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins cert";
+by (simp add: wt_method_def wtl_method_def del: split_paired_Ex)
+   (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex); 
+
+
+lemma wtl_method_complete:
+"\\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\\<rbrakk> \\<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)";
+proof -;
+  assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G";
+  
+  hence "fits ins (make_cert ins phi) phi";
+    by - (rule fits_make_cert, simp add: wt_method_def);
+
+  with *;
+  show ?thesis; by - (rule fits_imp_wtl_method_complete);
+qed;
+
+(*
+Goalw[wt_jvm_prog_def, wfprg_def] "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wfprg G";
+by Auto_tac;
+qed "wt_imp_wfprg";
+*)
+
+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'";
+  by (induct "l") auto;
+
+lemma unique_epsilon:
+"(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 simp add: unique_set);
+
+
+theorem wtl_complete: "\\<lbrakk>wt_jvm_prog G Phi\\<rbrakk> \\<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)";
+proof (simp only: wt_jvm_prog_def);
+
+  assume wfprog: "wf_prog (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G";
+
+  thus ?thesis; 
+  proof (simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def wf_mdecl_def, auto);
+    fix a aa ab b ac ba ad ae bb; 
+    assume 1 : "\\<forall>(C,sc,fs,ms)\\<in>set G.
+             Ball (set fs) (wf_fdecl G) \\<and>
+             unique fs \\<and>
+             (\\<forall>(sig,rT,mb)\\<in>set ms. wf_mhead G sig rT \\<and> (\\<lambda>(maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) mb) \\<and>
+             unique ms \\<and>
+             (case sc of None \\<Rightarrow> C = Object
+              | Some D \\<Rightarrow>
+                  is_class G D \\<and>
+                  (D, C) \\<notin> (subcls1 G)^* \\<and>
+                  (\\<forall>(sig,rT,b)\\<in>set ms. \\<forall>D' rT' b'. method (G, D) sig = Some (D', rT', b') \\<longrightarrow> G\\<turnstile>rT\\<preceq>rT'))"
+             "(a, aa, ab, b) \\<in> set G";
+  
+    assume uG : "unique G"; 
+    assume b  : "((ac, ba), ad, ae, bb) \\<in> set b";
+
+    from 1;
+    show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))";
+    proof (rule bspec [elimify], clarsimp_tac);
+      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);
+        assume "wt_method G a ba ad ae bb (Phi a (ac, ba))";         
+        with wfprog uG ub b 1;
+        show ?thesis;
+          by - (rule wtl_method_complete [elimify], assumption+, simp add: make_Cert_def unique_epsilon);
+      qed; 
+    qed;
+  qed;
+qed;
+
+end;
diff -r 0cfc347f8d19 -r d1bd2144ab5d src/HOL/MicroJava/BV/LBVCorrect.ML
--- a/src/HOL/MicroJava/BV/LBVCorrect.ML	Wed May 31 14:30:28 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,292 +0,0 @@
-(*  Title:      HOL/MicroJava/BV/BVLcorrect.ML
-    ID:         $Id$
-    Author:     Gerwin Klein
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-
-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 (case_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 (case_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 (case_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 \\<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_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";
-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, 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);
-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 (case_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 (case_tac "cert!(Suc (length a))" 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);
- 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, 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);
-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";
-
-
-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 (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);
- 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 (case_tac "cert!(length i1)" 1);
- by (forward_tac [fits_lemma2] 1);
-     by (TRYALL atac);
- by (case_tac "i" 1);
-        by (case_tac "check_object" 4);
-        by (case_tac "manipulate_object" 3);
-         by (case_tac "create_object" 2);
-         by (case_tac "load_and_store" 1);
-            by (GOALS (force_tac (claset(), 
-                simpset() addsimps [wt_instr_def,wtl_inst_option_def])) 1 8);
-    by (case_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 (pair_tac "s1" 1);
-    by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);    
-    by (Force_tac 1);
-   by (case_tac "meth_ret" 1);
-   by (asm_full_simp_tac (simpset() addsimps [wt_instr_def,wtl_inst_option_def]) 1);
-  by (case_tac "branch" 2);
-   by (case_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 (case_tac "i" 1);
-       by (case_tac "check_object" 4);
-       by (case_tac "manipulate_object" 3);
-        by (case_tac "create_object" 2);
-        by (case_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 (case_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 (case_tac "branch" 3);
-   by (case_tac "op_stack" 2);
-       by (case_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";
-
-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 [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);
-by (Asm_full_simp_tac 1);
-be impE 1;
-by (Force_tac 1);
-by (case_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 0cfc347f8d19 -r d1bd2144ab5d src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed May 31 14:30:28 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed May 31 18:06:02 2000 +0200
@@ -6,12 +6,9 @@
     Correctness of the lightweight bytecode verifier
 *)
 
-LBVCorrect = LBVSpec +
+theory 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> 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> 
@@ -19,5 +16,492 @@
                       ((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)))"
   
+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";
+
+lemma fitsD: 
+"fits phi is G rT s0 s2 cert \\<Longrightarrow>
+ (a@(i#b) = is) \\<Longrightarrow>
+ 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;
+
+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";
+  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; 
+    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:
+"\\<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";
+proof intro;
+  fix pc t;
+  assume wtl:  "wtl_inst_list is G rT s0 s3 cert (length is) 0";
+  assume fits: "fits phi is G rT s0 s3 cert";
+  assume pc:   "pc < length is";
+  assume cert: "cert ! pc = Some t";
+  from pc;
+  have "is \\<noteq> []"; by auto;
+  hence cons: "\\<exists>i y. is = i#y"; by (simp add: neq_Nil_conv);
+  from wtl pc;
+  have "\\<exists>a b s1. a@b = is \\<and> length a = pc \\<and> 
+                 wtl_inst_list a G rT s0 s1 cert (length is) 0 \\<and> 
+                 wtl_inst_list b G rT s1 s3 cert (length is) (0+length a)"
+    (is "\\<exists>a b s1. ?A a b \\<and> ?L a \\<and> ?W1 a s1 \\<and> ?W2 a b s1");
+  by (rule wtl_partial [rulify]);
+  with cons;
+  show "phi ! pc = t";
+  proof (elim exE conjE);
+    fix a b s1 i y;
+    assume * :"?A a b" "?L a" "?W1 a s1" "?W2 a b s1" "is = i#y";
+    with pc;
+    have "b \\<noteq> []"; by auto;
+    hence "\\<exists>b' bs. b = b'#bs"; by (simp add: neq_Nil_conv);
+    thus ?thesis;
+    proof (elim exE);
+      fix b' bs; assume Cons: "b=b'#bs";
+      with * fits cert;     
+      show ?thesis; 
+      proof (unfold fits_def fits_partial_def, elim allE impE); 
+        from * Cons; show "a@b'#bs=is"; by simp;
+      qed simp+;
+    qed;
+  qed;
+qed;
+
+lemma fits_lemma2:
+"\\<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";
+proof (unfold fits_def fits_partial_def, elim allE impE);
+qed (auto simp del: split_paired_Ex);
+
+
+
+lemma wtl_suc_pc:
+"\\<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)))";
+proof;
+  assume f: "fits phi (a@i#b) G rT s0 s3 cert";
+  assume "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)"
+  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 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;
+
+lemma wtl_lemma: 
+"\\<lbrakk>wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0;
+  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));
+  fits phi (i1@i#i2) G rT s0 s3 cert\\<rbrakk> \\<Longrightarrow>
+  wt_instr i G rT phi (length (i1@i#i2)) (length i1)" (concl is "?P i");
+proof -;
+  assume w1: "wtl_inst_list i1 G rT s0 s1 cert (length (i1@i#i2)) 0" (is ?w1);
+  assume wo: "wtl_inst_option i G rT s1 s2 cert (length (i1@i#i2)) (length i1)";
+  assume w2: "wtl_inst_list i2 G rT s2 s3 cert (length (i1@i#i2)) (Suc (length i1))";
+  assume f:  "fits phi (i1@i#i2) G rT s0 s3 cert";
+
+  from w1 wo w2;
+  have wtl: "wtl_inst_list (i1@i#i2) G rT s0 s3 cert (length (i1@i#i2)) 0"; 
+    by (rule wtl_cons_appendl);
+
+  with f;  
+  have c1: "\\<forall>t. cert ! (length i1) = Some t \\<longrightarrow> phi ! (length i1) = t";
+    by intro (rule fits_lemma1 [rulify], auto);
+
+  from w1 wo w2 f;
+  have c2: "cert ! (length i1) = None \\<Longrightarrow> phi ! (length i1) = s1";
+    by - (rule fits_lemma2);
+
+  from wtl f;
+  have c3: "\\<forall>pc t. pc < length(i1@i#i2) \\<longrightarrow> cert ! pc = Some t \\<longrightarrow> phi ! pc = t";
+    by (rule fits_lemma1);
+
+  from w1 wo w2 f;
+  have suc: "i2 \\<noteq> [] \\<Longrightarrow> G \\<turnstile> s2 <=s phi ! Suc (length i1)"; 
+    by (rule wtl_suc_pc [rulify]); 
+
+  show ?thesis;
+  proof (cases "i");
+    case LS;    
+    with wo suc;
+    show ?thesis;
+     by - (cases "load_and_store", 
+        (cases "cert ! (length i1)",
+         clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
+         clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);      
+  next;
+    case CO;
+    with wo suc;
+    show ?thesis; 
+     by - (cases "create_object" , 
+           cases "cert ! (length i1)",
+           clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
+           clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
+  next;
+    case MO;
+    with wo suc;
+    show ?thesis;
+     by - (cases "manipulate_object" , 
+           (cases "cert ! (length i1)",
+            clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
+            clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
+  next;
+    case CH;
+    with wo suc;
+    show ?thesis;
+     by - (cases "check_object" , cases "cert ! (length i1)",
+           clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
+           clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
+  next;
+    case MI; 
+    with wo suc;
+    show ?thesis; 
+     by - (cases "meth_inv", cases "cert ! (length i1)",
+           clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
+           intro exI conjI, rule refl, simp, force,
+           clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def,
+           intro exI conjI, rule refl, simp, force);
+  next;
+    case MR;
+    with wo suc;
+    show ?thesis;
+      by - (cases "meth_ret" , cases "cert ! (length i1)",
+            clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
+            clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def);
+  next;
+    case OS;
+    with wo suc;
+    show ?thesis;
+     by - (cases "op_stack" , 
+           (cases "cert ! (length i1)",
+            clarsimp_tac simp add: c2 wt_instr_def wtl_inst_option_def split_beta,
+            clarsimp_tac simp add: c1 wt_instr_def wtl_inst_option_def)+);
+  next;
+    case BR;
+    with wo suc;
+    show ?thesis;
+      by - (cases "branch", 
+            (cases "cert ! (length i1)",
+             clarsimp_tac simp add: c2 c3 wt_instr_def wtl_inst_option_def split_beta,
+             clarsimp_tac simp add: c1 c3 wt_instr_def wtl_inst_option_def)+);
+  qed;
+qed;
+
+lemma wtl_fits_wt:
+"\\<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. pc < length is \\<longrightarrow> wt_instr (is ! pc) G rT phi (length is) pc";
+proof intro;
+  assume fits: "fits phi is G rT s0 s3 cert";
+
+  fix pc;
+  assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0"
+     and pc:  "pc < length is";
+
+  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 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);
+        with l c;
+        show ?thesis; by (auto simp add: nth_append);
+      qed;
+    qed;
+  qed;
+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;
+    
+lemma fits_first:
+"\\<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";
+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 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; 
+qed;
   
-end
+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;
+
+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'";
+  by (induct "l") auto;
+
+lemma unique_epsilon:
+"(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 simp add: unique_set);
+
+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);
+
+  assume wtl_prog: "wtl_jvm_prog G cert";
+  thus "ObjectC \\<in> set G"; by (simp add: wtl_jvm_prog_def wf_prog_def);
+
+  from wtl_prog; 
+  show uniqueG: "unique G"; by (simp add: wtl_jvm_prog_def wf_prog_def);
+
+  show "\\<exists>Phi. Ball (set G) (wf_cdecl (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (Phi C sig)) G)"
+    (is "\\<exists>Phi. ?Q Phi");
+  proof (intro exI);
+    let "?Phi" = 
+        "\\<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";
+    from wtl_prog;
+    show "?Q ?Phi";
+    proof (unfold wf_cdecl_def, intro);
+      fix x a b aa ba ab bb m;
+      assume 1: "x \\<in> set G" "x = (a, b)" "b = (aa, ba)" "ba = (ab, bb)" "m \\<in> set bb";
+      with wtl_prog;
+      show "wf_mdecl (\\<lambda>G C (sig,rT,maxl,b). wt_method G C (snd sig) rT maxl b (?Phi C sig)) G a m";
+      proof (simp add: wf_mdecl_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def, elim conjE);
+        apply_end (drule bspec, assumption, simp, elim conjE);
+        assume "\\<forall>(sig,rT,mb)\\<in>set bb. wf_mhead G sig rT \\<and> 
+                 (\\<lambda>(maxl,b). wtl_method G a (snd sig) rT maxl b (cert a sig)) mb"
+               "unique bb";
+        with 1 uniqueG;
+        show "(\\<lambda>(sig,rT,mb).
+          wf_mhead G sig rT \\<and>
+          (\\<lambda>(maxl,b).
+              wt_method G a (snd sig) rT maxl b 
+               ((\\<lambda>(C,x,y,mdecls).
+                    (\\<lambda>(sig,rT,maxl,b). Eps (wt_method G C (snd sig) rT maxl b))
+                     (\\<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); 
+      qed;
+    qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def);
+  qed;
+qed;
+    
+
+end;
diff -r 0cfc347f8d19 -r d1bd2144ab5d src/HOL/MicroJava/BV/LBVSpec.ML
--- a/src/HOL/MicroJava/BV/LBVSpec.ML	Wed May 31 14:30:28 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-(*  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 (case_tac "i" 1);
-by (case_tac "branch" 8);
-by (case_tac "op_stack" 7);
-by (case_tac "meth_ret" 6);
-by (case_tac "meth_inv" 5);
-by (case_tac "check_object" 4);
-by (case_tac "manipulate_object" 3);
-by (case_tac "create_object" 2);
-by (case_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 (case_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 (case_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 (case_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 (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 0cfc347f8d19 -r d1bd2144ab5d src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed May 31 14:30:28 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Wed May 31 18:06:02 2000 +0200
@@ -6,15 +6,15 @@
 Specification of a lightweight bytecode verifier
 *)
 
-LBVSpec = BVSpec +
+theory LBVSpec = BVSpec:;
 
 types
   certificate       = "state_type option list" 
   class_certificate = "sig \\<Rightarrow> certificate"
-  prog_certificate  = "cname \\<Rightarrow> class_certificate"
+  prog_certificate  = "cname \\<Rightarrow> class_certificate";
 
 consts
- wtl_LS :: "[load_and_store,state_type,state_type,p_count,p_count] \\<Rightarrow> bool"
+ 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
@@ -42,10 +42,10 @@
 	(let (ST,LT) = s
 	 in
 	 pc+1 < max_pc \\<and>
-	 (NT # ST , LT) = s')"
+	 (NT # ST , LT) = s')";
 
 consts
- wtl_MO	:: "[manipulate_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool" 
+ 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
@@ -67,21 +67,21 @@
              ST = vT # oT # ST' \\<and> 
              G \\<turnstile> oT \\<preceq> (Class C) \\<and>
              G \\<turnstile> vT \\<preceq> T  \\<and>
-             (ST' , LT) = s'))"
+             (ST' , LT) = s'))";
 
 
 consts 
- wtl_CO	:: "[create_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool" 
+ 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')"
+	 ((Class C) # ST , LT) = s')";
 
 consts
- wtl_CH	:: "[check_object,jvm_prog,state_type,state_type,p_count,p_count] \\<Rightarrow> bool" 
+ 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
@@ -89,10 +89,10 @@
 	 pc+1 < max_pc \\<and>
 	 is_class G C \\<and> 
 	 (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
-                   (Class C # ST' , LT) = s'))"
+                   (Class C # ST' , LT) = s'))";
 
 consts 
- wtl_OS	:: "[op_stack,state_type,state_type,p_count,p_count] \\<Rightarrow> bool" 
+ 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
@@ -127,10 +127,10 @@
 	 in
 	 pc+1 < max_pc \\<and>
 	 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> 	 
-		       (ts # ts' # ST' , LT) = s'))"
+		       (ts # ts' # ST' , LT) = s'))";
 
 consts 
- wtl_BR	:: "[branch,jvm_prog,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool" 
+ 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
@@ -148,10 +148,10 @@
 	 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'))"
+   (cert ! (pc+1) = Some s'))";
   
 consts
- wtl_MI :: "[meth_inv,jvm_prog,state_type,state_type,certificate,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' cert max_pc pc =
 	(let (ST,LT) = s
@@ -164,20 +164,20 @@
           ((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')))))))"
+          (rT # ST' , LT) = s')))))))";
 
 consts
- wtl_MR	:: "[meth_ret,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+ 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'))"
+   (cert ! (pc+1) = Some s'))";
 
 
 consts 
- wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool"
+ 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"
@@ -186,7 +186,7 @@
  "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"
+ "wtl_inst (BR ins) G rT s s' cert max_pc pc = wtl_BR ins G s s' cert max_pc pc";
 
 
 constdefs
@@ -195,16 +195,16 @@
      (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)"
+                      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"
+ 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)"
 
   "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))"
+           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" 
@@ -216,9 +216,238 @@
                             ([],(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 :: "[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" 
+               wtl_method G C (snd sig) rT maxl b (cert C sig)) G"; 
+
+lemma rev_eq: "\\<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";
+proof auto;
+qed;
+
+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 LS;
+ show "?P (LS load_and_store)"; by (induct load_and_store) auto;
+case CO;
+ show "?P (CO create_object)"; by (induct create_object) auto;
+case MO;
+ show "?P (MO manipulate_object)"; by (induct manipulate_object) auto;
+case CH;
+ show "?P (CH check_object)"; by (induct check_object) auto;
+case MI;
+ show "?P (MI meth_inv)"; proof (induct meth_inv);
+ case Invoke;
+  have "\\<exists>x y. s0 = (x,y)"; by (simp);
+  thus "wtl_inst (MI (Invoke mname list)) G rT s0 s1 cert max_pc pc \\<longrightarrow>
+        wtl_inst (MI (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;
+case MR;
+ show "?P (MR meth_ret)"; by (induct meth_ret) auto;
+case OS; 
+ show "?P (OS op_stack)"; by (induct op_stack) auto;
+case BR;  
+ show "?P (BR branch)"; by (induct branch) auto;
+qed;
+
+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");
+proof (induct "?P" "is"); 
+  case Nil;
+  show "?P []"; by simp;
 
-end 
+  case Cons;
+  show "?P (a # list)"; 
+  proof (intro);
+    fix s0; fix pc; 
+    let "?o s0 s1" = "wtl_inst_option a G rT s0 s1 cert max_pc pc";
+    let "?l l s1 s2 pc" = "wtl_inst_list l G rT s1 s2 cert max_pc pc"; 
+    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;
+  qed;
+qed;
+        
+lemma wtl_partial:
+"\\<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))" (is "?P is");
+proof (induct "?P" "is");
+  case Nil;
+  show "?P []"; by auto;
+  
+  case Cons;
+  show "?P (a#list)";
+  proof (intro allI impI);
+    fix pc' pc s;
+    assume length: "pc' < length (a # list)";
+    assume wtl:    "wtl_inst_list (a # list) G rT s s' cert mpc pc";
+    show "\\<exists> a' b s1. 
+            a' @ b = a#list \\<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')"
+        (is "\\<exists> a b s1. ?E a b s1");
+    proof (cases "pc'");
+      case 0;
+      with wtl;
+      have "?E [] (a#list) s"; by simp;
+      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;
+    qed;
+  qed;
+qed;
+
+lemma "wtl_append1":
+"\\<lbrakk>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)\\<rbrakk> \\<Longrightarrow>
+  wtl_inst_list (x@y) G rT s0 s2 cert (length (x@y)) 0";
+proof -;
+  assume w:
+    "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";
+      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;      
+      with y Cons;
+      have "wtl_inst_list (list @ y) G rT s' s2 cert (Suc pc + length (list @ y)) (Suc pc)";
+        by elim (assumption, simp+);
+      with a;
+      show ?thesis; by (auto simp del: split_paired_Ex);
+    qed;
+  qed;
+qed;
+
+  with w;
+  show ?thesis; 
+  proof elim;
+    from w; show "wtl_inst_list x G rT s0 s1 cert (0+length (x @ y)) 0"; by simp;
+  qed simp+;
+qed;
+
+lemma wtl_cons_appendl:
+"\\<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#b) G rT s0 s3 cert (length (a@i#b)) 0";
+proof -;
+  assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0";
+
+  assume "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))";
+
+  hence "wtl_inst_list (i#b) G rT s1 s3 cert (length (a@i#b)) (length a)";
+    by (auto simp del: split_paired_Ex);
+
+  with a;
+  show ?thesis; by (rule wtl_append1);
+qed;
+
+lemma "wtl_append":
+"\\<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";
+proof -;
+  assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0";
+  assume i: "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)";
+  assume b: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))";
+
+  have "\\<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" (is "?P a");
+  proof (induct "?P" "a");
+    case Nil;
+    show "?P []"; by (simp del: split_paired_Ex);
+    case Cons;
+    show "?P (a#list)" (is "\\<forall>s0 pc. ?x s0 pc \\<longrightarrow> ?y s0 pc \\<longrightarrow> ?z s0 pc \\<longrightarrow> ?p s0 pc"); 
+    proof intro;
+      fix s0 pc;
+      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; 
+          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;
+    qed;
+  qed;
+  with a i b;
+  show ?thesis; 
+  proof elim;
+    from a; show "wtl_inst_list a G rT s0 s1 cert (0+length (a@i#b)) 0"; by simp;
+  qed auto;
+qed;
+
+end;