# HG changeset patch
# User kleing
# Date 966268999 -7200
# Node ID 42d11e0a7a8b40799da76cb87bdc8712321f2a70
# Parent  b732997cfc11306c9f94fd6b0b6c58443fbb77d3
Convert.thy now in Isar, tuned

diff -r b732997cfc11 -r 42d11e0a7a8b src/HOL/MicroJava/BV/BVSpecTypeSafe.ML
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.ML	Mon Aug 14 18:03:19 2000 +0200
@@ -4,7 +4,7 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-val defs1 = exec.simps@[split_def,sup_state_def,correct_state_def,
+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]
@@ -66,7 +66,7 @@
 \\\<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,sup_PTS_eq,map_eq_Cons]@defs1)) 1);
+	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))";
@@ -133,7 +133,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,map_eq_Cons]) 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);
 
@@ -164,7 +164,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,map_eq_Cons]) 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);
 
@@ -267,7 +267,7 @@
 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",sup_state_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [thm "wt_start_def",thm "sup_state_def"]) 1);
 by (Clarify_tac 1);
 
 (** approx_loc **)
diff -r b732997cfc11 -r 42d11e0a7a8b src/HOL/MicroJava/BV/Convert.ML
--- a/src/HOL/MicroJava/BV/Convert.ML	Mon Aug 14 14:57:29 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,246 +0,0 @@
-(*  Title:      HOL/MicroJava/BV/Convert.ML
-    ID:         $Id$
-    Author:     Cornelia Pusch
-    Copyright   1999 Technische Universitaet Muenchen
-*)
-
-
-Goalw[sup_ty_opt_def] "G \\<turnstile> t <=o t";
-by (case_tac "t" 1);
-by Auto_tac;
-qed "sup_ty_opt_refl";
-Addsimps [sup_ty_opt_refl];
-
-Goalw[sup_loc_def] "G \\<turnstile> t <=l t";
-by (induct_tac "t" 1);
-by Auto_tac;
-qed "sup_loc_refl";
-Addsimps [sup_loc_refl];
-
-Goalw[sup_state_def] "G \\<turnstile> s <=s s";
-by Auto_tac;
-qed "sup_state_refl";
-Addsimps [sup_state_refl];
-
-val widen_PrimT_conv1 =
- prove_typerel "(G \\<turnstile> PrimT x \\<preceq> T) = (T = PrimT x)"
- [ prove_widen_lemma "G\\<turnstile>S\\<preceq>T \\<Longrightarrow> S = PrimT x \\<longrightarrow> T = PrimT x"];
-Addsimps [widen_PrimT_conv1];
-
-Goalw [sup_ty_opt_def] "(G \\<turnstile> None <=o any) = (any = None)";
-by(simp_tac (simpset() addsplits [option.split]) 1);
-qed "anyConvNone";
-Addsimps [anyConvNone];
-
-Goalw [sup_ty_opt_def] "(G \\<turnstile> Some ty' <=o Some ty) = (G \\<turnstile> ty' \\<preceq> ty)";
-by(Simp_tac 1);
-qed "SomeanyConvSome";
-Addsimps [SomeanyConvSome];
-
-Goal
-"(G \\<turnstile> Some(PrimT Integer) <=o X) = (X=None \\<or> (X=Some(PrimT Integer)))";
-by (simp_tac (simpset() setloop (split_tac [ty.split,option.split]) addsimps [sup_ty_opt_def]) 1);
-qed "sup_PTS_eq";
-
-
-Goalw [sup_loc_def] "CFS \\<turnstile> [] <=l XT = (XT=[])";
-by(Simp_tac 1);
-qed "sup_loc_Nil";
-AddIffs [sup_loc_Nil];
-
-
-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(simp_tac (simpset() addsimps [list_all2_Cons1]) 1);
-qed "sup_loc_Cons";
-AddIffs [sup_loc_Cons];
-
-
-Goal "\\<forall> b. G \\<turnstile> a <=l b \\<longrightarrow> length a = length b";
-by (induct_tac "a" 1);
- by (Simp_tac 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "sup_loc_length";
-
-Goal "\\<forall> n b. (G \\<turnstile> a <=l b) \\<longrightarrow> n < length a \\<longrightarrow> (G \\<turnstile> (a!n) <=o (b!n))";
-by (induct_tac "a" 1);
- by (Simp_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "n" 1);
- by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("x","nat")] allE 1);
-by (smp_tac 1 1);
-by (Asm_full_simp_tac 1);
-qed_spec_mp "sup_loc_nth";
-
-Goalw[sup_state_def]
-"(G \\<turnstile> (x, y) <=s (a, b)) \\<Longrightarrow> length x = length a";
-by (Clarsimp_tac 1);
-bd sup_loc_length 1;
-by Auto_tac;
-qed "sup_state_length_fst";
-
-Goalw[sup_state_def] 
-"(G \\<turnstile> (x, y) <=s (a, b)) \\<longrightarrow> length y = length b";
-by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_length]) 1);
-qed "sup_state_length_snd";
-
-Goal "\\<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))";
-by (induct_tac "a" 1);
- by (Clarsimp_tac 1);
-by (Clarify_tac 1);
-by (case_tac "b" 1);
- by (Clarsimp_tac 1);  
-by (Clarsimp_tac 1);
-qed_spec_mp "sup_loc_append";
-
-
-Goalw[sup_state_def] 
-"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)))";
-by (auto_tac (claset(), simpset() addsimps [sup_loc_append]));
-qed "sup_state_append_snd";
-
-Goalw[sup_state_def]
-"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)))";
-by (auto_tac (claset(), simpset() addsimps [sup_loc_append]));
-qed "sup_state_append_fst";
-
-
-Goal "\\<forall> b. (G \\<turnstile> (rev a) <=l rev b) = (G \\<turnstile> a <=l b)";
-by (induct_tac "a" 1);
- by (Simp_tac 1);
-by (Clarsimp_tac 1);
-by Safe_tac;
- by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 2);
-by (case_tac "b" 1); 
- bd sup_loc_length 1;
- by (Clarsimp_tac 1);
-by (clarsimp_tac (claset(), simpset() addsimps [sup_loc_append, sup_loc_length]) 1);
-by (subgoal_tac "length (rev list) = length (rev lista)" 1);
- bd sup_loc_length 2;
- by (Clarsimp_tac 2);
-by (dres_inst_tac [("G","G"),("x","[a]"),("y","[aa]")] sup_loc_append 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "sup_loc_rev";
-
-Goalw[sup_state_def]
-"(G \\<turnstile> (rev a,x) <=s (rev b,y)) = (G \\<turnstile> (a,x) <=s (b,y))";
-by (auto_tac (claset(), simpset() addsimps [sup_loc_rev, rev_map RS sym]));
-qed "sup_state_rev_fst";
-
-Goal "map x a = Y # YT \\<longrightarrow> map x (tl a) = YT \\<and> x (hd a) = Y \\<and> (\\<exists> y yt. a = y#yt)";
-by (case_tac "a" 1);
-by Auto_tac;
-qed_spec_mp "map_hd_tl";
-
-Goalw[sup_state_def]
-"(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_tac;
-bd map_hd_tl 1;
-by Auto_tac;
-qed "sup_state_Cons1";
-
-Goalw [sup_loc_def]
-"CFS \\<turnstile> YT <=l (X#XT) = (\\<exists>Y YT'. YT=Y#YT' \\<and> CFS \\<turnstile> Y <=o X \\<and> CFS \\<turnstile> YT' <=l XT)";
-by(simp_tac (simpset() addsimps [list_all2_Cons2]) 1);
-qed "sup_loc_Cons2";
-
-Goalw[sup_state_def]
-"(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_tac (claset(), simpset() addsimps [sup_loc_Cons2]));
-bd map_hd_tl 1;
-by Auto_tac;
-qed "sup_state_Cons2"; 
-
-Goalw[sup_state_def] 
-"G \\<turnstile> (a, x) <=s (b, y) \\<Longrightarrow> G \\<turnstile> (c, x) <=s (c, y)";
-by Auto_tac;
-qed "sup_state_ignore_fst";
-
-Goalw[sup_ty_opt_def] 
-"\\<lbrakk>G \\<turnstile> a <=o b; G \\<turnstile> b <=o c\\<rbrakk> \\<Longrightarrow> G \\<turnstile> a <=o c";
-by (case_tac "c" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "a" 1);
- by (Clarsimp_tac 1);
- by (case_tac "b" 1);
-  by (Clarsimp_tac 1);
- by (Clarsimp_tac 1);
-by (case_tac "b" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-be widen_trans 1;
-ba 1;
-qed "sup_ty_opt_trans";
-
-Goal "\\<lbrakk>G \\<turnstile> a <=l b; G \\<turnstile> b <=l c\\<rbrakk> \\<Longrightarrow> \\<forall> n. n < length a \\<longrightarrow> G \\<turnstile> a!n <=o c!n";
-by (Clarify_tac 1);
-by (forward_tac [sup_loc_length] 1);
-bd sup_loc_nth 1;
- ba 1;
-bd sup_loc_nth 1;
- by (Force_tac 1);
-bd sup_ty_opt_trans 1;
- ba 1;
-ba 1;
-qed "sup_loc_all_trans";
-
-Goal "\\<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)";
-by (induct_tac "a" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (case_tac "b=[]" 1);
- by (Clarsimp_tac 1);
-by (Clarsimp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by (Clarify_tac 1);
-by (res_inst_tac [("x","y")] exI 1);
-by (res_inst_tac [("x","ys")] exI 1);
-by (eres_inst_tac [("x","ys")] allE 1);
-by (Full_simp_tac 1);
-by (Clarify_tac 1);
-be impE 1;
- by (Clarsimp_tac 1);
- by (eres_inst_tac [("x","Suc n")] allE 1);
- by (Clarsimp_tac 1);
-by (eres_inst_tac [("x","0")] allE 1);
-by (Clarsimp_tac 1);
-qed_spec_mp "all_nth_sup_loc";
-
-Goal "\\<lbrakk>G \\<turnstile> a <=l b; G \\<turnstile> b <=l c\\<rbrakk> \\<Longrightarrow> G \\<turnstile> a <=l c";
-by (forward_tac [sup_loc_all_trans] 1);
- ba 1;
-bd sup_loc_length 1;
-bd sup_loc_length 1;
-br all_nth_sup_loc 1;
- by (Clarsimp_tac 1);
-ba 1;
-qed "sup_loc_trans";
-
-Goalw[sup_state_def] 
-"\\<lbrakk>G \\<turnstile> a <=s b; G \\<turnstile> b <=s c\\<rbrakk> \\<Longrightarrow> G \\<turnstile> a <=s c";
-by Safe_tac;
- br sup_loc_trans 1;
-  ba 1;
- ba 1;
-br sup_loc_trans 1;
- ba 1;
-ba 1;
-qed "sup_state_trans";
-
-Goalw[sup_ty_opt_def] "G \\<turnstile> a <=o Some b \\<Longrightarrow> \\<exists> x. a = Some x";
-by (case_tac "a" 1);
- by Auto_tac;
-qed "sup_ty_opt_some";
-
-
-Goalw[sup_loc_def]
-"\\<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])";
-by (induct_tac "x" 1);
- by (Simp_tac 1);
-by (clarsimp_tac ((claset(), simpset()) addIffs [sup_loc_Cons2]) 1);
-by (case_tac "n" 1);
- by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
-by (clarsimp_tac (claset(), simpset() addsimps [list_all2_Cons1]) 1);
-qed_spec_mp "sup_loc_update";
diff -r b732997cfc11 -r 42d11e0a7a8b src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy	Mon Aug 14 18:03:19 2000 +0200
@@ -6,27 +6,357 @@
 The supertype relation lifted to type options, type lists and state types.
 *)
 
-Convert = JVMExec + 
+theory Convert = JVMExec:
 
 types
- locvars_type = ty option list
- opstack_type = ty list
- state_type   = "opstack_type \\<times> locvars_type"
+ locvars_type = "ty option list"
+ opstack_type = "ty list"
+ state_type   = "opstack_type \<times> locvars_type"
 
 constdefs
 
- sup_ty_opt :: "['code prog,ty option,ty option] \\<Rightarrow> bool" ("_ \\<turnstile>_ <=o _")
- "G \\<turnstile> a' <=o a \\<equiv>
-    case a of
-      None \\<Rightarrow> True
-    | Some t  \\<Rightarrow>  case a' of 
-		     None \\<Rightarrow> False
-		   | Some t' \\<Rightarrow> G \\<turnstile> t' \\<preceq> t" 
+  (* 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)"
+  "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)"
+
+
+ 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')"
+
+ 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 lift_top_refl [simp]:
+  "[| !!x. P x x |] ==> lift_top P x x"
+  by (simp add: lift_top_def split: option.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"
+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" 
+    hence ?thesis by (simp add: lift_top_def)
+  } note z_none = this
+
+  { assume "x = None"
+    with a b
+    have ?thesis
+      by (simp add: lift_top_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_top_def split: option.splits)
+    
+    from a x y
+    have "P r s" by (simp add: lift_top_def)
+    also
+    from b y z
+    have "P s t" by (simp add: lift_top_def)
+    finally 
+    have "P r t" .
+
+    with x z
+    have ?thesis by (simp add: lift_top_def)
+  } 
+
+  with x_none z_none
+  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_Some_Some [simp]:
+  "lift_top P (Some a) (Some b) = P a b"
+  by (simp add: lift_top_def split: option.splits)
+
+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)
+
+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)
+
+
+
+theorem sup_ty_opt_refl [simp]:
+  "G \<turnstile> t <=o t"
+  by (simp add: sup_ty_opt_def)
+
+theorem sup_loc_refl [simp]:
+  "G \<turnstile> t <=l t"
+  by (induct t, auto simp add: sup_loc_def)
+
+theorem sup_state_refl [simp]:
+  "G \<turnstile> s <=s s"
+  by (simp add: sup_state_def)
+
+
+
+theorem anyConvNone [simp]:
+  "(G \<turnstile> None <=o any) = (any = None)"
+  by (simp add: sup_ty_opt_def)
+
+theorem SomeanyConvSome [simp]:
+  "(G \<turnstile> (Some ty') <=o (Some 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"
+  by (clarsimp simp add: sup_ty_opt_def)
+
+lemma widen_PrimT_conv1 [simp]:
+  "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x"
+  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)
+
+
+
+theorem sup_loc_Nil [iff]:
+  "(G \<turnstile> [] <=l XT) = (XT=[])"
+  by (simp add: sup_loc_def)
+
+theorem sup_loc_Cons [iff]:
+  "(G \<turnstile> (Y#YT) <=l XT) = (\<exists>X XT'. XT=X#XT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT <=l XT'))"
+  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))";
+  by (simp add: sup_loc_def list_all2_Cons2)
+
+
+theorem sup_loc_length:
+  "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
+proof -
+  assume G: "G \<turnstile> a <=l b"
+  have "\<forall> b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
+    by (induct a, auto)
+  with G
+  show ?thesis by blast
+qed
+
+theorem sup_loc_nth:
+  "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)"
+proof -
+  assume a: "G \<turnstile> a <=l b" "n < length a"
+  have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
+    (is "?P a")
+  proof (induct a)
+    show "?P []" by simp
+    
+    fix x xs assume IH: "?P xs"
+
+    show "?P (x#xs)"
+    proof (intro strip)
+      fix n b
+      assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)"
+      with IH
+      show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)"
+        by - (cases n, auto)
+    qed
+  qed
+  with a
+  show ?thesis by blast
+qed
+
+
+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")
+proof (induct a)
+  show "?P []" by simp
 
