# HG changeset patch
# User nipkow
# Date 1251483732 -7200
# Node ID 5a03495c731a43cf045e5984e0a73c9a25b0e1f0
# Parent  6b93b73a712b1c8dd5ab77586306cf9355b85c8b# Parent  bd13b7756f47a1993effb6a90995e01e5da8321d
merged

diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -817,15 +817,9 @@
 text {* Degree and polynomial operations *}
 
 lemma deg_add [simp]:
-  assumes R: "p \<in> carrier P" "q \<in> carrier P"
-  shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
-proof (cases "deg R p <= deg R q")
-  case True show ?thesis
-    by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
-next
-  case False show ?thesis
-    by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
-qed
+  "p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
+  deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
+by(rule deg_aboveI)(simp_all add: deg_aboveD)
 
 lemma deg_monom_le:
   "a \<in> carrier R ==> deg R (monom P a n) <= n"
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -563,11 +563,7 @@
 
 lemma deg_add [simp]:
   "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)"
-proof (cases "deg p <= deg q")
-  case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) 
-next
-  case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD)
-qed
+by (rule deg_aboveI) (simp add: deg_aboveD)
 
 lemma deg_monom_ring:
   "deg (monom a n::'a::ring up) <= n"
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Complete_Lattice.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -76,11 +76,11 @@
 
 lemma sup_bot [simp]:
   "x \<squnion> bot = x"
-  using bot_least [of x] by (simp add: le_iff_sup sup_commute)
+  using bot_least [of x] by (simp add: sup_commute)
 
 lemma inf_top [simp]:
   "x \<sqinter> top = x"
-  using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
+  using top_greatest [of x] by (simp add: inf_commute)
 
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   "SUPR A f = \<Squnion> (f ` A)"
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -1904,7 +1904,7 @@
 	show "0 < real x * 2/3" using * by auto
 	show "real ?max + 1 \<le> real x * 2/3" using * up
 	  by (cases "0 < real x * real (lapprox_posrat prec 2 3) - 1",
-	      auto simp add: real_of_float_max max_def)
+	      auto simp add: real_of_float_max)
       qed
       finally have "real (?lb_horner (Float 1 -1)) + real (?lb_horner ?max)
 	\<le> ln (real x)"
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -512,7 +512,7 @@
   assumes g0: "numgcd t = 0"
   shows "Inum bs t = 0"
   using g0[simplified numgcd_def] 
-  by (induct t rule: numgcdh.induct, auto simp add: natabs0 max_def maxcoeff_pos)
+  by (induct t rule: numgcdh.induct, auto simp add: natabs0 maxcoeff_pos)
 
 lemma numgcdh_pos: assumes gp: "g \<ge> 0" shows "numgcdh t g \<ge> 0"
   using gp
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -2966,11 +2966,11 @@
 
 lemma dual_max:
   "ord.max (op \<ge>) = min"
-  by (auto simp add: ord.max_def_raw min_def_raw expand_fun_eq)
+  by (auto simp add: ord.max_def_raw expand_fun_eq)
 
 lemma dual_min:
   "ord.min (op \<ge>) = max"
-  by (auto simp add: ord.min_def_raw max_def_raw expand_fun_eq)
+  by (auto simp add: ord.min_def_raw expand_fun_eq)
 
 lemma strict_below_fold1_iff:
   assumes "finite A" and "A \<noteq> {}"
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/HoareParallel/Graph.thy
--- a/src/HOL/HoareParallel/Graph.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/HoareParallel/Graph.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -203,11 +203,11 @@
   apply(rule_tac x = "(take m path)@patha" in exI)
   apply(subgoal_tac "\<not>(length path\<le>m)")
    prefer 2 apply arith
-  apply(simp add: min_def)
+  apply(simp)
   apply(rule conjI)
    apply(subgoal_tac "\<not>(m + length patha - 1 < m)")
     prefer 2 apply arith
