# HG changeset patch # User haftmann # Date 1273606029 -7200 # Node ID cdfbf867688ef2f923474f2a8d61c40575da78e5 # Parent 7902dc7ea11d56ba74665c8392a6d03f5a7c9185# Parent 957b5cd9dbe599e7f8987cb4fdf240271893fd2a merged diff -r 957b5cd9dbe5 -r cdfbf867688e NEWS --- a/NEWS Tue May 11 19:06:18 2010 +0200 +++ b/NEWS Tue May 11 21:27:09 2010 +0200 @@ -158,9 +158,12 @@ contain multiple interpretations of local typedefs (with different non-emptiness proofs), even in a global theory context. -* Theory Library/Coinductive_List has been removed -- superceded by +* Theory Library/Coinductive_List has been removed -- superseded by AFP/thys/Coinductive. +* Theory PReal, including the type "preal" and related operations, has +been removed. INCOMPATIBILITY. + * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY. @@ -320,6 +323,58 @@ Nat_Int_Bij.bij_int_to_nat_bij ~> bij_int_decode +*** HOLCF *** + +* Variable names in lemmas generated by the domain package have +changed; the naming scheme is now consistent with the HOL datatype +package. Some proof scripts may be affected, INCOMPATIBILITY. + +* The domain package no longer defines the function "foo_copy" for +recursive domain "foo". The reach lemma is now stated directly in +terms of "foo_take". Lemmas and proofs that mention "foo_copy" must +be reformulated in terms of "foo_take", INCOMPATIBILITY. + +* Most definedness lemmas generated by the domain package (previously +of the form "x ~= UU ==> foo$x ~= UU") now have an if-and-only-if form +like "foo$x = UU <-> x = UU", which works better as a simp rule. +Proof scripts that used definedness lemmas as intro rules may break, +potential INCOMPATIBILITY. + +* Induction and casedist rules generated by the domain package now +declare proper case_names (one called "bottom", and one named for each +constructor). INCOMPATIBILITY. + +* For mutually-recursive domains, separate "reach" and "take_lemma" +rules are generated for each domain, INCOMPATIBILITY. + + foo_bar.reach ~> foo.reach bar.reach + foo_bar.take_lemmas ~> foo.take_lemma bar.take_lemma + +* Some lemmas generated by the domain package have been renamed for +consistency with the datatype package, INCOMPATIBILITY. + + foo.ind ~> foo.induct + foo.finite_ind ~> foo.finite_induct + foo.coind ~> foo.coinduct + foo.casedist ~> foo.exhaust + foo.exhaust ~> foo.nchotomy + +* For consistency with other definition packages, the fixrec package +now generates qualified theorem names, INCOMPATIBILITY. + + foo_simps ~> foo.simps + foo_unfold ~> foo.unfold + foo_induct ~> foo.induct + +* The "contlub" predicate has been removed. Proof scripts should use +lemma contI2 in place of monocontlub2cont, INCOMPATIBILITY. + +* The "admw" predicate has been removed, INCOMPATIBILITY. + +* The constants cpair, cfst, and csnd have been removed in favor of +Pair, fst, and snd from Isabelle/HOL, INCOMPATIBILITY. + + *** ML *** * Sorts.certify_sort and derived "cert" operations for types and terms @@ -3255,7 +3310,7 @@ * Pure: axiomatic type classes are now purely definitional, with explicit proofs of class axioms and super class relations performed internally. See Pure/axclass.ML for the main internal interfaces -- -notably AxClass.define_class supercedes AxClass.add_axclass, and +notably AxClass.define_class supersedes AxClass.add_axclass, and AxClass.axiomatize_class/classrel/arity supersede Sign.add_classes/classrel/arities. @@ -4149,7 +4204,7 @@ * Pure/library.ML: the exception LIST has been given up in favour of the standard exceptions Empty and Subscript, as well as Library.UnequalLengths. Function like Library.hd and Library.tl are -superceded by the standard hd and tl functions etc. +superseded by the standard hd and tl functions etc. A number of basic list functions are no longer exported to the ML toplevel, as they are variants of predefined functions. The following @@ -4280,15 +4335,15 @@ * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, fold_types traverse types/terms from left to right, observing natural -argument order. Supercedes previous foldl_XXX versions, add_frees, +argument order. Supersedes previous foldl_XXX versions, add_frees, add_vars etc. have been adapted as well: INCOMPATIBILITY. * Pure: name spaces have been refined, with significant changes of the internal interfaces -- INCOMPATIBILITY. Renamed cond_extern(_table) -to extern(_table). The plain name entry path is superceded by a +to extern(_table). The plain name entry path is superseded by a general 'naming' context, which also includes the 'policy' to produce a fully qualified name and external accesses of a fully qualified -name; NameSpace.extend is superceded by context dependent +name; NameSpace.extend is superseded by context dependent Sign.declare_name. Several theory and proof context operations modify the naming context. Especially note Theory.restore_naming and ProofContext.restore_naming to get back to a sane state; note that @@ -4328,7 +4383,7 @@ etc.) as well as the sign field in Thm.rep_thm etc. have been retained for convenience -- they merely return the theory. -* Pure: type Type.tsig is superceded by theory in most interfaces. +* Pure: type Type.tsig is superseded by theory in most interfaces. * Pure: the Isar proof context type is already defined early in Pure as Context.proof (note that ProofContext.context and Proof.context are @@ -5460,7 +5515,7 @@ Eps_sym_eq -> some_sym_eq_trivial Eps_eq -> some_eq_trivial -* HOL: exhaust_tac on datatypes superceded by new generic case_tac; +* HOL: exhaust_tac on datatypes superseded by new generic case_tac; * HOL: removed obsolete theorem binding expand_if (refer to split_if instead); @@ -5598,7 +5653,7 @@ replaced "delrule" by "rule del"; * Isar/Provers: new 'hypsubst' method, plain 'subst' method and -'symmetric' attribute (the latter supercedes [RS sym]); +'symmetric' attribute (the latter supersedes [RS sym]); * Isar/Provers: splitter support (via 'split' attribute and 'simp' method modifier); 'simp' method: 'only:' modifier removes loopers as diff -r 957b5cd9dbe5 -r cdfbf867688e src/HOL/Complex.thy --- a/src/HOL/Complex.thy Tue May 11 19:06:18 2010 +0200 +++ b/src/HOL/Complex.thy Tue May 11 21:27:09 2010 +0200 @@ -353,16 +353,26 @@ apply (simp add: complex_norm_def) done +lemma tendsto_Complex [tendsto_intros]: + assumes "(f ---> a) net" and "(g ---> b) net" + shows "((\x. Complex (f x) (g x)) ---> Complex a b) net" +proof (rule tendstoI) + fix r :: real assume "0 < r" + hence "0 < r / sqrt 2" by (simp add: divide_pos_pos) + have "eventually (\x. dist (f x) a < r / sqrt 2) net" + using `(f ---> a) net` and `0 < r / sqrt 2` by (rule tendstoD) + moreover + have "eventually (\x. dist (g x) b < r / sqrt 2) net" + using `(g ---> b) net` and `0 < r / sqrt 2` by (rule tendstoD) + ultimately + show "eventually (\x. dist (Complex (f x) (g x)) (Complex a b) < r) net" + by (rule eventually_elim2) + (simp add: dist_norm real_sqrt_sum_squares_less) +qed + lemma LIMSEQ_Complex: "\X ----> a; Y ----> b\ \ (\n. Complex (X n) (Y n)) ----> Complex a b" -apply (rule LIMSEQ_I) -apply (subgoal_tac "0 < r / sqrt 2") -apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe) -apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe) -apply (rename_tac M N, rule_tac x="max M N" in exI, safe) -apply (simp add: real_sqrt_sum_squares_less) -apply (simp add: divide_pos_pos) -done +by (rule tendsto_Complex) instance complex :: banach proof diff -r 957b5cd9dbe5 -r cdfbf867688e src/HOL/Limits.thy --- a/src/HOL/Limits.thy Tue May 11 19:06:18 2010 +0200 +++ b/src/HOL/Limits.thy Tue May 11 21:27:09 2010 +0200 @@ -5,7 +5,7 @@ header {* Filters and Limits *} theory Limits -imports RealVector RComplete +imports RealVector begin subsection {* Nets *} diff -r 957b5cd9dbe5 -r cdfbf867688e src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Tue May 11 19:06:18 2010 +0200 +++ b/src/HOL/Nat_Numeral.thy Tue May 11 21:27:09 2010 +0200 @@ -83,7 +83,7 @@ end -context comm_ring_1 +context ring_1 begin lemma power2_minus [simp]: @@ -113,6 +113,19 @@ end +context ring_1_no_zero_divisors +begin + +lemma zero_eq_power2 [simp]: + "a\ = 0 \ a = 0" + unfolding power2_eq_square by simp + +lemma power2_eq_1_iff [simp]: + "a\ = 1 \ a = 1 \ a = - 1" + unfolding power2_eq_square by simp + +end + context linordered_ring begin @@ -163,10 +176,6 @@ context linordered_idom begin -lemma zero_eq_power2 [simp]: - "a\ = 0 \ a = 0" - by (force simp add: power2_eq_square) - lemma zero_le_power2 [simp]: "0 \ a\" by (simp add: power2_eq_square) diff -r 957b5cd9dbe5 -r cdfbf867688e src/HOL/RComplete.thy --- a/src/HOL/RComplete.thy Tue May 11 19:06:18 2010 +0200 +++ b/src/HOL/RComplete.thy Tue May 11 21:27:09 2010 +0200 @@ -837,5 +837,27 @@ apply simp done +subsection {* Exponentiation with floor *} + +lemma floor_power: + assumes "x = real (floor x)" + shows "floor (x ^ n) = floor x ^ n" +proof - + have *: "x ^ n = real (floor x ^ n)" + using assms by (induct n arbitrary: x) simp_all + show ?thesis unfolding real_of_int_inject[symmetric] + unfolding * floor_real_of_int .. +qed + +lemma natfloor_power: + assumes "x = real (natfloor x)" + shows "natfloor (x ^ n) = natfloor x ^ n" +proof - + from assms have "0 \ floor x" by auto + note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \ floor x`]] + from floor_power[OF this] + show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \ floor x`, symmetric] + by simp +qed end diff -r 957b5cd9dbe5 -r cdfbf867688e src/HOL/RealPow.thy --- a/src/HOL/RealPow.thy Tue May 11 19:06:18 2010 +0200 +++ b/src/HOL/RealPow.thy Tue May 11 21:27:09 2010 +0200 @@ -69,18 +69,6 @@ shows "x * x - 1 = (x + 1) * (x - 1)" by (simp add: algebra_simps) -(* 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 - (* 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)" @@ -113,54 +101,4 @@ by (rule power_le_imp_le_base) qed -subsection {*Floor*} - -lemma floor_power: - assumes "x = real (floor x)" - shows "floor (x ^ n) = floor x ^ n" -proof - - have *: "x ^ n = real (floor x ^ n)" - using assms by (induct n arbitrary: x) simp_all - show ?thesis unfolding real_of_int_inject[symmetric] - unfolding * floor_real_of_int .. -qed - -lemma natfloor_power: - assumes "x = real (natfloor x)" - shows "natfloor (x ^ n) = natfloor x ^ n" -proof - - from assms have "0 \ floor x" by auto - note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \ floor x`]] - from floor_power[OF this] - show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \ floor x`, symmetric] - by simp -qed - -subsection {*Various Other Theorems*} - -lemma real_le_add_half_cancel: "(x + y/2 \ (y::real)) = (x \ y /2)" -by auto - -lemma real_mult_inverse_cancel: - "[|(0::real) < x; 0 < x1; x1 * y < x * u |] - ==> inverse x * y < inverse x1 * u" -apply (rule_tac c=x in mult_less_imp_less_left) -apply (auto simp add: mult_assoc [symmetric]) -apply (simp (no_asm) add: mult_ac) -apply (rule_tac c=x1 in mult_less_imp_less_right) -apply (auto simp add: mult_ac) -done - -lemma real_mult_inverse_cancel2: - "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1" -apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) -done - -(* 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 957b5cd9dbe5 -r cdfbf867688e src/HOL/Rings.thy --- a/src/HOL/Rings.thy Tue May 11 19:06:18 2010 +0200 +++ b/src/HOL/Rings.thy Tue May 11 21:27:09 2010 +0200 @@ -349,6 +349,17 @@ class ring_1_no_zero_divisors = ring_1 + ring_no_zero_divisors begin +lemma square_eq_1_iff [simp]: + "x * x = 1 \ x = 1 \ x = - 1" +proof - + have "(x - 1) * (x + 1) = x * x - 1" + by (simp add: algebra_simps) + hence "x * x = 1 \ (x - 1) * (x + 1) = 0" + by simp + thus ?thesis + by (simp add: eq_neg_iff_add_eq_0) +qed + lemma mult_cancel_right1 [simp]: "c = b * c \ c = 0 \ b = 1" by (insert mult_cancel_right [of 1 c b], force) diff -r 957b5cd9dbe5 -r cdfbf867688e src/HOL/SEQ.thy --- a/src/HOL/SEQ.thy Tue May 11 19:06:18 2010 +0200 +++ b/src/HOL/SEQ.thy Tue May 11 21:27:09 2010 +0200 @@ -10,7 +10,7 @@ header {* Sequences and Convergence *} theory SEQ -imports Limits +imports Limits RComplete begin abbreviation diff -r 957b5cd9dbe5 -r cdfbf867688e src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue May 11 19:06:18 2010 +0200 +++ b/src/HOL/Transcendental.thy Tue May 11 21:27:09 2010 +0200 @@ -1663,6 +1663,26 @@ lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)" by simp +lemma real_mult_inverse_cancel: + "[|(0::real) < x; 0 < x1; x1 * y < x * u |] + ==> inverse x * y < inverse x1 * u" +apply (rule_tac c=x in mult_less_imp_less_left) +apply (auto simp add: mult_assoc [symmetric]) +apply (simp (no_asm) add: mult_ac) +apply (rule_tac c=x1 in mult_less_imp_less_right) +apply (auto simp add: mult_ac) +done + +lemma real_mult_inverse_cancel2: + "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1" +apply (auto dest: real_mult_inverse_cancel simp add: mult_ac) +done + +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) + lemma cos_two_less_zero [simp]: "cos (2) < 0" apply (cut_tac x = 2 in cos_paired) apply (drule sums_minus)