# HG changeset patch
# User wenzelm
# Date 1375717927 -7200
# Node ID 438f578ef1d9b28eff83d1c0ff0bce14702db830
# Parent  02a7e7180ee57f2bd391dbb060bcad6eb2f7418b
tuned proofs;

diff -r 02a7e7180ee5 -r 438f578ef1d9 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Aug 05 17:14:02 2013 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Aug 05 17:52:07 2013 +0200
@@ -422,7 +422,7 @@
     apply (rule subsetI)
     apply (erule UN_E)
     apply (case_tac "\<not> stable r step ss p")
-    apply simp+
+    apply simp_all
     done
   also have "\<And>f. (UN p:{..<size ss}. f p) = Union (set (map f [0..<size ss]))" by auto
   also note Sup_set_fold also note fold_map
diff -r 02a7e7180ee5 -r 438f578ef1d9 src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Mon Aug 05 17:14:02 2013 +0200
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Mon Aug 05 17:52:07 2013 +0200
@@ -95,7 +95,7 @@
    apply simp
   apply clarsimp
   apply (case_tac aa)
-  apply simp+
+  apply simp_all
   done
 
 lemma [simp]: "Err.le r (OK a) (OK b) = r a b"
diff -r 02a7e7180ee5 -r 438f578ef1d9 src/HOL/MicroJava/Comp/AuxLemmas.thy
--- a/src/HOL/MicroJava/Comp/AuxLemmas.thy	Mon Aug 05 17:14:02 2013 +0200
+++ b/src/HOL/MicroJava/Comp/AuxLemmas.thy	Mon Aug 05 17:52:07 2013 +0200
@@ -15,20 +15,20 @@
 
 
 
-lemma app_nth_greater_len [rule_format (no_asm), simp]:
- "\<forall> ind. length pre \<le> ind \<longrightarrow> (pre @ a # post) ! (Suc ind) = (pre @ post) ! ind"
-apply (induct "pre")
+lemma app_nth_greater_len [simp]:
+ "length pre \<le> ind \<Longrightarrow> (pre @ a # post) ! (Suc ind) = (pre @ post) ! ind"
+apply (induct pre arbitrary: ind)
 apply auto
 apply (case_tac ind)
 apply auto
 done
 
 lemma length_takeWhile: "v \<in> set xs \<Longrightarrow> length (takeWhile (%z. z~=v) xs) < length xs"
-by (induct xs, auto)
+by (induct xs) auto
 
 lemma nth_length_takeWhile [simp]: 
   "v \<in> set xs \<Longrightarrow> xs ! (length (takeWhile (%z. z~=v) xs)) = v"
-by (induct xs, auto)
+by (induct xs) auto
 
 
 lemma map_list_update [simp]:
diff -r 02a7e7180ee5 -r 438f578ef1d9 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Aug 05 17:14:02 2013 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Aug 05 17:52:07 2013 +0200
@@ -16,7 +16,7 @@
  "(G \<turnstile> xs -ex\<succ>val-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
   (G \<turnstile> xs -exs[\<succ>]vals-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None) \<and>
   (G \<turnstile> xs -st-> xs' \<longrightarrow> gx xs' = None \<longrightarrow> gx xs = None)"
-by (induct rule: eval_evals_exec.induct, auto)
+by (induct rule: eval_evals_exec.induct) auto
 
 
 (* instance of eval_evals_exec_xcpt for eval *)
diff -r 02a7e7180ee5 -r 438f578ef1d9 src/HOL/MicroJava/Comp/TypeInf.thy
--- a/src/HOL/MicroJava/Comp/TypeInf.thy	Mon Aug 05 17:14:02 2013 +0200
+++ b/src/HOL/MicroJava/Comp/TypeInf.thy	Mon Aug 05 17:52:07 2013 +0200
@@ -15,67 +15,85 @@
 (*** Inversion of typing rules -- to be moved into WellType.thy
      Also modify the wtpd_expr_\<dots> proofs in CorrComp.thy ***)
 
-lemma NewC_invers: "E\<turnstile>NewC C::T 
-  \<Longrightarrow> T = Class C \<and> is_class (prg E) C"
-by (erule ty_expr.cases, auto)
+lemma NewC_invers:
+  assumes "E\<turnstile>NewC C::T"
+  shows "T = Class C \<and> is_class (prg E) C"
+  using assms by cases auto
 
-lemma Cast_invers: "E\<turnstile>Cast D e::T
-  \<Longrightarrow> \<exists> C. T = Class D \<and> E\<turnstile>e::C \<and> is_class (prg E) D \<and> prg E\<turnstile>C\<preceq>? Class D"
-by (erule ty_expr.cases, auto)
+lemma Cast_invers:
+  assumes "E\<turnstile>Cast D e::T"
+  shows "\<exists>C. T = Class D \<and> E\<turnstile>e::C \<and> is_class (prg E) D \<and> prg E\<turnstile>C\<preceq>? Class D"
+  using assms by cases auto
 
-lemma Lit_invers: "E\<turnstile>Lit x::T
-  \<Longrightarrow> typeof (\<lambda>v. None) x = Some T"
-by (erule ty_expr.cases, auto)
+lemma Lit_invers:
+  assumes "E\<turnstile>Lit x::T"
+  shows "typeof (\<lambda>v. None) x = Some T"
+  using assms by cases auto
 
-lemma LAcc_invers: "E\<turnstile>LAcc v::T
-  \<Longrightarrow> localT E v = Some T \<and> is_type (prg E) T"
-by (erule ty_expr.cases, auto)
+lemma LAcc_invers:
+  assumes "E\<turnstile>LAcc v::T"
+  shows "localT E v = Some T \<and> is_type (prg E) T"
+  using assms by cases auto
 
-lemma BinOp_invers: "E\<turnstile>BinOp bop e1 e2::T'
-  \<Longrightarrow> \<exists> T. E\<turnstile>e1::T \<and> E\<turnstile>e2::T \<and> 
+lemma BinOp_invers:
+  assumes "E\<turnstile>BinOp bop e1 e2::T'"
+  shows "\<exists>T. E\<turnstile>e1::T \<and> E\<turnstile>e2::T \<and>
             (if bop = Eq then T' = PrimT Boolean
                         else T' = T \<and> T = PrimT Integer)"
-by (erule ty_expr.cases, auto)
+  using assms by cases auto
 
-lemma LAss_invers: "E\<turnstile>v::=e::T'
-  \<Longrightarrow> \<exists> T. v ~= This \<and> E\<turnstile>LAcc v::T \<and> E\<turnstile>e::T' \<and> prg E\<turnstile>T'\<preceq>T"
-by (erule ty_expr.cases, auto)
+lemma LAss_invers:
+  assumes  "E\<turnstile>v::=e::T'"
+  shows "\<exists>T. v ~= This \<and> E\<turnstile>LAcc v::T \<and> E\<turnstile>e::T' \<and> prg E\<turnstile>T'\<preceq>T"
+  using assms by cases auto
 
-lemma FAcc_invers: "E\<turnstile>{fd}a..fn::fT
-  \<Longrightarrow> \<exists> C. E\<turnstile>a::Class C \<and> field (prg E,C) fn = Some (fd,fT)"
-by (erule ty_expr.cases, auto)
+lemma FAcc_invers:
+  assumes "E\<turnstile>{fd}a..fn::fT"
+  shows "\<exists>C. E\<turnstile>a::Class C \<and> field (prg E,C) fn = Some (fd, fT)"
+  using assms by cases auto
 
-lemma FAss_invers: "E\<turnstile>{fd}a..fn:=v::T' 
-\<Longrightarrow> \<exists> T. E\<turnstile>{fd}a..fn::T \<and> E\<turnstile>v ::T' \<and> prg E\<turnstile>T'\<preceq>T"
-by (erule ty_expr.cases, auto)
+lemma FAss_invers:
+  assumes "E\<turnstile>{fd}a..fn:=v::T'"
+  shows "\<exists>T. E\<turnstile>{fd}a..fn::T \<and> E\<turnstile>v ::T' \<and> prg E\<turnstile>T'\<preceq>T"
+  using assms by cases auto
 
-lemma Call_invers: "E\<turnstile>{C}a..mn({pTs'}ps)::rT
-  \<Longrightarrow> \<exists> pTs md. 
-  E\<turnstile>a::Class C \<and> E\<turnstile>ps[::]pTs \<and> max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}"
-by (erule ty_expr.cases, auto)
+lemma Call_invers:
+  assumes "E\<turnstile>{C}a..mn({pTs'}ps)::rT"
+  shows "\<exists>pTs md.
+    E\<turnstile>a::Class C \<and> E\<turnstile>ps[::]pTs \<and> max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')}"
+  using assms by cases auto
 
 
-lemma Nil_invers: "E\<turnstile>[] [::] Ts \<Longrightarrow> Ts = []"
-by (erule ty_exprs.cases, auto)
+lemma Nil_invers:
+  assumes "E\<turnstile>[] [::] Ts"
+  shows "Ts = []"
+  using assms by cases auto
 
-lemma Cons_invers: "E\<turnstile>e#es[::]Ts \<Longrightarrow> 
-  \<exists> T Ts'. Ts = T#Ts' \<and> E \<turnstile>e::T \<and> E \<turnstile>es[::]Ts'"
-by (erule ty_exprs.cases, auto)
+lemma Cons_invers:
+  assumes "E\<turnstile>e#es[::]Ts"
+  shows "\<exists>T Ts'. Ts = T#Ts' \<and> E \<turnstile>e::T \<and> E \<turnstile>es[::]Ts'"
+  using assms by cases auto
 
 
-lemma Expr_invers: "E\<turnstile>Expr e\<surd> \<Longrightarrow> \<exists> T. E\<turnstile>e::T"
-by (erule wt_stmt.cases, auto)
+lemma Expr_invers:
+  assumes "E\<turnstile>Expr e\<surd>"
+  shows "\<exists> T. E\<turnstile>e::T"
+  using assms by cases auto
 
-lemma Comp_invers: "E\<turnstile>s1;; s2\<surd> \<Longrightarrow> E\<turnstile>s1\<surd> \<and> E\<turnstile>s2\<surd>"
-by (erule wt_stmt.cases, auto)
+lemma Comp_invers:
+  assumes "E\<turnstile>s1;; s2\<surd>"
+  shows "E\<turnstile>s1\<surd> \<and> E\<turnstile>s2\<surd>"
+  using assms by cases auto
 
-lemma Cond_invers: "E\<turnstile>If(e) s1 Else s2\<surd> 
-  \<Longrightarrow> E\<turnstile>e::PrimT Boolean \<and> E\<turnstile>s1\<surd> \<and> E\<turnstile>s2\<surd>"
-by (erule wt_stmt.cases, auto)
+lemma Cond_invers:
+  assumes "E\<turnstile>If(e) s1 Else s2\<surd>"
+  shows "E\<turnstile>e::PrimT Boolean \<and> E\<turnstile>s1\<surd> \<and> E\<turnstile>s2\<surd>"
+  using assms by cases auto
 
-lemma Loop_invers: "E\<turnstile>While(e) s\<surd>
-  \<Longrightarrow> E\<turnstile>e::PrimT Boolean \<and> E\<turnstile>s\<surd>"
-by (erule wt_stmt.cases, auto)
+lemma Loop_invers:
+  assumes "E\<turnstile>While(e) s\<surd>"
+  shows "E\<turnstile>e::PrimT Boolean \<and> E\<turnstile>s\<surd>"
+  using assms by cases auto
 
 
 (**********************************************************************)