-   apply(simp add: nth_append min_def)
+   apply(simp add: nth_append)
   apply(rule conjI)
    apply(case_tac "m")
     apply force
@@ -236,7 +236,7 @@
     apply(erule_tac x = "m - 1" in allE)
     apply(simp add: nth_list_update)
    apply(force simp add: nth_list_update)
-  apply(simp add: nth_append min_def)
+  apply(simp add: nth_append)
   apply(rotate_tac -4)
   apply(erule_tac x = "i - m" in allE)
   apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
@@ -248,8 +248,7 @@
  apply(rule_tac x = "take (Suc m) path" in exI)
  apply(subgoal_tac "\<not>(length path\<le>Suc m)" )
   prefer 2 apply arith
- apply(simp add: min_def)
- apply clarify
+ apply clarsimp
  apply(erule_tac x = "i" in allE)
  apply simp
  apply clarify
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Int.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -266,7 +266,7 @@
 proof  
   fix k :: int
   show "abs k = sup k (- k)"
-    by (auto simp add: sup_int_def zabs_def max_def less_minus_self_iff [symmetric])
+    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
 qed
 
 lemma zless_imp_add1_zle: "w < z \<Longrightarrow> w + (1\<Colon>int) \<le> z"
@@ -1487,21 +1487,6 @@
        add_special diff_special eq_special less_special le_special
 
 
-lemma min_max_01: "min (0::int) 1 = 0 & min (1::int) 0 = 0 &
-                   max (0::int) 1 = 1 & max (1::int) 0 = 1"
-by(simp add:min_def max_def)
-
-lemmas min_max_special[simp] =
- min_max_01
- max_def[of "0::int" "number_of v", standard, simp]
- min_def[of "0::int" "number_of v", standard, simp]
- max_def[of "number_of u" "0::int", standard, simp]
- min_def[of "number_of u" "0::int", standard, simp]
- max_def[of "1::int" "number_of v", standard, simp]
- min_def[of "1::int" "number_of v", standard, simp]
- max_def[of "number_of u" "1::int", standard, simp]
- min_def[of "number_of u" "1::int", standard, simp]
-
 text {* Legacy theorems *}
 
 lemmas zle_int = of_nat_le_iff [where 'a=int]
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Lattices.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -125,10 +125,10 @@
 lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   by (rule antisym) (auto intro: le_infI2)
 
-lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
+lemma inf_absorb1[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   by (rule antisym) auto
 
-lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
+lemma inf_absorb2[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   by (rule antisym) auto
 
 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
@@ -153,10 +153,10 @@
 lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   by (rule antisym) (auto intro: le_supI2)
 
-lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
+lemma sup_absorb1[simp]: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   by (rule antisym) auto
 
-lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
+lemma sup_absorb2[simp]: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   by (rule antisym) auto
 
 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
@@ -199,7 +199,7 @@
 shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
 proof-
   have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
-  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
+  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc del:sup_absorb1)
   also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
     by(simp add:inf_sup_absorb inf_commute)
   also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
@@ -211,7 +211,7 @@
 shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
 proof-
   have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
-  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
+  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc del:inf_absorb1)
   also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
     by(simp add:sup_inf_absorb sup_commute)
   also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -331,7 +331,7 @@
 
 lemma multiset_inter_count:
   "count (A #\<inter> B) x = min (count A x) (count B x)"
-by (simp add: multiset_inter_def min_def)
+by (simp add: multiset_inter_def)
 
 lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
 by (simp add: multiset_eq_conv_count_eq multiset_inter_count
@@ -353,7 +353,7 @@
 by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
 
 lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
-apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
+apply (simp add: multiset_eq_conv_count_eq multiset_inter_count
     split: split_if_asm)
 apply clarsimp
 apply (erule_tac x = a in allE)
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Library/Word.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -1519,9 +1519,7 @@
 proof -
   have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \<le>
       2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)"
-    apply (cases "length w1 \<le> length w2")
-    apply (auto simp add: max_def)
-    done
+    by (auto simp:max_def)
   also have "... = 2 ^ max (length w1) (length w2)"
   proof -
     from lw
@@ -2173,16 +2171,16 @@
     apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"])
     apply simp_all
     apply (rule w_def)
-    apply (simp add: w_defs min_def)
-    apply (simp add: w_defs min_def)
+    apply (simp add: w_defs)
+    apply (simp add: w_defs)
     apply (subst bv_sliceI [where ?j = k and ?i = l and ?w = w and ?w1.0 = w1 and ?w2.0 = "w2 @ w3 @ w4" and ?w3.0 = w5])
     apply simp_all
     apply (rule w_def)
-    apply (simp add: w_defs min_def)
-    apply (simp add: w_defs min_def)
+    apply (simp add: w_defs)
+    apply (simp add: w_defs)
     apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4])
     apply simp_all
