# HG changeset patch
# User wenzelm
# Date 1376385206 -7200
# Node ID 3295927cf777dcc1fefa6e9177ee5b56eeac3309
# Parent  9a47c82560549c6a3b56755f5878732e644333df
tuned proofs;

diff -r 9a47c8256054 -r 3295927cf777 src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Aug 13 10:29:49 2013 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Aug 13 11:13:26 2013 +0200
@@ -22,13 +22,13 @@
 
 lemma app'Store[simp]:
   "app' (Store idx, G, pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST' \<and> idx < length LT)"
-  by (cases ST, auto)
+  by (cases ST) auto
 
 lemma app'GetField[simp]:
   "app' (Getfield F C, G, pc, maxs, rT, (ST,LT)) =  
   (\<exists>oT vT ST'. ST = oT#ST' \<and> is_class G C \<and>  
   field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> Class C)"
-  by (cases ST, auto)
+  by (cases ST) auto
 
 lemma app'PutField[simp]:
 "app' (Putfield F C, G,  pc, maxs, rT, (ST,LT)) = 
@@ -61,13 +61,13 @@
 
 lemma app'Pop[simp]: 
   "app' (Pop, G, pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST')"
-  by (cases ST, auto)
+  by (cases ST) auto
 
 
 lemma app'Dup[simp]:
   "app' (Dup, G, pc, maxs, rT, (ST,LT)) =
   (\<exists>T ST'. ST = T#ST' \<and> length ST < maxs)"
-  by (cases ST, auto)
+  by (cases ST) auto
  
 
 lemma app'Dup_x1[simp]:
@@ -125,13 +125,14 @@
 lemma app'Return[simp]:
   "app' (Return, G, pc, maxs, rT, (ST,LT)) = 
   (\<exists>T ST'. ST = T#ST'\<and> G \<turnstile> T \<preceq> rT)" 
-  by (cases ST, auto)
+  by (cases ST) auto
 
 
 lemma app'Throw[simp]:
   "app' (Throw, G, pc, maxs, rT, (ST,LT)) = 
   (\<exists>ST' r. ST = RefT r#ST')"
-  apply (cases ST, simp)
+  apply (cases ST)
+  apply simp
   apply (cases "hd ST")
   apply auto
   done
@@ -170,7 +171,7 @@
   with app
   show "?P ST LT"
     apply (clarsimp simp add: list_all2_def)
-    apply ((rule exI)+, (rule conjI)?)+
+    apply (intro exI conjI)
     apply auto
     done
 qed
@@ -198,9 +199,8 @@
   done
 
 lemma list_all2_approx:
-  "\<And>s. list_all2 (approx_val G hp) s (map OK S) = 
-       list_all2 (conf G hp) s S"
-  apply (induct S)
+  "list_all2 (approx_val G hp) s (map OK S) = list_all2 (conf G hp) s S"
+  apply (induct S arbitrary: s)
   apply (auto simp add: list_all2_Cons2 approx_val_def)
   done
 
diff -r 9a47c8256054 -r 3295927cf777 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Tue Aug 13 10:29:49 2013 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Tue Aug 13 11:13:26 2013 +0200
@@ -65,9 +65,7 @@
 
 lemma sup_ty_opt_OK:
   "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
-  apply (cases X)
-  apply auto
-  done
+  by (cases X) auto
 
 
 section {* approx-val *}
@@ -91,12 +89,12 @@
 lemma approx_val_heap_update:
   "\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
   \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
-  by (cases v, auto simp add: obj_ty_def conf_def)
+  by (cases v) (auto simp add: obj_ty_def conf_def)
 
 lemma approx_val_widen:
   "\<lbrakk> approx_val G hp v T; G \<turnstile> T <=o T'; wf_prog wt G \<rbrakk>
   \<Longrightarrow> approx_val G hp v T'"
-  by (cases T', auto simp add: sup_ty_opt_OK intro: conf_widen)
+  by (cases T') (auto simp add: sup_ty_opt_OK intro: conf_widen)
 
 section {* approx-loc *}
 
@@ -284,7 +282,7 @@
   shows preallocated_newref: "preallocated (hp(oref\<mapsto>obj))"
 proof (cases oref)
   case (XcptRef x) 
-  with none alloc have "False" by (auto elim: preallocatedE [of _ x])
+  with none alloc have False by (auto elim: preallocatedE [of _ x])
   thus ?thesis ..
 next
   case (Loc l)