# HG changeset patch # User haftmann # Date 1315474283 -7200 # Node ID d19c677eb8126e64f9325cd67fa1aa79c62572f1 # Parent 1120cba9bce438518998ec5b3db8f211f199a653# Parent 096ec174be5d22742893495578f7f064c1e9cc27 tuned diff -r 096ec174be5d -r d19c677eb812 ANNOUNCE --- a/ANNOUNCE Thu Sep 08 00:35:22 2011 +0200 +++ b/ANNOUNCE Thu Sep 08 11:31:23 2011 +0200 @@ -1,34 +1,15 @@ -Subject: Announcing Isabelle2011 +Subject: Announcing Isabelle2011-1 To: isabelle-users@cl.cam.ac.uk -Isabelle2011 is now available. - -This version significantly improves upon Isabelle2009-2, see the NEWS -file in the distribution for more details. Some notable changes are: - -* Experimental Prover IDE based on Isabelle/Scala and jEdit. - -* Coercive subtyping (configured in HOL/Complex_Main). - -* HOL code generation: Scala as another target language. - -* HOL: partial_function definitions. +Isabelle2011-1 is now available. -* HOL: various tool enhancements, including Quickcheck, Nitpick, - Sledgehammer, SMT integration. - -* HOL: various additions to theory library, including HOL-Algebra, - Imperative_HOL, Multivariate_Analysis, Probability. +This version improves upon Isabelle2011, see the NEWS file in the +distribution for more details. Some important changes are: -* HOLCF: reorganization of library and related tools. - -* HOL/SPARK: interactive proof environment for verification conditions - generated by the SPARK Ada program verifier. - -* Improved Isabelle/Isar implementation manual (covering Isabelle/ML). +* FIXME -You may get Isabelle2011 from the following mirror sites: +You may get Isabelle2011-1 from the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ diff -r 096ec174be5d -r d19c677eb812 Admin/CHECKLIST --- a/Admin/CHECKLIST Thu Sep 08 00:35:22 2011 +0200 +++ b/Admin/CHECKLIST Thu Sep 08 11:31:23 2011 +0200 @@ -3,9 +3,7 @@ - test polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj; -- test Proof General 4.1, 4.0, 3.7.1.1; - -- test Scala wrapper; +- test Proof General 4.1, 3.7.1.1; - check HTML header of library; diff -r 096ec174be5d -r d19c677eb812 Admin/makebundle --- a/Admin/makebundle Thu Sep 08 00:35:22 2011 +0200 +++ b/Admin/makebundle Thu Sep 08 11:31:23 2011 +0200 @@ -75,7 +75,13 @@ ) case "$PLATFORM" in - x86-cygwin) + *-darwin) + perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \ + "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props" + ;; + *-cygwin) + perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \ + "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props" rm "$TMP/$ISABELLE_NAME/contrib/ProofGeneral" ln -s ProofGeneral-3.7.1.1 "$TMP/$ISABELLE_NAME/contrib/ProofGeneral" ;; diff -r 096ec174be5d -r d19c677eb812 CONTRIBUTORS --- a/CONTRIBUTORS Thu Sep 08 00:35:22 2011 +0200 +++ b/CONTRIBUTORS Thu Sep 08 11:31:23 2011 +0200 @@ -3,8 +3,8 @@ who is listed as an author in one of the source files of this Isabelle distribution. -Contributions to this Isabelle version --------------------------------------- +Contributions to Isabelle2011-1 +------------------------------- * September 2011: Peter Gammie Theory HOL/Libary/Saturated: numbers with saturated arithmetic. diff -r 096ec174be5d -r d19c677eb812 NEWS --- a/NEWS Thu Sep 08 00:35:22 2011 +0200 +++ b/NEWS Thu Sep 08 11:31:23 2011 +0200 @@ -1,8 +1,8 @@ Isabelle NEWS -- history user-relevant changes ============================================== -New in this Isabelle version ----------------------------- +New in Isabelle2011-1 (October 2011) +------------------------------------ *** General *** @@ -319,6 +319,7 @@ * Theory Complex_Main: Several redundant theorems have been removed or replaced by more general versions. INCOMPATIBILITY. + real_of_int_real_of_nat ~> real_of_int_of_nat_eq real_0_le_divide_iff ~> zero_le_divide_iff realpow_two_disj ~> power2_eq_iff real_squared_diff_one_factored ~> square_diff_one_factored @@ -466,6 +467,9 @@ INCOMPATIBILITY, classical tactics and derived proof methods require proper Proof.context. + +*** System *** + * Scala layer provides JVM method invocation service for static methods of type (String)String, see Invoke_Scala.method in ML. For example: @@ -475,6 +479,10 @@ Togeter with YXML.string_of_body/parse_body and XML.Encode/Decode this allows to pass structured values between ML and Scala. +* The IsabelleText fonts includes some further glyphs to support the +Prover IDE. Potential INCOMPATIBILITY: users who happen to have +installed a local copy (which is normally *not* required) need to +delete or update it from ~~/lib/fonts/. New in Isabelle2011 (January 2011) diff -r 096ec174be5d -r d19c677eb812 README --- a/README Thu Sep 08 00:35:22 2011 +0200 +++ b/README Thu Sep 08 11:31:23 2011 +0200 @@ -16,8 +16,8 @@ * The Poly/ML compiler and runtime system (version 5.2.1 or later). * The GNU bash shell (version 3.x or 2.x). * Perl (version 5.x). + * Java 1.6.x from Oracle or Apple -- for Scala and jEdit. * GNU Emacs (version 23) -- for the Proof General 4.x interface. - * Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit. * A complete LaTeX installation -- for document preparation. Installation @@ -31,17 +31,18 @@ User interface + Isabelle/jEdit is an emerging Prover IDE based on advanced + technology of Isabelle/Scala. It provides a metaphor of continuous + proof checking of a versioned collection of theory sources, with + instantaneous feedback in real-time and rich semantic markup + associated with the formal text. + The classic Isabelle user interface is Proof General by David Aspinall and others. It is a generic Emacs interface for proof assistants, including Isabelle. Its most prominent feature is script management, providing a metaphor of stepwise proof script editing. - Isabelle/jEdit is an experimental Prover IDE based on advanced - technology of Isabelle/Scala. It provides a metaphor of continuous - proof checking of a versioned collection of theory sources, with - instantaneous feedback in real-time. - Other sources of information The Isabelle Page diff -r 096ec174be5d -r d19c677eb812 doc/Contents --- a/doc/Contents Thu Sep 08 00:35:22 2011 +0200 +++ b/doc/Contents Thu Sep 08 11:31:23 2011 +0200 @@ -1,4 +1,4 @@ -Learning and using Isabelle +Miscellaneous tutorials tutorial Tutorial on Isabelle/HOL main What's in Main isar-overview Tutorial on Isar diff -r 096ec174be5d -r d19c677eb812 src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Algebra/IntRing.thy Thu Sep 08 11:31:23 2011 +0200 @@ -35,8 +35,8 @@ apply (rule abelian_groupI, simp_all) defer 1 apply (rule comm_monoidI, simp_all) - apply (rule zadd_zmult_distrib) -apply (fast intro: zadd_zminus_inverse2) + apply (rule left_distrib) +apply (fast intro: left_minus) done (* @@ -298,7 +298,7 @@ from this obtain x where "1 = x * p" by best from this [symmetric] - have "p * x = 1" by (subst zmult_commute) + have "p * x = 1" by (subst mult_commute) hence "\p * x\ = 1" by simp hence "\p\ = 1" by (rule abs_zmult_eq_1) from this and prime diff -r 096ec174be5d -r d19c677eb812 src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Thu Sep 08 11:31:23 2011 +0200 @@ -1818,7 +1818,7 @@ lemma INTEG_cring: "cring INTEG" by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI - zadd_zminus_inverse2 zadd_zmult_distrib) + left_minus left_distrib) lemma INTEG_id_eval: "UP_pre_univ_prop INTEG INTEG id" diff -r 096ec174be5d -r d19c677eb812 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy --- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Thu Sep 08 11:31:23 2011 +0200 @@ -77,10 +77,10 @@ boogie_vc max (examine: L_14_5c L_14_5b L_14_5a) proof boogie_cases case L_14_5c - thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear) + thus ?case by (metis less_le_not_le zle_add1_eq_le less_linear) next case L_14_5b - thus ?case by (metis less_le_not_le xt1(10) zle_linear zless_add1_eq) + thus ?case by (metis less_le_not_le xt1(10) linorder_linear zless_add1_eq) next case L_14_5a note max0 = `max0 = array 0` diff -r 096ec174be5d -r d19c677eb812 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Code_Numeral.thy Thu Sep 08 11:31:23 2011 +0200 @@ -274,7 +274,7 @@ then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" by simp then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" - unfolding int_mult zadd_int [symmetric] by simp + unfolding of_nat_mult of_nat_add by simp then show ?thesis by (auto simp add: int_of_def mult_ac) qed diff -r 096ec174be5d -r d19c677eb812 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Complex.thy Thu Sep 08 11:31:23 2011 +0200 @@ -621,13 +621,6 @@ lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" by (simp add: rcis_def cis_def) -lemma sin_cos_squared_add2_mult: "(r * cos a)\ + (r * sin a)\ = r\" -proof - - have "(r * cos a)\ + (r * sin a)\ = r\ * ((cos a)\ + (sin a)\)" - by (simp only: power_mult_distrib right_distrib) - thus ?thesis by simp -qed - lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" by (simp add: rcis_def cis_def norm_mult) @@ -656,22 +649,11 @@ lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" by (simp add: rcis_def) -lemma complex_of_real_minus_one: - "complex_of_real (-(1::real)) = -(1::complex)" - by (simp add: complex_of_real_def complex_one_def) - lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x" by (simp add: mult_assoc [symmetric]) - -lemma cis_real_of_nat_Suc_mult: - "cis (real (Suc n) * a) = cis a * cis (real n * a)" - by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib) - lemma DeMoivre: "(cis a) ^ n = cis (real n * a)" -apply (induct_tac "n") -apply (auto simp add: cis_real_of_nat_Suc_mult) -done + by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult) lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" by (simp add: rcis_def power_mult_distrib DeMoivre) diff -r 096ec174be5d -r d19c677eb812 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Thu Sep 08 11:31:23 2011 +0200 @@ -295,7 +295,7 @@ unfolding real_sqrt_mult[of _ "pow2 (?E mod 2)"] real_sqrt_abs2 by auto also have "\ < pow2 (?E div 2) * 2" by (rule mult_strict_left_mono, auto intro: E_mod_pow) - also have "\ = pow2 (?E div 2 + 1)" unfolding zadd_commute[of _ 1] pow2_add1 by auto + also have "\ = pow2 (?E div 2 + 1)" unfolding add_commute[of _ 1] pow2_add1 by auto finally show ?thesis by auto qed finally show ?thesis diff -r 096ec174be5d -r d19c677eb812 src/HOL/Decision_Procs/Cooper.thy --- a/src/HOL/Decision_Procs/Cooper.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Decision_Procs/Cooper.thy Thu Sep 08 11:31:23 2011 +0200 @@ -1318,7 +1318,7 @@ also have "\ = (j dvd (- (c*x - ?e)))" by (simp only: dvd_minus_iff) also have "\ = (j dvd (c* (- x)) + ?e)" - apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib) + apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib) by (simp add: algebra_simps) also have "\ = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] @@ -1330,7 +1330,7 @@ also have "\ = (j dvd (- (c*x - ?e)))" by (simp only: dvd_minus_iff) also have "\ = (j dvd (c* (- x)) + ?e)" - apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib) + apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib) by (simp add: algebra_simps) also have "\ = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))" using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"] diff -r 096ec174be5d -r d19c677eb812 src/HOL/GCD.thy --- a/src/HOL/GCD.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/GCD.thy Thu Sep 08 11:31:23 2011 +0200 @@ -485,16 +485,16 @@ done lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n" -by (metis gcd_red_int mod_add_self1 zadd_commute) +by (metis gcd_red_int mod_add_self1 add_commute) lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n" -by (metis gcd_add1_int gcd_commute_int zadd_commute) +by (metis gcd_add1_int gcd_commute_int add_commute) lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n" by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat) lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n" -by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute) +by (metis gcd_commute_int gcd_red_int mod_mult_self1 add_commute) (* to do: differences, and all variations of addition rules @@ -1030,8 +1030,7 @@ apply (subst mod_div_equality [of m n, symmetric]) (* applying simp here undoes the last substitution! what is procedure cancel_div_mod? *) - apply (simp only: field_simps zadd_int [symmetric] - zmult_int [symmetric]) + apply (simp only: field_simps of_nat_add of_nat_mult) done qed @@ -1237,7 +1236,7 @@ lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b" by (simp add: lcm_int_def lcm_nat_def zdiv_int - zmult_int [symmetric] gcd_int_def) + of_nat_mult gcd_int_def) lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n" unfolding lcm_nat_def diff -r 096ec174be5d -r d19c677eb812 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Sep 08 11:31:23 2011 +0200 @@ -93,7 +93,7 @@ have even_minus_odd:"\x y. even x \ odd (y::int) \ odd (x - y)" using assms by auto have odd_minus_even:"\x y. odd x \ even (y::int) \ odd (x - y)" using assms by auto show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum] - unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding zadd_int[THEN sym] apply(rule odd_plus_even) + unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding of_nat_add apply(rule odd_plus_even) apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed subsection {* The odd/even result for faces of complete vertices, generalized. *} diff -r 096ec174be5d -r d19c677eb812 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Sep 08 11:31:23 2011 +0200 @@ -4590,7 +4590,7 @@ hence "b : affine hull S1" using rel_interior_subset hull_subset[of S2] ** by auto hence "b : S1" using T_def b_def by auto hence False using b_def assms unfolding rel_frontier_def by auto -} ultimately show ?thesis using zless_le by auto +} ultimately show ?thesis using less_le by auto qed diff -r 096ec174be5d -r d19c677eb812 src/HOL/NSA/NSComplex.thy --- a/src/HOL/NSA/NSComplex.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/NSA/NSComplex.thy Thu Sep 08 11:31:23 2011 +0200 @@ -561,8 +561,7 @@ "!!a. hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)" apply transfer -apply (fold real_of_nat_def) -apply (rule cis_real_of_nat_Suc_mult) +apply (simp add: left_distrib cis_mult) done lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)" @@ -574,7 +573,7 @@ lemma hcis_hypreal_of_hypnat_Suc_mult: "!! a n. hcis (hypreal_of_hypnat (n + 1) * a) = hcis a * hcis (hypreal_of_hypnat n * a)" -by transfer (fold real_of_nat_def, simp add: cis_real_of_nat_Suc_mult) +by transfer (simp add: left_distrib cis_mult) lemma NSDeMoivre_ext: "!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)" diff -r 096ec174be5d -r d19c677eb812 src/HOL/Number_Theory/Primes.thy --- a/src/HOL/Number_Theory/Primes.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Number_Theory/Primes.thy Thu Sep 08 11:31:23 2011 +0200 @@ -174,7 +174,7 @@ EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n" unfolding prime_int_altdef dvd_def apply auto - by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le) + by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le) lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) --> n > 0 --> (p dvd x^n --> p dvd x)" @@ -220,7 +220,7 @@ "prime (p::int) \ p > 1 \ (\n \ {1<.. prime q \ p \ q \ coprime p q" apply (rule prime_imp_coprime_int, assumption) apply (unfold prime_int_altdef) - apply (metis int_one_le_iff_zero_less zless_le) + apply (metis int_one_le_iff_zero_less less_le) done lemma primes_imp_powers_coprime_nat: "prime (p::nat) \ prime q \ p ~= q \ coprime (p^m) (q^n)" diff -r 096ec174be5d -r d19c677eb812 src/HOL/Number_Theory/UniqueFactorization.thy --- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu Sep 08 11:31:23 2011 +0200 @@ -766,7 +766,7 @@ lemma multiplicity_dvd'_int: "(0::int) < x \ 0 <= y \ \p. prime p \ multiplicity p x \ multiplicity p y \ x dvd y" by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int - multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le) + multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) less_le) lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \ 0 < y \ (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)" diff -r 096ec174be5d -r d19c677eb812 src/HOL/Old_Number_Theory/Fib.thy --- a/src/HOL/Old_Number_Theory/Fib.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Old_Number_Theory/Fib.thy Thu Sep 08 11:31:23 2011 +0200 @@ -87,7 +87,7 @@ else fib (Suc n) * fib (Suc n) + 1)" apply (rule int_int_eq [THEN iffD1]) apply (simp add: fib_Cassini_int) - apply (subst zdiff_int [symmetric]) + apply (subst of_nat_diff) apply (insert fib_Suc_gr_0 [of n], simp_all) done diff -r 096ec174be5d -r d19c677eb812 src/HOL/Old_Number_Theory/Legacy_GCD.thy --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Sep 08 11:31:23 2011 +0200 @@ -699,7 +699,7 @@ lemma zgcd_zmult_distrib2: "0 \ k ==> k * zgcd m n = zgcd (k * m) (k * n)" by (simp del: minus_mult_right [symmetric] add: minus_mult_right nat_mult_distrib zgcd_def abs_if - mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) + mult_less_0_iff gcd_mult_distrib2 [symmetric] of_nat_mult) lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n" by (simp add: abs_if zgcd_zmult_distrib2) diff -r 096ec174be5d -r d19c677eb812 src/HOL/Old_Number_Theory/WilsonRuss.thy --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Thu Sep 08 11:31:23 2011 +0200 @@ -122,7 +122,7 @@ lemma inv_inv_aux: "5 \ p ==> nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))" apply (subst int_int_eq [symmetric]) - apply (simp add: zmult_int [symmetric]) + apply (simp add: of_nat_mult) apply (simp add: left_diff_distrib right_diff_distrib) done diff -r 096ec174be5d -r d19c677eb812 src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/RealDef.thy Thu Sep 08 11:31:23 2011 +0200 @@ -1411,16 +1411,13 @@ lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" by (insert real_of_nat_div2 [of n x], simp) -lemma real_of_int_real_of_nat: "real (int n) = real n" -by (simp add: real_of_nat_def real_of_int_def) - lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n" by (simp add: real_of_int_def real_of_nat_def) lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x" apply (subgoal_tac "real(int(nat x)) = real(nat x)") apply force - apply (simp only: real_of_int_real_of_nat) + apply (simp only: real_of_int_of_nat_eq) done lemma Nats_real_of_nat [simp]: "real (n::nat) \ Nats" @@ -1534,7 +1531,7 @@ "real (number_of v :: nat) = (if neg (number_of v :: int) then 0 else (number_of v :: real))" -by (simp add: real_of_int_real_of_nat [symmetric]) +by (simp add: real_of_int_of_nat_eq [symmetric]) declaration {* K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2] diff -r 096ec174be5d -r d19c677eb812 src/HOL/Word/Misc_Numeric.thy --- a/src/HOL/Word/Misc_Numeric.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Word/Misc_Numeric.thy Thu Sep 08 11:31:23 2011 +0200 @@ -312,7 +312,7 @@ apply safe apply (simp add: dvd_eq_mod_eq_0 [symmetric]) apply (drule le_iff_add [THEN iffD1]) - apply (force simp: zpower_zadd_distrib) + apply (force simp: power_add) apply (rule mod_pos_pos_trivial) apply (simp) apply (rule power_strict_increasing) diff -r 096ec174be5d -r d19c677eb812 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Sep 08 00:35:22 2011 +0200 +++ b/src/HOL/Word/Word.thy Thu Sep 08 11:31:23 2011 +0200 @@ -1257,7 +1257,7 @@ word_of_int_Ex [of b] word_of_int_Ex [of c] by (auto simp: word_of_int_hom_syms [symmetric] - zadd_0_right add_commute add_assoc add_left_commute + add_0_right add_commute add_assoc add_left_commute mult_commute mult_assoc mult_left_commute left_distrib right_distrib) @@ -4219,7 +4219,7 @@ apply (rule rotater_eqs) apply (simp add: word_size nat_mod_distrib) apply (rule int_eq_0_conv [THEN iffD1]) - apply (simp only: zmod_int zadd_int [symmetric]) + apply (simp only: zmod_int of_nat_add) apply (simp add: rdmods) done diff -r 096ec174be5d -r d19c677eb812 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Sep 08 00:35:22 2011 +0200 +++ b/src/Pure/PIDE/document.ML Thu Sep 08 11:31:23 2011 +0200 @@ -331,7 +331,6 @@ let val is_init = Toplevel.is_init tr; val is_proof = Keyword.is_proof (Toplevel.name_of tr); - val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof); val _ = Multithreading.interrupted (); val _ = Toplevel.status tr Markup.forked; @@ -343,13 +342,18 @@ in (case result of NONE => - (if null errs then Exn.interrupt () else (); - Toplevel.status tr Markup.failed; - (st, no_print)) + let + val _ = if null errs then Exn.interrupt () else (); + val _ = Toplevel.status tr Markup.failed; + in (st, no_print) end | SOME st' => - (Toplevel.status tr Markup.finished; - proof_status tr st'; - (st', if do_print then print_state tr st' else no_print))) + let + val _ = Toplevel.status tr Markup.finished; + val _ = proof_status tr st'; + val do_print = + not is_init andalso + (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); + in (st', if do_print then print_state tr st' else no_print) end) end; end; diff -r 096ec174be5d -r d19c677eb812 src/Pure/PIDE/xml.ML --- a/src/Pure/PIDE/xml.ML Thu Sep 08 00:35:22 2011 +0200 +++ b/src/Pure/PIDE/xml.ML Thu Sep 08 11:31:23 2011 +0200 @@ -47,6 +47,7 @@ val parse_element: string list -> tree * string list val parse_document: string list -> tree * string list val parse: string -> tree + val cache: unit -> tree -> tree exception XML_ATOM of string exception XML_BODY of body structure Encode: XML_DATA_OPS @@ -228,6 +229,48 @@ end; +(** cache for substructural sharing **) + +fun tree_ord tu = + if pointer_eq tu then EQUAL + else + (case tu of + (Text _, Elem _) => LESS + | (Elem _, Text _) => GREATER + | (Text s, Text s') => fast_string_ord (s, s') + | (Elem e, Elem e') => + prod_ord + (prod_ord fast_string_ord (list_ord (prod_ord fast_string_ord fast_string_ord))) + (list_ord tree_ord) (e, e')); + +structure Treetab = Table(type key = tree val ord = tree_ord); + +fun cache () = + let + val strings = Unsynchronized.ref (Symtab.empty: unit Symtab.table); + val trees = Unsynchronized.ref (Treetab.empty: unit Treetab.table); + + fun string s = + if size s <= 1 then s + else + (case Symtab.lookup_key (! strings) s of + SOME (s', ()) => s' + | NONE => (Unsynchronized.change strings (Symtab.update (s, ())); s)); + + fun tree t = + (case Treetab.lookup_key (! trees) t of + SOME (t', ()) => t' + | NONE => + let + val t' = + (case t of + Elem ((a, ps), b) => Elem ((string a, map (pairself string) ps), map tree b) + | Text s => Text (string s)); + val _ = Unsynchronized.change trees (Treetab.update (t', ())); + in t' end); + in tree end; + + (** XML as data representation language **) diff -r 096ec174be5d -r d19c677eb812 src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Thu Sep 08 00:35:22 2011 +0200 +++ b/src/Pure/PIDE/xml.scala Thu Sep 08 11:31:23 2011 +0200 @@ -84,7 +84,8 @@ def content(body: Body): Iterator[String] = content_stream(body).iterator - /* pipe-lined cache for partial sharing */ + + /** cache for partial sharing (weak table) **/ class Cache(initial_size: Int = 131071, max_string: Int = 100) { diff -r 096ec174be5d -r d19c677eb812 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Thu Sep 08 00:35:22 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Thu Sep 08 11:31:23 2011 +0200 @@ -99,6 +99,7 @@ val string_of_sort_global: theory -> sort -> string type syntax val eq_syntax: syntax * syntax -> bool + val join_syntax: syntax -> unit val lookup_const: syntax -> string -> string option val is_keyword: syntax -> string -> bool val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list @@ -508,6 +509,8 @@ fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; +fun join_syntax (Syntax ({gram, ...}, _)) = ignore (Future.join gram); + fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts; fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; diff -r 096ec174be5d -r d19c677eb812 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Sep 08 00:35:22 2011 +0200 +++ b/src/Pure/System/session.scala Thu Sep 08 11:31:23 2011 +0200 @@ -22,7 +22,7 @@ //{{{ case object Global_Settings - case object Perspective + case object Caret_Focus case object Assignment case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command]) @@ -52,7 +52,7 @@ /* pervasive event buses */ val global_settings = new Event_Bus[Session.Global_Settings.type] - val perspective = new Event_Bus[Session.Perspective.type] + val caret_focus = new Event_Bus[Session.Caret_Focus.type] val assignments = new Event_Bus[Session.Assignment.type] val commands_changed = new Event_Bus[Session.Commands_Changed] val phase_changed = new Event_Bus[Session.Phase] diff -r 096ec174be5d -r d19c677eb812 src/Pure/theory.ML --- a/src/Pure/theory.ML Thu Sep 08 00:35:22 2011 +0200 +++ b/src/Pure/theory.ML Thu Sep 08 11:31:23 2011 +0200 @@ -147,6 +147,7 @@ |> Sign.local_path |> Sign.map_naming (Name_Space.set_theory_name name) |> apply_wrappers wrappers + |> tap (Syntax.join_syntax o Sign.syn_of) end; fun end_theory thy = diff -r 096ec174be5d -r d19c677eb812 src/Tools/jEdit/README.html --- a/src/Tools/jEdit/README.html Thu Sep 08 00:35:22 2011 +0200 +++ b/src/Tools/jEdit/README.html Thu Sep 08 11:31:23 2011 +0200 @@ -144,6 +144,11 @@ Workaround: Force re-parsing of files using such commands via reload menu of jEdit. +
  • No way to delete document nodes from the overall collection of + theories.
    + Workaround: Restart whole Isabelle/jEdit session in + worst-case situation.
    • +
  • No support for non-local markup, e.g. commands reporting on previous commands (proof end on proof head), or markup produced by loading external files.
    • diff -r 096ec174be5d -r d19c677eb812 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Thu Sep 08 00:35:22 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Thu Sep 08 11:31:23 2011 +0200 @@ -362,7 +362,7 @@ private val caret_listener = new CaretListener { private val delay = Swing_Thread.delay_last(session.input_delay) { - session.perspective.event(Session.Perspective) + session.caret_focus.event(Session.Caret_Focus) } override def caretUpdate(e: CaretEvent) { delay() } } diff -r 096ec174be5d -r d19c677eb812 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Thu Sep 08 00:35:22 2011 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu Sep 08 11:31:23 2011 +0200 @@ -106,7 +106,7 @@ react { case Session.Global_Settings => handle_resize() case changed: Session.Commands_Changed => handle_update(Some(changed.commands)) - case Session.Perspective => if (follow_caret && handle_perspective()) handle_update() + case Session.Caret_Focus => if (follow_caret && handle_perspective()) handle_update() case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) } } @@ -116,14 +116,14 @@ { Isabelle.session.global_settings += main_actor Isabelle.session.commands_changed += main_actor - Isabelle.session.perspective += main_actor + Isabelle.session.caret_focus += main_actor } override def exit() { Isabelle.session.global_settings -= main_actor Isabelle.session.commands_changed -= main_actor - Isabelle.session.perspective -= main_actor + Isabelle.session.caret_focus -= main_actor }