-    apply (simp_all add: w_defs min_def)
+    apply (simp_all add: w_defs)
     done
 qed
 
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Lim.thy
--- a/src/HOL/Lim.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Lim.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -544,8 +544,7 @@
     case True thus ?thesis using `0 < s` by auto
   next
     case False hence "s / 2 \<ge> (x - b) / 2" by auto
-    from inf_absorb2[OF this, unfolded inf_real_def]
-    have "?x = (x + b) / 2" by auto
+    hence "?x = (x + b) / 2" by(simp add:field_simps)
     thus ?thesis using `b < x` by auto
   qed
   hence "0 \<le> f ?x" using all_le `?x < x` by auto
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -1663,7 +1663,7 @@
 apply (simp add: times_matrix_def Rep_mult_matrix)
 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])
 apply (simp_all)
-by (simp add: max_def ncols)
+by (simp add: ncols)
 
 lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)"
 apply (subst Rep_matrix_inject[THEN sym])
@@ -1671,7 +1671,7 @@
 apply (simp add: times_matrix_def Rep_mult_matrix)
 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])
 apply (simp_all)
-by (simp add: max_def nrows)
+by (simp add: nrows)
 
 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
 apply (simp add: times_matrix_def)
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -145,7 +145,7 @@
   method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq> Class C)"
   (is "?app ST LT = ?P ST LT")
 proof
-  assume "?P ST LT" thus "?app ST LT" by (auto simp add: min_def list_all2_def)
+  assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_def)
 next  
   assume app: "?app ST LT"
   hence l: "length fpTs < length ST" by simp
@@ -153,7 +153,7 @@
   proof -
     have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp
     moreover from l have "length (take (length fpTs) ST) = length fpTs"
-      by (simp add: min_def)
+      by simp
     ultimately show ?thesis ..
   qed
   obtain apTs where
@@ -168,11 +168,11 @@
   have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
   with app
   show "?P ST LT"
-    apply (clarsimp simp add: list_all2_def min_def)
+    apply (clarsimp simp add: list_all2_def)
     apply ((rule exI)+, (rule conjI)?)+
     apply auto
     done
-qed 
+qed
 
 lemma approx_loc_len [simp]:
   "approx_loc G hp loc LT \<Longrightarrow> length loc = length LT"
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/MicroJava/BV/Effect.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -375,7 +375,7 @@
     hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l") 
       by auto
     hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs" 
-      by (auto simp add: min_def)
+      by (auto)
     hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> 0 < length ST" 
       by blast
     hence "\<exists>apTs ST. a = rev apTs @ ST \<and> length apTs = length fpTs \<and> ST \<noteq> []" 
@@ -391,7 +391,7 @@
   with Pair 
   have "?app s \<Longrightarrow> ?P s" by (simp only:)
   moreover
-  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp simp add: min_def)
+  have "?P s \<Longrightarrow> ?app s" by (unfold app_def) (clarsimp)
   ultimately
   show ?thesis by (rule iffI) 
 qed 
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/MicroJava/BV/LBVSpec.thy
--- a/src/HOL/MicroJava/BV/LBVSpec.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -293,7 +293,7 @@
   shows "wtl (take (pc+1) is) c 0 s = wtc c pc (wtl (take pc is) c 0 s)"
 proof -
   from suc have "take (pc+1) is=(take pc is)@[is!pc]" by (simp add: take_Suc)
-  with suc wtl show ?thesis by (simp add: min_def)
+  with suc wtl show ?thesis by (simp)
 qed
 
 lemma (in lbv) wtl_all:
@@ -308,7 +308,7 @@
   with all have take: "?wtl (take pc is@i#r) \<noteq> \<top>" by simp 
   from pc have "is!pc = drop pc is ! 0" by simp
   with Cons have "is!pc = i" by simp
-  with take pc show ?thesis by (auto simp add: min_def split: split_if_asm)
+  with take pc show ?thesis by (auto)
 qed
 
 section "preserves-type"
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -959,7 +959,7 @@
 apply simp
 apply (simp (no_asm_simp))+
 apply simp
-apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
+apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp))
 
   (* show check_type \<dots> *)
 apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
@@ -973,7 +973,7 @@
 apply (simp add: check_type_def)
 apply (rule states_lower, assumption)
 apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append)
-apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def max_def)
+apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def)
 apply (simp (no_asm_simp))+
 done
 
@@ -988,7 +988,7 @@
 apply (drule_tac x=sttp in spec, erule exE)
 apply simp
 apply (rule check_type_mono, assumption)
-apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def split: prod.split)
+apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split: prod.split)
 done
 
   (* ********************************************************************** *)
@@ -1058,8 +1058,7 @@
 lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
   \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-    max_ssize_def max_of_list_def ssize_sto_def max_def 
-    eff_def norm_eff_def)
+    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
 apply (intro strip)
 apply (rule conjI)
 apply (rule check_type_mono, assumption, simp)
@@ -1070,7 +1069,6 @@
   bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
-  apply (simp add: max_def)
   apply (simp add: check_type_simps)
   apply clarify
   apply (rule_tac x="(length ST)" in exI)
@@ -1082,7 +1080,7 @@
   \<Longrightarrow> bc_mt_corresp [Checkcast cname] (replST (Suc 0) (Class cname)) sttp cG rT mxr (Suc 0)"
   apply (erule exE)+
   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
-  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
   apply (simp add: check_type_simps)
   apply clarify
   apply (rule_tac x="Suc (length STo)" in exI)
@@ -1094,8 +1092,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1114,8 +1111,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1131,8 +1127,7 @@
   \<Longrightarrow> bc_mt_corresp [Load i] 
          (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1154,7 +1149,7 @@
   \<Longrightarrow> bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: max_ssize_def  max_of_list_def )
-  apply (simp add: ssize_sto_def) apply (simp add: max_def)
+  apply (simp add: ssize_sto_def)
   apply (intro strip)
 apply (simp add: check_type_simps)
 apply clarify
@@ -1170,7 +1165,6 @@
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: sup_state_conv)
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
-  apply (simp add: max_def)
  apply (intro strip)
 apply (simp add: check_type_simps)
 apply clarify
@@ -1182,8 +1176,7 @@
 lemma bc_mt_corresp_Dup: "
   bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1196,8 +1189,7 @@
 lemma bc_mt_corresp_Dup_x1: "
   bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1213,7 +1205,7 @@
   bc_mt_corresp [IAdd] (replST 2 (PrimT Integer)) 
          (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
-  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
   apply (simp add: check_type_simps)
   apply clarify
   apply (rule_tac x="Suc (length ST)" in exI)
@@ -1254,7 +1246,7 @@
   apply (frule widen_field, assumption+)
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
-  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
 
   apply (intro strip)
 apply (simp add: check_type_simps)
@@ -1305,7 +1297,7 @@
   apply (simp add: max_spec_preserves_length [THEN sym])
 
   -- "@{text check_type}"
-apply (simp add: max_ssize_def ssize_sto_def max_def)
+apply (simp add: max_ssize_def ssize_sto_def)
 apply (simp add: max_of_list_def)
 apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")
 apply simp
@@ -1316,7 +1308,7 @@
 apply (simp only: comp_is_type)
 apply (frule method_wf_mdecl) apply assumption apply assumption
 apply (simp add: wf_mdecl_def wf_mhead_def)
-apply (simp add: max_def)
+apply (simp)
   done
 
 
@@ -1473,7 +1465,7 @@
 apply (case_tac "sttp1", simp)
 apply (rule check_type_lower) apply assumption
 apply (simp (no_asm_simp) add: max_ssize_def ssize_sto_def)
-apply (simp (no_asm_simp) add: max_of_list_def max_def)
+apply (simp (no_asm_simp) add: max_of_list_def)
 
   (* subgoals \<exists> ... *)
 apply (rule surj_pair)+
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Nat.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -1512,7 +1512,7 @@
 by (simp split add: nat_diff_split)
 
 lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
-unfolding min_def by auto
+by auto
 
 lemma inj_on_diff_nat: 
   assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -1075,16 +1075,17 @@
 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
 
 lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
-by (simp add: pprt_def le_iff_sup sup_aci)
+by (simp add: pprt_def sup_aci)
+
 
 lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def le_iff_inf inf_aci)
+by (simp add: nprt_def inf_aci)
 
 lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def le_iff_sup sup_aci)
+by (simp add: pprt_def sup_aci)
 
 lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def le_iff_inf inf_aci)
+by (simp add: nprt_def inf_aci)
 
 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
 proof -
@@ -1118,13 +1119,13 @@
   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
 proof
   assume "0 <= a + a"
-  hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
+  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute)
   have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
     by (simp add: add_sup_inf_distribs inf_aci)
   hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
   hence "inf a 0 = 0" by (simp only: add_right_cancel)
-  then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
-next  
+  then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute)
+next
   assume a: "0 <= a"
   show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
 qed
@@ -1194,22 +1195,22 @@
 qed
 
 lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
-by (simp add: le_iff_inf nprt_def inf_commute)
+unfolding le_iff_inf by (simp add: nprt_def inf_commute)
 
 lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0"
-by (simp add: le_iff_sup pprt_def sup_commute)
+unfolding le_iff_sup by (simp add: pprt_def sup_commute)
 
 lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a"
-by (simp add: le_iff_sup pprt_def sup_commute)
+unfolding le_iff_sup by (simp add: pprt_def sup_commute)
 
 lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a"
-by (simp add: le_iff_inf nprt_def inf_commute)
+unfolding le_iff_inf by (simp add: nprt_def inf_commute)
 
 lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
-by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
+unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a])
 
 lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
-by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
+unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a])
 
 end
 
@@ -1274,7 +1275,7 @@
 proof -
   note add_le_cancel_right [of a a "- a", symmetric, simplified]
   moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
-  then show ?thesis by (auto simp: sup_max max_def)
+  then show ?thesis by (auto simp: sup_max)
 qed
 
 lemma abs_if_lattice:
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/SEQ.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -582,7 +582,7 @@
       ultimately
       have "a (max no n) < a n" by auto
       with monotone[where m=n and n="max no n"]
