# HG changeset patch # User hoelzl # Date 1273655295 -7200 # Node ID 7e6f334b294b384deb15e83560e6b4cc771d4c47 # Parent bf8e62da7613dbf336d6c54f89c43220b2f7b2d7# Parent ce939b5fd77b056f755597635fa455cba72b0a17 merged diff -r bf8e62da7613 -r 7e6f334b294b NEWS --- 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 diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/Complex.thy --- 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 "((\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 bf8e62da7613 -r 7e6f334b294b src/HOL/IsaMakefile --- 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 \ diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/Library/Char_nat.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 \ {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}" + "n mod 16 \ {15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0}" proof - have set_unfold: "\n. {0..Suc n} = insert (Suc n) {0..n}" by auto have "(n\nat) mod 16 \ {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 diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/Limits.thy --- 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 *} diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/Mirabelle/Tools/mirabelle.ML --- 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) diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/Nat_Numeral.thy --- 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\ = 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) @@ -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) diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/Parity.thy --- 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) \ 2 dvd x" - by (presburger add: even_nat_def even_def) + by presburger lemma int_even_iff_2_dvd[algebra]: "even (x::int) \ 2 dvd x" by presburger diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/RComplete.thy --- 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 \ 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 bf8e62da7613 -r 7e6f334b294b src/HOL/RealDef.thy --- 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) \ x+y) = (-x \ 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) \ 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 \ r; r \ 1 |] ==> r ^ Suc n \ 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 \ 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 \ 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 \ 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) \ 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) \ u ^ 2 + v ^ 2 + w ^ 2" +by (intro add_nonneg_nonneg zero_le_power2) + +lemma real_minus_mult_self_le [simp]: "-(u * u) \ (x * (x::real))" +by (rule_tac y = 0 in order_trans, auto) + +lemma realpow_square_minus_le [simp]: "-(u ^ 2) \ (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 |] ==> \e. 0 < e & e < d1 & e < d2" diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/RealPow.thy --- 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) \ 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 \ r; r \ 1 |] ==> r ^ Suc n \ 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 \ 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 \ 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 \ 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 \ 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)" -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_minus_mult_self_le [simp]: "-(u * u) \ (x * (x::real))" -by (rule_tac y = 0 in order_trans, auto) - -lemma realpow_square_minus_le [simp]: "-(u ^ 2) \ (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 \ x" and ygt0: "0 \ y" and sq: "x^2 \ y^2" - shows "x \ y" -proof - - from sq have "x ^ Suc (Suc 0) \ y ^ Suc (Suc 0)" - by (simp only: numeral_2_eq_2) - thus "x \ 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 \ 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 bf8e62da7613 -r 7e6f334b294b src/HOL/RealVector.thy --- 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 *} diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/Rings.thy --- 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 \ 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 bf8e62da7613 -r 7e6f334b294b src/HOL/SEQ.thy --- 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 diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/Tools/Qelim/cooper.ML --- 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 diff -r bf8e62da7613 -r 7e6f334b294b src/HOL/Transcendental.thy --- 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 "\ \ ?diff_part + \ (\n. ?diff (n + ?N) x) - (\ n. f' x0 (n + ?N)) \" 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 "\ \ ?diff_part + ?L_part + ?f'_part" using abs_triangle_ineq4 by auto also have "\ < r /3 + r/3 + r/3" - using `?diff_part < r/3` `?L_part \ r/3` and `?f'_part < r/3` by auto + using `?diff_part < r/3` `?L_part \ r/3` and `?f'_part < r/3` + by (rule add_strict_mono [OF add_less_le_mono]) finally have "\ (suminf (f (x0 + x)) - (suminf (f x0))) / x - suminf (f' x0) \ < r" by auto } thus "\ s > 0. \ x. x \ 0 \ norm (x - 0) < s \ @@ -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) diff -r bf8e62da7613 -r 7e6f334b294b src/HOLCF/Tools/Domain/domain_theorems.ML --- 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; diff -r bf8e62da7613 -r 7e6f334b294b src/Provers/blast.ML --- 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 => diff -r bf8e62da7613 -r 7e6f334b294b src/Pure/Isar/attrib.ML --- 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 diff -r bf8e62da7613 -r 7e6f334b294b src/Pure/System/isabelle_system.scala --- 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) diff -r bf8e62da7613 -r 7e6f334b294b src/Pure/config.ML --- 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 *) diff -r bf8e62da7613 -r 7e6f334b294b src/Pure/library.scala --- 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) _ diff -r bf8e62da7613 -r 7e6f334b294b src/Pure/unify.ML --- 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) = diff -r bf8e62da7613 -r 7e6f334b294b src/Tools/jEdit/README_BUILD --- 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/ diff -r bf8e62da7613 -r 7e6f334b294b src/Tools/jEdit/dist-template/properties/jedit.props --- 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 diff -r bf8e62da7613 -r 7e6f334b294b src/Tools/jEdit/nbproject/build-impl.xml --- 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 @@ - + @@ -549,7 +549,7 @@ --> - + diff -r bf8e62da7613 -r 7e6f334b294b src/Tools/jEdit/nbproject/genfiles.properties --- 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 diff -r bf8e62da7613 -r 7e6f334b294b src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r bf8e62da7613 -r 7e6f334b294b src/Tools/jEdit/src/jedit/html_panel.scala --- 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 + """ @@ -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 }" + """ """ + } + + + 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) } diff -r bf8e62da7613 -r 7e6f334b294b src/Tools/jEdit/src/jedit/isabelle_options.scala --- 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] } } diff -r bf8e62da7613 -r 7e6f334b294b src/Tools/jEdit/src/jedit/output_dockable.scala --- 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) } diff -r bf8e62da7613 -r 7e6f334b294b src/Tools/jEdit/src/jedit/plugin.scala --- 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 */