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