--- 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/
--- 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;
--- 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"
;;
--- 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.
--- 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)
--- 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
--- 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
--- 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 "\<bar>p * x\<bar> = 1" by simp
hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
from this and prime
--- 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"
--- 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`
--- 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
--- 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)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
-proof -
- have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
- 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)
--- 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 "\<dots> < pow2 (?E div 2) * 2"
by (rule mult_strict_left_mono, auto intro: E_mod_pow)
- also have "\<dots> = pow2 (?E div 2 + 1)" unfolding zadd_commute[of _ 1] pow2_add1 by auto
+ also have "\<dots> = pow2 (?E div 2 + 1)" unfolding add_commute[of _ 1] pow2_add1 by auto
finally show ?thesis by auto
qed
finally show ?thesis
--- 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 "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: dvd_minus_iff)
also have "\<dots> = (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 "\<dots> = 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 "\<dots> = (j dvd (- (c*x - ?e)))"
by (simp only: dvd_minus_iff)
also have "\<dots> = (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 "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
--- 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
--- 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:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> 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. *}
--- 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
--- 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)"
--- 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) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
proof
assume "?L" thus "?R"
- by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
+ by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
next
assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
qed
@@ -272,7 +272,7 @@
lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> 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) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
--- 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 \<Longrightarrow> 0 <= y \<Longrightarrow>
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> 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) \<Longrightarrow> 0 < y \<Longrightarrow>
(x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
--- 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
--- 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 \<le> 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)
--- 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 \<le> 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
--- 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) \<in> 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]
--- 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)
--- 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
--- 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;
--- 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 **)
--- 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)
{
--- 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;
--- 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]
--- 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 =
--- 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 @@
<em>Workaround:</em> Force re-parsing of files using such commands
via reload menu of jEdit.</li>
+ <li>No way to delete document nodes from the overall collection of
+ theories.<br/>
+ <em>Workaround:</em> Restart whole Isabelle/jEdit session in
+ worst-case situation.</li>
+
<li>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.</li>
--- 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() }
}
--- 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
}