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";
-
-
-
-
-