# HG changeset patch
# User wenzelm
# Date 1194633450 -3600
# Node ID 8d06e11a01d180537ca424ddfee09395f396fc4d
# Parent  1aa441e4849633513f8bc3ba2eb59e6a5ee8ffdf
tuned proofs -- avoid open cases;

diff -r 1aa441e48496 -r 8d06e11a01d1 src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Fri Nov 09 18:59:56 2007 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Fri Nov 09 19:37:30 2007 +0100
@@ -304,16 +304,16 @@
 
 lemma appSwap[simp]:
 "app Swap G maxs rT pc et (Some s) = (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))" 
-  by (cases s, cases "2 <length (fst s)", auto dest: 1 2)
+  by (cases s, cases "2 <length (fst s)") (auto dest: 1 2)
 
 
 lemma appIAdd[simp]:
 "app IAdd G maxs rT pc et (Some s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))"
   (is "?app s = ?P s")
-proof (cases (open) s)
-  case Pair
+proof (cases s)
+  case (Pair a b)
   have "?app (a,b) = ?P (a,b)"
-  proof (cases "a")
+  proof (cases a)
     fix t ts assume a: "a = t#ts"
     show ?thesis
     proof (cases t)
@@ -328,7 +328,7 @@
           proof (cases t')
             fix p' assume "t' = PrimT p'"
             with t' ip p a
-            show ?thesis by - (cases p', auto)
+            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)
@@ -363,9 +363,9 @@
   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') \<and> 
   (\<forall>C \<in> set (match_any G pc et). is_class G C))" (is "?app s = ?P s")
-proof (cases (open) s)
+proof (cases s)
   note list_all2_def [simp]
-  case Pair
+  case (Pair a b)
   have "?app (a,b) \<Longrightarrow> ?P (a,b)"
   proof -
     assume app: "?app (a,b)"
diff -r 1aa441e48496 -r 8d06e11a01d1 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Fri Nov 09 18:59:56 2007 +0100
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Fri Nov 09 19:37:30 2007 +0100
@@ -16,14 +16,14 @@
 lemma sup_loc_some [rule_format]:
 "\<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)
+proof (induct ?P b)
   show "?P []" by simp
-
-  case Cons
+next
+  case (Cons a list)
   show "?P (a#list)" 
   proof (clarsimp simp add: list_all2_Cons1 sup_loc_def Listn.le_def lesub_def)
     fix z zs n
-    assume * : 
+    assume *: 
       "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs" 
       "n < Suc (length list)" "(z # zs) ! n = OK t"
 
@@ -61,9 +61,9 @@
 
 lemma append_length_n [rule_format]: 
 "\<forall>n. n \<le> length x \<longrightarrow> (\<exists>a b. x = a@b \<and> length a = n)" (is "?P x")
-proof (induct (open) ?P x)
+proof (induct ?P x)
   show "?P []" by simp
-
+next
   fix l ls assume Cons: "?P ls"
 
   show "?P (l#ls)"
@@ -119,7 +119,7 @@
     note [simp] = sup_loc_length sup_loc_length_map
 
     have "app i G m rT pc et (Some s2)"
-    proof (cases (open) i)
+    proof (cases i)
       case Load
     
       from G Load app
@@ -130,19 +130,19 @@
     next
       case Store
       with G app show ?thesis
-        by (cases s2, auto simp add: sup_loc_Cons2 sup_state_conv)
+        by (cases s2) (auto simp add: sup_loc_Cons2 sup_state_conv)
     next
       case LitPush
-      with G app show ?thesis by (cases s2, auto simp add: sup_state_conv)
+      with G app show ?thesis by (cases s2) (auto simp add: sup_state_conv)
     next
       case New
-      with G app show ?thesis by (cases s2, auto simp add: sup_state_conv)
+      with G app show ?thesis by (cases s2) (auto simp add: sup_state_conv)
     next
       case Getfield
       with app G show ?thesis
         by (cases s2) (clarsimp simp add: sup_state_Cons2, rule widen_trans) 
     next
-      case Putfield
+      case (Putfield vname cname)
       
       with app 
       obtain vT oT ST LT b
@@ -171,7 +171,7 @@
     next
       case Checkcast
       with app G show ?thesis 
-        by (cases s2, auto intro!: widen_RefT2 simp add: sup_state_Cons2)
+        by (cases s2) (auto intro!: widen_RefT2 simp add: sup_state_Cons2)
     next
       case Return
       with app G show ?thesis
@@ -179,39 +179,39 @@
     next
       case Pop
       with app G show ?thesis
-        by (cases s2, clarsimp simp add: sup_state_Cons2)
+        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,
+        by (cases s2) (clarsimp simp add: sup_state_Cons2,
             auto dest: sup_state_length)
     next
       case Dup_x1
       with app G show ?thesis
-        by (cases s2, clarsimp simp add: sup_state_Cons2, 
+        by (cases s2) (clarsimp simp add: sup_state_Cons2, 
             auto dest: sup_state_length)
     next
       case Dup_x2
       with app G show ?thesis
-        by (cases s2, clarsimp simp add: sup_state_Cons2,
+        by (cases s2) (clarsimp simp add: sup_state_Cons2,
             auto dest: sup_state_length)
     next
       case Swap
       with app G show ?thesis
-        by (cases s2, clarsimp simp add: sup_state_Cons2)
+        by (cases s2) (auto simp add: sup_state_Cons2)
     next
       case IAdd
       with app G show ?thesis
-        by (cases s2, auto simp add: sup_state_Cons2 PrimT_PrimT)
+        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)
+        by (cases s2) (auto simp add: sup_state_Cons2 PrimT_PrimT widen_RefT2)
     next
-      case Invoke
+      case (Invoke cname mname list)
       
       with app
       obtain apTs X ST LT mD' rT' b' where
@@ -234,7 +234,7 @@
         hence "\<exists>a b c. (fst s2) = rev a @ b # c \<and> length a = length list"
           by (rule rev_append_cons [rule_format])
         thus ?thesis
-          by -  (cases s2, elim exE conjE, simp, rule that) 
+          by (cases s2) (elim exE conjE, simp, rule that)
       qed
 
       from l l'
@@ -296,16 +296,16 @@
   have app1: "app i G m rT pc et (Some s1)" by (rule app_mono)
 
   show ?thesis
-  proof (cases (open) i)
-    case Load
+  proof (cases i)
+    case (Load n)
 
     with s app1
     obtain y where
-       y:  "nat < length b1" "b1 ! nat = OK y" by clarsimp
+       y:  "n < length b1" "b1 ! n = OK y" by clarsimp
 
     from Load s app2
     obtain y' where
-       y': "nat < length b2" "b2 ! nat = OK y'" by clarsimp
+       y': "n < length b2" "b2 ! n = OK y'" by clarsimp
 
     from G s 
     have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_conv)
@@ -347,7 +347,7 @@
     show ?thesis
       by (clarsimp simp add: sup_state_Cons1)
   next
-    case Invoke
+    case (Invoke cname mname list)
 
     with s app1
     obtain a X ST where
diff -r 1aa441e48496 -r 8d06e11a01d1 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Fri Nov 09 18:59:56 2007 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Fri Nov 09 19:37:30 2007 +0100
@@ -317,11 +317,11 @@
     { 
       fix b
       have "?Q (l#ls) b"
-      proof (cases (open) b)
+      proof (cases b)
         case Nil
         thus ?thesis by (auto dest: sup_loc_length)
       next
-        case Cons 
+        case (Cons a list)
         show ?thesis
         proof
           assume "G \<turnstile> (l # ls) <=l b"