# HG changeset patch # User wenzelm # Date 1181838811 -7200 # Node ID aaca6a8e5414a2259e0155d8bb8c5c87f4b24401 # Parent 77645da0db85b3949c73b34f4b56c10a9b7342c3 tuned proofs: avoid implicit prems; diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Finite_Set.thy Thu Jun 14 18:33:31 2007 +0200 @@ -35,7 +35,7 @@ assume "finite F" thus "P F" proof induct - show "P {}" . + show "P {}" by fact fix x F assume F: "finite F" and P: "P F" show "P (insert x F)" proof cases @@ -61,30 +61,35 @@ case (insert x F) show ?case proof cases - assume "F = {}" thus ?thesis using insert(4) by simp + assume "F = {}" + thus ?thesis using `P {x}` by simp next - assume "F \ {}" thus ?thesis using insert by blast + assume "F \ {}" + thus ?thesis using insert by blast qed qed lemma finite_subset_induct [consumes 2, case_names empty insert]: - "finite F ==> F \ A ==> - P {} ==> (!!a F. finite F ==> a \ A ==> a \ F ==> P F ==> P (insert a F)) ==> - P F" + assumes "finite F" and "F \ A" + and empty: "P {}" + and insert: "!!a F. finite F ==> a \ A ==> a \ F ==> P F ==> P (insert a F)" + shows "P F" proof - - assume "P {}" and insert: - "!!a F. finite F ==> a \ A ==> a \ F ==> P F ==> P (insert a F)" - assume "finite F" - thus "F \ A ==> P F" + from `finite F` and `F \ A` + show ?thesis proof induct - show "P {}" . - fix x F assume "finite F" and "x \ F" - and P: "F \ A ==> P F" and i: "insert x F \ A" + show "P {}" by fact + next + fix x F + assume "finite F" and "x \ F" and + P: "F \ A ==> P F" and i: "insert x F \ A" show "P (insert x F)" proof (rule insert) from i show "x \ A" by blast from i have "F \ A" by blast with P show "P F" . + show "finite F" by fact + show "x \ F" by fact qed qed qed @@ -102,7 +107,7 @@ qed next case (insert a A) - have notinA: "a \ A" . + have notinA: "a \ A" by fact from insert.hyps obtain n f where "A = f ` {i::nat. i < n}" "inj_on f {i. i < n}" by blast hence "insert a A = f(n:=a) ` {i. i < Suc n}" @@ -151,17 +156,17 @@ thus ?case by simp next case (insert x F A) - have A: "A \ insert x F" and r: "A - {x} \ F ==> finite (A - {x})" . + have A: "A \ insert x F" and r: "A - {x} \ F ==> finite (A - {x})" by fact+ show "finite A" proof cases assume x: "x \ A" with A have "A - {x} \ F" by (simp add: subset_insert_iff) with r have "finite (A - {x})" . hence "finite (insert x (A - {x}))" .. - also have "insert x (A - {x}) = A" by (rule insert_Diff) + also have "insert x (A - {x}) = A" using x by (rule insert_Diff) finally show ?thesis . next - show "A \ F ==> ?thesis" . + show "A \ F ==> ?thesis" by fact assume "x \ A" with A show "A \ F" by (simp add: subset_insert_iff) qed @@ -188,35 +193,37 @@ by (induct rule:finite_induct) simp_all lemma finite_empty_induct: - "finite A ==> - P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}" + assumes "finite A" + and "P A" + and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})" + shows "P {}" proof - - assume "finite A" - and "P A" and "!!a A. finite A ==> a:A ==> P A ==> P (A - {a})" have "P (A - A)" proof - - fix c b :: "'a set" - presume c: "finite c" and b: "finite b" - and P1: "P b" and P2: "!!x y. finite y ==> x \ y ==> P y ==> P (y - {x})" - from c show "c \ b ==> P (b - c)" - proof induct - case empty - from P1 show ?case by simp - next - case (insert x F) - have "P (b - F - {x})" - proof (rule P2) - from _ b show "finite (b - F)" by (rule finite_subset) blast - from insert show "x \ b - F" by simp - from insert show "P (b - F)" by simp + { + fix c b :: "'a set" + assume c: "finite c" and b: "finite b" + and P1: "P b" and P2: "!!x y. finite y ==> x \ y ==> P y ==> P (y - {x})" + have "c \ b ==> P (b - c)" + using c + proof induct + case empty + from P1 show ?case by simp + next + case (insert x F) + have "P (b - F - {x})" + proof (rule P2) + from _ b show "finite (b - F)" by (rule finite_subset) blast + from insert show "x \ b - F" by simp + from insert show "P (b - F)" by simp + qed + also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric]) + finally show ?case . qed - also have "b - F - {x} = b - insert x F" by (rule Diff_insert [symmetric]) - finally show ?case . - qed - next - show "A \ A" .. + } + then show ?thesis by this (simp_all add: assms) qed - thus "P {}" by simp + then show ?thesis by simp qed lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)" @@ -526,7 +533,7 @@ case 0 thus ?thesis using aA by auto next case (Suc m) - have nSuc: "n = Suc m" . + have nSuc: "n = Suc m" by fact have mlessn: "mm \ x' = x" . + foldSet f g z A x; foldSet f g z A x'\ \ x' = x" by fact have Afoldx: "foldSet f g z A x" and Afoldx': "foldSet f g z A x'" - and A: "A = h`{i. i PROP P) \ PROP P" proof - assume prem: "True \ PROP P" - from prem [OF TrueI] show "PROP P" . + assume "True \ PROP P" + from this [OF TrueI] show "PROP P" . next assume "PROP P" - show "PROP P" . + then show "PROP P" . qed lemma ex_simps: diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Import/HOL4Compat.thy --- a/src/HOL/Import/HOL4Compat.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Import/HOL4Compat.thy Thu Jun 14 18:33:31 2007 +0200 @@ -157,7 +157,7 @@ fix k show "!q. q + k = m \ P q" proof (induct k,simp_all) - show "P m" . + show "P m" by fact next fix k assume ind: "!q. q + k = m \ P q" @@ -406,7 +406,7 @@ assume allt: "!t. P t \ (!h. P (h # t))" show "P l" proof (induct l) - show "P []" . + show "P []" by fact next fix h t assume "P t" diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Inductive.thy Thu Jun 14 18:33:31 2007 +0200 @@ -89,7 +89,7 @@ then show P .. next assume "\P\bool. P" - then show False .. + then show False . qed lemma not_eq_False: diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Lattices.thy Thu Jun 14 18:33:31 2007 +0200 @@ -259,7 +259,7 @@ and greatest: "\x y z. x \<^loc>\ y \ x \<^loc>\ z \ x \<^loc>\ y \ z" shows "x \ y = x \ y" proof (rule antisym) - show "x \ y \<^loc>\ x \ y" by (rule le_infI) (rule le1 le2) + show "x \ y \<^loc>\ x \ y" by (rule le_infI) (rule le1, rule le2) next have leI: "\x y z. x \<^loc>\ y \ x \<^loc>\ z \ x \<^loc>\ y \ z" by (blast intro: greatest) show "x \ y \<^loc>\ x \ y" by (rule leI) simp_all @@ -271,7 +271,7 @@ and least: "\x y z. y \<^loc>\ x \ z \<^loc>\ x \ y \ z \<^loc>\ x" shows "x \ y = x \ y" proof (rule antisym) - show "x \ y \<^loc>\ x \ y" by (rule le_supI) (rule ge1 ge2) + show "x \ y \<^loc>\ x \ y" by (rule le_supI) (rule ge1, rule ge2) next have leI: "\x y z. x \<^loc>\ z \ y \<^loc>\ z \ x \ y \<^loc>\ z" by (blast intro: least) show "x \ y \<^loc>\ x \ y" by (rule leI) simp_all diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Library/SCT_Theorem.thy --- a/src/HOL/Library/SCT_Theorem.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Library/SCT_Theorem.thy Thu Jun 14 18:33:31 2007 +0200 @@ -1139,12 +1139,12 @@ (auto simp:index_less) then obtain T i where inf: "infinite T" - and "i < length l" + and i: "i < length l" and d: "\x y. \x \ T; y\T; x \ y\ \ index_of l (f (set2pair {x, y})) = i" by auto - have "l ! i \ S" unfolding S + have "l ! i \ S" unfolding S using i by (rule nth_mem) moreover have "\x y. x \ T \ y\T \ x < y diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/NatBin.thy --- a/src/HOL/NatBin.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/NatBin.thy Thu Jun 14 18:33:31 2007 +0200 @@ -376,13 +376,13 @@ "(a::'a::{ordered_idom,recpower}) < 0 ==> a ^ Suc(2*n) < 0" proof (induct "n") case 0 - show ?case by (simp add: Power.power_Suc) + then show ?case by (simp add: Power.power_Suc) next case (Suc n) - have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" - by (simp add: mult_ac power_add power2_eq_square Power.power_Suc) - thus ?case - by (simp add: prems mult_less_0_iff mult_neg_neg) + have "a ^ Suc (2 * Suc n) = (a*a) * a ^ Suc(2*n)" + by (simp add: mult_ac power_add power2_eq_square Power.power_Suc) + thus ?case + by (simp add: prems mult_less_0_iff mult_neg_neg) qed lemma odd_0_le_power_imp_0_le: diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Numeral.thy --- a/src/HOL/Numeral.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Numeral.thy Thu Jun 14 18:33:31 2007 +0200 @@ -339,7 +339,7 @@ assumes le: "0 \ z" shows "(0::int) < 1 + z" proof - - have "0 \ z" . + have "0 \ z" by fact also have "... < z + 1" by (rule less_add_one) also have "... = 1 + z" by (simp add: add_ac) finally show "0 < 1 + z" . diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/OrderedGroup.thy Thu Jun 14 18:33:31 2007 +0200 @@ -377,10 +377,10 @@ subsection {* Ordering Rules for Unary Minus *} lemma le_imp_neg_le: - assumes "a \ (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \ -a" + assumes "a \ (b::'a::{pordered_ab_semigroup_add_imp_le, ab_group_add})" shows "-b \ -a" proof - have "-a+a \ -a+b" - by (rule add_left_mono) + using `a \ b` by (rule add_left_mono) hence "0 \ -a+b" by simp hence "0 + (-b) \ (-a + b) + (-b)" diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Predicate.thy Thu Jun 14 18:33:31 2007 +0200 @@ -34,11 +34,11 @@ proof fix S assume "!!S. PROP P S" - show "PROP P (Collect S)" . + then show "PROP P (Collect S)" . next fix S assume "!!S. PROP P (Collect S)" - have "PROP P {x. x : S}" . + then have "PROP P {x. x : S}" . thus "PROP P S" by simp qed @@ -46,11 +46,11 @@ proof fix S assume "!!S. PROP P S" - show "PROP P (member S)" . + then show "PROP P (member S)" . next fix S assume "!!S. PROP P (member S)" - have "PROP P (member {x. S x})" . + then have "PROP P (member {x. S x})" . thus "PROP P S" by simp qed @@ -96,11 +96,11 @@ proof fix S assume "!!S. PROP P S" - show "PROP P (Collect2 S)" . + then show "PROP P (Collect2 S)" . next fix S assume "!!S. PROP P (Collect2 S)" - have "PROP P (Collect2 (member2 S))" . + then have "PROP P (Collect2 (member2 S))" . thus "PROP P S" by simp qed @@ -108,11 +108,11 @@ proof fix S assume "!!S. PROP P S" - show "PROP P (member2 S)" . + then show "PROP P (member2 S)" . next fix S assume "!!S. PROP P (member2 S)" - have "PROP P (member2 (Collect2 S))" . + then have "PROP P (member2 (Collect2 S))" . thus "PROP P S" by simp qed diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Presburger.thy Thu Jun 14 18:33:31 2007 +0200 @@ -200,8 +200,8 @@ have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound) moreover have "x mod d : {1..d}" proof - - have "0 \ x mod d" by(rule pos_mod_sign) - moreover have "x mod d < d" by(rule pos_mod_bound) + from dpos have "0 \ x mod d" by(rule pos_mod_sign) + moreover from dpos have "x mod d < d" by(rule pos_mod_bound) ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff) qed ultimately show ?RHS .. @@ -243,7 +243,7 @@ qed lemma minusinfinity: - assumes "0 < d" and + assumes dpos: "0 < d" and P1eqP1: "ALL x k. P1 x = P1(x - k*d)" and ePeqP1: "EX z::int. ALL x. x < z \ (P x = P1 x)" shows "(EX x. P1 x) \ (EX x. P x)" proof @@ -251,7 +251,7 @@ then obtain x where P1: "P1 x" .. from ePeqP1 obtain z where P1eqP: "ALL x. x < z \ (P x = P1 x)" .. let ?w = "x - (abs(x-z)+1) * d" - have w: "?w < z" by(rule decr_lemma) + from dpos have w: "?w < z" by(rule decr_lemma) have "P1 x = P1 ?w" using P1eqP1 by blast also have "\ = P(?w)" using w P1eqP by blast finally have "P ?w" using P1 by blast @@ -289,7 +289,7 @@ subsection {* The @{text "+\"} Version*} lemma plusinfinity: - assumes "(0::int) < d" and + assumes dpos: "(0::int) < d" and P1eqP1: "\x k. P' x = P'(x - k*d)" and ePeqP1: "\ z. \ x>z. P x = P' x" shows "(\ x. P' x) \ (\ x. P x)" proof @@ -299,7 +299,7 @@ let ?w' = "x + (abs(x-z)+1) * d" let ?w = "x - (-(abs(x-z) + 1))*d" have ww'[simp]: "?w = ?w'" by (simp add: ring_eq_simps) - have w: "?w > z" by(simp only: ww', rule incr_lemma) + from dpos have w: "?w > z" by(simp only: ww' incr_lemma) hence "P' x = P' ?w" using P1eqP1 by blast also have "\ = P(?w)" using w P1eqP by blast finally have "P ?w" using P1 by blast diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Real/ContNotDenum.thy --- a/src/HOL/Real/ContNotDenum.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Real/ContNotDenum.thy Thu Jun 14 18:33:31 2007 +0200 @@ -85,7 +85,7 @@ lemma closed_mem: assumes "a \ c" and "c \ b" shows "c \ closed_int a b" - by (unfold closed_int_def) auto + using assms unfolding closed_int_def by auto lemma closed_subset: assumes ac: "a \ b" "c \ d" diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Real/PReal.thy --- a/src/HOL/Real/PReal.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Real/PReal.thy Thu Jun 14 18:33:31 2007 +0200 @@ -437,7 +437,7 @@ show "z = (z/y)*y" by (simp add: divide_inverse mult_commute [of y] mult_assoc order_less_imp_not_eq2) - show "y \ B" . + show "y \ B" by fact qed next show "z/y \ A" @@ -527,7 +527,7 @@ show "x = (x/v)*v" by (simp add: divide_inverse mult_assoc vpos order_less_imp_not_eq2) - show "v \ A" . + show "v \ A" by fact qed qed qed @@ -1280,8 +1280,8 @@ by (simp add: mult_ac) also have "... = x/y" using zpos by (simp add: divide_inverse) - also have "... < z" - by (simp add: pos_divide_less_eq [OF ypos] mult_commute) + also from xless have "... < z" + by (simp add: pos_divide_less_eq [OF ypos] mult_commute) finally show ?thesis . qed diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Real/RComplete.thy --- a/src/HOL/Real/RComplete.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Real/RComplete.thy Thu Jun 14 18:33:31 2007 +0200 @@ -59,16 +59,16 @@ then obtain py where y_is_py: "y = real_of_preal py" by (auto simp add: real_gt_zero_preal_Ex) - obtain a where a_in_P: "a \ P" using not_empty_P .. - have a_pos: "0 < a" using positive_P .. + obtain a where "a \ P" using not_empty_P .. + with positive_P have a_pos: "0 < a" .. then obtain pa where "a = real_of_preal pa" by (auto simp add: real_gt_zero_preal_Ex) - hence "pa \ ?pP" using a_in_P by auto + hence "pa \ ?pP" using `a \ P` by auto hence pP_not_empty: "?pP \ {}" by auto obtain sup where sup: "\x \ P. x < sup" using upper_bound_Ex .. - hence "a < sup" .. + from this and `a \ P` have "a < sup" .. hence "0 < sup" using a_pos by arith then obtain possup where "sup = real_of_preal possup" by (auto simp add: real_gt_zero_preal_Ex) @@ -521,9 +521,9 @@ assumes a1: "real m \ r" and a2: "r < real n + 1" shows "m \ (n::int)" proof - - have "real m < real n + 1" by (rule order_le_less_trans) - also have "... = real(n+1)" by simp - finally have "m < n+1" by (simp only: real_of_int_less_iff) + have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans) + also have "... = real (n + 1)" by simp + finally have "m < n + 1" by (simp only: real_of_int_less_iff) thus ?thesis by arith qed diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Ring_and_Field.thy Thu Jun 14 18:33:31 2007 +0200 @@ -170,6 +170,7 @@ class division_by_zero = zero + inverse + assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0" + subsection {* Distribution rules *} theorems ring_distrib = right_distrib left_distrib @@ -343,6 +344,7 @@ apply (simp add: compare_rls minus_mult_left [symmetric]) done + subsection {* Ordering Rules for Multiplication *} lemma mult_left_le_imp_le: @@ -386,6 +388,7 @@ apply (simp_all add: minus_mult_right [symmetric]) done + subsection{* Products of Signs *} lemma mult_pos_pos: "[| (0::'a::ordered_semiring_strict) < a; 0 < b |] ==> 0 < a*b" @@ -501,6 +504,7 @@ lemma not_one_less_zero [simp]: "~ (1::'a::ordered_semidom) < 0" by (simp add: linorder_not_less) + subsection{*More Monotonicity*} text{*Strict monotonicity in both arguments*} @@ -559,6 +563,7 @@ apply simp done + subsection{*Cancellation Laws for Relationships With a Common Factor*} text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"}, @@ -621,7 +626,7 @@ proof (rule ccontr) assume "~ a < b" hence "b \ a" by (simp add: linorder_not_less) - hence "c*b \ c*a" by (rule mult_left_mono) + hence "c*b \ c*a" using nonneg by (rule mult_left_mono) with this and less show False by (simp add: linorder_not_less [symmetric]) qed @@ -632,7 +637,7 @@ proof (rule ccontr) assume "~ a < b" hence "b \ a" by (simp add: linorder_not_less) - hence "b*c \ a*c" by (rule mult_right_mono) + hence "b*c \ a*c" using nonneg by (rule mult_right_mono) with this and less show False by (simp add: linorder_not_less [symmetric]) qed @@ -746,6 +751,7 @@ add_diff_eq diff_add_eq diff_diff_eq diff_diff_eq2 diff_eq_eq eq_diff_eq *) + subsection {* Fields *} lemma right_inverse_eq: "b \ 0 ==> (a / b = 1) = (a = (b::'a::field))" @@ -968,6 +974,7 @@ "inverse (a/b) = b / (a::'a::{field,division_by_zero})" by (simp add: divide_inverse mult_commute) + subsection {* Calculations with fractions *} lemma nonzero_mult_divide_cancel_left: @@ -1038,6 +1045,7 @@ apply assumption done + subsubsection{*Special Cancellation Simprules for Division*} lemma mult_divide_cancel_left_if [simp]: @@ -1136,6 +1144,7 @@ apply simp_all done + subsection {* Ordered Fields *} lemma positive_imp_inverse_positive: @@ -1171,15 +1180,15 @@ qed lemma inverse_positive_imp_positive: - assumes inv_gt_0: "0 < inverse a" - and [simp]: "a \ 0" - shows "0 < (a::'a::ordered_field)" - proof - + assumes inv_gt_0: "0 < inverse a" + and nz: "a \ 0" + shows "0 < (a::'a::ordered_field)" +proof - have "0 < inverse (inverse a)" - by (rule positive_imp_inverse_positive) + using inv_gt_0 by (rule positive_imp_inverse_positive) thus "0 < a" - by (simp add: nonzero_inverse_inverse_eq) - qed + using nz by (simp add: nonzero_inverse_inverse_eq) +qed lemma inverse_positive_iff_positive [simp]: "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))" @@ -1188,15 +1197,15 @@ done lemma inverse_negative_imp_negative: - assumes inv_less_0: "inverse a < 0" - and [simp]: "a \ 0" - shows "a < (0::'a::ordered_field)" - proof - + assumes inv_less_0: "inverse a < 0" + and nz: "a \ 0" + shows "a < (0::'a::ordered_field)" +proof - have "inverse (inverse a) < 0" - by (rule negative_imp_inverse_negative) + using inv_less_0 by (rule negative_imp_inverse_negative) thus "a < 0" - by (simp add: nonzero_inverse_inverse_eq) - qed + using nz by (simp add: nonzero_inverse_inverse_eq) +qed lemma inverse_negative_iff_negative [simp]: "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))" @@ -1334,6 +1343,7 @@ "(inverse x \ 1) = (x \ 0 | 1 \ (x::'a::{ordered_field,division_by_zero}))" by (simp add: linorder_not_less [symmetric] one_less_inverse_iff) + subsection{*Simplification of Inequalities Involving Literal Divisors*} lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \ b/c) = (a*c \ b)" @@ -1500,6 +1510,7 @@ apply (erule nonzero_divide_eq_eq) done + subsection{*Division and Signs*} lemma zero_less_divide_iff: @@ -1578,6 +1589,7 @@ apply simp done + subsection{*Cancellation Laws for Division*} lemma divide_cancel_right [simp]: @@ -1592,6 +1604,7 @@ apply (simp add: divide_inverse field_mult_cancel_left) done + subsection {* Division and the Number One *} text{*Simplify expressions equated with 1*} @@ -1629,6 +1642,7 @@ declare zero_le_divide_1_iff [simp] declare divide_le_0_1_iff [simp] + subsection {* Ordering Rules for Division *} lemma divide_strict_right_mono: @@ -1706,6 +1720,7 @@ shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)" by (auto simp add: divide_less_eq) + subsection{*Conditional Simplification Rules: No Case Splits*} lemma le_divide_eq_1_pos [simp]: @@ -1758,6 +1773,7 @@ shows "(b/a = 1) = ((a \ 0 & a = b))" by (auto simp add: divide_eq_eq) + subsection {* Reasoning about inequalities with division *} lemma mult_right_le_one_le: "0 <= (x::'a::ordered_idom) ==> 0 <= y ==> y <= 1 @@ -1823,6 +1839,7 @@ declare times_divide_eq [simp] + subsection {* Ordered Fields are Dense *} lemma less_add_one: "a < (a+1::'a::ordered_semidom)" @@ -1995,6 +2012,7 @@ apply (simp add: order_less_imp_le); done; + subsection {* Bounds of products via negative and positive Part *} lemma mult_le_prts: @@ -2063,6 +2081,7 @@ then show ?thesis by simp qed + subsection {* Theorems for proof tools *} lemma add_mono_thms_ordered_semiring: diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/Wellfounded_Recursion.thy --- a/src/HOL/Wellfounded_Recursion.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/Wellfounded_Recursion.thy Thu Jun 14 18:33:31 2007 +0200 @@ -301,7 +301,7 @@ with A2 show "y \ Q" . qed qed - thus ?thesis .. + with `z' \ Q` show ?thesis .. qed qed qed diff -r 77645da0db85 -r aaca6a8e5414 src/HOL/ex/CTL.thy --- a/src/HOL/ex/CTL.thy Thu Jun 14 18:33:29 2007 +0200 +++ b/src/HOL/ex/CTL.thy Thu Jun 14 18:33:31 2007 +0200 @@ -99,7 +99,7 @@ then have "f (- u) \ - u" by auto then have "lfp f \ - u" by (rule lfp_lowerbound) from l and this have "x \ u" by auto - then show False by contradiction + with `x \ u` show False by contradiction qed qed show "- gfp (\s. - f (- s)) \ lfp f"