--- 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"
--- 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"
--- 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)"
--- 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)"
--- 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
--- 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> {}"
--- 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
--- 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]
--- 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)
--- 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)
--- 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
--- 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
--- 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)
--- 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"
--- 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
--- 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"
--- 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)+
--- 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)"
--- 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:
--- 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"
--- 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 *}
--- 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
--- 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
--- 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:
--- 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
--- 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]
--- 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: