src/HOL/MicroJava/BV/Step.thy

 by (cases s, cases "2 < length (fst s)", auto dest: 1 2)
 
 
 lemma appIAdd[simp]:
 "app (IAdd, G, rT, s) = (\<exists> ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))"  (is "?app s = ?P s")
-proof (cases s)
+proof (cases (open) s)
   case Pair
   have "?app (a,b) = ?P (a,b)"
   proof (cases "a")
     fix t ts assume a: "a = t#ts"
     show ?thesis

                                        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")
-proof (cases 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"