--- a/NEWS Wed May 12 11:07:46 2010 +0200
+++ b/NEWS Wed May 12 11:08:15 2010 +0200
@@ -143,7 +143,11 @@
* Theorem Int.int_induct renamed to Int.int_of_nat_induct and is
no longer shadowed. INCOMPATIBILITY.
-* Dropped theorem duplicate comp_arith; use semiring_norm instead. INCOMPATIBILITY.
+* Dropped theorem duplicate comp_arith; use semiring_norm instead.
+INCOMPATIBILITY.
+
+* Dropped theorem RealPow.real_sq_order; use power2_le_imp_le instead.
+INCOMPATIBILITY.
* Dropped normalizing. Use semiring classes directly. INCOMPATIBILITY.
@@ -160,9 +164,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.
@@ -322,6 +329,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
@@ -3257,7 +3316,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.
@@ -4151,7 +4210,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
@@ -4282,15 +4341,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
@@ -4330,7 +4389,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
@@ -5462,7 +5521,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);
@@ -5600,7 +5659,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 Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/Complex.thy Wed May 12 11:08:15 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/IsaMakefile Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/IsaMakefile Wed May 12 11:08:15 2010 +0200
@@ -357,7 +357,6 @@
Rat.thy \
Real.thy \
RealDef.thy \
- RealPow.thy \
RealVector.thy \
SEQ.thy \
Series.thy \
--- a/src/HOL/Library/Char_nat.thy Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/Library/Char_nat.thy Wed May 12 11:08:15 2010 +0200
@@ -51,7 +51,7 @@
lemma nibble_of_nat_norm:
"nibble_of_nat (n mod 16) = nibble_of_nat n"
- unfolding nibble_of_nat_def Let_def by auto
+ unfolding nibble_of_nat_def mod_mod_trivial ..
lemmas [code] = nibble_of_nat_norm [symmetric]
@@ -72,7 +72,7 @@
"nibble_of_nat 13 = NibbleD"
"nibble_of_nat 14 = NibbleE"
"nibble_of_nat 15 = NibbleF"
- unfolding nibble_of_nat_def Let_def by auto
+ unfolding nibble_of_nat_def by auto
lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
[simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
@@ -83,15 +83,15 @@
lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
proof -
have nibble_nat_enum:
- "n mod 16 \<in> {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}"
+ "n mod 16 \<in> {15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0}"
proof -
have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))}" by simp
from this [simplified set_unfold atLeastAtMost_singleton]
- show ?thesis by auto
+ show ?thesis by (simp add: numeral_2_eq_2 [symmetric])
qed
- then show ?thesis unfolding nibble_of_nat_def Let_def
+ then show ?thesis unfolding nibble_of_nat_def
by auto
qed
--- a/src/HOL/Limits.thy Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/Limits.thy Wed May 12 11:08:15 2010 +0200
@@ -5,7 +5,7 @@
header {* Filters and Limits *}
theory Limits
-imports RealVector RComplete
+imports RealVector
begin
subsection {* Nets *}
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Wed May 12 11:08:15 2010 +0200
@@ -92,7 +92,7 @@
fun log thy s =
let fun append_to n = if n = "" then K () else File.append (Path.explode n)
- in append_to (Config.get_thy thy logfile) (s ^ "\n") end
+ in append_to (Config.get_global thy logfile) (s ^ "\n") end
(* FIXME: with multithreading and parallel proofs enabled, we might need to
encapsulate this inside a critical section *)
@@ -108,7 +108,7 @@
| in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
fun only_within_range thy pos f x =
- let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
+ let val l = Config.get_global thy start_line and r = Config.get_global thy end_line
in if in_range l r (Position.line_of pos) then f x else () end
in
@@ -118,7 +118,7 @@
val thy = Proof.theory_of pre
val pos = Toplevel.pos_of tr
val name = Toplevel.name_of tr
- val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
+ val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout))
val str0 = string_of_int o the_default 0
val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
--- a/src/HOL/Nat_Numeral.thy Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/Nat_Numeral.thy Wed May 12 11:08:15 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)
@@ -703,7 +712,7 @@
if_True add_0 add_Suc add_number_of_left mult_number_of_left
numeral_1_eq_1 [symmetric] Suc_eq_plus1
numeral_0_eq_0 [symmetric] numerals [symmetric]
- iszero_simps not_iszero_Numeral1
+ not_iszero_Numeral1
lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
by (fact Let_def)
--- a/src/HOL/Parity.thy Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/Parity.thy Wed May 12 11:08:15 2010 +0200
@@ -61,7 +61,7 @@
subsection {* Behavior under integer arithmetic operations *}
declare dvd_def[algebra]
lemma nat_even_iff_2_dvd[algebra]: "even (x::nat) \<longleftrightarrow> 2 dvd x"
- by (presburger add: even_nat_def even_def)
+ by presburger
lemma int_even_iff_2_dvd[algebra]: "even (x::int) \<longleftrightarrow> 2 dvd x"
by presburger
--- a/src/HOL/RComplete.thy Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/RComplete.thy Wed May 12 11:08:15 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/RealDef.thy Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/RealDef.thy Wed May 12 11:08:15 2010 +0200
@@ -1539,6 +1539,7 @@
lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
by arith
+text {* FIXME: redundant with @{text add_eq_0_iff} below *}
lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)"
by auto
@@ -1554,8 +1555,86 @@
lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (-x \<le> y)"
by auto
+subsection {* Lemmas about powers *}
-subsubsection{*Density of the Reals*}
+text {* FIXME: declare this in Rings.thy or not at all *}
+declare abs_mult_self [simp]
+
+(* used by Import/HOL/real.imp *)
+lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
+by simp
+
+lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
+apply (induct "n")
+apply (auto simp add: real_of_nat_Suc)
+apply (subst mult_2)
+apply (erule add_less_le_mono)
+apply (rule two_realpow_ge_one)
+done
+
+text {* TODO: no longer real-specific; rename and move elsewhere *}
+lemma realpow_Suc_le_self:
+ fixes r :: "'a::linordered_semidom"
+ shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
+by (insert power_decreasing [of 1 "Suc n" r], simp)
+
+text {* TODO: no longer real-specific; rename and move elsewhere *}
+lemma realpow_minus_mult:
+ fixes x :: "'a::monoid_mult"
+ shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
+by (simp add: power_commutes split add: nat_diff_split)
+
+text {* TODO: no longer real-specific; rename and move elsewhere *}
+lemma realpow_two_diff:
+ fixes x :: "'a::comm_ring_1"
+ shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
+by (simp add: algebra_simps)
+
+text {* TODO: move elsewhere *}
+lemma add_eq_0_iff:
+ fixes x y :: "'a::group_add"
+ shows "x + y = 0 \<longleftrightarrow> y = - x"
+by (auto dest: minus_unique)
+
+text {* TODO: no longer real-specific; rename and move elsewhere *}
+lemma realpow_two_disj:
+ 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)
+
+text {* 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 \<and> y = 0)"
+by (rule sum_squares_eq_zero_iff)
+
+text {* 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)
+
+text {* 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)
+
+text {* FIXME: declare this [simp] for all types, or not at all *}
+lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
+by (rule sum_power2_ge_zero)
+
+text {* FIXME: declare this [simp] for all types, or not at all *}
+lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
+by (intro add_nonneg_nonneg zero_le_power2)
+
+lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
+by (rule_tac y = 0 in order_trans, auto)
+
+lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
+by (auto simp add: power2_eq_square)
+
+
+subsection{*Density of the Reals*}
lemma real_lbound_gt_zero:
"[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
--- a/src/HOL/RealPow.thy Wed May 12 11:07:46 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,166 +0,0 @@
-(* Title : HOL/RealPow.thy
- Author : Jacques D. Fleuriot
- Copyright : 1998 University of Cambridge
-*)
-
-header {* Natural powers theory *}
-
-theory RealPow
-imports RealDef RComplete
-begin
-
-(* FIXME: declare this in Rings.thy or not at all *)
-declare abs_mult_self [simp]
-
-(* used by Import/HOL/real.imp *)
-lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
-by simp
-
-lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
-apply (induct "n")
-apply (auto simp add: real_of_nat_Suc)
-apply (subst mult_2)
-apply (erule add_less_le_mono)
-apply (rule two_realpow_ge_one)
-done
-
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma realpow_Suc_le_self:
- fixes r :: "'a::linordered_semidom"
- shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
-by (insert power_decreasing [of 1 "Suc n" r], simp)
-
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma realpow_minus_mult:
- fixes x :: "'a::monoid_mult"
- shows "0 < n \<Longrightarrow> 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:
- 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 \<longleftrightarrow> y = - x"
-by (auto dest: minus_unique)
-
-(* TODO: no longer real-specific; rename and move elsewhere *)
-lemma realpow_two_disj:
- 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 \<and> y = 0)"
-by (rule sum_squares_eq_zero_iff)
-
-(* 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)
-
-(* 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)"
-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) \<le> 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) \<le> u ^ 2 + v ^ 2 + w ^ 2"
-by (intro add_nonneg_nonneg zero_le_power2)
-
-lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
-by (rule_tac y = 0 in order_trans, auto)
-
-lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
-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 :: "'a::linordered_semidom"
- assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
- shows "x \<le> y"
-proof -
- from sq have "x ^ Suc (Suc 0) \<le> y ^ Suc (Suc 0)"
- by (simp only: numeral_2_eq_2)
- thus "x \<le> y" using ygt0
- 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/RealVector.thy Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/RealVector.thy Wed May 12 11:08:15 2010 +0200
@@ -5,7 +5,7 @@
header {* Vector Spaces and Algebras over the Reals *}
theory RealVector
-imports RealPow
+imports RComplete
begin
subsection {* Locale for additive functions *}
--- a/src/HOL/Rings.thy Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/Rings.thy Wed May 12 11:08:15 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 Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/SEQ.thy Wed May 12 11:08:15 2010 +0200
@@ -10,7 +10,7 @@
header {* Sequences and Convergence *}
theory SEQ
-imports Limits
+imports Limits RComplete
begin
abbreviation
--- a/src/HOL/Tools/Qelim/cooper.ML Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed May 12 11:08:15 2010 +0200
@@ -77,7 +77,9 @@
val iT = HOLogic.intT
val bT = HOLogic.boolT;
-val dest_numeral = HOLogic.dest_number #> snd;
+val dest_number = HOLogic.dest_number #> snd;
+val perhaps_number = try dest_number;
+val is_number = can dest_number;
val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
@@ -171,10 +173,8 @@
val [addC, mulC, subC] = map term_of [cadd, cmulC, cminus]
val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}];
-val is_numeral = can dest_numeral;
-
-fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
-fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));
+fun numeral1 f n = HOLogic.mk_number iT (f (dest_number n));
+fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n));
val [minus1,plus1] =
map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
@@ -253,16 +253,16 @@
exception COOPER of string;
-fun lint vars tm = if is_numeral tm then tm else case tm of
+fun lint vars tm = if is_number tm then tm else case tm of
Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
| Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
| Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
| Const (@{const_name Groups.times}, _) $ s $ t =>
let val s' = lint vars s
val t' = lint vars t
- in if is_numeral s' then (linear_cmul (dest_numeral s') t')
- else if is_numeral t' then (linear_cmul (dest_numeral t') s')
- else raise COOPER "lint: not linear"
+ in case perhaps_number s' of SOME n => linear_cmul n t'
+ | NONE => (case perhaps_number t' of SOME n => linear_cmul n s'
+ | NONE => raise COOPER "lint: not linear")
end
| _ => addC $ (mulC $ one $ tm) $ zero;
@@ -277,14 +277,14 @@
(case lint vs (subC$t$s) of
(t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
- else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
+ else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r
else b$(m$c$y)$(linear_neg r)
| t => b$zero$t)
| lin (vs as x::_) (b$s$t) =
(case lint vs (subC$t$s) of
(t as a$(m$c$y)$r) =>
if x <> y then b$zero$t
- else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
+ else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r
else b$(linear_neg r)$(m$c$y)
| t => b$zero$t)
| lin vs fm = fm;
@@ -307,12 +307,12 @@
val th = Conv.binop_conv (lint_conv ctxt vs) ct
val (d',t') = Thm.dest_binop (Thm.rhs_of th)
val (dt',tt') = (term_of d', term_of t')
- in if is_numeral dt' andalso is_numeral tt'
+ in if is_number dt' andalso is_number tt'
then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th
else
let
val dth =
- ((if dest_numeral (term_of d') < 0 then
+ ((if dest_number (term_of d') < 0 then
Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs)))
(Thm.transitive th (inst' [d',t'] dvd_uminus))
else th) handle TERM _ => th)
@@ -320,7 +320,7 @@
in
case tt' of
Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
- let val x = dest_numeral c
+ let val x = dest_number c
in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs)))
(Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
else dth end
@@ -345,13 +345,13 @@
Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x aconv y andalso member (op =)
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
- then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
+ then (ins (dest_number c) acc,dacc) else (acc,dacc)
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x aconv y andalso member (op =)
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
- then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
+ then (ins (dest_number c) acc, dacc) else (acc,dacc)
| Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
- if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
+ if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc)
| Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
| Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
@@ -374,7 +374,7 @@
let val tab = fold Inttab.update
(ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
in
- fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_numeral))
+ fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_number))
handle Option =>
(writeln ("noz: Theorems-Table contains no entry for " ^
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
@@ -387,15 +387,15 @@
| Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
if x=y andalso member (op =)
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
- then cv (l div dest_numeral c) t else Thm.reflexive t
+ then cv (l div dest_number c) t else Thm.reflexive t
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
if x=y andalso member (op =)
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
- then cv (l div dest_numeral c) t else Thm.reflexive t
+ then cv (l div dest_number c) t else Thm.reflexive t
| Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) =>
if x=y then
let
- val k = l div dest_numeral c
+ val k = l div dest_number c
val kt = HOLogic.mk_number iT k
val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
@@ -447,8 +447,8 @@
| Le t => (bacc, ins (plus1 t) aacc,dacc)
| Gt t => (ins t bacc, aacc,dacc)
| Ge t => (ins (minus1 t) bacc, aacc,dacc)
- | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc)
- | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc)
+ | Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_number) dacc)
+ | NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_number) dacc)
| _ => (bacc, aacc, dacc)
val (b0,a0,ds) = h p ([],[],[])
val d = Integer.lcms ds
@@ -462,7 +462,7 @@
in equal_elim (Thm.symmetric th) TrueI end;
val dvd =
let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
- fn ct => the (Inttab.lookup tab (term_of ct |> dest_numeral))
+ fn ct => the (Inttab.lookup tab (term_of ct |> dest_number))
handle Option =>
(writeln ("dvd: Theorems-Table contains no entry for" ^
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
@@ -554,128 +554,133 @@
fun integer_nnf_conv ctxt env =
nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
-local
- val pcv = Simplifier.rewrite
- (HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4)
- @ [not_all, all_not_ex, @{thm ex_disj_distrib}]))
- val postcv = Simplifier.rewrite presburger_ss
- fun conv ctxt p =
- let val _ = ()
- in
- Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
- (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
- (cooperex_conv ctxt) p
- end
- handle CTERM s => raise COOPER "bad cterm"
- | THM s => raise COOPER "bad thm"
- | TYPE s => raise COOPER "bad type"
-in val conv = conv
-end;
+val conv_ss = HOL_basic_ss addsimps
+ (@{thms simp_thms} @ take 4 @{thms ex_simps} @ [not_all, all_not_ex, @{thm ex_disj_distrib}]);
+
+fun conv ctxt p =
+ Qelim.gen_qelim_conv (Simplifier.rewrite conv_ss) (Simplifier.rewrite presburger_ss) (Simplifier.rewrite conv_ss)
+ (cons o term_of) (OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
+ (cooperex_conv ctxt) p
+ handle CTERM s => raise COOPER "bad cterm"
+ | THM s => raise COOPER "bad thm"
+ | TYPE s => raise COOPER "bad type"
-fun term_bools acc t =
+fun add_bools t =
let
- val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
- @{term "op = :: int => _"}, @{term "op < :: int => _"},
- @{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
- @{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
- fun ty t = not (fastype_of t = HOLogic.boolT)
+ val ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"}, @{term "op <= :: int => _"},
+ @{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
+ @{term "Not"}, @{term "All :: (int => _) => _"},
+ @{term "Ex :: (int => _) => _"}, @{term "True"}, @{term "False"}];
+ val is_op = member (op =) ops;
+ val skip = not (fastype_of t = HOLogic.boolT)
in case t of
- (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b
- else insert (op aconv) t acc
- | f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a
- else insert (op aconv) t acc
- | Abs p => term_bools acc (snd (variant_abs p))
- | _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc
+ (l as f $ a) $ b => if skip orelse is_op f then add_bools b o add_bools l
+ else insert (op aconv) t
+ | f $ a => if skip orelse is_op f then add_bools a o add_bools f
+ else insert (op aconv) t
+ | Abs p => add_bools (snd (variant_abs p))
+ | _ => if skip orelse is_op t then I else insert (op aconv) t
end;
-fun i_of_term vs t = case t
- of Free (xn, xT) => (case AList.lookup (op aconv) vs t
- of NONE => raise COOPER "reification: variable not found in list"
- | SOME n => Cooper_Procedure.Bound n)
- | @{term "0::int"} => Cooper_Procedure.C 0
- | @{term "1::int"} => Cooper_Procedure.C 1
- | Term.Bound i => Cooper_Procedure.Bound i
- | Const(@{const_name Groups.uminus},_)$t' => Cooper_Procedure.Neg (i_of_term vs t')
- | Const(@{const_name Groups.plus},_)$t1$t2 => Cooper_Procedure.Add (i_of_term vs t1,i_of_term vs t2)
- | Const(@{const_name Groups.minus},_)$t1$t2 => Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2)
- | Const(@{const_name Groups.times},_)$t1$t2 =>
- (Cooper_Procedure.Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
- handle TERM _ =>
- (Cooper_Procedure.Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
- handle TERM _ => raise COOPER "reification: unsupported kind of multiplication"))
- | _ => (Cooper_Procedure.C (HOLogic.dest_number t |> snd)
- handle TERM _ => raise COOPER "reification: unknown term");
+fun descend vs (abs as (_, xT, _)) =
+ let
+ val (xn', p') = variant_abs abs;
+ in ((xn', xT) :: vs, p') end;
+
+local structure Proc = Cooper_Procedure in
+
+fun num_of_term vs (Free vT) = Proc.Bound (find_index (fn vT' => vT' = vT) vs)
+ | num_of_term vs (Term.Bound i) = Proc.Bound i
+ | num_of_term vs @{term "0::int"} = Proc.C 0
+ | num_of_term vs @{term "1::int"} = Proc.C 1
+ | num_of_term vs (t as Const (@{const_name number_of}, _) $ _) =
+ Proc.C (dest_number t)
+ | num_of_term vs (Const (@{const_name Groups.uminus}, _) $ t') =
+ Proc.Neg (num_of_term vs t')
+ | num_of_term vs (Const (@{const_name Groups.plus}, _) $ t1 $ t2) =
+ Proc.Add (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (Const (@{const_name Groups.minus}, _) $ t1 $ t2) =
+ Proc.Sub (num_of_term vs t1, num_of_term vs t2)
+ | num_of_term vs (Const (@{const_name Groups.times}, _) $ t1 $ t2) =
+ (case perhaps_number t1
+ of SOME n => Proc.Mul (n, num_of_term vs t2)
+ | NONE => (case perhaps_number t2
+ of SOME n => Proc.Mul (n, num_of_term vs t1)
+ | NONE => raise COOPER "reification: unsupported kind of multiplication"))
+ | num_of_term _ _ = raise COOPER "reification: bad term";
-fun qf_of_term ps vs t = case t
- of Const("True",_) => Cooper_Procedure.T
- | Const("False",_) => Cooper_Procedure.F
- | Const(@{const_name Orderings.less},_)$t1$t2 => Cooper_Procedure.Lt (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Cooper_Procedure.Le (Cooper_Procedure.Sub(i_of_term vs t1,i_of_term vs t2))
- | Const(@{const_name Rings.dvd},_)$t1$t2 =>
- (Cooper_Procedure.Dvd (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
- handle TERM _ => raise COOPER "reification: unsupported dvd")
- | @{term "op = :: int => _"}$t1$t2 => Cooper_Procedure.Eq (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2))
- | @{term "op = :: bool => _ "}$t1$t2 => Cooper_Procedure.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op &",_)$t1$t2 => Cooper_Procedure.And(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op |",_)$t1$t2 => Cooper_Procedure.Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const("op -->",_)$t1$t2 => Cooper_Procedure.Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
- | Const (@{const_name Not},_)$t' => Cooper_Procedure.Not(qf_of_term ps vs t')
- | Const("Ex",_)$Abs(xn,xT,p) =>
- let val (xn',p') = variant_abs (xn,xT,p)
- val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
- in Cooper_Procedure.E (qf_of_term ps vs' p')
- end
- | Const("All",_)$Abs(xn,xT,p) =>
- let val (xn',p') = variant_abs (xn,xT,p)
- val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs)
- in Cooper_Procedure.A (qf_of_term ps vs' p')
- end
- | _ =>(case AList.lookup (op aconv) ps t of
- NONE => raise COOPER "reification: unknown term"
- | SOME n => Cooper_Procedure.Closed n);
+fun fm_of_term ps vs (Const (@{const_name True}, _)) = Proc.T
+ | fm_of_term ps vs (Const (@{const_name False}, _)) = Proc.F
+ | fm_of_term ps vs (Const ("op &", _) $ t1 $ t2) =
+ Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2)
+ | fm_of_term ps vs (Const ("op |", _) $ t1 $ t2) =
+ Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2)
+ | fm_of_term ps vs (Const ("op -->", _) $ t1 $ t2) =
+ Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2)
+ | fm_of_term ps vs (@{term "op = :: bool => _ "} $ t1 $ t2) =
+ Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2)
+ | fm_of_term ps vs (Const (@{const_name Not}, _) $ t') =
+ Proc.Not (fm_of_term ps vs t')
+ | fm_of_term ps vs (Const ("Ex", _) $ Abs abs) =
+ Proc.E (uncurry (fm_of_term ps) (descend vs abs))
+ | fm_of_term ps vs (Const ("All", _) $ Abs abs) =
+ Proc.A (uncurry (fm_of_term ps) (descend vs abs))
+ | fm_of_term ps vs (@{term "op = :: int => _"} $ t1 $ t2) =
+ Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term ps vs (Const (@{const_name Orderings.less_eq}, _) $ t1 $ t2) =
+ Proc.Le (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term ps vs (Const (@{const_name Orderings.less}, _) $ t1 $ t2) =
+ Proc.Lt (Proc.Sub (num_of_term vs t1, num_of_term vs t2))
+ | fm_of_term ps vs (Const (@{const_name Rings.dvd}, _) $ t1 $ t2) =
+ (case perhaps_number t1
+ of SOME n => Proc.Dvd (n, num_of_term vs t2)
+ | NONE => raise COOPER "reification: unsupported dvd")
+ | fm_of_term ps vs t = let val n = find_index (fn t' => t aconv t') ps
+ in if n > 0 then Proc.Closed n else raise COOPER "reification: unknown term" end;
-fun term_of_i vs t = case t
- of Cooper_Procedure.C i => HOLogic.mk_number HOLogic.intT i
- | Cooper_Procedure.Bound n => the (AList.lookup (op =) vs n)
- | Cooper_Procedure.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t'
- | Cooper_Procedure.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
- | Cooper_Procedure.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2
- | Cooper_Procedure.Mul (i, t2) => @{term "op * :: int => _"} $
- HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2
- | Cooper_Procedure.Cn (n, i, t') => term_of_i vs (Cooper_Procedure.Add (Cooper_Procedure.Mul (i, Cooper_Procedure.Bound n), t'));
+fun term_of_num vs (Proc.C i) = HOLogic.mk_number HOLogic.intT i
+ | term_of_num vs (Proc.Bound n) = Free (nth vs n)
+ | term_of_num vs (Proc.Neg t') =
+ @{term "uminus :: int => _"} $ term_of_num vs t'
+ | term_of_num vs (Proc.Add (t1, t2)) =
+ @{term "op + :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
+ | term_of_num vs (Proc.Sub (t1, t2)) =
+ @{term "op - :: int => _"} $ term_of_num vs t1 $ term_of_num vs t2
+ | term_of_num vs (Proc.Mul (i, t2)) =
+ @{term "op * :: int => _"} $ HOLogic.mk_number HOLogic.intT i $ term_of_num vs t2
+ | term_of_num vs (Proc.Cn (n, i, t')) =
+ term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t'));
-fun term_of_qf ps vs t =
- case t of
- Cooper_Procedure.T => HOLogic.true_const
- | Cooper_Procedure.F => HOLogic.false_const
- | Cooper_Procedure.Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | Cooper_Procedure.Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
- | Cooper_Procedure.Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
- | Cooper_Procedure.Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
- | Cooper_Procedure.Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
- | Cooper_Procedure.NEq t' => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Eq t'))
- | Cooper_Procedure.Dvd(i,t') => @{term "op dvd :: int => _ "} $
- HOLogic.mk_number HOLogic.intT i $ term_of_i vs t'
- | Cooper_Procedure.NDvd(i,t')=> term_of_qf ps vs (Cooper_Procedure.Not(Cooper_Procedure.Dvd(i,t')))
- | Cooper_Procedure.Not t' => HOLogic.Not$(term_of_qf ps vs t')
- | Cooper_Procedure.And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Cooper_Procedure.Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Cooper_Procedure.Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
- | Cooper_Procedure.Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2
- | Cooper_Procedure.Closed n => the (AList.lookup (op =) ps n)
- | Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n));
+fun term_of_fm ps vs Proc.T = HOLogic.true_const
+ | term_of_fm ps vs Proc.F = HOLogic.false_const
+ | term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ | term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ | term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ | term_of_fm ps vs (Proc.Iff (t1, t2)) = @{term "op = :: bool => _"} $ term_of_fm ps vs t1 $ term_of_fm ps vs t2
+ | term_of_fm ps vs (Proc.Not t') = HOLogic.Not $ term_of_fm ps vs t'
+ | term_of_fm ps vs (Proc.Eq t') = @{term "op = :: int => _ "} $ term_of_num vs t'$ @{term "0::int"}
+ | term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.Not (Proc.Eq t'))
+ | term_of_fm ps vs (Proc.Lt t') = @{term "op < :: int => _ "} $ term_of_num vs t' $ @{term "0::int"}
+ | term_of_fm ps vs (Proc.Le t') = @{term "op <= :: int => _ "} $ term_of_num vs t' $ @{term "0::int"}
+ | term_of_fm ps vs (Proc.Gt t') = @{term "op < :: int => _ "} $ @{term "0::int"} $ term_of_num vs t'
+ | term_of_fm ps vs (Proc.Ge t') = @{term "op <= :: int => _ "} $ @{term "0::int"} $ term_of_num vs t'
+ | term_of_fm ps vs (Proc.Dvd (i, t')) = @{term "op dvd :: int => _ "} $
+ HOLogic.mk_number HOLogic.intT i $ term_of_num vs t'
+ | term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.Not (Proc.Dvd (i, t')))
+ | term_of_fm ps vs (Proc.Closed n) = nth ps n
+ | term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.Not (Proc.Closed n));
-fun invoke t =
+fun procedure t =
let
- val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t);
- in
- Logic.mk_equals (HOLogic.mk_Trueprop t,
- HOLogic.mk_Trueprop (term_of_qf (map swap ps) (map swap vs) (Cooper_Procedure.pa (qf_of_term ps vs t))))
- end;
+ val vs = Term.add_frees t [];
+ val ps = add_bools t [];
+ in (term_of_fm ps vs o Proc.pa o fm_of_term ps vs) t end;
-val (_, oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "cooper",
- (fn (ctxt, t) => Thm.cterm_of (ProofContext.theory_of ctxt) (invoke t)))));
+end;
+
+val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "cooper",
+ (fn (ctxt, t) => (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
+ (t, procedure t)))));
val comp_ss = HOL_ss addsimps @{thms semiring_norm};
@@ -730,7 +735,7 @@
| Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
| Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
| Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
- | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
+ | _ => is_number t orelse can HOLogic.dest_nat t
fun ty cts t =
if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false
--- a/src/HOL/Transcendental.thy Wed May 12 11:07:46 2010 +0200
+++ b/src/HOL/Transcendental.thy Wed May 12 11:08:15 2010 +0200
@@ -732,7 +732,8 @@
also have "\<dots> \<le> ?diff_part + \<bar> (\<Sum>n. ?diff (n + ?N) x) - (\<Sum> n. f' x0 (n + ?N)) \<bar>" unfolding suminf_split_initial_segment[OF all_smbl, where k="?N"] unfolding suminf_diff[OF div_shft_smbl ign[OF `summable (f' x0)`]] by (rule abs_triangle_ineq)
also have "\<dots> \<le> ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto
also have "\<dots> < r /3 + r/3 + r/3"
- using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3` by auto
+ using `?diff_part < r/3` `?L_part \<le> r/3` and `?f'_part < r/3`
+ by (rule add_strict_mono [OF add_less_le_mono])
finally have "\<bar> (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \<bar> < r"
by auto
} thus "\<exists> s > 0. \<forall> x. x \<noteq> 0 \<and> norm (x - 0) < s \<longrightarrow>
@@ -1663,6 +1664,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)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Wed May 12 11:07:46 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Wed May 12 11:08:15 2010 +0200
@@ -154,7 +154,7 @@
val retraction_strict = @{thm retraction_strict};
val abs_strict = ax_rep_iso RS (allI RS retraction_strict);
val rep_strict = ax_abs_iso RS (allI RS retraction_strict);
-val iso_rews = map Drule.export_without_context [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
+val iso_rews = [ax_abs_iso, ax_rep_iso, abs_strict, rep_strict];
(* ----- theorems concerning one induction step ----------------------------- *)
@@ -287,22 +287,17 @@
map (K(atac 1)) (filter is_rec args))
cons))
conss);
- local
- (* check whether every/exists constructor of the n-th part of the equation:
- it has a possibly indirectly recursive argument that isn't/is possibly
- indirectly lazy *)
- fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg =>
+ local
+ fun rec_to ns lazy_rec (n,cons) = forall (exists (fn arg =>
is_rec arg andalso not (member (op =) ns (rec_of arg)) andalso
- ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
- rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
+ ((rec_of arg = n andalso not (lazy_rec orelse is_lazy arg)) orelse
+ rec_of arg <> n andalso rec_to (rec_of arg::ns)
(lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
) o snd) cons;
- fun all_rec_to ns = rec_to forall not all_rec_to ns;
fun warn (n,cons) =
- if all_rec_to [] false (n,cons)
+ if rec_to [] false (n,cons)
then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
else false;
- fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns;
in
val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
--- a/src/Provers/blast.ML Wed May 12 11:07:46 2010 +0200
+++ b/src/Provers/blast.ML Wed May 12 11:08:15 2010 +0200
@@ -1278,7 +1278,7 @@
val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" (K 20);
fun blast_tac cs i st =
- ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit)
+ ((DEEPEN (1, Config.get_global (Thm.theory_of_thm st) depth_limit)
(timing_depth_tac (start_timing ()) cs) 0) i
THEN flexflex_tac) st
handle TRANS s =>
--- a/src/Pure/Isar/attrib.ML Wed May 12 11:07:46 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Wed May 12 11:08:15 2010 +0200
@@ -355,7 +355,7 @@
| scan_value (Config.String _) = equals |-- Args.name >> Config.String;
fun scan_config thy config =
- let val config_type = Config.get_thy thy config
+ let val config_type = Config.get_global thy config
in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
in
--- a/src/Pure/System/isabelle_system.scala Wed May 12 11:07:46 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed May 12 11:08:15 2010 +0200
@@ -318,7 +318,7 @@
val font_family = "IsabelleText"
- def get_font(bold: Boolean = false, size: Int = 1): Font =
+ def get_font(size: Int = 1, bold: Boolean = false): Font =
new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
def install_fonts()
@@ -330,7 +330,7 @@
else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"
Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
}
- def check_font() = get_font(false).getFamily == font_family
+ def check_font() = get_font().getFamily == font_family
if (!check_font()) {
val font = create_font(false)
--- a/src/Pure/config.ML Wed May 12 11:07:46 2010 +0200
+++ b/src/Pure/config.ML Wed May 12 11:08:15 2010 +0200
@@ -16,9 +16,9 @@
val get: Proof.context -> 'a T -> 'a
val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
val put: 'a T -> 'a -> Proof.context -> Proof.context
- val get_thy: theory -> 'a T -> 'a
- val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
- val put_thy: 'a T -> 'a -> theory -> theory
+ val get_global: theory -> 'a T -> 'a
+ val map_global: 'a T -> ('a -> 'a) -> theory -> theory
+ val put_global: 'a T -> 'a -> theory -> theory
val get_generic: Context.generic -> 'a T -> 'a
val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
@@ -83,9 +83,9 @@
fun map_ctxt config f = Context.proof_map (map_generic config f);
fun put_ctxt config value = map_ctxt config (K value);
-fun get_thy thy = get_generic (Context.Theory thy);
-fun map_thy config f = Context.theory_map (map_generic config f);
-fun put_thy config value = map_thy config (K value);
+fun get_global thy = get_generic (Context.Theory thy);
+fun map_global config f = Context.theory_map (map_generic config f);
+fun put_global config value = map_global config (K value);
(* context information *)
--- a/src/Pure/library.scala Wed May 12 11:07:46 2010 +0200
+++ b/src/Pure/library.scala Wed May 12 11:08:15 2010 +0200
@@ -76,9 +76,11 @@
private def simple_dialog(kind: Int, default_title: String)
(parent: Component, title: String, message: Any*)
{
- JOptionPane.showMessageDialog(parent,
- message.toArray.asInstanceOf[Array[AnyRef]],
- if (title == null) default_title else title, kind)
+ Swing_Thread.now {
+ JOptionPane.showMessageDialog(parent,
+ message.toArray.asInstanceOf[Array[AnyRef]],
+ if (title == null) default_title else title, kind)
+ }
}
def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
--- a/src/Pure/unify.ML Wed May 12 11:07:46 2010 +0200
+++ b/src/Pure/unify.ML Wed May 12 11:08:15 2010 +0200
@@ -349,7 +349,7 @@
fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
: (term * (Envir.env * dpair list))Seq.seq =
let
- val trace_tps = Config.get_thy thy trace_types;
+ val trace_tps = Config.get_global thy trace_types;
(*Produce copies of uarg and cons them in front of uargs*)
fun copycons uarg (uargs, (env, dpairs)) =
Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
@@ -584,9 +584,9 @@
fun hounifiers (thy,env, tus : (term*term)list)
: (Envir.env * (term*term)list)Seq.seq =
let
- val trace_bnd = Config.get_thy thy trace_bound;
- val search_bnd = Config.get_thy thy search_bound;
- val trace_smp = Config.get_thy thy trace_simp;
+ val trace_bnd = Config.get_global thy trace_bound;
+ val search_bnd = Config.get_global thy search_bound;
+ val trace_smp = Config.get_global thy trace_simp;
fun add_unify tdepth ((env,dpairs), reseq) =
Seq.make (fn()=>
let val (env',flexflex,flexrigid) =
--- a/src/Tools/jEdit/README_BUILD Wed May 12 11:07:46 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD Wed May 12 11:08:15 2010 +0200
@@ -8,10 +8,10 @@
* Netbeans 6.8
http://www.netbeans.org/downloads/index.html
-* Scala for Netbeans: version 6.8v1.1
- http://sourceforge.net/project/showfiles.php?group_id=192439&package_id=256544
+* Scala for Netbeans: version 6.8v1.1.0rc2
+ http://wiki.netbeans.org/Scala
+ http://sourceforge.net/projects/erlybird/files/nb-scala/6.8v1.1.0rc2
http://blogtrader.net/dcaoyuan/category/NetBeans
- http://wiki.netbeans.org/Scala
* jEdit 4.3.1 or 4.3.2
http://www.jedit.org/
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Wed May 12 11:07:46 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Wed May 12 11:08:15 2010 +0200
@@ -185,6 +185,7 @@
sidekick.complete-delay=300
sidekick.splitter.location=721
tip.show=false
+twoStageSave=false
view.antiAlias=standard
view.blockCaret=true
view.caretBlink=false
--- a/src/Tools/jEdit/nbproject/build-impl.xml Wed May 12 11:07:46 2010 +0200
+++ b/src/Tools/jEdit/nbproject/build-impl.xml Wed May 12 11:08:15 2010 +0200
@@ -230,7 +230,7 @@
<attribute default="" name="sourcepath"/>
<element name="customize" optional="true"/>
<sequential>
- <scalac addparams="-make:transitive -dependencyfile ${basedir}/${build.dir}/.scala_dependencies @{addparams}" deprecation="${scalac.deprecation}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" extdirs="@{extdirs}" force="yes" fork="true" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}" unchecked="${scalac.unchecked}">
+ <scalac addparams="-make:transitive -dependencyfile "${basedir}/${build.dir}/.scala_dependencies" @{addparams}" deprecation="${scalac.deprecation}" destdir="@{destdir}" encoding="${source.encoding}" excludes="@{excludes}" extdirs="@{extdirs}" force="yes" fork="true" includes="@{includes}" sourcepath="@{sourcepath}" srcdir="@{srcdir}" target="jvm-${javac.target}" unchecked="${scalac.unchecked}">
<classpath>
<path>
<pathelement path="@{classpath}"/>
@@ -549,7 +549,7 @@
-->
<target depends="init" name="-javadoc-build">
<mkdir dir="${dist.javadoc.dir}"/>
- <scaladoc addparams="${javadoc.additionalparam}" deprecation="yes" destdir="${dist.javadoc.dir}" doctitle="${javadoc.windowtitle}" encoding="${javadoc.encoding.used}" srcdir="${src.dir}" unchecked="yes" windowtitle="${javadoc.windowtitle}">
+ <scaladoc addparams="${javadoc.additionalparam}" deprecation="yes" destdir="${dist.javadoc.dir}" doctitle="${javadoc.windowtitle}" encoding="${javadoc.encoding.used}" srcdir="${src.dir}" unchecked="yes">
<classpath>
<path path="${javac.classpath}"/>
<fileset dir="${scala.lib}">
--- a/src/Tools/jEdit/nbproject/genfiles.properties Wed May 12 11:07:46 2010 +0200
+++ b/src/Tools/jEdit/nbproject/genfiles.properties Wed May 12 11:08:15 2010 +0200
@@ -4,5 +4,5 @@
# This file is used by a NetBeans-based IDE to track changes in generated files such as build-impl.xml.
# Do not edit this file. You may delete it but then the IDE will never regenerate such files for you.
nbproject/build-impl.xml.data.CRC32=8f41dcce
-nbproject/build-impl.xml.script.CRC32=1c29c971
-nbproject/build-impl.xml.stylesheet.CRC32=8c3c03dd@1.3.4
+nbproject/build-impl.xml.script.CRC32=e3e2a5d5
+nbproject/build-impl.xml.stylesheet.CRC32=5220179f@1.3.5
--- a/src/Tools/jEdit/plugin/Isabelle.props Wed May 12 11:07:46 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props Wed May 12 11:08:15 2010 +0200
@@ -25,8 +25,10 @@
options.isabelle.label=Isabelle
options.isabelle.code=new isabelle.jedit.Isabelle_Options();
options.isabelle.logic.title=Logic
-options.isabelle.font-size.title=Font Size
-options.isabelle.font-size=14
+options.isabelle.relative-font-size.title=Relative Font Size
+options.isabelle.relative-font-size=100
+options.isabelle.relative-margin.title=Relative Margin
+options.isabelle.relative-margin=90
options.isabelle.startup-timeout=10000
#menu actions
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Wed May 12 11:07:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Wed May 12 11:08:15 2010 +0200
@@ -10,7 +10,7 @@
import isabelle._
import java.io.StringReader
-import java.awt.{BorderLayout, Dimension}
+import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit}
import java.awt.event.MouseEvent
import javax.swing.{JButton, JPanel, JScrollPane}
@@ -40,7 +40,7 @@
class HTML_Panel(
sys: Isabelle_System,
- initial_font_size: Int,
+ font_size0: Int, relative_margin0: Int,
handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
{
// global logging
@@ -56,6 +56,15 @@
}
private def template(font_size: Int): String =
+ {
+ // re-adjustment according to org.lobobrowser.html.style.HtmlValues.getFontSize
+ val dpi =
+ if (GraphicsEnvironment.isHeadless()) 72
+ else Toolkit.getDefaultToolkit().getScreenResolution()
+
+ val size0 = font_size * dpi / 96
+ val size = if (size0 * 96 / dpi == font_size) size0 else size0 + 1
+
"""<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
@@ -65,13 +74,24 @@
""" +
try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
- "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
+ "body { font-family: " + sys.font_family + "; font-size: " + size + "px }" +
"""
</style>
</head>
<body/>
</html>
"""
+ }
+
+
+ def panel_width(font_size: Int, relative_margin: Int): Int =
+ {
+ val font = sys.get_font(font_size)
+ Swing_Thread.now {
+ val char_width = (getFontMetrics(font).stringWidth("mix") / 3) max 1
+ ((getWidth() * relative_margin) / (100 * char_width)) max 20
+ }
+ }
/* actor with local state */
@@ -98,7 +118,7 @@
private val builder = new DocumentBuilderImpl(ucontext, rcontext)
- private case class Init(font_size: Int)
+ private case class Init(font_size: Int, relative_margin: Int)
private case class Render(body: List[XML.Tree])
private val main_actor = actor {
@@ -106,9 +126,15 @@
var doc1: org.w3c.dom.Document = null
var doc2: org.w3c.dom.Document = null
+ var current_font_size = 16
+ var current_relative_margin = 90
+
loop {
react {
- case Init(font_size) =>
+ case Init(font_size, relative_margin) =>
+ current_font_size = font_size
+ current_relative_margin = relative_margin
+
val src = template(font_size)
def parse() =
builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
@@ -118,7 +144,9 @@
case Render(body) =>
val doc = doc2
- val html_body = Pretty.formatted(body).map(t => XML.elem(HTML.PRE, HTML.spans(t)))
+ val html_body =
+ Pretty.formatted(body, panel_width(current_font_size, current_relative_margin))
+ .map(t => XML.elem(HTML.PRE, HTML.spans(t)))
val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body))
doc.removeChild(doc.getLastChild())
doc.appendChild(node)
@@ -131,11 +159,11 @@
}
}
- main_actor ! Init(initial_font_size)
-
/* main method wrappers */
- def init(font_size: Int) { main_actor ! Init(font_size) }
+ def init(font_size: Int, relative_margin: Int) { main_actor ! Init(font_size, relative_margin) }
def render(body: List[XML.Tree]) { main_actor ! Render(body) }
+
+ init(font_size0, relative_margin0)
}
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed May 12 11:07:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed May 12 11:08:15 2010 +0200
@@ -15,7 +15,8 @@
class Isabelle_Options extends AbstractOptionPane("isabelle")
{
private val logic_name = new JComboBox()
- private val font_size = new JSpinner()
+ private val relative_font_size = new JSpinner()
+ private val relative_margin = new JSpinner()
private class List_Item(val name: String, val descr: String) {
def this(name: String) = this(name, name)
@@ -36,18 +37,26 @@
logic_name
})
- addComponent(Isabelle.Property("font-size.title"), {
- font_size.setValue(Isabelle.Int_Property("font-size"))
- font_size
+ addComponent(Isabelle.Property("relative-font-size.title"), {
+ relative_font_size.setValue(Isabelle.Int_Property("relative-font-size"))
+ relative_font_size
+ })
+
+ addComponent(Isabelle.Property("relative-margin.title"), {
+ relative_margin.setValue(Isabelle.Int_Property("relative-margin"))
+ relative_margin
})
}
override def _save()
{
- val logic = logic_name.getSelectedItem.asInstanceOf[List_Item].name
- Isabelle.Property("logic") = logic
+ Isabelle.Property("logic") =
+ logic_name.getSelectedItem.asInstanceOf[List_Item].name
- val size = font_size.getValue().asInstanceOf[Int]
- Isabelle.Int_Property("font-size") = size
+ Isabelle.Int_Property("relative-font-size") =
+ relative_font_size.getValue().asInstanceOf[Int]
+
+ Isabelle.Int_Property("relative-margin") =
+ relative_margin.getValue().asInstanceOf[Int]
}
}
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Wed May 12 11:07:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Wed May 12 11:08:15 2010 +0200
@@ -24,8 +24,9 @@
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
- private val html_panel =
- new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null)
+ val html_panel =
+ new HTML_Panel(Isabelle.system,
+ Isabelle.font_size(), Isabelle.Int_Property("relative-margin"), null)
add(html_panel, BorderLayout.CENTER)
@@ -43,7 +44,7 @@
}
case Session.Global_Settings =>
- html_panel.init(Isabelle.Int_Property("font-size"))
+ html_panel.init(Isabelle.font_size(), Isabelle.Int_Property("relative-margin"))
case bad => System.err.println("output_actor: ignoring bad message " + bad)
}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Wed May 12 11:07:46 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Wed May 12 11:08:15 2010 +0200
@@ -42,22 +42,37 @@
object Property
{
- def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
- def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
+ def apply(name: String): String =
+ jEdit.getProperty(OPTION_PREFIX + name)
+ def apply(name: String, default: String): String =
+ jEdit.getProperty(OPTION_PREFIX + name, default)
+ def update(name: String, value: String) =
+ jEdit.setProperty(OPTION_PREFIX + name, value)
}
object Boolean_Property
{
- def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
- def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
+ def apply(name: String): Boolean =
+ jEdit.getBooleanProperty(OPTION_PREFIX + name)
+ def apply(name: String, default: Boolean): Boolean =
+ jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
+ def update(name: String, value: Boolean) =
+ jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
}
object Int_Property
{
- def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
- def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
+ def apply(name: String): Int =
+ jEdit.getIntegerProperty(OPTION_PREFIX + name)
+ def apply(name: String, default: Int): Int =
+ jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
+ def update(name: String, value: Int) =
+ jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
}
+ def font_size(): Int =
+ (jEdit.getIntegerProperty("view.fontsize", 16) * Int_Property("relative-font-size", 100)) / 100
+
/* settings */