# HG changeset patch
# User kleing
# Date 967664859 -7200
# Node ID 1024a2d80ac016781aeb5d71d00b5b0914397a0e
# Parent  3533e3e9267fb861ac6c9d5dfff2e2b6aae95f0b
functional LBV style, dead code, type safety -> Isar

diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/BVSpec.thy
--- a/src/HOL/MicroJava/BV/BVSpec.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -3,61 +3,62 @@
     Author:     Cornelia Pusch
     Copyright   1999 Technische Universitaet Muenchen
 
-Specification of bytecode verifier
 *)
 
-theory BVSpec = Step :
+header "The Bytecode Verifier"
+
+theory BVSpec = Step:
 
 types
- method_type = "state_type list"
- class_type	 = "sig \\<Rightarrow> method_type"
- prog_type	 = "cname \\<Rightarrow> class_type"
+ method_type = "state_type option list"
+ class_type	 = "sig \<Rightarrow> method_type"
+ prog_type	 = "cname \<Rightarrow> class_type"
 
 constdefs
-wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \\<Rightarrow> bool"
-"wt_instr i G rT phi max_pc pc \\<equiv> 
-    app (i, G, rT, phi!pc) \\<and>
-   (\\<forall> pc' \\<in> (succs i pc). pc' < max_pc \\<and> (G \\<turnstile> the (step (i, G, phi!pc)) <=s phi!pc'))"
+wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \<Rightarrow> bool"
+"wt_instr i G rT phi max_pc pc \<equiv> 
+    app i G rT (phi!pc) \<and>
+   (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))"
 
-wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
-"wt_start G C pTs mxl phi \\<equiv> 
-    G \\<turnstile> ([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) <=s phi!0"
+wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool"
+"wt_start G C pTs mxl phi \<equiv> 
+    G \<turnstile> Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err)) <=' phi!0"
 
 
-wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
-"wt_method G C pTs rT mxl ins phi \\<equiv>
+wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \<Rightarrow> bool"
+"wt_method G C pTs rT mxl ins phi \<equiv>
 	let max_pc = length ins
         in
-	length ins < length phi \\<and> 0 < max_pc \\<and> wt_start G C pTs mxl phi \\<and> 
-	(\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
+	0 < max_pc \<and> wt_start G C pTs mxl phi \<and> 
+	(\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
 
-wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool"
-"wt_jvm_prog G phi \\<equiv>
-   wf_prog (\\<lambda>G C (sig,rT,maxl,b).
+wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
+"wt_jvm_prog G phi \<equiv>
+   wf_prog (\<lambda>G C (sig,rT,maxl,b).
               wt_method G C (snd sig) rT maxl b (phi C sig)) G"
 
 
 
 lemma wt_jvm_progD:
-"wt_jvm_prog G phi \\<Longrightarrow> (\\<exists>wt. wf_prog wt G)"
+"wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
 by (unfold wt_jvm_prog_def, blast)
 
 lemma wt_jvm_prog_impl_wt_instr:
-"\\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \\<rbrakk> 
- \\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
+"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \<rbrakk> 
+ \<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
     simp, simp add: wf_mdecl_def wt_method_def)
 
 lemma wt_jvm_prog_impl_wt_start:
-"\\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \\<rbrakk> \\<Longrightarrow> 
- 0 < (length ins) \\<and> wt_start G C (snd sig) maxl (phi C sig)"
+"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \<rbrakk> \<Longrightarrow> 
+ 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
     simp, simp add: wf_mdecl_def wt_method_def)
 
-lemma [simp]: 
-"succs i pc = {pc+1} \\<Longrightarrow> wt_instr i G rT phi max_pc pc = 
-    (app (i, G, rT, phi!pc) \\<and> pc+1 < max_pc \\<and> 
-     (G \\<turnstile> the (step (i, G, phi!pc)) <=s phi!(pc+1)))"
+(* for most instructions wt_instr collapses: *)
+lemma  
+"succs i pc = [pc+1] \<Longrightarrow> wt_instr i G rT phi max_pc pc = 
+ (app i G rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
 by (simp add: wt_instr_def) 
 
 end
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Wed Aug 30 21:44:12 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,517 +0,0 @@
-(*  Title:      HOL/MicroJava/BV/BVSpecTypeSafe.ML
-    ID:         $Id$
-    Author:     Cornelia Pusch
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-val defs1 = exec.simps@[split_def,thm "sup_state_def",correct_state_def,
-		correct_frame_def, thm "wt_instr_def"];
-
-Goalw [correct_state_def,Let_def,correct_frame_def,split_def]
-"\\<lbrakk> wt_jvm_prog G phi; \
-\   method (G,C) sig = Some (C,rT,maxl,ins); \
-\   G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc";
-by (Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [thm "wt_jvm_prog_impl_wt_instr"]) 1);
-qed "wt_jvm_prog_impl_wt_instr_cor";
-
-
-Delsimps [split_paired_All]; 
-
-
-(******* LS *******)
-
-
-Goal
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = Load idx; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (case_tac "phi C sig!pc" 1);
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_val_sup,
-	approx_loc_imp_approx_loc_sup] 
-	addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Load_correct";
-
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = Store idx; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)]
-	addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Store_correct";
-
-
-Goalw [conf_def] "G,h \\<turnstile> Intg i \\<Colon>\\<preceq> PrimT Integer";
-by(Simp_tac 1);
-qed "conf_Intg_Integer";
-AddIffs [conf_Intg_Integer];
-
-Goal
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = Bipush i; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (case_tac "phi C sig ! pc" 1);
-by (fast_tac (claset()addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
-	addss (simpset() addsimps [approx_val_def,thm "sup_PTS_eq",map_eq_Cons]@defs1)) 1);
-qed "Bipush_correct";
-
-Goal "G \\<turnstile> T' \\<preceq> T \\<Longrightarrow> T' = NT \\<longrightarrow> (T=NT | (\\<exists>C. T = Class C))";
-be widen.induct 1;
-by(Auto_tac);
-by(rename_tac "R" 1);
-by(case_tac "R" 1);
-by(Auto_tac);
-val lemma = result();
-
-Goal "G \\<turnstile> NT \\<preceq> T = (T=NT | (\\<exists>C. T = Class C))";
-by(force_tac (claset() addIs widen.intrs addDs [lemma],simpset()) 1);
-qed "NT_subtype_conv";
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc =  Aconst_null; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (case_tac "phi C sig ! pc" 1);
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
-	addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,map_eq_Cons]@defs1)) 1);
-qed "Aconst_null_correct";
-
-
-Goalw [cast_ok_def]
- "\\<lbrakk> wf_prog ok G; G,h\\<turnstile>v\\<Colon>\\<preceq>RefT rt; cast_ok G C h v ; G\\<turnstile>Class C\\<preceq>T; is_class G C \\<rbrakk> \
-\ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T";
-by (forward_tac [widen_Class] 1);
-by (Clarify_tac 1);
-be disjE 1;
- by (asm_full_simp_tac (simpset() addsimps [widen.null]) 1);
-by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [obj_ty_def]) 1);
-by (case_tac "v" 1);
-by (ALLGOALS (fast_tac  (claset() addIs [rtrancl_trans] addss (simpset() addsimps [widen.null]))));
-qed "Cast_conf2";
-
-Goal
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = Checkcast D; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (asm_full_simp_tac (simpset() addsimps [map_eq_Cons,
-		raise_xcpt_def]@defs1 addsplits [option.split]) 1);
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2] 
-	addss (simpset() addsimps [map_eq_Cons,approx_val_def])) 1);
-qed "Checkcast_correct";
-
-Goal
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = Getfield F D; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [thm "sup_state_def",map_eq_Cons]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
-
-by (forward_tac [conf_widen] 1);
-  ba 1;
- ba 1;
-bd conf_RefTD 1;
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1); 
-
-br conjI 1;
- bd widen_cfs_fields 1;
-   ba 1;
-  ba 1;
- by (fast_tac (claset() addIs [conf_widen] addss (simpset() addsimps [hconf_def,oconf_def,lconf_def])) 1);
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]) 1);
-qed "Getfield_correct";
-
-
-
-Goal
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = Putfield F D; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (asm_full_simp_tac (simpset() addsimps [raise_xcpt_def]@defs1 addsplits [option.split]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [thm "sup_state_def",map_eq_Cons]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
-
-by (forward_tac [conf_widen] 1);
-  ba 2;
- ba 1;
-by (fast_tac (claset() addDs [conf_RefTD,widen_cfs_fields] 
-	addIs [sup_heap_update_value,approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
-		approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
-		hconf_imp_hconf_field_update,
-		correct_frames_imp_correct_frames_field_update,conf_widen] addss (simpset())) 1);
-qed "Putfield_correct";
-
-Goal "(\\<forall>x y. P(x,y)) = (\\<forall>z. P z)";
-by(Fast_tac 1);
-qed "collapse_paired_All";
-
-Goal
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = New cl_idx; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (case_tac "phi C sig ! pc" 1);
-by (fast_tac (claset() addSDs [collapse_paired_All RS iffD1]addIs [sup_heap_newref,
-		approx_stk_imp_approx_stk_sup_heap RSN(2,approx_stk_imp_approx_stk_sup),
-		approx_loc_imp_approx_loc_sup_heap RSN(2,approx_loc_imp_approx_loc_sup),
-		hconf_imp_hconf_newref,correct_frames_imp_correct_frames_newref,
-		rewrite_rule [split_def] correct_init_obj]
-	addss (simpset() addsimps [NT_subtype_conv,approx_val_def,conf_def,
-		fun_upd_apply,map_eq_Cons,is_class_def,raise_xcpt_def,init_vars_def]@defs1 
-	addsplits [option.split])) 1);
-qed "New_correct";
-
-
-
-Delsimps (thms "app.simps");
-
-(****** Method Invocation ******)
-
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = Invoke C' mn pTs; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(case_tac "phi C sig ! pc" 1);
-by(forward_tac [thm "wt_jvm_progD"] 1);
-by(etac exE 1);
-by(asm_full_simp_tac (simpset() addsimps defs1) 1);
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [raise_xcpt_def] addsplits [option.split]) 1);
-by(Clarify_tac 1);
-bd approx_stk_append_lemma 1;
-by(clarsimp_tac (claset(), simpset() addsimps [approx_val_def]) 1);
-
-by (subgoal_tac "\\<exists> D'. X = Class D'" 1);
- bd widen_RefT2 2;
- by (Clarsimp_tac 2);
- bd conf_RefTD 2;
- by (Clarsimp_tac 2);
- bd widen_Class 2;
- by (Clarsimp_tac 2);
-
-by (Clarsimp_tac 1);
-bd conf_RefTD 1;
-by (Clarify_tac 1);
-by(rename_tac "oloc oT ofs T'" 1);
-by (asm_full_simp_tac (simpset() addsimps defs1) 1);
-by (subgoal_tac "G\\<turnstile>oT\\<preceq>C C'" 1);
- bd widen.subcls 2;
- bd widen.subcls 2;
- by (((dtac widen_trans) THEN' atac THEN' Blast_tac) 2);
-bd subtype_widen_methd 1;
-  ba 1;
- ba 1;
-by (Clarify_tac 1);
-bd subtype_widen_methd 1;
-  ba 1;
- ba 1;
-be exE 1;
-by(rename_tac "oT'" 1);
-by (Clarify_tac 1);
-by(subgoal_tac "G \\<turnstile> oT \\<preceq>C oT'" 1);
- by(forw_inst_tac [("C","oT")] method_wf_mdecl 2); 
-  ba 2;
- by (Blast_tac 2);
-by (asm_full_simp_tac (simpset() addsimps defs1) 1);
-by(forward_tac [method_in_md] 1);
- ba 1;
- back();
- back();
- back();
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps defs1) 1);
-by (forward_tac [thm "wt_jvm_prog_impl_wt_start"] 1);
- ba 1;
- back();
-by (asm_full_simp_tac (simpset() addsimps [thm "wt_start_def",thm "sup_state_def"]) 1);
-by (Clarify_tac 1);
-
-(** approx_loc **)
-br conjI 1;
- br approx_loc_imp_approx_loc_sup 1;
-   ba 1;
-  by (Fast_tac 2);
- by (asm_full_simp_tac (simpset() addsimps [split_def,approx_val_def,approx_loc_append]) 1);
- br conjI 1;
-  br conf_widen 1;
-    ba 1;
-   by (Fast_tac 2);
-  by (asm_full_simp_tac (simpset() addsimps [conf_def]) 1);
- br conjI 1;
-  by (fast_tac (claset() addIs [approx_stk_rev RS iffD2 RSN(4,assConv_approx_stk_imp_approx_loc)] 
-	addss (simpset() addsimps [split_def,approx_val_def])) 1);
- by (asm_simp_tac (simpset() addsimps [list_all2_def,split_def,approx_loc_def,approx_val_None,set_replicate_conv_if]) 1);
- 
-br conjI 1;
- by (asm_simp_tac (simpset() addsimps [min_def]) 1);
-br exI 1;
-br exI 1;
-br conjI 1;
- by(Blast_tac 1);
-by (Clarsimp_tac 1);
-
-by (fast_tac (claset()
-       addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup]
-       addss (simpset()addsimps [map_eq_Cons])) 1);
-qed "Invoke_correct";
-
-Addsimps (thms "app.simps");
-
-
-Delsimps [map_append];
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = Return; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (asm_full_simp_tac (simpset() addsimps (neq_Nil_conv::defs1) addsplits [split_if_asm]) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [map_eq_Cons]@defs1) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps defs1) 1);
-by (forward_tac [thm "wt_jvm_prog_impl_wt_instr"] 1);
-  by(EVERY1[atac, etac Suc_lessD]);
-by(rewtac (thm "wt_jvm_prog_def"));
-by (case_tac "phi ab (ac, b) ! k" 1);
-by (fast_tac (claset()
- addDs [subcls_widen_methd]
- addEs [rotate_prems 1 widen_trans]
- addIs [conf_widen]
- addss (simpset() addsimps [approx_val_def,append_eq_conv_conj,map_eq_Cons]@defs1)) 1);
-qed "Return_correct";
-Addsimps [map_append];
-
-
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = Goto branch; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup,approx_stk_imp_approx_stk_sup]
-	addss (simpset() addsimps defs1)) 1);
-qed "Goto_correct";
-
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins!pc = Ifcmpeq branch; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
-qed "Ifcmpeq_correct";
-
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = Pop; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
-qed "Pop_correct";
-
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = Dup; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
-	addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Dup_correct";
-
-
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = Dup_x1; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
-	addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Dup_x1_correct";
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = Dup_x2; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
-	addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Dup_x2_correct";
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = Swap; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
-	addss (simpset() addsimps [map_eq_Cons]@defs1)) 1);
-qed "Swap_correct";
-
-
-Goal 
-"\\<lbrakk> wf_prog wt G; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  ins ! pc = IAdd; \
-\  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup]
-  addss (simpset() addsimps [map_eq_Cons, approx_val_def]@defs1)) 1);
-qed "IAdd_correct";
-
-
-
-(** instr correct **)
-
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; \
-\  method (G,C) sig = Some (C,rT,maxl,ins); \
-\  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; \
-\  G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \\<rbrakk> \
-\\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(forward_tac [wt_jvm_prog_impl_wt_instr_cor] 1);
-  ba 1;
- ba 1;
-by(case_tac "ins!pc" 1);
-by(fast_tac (claset() addIs [Invoke_correct]) 9);
-by(fast_tac (claset() addIs [Return_correct]) 9);
-by(rewtac (thm "wt_jvm_prog_def"));
-by (ALLGOALS (fast_tac (claset() addIs 
-      [Load_correct,Store_correct,Bipush_correct,Aconst_null_correct,
-       Checkcast_correct,Getfield_correct,Putfield_correct,New_correct,
-       Goto_correct,Ifcmpeq_correct,Pop_correct,Dup_correct,
-       Dup_x1_correct,Dup_x2_correct,Swap_correct,IAdd_correct])));
-qed "instr_correct";
-
-
-(** Main **)
-
-Goalw [correct_state_def,Let_def]
- "G,phi \\<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\\<surd> \
-\ \\<Longrightarrow> \\<exists>meth. method (G,C) sig = Some(C,meth)";
-by(Asm_full_simp_tac 1);
-by(Blast_tac 1);
-qed "correct_state_impl_Some_method";
-
-Goal
-"\\<And>state. \\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM state\\<surd>\\<rbrakk> \
-\ \\<Longrightarrow> exec (G,state) = Some state' \\<longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
-by(split_all_tac 1);
-by(rename_tac "xp hp frs" 1);
-by (case_tac "xp" 1);
- by (case_tac "frs" 1);
-  by (asm_full_simp_tac (simpset() addsimps exec.simps) 1);
- by(split_all_tac 1);
- by(hyp_subst_tac 1);
- by(forward_tac [correct_state_impl_Some_method] 1);
- by (force_tac (claset() addIs [instr_correct], simpset() addsplits [split_if_asm] addsimps exec.simps@[split_def]) 1);
-by (case_tac "frs" 1);
- by (ALLGOALS(asm_full_simp_tac (simpset() addsimps exec.simps)));
-qed_spec_mp "BV_correct_1";
-
-(*******)
-Goal
-"\\<lbrakk> xp=None; frs\\<noteq>[] \\<rbrakk> \\<Longrightarrow> (\\<exists>state'. exec (G,xp,hp,frs) = Some state')";
-by (auto_tac (claset() addIs [BV_correct_1],
-             (simpset() addsplits [instr.split] addsimps [neq_Nil_conv]@defs1)));
-by (case_tac "(snd (snd (snd (the (method (G, ab) (ac, b)))))) ! ba" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps defs1)));
-val lemma = result();
-
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; G,phi \\<turnstile>JVM (xp,hp,frs)\\<surd>; xp=None; frs\\<noteq>[] \\<rbrakk> \
-\ \\<Longrightarrow> \\<exists>state'. exec(G,xp,hp,frs) = Some state' \\<and> G,phi \\<turnstile>JVM state'\\<surd>";
-by (dres_inst_tac [("G","G"),("hp","hp")] lemma 1);
-ba 1;
-by (fast_tac (claset() addIs [BV_correct_1]) 1);
-qed "L1";
-(*******)
-
-Goalw [exec_all_def]
-"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s -jvm\\<rightarrow> t \\<rbrakk> \\<Longrightarrow> G,phi \\<turnstile>JVM s\\<surd> \\<longrightarrow> G,phi \\<turnstile>JVM t\\<surd>";
-be rtrancl_induct 1;
- by (Simp_tac 1);
-by (fast_tac (claset() addIs [BV_correct_1] addss (simpset())) 1);
-qed_spec_mp "BV_correct";
-
-
-Goal
-"\\<lbrakk> wt_jvm_prog G phi; G \\<turnstile> s0 -jvm\\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \\<turnstile>JVM s0 \\<surd>\\<rbrakk> \
-\ \\<Longrightarrow>  approx_stk G hp stk (fst (((phi  C)  sig) ! pc)) \\<and> approx_loc G hp loc (snd (((phi  C)  sig) ! pc)) ";
-bd BV_correct 1;
-ba 1;
-ba 1;
-by (asm_full_simp_tac (simpset() addsimps [correct_state_def,correct_frame_def,split_def] 
-	addsplits [option.split_asm]) 1);
-qed_spec_mp "BV_correct_initial";
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -7,4 +7,630 @@
 programs.
 *)
 
-BVSpecTypeSafe = Correct
+header "Type Safety Proof"
+
+theory BVSpecTypeSafe = Correct:
+
+lemmas defs1 = sup_state_def correct_state_def correct_frame_def wt_instr_def step_def
+lemmas [simp del] = split_paired_All
+
+lemma wt_jvm_prog_impl_wt_instr_cor:
+  "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); 
+      G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> |] 
+  ==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"
+apply (unfold correct_state_def Let_def correct_frame_def)
+apply simp
+apply (blast intro: wt_jvm_prog_impl_wt_instr)
+.
+
+lemma Load_correct:
+"\<lbrakk> wf_prog wt G;
+   method (G,C) sig = Some (C,rT,maxl,ins); 
+   ins!pc = Load idx; 
+   wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+   Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
+   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (rule conjI)
+ apply (rule approx_loc_imp_approx_val_sup)
+ apply simp+
+apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+.
+
+lemma Store_correct:
+"\<lbrakk> wf_prog wt G;
+  method (G,C) sig = Some (C,rT,maxl,ins);
+  ins!pc = Store idx;
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc;
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (rule conjI)
+ apply (blast intro: approx_stk_imp_approx_stk_sup)
+apply (blast intro: approx_loc_imp_approx_loc_subst approx_loc_imp_approx_loc_sup)
+.
+
+
+lemma conf_Intg_Integer [iff]:
+  "G,h \<turnstile> Intg i \<Colon>\<preceq> PrimT Integer"
+by (simp add: conf_def)
+
+
+lemma Bipush_correct:
+"\<lbrakk> wf_prog wt G;
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins!pc = Bipush i; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs);
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk>
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+apply (clarsimp simp add: defs1 approx_val_def sup_PTS_eq map_eq_Cons)
+apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+.
+
+lemma NT_subtype_conv:
+  "G \<turnstile> NT \<preceq> T = (T=NT \<or> (\<exists>C. T = Class C))"
+proof -
+  have "\<And>T T'. G \<turnstile> T' \<preceq> T \<Longrightarrow> T' = NT \<longrightarrow> (T=NT | (\<exists>C. T = Class C))"
+    apply (erule widen.induct)
+    apply auto
+    apply (case_tac R)
+    apply auto
+    .
+  note l = this
+
+  show ?thesis 
+    by (force intro: null dest: l)
+qed
+
+lemma Aconst_null_correct:
+"\<lbrakk> wf_prog wt G;
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins!pc =  Aconst_null; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (rule conjI)
+ apply (force simp add: approx_val_Null NT_subtype_conv)
+apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+.
+
+
+lemma Cast_conf2:
+  "\<lbrakk>wf_prog ok G; G,h\<turnstile>v\<Colon>\<preceq>RefT rt; cast_ok G C h v; G\<turnstile>Class C\<preceq>T; is_class G C\<rbrakk> 
+  \<Longrightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
+apply (unfold cast_ok_def)
+apply (frule widen_Class)
+apply (elim exE disjE)
+ apply (simp add: null)
+apply (clarsimp simp add: conf_def obj_ty_def)
+apply (cases v)
+apply (auto intro: null rtrancl_trans)
+.
+
+
+lemma Checkcast_correct:
+"\<lbrakk> wf_prog wt G;
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins!pc = Checkcast D; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1 map_eq_Cons raise_xcpt_def approx_val_def)
+apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup Cast_conf2)
+.
+
+
+lemma Getfield_correct:
+"\<lbrakk> wf_prog wt G;
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins!pc = Getfield F D; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+apply (clarsimp simp add: defs1 raise_xcpt_def map_eq_Cons approx_val_def split: option.split)
+apply (frule conf_widen)
+apply assumption+
+apply (drule conf_RefTD)
+apply (clarsimp simp add: defs1 approx_val_def)
+apply (rule conjI)
+ apply (drule widen_cfs_fields)
+ apply assumption+
+ apply (force intro: conf_widen simp add: hconf_def oconf_def lconf_def)
+apply (blast intro: approx_stk_imp_approx_stk_sup approx_loc_imp_approx_loc_sup)
+.
+
+lemma Putfield_correct:
+"\<lbrakk> wf_prog wt G;
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins!pc = Putfield F D; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+apply (clarsimp simp add: defs1 raise_xcpt_def split: option.split List.split)
+apply (clarsimp simp add: approx_val_def)
+apply (frule conf_widen)
+prefer 2
+apply assumption
+apply assumption
+apply (drule conf_RefTD)
+apply clarsimp
+apply (blast intro: sup_heap_update_value approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup
+		approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
+		hconf_imp_hconf_field_update
+		correct_frames_imp_correct_frames_field_update conf_widen dest: widen_cfs_fields)
+.
+
+lemma collapse_paired_All:
+  "(\<forall>x y. P(x,y)) = (\<forall>z. P z)"
+  by fast
+
+lemma New_correct:
+"\<lbrakk> wf_prog wt G;
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins!pc = New cl_idx; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: NT_subtype_conv approx_val_def conf_def
+		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
+       split: option.split)
+apply (force dest!: iffD1 [OF collapse_paired_All]
+            intro: sup_heap_newref approx_stk_imp_approx_stk_sup_heap approx_stk_imp_approx_stk_sup
+                   approx_loc_imp_approx_loc_sup_heap approx_loc_imp_approx_loc_sup
+                   hconf_imp_hconf_newref correct_frames_imp_correct_frames_newref
+                   correct_init_obj simp add:  NT_subtype_conv approx_val_def conf_def
+		   fun_upd_apply map_eq_Cons is_class_def raise_xcpt_def init_vars_def defs1 
+       split: option.split)
+.
+
+
+(****** Method Invocation ******)
+
+lemmas [simp del] = split_paired_Ex
+
+lemma Invoke_correct:
+"\<lbrakk> wt_jvm_prog G phi; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = Invoke C' mn pTs; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>" 
+proof -
+  assume wtprog: "wt_jvm_prog G phi"
+  assume method: "method (G,C) sig = Some (C,rT,maxl,ins)"
+  assume ins:    "ins ! pc = Invoke C' mn pTs"
+  assume wti:    "wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"
+  assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
+  assume approx: "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>"
+  
+  from wtprog 
+  obtain wfmb where
+    wfprog: "wf_prog wfmb G" 
+    by (simp add: wt_jvm_prog_def)
+
+  from ins method approx
+  obtain s where
+    heap_ok: "G\<turnstile>h hp\<surd>" and
+    phi_pc:  "phi C sig!pc = Some s" and
+    frame:   "correct_frame G hp s maxl ins (stk, loc, C, sig, pc)" and
+    frames:  "correct_frames G hp phi rT sig frs"
+    by (clarsimp simp add: correct_state_def)
+
+  from ins wti phi_pc
+  obtain apTs X ST LT D' rT body where 
+    s: "s = (rev apTs @ X # ST, LT)" and
+    l: "length apTs = length pTs" and
+    X: "G\<turnstile> X \<preceq> Class C'" and
+    w: "\<forall>x\<in>set (zip apTs pTs). x \<in> widen G" and
+    mC': "method (G, C') (mn, pTs) = Some (D', rT, body)" and
+    pc:  "Suc pc < length ins" and
+    step: "G \<turnstile> step (Invoke C' mn pTs) G (Some s) <=' phi C sig!Suc pc"
+    by (simp add: wt_instr_def) (elim exE conjE, rule that)
+
+  from step
+  obtain ST' LT' where
+    s': "phi C sig ! Suc pc = Some (ST', LT')"
+    by (simp add: step_def split_paired_Ex) (elim, rule that)
+
+  from X 
+  obtain T where
+    X_Ref: "X = RefT T"
+    by - (drule widen_RefT2, erule exE, rule that)
+  
+  from s ins frame 
+  obtain 
+    a_stk: "approx_stk G hp stk (rev apTs @ X # ST)" and
+    a_loc: "approx_loc G hp loc LT" and
+    suc_l: "length loc = Suc (length (snd sig) + maxl)"
+    by (simp add: correct_frame_def)
+
+  from a_stk
+  obtain opTs stk' oX where
+    opTs:   "approx_stk G hp opTs (rev apTs)" and
+    oX:     "approx_val G hp oX (Ok X)" and
+    a_stk': "approx_stk G hp stk' ST" and
+    stk':   "stk = opTs @ oX # stk'" and
+    l_o:    "length opTs = length apTs" 
+            "length stk' = length ST" 
+    by - (drule approx_stk_append_lemma, simp, elim, simp)
+
+  from oX 
+  have "\<exists>T'. typeof (option_map obj_ty \<circ> hp) oX = Some T' \<and> G \<turnstile> T' \<preceq> X"
+    by (clarsimp simp add: approx_val_def conf_def)
+
+  with X_Ref
+  obtain T' where
+    oX_Ref: "typeof (option_map obj_ty \<circ> hp) oX = Some (RefT T')"
+            "G \<turnstile> RefT T' \<preceq> X" 
+    apply (elim, simp)
+    apply (frule widen_RefT2)
+    by (elim, simp)
+
+  from stk' l_o l
+  have oX_pos: "last (take (Suc (length pTs)) stk) = oX" 
+    by simp
+
+  with state' method ins 
+  have Null_ok: "oX = Null \<Longrightarrow> ?thesis"
+    by (simp add: correct_state_def raise_xcpt_def)
+  
+  { fix ref
+    assume oX_Addr: "oX = Addr ref"
+    
+    with oX_Ref
+    obtain obj where
+      loc: "hp ref = Some obj" "obj_ty obj = RefT T'"
+      by clarsimp
+
+    then 
+    obtain D where
+      obj_ty: "obj_ty obj = Class D"
+      by (auto simp add: obj_ty_def)
+
+    with X_Ref oX_Ref loc
+    obtain D: "G \<turnstile> Class D \<preceq> X"
+      by simp
+
+    with X_Ref
+    obtain X' where 
+      X': "X = Class X'"
+      by - (drule widen_Class, elim, rule that)
+      
+    with X
+    have "G \<turnstile> X' \<preceq>C C'" 
+      by simp
+
+    with mC' wfprog
+    obtain D0 rT0 maxl0 ins0 where
+      mX: "method (G, X') (mn, pTs) = Some (D0, rT0, maxl0, ins0)" "G\<turnstile>rT0\<preceq>rT"
+      by (auto dest: subtype_widen_methd)
+
+    from X' D
+    have "G \<turnstile> D \<preceq>C X'" 
+      by simp
+
+    with wfprog mX
+    obtain D'' rT' mxl' ins' where
+      mD: "method (G, D) (mn, pTs) = Some (D'', rT', mxl', ins')" 
+          "G \<turnstile> rT' \<preceq> rT0"
+      by (auto dest: subtype_widen_methd)
+
+    from mX mD
+    have rT': "G \<turnstile> rT' \<preceq> rT"
+      by - (rule widen_trans)
+    
+    from mD wfprog
+    obtain mD'': 
+      "method (G, D'') (mn, pTs) = Some (D'', rT', mxl', ins')"
+      "is_class G D''" 
+      by (auto dest: method_in_md)
+      
+    from loc obj_ty
+    have "fst (the (hp ref)) = D"
+      by (simp add: obj_ty_def)
+
+    with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD 
+    have state'_val:
+      "state' =
+       Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, 
+                  D'', (mn, pTs), 0) # (stk', loc, C, sig, Suc pc) # frs)"
+      (is "state' = Norm (hp, ?f # ?f' # frs)")
+      by (simp add: raise_xcpt_def)
+    
+    from wtprog mD''
+    have start: "wt_start G D'' pTs mxl' (phi D'' (mn, pTs)) \<and> ins' \<noteq> []"
+      by (auto dest: wt_jvm_prog_impl_wt_start)
+    
+    then
+    obtain LT0 where
+      LT0: "phi D'' (mn, pTs) ! 0 = Some ([], LT0)"
+      by (clarsimp simp add: wt_start_def sup_state_def)
+
+    have c_f: "correct_frame G hp ([], LT0) mxl' ins' ?f"
+    proof -
+      from start LT0
+      have sup_loc: 
+        "G \<turnstile> (Ok (Class D'') # map Ok pTs @ replicate mxl' Err) <=l LT0"
+        (is "G \<turnstile> ?LT <=l LT0")
+        by (simp add: wt_start_def sup_state_def)
+
+      have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
+        by (simp add: approx_loc_def approx_val_Err list_all2_def set_replicate_conv_if)
+
+      from wfprog mD
+      have "G \<turnstile> Class D \<preceq> Class D''"
+        by (auto dest: method_wf_mdecl)
+      with obj_ty loc
+      have a: "approx_val G hp (Addr ref) (Ok (Class D''))"
+        by (simp add: approx_val_def conf_def)
+
+      from w l
+      have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G"
+        by (auto simp add: zip_rev)
+      with wfprog l l_o opTs
+      have "approx_loc G hp opTs (map Ok (rev pTs))"
+        by (auto intro: assConv_approx_stk_imp_approx_loc)
+      hence "approx_stk G hp opTs (rev pTs)"
+        by (simp add: approx_stk_def)
+      hence "approx_stk G hp (rev opTs) pTs"
+        by (simp add: approx_stk_rev)
+
+      with r a l_o l
+      have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT"
+        (is "approx_loc G hp ?lt ?LT")
+        by (auto simp add: approx_loc_append approx_stk_def)
+
+      from wfprog this sup_loc
+      have "approx_loc G hp ?lt LT0"
+        by (rule approx_loc_imp_approx_loc_sup)
+
+      with start l_o l
+      show ?thesis
+        by (simp add: correct_frame_def)
+    qed
+
+    have c_f': "correct_frame G hp (tl ST', LT') maxl ins ?f'"
+    proof -    
+      from s s' mC' step l
+      have "G \<turnstile> LT <=l LT'"
+        by (simp add: step_def sup_state_def)
+      with wfprog a_loc
+      have a: "approx_loc G hp loc LT'"
+        by (rule approx_loc_imp_approx_loc_sup)
+      moreover
+      from s s' mC' step l
+      have  "G \<turnstile> map Ok ST <=l map Ok (tl ST')"
+        by (auto simp add: step_def sup_state_def map_eq_Cons)
+      with wfprog a_stk'
+      have "approx_stk G hp stk' (tl ST')"
+        by (rule approx_stk_imp_approx_stk_sup)
+      ultimately
+      show ?thesis
+        by (simp add: correct_frame_def suc_l pc)
+    qed
+
+    with state'_val heap_ok mD'' ins method phi_pc s X' l 
+         frames s' LT0 c_f c_f'
+    have ?thesis
+      by (simp add: correct_state_def) (intro exI conjI, force+)
+  }
+  
+  with Null_ok oX_Ref
+  show "G,phi \<turnstile>JVM state'\<surd>"
+    by - (cases oX, auto)
+qed
+
+lemmas [simp del] = map_append
+
+lemma Return_correct:
+"\<lbrakk> wt_jvm_prog G phi;  
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = Return; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: neq_Nil_conv defs1 split: split_if_asm)
+apply (frule wt_jvm_prog_impl_wt_instr)
+apply (tactic "EVERY1[atac, etac Suc_lessD]")
+apply (unfold wt_jvm_prog_def)
+apply (tactic {* fast_tac (claset()
+ addDs [thm "subcls_widen_methd"]
+ addEs [rotate_prems 1 widen_trans]
+ addIs [conf_widen]
+ addss (simpset() addsimps [thm "approx_val_def",thm "append_eq_conv_conj", map_eq_Cons]@thms "defs1")) 1 *})
+.
+
+lemmas [simp] = map_append
+
+lemma Goto_correct:
+"\<lbrakk> wf_prog wt G; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = Goto branch; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1)
+apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+.
+
+
+lemma Ifcmpeq_correct:
+"\<lbrakk> wf_prog wt G; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = Ifcmpeq branch; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1)
+apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+.
+
+lemma Pop_correct:
+"\<lbrakk> wf_prog wt G; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = Pop;
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1)
+apply (fast intro: approx_loc_imp_approx_loc_sup approx_stk_imp_approx_stk_sup)
+.
+
+lemma Dup_correct:
+"\<lbrakk> wf_prog wt G; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = Dup;
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+             simp add: defs1 map_eq_Cons)
+.
+
+lemma Dup_x1_correct:
+"\<lbrakk> wf_prog wt G; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = Dup_x1;
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+             simp add: defs1 map_eq_Cons)
+.
+
+lemma Dup_x2_correct:
+"\<lbrakk> wf_prog wt G; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = Dup_x2;
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+             simp add: defs1 map_eq_Cons)
+.
+
+lemma Swap_correct:
+"\<lbrakk> wf_prog wt G; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = Swap;
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1 map_eq_Cons)
+apply (force intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup
+             simp add: defs1 map_eq_Cons)
+.
+
+lemma IAdd_correct:
+"\<lbrakk> wf_prog wt G; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  ins ! pc = IAdd; 
+  wt_instr (ins!pc) G rT (phi C sig) (length ins) pc; 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs) ; 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (clarsimp simp add: defs1 map_eq_Cons approx_val_def conf_def)
+apply (blast intro: approx_stk_imp_approx_stk_sup approx_val_imp_approx_val_sup approx_loc_imp_approx_loc_sup)
+.
+
+
+(** instr correct **)
+
+lemma instr_correct:
+"\<lbrakk> wt_jvm_prog G phi; 
+  method (G,C) sig = Some (C,rT,maxl,ins); 
+  Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs); 
+  G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> \<rbrakk> 
+\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
+apply (frule wt_jvm_prog_impl_wt_instr_cor)
+apply assumption+
+apply (cases "ins!pc")
+prefer 9
+apply (blast intro: Invoke_correct)
+prefer 9
+apply (blast intro: Return_correct)
+apply (unfold wt_jvm_prog_def)
+apply (fast intro: Load_correct Store_correct Bipush_correct Aconst_null_correct 
+       Checkcast_correct Getfield_correct Putfield_correct New_correct 
+       Goto_correct Ifcmpeq_correct Pop_correct Dup_correct 
+       Dup_x1_correct Dup_x2_correct Swap_correct IAdd_correct)+
+.
+
+
+(** Main **)
+
+lemma correct_state_impl_Some_method:
+  "G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd> 
+  \<Longrightarrow> \<exists>meth. method (G,C) sig = Some(C,meth)"
+by (auto simp add: correct_state_def Let_def)
+
+
+lemma BV_correct_1 [rulify]:
+"\<And>state. \<lbrakk> wt_jvm_prog G phi; G,phi \<turnstile>JVM state\<surd>\<rbrakk> 
+ \<Longrightarrow> exec (G,state) = Some state' \<longrightarrow> G,phi \<turnstile>JVM state'\<surd>";
+apply (tactic "split_all_tac 1")
+apply (rename_tac xp hp frs)
+apply (case_tac xp)
+ apply (case_tac frs)
+  apply simp
+ apply (tactic "split_all_tac 1")
+ apply (tactic "hyp_subst_tac 1")
+ apply (frule correct_state_impl_Some_method)
+ apply (force intro: instr_correct)
+apply (case_tac frs)
+apply simp+
+.
+
+
+lemma L0:
+  "\<lbrakk> xp=None; frs\<noteq>[] \<rbrakk> \<Longrightarrow> (\<exists>state'. exec (G,xp,hp,frs) = Some state')"
+by (clarsimp simp add: neq_Nil_conv simp del: split_paired_Ex)
+
+lemma L1:
+  "\<lbrakk>wt_jvm_prog G phi; G,phi \<turnstile>JVM (xp,hp,frs)\<surd>; xp=None; frs\<noteq>[]\<rbrakk> 
+  \<Longrightarrow> \<exists>state'. exec(G,xp,hp,frs) = Some state' \<and> G,phi \<turnstile>JVM state'\<surd>"
+apply (drule L0)
+apply assumption
+apply (fast intro: BV_correct_1)
+.
+
+
+theorem BV_correct [rulify]:
+"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s -jvm\<rightarrow> t \<rbrakk> \<Longrightarrow> G,phi \<turnstile>JVM s\<surd> \<longrightarrow> G,phi \<turnstile>JVM t\<surd>"
+apply (unfold exec_all_def)
+apply (erule rtrancl_induct)
+ apply simp
+apply (auto intro: BV_correct_1)
+.
+
+
+theorem BV_correct_initial:
+"\<lbrakk> wt_jvm_prog G phi; G \<turnstile> s0 -jvm\<rightarrow> (None,hp,(stk,loc,C,sig,pc)#frs); G,phi \<turnstile>JVM s0 \<surd>\<rbrakk> 
+ \<Longrightarrow>  approx_stk G hp stk (fst (the (((phi  C)  sig) ! pc))) \<and> approx_loc G hp loc (snd (the (((phi  C)  sig) ! pc)))"
+apply (drule BV_correct)
+apply assumption+
+apply (simp add: correct_state_def correct_frame_def split_def split: option.splits)
+.
+
+end
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -1,63 +1,106 @@
 (*  Title:      HOL/MicroJava/BV/Convert.thy
     ID:         $Id$
-    Author:     Cornelia Pusch
+    Author:     Cornelia Pusch and Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
+*)
 
-The supertype relation lifted to type options, type lists and state types.
-*)
+header "Lifted Type Relations"
 
 theory Convert = JVMExec:
 
+text "The supertype relation lifted to type err, type lists and state types."
+
+datatype 'a err = Err | Ok 'a
+
 types
- locvars_type = "ty option list"
+ locvars_type = "ty err list"
  opstack_type = "ty list"
  state_type   = "opstack_type \<times> locvars_type"
 
-constdefs
+
+consts
+  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
+primrec
+  "strict f Err    = Err"
+  "strict f (Ok x) = f x"
+
+consts
+  opt_map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a option \<Rightarrow> 'b option)"
+primrec
+  "opt_map f None     = None"
+  "opt_map f (Some x) = Some (f x)"
+
+consts
+  val :: "'a err \<Rightarrow> 'a"
+primrec
+  "val (Ok s) = s"
 
-  (* lifts a relation to option with None as top element *)
-  lift_top :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'a option \<Rightarrow> bool)"
+  
+constdefs
+  (* lifts a relation to err with Err as top element *)
+  lift_top :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> bool)"
   "lift_top P a' a \<equiv> case a of 
-                       None   \<Rightarrow> True
-                     | Some t \<Rightarrow> (case a' of None \<Rightarrow> False | Some t' \<Rightarrow> P t' t)"
+                       Err  \<Rightarrow> True
+                     | Ok t \<Rightarrow> (case a' of Err \<Rightarrow> False | Ok t' \<Rightarrow> P t' t)"
+
+  (* lifts a relation to option with None as bottom element *)
+  lift_bottom :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'b option \<Rightarrow> bool)"
+  "lift_bottom P a' a \<equiv> case a' of 
+                          None    \<Rightarrow> True 
+                        | Some t' \<Rightarrow> (case a of None \<Rightarrow> False | Some t \<Rightarrow> P t' t)"
+
+  sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
+  "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+
+  sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
+             ("_ \<turnstile> _ <=l _"  [71,71] 70)
+  "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
+
+  sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"	  
+               ("_ \<turnstile> _ <=s _"  [71,71] 70)
+  "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+
+  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
+                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
+  "sup_state_opt G \<equiv> lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
 
 
- sup_ty_opt :: "['code prog,ty option,ty option] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
- "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+lemma not_Err_eq [iff]:
+  "(x \<noteq> Err) = (\<exists>a. x = Ok a)" 
+  by (cases x) auto
 
- sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"	  ("_ \<turnstile> _ <=l _"  [71,71] 70)
- "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
-
- sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"	  ("_ \<turnstile> _ <=s _"  [71,71] 70)
- "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Some (fst s) <=l map Some (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+lemma not_Some_eq [iff]:
+  "(\<forall>y. x \<noteq> Ok y) = (x = Err)"
+  by (cases x) auto  
 
 
 lemma lift_top_refl [simp]:
   "[| !!x. P x x |] ==> lift_top P x x"
-  by (simp add: lift_top_def split: option.splits)
+  by (simp add: lift_top_def split: err.splits)
 
 lemma lift_top_trans [trans]:
-  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] ==> lift_top P x z"
+  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] 
+  ==> lift_top P x z"
 proof -
   assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
   assume a: "lift_top P x y"
   assume b: "lift_top P y z"
 
-  { assume "z = None" 
+  { assume "z = Err" 
     hence ?thesis by (simp add: lift_top_def)
   } note z_none = this
 
-  { assume "x = None"
+  { assume "x = Err"
     with a b
     have ?thesis
-      by (simp add: lift_top_def split: option.splits)
+      by (simp add: lift_top_def split: err.splits)
   } note x_none = this
   
   { fix r t
-    assume x: "x = Some r" and z: "z = Some t"    
+    assume x: "x = Ok r" and z: "z = Ok t"    
     with a b
-    obtain s where y: "y = Some s" 
-      by (simp add: lift_top_def split: option.splits)
+    obtain s where y: "y = Ok s" 
+      by (simp add: lift_top_def split: err.splits)
     
     from a x y
     have "P r s" by (simp add: lift_top_def)
@@ -75,21 +118,82 @@
   show ?thesis by blast
 qed
 
-lemma lift_top_None_any [simp]:
-  "lift_top P None any = (any = None)"
-  by (simp add: lift_top_def split: option.splits)
+lemma lift_top_Err_any [simp]:
+  "lift_top P Err any = (any = Err)"
+  by (simp add: lift_top_def split: err.splits)
+
+lemma lift_top_Ok_Ok [simp]:
+  "lift_top P (Ok a) (Ok b) = P a b"
+  by (simp add: lift_top_def split: err.splits)
+
+lemma lift_top_any_Ok [simp]:
+  "lift_top P any (Ok b) = (\<exists>a. any = Ok a \<and> P a b)"
+  by (simp add: lift_top_def split: err.splits)
+
+lemma lift_top_Ok_any:
+  "lift_top P (Ok a) any = (any = Err \<or> (\<exists>b. any = Ok b \<and> P a b))"
+  by (simp add: lift_top_def split: err.splits)
 
-lemma lift_top_Some_Some [simp]:
-  "lift_top P (Some a) (Some b) = P a b"
-  by (simp add: lift_top_def split: option.splits)
+
+lemma lift_bottom_refl [simp]:
+  "[| !!x. P x x |] ==> lift_bottom P x x"
+  by (simp add: lift_bottom_def split: option.splits)
+
+lemma lift_bottom_trans [trans]:
+  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_bottom P x y; lift_bottom P y z |]
+  ==> lift_bottom P x z"
+proof -
+  assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
+  assume a: "lift_bottom P x y"
+  assume b: "lift_bottom P y z"
+
+  { assume "x = None" 
+    hence ?thesis by (simp add: lift_bottom_def)
+  } note z_none = this
 
-lemma lift_top_any_Some [simp]:
-  "lift_top P any (Some b) = (\<exists>a. any = Some a \<and> P a b)"
-  by (simp add: lift_top_def split: option.splits)
+  { assume "z = None"
+    with a b
+    have ?thesis
+      by (simp add: lift_bottom_def split: option.splits)
+  } note x_none = this
+  
+  { fix r t
+    assume x: "x = Some r" and z: "z = Some t"    
+    with a b
+    obtain s where y: "y = Some s" 
+      by (simp add: lift_bottom_def split: option.splits)
+    
+    from a x y
+    have "P r s" by (simp add: lift_bottom_def)
+    also
+    from b y z
+    have "P s t" by (simp add: lift_bottom_def)
+    finally 
+    have "P r t" .
 
-lemma lift_top_Some_any:
-  "lift_top P (Some a) any = (any = None \<or> (\<exists>b. any = Some b \<and> P a b))"
-  by (simp add: lift_top_def split: option.splits)
+    with x z
+    have ?thesis by (simp add: lift_bottom_def)
+  } 
+
+  with x_none z_none
+  show ?thesis by blast
+qed
+
+lemma lift_bottom_any_None [simp]:
+  "lift_bottom P any None = (any = None)"
+  by (simp add: lift_bottom_def split: option.splits)
+
+lemma lift_bottom_Some_Some [simp]:
+  "lift_bottom P (Some a) (Some b) = P a b"
+  by (simp add: lift_bottom_def split: option.splits)
+
+lemma lift_bottom_any_Some [simp]:
+  "lift_bottom P (Some a) any = (\<exists>b. any = Some b \<and> P a b)"
+  by (simp add: lift_bottom_def split: option.splits)
+
+lemma lift_bottom_Some_any:
+  "lift_bottom P any (Some b) = (any = None \<or> (\<exists>a. any = Some a \<and> P a b))"
+  by (simp add: lift_bottom_def split: option.splits)
 
 
 
@@ -105,18 +209,21 @@
   "G \<turnstile> s <=s s"
   by (simp add: sup_state_def)
 
+theorem sup_state_opt_refl [simp]:
+  "G \<turnstile> s <=' s"
+  by (simp add: sup_state_opt_def)
 
 
-theorem anyConvNone [simp]:
-  "(G \<turnstile> None <=o any) = (any = None)"
+theorem anyConvErr [simp]:
+  "(G \<turnstile> Err <=o any) = (any = Err)"
   by (simp add: sup_ty_opt_def)
 
-theorem SomeanyConvSome [simp]:
-  "(G \<turnstile> (Some ty') <=o (Some ty)) = (G \<turnstile> ty' \<preceq> ty)"
+theorem OkanyConvOk [simp]:
+  "(G \<turnstile> (Ok ty') <=o (Ok ty)) = (G \<turnstile> ty' \<preceq> ty)"
   by (simp add: sup_ty_opt_def)
 
-theorem sup_ty_opt_Some:
-  "G \<turnstile> a <=o (Some b) \<Longrightarrow> \<exists> x. a = Some x"
+theorem sup_ty_opt_Ok:
+  "G \<turnstile> a <=o (Ok b) \<Longrightarrow> \<exists> x. a = Ok x"
   by (clarsimp simp add: sup_ty_opt_def)
 
 lemma widen_PrimT_conv1 [simp]:
@@ -124,8 +231,8 @@
   by (auto elim: widen.elims)
 
 theorem sup_PTS_eq:
-  "(G \<turnstile> Some (PrimT p) <=o X) = (X=None \<or> X = Some (PrimT p))"
-  by (auto simp add: sup_ty_opt_def lift_top_Some_any)
+  "(G \<turnstile> Ok (PrimT p) <=o X) = (X=Err \<or> X = Ok (PrimT p))"
+  by (auto simp add: sup_ty_opt_def lift_top_Ok_any)
 
 
 
@@ -138,7 +245,7 @@
   by (simp add: sup_loc_def list_all2_Cons1)
 
 theorem sup_loc_Cons2:
-  "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))";
+  "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
   by (simp add: sup_loc_def list_all2_Cons2)
 
 
@@ -178,8 +285,8 @@
 
 
 theorem all_nth_sup_loc:
-  "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> (G \<turnstile> a <=l b)"
-  (is "?P a")
+  "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> 
+       (G \<turnstile> a <=l b)" (is "?P a")
 proof (induct a)
   show "?P []" by simp
 
@@ -206,12 +313,13 @@
 
 
 theorem sup_loc_append:
-  "[| length a = length b |] ==> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
+  "length a = length b ==> 
+   (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
 proof -
   assume l: "length a = length b"
 
-  have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
-    (is "?P a") 
+  have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
+            (G \<turnstile> x <=l y))" (is "?P a") 
   proof (induct a)
     show "?P []" by simp
     
@@ -219,7 +327,7 @@
     show "?P (l#ls)" 
     proof (intro strip)
       fix b
-      assume "length (l#ls) = length (b::ty option list)"
+      assume "length (l#ls) = length (b::ty err list)"
       with IH
       show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))"
         by - (cases b, auto)
@@ -276,8 +384,8 @@
 
 
 theorem sup_loc_update [rulify]:
-  "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> (G \<turnstile> x[n := a] <=l y[n := b])"
-  (is "?P x")
+  "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
+          (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
 proof (induct x)
   show "?P []" by simp
 
@@ -294,23 +402,28 @@
 
 
 theorem sup_state_length [simp]:
-  "G \<turnstile> s2 <=s s1 \<Longrightarrow> length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
+  "G \<turnstile> s2 <=s s1 ==> 
+   length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
   by (auto dest: sup_loc_length simp add: sup_state_def);
 
 theorem sup_state_append_snd:
-  "length a = length b \<Longrightarrow> (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
+  "length a = length b ==> 
+  (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
   by (auto simp add: sup_state_def sup_loc_append)
 
 theorem sup_state_append_fst:
-  "length a = length b \<Longrightarrow> (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
+  "length a = length b ==> 
+  (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
   by (auto simp add: sup_state_def sup_loc_append)
 
 theorem sup_state_Cons1:
-  "(G \<turnstile> (x#xt, a) <=s (yt, b)) = (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
+  "(G \<turnstile> (x#xt, a) <=s (yt, b)) = 
+   (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
   by (auto simp add: sup_state_def map_eq_Cons)
 
 theorem sup_state_Cons2:
-  "(G \<turnstile> (xt, a) <=s (y#yt, b)) = (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
+  "(G \<turnstile> (xt, a) <=s (y#yt, b)) = 
+   (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
   by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2)
 
 theorem sup_state_ignore_fst:  
@@ -324,11 +437,32 @@
   show ?thesis by (simp add: m sup_state_def)
 qed
   
+
+lemma sup_state_opt_None_any [iff]:
+  "(G \<turnstile> None <=' any) = True"
+  by (simp add: sup_state_opt_def lift_bottom_def)
+
+lemma sup_state_opt_any_None [iff]:
+  "(G \<turnstile> any <=' None) = (any = None)"
+  by (simp add: sup_state_opt_def)
+
+lemma sup_state_opt_Some_Some [iff]:
+  "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)"
+  by (simp add: sup_state_opt_def del: split_paired_Ex)
+
+lemma sup_state_opt_any_Some [iff]:
+  "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)"
+  by (simp add: sup_state_opt_def)
+
+lemma sup_state_opt_Some_any:
+  "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))"
+  by (simp add: sup_state_opt_def lift_bottom_Some_any)
+
+
 theorem sup_ty_opt_trans [trans]:
   "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
   by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def)
 
-
 theorem sup_loc_trans [trans]:
   "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
 proof -
@@ -359,4 +493,9 @@
   "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
   by (auto intro: sup_loc_trans simp add: sup_state_def)
 
+theorem sup_state_opt_trans [trans]:
+  "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
+  by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def)
+
+
 end
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/Correct.ML
--- a/src/HOL/MicroJava/BV/Correct.ML	Wed Aug 30 21:44:12 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,263 +0,0 @@
-(*  Title:      HOL/MicroJava/BV/Correct.ML
-    ID:         $Id$
-    Author:     Cornelia Pusch
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-(** sup_heap **)
-
-Goalw [hext_def]
- "hp x = None \\<longrightarrow> hp \\<le>| (hp((newref hp) \\<mapsto> obj))";
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (Clarify_tac 1);
-bd newref_None 1;
-back();
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-qed_spec_mp "sup_heap_newref";
-
-
-Goalw [hext_def]
-"hp a = Some (C,od') \\<longrightarrow> hp \\<le>| (hp(a \\<mapsto> (C,od)))";
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-qed_spec_mp "sup_heap_update_value";
-
-
-(** approx_val **)
-
-Goalw [approx_val_def]
-"approx_val G hp x None";
-by (Asm_full_simp_tac 1);
-qed_spec_mp "approx_val_None";
-
-
-Goalw [approx_val_def]
-"approx_val G hp Null (Some(RefT x))";
-by(Simp_tac 1);
-by (fast_tac (claset() addIs widen.intrs) 1);
-qed_spec_mp "approx_val_Null";
-
-
-Goal
-"\\<lbrakk> wf_prog wt G \\<rbrakk> \
-\\\<Longrightarrow> approx_val G hp v (Some T) \\<longrightarrow> G\\<turnstile> T\\<preceq>T' \\<longrightarrow> approx_val G hp v (Some T')";
-by (case_tac "T" 1);
- by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
-by (fast_tac (claset() addIs [conf_widen] addss (simpset()addsimps[approx_val_def])) 1);
-qed_spec_mp "approx_val_imp_approx_val_assConvertible";
-
-
-Goal
-"approx_val G hp val at \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_val G hp' val at";
-by (asm_full_simp_tac (simpset() setloop (split_tac [option.split]) 
-	addsimps [approx_val_def]) 1);
-by(blast_tac (claset() addIs [conf_hext]) 1);
-qed_spec_mp "approx_val_imp_approx_val_sup_heap";
-
-Goal
-"\\<lbrakk> hp a = Some obj' ; G,hp\\<turnstile> v\\<Colon>\\<preceq>T ; obj_ty obj = obj_ty obj' \\<rbrakk> \
-\\\<Longrightarrow>G,(hp(a\\<mapsto>obj))\\<turnstile> v\\<Colon>\\<preceq>T";
-by (case_tac "v" 1);
-by (auto_tac (claset() , simpset() addsimps [obj_ty_def,conf_def] addsplits [option.split]));
-qed_spec_mp "approx_val_imp_approx_val_heap_update";
-
-
-Goal
-"wf_prog wt G \\<Longrightarrow> approx_val G h val us \\<longrightarrow> G \\<turnstile> us <=o us' \\<longrightarrow> approx_val G h val us'";
-by (asm_simp_tac (simpset() addsimps [thm "sup_PTS_eq",approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
-by(blast_tac (claset() addIs [conf_widen]) 1);
-qed_spec_mp "approx_val_imp_approx_val_sup";
-
-
-Goalw [approx_loc_def,list_all2_def]
-"\\<lbrakk> wf_prog wt G; approx_loc G hp loc LT; idx < length LT ; val = loc ! idx ; G \\<turnstile> LT ! idx <=o at\\<rbrakk> \
-\\\<Longrightarrow> approx_val G hp val at";
-by (fast_tac (claset() addIs [approx_val_imp_approx_val_sup] addss (simpset() addsimps 
-	[split_def,all_set_conv_all_nth])) 1);
-qed "approx_loc_imp_approx_val_sup";
-
-
-(** approx_loc **)
-
-Goalw [approx_loc_def]
-"approx_loc G hp (s#xs) (l#ls) = \
-\   (approx_val G hp s l \\<and> approx_loc G hp xs ls)";
-by (Simp_tac 1);
-qed "approx_loc_Cons";
-AddIffs [approx_loc_Cons];
-
-
-Goalw [approx_stk_def,approx_loc_def,list_all2_def]
-"\\<lbrakk> wf_prog wt G \\<rbrakk> \
-\\\<Longrightarrow> (\\<forall>tt'\\<in>set (zip tys_n ts). tt' \\<in> widen G) \\<longrightarrow> \
-\     length tys_n = length ts \\<longrightarrow> approx_stk G hp s tys_n \\<longrightarrow> approx_loc G hp s (map Some ts)";
-by (force_tac (claset() addIs [approx_val_imp_approx_val_assConvertible], simpset() 
-	addsimps [all_set_conv_all_nth,split_def]) 1);
-qed_spec_mp "assConv_approx_stk_imp_approx_loc";
-
-
-Goalw [approx_loc_def,list_all2_def]
-"\\<forall> lvars. approx_loc G hp lvars lt \\<longrightarrow>  hp \\<le>| hp' \\<longrightarrow> approx_loc G hp' lvars lt";
-by (case_tac "lt" 1);
- by (Asm_simp_tac 1);
-by (force_tac (claset() addIs [approx_val_imp_approx_val_sup_heap],
-	       simpset() addsimps [neq_Nil_conv]) 1);
-qed_spec_mp "approx_loc_imp_approx_loc_sup_heap";
-
-
-Goalw [thm "sup_loc_def",approx_loc_def,list_all2_def]
-"wf_prog wt G \\<Longrightarrow> approx_loc G hp lvars lt \\<longrightarrow> G \\<turnstile> lt <=l lt' \\<longrightarrow> approx_loc G hp lvars lt'";
-by (auto_tac (claset() , simpset() addsimps [all_set_conv_all_nth,split_def]));
-by (auto_tac (claset() addEs [approx_val_imp_approx_val_sup] , simpset()));
-qed_spec_mp "approx_loc_imp_approx_loc_sup";
-
-
-Goalw [approx_loc_def,list_all2_def]
-"\\<forall>loc idx x X. (approx_loc G hp loc LT) \\<longrightarrow> (approx_val G hp x X) \
-\ \\<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))";
-by (fast_tac (claset() addDs [set_update_subset_insert RS subsetD]
-              addss (simpset() addsimps [zip_update])) 1);
-qed_spec_mp "approx_loc_imp_approx_loc_subst";
-
-
-Goalw [approx_loc_def,list_all2_def]
-"\\<forall>L1 l2 L2. length l1=length L1 \
-\ \\<longrightarrow> approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \\<and> approx_loc G hp l2 L2)";
-by(simp_tac (simpset() addcongs [conj_cong] addsimps [zip_append]) 1);
-by(Blast_tac 1);
-qed_spec_mp "approx_loc_append";
-
-
-(** approx_stk **)
-
-Goalw [approx_stk_def,approx_loc_def,list_all2_def]
-"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t";
-by (fast_tac (claset() addss (simpset() addsimps [zip_rev,rev_map RS sym])) 1);
-qed_spec_mp "approx_stk_rev_lem";
-
-Goal 
-"approx_stk G hp (rev s) t = approx_stk G hp s (rev t)";
-by (fast_tac (claset() addIs [approx_stk_rev_lem RS subst] addss (simpset()))  1);
-qed_spec_mp "approx_stk_rev";
-
-Goalw [approx_stk_def]
-"\\<forall> lvars. approx_stk G hp lvars lt \\<longrightarrow> hp \\<le>| hp' \\<longrightarrow> approx_stk G hp' lvars lt";
-by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup_heap])  1);
-qed_spec_mp "approx_stk_imp_approx_stk_sup_heap";
-
-
-Goalw [approx_stk_def]
-"wf_prog wt G \\<Longrightarrow> approx_stk G hp lvars st \\<longrightarrow> G \\<turnstile> (map Some st) <=l (map Some st') \\<longrightarrow> approx_stk G hp lvars st'";
-by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup])  1);
-qed_spec_mp "approx_stk_imp_approx_stk_sup";
-
-Goalw [approx_stk_def,approx_loc_def]
-"approx_stk G hp [] []";
-by (Simp_tac 1);
-qed "approx_stk_Nil";
-AddIffs [approx_stk_Nil];
-
-Goalw [approx_stk_def,approx_loc_def]
-"approx_stk G hp (x # stk) (S#ST) = (approx_val G hp x (Some S) \\<and> approx_stk G hp stk ST)";
-by (Simp_tac 1);
-qed "approx_stk_Cons";
-AddIffs [approx_stk_Cons];
-
-Goalw [approx_stk_def,approx_loc_def]
-"approx_stk G hp stk (S#ST') = \
-\ (\\<exists>s stk'. stk = s#stk' \\<and> approx_val G hp s (Some S) \\<and> approx_stk G hp stk' ST')";
-by (asm_full_simp_tac (simpset() addsimps [list_all2_Cons2]) 1);
-qed "approx_stk_Cons_lemma";
-AddIffs [approx_stk_Cons_lemma];
-
-
-Goalw [approx_stk_def,approx_loc_def]
-"approx_stk G hp stk (S@ST')  \
-\ \\<Longrightarrow> (\\<exists>s stk'. stk = s@stk' \\<and> length s = length S \\<and> length stk' = length ST' \\<and> \
-\             approx_stk G hp s S \\<and> approx_stk G hp stk' ST')";
-by(asm_full_simp_tac (simpset() addsimps [list_all2_append2]) 1);
-qed_spec_mp "approx_stk_append_lemma";
-
-
-(** oconf **)
-
-Goalw [oconf_def,lconf_def]
-"\\<lbrakk> is_class G C; wf_prog wt G \\<rbrakk> \\<Longrightarrow> \
-\G,h\\<turnstile> (C, map_of (map (\\<lambda>(f,fT).(f,default_val fT)) (fields(G,C))))\\<surd>";
-by (asm_full_simp_tac (simpset() addsimps [map_of_map]) 1);
-by (force_tac (claset() addIs [defval_conf]
-                        addDs [map_of_SomeD,is_type_fields],simpset()) 1);
-qed "correct_init_obj";
-
-
-Goalw [oconf_def,lconf_def]
-"\\<lbrakk> map_of (fields (G, oT)) FD = Some T ; G,hp\\<turnstile>v\\<Colon>\\<preceq>T ; \
-\   G,hp\\<turnstile>(oT,fs)\\<surd> \\<rbrakk>  \
-\\\<Longrightarrow> G,hp\\<turnstile>(oT, fs(FD\\<mapsto>v))\\<surd>";
-by (asm_full_simp_tac (simpset() addsplits [ty.split]) 1);
-qed_spec_mp "oconf_imp_oconf_field_update";
-
-
-Goalw [oconf_def,lconf_def]
-"hp x = None \\<longrightarrow> G,hp\\<turnstile>obj\\<surd>  \\<longrightarrow>  G,hp\\<turnstile>obj'\\<surd> \
-\  \\<longrightarrow> G,(hp(newref hp\\<mapsto>obj'))\\<turnstile>obj\\<surd>";
-by (Asm_full_simp_tac 1);
-by (fast_tac (claset() addIs [conf_hext,sup_heap_newref]) 1);
-qed_spec_mp "oconf_imp_oconf_heap_newref";
-
-Goalw [oconf_def,lconf_def]
-"hp a = Some obj'  \\<longrightarrow> obj_ty obj' = obj_ty obj'' \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \
-\  \\<longrightarrow> G,hp(a\\<mapsto>obj'')\\<turnstile>obj\\<surd>";
-by (Asm_full_simp_tac 1);
-by (fast_tac (claset() addIs [approx_val_imp_approx_val_heap_update] addss (simpset())) 1);
-qed_spec_mp "oconf_imp_oconf_heap_update";
-
-
-(** hconf **)
-
-
-Goal "hp x = None \\<longrightarrow> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G,hp\\<turnstile>obj\\<surd> \\<longrightarrow> G\\<turnstile>h hp(newref hp\\<mapsto>obj)\\<surd>";
-by (asm_full_simp_tac (simpset() addsplits [split_split] 
-				 addsimps [hconf_def]) 1);
- by (fast_tac (claset()addIs[oconf_imp_oconf_heap_newref] addss (simpset())) 1);
-qed_spec_mp "hconf_imp_hconf_newref";
-
-
-Goal "map_of (fields (G, oT)) (F, D) = Some T \\<and> hp oloc = Some(oT,fs) \\<and> \
-\ G,hp\\<turnstile>v\\<Colon>\\<preceq>T \\<and> G\\<turnstile>h hp\\<surd> \\<longrightarrow> G\\<turnstile>h hp(oloc \\<mapsto> (oT, fs((F,D)\\<mapsto>v)))\\<surd>";
-by (asm_full_simp_tac (simpset() addsimps [hconf_def]) 1);
-by (fast_tac (claset() addIs 
-        [oconf_imp_oconf_heap_update, oconf_imp_oconf_field_update]
-        addss (simpset() addsimps [obj_ty_def])) 1);
-qed_spec_mp "hconf_imp_hconf_field_update";
-
-
-(** correct_frames **)
-
-Delsimps [fun_upd_apply]; 
-Goal
-"\\<forall>rT C sig. correct_frames G hp phi rT sig frs \\<longrightarrow> \
-\    hp a = Some (C,od) \\<longrightarrow> map_of (fields (G, C)) fl = Some fd \\<longrightarrow> \
-\    G,hp\\<turnstile>v\\<Colon>\\<preceq>fd \
-\ \\<longrightarrow> correct_frames G (hp(a \\<mapsto> (C, od(fl\\<mapsto>v)))) phi rT sig frs";
-by (induct_tac "frs" 1);
- by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
-				approx_loc_imp_approx_loc_sup_heap,
-				sup_heap_update_value] addss (simpset())) 1);
-qed_spec_mp "correct_frames_imp_correct_frames_field_update";
-
-
-Goal
-"\\<forall>rT C sig. hp x = None \\<longrightarrow> correct_frames G hp phi rT sig frs \\<and> \
-\    oconf G hp obj \
-\ \\<longrightarrow> correct_frames G (hp(newref hp \\<mapsto> obj)) phi rT sig frs";
-by (induct_tac "frs" 1);
-by  (asm_full_simp_tac (simpset() addsimps []) 1);
-by (asm_full_simp_tac (simpset() addsimps [split_def,correct_frame_def]) 1);
-by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup_heap,
-				approx_loc_imp_approx_loc_sup_heap,
-				hconf_imp_hconf_newref,
-				sup_heap_newref] addss (simpset())) 1);
-qed_spec_mp "correct_frames_imp_correct_frames_newref";
-
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -6,60 +6,319 @@
 The invariant for the type safety proof.
 *)
 
-Correct = BVSpec + 
+header "Type Safety Invariant"
+
+theory Correct = BVSpec:
 
 constdefs
- approx_val :: "[jvm_prog,aheap,val,ty option] \\<Rightarrow> bool"
-"approx_val G h v any \\<equiv> case any of None \\<Rightarrow> True | Some T \\<Rightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T"
+ approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
+"approx_val G h v any \<equiv> case any of Err \<Rightarrow> True | Ok T \<Rightarrow> G,h\<turnstile>v\<Colon>\<preceq>T"
 
- approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \\<Rightarrow> bool"
-"approx_loc G hp loc LT \\<equiv> list_all2 (approx_val G hp) loc LT" 
+ approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
+"approx_loc G hp loc LT \<equiv> list_all2 (approx_val G hp) loc LT"
+
+ approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
+"approx_stk G hp stk ST \<equiv> approx_loc G hp stk (map Ok ST)"
 
- approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \\<Rightarrow> bool"
-"approx_stk G hp stk ST \\<equiv> approx_loc G hp stk (map Some ST)"
+ correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
+"correct_frame G hp \<equiv> \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
+   approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
+   pc < length ins \<and> length loc=length(snd sig)+maxl+1"
 
- correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \\<Rightarrow> frame \\<Rightarrow> bool"
-"correct_frame G hp \\<equiv> \\<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
-   approx_stk G hp stk ST  \\<and> approx_loc G hp loc LT \\<and> 
-   pc < length ins \\<and> length loc=length(snd sig)+maxl+1"
+ correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
+"correct_frame_opt G hp s \<equiv> case s of None \<Rightarrow> \<lambda>maxl ins f. False | Some t \<Rightarrow> correct_frame G hp t"
+
 
 consts
- correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \\<Rightarrow> bool"
+ correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
 primrec
 "correct_frames G hp phi rT0 sig0 [] = True"
 
 "correct_frames G hp phi rT0 sig0 (f#frs) =
-	(let (stk,loc,C,sig,pc) = f;
-	     (ST,LT) = (phi C sig) ! pc
-	 in
-         (\\<exists>rT maxl ins.
-         method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and>
-	(\\<exists>C' mn pTs k. pc = k+1 \\<and> ins!k = (Invoke C' mn pTs) \\<and>
-         (mn,pTs) = sig0 \\<and> 
-         (\\<exists>apTs D ST'.
-         fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>
-         length apTs = length pTs \\<and>
-         (\\<exists>D' rT' maxl' ins'.
-           method (G,D) sig0 = Some(D',rT',(maxl',ins')) \\<and>
-           G \\<turnstile> rT0 \\<preceq> rT') \\<and>
-	 correct_frame G hp (tl ST, LT) maxl ins f \\<and> 
+	(let (stk,loc,C,sig,pc) = f in
+  (\<exists>ST LT rT maxl ins.
+    phi C sig ! pc = Some (ST,LT) \<and> 
+    method (G,C) sig = Some(C,rT,(maxl,ins)) \<and>
+	(\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and>
+         (mn,pTs) = sig0 \<and> 
+         (\<exists>apTs D ST' LT'.
+         (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
+         length apTs = length pTs \<and>
+         (\<exists>D' rT' maxl' ins'.
+           method (G,D) sig0 = Some(D',rT',(maxl',ins')) \<and>
+           G \<turnstile> rT0 \<preceq> rT') \<and>
+	 correct_frame G hp (tl ST, LT) maxl ins f \<and> 
 	 correct_frames G hp phi rT sig frs))))"
 
 
 constdefs
- correct_state :: "[jvm_prog,prog_type,jvm_state] \\<Rightarrow> bool"
-                  ("_,_\\<turnstile>JVM _\\<surd>"  [51,51] 50)
-"correct_state G phi \\<equiv> \\<lambda>(xp,hp,frs).
+ correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
+                  ("_,_\<turnstile>JVM _\<surd>"  [51,51] 50)
+"correct_state G phi \<equiv> \<lambda>(xp,hp,frs).
    case xp of
-     None \\<Rightarrow> (case frs of
-	           [] \\<Rightarrow> True
-             | (f#fs) \\<Rightarrow> G\\<turnstile>h hp\\<surd> \\<and>
+     None \<Rightarrow> (case frs of
+	           [] \<Rightarrow> True
+             | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and>
 			(let (stk,loc,C,sig,pc) = f
 		         in
-                         \\<exists>rT maxl ins.
-                         method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and>
-			 correct_frame G hp ((phi C sig) ! pc) maxl ins f \\<and> 
+                         \<exists>rT maxl ins s.
+                         method (G,C) sig = Some(C,rT,(maxl,ins)) \<and>
+                         phi C sig ! pc = Some s \<and>
+			 correct_frame G hp s maxl ins f \<and> 
 		         correct_frames G hp phi rT sig fs))
-   | Some x \\<Rightarrow> True" 
+   | Some x \<Rightarrow> True" 
+
+
+lemma sup_heap_newref:
+  "hp x = None \<Longrightarrow> hp \<le>| hp(newref hp \<mapsto> obj)"
+apply (unfold hext_def)
+apply clarsimp
+apply (drule newref_None 1) back
+apply simp
+.
+
+lemma sup_heap_update_value:
+  "hp a = Some (C,od') \<Longrightarrow> hp \<le>| hp (a \<mapsto> (C,od))"
+by (simp add: hext_def)
+
+
+(** approx_val **)
+
+lemma approx_val_Err:
+  "approx_val G hp x Err"
+by (simp add: approx_val_def)
+
+lemma approx_val_Null:
+  "approx_val G hp Null (Ok (RefT x))"
+by (auto intro: null simp add: approx_val_def)
+
+lemma approx_val_imp_approx_val_assConvertible [rulify]: 
+  "wf_prog wt G \<Longrightarrow> approx_val G hp v (Ok T) \<longrightarrow> G\<turnstile> T\<preceq>T' \<longrightarrow> approx_val G hp v (Ok T')"
+by (cases T) (auto intro: conf_widen simp add: approx_val_def)
+
+lemma approx_val_imp_approx_val_sup_heap [rulify]:
+  "approx_val G hp v at \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_val G hp' v at"
+apply (simp add: approx_val_def split: err.split)
+apply (blast intro: conf_hext)
+.
+
+lemma approx_val_imp_approx_val_heap_update:
+  "\<lbrakk>hp a = Some obj'; G,hp\<turnstile> v\<Colon>\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
+  \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v\<Colon>\<preceq>T"
+by (cases v, auto simp add: obj_ty_def conf_def)
+
+lemma approx_val_imp_approx_val_sup [rulify]:
+  "wf_prog wt G \<Longrightarrow> (approx_val G h v us) \<longrightarrow> (G \<turnstile> us <=o us') \<longrightarrow> (approx_val G h v us')"
+apply (simp add: sup_PTS_eq approx_val_def split: err.split)
+apply (blast intro: conf_widen)
+.
+
+lemma approx_loc_imp_approx_val_sup:
+  "\<lbrakk>wf_prog wt G; approx_loc G hp loc LT; idx < length LT; v = loc!idx; G \<turnstile> LT!idx <=o at\<rbrakk>
+  \<Longrightarrow> approx_val G hp v at"
+apply (unfold approx_loc_def)
+apply (unfold list_all2_def)
+apply (auto intro: approx_val_imp_approx_val_sup simp add: split_def all_set_conv_all_nth)
+.
+
+
+(** approx_loc **)
+
+lemma approx_loc_Cons [iff]:
+  "approx_loc G hp (s#xs) (l#ls) = (approx_val G hp s l \<and> approx_loc G hp xs ls)"
+by (simp add: approx_loc_def)
+
+lemma assConv_approx_stk_imp_approx_loc [rulify]:
+  "wf_prog wt G \<Longrightarrow> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
+  \<longrightarrow> length tys_n = length ts \<longrightarrow> approx_stk G hp s tys_n \<longrightarrow> 
+  approx_loc G hp s (map Ok ts)"
+apply (unfold approx_stk_def approx_loc_def list_all2_def)
+apply (clarsimp simp add: all_set_conv_all_nth)
+apply (rule approx_val_imp_approx_val_assConvertible)
+apply auto
+.
+
+
+lemma approx_loc_imp_approx_loc_sup_heap [rulify]:
+  "\<forall>lvars. approx_loc G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_loc G hp' lvars lt"
+apply (unfold approx_loc_def list_all2_def)
+apply (cases lt)
+ apply simp
+apply clarsimp
+apply (rule approx_val_imp_approx_val_sup_heap)
+apply auto
+.
+
+lemma approx_loc_imp_approx_loc_sup [rulify]:
+  "wf_prog wt G \<Longrightarrow> approx_loc G hp lvars lt \<longrightarrow> G \<turnstile> lt <=l lt' \<longrightarrow> approx_loc G hp lvars lt'"
+apply (unfold sup_loc_def approx_loc_def list_all2_def)
+apply (auto simp add: all_set_conv_all_nth)
+apply (auto elim: approx_val_imp_approx_val_sup)
+.
+
+
+lemma approx_loc_imp_approx_loc_subst [rulify]:
+  "\<forall>loc idx x X. (approx_loc G hp loc LT) \<longrightarrow> (approx_val G hp x X) 
+  \<longrightarrow> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))"
+apply (unfold approx_loc_def list_all2_def)
+apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
+.
+
+
+lemmas [cong] = conj_cong 
+
+lemma approx_loc_append [rulify]:
+  "\<forall>L1 l2 L2. length l1=length L1 \<longrightarrow> 
+  approx_loc G hp (l1@l2) (L1@L2) = (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
+apply (unfold approx_loc_def list_all2_def)
+apply simp
+apply blast
+.
+
+lemmas [cong del] = conj_cong
+
+
+(** approx_stk **)
+
+lemma approx_stk_rev_lem:
+  "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
+apply (unfold approx_stk_def approx_loc_def list_all2_def)
+apply (auto simp add: zip_rev sym [OF rev_map])
+.
+
+lemma approx_stk_rev:
+  "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
+by (auto intro: subst [OF approx_stk_rev_lem])
+
+
+lemma approx_stk_imp_approx_stk_sup_heap [rulify]:
+  "\<forall>lvars. approx_stk G hp lvars lt \<longrightarrow> hp \<le>| hp' \<longrightarrow> approx_stk G hp' lvars lt"
+by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
+
+lemma approx_stk_imp_approx_stk_sup [rulify]:
+  "wf_prog wt G \<Longrightarrow> approx_stk G hp lvars st \<longrightarrow> (G \<turnstile> map Ok st <=l (map Ok st')) 
+  \<longrightarrow> approx_stk G hp lvars st'" 
+by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
+
+lemma approx_stk_Nil [iff]:
+  "approx_stk G hp [] []"
+by (simp add: approx_stk_def approx_loc_def)
+
+lemma approx_stk_Cons [iff]:
+  "approx_stk G hp (x # stk) (S#ST) = 
+   (approx_val G hp x (Ok S) \<and> approx_stk G hp stk ST)"
+by (simp add: approx_stk_def approx_loc_def)
+
+lemma approx_stk_Cons_lemma [iff]:
+  "approx_stk G hp stk (S#ST') = 
+  (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (Ok S) \<and> approx_stk G hp stk' ST')"
+by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
+
+lemma approx_stk_append_lemma:
+  "approx_stk G hp stk (S@ST') \<Longrightarrow>
+   (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and> 
+             approx_stk G hp s S \<and> approx_stk G hp stk' ST')"
+by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
+
+
+(** oconf **)
+
+lemma correct_init_obj:
+  "\<lbrakk>is_class G C; wf_prog wt G\<rbrakk> \<Longrightarrow> 
+  G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>"
+apply (unfold oconf_def lconf_def)
+apply (simp add: map_of_map)
+apply (force intro: defval_conf dest: map_of_SomeD is_type_fields)
+.
+
+
+lemma oconf_imp_oconf_field_update [rulify]:
+  "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v\<Colon>\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
+  \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
+by (simp add: oconf_def lconf_def)
+
+
+lemma oconf_imp_oconf_heap_newref [rulify]:
+"hp x = None \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G,hp\<turnstile>obj'\<surd> \<longrightarrow> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>"
+apply (unfold oconf_def lconf_def)
+apply simp
+apply (fast intro: conf_hext sup_heap_newref)
+.
+
+
+lemma oconf_imp_oconf_heap_update [rulify]:
+  "hp a = Some obj' \<longrightarrow> obj_ty obj' = obj_ty obj'' \<longrightarrow> G,hp\<turnstile>obj\<surd> 
+  \<longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
+apply (unfold oconf_def lconf_def)
+apply simp
+apply (force intro: approx_val_imp_approx_val_heap_update)
+.
+
+
+(** hconf **)
+
+
+lemma hconf_imp_hconf_newref [rulify]:
+  "hp x = None \<longrightarrow> G\<turnstile>h hp\<surd> \<longrightarrow> G,hp\<turnstile>obj\<surd> \<longrightarrow> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>"
+apply (simp add: hconf_def)
+apply (fast intro: oconf_imp_oconf_heap_newref)
+.
+
+lemma hconf_imp_hconf_field_update [rulify]:
+  "map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> 
+  G,hp\<turnstile>v\<Colon>\<preceq>T \<and> G\<turnstile>h hp\<surd> \<longrightarrow> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>"
+apply (simp add: hconf_def)
+apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update 
+             simp add: obj_ty_def)
+.
+
+(** correct_frames **)
+
+lemmas [simp del] = fun_upd_apply
+
+lemma correct_frames_imp_correct_frames_field_update [rulify]:
+  "\<forall>rT C sig. correct_frames G hp phi rT sig frs \<longrightarrow> 
+  hp a = Some (C,od) \<longrightarrow> map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
+  G,hp\<turnstile>v\<Colon>\<preceq>fd 
+  \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs";
+apply (induct frs)
+ apply simp
+apply (clarsimp simp add: correct_frame_def) (*takes long*)
+apply (intro exI conjI)
+     apply simp
+    apply simp
+   apply force
+  apply simp
+ apply (rule approx_stk_imp_approx_stk_sup_heap)
+  apply simp
+ apply (rule sup_heap_update_value)
+ apply simp
+apply (rule approx_loc_imp_approx_loc_sup_heap)
+ apply simp
+apply (rule sup_heap_update_value)
+apply simp
+.
+
+lemma correct_frames_imp_correct_frames_newref [rulify]:
+  "\<forall>rT C sig. hp x = None \<longrightarrow> correct_frames G hp phi rT sig frs \<and> oconf G hp obj 
+  \<longrightarrow> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs"
+apply (induct frs)
+ apply simp
+apply (clarsimp simp add: correct_frame_def)
+apply (intro exI conjI)
+     apply simp
+    apply simp
+   apply force
+  apply simp
+ apply (rule approx_stk_imp_approx_stk_sup_heap)
+  apply simp
+ apply (rule sup_heap_newref)
+ apply simp
+apply (rule approx_loc_imp_approx_loc_sup_heap)
+ apply simp
+apply (rule sup_heap_newref)
+apply simp
+.
 
 end
+
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -8,244 +8,119 @@
 
 theory LBVComplete = BVSpec + LBVSpec + StepMono:
 
-
 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)))"
-  
-  contains_dead :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
-  "contains_dead ins cert phi pc \<equiv>
-     Suc pc \<notin> succs (ins!pc) pc \<and> Suc pc < length phi \<longrightarrow>
-     cert ! (Suc pc) = Some (phi ! Suc pc)"
-
   contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool"
-  "contains_targets ins cert phi pc \<equiv> (
-     \<forall> pc' \<in> succs (ins!pc) pc. pc' \<noteq> Suc pc \<and> pc' < length phi \<longrightarrow> 
-     cert!pc' = Some (phi!pc'))" 
-
+  "contains_targets ins cert phi pc \<equiv> 
+     \<forall>pc' \<in> set (succs (ins!pc) pc). 
+      pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = 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)"
+  "fits ins cert phi \<equiv> \<forall>pc. pc < length ins \<longrightarrow> 
+                       contains_targets ins cert phi pc \<and>
+                       (cert!pc = None \<or> cert!pc = phi!pc)"
 
   is_target :: "[instr list, p_count] \<Rightarrow> bool" 
-  "is_target ins pc \<equiv> \<exists> pc'. pc' < length ins \<and> pc \<in> succs (ins!pc') pc'"
-
-  maybe_dead :: "[instr list, p_count] \<Rightarrow> bool"
-  "maybe_dead ins pc \<equiv> \<exists> pc'. pc = pc'+1 \<and> pc \<notin> succs (ins!pc') pc'"
-
-  mdot :: "[instr list, p_count] \<Rightarrow> bool"
-  "mdot ins pc \<equiv> maybe_dead ins pc \<or> is_target ins pc"
+  "is_target ins pc \<equiv> 
+     \<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')"
 
 
-consts
-  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))"  
-  
 constdefs 
-  option_filter :: "['a list, nat \<Rightarrow> bool] \<Rightarrow> 'a option list" 
-  "option_filter l P \<equiv> option_filter_n l P 0" 
-  
   make_cert :: "[instr list, method_type] \<Rightarrow> certificate"
-  "make_cert ins phi \<equiv> option_filter phi (mdot ins)"
-  
+  "make_cert ins phi \<equiv> 
+     map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]"
+
   make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate"
   "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)"
+     let (C,x,y,mdecls)  = \<epsilon> (Cl,x,y,mdecls). (Cl,x,y,mdecls) \<in> set G \<and> Cl = C;
+         (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)"
   
 
 lemmas [simp del] = split_paired_Ex
 
-lemma length_ofn [rulify]: "\<forall>n. length (option_filter_n l P n) = length l"
-  by (induct l) auto
-
+lemma make_cert_target:
+  "[| pc < length ins; is_target ins pc |] ==> make_cert ins phi ! pc = phi!pc"
+  by (simp add: make_cert_def)
 
-lemma is_approx_option_filter: "is_approx (option_filter l P) l" 
-proof -
-  {
-    fix a n
-    have "\<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
-  }
-  
-  thus ?thesis    
-    by (auto simp add: option_filter_def)
-qed
+lemma make_cert_approx:
+  "[| pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc |] ==> 
+   make_cert ins phi ! pc = None"
+  by (auto simp add: make_cert_def)
 
-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 (unfold contains_targets_def, clarsimp)
+lemma make_cert_contains_targets:
+  "pc < length ins ==> contains_targets ins (make_cert ins phi) phi pc"
+proof (unfold contains_targets_def, intro strip, elim conjE)
  
   fix pc'
   assume "pc < length ins" 
-         "pc' \<in> succs (ins ! pc) pc" 
-         "pc' \<noteq> Suc pc" and
-    pc': "pc' < length phi"
+         "pc' \<in> set (succs (ins ! pc) pc)" 
+         "pc' \<noteq> pc+1" and
+    pc': "pc' < length ins"
 
-  hence "is_target ins pc'" by (auto simp add: is_target_def)
+  hence "is_target ins pc'" 
+    by (auto simp add: is_target_def)
 
   with pc'
-  show "option_filter phi (mdot ins) ! pc' = Some (phi ! pc')"
-    by (auto intro: option_filter_Some simp add: mdot_def)
+  show "make_cert ins phi ! pc' = phi ! pc'" 
+    by (auto intro: make_cert_target)
 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" .
+theorem fits_make_cert:
+  "fits ins (make_cert ins phi) phi"
+  by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets)
 
-    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 fitsD: 
-"\<lbrakk>fits ins cert phi; pc' \<in> succs (ins!pc) pc; pc' \<noteq> Suc pc; pc < length ins; pc' < length ins\<rbrakk> 
-  \<Longrightarrow> cert!pc' = Some (phi!pc')"
-by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
+  "[| fits ins cert phi; pc' \<in> set (succs (ins!pc) pc); 
+      pc' \<noteq> Suc pc; pc < length ins; pc' < length ins |]
+  ==> cert!pc' = phi!pc'"
+  by (clarsimp simp add: fits_def contains_targets_def)
 
 lemma fitsD2:
-"\<lbrakk>fits ins cert phi; Suc pc \<notin> succs (ins!pc) pc;  pc < length ins\<rbrakk> 
-  \<Longrightarrow> cert ! Suc pc = Some (phi ! Suc pc)"
-by (clarsimp simp add: fits_def contains_dead_def contains_targets_def)
-
+   "[| fits ins cert phi; pc < length ins; cert!pc = Some s |]
+  ==> cert!pc = phi!pc"
+  by (auto simp add: fits_def)
+                           
 
 lemma wtl_inst_mono:
-"\<lbrakk>wtl_inst i G rT s1 s1' cert mpc pc; fits ins cert phi; pc < length ins; 
-  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')"
+  "[| wtl_inst i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi; 
+      pc < length ins;  G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
+  \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> s2' <=' s1')"
 proof -
   assume pc:   "pc < length ins" "i = ins!pc"
-  assume wtl:  "wtl_inst i G rT s1 s1' cert mpc pc"
+  assume wtl:  "wtl_inst i G rT s1 cert mpc pc = Ok s1'"
   assume fits: "fits ins cert phi"
-  assume G:    "G \<turnstile> s2 <=s s1"
+  assume G:    "G \<turnstile> s2 <=' s1"
   
-  let "?step s" = "step (i, G, s)"
+  let "?step s" = "step i G s"
 
   from wtl G
-  have app: "app (i, G, rT, s2)" by (auto simp add: wtl_inst_def app_mono)
+  have app: "app i G rT s2" by (auto simp add: wtl_inst_Ok app_mono)
   
   from wtl G
-  have step: "succs i pc \<noteq> {} \<Longrightarrow> G \<turnstile> the (?step s2) <=s the (?step s1)" 
-    by - (drule step_mono, auto simp add: wtl_inst_def)
-  
-  with app
-  have some: "succs i pc \<noteq> {} \<Longrightarrow> ?step s2 \<noteq> None" by (simp add: app_step_some)
+  have step: "succs i pc \<noteq> [] ==> G \<turnstile> ?step s2 <=' ?step s1" 
+    by - (drule step_mono, auto simp add: wtl_inst_Ok)
 
   {
     fix pc'
-    assume 0: "pc' \<in> succs i pc" "pc' \<noteq> pc+1"
-    hence "succs i pc \<noteq> {}" by auto
-    hence "G \<turnstile> the (?step s2) <=s the (?step s1)" by (rule step)
+    assume 0: "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1"
+    hence "succs i pc \<noteq> []" by auto
+    hence "G \<turnstile> ?step s2 <=' ?step s1" by (rule step)
     also 
     from wtl 0
-    have "G \<turnstile> the (?step s1) <=s the (cert!pc')"
-      by (auto simp add: wtl_inst_def) 
+    have "G \<turnstile> ?step s1 <=' cert!pc'"
+      by (auto simp add: wtl_inst_Ok) 
     finally
-    have "G\<turnstile> the (?step s2) <=s the (cert!pc')" .
+    have "G\<turnstile> ?step s2 <=' cert!pc'" .
   } note cert = this
     
-  have "\<exists>s2'. wtl_inst i G rT s2 s2' cert mpc pc \<and> G \<turnstile> s2' <=s s1'"
-  proof (cases "pc+1 \<in> succs i pc")
+  have "\<exists>s2'. wtl_inst i G rT s2 cert mpc pc = Ok s2' \<and> G \<turnstile> s2' <=' s1'"
+  proof (cases "pc+1 \<in> set (succs i pc)")
     case True
     with wtl
-    have s1': "s1' = the (?step s1)" by (simp add: wtl_inst_def)
+    have s1': "s1' = ?step s1" by (simp add: wtl_inst_Ok)
 
-    have "wtl_inst i G rT s2 (the (?step s2)) cert mpc pc \<and> G \<turnstile> (the (?step s2)) <=s s1'" 
+    have "wtl_inst i G rT s2 cert mpc pc = Ok (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'" 
       (is "?wtl \<and> ?G")
     proof
       from True s1'
@@ -253,145 +128,193 @@
 
       from True app wtl
       show ?wtl
-        by (clarsimp intro!: cert simp add: wtl_inst_def)
+        by (clarsimp intro!: cert simp add: wtl_inst_Ok)
     qed
     thus ?thesis by blast
   next
     case False
     with wtl
-    have "s1' = the (cert ! Suc pc)" by (simp add: wtl_inst_def)
+    have "s1' = cert ! Suc pc" by (simp add: wtl_inst_Ok)
 
     with False app wtl
-    have "wtl_inst i G rT s2 s1' cert mpc pc \<and> G \<turnstile> s1' <=s s1'"
-      by (clarsimp intro!: cert simp add: wtl_inst_def)
+    have "wtl_inst i G rT s2 cert mpc pc = Ok s1' \<and> G \<turnstile> s1' <=' s1'"
+      by (clarsimp intro!: cert simp add: wtl_inst_Ok)
 
     thus ?thesis by blast
   qed
   
   with pc show ?thesis by simp
 qed
-    
+
 
-lemma wtl_option_mono:
-"\<lbrakk>wtl_inst_option i G rT s1 s1' cert mpc pc; fits ins cert phi; 
-  pc < length ins; 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')"
+lemma wtl_cert_mono:
+  "[| wtl_cert i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi; 
+      pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
+  \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> s2' <=' s1')"
 proof -
-  assume wtl:  "wtl_inst_option i G rT s1 s1' cert mpc pc" and
+  assume wtl:  "wtl_cert i G rT s1 cert mpc pc = Ok s1'" and
          fits: "fits ins cert phi" "pc < length ins"
-               "G \<turnstile> s2 <=s s1" "i = ins!pc"
+               "G \<turnstile> s2 <=' s1" "i = ins!pc"
 
   show ?thesis
   proof (cases (open) "cert!pc")
     case None
     with wtl fits
     show ?thesis 
-      by - (rule wtl_inst_mono [elimify], (simp add: wtl_inst_option_def)+)
+      by - (rule wtl_inst_mono [elimify], (simp add: wtl_cert_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)+)
+    have G: "G \<turnstile> s2 <=' (Some a)"
+      by - (rule sup_state_opt_trans, auto simp add: wtl_cert_def split: if_splits)
 
     from Some wtl
-    have "wtl_inst i G rT a s1' cert mpc pc" by (simp add: wtl_inst_option_def)
+    have "wtl_inst i G rT (Some a) cert mpc pc = Ok s1'" 
+      by (simp add: wtl_cert_def split: if_splits)
 
     with G fits
-    have "\<exists> s2'. wtl_inst (ins!pc) G rT a s2' cert mpc pc \<and> (G \<turnstile> s2' <=s s1')"
-      by - (rule wtl_inst_mono, (simp add: wtl_inst_option_def)+)
+    have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = Ok s2' \<and> 
+                 (G \<turnstile> s2' <=' s1')"
+      by - (rule wtl_inst_mono, (simp add: wtl_cert_def)+)
     
     with Some G
-    show ?thesis by (simp add: wtl_inst_option_def)
+    show ?thesis by (simp add: wtl_cert_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 -
+  "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
+      pc < length ins; length ins = max_pc |] ==> 
+  wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \<noteq> Err"
+ proof -
   assume wt:   "wt_instr (ins!pc) G rT phi max_pc pc" 
   assume fits: "fits ins cert phi"
   assume pc:   "pc < length ins" "length ins = max_pc"
 
   from wt 
-  have app: "app (ins!pc, G, rT, phi!pc)" by (simp add: wt_instr_def)
+  have app: "app (ins!pc) G rT (phi!pc)" by (simp add: wt_instr_def)
 
   from wt pc
-  have pc': "!!pc'. pc' \<in> succs (ins!pc) pc \<Longrightarrow> pc' < length ins"
+  have pc': "\<And>pc'. pc' \<in> set (succs (ins!pc) pc) ==> pc' < length ins"
     by (simp add: wt_instr_def)
 
-  let ?s' = "the (step (ins!pc,G, phi!pc))"
-
-  from wt
-  have G: "!!pc'. pc' \<in> succs (ins!pc) pc \<Longrightarrow> G \<turnstile> ?s' <=s phi ! pc'"
-    by (simp add: wt_instr_def)
+  let ?s' = "step (ins!pc) G (phi!pc)"
 
   from wt fits pc
-  have cert: "!!pc'. \<lbrakk>pc' \<in> succs (ins!pc) pc; pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> 
-    \<Longrightarrow> cert!pc' \<noteq> None \<and> G \<turnstile> ?s' <=s the (cert!pc')"
-    by (auto dest: fitsD simp add: wt_instr_def)
-
-  show ?thesis
-  proof (cases "pc+1 \<in> succs (ins!pc) pc")
-    case True
-
-    have "wtl_inst (ins!pc) G rT (phi!pc) ?s' cert max_pc pc \<and> G \<turnstile> ?s' <=s phi ! Suc pc" (is "?wtl \<and> ?G")
-    proof 
-      from True
-      show "G \<turnstile> ?s' <=s phi ! Suc pc"  by (simp add: G)
+  have cert: "!!pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> 
+    \<Longrightarrow> G \<turnstile> ?s' <=' cert!pc'"
+    by (auto dest: fitsD simp add: wt_instr_def)     
 
-      from True fits app pc cert pc'
-      show "?wtl"
-        by (auto simp add: wtl_inst_def)
-    qed
-
-    thus ?thesis by blast
-    
-  next    
-    let ?s'' = "the (cert ! Suc pc)"
-
-    case False
-    with fits app pc cert pc'
-    have "wtl_inst (ins ! pc) G rT (phi ! pc) ?s'' cert max_pc pc \<and> G \<turnstile> ?s'' <=s phi ! Suc pc" 
-      by (auto dest: fitsD2 simp add: wtl_inst_def)
-
-    thus ?thesis by blast
-  qed
+  from app pc cert pc'
+  show ?thesis
+    by (auto simp add: wtl_inst_Ok)
 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"
+lemma wt_less_wtl:
+  "[| wt_instr (ins!pc) G rT phi max_pc pc; 
+      wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s;
+      fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
+  G \<turnstile> 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"
+  assume wt:   "wt_instr (ins!pc) G rT phi max_pc pc" 
+  assume wtl:  "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
+  assume fits: "fits ins cert phi"
+  assume pc:   "Suc pc < length ins" "length ins = max_pc"
+
+  { assume suc: "Suc pc \<in> set (succs (ins ! pc) pc)"
+    with wtl         have "s = step (ins!pc) G (phi!pc)"
+      by (simp add: wtl_inst_Ok)
+    also from suc wt have "G \<turnstile> ... <=' phi!Suc pc"
+      by (simp add: wt_instr_def)
+    finally have ?thesis .
+  }
 
-  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+)
+  moreover
+  { assume "Suc pc \<notin> set (succs (ins ! pc) pc)"
+    
+    with wtl
+    have "s = cert!Suc pc" 
+      by (simp add: wtl_inst_Ok)
+    with fits pc
+    have ?thesis
+      by - (cases "cert!Suc pc", simp, drule fitsD2, assumption+, simp)
+  }
+
+  ultimately
+  show ?thesis by blast
+qed
+  
+
+lemma wt_instr_imp_wtl_cert:
+  "[| wt_instr (ins!pc) G rT phi max_pc pc; fits ins cert phi;
+      pc < length ins; length ins = max_pc |] ==> 
+  wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc \<noteq> Err"
+proof -
+  assume "wt_instr (ins!pc) G rT phi max_pc pc" and 
+   fits: "fits ins cert phi" and
+     pc: "pc < length ins" and
+         "length ins = max_pc"
   
-  show ?thesis
-  proof (cases "cert ! pc")
-    case None
-    with *
-    show ?thesis by (simp add: wtl_inst_option_def)
+  hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc \<noteq> Err"
+    by (rule wt_instr_imp_wtl_inst)
+
+  hence "cert!pc = None ==> ?thesis"
+    by (simp add: wtl_cert_def)
 
-  next
-    case Some
+  moreover
+  { fix s
+    assume c: "cert!pc = Some s"
+    with fits pc
+    have "cert!pc = phi!pc"
+      by (rule fitsD2)
+    from this c wtl
+    have ?thesis
+      by (clarsimp simp add: wtl_cert_def)
+  }
+
+  ultimately
+  show ?thesis by blast
+qed
+  
 
-    from fits 
-    have "pc < length phi" by (clarsimp 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
+lemma wt_less_wtl_cert:
+  "[| wt_instr (ins!pc) G rT phi max_pc pc; 
+      wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s;
+      fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
+  G \<turnstile> s <=' phi ! Suc pc"
+proof -
+  assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
+
+  assume wti: "wt_instr (ins!pc) G rT phi max_pc pc"
+              "fits ins cert phi" 
+              "Suc pc < length ins" "length ins = max_pc"
+  
+  { assume "cert!pc = None"
+    with wtl
+    have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
+      by (simp add: wtl_cert_def)
+    with wti
+    have ?thesis
+      by - (rule wt_less_wtl)
+  }
+  moreover
+  { fix t
+    assume c: "cert!pc = Some t"
+    with wti
+    have "cert!pc = phi!pc"
+      by - (rule fitsD2, simp+)
+    with c wtl
+    have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
+      by (simp add: wtl_cert_def)
+    with wti
+    have ?thesis
+      by - (rule wt_less_wtl)
+  }   
+    
+  ultimately
+  show ?thesis by blast
 qed
 
 
@@ -401,13 +324,15 @@
 *}
 
 theorem wt_imp_wtl_inst_list:
-"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \<longrightarrow>   
+"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> 
+        wt_instr (all_ins ! pc') G rT phi (length all_ins) pc') \<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 (length all_ins) pc))" 
-(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins" is "\<forall>pc. ?C pc ins" is "?P ins") 
+       (\<forall> s. (G \<turnstile> s <=' (phi!pc)) \<longrightarrow> 
+             wtl_inst_list ins G rT cert (length all_ins) pc s \<noteq> Err)" 
+(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins"  
+ is "\<forall>pc. ?C pc ins" is "?P ins") 
 proof (induct "?P" "ins")
   case Nil
   show "?P []" by simp
@@ -421,53 +346,56 @@
     assume wt  : "\<forall>pc'. pc' < length all_ins \<longrightarrow> 
                         wt_instr (all_ins ! pc') G rT phi (length all_ins) pc'"
     assume fits: "fits all_ins cert phi"
-    assume G   : "G \<turnstile> s <=s phi ! pc"
     assume l   : "pc < length all_ins"
-
+    assume G   : "G \<turnstile> s <=' phi ! pc"
     assume pc  : "all_ins = l@i#ins'" "pc = length l"
     hence  i   : "all_ins ! pc = i"
       by (simp add: nth_append)
 
     from l wt
-    have "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast
+    have wti: "wt_instr (all_ins!pc) G rT phi (length all_ins) pc" by blast
 
     with fits l 
-    obtain s1 where
-          "wtl_inst_option (all_ins!pc) G rT (phi!pc) s1 cert (length all_ins) pc" and
-      s1: "G \<turnstile> s1 <=s phi ! (Suc pc)"
-      by - (drule wt_instr_imp_wtl_option, assumption+, simp, elim exE conjE, simp) 
+    have c: "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc \<noteq> Err"
+      by - (drule wt_instr_imp_wtl_cert, auto)
     
-    with fits l
-    obtain s2 where
-      o:  "wtl_inst_option (all_ins!pc) G rT s s2 cert (length all_ins) pc" 
-      and "G \<turnstile> s2 <=s s1"
-      by - (drule wtl_option_mono, assumption+, simp, elim exE conjE, rule that) 
-
-    with s1
-    have G': "G \<turnstile> s2 <=s phi ! (Suc pc)"
-      by - (rule sup_state_trans, auto)
-
     from Cons
     have "?C (Suc pc) ins'" by blast
     with wt fits pc
     have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto
 
-    show "\<exists>s'. wtl_inst_list (i#ins') G rT s s' cert (length all_ins) pc"
+    show "wtl_inst_list (i#ins') G rT cert (length all_ins) pc s \<noteq> Err" 
     proof (cases "?len (Suc pc)")
       case False
       with pc
       have "ins' = []" by simp
-      with i o 
-      show ?thesis by auto
+      with G i c fits l
+      show ?thesis by (auto dest: wtl_cert_mono)
     next
       case True
       with IH
-      have "?wtl (Suc pc) ins'" by blast
-      with G'
+      have wtl: "?wtl (Suc pc) ins'" by blast
+
+      from c wti fits l True
+      obtain s'' where
+        "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc = Ok s''"
+        "G \<turnstile> s'' <=' phi ! Suc pc"
+        by clarsimp (drule wt_less_wtl_cert, auto)
+      moreover
+      from calculation fits G l
       obtain s' where
-        "wtl_inst_list ins' G rT s2 s' cert (length all_ins) (Suc pc)"
-        by - (elim allE impE, auto)        
-      with i o
+        c': "wtl_cert (all_ins!pc) G rT s cert (length all_ins) pc = Ok s'" and
+        "G \<turnstile> s' <=' s''"
+        by - (drule wtl_cert_mono, auto)
+      ultimately
+      have G': "G \<turnstile> s' <=' phi ! Suc pc" 
+        by - (rule sup_state_opt_trans)
+
+      with wtl
+      have "wtl_inst_list ins' G rT cert (length all_ins) (Suc pc) s' \<noteq> Err"
+        by auto
+
+      with i c'
       show ?thesis by auto
     qed
   qed
@@ -475,38 +403,42 @@
   
 
 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"
+  "[| wt_method G C pTs rT mxl ins phi; fits ins cert phi |] ==> 
+  wtl_method G C pTs rT mxl ins cert"
 by (simp add: wt_method_def wtl_method_def)
    (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def) 
 
 
 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)"
+  "wt_method G C pTs rT mxl ins phi ==> 
+  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)
+  assume "wt_method G C pTs rT mxl ins phi" 
+  moreover
+  have "fits ins (make_cert ins phi) phi"
+    by (rule fits_make_cert)
+  ultimately
+  show ?thesis 
+    by (rule fits_imp_wtl_method_complete)
 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'"
+"(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)"
+  "(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)"
+theorem wtl_complete: 
+  "wt_jvm_prog G Phi ==> 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"
+  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)
@@ -514,13 +446,15 @@
     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>
+             (\<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'))"
+                  (\<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" 
@@ -530,14 +464,16 @@
     show "wtl_method G a ba ad ae bb (make_Cert G Phi a (ac, ba))"
     proof (rule bspec [elimify], clarsimp)
       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" 
+      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)
         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)
+          by - (rule wtl_method_complete [elimify], assumption+, 
+                simp add: make_Cert_def unique_epsilon)
       qed 
     qed
   qed
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/LBVCorrect.thy
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/MicroJava/BV/BVLcorrect.thy
+(*  Title:      HOL/MicroJava/BV/BVLCorrect.thy
     ID:         $Id$
     Author:     Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
@@ -8,407 +8,285 @@
 
 theory LBVCorrect = BVSpec + LBVSpec:
 
+lemmas [simp del] = split_paired_Ex split_paired_All
+
 constdefs
-fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \<Rightarrow> bool" 
-"fits_partial phi pc is G rT s0 s2 cert \<equiv> (\<forall> a b i s1. (a@(i#b) = is) \<longrightarrow> 
-                   wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \<longrightarrow> 
-                   wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \<longrightarrow> 
-                      ((cert!(pc+length a)      = None   \<longrightarrow> phi!(pc+length a) = s1) \<and> 
-                       (\<forall> t. cert!(pc+length a) = Some t \<longrightarrow> phi!(pc+length a) = t)))"
-  
-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 :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> bool"
+"fits phi is G rT s0 cert \<equiv> 
+  (\<forall>pc s1. pc < length is \<longrightarrow>
+    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 \<longrightarrow>
+    (case cert!pc of None   \<Rightarrow> phi!pc = s1
+                   | Some t \<Rightarrow> phi!pc = Some t)))"
+
+constdefs
+make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] \<Rightarrow> method_type"
+"make_phi is G rT s0 cert \<equiv> 
+   map (\<lambda>pc. case cert!pc of 
+               None   \<Rightarrow> val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
+             | Some t \<Rightarrow> Some t) [0..length is(]"
+
 
-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 fitsD_None:
+  "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
+    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
+    cert ! pc = None\<rbrakk> \<Longrightarrow> phi!pc = s1"
+  by (auto simp add: fits_def)
 
-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 fitsD_Some:
+  "\<lbrakk>fits phi is G rT s0 cert; pc < length is;
+    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
+    cert ! pc = Some t\<rbrakk> \<Longrightarrow> phi!pc = Some t"
+  by (auto simp add: fits_def)
+
+lemma make_phi_Some:
+  "[| pc < length is; cert!pc = Some t |] ==> 
+  make_phi is G rT s0 cert ! pc = Some t"
+  by (simp add: make_phi_def)
+
+lemma make_phi_None:
+  "[| pc < length is; cert!pc = None |] ==> 
+  make_phi is G rT s0 cert ! pc = 
+  val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
+  by (simp add: make_phi_def)
 
 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 (open) ?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"
-
-      from this
-      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
-      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)"
+  "\<exists>phi. fits phi is G rT s0 cert"  
+proof - 
+  have "fits (make_phi is G rT s0 cert) is G rT s0 cert"
+    by (auto simp add: fits_def make_phi_Some make_phi_None 
+             split: option.splits) 
 
-      show "\<exists>phi. pc + length (a # list) < length phi \<and> 
-                  fits_partial phi pc (a # list) G rT s0 s2 cert" 
-      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  
-  with all 
-  show ?thesis  
-  proof (elim exE allE impE conjE) 
-    show "wtl_inst_list is G rT s0 s2 cert (0+length is) 0" by simp 
-  qed (auto simp add: fits_def)  
-qed 
-
-
+  thus ?thesis
+    by blast
+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
+  "[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |]
+  ==> \<forall>pc t. pc < length is \<longrightarrow> cert!pc = Some t \<longrightarrow> phi!pc = Some t"
+proof (intro strip)
+  fix pc t 
+  assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'"
+  then 
+  obtain s'' where
+    "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s''"
+    by (blast dest: wtl_take)
+  moreover
+  assume "fits phi is G rT s cert" 
+         "pc < length is" 
+         "cert ! pc = Some t"
+  ultimately
+  show "phi!pc = Some t" by (auto dest: fitsD_Some)
 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> []"
+ "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
+     wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s';
+     wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s'';
+     fits phi is G rT s cert; Suc pc < length is |] ==>
+  G \<turnstile> s'' <=' phi ! Suc pc"
+proof -
+  
+  assume all:  "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
+  assume fits: "fits phi is G rT s cert"
+
+  assume wtl:  "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
+         wtc:  "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" and
+         pc:   "Suc pc < length is"
+
+  hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''"
+    by (rule wtl_Suc)
+
+  from all
+  have app: 
+  "wtl_inst_list (take (Suc pc) is@drop (Suc pc) is) G rT cert (length is) 0 s \<noteq> Err"
+    by simp
 
-  from this
-  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 "G \<turnstile> s2 <=s phi ! Suc (length a)"
-  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
+  from pc 
+  have "0 < length (drop (Suc pc) is)" 
+    by simp
+  then 
+  obtain l ls where
+    "drop (Suc pc) is = l#ls"
+    by (auto simp add: neq_Nil_conv simp del: length_drop)
+  with app wts pc
+  obtain x where 
+    "wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x"
+    by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
 
-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)
+  hence c1: "\<And>t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
+    by (simp add: wtl_cert_def split: if_splits)
+  moreover
+  from fits pc wts
+  have c2: "\<And>t. cert!Suc pc = Some t ==> phi!Suc pc = cert!Suc pc"
+    by - (drule fitsD_Some, auto)
+  moreover
+  from fits pc wts
+  have c3: "cert!Suc pc = None ==> phi!Suc pc = s''"
+    by (rule fitsD_None)
+  ultimately
 
-  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]) 
-
-  with wo
-  show ?thesis
-    by (auto simp add: c1 c2 c3 wt_instr_def wtl_inst_def wtl_inst_option_def split: option.split_asm)
+  show ?thesis 
+    by - (cases "cert ! Suc pc", auto)
 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"
+  "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; 
+      fits phi is G rT s cert; pc < length is |] ==>
+   wt_instr (is!pc) G rT phi (length is) pc"
+proof -
+
+  assume fits: "fits phi is G rT s cert"
 
-  fix pc
-  assume wtl: "wtl_inst_list is G rT s0 s3 cert (length is) 0"
-     and pc:  "pc < length is"
+  assume pc:  "pc < length is" and
+         wtl: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
+        
+  then
+  obtain s' s'' where
+    w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
+    c: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
+    by - (drule wtl_all, auto)
+
+  from fits wtl pc
+  have cert_Some: 
+    "\<And>t pc. [| pc < length is; cert!pc = Some t |] ==> phi!pc = Some t"
+    by (auto dest: fits_lemma1)
   
-  from this
-  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 fits wtl pc
+  have cert_None: "cert!pc = None ==> phi!pc = s'"
+    by - (drule fitsD_None)
+  
+  from pc c cert_None cert_Some
+  have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = Ok s''"
+    by (auto simp add: wtl_cert_def split: if_splits option.splits)
+
+  { fix pc'
+    assume pc': "pc' \<in> set (succs (is!pc) pc)"
 
-  from l pc
-  have "i2' \<noteq> []" by auto
+    with wti
+    have less: "pc' < length is"  
+      by (simp add: wtl_inst_Ok)
 
-  from this
-  obtain i i2 where c: "i2' = i#i2" 
-    by (simp add: neq_Nil_conv) (elim, rule that)
+    have "G \<turnstile> step (is!pc) G (phi!pc) <=' phi ! pc'" 
+    proof (cases "pc' = Suc pc")
+      case False          
+      with wti pc'
+      have G: "G \<turnstile> step (is ! pc) G (phi ! pc) <=' cert ! pc'" 
+        by (simp add: wtl_inst_Ok)
 
-  with w2 l
-  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)
+      hence "cert!pc' = None ==> step (is ! pc) G (phi ! pc) = None"
+        by simp
+      hence "cert!pc' = None ==> ?thesis"
+        by simp
+
+      moreover
+      { fix t
+        assume "cert!pc' = Some t"
+        with less
+        have "phi!pc' = cert!pc'"
+          by (simp add: cert_Some)
+        with G
+        have ?thesis
+          by simp
+      }
 
-  with l c
-  show "wt_instr (is ! pc) G rT phi (length is) pc"
-    by (auto simp add: nth_append)
+      ultimately
+      show ?thesis by blast      
+    next
+      case True
+      with pc' wti
+      have "step (is ! pc) G (phi ! pc) = s''"  
+        by (simp add: wtl_inst_Ok)
+      also
+      from w c fits pc wtl 
+      have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc"
+        by - (drule wtl_suc_pc)
+      with True less
+      have "G \<turnstile> s'' <=' phi ! Suc pc" 
+        by blast
+      finally
+      show ?thesis 
+        by (simp add: True)
+    qed
+  }
+  
+  with wti
+  show ?thesis
+    by (auto simp add: wtl_inst_Ok wt_instr_def)
 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"
 
-  from this
-  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
     
 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"
+  "[| 0 < length is; wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err; 
+      fits phi is G rT s cert |] ==> 
+  G \<turnstile> 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> []"
+  assume wtl:  "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
+  assume fits: "fits phi is G rT s cert"
+  assume pc:   "0 < length is"
+
+  from wtl
+  have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = Ok s"
+    by simp
   
-  from this 
-  obtain y ys where cons: "is = y#ys" 
+  with fits pc
+  have "cert!0 = None ==> phi!0 = s"
+    by (rule fitsD_None)
+  moreover    
+  from fits pc wt0
+  have "\<And>t. cert!0 = Some t ==> phi!0 = cert!0"
+    by - (drule fitsD_Some, auto)
+  moreover
+  from pc
+  obtain x xs where "is = x#xs" 
     by (simp add: neq_Nil_conv) (elim, rule that)
+  with wtl
+  obtain s' where
+    "wtl_cert x G rT s cert (length is) 0 = Ok s'"
+    by simp (elim, rule that, simp)
+  hence 
+    "\<And>t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
+    by (simp add: wtl_cert_def split: if_splits)
 
-  from fits
+  ultimately
   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)"
+    by - (cases "cert!0", auto)
+qed
 
-    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
   
 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"
+"wtl_method G C pTs rT mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxl ins phi"
+proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
+  let "?s0" = "Some ([], Ok (Class C) # map Ok pTs @ replicate mxl Err)"
+  assume pc:  "0 < length ins"
+  assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
 
-  from this
-  obtain phi where fits: "fits phi ins G rT ?s0 s2 cert \<and> length ins < length phi"
+  obtain phi where fits: "fits phi ins G rT ?s0 cert"    
     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])
+    by (blast intro: wtl_fits_wt)
 
-  from neqNil wtl fits
+  from pc wtl fits
   have "wt_start G C pTs mxl phi"
-    by (elim conjE, unfold wt_start_def) (rule fits_first)
+    by (unfold wt_start_def) (rule fits_first)
 
-  with neqNil allpc fits
+  with pc allpc 
   show ?thesis by (auto simp add: wt_method_def)
 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'"
+  "(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)"
+  "(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:
@@ -421,21 +299,24 @@
   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)"
+  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"
+    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;
+          (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)
+      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"
@@ -451,7 +332,7 @@
                  (\<epsilon>(Cl,x,y,mdecls). (Cl, x, y, mdecls) \<in> set G \<and> Cl = a))) mb) m"
           by - (drule bspec, assumption, 
                 clarsimp dest!: wtl_method_correct,
-                clarsimp intro!: selectI simp add: unique_epsilon)
+                clarsimp intro!: selectI simp add: unique_epsilon) 
       qed
     qed (auto simp add: wtl_jvm_prog_def wf_prog_def wf_cdecl_def)
   qed
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -1,10 +1,10 @@
-(*  Title:      HOL/MicroJava/BV/BVLightSpec.thy
+(*  Title:      HOL/MicroJava/BV/LBVSpec.thy
     ID:         $Id$
     Author:     Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header {* Specification of the LBV *}
+header {* The Lightweight Bytecode Verifier *}
 
 
 theory LBVSpec = Step :
@@ -14,256 +14,181 @@
   class_certificate = "sig \<Rightarrow> certificate"
   prog_certificate  = "cname \<Rightarrow> class_certificate"
 
+
 constdefs
-wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
+  check_cert :: "[instr, jvm_prog, state_type option, certificate, p_count, p_count]
+                 \<Rightarrow> bool"
+  "check_cert i G s cert pc max_pc \<equiv> \<forall>pc' \<in> set (succs i pc). pc' < max_pc \<and>  
+                                     (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')"
 
-"wtl_inst i G rT s s' cert max_pc pc \<equiv> app (i,G,rT,s) \<and> 
-                                       (let s'' = the (step (i,G,s)) in
-                                          (\<forall> pc' \<in> (succs i pc). pc' < max_pc \<and>  
-                                             ((pc' \<noteq> pc+1) \<longrightarrow> cert!pc' \<noteq> None \<and> G \<turnstile> s'' <=s the (cert!pc'))) \<and>  
-                                          (if (pc+1) \<in> (succs i pc) then  
-                                             s' = s'' 
-                                           else 
-                                             cert ! (pc+1) = Some s'))" 
+  wtl_inst :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] 
+               \<Rightarrow> state_type option err" 
+  "wtl_inst i G rT s cert max_pc pc \<equiv> 
+     if app i G rT s \<and> check_cert i G s cert pc max_pc then 
+       if pc+1 mem (succs i pc) then Ok (step i G s) else Ok (cert!(pc+1))
+     else Err";
 
-lemma [simp]: 
-"succs i pc = {pc+1} \<Longrightarrow> 
-  wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \<and> pc+1 < max_pc \<and> (s' = the (step (i,G,s))))"
-by (unfold wtl_inst_def, auto)
-
-lemma [simp]:
-"succs i pc = {} \<Longrightarrow> wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \<and> cert!(pc+1) = Some s')"
-by (unfold wtl_inst_def, auto)
+lemma wtl_inst_Ok:
+"(wtl_inst i G rT s cert max_pc pc = Ok s') =
+ (app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc). 
+                   pc' < max_pc \<and> (pc' \<noteq> pc+1 \<longrightarrow> G \<turnstile> step i G s <=' cert!pc')) \<and> 
+ (if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
+  by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
 
 
 constdefs
-wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
-"wtl_inst_option i G rT s0 s1 cert max_pc pc \<equiv>
-     (case cert!pc of 
-          None     \<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc
-        | Some s0' \<Rightarrow> (G \<turnstile> s0 <=s s0') \<and>
-                      wtl_inst i G rT s0' s1 cert max_pc pc)"
-  
-consts
- wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \<Rightarrow> bool"
+  wtl_cert :: "[instr,jvm_prog,ty,state_type option,certificate,p_count,p_count] 
+               \<Rightarrow> state_type option err"  
+  "wtl_cert i G rT s cert max_pc pc \<equiv>
+     case cert!pc of
+        None    \<Rightarrow> wtl_inst i G rT s cert max_pc pc
+      | Some s' \<Rightarrow> if G \<turnstile> s <=' (Some s') then 
+                    wtl_inst i G rT (Some s') cert max_pc pc 
+                  else Err"
+
+consts 
+  wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count, 
+                     state_type option] \<Rightarrow> state_type option err"
 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 []     G rT cert max_pc pc s = Ok s"
+  "wtl_inst_list (i#is) G rT cert max_pc pc s = 
+    (let s' = wtl_cert i G rT s cert max_pc pc in
+     strict (wtl_inst_list is G rT cert max_pc (pc+1)) s')";
+              
 
 constdefs
- wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \<Rightarrow> bool" 
- "wtl_method G C pTs rT mxl ins cert \<equiv> 
-	let max_pc = length ins 
-        in 
-	0 < max_pc \<and>  
-        (\<exists>s2. wtl_inst_list ins G rT 
-                            ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))
-                            s2 cert max_pc 0)"
+ wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \<Rightarrow> bool"  
+ "wtl_method G C pTs rT mxl ins cert \<equiv>  
+	let max_pc = length ins  
+  in 
+  0 < max_pc \<and>   
+  wtl_inst_list ins G rT cert max_pc 0 
+                (Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err))) \<noteq> Err"
 
- 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" 
-
-text {* \medskip *}
-
-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"
-by auto
-
-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")
-by (unfold wtl_inst_def, auto)
+ 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"
 
-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)
+text {* \medskip *} 
 
-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 (open) ?P "is")
-  case Nil
-  show "?P []" by simp
+lemma strict_Some [simp]: 
+"(strict f x = Ok y) = (\<exists> z. x = Ok z \<and> f z = Ok y)"
+  by (cases x, auto)
 
-  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
-    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
+lemma wtl_Cons:
+  "wtl_inst_list (i#is) G rT cert max_pc pc s \<noteq> Err = 
+  (\<exists>s'. wtl_cert i G rT s cert max_pc pc = Ok s' \<and> 
+        wtl_inst_list is G rT cert max_pc (pc+1) s' \<noteq> Err)"
+by (auto simp del: split_paired_Ex)
 
-    have "s=s'" by(rule wtl_inst_option_unique)
-    with l l' Cons
-    show "s1 = s1'" by blast
-  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 (open) ?P "is")
-  case Nil
-  show "?P []" by auto
+lemma wtl_append:
+"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = Ok s') =
+   (\<exists>s''. wtl_inst_list a G rT cert mpc pc s = Ok s'' \<and> 
+          wtl_inst_list b G rT cert mpc (pc+length a) s'' = Ok s')" 
+  (is "\<forall> s pc. ?C s pc a" is "?P a")
+proof (induct ?P a)
+
+  show "?P []" by simp
   
-  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 (open) pc')
-      case 0
-      with wtl
-      have "?E [] (a#list) s" by simp
-      thus ?thesis by blast
+  fix x xs
+  assume IH: "?P xs"
+
+  show "?P (x#xs)"
+  proof (intro allI)
+    fix s pc 
+
+    show "?C s pc (x#xs)"
+    proof (cases "wtl_cert x G rT s cert mpc pc")
+      case Err thus ?thesis by simp
     next
-      case Suc
-      with wtl      
-      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
-      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
+      fix s0
+      assume Ok: "wtl_cert x G rT s cert mpc pc = Ok s0"
+
+      with IH
+      have "?C s0 (Suc pc) xs" by blast
+      
+      with Ok
+      show ?thesis by simp
     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"
+lemma wtl_take:
+  "wtl_inst_list is G rT cert mpc pc s = Ok s'' ==>
+   \<exists>s'. wtl_inst_list (take pc' is) G rT cert mpc pc s = Ok s'"
 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)"
+  assume "wtl_inst_list is G rT cert mpc pc s = Ok s''"
+
+  hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mpc pc s = Ok s''"
+    by simp
+
+  thus ?thesis 
+    by (auto simp add: wtl_append simp del: append_take_drop_id)
+qed
 
-  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 (open) ?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"
-      from this
-      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 allE impE) (assumption, simp+)
-      with a
-      show "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc"
-        by (auto simp del: split_paired_Ex)
-    qed
+lemma take_Suc:
+  "\<forall>n. n < length l \<longrightarrow> take (Suc n) l = (take n l)@[l!n]" (is "?P l")
+proof (induct l)
+  show "?P []" by simp
+
+  fix x xs
+  assume IH: "?P xs"
+  
+  show "?P (x#xs)"
+  proof (intro strip)
+    fix n
+    assume "n < length (x#xs)"
+    with IH
+    show "take (Suc n) (x # xs) = take n (x # xs) @ [(x # xs) ! n]"
+      by - (cases n, auto)
   qed
-  
-  with w
-  show ?thesis 
-  proof (elim allE impE)
-    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"
+lemma wtl_Suc:
+ "[| wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'; 
+     wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s'';
+     Suc pc < length is |] ==>
+  wtl_inst_list (take (Suc pc) is)  G rT cert (length is) 0 s = Ok s''" 
 proof -
-  assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0"
+  assume wtt: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'"
+  assume wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
+  assume pc: "Suc pc < length is"
 
-  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 "take (Suc pc) is = (take pc is)@[is!pc]" 
+    by (simp add: take_Suc)
 
-  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)
+  with wtt wtc pc
+  show ?thesis
+    by (simp add: wtl_append min_def)
 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"
+lemma wtl_all:
+  "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
+      pc < length is |] ==> 
+   \<exists>s' s''. wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s' \<and> 
+            wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
 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))"
+  assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
 
-  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 (open) ?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"
-      from this
-      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 allE impE) 
-        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 "?p s0 pc"
-        by (auto simp del: split_paired_Ex)
-    qed
-  qed
-  with a i b
-  show ?thesis 
-  proof (elim allE impE)
-    from a show "wtl_inst_list a G rT s0 s1 cert (0+length (a@i#b)) 0" by simp
-  qed auto
+  assume pc: "pc < length is"
+  hence  "0 < length (drop pc is)" by simp
+  then 
+  obtain i r where 
+    Cons: "drop pc is = i#r" 
+    by (auto simp add: neq_Nil_conv simp del: length_drop)
+  hence "i#r = drop pc is" ..
+  with all
+  have take: "wtl_inst_list (take pc is@i#r) G rT cert (length is) 0 s \<noteq> Err"
+    by simp
+ 
+  from pc
+  have "is!pc = drop pc is ! 0" by simp
+  with Cons
+  have "is!pc = i" by simp
+
+  with take pc
+  show ?thesis
+    by (auto simp add: wtl_append min_def)
 qed
 
 end
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/Step.thy
--- a/src/HOL/MicroJava/BV/Step.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -7,107 +7,114 @@
 header {* Effect of instructions on the state type *}
 
 
-theory Step = Convert :
+theory Step = Convert:
 
 
 text "Effect of instruction on the state type:"
 consts 
-step :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type option"
+step' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
 
-recdef step "{}"
-"step (Load idx,  G, (ST, LT))          = Some (the (LT ! idx) # ST, LT)"
-"step (Store idx, G, (ts#ST, LT))       = Some (ST, LT[idx:= Some ts])"
-"step (Bipush i, G, (ST, LT))           = Some (PrimT Integer # ST, LT)"
-"step (Aconst_null, G, (ST, LT))        = Some (NT#ST,LT)"
-"step (Getfield F C, G, (oT#ST, LT))    = Some (snd (the (field (G,C) F)) # ST, LT)"
-"step (Putfield F C, G, (vT#oT#ST, LT)) = Some (ST,LT)"
-"step (New C, G, (ST,LT))               = Some (Class C # ST, LT)"
-"step (Checkcast C, G, (RefT rt#ST,LT)) = Some (Class C # ST,LT)"
-"step (Pop, G, (ts#ST,LT))              = Some (ST,LT)"
-"step (Dup, G, (ts#ST,LT))              = Some (ts#ts#ST,LT)"
-"step (Dup_x1, G, (ts1#ts2#ST,LT))      = Some (ts1#ts2#ts1#ST,LT)"
-"step (Dup_x2, G, (ts1#ts2#ts3#ST,LT))  = Some (ts1#ts2#ts3#ts1#ST,LT)"
-"step (Swap, G, (ts1#ts2#ST,LT))        = Some (ts2#ts1#ST,LT)"
-"step (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) 
-                                          = Some (PrimT Integer#ST,LT)"
-"step (Ifcmpeq b, G, (ts1#ts2#ST,LT))   = Some (ST,LT)"
-"step (Goto b, G, s)                    = Some s"
-"step (Return, G, (T#ST,LT))            = None"   (* Return has no successor instruction in the same method *)
-"step (Invoke C mn fpTs, G, (ST,LT))    = (let ST' = drop (length fpTs) ST in
-                                              Some (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" 
+recdef step' "{}"
+"step' (Load idx,  G, (ST, LT))          = (val (LT ! idx) # ST, LT)"
+"step' (Store idx, G, (ts#ST, LT))       = (ST, LT[idx:= Ok ts])"
+"step' (Bipush i, G, (ST, LT))           = (PrimT Integer # ST, LT)"
+"step' (Aconst_null, G, (ST, LT))        = (NT#ST,LT)"
+"step' (Getfield F C, G, (oT#ST, LT))    = (snd (the (field (G,C) F)) # ST, LT)"
+"step' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)"
+"step' (New C, G, (ST,LT))               = (Class C # ST, LT)"
+"step' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)"
+"step' (Pop, G, (ts#ST,LT))              = (ST,LT)"
+"step' (Dup, G, (ts#ST,LT))              = (ts#ts#ST,LT)"
+"step' (Dup_x1, G, (ts1#ts2#ST,LT))      = (ts1#ts2#ts1#ST,LT)"
+"step' (Dup_x2, G, (ts1#ts2#ts3#ST,LT))  = (ts1#ts2#ts3#ts1#ST,LT)"
+"step' (Swap, G, (ts1#ts2#ST,LT))        = (ts2#ts1#ST,LT)"
+"step' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT)) 
+                                         = (PrimT Integer#ST,LT)"
+"step' (Ifcmpeq b, G, (ts1#ts2#ST,LT))   = (ST,LT)"
+"step' (Goto b, G, s)                    = s"
+  (* Return has no successor instruction in the same method: *)
+(* "step' (Return, G, (T#ST,LT))            = None" *)
+"step' (Invoke C mn fpTs, G, (ST,LT))    = (let ST' = drop (length fpTs) ST 
+  in  (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" 
 
-"step (i,G,s)                           = None"
+(* "step' (i,G,s)                           = None" *)
+
+constdefs
+  step :: "instr \<Rightarrow> jvm_prog \<Rightarrow> state_type option \<Rightarrow> state_type option"
+  "step i G \<equiv> opt_map (\<lambda>s. step' (i,G,s))"
 
 
 text "Conditions under which step is applicable:"
 consts
-app :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
+app' :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
 
-recdef app "{}"
-"app (Load idx, G, rT, s)                  = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> None)"
-"app (Store idx, G, rT, (ts#ST, LT))       = (idx < length LT)"
-"app (Bipush i, G, rT, s)                  = True"
-"app (Aconst_null, G, rT, s)               = True"
-"app (Getfield F C, G, rT, (oT#ST, LT))    = (is_class G C \<and> 
+recdef app' "{}"
+"app' (Load idx, G, rT, s)                  = (idx < length (snd s) \<and> 
+                                              (snd s) ! idx \<noteq> Err)"
+"app' (Store idx, G, rT, (ts#ST, LT))       = (idx < length LT)"
+"app' (Bipush i, G, rT, s)                  = True"
+"app' (Aconst_null, G, rT, s)               = True"
+"app' (Getfield F C, G, rT, (oT#ST, LT))    = (is_class G C \<and> 
                                               field (G,C) F \<noteq> None \<and>
                                               fst (the (field (G,C) F)) = C \<and>
                                               G \<turnstile> oT \<preceq> (Class C))"
-"app (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \<and> 
+"app' (Putfield F C, G, rT, (vT#oT#ST, LT)) = (is_class G C \<and> 
                                               field (G,C) F \<noteq> None \<and>
                                               fst (the (field (G,C) F)) = C \<and>
                                               G \<turnstile> oT \<preceq> (Class C) \<and>
                                               G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" 
-"app (New C, G, rT, s)                     = (is_class G C)"
-"app (Checkcast C, G, rT, (RefT rt#ST,LT)) = (is_class G C)"
-"app (Pop, G, rT, (ts#ST,LT))              = True"
-"app (Dup, G, rT, (ts#ST,LT))              = True"
-"app (Dup_x1, G, rT, (ts1#ts2#ST,LT))      = True"
-"app (Dup_x2, G, rT, (ts1#ts2#ts3#ST,LT))  = True"
-"app (Swap, G, rT, (ts1#ts2#ST,LT))        = True"
-"app (IAdd, G, rT, (PrimT Integer#PrimT Integer#ST,LT)) 
-                                           = True"
-"app (Ifcmpeq b, G, rT, (ts1#ts2#ST,LT))   = ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or> 
-                                              (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r'))"
-"app (Goto b, G, rT, s)                    = True"
-"app (Return, G, rT, (T#ST,LT))            = (G \<turnstile> T \<preceq> rT)"
-app_invoke:
-"app (Invoke C mn fpTs, G, rT, s)          = (length fpTs < length (fst s) \<and> 
-                                              (let 
-                                                apTs = rev (take (length fpTs) (fst s));
-                                                X    = hd (drop (length fpTs) (fst s)) 
-                                              in
-                                                G \<turnstile> X \<preceq> Class C \<and> 
-                                                (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
-                                                method (G,C) (mn,fpTs) \<noteq> None
-                                             ))"
+"app' (New C, G, rT, s)                     = (is_class G C)"
+"app' (Checkcast C, G, rT, (RefT rt#ST,LT)) = (is_class G C)"
+"app' (Pop, G, rT, (ts#ST,LT))              = True"
+"app' (Dup, G, rT, (ts#ST,LT))              = True"
+"app' (Dup_x1, G, rT, (ts1#ts2#ST,LT))      = True"
+"app' (Dup_x2, G, rT, (ts1#ts2#ts3#ST,LT))  = True"
+"app' (Swap, G, rT, (ts1#ts2#ST,LT))        = True"
+"app' (IAdd, G, rT, (PrimT Integer#PrimT Integer#ST,LT)) 
+                                            = True"
+"app' (Ifcmpeq b, G, rT, (ts#ts'#ST,LT))    = ((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or> 
+                                              (\<exists>r r'. ts = RefT r \<and> ts' = RefT r'))"
+"app' (Goto b, G, rT, s)                    = True"
+"app' (Return, G, rT, (T#ST,LT))            = (G \<turnstile> T \<preceq> rT)"
+"app' (Invoke C mn fpTs, G, rT, s)          = 
+   (length fpTs < length (fst s) \<and> 
+   (let apTs = rev (take (length fpTs) (fst s));
+        X    = hd (drop (length fpTs) (fst s)) 
+    in  
+        G \<turnstile> X \<preceq> Class C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and> 
+        (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT)))"
 
-"app (i,G,rT,s)                            = False"
+"app' (i,G,rT,s)                            = False"
+
 
+constdefs
+  app :: "instr \<Rightarrow> jvm_prog \<Rightarrow> ty \<Rightarrow> state_type option \<Rightarrow> bool"
+  "app i G rT s \<equiv> case s of None \<Rightarrow> True | Some t \<Rightarrow> app' (i,G,rT,t)"
 
 text {* program counter of successor instructions: *}
 
 consts
-succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set"
+succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count list"
 
 primrec 
-"succs (Load idx) pc         = {pc+1}"
-"succs (Store idx) pc        = {pc+1}"
-"succs (Bipush i) pc         = {pc+1}"
-"succs (Aconst_null) pc      = {pc+1}"
-"succs (Getfield F C) pc     = {pc+1}"
-"succs (Putfield F C) pc     = {pc+1}"
-"succs (New C) pc            = {pc+1}"
-"succs (Checkcast C) pc      = {pc+1}"
-"succs Pop pc                = {pc+1}"
-"succs Dup pc                = {pc+1}"
-"succs Dup_x1 pc             = {pc+1}"
-"succs Dup_x2 pc             = {pc+1}"
-"succs Swap pc               = {pc+1}"
-"succs IAdd pc               = {pc+1}"
-"succs (Ifcmpeq b) pc        = {pc+1, nat (int pc + b)}"
-"succs (Goto b) pc           = {nat (int pc + b)}"
-"succs Return pc             = {}"  
-"succs (Invoke C mn fpTs) pc = {pc+1}"
+"succs (Load idx) pc         = [pc+1]"
+"succs (Store idx) pc        = [pc+1]"
+"succs (Bipush i) pc         = [pc+1]"
+"succs (Aconst_null) pc      = [pc+1]"
+"succs (Getfield F C) pc     = [pc+1]"
+"succs (Putfield F C) pc     = [pc+1]"
+"succs (New C) pc            = [pc+1]"
+"succs (Checkcast C) pc      = [pc+1]"
+"succs Pop pc                = [pc+1]"
+"succs Dup pc                = [pc+1]"
+"succs Dup_x1 pc             = [pc+1]"
+"succs Dup_x2 pc             = [pc+1]"
+"succs Swap pc               = [pc+1]"
+"succs IAdd pc               = [pc+1]"
+"succs (Ifcmpeq b) pc        = [pc+1, nat (int pc + b)]"
+"succs (Goto b) pc           = [nat (int pc + b)]"
+"succs Return pc             = []"  
+"succs (Invoke C mn fpTs) pc = [pc+1]"
 
 
 lemma 1: "2 < length a \<Longrightarrow> (\<exists>l l' l'' ls. a = l#l'#l''#ls)"
@@ -120,7 +127,8 @@
 proof -;
   assume "\<not>(2 < length a)"
   hence "length a < (Suc 2)" by simp
-  hence * : "length a = 0 \<or> length a = 1 \<or> length a = 2" by (auto simp add: less_Suc_eq)
+  hence * : "length a = 0 \<or> length a = 1 \<or> length a = 2" 
+    by (auto simp add: less_Suc_eq)
 
   { 
     fix x 
@@ -134,59 +142,79 @@
 
 text {* 
 \medskip
-simp rules for \isa{app} without patterns, better suited for proofs:
+simp rules for @{term app}
 *}
-lemma appStore[simp]:
-"app (Store idx, G, rT, s) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+lemma appNone[simp]:
+"app i G rT None = True"
+  by (simp add: app_def)
+
 
 
+lemma appLoad[simp]:
+"(app (Load idx) G rT (Some s)) = (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err)"
+  by (simp add: app_def)
+
+lemma appStore[simp]:
+"(app (Store idx) G rT (Some s)) = (\<exists> ts ST LT. s = (ts#ST,LT) \<and> idx < length LT)"
+  by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
+
+lemma appBipush[simp]:
+"(app (Bipush i) G rT (Some s)) = True"
+  by (simp add: app_def)
+
+lemma appAconst[simp]:
+"(app Aconst_null G rT (Some s)) = True"
+  by (simp add: app_def)
+
 lemma appGetField[simp]:
-"app (Getfield F C, G, rT, s) = (\<exists> oT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and> 
-                                 fst (the (field (G,C) F)) = C \<and>
-                                 field (G,C) F \<noteq> None \<and> G \<turnstile> oT \<preceq> (Class C))"
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
-
+"(app (Getfield F C) G rT (Some s)) = 
+ (\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and>  
+  field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C))"
+  by (cases s, cases "2 < length (fst s)", auto dest!: 1 2 simp add: app_def)
 
 lemma appPutField[simp]:
-"app (Putfield F C, G, rT, s) = (\<exists> vT oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and> 
-                                 field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
-                                 G \<turnstile> oT \<preceq> (Class C) \<and>
-                                 G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" 
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"(app (Putfield F C) G rT (Some s)) = 
+ (\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and> 
+  field (G,C) F = Some (C, vT') \<and> G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> vT')"
+  by (cases s, cases "2 < length (fst s)", auto dest!: 1 2 simp add: app_def)
 
+lemma appNew[simp]:
+"(app (New C) G rT (Some s)) = is_class G C"
+  by (simp add: app_def)
 
 lemma appCheckcast[simp]:
-"app (Checkcast C, G, rT, s) = (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C)"
-by (cases s, cases "fst s", simp, cases "hd (fst s)", auto)
+"(app (Checkcast C) G rT (Some s)) = (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C)"
+  by (cases s, cases "fst s", simp add: app_def)
+     (cases "hd (fst s)", auto simp add: app_def)
 
 lemma appPop[simp]:
-"app (Pop, G, rT, s) = (\<exists>ts ST LT. s = (ts#ST,LT))" 
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"(app Pop G rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))" 
+  by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
 
 
 lemma appDup[simp]:
-"app (Dup, G, rT, s) = (\<exists>ts ST LT. s = (ts#ST,LT))" 
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"(app Dup G rT (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))" 
+  by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
 
 
 lemma appDup_x1[simp]:
-"app (Dup_x1, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" 
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"(app Dup_x1 G rT (Some s)) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" 
+  by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
 
 
 lemma appDup_x2[simp]:
-"app (Dup_x2, G, rT, s) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"(app Dup_x2 G rT (Some s)) = (\<exists>ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT))"
+  by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
 
 
 lemma appSwap[simp]:
-"app (Swap, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" 
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"app Swap G rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" 
+  by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
 
 
 lemma appIAdd[simp]:
-"app (IAdd, G, rT, s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))"  (is "?app s = ?P s")
+"app IAdd G rT (Some s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))"  
+  (is "?app s = ?P s")
 proof (cases (open) s)
   case Pair
   have "?app (a,b) = ?P (a,b)"
@@ -205,60 +233,69 @@
           proof (cases t')
             fix p' assume "t' = PrimT p'"
             with t' ip p a
-            show ?thesis by - (cases p', auto)
-          qed (auto simp add: a p ip t')
-        qed (auto simp add: a p ip)
-      qed (auto simp add: a p)
-    qed (auto simp add: a)
-  qed auto
+            show ?thesis by - (cases p', auto simp add: app_def)
+          qed (auto simp add: a p ip t' app_def)
+        qed (auto simp add: a p ip app_def)
+      qed (auto simp add: a p app_def)
+    qed (auto simp add: a app_def)
+  qed (auto simp add: app_def)
   with Pair show ?thesis by simp
 qed
 
 
 lemma appIfcmpeq[simp]:
-"app (Ifcmpeq b, G, rT, s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 
-                              ((\<exists> p. ts1 = PrimT p \<and> ts1 = PrimT p) \<or>  
-                               (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))" 
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"app (Ifcmpeq b) G rT (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 
+ ((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))" 
+  by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
 
 
 lemma appReturn[simp]:
-"app (Return, G, rT, s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))" 
-by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
+"app Return G rT (Some s) = (\<exists>T ST LT. s = (T#ST,LT) \<and> (G \<turnstile> T \<preceq> rT))" 
+  by (cases s, cases "2 < length (fst s)", auto dest: 1 2 simp add: app_def)
 
+lemma appGoto[simp]:
+"app (Goto branch) G rT (Some s) = True"
+  by (simp add: app_def)
 
 lemma appInvoke[simp]:
-"app (Invoke C mn fpTs, G, rT, s) = (\<exists>apTs X ST LT.
-                                       s = ((rev apTs) @ (X # ST), LT) \<and> 
-                                       length apTs = length fpTs \<and> 
-                                       G \<turnstile> X \<preceq> Class C \<and>  
-                                       (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> 
-                                       method (G,C) (mn,fpTs) \<noteq> None)" (is "?app s = ?P s")
+"app (Invoke C mn fpTs) G rT (Some s) = (\<exists>apTs X ST LT mD' rT' b'.
+  s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and> 
+  G \<turnstile> X \<preceq> Class C \<and> (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> 
+  method (G,C) (mn,fpTs) = Some (mD', rT', b'))" (is "?app s = ?P s")
 proof (cases (open) s)
   case Pair
   have "?app (a,b) \<Longrightarrow> ?P (a,b)"
   proof -
     assume app: "?app (a,b)"
-    hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> length fpTs < length a" 
-      (is "?a \<and> ?l") by auto    
-    hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") by auto
-    hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" by (auto simp add: min_def)
-    hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" by blast
-    hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" by blast        
-    hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> (\<exists>X ST'. ST = X#ST')" by (simp add: neq_Nil_conv)
-    hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" by blast
+    hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and> 
+           length fpTs < length a" (is "?a \<and> ?l") 
+      by (auto simp add: app_def)
+    hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") 
+      by auto
+    hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" 
+      by (auto simp add: min_def)
+    hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" 
+      by blast
+    hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" 
+      by blast
+    hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 
+           (\<exists>X ST'. ST = X#ST')" 
+      by (simp add: neq_Nil_conv)
+    hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs" 
+      by blast
     with app
-    show ?thesis by auto blast
+    show ?thesis by (auto simp add: app_def) blast
   qed
   with Pair have "?app s \<Longrightarrow> ?P s" by simp
-  thus ?thesis by auto
+  thus ?thesis by (auto simp add: app_def)
 qed 
 
-lemmas [simp del] = app_invoke
-
+lemma step_Some:
+  "step i G (Some s) \<noteq> None"
+  by (simp add: step_def)
 
-lemma app_step_some:
-  "\<lbrakk>app (i,G,rT,s); succs i pc \<noteq> {}\<rbrakk> \<Longrightarrow> step (i,G,s) \<noteq> None";
-  by (cases s, cases i, auto)
+lemma step_None [simp]:
+  "step i G None = None"
+  by (simp add: step_def)
 
 end
diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/StepMono.thy
--- a/src/HOL/MicroJava/BV/StepMono.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -14,7 +14,8 @@
 
 
 lemma sup_loc_some [rulify]:
-"\<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")
+"\<forall> y n. (G \<turnstile> b <=l y) \<longrightarrow> n < length y \<longrightarrow> y!n = Ok t \<longrightarrow> 
+  (\<exists>t. b!n = Ok t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
 proof (induct (open) ?P b)
   show "?P []" by simp
 
@@ -24,12 +25,12 @@
     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"
+      "n < Suc (length zs)" "(z # zs) ! n = Ok t"
 
-    show "(\<exists>t. (a # list) ! n = Some t) \<and> G \<turnstile>(a # list) ! n <=o Some t" 
+    show "(\<exists>t. (a # list) ! n = Ok t) \<and> G \<turnstile>(a # list) ! n <=o Ok t" 
     proof (cases n) 
       case 0
-      with * show ?thesis by (simp add: sup_ty_opt_Some)
+      with * show ?thesis by (simp add: sup_ty_opt_Ok)
     next
       case Suc
       with Cons *
@@ -40,7 +41,8 @@
    
 
 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))" 
+"\<forall>b. length a = length b \<longrightarrow> 
+     (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map Ok a) <=l (map Ok b))" 
  (is "\<forall>b. length a = length b \<longrightarrow> ?Q a b" is "?P a")
 proof (induct "a")
   show "?P []" by simp
@@ -116,196 +118,211 @@
 
 
 lemma app_mono: 
-"\<lbrakk>G \<turnstile> s2 <=s s1; app (i, G, rT, s1)\<rbrakk> \<Longrightarrow> app (i, G, rT, s2)";
+"\<lbrakk>G \<turnstile> s <=' s'; app i G rT s'\<rbrakk> \<Longrightarrow> app i G rT s";
 proof -
-  assume G:   "G \<turnstile> s2 <=s s1"
-  assume app: "app (i, G, rT, s1)"
-  
-  show ?thesis
-  proof (cases (open) i)
-    case Load
-    
-    from G
-    have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length)
 
-    from G Load app
-    have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
-    
-    with G Load app l
-    show ?thesis by clarsimp (drule sup_loc_some, simp+)
-  next
-    case Store
-    with G app
-    show ?thesis
-      by - (cases s2,
-            auto simp add: map_eq_Cons sup_loc_Cons2 sup_loc_length sup_state_def)
-  next
-    case Bipush
-    thus ?thesis by simp 
-  next
-    case Aconst_null
-    thus ?thesis by simp
-  next
-    case New
-    with app
-    show ?thesis by simp
-  next
-    case Getfield
-    with app G
-    show ?thesis
-      by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
-  next
-    case Putfield
+  { fix s1 s2
+    assume G:   "G \<turnstile> s2 <=s s1"
+    assume app: "app i G rT (Some s1)"
 
-    with app 
-    obtain vT oT ST LT b
-      where s1: "s1 = (vT # oT # ST, LT)" and
-                "field (G, cname) vname = Some (cname, b)" 
-                "is_class G cname" and
-            oT: "G\<turnstile> oT\<preceq> (Class cname)" and
-            vT: "G\<turnstile> vT\<preceq> b"
-      by simp (elim exE conjE, simp, rule that)
-    moreover
-    from s1 G
-    obtain vT' oT' ST' LT'
-      where s2:  "s2 = (vT' # oT' # ST', LT')" and
-            oT': "G\<turnstile> oT' \<preceq> oT" and
-            vT': "G\<turnstile> vT' \<preceq> vT"
-      by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
-    moreover
-    from vT' vT
-    have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
-    moreover
-    from oT' oT
-    have "G\<turnstile> oT' \<preceq> (Class cname)" by (rule widen_trans)
-    ultimately
-    show ?thesis
-      by (auto simp add: Putfield)
-  next
-    case Checkcast
-    with app G
-    show ?thesis 
-      by - (cases s2, auto intro!: widen_RefT2 simp add: sup_state_Cons2)
-  next
-    case Return
-    with app G
-    show ?thesis
-      by - (cases s2, auto simp add: sup_state_Cons2, rule widen_trans)
-  next
-    case Pop
-    with app G
-    show ?thesis
-      by - (cases s2, clarsimp simp add: sup_state_Cons2)
-  next
-    case Dup
-    with app G
-    show ?thesis
-      by - (cases s2, clarsimp simp add: sup_state_Cons2)
-  next
-    case Dup_x1
-    with app G
-    show ?thesis
-      by - (cases s2, clarsimp simp add: sup_state_Cons2)
-  next
-    case Dup_x2
-    with app G
-    show ?thesis
-      by - (cases s2, clarsimp simp add: sup_state_Cons2)
-  next
-    case Swap
-    with app G
-    show ?thesis
-      by - (cases s2, clarsimp simp add: sup_state_Cons2)
-  next
-    case IAdd
-    with app G
-    show ?thesis
-      by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT)
-  next
-    case Goto 
-    with app
-    show ?thesis by simp
-  next
-    case Ifcmpeq
-    with app G
-    show ?thesis
-      by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2)
-  next
-    case Invoke
+    have "app i G rT (Some s2)"
+    proof (cases (open) i)
+      case Load
+    
+      from G
+      have l: "length (snd s1) = length (snd s2)" by (simp add: sup_state_length)
+      
+      from G Load app
+      have "G \<turnstile> snd s2 <=l snd s1" by (auto simp add: sup_state_def)
+      
+      with G Load app l
+      show ?thesis by clarsimp (drule sup_loc_some, simp+)
+    next
+      case Store
+      with G app
+      show ?thesis
+        by - (cases s2,
+              auto simp add: map_eq_Cons sup_loc_Cons2 sup_loc_length sup_state_def)
+    next
+      case Bipush
+      thus ?thesis by simp 
+    next
+      case Aconst_null
+      thus ?thesis by simp
+    next
+      case New
+      with app
+      show ?thesis by simp
+    next
+      case Getfield
+      with app G
+      show ?thesis
+        by - (cases s2, clarsimp simp add: sup_state_Cons2, rule widen_trans)
+    next
+      case Putfield
+      
+      with app 
+      obtain vT oT ST LT b
+        where s1: "s1 = (vT # oT # ST, LT)" and
+                  "field (G, cname) vname = Some (cname, b)" 
+                  "is_class G cname" and
+              oT: "G\<turnstile> oT\<preceq> (Class cname)" and
+              vT: "G\<turnstile> vT\<preceq> b"
+        by simp (elim exE conjE, rule that) 
+      moreover
+      from s1 G
+      obtain vT' oT' ST' LT'
+        where s2:  "s2 = (vT' # oT' # ST', LT')" and
+              oT': "G\<turnstile> oT' \<preceq> oT" and
+              vT': "G\<turnstile> vT' \<preceq> vT"
+        by - (cases s2, simp add: sup_state_Cons2, elim exE conjE, simp, rule that)
+      moreover
+      from vT' vT
+      have "G \<turnstile> vT' \<preceq> b" by (rule widen_trans)
+      moreover
+      from oT' oT
+      have "G\<turnstile> oT' \<preceq> (Class cname)" by (rule widen_trans)
+      ultimately
+      show ?thesis
+        by (auto simp add: Putfield)
+    next
+      case Checkcast
+      with app G
+      show ?thesis 
+        by - (cases s2, auto intro!: widen_RefT2 simp add: sup_state_Cons2)
+    next
+      case Return
+      with app G
+      show ?thesis
+        by - (cases s2, auto simp add: sup_state_Cons2, rule widen_trans)
+    next
+      case Pop
+      with app G
+      show ?thesis
+        by - (cases s2, clarsimp simp add: sup_state_Cons2)
+    next
+      case Dup
+      with app G
+      show ?thesis
+        by - (cases s2, clarsimp simp add: sup_state_Cons2)
+    next
+      case Dup_x1
+      with app G
+      show ?thesis
+        by - (cases s2, clarsimp simp add: sup_state_Cons2)
+    next
+      case Dup_x2
+      with app G
+      show ?thesis
+        by - (cases s2, clarsimp simp add: sup_state_Cons2)
+    next
+      case Swap
+      with app G
+      show ?thesis
+        by - (cases s2, clarsimp simp add: sup_state_Cons2)
+    next
+      case IAdd
+      with app G
+      show ?thesis
+        by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT)
+    next
+      case Goto 
+      with app
+      show ?thesis by simp
+    next
+      case Ifcmpeq
+      with app G
+      show ?thesis
+        by - (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2)
+    next
+      case Invoke
+      
+      with app
+      obtain apTs X ST LT mD' rT' b' where
+        s1: "s1 = (rev apTs @ X # ST, LT)" and
+        l:  "length apTs = length list" and
+        C:  "G \<turnstile> X \<preceq> Class cname" and
+        w:  "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and
+        m:  "method (G, cname) (mname, list) = Some (mD', rT', b')"
+        by (simp, elim exE conjE) (rule that)
 
-    with app
-    obtain apTs X ST LT where
-      s1: "s1 = (rev apTs @ X # ST, LT)" and
-      l:  "length apTs = length list" and
-      C:  "G \<turnstile> X \<preceq> Class cname" and
-      w:  "\<forall>x \<in> set (zip apTs list). x \<in> widen G" and
-      m:  "method (G, cname) (mname, list) \<noteq> None"
-      by (simp del: not_None_eq, elim exE conjE) (rule that)
+      obtain apTs' X' ST' LT' where
+        s2: "s2 = (rev apTs' @ X' # ST', LT')" and
+        l': "length apTs' = length list"
+      proof -
+        from l s1 G 
+        have "length list < length (fst s2)" 
+          by (simp add: sup_state_length)
+        hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
+          by (rule rev_append_cons [rulify])
+        thus ?thesis
+          by -  (cases s2, elim exE conjE, simp, rule that) 
+      qed
 
-    obtain apTs' X' ST' LT' where
-      s2: "s2 = (rev apTs' @ X' # ST', LT')" and
-      l': "length apTs' = length list"
-    proof -
-      from l s1 G 
-      have "length list < length (fst s2)" 
-        by (simp add: sup_state_length)
-      hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
-        by (rule rev_append_cons [rulify])
-      thus ?thesis
-        by -  (cases s2, elim exE conjE, simp, rule that) 
-    qed
-
-    from l l'
-    have "length (rev apTs') = length (rev apTs)" by simp
+      from l l'
+      have "length (rev apTs') = length (rev apTs)" by simp
     
-    from this s1 s2 G 
-    obtain
-      G': "G \<turnstile> (apTs',LT') <=s (apTs,LT)" and
-      X : "G \<turnstile>  X' \<preceq> X" and "G \<turnstile> (ST',LT') <=s (ST,LT)"
-      by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1);
+      from this s1 s2 G 
+      obtain
+        G': "G \<turnstile> (apTs',LT') <=s (apTs,LT)" and
+        X : "G \<turnstile>  X' \<preceq> X" and "G \<turnstile> (ST',LT') <=s (ST,LT)"
+        by (simp add: sup_state_rev_fst sup_state_append_fst sup_state_Cons1)
         
-    with C
-    have C': "G \<turnstile> X' \<preceq> Class cname"
-      by - (rule widen_trans, auto)
+      with C
+      have C': "G \<turnstile> X' \<preceq> Class cname"
+        by - (rule widen_trans, auto)
     
-    from G'
-    have "G \<turnstile> map Some apTs' <=l map Some apTs"
-      by (simp add: sup_state_def)
-    also
-    from l w
-    have "G \<turnstile> map Some apTs <=l map Some list" 
-      by (simp add: all_widen_is_sup_loc)
-    finally
-    have "G \<turnstile> map Some apTs' <=l map Some list" .
+      from G'
+      have "G \<turnstile> map Ok apTs' <=l map Ok apTs"
+        by (simp add: sup_state_def)
+      also
+      from l w
+      have "G \<turnstile> map Ok apTs <=l map Ok list" 
+        by (simp add: all_widen_is_sup_loc)
+      finally
+      have "G \<turnstile> map Ok apTs' <=l map Ok list" .
 
-    with l'
-    have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
-      by (simp add: all_widen_is_sup_loc)
+      with l'
+      have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
+        by (simp add: all_widen_is_sup_loc)
 
-    from Invoke s2 l' w' C' m
-    show ?thesis 
-      by simp blast
-  qed
+      from Invoke s2 l' w' C' m
+      show ?thesis 
+        by simp blast
+    qed
+  } note mono_Some = this
+
+  assume "G \<turnstile> s <=' s'" "app i G rT s'"
+  
+  thus ?thesis 
+    by - (cases s, cases s', auto simp add: mono_Some)
 qed
     
+lemmas [simp del] = split_paired_Ex
+lemmas [simp] = step_def
 
-lemma step_mono:
-"\<lbrakk>succs i pc \<noteq> {}; app (i,G,rT,s2); G \<turnstile> s1 <=s s2\<rbrakk> \<Longrightarrow> 
-  G \<turnstile> the (step (i,G,s1)) <=s the (step (i,G,s2))"
+lemma step_mono_Some:
+"[| succs i pc \<noteq> []; app i G rT (Some s2); G \<turnstile> s1 <=s s2 |] ==>
+  G \<turnstile> the (step i G (Some s1)) <=s the (step i G (Some s2))"
 proof (cases s1, cases s2) 
   fix a1 b1 a2 b2
   assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
-  assume succs: "succs i pc \<noteq> {}"
-  assume app2: "app (i,G,rT,s2)"
+  assume succs: "succs i pc \<noteq> []"
+  assume app2: "app i G rT (Some s2)"
   assume G: "G \<turnstile> s1 <=s s2"
 
-  from G app2
-  have app1: "app (i,G,rT,s1)" by (rule app_mono)
-
-  from app1 app2 succs
+  hence "G \<turnstile> Some s1 <=' Some s2" 
+    by simp
+  from this app2
+  have app1: "app i G rT (Some s1)" by (rule app_mono)
+  
+  have "step i G (Some s1) \<noteq> None \<and> step i G (Some s2) \<noteq> None"
+    by simp
+  then 
   obtain a1' b1' a2' b2'
-    where step: "step (i,G,s1) = Some (a1',b1')" "step (i,G,s2) = Some (a2',b2')";
-    by (auto dest!: app_step_some);
+    where step: "step i G (Some s1) = Some (a1',b1')" 
+                "step i G (Some s2) = Some (a2',b2')"
+    by (auto simp del: step_def simp add: s)
 
   have "G \<turnstile> (a1',b1') <=s (a2',b2')"
   proof (cases (open) i)
@@ -313,11 +330,11 @@
 
     with s app1
     obtain y where
-       y:  "nat < length b1" "b1 ! nat = Some y" by clarsimp
+       y:  "nat < length b1" "b1 ! nat = Ok y" by clarsimp
 
     from Load s app2
     obtain y' where
-       y': "nat < length b2" "b2 ! nat = Some y'" by clarsimp
+       y': "nat < length b2" "b2 ! nat = Ok y'" by clarsimp
 
     from G s 
     have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_def)
@@ -446,6 +463,12 @@
   show ?thesis by auto  
 qed
 
+lemma step_mono:
+  "[| succs i pc \<noteq> []; app i G rT s2; G \<turnstile> s1 <=' s2 |] ==>
+  G \<turnstile> step i G s1 <=' step i G s2"
+  by (cases s1, cases s2, auto dest: step_mono_Some)
 
+lemmas [simp del] = step_def
 
 end
+