# HG changeset patch # User wenzelm # Date 1345130388 -7200 # Node ID 2cc51d1cabd7364031cff217b37a546711b0ccc9 # Parent 6ed588c4f963c1bd207681cf9429c086a719f8e1# Parent 72efe3e0a46bafd4cf066ae6fab57e7e773fc2e6 merged diff -r 6ed588c4f963 -r 2cc51d1cabd7 Admin/components --- a/Admin/components Thu Aug 16 15:41:36 2012 +0200 +++ b/Admin/components Thu Aug 16 17:19:48 2012 +0200 @@ -4,9 +4,10 @@ contrib/hol-light-bundle-0.5-126 contrib/kodkodi-1.2.16 contrib/spass-3.8ds -contrib/scala-2.9.2 contrib/vampire-1.0 contrib/yices-1.0.28 contrib/z3-4.0 -contrib/jedit_build-20120414 -contrib/jdk-6u31 +contrib/jdk-7u6 +contrib/scala-2.9.2 +contrib/jedit_build-20120813 + diff -r 6ed588c4f963 -r 2cc51d1cabd7 Admin/java/README --- a/Admin/java/README Thu Aug 16 15:41:36 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -This is JDK 1.6.0_31 for Linux and Windows from -http://www.oracle.com/technetwork/java/javase/downloads/index.html - -On Mac OS X the version provided by Apple is used instead. diff -r 6ed588c4f963 -r 2cc51d1cabd7 Admin/java/build --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/java/build Thu Aug 16 17:19:48 2012 +0200 @@ -0,0 +1,117 @@ +#!/usr/bin/env bash + +## diagnostics + +function fail() +{ + echo "$1" >&2 + exit 2 +} + + +## parameters + +ARCHIVE_LINUX32="jdk-7u6-linux-i586.tar.gz" +ARCHIVE_LINUX64="jdk-7u6-linux-x64.tar.gz" +ARCHIVE_DARWIN="jdk1.7.0_06.jdk.tar.gz" +ARCHIVE_WINDOWS="jdk1.7.0_06.tar.gz" + +VERSION="7u6" + + +## variations on version + +case "$VERSION" in + *u?) + MAJOR="$(echo "$VERSION" | cut -du -f1)" + MINOR="0$(echo "$VERSION" | cut -du -f2)" + ;; + *u??) + MAJOR="$(echo "$VERSION" | cut -du -f1)" + MINOR="$(echo "$VERSION" | cut -du -f2)" + ;; + *) + fail "Bad version identifier: \"$VERSION\"" + ;; +esac + +FULL_VERSION="1.${MAJOR}.0_${MINOR}" + + +## main + +DIR="jdk-${VERSION}" +mkdir "$DIR" || fail "Cannot create fresh directory: \"$DIR\"" + + +# README + +cat >> "$DIR/README" << EOF +This is JDK $FULL_VERSION for Linux, Mac OS X, Windows. + +See http://www.oracle.com/technetwork/java/javase/downloads/index.html +for the original downloads, which are covered by the Oracle Binary +Code License Agreement for Java SE. + +Note that Java 1.7 requires 64bit hardware on Mac OS X. +EOF + + +# settings + +mkdir "$DIR/etc" +cat >> "$DIR/etc/settings" << EOF +# -*- shell-script -*- :mode=shellscript: + +case "\${ISABELLE_PLATFORM64:-\$ISABELLE_PLATFORM32}" in + x86-darwin) + echo "### Java 1.7 unavailable on 32bit Macintosh!" >&2 + ;; + x86_64-darwin) + ISABELLE_JDK_HOME="\$COMPONENT/\$ISABELLE_PLATFORM64/jdk${FULL_VERSION}.jdk/Contents/Home" + ;; + *) + ISABELLE_JDK_HOME="\$COMPONENT/\${ISABELLE_PLATFORM64:-\$ISABELLE_PLATFORM32}/jdk${FULL_VERSION}" + ;; +esac + +if [ -n "\$ISABELLE_JDK_HOME" ]; then + ISABELLE_JAVA_EXT="\${ISABELLE_JDK_HOME}/jre/lib/ext" +fi +EOF + + +# content + +mkdir "$DIR/x86-linux" "$DIR/x86_64-linux" "$DIR/x86_64-darwin" "$DIR/x86-cygwin" + +tar -C "$DIR/x86-linux" -xf "$ARCHIVE_LINUX32" +tar -C "$DIR/x86_64-linux" -xf "$ARCHIVE_LINUX64" +tar -C "$DIR/x86_64-darwin" -xf "$ARCHIVE_DARWIN" +tar -C "$DIR/x86-cygwin" -xf "$ARCHIVE_WINDOWS" + +chgrp -R isabelle "$DIR" +chmod -R a+r "$DIR" +chmod -R a+X "$DIR" + +( + cd "$DIR/x86-linux/jdk${FULL_VERSION}" + for FILE in $(find . -type f) + do + for OTHER in \ + "../../x86_64-linux/jdk${FULL_VERSION}/$FILE" \ + "../../x86_64-darwin/jdk${FULL_VERSION}.jdk/Contents/Home/$FILE" \ + "../../x86-cygwin/jdk${FULL_VERSION}/$FILE" + do + if cmp -s "$FILE" "$OTHER" + then + ln -f "$FILE" "$OTHER" + fi + done + done +) + + +# create archive + +tar -cz -f "${DIR}.tar.gz" "$DIR" diff -r 6ed588c4f963 -r 2cc51d1cabd7 Admin/java/build_linux --- a/Admin/java/build_linux Thu Aug 16 15:41:36 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,106 +0,0 @@ -#!/usr/bin/env bash - - -## diagnostics - -PRG="$(basename "$0")" -THIS="$(cd $(dirname "$0"); pwd)" - -function usage() -{ - cat <&2 - exit 2 -} - - -## process command line - -# args - -VERSION="" -[ "$#" -gt 0 ] && { VERSION="$1"; shift; } - -[ "$#" -gt 0 ] && usage - -case "$VERSION" in - *u?) - MAJOR="$(echo "$VERSION" | cut -du -f1)" - MINOR="0$(echo "$VERSION" | cut -du -f2)" - ;; - *u??) - MAJOR="$(echo "$VERSION" | cut -du -f1)" - MINOR="$(echo "$VERSION" | cut -du -f2)" - ;; - *) - fail "Bad version identifier: \"$VERSION\"" - ;; -esac - -FULL_VERSION="1.${MAJOR}.0_${MINOR}" - - -## main - -DIR="jdk${FULL_VERSION}_x86-linux" -mkdir "$DIR" || fail "Cannot create fresh directory: \"$DIR\"" - - -# README - -cat >> "$DIR/README" << EOF -This is JDK $FULL_VERSION for x86-linux and x86_64-linux - -See http://www.oracle.com/technetwork/java/javase/downloads/index.html -for the original downloads, which are covered by the Oracle Binary -Code License Agreement for Java SE. -EOF - - -# settings - -mkdir "$DIR/etc" -cat >> "$DIR/etc/settings" << EOF -# -*- shell-script -*- :mode=shellscript: - -ISABELLE_JDK_HOME="\$COMPONENT/\${ISABELLE_PLATFORM64:-\$ISABELLE_PLATFORM}" -EOF - - -# content - -tar -C "$DIR" -x -f "jdk-$VERSION-linux-i586.tar.gz" || \ - fail "Bad archive: \"jdk-$VERSION-linux-i586.tar.gz\"" -mv "$DIR/jdk$FULL_VERSION" "$DIR/x86-linux" - -tar -C "$DIR" -x -f "jdk-$VERSION-linux-x64.tar.gz" || \ - fail "Bad archive: \"jdk-$VERSION-linux-x64.tar.gz\"" -mv "$DIR/jdk$FULL_VERSION" "$DIR/x86_64-linux" - -( - cd "$DIR/x86-linux" - for FILE in $(find . -type f) - do - if cmp -s "$FILE" "../x86_64-linux/$FILE" - then - ln -f "$FILE" "../x86_64-linux/$FILE" - fi - done -) - - -# create archive - -tar -cz -f "${DIR}.tar.gz" "$DIR" && rm -rf "$DIR" diff -r 6ed588c4f963 -r 2cc51d1cabd7 Admin/java/settings --- a/Admin/java/settings Thu Aug 16 15:41:36 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,10 +0,0 @@ -# -*- shell-script -*- :mode=shellscript: - -case "$ISABELLE_PLATFORM" in - *-darwin) - ISABELLE_JDK_HOME="$(/usr/libexec/java_home -v 1.6)" - ;; - *) - ISABELLE_JDK_HOME="$COMPONENT/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}/jdk1.6.0_31" - ;; -esac diff -r 6ed588c4f963 -r 2cc51d1cabd7 src/HOL/Library/Binomial.thy --- a/src/HOL/Library/Binomial.thy Thu Aug 16 15:41:36 2012 +0200 +++ b/src/HOL/Library/Binomial.thy Thu Aug 16 17:19:48 2012 +0200 @@ -14,55 +14,53 @@ primrec binomial :: "nat \ nat \ nat" (infixl "choose" 65) where binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)" - | binomial_Suc: "(Suc n choose k) = +| binomial_Suc: "(Suc n choose k) = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))" lemma binomial_n_0 [simp]: "(n choose 0) = 1" -by (cases n) simp_all + by (cases n) simp_all lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0" -by simp + by simp lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)" -by simp + by simp lemma binomial_eq_0: "!!k. n < k ==> (n choose k) = 0" -by (induct n) auto + by (induct n) auto declare binomial_0 [simp del] binomial_Suc [simp del] lemma binomial_n_n [simp]: "(n choose n) = 1" -by (induct n) (simp_all add: binomial_eq_0) + by (induct n) (simp_all add: binomial_eq_0) lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n" -by (induct n) simp_all + by (induct n) simp_all lemma binomial_1 [simp]: "(n choose Suc 0) = n" -by (induct n) simp_all + by (induct n) simp_all lemma zero_less_binomial: "k \ n ==> (n choose k) > 0" -by (induct n k rule: diff_induct) simp_all + by (induct n k rule: diff_induct) simp_all lemma binomial_eq_0_iff: "(n choose k = 0) = (n 0) = (k\n)" -by(simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric] - del:neq0_conv) + by (simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric] del: neq0_conv) (*Might be more useful if re-oriented*) lemma Suc_times_binomial_eq: "!!k. k \ n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k" -apply (induct n) -apply (simp add: binomial_0) -apply (case_tac k) -apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq - binomial_eq_0) -done + apply (induct n) + apply (simp add: binomial_0) + apply (case_tac k) + apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0) + done text{*This is the well-known version, but it's harder to use because of the need to reason about division.*} @@ -74,7 +72,7 @@ lemma times_binomial_minus1_eq: "[|k \ n; 0 (n choose k) * k = n * ((n - 1) choose (k - 1))" apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq) - apply (simp split add: nat_diff_split, auto) + apply (simp split add: nat_diff_split, auto) done @@ -85,20 +83,19 @@ Kamm\"uller, tidied by LCP. *} -lemma card_s_0_eq_empty: - "finite A ==> card {B. B \ A & card B = 0} = 1" -by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) +lemma card_s_0_eq_empty: "finite A ==> card {B. B \ A & card B = 0} = 1" + by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq]) lemma choose_deconstruct: "finite M ==> x \ M ==> {s. s <= insert x M & card(s) = Suc k} = {s. s <= M & card(s) = Suc k} Un {s. EX t. t <= M & card(t) = k & s = insert x t}" apply safe - apply (auto intro: finite_subset [THEN card_insert_disjoint]) + apply (auto intro: finite_subset [THEN card_insert_disjoint]) apply (drule_tac x = "xa - {x}" in spec) apply (subgoal_tac "x \ xa", auto) apply (erule rev_mp, subst card_Diff_singleton) - apply (auto intro: finite_subset) + apply (auto intro: finite_subset) done (* lemma "finite(UN y. {x. P x y})" @@ -111,10 +108,10 @@ lemma finite_bex_subset[simp]: "finite B \ (!!A. A<=B \ finite{x. P x A}) \ finite{x. EX A<=B. P x A}" -apply(subgoal_tac "{x. EX A<=B. P x A} = (UN A:Pow B. {x. P x A})") - apply simp -apply blast -done + apply (subgoal_tac "{x. EX A<=B. P x A} = (UN A:Pow B. {x. P x A})") + apply simp + apply blast + done text{*There are as many subsets of @{term A} having cardinality @{term k} as there are sets obtained from the former by inserting a fixed element @@ -123,10 +120,10 @@ "[|finite A; x \ A|] ==> card {B. EX C. C <= A & card(C) = k & B = insert x C} = card {B. B <= A & card(B) = k}" -apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq) - apply (auto elim!: equalityE simp add: inj_on_def) -apply (subst Diff_insert0, auto) -done + apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq) + apply (auto elim!: equalityE simp add: inj_on_def) + apply (subst Diff_insert0, auto) + done text {* Main theorem: combinatorial statement about number of subsets of a set. @@ -191,11 +188,11 @@ definition "pochhammer (a::'a::comm_semiring_1) n = (if n = 0 then 1 else setprod (\n. a + of_nat n) {0 .. n - 1})" -lemma pochhammer_0[simp]: "pochhammer a 0 = 1" +lemma pochhammer_0[simp]: "pochhammer a 0 = 1" by (simp add: pochhammer_def) lemma pochhammer_1[simp]: "pochhammer a 1 = a" by (simp add: pochhammer_def) -lemma pochhammer_Suc0[simp]: "pochhammer a (Suc 0) = a" +lemma pochhammer_Suc0[simp]: "pochhammer a (Suc 0) = a" by (simp add: pochhammer_def) lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\n. a + of_nat n) {0 .. n}" @@ -216,18 +213,18 @@ lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)" proof- - {assume "n=0" then have ?thesis by simp} + { assume "n=0" then have ?thesis by simp } moreover - {fix m assume m: "n = Suc m" - have ?thesis unfolding m pochhammer_Suc_setprod setprod_nat_ivl_Suc ..} - ultimately show ?thesis by (cases n, auto) -qed + { fix m assume m: "n = Suc m" + have ?thesis unfolding m pochhammer_Suc_setprod setprod_nat_ivl_Suc .. } + ultimately show ?thesis by (cases n) auto +qed lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n" proof- - {assume "n=0" then have ?thesis by (simp add: pochhammer_Suc_setprod)} + { assume "n=0" then have ?thesis by (simp add: pochhammer_Suc_setprod) } moreover - {assume n0: "n \ 0" + { assume n0: "n \ 0" have th0: "finite {1 .. n}" "0 \ {1 .. n}" by auto have eq: "insert 0 {1 .. n} = {0..n}" by auto have th1: "(\n\{1\nat..n}. a + of_nat n) = @@ -236,74 +233,80 @@ using n0 by (auto simp add: fun_eq_iff field_simps) have ?thesis apply (simp add: pochhammer_def) unfolding setprod_insert[OF th0, unfolded eq] - using th1 by (simp add: field_simps)} -ultimately show ?thesis by blast + using th1 by (simp add: field_simps) } + ultimately show ?thesis by blast qed lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n" unfolding fact_altdef_nat - - apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod) + apply (cases n) + apply (simp_all add: of_nat_setprod pochhammer_Suc_setprod) apply (rule setprod_reindex_cong[where f=Suc]) - by (auto simp add: fun_eq_iff) + apply (auto simp add: fun_eq_iff) + done -lemma pochhammer_of_nat_eq_0_lemma: assumes kn: "k > n" +lemma pochhammer_of_nat_eq_0_lemma: + assumes kn: "k > n" shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0" proof- - from kn obtain h where h: "k = Suc h" by (cases k, auto) - {assume n0: "n=0" then have ?thesis using kn - by (cases k) (simp_all add: pochhammer_rec)} + from kn obtain h where h: "k = Suc h" by (cases k) auto + { assume n0: "n=0" then have ?thesis using kn + by (cases k) (simp_all add: pochhammer_rec) } moreover - {assume n0: "n \ 0" - then have ?thesis apply (simp add: h pochhammer_Suc_setprod) - apply (rule_tac x="n" in bexI) - using h kn by auto} -ultimately show ?thesis by blast + { assume n0: "n \ 0" + then have ?thesis + apply (simp add: h pochhammer_Suc_setprod) + apply (rule_tac x="n" in bexI) + using h kn + apply auto + done } + ultimately show ?thesis by blast qed lemma pochhammer_of_nat_eq_0_lemma': assumes kn: "k \ n" shows "pochhammer (- (of_nat n :: 'a:: {idom, ring_char_0})) k \ 0" proof- - {assume "k=0" then have ?thesis by simp} + { assume "k=0" then have ?thesis by simp } moreover - {fix h assume h: "k = Suc h" + { fix h assume h: "k = Suc h" then have ?thesis apply (simp add: pochhammer_Suc_setprod) - using h kn by (auto simp add: algebra_simps)} - ultimately show ?thesis by (cases k, auto) + using h kn by (auto simp add: algebra_simps) } + ultimately show ?thesis by (cases k) auto qed -lemma pochhammer_of_nat_eq_0_iff: +lemma pochhammer_of_nat_eq_0_iff: shows "pochhammer (- (of_nat n :: 'a:: {idom, ring_char_0})) k = 0 \ k > n" (is "?l = ?r") - using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a] + using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a] pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a] by (auto simp add: not_le[symmetric]) -lemma pochhammer_eq_0_iff: +lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \ (EX k < n . a = - of_nat k) " apply (auto simp add: pochhammer_of_nat_eq_0_iff) - apply (cases n, auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0) + apply (cases n) + apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0) apply (rule_tac x=x in exI) apply auto done -lemma pochhammer_eq_0_mono: +lemma pochhammer_eq_0_mono: "pochhammer a n = (0::'a::field_char_0) \ m \ n \ pochhammer a m = 0" - unfolding pochhammer_eq_0_iff by auto + unfolding pochhammer_eq_0_iff by auto -lemma pochhammer_neq_0_mono: +lemma pochhammer_neq_0_mono: "pochhammer a m \ (0::'a::field_char_0) \ m \ n \ pochhammer a n \ 0" - unfolding pochhammer_eq_0_iff by auto + unfolding pochhammer_eq_0_iff by auto lemma pochhammer_minus: - assumes kn: "k \ n" + assumes kn: "k \ n" shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k" proof- - {assume k0: "k = 0" then have ?thesis by simp} - moreover - {fix h assume h: "k = Suc h" + { assume k0: "k = 0" then have ?thesis by simp } + moreover + { fix h assume h: "k = Suc h" have eq: "((- 1) ^ Suc h :: 'a) = setprod (%i. - 1) {0 .. h}" using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"] by auto @@ -312,12 +315,13 @@ apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"]) apply (auto simp add: inj_on_def image_def h ) apply (rule_tac x="h - x" in bexI) - by (auto simp add: fun_eq_iff h of_nat_diff)} - ultimately show ?thesis by (cases k, auto) + apply (auto simp add: fun_eq_iff h of_nat_diff) + done } + ultimately show ?thesis by (cases k) auto qed lemma pochhammer_minus': - assumes kn: "k \ n" + assumes kn: "k \ n" shows "pochhammer (b - of_nat k + 1) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (- b) k" unfolding pochhammer_minus[OF kn, where b=b] unfolding mult_assoc[symmetric] @@ -332,103 +336,112 @@ subsection{* Generalized binomial coefficients *} definition gbinomial :: "'a::field_char_0 \ nat \ 'a" (infixl "gchoose" 65) - where "a gchoose n = (if n = 0 then 1 else (setprod (\i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))" + where "a gchoose n = + (if n = 0 then 1 else (setprod (\i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))" lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0" -apply (simp_all add: gbinomial_def) -apply (subgoal_tac "(\i\nat\{0\nat..n}. - of_nat i) = (0::'b)") - apply (simp del:setprod_zero_iff) -apply simp -done + apply (simp_all add: gbinomial_def) + apply (subgoal_tac "(\i\nat\{0\nat..n}. - of_nat i) = (0::'b)") + apply (simp del:setprod_zero_iff) + apply simp + done lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)" -proof- - {assume "n=0" then have ?thesis by simp} +proof - + { assume "n=0" then have ?thesis by simp } moreover - {assume n0: "n\0" + { assume n0: "n\0" from n0 setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"] have eq: "(- (1\'a)) ^ n = setprod (\i. - 1) {0 .. n - 1}" by auto - from n0 have ?thesis - by (simp add: pochhammer_def gbinomial_def field_simps eq setprod_timesf[symmetric] del: minus_one) (* FIXME: del: minus_one *)} + from n0 have ?thesis + by (simp add: pochhammer_def gbinomial_def field_simps + eq setprod_timesf[symmetric] del: minus_one) (* FIXME: del: minus_one *) } ultimately show ?thesis by blast qed -lemma binomial_fact_lemma: - "k \ n \ fact k * fact (n - k) * (n choose k) = fact n" -proof(induct n arbitrary: k rule: nat_less_induct) +lemma binomial_fact_lemma: "k \ n \ fact k * fact (n - k) * (n choose k) = fact n" +proof (induct n arbitrary: k rule: nat_less_induct) fix n k assume H: "\mx\m. fact x * fact (m - x) * (m choose x) = fact m" and kn: "k \ n" - let ?ths = "fact k * fact (n - k) * (n choose k) = fact n" - {assume "n=0" then have ?ths using kn by simp} + let ?ths = "fact k * fact (n - k) * (n choose k) = fact n" + { assume "n=0" then have ?ths using kn by simp } moreover - {assume "k=0" then have ?ths using kn by simp} + { assume "k=0" then have ?ths using kn by simp } moreover - {assume nk: "n=k" then have ?ths by simp} + { assume nk: "n=k" then have ?ths by simp } moreover - {fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m" + { fix m h assume n: "n = Suc m" and h: "k = Suc h" and hm: "h < m" from n have mn: "m < n" by arith from hm have hm': "h \ m" by arith from hm h n kn have km: "k \ m" by arith - have "m - h = Suc (m - Suc h)" using h km hm by arith + have "m - h = Suc (m - Suc h)" using h km hm by arith with km h have th0: "fact (m - h) = (m - h) * fact (m - k)" by simp - from n h th0 - have "fact k * fact (n - k) * (n choose k) = k * (fact h * fact (m - h) * (m choose h)) + (m - h) * (fact k * fact (m - k) * (m choose k))" + from n h th0 + have "fact k * fact (n - k) * (n choose k) = + k * (fact h * fact (m - h) * (m choose h)) + (m - h) * (fact k * fact (m - k) * (m choose k))" by (simp add: field_simps) also have "\ = (k + (m - h)) * fact m" using H[rule_format, OF mn hm'] H[rule_format, OF mn km] by (simp add: field_simps) - finally have ?ths using h n km by simp} - moreover have "n=0 \ k = 0 \ k = n \ (EX m h. n=Suc m \ k = Suc h \ h < m)" using kn by presburger + finally have ?ths using h n km by simp } + moreover have "n=0 \ k = 0 \ k = n \ (EX m h. n=Suc m \ k = Suc h \ h < m)" + using kn by presburger ultimately show ?ths by blast qed - -lemma binomial_fact: - assumes kn: "k \ n" - shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))" + +lemma binomial_fact: + assumes kn: "k \ n" + shows "(of_nat (n choose k) :: 'a::field_char_0) = + of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))" using binomial_fact_lemma[OF kn] by (simp add: field_simps of_nat_mult [symmetric]) lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k" -proof- - {assume kn: "k > n" - from kn binomial_eq_0[OF kn] have ?thesis - by (simp add: gbinomial_pochhammer field_simps - pochhammer_of_nat_eq_0_iff)} +proof - + { assume kn: "k > n" + from kn binomial_eq_0[OF kn] have ?thesis + by (simp add: gbinomial_pochhammer field_simps pochhammer_of_nat_eq_0_iff) } moreover - {assume "k=0" then have ?thesis by simp} + { assume "k=0" then have ?thesis by simp } moreover - {assume kn: "k \ n" and k0: "k\ 0" - from k0 obtain h where h: "k = Suc h" by (cases k, auto) + { assume kn: "k \ n" and k0: "k\ 0" + from k0 obtain h where h: "k = Suc h" by (cases k) auto from h have eq:"(- 1 :: 'a) ^ k = setprod (\i. - 1) {0..h}" by (subst setprod_constant, auto) have eq': "(\i\{0..h}. of_nat n + - (of_nat i :: 'a)) = (\i\{n - h..n}. of_nat i)" apply (rule strong_setprod_reindex_cong[where f="op - n"]) - using h kn - apply (simp_all add: inj_on_def image_iff Bex_def set_eq_iff) - apply clarsimp - apply (presburger) - apply presburger - by (simp add: fun_eq_iff field_simps of_nat_add[symmetric] del: of_nat_add) - have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" -"{1..n - Suc h} \ {n - h .. n} = {}" and eq3: "{1..n - Suc h} \ {n - h .. n} = {1..n}" using h kn by auto + using h kn + apply (simp_all add: inj_on_def image_iff Bex_def set_eq_iff) + apply clarsimp + apply presburger + apply presburger + apply (simp add: fun_eq_iff field_simps of_nat_add[symmetric] del: of_nat_add) + done + have th0: "finite {1..n - Suc h}" "finite {n - h .. n}" + "{1..n - Suc h} \ {n - h .. n} = {}" and + eq3: "{1..n - Suc h} \ {n - h .. n} = {1..n}" + using h kn by auto from eq[symmetric] have ?thesis using kn - apply (simp add: binomial_fact[OF kn, where ?'a = 'a] + apply (simp add: binomial_fact[OF kn, where ?'a = 'a] gbinomial_pochhammer field_simps pochhammer_Suc_setprod del: minus_one) - apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc del: minus_one) + apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h + of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc del: minus_one) unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \ 'a"] eq[unfolded h] - unfolding mult_assoc[symmetric] + unfolding mult_assoc[symmetric] unfolding setprod_timesf[symmetric] apply simp apply (rule strong_setprod_reindex_cong[where f= "op - n"]) - apply (auto simp add: inj_on_def image_iff Bex_def) - apply presburger + apply (auto simp add: inj_on_def image_iff Bex_def) + apply presburger apply (subgoal_tac "(of_nat (n - x) :: 'a) = of_nat n - of_nat x") + apply simp + apply (rule of_nat_diff) apply simp - by (rule of_nat_diff, simp) + done } moreover have "k > n \ k = 0 \ (k \ n \ k \ 0)" by arith @@ -441,72 +454,86 @@ lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a" by (simp add: gbinomial_def) -lemma gbinomial_mult_1: "a * (a gchoose n) = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") -proof- +lemma gbinomial_mult_1: + "a * (a gchoose n) = + of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" (is "?l = ?r") +proof - have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))" unfolding gbinomial_pochhammer - pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc + pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc by (simp add: field_simps del: of_nat_Suc) also have "\ = ?l" unfolding gbinomial_pochhammer by (simp add: field_simps) finally show ?thesis .. qed -lemma gbinomial_mult_1': "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" +lemma gbinomial_mult_1': + "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))" by (simp add: mult_commute gbinomial_mult_1) -lemma gbinomial_Suc: "a gchoose (Suc k) = (setprod (\i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))" +lemma gbinomial_Suc: + "a gchoose (Suc k) = (setprod (\i. a - of_nat i) {0 .. k}) / of_nat (fact (Suc k))" by (simp add: gbinomial_def) - + lemma gbinomial_mult_fact: - "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = (setprod (\i. a - of_nat i) {0 .. k})" - unfolding gbinomial_Suc - by (simp_all add: field_simps del: fact_Suc) + "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = + (setprod (\i. a - of_nat i) {0 .. k})" + by (simp_all add: gbinomial_Suc field_simps del: fact_Suc) lemma gbinomial_mult_fact': - "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\i. a - of_nat i) {0 .. k})" + "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = + (setprod (\i. a - of_nat i) {0 .. k})" using gbinomial_mult_fact[of k a] - apply (subst mult_commute) . + apply (subst mult_commute) + apply assumption + done -lemma gbinomial_Suc_Suc: "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" -proof- - {assume "k = 0" then have ?thesis by simp} + +lemma gbinomial_Suc_Suc: + "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))" +proof - + { assume "k = 0" then have ?thesis by simp } moreover - {fix h assume h: "k = Suc h" - have eq0: "(\i\{1..k}. (a + 1) - of_nat i) = (\i\{0..h}. a - of_nat i)" - apply (rule strong_setprod_reindex_cong[where f = Suc]) - using h by auto + { fix h assume h: "k = Suc h" + have eq0: "(\i\{1..k}. (a + 1) - of_nat i) = (\i\{0..h}. a - of_nat i)" + apply (rule strong_setprod_reindex_cong[where f = Suc]) + using h + apply auto + done - have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\i\{0\nat..Suc h}. a - of_nat i)" - unfolding h - apply (simp add: field_simps del: fact_Suc) + have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = + ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\i\{0\nat..Suc h}. a - of_nat i)" + apply (simp add: h field_simps del: fact_Suc) unfolding gbinomial_mult_fact' apply (subst fact_Suc) - unfolding of_nat_mult + unfolding of_nat_mult apply (subst mult_commute) unfolding mult_assoc unfolding gbinomial_mult_fact - by (simp add: field_simps) + apply (simp add: field_simps) + done also have "\ = (\i\{0..h}. a - of_nat i) * (a + 1)" unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc by (simp add: field_simps h) also have "\ = (\i\{0..k}. (a + 1) - of_nat i)" using eq0 - unfolding h setprod_nat_ivl_1_Suc - by simp + by (simp add: h setprod_nat_ivl_1_Suc) also have "\ = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))" unfolding gbinomial_mult_fact .. - finally have ?thesis by (simp del: fact_Suc) } - ultimately show ?thesis by (cases k, auto) + finally have ?thesis by (simp del: fact_Suc) + } + ultimately show ?thesis by (cases k) auto qed -lemma binomial_symmetric: assumes kn: "k \ n" +lemma binomial_symmetric: + assumes kn: "k \ n" shows "n choose k = n choose (n - k)" proof- from kn have kn': "n - k \ n" by arith from binomial_fact_lemma[OF kn] binomial_fact_lemma[OF kn'] - have "fact k * fact (n - k) * (n choose k) = fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp + have "fact k * fact (n - k) * (n choose k) = + fact (n - k) * fact (n - (n - k)) * (n choose (n - k))" by simp then show ?thesis using kn by simp qed diff -r 6ed588c4f963 -r 2cc51d1cabd7 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Thu Aug 16 15:41:36 2012 +0200 +++ b/src/Pure/Thy/thy_load.scala Thu Aug 16 17:19:48 2012 +0200 @@ -43,9 +43,9 @@ def read_header(name: Document.Node.Name): Thy_Header = { - val file = new JFile(name.node) - if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) - Thy_Header.read(file) + val path = Path.explode(name.node) + if (!path.is_file) error("No such file: " + path.toString) + Thy_Header.read(path.file) } diff -r 6ed588c4f963 -r 2cc51d1cabd7 src/Tools/jEdit/README_BUILD --- a/src/Tools/jEdit/README_BUILD Thu Aug 16 15:41:36 2012 +0200 +++ b/src/Tools/jEdit/README_BUILD Thu Aug 16 17:19:48 2012 +0200 @@ -1,28 +1,22 @@ -Requirements for instantaneous build from sources -================================================= +Requirements for instantaneous build from repository +==================================================== -* Official Java JDK 1.6 from Sun/Oracle/Apple +* Java JDK 1.7 from Oracle http://www.oracle.com/technetwork/java/javase/downloads/index.html - (experimental support for JDK/OpenJDK 1.7, but not OpenJDK 1.6) + (experimental support for JDK/OpenJDK 1.7) * Scala 2.9.2 http://www.scala-lang.org (experimental support for Scala 2.10.x milestones) + Note that the official directory layout of JDK and Scala is required! + * Auxiliary jedit_build component - http://www4.in.tum.de/~wenzelm/test/jedit_build-20120414.tar.gz -Important settings within Isabelle environment -============================================== - -* init_component ".../jedit_build-20120414" -* ISABELLE_JDK_HOME -* SCALA_HOME - -Note that the official directory layout of JDK and Scala is required! +See also http://isabelle.in.tum.de/components/. Build and run diff -r 6ed588c4f963 -r 2cc51d1cabd7 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Aug 16 15:41:36 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Aug 16 17:19:48 2012 +0200 @@ -110,11 +110,12 @@ else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { override def getRenderer() = - new ListCellRenderer { - val default_renderer = new DefaultListCellRenderer + new ListCellRenderer[Any] { + val default_renderer = + (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]] override def getListCellRendererComponent( - list: JList, value: Any, index: Int, + list: JList[_ <: Any], value: Any, index: Int, selected: Boolean, focus: Boolean): Component = { val renderer: Component =