# 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 \ carrier P" "q \ carrier P" - shows "deg R (p \\<^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 \ carrier P \ q \ carrier P \ + deg R (p \\<^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 \ 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 \ 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 \ 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 \ ('b \ 'a) \ 'a" where "SUPR A f = \ (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 \ 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) \ 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 \ 0" shows "numgcdh t g \ 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 \) = 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 \) = 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 \ {}" 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 "\(length path\m)") prefer 2 apply arith - apply(simp add: min_def) + apply(simp) apply(rule conjI) apply(subgoal_tac "\(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 "\(length path\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 \ w + (1\int) \ 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 \ (x \ y) = x \ y" by (rule antisym) (auto intro: le_infI2) -lemma inf_absorb1: "x \ y \ x \ y = x" +lemma inf_absorb1[simp]: "x \ y \ x \ y = x" by (rule antisym) auto -lemma inf_absorb2: "y \ x \ x \ y = y" +lemma inf_absorb2[simp]: "y \ x \ x \ y = y" by (rule antisym) auto lemma inf_left_commute: "x \ (y \ z) = y \ (x \ z)" @@ -153,10 +153,10 @@ lemma sup_left_idem[simp]: "x \ (x \ y) = x \ y" by (rule antisym) (auto intro: le_supI2) -lemma sup_absorb1: "y \ x \ x \ y = x" +lemma sup_absorb1[simp]: "y \ x \ x \ y = x" by (rule antisym) auto -lemma sup_absorb2: "x \ y \ x \ y = y" +lemma sup_absorb2[simp]: "x \ y \ x \ y = y" by (rule antisym) auto lemma sup_left_commute: "x \ (y \ z) = y \ (x \ z)" @@ -199,7 +199,7 @@ shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by(simp add:sup_inf_absorb) - also have "\ = x \ (z \ (x \ y))" by(simp add:D inf_commute sup_assoc) + also have "\ = x \ (z \ (x \ y))" by(simp add:D inf_commute sup_assoc del:sup_absorb1) also have "\ = ((x \ y) \ x) \ ((x \ y) \ z)" by(simp add:inf_sup_absorb inf_commute) also have "\ = (x \ y) \ (x \ z)" by(simp add:D) @@ -211,7 +211,7 @@ shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by(simp add:inf_sup_absorb) - also have "\ = x \ (z \ (x \ y))" by(simp add:D sup_commute inf_assoc) + also have "\ = x \ (z \ (x \ y))" by(simp add:D sup_commute inf_assoc del:inf_absorb1) also have "\ = ((x \ y) \ x) \ ((x \ y) \ z)" by(simp add:sup_inf_absorb sup_commute) also have "\ = (x \ y) \ (x \ 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 #\ 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 #\ B = B #\ 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 #\ C = {#} \ 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)) \ 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)" - apply (cases "length w1 \ 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 \ (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 \ 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 \ (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') \ G \ X \ 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 \ 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 \ 0 < length (drop (length fpTs) a)" (is "?a \ ?l") by auto hence "?a \ ?l \ length (rev (take (length fpTs) a)) = length fpTs" - by (auto simp add: min_def) + by (auto) hence "\apTs ST. a = rev apTs @ ST \ length apTs = length fpTs \ 0 < length ST" by blast hence "\apTs ST. a = rev apTs @ ST \ length apTs = length fpTs \ ST \ []" @@ -391,7 +391,7 @@ with Pair have "?app s \ ?P s" by (simp only:) moreover - have "?P s \ ?app s" by (unfold app_def) (clarsimp simp add: min_def) + have "?P s \ ?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) \ \" 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 \ *) 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: "\is_class cG cname \ \ 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 @@ \ 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 @@ \ bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)" apply (subgoal_tac "\ 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 @@ \ bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)" apply (subgoal_tac "\ 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 @@ \ bc_mt_corresp [Load i] (\(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 @@ \ 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 \ ... *) 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: "\n \ N. k \ (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 \ x \ 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 \ 0 \ 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 \ 0 \ 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 \ x \ 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 \ a = 0" proof - @@ -1118,13 +1119,13 @@ "0 \ a + a \ 0 \ 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 \ a \ 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 \ 0 \ 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 \ a \ 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 \ 0 \ 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 \ b \ pprt a \ 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 \ b \ nprt a \ 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 \ 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) \ {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 {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: