# HG changeset patch # User haftmann # Date 1245226086 -7200 # Node ID e5d4f7097c1bd3475f74a1d89549a7889b86501b # Parent d0115c3038462ea45fbffbe9366791c0f6948f7e# Parent 752f23a37240d8c3128aee8bc7b47c72ff452c06 merged diff -r 752f23a37240 -r e5d4f7097c1b .hgignore --- a/.hgignore Wed Jun 17 10:07:25 2009 +0200 +++ b/.hgignore Wed Jun 17 10:08:06 2009 +0200 @@ -8,6 +8,7 @@ syntax: regexp +^contrib ^heaps/ ^browser_info/ ^doc-src/.*\.aux diff -r 752f23a37240 -r e5d4f7097c1b Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Wed Jun 17 10:07:25 2009 +0200 +++ b/Admin/isatest/isatest-makedist Wed Jun 17 10:08:06 2009 +0200 @@ -102,7 +102,7 @@ #sleep 15 $SSH macbroy22 "$MAKEALL $HOME/settings/at64-poly-5.1-para" sleep 15 -$SSH macbroy23 "$MAKEALL $HOME/settings/at-sml-dev-e" +$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e" sleep 15 $SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly" sleep 15 diff -r 752f23a37240 -r e5d4f7097c1b Admin/isatest/isatest-statistics --- a/Admin/isatest/isatest-statistics Wed Jun 17 10:07:25 2009 +0200 +++ b/Admin/isatest/isatest-statistics Wed Jun 17 10:08:06 2009 +0200 @@ -51,7 +51,7 @@ SESSIONS="$@" case "$PLATFORM" in - *para*) + *para* | *-M*) PARALLEL=true ;; *) diff -r 752f23a37240 -r e5d4f7097c1b Admin/isatest/settings/mac-poly-M8 --- a/Admin/isatest/settings/mac-poly-M8 Wed Jun 17 10:07:25 2009 +0200 +++ b/Admin/isatest/settings/mac-poly-M8 Wed Jun 17 10:08:06 2009 +0200 @@ -4,7 +4,7 @@ ML_SYSTEM="polyml-experimental" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="--mutable 800 --immutable 2000" + ML_OPTIONS="--mutable 600 --immutable 1800" ISABELLE_HOME_USER=~/isabelle-mac-poly-M8 diff -r 752f23a37240 -r e5d4f7097c1b NEWS --- a/NEWS Wed Jun 17 10:07:25 2009 +0200 +++ b/NEWS Wed Jun 17 10:08:06 2009 +0200 @@ -40,6 +40,9 @@ * Implementation of quickcheck using generic code generator; default generators are provided for all suitable HOL types, records and datatypes. +* Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions +Set.Pow_def and Set.image_def. INCOMPATIBILITY. + *** ML *** diff -r 752f23a37240 -r e5d4f7097c1b etc/settings --- a/etc/settings Wed Jun 17 10:07:25 2009 +0200 +++ b/etc/settings Wed Jun 17 10:08:06 2009 +0200 @@ -91,8 +91,7 @@ ### Batch sessions (cf. isabelle usedir) ### -ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -v true -V outline=/proof,/ML" -#ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML" +ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML" # Specifically for the HOL image HOL_USEDIR_OPTIONS="" diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Divides.thy Wed Jun 17 10:08:06 2009 +0200 @@ -331,17 +331,22 @@ "(a * c) mod (b * c) = (a mod b) * c" using mod_mult_mult1 [of c a b] by (simp add: mult_commute) -end +lemma dvd_mod: "k dvd m \ k dvd n \ k dvd (m mod n)" + unfolding dvd_def by (auto simp add: mod_mult_mult1) + +lemma dvd_mod_iff: "k dvd n \ k dvd (m mod n) \ k dvd m" +by (blast intro: dvd_mod_imp_dvd dvd_mod) lemma div_power: - "(y::'a::{semiring_div,no_zero_divisors,power}) dvd x \ - (x div y) ^ n = x ^ n div y ^ n" + "y dvd x \ (x div y) ^ n = x ^ n div y ^ n" apply (induct n) apply simp apply(simp add: div_mult_div_if_dvd dvd_power_same) done -class ring_div = semiring_div + comm_ring_1 +end + +class ring_div = semiring_div + idom begin text {* Negation respects modular equivalence. *} @@ -905,15 +910,6 @@ apply (rule dvd_refl) done -lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n" - unfolding dvd_def - apply (case_tac "n = 0", auto) - apply (blast intro: mod_mult_distrib2 [symmetric]) - done - -lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)" -by (blast intro: dvd_mod_imp_dvd dvd_mod) - lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0 m dvd n" unfolding dvd_def apply (erule exE) diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/IntDiv.thy --- a/src/HOL/IntDiv.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/IntDiv.thy Wed Jun 17 10:08:06 2009 +0200 @@ -1059,13 +1059,10 @@ done lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n" - by (auto elim!: dvdE simp add: mod_mult_mult1) + by (rule dvd_mod) (* TODO: remove *) lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)" - apply (subgoal_tac "k dvd n * (m div n) + m mod n") - apply (simp add: zmod_zdiv_equality [symmetric]) - apply (simp only: dvd_add dvd_mult2) - done + by (rule dvd_mod_imp_dvd) (* TODO: remove *) lemma zdvd_not_zless: "0 < m ==> m < n ==> \ n dvd (m::int)" apply (auto elim!: dvdE) diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Library/Convex_Euclidean_Space.thy --- a/src/HOL/Library/Convex_Euclidean_Space.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy Wed Jun 17 10:08:06 2009 +0200 @@ -46,7 +46,8 @@ "setsum (\y. if (x = y) then P y else Q y) s = setsum Q s" apply(rule_tac [!] setsum_cong2) using assms by auto -lemma setsum_delta'': fixes s::"(real^'n) set" assumes "finite s" +lemma setsum_delta'': + fixes s::"'a::real_vector set" assumes "finite s" shows "(\x\s. (if y = x then f x else 0) *\<^sub>R x) = (if y\s then (f y) *\<^sub>R y else 0)" proof- have *:"\x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto @@ -107,8 +108,8 @@ subsection {* Affine set and affine hull.*} definition - affine :: "(real ^ 'n::finite) set \ bool" where - "affine s \ (\x\s. \y\s. \u v::real. u + v = 1 \ (u *\<^sub>R x + v *\<^sub>R y) \ s)" + affine :: "'a::real_vector set \ bool" where + "affine s \ (\x\s. \y\s. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)" lemma affine_alt: "affine s \ (\x\s. \y\s. \u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \ s)" proof- have *:"\u v ::real. u + v = 1 \ v = 1 - u" by auto @@ -149,7 +150,7 @@ subsection {* Some explicit formulations (from Lars Schewe). *} -lemma affine: fixes V::"(real^'n::finite) set" +lemma affine: fixes V::"'a::real_vector set" shows "affine V \ (\s u. finite s \ s \ {} \ s \ V \ setsum u s = 1 \ (setsum (\x. (u x) *\<^sub>R x)) s \ V)" unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+ defer apply(rule, rule, rule, rule, rule) proof- @@ -169,7 +170,7 @@ thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5) by(auto simp add: setsum_clauses(2)) next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s) - case (Suc n) fix s::"(real^'n) set" and u::"real^'n\ real" + case (Suc n) fix s::"'a set" and u::"'a \ real" assume IA:"\u s. \2 < card s; \x\V. \y\V. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ V; finite s; s \ {}; s \ V; setsum u s = 1; n \ card s \ \ (\x\s. u x *\<^sub>R x) \ V" and as:"Suc n \ card s" "2 < card s" "\x\V. \y\V. \u v. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ V" @@ -251,7 +252,8 @@ apply(rule hull_unique) unfolding mem_def by auto lemma affine_hull_finite_step: - shows "(\u::real^'n=>real. setsum u {} = w \ setsum (\x. u x *\<^sub>R x) {} = y) \ w = 0 \ y = 0" (is ?th1) + fixes y :: "'a::real_vector" + shows "(\u. setsum u {} = w \ setsum (\x. u x *\<^sub>R x) {} = y) \ w = 0 \ y = 0" (is ?th1) "finite s \ (\u. setsum u (insert a s) = w \ setsum (\x. u x *\<^sub>R x) (insert a s) = y) \ (\v u. setsum u s = w - v \ setsum (\x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \ (?lhs = ?rhs)") proof- @@ -288,10 +290,12 @@ ultimately show "?lhs = ?rhs" by blast qed -lemma affine_hull_2:"affine hull {a,b::real^'n::finite} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs") +lemma affine_hull_2: + fixes a b :: "'a::real_vector" + shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs") proof- have *:"\x y z. z = x - y \ y + z = (x::real)" - "\x y z. z = x - y \ y + z = (x::real^'n)" by auto + "\x y z. z = x - y \ y + z = (x::'a)" by auto have "?lhs = {y. \u. setsum u {a, b} = 1 \ (\v\{a, b}. u v *\<^sub>R v) = y}" using affine_hull_finite[of "{a,b}"] by auto also have "\ = {y. \v u. u b = 1 - v \ u b *\<^sub>R b = y - v *\<^sub>R a}" @@ -300,10 +304,12 @@ finally show ?thesis by auto qed -lemma affine_hull_3: "affine hull {a,b,c::real^'n::finite} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs") +lemma affine_hull_3: + fixes a b c :: "'a::real_vector" + shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs") proof- have *:"\x y z. z = x - y \ y + z = (x::real)" - "\x y z. z = x - y \ y + z = (x::real^'n)" by auto + "\x y z. z = x - y \ y + z = (x::'a)" by auto show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step) unfolding * apply auto apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto @@ -313,7 +319,8 @@ subsection {* Some relations between affine hull and subspaces. *} lemma affine_hull_insert_subset_span: - "affine hull (insert a s) \ {a + v| v . v \ span {x - a | x . x \ s}}" + fixes a :: "real ^ _" + shows "affine hull (insert a s) \ {a + v| v . v \ span {x - a | x . x \ s}}" unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq smult_conv_scaleR apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof- fix x t u assume as:"finite t" "t \ {}" "t \ insert a s" "setsum u t = 1" "(\v\t. u v *\<^sub>R v) = x" @@ -330,6 +337,7 @@ unfolding as by simp qed lemma affine_hull_insert_span: + fixes a :: "real ^ _" assumes "a \ s" shows "affine hull (insert a s) = {a + v | v . v \ span {x - a | x. x \ s}}" @@ -349,14 +357,16 @@ by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps) qed lemma affine_hull_span: + fixes a :: "real ^ _" assumes "a \ s" shows "affine hull s = {a + v | v. v \ span {x - a | x. x \ s - {a}}}" using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto subsection {* Convexity. *} -definition "convex (s::(real^'n::finite) set) \ - (\x\s. \y\s. \u\0. \v\0. (u + v = 1) \ (u *\<^sub>R x + v *\<^sub>R y) \ s)" +definition + convex :: "'a::real_vector set \ bool" where + "convex s \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s)" lemma convex_alt: "convex s \ (\x\s. \y\s. \u. 0 \ u \ u \ 1 \ ((1 - u) *\<^sub>R x + u *\<^sub>R y) \ s)" proof- have *:"\u v::real. u + v = 1 \ u = 1 - v" by auto @@ -445,7 +455,9 @@ thus ?thesis unfolding setsum_cl_ivl_Suc and *** and scaleR_right.setsum [symmetric] using nn by auto qed qed auto qed -lemma convex_explicit: "convex (s::(real^'n::finite) set) \ +lemma convex_explicit: + fixes s :: "'a::real_vector set" + shows "convex s \ (\t u. finite t \ t \ s \ (\x\t. 0 \ u x) \ setsum u t = 1 \ setsum (\x. u x *\<^sub>R x) t \ s)" unfolding convex_def apply(rule,rule,rule) apply(subst imp_conjL,rule) defer apply(rule,rule,rule,rule,rule,rule,rule) proof- fix x y u v assume as:"\t u. finite t \ t \ s \ (\x\t. 0 \ u x) \ setsum u t = 1 \ (\x\t. u x *\<^sub>R x) \ s" "x \ s" "y \ s" "0 \ u" "0 \ v" "u + v = (1::real)" @@ -453,7 +465,7 @@ case True show ?thesis unfolding True and scaleR_left_distrib[THEN sym] using as(3,6) by auto next case False thus ?thesis using as(1)[THEN spec[where x="{x,y}"], THEN spec[where x="\z. if z=x then u else v"]] and as(2-) by auto qed next - fix t u assume asm:"\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" "finite (t::(real^'n) set)" + fix t u assume asm:"\x\s. \y\s. \u\0. \v\0. u + v = 1 \ u *\<^sub>R x + v *\<^sub>R y \ s" "finite (t::'a set)" (*"finite t" "t \ s" "\x\t. (0::real) \ u x" "setsum u t = 1"*) from this(2) have "\u. t \ s \ (\x\t. 0 \ u x) \ setsum u t = 1 \ (\x\t. u x *\<^sub>R x) \ s" apply(induct_tac t rule:finite_induct) prefer 3 apply (rule,rule) apply(erule conjE)+ proof- @@ -493,7 +505,9 @@ subsection {* Cones. *} -definition "cone (s::(real^'n) set) \ (\x\s. \c\0. (c *\<^sub>R x) \ s)" +definition + cone :: "'a::real_vector set \ bool" where + "cone s \ (\x\s. \c\0. (c *\<^sub>R x) \ s)" lemma cone_empty[intro, simp]: "cone {}" unfolding cone_def by auto @@ -517,7 +531,7 @@ subsection {* Affine dependence and consequential theorems (from Lars Schewe). *} definition - affine_dependent :: "(real ^ 'n::finite) set \ bool" where + affine_dependent :: "'a::real_vector set \ bool" where "affine_dependent s \ (\x\s. x \ (affine hull (s - {x})))" lemma affine_dependent_explicit: @@ -537,21 +551,21 @@ have "s \ {v}" using as(3,6) by auto thus "\x\p. \s u. finite s \ s \ {} \ s \ p - {x} \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = x" apply(rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, rule_tac x="\x. - (1 / u v) * u x" in exI) - unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1_ring[OF as(1,5)] using as by auto + unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] using as by auto qed lemma affine_dependent_explicit_finite: - assumes "finite (s::(real^'n::finite) set)" + fixes s :: "'a::real_vector set" assumes "finite s" shows "affine_dependent s \ (\u. setsum u s = 0 \ (\v\s. u v \ 0) \ setsum (\v. u v *\<^sub>R v) s = 0)" (is "?lhs = ?rhs") proof - have *:"\vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::real^'n))" by auto + have *:"\vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" by auto assume ?lhs then obtain t u v where "finite t" "t \ s" "setsum u t = 0" "v\t" "u v \ 0" "(\v\t. u v *\<^sub>R v) = 0" unfolding affine_dependent_explicit by auto thus ?rhs apply(rule_tac x="\x. if x\t then u x else 0" in exI) apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym] - unfolding Int_absorb2[OF `t\s`, unfolded Int_commute] by auto + unfolding Int_absorb1[OF `t\s`] by auto next assume ?rhs then obtain u v where "setsum u s = 0" "v\s" "u v \ 0" "(\v\s. u v *\<^sub>R v) = 0" by auto @@ -561,6 +575,7 @@ subsection {* A general lemma. *} lemma convex_connected: + fixes s :: "'a::real_normed_vector set" assumes "convex s" shows "connected s" proof- { fix e1 e2 assume as:"open e1" "open e2" "e1 \ e2 \ s = {}" "s \ e1 \ e2" @@ -595,12 +610,14 @@ subsection {* One rather trivial consequence. *} -lemma connected_UNIV: "connected (UNIV :: (real ^ _) set)" +lemma connected_UNIV: "connected (UNIV :: 'a::real_normed_vector set)" by(simp add: convex_connected convex_UNIV) subsection {* Convex functions into the reals. *} -definition "convex_on s (f::real^'n \ real) = +definition + convex_on :: "'a::real_vector set \ ('a \ real) \ bool" where + "convex_on s f \ (\x\s. \y\s. \u\0. \v\0. u + v = 1 \ f (u *\<^sub>R x + v *\<^sub>R y) \ u * f x + v * f y)" lemma convex_on_subset: "convex_on t f \ s \ t \ convex_on s f" @@ -641,6 +658,7 @@ qed lemma convex_local_global_minimum: + fixes s :: "'a::real_normed_vector set" assumes "0 s" "\y\ball x e. f x \ f y" shows "\y\s. f x \ f y" proof(rule ccontr) @@ -661,7 +679,9 @@ ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto qed -lemma convex_distance: "convex_on s (\x. dist a x)" +lemma convex_distance: + fixes s :: "'a::real_normed_vector set" + shows "convex_on s (\x. dist a x)" proof(auto simp add: convex_on_def dist_norm) fix x y assume "x\s" "y\s" fix u v ::real assume "0 \ u" "0 \ v" "u + v = 1" @@ -710,23 +730,28 @@ proof- have "{a + y |y. y \ s} = (\x. a + x) ` s" by auto thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed -lemma convex_affinity: assumes "convex (s::(real^'n::finite) set)" shows "convex ((\x. a + c *\<^sub>R x) ` s)" +lemma convex_affinity: assumes "convex s" shows "convex ((\x. a + c *\<^sub>R x) ` s)" proof- have "(\x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed -lemma convex_linear_image: assumes c:"convex s" and l:"linear f" shows "convex(f ` s)" +lemma convex_linear_image: + assumes c:"convex s" and l:"bounded_linear f" + shows "convex(f ` s)" proof(auto simp add: convex_def) + interpret f: bounded_linear f by fact fix x y assume xy:"x \ s" "y \ s" fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" show "u *\<^sub>R f x + v *\<^sub>R f y \ f ` s" unfolding image_iff apply(rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in bexI) - unfolding linear_add[OF l] linear_cmul[OF l, unfolded smult_conv_scaleR] + unfolding f.add f.scaleR using c[unfolded convex_def] xy uv by auto qed subsection {* Balls, being convex, are connected. *} -lemma convex_ball: "convex (ball x e)" +lemma convex_ball: + fixes x :: "'a::real_normed_vector" + shows "convex (ball x e)" proof(auto simp add: convex_def) fix y z assume yz:"dist x y < e" "dist x z < e" fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" @@ -735,7 +760,9 @@ thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using real_convex_bound_lt[OF yz uv] by auto qed -lemma convex_cball: "convex(cball x e)" +lemma convex_cball: + fixes x :: "'a::real_normed_vector" + shows "convex(cball x e)" proof(auto simp add: convex_def Ball_def mem_cball) fix y z assume yz:"dist x y \ e" "dist x z \ e" fix u v ::real assume uv:" 0 \ u" "0 \ v" "u + v = 1" @@ -744,10 +771,14 @@ thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \ e" using real_convex_bound_le[OF yz uv] by auto qed -lemma connected_ball: "connected(ball (x::real^_) e)" (* FIXME: generalize *) +lemma connected_ball: + fixes x :: "'a::real_normed_vector" + shows "connected (ball x e)" using convex_connected convex_ball by auto -lemma connected_cball: "connected(cball (x::real^_) e)" (* FIXME: generalize *) +lemma connected_cball: + fixes x :: "'a::real_normed_vector" + shows "connected(cball x e)" using convex_connected convex_cball by auto subsection {* Convex hull. *} @@ -759,14 +790,17 @@ lemma convex_hull_eq: "(convex hull s = s) \ convex s" apply(rule hull_eq[unfolded mem_def]) using convex_Inter[unfolded Ball_def mem_def] by auto -lemma bounded_convex_hull: assumes "bounded s" shows "bounded(convex hull s)" +lemma bounded_convex_hull: + fixes s :: "'a::real_normed_vector set" + assumes "bounded s" shows "bounded(convex hull s)" proof- from assms obtain B where B:"\x\s. norm x \ B" unfolding bounded_iff by auto show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B]) unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball] unfolding subset_eq mem_cball dist_norm using B by auto qed lemma finite_imp_bounded_convex_hull: - "finite s \ bounded(convex hull s)" + fixes s :: "'a::real_normed_vector set" + shows "finite s \ bounded(convex hull s)" using bounded_convex_hull finite_imp_bounded by auto subsection {* Stepping theorems for convex hulls of finite sets. *} @@ -778,6 +812,7 @@ apply(rule hull_unique) unfolding mem_def by auto lemma convex_hull_insert: + fixes s :: "'a::real_vector set" assumes "s \ {}" shows "convex hull (insert a s) = {x. \u\0. \v\0. \b. (u + v = 1) \ b \ (convex hull s) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull") @@ -797,10 +832,10 @@ fix x y u v assume as:"(0::real) \ u" "0 \ v" "u + v = 1" "x\?hull" "y\?hull" from as(4) obtain u1 v1 b1 where obt1:"u1\0" "v1\0" "u1 + v1 = 1" "b1 \ convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto from as(5) obtain u2 v2 b2 where obt2:"u2\0" "v2\0" "u2 + v2 = 1" "b2 \ convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto - have *:"\(x::real^_) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) + have *:"\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) have "\b \ convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" proof(cases "u * v1 + v * v2 = 0") - have *:"\(x::real^_) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) + have *:"\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) case True hence **:"u * v1 = 0" "v * v2 = 0" apply- apply(rule_tac [!] ccontr) using mult_nonneg_nonneg[OF `u\0` `v1\0`] mult_nonneg_nonneg[OF `v\0` `v2\0`] by auto hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto @@ -834,7 +869,8 @@ subsection {* Explicit expression for convex hull. *} lemma convex_hull_indexed: - "convex hull s = {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ s) \ + fixes s :: "'a::real_vector set" + shows "convex hull s = {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ s) \ (setsum u {1..k} = 1) \ (setsum (\i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull") apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer @@ -852,7 +888,7 @@ fix x y u v assume uv:"0\u" "0\v" "u+v=(1::real)" and xy:"x\?hull" "y\?hull" from xy obtain k1 u1 x1 where x:"\i\{1::nat..k1}. 0\u1 i \ x1 i \ s" "setsum u1 {Suc 0..k1} = 1" "(\i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto from xy obtain k2 u2 x2 where y:"\i\{1::nat..k2}. 0\u2 i \ x2 i \ s" "setsum u2 {Suc 0..k2} = 1" "(\i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto - have *:"\P x1 x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)" + have *:"\P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)" "{1..k1 + k2} \ {1..k1} = {1..k1}" "{1..k1 + k2} \ - {1..k1} = (\i. i + k1) ` {1..k2}" prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le) have inj:"inj_on (\i. i + k1) {1..k2}" unfolding inj_on_def by auto @@ -873,7 +909,8 @@ qed lemma convex_hull_finite: - assumes "finite (s::(real^'n::finite)set)" + fixes s :: "'a::real_vector set" + assumes "finite s" shows "convex hull s = {y. \u. (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set") proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set]) @@ -902,8 +939,17 @@ subsection {* Another formulation from Lars Schewe. *} +lemma setsum_constant_scaleR: + fixes y :: "'a::real_vector" + shows "(\x\A. y) = of_nat (card A) *\<^sub>R y" +apply (cases "finite A") +apply (induct set: finite) +apply (simp_all add: algebra_simps) +done + lemma convex_hull_explicit: - "convex hull p = {y. \s u. finite s \ s \ p \ + fixes p :: "'a::real_vector set" + shows "convex hull p = {y. \s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs") proof- { fix x assume "x\?lhs" @@ -940,7 +986,9 @@ then obtain i where "i\{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto hence "{x. Suc 0 \ x \ x \ card s \ f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto hence "card {x. Suc 0 \ x \ x \ card s \ f x = y} = 1" by auto - hence "(\x\{x \ {1..card s}. f x = y}. u (f x)) = u y" "(\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" by auto } + hence "(\x\{x \ {1..card s}. f x = y}. u (f x)) = u y" + "(\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" + by (auto simp add: setsum_constant_scaleR) } hence "(\x = 1..card s. u (f x)) = 1" "(\i = 1..card s. u (f i) *\<^sub>R f i) = y" unfolding setsum_image_gen[OF *(1), of "\x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\x. u (f x)" f] @@ -956,7 +1004,7 @@ subsection {* A stepping theorem for that expansion. *} lemma convex_hull_finite_step: - assumes "finite (s::(real^'n) set)" + fixes s :: "'a::real_vector set" assumes "finite s" shows "(\u. (\x\insert a s. 0 \ u x) \ setsum u (insert a s) = w \ setsum (\x. u x *\<^sub>R x) (insert a s) = y) \ (\v\0. \u. (\x\s. 0 \ u x) \ setsum u s = w - v \ setsum (\x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs") proof(rule, case_tac[!] "a\s") @@ -995,7 +1043,7 @@ unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed lemma convex_hull_3: - "convex hull {a::real^'n::finite,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \ u \ 0 \ v \ 0 \ w \ u + v + w = 1}" + "convex hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \ u \ 0 \ v \ 0 \ w \ u + v + w = 1}" proof- have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto have *:"\x y z ::real. x + y + z = 1 \ x = 1 - y - z" @@ -1013,20 +1061,27 @@ subsection {* Relations among closure notions and corresponding hulls. *} -lemma subspace_imp_affine: "subspace s \ affine s" +text {* TODO: Generalize linear algebra concepts defined in @{text +Euclidean_Space.thy} so that we can generalize these lemmas. *} + +lemma subspace_imp_affine: + fixes s :: "(real ^ _) set" shows "subspace s \ affine s" unfolding subspace_def affine_def smult_conv_scaleR by auto lemma affine_imp_convex: "affine s \ convex s" unfolding affine_def convex_def by auto -lemma subspace_imp_convex: "subspace s \ convex s" +lemma subspace_imp_convex: + fixes s :: "(real ^ _) set" shows "subspace s \ convex s" using subspace_imp_affine affine_imp_convex by auto -lemma affine_hull_subset_span: "(affine hull s) \ (span s)" +lemma affine_hull_subset_span: + fixes s :: "(real ^ _) set" shows "(affine hull s) \ (span s)" unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def using subspace_imp_affine by auto -lemma convex_hull_subset_span: "(convex hull s) \ (span s)" +lemma convex_hull_subset_span: + fixes s :: "(real ^ _) set" shows "(convex hull s) \ (span s)" unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def using subspace_imp_convex by auto @@ -1034,11 +1089,13 @@ unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def using affine_imp_convex by auto -lemma affine_dependent_imp_dependent: "affine_dependent s \ dependent s" +lemma affine_dependent_imp_dependent: + fixes s :: "(real ^ _) set" shows "affine_dependent s \ dependent s" unfolding affine_dependent_def dependent_def using affine_hull_subset_span by auto lemma dependent_imp_affine_dependent: + fixes s :: "(real ^ _) set" assumes "dependent {x - a| x . x \ s}" "a \ s" shows "affine_dependent (insert a s)" proof- @@ -1188,6 +1245,7 @@ subsection {* Openness and compactness are preserved by convex hull operation. *} lemma open_convex_hull: + fixes s :: "'a::real_normed_vector set" assumes "open s" shows "open(convex hull s)" unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10) @@ -1255,7 +1313,7 @@ qed lemma compact_convex_combinations: - fixes s t :: "(real ^ 'n::finite) set" + fixes s t :: "'a::real_normed_vector set" assumes "compact s" "compact t" shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \ u \ u \ 1 \ x \ s \ y \ t}" proof- @@ -1351,13 +1409,14 @@ qed lemma finite_imp_compact_convex_hull: - "finite s \ compact(convex hull s)" + fixes s :: "(real ^ _) set" + shows "finite s \ compact(convex hull s)" apply(drule finite_imp_compact, drule compact_convex_hull) by assumption subsection {* Extremal points of a simplex are some vertices. *} lemma dist_increases_online: - fixes a b d :: "real ^ 'n::finite" + fixes a b d :: "'a::real_inner" assumes "d \ 0" shows "dist a (b + d) > dist a b \ dist a (b - d) > dist a b" proof(cases "inner a d - inner b d > 0") @@ -1373,11 +1432,12 @@ qed lemma norm_increases_online: - "(d::real^'n::finite) \ 0 \ norm(a + d) > norm a \ norm(a - d) > norm a" + fixes d :: "'a::real_inner" + shows "d \ 0 \ norm(a + d) > norm a \ norm(a - d) > norm a" using dist_increases_online[of d a 0] unfolding dist_norm by auto lemma simplex_furthest_lt: - fixes s::"(real^'n::finite) set" assumes "finite s" + fixes s::"'a::real_inner set" assumes "finite s" shows "\x \ (convex hull s). x \ s \ (\y\(convex hull s). norm(x - a) < norm(y - a))" proof(induct_tac rule: finite_induct[of s]) fix x s assume as:"finite s" "x\s" "\x\convex hull s. x \ s \ (\y\convex hull s. norm (x - a) < norm (y - a))" @@ -1432,6 +1492,7 @@ qed (auto simp add: assms) lemma simplex_furthest_le: + fixes s :: "(real ^ _) set" assumes "finite s" "s \ {}" shows "\y\s. \x\(convex hull s). norm(x - a) \ norm(y - a)" proof- @@ -1447,10 +1508,12 @@ qed lemma simplex_furthest_le_exists: - "finite s \ (\x\(convex hull s). \y\s. norm(x - a) \ norm(y - a))" + fixes s :: "(real ^ _) set" + shows "finite s \ (\x\(convex hull s). \y\s. norm(x - a) \ norm(y - a))" using simplex_furthest_le[of s] by (cases "s={}")auto lemma simplex_extremal_le: + fixes s :: "(real ^ _) set" assumes "finite s" "s \ {}" shows "\u\s. \v\s. \x\convex hull s. \y \ convex hull s. norm(x - y) \ norm(u - v)" proof- @@ -1471,7 +1534,8 @@ qed lemma simplex_extremal_le_exists: - "finite s \ x \ convex hull s \ y \ convex hull s + fixes s :: "(real ^ _) set" + shows "finite s \ x \ convex hull s \ y \ convex hull s \ (\u\s. \v\s. norm(x - y) \ norm(u - v))" using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto @@ -1532,6 +1596,7 @@ unfolding dist_norm by(auto simp add: norm_minus_commute field_simps) qed lemma any_closest_point_dot: + fixes s :: "(real ^ _) set" assumes "convex s" "closed s" "x \ s" "y \ s" "\z\s. dist a x \ dist a z" shows "inner (a - x) (y - x) \ 0" proof(rule ccontr) assume "\ inner (a - x) (y - x) \ 0" @@ -1552,6 +1617,7 @@ qed lemma any_closest_point_unique: + fixes s :: "(real ^ _) set" assumes "convex s" "closed s" "x \ s" "y \ s" "\z\s. dist a x \ dist a z" "\z\s. dist a y \ dist a z" shows "x = y" using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)] @@ -1603,6 +1669,7 @@ subsection {* Various point-to-set separating/supporting hyperplane theorems. *} lemma supporting_hyperplane_closed_point: + fixes s :: "(real ^ _) set" assumes "convex s" "closed s" "s \ {}" "z \ s" shows "\a b. \y\s. inner a z < b \ (inner a y = b) \ (\x\s. inner a x \ b)" proof- @@ -1621,6 +1688,7 @@ qed lemma separating_hyperplane_closed_point: + fixes s :: "(real ^ _) set" assumes "convex s" "closed s" "z \ s" shows "\a b. inner a z < b \ (\x\s. inner a x > b)" proof(cases "s={}") @@ -1691,6 +1759,7 @@ qed lemma separating_hyperplane_compact_closed: + fixes s :: "(real ^ _) set" assumes "convex s" "compact s" "s \ {}" "convex t" "closed t" "s \ t = {}" shows "\a b. (\x\s. inner a x < b) \ (\x\t. inner a x > b)" proof- obtain a b where "(\x\t. inner a x < b) \ (\x\s. b < inner a x)" @@ -1733,14 +1802,18 @@ subsection {* More convexity generalities. *} -lemma convex_closure: assumes "convex s" shows "convex(closure s)" +lemma convex_closure: + fixes s :: "'a::real_normed_vector set" + assumes "convex s" shows "convex(closure s)" unfolding convex_def Ball_def closure_sequential apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+ apply(rule_tac x="\n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule) apply(rule assms[unfolded convex_def, rule_format]) prefer 6 apply(rule Lim_add) apply(rule_tac [1-2] Lim_cmul) by auto -lemma convex_interior: assumes "convex s" shows "convex(interior s)" +lemma convex_interior: + fixes s :: "'a::real_normed_vector set" + assumes "convex s" shows "convex(interior s)" unfolding convex_alt Ball_def mem_interior apply(rule,rule,rule,rule,rule,rule) apply(erule exE | erule conjE)+ proof- fix x y u assume u:"0 \ u" "u \ (1::real)" fix e d assume ed:"ball x e \ s" "ball y d \ s" "0 {h. s \ h \ (\a b. h = {x. inner a x \ b})}" apply(rule set_ext, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof- @@ -1915,20 +1989,23 @@ subsection {* Convex hull is "preserved" by a linear function. *} lemma convex_hull_linear_image: - assumes "linear f" + assumes "bounded_linear f" shows "f ` (convex hull s) = convex hull (f ` s)" apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption -proof- show "convex {x. f x \ convex hull f ` s}" - unfolding convex_def by(auto simp add: linear_cmul[OF assms, unfolded smult_conv_scaleR] linear_add[OF assms] - convex_convex_hull[unfolded convex_def, rule_format]) next +proof- + interpret f: bounded_linear f by fact + show "convex {x. f x \ convex hull f ` s}" + unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next + interpret f: bounded_linear f by fact show "convex {x. x \ f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s] - unfolding convex_def by (auto simp add: linear_cmul[OF assms, THEN sym, unfolded smult_conv_scaleR] linear_add[OF assms, THEN sym]) + unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric]) qed auto lemma in_convex_hull_linear_image: - assumes "linear f" "x \ convex hull s" shows "(f x) \ convex hull (f ` s)" + assumes "bounded_linear f" "x \ convex hull s" + shows "(f x) \ convex hull (f ` s)" using convex_hull_linear_image[OF assms(1)] assms(2) by auto subsection {* Homeomorphism of all convex compact sets with nonempty interior. *} @@ -2188,6 +2265,7 @@ apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto lemma convex_on: + fixes s :: "(real ^ _) set" assumes "convex s" shows "convex_on s f \ (\k u x. (\i\{1..k::nat}. 0 \ u i \ x i \ s) \ setsum u {1..k} = 1 \ f (setsum (\i. u i *\<^sub>R x i) {1..k} ) \ setsum (\i. u i * f(x i)) {1..k} ) " @@ -2203,7 +2281,9 @@ subsection {* Convexity of general and special intervals. *} -lemma is_interval_convex: assumes "is_interval s" shows "convex s" +lemma is_interval_convex: + fixes s :: "(real ^ _) set" + assumes "is_interval s" shows "convex s" unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof- fix x y u v assume as:"x \ s" "y \ s" "0 \ u" "0 \ v" "u + v = (1::real)" hence *:"u = 1 - v" "1 - v \ 0" and **:"v = 1 - u" "1 - u \ 0" by auto @@ -2288,6 +2368,7 @@ subsection {* A bound within a convex hull, and so an interval. *} lemma convex_on_convex_hull_bound: + fixes s :: "(real ^ _) set" assumes "convex_on (convex hull s) f" "\x\s. f x \ b" shows "\x\ convex hull s. f x \ b" proof fix x assume "x\convex hull s" @@ -2390,6 +2471,7 @@ subsection {* Bounded convex function on open set is continuous. *} lemma convex_on_bounded_continuous: + fixes s :: "(real ^ _) set" assumes "open s" "convex_on s f" "\x\s. abs(f x) \ b" shows "continuous_on s f" apply(rule continuous_at_imp_continuous_on) unfolding continuous_at_real_range proof(rule,rule,rule) @@ -2440,6 +2522,7 @@ subsection {* Upper bound on a ball implies upper and lower bounds. *} lemma convex_bounds_lemma: + fixes x :: "real ^ _" assumes "convex_on (cball x e) f" "\y \ cball x e. f y \ b" shows "\y \ cball x e. abs(f y) \ b + 2 * abs(f x)" apply(rule) proof(cases "0 \ e") case True @@ -2619,6 +2702,7 @@ subsection {* Shrinking towards the interior of a convex set. *} lemma mem_interior_convex_shrink: + fixes s :: "(real ^ _) set" assumes "convex s" "c \ interior s" "x \ s" "0 < e" "e \ 1" shows "x - e *\<^sub>R (x - c) \ interior s" proof- obtain d where "d>0" and d:"ball c d \ s" using assms(2) unfolding mem_interior by auto @@ -2637,6 +2721,7 @@ qed(rule mult_pos_pos, insert `e>0` `d>0`, auto) qed lemma mem_interior_closure_convex_shrink: + fixes s :: "(real ^ _) set" assumes "convex s" "c \ interior s" "x \ closure s" "0 < e" "e \ 1" shows "x - e *\<^sub>R (x - c) \ interior s" proof- obtain d where "d>0" and d:"ball c d \ s" using assms(2) unfolding mem_interior by auto diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Library/Euclidean_Space.thy Wed Jun 17 10:08:06 2009 +0200 @@ -889,7 +889,7 @@ subsection {* A connectedness or intermediate value lemma with several applications. *} lemma connected_real_lemma: - fixes f :: "real \ real ^ 'n::finite" + fixes f :: "real \ 'a::metric_space" assumes ab: "a \ b" and fa: "f a \ e1" and fb: "f b \ e2" and dst: "\e x. a <= x \ x <= b \ 0 < e ==> \d > 0. \y. abs(y - x) < d \ dist(f y) (f x) < e" and e1: "\y \ e1. \e > 0. \y'. dist y' y < e \ y' \ e1" diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Library/Fin_Fun.thy --- a/src/HOL/Library/Fin_Fun.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Library/Fin_Fun.thy Wed Jun 17 10:08:06 2009 +0200 @@ -323,13 +323,13 @@ primrec random_finfun_aux :: "code_numeral \ code_numeral \ Random.seed \ ('a \\<^isub>f 'b \ (unit \ Code_Eval.term)) \ Random.seed" where "random_finfun_aux 0 j = Quickcheck.collapse (Random.select_weight - [(1, random j o\ (\y. Pair (valtermify_finfun_const y)))])" + [(1, Quickcheck.random j o\ (\y. Pair (valtermify_finfun_const y)))])" | "random_finfun_aux (Suc_code_numeral i) j = Quickcheck.collapse (Random.select_weight - [(Suc_code_numeral i, random j o\ (\x. random j o\ (\y. random_finfun_aux i j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), - (1, random j o\ (\y. Pair (valtermify_finfun_const y)))])" + [(Suc_code_numeral i, Quickcheck.random j o\ (\x. Quickcheck.random j o\ (\y. random_finfun_aux i j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), + (1, Quickcheck.random j o\ (\y. Pair (valtermify_finfun_const y)))])" definition - "random i = random_finfun_aux i i" + "Quickcheck.random i = random_finfun_aux i i" instance .. @@ -337,8 +337,8 @@ lemma random_finfun_aux_code [code]: "random_finfun_aux i j = Quickcheck.collapse (Random.select_weight - [(i, random j o\ (\x. random j o\ (\y. random_finfun_aux (i - 1) j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), - (1, random j o\ (\y. Pair (valtermify_finfun_const y)))])" + [(i, Quickcheck.random j o\ (\x. Quickcheck.random j o\ (\y. random_finfun_aux (i - 1) j o\ (\f. Pair (valtermify_finfun_update_code x y f))))), + (1, Quickcheck.random j o\ (\y. Pair (valtermify_finfun_const y)))])" apply (cases i rule: code_numeral.exhaust) apply (simp_all only: random_finfun_aux.simps code_numeral_zero_minus_one Suc_code_numeral_minus_one) apply (subst select_weight_cons_zero) apply (simp only:) diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Library/Polynomial.thy Wed Jun 17 10:08:06 2009 +0200 @@ -632,6 +632,25 @@ shows "a \ 0 \ p dvd smult a q \ p dvd q" by (safe elim!: dvd_smult dvd_smult_cancel) +lemma smult_dvd_cancel: + "smult a p dvd q \ p dvd q" +proof - + assume "smult a p dvd q" + then obtain k where "q = smult a p * k" .. + then have "q = p * smult a k" by simp + then show "p dvd q" .. +qed + +lemma smult_dvd: + fixes a :: "'a::field" + shows "p dvd q \ a \ 0 \ smult a p dvd q" + by (rule smult_dvd_cancel [where a="inverse a"]) simp + +lemma smult_dvd_iff: + fixes a :: "'a::field" + shows "smult a p dvd q \ (if a = 0 then q = 0 else p dvd q)" + by (auto elim: smult_dvd smult_dvd_cancel) + lemma degree_power_le: "degree (p ^ n) \ degree p * n" by (induct n, simp, auto intro: order_trans degree_mult_le) @@ -1102,6 +1121,109 @@ done +subsection {* GCD of polynomials *} + +function + poly_gcd :: "'a::field poly \ 'a poly \ 'a poly" where + "poly_gcd x 0 = smult (inverse (coeff x (degree x))) x" +| "y \ 0 \ poly_gcd x y = poly_gcd y (x mod y)" +by auto + +termination poly_gcd +by (relation "measure (\(x, y). if y = 0 then 0 else Suc (degree y))") + (auto dest: degree_mod_less) + +declare poly_gcd.simps [simp del, code del] + +lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x" + and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y" + apply (induct x y rule: poly_gcd.induct) + apply (simp_all add: poly_gcd.simps) + apply (fastsimp simp add: smult_dvd_iff dest: inverse_zero_imp_zero) + apply (blast dest: dvd_mod_imp_dvd) + done + +lemma poly_gcd_greatest: "k dvd x \ k dvd y \ k dvd poly_gcd x y" + by (induct x y rule: poly_gcd.induct) + (simp_all add: poly_gcd.simps dvd_mod dvd_smult) + +lemma dvd_poly_gcd_iff [iff]: + "k dvd poly_gcd x y \ k dvd x \ k dvd y" + by (blast intro!: poly_gcd_greatest intro: dvd_trans) + +lemma poly_gcd_monic: + "coeff (poly_gcd x y) (degree (poly_gcd x y)) = + (if x = 0 \ y = 0 then 0 else 1)" + by (induct x y rule: poly_gcd.induct) + (simp_all add: poly_gcd.simps nonzero_imp_inverse_nonzero) + +lemma poly_gcd_zero_iff [simp]: + "poly_gcd x y = 0 \ x = 0 \ y = 0" + by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff) + +lemma poly_gcd_0_0 [simp]: "poly_gcd 0 0 = 0" + by simp + +lemma poly_dvd_antisym: + fixes p q :: "'a::idom poly" + assumes coeff: "coeff p (degree p) = coeff q (degree q)" + assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q" +proof (cases "p = 0") + case True with coeff show "p = q" by simp +next + case False with coeff have "q \ 0" by auto + have degree: "degree p = degree q" + using `p dvd q` `q dvd p` `p \ 0` `q \ 0` + by (intro order_antisym dvd_imp_degree_le) + + from `p dvd q` obtain a where a: "q = p * a" .. + with `q \ 0` have "a \ 0" by auto + with degree a `p \ 0` have "degree a = 0" + by (simp add: degree_mult_eq) + with coeff a show "p = q" + by (cases a, auto split: if_splits) +qed + +lemma poly_gcd_unique: + assumes dvd1: "d dvd x" and dvd2: "d dvd y" + and greatest: "\k. k dvd x \ k dvd y \ k dvd d" + and monic: "coeff d (degree d) = (if x = 0 \ y = 0 then 0 else 1)" + shows "poly_gcd x y = d" +proof - + have "coeff (poly_gcd x y) (degree (poly_gcd x y)) = coeff d (degree d)" + by (simp_all add: poly_gcd_monic monic) + moreover have "poly_gcd x y dvd d" + using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest) + moreover have "d dvd poly_gcd x y" + using dvd1 dvd2 by (rule poly_gcd_greatest) + ultimately show ?thesis + by (rule poly_dvd_antisym) +qed + +lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x" +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) + +lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)" +by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic) + +lemmas poly_gcd_left_commute = + mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute] + +lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute + +lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1" +by (rule poly_gcd_unique) simp_all + +lemma poly_gcd_1_right [simp]: "poly_gcd x 1 = 1" +by (rule poly_gcd_unique) simp_all + +lemma poly_gcd_minus_left [simp]: "poly_gcd (- x) y = poly_gcd x y" +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) + +lemma poly_gcd_minus_right [simp]: "poly_gcd x (- y) = poly_gcd x y" +by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) + + subsection {* Evaluation of polynomials *} definition @@ -1472,4 +1594,10 @@ apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl]) done +lemma poly_gcd_code [code]: + "poly_gcd x y = + (if y = 0 then smult (inverse (coeff x (degree x))) x + else poly_gcd y (x mod y))" + by (simp add: poly_gcd.simps) + end diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Library/Topology_Euclidean_Space.thy --- a/src/HOL/Library/Topology_Euclidean_Space.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy Wed Jun 17 10:08:06 2009 +0200 @@ -1102,7 +1102,7 @@ text{* Notation Lim to avoid collition with lim defined in analysis *} definition - Lim :: "'a net \ ('a \ 'b::metric_space) \ 'b" where + Lim :: "'a net \ ('a \ 'b::t2_space) \ 'b" where "Lim net f = (THE l. (f ---> l) net)" lemma Lim: @@ -1238,11 +1238,10 @@ text{* Basic arithmetical combining theorems for limits. *} -lemma Lim_linear: fixes f :: "('a \ real^'n::finite)" and h :: "(real^'n \ real^'m::finite)" - assumes "(f ---> l) net" "linear h" +lemma Lim_linear: + assumes "(f ---> l) net" "bounded_linear h" shows "((\x. h (f x)) ---> h l) net" -using `linear h` `(f ---> l) net` -unfolding linear_conv_bounded_linear +using `bounded_linear h` `(f ---> l) net` by (rule bounded_linear.tendsto) lemma Lim_ident_at: "((\x. x) ---> a) (at a)" @@ -1252,7 +1251,7 @@ by (rule tendsto_const) lemma Lim_cmul: - fixes f :: "'a \ real ^ 'n::finite" + fixes f :: "'a \ 'b::real_normed_vector" shows "(f ---> l) net ==> ((\x. c *\<^sub>R f x) ---> c *\<^sub>R l) net" by (intro tendsto_intros) @@ -1402,47 +1401,41 @@ text{* Uniqueness of the limit, when nontrivial. *} lemma Lim_unique: - fixes f :: "'a \ 'b::metric_space" + fixes f :: "'a \ 'b::t2_space" assumes "\ trivial_limit net" "(f ---> l) net" "(f ---> l') net" shows "l = l'" proof (rule ccontr) - let ?d = "dist l l' / 2" assume "l \ l'" - then have "0 < ?d" by (simp add: dist_nz) - have "eventually (\x. dist (f x) l < ?d) net" - using `(f ---> l) net` `0 < ?d` by (rule tendstoD) + obtain U V where "open U" "open V" "l \ U" "l' \ V" "U \ V = {}" + using hausdorff [OF `l \ l'`] by fast + have "eventually (\x. f x \ U) net" + using `(f ---> l) net` `open U` `l \ U` by (rule topological_tendstoD) moreover - have "eventually (\x. dist (f x) l' < ?d) net" - using `(f ---> l') net` `0 < ?d` by (rule tendstoD) + have "eventually (\x. f x \ V) net" + using `(f ---> l') net` `open V` `l' \ V` by (rule topological_tendstoD) ultimately have "eventually (\x. False) net" proof (rule eventually_elim2) fix x - assume *: "dist (f x) l < ?d" "dist (f x) l' < ?d" - have "dist l l' \ dist (f x) l + dist (f x) l'" - by (rule dist_triangle_alt) - also from * have "\ < ?d + ?d" - by (rule add_strict_mono) - also have "\ = dist l l'" by simp - finally show "False" by simp + assume "f x \ U" "f x \ V" + hence "f x \ U \ V" by simp + with `U \ V = {}` show "False" by simp qed with `\ trivial_limit net` show "False" by (simp add: eventually_False) qed lemma tendsto_Lim: - fixes f :: "'a \ 'b::metric_space" + fixes f :: "'a \ 'b::t2_space" shows "~(trivial_limit net) \ (f ---> l) net ==> Lim net f = l" unfolding Lim_def using Lim_unique[of net f] by auto text{* Limit under bilinear function *} lemma Lim_bilinear: - fixes net :: "'a net" and h:: "real ^'m::finite \ real ^'n::finite \ real ^'p::finite" - assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h" + assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h" shows "((\x. h (f x) (g x)) ---> (h l m)) net" -using `bilinear h` `(f ---> l) net` `(g ---> m) net` -unfolding bilinear_conv_bounded_bilinear +using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net` by (rule bounded_bilinear.tendsto) text{* These are special for limits out of the same vector space. *} @@ -1496,29 +1489,19 @@ text{* It's also sometimes useful to extract the limit point from the net. *} definition - netlimit :: "'a::metric_space net \ 'a" where - "netlimit net = (SOME a. \r>0. eventually (\x. dist x a < r) net)" + netlimit :: "'a::t2_space net \ 'a" where + "netlimit net = (SOME a. ((\x. x) ---> a) net)" lemma netlimit_within: assumes "\ trivial_limit (at a within S)" shows "netlimit (at a within S) = a" -using assms -apply (simp add: trivial_limit_within) -apply (simp add: netlimit_def eventually_within zero_less_dist_iff) -apply (rule some_equality, fast) -apply (rename_tac b) -apply (rule ccontr) -apply (drule_tac x="dist b a / 2" in spec, drule mp, simp add: dist_nz) -apply (clarify, rename_tac r) -apply (simp only: islimpt_approachable) -apply (drule_tac x="min r (dist b a / 2)" in spec, drule mp, simp add: dist_nz) -apply (clarify) -apply (drule_tac x=x' in bspec, simp) -apply (drule mp, simp) -apply (subgoal_tac "dist b a < dist b a / 2 + dist b a / 2", simp) -apply (rule le_less_trans [OF dist_triangle3]) -apply (erule add_strict_mono) -apply simp +unfolding netlimit_def +apply (rule some_equality) +apply (rule Lim_at_within) +apply (rule Lim_ident_at) +apply (erule Lim_unique [OF assms]) +apply (rule Lim_at_within) +apply (rule Lim_ident_at) done lemma netlimit_at: @@ -2078,12 +2061,11 @@ qed lemma bounded_linear_image: - fixes f :: "real^'m::finite \ real^'n::finite" - assumes "bounded S" "linear f" + assumes "bounded S" "bounded_linear f" shows "bounded(f ` S)" proof- from assms(1) obtain b where b:"b>0" "\x\S. norm x \ b" unfolding bounded_pos by auto - from assms(2) obtain B where B:"B>0" "\x. norm (f x) \ B * norm x" using linear_bounded_pos by auto + from assms(2) obtain B where B:"B>0" "\x. norm (f x) \ B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac) { fix x assume "x\S" hence "norm x \ b" using b by auto hence "norm (f x) \ B * b" using B(2) apply(erule_tac x=x in allE) @@ -2094,10 +2076,9 @@ qed lemma bounded_scaling: - fixes S :: "(real ^ 'n::finite) set" + fixes S :: "'a::real_normed_vector set" shows "bounded S \ bounded ((\x. c *\<^sub>R x) ` S)" apply (rule bounded_linear_image, assumption) - apply (simp only: linear_conv_bounded_linear) apply (rule scaleR.bounded_linear_right) done @@ -3148,17 +3129,16 @@ subsection{* Define continuity over a net to take in restrictions of the set. *} definition - continuous :: "'a::metric_space net \ ('a \ 'b::metric_space) \ bool" where + continuous :: "'a::t2_space net \ ('a \ 'b::topological_space) \ bool" where "continuous net f \ (f ---> f(netlimit net)) net" - (* FIXME: generalize 'b to topological_space *) lemma continuous_trivial_limit: "trivial_limit net ==> continuous net f" - unfolding continuous_def tendsto_iff trivial_limit_eq by auto + unfolding continuous_def tendsto_def trivial_limit_eq by auto lemma continuous_within: "continuous (at x within s) f \ (f ---> f(x)) (at x within s)" unfolding continuous_def - unfolding tendsto_iff + unfolding tendsto_def using netlimit_within[of x s] by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually) @@ -3166,17 +3146,9 @@ using continuous_within [of x UNIV f] by (simp add: within_UNIV) lemma continuous_at_within: - fixes x :: "'a::perfect_space" assumes "continuous (at x) f" shows "continuous (at x within s) f" - (* FIXME: generalize *) -proof(cases "x islimpt s") - case True show ?thesis using assms unfolding continuous_def and netlimit_at - using Lim_at_within[of f "f x" "at x" s] - unfolding netlimit_within[unfolded trivial_limit_within not_not, OF True] by blast -next - case False thus ?thesis unfolding continuous_def and netlimit_at - unfolding Lim and trivial_limit_within by auto -qed + using assms unfolding continuous_at continuous_within + by (rule Lim_at_within) text{* Derive the epsilon-delta forms, which we often use as "definitions" *} @@ -3308,8 +3280,10 @@ text{* Characterization of various kinds of continuity in terms of sequences. *} +(* \ could be generalized, but \ requires metric space *) lemma continuous_within_sequentially: - "continuous (at a within s) f \ + fixes f :: "'a::metric_space \ 'b::metric_space" + shows "continuous (at a within s) f \ (\x. (\n::nat. x n \ s) \ (x ---> a) sequentially --> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs") proof @@ -3349,7 +3323,8 @@ qed lemma continuous_at_sequentially: - "continuous (at a) f \ (\x. (x ---> a) sequentially + fixes f :: "'a::metric_space \ 'b::metric_space" + shows "continuous (at a) f \ (\x. (x ---> a) sequentially --> ((f o x) ---> f a) sequentially)" using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto @@ -3449,22 +3424,22 @@ by (auto simp add: continuous_def Lim_const) lemma continuous_cmul: - fixes f :: "'a::metric_space \ real ^ 'n::finite" + fixes f :: "'a::t2_space \ 'b::real_normed_vector" shows "continuous net f ==> continuous net (\x. c *\<^sub>R f x)" by (auto simp add: continuous_def Lim_cmul) lemma continuous_neg: - fixes f :: "'a::metric_space \ 'b::real_normed_vector" + fixes f :: "'a::t2_space \ 'b::real_normed_vector" shows "continuous net f ==> continuous net (\x. -(f x))" by (auto simp add: continuous_def Lim_neg) lemma continuous_add: - fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + fixes f g :: "'a::t2_space \ 'b::real_normed_vector" shows "continuous net f \ continuous net g \ continuous net (\x. f x + g x)" by (auto simp add: continuous_def Lim_add) lemma continuous_sub: - fixes f g :: "'a::metric_space \ 'b::real_normed_vector" + fixes f g :: "'a::t2_space \ 'b::real_normed_vector" shows "continuous net f \ continuous net g \ continuous net (\x. f x - g x)" by (auto simp add: continuous_def Lim_sub) @@ -3475,7 +3450,7 @@ unfolding continuous_on_eq_continuous_within using continuous_const by blast lemma continuous_on_cmul: - fixes f :: "'a::metric_space \ real ^ _" + fixes f :: "'a::metric_space \ 'b::real_normed_vector" shows "continuous_on s f ==> continuous_on s (\x. c *\<^sub>R (f x))" unfolding continuous_on_eq_continuous_within using continuous_cmul by blast @@ -3503,7 +3478,8 @@ unfolding uniformly_continuous_on_def by simp lemma uniformly_continuous_on_cmul: - fixes f :: "'a::real_normed_vector \ real ^ _" + fixes f :: "'a::real_normed_vector \ 'b::real_normed_vector" + (* FIXME: generalize 'a to metric_space *) assumes "uniformly_continuous_on s f" shows "uniformly_continuous_on s (\x. c *\<^sub>R f(x))" proof- @@ -3551,11 +3527,11 @@ lemma continuous_within_id: "continuous (at a within s) (\x. x)" - unfolding continuous_within Lim_within by auto + unfolding continuous_within by (rule Lim_at_within [OF Lim_ident_at]) lemma continuous_at_id: "continuous (at a) (\x. x)" - unfolding continuous_at Lim_at by auto + unfolding continuous_at by (rule Lim_ident_at) lemma continuous_on_id: "continuous_on s (\x. x)" @@ -3568,6 +3544,8 @@ text{* Continuity of all kinds is preserved under composition. *} lemma continuous_within_compose: + fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) + fixes g :: "'b::metric_space \ 'c::metric_space" assumes "continuous (at x within s) f" "continuous (at (f x) within f ` s) g" shows "continuous (at x within s) (g o f)" proof- @@ -3582,6 +3560,8 @@ qed lemma continuous_at_compose: + fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) + fixes g :: "'b::metric_space \ 'c::metric_space" assumes "continuous (at x) f" "continuous (at (f x)) g" shows "continuous (at x) (g o f)" proof- @@ -3607,7 +3587,8 @@ text{* Continuity in terms of open preimages. *} lemma continuous_at_open: - "continuous (at x) f \ (\t. open t \ f x \ t --> (\s. open s \ x \ s \ (\x' \ s. (f x') \ t)))" (is "?lhs = ?rhs") + fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) + shows "continuous (at x) f \ (\t. open t \ f x \ t --> (\s. open s \ x \ s \ (\x' \ s. (f x') \ t)))" (is "?lhs = ?rhs") proof assume ?lhs { fix t assume as: "open t" "f x \ t" @@ -3736,13 +3717,25 @@ qed lemma continuous_open_preimage_univ: - "\x. continuous (at x) f \ open s \ open {x. f x \ s}" + fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) + shows "\x. continuous (at x) f \ open s \ open {x. f x \ s}" using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto lemma continuous_closed_preimage_univ: - "(\x. continuous (at x) f) \ closed s ==> closed {x. f x \ s}" + fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) + shows "(\x. continuous (at x) f) \ closed s ==> closed {x. f x \ s}" using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto +lemma continuous_open_vimage: + fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) + shows "\x. continuous (at x) f \ open s \ open (f -` s)" + unfolding vimage_def by (rule continuous_open_preimage_univ) + +lemma continuous_closed_vimage: + fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) + shows "\x. continuous (at x) f \ closed s \ closed (f -` s)" + unfolding vimage_def by (rule continuous_closed_preimage_univ) + text{* Equality of continuous functions on closure and related results. *} lemma continuous_closed_in_preimage_constant: @@ -3786,6 +3779,7 @@ text{* Making a continuous function avoid some value in a neighbourhood. *} lemma continuous_within_avoid: + fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) assumes "continuous (at x within s) f" "x \ s" "f x \ a" shows "\e>0. \y \ s. dist x y < e --> f y \ a" proof- @@ -3798,6 +3792,7 @@ qed lemma continuous_at_avoid: + fixes f :: "'a::metric_space \ 'b::metric_space" (* FIXME: generalize *) assumes "continuous (at x) f" "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ a" using assms using continuous_within_avoid[of x UNIV f a, unfolded within_UNIV] by auto @@ -3873,7 +3868,7 @@ qed lemma open_affinity: - fixes s :: "(real ^ _) set" + fixes s :: "'a::real_normed_vector set" assumes "open s" "c \ 0" shows "open ((\x. a + c *\<^sub>R x) ` s)" proof- @@ -4025,59 +4020,44 @@ subsection{* Topological properties of linear functions. *} -lemma linear_lim_0: fixes f::"real^'a::finite \ real^'b::finite" - assumes "linear f" shows "(f ---> 0) (at (0))" +lemma linear_lim_0: + assumes "bounded_linear f" shows "(f ---> 0) (at (0))" proof- - obtain B where "B>0" and B:"\x. norm (f x) \ B * norm x" using linear_bounded_pos[OF assms] by auto - { fix e::real assume "e>0" - { fix x::"real^'a" assume "norm x < e / B" - hence "B * norm x < e" using `B>0` using mult_strict_right_mono[of "norm x" " e / B" B] unfolding real_mult_commute by auto - hence "norm (f x) < e" using B[THEN spec[where x=x]] `B>0` using order_le_less_trans[of "norm (f x)" "B * norm x" e] by auto } - moreover have "e / B > 0" using `e>0` `B>0` divide_pos_pos by auto - ultimately have "\d>0. \x. 0 < dist x 0 \ dist x 0 < d \ dist (f x) 0 < e" unfolding dist_norm by auto } - thus ?thesis unfolding Lim_at by auto -qed - -lemma bounded_linear_continuous_at: + interpret f: bounded_linear f by fact + have "(f ---> f 0) (at 0)" + using tendsto_ident_at by (rule f.tendsto) + thus ?thesis unfolding f.zero . +qed + +lemma linear_continuous_at: assumes "bounded_linear f" shows "continuous (at a) f" unfolding continuous_at using assms apply (rule bounded_linear.tendsto) - apply (rule Lim_at_id [unfolded id_def]) + apply (rule tendsto_ident_at) done -lemma linear_continuous_at: - fixes f :: "real ^ _ \ real ^ _" - assumes "linear f" shows "continuous (at a) f" - using assms unfolding linear_conv_bounded_linear - by (rule bounded_linear_continuous_at) - lemma linear_continuous_within: - fixes f :: "real ^ _ \ real ^ _" - shows "linear f ==> continuous (at x within s) f" + shows "bounded_linear f ==> continuous (at x within s) f" using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto lemma linear_continuous_on: - fixes f :: "real ^ _ \ real ^ _" - shows "linear f ==> continuous_on s f" + shows "bounded_linear f ==> continuous_on s f" using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto text{* Also bilinear functions, in composition form. *} lemma bilinear_continuous_at_compose: - fixes f :: "real ^ _ \ real ^ _" - shows "continuous (at x) f \ continuous (at x) g \ bilinear h + shows "continuous (at x) f \ continuous (at x) g \ bounded_bilinear h ==> continuous (at x) (\x. h (f x) (g x))" unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto lemma bilinear_continuous_within_compose: - fixes h :: "real ^ _ \ real ^ _ \ real ^ _" - shows "continuous (at x within s) f \ continuous (at x within s) g \ bilinear h + shows "continuous (at x within s) f \ continuous (at x within s) g \ bounded_bilinear h ==> continuous (at x within s) (\x. h (f x) (g x))" unfolding continuous_within using Lim_bilinear[of f "f x"] by auto lemma bilinear_continuous_on_compose: - fixes h :: "real ^ _ \ real ^ _ \ real ^ _" - shows "continuous_on s f \ continuous_on s g \ bilinear h + shows "continuous_on s f \ continuous_on s g \ bounded_bilinear h ==> continuous_on s (\x. h (f x) (g x))" unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto using bilinear_continuous_within_compose[of _ s f g h] by auto @@ -4233,10 +4213,10 @@ subsection{* We can now extend limit compositions to consider the scalar multiplier. *} lemma Lim_mul: - fixes f :: "'a \ real ^ _" + fixes f :: "'a \ 'b::real_normed_vector" assumes "(c ---> d) net" "(f ---> l) net" shows "((\x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net" - unfolding smult_conv_scaleR using assms by (rule scaleR.tendsto) + using assms by (rule scaleR.tendsto) lemma Lim_vmul: fixes c :: "'a \ real" and v :: "'b::real_normed_vector" @@ -4367,25 +4347,20 @@ text{* Hence some useful properties follow quite easily. *} -lemma compact_scaleR_image: +lemma compact_scaling: fixes s :: "'a::real_normed_vector set" - assumes "compact s" shows "compact ((\x. scaleR c x) ` s)" + assumes "compact s" shows "compact ((\x. c *\<^sub>R x) ` s)" proof- let ?f = "\x. scaleR c x" have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right) show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f] - using bounded_linear_continuous_at[OF *] assms by auto -qed - -lemma compact_scaling: - fixes s :: "(real ^ _) set" - assumes "compact s" shows "compact ((\x. c *\<^sub>R x) ` s)" - using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image) + using linear_continuous_at[OF *] assms by auto +qed lemma compact_negations: fixes s :: "'a::real_normed_vector set" assumes "compact s" shows "compact ((\x. -x) ` s)" - using compact_scaleR_image [OF assms, of "- 1"] by auto + using compact_scaling [OF assms, of "- 1"] by auto lemma compact_sums: fixes s t :: "'a::real_normed_vector set" @@ -4416,7 +4391,7 @@ qed lemma compact_affinity: - fixes s :: "(real ^ _) set" + fixes s :: "'a::real_normed_vector set" assumes "compact s" shows "compact ((\x. a + c *\<^sub>R x) ` s)" proof- have "op + a ` op *\<^sub>R c ` s = (\x. a + c *\<^sub>R x) ` s" by auto @@ -4490,9 +4465,9 @@ text{* Related results with closure as the conclusion. *} -lemma closed_scaleR_image: +lemma closed_scaling: fixes s :: "'a::real_normed_vector set" - assumes "closed s" shows "closed ((\x. scaleR c x) ` s)" + assumes "closed s" shows "closed ((\x. c *\<^sub>R x) ` s)" proof(cases "s={}") case True thus ?thesis by auto next @@ -4524,15 +4499,10 @@ qed qed -lemma closed_scaling: - fixes s :: "(real ^ _) set" - assumes "closed s" shows "closed ((\x. c *\<^sub>R x) ` s)" - using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image) - lemma closed_negations: fixes s :: "'a::real_normed_vector set" assumes "closed s" shows "closed ((\x. -x) ` s)" - using closed_scaleR_image[OF assms, of "- 1"] by simp + using closed_scaling[OF assms, of "- 1"] by simp lemma compact_closed_sums: fixes s :: "'a::real_normed_vector set" @@ -5149,24 +5119,12 @@ subsection{* Closure of halfspaces and hyperplanes. *} -lemma Lim_dot: fixes f :: "real^'m \ real^'n::finite" - assumes "(f ---> l) net" shows "((\y. a \ (f y)) ---> a \ l) net" - unfolding dot_def by (intro tendsto_intros assms) - -lemma continuous_at_dot: - fixes x :: "real ^ _" - shows "continuous (at x) (\y. a \ y)" -proof- - have "((\x. x) ---> x) (at x)" unfolding Lim_at by auto - thus ?thesis unfolding continuous_at and o_def using Lim_dot[of "\x. x" x "at x" a] by auto -qed - -lemma continuous_on_dot: - fixes s :: "(real ^ _) set" - shows "continuous_on s (\y. a \ y)" - using continuous_at_imp_continuous_on[of s "\y. a \ y"] - using continuous_at_dot - by auto +lemma Lim_inner: + assumes "(f ---> l) net" shows "((\y. inner a (f y)) ---> inner a l) net" + by (intro tendsto_intros assms) + +lemma continuous_at_inner: "continuous (at x) (inner a)" + unfolding continuous_at by (intro tendsto_intros) lemma continuous_on_inner: fixes s :: "'a::real_inner set" @@ -5175,16 +5133,12 @@ lemma closed_halfspace_le: "closed {x. inner a x \ b}" proof- - have *:"{x \ UNIV. inner a x \ {r. \x. inner a x = r \ r \ b}} = {x. inner a x \ b}" by auto - let ?T = "{..b}" - have "closed ?T" by (rule closed_real_atMost) - moreover have "{r. \x. inner a x = r \ r \ b} = range (inner a) \ ?T" - unfolding image_def by auto - ultimately have "\T. closed T \ {r. \x. inner a x = r \ r \ b} = range (inner a) \ T" by fast - hence "closedin euclidean {x \ UNIV. inner a x \ {r. \x. inner a x = r \ r \ b}}" - using continuous_on_inner[of UNIV a, unfolded continuous_on_closed subtopology_UNIV] unfolding closedin_closed - by (fast elim!: allE[where x="{r. (\x. inner a x = r \ r \ b)}"]) - thus ?thesis unfolding closed_closedin[THEN sym] and * by auto + have "\x. continuous (at x) (inner a)" + unfolding continuous_at by (rule allI) (intro tendsto_intros) + hence "closed (inner a -` {..b})" + using closed_real_atMost by (rule continuous_closed_vimage) + moreover have "{x. inner a x \ b} = inner a -` {..b}" by auto + ultimately show ?thesis by simp qed lemma closed_halfspace_ge: "closed {x. inner a x \ b}" @@ -5279,7 +5233,7 @@ using assms unfolding continuous_on unfolding Lim_within_union unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto -lemma continuous_on_cases: fixes g :: "real^'m::finite \ real ^'n::finite" +lemma continuous_on_cases: assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g" "\x. (x\s \ \ P x) \ (x \ t \ P x) \ f x = g x" shows "continuous_on (s \ t) (\x. if P x then f x else g x)" @@ -5335,22 +5289,24 @@ (\x\s. (g(f x) = x)) \ (f ` s = t) \ continuous_on s f \ (\y\t. (f(g y) = y)) \ (g ` t = s) \ continuous_on t g" -definition homeomorphic :: "((real^'a::finite) set) \ ((real^'b::finite) set) \ bool" (infixr "homeomorphic" 60) where +definition + homeomorphic :: "'a::metric_space set \ 'b::metric_space set \ bool" + (infixr "homeomorphic" 60) where homeomorphic_def: "s homeomorphic t \ (\f g. homeomorphism s t f g)" lemma homeomorphic_refl: "s homeomorphic s" unfolding homeomorphic_def unfolding homeomorphism_def using continuous_on_id - apply(rule_tac x = "(\x::real^'a.x)" in exI) - apply(rule_tac x = "(\x::real^'b.x)" in exI) + apply(rule_tac x = "(\x. x)" in exI) + apply(rule_tac x = "(\x. x)" in exI) by blast lemma homeomorphic_sym: "s homeomorphic t \ t homeomorphic s" unfolding homeomorphic_def unfolding homeomorphism_def -by blast +by blast (* FIXME: slow *) lemma homeomorphic_trans: assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u" @@ -5392,7 +5348,8 @@ using assms unfolding inj_on_def inv_on_def by auto lemma homeomorphism_compact: - fixes f :: "real ^ _ \ real ^ _" + fixes f :: "'a::heine_borel \ 'b::heine_borel" + (* class constraint due to continuous_on_inverse *) assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s" shows "\g. homeomorphism s t f g" proof- @@ -5419,7 +5376,9 @@ qed lemma homeomorphic_compact: - "compact s \ continuous_on s f \ (f ` s = t) \ inj_on f s + fixes f :: "'a::heine_borel \ 'b::heine_borel" + (* class constraint due to continuous_on_inverse *) + shows "compact s \ continuous_on s f \ (f ` s = t) \ inj_on f s \ s homeomorphic t" unfolding homeomorphic_def by(metis homeomorphism_compact) @@ -5433,6 +5392,7 @@ text{* Results on translation, scaling etc. *} lemma homeomorphic_scaling: + fixes s :: "'a::real_normed_vector set" assumes "c \ 0" shows "s homeomorphic ((\x. c *\<^sub>R x) ` s)" unfolding homeomorphic_minimal apply(rule_tac x="\x. c *\<^sub>R x" in exI) @@ -5441,13 +5401,15 @@ using continuous_on_cmul[OF continuous_on_id] by auto lemma homeomorphic_translation: - "s homeomorphic ((\x. a + x) ` s)" + fixes s :: "'a::real_normed_vector set" + shows "s homeomorphic ((\x. a + x) ` s)" unfolding homeomorphic_minimal apply(rule_tac x="\x. a + x" in exI) apply(rule_tac x="\x. -a + x" in exI) using continuous_on_add[OF continuous_on_const continuous_on_id] by auto lemma homeomorphic_affinity: + fixes s :: "'a::real_normed_vector set" assumes "c \ 0" shows "s homeomorphic ((\x. a + c *\<^sub>R x) ` s)" proof- have *:"op + a ` op *\<^sub>R c ` s = (\x. a + c *\<^sub>R x) ` s" by auto @@ -5457,7 +5419,8 @@ using homeomorphic_translation[of "(\x. c *\<^sub>R x) ` s" a] unfolding * by auto qed -lemma homeomorphic_balls: fixes a b ::"real^'a::finite" +lemma homeomorphic_balls: + fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *) assumes "0 < d" "0 < e" shows "(ball a d) homeomorphic (ball b e)" (is ?th) "(cball a d) homeomorphic (cball b e)" (is ?cth) @@ -5487,14 +5450,15 @@ lemma cauchy_isometric: fixes x :: "nat \ real ^ 'n::finite" - assumes e:"0 < e" and s:"subspace s" and f:"linear f" and normf:"\x\s. norm(f x) \ e * norm(x)" and xs:"\n::nat. x n \ s" and cf:"Cauchy(f o x)" + assumes e:"0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\x\s. norm(f x) \ e * norm(x)" and xs:"\n::nat. x n \ s" and cf:"Cauchy(f o x)" shows "Cauchy x" proof- + interpret f: bounded_linear f by fact { fix d::real assume "d>0" then obtain N where N:"\n\N. norm (f (x n) - f (x N)) < e * d" using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto { fix n assume "n\N" - hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding linear_sub[OF f, THEN sym] by auto + hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding f.diff[THEN sym] by auto moreover have "e * norm (x n - x N) \ norm (f (x n - x N))" using subspace_sub[OF s, of "x n" "x N"] using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]] using normf[THEN bspec[where x="x n - x N"]] by auto @@ -5506,7 +5470,7 @@ lemma complete_isometric_image: fixes f :: "real ^ _ \ real ^ _" - assumes "0 < e" and s:"subspace s" and f:"linear f" and normf:"\x\s. norm(f x) \ e * norm(x)" and cs:"complete s" + assumes "0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\x\s. norm(f x) \ e * norm(x)" and cs:"complete s" shows "complete(f ` s)" proof- { fix g assume as:"\n::nat. g n \ f ` s" and cfg:"Cauchy g" @@ -5529,7 +5493,7 @@ unfolding dist_norm by simp lemma injective_imp_isometric: fixes f::"real^'m::finite \ real^'n::finite" - assumes s:"closed s" "subspace s" and f:"linear f" "\x\s. (f x = 0) \ (x = 0)" + assumes s:"closed s" "subspace s" and f:"bounded_linear f" "\x\s. (f x = 0) \ (x = 0)" shows "\e>0. \x\s. norm (f x) \ e * norm(x)" proof(cases "s \ {0::real^'m}") case True @@ -5538,6 +5502,7 @@ hence "norm x \ norm (f x)" by auto } thus ?thesis by(auto intro!: exI[where x=1]) next + interpret f: bounded_linear f by fact case False then obtain a where a:"a\0" "a\s" by auto from False have "s \ {}" by auto @@ -5571,7 +5536,7 @@ have "\c. \x\s. c *\<^sub>R x \ s" using s[unfolded subspace_def smult_conv_scaleR] by auto hence "(norm a / norm x) *\<^sub>R x \ {x \ s. norm x = norm a}" using `x\s` and `x\0` by auto thus "norm (f b) / norm b * norm x \ norm (f x)" using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]] - unfolding linear_cmul[OF f(1), unfolded smult_conv_scaleR] and ba using `x\0` `a\0` + unfolding f.scaleR and ba using `x\0` `a\0` by (auto simp add: real_mult_commute pos_le_divide_eq pos_divide_le_eq) qed } ultimately @@ -5579,8 +5544,8 @@ qed lemma closed_injective_image_subspace: - fixes s :: "(real ^ _) set" - assumes "subspace s" "linear f" "\x\s. f x = 0 --> x = 0" "closed s" + fixes f :: "real ^ _ \ real ^ _" + assumes "subspace s" "bounded_linear f" "\x\s. f x = 0 --> x = 0" "closed s" shows "closed(f ` s)" proof- obtain e where "e>0" and e:"\x\s. e * norm x \ norm (f x)" using injective_imp_isometric[OF assms(4,1,2,3)] by auto @@ -5688,10 +5653,11 @@ then obtain d::"'n set" where t: "card d = dim s" using closed_subspace_lemma by auto let ?t = "{x::real^'n. \i. i \ d \ x$i = 0}" - obtain f where f:"linear f" "f ` ?t = s" "inj_on f ?t" - using subspace_isomorphism[OF subspace_substandard[of "\i. i \ d"] assms] + obtain f where f:"bounded_linear f" "f ` ?t = s" "inj_on f ?t" + using subspace_isomorphism[unfolded linear_conv_bounded_linear, OF subspace_substandard[of "\i. i \ d"] assms] using dim_substandard[of d] and t by auto - have "\x\?t. f x = 0 \ x = 0" using linear_0[OF f(1)] using f(3)[unfolded inj_on_def] + interpret f: bounded_linear f by fact + have "\x\?t. f x = 0 \ x = 0" using f.zero using f(3)[unfolded inj_on_def] by(erule_tac x=0 in ballE) auto moreover have "closed ?t" using closed_substandard . moreover have "subspace ?t" using subspace_substandard . diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Jun 17 10:08:06 2009 +0200 @@ -101,8 +101,9 @@ val (_,thy1) = fold_map (fn ak => fn thy => let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)]) - val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy - val inject_flat = Library.flat inject + val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype + DatatypeAux.default_datatype_config [ak] [dt] thy + val inject_flat = flat inject val ak_type = Type (Sign.intern_type thy1 ak,[]) val ak_sign = Sign.intern_const thy1 ak diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Wed Jun 17 10:08:06 2009 +0200 @@ -6,8 +6,9 @@ signature NOMINAL_PACKAGE = sig - val add_nominal_datatype : bool -> string list -> (string list * bstring * mixfix * - (bstring * string list * mixfix) list) list -> theory -> theory + val add_nominal_datatype : DatatypeAux.datatype_config -> string list -> + (string list * bstring * mixfix * + (bstring * string list * mixfix) list) list -> theory -> theory type descr type nominal_datatype_info val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table @@ -190,7 +191,7 @@ fun fresh_star_const T U = Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT); -fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy = +fun gen_add_nominal_datatype prep_typ config new_type_names dts thy = let (* this theory is used just for parsing *) @@ -243,7 +244,7 @@ val full_new_type_names' = map (Sign.full_bname thy) new_type_names'; val ({induction, ...},thy1) = - DatatypePackage.add_datatype err flat_names new_type_names' dts'' thy; + DatatypePackage.add_datatype config new_type_names' dts'' thy; val SOME {descr, ...} = Symtab.lookup (DatatypePackage.get_datatypes thy1) (hd full_new_type_names'); @@ -815,7 +816,7 @@ val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T') ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax) in - (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) + (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) end; val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs @@ -1509,7 +1510,7 @@ val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) = thy10 |> InductivePackage.add_inductive_global (serial_string ()) - {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, + {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) @@ -2067,7 +2068,7 @@ thy13 end; -val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ true; +val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ; (* FIXME: The following stuff should be exported by DatatypePackage *) @@ -2083,7 +2084,7 @@ val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args; val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; - in add_nominal_datatype false names specs end; + in add_nominal_datatype DatatypeAux.default_datatype_config names specs end; val _ = OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Product_Type.thy Wed Jun 17 10:08:06 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Product_Type.thy - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge *) diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Quickcheck.thy Wed Jun 17 10:08:06 2009 +0200 @@ -137,7 +137,7 @@ code_reserved Quickcheck Quickcheck_Generators -hide (open) const collapse beyond random_fun_aux random_fun_lift +hide (open) const random collapse beyond random_fun_aux random_fun_lift no_notation fcomp (infixl "o>" 60) no_notation scomp (infixl "o\" 60) diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Rational.thy --- a/src/HOL/Rational.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Rational.thy Wed Jun 17 10:08:06 2009 +0200 @@ -1012,7 +1012,7 @@ begin definition - "random i = random i o\ (\num. Random.range i o\ (\denom. Pair ( + "Quickcheck.random i = Quickcheck.random i o\ (\num. Random.range i o\ (\denom. Pair ( let j = Code_Numeral.int_of (denom + 1) in valterm_fract num (j, \u. Code_Eval.term_of j))))" @@ -1048,7 +1048,7 @@ val p' = p div g; val q' = q div g; val r = (if one_of [true, false] then p' else ~ p', - if p' = 0 then 0 else q') + if p' = 0 then 1 else q') in (r, fn () => term_of_rat r) end; @@ -1060,8 +1060,7 @@ consts_code "of_int :: int \ rat" ("\rat'_of'_int") attach {* -fun rat_of_int 0 = (0, 0) - | rat_of_int i = (i, 1); +fun rat_of_int i = (i, 1); *} end diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/RealDef.thy --- a/src/HOL/RealDef.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/RealDef.thy Wed Jun 17 10:08:06 2009 +0200 @@ -1137,7 +1137,7 @@ begin definition - "random i = random i o\ (\r. Pair (valterm_ratreal r))" + "Quickcheck.random i = Quickcheck.random i o\ (\r. Pair (valterm_ratreal r))" instance .. @@ -1169,7 +1169,7 @@ val p' = p div g; val q' = q div g; val r = (if one_of [true, false] then p' else ~ p', - if p' = 0 then 0 else q') + if p' = 0 then 1 else q') in (r, fn () => term_of_real r) end; @@ -1181,8 +1181,7 @@ consts_code "of_int :: int \ real" ("\real'_of'_int") attach {* -fun real_of_int 0 = (0, 0) - | real_of_int i = (i, 1); +fun real_of_int i = (i, 1); *} end diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Set.thy --- a/src/HOL/Set.thy Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Set.thy Wed Jun 17 10:08:06 2009 +0200 @@ -23,8 +23,6 @@ Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers" Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers" Bex1 :: "'a set => ('a => bool) => bool" -- "bounded unique existential quantifiers" - Pow :: "'a set => 'a set set" -- "powerset" - image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) local @@ -215,9 +213,6 @@ supset_eq ("op \") and supset_eq ("(_/ \ _)" [50, 51] 50) -abbreviation - range :: "('a => 'b) => 'b set" where -- "of function" - "range f == f ` UNIV" subsubsection "Bounded quantifiers" @@ -408,9 +403,15 @@ end -defs - Pow_def: "Pow A == {B. B <= A}" - image_def: "f`A == {y. EX x:A. y = f(x)}" +definition Pow :: "'a set => 'a set set" where + Pow_def: "Pow A = {B. B \ A}" + +definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where + image_def: "f ` A = {y. EX x:A. y = f(x)}" + +abbreviation + range :: "('a => 'b) => 'b set" where -- "of function" + "range f == f ` UNIV" subsection {* Lemmas and proof tool setup *} diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/datatype_package/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML Wed Jun 17 10:08:06 2009 +0200 @@ -14,26 +14,29 @@ signature DATATYPE_ABS_PROOFS = sig - val prove_casedist_thms : string list -> - DatatypeAux.descr list -> (string * sort) list -> thm -> + type datatype_config = DatatypeAux.datatype_config + type descr = DatatypeAux.descr + type datatype_info = DatatypeAux.datatype_info + val prove_casedist_thms : datatype_config -> string list -> + descr list -> (string * sort) list -> thm -> attribute list -> theory -> thm list * theory - val prove_primrec_thms : bool -> string list -> - DatatypeAux.descr list -> (string * sort) list -> - DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list -> + val prove_primrec_thms : datatype_config -> string list -> + descr list -> (string * sort) list -> + datatype_info Symtab.table -> thm list list -> thm list list -> simpset -> thm -> theory -> (string list * thm list) * theory - val prove_case_thms : bool -> string list -> - DatatypeAux.descr list -> (string * sort) list -> + val prove_case_thms : datatype_config -> string list -> + descr list -> (string * sort) list -> string list -> thm list -> theory -> (thm list list * string list) * theory - val prove_split_thms : string list -> - DatatypeAux.descr list -> (string * sort) list -> + val prove_split_thms : datatype_config -> string list -> + descr list -> (string * sort) list -> thm list list -> thm list list -> thm list -> thm list list -> theory -> (thm * thm) list * theory - val prove_nchotomys : string list -> DatatypeAux.descr list -> + val prove_nchotomys : datatype_config -> string list -> descr list -> (string * sort) list -> thm list -> theory -> thm list * theory - val prove_weak_case_congs : string list -> DatatypeAux.descr list -> + val prove_weak_case_congs : string list -> descr list -> (string * sort) list -> theory -> thm list * theory val prove_case_congs : string list -> - DatatypeAux.descr list -> (string * sort) list -> + descr list -> (string * sort) list -> thm list -> thm list list -> theory -> thm list * theory end; @@ -44,9 +47,9 @@ (************************ case distinction theorems ***************************) -fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy = +fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy = let - val _ = message "Proving case distinction theorems ..."; + val _ = message config "Proving case distinction theorems ..."; val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; @@ -86,13 +89,13 @@ (*************************** primrec combinators ******************************) -fun prove_primrec_thms flat_names new_type_names descr sorts +fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy = let - val _ = message "Constructing primrec combinators ..."; + val _ = message config "Constructing primrec combinators ..."; val big_name = space_implode "_" new_type_names; - val thy0 = add_path flat_names big_name thy; + val thy0 = add_path (#flat_names config) big_name thy; val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; @@ -153,7 +156,7 @@ val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) = InductivePackage.add_inductive_global (serial_string ()) - {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, + {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false} (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) @@ -162,7 +165,7 @@ (* prove uniqueness and termination of primrec combinators *) - val _ = message "Proving termination and uniqueness of primrec functions ..."; + val _ = message config "Proving termination and uniqueness of primrec functions ..."; fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) = let @@ -242,13 +245,13 @@ Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) - ||> parent_path flat_names + ||> parent_path (#flat_names config) ||> Theory.checkpoint; (* prove characteristic equations for primrec combinators *) - val _ = message "Proving characteristic theorems for primrec combinators ..." + val _ = message config "Proving characteristic theorems for primrec combinators ..." val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t (fn _ => EVERY @@ -272,11 +275,11 @@ (***************************** case combinators *******************************) -fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy = +fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy = let - val _ = message "Proving characteristic theorems for case combinators ..."; + val _ = message config "Proving characteristic theorems for case combinators ..."; - val thy1 = add_path flat_names (space_implode "_" new_type_names) thy; + val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy; val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; @@ -338,7 +341,7 @@ thy2 |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms o Context.Theory - |> parent_path flat_names + |> parent_path (#flat_names config) |> store_thmss "cases" new_type_names case_thms |-> (fn thmss => pair (thmss, case_names)) end; @@ -346,12 +349,12 @@ (******************************* case splitting *******************************) -fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites +fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites casedist_thms case_thms thy = let - val _ = message "Proving equations for case splitting ..."; + val _ = message config "Proving equations for case splitting ..."; - val descr' = List.concat descr; + val descr' = flat descr; val recTs = get_rec_types descr' sorts; val newTs = Library.take (length (hd descr), recTs); @@ -395,9 +398,9 @@ (************************* additional theorems for TFL ************************) -fun prove_nchotomys new_type_names descr sorts casedist_thms thy = +fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy = let - val _ = message "Proving additional theorems for TFL ..."; + val _ = message config "Proving additional theorems for TFL ..."; fun prove_nchotomy (t, exhaustion) = let diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/datatype_package/datatype_aux.ML --- a/src/HOL/Tools/datatype_package/datatype_aux.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_aux.ML Wed Jun 17 10:08:06 2009 +0200 @@ -6,8 +6,9 @@ signature DATATYPE_AUX = sig - val quiet_mode : bool ref - val message : string -> unit + type datatype_config + val default_datatype_config : datatype_config + val message : datatype_config -> string -> unit val add_path : bool -> string -> theory -> theory val parent_path : bool -> theory -> theory @@ -67,8 +68,13 @@ structure DatatypeAux : DATATYPE_AUX = struct -val quiet_mode = ref false; -fun message s = if !quiet_mode then () else writeln s; +(* datatype option flags *) + +type datatype_config = { strict: bool, flat_names: bool, quiet: bool }; +val default_datatype_config : datatype_config = + { strict = true, flat_names = false, quiet = false }; +fun message ({ quiet, ...} : datatype_config) s = + if quiet then () else writeln s; fun add_path flat_names s = if flat_names then I else Sign.add_path s; fun parent_path flat_names = if flat_names then I else Sign.parent_path; diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/datatype_package/datatype_codegen.ML --- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Wed Jun 17 10:08:06 2009 +0200 @@ -426,7 +426,7 @@ (* register a datatype etc. *) -fun add_all_code dtcos thy = +fun add_all_code config dtcos thy = let val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos; val any_css = map2 (mk_constr_consts thy vs) dtcos coss; @@ -437,7 +437,7 @@ in if null css then thy else thy - |> tap (fn _ => DatatypeAux.message "Registering datatype for code generator ...") + |> tap (fn _ => DatatypeAux.message config "Registering datatype for code generator ...") |> fold Code.add_datatype css |> fold_rev Code.add_default_eqn case_rewrites |> fold Code.add_case certs diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/datatype_package/datatype_package.ML --- a/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 10:08:06 2009 +0200 @@ -6,6 +6,7 @@ signature DATATYPE_PACKAGE = sig + type datatype_config = DatatypeAux.datatype_config type datatype_info = DatatypeAux.datatype_info type descr = DatatypeAux.descr val get_datatypes : theory -> datatype_info Symtab.table @@ -24,39 +25,23 @@ val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option val read_typ: theory -> (typ list * (string * sort) list) * string -> typ list * (string * sort) list - val interpretation : (string list -> theory -> theory) -> theory -> theory - val rep_datatype : ({distinct : thm list list, - inject : thm list list, - exhaustion : thm list, - rec_thms : thm list, - case_thms : thm list list, - split_thms : (thm * thm) list, - induction : thm, - simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list - -> theory -> Proof.state; - val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state; - val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix * - (binding * typ list * mixfix) list) list -> theory -> - {distinct : thm list list, - inject : thm list list, - exhaustion : thm list, - rec_thms : thm list, - case_thms : thm list list, - split_thms : (thm * thm) list, - induction : thm, - simps : thm list} * theory - val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix * - (binding * string list * mixfix) list) list -> theory -> - {distinct : thm list list, - inject : thm list list, - exhaustion : thm list, - rec_thms : thm list, - case_thms : thm list list, - split_thms : (thm * thm) list, - induction : thm, - simps : thm list} * theory + val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory + type rules = {distinct : thm list list, + inject : thm list list, + exhaustion : thm list, + rec_thms : thm list, + case_thms : thm list list, + split_thms : (thm * thm) list, + induction : thm, + simps : thm list} + val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context) + -> string list option -> term list -> theory -> Proof.state; + val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state + val add_datatype : datatype_config -> string list -> (string list * binding * mixfix * + (binding * typ list * mixfix) list) list -> theory -> rules * theory + val add_datatype_cmd : string list -> (string list * binding * mixfix * + (binding * string list * mixfix) list) list -> theory -> rules * theory val setup: theory -> theory - val quiet_mode : bool ref val print_datatypes : theory -> unit end; @@ -65,8 +50,6 @@ open DatatypeAux; -val quiet_mode = quiet_mode; - (* theory data *) @@ -358,31 +341,41 @@ case_cong = case_cong, weak_case_cong = weak_case_cong}); -structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =); -val interpretation = DatatypeInterpretation.interpretation; +type rules = {distinct : thm list list, + inject : thm list list, + exhaustion : thm list, + rec_thms : thm list, + case_thms : thm list list, + split_thms : (thm * thm) list, + induction : thm, + simps : thm list} + +structure DatatypeInterpretation = InterpretationFun + (type T = datatype_config * string list val eq = eq_snd op =); +fun interpretation f = DatatypeInterpretation.interpretation (uncurry f); (******************* definitional introduction of datatypes *******************) -fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info +fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info case_names_induct case_names_exhausts thy = let - val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names); + val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names); val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |> - DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts + DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts types_syntax constr_syntax case_names_induct; - val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr + val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr sorts induct case_names_exhausts thy2; val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms - flat_names new_type_names descr sorts dt_info inject dist_rewrites + config new_type_names descr sorts dt_info inject dist_rewrites (Simplifier.theory_context thy3 dist_ss) induct thy3; val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms - flat_names new_type_names descr sorts reccomb_names rec_thms thy4; - val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names + config new_type_names descr sorts reccomb_names rec_thms thy4; + val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names descr sorts inject dist_rewrites casedist_thms case_thms thy6; - val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names + val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names descr sorts casedist_thms thy7; val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names descr sorts nchotomys case_thms thy8; @@ -406,7 +399,7 @@ |> add_cases_induct dt_infos induct |> Sign.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd - |> DatatypeInterpretation.data (map fst dt_infos); + |> DatatypeInterpretation.data (config, map fst dt_infos); in ({distinct = distinct, inject = inject, @@ -421,7 +414,7 @@ (*********************** declare existing type as datatype *********************) -fun prove_rep_datatype alt_names new_type_names descr sorts induct inject half_distinct thy = +fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy = let val ((_, [induct']), _) = Variable.importT_thms [induct] (Variable.thm_context induct); @@ -440,19 +433,19 @@ val (case_names_induct, case_names_exhausts) = (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames)); - val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names); + val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names); val (casedist_thms, thy2) = thy |> - DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct + DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct case_names_exhausts; val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms - false new_type_names [descr] sorts dt_info inject distinct + config new_type_names [descr] sorts dt_info inject distinct (Simplifier.theory_context thy2 dist_ss) induct thy2; - val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false - new_type_names [descr] sorts reccomb_names rec_thms thy3; + val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms + config new_type_names [descr] sorts reccomb_names rec_thms thy3; val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms - new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4; - val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names + config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4; + val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys config new_type_names [descr] sorts casedist_thms thy5; val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names [descr] sorts nchotomys case_thms thy6; @@ -482,7 +475,7 @@ |> Sign.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd - |> DatatypeInterpretation.data (map fst dt_infos); + |> DatatypeInterpretation.data (config, map fst dt_infos); in ({distinct = distinct, inject = inject, @@ -494,7 +487,7 @@ simps = simps}, thy11) end; -fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy = +fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy = let fun constr_of_term (Const (c, T)) = (c, T) | constr_of_term t = @@ -550,7 +543,7 @@ (*FIXME somehow dubious*) in ProofContext.theory_result - (prove_rep_datatype alt_names new_type_names descr vs induct injs half_distincts) + (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts) #-> after_qed end; in @@ -560,13 +553,13 @@ end; val rep_datatype = gen_rep_datatype Sign.cert_term; -val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I); +val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I); (******************************** add datatype ********************************) -fun gen_add_datatype prep_typ err flat_names new_type_names dts thy = +fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy = let val _ = Theory.requires thy "Datatype" "datatype definitions"; @@ -598,7 +591,7 @@ val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of [] => () | vs => error ("Extra type variables on rhs: " ^ commas vs)) - in (constrs @ [((if flat_names then Sign.full_name tmp_thy else + in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else Sign.full_name_path tmp_thy tname') (Binding.map_name (Syntax.const_name mx') cname), map (dtyp_of_typ new_dts) cargs')], @@ -626,7 +619,7 @@ val dt_info = get_datatypes thy; val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i; val _ = check_nonempty descr handle (exn as Datatype_Empty s) => - if err then error ("Nonemptiness check failed for datatype " ^ s) + if #strict config then error ("Nonemptiness check failed for datatype " ^ s) else raise exn; val descr' = flat descr; @@ -634,12 +627,12 @@ val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts); in add_datatype_def - flat_names new_type_names descr sorts types_syntax constr_syntax dt_info + (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info case_names_induct case_names_exhausts thy end; val add_datatype = gen_add_datatype cert_typ; -val add_datatype_cmd = gen_add_datatype read_typ true; +val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config; @@ -668,7 +661,7 @@ (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args; val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; - in snd o add_datatype_cmd false names specs end; + in snd o add_datatype_cmd names specs end; val _ = OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/datatype_package/datatype_realizer.ML --- a/src/HOL/Tools/datatype_package/datatype_realizer.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML Wed Jun 17 10:08:06 2009 +0200 @@ -7,7 +7,7 @@ signature DATATYPE_REALIZER = sig - val add_dt_realizers: string list -> theory -> theory + val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory val setup: theory -> theory end; @@ -213,10 +213,10 @@ (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy' end; -fun add_dt_realizers names thy = +fun add_dt_realizers config names thy = if ! Proofterm.proofs < 2 then thy else let - val _ = message "Adding realizers for induction and case analysis ..." + val _ = message config "Adding realizers for induction and case analysis ..." val infos = map (DatatypePackage.the_datatype thy) names; val info :: _ = infos; in diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/datatype_package/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML Wed Jun 17 10:08:06 2009 +0200 @@ -11,10 +11,13 @@ signature DATATYPE_REP_PROOFS = sig + type datatype_config = DatatypeAux.datatype_config + type descr = DatatypeAux.descr + type datatype_info = DatatypeAux.datatype_info val distinctness_limit : int Config.T val distinctness_limit_setup : theory -> theory - val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table -> - string list -> DatatypeAux.descr list -> (string * sort) list -> + val representation_proofs : datatype_config -> datatype_info Symtab.table -> + string list -> descr list -> (string * sort) list -> (binding * mixfix) list -> (binding * mixfix) list list -> attribute -> theory -> (thm list list * thm list list * thm list list * DatatypeAux.simproc_dist list * thm) * theory @@ -45,7 +48,7 @@ (******************************************************************************) -fun representation_proofs flat_names (dt_info : datatype_info Symtab.table) +fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table) new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = let val Datatype_thy = ThyInfo.the_theory "Datatype" thy; @@ -69,7 +72,7 @@ val descr' = flat descr; val big_name = space_implode "_" new_type_names; - val thy1 = add_path flat_names big_name thy; + val thy1 = add_path (#flat_names config) big_name thy; val big_rec_name = big_name ^ "_rep_set"; val rep_set_names' = (if length descr' = 1 then [big_rec_name] else @@ -147,7 +150,7 @@ (************** generate introduction rules for representing set **********) - val _ = message "Constructing representing sets ..."; + val _ = message config "Constructing representing sets ..."; (* make introduction rule for a single constructor *) @@ -181,7 +184,7 @@ val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) = InductivePackage.add_inductive_global (serial_string ()) - {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, + {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK, alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false} (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') [] @@ -190,7 +193,7 @@ (********************************* typedef ********************************) val (typedefs, thy3) = thy2 |> - parent_path flat_names |> + parent_path (#flat_names config) |> fold_map (fn ((((name, mx), tvs), c), name') => TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE @@ -199,7 +202,7 @@ (resolve_tac rep_intrs 1))) (types_syntax ~~ tyvars ~~ (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||> - add_path flat_names big_name; + add_path (#flat_names config) big_name; (*********************** definition of constructors ***********************) @@ -257,19 +260,19 @@ val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong); val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs)) - ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax) + ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax) in - (parent_path flat_names thy', defs', eqns @ [eqns'], + (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], rep_congs @ [cong'], dist_lemmas @ [dist]) end; val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs - ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []), + ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []), hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); (*********** isomorphisms for new types (introduced by typedef) ***********) - val _ = message "Proving isomorphism properties ..."; + val _ = message config "Proving isomorphism properties ..."; val newT_iso_axms = map (fn (_, td) => (collect_simp (#Abs_inverse td), #Rep_inverse td, @@ -358,7 +361,7 @@ in (thy', char_thms' @ char_thms) end; val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs - (add_path flat_names big_name thy4, []) (tl descr)); + (add_path (#flat_names config) big_name thy4, []) (tl descr)); (* prove isomorphism properties *) @@ -458,9 +461,9 @@ let val isoT = T --> Univ_elT in HOLogic.imp $ (Const (set_name, UnivT') $ mk_Free "x" Univ_elT i) $ - (if i < length newTs then Const ("True", HOLogic.boolT) + (if i < length newTs then HOLogic.true_const else HOLogic.mk_mem (mk_Free "x" Univ_elT i, - Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $ + Const (@{const_name image}, isoT --> HOLogic.mk_setT T --> UnivT) $ Const (iso_name, isoT) $ Const (@{const_name UNIV}, HOLogic.mk_setT T))) end; @@ -496,7 +499,7 @@ (******************* freeness theorems for constructors *******************) - val _ = message "Proving freeness of constructors ..."; + val _ = message config "Proving freeness of constructors ..."; (* prove theorem Rep_i (Constr_j ...) = Inj_j ... *) @@ -568,13 +571,13 @@ val ((constr_inject', distinct_thms'), thy6) = thy5 - |> parent_path flat_names + |> parent_path (#flat_names config) |> store_thmss "inject" new_type_names constr_inject ||>> store_thmss "distinct" new_type_names distinct_thms; (*************************** induction theorem ****************************) - val _ = message "Proving induction rule for datatypes ..."; + val _ = message config "Proving induction rule for datatypes ..."; val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @ (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded); diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Wed Jun 17 10:08:06 2009 +0200 @@ -191,9 +191,7 @@ |> safe_mk_meta_eq))) thy -val case_cong = fold add_case_cong - -val setup_case_cong = DatatypePackage.interpretation case_cong +val setup_case_cong = DatatypePackage.interpretation (K (fold add_case_cong)) (* setup *) diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/function_package/size.ML Wed Jun 17 10:08:06 2009 +0200 @@ -218,7 +218,7 @@ (new_type_names ~~ size_names)) thy'' end; -fun add_size_thms (new_type_names as name :: _) thy = +fun add_size_thms config (new_type_names as name :: _) thy = let val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name; val prefix = Long_Name.map_base_name (K (space_implode "_" diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Wed Jun 17 10:08:06 2009 +0200 @@ -307,8 +307,8 @@ val ((dummies, dt_info), thy2) = thy1 - |> add_dummies - (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts)) + |> add_dummies (DatatypePackage.add_datatype + { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts)) (map (pair false) dts) [] ||> Extraction.add_typeof_eqns_i ty_eqs ||> Extraction.add_realizes_eqns_i rlz_eqs; diff -r 752f23a37240 -r e5d4f7097c1b src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Wed Jun 17 10:08:06 2009 +0200 @@ -15,7 +15,7 @@ val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list -> string list -> string list * string list -> typ list * typ list -> string * (term list * (term * term) list) - val ensure_random_datatype: string list -> theory -> theory + val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory val eval_ref: (unit -> int -> seed -> term list option * seed) option ref val setup: theory -> theory end; @@ -49,7 +49,7 @@ mk_scomp (mk_termtyp ty) @{typ "term list option"} @{typ Random.seed} t (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit => term"}, t'))); fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty - (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i); + (Sign.mk_const thy (@{const_name Quickcheck.random}, [ty]) $ Bound i); in Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check)) end; fun compile_generator_expr thy t = @@ -98,7 +98,7 @@ val Ttm = mk_termifyT T; val typtm = mk_termifyT typ; fun mk_const c Ts = Const (c, Sign.const_instance thy (c, Ts)); - fun mk_random T = mk_const @{const_name random} [T]; + fun mk_random T = mk_const @{const_name Quickcheck.random} [T]; val size = @{term "j::code_numeral"}; val v = "x"; val t_v = Free (v, typtm); @@ -212,7 +212,7 @@ fun prove_eqs aux_simp proj_defs lthy = let val proj_simps = map (snd o snd) proj_defs; - fun tac { context = ctxt, ... } = + fun tac { context = ctxt, prems = _ } = ALLGOALS (simp_tac (HOL_ss addsimps proj_simps)) THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp]) THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv])); @@ -320,9 +320,9 @@ val prefix = space_implode "_" (random_auxN :: names); in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end; -fun mk_random_datatype descr vs tycos (names, auxnames) (Ts, Us) thy = +fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy = let - val _ = DatatypeAux.message "Creating quickcheck generators ..."; + val _ = DatatypeAux.message config "Creating quickcheck generators ..."; val i = @{term "i\code_numeral"}; val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k @@ -356,7 +356,7 @@ in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) end handle CLASS_ERROR => NONE; -fun ensure_random_datatype raw_tycos thy = +fun ensure_random_datatype config raw_tycos thy = let val pp = Syntax.pp_global thy; val algebra = Sign.classes_of thy; @@ -370,7 +370,7 @@ can (Sorts.mg_domain algebra tyco) @{sort random}) tycos; in if has_inst then thy else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs - of SOME constrain => mk_random_datatype descr + of SOME constrain => mk_random_datatype config descr (map constrain raw_vs) tycos (names, auxnames) ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy | NONE => thy diff -r 752f23a37240 -r e5d4f7097c1b src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Wed Jun 17 10:08:06 2009 +0200 @@ -122,7 +122,7 @@ val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], lessD = [], neqE = [], simpset = Simplifier.empty_ss, - number_of = (serial (), no_number_of) }; + number_of = (serial (), no_number_of) } : T; val extend = I; fun merge _ ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, diff -r 752f23a37240 -r e5d4f7097c1b src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Pure/Concurrent/future.ML Wed Jun 17 10:08:06 2009 +0200 @@ -301,19 +301,10 @@ val _ = scheduler_check "join check"; val _ = Multithreading.self_critical () andalso error "Cannot join future values within critical section"; - val _ = - (case thread_data () of - NONE => List.app join_wait xs (*alien thread -- refrain from contending for resources*) - | SOME (name, task) => (*proper task -- continue work*) - let - val pending = filter_out is_finished xs; - val deps = map task_of pending; - val _ = SYNCHRONIZED "join" (fn () => - (change queue (Task_Queue.depend deps task); notify_all ())); - val _ = List.app join_loop pending; - in () end); - + if is_some (thread_data ()) + then List.app join_loop xs (*proper task -- continue work*) + else List.app join_wait xs; (*alien thread -- refrain from contending for resources*) in map get_result xs end) (); end; diff -r 752f23a37240 -r e5d4f7097c1b src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Pure/Concurrent/task_queue.ML Wed Jun 17 10:08:06 2009 +0200 @@ -21,7 +21,6 @@ val is_empty: queue -> bool val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue val extend: task -> (bool -> bool) -> queue -> queue option - val depend: task list -> task -> queue -> queue val dequeue: queue -> (task * group * (bool -> bool) list) option * queue val interrupt: queue -> task -> unit val interrupt_external: queue -> string -> unit @@ -74,9 +73,6 @@ fun add_job task dep (jobs: jobs) = Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs; -fun add_job_acyclic task dep (jobs: jobs) = - Task_Graph.add_edge_acyclic (dep, task) jobs handle Task_Graph.UNDEF _ => jobs; - (* queue of grouped jobs *) @@ -95,22 +91,25 @@ (* enqueue *) -fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, ...}) = +fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, cache}) = let val task = new_task pri; val groups' = Inttab.cons_list (gid, task) groups; val jobs' = jobs |> Task_Graph.new_node (task, (group, Job [job])) |> fold (add_job task) deps; - in (task, make_queue groups' jobs' Unknown) end; + val cache' = + (case cache of + Result last => + if task_ord (last, task) = LESS + then cache else Unknown + | _ => Unknown); + in (task, make_queue groups' jobs' cache') end; fun extend task job (Queue {groups, jobs, cache}) = (case try (get_job jobs) task of SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) cache) | _ => NONE); -fun depend deps task (Queue {groups, jobs, ...}) = - make_queue groups (fold (add_job_acyclic task) deps jobs) Unknown; - (* dequeue *) @@ -168,11 +167,14 @@ val _ = List.app SimpleThread.interrupt running; in groups end; -fun finish task (Queue {groups, jobs, ...}) = +fun finish task (Queue {groups, jobs, cache}) = let val Group (gid, _) = get_group jobs task; val groups' = Inttab.remove_list (op =) (gid, task) groups; val jobs' = Task_Graph.del_node task jobs; - in make_queue groups' jobs' Unknown end; + val cache' = + if null (Task_Graph.imm_succs jobs task) then cache + else Unknown; + in make_queue groups' jobs' cache' end; end; diff -r 752f23a37240 -r e5d4f7097c1b src/Pure/General/scan.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/scan.scala Wed Jun 17 10:08:06 2009 +0200 @@ -0,0 +1,140 @@ +/* Title: Pure/General/scan.scala + Author: Makarius + +Efficient scanning of keywords. +*/ + +package isabelle + +import scala.util.parsing.combinator.RegexParsers + + +object Scan +{ + + /** Lexicon -- position tree **/ + + object Lexicon + { + private case class Tree(val branches: Map[Char, (String, Tree)]) + private val empty_tree = Tree(Map()) + + private def make(tree: Tree, max: Int): Lexicon = + new Lexicon { + override val main_tree = tree + override val max_entry = max + } + + val empty: Lexicon = new Lexicon + def apply(strs: String*): Lexicon = (empty /: strs) ((lex, str) => lex + str) + } + + class Lexicon extends scala.collection.immutable.Set[String] with RegexParsers + { + /* representation */ + + import Lexicon.Tree + val main_tree: Tree = Lexicon.empty_tree + val max_entry = -1 + + + /* auxiliary operations */ + + private def content(tree: Tree, result: List[String]): List[String] = + (result /: tree.branches.toList) ((res, entry) => + entry match { case (_, (s, tr)) => + if (s.isEmpty) content(tr, res) else content(tr, s :: res) }) + + private def lookup(str: CharSequence): Option[(Boolean, Tree)] = + { + val len = str.length + def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] = + { + if (i < len) { + tree.branches.get(str.charAt(i)) match { + case Some((s, tr)) => look(tr, !s.isEmpty, i + 1) + case None => None + } + } else Some(tip, tree) + } + look(main_tree, false, 0) + } + + def completions(str: CharSequence): List[String] = + { + (lookup(str) match { + case Some((true, tree)) => content(tree, List(str.toString)) + case Some((false, tree)) => content(tree, Nil) + case None => Nil + }).sort((s1, s2) => s1.length < s2.length || s1.length == s2.length && s1 <= s2) + } + + + /* Set methods */ + + override def stringPrefix = "Lexicon" + + override def isEmpty: Boolean = { max_entry < 0 } + + def size: Int = content(main_tree, Nil).length + def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements + + def contains(str: String): Boolean = + lookup(str) match { + case Some((tip, _)) => tip + case _ => false + } + + def +(str: String): Lexicon = + { + val len = str.length + def extend(tree: Tree, i: Int): Tree = + { + if (i < len) { + val c = str.charAt(i) + val end = (i + 1 == len) + tree.branches.get(c) match { + case Some((s, tr)) => + Tree(tree.branches + (c -> (if (end) str else s, extend(tr, i + 1)))) + case None => + Tree(tree.branches + (c -> (if (end) str else "", extend(Lexicon.empty_tree, i + 1)))) + } + } else tree + } + if (contains(str)) this + else Lexicon.make(extend(main_tree, 0), max_entry max str.length) + } + + def empty[A]: Set[A] = error("Undefined") + def -(str: String): Lexicon = error("Undefined") + + + /* RegexParsers methods */ + + override val whiteSpace = "".r + + def keyword: Parser[String] = new Parser[String] { + def apply(in: Input) = + { + val source = in.source + val offset = in.offset + val len = source.length - offset + + def scan(tree: Tree, text: String, i: Int): String = + { + if (i < len) { + tree.branches.get(source.charAt(offset + i)) match { + case Some((s, tr)) => scan(tr, if (s.isEmpty) text else s, i + 1) + case None => text + } + } else text + } + val text = scan(main_tree, "", 0) + if (text.isEmpty) Failure("keyword expected", in) + else Success(text, in.drop(text.length)) + } + }.named("keyword") + + } +} + diff -r 752f23a37240 -r e5d4f7097c1b src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Pure/General/symbol.scala Wed Jun 17 10:08:06 2009 +0200 @@ -118,6 +118,18 @@ yield read_decl(decl) + /* misc properties */ + + val names: Map[String, String] = { + val name = new Regex("""\\<([A-Za-z][A-Za-z0-9_']*)>""") + Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*) + } + + val abbrevs: Map[String, String] = Map(( + for ((sym, props) <- symbols if props.isDefinedAt("abbrev")) + yield (sym -> props("abbrev"))): _*) + + /* main recoder methods */ private val (decoder, encoder) = diff -r 752f23a37240 -r e5d4f7097c1b src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Pure/IsaMakefile Wed Jun 17 10:08:06 2009 +0200 @@ -115,9 +115,9 @@ ## Scala material SCALA_FILES = General/event_bus.scala General/markup.scala \ - General/position.scala General/swing.scala General/symbol.scala \ - General/xml.scala General/yxml.scala Isar/isar.scala \ - Isar/isar_document.scala Isar/outer_keyword.scala \ + General/position.scala General/scan.scala General/swing.scala \ + General/symbol.scala General/xml.scala General/yxml.scala \ + Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala \ System/cygwin.scala System/isabelle_process.scala \ System/isabelle_system.scala Thy/thy_header.scala \ Tools/isabelle_syntax.scala diff -r 752f23a37240 -r e5d4f7097c1b src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Pure/Isar/code.ML Wed Jun 17 10:08:06 2009 +0200 @@ -30,6 +30,7 @@ (*code equations*) val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool + val mk_eqn_warning: theory -> (string -> bool) -> thm -> (thm * bool) option val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option val assert_eqn: theory -> thm * bool -> thm * bool val assert_eqns_const: theory -> string @@ -72,6 +73,7 @@ val get_datatype_of_constr: theory -> string -> string option val default_typscheme: theory -> string -> (string * sort) list * typ val these_eqns: theory -> string -> (thm * bool) list + val all_eqns: theory -> (thm * bool) list val get_case_scheme: theory -> string -> (int * (int * string list)) option val is_undefined: theory -> string -> bool val print_codesetup: theory -> unit @@ -363,6 +365,7 @@ exception BAD_THM of string; fun bad_thm msg = raise BAD_THM msg; fun error_thm f thm = f thm handle BAD_THM msg => error msg; +fun warning_thm f thm = SOME (f thm) handle BAD_THM msg => (warning msg; NONE) fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; fun is_linear thm = @@ -445,6 +448,10 @@ fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy)); +fun mk_eqn_warning thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) + o warning_thm (gen_assert_eqn thy is_constr_head (K true)) + o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); + fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) o try_thm (gen_assert_eqn thy is_constr_head (K true)) o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); @@ -861,6 +868,11 @@ fun add_eqn thm thy = gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, true)) thy; +fun add_warning_eqn thm thy = + case mk_eqn_warning thy (is_constr thy) thm + of SOME eqn => gen_add_eqn false eqn thy + | NONE => thy; + fun add_default_eqn thm thy = case mk_eqn_liberal thy (is_constr thy) thm of SOME eqn => gen_add_eqn true eqn thy @@ -938,7 +950,7 @@ || Scan.succeed (mk_attribute add)) in TypeInterpretation.init - #> add_del_attribute ("", (add_eqn, del_eqn)) + #> add_del_attribute ("", (add_warning_eqn, del_eqn)) #> add_simple_attribute ("nbe", add_nbe_eqn) end)); @@ -947,6 +959,10 @@ |> (map o apfst) (Thm.transfer thy) |> burrow_fst (common_typ_eqns thy); +fun all_eqns thy = + Symtab.dest ((the_eqns o the_exec) thy) + |> maps (Lazy.force o snd o snd o fst o snd); + fun default_typscheme thy c = let fun the_const_typscheme c = (curry (typscheme thy) c o snd o dest_Const diff -r 752f23a37240 -r e5d4f7097c1b src/Pure/ML-Systems/multithreading_polyml.ML --- a/src/Pure/ML-Systems/multithreading_polyml.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML Wed Jun 17 10:08:06 2009 +0200 @@ -40,9 +40,16 @@ val max_threads = ref 1; +val tested_platform = + let val ml_platform = getenv "ML_PLATFORM" + in String.isSuffix "linux" ml_platform orelse String.isSuffix "darwin" ml_platform end; + fun max_threads_value () = - let val m = ! max_threads - in if m <= 0 then Int.max (Thread.numProcessors (), 1) else m end; + let val m = ! max_threads in + if m > 0 then m + else if not tested_platform then 1 + else Int.min (Int.max (Thread.numProcessors (), 1), 8) + end; fun enabled () = max_threads_value () > 1; diff -r 752f23a37240 -r e5d4f7097c1b src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Pure/pure_setup.ML Wed Jun 17 10:08:06 2009 +0200 @@ -4,15 +4,6 @@ Pure theory and ML toplevel setup. *) -(* ML toplevel use commands *) - -fun use name = Toplevel.program (fn () => ThyInfo.use name); -fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name); -fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name); -fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name); -fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name); - - (* the Pure theories *) val theory = ThyInfo.get_theory; @@ -49,6 +40,15 @@ else (); +(* ML toplevel use commands *) + +fun use name = Toplevel.program (fn () => ThyInfo.use name); +fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name); +fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name); +fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name); +fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name); + + (* misc *) val cd = File.cd o Path.explode; diff -r 752f23a37240 -r e5d4f7097c1b src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Tools/code/code_haskell.ML Wed Jun 17 10:08:06 2009 +0200 @@ -106,11 +106,9 @@ |> pr_bind tyvars thm BR ((NONE, SOME pat), ty) |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t]) val (ps, vars') = fold_map pr binds vars; - in - Pretty.block_enclose ( - str "(let {", - concat [str "}", str "in", pr_term tyvars thm vars' NOBR body, str ")"] - ) ps + in brackify_block fxy (str "let {") + ps + (concat [str "}", str "in", pr_term tyvars thm vars' NOBR body]) end | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) = let @@ -118,11 +116,10 @@ let val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars; in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end; - in - Pretty.block_enclose ( - concat [str "(case", pr_term tyvars thm vars NOBR t, str "of", str "{"], - str "})" - ) (map pr clauses) + in brackify_block fxy + (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"]) + (map pr clauses) + (str "}") end | pr_case tyvars thm vars fxy ((_, []), _) = (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]; diff -r 752f23a37240 -r e5d4f7097c1b src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Tools/code/code_ml.ML Wed Jun 17 10:08:06 2009 +0200 @@ -151,7 +151,7 @@ concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body] end; in - (Pretty.enclose "(" ")" o single o brackify fxy) ( + brackets ( str "case" :: pr_term is_closure thm vars NOBR t :: pr "of" clause @@ -441,8 +441,10 @@ |>> (fn p => concat [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"]) val (ps, vars') = fold_map pr binds vars; - fun mk_brack (p :: ps) = Pretty.block [str "(", p] :: ps; - in Pretty.chunks (mk_brack ps @| Pretty.block [pr_term is_closure thm vars' NOBR body, str ")"]) end + in + brackify_block fxy (Pretty.chunks ps) [] + (pr_term is_closure thm vars' NOBR body) + end | pr_case is_closure thm vars fxy (((t, ty), clause :: clauses), _) = let fun pr delim (pat, body) = @@ -450,7 +452,7 @@ val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars; in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end; in - (Pretty.enclose "(" ")" o single o brackify fxy) ( + brackets ( str "match" :: pr_term is_closure thm vars NOBR t :: pr "with" clause diff -r 752f23a37240 -r e5d4f7097c1b src/Tools/code/code_printer.ML --- a/src/Tools/code/code_printer.ML Wed Jun 17 10:07:25 2009 +0200 +++ b/src/Tools/code/code_printer.ML Wed Jun 17 10:08:06 2009 +0200 @@ -45,6 +45,7 @@ val APP: fixity val brackify: fixity -> Pretty.T list -> Pretty.T val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T + val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T type itype = Code_Thingol.itype type iterm = Code_Thingol.iterm @@ -175,6 +176,13 @@ fun brackify_infix infx fxy_ctxt = gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks; +fun brackify_block fxy_ctxt p1 ps p2 = + let val p = Pretty.block_enclose (p1, p2) ps + in if fixity BR fxy_ctxt + then Pretty.enclose "(" ")" [p] + else p + end; + (* generic syntax *)