# HG changeset patch # User huffman # Date 1267984996 28800 # Node ID e0b2a6e773db7d45fd842b76c9c779b942477a1d # Parent fe9b43a08187c444a67e9f56197317de72484074# Parent f1456d045151406ef0da6f085493b398acb34cfa merged diff -r f1456d045151 -r e0b2a6e773db src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOL/Complete_Lattice.thy Sun Mar 07 10:03:16 2010 -0800 @@ -82,6 +82,12 @@ "\UNIV = top" by (simp add: Inf_Sup Inf_empty [symmetric]) +lemma Sup_le_iff: "Sup A \ b \ (\a\A. a \ b)" + by (auto intro: Sup_least dest: Sup_upper) + +lemma le_Inf_iff: "b \ Inf A \ (\a\A. b \ a)" + by (auto intro: Inf_greatest dest: Inf_lower) + definition SUPR :: "'b set \ ('b \ 'a) \ 'a" where "SUPR A f = \ (f ` A)" @@ -126,6 +132,12 @@ lemma le_INFI: "(\i. i : A \ u \ M i) \ u \ (INF i:A. M i)" by (auto simp add: INFI_def intro: Inf_greatest) +lemma SUP_le_iff: "(SUP i:A. M i) \ u \ (\i \ A. M i \ u)" + unfolding SUPR_def by (auto simp add: Sup_le_iff) + +lemma le_INF_iff: "u \ (INF i:A. M i) \ (\i \ A. u \ M i)" + unfolding INFI_def by (auto simp add: le_Inf_iff) + lemma SUP_const[simp]: "A \ {} \ (SUP i:A. M) = M" by (auto intro: antisym SUP_leI le_SUPI) @@ -384,7 +396,7 @@ by blast lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)" - by blast + by (fact SUP_le_iff) lemma image_Union: "f ` \S = (\x\S. f ` x)" by blast @@ -591,7 +603,7 @@ by blast lemma INT_subset_iff: "(B \ (\i\I. A i)) = (\i\I. B \ A i)" - by blast + by (fact le_INF_iff) lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ INTER A B" by blast diff -r f1456d045151 -r e0b2a6e773db src/HOL/Int.thy --- a/src/HOL/Int.thy Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOL/Int.thy Sun Mar 07 10:03:16 2010 -0800 @@ -1262,6 +1262,15 @@ notation (xsymbols) Ints ("\") +lemma Ints_of_int [simp]: "of_int z \ \" + by (simp add: Ints_def) + +lemma Ints_of_nat [simp]: "of_nat n \ \" +apply (simp add: Ints_def) +apply (rule range_eqI) +apply (rule of_int_of_nat_eq [symmetric]) +done + lemma Ints_0 [simp]: "0 \ \" apply (simp add: Ints_def) apply (rule range_eqI) @@ -1286,12 +1295,21 @@ apply (rule of_int_minus [symmetric]) done +lemma Ints_diff [simp]: "a \ \ \ b \ \ \ a - b \ \" +apply (auto simp add: Ints_def) +apply (rule range_eqI) +apply (rule of_int_diff [symmetric]) +done + lemma Ints_mult [simp]: "a \ \ \ b \ \ \ a * b \ \" apply (auto simp add: Ints_def) apply (rule range_eqI) apply (rule of_int_mult [symmetric]) done +lemma Ints_power [simp]: "a \ \ \ a ^ n \ \" +by (induct n) simp_all + lemma Ints_cases [cases set: Ints]: assumes "q \ \" obtains (of_int) z where "q = of_int z" @@ -1308,12 +1326,6 @@ end -lemma Ints_diff [simp]: "a \ \ \ b \ \ \ a-b \ \" -apply (auto simp add: Ints_def) -apply (rule range_eqI) -apply (rule of_int_diff [symmetric]) -done - text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} lemma Ints_double_eq_0_iff: @@ -1350,10 +1362,15 @@ qed qed -lemma Ints_number_of: +lemma Ints_number_of [simp]: "(number_of w :: 'a::number_ring) \ Ints" unfolding number_of_eq Ints_def by simp +lemma Nats_number_of [simp]: + "Int.Pls \ w \ (number_of w :: 'a::number_ring) \ Nats" +unfolding Int.Pls_def number_of_eq +by (simp only: of_nat_nat [symmetric] of_nat_in_Nats) + lemma Ints_odd_less_0: assumes in_Ints: "a \ Ints" shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" diff -r f1456d045151 -r e0b2a6e773db src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOL/Nat.thy Sun Mar 07 10:03:16 2010 -0800 @@ -1400,6 +1400,20 @@ apply (rule of_nat_mult [symmetric]) done +lemma Nats_cases [cases set: Nats]: + assumes "x \ \" + obtains (of_nat) n where "x = of_nat n" + unfolding Nats_def +proof - + from `x \ \` have "x \ range of_nat" unfolding Nats_def . + then obtain n where "x = of_nat n" .. + then show thesis .. +qed + +lemma Nats_induct [case_names of_nat, induct set: Nats]: + "x \ \ \ (\n. P (of_nat n)) \ P x" + by (rule Nats_cases) auto + end diff -r f1456d045151 -r e0b2a6e773db src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOL/Nat_Numeral.thy Sun Mar 07 10:03:16 2010 -0800 @@ -113,7 +113,7 @@ end -context linordered_ring_strict +context linordered_ring begin lemma sum_squares_ge_zero: @@ -124,6 +124,11 @@ "\ x * x + y * y < 0" by (simp add: not_less sum_squares_ge_zero) +end + +context linordered_ring_strict +begin + lemma sum_squares_eq_zero_iff: "x * x + y * y = 0 \ x = 0 \ y = 0" by (simp add: add_nonneg_eq_0_iff) @@ -134,14 +139,7 @@ lemma sum_squares_gt_zero_iff: "0 < x * x + y * y \ x \ 0 \ y \ 0" -proof - - have "x * x + y * y \ 0 \ x \ 0 \ y \ 0" - by (simp add: sum_squares_eq_zero_iff) - then have "0 \ x * x + y * y \ x \ 0 \ y \ 0" - by auto - then show ?thesis - by (simp add: less_le sum_squares_ge_zero) -qed + by (simp add: not_le [symmetric] sum_squares_le_zero_iff) end diff -r f1456d045151 -r e0b2a6e773db src/HOL/Parity.thy --- a/src/HOL/Parity.thy Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOL/Parity.thy Sun Mar 07 10:03:16 2010 -0800 @@ -218,7 +218,7 @@ done lemma zero_le_even_power: "even n ==> - 0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n" + 0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n" apply (simp add: even_nat_equiv_def2) apply (erule exE) apply (erule ssubst) diff -r f1456d045151 -r e0b2a6e773db src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOL/RealDef.thy Sun Mar 07 10:03:16 2010 -0800 @@ -701,6 +701,9 @@ lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" by (insert real_of_int_div2 [of n x], simp) +lemma Ints_real_of_int [simp]: "real (x::int) \ Ints" +unfolding real_of_int_def by (rule Ints_of_int) + subsection{*Embedding the Naturals into the Reals*} @@ -852,6 +855,12 @@ apply (simp only: real_of_int_real_of_nat) done +lemma Nats_real_of_nat [simp]: "real (n::nat) \ Nats" +unfolding real_of_nat_def by (rule of_nat_in_Nats) + +lemma Ints_real_of_nat [simp]: "real (n::nat) \ Ints" +unfolding real_of_nat_def by (rule Ints_of_nat) + subsection{* Rationals *} diff -r f1456d045151 -r e0b2a6e773db src/HOL/RealPow.thy --- a/src/HOL/RealPow.thy Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOL/RealPow.thy Sun Mar 07 10:03:16 2010 -0800 @@ -24,71 +24,76 @@ apply (rule two_realpow_ge_one) done -lemma realpow_Suc_le_self: "[| 0 \ r; r \ (1::real) |] ==> r ^ Suc n \ r" +(* TODO: no longer real-specific; rename and move elsewhere *) +lemma realpow_Suc_le_self: + fixes r :: "'a::linordered_semidom" + shows "[| 0 \ r; r \ 1 |] ==> r ^ Suc n \ r" by (insert power_decreasing [of 1 "Suc n" r], simp) -lemma realpow_minus_mult [rule_format]: - "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" -apply (simp split add: nat_diff_split) -done +(* TODO: no longer real-specific; rename and move elsewhere *) +lemma realpow_minus_mult: + fixes x :: "'a::monoid_mult" + shows "0 < n \ x ^ (n - 1) * x = x ^ n" +by (simp add: power_commutes split add: nat_diff_split) +(* TODO: no longer real-specific; rename and move elsewhere *) lemma realpow_two_diff: - "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" + fixes x :: "'a::comm_ring_1" + shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)" by (simp add: algebra_simps) +(* TODO: move elsewhere *) +lemma add_eq_0_iff: + fixes x y :: "'a::group_add" + shows "x + y = 0 \ y = - x" +by (auto dest: minus_unique) + +(* TODO: no longer real-specific; rename and move elsewhere *) lemma realpow_two_disj: - "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" -apply (cut_tac x = x and y = y in realpow_two_diff) -apply auto -done + fixes x :: "'a::idom" + shows "(x^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)" +using realpow_two_diff [of x y] +by (auto simp add: add_eq_0_iff) subsection{* Squares of Reals *} +(* FIXME: declare this [simp] for all types, or not at all *) lemma real_two_squares_add_zero_iff [simp]: "(x * x + y * y = 0) = ((x::real) = 0 \ y = 0)" by (rule sum_squares_eq_zero_iff) -lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" -by simp - -lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" -by simp - -lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0" -by (simp add: real_add_eq_0_iff [symmetric]) - -lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)" -by (simp add: left_distrib right_diff_distrib) +(* TODO: no longer real-specific; rename and move elsewhere *) +lemma real_squared_diff_one_factored: + fixes x :: "'a::ring_1" + shows "x * x - 1 = (x + 1) * (x - 1)" +by (simp add: algebra_simps) -lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)" -apply auto -apply (drule right_minus_eq [THEN iffD2]) -apply (auto simp add: real_squared_diff_one_factored) -done +(* TODO: no longer real-specific; rename and move elsewhere *) +lemma real_mult_is_one [simp]: + fixes x :: "'a::ring_1_no_zero_divisors" + shows "x * x = 1 \ x = 1 \ x = - 1" +proof - + have "x * x = 1 \ (x + 1) * (x - 1) = 0" + by (simp add: algebra_simps) + also have "\ \ x = 1 \ x = - 1" + by (auto simp add: add_eq_0_iff minus_equation_iff [of _ 1]) + finally show ?thesis . +qed -lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)" -by simp - -lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)" -by simp - +(* FIXME: declare this [simp] for all types, or not at all *) lemma realpow_two_sum_zero_iff [simp]: "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" by (rule sum_power2_eq_zero_iff) +(* FIXME: declare this [simp] for all types, or not at all *) lemma realpow_two_le_add_order [simp]: "(0::real) \ u ^ 2 + v ^ 2" by (rule sum_power2_ge_zero) +(* FIXME: declare this [simp] for all types, or not at all *) lemma realpow_two_le_add_order2 [simp]: "(0::real) \ u ^ 2 + v ^ 2 + w ^ 2" by (intro add_nonneg_nonneg zero_le_power2) -lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y" -by (simp add: sum_squares_gt_zero_iff) - -lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y" -by (simp add: sum_squares_gt_zero_iff) - lemma real_minus_mult_self_le [simp]: "-(u * u) \ (x * (x::real))" by (rule_tac j = 0 in real_le_trans, auto) @@ -96,8 +101,9 @@ by (auto simp add: power2_eq_square) (* The following theorem is by Benjamin Porter *) +(* TODO: no longer real-specific; rename and move elsewhere *) lemma real_sq_order: - fixes x::real + fixes x :: "'a::linordered_semidom" assumes xgt0: "0 \ x" and ygt0: "0 \ y" and sq: "x^2 \ y^2" shows "x \ y" proof - @@ -150,8 +156,11 @@ apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) done -lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))" -by (case_tac "n", auto) +(* TODO: no longer real-specific; rename and move elsewhere *) +lemma realpow_num_eq_if: + fixes m :: "'a::power" + shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))" +by (cases n, auto) end diff -r f1456d045151 -r e0b2a6e773db src/HOL/Rings.thy --- a/src/HOL/Rings.thy Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOL/Rings.thy Sun Mar 07 10:03:16 2010 -0800 @@ -796,6 +796,13 @@ auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg) qed (auto simp add: abs_if) +lemma zero_le_square [simp]: "0 \ a * a" + using linear [of 0 a] + by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) + +lemma not_square_less_zero [simp]: "\ (a * a < 0)" + by (simp add: not_less) + end (* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors. @@ -873,12 +880,6 @@ apply force done -lemma zero_le_square [simp]: "0 \ a * a" -by (simp add: zero_le_mult_iff linear) - -lemma not_square_less_zero [simp]: "\ (a * a < 0)" -by (simp add: not_less) - text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"}, also with the relations @{text "\"} and equality.*} diff -r f1456d045151 -r e0b2a6e773db src/HOL/Tools/arith_data.ML --- a/src/HOL/Tools/arith_data.ML Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOL/Tools/arith_data.ML Sun Mar 07 10:03:16 2010 -0800 @@ -55,7 +55,7 @@ let val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt fun invoke (_, (name, tac)) k st = (if verbose - then warning ("Trying " ^ name ^ "...") else (); + then priority ("Trying " ^ name ^ "...") else (); tac verbose ctxt k st); in FIRST' (map invoke (rev tactics)) end; diff -r f1456d045151 -r e0b2a6e773db src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Mar 07 15:51:29 2010 +0100 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Mar 07 10:03:16 2010 -0800 @@ -168,13 +168,17 @@ val take_rews = ax_take_0 :: ax_take_strict :: take_apps; end; +val case_ns = + "bottom" :: map (fn (b,_,_) => Binding.name_of b) (snd dom_eqn); + in thy |> Sign.add_path (Long_Name.base_name dname) |> snd o PureThy.add_thmss [ ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]), ((Binding.name "exhaust" , [exhaust] ), []), - ((Binding.name "casedist" , [casedist] ), [Induct.cases_type dname]), + ((Binding.name "casedist" , [casedist] ), + [Rule_Cases.case_names case_ns, Induct.cases_type dname]), ((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]), ((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]), ((Binding.name "con_rews" , con_rews ), @@ -422,8 +426,20 @@ | ERROR _ => (warning "Cannot prove induction rule"; ([], TrueI)); +val case_ns = + let + val bottoms = + if length dnames = 1 then ["bottom"] else + map (fn s => "bottom_" ^ Long_Name.base_name s) dnames; + fun one_eq bot (_,cons) = + bot :: map (fn (c,_) => Long_Name.base_name c) cons; + in flat (map2 one_eq bottoms eqs) end; + val inducts = Project_Rule.projections (ProofContext.init thy) ind; -fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); +fun ind_rule (dname, rule) = + ((Binding.empty, [rule]), + [Rule_Cases.case_names case_ns, Induct.induct_type dname]); + val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); in thy |> Sign.add_path comp_dnam