# HG changeset patch
# User nipkow
# Date 947689096 -3600
# Node ID 60b606eddec8342ec50000217b05b0d3e3efa62d
# Parent  746c5cf09bde6fbb0c9e4ba476983cfb2b4bac36
Move some lemmas to List.

diff -r 746c5cf09bde -r 60b606eddec8 src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Wed Jan 12 15:58:01 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Wed Jan 12 15:58:16 2000 +0100
@@ -32,10 +32,9 @@
 \\\<Longrightarrow> G,phi \\<turnstile>JVM state'\\<surd>";
 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 [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+	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); \
@@ -44,9 +43,8 @@
 \  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() addDs [approx_stk_Cons_lemma]
-	addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_subst RSN(2, approx_loc_imp_approx_loc_sup)]
-	addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+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";
@@ -63,7 +61,7 @@
 \  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 [approx_val_def,sup_PTS_eq,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
+	addss (simpset() addsimps [approx_val_def,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))";
@@ -87,7 +85,7 @@
 \  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 [approx_val_Null,NT_subtype_conv,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
+	addss (simpset() addsimps [approx_val_Null,NT_subtype_conv,map_eq_Cons]@defs1)) 1);
 qed "Aconst_null_correct";
 
 
@@ -133,11 +131,10 @@
 \  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 [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,
+by (asm_full_simp_tac (simpset() addsimps [map_eq_Cons,
 		raise_xcpt_def]@defs1 addsplits [option.split]) 1);
-by (fast_tac (claset() addDs [approx_stk_Cons_lemma] 
-	addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup,Cast_conf2] 
-	addss (simpset() addsimps [sup_loc_Cons,map_eq_Cons,approx_stk_Cons,approx_val_def])) 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";
 
 
@@ -169,9 +166,7 @@
 \\\<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 [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
-by (Clarify_tac 1);
-bd approx_stk_Cons_lemma 1;
+by (asm_full_simp_tac (simpset() addsimps [sup_state_def,map_eq_Cons]) 1);
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
 
@@ -182,19 +177,13 @@
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps []) 1);
 
-(* approx_stk *)
 br conjI 1;
-by  (asm_full_simp_tac (simpset() addsimps [approx_stk_Cons]) 1);
-br  conjI 1;
-by   (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup]) 1);
-by  (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
-bd  widen_cfs_fields 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 [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);
 
-(* approx_loc *)
-by (fast_tac (claset() addIs [approx_loc_imp_approx_loc_sup]) 1);
 qed "Getfield_correct";
 
 
@@ -208,11 +197,7 @@
 \\\<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 [sup_state_def,sup_loc_Cons,map_eq_Cons]) 1);
-by (Clarify_tac 1);
-bd approx_stk_Cons_lemma 1;
-by (Clarify_tac 1);
-bd approx_stk_Cons_lemma 1;
+by (asm_full_simp_tac (simpset() addsimps [sup_state_def,map_eq_Cons]) 1);
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
 
@@ -262,8 +247,8 @@
 		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_stk_Cons,approx_val_def,conf_def,
-		fun_upd_apply,sup_loc_Cons,map_eq_Cons,is_class_def,raise_xcpt_def,init_vars_def]@defs1 
+	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";
 
@@ -301,9 +286,6 @@
 by (asm_full_simp_tac (simpset() addsimps []@defs1) 1);
 bd approx_stk_append_lemma 1;   
 by (Clarify_tac 1);
-bd approx_stk_Cons_lemma 1;
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [approx_val_def]) 1);
 bd conf_RefTD 1;
 by (Clarify_tac 1);
@@ -332,17 +314,12 @@
 by (asm_full_simp_tac (simpset() addsimps [wt_start_def,sup_state_def]) 1);
 by (Clarify_tac 1);
 
-(** approx_stk **)
-br conjI 1;
- by (asm_full_simp_tac (simpset() addsimps [sup_loc_Nil,approx_stk_Nil]) 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_loc_Cons,approx_val_def,approx_loc_append]) 1);
+ 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;
@@ -350,8 +327,8 @@
   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_loc_Cons,approx_val_def])) 1);
- by (asm_simp_tac (simpset() addsimps [split_def,approx_loc_def,zip_replicate,approx_val_None,set_replicate_conv_if]) 1);
+	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);
@@ -361,7 +338,7 @@
  by(Blast_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,sup_loc_Cons])) 1);
+       addss (simpset()addsimps [map_eq_Cons])) 1);
 qed "Invoke_correct";
 
 Goal
@@ -380,16 +357,6 @@
 
 (****** MR ******)
 
-Goal
- "\\<forall>zs. (xs@ys = zs) = (xs = take (length xs) zs \\<and> ys = drop (length xs) zs)";
-by(induct_tac "xs" 1);
-by(Simp_tac 1);
-by(Asm_full_simp_tac 1);
-by(Clarify_tac 1);
-by(exhaust_tac "zs" 1);
-by(Auto_tac);
-qed_spec_mp "append_eq_conv_conj";
-
 Delsimps [map_append];
 Goal
 "\\<lbrakk> wt_jvm_prog G phi; \
@@ -401,18 +368,17 @@
 \\\<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 [sup_loc_Cons,map_eq_Cons]@defs1) 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 [wt_jvm_prog_impl_wt_instr] 1);
   by(EVERY1[atac, etac Suc_lessD]);
 by(rewtac wt_jvm_prog_def);
 by (fast_tac (claset()
- addDs [approx_stk_Cons_lemma,subcls_widen_methd]
+ addDs [subcls_widen_methd]
  addEs [rotate_prems 1 widen_trans]
- addIs [conf_widen] 
-	addss (simpset()
- addsimps [approx_val_def,append_eq_conv_conj,sup_loc_Cons,map_eq_Cons,approx_stk_Cons]@defs1)) 1);
+ addIs [conf_widen]
+ addss (simpset() addsimps [approx_val_def,append_eq_conv_conj,map_eq_Cons]@defs1)) 1);
 qed "Return_correct";
 Addsimps [map_append];
 
@@ -452,8 +418,7 @@
 \  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() addDs [approx_stk_Cons_lemma] 
-	addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
+by (fast_tac (claset() addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
 qed "Ifiacmpeq_correct";
 
 
@@ -483,8 +448,7 @@
 \  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() addDs [approx_stk_Cons_lemma] 
-	addIs [approx_stk_imp_approx_stk_sup,approx_loc_imp_approx_loc_sup] addss (simpset() addsimps defs1)) 1);
+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";
 
 
@@ -496,9 +460,8 @@
 \  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() addDs [approx_stk_Cons_lemma]
-	addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
-	addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+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";
 
 
@@ -510,9 +473,8 @@
 \  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() addDs [approx_stk_Cons_lemma]
-	addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
-	addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+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 
@@ -523,9 +485,8 @@
 \  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() addDs [approx_stk_Cons_lemma]
-	addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
-	addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+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 
@@ -536,9 +497,8 @@
 \  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() addDs [approx_stk_Cons_lemma] 
-	addIs [approx_stk_imp_approx_stk_sup,approx_val_imp_approx_val_sup,approx_loc_imp_approx_loc_sup] 
-	addss (simpset() addsimps [approx_stk_Cons,sup_loc_Cons,map_eq_Cons]@defs1)) 1);
+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
diff -r 746c5cf09bde -r 60b606eddec8 src/HOL/MicroJava/BV/Convert.ML
--- a/src/HOL/MicroJava/BV/Convert.ML	Wed Jan 12 15:58:01 2000 +0100
+++ b/src/HOL/MicroJava/BV/Convert.ML	Wed Jan 12 15:58:16 2000 +0100
@@ -26,16 +26,14 @@
 
 
 
-Goal
-"CFS \\<turnstile> [] <=l XT = (XT=[])";
-by (case_tac "XT=[]" 1);
-by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
-by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
+Goalw [sup_loc_def] "CFS \\<turnstile> [] <=l XT = (XT=[])";
+by(Simp_tac 1);
 qed "sup_loc_Nil";
+AddIffs [sup_loc_Nil];
+
 
-Goal
+Goalw [sup_loc_def]
 "CFS \\<turnstile> (Y#YT) <=l XT = (\\<exists>X XT'. XT=X#XT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT <=l XT')";
-by (case_tac "XT=[]" 1);
-by (asm_simp_tac (simpset() addsimps [sup_loc_def]) 1);
-by (fast_tac (claset() addss (simpset() addsimps [sup_loc_def,neq_Nil_conv])) 1);
+by(simp_tac (simpset() addsimps [list_all2_Cons1]) 1);
 qed "sup_loc_Cons";
+AddIffs [sup_loc_Cons];
diff -r 746c5cf09bde -r 60b606eddec8 src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Wed Jan 12 15:58:01 2000 +0100
+++ b/src/HOL/MicroJava/BV/Convert.thy	Wed Jan 12 15:58:16 2000 +0100
@@ -24,8 +24,7 @@
 		   | Some t' \\<Rightarrow> 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> (length LT=length LT') \\<and> (\\<forall>(t,t')\\<in>set (zip LT LT'). G \\<turnstile> t <=o t')"
-
+ "G \\<turnstile> LT <=l LT' \\<equiv> list_all2 (%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'"
diff -r 746c5cf09bde -r 60b606eddec8 src/HOL/MicroJava/BV/Correct.ML
--- a/src/HOL/MicroJava/BV/Correct.ML	Wed Jan 12 15:58:01 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.ML	Wed Jan 12 15:58:16 2000 +0100
@@ -68,24 +68,25 @@
 qed_spec_mp "approx_val_imp_approx_val_sup";
 
 
-Goal 
+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,approx_loc_def,all_set_conv_all_nth])) 1);
+	[split_def,all_set_conv_all_nth])) 1);
 qed "approx_loc_imp_approx_val_sup";
 
 
 (** approx_loc **)
 
-Goal 
+Goalw [approx_loc_def]
 "approx_loc G hp (s#xs) (l#ls) = \
-\   ((length xs = length ls) \\<and> (approx_val G hp s l) \\<and> (approx_loc G hp xs ls))";
-by (fast_tac (claset() addss (simpset() addsimps [approx_loc_def])) 1);
+\   (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]
+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)";
@@ -94,7 +95,7 @@
 qed_spec_mp "assConv_approx_stk_imp_approx_loc";
 
 
-Goalw [approx_loc_def]
+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 (exhaust_tac "lt" 1);
  by (Asm_simp_tac 1);
@@ -103,14 +104,14 @@
 qed_spec_mp "approx_loc_imp_approx_loc_sup_heap";
 
 
-Goalw [sup_loc_def,approx_loc_def]
+Goalw [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]
+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 RS subsetD]
@@ -118,26 +119,17 @@
 qed_spec_mp "approx_loc_imp_approx_loc_subst";
 
 
-Goal 
+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 (induct_tac "l1" 1);
- by (fast_tac (claset() addDs [] addss (simpset() addsimps [approx_loc_def])) 1);
-br allI 1;
-by (exhaust_tac "L1" 1);
- by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [approx_loc_Cons]) 1);
-by (case_tac "length l2 = length L2" 1);
- by (asm_full_simp_tac (simpset() addsimps []) 1);
-by (asm_full_simp_tac (simpset() addsimps [approx_loc_def]) 1);
+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]
+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";
@@ -160,39 +152,29 @@
 
 Goalw [approx_stk_def,approx_loc_def]
 "approx_stk G hp [] []";
-by (asm_full_simp_tac (simpset() addsimps []) 1);
+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 (x # stk) (S#ST) = (approx_stk G hp stk ST \\<and> approx_val G hp x (Some S))";
-by (fast_tac (claset() addss (simpset())) 1);
-qed "approx_stk_Cons";
-
-Goal 
-"\\<lbrakk> approx_stk G hp stk (S#ST') \\<rbrakk> \
-\ \\<Longrightarrow> \\<exists>s stk'. stk = s#stk' \\<and> approx_stk G hp stk' ST' \\<and> approx_val G hp s (Some S)";
-by (exhaust_tac "stk" 1);
- by (fast_tac (claset() addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
-by (fast_tac (claset() addss (simpset() addsimps [approx_stk_Cons])) 1);
-qed "approx_stk_Cons_lemma";
-
-Goal 
-"\\<forall>ST' stk. 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 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 (induct_tac "S" 1);
- by (fast_tac (claset() addDs [] addss (simpset() addsimps [approx_stk_def,approx_loc_def])) 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps []) 1);
-bd approx_stk_Cons_lemma 1;
-by (Clarify_tac 1);
-by (eres_inst_tac [("x","ST'")] allE 1);
-by (eres_inst_tac [("x","stk'")] allE 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("x","s#sa")] exI 1);
-by (res_inst_tac [("x","stk'a")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [approx_stk_Cons]) 1);
+by(asm_full_simp_tac (simpset() addsimps [list_all2_append2]) 1);
 qed_spec_mp "approx_stk_append_lemma";
 
 
diff -r 746c5cf09bde -r 60b606eddec8 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Jan 12 15:58:01 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Wed Jan 12 15:58:16 2000 +0100
@@ -13,8 +13,7 @@
 "approx_val G h v any \\<equiv> case any of None \\<Rightarrow> True | Some 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> 
-   length loc=length LT \\<and> (\\<forall>(val,any)\\<in>set (zip loc LT). approx_val G hp val any)" 
+"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 Some ST)"