-      show False by auto
+      show False by (auto simp:max_def split:split_if_asm)
     qed
   } note top_down = this
   { fix x n m fix a :: "nat \<Rightarrow> real"
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/SetInterval.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -181,9 +181,10 @@
   "(i : {l..u}) = (l <= i & i <= u)"
 by (simp add: atLeastAtMost_def)
 
-text {* The above four lemmas could be declared as iffs.
-  If we do so, a call to blast in Hyperreal/Star.ML, lemma @{text STAR_Int}
-  seems to take forever (more than one hour). *}
+text {* The above four lemmas could be declared as iffs. Unfortunately this
+breaks many proofs. Since it only helps blast, it is better to leave well
+alone *}
+
 end
 
 subsubsection{* Emptyness, singletons, subset *}
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Tools/ATP_Manager/SystemOnTPTP
--- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Fri Aug 28 20:22:12 2009 +0200
@@ -19,6 +19,7 @@
     "QuietFlag" => "-q01",
     "SubmitButton" => "RunSelectedSystems",
     "ProblemSource" => "UPLOAD",
+    "ForceSystem" => "-force",
     );
 
 #----Get format and transform options if specified
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -65,7 +65,7 @@
 lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def max_def gasc)
+apply (simp add: constrains_def maxfg_def gasc)
 done
 
 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
@@ -73,7 +73,7 @@
           (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def max_def gasc)
+apply (simp add: constrains_def maxfg_def gasc)
 done
 
 
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -918,8 +918,8 @@
   apply (frule asm_rl)
   apply (drule spec)
   apply (erule trans)
-  apply (drule_tac x = "bin_cat y n a" in spec) 
-  apply (simp add : bin_cat_assoc_sym min_def)
+  apply (drule_tac x = "bin_cat y n a" in spec)
+  apply (simp add : bin_cat_assoc_sym)
   done
 
 lemma bin_rcat_bl:
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -493,7 +493,7 @@
 
 lemma sbintrunc_sbintrunc_l:
   "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
-  by (rule bin_eqI) (auto simp: nth_sbintr min_def)
+  by (rule bin_eqI) (auto simp: nth_sbintr)
 
 lemma bintrunc_bintrunc_ge:
   "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
@@ -501,14 +501,12 @@
 
 lemma bintrunc_bintrunc_min [simp]:
   "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
-  apply (unfold min_def)
   apply (rule bin_eqI)
   apply (auto simp: nth_bintr)
   done
 
 lemma sbintrunc_sbintrunc_min [simp]:
   "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
-  apply (unfold min_def)
   apply (rule bin_eqI)
   apply (auto simp: nth_sbintr)
   done
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -380,7 +380,7 @@
   "n >= size w ==> bintrunc n (uint w) = uint w"
   apply (unfold word_size)
   apply (subst word_ubin.norm_Rep [symmetric]) 
-  apply (simp only: bintrunc_bintrunc_min word_size min_def)
+  apply (simp only: bintrunc_bintrunc_min word_size)
   apply simp
   done
 
@@ -388,7 +388,7 @@
   "wb = word_of_int bin ==> n >= size wb ==> 
     word_of_int (bintrunc n bin) = wb"
   unfolding word_size
-  by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric] min_def)
+  by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric])
 
 lemmas bintr_uint = bintr_uint' [unfolded word_size]
 lemmas wi_bintr = wi_bintr' [unfolded word_size]
diff -r 6b93b73a712b -r 5a03495c731a src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Fri Aug 28 19:57:12 2009 +0200
+++ b/src/HOL/Word/WordShift.thy	Fri Aug 28 20:22:12 2009 +0200
@@ -319,7 +319,7 @@
 
 lemma bl_shiftl:
   "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
-  by (simp add: shiftl_bl word_rep_drop word_size min_def)
+  by (simp add: shiftl_bl word_rep_drop word_size)
 
 lemma shiftl_zero_size: 
   fixes x :: "'a::len0 word"
@@ -1018,8 +1018,7 @@
   word_of_int (bin_cat w (size b) (uint b))"
   apply (unfold word_cat_def word_size) 
   apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
-      word_ubin.eq_norm bintr_cat min_def)
-  apply arith
+      word_ubin.eq_norm bintr_cat)
   done
 
 lemma word_cat_split_alt: