--- 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
--- 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 "((\<lambda>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 (\<lambda>x. dist (f x) a < r / sqrt 2) net"
+ using `(f ---> a) net` and `0 < r / sqrt 2` by (rule tendstoD)
+ moreover
+ have "eventually (\<lambda>x. dist (g x) b < r / sqrt 2) net"
+ using `(g ---> b) net` and `0 < r / sqrt 2` by (rule tendstoD)
+ ultimately
+ show "eventually (\<lambda>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:
"\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>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
--- 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 *}
--- 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\<twosuperior> = 0 \<longleftrightarrow> a = 0"
+ unfolding power2_eq_square by simp
+
+lemma power2_eq_1_iff [simp]:
+ "a\<twosuperior> = 1 \<longleftrightarrow> a = 1 \<or> 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\<twosuperior> = 0 \<longleftrightarrow> a = 0"
- by (force simp add: power2_eq_square)
-
lemma zero_le_power2 [simp]:
"0 \<le> a\<twosuperior>"
by (simp add: power2_eq_square)
--- 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 \<le> floor x" by auto
+ note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
+ from floor_power[OF this]
+ show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
+ by simp
+qed
end
--- 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 \<longleftrightarrow> x = 1 \<or> x = - 1"
-proof -
- have "x * x = 1 \<longleftrightarrow> (x + 1) * (x - 1) = 0"
- by (simp add: algebra_simps)
- also have "\<dots> \<longleftrightarrow> x = 1 \<or> 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 \<le> floor x" by auto
- note assms[unfolded natfloor_def real_nat_eq_real[OF `0 \<le> floor x`]]
- from floor_power[OF this]
- show ?thesis unfolding natfloor_def nat_power_eq[OF `0 \<le> floor x`, symmetric]
- by simp
-qed
-
-subsection {*Various Other Theorems*}
-
-lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> 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
--- 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 \<longleftrightarrow> x = 1 \<or> x = - 1"
+proof -
+ have "(x - 1) * (x + 1) = x * x - 1"
+ by (simp add: algebra_simps)
+ hence "x * x = 1 \<longleftrightarrow> (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 \<longleftrightarrow> c = 0 \<or> b = 1"
by (insert mult_cancel_right [of 1 c b], force)
--- 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
--- 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)