# HG changeset patch # User haftmann # Date 1262956027 -3600 # Node ID 6cd289eca3e4bbc993f3d51e88f5265fdcca2a6e # Parent df93c72c0206746da2a2d3cb9f667d69e9d9eab5# Parent 19c1fd52d6c947d2b6b30349981a431485fe9eca merged diff -r 19c1fd52d6c9 -r 6cd289eca3e4 Admin/build --- a/Admin/build Fri Jan 08 12:25:15 2010 +0100 +++ b/Admin/build Fri Jan 08 14:07:07 2010 +0100 @@ -2,21 +2,12 @@ # # Administrative build for Isabelle source distribution. -## global environment - -#paranoia setting for sunbroy -PATH="/usr/local/dist/DIR/j2sdk1.5.0/bin:$PATH" - -PATH="/home/scala/current/bin:$PATH" -if [ -z "$SCALA_HOME" ]; then - export SCALA_HOME="$(dirname "$(dirname "$(type -p scalac)")")" -fi - - ## directory layout -ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" -ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" +if [ -z "$ISABELLE_HOME" ]; then + ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)" + ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle" +fi ## diagnostics @@ -35,7 +26,7 @@ all all modules below browser graph browser (requires jdk) doc documentation (requires latex and rail) - jars Scala/JVM components (requires scala) + jars Scala/JVM components (requires scala in SCALA_HOME) EOF exit 1 @@ -67,12 +58,9 @@ function build_browser () { - echo "###" - echo "### Building graph browser ..." - echo "###" - - cd "$ISABELLE_HOME/lib/browser" - make clean all || fail "Failed to build graph browser!" + pushd "$ISABELLE_HOME/lib/browser" >/dev/null + "$ISABELLE_TOOL" env ./build || fail "Failed!" + popd >/dev/null } @@ -95,14 +83,8 @@ function build_jars () { - echo "###" - echo "### Building Scala/JVM components ..." - echo "###" - - [ -z "$SCALA_HOME" ] && fail "Scala unavailable: unknown SCALA_HOME" - pushd "$ISABELLE_HOME/src/Pure" >/dev/null - "$ISABELLE_TOOL" make jars || fail "Failed to build isabelle-scala.jar" + "$ISABELLE_TOOL" env ./build-jars || fail "Failed!" popd >/dev/null } diff -r 19c1fd52d6c9 -r 6cd289eca3e4 Isabelle --- a/Isabelle Fri Jan 08 12:25:15 2010 +0100 +++ b/Isabelle Fri Jan 08 14:07:07 2010 +0100 @@ -16,12 +16,14 @@ source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2 unset ISABELLE_SETTINGS_PRESENT +unset ISABELLE_SITE_SETTINGS_PRESENT ## main +[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars + CLASSPATH="$(jvmpath "$CLASSPATH")" - exec "$ISABELLE_JAVA" \ "-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \ -jar "$(jvmpath "$ISABELLE_HOME/lib/classes/isabelle-scala.jar")" "$@" diff -r 19c1fd52d6c9 -r 6cd289eca3e4 lib/Tools/browser --- a/lib/Tools/browser Fri Jan 08 12:25:15 2010 +0100 +++ b/lib/Tools/browser Fri Jan 08 14:07:07 2010 +0100 @@ -60,6 +60,8 @@ ## main +[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" browser + classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar" if [ -z "$GRAPHFILE" ]; then diff -r 19c1fd52d6c9 -r 6cd289eca3e4 lib/Tools/scala --- a/lib/Tools/scala Fri Jan 08 12:25:15 2010 +0100 +++ b/lib/Tools/scala Fri Jan 08 14:07:07 2010 +0100 @@ -4,5 +4,7 @@ # # DESCRIPTION: invoke Scala within the Isabelle environment +[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars + CLASSPATH="$(jvmpath "$CLASSPATH")" exec "$ISABELLE_SCALA" "$@" diff -r 19c1fd52d6c9 -r 6cd289eca3e4 lib/browser/Makefile --- a/lib/browser/Makefile Fri Jan 08 12:25:15 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ - -DST=classes - -all: GraphBrowser.jar - -GraphBrowser.jar: GraphBrowser/*.java awtUtilities/*.java - mkdir -p $(DST) - javac -source 1.4 -d $(DST) GraphBrowser/GraphBrowser.java GraphBrowser/Console.java - jar cf GraphBrowser.jar -C $(DST) . - rm -rf $(DST) - -clean: - rm -f GraphBrowser/*.class - rm -f awtUtilities/*.class - rm -rf $(DST) - rm -f GraphBrowser.jar diff -r 19c1fd52d6c9 -r 6cd289eca3e4 lib/browser/build --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/browser/build Fri Jan 08 14:07:07 2010 +0100 @@ -0,0 +1,74 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# mk - build graph browser +# +# Requires proper Isabelle settings environment. + + +## diagnostics + +function fail() +{ + echo "$1" >&2 + exit 2 +} + +[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment" + + +## dependencies + +declare -a SOURCES=( + GraphBrowser/AWTFontMetrics.java + GraphBrowser/AbstractFontMetrics.java + GraphBrowser/Box.java + GraphBrowser/Console.java + GraphBrowser/DefaultFontMetrics.java + GraphBrowser/Directory.java + GraphBrowser/DummyVertex.java + GraphBrowser/Graph.java + GraphBrowser/GraphBrowser.java + GraphBrowser/GraphBrowserFrame.java + GraphBrowser/GraphView.java + GraphBrowser/NormalVertex.java + GraphBrowser/ParseError.java + GraphBrowser/Region.java + GraphBrowser/Spline.java + GraphBrowser/TreeBrowser.java + GraphBrowser/TreeNode.java + GraphBrowser/Vertex.java + awtUtilities/Border.java + awtUtilities/MessageDialog.java + awtUtilities/TextFrame.java +) + +TARGET="$ISABELLE_HOME/lib/browser/GraphBrowser.jar" + + +## main + +OUTDATED=false + +for SOURCE in "${SOURCES[@]}" +do + [ ! -e "$SOURCE" ] && fail "Missing source file: $SOURCE" + [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true +done + +if [ "$OUTDATED" = true ] +then + echo "###" + echo "### Building graph browser ..." + echo "###" + + rm -rf classes && mkdir classes + + javac -d classes -source 1.4 "${SOURCES[@]}" || \ + fail "Failed to compile sources" + jar cf "$(jvmpath "$TARGET")" -C classes . || + fail "Failed to produce $TARGET" + + rm -rf classes +fi diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Jan 08 14:07:07 2010 +0100 @@ -25,7 +25,7 @@ declare norm_scaleR[simp] lemma brouwer_compactness_lemma: - assumes "compact s" "continuous_on s f" "\ (\x\s. (f x = (0::real^'n::finite)))" + assumes "compact s" "continuous_on s f" "\ (\x\s. (f x = (0::real^'n)))" obtains d where "0 < d" "\x\s. d \ norm(f x)" proof(cases "s={}") case False have "continuous_on s (norm \ f)" by(rule continuous_on_intros continuous_on_norm assms(2))+ then obtain x where x:"x\s" "\y\s. (norm \ f) x \ (norm \ f) y" @@ -34,7 +34,7 @@ thus ?thesis apply(rule that) using x(2) unfolding o_def by auto qed(rule that[of 1], auto) lemma kuhn_labelling_lemma: - assumes "(\x::real^'n. P x \ P (f x))" "\x. P x \ (\i::'n. Q i \ 0 \ x$i \ x$i \ 1)" + assumes "(\x::real^_. P x \ P (f x))" "\x. P x \ (\i. Q i \ 0 \ x$i \ x$i \ 1)" shows "\l. (\x i. l x i \ (1::nat)) \ (\x i. P x \ Q i \ (x$i = 0) \ (l x i = 0)) \ (\x i. P x \ Q i \ (x$i = 1) \ (l x i = 1)) \ @@ -1161,7 +1161,7 @@ apply(drule_tac assms(1)[rule_format]) by auto } hence "?R 0 \ ?R 1" by auto thus ?case by auto qed qed -lemma brouwer_cube: fixes f::"real^'n::finite \ real^'n::finite" +lemma brouwer_cube: fixes f::"real^'n \ real^'n" assumes "continuous_on {0..1} f" "f ` {0..1} \ {0..1}" shows "\x\{0..1}. f x = x" apply(rule ccontr) proof- def n \ "CARD('n)" have n:"1 \ n" "0 < n" "n \ 0" unfolding n_def by auto @@ -1291,7 +1291,7 @@ subsection {* Retractions. *} -definition "retraction s t (r::real^'n::finite\real^'n) \ +definition "retraction s t (r::real^'n\real^'n) \ t \ s \ continuous_on s r \ (r ` s \ t) \ (\x\t. r x = x)" definition retract_of (infixl "retract'_of" 12) where @@ -1302,7 +1302,7 @@ subsection {*preservation of fixpoints under (more general notion of) retraction. *} -lemma invertible_fixpoint_property: fixes s::"(real^'n::finite) set" and t::"(real^'m::finite) set" +lemma invertible_fixpoint_property: fixes s::"(real^'n) set" and t::"(real^'m) set" assumes "continuous_on t i" "i ` t \ s" "continuous_on s r" "r ` s \ t" "\y\t. r (i y) = y" "\f. continuous_on s f \ f ` s \ s \ (\x\s. f x = x)" "continuous_on t g" "g ` t \ t" obtains y where "y\t" "g y = y" proof- @@ -1315,7 +1315,7 @@ unfolding assms(5)[rule_format,OF *] using assms(4) by auto qed lemma homeomorphic_fixpoint_property: - fixes s::"(real^'n::finite) set" and t::"(real^'m::finite) set" assumes "s homeomorphic t" + fixes s::"(real^'n) set" and t::"(real^'m) set" assumes "s homeomorphic t" shows "(\f. continuous_on s f \ f ` s \ s \ (\x\s. f x = x)) \ (\g. continuous_on t g \ g ` t \ t \ (\y\t. g y = y))" proof- guess r using assms[unfolded homeomorphic_def homeomorphism_def] .. then guess i .. @@ -1332,7 +1332,7 @@ subsection {*So the Brouwer theorem for any set with nonempty interior. *} -lemma brouwer_weak: fixes f::"real^'n::finite \ real^'n::finite" +lemma brouwer_weak: fixes f::"real^'n \ real^'n" assumes "compact s" "convex s" "interior s \ {}" "continuous_on s f" "f ` s \ s" obtains x where "x \ s" "f x = x" proof- have *:"interior {0..1::real^'n} \ {}" unfolding interior_closed_interval interval_eq_empty by auto @@ -1343,7 +1343,7 @@ subsection {* And in particular for a closed ball. *} -lemma brouwer_ball: fixes f::"real^'n::finite \ real^'n::finite" +lemma brouwer_ball: fixes f::"real^'n \ real^'n" assumes "0 < e" "continuous_on (cball a e) f" "f ` (cball a e) \ (cball a e)" obtains x where "x \ cball a e" "f x = x" using brouwer_weak[OF compact_cball convex_cball,of a e f] unfolding interior_cball ball_eq_empty @@ -1353,7 +1353,7 @@ rather involved HOMEOMORPHIC_CONVEX_COMPACT theorem, just using a scaling and translation to put the set inside the unit cube. *} -lemma brouwer: fixes f::"real^'n::finite \ real^'n::finite" +lemma brouwer: fixes f::"real^'n \ real^'n" assumes "compact s" "convex s" "s \ {}" "continuous_on s f" "f ` s \ s" obtains x where "x \ s" "f x = x" proof- have "\e>0. s \ cball 0 e" using compact_imp_bounded[OF assms(1)] unfolding bounded_pos @@ -1389,7 +1389,7 @@ subsection {*Bijections between intervals. *} -definition "interval_bij = (\ (a,b) (u,v) (x::real^'n::finite). +definition "interval_bij = (\ (a,b) (u,v) (x::real^'n). (\ i. u$i + (x$i - a$i) / (b$i - a$i) * (v$i - u$i))::real^'n)" lemma interval_bij_affine: @@ -1399,7 +1399,7 @@ by(auto simp add:group_simps field_simps add_divide_distrib[THEN sym]) lemma continuous_interval_bij: - "continuous (at x) (interval_bij (a,b::real^'n::finite) (u,v))" + "continuous (at x) (interval_bij (a,b::real^'n) (u,v))" unfolding interval_bij_affine apply(rule continuous_intros) apply(rule linear_continuous_at) unfolding linear_conv_bounded_linear[THEN sym] unfolding linear_def unfolding Cart_eq unfolding Cart_lambda_beta defer @@ -1413,7 +1413,7 @@ apply(cases "b=0") defer apply(rule divide_nonneg_pos) using assms by auto lemma in_interval_interval_bij: assumes "x \ {a..b}" "{u..v} \ {}" - shows "interval_bij (a,b) (u,v) x \ {u..v::real^'n::finite}" + shows "interval_bij (a,b) (u,v) x \ {u..v::real^'n}" unfolding interval_bij_def split_conv mem_interval Cart_lambda_beta proof(rule,rule) fix i::'n have "{a..b} \ {}" using assms by auto hence *:"a$i \ b$i" "u$i \ v$i" using assms(2) unfolding interval_eq_empty not_ex apply- @@ -1979,5 +1979,4 @@ ==> connected((:real^N) DIFF path_image p)`, SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *) -end - +end diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 08 14:07:07 2010 +0100 @@ -19,8 +19,6 @@ declare dot_lmult[simp] dot_rmult[simp] dot_lneg[simp] dot_rneg[simp] declare UNIV_1[simp] -term "(x::real^'n \ real) 0" - lemma dim1in[intro]:"Suc 0 \ {1::nat .. CARD(1)}" by auto lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta dest_vec1_def basis_component vector_uminus_component @@ -37,7 +35,7 @@ lemma nequals0I:"x\A \ A \ {}" by auto -lemma norm_not_0:"(x::real^'n::finite)\0 \ norm x \ 0" by auto +lemma norm_not_0:"(x::real^'n)\0 \ norm x \ 0" by auto lemma setsum_delta_notmem: assumes "x\s" shows "setsum (\y. if (y = x) then P x else Q y) s = setsum Q s" @@ -63,7 +61,7 @@ "(x \ {a<.. dest_vec1 a < dest_vec1 x \ dest_vec1 x < dest_vec1 b)" by(simp_all add: Cart_eq vector_less_def vector_le_def dest_vec1_def all_1) -lemma image_smult_interval:"(\x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} = +lemma image_smult_interval:"(\x. m *\<^sub>R (x::real^'n)) ` {a..b} = (if {a..b} = {} then {} else if 0 \ m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})" using image_affinity_interval[of m 0 a b] by auto @@ -92,7 +90,7 @@ by(auto simp add:norm_minus_commute) qed lemma norm_eqI:"x = y \ norm x = norm y" by auto -lemma norm_minus_eqI:"(x::real^'n::finite) = - y \ norm x = norm y" by auto +lemma norm_minus_eqI:"(x::real^'n) = - y \ norm x = norm y" by auto lemma Min_grI: assumes "finite A" "A \ {}" "\a\A. x < a" shows "x < Min A" unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto @@ -420,7 +418,7 @@ lemma convex_halfspace_gt: "convex {x. inner a x > b}" using convex_halfspace_lt[of "-a" "-b"] by auto -lemma convex_positive_orthant: "convex {x::real^'n::finite. (\i. 0 \ x$i)}" +lemma convex_positive_orthant: "convex {x::real^'n. (\i. 0 \ x$i)}" unfolding convex_def apply auto apply(erule_tac x=i in allE)+ apply(rule add_nonneg_nonneg) by(auto simp add: mult_nonneg_nonneg) @@ -1053,7 +1051,7 @@ 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" - "\x y z ::real^'n. x + y + z = 1 \ x = 1 - y - z" by (auto simp add: ring_simps) + "\x y z ::real^_. x + y + z = 1 \ x = 1 - y - z" by (auto simp add: ring_simps) show ?thesis unfolding convex_hull_finite[OF fin(1)] and Collect_def and convex_hull_finite_step[OF fin(2)] and * unfolding convex_hull_finite_step[OF fin(3)] apply(rule ext) apply simp apply auto apply(rule_tac x=va in exI) apply (rule_tac x="u c" in exI) apply simp @@ -1142,7 +1140,7 @@ thus ?thesis unfolding convex_def cone_def by auto qed -lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set" +lemma affine_dependent_biggerset: fixes s::"(real^'n) set" assumes "finite s" "card s \ CARD('n) + 2" shows "affine_dependent s" proof- @@ -1157,7 +1155,7 @@ apply(rule dependent_biggerset) by auto qed lemma affine_dependent_biggerset_general: - assumes "finite (s::(real^'n::finite) set)" "card s \ dim s + 2" + assumes "finite (s::(real^'n) set)" "card s \ dim s + 2" shows "affine_dependent s" proof- from assms(2) have "s \ {}" by auto @@ -1176,7 +1174,7 @@ subsection {* Caratheodory's theorem. *} -lemma convex_hull_caratheodory: fixes p::"(real^'n::finite) set" +lemma convex_hull_caratheodory: fixes p::"(real^'n) set" shows "convex hull p = {y. \s u. finite s \ s \ p \ card s \ CARD('n) + 1 \ (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" unfolding convex_hull_explicit expand_set_eq mem_Collect_eq @@ -1233,7 +1231,7 @@ qed auto lemma caratheodory: - "convex hull p = {x::real^'n::finite. \s. finite s \ s \ p \ + "convex hull p = {x::real^'n. \s. finite s \ s \ p \ card s \ CARD('n) + 1 \ x \ convex hull s}" unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof- fix x assume "x \ convex hull p" @@ -1340,7 +1338,7 @@ done qed -lemma compact_convex_hull: fixes s::"(real^'n::finite) set" +lemma compact_convex_hull: fixes s::"(real^'n) set" assumes "compact s" shows "compact(convex hull s)" proof(cases "s={}") case True thus ?thesis using compact_empty by simp @@ -1548,7 +1546,7 @@ subsection {* Closest point of a convex set is unique, with a continuous projection. *} definition - closest_point :: "(real ^ 'n::finite) set \ real ^ 'n \ real ^ 'n" where + closest_point :: "(real ^ 'n) set \ real ^ 'n \ real ^ 'n" where "closest_point s a = (SOME x. x \ s \ (\y\s. dist a x \ dist a y))" lemma closest_point_exists: @@ -1582,7 +1580,7 @@ lemma norm_le: "norm x \ norm y \ inner x x \ inner y y" unfolding norm_eq_sqrt_inner by simp -lemma closer_points_lemma: fixes y::"real^'n::finite" +lemma closer_points_lemma: fixes y::"real^'n" assumes "inner y z > 0" shows "\u>0. \v>0. v \ u \ norm(v *\<^sub>R z - y) < norm y" proof- have z:"inner z z > 0" unfolding inner_gt_zero_iff using assms by auto @@ -1593,7 +1591,7 @@ qed(rule divide_pos_pos, auto) qed lemma closer_point_lemma: - fixes x y z :: "real ^ 'n::finite" + fixes x y z :: "real ^ 'n" assumes "inner (y - x) (z - x) > 0" shows "\u>0. u \ 1 \ dist (x + u *\<^sub>R (z - x)) y < dist x y" proof- obtain u where "u>0" and u:"\v>0. v \ u \ norm (v *\<^sub>R (z - x) - (y - x)) < norm (y - x)" @@ -1720,10 +1718,10 @@ qed lemma separating_hyperplane_closed_0: - assumes "convex (s::(real^'n::finite) set)" "closed s" "0 \ s" + assumes "convex (s::(real^'n) set)" "closed s" "0 \ s" shows "\a b. a \ 0 \ 0 < b \ (\x\s. inner a x > b)" proof(cases "s={}") guess a using UNIV_witness[where 'a='n] .. - case True have "norm ((basis a)::real^'n::finite) = 1" + case True have "norm ((basis a)::real^'n) = 1" using norm_basis and dimindex_ge_1 by auto thus ?thesis apply(rule_tac x="basis a" in exI, rule_tac x=1 in exI) using True by auto next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms] @@ -1732,7 +1730,7 @@ subsection {* Now set-to-set for closed/compact sets. *} lemma separating_hyperplane_closed_compact: - assumes "convex (s::(real^'n::finite) set)" "closed s" "convex t" "compact t" "t \ {}" "s \ t = {}" + assumes "convex (s::(real^'n) set)" "closed s" "convex t" "compact t" "t \ {}" "s \ t = {}" shows "\a b. (\x\s. inner a x < b) \ (\x\t. inner a x > b)" proof(cases "s={}") case True @@ -1774,7 +1772,7 @@ subsection {* General case without assuming closure and getting non-strict separation. *} lemma separating_hyperplane_set_0: - assumes "convex s" "(0::real^'n::finite) \ s" + assumes "convex s" "(0::real^'n) \ s" shows "\a. a \ 0 \ (\x\s. 0 \ inner a x)" proof- let ?k = "\c. {x::real^'n. 0 \ inner c x}" have "frontier (cball 0 1) \ (\ (?k ` s)) \ {}" @@ -1796,7 +1794,7 @@ thus ?thesis apply(rule_tac x=x in exI) by(auto simp add: inner_commute) qed lemma separating_hyperplane_sets: - assumes "convex s" "convex (t::(real^'n::finite) set)" "s \ {}" "t \ {}" "s \ t = {}" + assumes "convex s" "convex (t::(real^'n) set)" "s \ {}" "t \ {}" "s \ t = {}" shows "\a b. a \ 0 \ (\x\s. inner a x \ b) \ (\x\t. inner a x \ b)" proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]] obtain a where "a\0" "\x\{x - y |x y. x \ t \ y \ s}. 0 \ inner a x" @@ -1903,7 +1901,7 @@ using assms(2) by assumption qed lemma radon_v_lemma: - assumes "finite s" "setsum f s = 0" "\x. g x = (0::real) \ f x = (0::real^'n)" + assumes "finite s" "setsum f s = 0" "\x. g x = (0::real) \ f x = (0::real^_)" shows "(setsum f {x\s. 0 < g x}) = - setsum f {x\s. g x < 0}" proof- have *:"\x. (if 0 < g x then f x else 0) + (if g x < 0 then f x else 0) = f x" using assms(3) by auto @@ -1957,7 +1955,7 @@ subsection {* Helly's theorem. *} -lemma helly_induct: fixes f::"(real^'n::finite) set set" +lemma helly_induct: fixes f::"(real^'n) set set" assumes "card f = n" "n \ CARD('n) + 1" "\s\f. convex s" "\t\f. card t = CARD('n) + 1 \ \ t \ {}" shows "\ f \ {}" @@ -1995,7 +1993,7 @@ thus ?thesis unfolding f using mp(3)[unfolded gh] by blast qed qed(insert dimindex_ge_1, auto) qed(auto) -lemma helly: fixes f::"(real^'n::finite) set set" +lemma helly: fixes f::"(real^'n) set set" assumes "card f \ CARD('n) + 1" "\s\f. convex s" "\t\f. card t = CARD('n) + 1 \ \ t \ {}" shows "\ f \{}" @@ -2064,9 +2062,9 @@ apply(rule,rule,rule ccontr) apply(rule u_max) by auto qed lemma starlike_compact_projective: - assumes "compact s" "cball (0::real^'n::finite) 1 \ s " + assumes "compact s" "cball (0::real^'n) 1 \ s " "\x\s. \u. 0 \ u \ u < 1 \ (u *\<^sub>R x) \ (s - frontier s )" - shows "s homeomorphic (cball (0::real^'n::finite) 1)" + shows "s homeomorphic (cball (0::real^'n) 1)" proof- have fs:"frontier s \ s" apply(rule frontier_subset_closed) using compact_imp_closed[OF assms(1)] by simp def pi \ "\x::real^'n. inverse (norm x) *\<^sub>R x" @@ -2202,7 +2200,7 @@ ultimately show ?thesis using injpi by auto qed qed qed auto qed -lemma homeomorphic_convex_compact_lemma: fixes s::"(real^'n::finite) set" +lemma homeomorphic_convex_compact_lemma: fixes s::"(real^'n) set" assumes "convex s" "compact s" "cball 0 1 \ s" shows "s homeomorphic (cball (0::real^'n) 1)" apply(rule starlike_compact_projective[OF assms(2-3)]) proof(rule,rule,rule,erule conjE) @@ -2220,9 +2218,9 @@ using as unfolding scaleR_scaleR by auto qed auto thus "u *\<^sub>R x \ s - frontier s" using frontier_def and interior_subset by auto qed -lemma homeomorphic_convex_compact_cball: fixes e::real and s::"(real^'n::finite) set" +lemma homeomorphic_convex_compact_cball: fixes e::real and s::"(real^'n) set" assumes "convex s" "compact s" "interior s \ {}" "0 < e" - shows "s homeomorphic (cball (b::real^'n::finite) e)" + shows "s homeomorphic (cball (b::real^'n) e)" proof- obtain a where "a\interior s" using assms(3) by auto then obtain d where "d>0" and d:"cball a d \ s" unfolding mem_interior_cball by auto let ?d = "inverse d" and ?n = "0::real^'n" @@ -2237,7 +2235,7 @@ apply(rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]]) using `d>0` `e>0` by(auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib) qed -lemma homeomorphic_convex_compact: fixes s::"(real^'n::finite) set" and t::"(real^'n) set" +lemma homeomorphic_convex_compact: fixes s::"(real^'n) set" and t::"(real^'n) set" assumes "convex s" "compact s" "interior s \ {}" "convex t" "compact t" "interior t \ {}" shows "s homeomorphic t" @@ -2319,7 +2317,7 @@ shows "is_interval s \ connected s" using is_interval_convex convex_connected by auto -lemma convex_interval: "convex {a .. b}" "convex {a<.. real^'n::finite" +lemma ivt_increasing_component_on_1: fixes f::"real^1 \ real^'n" assumes "dest_vec1 a \ dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \ y" "y \ (f b)$k" shows "\x\{a..b}. (f x)$k = y" proof- have "f a \ f ` {a..b}" "f b \ f ` {a..b}" apply(rule_tac[!] imageI) @@ -2362,20 +2360,20 @@ using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]] using assms by(auto intro!: imageI) qed -lemma ivt_increasing_component_1: fixes f::"real^1 \ real^'n::finite" +lemma ivt_increasing_component_1: fixes f::"real^1 \ real^'n" assumes "dest_vec1 a \ dest_vec1 b" "\x\{a .. b}. continuous (at x) f" "f a$k \ y" "y \ f b$k" shows "\x\{a..b}. (f x)$k = y" apply(rule ivt_increasing_component_on_1) using assms using continuous_at_imp_continuous_on by auto -lemma ivt_decreasing_component_on_1: fixes f::"real^1 \ real^'n::finite" +lemma ivt_decreasing_component_on_1: fixes f::"real^1 \ real^'n" assumes "dest_vec1 a \ dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \ y" "y \ (f a)$k" shows "\x\{a..b}. (f x)$k = y" apply(subst neg_equal_iff_equal[THEN sym]) unfolding vector_uminus_component[THEN sym] apply(rule ivt_increasing_component_on_1) using assms using continuous_on_neg by(auto simp add:vector_uminus_component) -lemma ivt_decreasing_component_1: fixes f::"real^1 \ real^'n::finite" +lemma ivt_decreasing_component_1: fixes f::"real^1 \ real^'n" assumes "dest_vec1 a \ dest_vec1 b" "\x\{a .. b}. continuous (at x) f" "f b$k \ y" "y \ f a$k" shows "\x\{a..b}. (f x)$k = y" apply(rule ivt_decreasing_component_on_1) using assms using continuous_at_imp_continuous_on by auto @@ -2396,7 +2394,7 @@ unfolding obt(2-3) using obt(1) and hull_subset[unfolded subset_eq, rule_format, of _ s] by auto qed lemma unit_interval_convex_hull: - "{0::real^'n::finite .. 1} = convex hull {x. \i. (x$i = 0) \ (x$i = 1)}" (is "?int = convex hull ?points") + "{0::real^'n .. 1} = convex hull {x. \i. (x$i = 0) \ (x$i = 1)}" (is "?int = convex hull ?points") proof- have 01:"{0,1} \ convex hull ?points" apply rule apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) by auto { fix n x assume "x\{0::real^'n .. 1}" "n \ CARD('n)" "card {i. x$i \ 0} \ n" hence "x\convex hull ?points" proof(induct n arbitrary: x) @@ -2432,8 +2430,8 @@ using Suc(2)[unfolded mem_interval, rule_format, of j] by(auto simp add:field_simps Cart_lambda_beta) hence "0 \ ?y j \ ?y j \ 1" by auto } moreover have "i\{j. x$j \ 0} - {j. ((\ j. ?y j)::real^'n) $ j \ 0}" using i01 by(auto simp add: Cart_lambda_beta) - hence "{j. x$j \ 0} \ {j. ((\ j. ?y j)::real^'n::finite) $ j \ 0}" by auto - hence **:"{j. ((\ j. ?y j)::real^'n::finite) $ j \ 0} \ {j. x$j \ 0}" apply - apply rule by(auto simp add: Cart_lambda_beta) + hence "{j. x$j \ 0} \ {j. ((\ j. ?y j)::real^'n) $ j \ 0}" by auto + hence **:"{j. ((\ j. ?y j)::real^'n) $ j \ 0} \ {j. x$j \ 0}" apply - apply rule by(auto simp add: Cart_lambda_beta) have "card {j. ((\ j. ?y j)::real^'n) $ j \ 0} \ n" using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format]) apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) defer apply(rule Suc(1)) @@ -2446,9 +2444,9 @@ subsection {* And this is a finite set of vertices. *} -lemma unit_cube_convex_hull: obtains s where "finite s" "{0 .. 1::real^'n::finite} = convex hull s" - apply(rule that[of "{x::real^'n::finite. \i. x$i=0 \ x$i=1}"]) - apply(rule finite_subset[of _ "(\s. (\ i. if i\s then 1::real else 0)::real^'n::finite) ` UNIV"]) +lemma unit_cube_convex_hull: obtains s where "finite s" "{0 .. 1::real^'n} = convex hull s" + apply(rule that[of "{x::real^'n. \i. x$i=0 \ x$i=1}"]) + apply(rule finite_subset[of _ "(\s. (\ i. if i\s then 1::real else 0)::real^'n) ` UNIV"]) prefer 3 apply(rule unit_interval_convex_hull) apply rule unfolding mem_Collect_eq proof- fix x::"real^'n" assume as:"\i. x $ i = 0 \ x $ i = 1" show "x \ (\s. \ i. if i \ s then 1 else 0) ` UNIV" apply(rule image_eqI[where x="{i. x$i = 1}"]) @@ -2457,7 +2455,7 @@ subsection {* Hence any cube (could do any nonempty interval). *} lemma cube_convex_hull: - assumes "0 < d" obtains s::"(real^'n::finite) set" where "finite s" "{x - (\ i. d) .. x + (\ i. d)} = convex hull s" proof- + assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "{x - (\ i. d) .. x + (\ i. d)} = convex hull s" proof- let ?d = "(\ i. d)::real^'n" have *:"{x - ?d .. x + ?d} = (\y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. 1}" apply(rule set_ext, rule) unfolding image_iff defer apply(erule bexE) proof- @@ -2554,7 +2552,7 @@ subsection {* Hence a convex function on an open set is continuous. *} lemma convex_on_continuous: - assumes "open (s::(real^'n::finite) set)" "convex_on s f" + assumes "open (s::(real^'n) set)" "convex_on s f" shows "continuous_on s f" unfolding continuous_on_eq_continuous_at[OF assms(1)] proof note dimge1 = dimindex_ge_1[where 'a='n] @@ -2599,15 +2597,15 @@ segment[a,b] is closed and segment(a,b) is open relative to affine hull. *) definition - midpoint :: "real ^ 'n::finite \ real ^ 'n \ real ^ 'n" where + midpoint :: "real ^ 'n \ real ^ 'n \ real ^ 'n" where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" definition - open_segment :: "real ^ 'n::finite \ real ^ 'n \ (real ^ 'n) set" where + open_segment :: "real ^ 'n \ real ^ 'n \ (real ^ 'n) set" where "open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \ u < 1}" definition - closed_segment :: "real ^ 'n::finite \ real ^ 'n \ (real ^ 'n) set" where + closed_segment :: "real ^ 'n \ real ^ 'n \ (real ^ 'n) set" where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \ u \ u \ 1}" definition "between = (\ (a,b). closed_segment a b)" @@ -2627,8 +2625,8 @@ "dist (midpoint a b) a = (dist a b) / 2" (is ?t3) "dist (midpoint a b) b = (dist a b) / 2" (is ?t4) proof- - have *: "\x y::real^'n::finite. 2 *\<^sub>R x = - y \ norm x = (norm y) / 2" unfolding equation_minus_iff by auto - have **:"\x y::real^'n::finite. 2 *\<^sub>R x = y \ norm x = (norm y) / 2" by auto + have *: "\x y::real^'n. 2 *\<^sub>R x = - y \ norm x = (norm y) / 2" unfolding equation_minus_iff by auto + have **:"\x y::real^'n. 2 *\<^sub>R x = y \ norm x = (norm y) / 2" by auto note scaleR_right_distrib [simp] show ?t1 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector) show ?t2 unfolding midpoint_def dist_norm apply (rule *) by(auto,vector) @@ -2636,7 +2634,7 @@ show ?t4 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector) qed lemma midpoint_eq_endpoint: - "midpoint a b = a \ a = (b::real^'n::finite)" + "midpoint a b = a \ a = (b::real^'n)" "midpoint a b = b \ a = b" unfolding dist_eq_0_iff[where 'a="real^'n", THEN sym] dist_midpoint by auto @@ -2681,7 +2679,7 @@ lemma between_mem_segment: "between (a,b) x \ x \ closed_segment a b" unfolding between_def mem_def by auto -lemma between:"between (a,b) (x::real^'n::finite) \ dist a b = (dist a x) + (dist x b)" +lemma between:"between (a,b) (x::real^'n) \ dist a b = (dist a x) + (dist x b)" proof(cases "a = b") case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric] by(auto simp add:segment_refl dist_commute) next @@ -2708,7 +2706,7 @@ finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $ i" by auto qed(insert Fal2, auto) qed qed -lemma between_midpoint: fixes a::"real^'n::finite" shows +lemma between_midpoint: fixes a::"real^'n" shows "between (a,b) (midpoint a b)" (is ?t1) "between (b,a) (midpoint a b)" (is ?t2) proof- have *:"\x y z. x = (1/2::real) *\<^sub>R z \ y = (1/2) *\<^sub>R z \ norm z = norm x + norm y" by auto @@ -2778,7 +2776,7 @@ lemma std_simplex: "convex hull (insert 0 { basis i | i. i\UNIV}) = - {x::real^'n::finite . (\i. 0 \ x$i) \ setsum (\i. x$i) UNIV \ 1 }" (is "convex hull (insert 0 ?p) = ?s") + {x::real^'n . (\i. 0 \ x$i) \ setsum (\i. x$i) UNIV \ 1 }" (is "convex hull (insert 0 ?p) = ?s") proof- let ?D = "UNIV::'n set" have "0\?p" by(auto simp add: basis_nonzero) have "{(basis i)::real^'n |i. i \ ?D} = basis ` ?D" by auto @@ -2798,7 +2796,7 @@ lemma interior_std_simplex: "interior (convex hull (insert 0 { basis i| i. i\UNIV})) = - {x::real^'n::finite. (\i. 0 < x$i) \ setsum (\i. x$i) UNIV < 1 }" + {x::real^'n. (\i. 0 < x$i) \ setsum (\i. x$i) UNIV < 1 }" apply(rule set_ext) unfolding mem_interior std_simplex unfolding subset_eq mem_Collect_eq Ball_def mem_ball unfolding Ball_def[symmetric] apply rule apply(erule exE, (erule conjE)+) defer apply(erule conjE) proof- fix x::"real^'n" and e assume "0xa. dist x xa < e \ (\x. 0 \ xa $ x) \ setsum (op $ xa) UNIV \ 1" @@ -2815,7 +2813,7 @@ also have "\ \ 1" using ** apply(drule_tac as[rule_format]) by auto finally show "setsum (op $ x) UNIV < 1" by auto qed next - fix x::"real^'n::finite" assume as:"\i. 0 < x $ i" "setsum (op $ x) UNIV < 1" + fix x::"real^'n" assume as:"\i. 0 < x $ i" "setsum (op $ x) UNIV < 1" guess a using UNIV_witness[where 'a='b] .. let ?d = "(1 - setsum (op $ x) UNIV) / real (CARD('n))" have "Min ((op $ x) ` UNIV) > 0" apply(rule Min_grI) using as(1) dimindex_ge_1 by auto @@ -2834,7 +2832,7 @@ thus "0 \ y$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by(auto simp add: vector_component_simps) qed auto qed auto qed -lemma interior_std_simplex_nonempty: obtains a::"real^'n::finite" where +lemma interior_std_simplex_nonempty: obtains a::"real^'n" where "a \ interior(convex hull (insert 0 {basis i | i . i \ UNIV}))" proof- let ?D = "UNIV::'n set" let ?a = "setsum (\b::real^'n. inverse (2 * real CARD('n)) *\<^sub>R b) {(basis i) | i. i \ ?D}" have *:"{basis i :: real ^ 'n | i. i \ ?D} = basis ` ?D" by auto @@ -2851,7 +2849,7 @@ subsection {* Paths. *} -definition "path (g::real^1 \ real^'n::finite) \ continuous_on {0 .. 1} g" +definition "path (g::real^1 \ real^'n) \ continuous_on {0 .. 1} g" definition "pathstart (g::real^1 \ real^'n) = g 0" @@ -3140,7 +3138,7 @@ subsection {* Special case of straight-line paths. *} definition - linepath :: "real ^ 'n::finite \ real ^ 'n \ real ^ 1 \ real ^ 'n" where + linepath :: "real ^ 'n \ real ^ 'n \ real ^ 1 \ real ^ 'n" where "linepath a b = (\x. (1 - dest_vec1 x) *\<^sub>R a + dest_vec1 x *\<^sub>R b)" lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a" @@ -3325,7 +3323,7 @@ subsection {* sphere is path-connected. *} lemma path_connected_punctured_universe: - assumes "2 \ CARD('n::finite)" shows "path_connected((UNIV::(real^'n::finite) set) - {a})" proof- + assumes "2 \ CARD('n::finite)" shows "path_connected((UNIV::(real^'n) set) - {a})" proof- obtain \ where \:"bij_betw \ {1..CARD('n)} (UNIV::'n set)" using ex_bij_betw_nat_finite_1[OF finite_UNIV] by auto let ?U = "UNIV::(real^'n) set" let ?u = "?U - {0}" let ?basis = "\k. basis (\ k)" @@ -3368,7 +3366,7 @@ show ?thesis unfolding * apply(rule path_connected_continuous_image) apply(rule continuous_on_intros)+ unfolding ** apply(rule lem[THEN bspec[where x="CARD('n)"], unfolded ***]) using assms by auto qed -lemma path_connected_sphere: assumes "2 \ CARD('n::finite)" shows "path_connected {x::real^'n::finite. norm(x - a) = r}" proof(cases "r\0") +lemma path_connected_sphere: assumes "2 \ CARD('n::finite)" shows "path_connected {x::real^'n. norm(x - a) = r}" proof(cases "r\0") case True thus ?thesis proof(cases "r=0") case False hence "{x::real^'n. norm(x - a) = r} = {}" using True by auto thus ?thesis using path_connected_empty by auto @@ -3383,7 +3381,7 @@ thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms] by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed -lemma connected_sphere: "2 \ CARD('n) \ connected {x::real^'n::finite. norm(x - a) = r}" +lemma connected_sphere: "2 \ CARD('n) \ connected {x::real^'n. norm(x - a) = r}" using path_connected_sphere path_connected_imp_connected by auto - + end diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Jan 08 14:07:07 2010 +0100 @@ -122,7 +122,7 @@ "((f \ dest_vec1) has_derivative (f' \ dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)" using has_derivative_within_dest_vec1[where s=UNIV] by(auto simp add:within_UNIV) -lemma derivative_is_linear: fixes f::"real^'a::finite \ real^'b::finite" shows +lemma derivative_is_linear: fixes f::"real^'a \ real^'b" shows "(f has_derivative f') net \ linear f'" unfolding has_derivative_def and linear_conv_bounded_linear by auto @@ -194,7 +194,7 @@ subsection {* somewhat different results for derivative of scalar multiplier. *} -lemma has_derivative_vmul_component: fixes c::"real^'a::finite \ real^'b::finite" and v::"real^'c::finite" +lemma has_derivative_vmul_component: fixes c::"real^'a \ real^'b" and v::"real^'c" assumes "(c has_derivative c') net" shows "((\x. c(x)$k *\<^sub>R v) has_derivative (\x. (c' x)$k *\<^sub>R v)) net" proof- have *:"\y. (c y $ k *\<^sub>R v - (c (netlimit net) $ k *\<^sub>R v + c' (y - netlimit net) $ k *\<^sub>R v)) = @@ -217,14 +217,14 @@ qed qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed -lemma has_derivative_vmul_within: fixes c::"real \ real" and v::"real^'a::finite" +lemma has_derivative_vmul_within: fixes c::"real \ real" and v::"real^'a" assumes "(c has_derivative c') (at x within s)" shows "((\x. (c x) *\<^sub>R v) has_derivative (\x. (c' x) *\<^sub>R v)) (at x within s)" proof- have *:"\c. (\x. (vec1 \ c \ dest_vec1) x $ 1 *\<^sub>R v) = (\x. (c x) *\<^sub>R v) \ dest_vec1" unfolding o_def by auto show ?thesis using has_derivative_vmul_component[of "vec1 \ c \ dest_vec1" "vec1 \ c' \ dest_vec1" "at (vec1 x) within vec1 ` s" 1 v] unfolding * and has_derivative_within_vec1_dest_vec1 unfolding has_derivative_within_dest_vec1 using assms by auto qed -lemma has_derivative_vmul_at: fixes c::"real \ real" and v::"real^'a::finite" +lemma has_derivative_vmul_at: fixes c::"real \ real" and v::"real^'a" assumes "(c has_derivative c') (at x)" shows "((\x. (c x) *\<^sub>R v) has_derivative (\x. (c' x) *\<^sub>R v)) (at x)" using has_derivative_vmul_within[where s=UNIV] and assms by(auto simp add: within_UNIV) @@ -281,7 +281,7 @@ "f differentiable (at a within s) \ (f differentiable (at a))" unfolding differentiable_def has_derivative_within_open[OF assms] by auto -lemma differentiable_at_imp_differentiable_on: "(\x\(s::(real^'n::finite) set). f differentiable at x) \ f differentiable_on s" +lemma differentiable_at_imp_differentiable_on: "(\x\(s::(real^'n) set). f differentiable at x) \ f differentiable_on s" unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI) lemma differentiable_on_eq_differentiable_at: "open s \ (f differentiable_on s \ (\x\s. f differentiable at x))" @@ -305,13 +305,13 @@ "f differentiable net \ (f has_derivative (frechet_derivative f net)) net" unfolding frechet_derivative_def differentiable_def and some_eq_ex[of "\ f' . (f has_derivative f') net"] .. -lemma linear_frechet_derivative: fixes f::"real^'a::finite \ real^'b::finite" +lemma linear_frechet_derivative: fixes f::"real^'a \ real^'b" shows "f differentiable net \ linear(frechet_derivative f net)" unfolding frechet_derivative_works has_derivative_def unfolding linear_conv_bounded_linear by auto definition "jacobian f net = matrix(frechet_derivative f net)" -lemma jacobian_works: "(f::(real^'a::finite) \ (real^'b::finite)) differentiable net \ (f has_derivative (\h. (jacobian f net) *v h)) net" +lemma jacobian_works: "(f::(real^'a) \ (real^'b)) differentiable net \ (f has_derivative (\h. (jacobian f net) *v h)) net" apply rule unfolding jacobian_def apply(simp only: matrix_works[OF linear_frechet_derivative]) defer apply(rule differentiableI) apply assumption unfolding frechet_derivative_works by assumption @@ -387,7 +387,7 @@ apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:group_simps) qed auto qed lemma has_derivative_at_alt: - "(f has_derivative f') (at (x::real^'n::finite)) \ bounded_linear f' \ + "(f has_derivative f') (at (x::real^'n)) \ bounded_linear f' \ (\e>0. \d>0. \y. norm(y - x) < d \ norm(f y - f x - f'(y - x)) \ e * norm(y - x))" using has_derivative_within_alt[where s=UNIV] unfolding within_UNIV by auto @@ -474,13 +474,13 @@ unfolding differentiable_def apply(erule exE)+ apply(rule_tac x="\z. f' z - f'a z" in exI) apply(rule has_derivative_sub) by auto -lemma differentiable_setsum: fixes f::"'a \ (real^'n::finite \real^'n)" +lemma differentiable_setsum: fixes f::"'a \ (real^'n \real^'n)" assumes "finite s" "\a\s. (f a) differentiable net" shows "(\x. setsum (\a. f a x) s) differentiable net" proof- guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] .. thus ?thesis unfolding differentiable_def apply- apply(rule,rule has_derivative_setsum[where f'=f'],rule assms(1)) by auto qed -lemma differentiable_setsum_numseg: fixes f::"_ \ (real^'n::finite \real^'n)" +lemma differentiable_setsum_numseg: fixes f::"_ \ (real^'n \real^'n)" shows "\i. m \ i \ i \ n \ (f i) differentiable net \ (\x. setsum (\a. f a x) {m::nat..n}) differentiable net" apply(rule differentiable_setsum) using finite_atLeastAtMost[of n m] by auto @@ -498,7 +498,7 @@ (* The general result is a bit messy because we need approachability of the *) (* limit point from any direction. But OK for nontrivial intervals etc. *} -lemma frechet_derivative_unique_within: fixes f::"real^'a::finite \ real^'b::finite" +lemma frechet_derivative_unique_within: fixes f::"real^'a \ real^'b" assumes "(f has_derivative f') (at x within s)" "(f has_derivative f'') (at x within s)" "(\i::'a::finite. \e>0. \d. 0 < abs(d) \ abs(d) < e \ (x + d *\<^sub>R basis i) \ s)" shows "f' = f''" proof- note as = assms(1,2)[unfolded has_derivative_def] @@ -523,7 +523,7 @@ finally show False using c using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] using norm_basis[of i] unfolding vector_dist_norm unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib by auto qed qed -lemma frechet_derivative_unique_at: fixes f::"real^'a::finite \ real^'b::finite" +lemma frechet_derivative_unique_at: fixes f::"real^'a \ real^'b" shows "(f has_derivative f') (at x) \ (f has_derivative f'') (at x) \ f' = f''" apply(rule frechet_derivative_unique_within[of f f' x UNIV f'']) unfolding within_UNIV apply(assumption)+ apply(rule,rule,rule) apply(rule_tac x="e/2" in exI) by auto @@ -531,7 +531,7 @@ lemma "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def unfolding continuous_at Lim_at unfolding dist_nz by auto -lemma frechet_derivative_unique_within_closed_interval: fixes f::"real^'a::finite \ real^'b::finite" +lemma frechet_derivative_unique_within_closed_interval: fixes f::"real^'a \ real^'b" assumes "\i. a$i < b$i" "x \ {a..b}" (is "x\?I") and "(f has_derivative f' ) (at x within {a..b})" and "(f has_derivative f'') (at x within {a..b})" @@ -552,7 +552,7 @@ using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2) unfolding mem_interval by(auto simp add:field_simps) qed qed -lemma frechet_derivative_unique_within_open_interval: fixes f::"real^'a::finite \ real^'b::finite" +lemma frechet_derivative_unique_within_open_interval: fixes f::"real^'a \ real^'b" assumes "x \ {a<..0` and assms(1) unfolding mem_interval by(auto simp add:field_simps) qed -lemma frechet_derivative_at: fixes f::"real^'a::finite \ real^'b::finite" +lemma frechet_derivative_at: fixes f::"real^'a \ real^'b" shows "(f has_derivative f') (at x) \ (f' = frechet_derivative f (at x))" apply(rule frechet_derivative_unique_at[of f],assumption) unfolding frechet_derivative_works[THEN sym] using differentiable_def by auto -lemma frechet_derivative_within_closed_interval: fixes f::"real^'a::finite \ real^'b::finite" +lemma frechet_derivative_within_closed_interval: fixes f::"real^'a \ real^'b" assumes "\i. a$i < b$i" "x \ {a..b}" "(f has_derivative f') (at x within {a.. b})" shows "frechet_derivative f (at x within {a.. b}) = f'" apply(rule frechet_derivative_unique_within_closed_interval[where f=f]) @@ -583,7 +583,7 @@ subsection {* Component of the differential must be zero if it exists at a local *) (* maximum or minimum for that corresponding component. *} -lemma differential_zero_maxmin_component: fixes f::"real^'a::finite \ real^'b::finite" +lemma differential_zero_maxmin_component: fixes f::"real^'a \ real^'b" assumes "0 < e" "((\y \ ball x e. (f y)$k \ (f x)$k) \ (\y\ball x e. (f x)$k \ (f y)$k))" "f differentiable (at x)" shows "jacobian f (at x) $ k = 0" proof(rule ccontr) def D \ "jacobian f (at x)" assume "jacobian f (at x) $ k \ 0" @@ -611,7 +611,7 @@ subsection {* In particular if we have a mapping into R^1. *} -lemma differential_zero_maxmin: fixes f::"real^'a::finite \ real" +lemma differential_zero_maxmin: fixes f::"real^'a \ real" assumes "x \ s" "open s" "(f has_derivative f') (at x)" "(\y\s. f y \ f x) \ (\y\s. f x \ f y)" shows "f' = (\v. 0)" proof- @@ -688,10 +688,10 @@ subsection {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *} -lemma inner_eq_dot: fixes a::"real^'n::finite" +lemma inner_eq_dot: fixes a::"real^'n" shows "a \ b = inner a b" unfolding inner_vector_def dot_def by auto -lemma mvt_general: fixes f::"real\real^'n::finite" +lemma mvt_general: fixes f::"real\real^'n" assumes "ax\{a<..x\{a<.. norm(f'(x) (b - a))" proof- have "\x\{a<.. (f b - f a) \ f) b - (op \ (f b - f a) \ f) a = (f b - f a) \ f' x (b - a)" @@ -708,7 +708,7 @@ subsection {* Still more general bound theorem. *} -lemma differentiable_bound: fixes f::"real^'a::finite \ real^'b::finite" +lemma differentiable_bound: fixes f::"real^'a \ real^'b" assumes "convex s" "\x\s. (f has_derivative f'(x)) (at x within s)" "\x\s. onorm(f' x) \ B" and x:"x\s" and y:"y\s" shows "norm(f x - f y) \ B * norm(x - y)" proof- let ?p = "\u. x + u *\<^sub>R (y - x)" @@ -771,7 +771,7 @@ subsection {* Differentiability of inverse function (most basic form). *} -lemma has_derivative_inverse_basic: fixes f::"real^'b::finite \ real^'c::finite" +lemma has_derivative_inverse_basic: fixes f::"real^'b \ real^'c" assumes "(f has_derivative f') (at (g y))" "bounded_linear g'" "g' \ f' = id" "continuous (at y) g" "open t" "y \ t" "\z\t. f(g z) = z" shows "(g has_derivative g') (at y)" proof- @@ -815,7 +815,7 @@ subsection {* Simply rewrite that based on the domain point x. *} -lemma has_derivative_inverse_basic_x: fixes f::"real^'b::finite \ real^'c::finite" +lemma has_derivative_inverse_basic_x: fixes f::"real^'b \ real^'c" assumes "(f has_derivative f') (at x)" "bounded_linear g'" "g' o f' = id" "continuous (at (f x)) g" "g(f x) = x" "open t" "f x \ t" "\y\t. f(g y) = y" shows "(g has_derivative g') (at (f(x)))" @@ -823,7 +823,7 @@ subsection {* This is the version in Dieudonne', assuming continuity of f and g. *} -lemma has_derivative_inverse_dieudonne: fixes f::"real^'a::finite \ real^'b::finite" +lemma has_derivative_inverse_dieudonne: fixes f::"real^'a \ real^'b" assumes "open s" "open (f ` s)" "continuous_on s f" "continuous_on (f ` s) g" "\x\s. g(f x) = x" (**) "x\s" "(f has_derivative f') (at x)" "bounded_linear g'" "g' o f' = id" shows "(g has_derivative g') (at (f x))" @@ -832,7 +832,7 @@ subsection {* Here's the simplest way of not assuming much about g. *} -lemma has_derivative_inverse: fixes f::"real^'a::finite \ real^'b::finite" +lemma has_derivative_inverse: fixes f::"real^'a \ real^'b" assumes "compact s" "x \ s" "f x \ interior(f ` s)" "continuous_on s f" "\y\s. g(f y) = y" "(f has_derivative f') (at x)" "bounded_linear g'" "g' \ f' = id" shows "(g has_derivative g') (at (f x))" proof- @@ -845,7 +845,7 @@ subsection {* Proving surjectivity via Brouwer fixpoint theorem. *} -lemma brouwer_surjective: fixes f::"real^'n::finite \ real^'n" +lemma brouwer_surjective: fixes f::"real^'n \ real^'n" assumes "compact t" "convex t" "t \ {}" "continuous_on t f" "\x\s. \y\t. x + (y - f y) \ t" "x\s" shows "\y\t. f y = x" proof- @@ -853,7 +853,7 @@ show ?thesis unfolding * apply(rule brouwer[OF assms(1-3), of "\y. x + (y - f y)"]) apply(rule continuous_on_intros assms)+ using assms(4-6) by auto qed -lemma brouwer_surjective_cball: fixes f::"real^'n::finite \ real^'n" +lemma brouwer_surjective_cball: fixes f::"real^'n \ real^'n" assumes "0 < e" "continuous_on (cball a e) f" "\x\s. \y\cball a e. x + (y - f y) \ cball a e" "x\s" shows "\y\cball a e. f y = x" apply(rule brouwer_surjective) apply(rule compact_cball convex_cball)+ @@ -861,7 +861,7 @@ text {* See Sussmann: "Multidifferential calculus", Theorem 2.1.1 *} -lemma sussmann_open_mapping: fixes f::"real^'a::finite \ real^'b::finite" +lemma sussmann_open_mapping: fixes f::"real^'a \ real^'b" assumes "open s" "continuous_on s f" "x \ s" "(f has_derivative f') (at x)" "bounded_linear g'" "f' \ g' = id" (**) "t \ s" "x \ interior t" @@ -918,7 +918,7 @@ (* We could put f' o g = I but this happens to fit with the minimal linear *) (* algebra theory I've set up so far. *} -lemma has_derivative_inverse_strong: fixes f::"real^'n::finite \ real^'n" +lemma has_derivative_inverse_strong: fixes f::"real^'n \ real^'n" assumes "open s" "x \ s" "continuous_on s f" "\x\s. g(f x) = x" "(f has_derivative f') (at x)" "f' o g' = id" shows "(g has_derivative g') (at (f x))" proof- @@ -949,7 +949,7 @@ subsection {* A rewrite based on the other domain. *} -lemma has_derivative_inverse_strong_x: fixes f::"real^'n::finite \ real^'n" +lemma has_derivative_inverse_strong_x: fixes f::"real^'n \ real^'n" assumes "open s" "g y \ s" "continuous_on s f" "\x\s. g(f x) = x" "(f has_derivative f') (at (g y))" "f' o g' = id" "f(g y) = y" shows "(g has_derivative g') (at y)" @@ -957,7 +957,7 @@ subsection {* On a region. *} -lemma has_derivative_inverse_on: fixes f::"real^'n::finite \ real^'n" +lemma has_derivative_inverse_on: fixes f::"real^'n \ real^'n" assumes "open s" "\x\s. (f has_derivative f'(x)) (at x)" "\x\s. g(f x) = x" "f'(x) o g'(x) = id" "x\s" shows "(g has_derivative g'(x)) (at (f x))" apply(rule has_derivative_inverse_strong[where g'="g' x" and f=f]) apply(rule assms)+ @@ -972,7 +972,7 @@ lemma bounded_linear_sub: "bounded_linear f \ bounded_linear g ==> bounded_linear (\x. f x - g x)" using bounded_linear_add[of f "\x. - g x"] bounded_linear_minus[of g] by(auto simp add:group_simps) -lemma has_derivative_locally_injective: fixes f::"real^'n::finite \ real^'m::finite" +lemma has_derivative_locally_injective: fixes f::"real^'n \ real^'m" assumes "a \ s" "open s" "bounded_linear g'" "g' o f'(a) = id" "\x\s. (f has_derivative f'(x)) (at x)" "\e>0. \d>0. \x. dist a x < d \ onorm(\v. f' x v - f' a v) < e" @@ -1016,7 +1016,7 @@ subsection {* Uniformly convergent sequence of derivatives. *} -lemma has_derivative_sequence_lipschitz_lemma: fixes f::"nat \ real^'m::finite \ real^'n::finite" +lemma has_derivative_sequence_lipschitz_lemma: fixes f::"nat \ real^'m \ real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\n\N. \x\s. \h. norm(f' n x h - g' x h) \ e * norm(h)" shows "\m\N. \n\N. \x\s. \y\s. norm((f m x - f n x) - (f m y - f n y)) \ 2 * e * norm(x - y)" proof(default)+ @@ -1033,7 +1033,7 @@ thus "onorm (\h. f' m x h - f' n x h) \ 2 * e" apply-apply(rule onorm(2)) apply(rule linear_compose_sub) unfolding linear_conv_bounded_linear using assms(2)[rule_format,OF `x\s`, THEN derivative_linear] by auto qed qed -lemma has_derivative_sequence_lipschitz: fixes f::"nat \ real^'m::finite \ real^'n::finite" +lemma has_derivative_sequence_lipschitz: fixes f::"nat \ real^'m \ real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\e>0. \N. \n\N. \x\s. \h. norm(f' n x h - g' x h) \ e * norm(h)" "0 < e" shows "\e>0. \N. \m\N. \n\N. \x\s. \y\s. norm((f m x - f n x) - (f m y - f n y)) \ e * norm(x - y)" proof(rule,rule) @@ -1041,7 +1041,7 @@ guess N using assms(3)[rule_format,OF *(2)] .. thus ?case apply(rule_tac x=N in exI) apply(rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *]) using assms by auto qed -lemma has_derivative_sequence: fixes f::"nat\real^'m::finite\real^'n::finite" +lemma has_derivative_sequence: fixes f::"nat\real^'m\real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\e>0. \N. \n\N. \x\s. \h. norm(f' n x h - g' x h) \ e * norm(h)" "x0 \ s" "((\n. f n x0) ---> l) sequentially" @@ -1115,7 +1115,7 @@ subsection {* Can choose to line up antiderivatives if we want. *} -lemma has_antiderivative_sequence: fixes f::"nat\ real^'m::finite \ real^'n::finite" +lemma has_antiderivative_sequence: fixes f::"nat\ real^'m \ real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\e>0. \N. \n\N. \x\s. \h. norm(f' n x h - g' x h) \ e * norm h" shows "\g. \x\s. (g has_derivative g'(x)) (at x within s)" proof(cases "s={}") @@ -1124,7 +1124,7 @@ apply(rule,rule) apply(rule has_derivative_add_const, rule assms(2)[rule_format], assumption) apply(rule `a\s`) by(auto intro!: Lim_const) qed auto -lemma has_antiderivative_limit: fixes g'::"real^'m::finite \ real^'m::finite \ real^'n::finite" +lemma has_antiderivative_limit: fixes g'::"real^'m \ real^'m \ real^'n" assumes "convex s" "\e>0. \f f'. \x\s. (f has_derivative (f' x)) (at x within s) \ (\h. norm(f' x h - g' x h) \ e * norm(h))" shows "\g. \x\s. (g has_derivative g'(x)) (at x within s)" proof- have *:"\n. \f f'. \x\s. (f has_derivative (f' x)) (at x within s) \ (\h. norm(f' x h - g' x h) \ inverse (real (Suc n)) * norm(h))" @@ -1143,7 +1143,7 @@ definition sums_seq :: "(nat \ 'a::real_normed_vector) \ 'a \ (nat set) \ bool" (infixl "sums'_seq" 12) where "(f sums_seq l) s \ ((\n. setsum f (s \ {0..n})) ---> l) sequentially" -lemma has_derivative_series: fixes f::"nat \ real^'m::finite \ real^'n::finite" +lemma has_derivative_series: fixes f::"nat \ real^'m \ real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\e>0. \N. \n\N. \x\s. \h. norm(setsum (\i. f' i x h) (k \ {0..n}) - g' x h) \ e * norm(h)" "x\s" "((\n. f n x) sums_seq l) k" @@ -1154,7 +1154,7 @@ subsection {* Derivative with composed bilinear function. *} -lemma has_derivative_bilinear_within: fixes h::"real^'m::finite \ real^'n::finite \ real^'p::finite" and f::"real^'q::finite \ real^'m" +lemma has_derivative_bilinear_within: fixes h::"real^'m \ real^'n \ real^'p" and f::"real^'q \ real^'m" assumes "(f has_derivative f') (at x within s)" "(g has_derivative g') (at x within s)" "bounded_bilinear h" shows "((\x. h (f x) (g x)) has_derivative (\d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)" proof- have "(g ---> g x) (at x within s)" apply(rule differentiable_imp_continuous_within[unfolded continuous_within]) @@ -1194,7 +1194,7 @@ h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right h.diff_right h.diff_left scaleR_right_diff_distrib h.zero_right h.zero_left by(auto simp add:field_simps) qed -lemma has_derivative_bilinear_at: fixes h::"real^'m::finite \ real^'n::finite \ real^'p::finite" and f::"real^'p::finite \ real^'m" +lemma has_derivative_bilinear_at: fixes h::"real^'m \ real^'n \ real^'p" and f::"real^'p \ real^'m" assumes "(f has_derivative f') (at x)" "(g has_derivative g') (at x)" "bounded_bilinear h" shows "((\x. h (f x) (g x)) has_derivative (\d. h (f x) (g' d) + h (f' d) (g x))) (at x)" using has_derivative_bilinear_within[of f f' x UNIV g g' h] unfolding within_UNIV using assms by auto @@ -1216,7 +1216,7 @@ using f' unfolding scaleR[THEN sym] by auto next assume ?r thus ?l unfolding vector_derivative_def has_vector_derivative_def differentiable_def by auto qed -lemma vector_derivative_unique_at: fixes f::"real\real^'n::finite" +lemma vector_derivative_unique_at: fixes f::"real\real^'n" assumes "(f has_vector_derivative f') (at x)" "(f has_vector_derivative f'') (at x)" shows "f' = f''" proof- have *:"(\x. x *\<^sub>R f') \ dest_vec1 = (\x. x *\<^sub>R f'') \ dest_vec1" apply(rule frechet_derivative_unique_at) using assms[unfolded has_vector_derivative_def] unfolding has_derivative_at_dest_vec1[THEN sym] by auto @@ -1224,7 +1224,7 @@ hence "((\x. x *\<^sub>R f') \ dest_vec1) (vec1 1) = ((\x. x *\<^sub>R f'') \ dest_vec1) (vec1 1)" using * by auto ultimately show False unfolding o_def vec1_dest_vec1 by auto qed qed -lemma vector_derivative_unique_within_closed_interval: fixes f::"real \ real^'n::finite" +lemma vector_derivative_unique_within_closed_interval: fixes f::"real \ real^'n" assumes "a < b" "x \ {a..b}" "(f has_vector_derivative f') (at x within {a..b})" "(f has_vector_derivative f'') (at x within {a..b})" shows "f' = f''" proof- @@ -1236,35 +1236,35 @@ hence "((\x. x *\<^sub>R f') \ dest_vec1) (vec1 1) = ((\x. x *\<^sub>R f'') \ dest_vec1) (vec1 1)" using * by auto ultimately show False unfolding o_def vec1_dest_vec1 by auto qed qed -lemma vector_derivative_at: fixes f::"real \ real^'a::finite" shows +lemma vector_derivative_at: fixes f::"real \ real^'a" shows "(f has_vector_derivative f') (at x) \ vector_derivative f (at x) = f'" apply(rule vector_derivative_unique_at) defer apply assumption unfolding vector_derivative_works[THEN sym] differentiable_def unfolding has_vector_derivative_def by auto -lemma vector_derivative_within_closed_interval: fixes f::"real \ real^'a::finite" +lemma vector_derivative_within_closed_interval: fixes f::"real \ real^'a" assumes "a < b" "x \ {a..b}" "(f has_vector_derivative f') (at x within {a..b})" shows "vector_derivative f (at x within {a..b}) = f'" apply(rule vector_derivative_unique_within_closed_interval) using vector_derivative_works[unfolded differentiable_def] using assms by(auto simp add:has_vector_derivative_def) -lemma has_vector_derivative_within_subset: fixes f::"real \ real^'a::finite" shows +lemma has_vector_derivative_within_subset: fixes f::"real \ real^'a" shows "(f has_vector_derivative f') (at x within s) \ t \ s \ (f has_vector_derivative f') (at x within t)" unfolding has_vector_derivative_def apply(rule has_derivative_within_subset) by auto -lemma has_vector_derivative_const: fixes c::"real^'n::finite" shows +lemma has_vector_derivative_const: fixes c::"real^'n" shows "((\x. c) has_vector_derivative 0) net" unfolding has_vector_derivative_def using has_derivative_const by auto lemma has_vector_derivative_id: "((\x::real. x) has_vector_derivative 1) net" unfolding has_vector_derivative_def using has_derivative_id by auto -lemma has_vector_derivative_cmul: fixes f::"real \ real^'a::finite" +lemma has_vector_derivative_cmul: fixes f::"real \ real^'a" shows "(f has_vector_derivative f') net \ ((\x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net" unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:group_simps) -lemma has_vector_derivative_cmul_eq: fixes f::"real \ real^'a::finite" assumes "c \ 0" +lemma has_vector_derivative_cmul_eq: fixes f::"real \ real^'a" assumes "c \ 0" shows "(((\x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \ (f has_vector_derivative f') net)" apply rule apply(drule has_vector_derivative_cmul[where c="1/c"]) defer apply(rule has_vector_derivative_cmul) using assms by auto @@ -1285,7 +1285,7 @@ using has_derivative_sub[OF assms[unfolded has_vector_derivative_def]] unfolding has_vector_derivative_def scaleR_right_diff_distrib by auto -lemma has_vector_derivative_bilinear_within: fixes h::"real^'m::finite \ real^'n::finite \ real^'p::finite" +lemma has_vector_derivative_bilinear_within: fixes h::"real^'m \ real^'n \ real^'p" assumes "(f has_vector_derivative f') (at x within s)" "(g has_vector_derivative g') (at x within s)" "bounded_bilinear h" shows "((\x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x within s)" proof- interpret bounded_bilinear h using assms by auto @@ -1294,7 +1294,7 @@ unfolding has_derivative_within_dest_vec1[unfolded o_def, where f="\x. h (f x) (g x)" and f'="\d. h (f x) (d *\<^sub>R g') + h (d *\<^sub>R f') (g x)"] using assms(3) unfolding scaleR_right scaleR_left scaleR_right_distrib by auto qed -lemma has_vector_derivative_bilinear_at: fixes h::"real^'m::finite \ real^'n::finite \ real^'p::finite" +lemma has_vector_derivative_bilinear_at: fixes h::"real^'m \ real^'n \ real^'p" assumes "(f has_vector_derivative f') (at x)" "(g has_vector_derivative g') (at x)" "bounded_bilinear h" shows "((\x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)" apply(rule has_vector_derivative_bilinear_within[where s=UNIV, unfolded within_UNIV]) using assms by auto @@ -1330,4 +1330,3 @@ unfolding o_def scaleR.scaleR_left by auto end - diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Fri Jan 08 14:07:07 2010 +0100 @@ -121,7 +121,7 @@ (* Basic determinant properties. *) (* ------------------------------------------------------------------------- *) -lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n::finite)" +lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n)" proof- let ?di = "\A i j. A$i$j" let ?U = "(UNIV :: 'n set)" @@ -151,7 +151,7 @@ qed lemma det_lowerdiagonal: - fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}" + fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})" assumes ld: "\i j. i < j \ A$i$j = 0" shows "det A = setprod (\i. A$i$i) (UNIV:: 'n set)" proof- @@ -173,7 +173,7 @@ qed lemma det_upperdiagonal: - fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}" + fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}" assumes ld: "\i j. i > j \ A$i$j = 0" shows "det A = setprod (\i. A$i$i) (UNIV:: 'n set)" proof- @@ -195,7 +195,7 @@ qed lemma det_diagonal: - fixes A :: "'a::comm_ring_1^'n^'n::finite" + fixes A :: "'a::comm_ring_1^'n^'n" assumes ld: "\i j. i \ j \ A$i$j = 0" shows "det A = setprod (\i. A$i$i) (UNIV::'n set)" proof- @@ -215,7 +215,7 @@ unfolding det_def by (simp add: sign_id) qed -lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n::finite) = 1" +lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" proof- let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n" let ?U = "UNIV :: 'n set" @@ -232,11 +232,11 @@ finally show ?thesis . qed -lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n::finite) = 0" +lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" by (simp add: det_def setprod_zero) lemma det_permute_rows: - fixes A :: "'a::comm_ring_1^'n^'n::finite" + fixes A :: "'a::comm_ring_1^'n^'n" assumes p: "p permutes (UNIV :: 'n::finite set)" shows "det(\ i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric]) @@ -262,7 +262,7 @@ qed lemma det_permute_columns: - fixes A :: "'a::comm_ring_1^'n^'n::finite" + fixes A :: "'a::comm_ring_1^'n^'n" assumes p: "p permutes (UNIV :: 'n set)" shows "det(\ i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" proof- @@ -277,7 +277,7 @@ qed lemma det_identical_rows: - fixes A :: "'a::ordered_idom^'n^'n::finite" + fixes A :: "'a::ordered_idom^'n^'n" assumes ij: "i \ j" and r: "row i A = row j A" shows "det A = 0" @@ -295,7 +295,7 @@ qed lemma det_identical_columns: - fixes A :: "'a::ordered_idom^'n^'n::finite" + fixes A :: "'a::ordered_idom^'n^'n" assumes ij: "i \ j" and r: "column i A = column j A" shows "det A = 0" @@ -304,7 +304,7 @@ by (metis row_transp r) lemma det_zero_row: - fixes A :: "'a::{idom, ring_char_0}^'n^'n::finite" + fixes A :: "'a::{idom, ring_char_0}^'n^'n" assumes r: "row i A = 0" shows "det A = 0" using r @@ -314,7 +314,7 @@ done lemma det_zero_column: - fixes A :: "'a::{idom,ring_char_0}^'n^'n::finite" + fixes A :: "'a::{idom,ring_char_0}^'n^'n" assumes r: "column i A = 0" shows "det A = 0" apply (subst det_transp[symmetric]) @@ -407,7 +407,7 @@ unfolding vector_smult_lzero . lemma det_row_operation: - fixes A :: "'a::ordered_idom^'n^'n::finite" + fixes A :: "'a::ordered_idom^'n^'n" assumes ij: "i \ j" shows "det (\ k. if k = i then row i A + c *s row j A else row k A) = det A" proof- @@ -421,7 +421,7 @@ qed lemma det_row_span: - fixes A :: "'a:: ordered_idom^'n^'n::finite" + fixes A :: "'a:: ordered_idom^'n^'n" assumes x: "x \ span {row j A |j. j \ i}" shows "det (\ k. if k = i then row i A + x else row k A) = det A" proof- @@ -462,7 +462,7 @@ (* ------------------------------------------------------------------------- *) lemma det_dependent_rows: - fixes A:: "'a::ordered_idom^'n^'n::finite" + fixes A:: "'a::ordered_idom^'n^'n" assumes d: "dependent (rows A)" shows "det A = 0" proof- @@ -488,7 +488,7 @@ ultimately show ?thesis by blast qed -lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n::finite))" shows "det A = 0" +lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n))" shows "det A = 0" by (metis d det_dependent_rows rows_transp det_transp) (* ------------------------------------------------------------------------- *) @@ -500,7 +500,7 @@ lemma det_linear_row_setsum: assumes fS: "finite S" - shows "det ((\ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n::finite) = setsum (\j. det ((\ i. if i = k then a i j else c i)::'a^'n^'n)) S" + shows "det ((\ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (\j. det ((\ i. if i = k then a i j else c i)::'a^'n^'n)) S" proof(induct rule: finite_induct[OF fS]) case 1 thus ?case apply simp unfolding setsum_empty det_row_0[of k] .. next @@ -534,7 +534,7 @@ lemma det_linear_rows_setsum_lemma: assumes fS: "finite S" and fT: "finite T" - shows "det((\ i. if i \ T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n::finite) = + shows "det((\ i. if i \ T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = setsum (\f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)) {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" using fT @@ -580,7 +580,7 @@ lemma det_linear_rows_setsum: assumes fS: "finite (S::'n::finite set)" - shows "det (\ i. setsum (a i) S) = setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n::finite)) {f. \i. f i \ S}" + shows "det (\ i. setsum (a i) S) = setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \i. f i \ S}" proof- have th0: "\x y. ((\ i. if i \ (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\ i. x i)" by vector @@ -588,12 +588,12 @@ qed lemma matrix_mul_setsum_alt: - fixes A B :: "'a::comm_ring_1^'n^'n::finite" + fixes A B :: "'a::comm_ring_1^'n^'n" shows "A ** B = (\ i. setsum (\k. A$i$k *s B $ k) (UNIV :: 'n set))" by (vector matrix_matrix_mult_def setsum_component) lemma det_rows_mul: - "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n::finite) = + "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n) = setprod (\i. c i) (UNIV:: 'n set) * det((\ i. a i)::'a^'n^'n)" proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2) let ?U = "UNIV :: 'n set" @@ -608,7 +608,7 @@ qed lemma det_mul: - fixes A B :: "'a::ordered_idom^'n^'n::finite" + fixes A B :: "'a::ordered_idom^'n^'n" shows "det (A ** B) = det A * det B" proof- let ?U = "UNIV :: 'n set" @@ -700,17 +700,17 @@ (* ------------------------------------------------------------------------- *) lemma invertible_left_inverse: - fixes A :: "real^'n^'n::finite" + fixes A :: "real^'n^'n" shows "invertible A \ (\(B::real^'n^'n). B** A = mat 1)" by (metis invertible_def matrix_left_right_inverse) lemma invertible_righ_inverse: - fixes A :: "real^'n^'n::finite" + fixes A :: "real^'n^'n" shows "invertible A \ (\(B::real^'n^'n). A** B = mat 1)" by (metis invertible_def matrix_left_right_inverse) lemma invertible_det_nz: - fixes A::"real ^'n^'n::finite" + fixes A::"real ^'n^'n" shows "invertible A \ det A \ 0" proof- {assume "invertible A" @@ -761,7 +761,7 @@ (* ------------------------------------------------------------------------- *) lemma cramer_lemma_transp: - fixes A:: "'a::ordered_idom^'n^'n::finite" and x :: "'a ^'n::finite" + fixes A:: "'a::ordered_idom^'n^'n" and x :: "'a ^'n" shows "det ((\ i. if i = k then setsum (\i. x$i *s row i A) (UNIV::'n set) else row i A)::'a^'n^'n) = x$k * det A" (is "?lhs = ?rhs") @@ -797,7 +797,7 @@ qed lemma cramer_lemma: - fixes A :: "'a::ordered_idom ^'n^'n::finite" + fixes A :: "'a::ordered_idom ^'n^'n" shows "det((\ i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A" proof- let ?U = "UNIV :: 'n set" @@ -811,7 +811,7 @@ qed lemma cramer: - fixes A ::"real^'n^'n::finite" + fixes A ::"real^'n^'n" assumes d0: "det A \ 0" shows "A *v x = b \ x = (\ k. det(\ i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)" proof- @@ -842,14 +842,14 @@ definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \ transp Q ** Q = mat 1 \ Q ** transp Q = mat 1" -lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n::finite) \ transp Q ** Q = mat 1" +lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transp Q ** Q = mat 1" by (metis matrix_left_right_inverse orthogonal_matrix_def) -lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n::finite)" +lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)" by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid) lemma orthogonal_matrix_mul: - fixes A :: "real ^'n^'n::finite" + fixes A :: "real ^'n^'n" assumes oA : "orthogonal_matrix A" and oB: "orthogonal_matrix B" shows "orthogonal_matrix(A ** B)" @@ -860,7 +860,7 @@ by (simp add: matrix_mul_rid) lemma orthogonal_transformation_matrix: - fixes f:: "real^'n \ real^'n::finite" + fixes f:: "real^'n \ real^'n" shows "orthogonal_transformation f \ linear f \ orthogonal_matrix(matrix f)" (is "?lhs \ ?rhs") proof- @@ -893,7 +893,7 @@ qed lemma det_orthogonal_matrix: - fixes Q:: "'a::ordered_idom^'n^'n::finite" + fixes Q:: "'a::ordered_idom^'n^'n" assumes oQ: "orthogonal_matrix Q" shows "det Q = 1 \ det Q = - 1" proof- @@ -918,7 +918,7 @@ (* Linearity of scaling, and hence isometry, that preserves origin. *) (* ------------------------------------------------------------------------- *) lemma scaling_linear: - fixes f :: "real ^'n \ real ^'n::finite" + fixes f :: "real ^'n \ real ^'n" assumes f0: "f 0 = 0" and fd: "\x y. dist (f x) (f y) = c * dist x y" shows "linear f" proof- @@ -934,7 +934,7 @@ qed lemma isometry_linear: - "f (0:: real^'n) = (0:: real^'n::finite) \ \x y. dist(f x) (f y) = dist x y + "f (0:: real^'n) = (0:: real^'n) \ \x y. dist(f x) (f y) = dist x y \ linear f" by (rule scaling_linear[where c=1]) simp_all @@ -943,7 +943,7 @@ (* ------------------------------------------------------------------------- *) lemma orthogonal_transformation_isometry: - "orthogonal_transformation f \ f(0::real^'n) = (0::real^'n::finite) \ (\x y. dist(f x) (f y) = dist x y)" + "orthogonal_transformation f \ f(0::real^'n) = (0::real^'n) \ (\x y. dist(f x) (f y) = dist x y)" unfolding orthogonal_transformation apply (rule iffI) apply clarify @@ -962,7 +962,7 @@ (* ------------------------------------------------------------------------- *) lemma isometry_sphere_extend: - fixes f:: "real ^'n \ real ^'n::finite" + fixes f:: "real ^'n \ real ^'n" assumes f1: "\x. norm x = 1 \ norm (f x) = 1" and fd1: "\ x y. norm x = 1 \ norm y = 1 \ dist (f x) (f y) = dist x y" shows "\g. orthogonal_transformation g \ (\x. norm x = 1 \ g x = f x)" @@ -1034,7 +1034,7 @@ definition "rotoinversion_matrix Q \ orthogonal_matrix Q \ det Q = - 1" lemma orthogonal_rotation_or_rotoinversion: - fixes Q :: "'a::ordered_idom^'n^'n::finite" + fixes Q :: "'a::ordered_idom^'n^'n" shows " orthogonal_matrix Q \ rotation_matrix Q \ rotoinversion_matrix Q" by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) (* ------------------------------------------------------------------------- *) diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Jan 08 14:07:07 2010 +0100 @@ -61,38 +61,39 @@ subsection{* Basic componentwise operations on vectors. *} -instantiation "^" :: (plus,type) plus +instantiation cart :: (plus,finite) plus begin definition vector_add_def : "op + \ (\ x y. (\ i. (x$i) + (y$i)))" instance .. end -instantiation "^" :: (times,type) times +instantiation cart :: (times,finite) times begin definition vector_mult_def : "op * \ (\ x y. (\ i. (x$i) * (y$i)))" instance .. end -instantiation "^" :: (minus,type) minus begin +instantiation cart :: (minus,finite) minus begin definition vector_minus_def : "op - \ (\ x y. (\ i. (x$i) - (y$i)))" instance .. end -instantiation "^" :: (uminus,type) uminus begin +instantiation cart :: (uminus,finite) uminus begin definition vector_uminus_def : "uminus \ (\ x. (\ i. - (x$i)))" instance .. end -instantiation "^" :: (zero,type) zero begin + +instantiation cart :: (zero,finite) zero begin definition vector_zero_def : "0 \ (\ i. 0)" instance .. end -instantiation "^" :: (one,type) one begin +instantiation cart :: (one,finite) one begin definition vector_one_def : "1 \ (\ i. 1)" instance .. end -instantiation "^" :: (ord,type) ord +instantiation cart :: (ord,finite) ord begin definition vector_le_def: "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)" @@ -101,7 +102,7 @@ instance by (intro_classes) end -instantiation "^" :: (scaleR, type) scaleR +instantiation cart :: (scaleR, finite) scaleR begin definition vector_scaleR_def: "scaleR = (\ r x. (\ i. scaleR r (x$i)))" instance .. @@ -109,7 +110,7 @@ text{* Also the scalar-vector multiplication. *} -definition vector_scalar_mult:: "'a::times \ 'a ^'n \ 'a ^ 'n" (infixl "*s" 70) +definition vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) where "c *s x = (\ i. c * (x$i))" text{* Constant Vectors *} @@ -162,37 +163,25 @@ text{* Obvious "component-pushing". *} -lemma vec_component [simp]: "(vec x :: 'a ^ 'n)$i = x" +lemma vec_component [simp]: "vec x $ i = x" by (vector vec_def) -lemma vector_add_component [simp]: - fixes x y :: "'a::{plus} ^ 'n" - shows "(x + y)$i = x$i + y$i" +lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i" by vector -lemma vector_minus_component [simp]: - fixes x y :: "'a::{minus} ^ 'n" - shows "(x - y)$i = x$i - y$i" +lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i" by vector -lemma vector_mult_component [simp]: - fixes x y :: "'a::{times} ^ 'n" - shows "(x * y)$i = x$i * y$i" +lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i" by vector -lemma vector_smult_component [simp]: - fixes y :: "'a::{times} ^ 'n" - shows "(c *s y)$i = c * (y$i)" +lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)" by vector -lemma vector_uminus_component [simp]: - fixes x :: "'a::{uminus} ^ 'n" - shows "(- x)$i = - (x$i)" +lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" by vector -lemma vector_scaleR_component [simp]: - fixes x :: "'a::scaleR ^ 'n" - shows "(scaleR r x)$i = scaleR r (x$i)" +lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" by vector lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector @@ -204,83 +193,83 @@ subsection {* Some frequently useful arithmetic lemmas over vectors. *} -instance "^" :: (semigroup_add,type) semigroup_add +instance cart :: (semigroup_add,finite) semigroup_add apply (intro_classes) by (vector add_assoc) -instance "^" :: (monoid_add,type) monoid_add +instance cart :: (monoid_add,finite) monoid_add apply (intro_classes) by vector+ -instance "^" :: (group_add,type) group_add +instance cart :: (group_add,finite) group_add apply (intro_classes) by (vector algebra_simps)+ -instance "^" :: (ab_semigroup_add,type) ab_semigroup_add +instance cart :: (ab_semigroup_add,finite) ab_semigroup_add apply (intro_classes) by (vector add_commute) -instance "^" :: (comm_monoid_add,type) comm_monoid_add +instance cart :: (comm_monoid_add,finite) comm_monoid_add apply (intro_classes) by vector -instance "^" :: (ab_group_add,type) ab_group_add +instance cart :: (ab_group_add,finite) ab_group_add apply (intro_classes) by vector+ -instance "^" :: (cancel_semigroup_add,type) cancel_semigroup_add +instance cart :: (cancel_semigroup_add,finite) cancel_semigroup_add apply (intro_classes) by (vector Cart_eq)+ -instance "^" :: (cancel_ab_semigroup_add,type) cancel_ab_semigroup_add +instance cart :: (cancel_ab_semigroup_add,finite) cancel_ab_semigroup_add apply (intro_classes) by (vector Cart_eq) -instance "^" :: (real_vector, type) real_vector +instance cart :: (real_vector, finite) real_vector by default (vector scaleR_left_distrib scaleR_right_distrib)+ -instance "^" :: (semigroup_mult,type) semigroup_mult +instance cart :: (semigroup_mult,finite) semigroup_mult apply (intro_classes) by (vector mult_assoc) -instance "^" :: (monoid_mult,type) monoid_mult +instance cart :: (monoid_mult,finite) monoid_mult apply (intro_classes) by vector+ -instance "^" :: (ab_semigroup_mult,type) ab_semigroup_mult +instance cart :: (ab_semigroup_mult,finite) ab_semigroup_mult apply (intro_classes) by (vector mult_commute) -instance "^" :: (ab_semigroup_idem_mult,type) ab_semigroup_idem_mult +instance cart :: (ab_semigroup_idem_mult,finite) ab_semigroup_idem_mult apply (intro_classes) by (vector mult_idem) -instance "^" :: (comm_monoid_mult,type) comm_monoid_mult +instance cart :: (comm_monoid_mult,finite) comm_monoid_mult apply (intro_classes) by vector -fun vector_power :: "('a::{one,times} ^'n) \ nat \ 'a^'n" where +fun vector_power where "vector_power x 0 = 1" | "vector_power x (Suc n) = x * vector_power x n" -instance "^" :: (semiring,type) semiring +instance cart :: (semiring,finite) semiring apply (intro_classes) by (vector ring_simps)+ -instance "^" :: (semiring_0,type) semiring_0 +instance cart :: (semiring_0,finite) semiring_0 apply (intro_classes) by (vector ring_simps)+ -instance "^" :: (semiring_1,type) semiring_1 +instance cart :: (semiring_1,finite) semiring_1 apply (intro_classes) by vector -instance "^" :: (comm_semiring,type) comm_semiring +instance cart :: (comm_semiring,finite) comm_semiring apply (intro_classes) by (vector ring_simps)+ -instance "^" :: (comm_semiring_0,type) comm_semiring_0 by (intro_classes) -instance "^" :: (cancel_comm_monoid_add, type) cancel_comm_monoid_add .. -instance "^" :: (semiring_0_cancel,type) semiring_0_cancel by (intro_classes) -instance "^" :: (comm_semiring_0_cancel,type) comm_semiring_0_cancel by (intro_classes) -instance "^" :: (ring,type) ring by (intro_classes) -instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes) -instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes) - -instance "^" :: (ring_1,type) ring_1 .. - -instance "^" :: (real_algebra,type) real_algebra +instance cart :: (comm_semiring_0,finite) comm_semiring_0 by (intro_classes) +instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. +instance cart :: (semiring_0_cancel,finite) semiring_0_cancel by (intro_classes) +instance cart :: (comm_semiring_0_cancel,finite) comm_semiring_0_cancel by (intro_classes) +instance cart :: (ring,finite) ring by (intro_classes) +instance cart :: (semiring_1_cancel,finite) semiring_1_cancel by (intro_classes) +instance cart :: (comm_semiring_1,finite) comm_semiring_1 by (intro_classes) + +instance cart :: (ring_1,finite) ring_1 .. + +instance cart :: (real_algebra,finite) real_algebra apply intro_classes apply (simp_all add: vector_scaleR_def ring_simps) apply vector apply vector done -instance "^" :: (real_algebra_1,type) real_algebra_1 .. +instance cart :: (real_algebra_1,finite) real_algebra_1 .. lemma of_nat_index: "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n" @@ -288,6 +277,7 @@ apply vector apply vector done + lemma zero_index[simp]: "(0 :: 'a::zero ^'n)$i = 0" by vector @@ -301,15 +291,15 @@ finally show ?thesis by simp qed -instance "^" :: (semiring_char_0,type) semiring_char_0 +instance cart :: (semiring_char_0,finite) semiring_char_0 proof (intro_classes) fix m n ::nat show "(of_nat m :: 'a^'b) = of_nat n \ m = n" by (simp add: Cart_eq of_nat_index) qed -instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes -instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes +instance cart :: (comm_ring_1,finite) comm_ring_1 by intro_classes +instance cart :: (ring_char_0,finite) ring_char_0 by intro_classes lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" by (vector mult_assoc) @@ -333,7 +323,7 @@ subsection {* Topological space *} -instantiation "^" :: (topological_space, finite) topological_space +instantiation cart :: (topological_space, finite) topological_space begin definition open_vector_def: @@ -589,7 +579,7 @@ apply (rule_tac x="f(x:=y)" in exI, simp) done -instantiation "^" :: (metric_space, finite) metric_space +instantiation cart :: (metric_space, finite) metric_space begin definition dist_vector_def: @@ -667,7 +657,7 @@ unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le]) lemma LIMSEQ_vector: - fixes X :: "nat \ 'a::metric_space ^ 'n::finite" + fixes X :: "nat \ 'a::metric_space ^ 'n" assumes X: "\i. (\n. X n $ i) ----> (a $ i)" shows "X ----> a" proof (rule metric_LIMSEQ_I) @@ -700,7 +690,7 @@ qed lemma Cauchy_vector: - fixes X :: "nat \ 'a::metric_space ^ 'n::finite" + fixes X :: "nat \ 'a::metric_space ^ 'n" assumes X: "\i. Cauchy (\n. X n $ i)" shows "Cauchy (\n. X n)" proof (rule metric_CauchyI) @@ -733,7 +723,7 @@ then show "\M. \m\M. \n\M. dist (X m) (X n) < r" .. qed -instance "^" :: (complete_space, finite) complete_space +instance cart :: (complete_space, finite) complete_space proof fix X :: "nat \ 'a ^ 'b" assume "Cauchy X" have "\i. (\n. X n $ i) ----> lim (\n. X n $ i)" @@ -747,7 +737,7 @@ subsection {* Norms *} -instantiation "^" :: (real_normed_vector, finite) real_normed_vector +instantiation cart :: (real_normed_vector, finite) real_normed_vector begin definition norm_vector_def: @@ -792,11 +782,11 @@ apply (rule_tac x="1" in exI, simp add: norm_nth_le) done -instance "^" :: (banach, finite) banach .. +instance cart :: (banach, finite) banach .. subsection {* Inner products *} -instantiation "^" :: (real_inner, finite) real_inner +instantiation cart :: (real_inner, finite) real_inner begin definition inner_vector_def: @@ -860,10 +850,10 @@ show ?case by (simp add: h) qed -lemma dot_eq_0: "x \ x = 0 \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) = 0" +lemma dot_eq_0: "x \ x = 0 \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0" by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq) -lemma dot_pos_lt[simp]: "(0 < x \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) \ 0" using dot_eq_0[of x] dot_pos_le[of x] +lemma dot_pos_lt[simp]: "(0 < x \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \ 0" using dot_eq_0[of x] dot_pos_le[of x] by (auto simp add: le_less) subsection{* The collapse of the general concepts to dimension one. *} @@ -1005,7 +995,7 @@ by (simp add: norm_vector_def setL2_def dot_def power2_eq_square) lemma norm_pow_2: "norm x ^ 2 = x \ x" by (simp add: real_vector_norm_def) -lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n::finite)" by (metis norm_eq_zero) +lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) lemma vector_mul_eq_0[simp]: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0" by vector lemma vector_mul_lcancel[simp]: "a *s x = a *s y \ a = (0::real) \ x = y" @@ -1017,7 +1007,7 @@ lemma vector_mul_rcancel_imp: "x \ 0 \ (a::real) *s x = b *s x ==> a = b" by (metis vector_mul_rcancel) lemma norm_cauchy_schwarz: - fixes x y :: "real ^ 'n::finite" + fixes x y :: "real ^ 'n" shows "x \ y <= norm x * norm y" proof- {assume "norm x = 0" @@ -1040,7 +1030,7 @@ qed lemma norm_cauchy_schwarz_abs: - fixes x y :: "real ^ 'n::finite" + fixes x y :: "real ^ 'n" shows "\x \ y\ \ norm x * norm y" using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"] by (simp add: real_abs_def dot_rneg) @@ -1050,38 +1040,36 @@ shows "norm x \ norm y + norm (x - y)" using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps) -lemma norm_triangle_le: "norm(x::real ^'n::finite) + norm y <= e ==> norm(x + y) <= e" +lemma norm_triangle_le: "norm(x::real ^ 'n) + norm y <= e ==> norm(x + y) <= e" by (metis order_trans norm_triangle_ineq) -lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e" +lemma norm_triangle_lt: "norm(x::real ^ 'n) + norm(y) < e ==> norm(x + y) < e" by (metis basic_trans_rules(21) norm_triangle_ineq) -lemma component_le_norm: "\x$i\ <= norm (x::real ^ 'n::finite)" +lemma component_le_norm: "\x$i\ <= norm x" apply (simp add: norm_vector_def) apply (rule member_le_setL2, simp_all) done -lemma norm_bound_component_le: "norm(x::real ^ 'n::finite) <= e - ==> \x$i\ <= e" +lemma norm_bound_component_le: "norm x <= e ==> \x$i\ <= e" by (metis component_le_norm order_trans) -lemma norm_bound_component_lt: "norm(x::real ^ 'n::finite) < e - ==> \x$i\ < e" +lemma norm_bound_component_lt: "norm x < e ==> \x$i\ < e" by (metis component_le_norm basic_trans_rules(21)) -lemma norm_le_l1: "norm (x:: real ^'n::finite) <= setsum(\i. \x$i\) UNIV" +lemma norm_le_l1: "norm x <= setsum(\i. \x$i\) UNIV" by (simp add: norm_vector_def setL2_le_setsum) -lemma real_abs_norm: "\norm x\ = norm (x :: real ^ _)" +lemma real_abs_norm: "\norm x\ = norm x" by (rule abs_norm_cancel) -lemma real_abs_sub_norm: "\norm(x::real ^'n::finite) - norm y\ <= norm(x - y)" +lemma real_abs_sub_norm: "\norm (x::real ^ 'n) - norm y\ <= norm(x - y)" by (rule norm_triangle_ineq3) -lemma norm_le: "norm(x::real ^ _) <= norm(y) \ x \ x <= y \ y" +lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \ x \ x <= y \ y" by (simp add: real_vector_norm_def) -lemma norm_lt: "norm(x::real ^ _) < norm(y) \ x \ x < y \ y" +lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \ x \ x < y \ y" by (simp add: real_vector_norm_def) -lemma norm_eq: "norm (x::real ^ _) = norm y \ x \ x = y \ y" +lemma norm_eq: "norm(x::real ^ 'n) = norm y \ x \ x = y \ y" by (simp add: order_eq_iff norm_le) -lemma norm_eq_1: "norm(x::real ^ _) = 1 \ x \ x = 1" +lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \ x \ x = 1" by (simp add: real_vector_norm_def) text{* Squaring equations and inequalities involving norms. *} @@ -1127,7 +1115,7 @@ text{* Equality of vectors in terms of @{term "op \"} products. *} -lemma vector_eq: "(x:: real ^ 'n::finite) = y \ x \ x = x \ y\ y \ y = x \ x" (is "?lhs \ ?rhs") +lemma vector_eq: "(x:: real ^ 'n) = y \ x \ x = x \ y\ y \ y = x \ x" (is "?lhs \ ?rhs") proof assume "?lhs" then show ?rhs by simp next @@ -1332,7 +1320,7 @@ qed lemma real_setsum_norm: - fixes f :: "'a \ real ^'n::finite" + fixes f :: "'a \ real ^'n" assumes fS: "finite S" shows "norm (setsum f S) <= setsum (\x. norm(f x)) S" proof(induct rule: finite_induct[OF fS]) @@ -1358,7 +1346,7 @@ qed lemma real_setsum_norm_le: - fixes f :: "'a \ real ^ 'n::finite" + fixes f :: "'a \ real ^ 'n" assumes fS: "finite S" and fg: "\x \ S. norm (f x) \ g x" shows "norm (setsum f S) \ setsum g S" @@ -1378,7 +1366,7 @@ by simp lemma real_setsum_norm_bound: - fixes f :: "'a \ real ^ 'n::finite" + fixes f :: "'a \ real ^ 'n" assumes fS: "finite S" and K: "\x \ S. norm (f x) \ K" shows "norm (setsum f S) \ of_nat (card S) * K" @@ -1414,7 +1402,7 @@ by (auto intro: setsum_0') lemma vsum_norm_allsubsets_bound: - fixes f:: "'a \ real ^'n::finite" + fixes f:: "'a \ real ^'n" assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" shows "setsum (\x. norm (f x)) P \ 2 * real CARD('n) * e" proof- @@ -1470,7 +1458,7 @@ "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto) lemma norm_basis: - shows "norm (basis k :: real ^'n::finite) = 1" + shows "norm (basis k :: real ^'n) = 1" apply (simp add: basis_def real_vector_norm_def dot_def) apply (vector delta_mult_idempotent) using setsum_delta[of "UNIV :: 'n set" "k" "\k. 1::real"] @@ -1480,12 +1468,12 @@ lemma norm_basis_1: "norm(basis 1 :: real ^'n::{finite,one}) = 1" by (rule norm_basis) -lemma vector_choose_size: "0 <= c ==> \(x::real^'n::finite). norm x = c" +lemma vector_choose_size: "0 <= c ==> \(x::real^'n). norm x = c" apply (rule exI[where x="c *s basis arbitrary"]) by (simp only: norm_mul norm_basis) lemma vector_choose_dist: assumes e: "0 <= e" - shows "\(y::real^'n::finite). dist x y = e" + shows "\(y::real^'n). dist x y = e" proof- from vector_choose_size[OF e] obtain c:: "real ^'n" where "norm c = e" by blast @@ -1493,29 +1481,29 @@ then show ?thesis by blast qed -lemma basis_inj: "inj (basis :: 'n \ real ^'n::finite)" +lemma basis_inj: "inj (basis :: 'n \ real ^'n)" by (simp add: inj_on_def Cart_eq) lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)" by auto lemma basis_expansion: - "setsum (\i. (x$i) *s basis i) UNIV = (x::('a::ring_1) ^'n::finite)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") + "setsum (\i. (x$i) *s basis i) UNIV = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") by (auto simp add: Cart_eq cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) lemma basis_expansion_unique: - "setsum (\i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n::finite) \ (\i. f i = x$i)" + "setsum (\i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n) \ (\i. f i = x$i)" by (simp add: Cart_eq setsum_delta cond_value_iff cong del: if_weak_cong) lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" by auto lemma dot_basis: - shows "basis i \ x = x$i" "x \ (basis i :: 'a^'n::finite) = (x$i :: 'a::semiring_1)" + shows "basis i \ x = x$i" "x \ (basis i :: 'a^'n) = (x$i :: 'a::semiring_1)" by (auto simp add: dot_def basis_def cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong) lemma inner_basis: - fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n::finite" + fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n" shows "inner (basis i) x = inner 1 (x $ i)" and "inner x (basis i) = inner (x $ i) 1" unfolding inner_vector_def basis_def @@ -1528,7 +1516,7 @@ shows "basis k \ (0:: 'a::semiring_1 ^'n)" by (simp add: basis_eq_0) -lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = (z::'a::semiring_1^'n::finite)" +lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = (z::'a::semiring_1^'n)" apply (auto simp add: Cart_eq dot_basis) apply (erule_tac x="basis i" in allE) apply (simp add: dot_basis) @@ -1537,7 +1525,7 @@ apply (simp add: Cart_eq) done -lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = (y::'a::semiring_1^'n::finite)" +lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = (y::'a::semiring_1^'n)" apply (auto simp add: Cart_eq dot_basis) apply (erule_tac x="basis i" in allE) apply (simp add: dot_basis) @@ -1551,11 +1539,11 @@ definition "orthogonal x y \ (x \ y = 0)" lemma orthogonal_basis: - shows "orthogonal (basis i :: 'a^'n::finite) x \ x$i = (0::'a::ring_1)" + shows "orthogonal (basis i :: 'a^'n) x \ x$i = (0::'a::ring_1)" by (auto simp add: orthogonal_def dot_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong) lemma orthogonal_basis_basis: - shows "orthogonal (basis i :: 'a::ring_1^'n::finite) (basis j) \ i \ j" + shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \ i \ j" unfolding orthogonal_basis[of i] basis_component[of j] by simp (* FIXME : Maybe some of these require less than comm_ring, but not all*) @@ -1664,7 +1652,7 @@ lemma linear_zero: "linear (\x. 0::'a::semiring_1 ^ 'n)" by (simp add: linear_def) lemma linear_compose_setsum: - assumes fS: "finite S" and lS: "\a \ S. linear (f a :: 'a::semiring_1 ^ 'n \ 'a ^ 'm)" + assumes fS: "finite S" and lS: "\a \ S. linear (f a :: 'a::semiring_1 ^ 'n \ 'a ^'m)" shows "linear(\x. setsum (\a. f a x :: 'a::semiring_1 ^'m) S)" using lS apply (induct rule: finite_induct[OF fS]) @@ -1731,7 +1719,7 @@ qed lemma linear_bounded: - fixes f:: "real ^'m::finite \ real ^'n::finite" + fixes f:: "real ^'m \ real ^'n" assumes lf: "linear f" shows "\B. \x. norm (f x) \ B * norm x" proof- @@ -1760,7 +1748,7 @@ qed lemma linear_bounded_pos: - fixes f:: "real ^'n::finite \ real ^ 'm::finite" + fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" shows "\B > 0. \x. norm (f x) \ B * norm x" proof- @@ -1815,7 +1803,7 @@ by (simp add: f.add f.scaleR) qed -lemma bounded_linearI': fixes f::"real^'n::finite \ real^'m::finite" +lemma bounded_linearI': fixes f::"real^'n \ real^'m" assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *s x) = c *s f x" shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym] by(rule linearI[OF assms]) @@ -1850,18 +1838,18 @@ by (simp add: eq_add_iff ring_simps) lemma bilinear_rzero: - fixes h :: "'a::ring^'n \ _" assumes bh: "bilinear h" shows "h x 0 = 0" + fixes h :: "'a::ring^_ \ _" assumes bh: "bilinear h" shows "h x 0 = 0" using bilinear_radd[OF bh, of x 0 0 ] by (simp add: eq_add_iff ring_simps) -lemma bilinear_lsub: "bilinear h ==> h (x - (y:: 'a::ring_1 ^ 'n)) z = h x z - h y z" +lemma bilinear_lsub: "bilinear h ==> h (x - (y:: 'a::ring_1 ^ _)) z = h x z - h y z" by (simp add: diff_def bilinear_ladd bilinear_lneg) -lemma bilinear_rsub: "bilinear h ==> h z (x - (y:: 'a::ring_1 ^ 'n)) = h z x - h z y" +lemma bilinear_rsub: "bilinear h ==> h z (x - (y:: 'a::ring_1 ^ _)) = h z x - h z y" by (simp add: diff_def bilinear_radd bilinear_rneg) lemma bilinear_setsum: - fixes h:: "'a ^'n \ 'a::semiring_1^'m \ 'a ^ 'k" + fixes h:: "'a ^_ \ 'a::semiring_1^_\ 'a ^ _" assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T" shows "h (setsum f S) (setsum g T) = setsum (\(i,j). h (f i) (g j)) (S \ T) " proof- @@ -1876,7 +1864,7 @@ qed lemma bilinear_bounded: - fixes h:: "real ^'m::finite \ real^'n::finite \ real ^ 'k::finite" + fixes h:: "real ^'m \ real^'n \ real ^'k" assumes bh: "bilinear h" shows "\B. \x y. norm (h x y) \ B * norm x * norm y" proof- @@ -1903,7 +1891,7 @@ qed lemma bilinear_bounded_pos: - fixes h:: "real ^'m::finite \ real^'n::finite \ real ^ 'k::finite" + fixes h:: "real ^'m \ real^'n \ real ^'k" assumes bh: "bilinear h" shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" proof- @@ -1965,7 +1953,7 @@ lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis lemma adjoint_works_lemma: - fixes f:: "'a::ring_1 ^'n::finite \ 'a ^ 'm::finite" + fixes f:: "'a::ring_1 ^'n \ 'a ^'m" assumes lf: "linear f" shows "\x y. f x \ y = x \ adjoint f y" proof- @@ -1993,34 +1981,34 @@ qed lemma adjoint_works: - fixes f:: "'a::ring_1 ^'n::finite \ 'a ^ 'm::finite" + fixes f:: "'a::ring_1 ^'n \ 'a ^'m" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" using adjoint_works_lemma[OF lf] by metis lemma adjoint_linear: - fixes f :: "'a::comm_ring_1 ^'n::finite \ 'a ^ 'm::finite" + fixes f :: "'a::comm_ring_1 ^'n \ 'a ^'m" assumes lf: "linear f" shows "linear (adjoint f)" by (simp add: linear_def vector_eq_ldot[symmetric] dot_radd dot_rmult adjoint_works[OF lf]) lemma adjoint_clauses: - fixes f:: "'a::comm_ring_1 ^'n::finite \ 'a ^ 'm::finite" + fixes f:: "'a::comm_ring_1 ^'n \ 'a ^'m" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" and "adjoint f y \ x = y \ f x" by (simp_all add: adjoint_works[OF lf] dot_sym ) lemma adjoint_adjoint: - fixes f:: "'a::comm_ring_1 ^ 'n::finite \ 'a ^ 'm::finite" + fixes f:: "'a::comm_ring_1 ^ 'n \ 'a ^'m" assumes lf: "linear f" shows "adjoint (adjoint f) = f" apply (rule ext) by (simp add: vector_eq_ldot[symmetric] adjoint_clauses[OF adjoint_linear[OF lf]] adjoint_clauses[OF lf]) lemma adjoint_unique: - fixes f:: "'a::comm_ring_1 ^ 'n::finite \ 'a ^ 'm::finite" + fixes f:: "'a::comm_ring_1 ^ 'n \ 'a ^'m" assumes lf: "linear f" and u: "\x y. f' x \ y = x \ f y" shows "f' = adjoint f" apply (rule ext) @@ -2029,30 +2017,14 @@ text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *} -consts generic_mult :: "'a \ 'b \ 'c" (infixr "\" 75) - -defs (overloaded) -matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^'n^'m) \ (m' :: 'a ^'p^'n) \ (\ i j. setsum (\k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m" - -abbreviation - matrix_matrix_mult' :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" (infixl "**" 70) - where "m ** m' == m\ m'" - -defs (overloaded) - matrix_vector_mult_def: "(m::('a::semiring_1) ^'n^'m) \ (x::'a ^'n) \ (\ i. setsum (\j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m" - -abbreviation - matrix_vector_mult' :: "('a::semiring_1) ^'n^'m \ 'a ^'n \ 'a ^ 'm" (infixl "*v" 70) - where - "m *v v == m \ v" - -defs (overloaded) - vector_matrix_mult_def: "(x::'a^'m) \ (m::('a::semiring_1) ^'n^'m) \ (\ j. setsum (\i. ((m$i)$j) * (x$i)) (UNIV :: 'm set)) :: 'a^'n" - -abbreviation - vactor_matrix_mult' :: "'a ^ 'm \ ('a::semiring_1) ^'n^'m \ 'a ^'n " (infixl "v*" 70) - where - "v v* m == v \ m" +definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" (infixl "**" 70) + where "m ** m' == (\ i j. setsum (\k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m" + +definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \ 'a ^'n \ 'a ^ 'm" (infixl "*v" 70) + where "m *v x \ (\ i. setsum (\j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m" + +definition vector_matrix_mult :: "'a ^ 'm \ ('a::semiring_1) ^'n^'m \ 'a ^'n " (infixl "v*" 70) + where "v v* m == (\ j. setsum (\i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n" definition "(mat::'a::zero => 'a ^'n^'n) k = (\ i j. if i = j then k else 0)" definition "(transp::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A$j)$i))" @@ -2062,11 +2034,11 @@ definition "columns(A::'a^'n^'m) = { column i A | i. i \ (UNIV :: 'n set)}" lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) -lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \ B) + (A \ C)" +lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps) lemma matrix_mul_lid: - fixes A :: "'a::semiring_1 ^ 'm ^ 'n::finite" + fixes A :: "'a::semiring_1 ^ 'm ^ 'n" shows "mat 1 ** A = A" apply (simp add: matrix_matrix_mult_def mat_def) apply vector @@ -2074,7 +2046,7 @@ lemma matrix_mul_rid: - fixes A :: "'a::semiring_1 ^ 'm::finite ^ 'n" + fixes A :: "'a::semiring_1 ^ 'm ^ 'n" shows "A ** mat 1 = A" apply (simp add: matrix_matrix_mult_def mat_def) apply vector @@ -2092,16 +2064,16 @@ apply simp done -lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n::finite)" +lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" apply (vector matrix_vector_mult_def mat_def) by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong) -lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^'m^'n)" +lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^_^_)" by (simp add: matrix_matrix_mult_def transp_def Cart_eq mult_commute) lemma matrix_eq: - fixes A B :: "'a::semiring_1 ^ 'n::finite ^ 'm" + fixes A B :: "'a::semiring_1 ^ 'n ^ 'm" shows "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") apply auto apply (subst Cart_eq) @@ -2112,10 +2084,10 @@ by (auto simp add: basis_def cond_value_iff cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong) lemma matrix_vector_mul_component: - shows "((A::'a::semiring_1^'n'^'m) *v x)$k = (A$k) \ x" + shows "((A::'a::semiring_1^_^_) *v x)$k = (A$k) \ x" by (simp add: matrix_vector_mult_def dot_def) -lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^'n) v* A) \ y = x \ (A *v y)" +lemma dot_lmul_matrix: "((x::'a::comm_semiring_1 ^_) v* A) \ y = x \ (A *v y)" apply (simp add: dot_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) apply (subst setsum_commute) by simp @@ -2127,19 +2099,19 @@ by (vector transp_def) lemma row_transp: - fixes A:: "'a::semiring_1^'n^'m" + fixes A:: "'a::semiring_1^_^_" shows "row i (transp A) = column i A" by (simp add: row_def column_def transp_def Cart_eq) lemma column_transp: - fixes A:: "'a::semiring_1^'n^'m" + fixes A:: "'a::semiring_1^_^_" shows "column i (transp A) = row i A" by (simp add: row_def column_def transp_def Cart_eq) -lemma rows_transp: "rows(transp (A::'a::semiring_1^'n^'m)) = columns A" +lemma rows_transp: "rows(transp (A::'a::semiring_1^_^_)) = columns A" by (auto simp add: rows_def columns_def row_transp intro: set_ext) -lemma columns_transp: "columns(transp (A::'a::semiring_1^'n^'m)) = rows A" by (metis transp_transp rows_transp) +lemma columns_transp: "columns(transp (A::'a::semiring_1^_^_)) = rows A" by (metis transp_transp rows_transp) text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *} @@ -2150,12 +2122,12 @@ by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute) lemma vector_componentwise: - "(x::'a::ring_1^'n::finite) = (\ j. setsum (\i. (x$i) * (basis i :: 'a^'n)$j) (UNIV :: 'n set))" + "(x::'a::ring_1^'n) = (\ j. setsum (\i. (x$i) * (basis i :: 'a^'n)$j) (UNIV :: 'n set))" apply (subst basis_expansion[symmetric]) by (vector Cart_eq setsum_component) lemma linear_componentwise: - fixes f:: "'a::ring_1 ^ 'm::finite \ 'a ^ 'n" + fixes f:: "'a::ring_1 ^'m \ 'a ^ _" assumes lf: "linear f" shows "(f x)$j = setsum (\i. (x$i) * (f (basis i)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") proof- @@ -2181,31 +2153,31 @@ definition matrix:: "('a::{plus,times, one, zero}^'m \ 'a ^ 'n) \ 'a^'m^'n" where "matrix f = (\ i j. (f(basis j))$i)" -lemma matrix_vector_mul_linear: "linear(\x. A *v (x::'a::comm_semiring_1 ^ 'n))" +lemma matrix_vector_mul_linear: "linear(\x. A *v (x::'a::comm_semiring_1 ^ _))" by (simp add: linear_def matrix_vector_mult_def Cart_eq ring_simps setsum_right_distrib setsum_addf) -lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n::finite)" +lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n)" apply (simp add: matrix_def matrix_vector_mult_def Cart_eq mult_commute) apply clarify apply (rule linear_componentwise[OF lf, symmetric]) done -lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::'a::comm_ring_1 ^ 'n::finite))" by (simp add: ext matrix_works) - -lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: 'a:: comm_ring_1 ^ 'n::finite)) = A" +lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::'a::comm_ring_1 ^ 'n))" by (simp add: ext matrix_works) + +lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: 'a:: comm_ring_1 ^ 'n)) = A" by (simp add: matrix_eq matrix_vector_mul_linear matrix_works) lemma matrix_compose: - assumes lf: "linear (f::'a::comm_ring_1^'n::finite \ 'a^'m::finite)" - and lg: "linear (g::'a::comm_ring_1^'m::finite \ 'a^'k)" + assumes lf: "linear (f::'a::comm_ring_1^'n \ 'a^'m)" + and lg: "linear (g::'a::comm_ring_1^'m \ 'a^_)" shows "matrix (g o f) = matrix g ** matrix f" using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) -lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x$i) *s ((transp A)$i)) (UNIV:: 'n set)" +lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\i. (x$i) *s ((transp A)$i)) (UNIV:: 'n set)" by (simp add: matrix_vector_mult_def transp_def Cart_eq mult_commute) -lemma adjoint_matrix: "adjoint(\x. (A::'a::comm_ring_1^'n::finite^'m::finite) *v x) = (\x. transp A *v x)" +lemma adjoint_matrix: "adjoint(\x. (A::'a::comm_ring_1^'n^'m) *v x) = (\x. transp A *v x)" apply (rule adjoint_unique[symmetric]) apply (rule matrix_vector_mul_linear) apply (simp add: transp_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) @@ -2213,7 +2185,7 @@ apply (auto simp add: mult_ac) done -lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n::finite \ 'a ^ 'm::finite)" +lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \ 'a ^'m)" shows "matrix(adjoint f) = transp(matrix f)" apply (subst matrix_vector_mul[OF lf]) unfolding adjoint_matrix matrix_of_matrix_vector_mul .. @@ -2310,7 +2282,7 @@ definition "onorm f = Sup {norm (f x)| x. norm x = 1}" lemma norm_bound_generalize: - fixes f:: "real ^'n::finite \ real^'m::finite" + fixes f:: "real ^'n \ real^'m" assumes lf: "linear f" shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" (is "?lhs \ ?rhs") proof- @@ -2343,7 +2315,7 @@ qed lemma onorm: - fixes f:: "real ^'n::finite \ real ^'m::finite" + fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" shows "norm (f x) <= onorm f * norm x" and "\x. norm (f x) <= b * norm x \ onorm f <= b" @@ -2367,10 +2339,10 @@ } qed -lemma onorm_pos_le: assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" shows "0 <= onorm f" +lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \ real ^'m)" shows "0 <= onorm f" using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis arbitrary"], unfolded norm_basis] by simp -lemma onorm_eq_0: assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" +lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \ real ^'m)" shows "onorm f = 0 \ (\x. f x = 0)" using onorm[OF lf] apply (auto simp add: onorm_pos_le) @@ -2380,7 +2352,7 @@ apply arith done -lemma onorm_const: "onorm(\x::real^'n::finite. (y::real ^ 'm::finite)) = norm y" +lemma onorm_const: "onorm(\x::real^'n. (y::real ^'m)) = norm y" proof- let ?f = "\x::real^'n. (y::real ^ 'm)" have th: "{norm (?f x)| x. norm x = 1} = {norm y}" @@ -2390,14 +2362,14 @@ apply (rule Sup_unique) by (simp_all add: setle_def) qed -lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \ real ^'m::finite)" +lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n \ real ^'m)" shows "0 < onorm f \ ~(\x. f x = 0)" unfolding onorm_eq_0[OF lf, symmetric] using onorm_pos_le[OF lf] by arith lemma onorm_compose: - assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" - and lg: "linear (g::real^'k::finite \ real^'n::finite)" + assumes lf: "linear (f::real ^'n \ real ^'m)" + and lg: "linear (g::real^'k \ real^'n)" shows "onorm (f o g) <= onorm f * onorm g" apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format]) unfolding o_def @@ -2409,18 +2381,18 @@ apply (rule onorm_pos_le[OF lf]) done -lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n::finite \ real^'m::finite)" +lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \ real^'m)" shows "onorm (\x. - f x) \ onorm f" using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf] unfolding norm_minus_cancel by metis -lemma onorm_neg: assumes lf: "linear (f::real ^'n::finite \ real^'m::finite)" +lemma onorm_neg: assumes lf: "linear (f::real ^'n \ real^'m)" shows "onorm (\x. - f x) = onorm f" using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]] by simp lemma onorm_triangle: - assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" and lg: "linear g" + assumes lf: "linear (f::real ^'n \ real ^'m)" and lg: "linear g" shows "onorm (\x. f x + g x) <= onorm f + onorm g" apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format]) apply (rule order_trans) @@ -2431,14 +2403,14 @@ apply (rule onorm(1)[OF lg]) done -lemma onorm_triangle_le: "linear (f::real ^'n::finite \ real ^'m::finite) \ linear g \ onorm(f) + onorm(g) <= e +lemma onorm_triangle_le: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) <= e \ onorm(\x. f x + g x) <= e" apply (rule order_trans) apply (rule onorm_triangle) apply assumption+ done -lemma onorm_triangle_lt: "linear (f::real ^'n::finite \ real ^'m::finite) \ linear g \ onorm(f) + onorm(g) < e +lemma onorm_triangle_lt: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) < e ==> onorm(\x. f x + g x) < e" apply (rule order_le_less_trans) apply (rule onorm_triangle) @@ -2534,21 +2506,21 @@ apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto lemma linear_vmul_dest_vec1: - fixes f:: "'a::semiring_1^'n \ 'a^1" + fixes f:: "'a::semiring_1^_ \ 'a^1" shows "linear f \ linear (\x. dest_vec1(f x) *s v)" unfolding dest_vec1_def apply (rule linear_vmul_component) by auto lemma linear_from_scalars: - assumes lf: "linear (f::'a::comm_ring_1 ^1 \ 'a^'n)" + assumes lf: "linear (f::'a::comm_ring_1 ^1 \ 'a^_)" shows "f = (\x. dest_vec1 x *s column 1 (matrix f))" apply (rule ext) apply (subst matrix_works[OF lf, symmetric]) apply (auto simp add: Cart_eq matrix_vector_mult_def dest_vec1_def column_def mult_commute UNIV_1) done -lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n::finite \ 'a^1)" +lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \ 'a^1)" shows "f = (\x. vec1(row 1 (matrix f) \ x))" apply (rule ext) apply (subst matrix_works[OF lf, symmetric]) @@ -2580,16 +2552,16 @@ lemma fstcart_vec[simp]: "fstcart(vec x) = vec x" by (simp add: Cart_eq) -lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b + 'c)) + fstcart y" +lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b::finite + 'c::finite)) + fstcart y" by (simp add: Cart_eq) -lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b + 'c))" +lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b::finite + 'c::finite))" by (simp add: Cart_eq) -lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^('b + 'c))" +lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^(_ + _))" by (simp add: Cart_eq) -lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^('b + 'c)) - fstcart y" +lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^(_ + _)) - fstcart y" by (simp add: Cart_eq) lemma fstcart_setsum: @@ -2601,16 +2573,16 @@ lemma sndcart_vec[simp]: "sndcart(vec x) = vec x" by (simp add: Cart_eq) -lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^('b + 'c)) + sndcart y" +lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^(_ + _)) + sndcart y" by (simp add: Cart_eq) -lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^('b + 'c))" +lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^(_ + _))" by (simp add: Cart_eq) -lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^('b + 'c))" +lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^(_ + _))" by (simp add: Cart_eq) -lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^('b + 'c)) - sndcart y" +lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^(_ + _)) - sndcart y" by (simp add: Cart_eq) lemma sndcart_setsum: @@ -2683,7 +2655,7 @@ lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y" unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart) -lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \ (pastecart y1 y2) = x1 \ y1 + x2 \ y2" +lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n) (x2::'a::{times,comm_monoid_add}^'m)) \ (pastecart y1 y2) = x1 \ y1 + x2 \ y2" by (simp add: dot_def setsum_UNIV_sum pastecart_def) text {* TODO: move to NthRoot *} @@ -2922,10 +2894,10 @@ lemma subspace_mul: "subspace S \ x \ S \ c *s x \ S" by (metis subspace_def) -lemma subspace_neg: "subspace S \ (x::'a::ring_1^'n) \ S \ - x \ S" +lemma subspace_neg: "subspace S \ (x::'a::ring_1^_) \ S \ - x \ S" by (metis vector_sneg_minus1 subspace_mul) -lemma subspace_sub: "subspace S \ (x::'a::ring_1^'n) \ S \ y \ S \ x - y \ S" +lemma subspace_sub: "subspace S \ (x::'a::ring_1^_) \ S \ y \ S \ x - y \ S" by (metis diff_def subspace_add subspace_neg) lemma subspace_setsum: @@ -2937,7 +2909,7 @@ by (simp add: subspace_def sA, auto simp add: sA subspace_add) lemma subspace_linear_image: - assumes lf: "linear (f::'a::semiring_1^'n \ _)" and sS: "subspace S" + assumes lf: "linear (f::'a::semiring_1^_ \ _)" and sS: "subspace S" shows "subspace(f ` S)" using lf sS linear_0[OF lf] unfolding linear_def subspace_def @@ -2946,7 +2918,7 @@ apply (rule_tac x="c*s x" in bexI, auto) done -lemma subspace_linear_preimage: "linear (f::'a::semiring_1^'n \ _) ==> subspace S ==> subspace {x. f x \ S}" +lemma subspace_linear_preimage: "linear (f::'a::semiring_1^_ \ _) ==> subspace S ==> subspace {x. f x \ S}" by (auto simp add: subspace_def linear_def linear_0[of f]) lemma subspace_trivial: "subspace {0::'a::semiring_1 ^_}" @@ -2997,11 +2969,11 @@ show "P x" by (metis mem_def subset_eq) qed -lemma span_empty: "span {} = {(0::'a::semiring_0 ^ 'n)}" +lemma span_empty: "span {} = {(0::'a::semiring_0 ^ _)}" apply (simp add: span_def) apply (rule hull_unique) apply (auto simp add: mem_def subspace_def) - unfolding mem_def[of "0::'a^'n", symmetric] + unfolding mem_def[of "0::'a^_", symmetric] apply simp done @@ -3023,7 +2995,7 @@ and P: "subspace P" shows "\x \ span S. P x" using span_induct SP P by blast -inductive span_induct_alt_help for S:: "'a::semiring_1^'n \ bool" +inductive span_induct_alt_help for S:: "'a::semiring_1^_ \ bool" where span_induct_alt_help_0: "span_induct_alt_help S 0" | span_induct_alt_help_S: "x \ S \ span_induct_alt_help S z \ span_induct_alt_help S (c *s x + z)" @@ -3094,24 +3066,24 @@ lemma span_mul: "x \ span S ==> (c *s x) \ span S" by (metis subspace_span subspace_mul) -lemma span_neg: "x \ span S ==> - (x::'a::ring_1^'n) \ span S" +lemma span_neg: "x \ span S ==> - (x::'a::ring_1^_) \ span S" by (metis subspace_neg subspace_span) -lemma span_sub: "(x::'a::ring_1^'n) \ span S \ y \ span S ==> x - y \ span S" +lemma span_sub: "(x::'a::ring_1^_) \ span S \ y \ span S ==> x - y \ span S" by (metis subspace_span subspace_sub) lemma span_setsum: "finite A \ \x \ A. f x \ span S ==> setsum f A \ span S" apply (rule subspace_setsum) by (metis subspace_span subspace_setsum)+ -lemma span_add_eq: "(x::'a::ring_1^'n) \ span S \ x + y \ span S \ y \ span S" +lemma span_add_eq: "(x::'a::ring_1^_) \ span S \ x + y \ span S \ y \ span S" apply (auto simp only: span_add span_sub) apply (subgoal_tac "(x + y) - x \ span S", simp) by (simp only: span_add span_sub) (* Mapping under linear image. *) -lemma span_linear_image: assumes lf: "linear (f::'a::semiring_1 ^ 'n => _)" +lemma span_linear_image: assumes lf: "linear (f::'a::semiring_1 ^ _ => _)" shows "span (f ` S) = f ` (span S)" proof- {fix x @@ -3144,7 +3116,7 @@ (* The key breakdown property. *) lemma span_breakdown: - assumes bS: "(b::'a::ring_1 ^ 'n) \ S" and aS: "a \ span S" + assumes bS: "(b::'a::ring_1 ^ _) \ S" and aS: "a \ span S" shows "\k. a - k*s b \ span (S - {b})" (is "?P a") proof- {fix x assume xS: "x \ S" @@ -3186,7 +3158,7 @@ qed lemma span_breakdown_eq: - "(x::'a::ring_1^'n) \ span (insert a S) \ (\k. (x - k *s a) \ span S)" (is "?lhs \ ?rhs") + "(x::'a::ring_1^_) \ span (insert a S) \ (\k. (x - k *s a) \ span S)" (is "?lhs \ ?rhs") proof- {assume x: "x \ span (insert a S)" from x span_breakdown[of "a" "insert a S" "x"] @@ -3217,7 +3189,7 @@ (* Hence some "reversal" results.*) lemma in_span_insert: - assumes a: "(a::'a::field^'n) \ span (insert b S)" and na: "a \ span S" + assumes a: "(a::'a::field^_) \ span (insert b S)" and na: "a \ span S" shows "b \ span (insert a S)" proof- from span_breakdown[of b "insert b S" a, OF insertI1 a] @@ -3256,7 +3228,7 @@ qed lemma in_span_delete: - assumes a: "(a::'a::field^'n) \ span S" + assumes a: "(a::'a::field^_) \ span S" and na: "a \ span (S-{b})" shows "b \ span (insert a (S - {b}))" apply (rule in_span_insert) @@ -3270,7 +3242,7 @@ (* Transitivity property. *) lemma span_trans: - assumes x: "(x::'a::ring_1^'n) \ span S" and y: "y \ span (insert x S)" + assumes x: "(x::'a::ring_1^_) \ span S" and y: "y \ span (insert x S)" shows "y \ span S" proof- from span_breakdown[of x "insert x S" y, OF insertI1 y] @@ -3292,7 +3264,7 @@ (* ------------------------------------------------------------------------- *) lemma span_explicit: - "span P = {y::'a::semiring_1^'n. \S u. finite S \ S \ P \ setsum (\v. u v *s v) S = y}" + "span P = {y::'a::semiring_1^_. \S u. finite S \ S \ P \ setsum (\v. u v *s v) S = y}" (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \S u. ?Q S u y}") proof- {fix x assume x: "x \ ?E" @@ -3351,7 +3323,7 @@ qed lemma dependent_explicit: - "dependent P \ (\S u. finite S \ S \ P \ (\(v::'a::{idom,field}^'n) \S. u v \ 0 \ setsum (\v. u v *s v) S = 0))" (is "?lhs = ?rhs") + "dependent P \ (\S u. finite S \ S \ P \ (\(v::'a::{idom,field}^_) \S. u v \ 0 \ setsum (\v. u v *s v) S = 0))" (is "?lhs = ?rhs") proof- {assume dP: "dependent P" then obtain a S u where aP: "a \ P" and fS: "finite S" @@ -3402,7 +3374,7 @@ lemma span_finite: assumes fS: "finite S" - shows "span S = {(y::'a::semiring_1^'n). \u. setsum (\v. u v *s v) S = y}" + shows "span S = {(y::'a::semiring_1^_). \u. setsum (\v. u v *s v) S = y}" (is "_ = ?rhs") proof- {fix y assume y: "y \ span S" @@ -3424,7 +3396,7 @@ (* Standard bases are a spanning set, and obviously finite. *) -lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n::finite | i. i \ (UNIV :: 'n set)} = UNIV" +lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n | i. i \ (UNIV :: 'n set)} = UNIV" apply (rule set_ext) apply auto apply (subst basis_expansion[symmetric]) @@ -3436,13 +3408,13 @@ apply (auto simp add: Collect_def mem_def) done -lemma finite_stdbasis: "finite {basis i ::real^'n::finite |i. i\ (UNIV:: 'n set)}" (is "finite ?S") +lemma finite_stdbasis: "finite {basis i ::real^'n |i. i\ (UNIV:: 'n set)}" (is "finite ?S") proof- have eq: "?S = basis ` UNIV" by blast show ?thesis unfolding eq by auto qed -lemma card_stdbasis: "card {basis i ::real^'n::finite |i. i\ (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _") +lemma card_stdbasis: "card {basis i ::real^'n |i. i\ (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _") proof- have eq: "?S = basis ` UNIV" by blast show ?thesis unfolding eq using card_image[OF basis_inj] by simp @@ -3450,14 +3422,14 @@ lemma independent_stdbasis_lemma: - assumes x: "(x::'a::semiring_1 ^ 'n) \ span (basis ` S)" + assumes x: "(x::'a::semiring_1 ^ _) \ span (basis ` S)" and iS: "i \ S" shows "(x$i) = 0" proof- let ?U = "UNIV :: 'n set" let ?B = "basis ` S" - let ?P = "\(x::'a^'n). \i\ ?U. i \ S \ x$i =0" - {fix x::"'a^'n" assume xS: "x\ ?B" + let ?P = "\(x::'a^_). \i\ ?U. i \ S \ x$i =0" + {fix x::"'a^_" assume xS: "x\ ?B" from xS have "?P x" by auto} moreover have "subspace ?P" @@ -3466,7 +3438,7 @@ using x span_induct[of ?B ?P x] iS by blast qed -lemma independent_stdbasis: "independent {basis i ::real^'n::finite |i. i\ (UNIV :: 'n set)}" +lemma independent_stdbasis: "independent {basis i ::real^'n |i. i\ (UNIV :: 'n set)}" proof- let ?I = "UNIV :: 'n set" let ?b = "basis :: _ \ real ^'n" @@ -3490,7 +3462,7 @@ (* This is useful for building a basis step-by-step. *) lemma independent_insert: - "independent(insert (a::'a::field ^'n) S) \ + "independent(insert (a::'a::field ^_) S) \ (if a \ S then independent S else independent S \ a \ span S)" (is "?lhs \ ?rhs") proof- @@ -3539,7 +3511,7 @@ by (metis subset_eq span_superset) lemma spanning_subset_independent: - assumes BA: "B \ A" and iA: "independent (A::('a::field ^'n) set)" + assumes BA: "B \ A" and iA: "independent (A::('a::field ^_) set)" and AsB: "A \ span B" shows "A = B" proof @@ -3650,7 +3622,7 @@ (* This implies corresponding size bounds. *) lemma independent_span_bound: - assumes f: "finite t" and i: "independent (s::('a::field^'n) set)" and sp:"s \ span t" + assumes f: "finite t" and i: "independent (s::('a::field^_) set)" and sp:"s \ span t" shows "finite s \ card s \ card t" by (metis exchange_lemma[OF f i sp] finite_subset card_mono) @@ -3666,7 +3638,7 @@ lemma independent_bound: - fixes S:: "(real^'n::finite) set" + fixes S:: "(real^'n) set" shows "independent S \ finite S \ card S <= CARD('n)" apply (subst card_stdbasis[symmetric]) apply (rule independent_span_bound) @@ -3676,13 +3648,13 @@ apply (rule subset_UNIV) done -lemma dependent_biggerset: "(finite (S::(real ^'n::finite) set) ==> card S > CARD('n)) ==> dependent S" +lemma dependent_biggerset: "(finite (S::(real ^'n) set) ==> card S > CARD('n)) ==> dependent S" by (metis independent_bound not_less) (* Hence we can create a maximal independent subset. *) lemma maximal_independent_subset_extend: - assumes sv: "(S::(real^'n::finite) set) \ V" and iS: "independent S" + assumes sv: "(S::(real^'n) set) \ V" and iS: "independent S" shows "\B. S \ B \ B \ V \ independent B \ V \ span B" using sv iS proof(induct d\ "CARD('n) - card S" arbitrary: S rule: nat_less_induct) @@ -3715,14 +3687,14 @@ qed lemma maximal_independent_subset: - "\(B:: (real ^'n::finite) set). B\ V \ independent B \ V \ span B" + "\(B:: (real ^'n) set). B\ V \ independent B \ V \ span B" by (metis maximal_independent_subset_extend[of "{}:: (real ^'n) set"] empty_subsetI independent_empty) (* Notion of dimension. *) definition "dim V = (SOME n. \B. B \ V \ independent B \ V \ span B \ (card B = n))" -lemma basis_exists: "\B. (B :: (real ^'n::finite) set) \ V \ independent B \ V \ span B \ (card B = dim V)" +lemma basis_exists: "\B. (B :: (real ^'n) set) \ V \ independent B \ V \ span B \ (card B = dim V)" unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (card B = n)"] using maximal_independent_subset[of V] independent_bound by auto @@ -3730,7 +3702,7 @@ (* Consequences of independence or spanning for cardinality. *) lemma independent_card_le_dim: - assumes "(B::(real ^'n::finite) set) \ V" and "independent B" shows "card B \ dim V" + assumes "(B::(real ^'n) set) \ V" and "independent B" shows "card B \ dim V" proof - from basis_exists[of V] `B \ V` obtain B' where "independent B'" and "B \ span B'" and "card B' = dim V" by blast @@ -3738,34 +3710,34 @@ show ?thesis by auto qed -lemma span_card_ge_dim: "(B::(real ^'n::finite) set) \ V \ V \ span B \ finite B \ dim V \ card B" +lemma span_card_ge_dim: "(B::(real ^'n) set) \ V \ V \ span B \ finite B \ dim V \ card B" by (metis basis_exists[of V] independent_span_bound subset_trans) lemma basis_card_eq_dim: - "B \ (V:: (real ^'n::finite) set) \ V \ span B \ independent B \ finite B \ card B = dim V" + "B \ (V:: (real ^'n) set) \ V \ span B \ independent B \ finite B \ card B = dim V" by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_mono independent_bound) -lemma dim_unique: "(B::(real ^'n::finite) set) \ V \ V \ span B \ independent B \ card B = n \ dim V = n" +lemma dim_unique: "(B::(real ^'n) set) \ V \ V \ span B \ independent B \ card B = n \ dim V = n" by (metis basis_card_eq_dim) (* More lemmas about dimension. *) -lemma dim_univ: "dim (UNIV :: (real^'n::finite) set) = CARD('n)" +lemma dim_univ: "dim (UNIV :: (real^'n) set) = CARD('n)" apply (rule dim_unique[of "{basis i |i. i\ (UNIV :: 'n set)}"]) by (auto simp only: span_stdbasis card_stdbasis finite_stdbasis independent_stdbasis) lemma dim_subset: - "(S:: (real ^'n::finite) set) \ T \ dim S \ dim T" + "(S:: (real ^'n) set) \ T \ dim S \ dim T" using basis_exists[of T] basis_exists[of S] by (metis independent_card_le_dim subset_trans) -lemma dim_subset_univ: "dim (S:: (real^'n::finite) set) \ CARD('n)" +lemma dim_subset_univ: "dim (S:: (real^'n) set) \ CARD('n)" by (metis dim_subset subset_UNIV dim_univ) (* Converses to those. *) lemma card_ge_dim_independent: - assumes BV:"(B::(real ^'n::finite) set) \ V" and iB:"independent B" and dVB:"dim V \ card B" + assumes BV:"(B::(real ^'n) set) \ V" and iB:"independent B" and dVB:"dim V \ card B" shows "V \ span B" proof- {fix a assume aV: "a \ V" @@ -3779,7 +3751,7 @@ qed lemma card_le_dim_spanning: - assumes BV: "(B:: (real ^'n::finite) set) \ V" and VB: "V \ span B" + assumes BV: "(B:: (real ^'n) set) \ V" and VB: "V \ span B" and fB: "finite B" and dVB: "dim V \ card B" shows "independent B" proof- @@ -3800,7 +3772,7 @@ then show ?thesis unfolding dependent_def by blast qed -lemma card_eq_dim: "(B:: (real ^'n::finite) set) \ V \ card B = dim V \ finite B \ independent B \ V \ span B" +lemma card_eq_dim: "(B:: (real ^'n) set) \ V \ card B = dim V \ finite B \ independent B \ V \ span B" by (metis order_eq_iff card_le_dim_spanning card_ge_dim_independent) @@ -3809,13 +3781,13 @@ (* ------------------------------------------------------------------------- *) lemma independent_bound_general: - "independent (S:: (real^'n::finite) set) \ finite S \ card S \ dim S" + "independent (S:: (real^'n) set) \ finite S \ card S \ dim S" by (metis independent_card_le_dim independent_bound subset_refl) -lemma dependent_biggerset_general: "(finite (S:: (real^'n::finite) set) \ card S > dim S) \ dependent S" +lemma dependent_biggerset_general: "(finite (S:: (real^'n) set) \ card S > dim S) \ dependent S" using independent_bound_general[of S] by (metis linorder_not_le) -lemma dim_span: "dim (span (S:: (real ^'n::finite) set)) = dim S" +lemma dim_span: "dim (span (S:: (real ^'n) set)) = dim S" proof- have th0: "dim S \ dim (span S)" by (auto simp add: subset_eq intro: dim_subset span_superset) @@ -3828,21 +3800,21 @@ using fB(2) by arith qed -lemma subset_le_dim: "(S:: (real ^'n::finite) set) \ span T \ dim S \ dim T" +lemma subset_le_dim: "(S:: (real ^'n) set) \ span T \ dim S \ dim T" by (metis dim_span dim_subset) -lemma span_eq_dim: "span (S:: (real ^'n::finite) set) = span T ==> dim S = dim T" +lemma span_eq_dim: "span (S:: (real ^'n) set) = span T ==> dim S = dim T" by (metis dim_span) lemma spans_image: - assumes lf: "linear (f::'a::semiring_1^'n \ _)" and VB: "V \ span B" + assumes lf: "linear (f::'a::semiring_1^_ \ _)" and VB: "V \ span B" shows "f ` V \ span (f ` B)" unfolding span_linear_image[OF lf] by (metis VB image_mono) lemma dim_image_le: - fixes f :: "real^'n::finite \ real^'m::finite" - assumes lf: "linear f" shows "dim (f ` S) \ dim (S:: (real ^'n::finite) set)" + fixes f :: "real^'n \ real^'m" + assumes lf: "linear f" shows "dim (f ` S) \ dim (S:: (real ^'n) set)" proof- from basis_exists[of S] obtain B where B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast @@ -3857,7 +3829,7 @@ (* Relation between bases and injectivity/surjectivity of map. *) lemma spanning_surjective_image: - assumes us: "UNIV \ span (S:: ('a::semiring_1 ^'n) set)" + assumes us: "UNIV \ span (S:: ('a::semiring_1 ^_) set)" and lf: "linear f" and sf: "surj f" shows "UNIV \ span (f ` S)" proof- @@ -3867,7 +3839,7 @@ qed lemma independent_injective_image: - assumes iS: "independent (S::('a::semiring_1^'n) set)" and lf: "linear f" and fi: "inj f" + assumes iS: "independent (S::('a::semiring_1^_) set)" and lf: "linear f" and fi: "inj f" shows "independent (f ` S)" proof- {fix a assume a: "a \ S" "f a \ span (f ` S - {f a})" @@ -3886,14 +3858,14 @@ (* FIXME : Move to some general theory ?*) definition "pairwise R S \ (\x \ S. \y\ S. x\y \ R x y)" -lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n::finite) \ (x - ((b \ x) / (b\b)) *s b) = 0" +lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n) \ (x - ((b \ x) / (b\b)) *s b) = 0" apply (cases "b = 0", simp) apply (simp add: dot_rsub dot_rmult) unfolding times_divide_eq_right[symmetric] by (simp add: field_simps dot_eq_0) lemma basis_orthogonal: - fixes B :: "(real ^'n::finite) set" + fixes B :: "(real ^'n) set" assumes fB: "finite B" shows "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" (is " \C. ?P B C") @@ -3969,7 +3941,7 @@ qed lemma orthogonal_basis_exists: - fixes V :: "(real ^'n::finite) set" + fixes V :: "(real ^'n) set" shows "\B. independent B \ B \ span V \ V \ span B \ (card B = dim V) \ pairwise orthogonal B" proof- from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "card B = dim V" by blast @@ -3997,7 +3969,7 @@ lemma span_not_univ_orthogonal: assumes sU: "span S \ UNIV" - shows "\(a:: real ^'n::finite). a \0 \ (\x \ span S. a \ x = 0)" + shows "\(a:: real ^'n). a \0 \ (\x \ span S. a \ x = 0)" proof- from sU obtain a where a: "a \ span S" by blast from orthogonal_basis_exists obtain B where @@ -4036,13 +4008,13 @@ qed lemma span_not_univ_subset_hyperplane: - assumes SU: "span S \ (UNIV ::(real^'n::finite) set)" + assumes SU: "span S \ (UNIV ::(real^'n) set)" shows "\ a. a \0 \ span S \ {x. a \ x = 0}" using span_not_univ_orthogonal[OF SU] by auto lemma lowdim_subset_hyperplane: assumes d: "dim S < CARD('n::finite)" - shows "\(a::real ^'n::finite). a \ 0 \ span S \ {x. a \ x = 0}" + shows "\(a::real ^'n). a \ 0 \ span S \ {x. a \ x = 0}" proof- {assume "span S = UNIV" hence "dim (span S) = dim (UNIV :: (real ^'n) set)" by simp @@ -4058,7 +4030,7 @@ assumes lf: "linear f" and fB: "finite B" and ifB: "independent (f ` B)" and fi: "inj_on f B" and xsB: "x \ span B" - and fx: "f (x::'a::field^'n) = 0" + and fx: "f (x::'a::field^_) = 0" shows "x = 0" using fB ifB fi xsB fx proof(induct arbitrary: x rule: finite_induct[OF fB]) @@ -4193,7 +4165,7 @@ qed lemma linear_independent_extend: - assumes iB: "independent (B:: (real ^'n::finite) set)" + assumes iB: "independent (B:: (real ^'n) set)" shows "\g. linear g \ (\x\B. g x = f x)" proof- from maximal_independent_subset_extend[of B UNIV] iB @@ -4246,8 +4218,8 @@ qed lemma subspace_isomorphism: - assumes s: "subspace (S:: (real ^'n::finite) set)" - and t: "subspace (T :: (real ^ 'm::finite) set)" + assumes s: "subspace (S:: (real ^'n) set)" + and t: "subspace (T :: (real ^'m) set)" and d: "dim S = dim T" shows "\f. linear f \ f ` S = T \ inj_on f S" proof- @@ -4288,14 +4260,14 @@ (* linear functions are equal on a subspace if they are on a spanning set. *) lemma subspace_kernel: - assumes lf: "linear (f::'a::semiring_1 ^'n \ _)" + assumes lf: "linear (f::'a::semiring_1 ^_ \ _)" shows "subspace {x. f x = 0}" apply (simp add: subspace_def) by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf]) lemma linear_eq_0_span: assumes lf: "linear f" and f0: "\x\B. f x = 0" - shows "\x \ span B. f x = (0::'a::semiring_1 ^'n)" + shows "\x \ span B. f x = (0::'a::semiring_1 ^_)" proof fix x assume x: "x \ span B" let ?P = "\x. f x = 0" @@ -4305,11 +4277,11 @@ lemma linear_eq_0: assumes lf: "linear f" and SB: "S \ span B" and f0: "\x\B. f x = 0" - shows "\x \ S. f x = (0::'a::semiring_1^'n)" + shows "\x \ S. f x = (0::'a::semiring_1^_)" by (metis linear_eq_0_span[OF lf] subset_eq SB f0) lemma linear_eq: - assumes lf: "linear (f::'a::ring_1^'n \ _)" and lg: "linear g" and S: "S \ span B" + assumes lf: "linear (f::'a::ring_1^_ \ _)" and lg: "linear g" and S: "S \ span B" and fg: "\ x\ B. f x = g x" shows "\x\ S. f x = g x" proof- @@ -4320,7 +4292,7 @@ qed lemma linear_eq_stdbasis: - assumes lf: "linear (f::'a::ring_1^'m::finite \ 'a^'n::finite)" and lg: "linear g" + assumes lf: "linear (f::'a::ring_1^'m \ 'a^'n)" and lg: "linear g" and fg: "\i. f (basis i) = g(basis i)" shows "f = g" proof- @@ -4337,7 +4309,7 @@ (* Similar results for bilinear functions. *) lemma bilinear_eq: - assumes bf: "bilinear (f:: 'a::ring^'m \ 'a^'n \ 'a^'p)" + assumes bf: "bilinear (f:: 'a::ring^_ \ 'a^_ \ 'a^_)" and bg: "bilinear g" and SB: "S \ span B" and TC: "T \ span C" and fg: "\x\ B. \y\ C. f x y = g x y" @@ -4365,7 +4337,7 @@ qed lemma bilinear_eq_stdbasis: - assumes bf: "bilinear (f:: 'a::ring_1^'m::finite \ 'a^'n::finite \ 'a^'p)" + assumes bf: "bilinear (f:: 'a::ring_1^'m \ 'a^'n \ 'a^_)" and bg: "bilinear g" and fg: "\i j. f (basis i) (basis j) = g (basis i) (basis j)" shows "f = g" @@ -4377,15 +4349,15 @@ (* Detailed theorems about left and right invertibility in general case. *) lemma left_invertible_transp: - "(\(B::'a^'n^'m). B ** transp (A::'a^'n^'m) = mat (1::'a::comm_semiring_1)) \ (\(B::'a^'m^'n). A ** B = mat 1)" + "(\(B). B ** transp (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" by (metis matrix_transp_mul transp_mat transp_transp) lemma right_invertible_transp: - "(\(B::'a^'n^'m). transp (A::'a^'n^'m) ** B = mat (1::'a::comm_semiring_1)) \ (\(B::'a^'m^'n). B ** A = mat 1)" + "(\(B). transp (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(B). B ** A = mat 1)" by (metis matrix_transp_mul transp_mat transp_transp) lemma linear_injective_left_inverse: - assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" and fi: "inj f" + assumes lf: "linear (f::real ^'n \ real ^'m)" and fi: "inj f" shows "\g. linear g \ g o f = id" proof- from linear_independent_extend[OF independent_injective_image, OF independent_stdbasis, OF lf fi] @@ -4401,7 +4373,7 @@ qed lemma linear_surjective_right_inverse: - assumes lf: "linear (f:: real ^'m::finite \ real ^'n::finite)" and sf: "surj f" + assumes lf: "linear (f:: real ^'m \ real ^'n)" and sf: "surj f" shows "\g. linear g \ f o g = id" proof- from linear_independent_extend[OF independent_stdbasis] @@ -4420,7 +4392,7 @@ qed lemma matrix_left_invertible_injective: -"(\B. (B::real^'m^'n) ** (A::real^'n::finite^'m::finite) = mat 1) \ (\x y. A *v x = A *v y \ x = y)" +"(\B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x y. A *v x = A *v y \ x = y)" proof- {fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y" from xy have "B*v (A *v x) = B *v (A*v y)" by simp @@ -4439,13 +4411,13 @@ qed lemma matrix_left_invertible_ker: - "(\B. (B::real ^'m::finite^'n::finite) ** (A::real^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" + "(\B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" unfolding matrix_left_invertible_injective using linear_injective_0[OF matrix_vector_mul_linear, of A] by (simp add: inj_on_def) lemma matrix_right_invertible_surjective: -"(\B. (A::real^'n::finite^'m::finite) ** (B::real^'m^'n) = mat 1) \ surj (\x. A *v x)" +"(\B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \ surj (\x. A *v x)" proof- {fix B :: "real ^'m^'n" assume AB: "A ** B = mat 1" {fix x :: "real ^ 'm" @@ -4469,7 +4441,7 @@ qed lemma matrix_left_invertible_independent_columns: - fixes A :: "real^'n::finite^'m::finite" + fixes A :: "real^'n^'m" shows "(\(B::real ^'m^'n). B ** A = mat 1) \ (\c. setsum (\i. c i *s column i A) (UNIV :: 'n set) = 0 \ (\i. c i = 0))" (is "?lhs \ ?rhs") proof- @@ -4495,14 +4467,14 @@ qed lemma matrix_right_invertible_independent_rows: - fixes A :: "real^'n::finite^'m::finite" + fixes A :: "real^'n^'m" shows "(\(B::real^'m^'n). A ** B = mat 1) \ (\c. setsum (\i. c i *s row i A) (UNIV :: 'm set) = 0 \ (\i. c i = 0))" unfolding left_invertible_transp[symmetric] matrix_left_invertible_independent_columns by (simp add: column_transp) lemma matrix_right_invertible_span_columns: - "(\(B::real ^'n::finite^'m::finite). (A::real ^'m^'n) ** B = mat 1) \ span (columns A) = UNIV" (is "?lhs = ?rhs") + "(\(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \ span (columns A) = UNIV" (is "?lhs = ?rhs") proof- let ?U = "UNIV :: 'm set" have fU: "finite ?U" by simp @@ -4564,7 +4536,7 @@ qed lemma matrix_left_invertible_span_rows: - "(\(B::real^'m::finite^'n::finite). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" + "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" unfolding right_invertible_transp[symmetric] unfolding columns_transp[symmetric] unfolding matrix_right_invertible_span_columns @@ -4573,7 +4545,7 @@ (* An injective map real^'n->real^'n is also surjective. *) lemma linear_injective_imp_surjective: - assumes lf: "linear (f:: real ^'n::finite \ real ^'n)" and fi: "inj f" + assumes lf: "linear (f:: real ^'n \ real ^'n)" and fi: "inj f" shows "surj f" proof- let ?U = "UNIV :: (real ^'n) set" @@ -4635,7 +4607,7 @@ qed lemma linear_surjective_imp_injective: - assumes lf: "linear (f::real ^'n::finite => real ^'n)" and sf: "surj f" + assumes lf: "linear (f::real ^'n => real ^'n)" and sf: "surj f" shows "inj f" proof- let ?U = "UNIV :: (real ^'n) set" @@ -4694,14 +4666,14 @@ by (simp add: expand_fun_eq o_def id_def) lemma linear_injective_isomorphism: - assumes lf: "linear (f :: real^'n::finite \ real ^'n)" and fi: "inj f" + assumes lf: "linear (f :: real^'n \ real ^'n)" and fi: "inj f" shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)" unfolding isomorphism_expand[symmetric] using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]] linear_injective_left_inverse[OF lf fi] by (metis left_right_inverse_eq) lemma linear_surjective_isomorphism: - assumes lf: "linear (f::real ^'n::finite \ real ^'n)" and sf: "surj f" + assumes lf: "linear (f::real ^'n \ real ^'n)" and sf: "surj f" shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\x. f (f' x) = x)" unfolding isomorphism_expand[symmetric] using linear_surjective_right_inverse[OF lf sf] linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]] @@ -4710,7 +4682,7 @@ (* Left and right inverses are the same for R^N->R^N. *) lemma linear_inverse_left: - assumes lf: "linear (f::real ^'n::finite \ real ^'n)" and lf': "linear f'" + assumes lf: "linear (f::real ^'n \ real ^'n)" and lf': "linear f'" shows "f o f' = id \ f' o f = id" proof- {fix f f':: "real ^'n \ real ^'n" @@ -4728,7 +4700,7 @@ (* Moreover, a one-sided inverse is automatically linear. *) lemma left_inverse_linear: - assumes lf: "linear (f::real ^'n::finite \ real ^'n)" and gf: "g o f = id" + assumes lf: "linear (f::real ^'n \ real ^'n)" and gf: "g o f = id" shows "linear g" proof- from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def stupid_ext[symmetric]) @@ -4743,7 +4715,7 @@ qed lemma right_inverse_linear: - assumes lf: "linear (f:: real ^'n::finite \ real ^'n)" and gf: "f o g = id" + assumes lf: "linear (f:: real ^'n \ real ^'n)" and gf: "f o g = id" shows "linear g" proof- from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def stupid_ext[symmetric]) @@ -4760,7 +4732,7 @@ (* The same result in terms of square matrices. *) lemma matrix_left_right_inverse: - fixes A A' :: "real ^'n::finite^'n" + fixes A A' :: "real ^'n^'n" shows "A ** A' = mat 1 \ A' ** A = mat 1" proof- {fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1" @@ -4798,11 +4770,11 @@ "columnvector (A *v v) = A ** columnvector v" by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) -lemma dot_matrix_product: "(x::'a::semiring_1^'n::finite) \ y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1" +lemma dot_matrix_product: "(x::'a::semiring_1^'n) \ y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1" by (vector matrix_matrix_mult_def rowvector_def columnvector_def dot_def) lemma dot_matrix_vector_mul: - fixes A B :: "real ^'n::finite ^'n" and x y :: "real ^'n" + fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" shows "(A *v x) \ (B *v y) = (((rowvector x :: real^'n^1) ** ((transp A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" unfolding dot_matrix_product transp_columnvector[symmetric] @@ -4810,28 +4782,28 @@ (* Infinity norm. *) -definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\ (UNIV :: 'n set)}" +definition "infnorm (x::real^'n) = Sup {abs(x$i) |i. i\ (UNIV :: 'n set)}" lemma numseg_dimindex_nonempty: "\i. i \ (UNIV :: 'n set)" by auto lemma infnorm_set_image: - "{abs(x$i) |i. i\ (UNIV :: 'n set)} = - (\i. abs(x$i)) ` (UNIV :: 'n set)" by blast + "{abs(x$i) |i. i\ (UNIV :: _ set)} = + (\i. abs(x$i)) ` (UNIV)" by blast lemma infnorm_set_lemma: - shows "finite {abs((x::'a::abs ^'n::finite)$i) |i. i\ (UNIV :: 'n set)}" + shows "finite {abs((x::'a::abs ^'n)$i) |i. i\ (UNIV :: 'n set)}" and "{abs(x$i) |i. i\ (UNIV :: 'n::finite set)} \ {}" unfolding infnorm_set_image by (auto intro: finite_imageI) -lemma infnorm_pos_le: "0 \ infnorm (x::real^'n::finite)" +lemma infnorm_pos_le: "0 \ infnorm (x::real^'n)" unfolding infnorm_def unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma] unfolding infnorm_set_image by auto -lemma infnorm_triangle: "infnorm ((x::real^'n::finite) + y) \ infnorm x + infnorm y" +lemma infnorm_triangle: "infnorm ((x::real^'n) + y) \ infnorm x + infnorm y" proof- have th: "\x y (z::real). x - y <= z \ x - z <= y" by arith have th1: "\S f. f ` S = { f i| i. i \ S}" by blast @@ -4852,7 +4824,7 @@ done qed -lemma infnorm_eq_0: "infnorm x = 0 \ (x::real ^'n::finite) = 0" +lemma infnorm_eq_0: "infnorm x = 0 \ (x::real ^'n) = 0" proof- have "infnorm x <= 0 \ x = 0" unfolding infnorm_def @@ -4894,7 +4866,7 @@ using infnorm_pos_le[of x] by arith lemma component_le_infnorm: - shows "\x$i\ \ infnorm (x::real^'n::finite)" + shows "\x$i\ \ infnorm (x::real^'n)" proof- let ?U = "UNIV :: 'n set" let ?S = "{\x$i\ |i. i\ ?U}" @@ -4947,7 +4919,7 @@ unfolding infnorm_set_image ball_simps by (metis component_le_norm) lemma card_enum: "card {1 .. n} = n" by auto -lemma norm_le_infnorm: "norm(x) <= sqrt(real CARD('n)) * infnorm(x::real ^'n::finite)" +lemma norm_le_infnorm: "norm(x) <= sqrt(real CARD('n)) * infnorm(x::real ^'n)" proof- let ?d = "CARD('n)" have "real ?d \ 0" by simp @@ -4973,7 +4945,7 @@ (* Equality in Cauchy-Schwarz and triangle inequalities. *) -lemma norm_cauchy_schwarz_eq: "(x::real ^'n::finite) \ y = norm x * norm y \ norm x *s y = norm y *s x" (is "?lhs \ ?rhs") +lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \ y = norm x * norm y \ norm x *s y = norm y *s x" (is "?lhs \ ?rhs") proof- {assume h: "x = 0" hence ?thesis by simp} @@ -5000,7 +4972,7 @@ qed lemma norm_cauchy_schwarz_abs_eq: - fixes x y :: "real ^ 'n::finite" + fixes x y :: "real ^ 'n" shows "abs(x \ y) = norm x * norm y \ norm x *s y = norm y *s x \ norm(x) *s y = - norm y *s x" (is "?lhs \ ?rhs") proof- @@ -5019,7 +4991,7 @@ qed lemma norm_triangle_eq: - fixes x y :: "real ^ 'n::finite" + fixes x y :: "real ^ 'n" shows "norm(x + y) = norm x + norm y \ norm x *s y = norm y *s x" proof- {assume x: "x =0 \ y =0" @@ -5049,12 +5021,12 @@ lemma collinear_empty: "collinear {}" by (simp add: collinear_def) -lemma collinear_sing: "collinear {(x::'a::ring_1^'n)}" +lemma collinear_sing: "collinear {(x::'a::ring_1^_)}" apply (simp add: collinear_def) apply (rule exI[where x=0]) by simp -lemma collinear_2: "collinear {(x::'a::ring_1^'n),y}" +lemma collinear_2: "collinear {(x::'a::ring_1^_),y}" apply (simp add: collinear_def) apply (rule exI[where x="x - y"]) apply auto @@ -5064,7 +5036,7 @@ apply (rule exI[where x=0], simp) done -lemma collinear_lemma: "collinear {(0::real^'n),x,y} \ x = 0 \ y = 0 \ (\c. y = c *s x)" (is "?lhs \ ?rhs") +lemma collinear_lemma: "collinear {(0::real^_),x,y} \ x = 0 \ y = 0 \ (\c. y = c *s x)" (is "?lhs \ ?rhs") proof- {assume "x=0 \ y = 0" hence ?thesis by (cases "x = 0", simp_all add: collinear_2 insert_commute)} @@ -5099,7 +5071,7 @@ qed lemma norm_cauchy_schwarz_equal: - fixes x y :: "real ^ 'n::finite" + fixes x y :: "real ^ 'n" shows "abs(x \ y) = norm x * norm y \ collinear {(0::real^'n),x,y}" unfolding norm_cauchy_schwarz_abs_eq apply (cases "x=0", simp_all add: collinear_2) diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Jan 08 14:07:07 2010 +0100 @@ -11,29 +11,46 @@ subsection {* Finite Cartesian products, with indexing and lambdas. *} typedef (open Cart) - ('a, 'b) "^" (infixl "^" 15) - = "UNIV :: ('b \ 'a) set" + ('a, 'b) cart = "UNIV :: (('b::finite) \ 'a) set" morphisms Cart_nth Cart_lambda .. notation Cart_nth (infixl "$" 90) notation (xsymbols) Cart_lambda (binder "\" 10) +(* + Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than + the finite type class write "cart 'b 'n" +*) + +syntax "_finite_cart" :: "type \ type \ type" ("(_ ^/ _)" [15, 16] 15) + +parse_translation {* +let + fun cart t u = Syntax.const @{type_name cart} $ t $ u + fun finite_cart_tr [t, u as Free (x, _)] = + if Syntax.is_tid x + then cart t (Syntax.const "_ofsort" $ u $ Syntax.const (hd @{sort finite})) + else cart t u + | finite_cart_tr [t, u] = cart t u +in + [("_finite_cart", finite_cart_tr)] +end +*} + lemma stupid_ext: "(\x. f x = g x) \ (f = g)" apply auto apply (rule ext) apply auto done -lemma Cart_eq: "((x:: 'a ^ 'b) = y) \ (\i. x$i = y$i)" +lemma Cart_eq: "(x = y) \ (\i. x$i = y$i)" by (simp add: Cart_nth_inject [symmetric] expand_fun_eq) lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" by (simp add: Cart_lambda_inverse) -lemma Cart_lambda_unique: - fixes f :: "'a ^ 'b" - shows "(\i. f$i = g i) \ Cart_lambda g = f" +lemma Cart_lambda_unique: "(\i. f$i = g i) \ Cart_lambda g = f" by (auto simp add: Cart_eq) lemma Cart_lambda_eta: "(\ i. (g$i)) = g" @@ -41,14 +58,9 @@ text{* A non-standard sum to "paste" Cartesian products. *} -definition pastecart :: "'a ^ 'm \ 'a ^ 'n \ 'a ^ ('m + 'n)" where - "pastecart f g = (\ i. case i of Inl a \ f$a | Inr b \ g$b)" - -definition fstcart:: "'a ^('m + 'n) \ 'a ^ 'm" where - "fstcart f = (\ i. (f$(Inl i)))" - -definition sndcart:: "'a ^('m + 'n) \ 'a ^ 'n" where - "sndcart f = (\ i. (f$(Inr i)))" +definition "pastecart f g = (\ i. case i of Inl a \ f$a | Inr b \ g$b)" +definition "fstcart f = (\ i. (f$(Inl i)))" +definition "sndcart f = (\ i. (f$(Inr i)))" lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" unfolding pastecart_def by simp @@ -65,10 +77,10 @@ lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \ range Inr" by (auto, case_tac x, auto) -lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = x" +lemma fstcart_pastecart: "fstcart (pastecart x y) = x" by (simp add: Cart_eq) -lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m ) (y:: 'a ^ 'n)) = y" +lemma sndcart_pastecart: "sndcart (pastecart x y) = y" by (simp add: Cart_eq) lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z" diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jan 08 14:07:07 2010 +0100 @@ -532,7 +532,7 @@ apply (auto simp add: dist_norm) done -instance "^" :: (perfect_space, finite) perfect_space +instance cart :: (perfect_space, finite) perfect_space proof fix x :: "'a ^ 'b" { @@ -565,7 +565,7 @@ lemma islimpt_EMPTY[simp]: "\ x islimpt {}" unfolding islimpt_def by auto -lemma closed_positive_orthant: "closed {x::real^'n::finite. \i. 0 \x$i}" +lemma closed_positive_orthant: "closed {x::real^'n. \i. 0 \x$i}" proof- let ?U = "UNIV :: 'n set" let ?O = "{x::real^'n. \i. x$i\0}" @@ -1296,7 +1296,7 @@ qed lemma Lim_component: - fixes f :: "'a \ 'b::metric_space ^ 'n::finite" + fixes f :: "'a \ 'b::metric_space ^ 'n" shows "(f ---> l) net \ ((\a. f a $i) ---> l$i) net" unfolding tendsto_iff apply (clarify) @@ -2284,7 +2284,7 @@ done lemma compact_lemma: - fixes f :: "nat \ 'a::heine_borel ^ 'n::finite" + fixes f :: "nat \ 'a::heine_borel ^ 'n" assumes "bounded s" and "\n. f n \ s" shows "\d. \l r. subseq r \ @@ -2317,7 +2317,7 @@ qed qed -instance "^" :: (heine_borel, finite) heine_borel +instance cart :: (heine_borel, finite) heine_borel proof fix s :: "('a ^ 'b) set" and f :: "nat \ 'a ^ 'b" assume s: "bounded s" and f: "\n. f n \ s" @@ -4283,7 +4283,7 @@ qed lemma closed_pastecart: - fixes s :: "(real ^ 'a::finite) set" (* FIXME: generalize *) + fixes s :: "(real ^ 'a) set" (* FIXME: generalize *) assumes "closed s" "closed t" shows "closed {pastecart x y | x y . x \ s \ y \ t}" proof- @@ -4623,12 +4623,12 @@ (* A cute way of denoting open and closed intervals using overloading. *) -lemma interval: fixes a :: "'a::ord^'n::finite" shows +lemma interval: fixes a :: "'a::ord^'n" shows "{a <..< b} = {x::'a^'n. \i. a$i < x$i \ x$i < b$i}" and "{a .. b} = {x::'a^'n. \i. a$i \ x$i \ x$i \ b$i}" by (auto simp add: expand_set_eq vector_less_def vector_le_def) -lemma mem_interval: fixes a :: "'a::ord^'n::finite" shows +lemma mem_interval: fixes a :: "'a::ord^'n" shows "x \ {a<.. (\i. a$i < x$i \ x$i < b$i)" "x \ {a .. b} \ (\i. a$i \ x$i \ x$i \ b$i)" using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def) @@ -4647,7 +4647,7 @@ apply(rule_tac x="dest_vec1 x" in bexI) by auto -lemma interval_eq_empty: fixes a :: "real^'n::finite" shows +lemma interval_eq_empty: fixes a :: "real^'n" shows "({a <..< b} = {} \ (\i. b$i \ a$i))" (is ?th1) and "({a .. b} = {} \ (\i. b$i < a$i))" (is ?th2) proof- @@ -4682,12 +4682,12 @@ ultimately show ?th2 by blast qed -lemma interval_ne_empty: fixes a :: "real^'n::finite" shows +lemma interval_ne_empty: fixes a :: "real^'n" shows "{a .. b} \ {} \ (\i. a$i \ b$i)" and "{a <..< b} \ {} \ (\i. a$i < b$i)" unfolding interval_eq_empty[of a b] by (auto simp add: not_less not_le) (* BH: Why doesn't just "auto" work here? *) -lemma subset_interval_imp: fixes a :: "real^'n::finite" shows +lemma subset_interval_imp: fixes a :: "real^'n" shows "(\i. a$i \ c$i \ d$i \ b$i) \ {c .. d} \ {a .. b}" and "(\i. a$i < c$i \ d$i < b$i) \ {c .. d} \ {a<..i. a$i \ c$i \ d$i \ b$i) \ {c<.. {a .. b}" and @@ -4695,14 +4695,14 @@ unfolding subset_eq[unfolded Ball_def] unfolding mem_interval by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *) -lemma interval_sing: fixes a :: "'a::linorder^'n::finite" shows +lemma interval_sing: fixes a :: "'a::linorder^'n" shows "{a .. a} = {a} \ {a<.. {a .. b}" proof(simp add: subset_eq, rule) fix x @@ -4723,7 +4723,7 @@ by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq) qed -lemma subset_interval: fixes a :: "real^'n::finite" shows +lemma subset_interval: fixes a :: "real^'n" shows "{c .. d} \ {a .. b} \ (\i. c$i \ d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th1) and "{c .. d} \ {a<.. (\i. c$i \ d$i) --> (\i. a$i < c$i \ d$i < b$i)" (is ?th2) and "{c<.. {a .. b} \ (\i. c$i < d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th3) and @@ -4775,7 +4775,7 @@ thus ?th4 unfolding subset_eq and Ball_def and mem_interval apply auto apply (erule_tac x=ia in allE, simp)+ by (erule_tac x=i in allE, erule_tac x=i in allE, simp)+ qed -lemma disjoint_interval: fixes a::"real^'n::finite" shows +lemma disjoint_interval: fixes a::"real^'n" shows "{a .. b} \ {c .. d} = {} \ (\i. (b$i < a$i \ d$i < c$i \ b$i < c$i \ d$i < a$i))" (is ?th1) and "{a .. b} \ {c<.. (\i. (b$i < a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th2) and "{a<.. {c .. d} = {} \ (\i. (b$i \ a$i \ d$i < c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th3) and @@ -4789,7 +4789,7 @@ done qed -lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows +lemma inter_interval: fixes a :: "'a::linorder^'n" shows "{a .. b} \ {c .. d} = {(\ i. max (a$i) (c$i)) .. (\ i. min (b$i) (d$i))}" unfolding expand_set_eq and Int_iff and mem_interval by (auto simp add: less_divide_eq_number_of1 intro!: bexI) @@ -4800,7 +4800,7 @@ "a < x \ x < b ==> (\d>0. \x'. abs(x' - x) < d --> a < x' \ x' < b)" by(rule_tac x="min (x - a) (b - x)" in exI, auto) -lemma open_interval: fixes a :: "real^'n::finite" shows "open {a<..{a<..e>0. \x'\{a..b}. x' \ x \ dist x' x < e"(* and xab:"a$i > x$i \ b$i < x$i"*) { assume xa:"a$i > x$i" @@ -4853,7 +4853,7 @@ thus ?thesis unfolding closed_limpt islimpt_approachable mem_interval by auto qed -lemma interior_closed_interval: fixes a :: "real^'n::finite" shows +lemma interior_closed_interval: fixes a :: "real^'n" shows "interior {a .. b} = {a<.. ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto @@ -4878,7 +4878,7 @@ thus "?L \ ?R" unfolding interior_def and subset_eq by auto qed -lemma bounded_closed_interval: fixes a :: "real^'n::finite" shows +lemma bounded_closed_interval: fixes a :: "real^'n" shows "bounded {a .. b}" proof- let ?b = "\i\UNIV. \a$i\ + \b$i\" @@ -4890,23 +4890,23 @@ thus ?thesis unfolding interval and bounded_iff by auto qed -lemma bounded_interval: fixes a :: "real^'n::finite" shows +lemma bounded_interval: fixes a :: "real^'n" shows "bounded {a .. b} \ bounded {a<.. UNIV) \ ({a<.. UNIV)" using bounded_interval[of a b] by auto -lemma compact_interval: fixes a :: "real^'n::finite" shows +lemma compact_interval: fixes a :: "real^'n" shows "compact {a .. b}" using bounded_closed_imp_compact using bounded_interval[of a b] using closed_interval[of a b] by auto -lemma open_interval_midpoint: fixes a :: "real^'n::finite" +lemma open_interval_midpoint: fixes a :: "real^'n" assumes "{a<.. {}" shows "((1/2) *\<^sub>R (a + b)) \ {a<.. {a<.. {a .. b}" and e:"0 < e" "e \ 1" shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \ {a<.. {}" shows "closure {a<..a. s \ {-a<..0" and b:"\x\s. norm x \ b" using assms[unfolded bounded_pos] by auto @@ -4987,12 +4987,12 @@ qed lemma bounded_subset_open_interval: - fixes s :: "(real ^ 'n::finite) set" + fixes s :: "(real ^ 'n) set" shows "bounded s ==> (\a b. s \ {a<..a. s \ {-a .. a}" proof- obtain a where "s \ {- a<.. (\a b. s \ {a .. b})" using bounded_subset_closed_interval_symmetric[of s] by auto @@ -5018,7 +5018,7 @@ case False thus ?thesis unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_interval] by auto qed -lemma inter_interval_mixed_eq_empty: fixes a :: "real^'n::finite" +lemma inter_interval_mixed_eq_empty: fixes a :: "real^'n" assumes "{c<.. {}" shows "{a<.. {c .. d} = {} \ {a<.. {c<..i. x$i \ b$i}" proof- { fix i @@ -5093,7 +5093,7 @@ thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast qed -lemma closed_interval_right: fixes a::"real^'n::finite" +lemma closed_interval_right: fixes a::"real^'n" shows "closed {x::real^'n. \i. a$i \ x$i}" proof- { fix i @@ -5109,7 +5109,7 @@ definition "is_interval s \ (\a\s. \b\s. \x. (\i. ((a$i \ x$i \ x$i \ b$i) \ (b$i \ x$i \ x$i \ a$i))) \ x \ s)" -lemma is_interval_interval: "is_interval {a .. b::real^'n::finite}" (is ?th1) "is_interval {a<..x y z::real. x < y \ y < z \ x < z" by auto show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff by(meson real_le_trans le_less_trans less_le_trans *)+ qed @@ -5158,11 +5158,11 @@ qed lemma closed_halfspace_component_le: - shows "closed {x::real^'n::finite. x$i \ a}" + shows "closed {x::real^'n. x$i \ a}" using closed_halfspace_le[of "(basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto lemma closed_halfspace_component_ge: - shows "closed {x::real^'n::finite. x$i \ a}" + shows "closed {x::real^'n. x$i \ a}" using closed_halfspace_ge[of a "(basis i)::real^'n"] unfolding inner_basis[OF assms] by auto text{* Openness of halfspaces. *} @@ -5180,16 +5180,16 @@ qed lemma open_halfspace_component_lt: - shows "open {x::real^'n::finite. x$i < a}" + shows "open {x::real^'n. x$i < a}" using open_halfspace_lt[of "(basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto lemma open_halfspace_component_gt: - shows "open {x::real^'n::finite. x$i > a}" + shows "open {x::real^'n. x$i > a}" using open_halfspace_gt[of a "(basis i)::real^'n"] unfolding inner_basis[OF assms] by auto text{* This gives a simple derivation of limit component bounds. *} -lemma Lim_component_le: fixes f :: "'a \ real^'n::finite" +lemma Lim_component_le: fixes f :: "'a \ real^'n" assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. f(x)$i \ b) net" shows "l$i \ b" proof- @@ -5198,7 +5198,7 @@ using closed_halfspace_le[of "(basis i)::real^'n" b] and assms(1,2,3) by auto qed -lemma Lim_component_ge: fixes f :: "'a \ real^'n::finite" +lemma Lim_component_ge: fixes f :: "'a \ real^'n" assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)$i) net" shows "b \ l$i" proof- @@ -5207,7 +5207,7 @@ using closed_halfspace_ge[of b "(basis i)::real^'n"] and assms(1,2,3) by auto qed -lemma Lim_component_eq: fixes f :: "'a \ real^'n::finite" +lemma Lim_component_eq: fixes f :: "'a \ real^'n" assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\x. f(x)$i = b) net" shows "l$i = b" using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto @@ -5270,7 +5270,7 @@ ultimately show False using assms(1)[unfolded connected_def not_ex, THEN spec[where x="?A"], THEN spec[where x="?B"]] and assms(2-5) by auto qed -lemma connected_ivt_component: fixes x::"real^'n::finite" shows +lemma connected_ivt_component: fixes x::"real^'n" shows "connected s \ x \ s \ y \ s \ x$k \ a \ a \ y$k \ (\z\s. z$k = a)" using connected_ivt_hyperplane[of s x y "(basis k)::real^'n" a] by (auto simp add: inner_basis) @@ -5456,7 +5456,7 @@ text{* "Isometry" (up to constant bounds) of injective linear map etc. *} lemma cauchy_isometric: - fixes x :: "nat \ real ^ 'n::finite" + fixes x :: "nat \ real ^ 'n" 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- @@ -5499,7 +5499,7 @@ shows "dist 0 x = norm x" unfolding dist_norm by simp -lemma injective_imp_isometric: fixes f::"real^'m::finite \ real^'n::finite" +lemma injective_imp_isometric: fixes f::"real^'m \ real^'n" 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}") @@ -5563,11 +5563,11 @@ subsection{* Some properties of a canonical subspace. *} lemma subspace_substandard: - "subspace {x::real^'n. (\i. P i \ x$i = 0)}" + "subspace {x::real^_. (\i. P i \ x$i = 0)}" unfolding subspace_def by(auto simp add: vector_add_component vector_smult_component elim!: ballE) lemma closed_substandard: - "closed {x::real^'n::finite. \i. P i --> x$i = 0}" (is "closed ?A") + "closed {x::real^'n. \i. P i --> x$i = 0}" (is "closed ?A") proof- let ?D = "{i. P i}" let ?Bs = "{{x::real^'n. inner (basis i) x = 0}| i. i \ ?D}" @@ -5587,7 +5587,7 @@ qed lemma dim_substandard: - shows "dim {x::real^'n::finite. \i. i \ d \ x$i = 0} = card d" (is "dim ?A = _") + shows "dim {x::real^'n. \i. i \ d \ x$i = 0} = card d" (is "dim ?A = _") proof- let ?D = "UNIV::'n set" let ?B = "(basis::'n\real^'n) ` d" @@ -5653,7 +5653,7 @@ apply (subgoal_tac "A \ UNIV", auto) done -lemma closed_subspace: fixes s::"(real^'n::finite) set" +lemma closed_subspace: fixes s::"(real^'n) set" assumes "subspace s" shows "closed s" proof- have "dim s \ card (UNIV :: 'n set)" using dim_subset_univ by auto @@ -5742,7 +5742,7 @@ by metis lemma image_affinity_interval: fixes m::real - fixes a b c :: "real^'n::finite" + fixes a b c :: "real^'n" shows "(\x. m *\<^sub>R x + c) ` {a .. b} = (if {a .. b} = {} then {} else (if 0 \ m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} @@ -5780,7 +5780,7 @@ ultimately show ?thesis using False by auto qed -lemma image_smult_interval:"(\x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} = +lemma image_smult_interval:"(\x. m *\<^sub>R (x::real^'n)) ` {a..b} = (if {a..b} = {} then {} else if 0 \ m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})" using image_affinity_interval[of m 0 a b] by auto diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Jan 08 14:07:07 2010 +0100 @@ -1629,7 +1629,7 @@ (KK.Atom j0) KK.None) | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u])) | Construct ([u'], _, _, []) => to_r u' - | Construct (_ :: sel_us, T, R, arg_us) => + | Construct (discr_u :: sel_us, T, R, arg_us) => let val set_rs = map2 (fn sel_u => fn arg_u => @@ -1642,8 +1642,7 @@ kk_n_fold_join kk true R2 R1 arg_r (kk_project sel_r (flip_nums (arity_of_rep R2))) else - kk_comprehension - (decls_for_atom_schema ~1 (atom_schema_of_rep R1)) + kk_comprehension [KK.DeclOne ((1, ~1), to_r discr_u)] (kk_rel_eq (kk_join (KK.Var (1, ~1)) sel_r) arg_r) end) sel_us arg_us in fold1 kk_intersect set_rs end diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Jan 08 14:07:07 2010 +0100 @@ -746,7 +746,9 @@ (vs, table) = let val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n - val R' = if n = ~1 orelse is_word_type (body_type T) then + val R' = if n = ~1 orelse is_word_type (body_type T) + orelse (is_fun_type (range_type T') + andalso is_boolean_type (body_type T')) then best_non_opt_set_rep_for_type scope T' else best_opt_set_rep_for_type scope T' |> unopt_rep diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Jan 08 12:25:15 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Jan 08 14:07:07 2010 +0100 @@ -322,7 +322,7 @@ (* string -> unit *) fun run_test name = - case Kodkod.solve_any_problem true NONE 0 1 + case Kodkod.solve_any_problem false NONE 0 1 [problem_for_nut @{context} name (the (AList.lookup (op =) tests name))] of Kodkod.Normal ([], _) => () diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Fri Jan 08 12:25:15 2010 +0100 +++ b/src/Pure/Concurrent/future.ML Fri Jan 08 14:07:07 2010 +0100 @@ -23,6 +23,10 @@ of runtime resources is distorted either if workers yield CPU time (e.g. via system sleep or wait operations), or if non-worker threads contend for significant runtime resources independently. + + * Promised futures are fulfilled by external means. There is no + associated evaluation task, but other futures can depend on them + as usual. *) signature FUTURE = @@ -37,7 +41,6 @@ val group_of: 'a future -> group val peek: 'a future -> 'a Exn.result option val is_finished: 'a future -> bool - val value: 'a -> 'a future val fork_group: group -> (unit -> 'a) -> 'a future val fork_deps_pri: 'b future list -> int -> (unit -> 'a) -> 'a future val fork_deps: 'b future list -> (unit -> 'a) -> 'a future @@ -46,7 +49,12 @@ val join_results: 'a future list -> 'a Exn.result list val join_result: 'a future -> 'a Exn.result val join: 'a future -> 'a + val value: 'a -> 'a future val map: ('a -> 'b) -> 'a future -> 'b future + val promise_group: group -> 'a future + val promise: unit -> 'a future + val fulfill_result: 'a future -> 'a Exn.result -> unit + val fulfill: 'a future -> 'a -> unit val interruptible_task: ('a -> 'b) -> 'a -> 'b val cancel_group: group -> unit val cancel: 'a future -> unit @@ -75,11 +83,14 @@ val worker_task = Option.map #1 o thread_data; val worker_group = Option.map #2 o thread_data; +fun new_group () = Task_Queue.new_group (worker_group ()); + (* datatype future *) datatype 'a future = Future of - {task: task, + {promised: bool, + task: task, group: group, result: 'a Exn.result option Synchronized.var}; @@ -90,10 +101,14 @@ fun peek x = Synchronized.value (result_of x); fun is_finished x = is_some (peek x); -fun value x = Future - {task = Task_Queue.new_task 0, - group = Task_Queue.new_group NONE, - result = Synchronized.var "future" (SOME (Exn.Result x))}; +fun assign_result group result res = + let + val _ = Synchronized.assign result (K (SOME res)); + val ok = + (case res of + Exn.Exn exn => (Task_Queue.cancel_group group exn; false) + | Exn.Result _ => true); + in ok end; @@ -160,15 +175,13 @@ Exn.capture (fn () => Multithreading.with_attributes Multithreading.private_interrupts (fn _ => e ())) () else Exn.Exn Exn.Interrupt; - val _ = Synchronized.assign result (K (SOME res)); - in - (case res of - Exn.Exn exn => (Task_Queue.cancel_group group exn; false) - | Exn.Result _ => true) - end; + in assign_result group result res end; in (result, job) end; -fun do_cancel group = (*requires SYNCHRONIZED*) +fun cancel_now group = (*requires SYNCHRONIZED*) + Task_Queue.cancel (! queue) group; + +fun cancel_later group = (*requires SYNCHRONIZED*) (Unsynchronized.change canceled (insert Task_Queue.eq_group group); broadcast scheduler_event); @@ -182,8 +195,8 @@ val maximal = Unsynchronized.change_result queue (Task_Queue.finish task); val _ = if ok then () - else if Task_Queue.cancel (! queue) group then () - else do_cancel group; + else if cancel_now group then () + else cancel_later group; val _ = broadcast work_finished; val _ = if maximal then () else signal work_available; in () end); @@ -247,7 +260,7 @@ if tick andalso ! status_ticks = 0 then Multithreading.tracing 1 (fn () => let - val {ready, pending, running} = Task_Queue.status (! queue); + val {ready, pending, running, passive} = Task_Queue.status (! queue); val total = length (! workers); val active = count_workers Working; val waiting = count_workers Waiting; @@ -255,7 +268,8 @@ "SCHEDULE " ^ Time.toString now ^ ": " ^ string_of_int ready ^ " ready, " ^ string_of_int pending ^ " pending, " ^ - string_of_int running ^ " running; " ^ + string_of_int running ^ " running, " ^ + string_of_int passive ^ " passive; " ^ string_of_int total ^ " workers, " ^ string_of_int active ^ " active, " ^ string_of_int waiting ^ " waiting " @@ -318,7 +332,7 @@ else (Multithreading.tracing 1 (fn () => string_of_int (length (! canceled)) ^ " canceled groups"); - Unsynchronized.change canceled (filter_out (Task_Queue.cancel (! queue))); + Unsynchronized.change canceled (filter_out cancel_now); broadcast_work ()); @@ -329,7 +343,7 @@ (* shutdown *) - val _ = if Task_Queue.is_empty (! queue) then do_shutdown := true else (); + val _ = if Task_Queue.all_passive (! queue) then do_shutdown := true else (); val continue = not (! do_shutdown andalso null (! workers)); val _ = if continue then () else scheduler := NONE; @@ -337,7 +351,8 @@ in continue end handle Exn.Interrupt => (Multithreading.tracing 1 (fn () => "Interrupt"); - List.app do_cancel (Task_Queue.cancel_all (! queue)); true); + List.app cancel_later (Task_Queue.cancel_all (! queue)); + broadcast_work (); true); fun scheduler_loop () = while @@ -364,8 +379,8 @@ let val group = (case opt_group of - SOME group => group - | NONE => Task_Queue.new_group (worker_group ())); + NONE => new_group () + | SOME group => group); val (result, job) = future_job group e; val task = SYNCHRONIZED "enqueue" (fn () => let @@ -374,7 +389,7 @@ val _ = if minimal then signal work_available else (); val _ = scheduler_check (); in task end); - in Future {task = task, group = group, result = result} end; + in Future {promised = false, task = task, group = group, result = result} end; fun fork_group group e = fork_future (SOME group) [] 0 e; fun fork_deps_pri deps pri e = fork_future NONE (map task_of deps) pri e; @@ -432,7 +447,14 @@ fun join x = Exn.release (join_result x); -(* map *) +(* fast-path versions -- bypassing full task management *) + +fun value (x: 'a) = + let + val group = Task_Queue.new_group NONE; + val result = Synchronized.var "value" NONE : 'a Exn.result option Synchronized.var; + val _ = assign_result group result (Exn.Result x); + in Future {promised = false, task = Task_Queue.dummy_task, group = group, result = result} end; fun map_future f x = let @@ -445,11 +467,32 @@ SOME queue' => (queue := queue'; true) | NONE => false)); in - if extended then Future {task = task, group = group, result = result} + if extended then Future {promised = false, task = task, group = group, result = result} else fork_future (SOME group) [task] (Task_Queue.pri_of_task task) (fn () => f (join x)) end; +(* promised futures -- fulfilled by external means *) + +fun promise_group group : 'a future = + let + val result = Synchronized.var "promise" (NONE: 'a Exn.result option); + val task = SYNCHRONIZED "enqueue" (fn () => + Unsynchronized.change_result queue (Task_Queue.enqueue_passive group)); + in Future {promised = true, task = task, group = group, result = result} end; + +fun promise () = promise_group (new_group ()); + +fun fulfill_result (Future {promised, task, group, result}) res = + let + val _ = promised orelse raise Fail "Not a promised future"; + fun job ok = assign_result group result (if ok then res else Exn.Exn Exn.Interrupt); + val _ = execute (task, group, [job]); + in () end; + +fun fulfill x res = fulfill_result x (Exn.Result res); + + (* cancellation *) fun interruptible_task f x = @@ -462,7 +505,8 @@ else interruptible f x; (*cancel: present and future group members will be interrupted eventually*) -fun cancel_group group = SYNCHRONIZED "cancel" (fn () => do_cancel group); +fun cancel_group group = + SYNCHRONIZED "cancel" (fn () => if cancel_now group then () else cancel_later group); fun cancel x = cancel_group (group_of x); diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/Pure/Concurrent/lazy.ML --- a/src/Pure/Concurrent/lazy.ML Fri Jan 08 12:25:15 2010 +0100 +++ b/src/Pure/Concurrent/lazy.ML Fri Jan 08 14:07:07 2010 +0100 @@ -1,7 +1,9 @@ (* Title: Pure/Concurrent/lazy.ML Author: Makarius -Lazy evaluation based on futures. +Lazy evaluation with memoing of results and regular exceptions. +Parallel version based on futures -- avoids critical or multiple +evaluation, unless interrupted. *) signature LAZY = @@ -21,30 +23,46 @@ datatype 'a expr = Expr of unit -> 'a | - Future of 'a future; + Result of 'a; -abstype 'a lazy = Lazy of 'a expr Synchronized.var +abstype 'a lazy = Lazy of 'a expr future Synchronized.var with fun peek (Lazy var) = - (case Synchronized.value var of - Expr _ => NONE - | Future x => Future.peek x); + (case Future.peek (Synchronized.value var) of + NONE => NONE + | SOME (Exn.Result (Expr _)) => NONE + | SOME (Exn.Result (Result x)) => SOME (Exn.Result x) + | SOME (Exn.Exn exn) => SOME (Exn.Exn exn)); -fun lazy e = Lazy (Synchronized.var "lazy" (Expr e)); -fun value a = Lazy (Synchronized.var "lazy" (Future (Future.value a))); +fun lazy e = Lazy (Synchronized.var "lazy" (Future.value (Expr e))); +fun value a = Lazy (Synchronized.var "lazy" (Future.value (Result a))); (* force result *) +fun fork e = + let val x = Future.fork (fn () => Result (e ()) handle Exn.Interrupt => Expr e) + in (x, x) end; + fun force_result (Lazy var) = (case peek (Lazy var) of SOME res => res | NONE => - Synchronized.guarded_access var - (fn Expr e => let val x = Future.fork e in SOME (x, Future x) end - | Future x => SOME (x, Future x)) - |> Future.join_result); + let + val result = + Synchronized.change_result var + (fn x => + (case Future.peek x of + SOME (Exn.Result (Expr e)) => fork e + | _ => (x, x))) + |> Future.join_result; + in + case result of + Exn.Result (Expr _) => Exn.Exn Exn.Interrupt + | Exn.Result (Result x) => Exn.Result x + | Exn.Exn exn => Exn.Exn exn + end); fun force r = Exn.release (force_result r); diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/Pure/Concurrent/lazy_sequential.ML --- a/src/Pure/Concurrent/lazy_sequential.ML Fri Jan 08 12:25:15 2010 +0100 +++ b/src/Pure/Concurrent/lazy_sequential.ML Fri Jan 08 14:07:07 2010 +0100 @@ -1,7 +1,8 @@ (* Title: Pure/Concurrent/lazy_sequential.ML Author: Florian Haftmann and Makarius, TU Muenchen -Lazy evaluation with memoing (sequential version). +Lazy evaluation with memoing of results and regular exceptions +(sequential version). *) structure Lazy: LAZY = @@ -28,9 +29,16 @@ (* force result *) fun force_result (Lazy r) = - (case ! r of - Expr e => Exn.capture e () - | Result res => res); + let + val result = + (case ! r of + Expr e => Exn.capture e () + | Result res => res); + val _ = + (case result of + Exn.Exn Exn.Interrupt => () + | _ => r := Result result); + in result end; fun force r = Exn.release (force_result r); diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Fri Jan 08 12:25:15 2010 +0100 +++ b/src/Pure/Concurrent/task_queue.ML Fri Jan 08 14:07:07 2010 +0100 @@ -7,7 +7,7 @@ signature TASK_QUEUE = sig type task - val new_task: int -> task + val dummy_task: task val pri_of_task: task -> int val str_of_task: task -> string type group @@ -20,10 +20,11 @@ val str_of_group: group -> string type queue val empty: queue - val is_empty: queue -> bool - val status: queue -> {ready: int, pending: int, running: int} + val all_passive: queue -> bool + val status: queue -> {ready: int, pending: int, running: int, passive: int} val cancel: queue -> group -> bool val cancel_all: queue -> group list + val enqueue_passive: group -> queue -> task * queue val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue val extend: task -> (bool -> bool) -> queue -> queue option val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue @@ -38,13 +39,14 @@ (* tasks *) -datatype task = Task of int * serial; +datatype task = Task of int option * serial; +val dummy_task = Task (NONE, ~1); fun new_task pri = Task (pri, serial ()); -fun pri_of_task (Task (pri, _)) = pri; +fun pri_of_task (Task (pri, _)) = the_default 0 pri; fun str_of_task (Task (_, i)) = string_of_int i; -fun task_ord (Task t1, Task t2) = prod_ord (rev_order o int_ord) int_ord (t1, t2); +fun task_ord (Task t1, Task t2) = prod_ord (rev_order o option_ord int_ord) int_ord (t1, t2); structure Task_Graph = Graph(type key = task val ord = task_ord); @@ -79,6 +81,8 @@ not (null (Synchronized.value status)) orelse (case parent of NONE => false | SOME group => is_canceled group); +fun is_ready deps group = null deps orelse is_canceled group; + fun group_status (Group {parent, status, ...}) = Synchronized.value status @ (case parent of NONE => [] | SOME group => group_status group); @@ -91,7 +95,8 @@ datatype job = Job of (bool -> bool) list | - Running of Thread.thread; + Running of Thread.thread | + Passive; type jobs = (group * job) Task_Graph.T; @@ -113,35 +118,36 @@ (* queue of grouped jobs *) -datatype result = Unknown | Result of task | No_Result; - datatype queue = Queue of {groups: task list Inttab.table, (*groups with presently active members*) - jobs: jobs, (*job dependency graph*) - cache: result}; (*last dequeue result*) + jobs: jobs}; (*job dependency graph*) + +fun make_queue groups jobs = Queue {groups = groups, jobs = jobs}; -fun make_queue groups jobs cache = Queue {groups = groups, jobs = jobs, cache = cache}; +val empty = make_queue Inttab.empty Task_Graph.empty; -val empty = make_queue Inttab.empty Task_Graph.empty No_Result; -fun is_empty (Queue {jobs, ...}) = Task_Graph.is_empty jobs; +fun all_passive (Queue {jobs, ...}) = + Task_Graph.get_first NONE + ((fn Job _ => SOME () | Running _ => SOME () | Passive => NONE) o #2 o #1 o #2) jobs |> is_none; (* queue status *) fun status (Queue {jobs, ...}) = let - val (x, y, z) = - Task_Graph.fold (fn (_, ((_, job), (deps, _))) => fn (x, y, z) => + val (x, y, z, w) = + Task_Graph.fold (fn (_, ((group, job), (deps, _))) => fn (x, y, z, w) => (case job of - Job _ => if null deps then (x + 1, y, z) else (x, y + 1, z) - | Running _ => (x, y, z + 1))) - jobs (0, 0, 0); - in {ready = x, pending = y, running = z} end; + Job _ => if is_ready deps group then (x + 1, y, z, w) else (x, y + 1, z, w) + | Running _ => (x, y, z + 1, w) + | Passive => (x, y, z, w + 1))) + jobs (0, 0, 0, 0); + in {ready = x, pending = y, running = z, passive = w} end; (* cancel -- peers and sub-groups *) -fun cancel (Queue {groups, jobs, ...}) group = +fun cancel (Queue {groups, jobs}) group = let val _ = cancel_group group Exn.Interrupt; val tasks = Inttab.lookup_list groups (group_id group); @@ -150,22 +156,31 @@ val _ = List.app SimpleThread.interrupt running; in null running end; -fun cancel_all (Queue {jobs, ...}) = +fun cancel_all (Queue {groups, jobs}) = let fun cancel_job (group, job) (groups, running) = (cancel_group group Exn.Interrupt; - (case job of Running t => (insert eq_group group groups, insert Thread.equal t running) + (case job of + Running t => (insert eq_group group groups, insert Thread.equal t running) | _ => (groups, running))); - val (groups, running) = Task_Graph.fold (cancel_job o #1 o #2) jobs ([], []); + val (running_groups, running) = Task_Graph.fold (cancel_job o #1 o #2) jobs ([], []); val _ = List.app SimpleThread.interrupt running; - in groups end; + in running_groups end; (* enqueue *) -fun enqueue group deps pri job (Queue {groups, jobs, cache}) = +fun enqueue_passive group (Queue {groups, jobs}) = let - val task = new_task pri; + val task = new_task NONE; + val groups' = groups + |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group); + val jobs' = jobs |> Task_Graph.new_node (task, (group, Passive)); + in (task, make_queue groups' jobs') end; + +fun enqueue group deps pri job (Queue {groups, jobs}) = + let + val task = new_task (SOME pri); val groups' = groups |> fold (fn gid => Inttab.cons_list (gid, task)) (group_ancestry group); val jobs' = jobs @@ -173,62 +188,48 @@ |> fold (add_job task) deps |> fold (fold (add_job task) o get_deps jobs) deps; val minimal = null (get_deps jobs' task); - val cache' = - (case cache of - Result last => - if task_ord (last, task) = LESS - then cache else Unknown - | _ => Unknown); - in ((task, minimal), make_queue groups' jobs' cache') end; + in ((task, minimal), make_queue groups' jobs') end; -fun extend task job (Queue {groups, jobs, cache}) = +fun extend task job (Queue {groups, jobs}) = (case try (get_job jobs) task of - SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) cache) + SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs)) | _ => NONE); (* dequeue *) -fun dequeue thread (queue as Queue {groups, jobs, cache}) = +fun dequeue thread (queue as Queue {groups, jobs}) = let - fun ready (task, ((group, Job list), ([], _))) = SOME (task, group, rev list) + fun ready (task, ((group, Job list), (deps, _))) = + if is_ready deps group then SOME (task, group, rev list) else NONE | ready _ = NONE; - fun deq boundary = - (case Task_Graph.get_first boundary ready jobs of - NONE => (NONE, make_queue groups jobs No_Result) - | SOME (result as (task, _, _)) => - let - val jobs' = set_job task (Running thread) jobs; - val cache' = Result task; - in (SOME result, make_queue groups jobs' cache') end); in - (case cache of - Unknown => deq NONE - | Result last => deq (SOME last) - | No_Result => (NONE, queue)) + (case Task_Graph.get_first NONE ready jobs of + NONE => (NONE, queue) + | SOME (result as (task, _, _)) => + let val jobs' = set_job task (Running thread) jobs + in (SOME result, make_queue groups jobs') end) end; (* dequeue_towards -- adhoc dependencies *) -fun depend task deps (Queue {groups, jobs, ...}) = - make_queue groups (fold (add_dep task) deps jobs) Unknown; +fun depend task deps (Queue {groups, jobs}) = + make_queue groups (fold (add_dep task) deps jobs); -fun dequeue_towards thread deps (queue as Queue {groups, jobs, ...}) = +fun dequeue_towards thread deps (queue as Queue {groups, jobs}) = let fun ready task = (case Task_Graph.get_node jobs task of (group, Job list) => - if null (get_deps jobs task) + if is_ready (get_deps jobs task) group then SOME (task, group, rev list) else NONE | _ => NONE); val tasks = filter (can (Task_Graph.get_node jobs)) deps; fun result (res as (task, _, _)) = - let - val jobs' = set_job task (Running thread) jobs; - val cache' = Unknown; - in ((SOME res, tasks), make_queue groups jobs' cache') end; + let val jobs' = set_job task (Running thread) jobs + in ((SOME res, tasks), make_queue groups jobs') end; in (case get_first ready tasks of SOME res => result res @@ -241,14 +242,13 @@ (* finish *) -fun finish task (Queue {groups, jobs, cache}) = +fun finish task (Queue {groups, jobs}) = let val group = get_group jobs task; val groups' = groups |> fold (fn gid => Inttab.remove_list (op =) (gid, task)) (group_ancestry group); val jobs' = Task_Graph.del_node task jobs; val maximal = null (Task_Graph.imm_succs jobs task); - val cache' = if maximal then cache else Unknown; - in (maximal, make_queue groups' jobs' cache') end; + in (maximal, make_queue groups' jobs') end; end; diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Jan 08 12:25:15 2010 +0100 +++ b/src/Pure/IsaMakefile Fri Jan 08 14:07:07 2010 +0100 @@ -117,39 +117,3 @@ clean: @rm -f $(OUT)/Pure $(LOG)/Pure.gz $(OUT)/RAW $(LOG)/RAW.gz \ $(LOG)/Pure-ProofGeneral.gz - - -## Scala material - -SCALA_FILES = Concurrent/future.scala General/download.scala \ - General/event_bus.scala General/exn.scala General/linear_set.scala \ - General/markup.scala General/position.scala General/scan.scala \ - General/swing_thread.scala General/symbol.scala General/xml.scala \ - General/yxml.scala Isar/isar_document.scala Isar/outer_keyword.scala \ - Isar/outer_lex.scala Isar/outer_parse.scala Isar/outer_syntax.scala \ - System/cygwin.scala System/gui_setup.scala \ - System/isabelle_process.scala System/isabelle_syntax.scala \ - System/isabelle_system.scala System/platform.scala \ - System/session_manager.scala System/standard_system.scala \ - Thy/completion.scala Thy/html.scala Thy/thy_header.scala \ - Thy/thy_syntax.scala library.scala - -JAR_DIR = $(ISABELLE_HOME)/lib/classes -PURE_JAR = $(JAR_DIR)/Pure.jar -FULL_JAR = $(JAR_DIR)/isabelle-scala.jar - -jars: $(FULL_JAR) - -$(FULL_JAR): $(SCALA_FILES) - @rm -rf classes && mkdir classes - "$(SCALA_HOME)/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 $(SCALA_FILES) - @cp $(SCALA_FILES) classes/isabelle - @mkdir -p "$(JAR_DIR)" - @cd classes; jar cfe `jvmpath "$(PURE_JAR)"` isabelle.GUI_Setup isabelle - @cd classes; cp "$(SCALA_HOME)/lib/scala-swing.jar" .; jar xf scala-swing.jar; \ - cp "$(SCALA_HOME)/lib/scala-library.jar" "$(FULL_JAR)"; \ - jar ufe `jvmpath $(FULL_JAR)` isabelle.GUI_Setup isabelle scala - @rm -rf classes - -clean-jars: - @rm -f "$(PURE_JAR)" "$(FULL_JAR)" diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Fri Jan 08 12:25:15 2010 +0100 +++ b/src/Pure/Isar/isar_document.ML Fri Jan 08 14:07:07 2010 +0100 @@ -232,11 +232,10 @@ in put_state state_id' state' end; in (state_id', ((id, state_id'), make_state') :: updates) end; -fun report_updates [] = () - | report_updates updates = - implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates) - |> Markup.markup Markup.assign - |> Output.status; +fun report_updates updates = + implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates) + |> Markup.markup Markup.assign + |> Output.status; in diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/Pure/Thy/text_edit.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/text_edit.scala Fri Jan 08 14:07:07 2010 +0100 @@ -0,0 +1,77 @@ +/* Title: Pure/Thy/text_edit.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Basic edits on plain text. +*/ + +package isabelle + + +sealed abstract class Text_Edit +{ + val start: Int + def after(offset: Int): Int + def before(offset: Int): Int + def edit(string: String, shift: Int): (Option[Text_Edit], String) +} + + +object Text_Edit +{ + /* transform offsets */ + + private def after_insert(start: Int, text: String, offset: Int): Int = + if (start <= offset) offset + text.length + else offset + + private def after_remove(start: Int, text: String, offset: Int): Int = + if (start > offset) offset + else (offset - text.length) max start + + + /* edit strings */ + + private def insert(index: Int, text: String, string: String): String = + string.substring(0, index) + text + string.substring(index) + + private def remove(index: Int, count: Int, string: String): String = + string.substring(0, index) + string.substring(index + count) + + + /* explicit edits */ + + case class Insert(start: Int, text: String) extends Text_Edit + { + def after(offset: Int): Int = after_insert(start, text, offset) + def before(offset: Int): Int = after_remove(start, text, offset) + + def can_edit(string_length: Int, shift: Int): Boolean = + shift <= start && start <= shift + string_length + + def edit(string: String, shift: Int): (Option[Insert], String) = + if (can_edit(string.length, shift)) (None, insert(start - shift, text, string)) + else (Some(this), string) + } + + case class Remove(start: Int, text: String) extends Text_Edit + { + def after(offset: Int): Int = after_remove(start, text, offset) + def before(offset: Int): Int = after_insert(start, text, offset) + + def can_edit(string_length: Int, shift: Int): Boolean = + shift <= start && start < shift + string_length + + def edit(string: String, shift: Int): (Option[Remove], String) = + if (can_edit(string.length, shift)) { + val index = start - shift + val count = text.length min (string.length - index) + val rest = + if (count == text.length) None + else Some(Remove(start, text.substring(count))) + (rest, remove(index, count, string)) + } + else (Some(this), string) + } +} + diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/Pure/build-jars --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/build-jars Fri Jan 08 14:07:07 2010 +0100 @@ -0,0 +1,101 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# mk-jars - build Isabelle/Scala +# +# Requires proper Isabelle settings environment. + + +## diagnostics + +function fail() +{ + echo "$1" >&2 + exit 2 +} + +[ -n "$ISABELLE_HOME" ] || fail "Missing Isabelle settings environment" +[ -z "$SCALA_HOME" ] && fail "Scala unavailable: unknown SCALA_HOME" + + +## dependencies + +declare -a SOURCES=( + Concurrent/future.scala + General/download.scala + General/event_bus.scala + General/exn.scala + General/linear_set.scala + General/markup.scala + General/position.scala + General/scan.scala + General/swing_thread.scala + General/symbol.scala + General/xml.scala + General/yxml.scala + Isar/isar_document.scala + Isar/outer_keyword.scala + Isar/outer_lex.scala + Isar/outer_parse.scala + Isar/outer_syntax.scala + System/cygwin.scala + System/gui_setup.scala + System/isabelle_process.scala + System/isabelle_syntax.scala + System/isabelle_system.scala + System/platform.scala + System/session_manager.scala + System/standard_system.scala + Thy/completion.scala + Thy/html.scala + Thy/text_edit.scala + Thy/thy_header.scala + Thy/thy_syntax.scala + library.scala +) + +TARGET_DIR="$ISABELLE_HOME/lib/classes" +PURE_JAR="$TARGET_DIR/Pure.jar" +FULL_JAR="$TARGET_DIR/isabelle-scala.jar" + +declare -a TARGETS=("$PURE_JAR" "$FULL_JAR") + + +## main + +OUTDATED=false + +for SOURCE in "${SOURCES[@]}" +do + [ ! -e "$SOURCE" ] && fail "Missing source file: $SOURCE" + for TARGET in "${TARGETS[@]}" + do + [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true + done +done + +if [ "$OUTDATED" = true ] +then + echo "###" + echo "### Building Isabelle/Scala components ..." + echo "###" + + rm -rf classes && mkdir classes + "$SCALA_HOME/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 "${SOURCES[@]}" || \ + fail "Failed to compile sources" + mkdir -p "$TARGET_DIR" || fail "Failed to create directory $TARGET_DIR" + ( + cd classes + jar cfe "$(jvmpath "$PURE_JAR")" isabelle.GUI_Setup isabelle || \ + fail "Failed to produce $PURE_JAR" + + cp "$SCALA_HOME/lib/scala-swing.jar" . + jar xf scala-swing.jar + + cp "$SCALA_HOME/lib/scala-library.jar" "$FULL_JAR" + jar ufe "$(jvmpath "$FULL_JAR")" isabelle.GUI_Setup isabelle scala || \ + fail "Failed to produce $FULL_JAR" + ) + rm -rf classes +fi diff -r 19c1fd52d6c9 -r 6cd289eca3e4 src/Pure/mk --- a/src/Pure/mk Fri Jan 08 12:25:15 2010 +0100 +++ b/src/Pure/mk Fri Jan 08 14:07:07 2010 +0100 @@ -2,9 +2,9 @@ # # Author: Markus Wenzel, TU Muenchen # -# mk - build Pure Isabelle. +# mk - build Isabelle/Pure. # -# Requires proper Isabelle settings environment (cf. IsaMakefile). +# Requires proper Isabelle settings environment. ## diagnostics