- sup_loc :: "['code prog,locvars_type,locvars_type] \\<Rightarrow> bool"	  ("_ \\<turnstile> _ <=l _"  [71,71] 70)
- "G \\<turnstile> LT <=l LT' \\<equiv> list_all2 (%t t'. G \\<turnstile> t <=o t') LT LT'"
+  fix l ls assume IH: "?P ls"
+  
+  show "?P (l#ls)"
+  proof (intro strip)
+    fix b
+    assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
+    assume l: "length (l#ls) = length b"
+    
+    then obtain b' bs where b: "b = b'#bs"
+      by - (cases b, simp, simp add: neq_Nil_conv, rule that)
+
+    with f
+    have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
+      by auto
+
+    with f b l IH
+    show "G \<turnstile> (l # ls) <=l b"
+      by auto
+  qed
+qed
+
+
+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))"
+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") 
+  proof (induct a)
+    show "?P []" by simp
+    
+    fix l ls assume IH: "?P ls"    
+    show "?P (l#ls)" 
+    proof (intro strip)
+      fix b
+      assume "length (l#ls) = length (b::ty option 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)
+    qed
+  qed
+  with l
+  show ?thesis by blast
+qed
+
+theorem sup_loc_rev [simp]:
+  "(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)"
+proof -
+  have "\<forall>b. (G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" (is "\<forall>b. ?Q a b" is "?P a")
+  proof (induct a)
+    show "?P []" by simp
+
+    fix l ls assume IH: "?P ls"
+
+    { 
+      fix b
+      have "?Q (l#ls) b"
+      proof (cases b)
+        case Nil
+        thus ?thesis by (auto dest: sup_loc_length)
+      next
+        case Cons 
+        show ?thesis
+        proof
+          assume "G \<turnstile> (l # ls) <=l b"
+          thus "G \<turnstile> rev (l # ls) <=l rev b"
+            by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append)
+        next
+          assume "G \<turnstile> rev (l # ls) <=l rev b"
+          hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])"
+            by (simp add: Cons)          
+          
+          hence "length (rev ls) = length (rev list)"
+            by (auto dest: sup_loc_length)
+
+          from this G
+          obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a"
+            by (simp add: sup_loc_append)
+
+          thus "G \<turnstile> (l # ls) <=l b"
+            by (simp add: Cons IH)
+        qed
+      qed    
+    }
+    thus "?P (l#ls)" by blast
+  qed
 
- 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'"
+  thus ?thesis by blast
+qed
+
+
+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")
+proof (induct x)
+  show "?P []" by simp
+
+  fix l ls assume IH: "?P ls"
+  show "?P (l#ls)"
+  proof (intro strip)
+    fix n y
+    assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y"
+    with IH
+    show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]"
+      by - (cases n, auto simp add: sup_loc_Cons2 list_all2_Cons1)
+  qed
+qed
+
+
+theorem sup_state_length [simp]:
+  "G \<turnstile> s2 <=s s1 \<Longrightarrow> 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)))"
+  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)))"
+  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)))"
+  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)))"
+  by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2)
+
+theorem sup_state_ignore_fst:  
+  "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
+  by (simp add: sup_state_def)
+
+theorem sup_state_rev_fst:
+  "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
+proof -
+  have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
+  show ?thesis by (simp add: m sup_state_def)
+qed
+  
+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 -
+  assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
+ 
+  hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
+  proof (intro strip)
+    fix n 
+    assume n: "n < length a"
+    with G
+    have "G \<turnstile> (a!n) <=o (b!n)"
+      by - (rule sup_loc_nth)
+    also 
+    from n G
+    have "G \<turnstile> ... <=o (c!n)"
+      by - (rule sup_loc_nth, auto dest: sup_loc_length)
+    finally
+    show "G \<turnstile> (a!n) <=o (c!n)" .
+  qed
+
+  with G
+  show ?thesis 
+    by (auto intro!: all_nth_sup_loc [rulify] dest!: sup_loc_length) 
+qed
+  
+
+theorem sup_state_trans [trans]:
+  "\<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)
 
 end
diff -r b732997cfc11 -r 42d11e0a7a8b src/HOL/MicroJava/BV/Correct.ML
--- a/src/HOL/MicroJava/BV/Correct.ML	Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.ML	Mon Aug 14 18:03:19 2000 +0200
@@ -41,7 +41,7 @@
 "\\<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 (Asm_simp_tac 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";
 
@@ -63,7 +63,7 @@
 
 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 [sup_PTS_eq,approx_val_def] addsplits [option.split,val_.split,ty.split]) 1);
+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";
 
@@ -104,7 +104,7 @@
 qed_spec_mp "approx_loc_imp_approx_loc_sup_heap";
 
 
-Goalw [sup_loc_def,approx_loc_def,list_all2_def]
+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()));
diff -r b732997cfc11 -r 42d11e0a7a8b src/HOL/MicroJava/BV/LBVComplete.thy
--- a/src/HOL/MicroJava/BV/LBVComplete.thy	Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Mon Aug 14 18:03:19 2000 +0200
@@ -475,13 +475,15 @@
   
 
 lemma fits_imp_wtl_method_complete:
-"\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\<rbrakk> \<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
-by (simp add: wt_method_def wtl_method_def del: split_paired_Ex)
-   (rule wt_imp_wtl_inst_list [rulify, elimify], auto simp add: wt_start_def simp del: split_paired_Ex) 
+"\<lbrakk>wt_method G C pTs rT mxl ins phi; fits ins cert phi; wf_prog wf_mb G\<rbrakk> 
+  \<Longrightarrow> wtl_method G C pTs rT mxl ins cert"
+by (simp add: wt_method_def wtl_method_def)
+   (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)"
+"\<lbrakk>wt_method G C pTs rT mxl ins phi; wf_prog wf_mb G\<rbrakk> 
+  \<Longrightarrow> wtl_method G C pTs rT mxl ins (make_cert ins phi)"
 proof -
   assume * : "wt_method G C pTs rT mxl ins phi" "wf_prog wf_mb G"
   
diff -r b732997cfc11 -r 42d11e0a7a8b src/HOL/MicroJava/BV/Step.thy
--- a/src/HOL/MicroJava/BV/Step.thy	Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/Step.thy	Mon Aug 14 18:03:19 2000 +0200
@@ -10,7 +10,7 @@
 theory Step = Convert :
 
 
-text "Effect of instruction on the state type"
+text "Effect of instruction on the state type:"
 consts 
 step :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type option"
 
@@ -39,7 +39,7 @@
 "step (i,G,s)                           = None"
 
 
-text "Conditions under which step is applicable"
+text "Conditions under which step is applicable:"
 consts
 app :: "instr \<times> jvm_prog \<times> ty \<times> state_type \<Rightarrow> bool"
 
@@ -84,7 +84,7 @@
 "app (i,G,rT,s)                            = False"
 
 
-text {* \verb,p_count, of successor instructions *}
+text {* program counter of successor instructions: *}
 
 consts
 succs :: "instr \<Rightarrow> p_count \<Rightarrow> p_count set"
@@ -134,10 +134,8 @@
 
 text {* 
 \medskip
-simp rules for @{term app} without patterns, better suited for proofs
-\medskip
+simp rules for \isa{app} without patterns, better suited for proofs:
 *}
-
 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)
diff -r b732997cfc11 -r 42d11e0a7a8b src/HOL/MicroJava/BV/StepMono.thy
--- a/src/HOL/MicroJava/BV/StepMono.thy	Mon Aug 14 14:57:29 2000 +0200
+++ b/src/HOL/MicroJava/BV/StepMono.thy	Mon Aug 14 18:03:19 2000 +0200
@@ -4,34 +4,13 @@
     Copyright   2000 Technische Universitaet Muenchen
 *)
 
-header {* Monotonicity of \texttt{step} and \texttt{app} *}
-
-theory StepMono = Step :
-
+header {* Monotonicity of step and app *}
 
-lemmas [trans] = sup_state_trans sup_loc_trans widen_trans
-
+theory StepMono = Step:
 
-lemma sup_state_length:
-"G \<turnstile> s2 <=s s1 \<Longrightarrow> length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
-  by (cases s1, cases s2, simp add: sup_state_length_fst sup_state_length_snd)
-  
 
 lemma PrimT_PrimT: "(G \<turnstile> xb \<preceq> PrimT p) = (xb = PrimT p)"
-proof
-  show "xb = PrimT p \<Longrightarrow> G \<turnstile> xb \<preceq> PrimT p" by blast
-
-  show "G\<turnstile> xb \<preceq> PrimT p \<Longrightarrow> xb = PrimT p"
-  proof (cases xb)
-    fix prim
-    assume "xb = PrimT prim" "G\<turnstile>xb\<preceq>PrimT p"
-    thus ?thesis by simp
-  next
-    fix ref
-    assume "G\<turnstile>xb\<preceq>PrimT p" "xb = RefT ref"
-    thus ?thesis by simp (rule widen_RefT [elimify], auto)
-  qed
-qed
+  by (auto elim: widen.elims)
 
 
 lemma sup_loc_some [rulify]:
@@ -50,7 +29,7 @@
     show "(\<exists>t. (a # list) ! n = Some t) \<and> G \<turnstile>(a # list) ! n <=o Some t" 
     proof (cases n) 
       case 0
-      with * show ?thesis by (simp add: sup_ty_opt_some)
+      with * show ?thesis by (simp add: sup_ty_opt_Some)
     next
       case Suc
       with Cons *
@@ -159,7 +138,7 @@
     with G app
     show ?thesis
       by - (cases s2,
-            auto dest: map_hd_tl simp add: sup_loc_Cons2 sup_loc_length sup_state_def)
+            auto simp add: map_eq_Cons sup_loc_Cons2 sup_loc_length sup_state_def)
   next
     case Bipush
     thus ?thesis by simp