# HG changeset patch # User wenzelm # Date 1357855378 -3600 # Node ID b6659475b5afb4748f50187ac76b28346a3fb790 # Parent fec14e8fefb82752bee7c1d50856ea9f9308e714# Parent eb38dfcf834a5befffccc96dc4792d5035e79cda merged diff -r fec14e8fefb8 -r b6659475b5af Admin/MacOS/App1/build --- a/Admin/MacOS/App1/build Thu Jan 10 18:19:13 2013 +0100 +++ b/Admin/MacOS/App1/build Thu Jan 10 23:02:58 2013 +0100 @@ -18,3 +18,6 @@ -f "$COCOADIALOG_APP" \ "$THIS/script" \ "$PWD/Isabelle.app" + +rm -f Contents/Resources/Isabelle +ln -s Contents/Resources/Isabelle Isabelle.app/Isabelle \ No newline at end of file diff -r fec14e8fefb8 -r b6659475b5af Admin/MacOS/App1/script --- a/Admin/MacOS/App1/script Thu Jan 10 18:19:13 2013 +0100 +++ b/Admin/MacOS/App1/script Thu Jan 10 23:02:58 2013 +0100 @@ -9,7 +9,13 @@ SUPER_APP="$(cd "$THIS/../../.."; pwd)" -# sane environment defaults +# global defaults + +ISABELLE_TOOL="$THIS/Isabelle/bin/isabelle" +PROOFGENERAL_EMACS="$THIS/Aquamacs.app/Contents/MacOS/Aquamacs" + + +# environment cd "$HOME" if [ -x /usr/libexec/path_helper ]; then @@ -19,46 +25,6 @@ [ -z "$LANG" ] && export LANG=en_US.UTF-8 -# settings support - -function choosefrom () -{ - local RESULT="" - local FILE="" - - for FILE in "$@" - do - [ -z "$RESULT" -a -e "$FILE" ] && RESULT="$FILE" - done - - [ -z "$RESULT" ] && RESULT="$FILE" - echo "$RESULT" -} - - -# Isabelle - -ISABELLE_TOOL="$(choosefrom \ - "$THIS/Isabelle/bin/isabelle" \ - "$SUPER_APP/Isabelle/bin/isabelle" \ - "$HOME/bin/isabelle" \ - isabelle)" - - -# Proof General / Emacs - -PROOFGENERAL_EMACS="$(choosefrom \ - "$THIS/Aquamacs.app/Contents/MacOS/Aquamacs" \ - "$SUPER_APP/Aquamacs.app/Contents/MacOS/Aquamacs" \ - /Applications/Aquamacs.app/Contents/MacOS/Aquamacs \ - "")" - -declare -a EMACS_OPTIONS=() -if [ -n "$PROOFGENERAL_EMACS" ]; then - EMACS_OPTIONS=(-p "$PROOFGENERAL_EMACS") -fi - - # run interface with error feedback ISABELLE_INTERFACE_CHOICE="$("$ISABELLE_TOOL" getenv -b ISABELLE_INTERFACE_CHOICE)" @@ -68,12 +34,12 @@ CHOICE=($("$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" dropdown \ --title Isabelle \ --text "Which Isabelle interface?" \ - --items "Emacs / Proof General" "Isabelle/jEdit PIDE" \ + --items "Isabelle/jEdit PIDE" "Emacs / Proof General" \ --button2 "OK, do not ask again" --button1 "OK")) if [ "${CHOICE[1]}" = 0 ]; then - ISABELLE_INTERFACE_CHOICE=emacs + ISABELLE_INTERFACE_CHOICE=jedit else - ISABELLE_INTERFACE_CHOICE=jedit + ISABELLE_INTERFACE_CHOICE=emacs fi if [ "${CHOICE[0]}" = 2 ]; then ISABELLE_HOME_USER="$("$ISABELLE_TOOL" getenv -b ISABELLE_HOME_USER)" @@ -91,10 +57,10 @@ OUTPUT="/tmp/isabelle$$.out" if [ "$ISABELLE_INTERFACE_CHOICE" = emacs ]; then - ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1 + ( "$ISABELLE_TOOL" emacs -p "$PROOFGENERAL_EMACS" "$@" ) > "$OUTPUT" 2>&1 RC=$? else - ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1 + ( "$ISABELLE_TOOL" jedit -s "$@" ) > "$OUTPUT" 2>&1 RC=$? fi diff -r fec14e8fefb8 -r b6659475b5af Admin/Release/CHECKLIST --- a/Admin/Release/CHECKLIST Thu Jan 10 18:19:13 2013 +0100 +++ b/Admin/Release/CHECKLIST Thu Jan 10 23:02:58 2013 +0100 @@ -7,6 +7,8 @@ - test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj; +- test scala-2.9.2; + - test Proof General 4.1, 3.7.1.1; - check HTML header of library; @@ -53,9 +55,7 @@ - hg up -r DISTNAME && isabelle makedist -r DISTNAME; -- makebin (multiplatform); - -- makebundle (multiplatform); +- isabelle makedist_bundles; - Mac OS X: hdiutil create -srcfolder DIR DMG; @@ -67,8 +67,6 @@ Final release stage =================== -- makedist: REPOS_NAME="isabelle-release" - - various .hg/hgrc files: default = /home/isabelle-repository/repos/isabelle-release diff -r fec14e8fefb8 -r b6659475b5af Admin/Release/makebundle --- a/Admin/Release/makebundle Thu Jan 10 18:19:13 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,147 +0,0 @@ -#!/usr/bin/env bash -# -# makebundle -- re-package with add-on components - -## diagnostics - -PRG=$(basename "$0") - -function usage() -{ - echo - echo "Usage: $PRG ARCHIVE PLATFORM" - echo - echo " Re-package Isabelle source distribution with add-on components" - echo " and heap images" - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## implicit and explicit arguments - -TMP="/var/tmp/isabelle-makebundle$$" -mkdir "$TMP" || fail "Cannot create directory $TMP" - -[ "$#" -ne 2 ] && usage - -ARCHIVE="$1"; shift -PLATFORM="$1"; shift - -[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE" - - -## main - -ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")" -ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)" -ISABELLE_HOME="$TMP/$ISABELLE_NAME" - -tar -C "$TMP" -x -z -f "$ARCHIVE" - - -echo "#bundled components" >> "$ISABELLE_HOME/etc/components" - -for CONTRIB in "$ARCHIVE_DIR/contrib/"*.tar.gz "$ARCHIVE_DIR/contrib/$PLATFORM"/*.tar.gz -do - if [ -f "$CONTRIB" ]; then - tar -C "$ISABELLE_HOME/contrib" -x -z -f "$CONTRIB" - NAME="$(basename "$CONTRIB" .tar.gz)" - [ -d "$ISABELLE_HOME/contrib/$NAME" ] || fail "Bad archive content $CONTRIB" - - if [ -e "$ISABELLE_HOME/contrib/$NAME/etc/settings" ]; then - echo "component $NAME" - if [ "$PLATFORM" != x86-cygwin -a "$NAME" = ProofGeneral-3.7.1.1 ]; then - echo "#contrib/$NAME" >> "$ISABELLE_HOME/etc/components" - elif [ "$PLATFORM" = x86-cygwin -a "$NAME" = ProofGeneral-4.1 ]; then - echo "#contrib/$NAME" >> "$ISABELLE_HOME/etc/components" - else - echo "contrib/$NAME" >> "$ISABELLE_HOME/etc/components" - fi - else - echo "package $NAME" - fi - fi -done - -if [ "$PLATFORM" = x86-cygwin ]; then - TAR="$ARCHIVE_DIR/contrib/x86-cygwin/Isabelle.tar" - [ -e "$TAR" ] || fail "Missing $TAR" - rm -f "$ISABELLE_HOME/Isabelle" - tar -C "$ISABELLE_HOME" -xv -f "$TAR" - - ( - cd "$ISABELLE_HOME" - for DIR in $(find contrib -name x86-linux -o -name x86_64-linux -o -name x86-darwin -o -name x86_64-darwin | sort) - do - echo "removing $DIR" - rm -rf "$DIR" - done - ) - - mv "$ISABELLE_HOME/contrib"/polyml* "$ISABELLE_HOME/contrib/cygwin-1.7.9/usr/local/" - ( - cd "$ISABELLE_HOME/contrib/cygwin-1.7.9" - find usr/local/polyml-*/x86-cygwin | gzip > etc/setup/polyml.lst.gz - ) - - for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README - do - FILE="$ISABELLE_HOME/$NAME" - { - echo '' - echo '' - echo '' - echo '' - echo '' - echo "${NAME}" - echo '' - echo '' - echo '
'
-      perl -w -p -e "s/&/&/g; s//>/g; s/'/'/g; s/\"/"/g;" "$FILE"
-      echo '
' - echo '' - } > "${FILE}.html" - done -fi - - -HEAPS_ARCHIVE="$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" -[ -f "$HEAPS_ARCHIVE" ] || fail "Bad heaps archive: $HEAPS_ARCHIVE" -echo "heaps" -tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE" - -case "$PLATFORM" in - x86_64-linux) - perl -pi -e 's,^ML_PLATFORM=.*$,ML_PLATFORM="\$ISABELLE_PLATFORM64",g;' "$TMP/$ISABELLE_NAME/etc/settings" - perl -pi -e "s,^ML_OPTIONS=.*$,ML_OPTIONS=\"-H 400\",g;" "$TMP/$ISABELLE_NAME/etc/settings" - ;; - *-darwin) - perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \ - -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \ - -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \ - "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props" - ;; - *-cygwin) - perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \ - "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props" - ;; - *) - ;; -esac - -BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz" - -echo "$(basename "$BUNDLE_ARCHIVE")" -tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" - - -# clean up -cd /tmp -rm -rf "$TMP" diff -r fec14e8fefb8 -r b6659475b5af Admin/Windows/Cygwin/Cygwin-Setup.bat --- a/Admin/Windows/Cygwin/Cygwin-Setup.bat Thu Jan 10 18:19:13 2013 +0100 +++ b/Admin/Windows/Cygwin/Cygwin-Setup.bat Thu Jan 10 23:02:58 2013 +0100 @@ -1,4 +1,4 @@ @echo off -"%CD%\contrib\cygwin-1.7.9\setup" --site http://isabelle.in.tum.de/cygwin --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\contrib\cygwin-1.7.9" +"%CD%\cygwin\isabelle\cygwin" --site http://isabelle.in.tum.de/cygwin_2013 --no-verify --only-site --local-package-dir "%TEMP%" --root "%CD%\cygwin" diff -r fec14e8fefb8 -r b6659475b5af Admin/Windows/Cygwin/Cygwin-Terminal.bat --- a/Admin/Windows/Cygwin/Cygwin-Terminal.bat Thu Jan 10 18:19:13 2013 +0100 +++ b/Admin/Windows/Cygwin/Cygwin-Terminal.bat Thu Jan 10 23:02:58 2013 +0100 @@ -6,4 +6,4 @@ echo This is the GNU Bash interpreter of Cygwin. echo Use command "isabelle" to invoke Isabelle tools. -"%CD%\contrib\cygwin-1.7.9\bin\bash" --login -i +"%CD%\cygwin\bin\bash" --login -i diff -r fec14e8fefb8 -r b6659475b5af Admin/Windows/Cygwin/init.bat --- a/Admin/Windows/Cygwin/init.bat Thu Jan 10 18:19:13 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -@echo off - -cd "%~dp0" -cd "..\.." - -echo Initializing ... -"contrib\cygwin-1.7.9\bin\ash" /bin/rebaseall -"contrib\cygwin-1.7.9\bin\bash" -c "PATH=/bin; chmod -wx $(find heaps -type f); mkpasswd -l >/etc/passwd; mkgroup -l >/etc/group" diff -r fec14e8fefb8 -r b6659475b5af Admin/Windows/Cygwin/isabelle/init.bat --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/Windows/Cygwin/isabelle/init.bat Thu Jan 10 23:02:58 2013 +0100 @@ -0,0 +1,11 @@ +@echo off + +cd "%~dp0" +cd "..\.." + +set CYGWIN=nodosfilewarning + +echo Initializing Cygwin ... +"cygwin\bin\dash" /isabelle/rebaseall contrib/polyml-5.5.0 +"cygwin\bin\bash" /isabelle/postinstall + diff -r fec14e8fefb8 -r b6659475b5af Admin/Windows/Cygwin/isabelle/postinstall --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/Windows/Cygwin/isabelle/postinstall Thu Jan 10 23:02:58 2013 +0100 @@ -0,0 +1,8 @@ +#!/bin/dash + +PATH=/bin + +bash /etc/postinstall/base-files-mketc.sh.done + +mkpasswd -l >/etc/passwd +mkgroup -l >/etc/group diff -r fec14e8fefb8 -r b6659475b5af Admin/Windows/Cygwin/isabelle/rebaseall --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/Windows/Cygwin/isabelle/rebaseall Thu Jan 10 23:02:58 2013 +0100 @@ -0,0 +1,14 @@ +#!/bin/dash + +PATH=/bin + +FILE_LIST="$(mktemp)" + +for DIR in "$@" +do + find "$DIR" -name "*.dll" >> "$FILE_LIST" +done + +dash /bin/rebaseall -T "$FILE_LIST" + +rm -f "$FILE_LIST" diff -r fec14e8fefb8 -r b6659475b5af Admin/Windows/Cygwin/sfx.txt --- a/Admin/Windows/Cygwin/sfx.txt Thu Jan 10 18:19:13 2013 +0100 +++ b/Admin/Windows/Cygwin/sfx.txt Thu Jan 10 23:02:58 2013 +0100 @@ -1,9 +1,9 @@ ;!@Install@!UTF-8! GUIFlags="64" InstallPath="%UserDesktop%" -BeginPrompt="Unpack Isabelle2012?" +BeginPrompt="Unpack Isabelle2013?" ExtractPathText="Target directory" -ExtractTitle="Unpacking Isabelle2012 ..." -Shortcut="Du,{%%T\Isabelle2012\Isabelle.exe},{},{},{},{},{%%T\Isabelle2012}" -RunProgram="\"%%T\Isabelle2012\contrib\cygwin-1.7.9\init.bat\"" +ExtractTitle="Unpacking Isabelle2013 ..." +Shortcut="Du,{%%T\Isabelle2013\Isabelle2013.exe},{},{},{},{},{%%T\Isabelle2013}" +RunProgram="\"%%T\Isabelle2013\cygwin\init.bat\"" ;!@InstallEnd@! diff -r fec14e8fefb8 -r b6659475b5af Admin/Windows/launch4j/Isabelle.exe Binary file Admin/Windows/launch4j/Isabelle.exe has changed diff -r fec14e8fefb8 -r b6659475b5af Admin/Windows/launch4j/isabelle.xml --- a/Admin/Windows/launch4j/isabelle.xml Thu Jan 10 18:19:13 2013 +0100 +++ b/Admin/Windows/launch4j/isabelle.xml Thu Jan 10 23:02:58 2013 +0100 @@ -20,11 +20,11 @@ %EXEDIR%\lib\classes\ext\scala-swing.jar - %EXEDIR%\contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31 + %EXEDIR%\contrib\jdk-7u9\x86-cygwin\jdk1.7.0_09 jdkOnly - -Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\contrib\\cygwin-1.7.9" + -Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\cygwin" isabelle.bmp diff -r fec14e8fefb8 -r b6659475b5af Admin/components/bundled --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/components/bundled Thu Jan 10 23:02:58 2013 +0100 @@ -0,0 +1,3 @@ +#additional components to be bundled for release +ProofGeneral-4.1 + diff -r fec14e8fefb8 -r b6659475b5af Admin/components/bundled-windows --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/components/bundled-windows Thu Jan 10 23:02:58 2013 +0100 @@ -0,0 +1,3 @@ +#additional components to be bundled for release +cygwin-20130110 + diff -r fec14e8fefb8 -r b6659475b5af Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Jan 10 18:19:13 2013 +0100 +++ b/Admin/components/components.sha1 Thu Jan 10 23:02:58 2013 +0100 @@ -1,4 +1,5 @@ 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz +842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz 0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz b98a98025d1f7e560ca6864a53296137dae736b4 e-1.6.tar.gz 6d34b18ca0aa1e10bab6413045d079188c0e2dfb exec_process-1.0.1.tar.gz diff -r fec14e8fefb8 -r b6659475b5af Admin/lib/Tools/makedist --- a/Admin/lib/Tools/makedist Thu Jan 10 18:19:13 2013 +0100 +++ b/Admin/lib/Tools/makedist Thu Jan 10 23:02:58 2013 +0100 @@ -32,7 +32,7 @@ echo " VERSION identifies the snapshot, using usual Mercurial terminology;" echo " the default is RELEASE if given, otherwise \"tip\"." echo - echo " Auxiliary components are that of the running Isabelle version!" + echo " Add-on components are that of the running Isabelle version!" echo exit 1 } @@ -170,17 +170,14 @@ ./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \ ./Admin/build all || fail "Failed to build distribution" -if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then - ./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \ - ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit" -else - echo "### Missing jEdit build component" -fi +./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS -optimise" \ + ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit" -cp -a src/Doc src/Doc.orig -./bin/isabelle env ./bin/isabelle build_doc -a || fail "Failed to build documentation" -rm -rf src/Doc -mv src/Doc.orig src/Doc +cp -a src src.orig +env ISABELLE_IDENTIFIER="${DISTNAME}-build" \ + ./bin/isabelle build_doc $JOBS -a || fail "Failed to build documentation" +rm -rf src +mv src.orig src rm -rf Admin diff -r fec14e8fefb8 -r b6659475b5af Admin/lib/Tools/makedist_bundles --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/lib/Tools/makedist_bundles Thu Jan 10 23:02:58 2013 +0100 @@ -0,0 +1,174 @@ +#!/usr/bin/env bash +# +# DESCRIPTION: re-package Isabelle distribution with add-on components + +## diagnostics + +PRG=$(basename "$0") + +function usage() +{ + echo + echo "Usage: isabelle $PRG ARCHIVE" + echo + echo " Re-package Isabelle source distribution with add-on components" + echo " and post-hoc patches for platform families linux, macos, windows." + echo + echo " Add-on components are that of the running Isabelle version!" + echo + exit 1 +} + +function fail() +{ + echo "$1" >&2 + exit 2 +} + + +## arguments + +[ "$#" -ne 1 ] && usage + +ARCHIVE="$1"; shift + +[ -f "$ARCHIVE" ] || fail "Bad source archive: $ARCHIVE" + +ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")" +ISABELLE_NAME="$(basename "$ARCHIVE" .tar.gz)" + + +## main + +for PLATFORM_FAMILY in linux macos windows +do + +echo +echo "*** $PLATFORM_FAMILY ***" + +TMP="/var/tmp/isabelle-makedist$$" +mkdir "$TMP" || fail "Cannot create directory $TMP" + +ISABELLE_TARGET="$TMP/$ISABELLE_NAME" + +tar -C "$TMP" -x -z -f "$ARCHIVE" + + +# bundled components + +mkdir -p "$ARCHIVE_DIR/contrib" + +echo "#bundled components" >> "$ISABELLE_TARGET/etc/components" + +for CATALOG in main "$PLATFORM_FAMILY" bundled "bundled-$PLATFORM_FAMILY" +do + CATALOG_FILE="$ISABELLE_HOME/Admin/components/$CATALOG" + if [ -f "$CATALOG_FILE" ] + then + echo "catalog ${CATALOG}" + { + while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; } + do + case "$REPLY" in + \#* | "") ;; + *) + COMPONENT="$REPLY" + case "$COMPONENT" in + jedit_build*) ;; + *) + echo " component $COMPONENT" + CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz" + if [ ! -f "$CONTRIB" ]; then + REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz" + echo " download $REMOTE" + perl -MLWP::Simple -e "getprint '$REMOTE';" > "$CONTRIB" + perl -e "exit((stat('${CONTRIB}'))[7] == 0 ? 0 : 1);" && exit 2 + fi + + tar -C "$ISABELLE_TARGET/contrib" -x -z -f "$CONTRIB" + echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components" + ;; + esac + ;; + esac + done + } < "$CATALOG_FILE" + fi +done + + +# platform-specific patches + +case "$PLATFORM_FAMILY" in + linux) + OTHER_PLATFORMS='-name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"' + ;; + macos) + OTHER_PLATFORMS='-name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"' + + perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \ + -e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \ + -e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \ + "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props" + ;; + windows) + OTHER_PLATFORMS='-name "x86*-linux" -o -name "x86*-darwin"' + + perl -pi -e "s,lookAndFeel=.*,lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel,g;" \ + "$TMP/$ISABELLE_NAME/src/Tools/jEdit/dist/properties/jEdit.props" + + mv "$ISABELLE_TARGET/contrib/cygwin" "$ISABELLE_TARGET" + + cp "$ISABELLE_HOME/Admin/Windows/launch4j/Isabelle.exe" "$ISABELLE_TARGET/Isabelle2013.exe" + cp "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Setup.bat" \ + "$ISABELLE_HOME/Admin/Windows/Cygwin/Cygwin-Terminal.bat" "$ISABELLE_TARGET" + + for NAME in ANNOUNCE README NEWS COPYRIGHT CONTRIBUTORS contrib/README + do + FILE="$ISABELLE_TARGET/$NAME" + { + echo '' + echo '' + echo '' + echo '' + echo '' + echo "${NAME}" + echo '' + echo '' + echo '
'
+        perl -w -p -e "s/&/&/g; s//>/g; s/'/'/g; s/\"/"/g;" "$FILE"
+        echo '
' + echo '' + } > "${FILE}.html" + done + ;; + *) + ;; +esac + + +# purge other platforms + +( + cd "$ISABELLE_TARGET" + for DIR in $(eval find contrib $OTHER_PLATFORMS | sort) + do + echo "removing $DIR" + rm -rf "$DIR" + done +) + + +# archive + +BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_${PLATFORM_FAMILY}.tar.gz" + +echo "packaging $(basename "$BUNDLE_ARCHIVE")" +tar -C "$TMP" -c -z -f "$BUNDLE_ARCHIVE" "$ISABELLE_NAME" + + +# clean up +rm -rf "$TMP" + +done + diff -r fec14e8fefb8 -r b6659475b5af Admin/lib/Tools/makedist_cygwin --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/lib/Tools/makedist_cygwin Thu Jan 10 23:02:58 2013 +0100 @@ -0,0 +1,74 @@ +#!/usr/bin/env bash +# +# DESCRIPTION: produce pre-canned Cygwin distribution for Isabelle + +## diagnostics + +PRG=$(basename "$0") + +function usage() +{ + echo + echo "Usage: isabelle $PRG" + echo + echo " Produce pre-canned Cygwin distribution for Isabelle." + echo + exit 1 +} + +function fail() +{ + echo "$1" >&2 + exit 2 +} + + +## arguments + +[ "$#" -ne 0 ] && usage + + +## main + +TARGET="$PWD/cygwin" + + +# download + +[ ! -e "$TARGET" ] || fail "Target already exists: \"$TARGET\"" +mkdir -p "$TARGET/isabelle" || fail "Failed to create target directory: \"$TARGET\"" + +perl -MLWP::Simple -e "getprint 'http://cygwin.com/setup.exe';" > "$TARGET/isabelle/cygwin.exe" +chmod +x "$TARGET/isabelle/cygwin.exe" + +"$TARGET/isabelle/cygwin.exe" -h /dev/null || exit 2 + + +# install + +"$TARGET/isabelle/cygwin.exe" \ + --local-package-dir "$(cygpath -w "$TMP/cygwin")" \ + --root "$(cygpath -w "$TARGET")" \ + --packages libgmp3,perl,python,rlwrap \ + --no-shortcuts --no-startmenu --no-desktop --quiet-mode + +[ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2 + + +# patches + +for NAME in hosts protocols services networks +do + rm "$TARGET/etc/$NAME" +done + +ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll" + +rm "$TARGET/Cygwin.bat" + +cp -a "$ISABELLE_HOME/Admin/Windows/Cygwin/isabelle/." "$TARGET/isabelle/." + + +# archive + +tar cvzf "${TARGET}.tar.gz" "$TARGET" diff -r fec14e8fefb8 -r b6659475b5af Isabelle --- a/Isabelle Thu Jan 10 18:19:13 2013 +0100 +++ b/Isabelle Thu Jan 10 23:02:58 2013 +0100 @@ -4,5 +4,5 @@ # # Default Isabelle application wrapper. -exec "$(dirname "$0")"/bin/isabelle jedit "$@" +exec "$(dirname "$0")"/bin/isabelle jedit -s "$@" diff -r fec14e8fefb8 -r b6659475b5af src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 10 18:19:13 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 10 23:02:58 2013 +0100 @@ -125,8 +125,8 @@ { fix x :: "'n::euclidean_space" def y == "(e/norm x) *\<^sub>R x" then have "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto - moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp - moreover hence "x = (norm x/e) *\<^sub>R y" by auto + moreover have *: "x = (norm x/e) *\<^sub>R y" using y_def assms by simp + moreover from * have "x = (norm x/e) *\<^sub>R y" by auto ultimately have "x : span (cball 0 e)" using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto } then have "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto @@ -297,7 +297,7 @@ and "setsum (\y. if (x = y) then P x else Q y) s = setsum Q s" and "setsum (\y. if (y = x) then P y else Q y) s = setsum Q s" and "setsum (\y. if (x = y) then P y else Q y) s = setsum Q s" - apply(rule_tac [!] setsum_cong2) + apply (rule_tac [!] setsum_cong2) using assms apply auto done @@ -659,12 +659,12 @@ qed lemma mem_affine: - assumes "affine S" "x : S" "y : S" "u+v=1" + assumes "affine S" "x : S" "y : S" "u + v = 1" shows "(u *\<^sub>R x + v *\<^sub>R y) : S" using assms affine_def[of S] by auto lemma mem_affine_3: - assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1" + assumes "affine S" "x : S" "y : S" "z : S" "u + v + w = 1" shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S" proof - have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}" @@ -689,7 +689,9 @@ "affine hull (insert a s) \ {a + v| v . v \ span {x - a | x . x \ s}}" unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq - apply (rule, rule) apply (erule exE)+ apply (erule conjE)+ + apply (rule, rule) + apply (erule exE)+ + apply (erule conjE)+ proof - fix x t u assume as: "finite t" "t \ {}" "t \ insert a s" "setsum u t = 1" "(\v\t. u v *\<^sub>R v) = x" @@ -1163,90 +1165,109 @@ shows "\x \ a. x <= b \ f x \ e1 \ f x \ e2" (is "\ x. ?P x") proof - let ?S = "{c. \x \ a. x <= c \ f x \ e1}" - have Se: " \x. x \ ?S" apply (rule exI[where x=a]) by (auto simp add: fa) + have Se: " \x. x \ ?S" + apply (rule exI[where x=a]) + apply (auto simp add: fa) + done have Sub: "\y. isUb UNIV ?S y" apply (rule exI[where x= b]) - using ab fb e12 by (auto simp add: isUb_def setle_def) + using ab fb e12 apply (auto simp add: isUb_def setle_def) + done from reals_complete[OF Se Sub] obtain l where l: "isLub UNIV ?S l"by blast have alb: "a \ l" "l \ b" using l ab fa fb e12 apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) - by (metis linorder_linear) + apply (metis linorder_linear) + done have ale1: "\z \ a. z < l \ f z \ e1" using l apply (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def) - by (metis linorder_linear not_le) - have th1: "\z x e d :: real. z <= x + e \ e < d ==> z < x \ abs(z - x) < d" by arith - have th2: "\e x:: real. 0 < e ==> ~(x + e <= x)" by arith - have "\d::real. 0 < d \ 0 < d/2 \ d/2 < d" by simp - then have th3: "\d::real. d > 0 \ \e > 0. e < d" by blast - {assume le2: "f l \ e2" - from le2 fa fb e12 alb have la: "l \ a" by metis - hence lap: "l - a > 0" using alb by arith - from e2[rule_format, OF le2] obtain e where - e: "e > 0" "\y. dist y (f l) < e \ y \ e2" by metis - from dst[OF alb e(1)] obtain d where - d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis - let ?d' = "min (d/2) ((l - a)/2)" - have "?d' < d \ 0 < ?d' \ ?d' < l - a" using lap d(1) - by (simp add: min_max.less_infI2) - then have "\d'. d' < d \ d' >0 \ l - d' > a" by auto - then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis - from d e have th0: "\y. \y - l\ < d \ f y \ e2" by metis - from th0[rule_format, of "l - d'"] d' have "f (l - d') \ e2" by auto - moreover - have "f (l - d') \ e1" using ale1[rule_format, of "l -d'"] d' by auto - ultimately have False using e12 alb d' by auto} + apply (metis linorder_linear not_le) + done + have th1: "\z x e d :: real. z <= x + e \ e < d ==> z < x \ abs(z - x) < d" by arith + have th2: "\e x:: real. 0 < e ==> ~(x + e <= x)" by arith + have "\d::real. 0 < d \ 0 < d/2 \ d/2 < d" by simp + then have th3: "\d::real. d > 0 \ \e > 0. e < d" by blast + { assume le2: "f l \ e2" + from le2 fa fb e12 alb have la: "l \ a" by metis + then have lap: "l - a > 0" using alb by arith + from e2[rule_format, OF le2] obtain e where + e: "e > 0" "\y. dist y (f l) < e \ y \ e2" by metis + from dst[OF alb e(1)] obtain d where + d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis + let ?d' = "min (d/2) ((l - a)/2)" + have "?d' < d \ 0 < ?d' \ ?d' < l - a" using lap d(1) + by (simp add: min_max.less_infI2) + then have "\d'. d' < d \ d' >0 \ l - d' > a" by auto + then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis + from d e have th0: "\y. \y - l\ < d \ f y \ e2" by metis + from th0[rule_format, of "l - d'"] d' have "f (l - d') \ e2" by auto moreover - {assume le1: "f l \ e1" + have "f (l - d') \ e1" using ale1[rule_format, of "l -d'"] d' by auto + ultimately have False using e12 alb d' by auto } + moreover + { assume le1: "f l \ e1" from le1 fa fb e12 alb have lb: "l \ b" by metis - hence blp: "b - l > 0" using alb by arith - from e1[rule_format, OF le1] obtain e where - e: "e > 0" "\y. dist y (f l) < e \ y \ e1" by metis - from dst[OF alb e(1)] obtain d where - d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis - have "\d::real. 0 < d \ d/2 < d \ 0 < d/2" by simp - then have "\d'. d' < d \ d' >0" using d(1) by blast - then obtain d' where d': "d' > 0" "d' < d" by metis - from d e have th0: "\y. \y - l\ < d \ f y \ e1" by auto - hence "\y. l \ y \ y \ l + d' \ f y \ e1" using d' by auto - with ale1 have "\y. a \ y \ y \ l + d' \ f y \ e1" by auto - with l d' have False - by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } - ultimately show ?thesis using alb by metis + then have blp: "b - l > 0" using alb by arith + from e1[rule_format, OF le1] obtain e where + e: "e > 0" "\y. dist y (f l) < e \ y \ e1" by metis + from dst[OF alb e(1)] obtain d where + d: "d > 0" "\y. \y - l\ < d \ dist (f y) (f l) < e" by metis + have "\d::real. 0 < d \ d/2 < d \ 0 < d/2" by simp + then have "\d'. d' < d \ d' >0" using d(1) by blast + then obtain d' where d': "d' > 0" "d' < d" by metis + from d e have th0: "\y. \y - l\ < d \ f y \ e1" by auto + then have "\y. l \ y \ y \ l + d' \ f y \ e1" using d' by auto + with ale1 have "\y. a \ y \ y \ l + d' \ f y \ e1" by auto + with l d' have False + by (auto simp add: isLub_def isUb_def setle_def setge_def leastP_def) } + ultimately show ?thesis using alb by metis qed lemma convex_connected: fixes s :: "'a::real_normed_vector set" assumes "convex s" shows "connected s" -proof- - { fix e1 e2 assume as:"open e1" "open e2" "e1 \ e2 \ s = {}" "s \ e1 \ e2" +proof - + { fix e1 e2 + assume as:"open e1" "open e2" "e1 \ e2 \ s = {}" "s \ e1 \ e2" assume "e1 \ s \ {}" "e2 \ s \ {}" then obtain x1 x2 where x1:"x1\e1" "x1\s" and x2:"x2\e2" "x2\s" by auto - hence n:"norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto + then have n: "norm (x1 - x2) > 0" unfolding zero_less_norm_iff using as(3) by auto { fix x e::real assume as:"0 \ x" "x \ 1" "0 < e" - { fix y have *:"(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2" + { fix y + have *: "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2) = (y - x) *\<^sub>R x1 - (y - x) *\<^sub>R x2" by (simp add: algebra_simps) assume "\y - x\ < e / norm (x1 - x2)" hence "norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e" unfolding * and scaleR_right_diff_distrib[symmetric] - unfolding less_divide_eq using n by auto } - hence "\d>0. \y. \y - x\ < d \ norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e" - apply(rule_tac x="e / norm (x1 - x2)" in exI) using as - apply auto unfolding zero_less_divide_iff using n by simp } note * = this + unfolding less_divide_eq using n by auto + } + then have "\d>0. \y. \y - x\ < d \ norm ((1 - x) *\<^sub>R x1 + x *\<^sub>R x2 - ((1 - y) *\<^sub>R x1 + y *\<^sub>R x2)) < e" + apply (rule_tac x="e / norm (x1 - x2)" in exI) + using as + apply auto + unfolding zero_less_divide_iff + using n apply simp + done + } note * = this have "\x\0. x \ 1 \ (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e1 \ (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e2" - apply(rule connected_real_lemma) apply (simp add: `x1\e1` `x2\e2` dist_commute)+ - using * apply(simp add: dist_norm) + apply (rule connected_real_lemma) + apply (simp add: `x1\e1` `x2\e2` dist_commute)+ + using * apply (simp add: dist_norm) using as(1,2)[unfolded open_dist] apply simp using as(1,2)[unfolded open_dist] apply simp using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2 - using as(3) by auto - then obtain x where "x\0" "x\1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e2" by auto - hence False using as(4) + using as(3) apply auto + done + then obtain x where "x\0" "x\1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \ e2" + by auto + then have False + using as(4) using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] - using x1(2) x2(2) by auto } - thus ?thesis unfolding connected_def by auto + using x1(2) x2(2) by auto + } + then show ?thesis unfolding connected_def by auto qed text {* One rather trivial consequence. *} @@ -1276,37 +1297,53 @@ hence xy:"0 < dist x y" by (auto simp add: dist_nz[symmetric]) then obtain u where "0 < u" "u \ 1" and u:"u < e / dist x y" - using real_lbound_gt_zero[of 1 "e / dist x y"] using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto + using real_lbound_gt_zero[of 1 "e / dist x y"] + using xy `e>0` and divide_pos_pos[of e "dist x y"] by auto hence "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \ (1-u) * f x + u * f y" using `x\s` `y\s` - using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto + using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] + by auto moreover - have *:"x - ((1 - u) *\<^sub>R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" by (simp add: algebra_simps) - have "(1 - u) *\<^sub>R x + u *\<^sub>R y \ ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0R x + u *\<^sub>R y) = u *\<^sub>R (x - y)" + by (simp add: algebra_simps) + have "(1 - u) *\<^sub>R x + u *\<^sub>R y \ ball x e" + unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0 f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto - ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto + then have "f x \ f ((1 - u) *\<^sub>R x + u *\<^sub>R y)" using assms(4) by auto + ultimately show False + using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto qed lemma convex_ball: fixes x :: "'a::real_normed_vector" shows "convex (ball x e)" -proof(auto simp add: convex_def) - fix y z assume yz:"dist x y < e" "dist x z < e" - fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" - have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" using uv yz - using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto - thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using convex_bound_lt[OF yz uv] by auto +proof (auto simp add: convex_def) + fix y z + assume yz: "dist x y < e" "dist x z < e" + fix u v :: real + assume uv: "0 \ u" "0 \ v" "u + v = 1" + have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" + using uv yz + using convex_distance[of "ball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] + by auto + then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" + using convex_bound_lt[OF yz uv] by auto qed lemma convex_cball: fixes x :: "'a::real_normed_vector" shows "convex(cball x e)" -proof(auto simp add: convex_def Ball_def) - fix y z assume yz:"dist x y \ e" "dist x z \ e" - fix u v ::real assume uv:" 0 \ u" "0 \ v" "u + v = 1" - have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" using uv yz - using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] by auto - thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \ e" using convex_bound_le[OF yz uv] by auto +proof (auto simp add: convex_def Ball_def) + fix y z + assume yz: "dist x y \ e" "dist x z \ e" + fix u v :: real + assume uv: "0 \ u" "0 \ v" "u + v = 1" + have "dist x (u *\<^sub>R y + v *\<^sub>R z) \ u * dist x y + v * dist x z" + using uv yz + using convex_distance[of "cball x e" x, unfolded convex_on_def, THEN bspec[where x=y], THEN bspec[where x=z]] + by auto + then show "dist x (u *\<^sub>R y + v *\<^sub>R z) \ e" + using convex_bound_le[OF yz uv] by auto qed lemma connected_ball: @@ -1319,6 +1356,7 @@ shows "connected(cball x e)" using convex_connected convex_cball by auto + subsection {* Convex hull *} lemma convex_convex_hull: "convex(convex hull s)" @@ -1326,102 +1364,182 @@ by auto lemma convex_hull_eq: "convex hull s = s \ convex s" -by (metis convex_convex_hull hull_same) + by (metis convex_convex_hull hull_same) lemma bounded_convex_hull: fixes s :: "'a::real_normed_vector set" assumes "bounded s" shows "bounded(convex hull s)" -proof- from assms obtain B where B:"\x\s. norm x \ B" unfolding bounded_iff by auto - show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B]) +proof - + from assms obtain B where B: "\x\s. norm x \ B" + unfolding bounded_iff by auto + show ?thesis + apply (rule bounded_subset[OF bounded_cball, of _ 0 B]) unfolding subset_hull[of convex, OF convex_cball] - unfolding subset_eq mem_cball dist_norm using B by auto qed + unfolding subset_eq mem_cball dist_norm using B apply auto + done +qed lemma finite_imp_bounded_convex_hull: fixes s :: "'a::real_normed_vector set" shows "finite s \ bounded(convex hull s)" using bounded_convex_hull finite_imp_bounded by auto + subsubsection {* Convex hull is "preserved" by a linear function *} lemma convex_hull_linear_image: assumes "bounded_linear f" shows "f ` (convex hull s) = convex hull (f ` s)" - apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3 - apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption - apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption -proof- + apply rule + unfolding subset_eq ball_simps + apply (rule_tac[!] hull_induct, rule hull_inc) + prefer 3 + apply (erule imageE) + apply (rule_tac x=xa in image_eqI) + apply assumption + apply (rule hull_subset[unfolded subset_eq, rule_format]) + apply assumption +proof - interpret f: bounded_linear f by fact show "convex {x. f x \ convex hull f ` s}" - unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next + unfolding convex_def + by (auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) +next interpret f: bounded_linear f by fact - show "convex {x. x \ f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s] + show "convex {x. x \ f ` (convex hull s)}" + using convex_convex_hull[unfolded convex_def, of s] unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric]) qed auto lemma in_convex_hull_linear_image: assumes "bounded_linear f" "x \ convex hull s" shows "(f x) \ convex hull (f ` s)" -using convex_hull_linear_image[OF assms(1)] assms(2) by auto + using convex_hull_linear_image[OF assms(1)] assms(2) by auto + subsubsection {* Stepping theorems for convex hulls of finite sets *} lemma convex_hull_empty[simp]: "convex hull {} = {}" - apply(rule hull_unique) by auto + by (rule hull_unique) auto lemma convex_hull_singleton[simp]: "convex hull {a} = {a}" - apply(rule hull_unique) by auto + by (rule hull_unique) auto lemma convex_hull_insert: fixes s :: "'a::real_vector set" assumes "s \ {}" - shows "convex hull (insert a s) = {x. \u\0. \v\0. \b. (u + v = 1) \ - b \ (convex hull s) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull") - apply(rule,rule hull_minimal,rule) unfolding insert_iff prefer 3 apply rule proof- - fix x assume x:"x = a \ x \ s" - thus "x\?hull" apply rule unfolding mem_Collect_eq apply(rule_tac x=1 in exI) defer - apply(rule_tac x=0 in exI) using assms hull_subset[of s convex] by auto + shows "convex hull (insert a s) = + {x. \u\0. \v\0. \b. (u + v = 1) \ b \ (convex hull s) \ (x = u *\<^sub>R a + v *\<^sub>R b)}" + (is "?xyz = ?hull") + apply (rule, rule hull_minimal, rule) + unfolding insert_iff + prefer 3 + apply rule +proof - + fix x + assume x: "x = a \ x \ s" + then show "x \ ?hull" + apply rule + unfolding mem_Collect_eq + apply (rule_tac x=1 in exI) + defer + apply (rule_tac x=0 in exI) + using assms hull_subset[of s convex] + apply auto + done next - fix x assume "x\?hull" - then obtain u v b where obt:"u\0" "v\0" "u + v = 1" "b \ convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" by auto - have "a\convex hull insert a s" "b\convex hull insert a s" - using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) by auto - thus "x\ convex hull insert a s" unfolding obt(5) using convex_convex_hull[of "insert a s", unfolded convex_def] - apply(erule_tac x=a in ballE) apply(erule_tac x=b in ballE) apply(erule_tac x=u in allE) using obt by auto + fix x + assume "x \ ?hull" + then obtain u v b where obt: "u\0" "v\0" "u + v = 1" "b \ convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" + by auto + have "a \ convex hull insert a s" "b\convex hull insert a s" + using hull_mono[of s "insert a s" convex] hull_mono[of "{a}" "insert a s" convex] and obt(4) + by auto + then show "x \ convex hull insert a s" + unfolding obt(5) + using convex_convex_hull[of "insert a s", unfolded convex_def] + apply (erule_tac x = a in ballE) + apply (erule_tac x = b in ballE) + apply (erule_tac x = u in allE) + using obt apply auto + done next - show "convex ?hull" unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof- - fix x y u v assume as:"(0::real) \ u" "0 \ v" "u + v = 1" "x\?hull" "y\?hull" - from as(4) obtain u1 v1 b1 where obt1:"u1\0" "v1\0" "u1 + v1 = 1" "b1 \ convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto - from as(5) obtain u2 v2 b2 where obt2:"u2\0" "v2\0" "u2 + v2 = 1" "b2 \ convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto - have *:"\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) - have "\b \ convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" - proof(cases "u * v1 + v * v2 = 0") - have *:"\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps) - case True hence **:"u * v1 = 0" "v * v2 = 0" + show "convex ?hull" + unfolding convex_def + apply (rule, rule, rule, rule, rule, rule, rule) + proof - + fix x y u v + assume as: "(0::real) \ u" "0 \ v" "u + v = 1" "x\?hull" "y\?hull" + from as(4) obtain u1 v1 b1 + where obt1: "u1\0" "v1\0" "u1 + v1 = 1" "b1 \ convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto + from as(5) obtain u2 v2 b2 + where obt2: "u2\0" "v2\0" "u2 + v2 = 1" "b2 \ convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto + have *: "\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" + by (auto simp add: algebra_simps) + have **: "\b \ convex hull s. u *\<^sub>R x + v *\<^sub>R y = + (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)" + proof (cases "u * v1 + v * v2 = 0") + case True + have *: "\(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" + by (auto simp add: algebra_simps) + from True have ***: "u * v1 = 0" "v * v2 = 0" using mult_nonneg_nonneg[OF `u\0` `v1\0`] mult_nonneg_nonneg[OF `v\0` `v2\0`] by arith+ - hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto - thus ?thesis unfolding obt1(5) obt2(5) * using assms hull_subset[of s convex] by(auto simp add: ** scaleR_right_distrib) + then have "u * u1 + v * u2 = 1" + using as(3) obt1(3) obt2(3) by auto + then show ?thesis + unfolding obt1(5) obt2(5) * + using assms hull_subset[of s convex] + by (auto simp add: *** scaleR_right_distrib) next - have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) - also have "\ = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) - also have "\ = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto - case False have "0 \ u * v1 + v * v2" "0 \ u * v1" "0 \ u * v1 + v * v2" "0 \ v * v2" apply - - apply(rule add_nonneg_nonneg) prefer 4 apply(rule add_nonneg_nonneg) apply(rule_tac [!] mult_nonneg_nonneg) - using as(1,2) obt1(1,2) obt2(1,2) by auto - thus ?thesis unfolding obt1(5) obt2(5) unfolding * and ** using False - apply(rule_tac x="((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) defer - apply(rule convex_convex_hull[of s, unfolded convex_def, rule_format]) using obt1(4) obt2(4) + case False + have "1 - (u * u1 + v * u2) = (u + v) - (u * u1 + v * u2)" + using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) + also have "\ = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" + using as(3) obt1(3) obt2(3) by (auto simp add: field_simps) + also have "\ = u * v1 + v * v2" + by simp + finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto + have "0 \ u * v1 + v * v2" "0 \ u * v1" "0 \ u * v1 + v * v2" "0 \ v * v2" + apply (rule add_nonneg_nonneg) + prefer 4 + apply (rule add_nonneg_nonneg) + apply (rule_tac [!] mult_nonneg_nonneg) + using as(1,2) obt1(1,2) obt2(1,2) apply auto + done + then show ?thesis + unfolding obt1(5) obt2(5) + unfolding * and ** + using False + apply (rule_tac x = "((u * v1) / (u * v1 + v * v2)) *\<^sub>R b1 + ((v * v2) / (u * v1 + v * v2)) *\<^sub>R b2" in bexI) + defer + apply (rule convex_convex_hull[of s, unfolded convex_def, rule_format]) + using obt1(4) obt2(4) unfolding add_divide_distrib[symmetric] and zero_le_divide_iff - by (auto simp add: scaleR_left_distrib scaleR_right_distrib) - qed note * = this - have u1:"u1 \ 1" unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto - have u2:"u2 \ 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto - have "u1 * u + u2 * v \ (max u1 u2) * u + (max u1 u2) * v" apply(rule add_mono) - apply(rule_tac [!] mult_right_mono) using as(1,2) obt1(1,2) obt2(1,2) by auto - also have "\ \ 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto - finally - show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" unfolding mem_Collect_eq apply(rule_tac x="u * u1 + v * u2" in exI) - apply(rule conjI) defer apply(rule_tac x="1 - u * u1 - v * u2" in exI) unfolding Bex_def - using as(1,2) obt1(1,2) obt2(1,2) * by(auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps) + apply (auto simp add: scaleR_left_distrib scaleR_right_distrib) + done + qed + have u1: "u1 \ 1" + unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto + have u2: "u2 \ 1" + unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto + have "u1 * u + u2 * v \ (max u1 u2) * u + (max u1 u2) * v" + apply (rule add_mono) + apply (rule_tac [!] mult_right_mono) + using as(1,2) obt1(1,2) obt2(1,2) + apply auto + done + also have "\ \ 1" + unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto + finally show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" + unfolding mem_Collect_eq + apply (rule_tac x="u * u1 + v * u2" in exI) + apply (rule conjI) + defer + apply (rule_tac x="1 - u * u1 - v * u2" in exI) + unfolding Bex_def + using as(1,2) obt1(1,2) obt2(1,2) ** + apply (auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps) + done qed qed @@ -1430,162 +1548,307 @@ lemma convex_hull_indexed: fixes s :: "'a::real_vector set" - shows "convex hull s = {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ s) \ - (setsum u {1..k} = 1) \ - (setsum (\i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull") - apply(rule hull_unique) apply(rule) defer - apply(subst convex_def) apply(rule,rule,rule,rule,rule,rule,rule) -proof- - fix x assume "x\s" - thus "x \ ?hull" unfolding mem_Collect_eq apply(rule_tac x=1 in exI, rule_tac x="\x. 1" in exI) by auto + shows "convex hull s = + {y. \k u x. (\i\{1::nat .. k}. 0 \ u i \ x i \ s) \ + (setsum u {1..k} = 1) \ + (setsum (\i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull") + apply (rule hull_unique) + apply rule + defer + apply (subst convex_def) + apply (rule, rule, rule, rule, rule, rule, rule) +proof - + fix x + assume "x\s" + then show "x \ ?hull" + unfolding mem_Collect_eq + apply (rule_tac x=1 in exI, rule_tac x="\x. 1" in exI) + apply auto + done next - fix t assume as:"s \ t" "convex t" - show "?hull \ t" apply(rule) unfolding mem_Collect_eq apply(erule exE | erule conjE)+ proof- - fix x k u y assume assm:"\i\{1::nat..k}. 0 \ u i \ y i \ s" "setsum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x" - show "x\t" unfolding assm(3)[symmetric] apply(rule as(2)[unfolded convex, rule_format]) - using assm(1,2) as(1) by auto qed + fix t + assume as: "s \ t" "convex t" + show "?hull \ t" + apply rule + unfolding mem_Collect_eq + apply (erule exE | erule conjE)+ + proof - + fix x k u y + assume assm: + "\i\{1::nat..k}. 0 \ u i \ y i \ s" + "setsum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x" + show "x\t" + unfolding assm(3) [symmetric] + apply (rule as(2)[unfolded convex, rule_format]) + using assm(1,2) as(1) apply auto + done + qed next - fix x y u v assume uv:"0\u" "0\v" "u+v=(1::real)" and xy:"x\?hull" "y\?hull" - from xy obtain k1 u1 x1 where x:"\i\{1::nat..k1}. 0\u1 i \ x1 i \ s" "setsum u1 {Suc 0..k1} = 1" "(\i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto - from xy obtain k2 u2 x2 where y:"\i\{1::nat..k2}. 0\u2 i \ x2 i \ s" "setsum u2 {Suc 0..k2} = 1" "(\i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto - have *:"\P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)" + fix x y u v + assume uv: "0\u" "0\v" "u + v = (1::real)" and xy: "x\?hull" "y\?hull" + from xy obtain k1 u1 x1 where + x: "\i\{1::nat..k1}. 0\u1 i \ x1 i \ s" "setsum u1 {Suc 0..k1} = 1" "(\i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" + by auto + from xy obtain k2 u2 x2 where + y: "\i\{1::nat..k2}. 0\u2 i \ x2 i \ s" "setsum u2 {Suc 0..k2} = 1" "(\i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" + by auto + have *: "\P (x1::'a) x2 s1 s2 i. + (if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)" "{1..k1 + k2} \ {1..k1} = {1..k1}" "{1..k1 + k2} \ - {1..k1} = (\i. i + k1) ` {1..k2}" - prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le) - have inj:"inj_on (\i. i + k1) {1..k2}" unfolding inj_on_def by auto - show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" apply(rule) - apply(rule_tac x="k1 + k2" in exI, rule_tac x="\i. if i \ {1..k1} then u * u1 i else v * u2 (i - k1)" in exI) - apply(rule_tac x="\i. if i \ {1..k1} then x1 i else x2 (i - k1)" in exI) apply(rule,rule) defer apply(rule) - unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and setsum_reindex[OF inj] and o_def Collect_mem_eq - unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric] proof- - fix i assume i:"i \ {1..k1+k2}" - show "0 \ (if i \ {1..k1} then u * u1 i else v * u2 (i - k1)) \ (if i \ {1..k1} then x1 i else x2 (i - k1)) \ s" - proof(cases "i\{1..k1}") - case True thus ?thesis using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto - next def j \ "i - k1" - case False with i have "j \ {1..k2}" unfolding j_def by auto - thus ?thesis unfolding j_def[symmetric] using False - using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] by auto qed - qed(auto simp add: not_le x(2,3) y(2,3) uv(3)) + prefer 3 + apply (rule, rule) + unfolding image_iff + apply (rule_tac x = "x - k1" in bexI) + apply (auto simp add: not_le) + done + have inj: "inj_on (\i. i + k1) {1..k2}" + unfolding inj_on_def by auto + show "u *\<^sub>R x + v *\<^sub>R y \ ?hull" + apply rule + apply (rule_tac x="k1 + k2" in exI) + apply (rule_tac x="\i. if i \ {1..k1} then u * u1 i else v * u2 (i - k1)" in exI) + apply (rule_tac x="\i. if i \ {1..k1} then x1 i else x2 (i - k1)" in exI) + apply (rule, rule) + defer + apply rule + unfolding * and setsum_cases[OF finite_atLeastAtMost[of 1 "k1 + k2"]] and + setsum_reindex[OF inj] and o_def Collect_mem_eq + unfolding scaleR_scaleR[symmetric] scaleR_right.setsum [symmetric] setsum_right_distrib[symmetric] + proof - + fix i + assume i: "i \ {1..k1+k2}" + show "0 \ (if i \ {1..k1} then u * u1 i else v * u2 (i - k1)) \ + (if i \ {1..k1} then x1 i else x2 (i - k1)) \ s" + proof (cases "i\{1..k1}") + case True + then show ?thesis + using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]] by auto + next + case False + def j \ "i - k1" + from i False have "j \ {1..k2}" unfolding j_def by auto + then show ?thesis + unfolding j_def[symmetric] + using False + using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]] + apply auto + done + qed + qed (auto simp add: not_le x(2,3) y(2,3) uv(3)) qed lemma convex_hull_finite: fixes s :: "'a::real_vector set" assumes "finite s" shows "convex hull s = {y. \u. (\x\s. 0 \ u x) \ - setsum u s = 1 \ setsum (\x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set") -proof(rule hull_unique, auto simp add: convex_def[of ?set]) - fix x assume "x\s" thus " \u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) = x" - apply(rule_tac x="\y. if x=y then 1 else 0" in exI) apply auto - unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] by auto + setsum u s = 1 \ setsum (\x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set") +proof (rule hull_unique, auto simp add: convex_def[of ?set]) + fix x + assume "x \ s" + then show "\u. (\x\s. 0 \ u x) \ setsum u s = 1 \ (\x\s. u x *\<^sub>R x) = x" + apply (rule_tac x="\y. if x=y then 1 else 0" in exI) + apply auto + unfolding setsum_delta'[OF assms] and setsum_delta''[OF assms] + apply auto + done next - fix u v ::real assume uv:"0 \ u" "0 \ v" "u + v = 1" - fix ux assume ux:"\x\s. 0 \ ux x" "setsum ux s = (1::real)" - fix uy assume uy:"\x\s. 0 \ uy x" "setsum uy s = (1::real)" - { fix x assume "x\s" - hence "0 \ u * ux x + v * uy x" using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2) - by (auto, metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2)) } - moreover have "(\x\s. u * ux x + v * uy x) = 1" + fix u v :: real + assume uv: "0 \ u" "0 \ v" "u + v = 1" + fix ux assume ux: "\x\s. 0 \ ux x" "setsum ux s = (1::real)" + fix uy assume uy: "\x\s. 0 \ uy x" "setsum uy s = (1::real)" + { fix x + assume "x\s" + then have "0 \ u * ux x + v * uy x" + using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2) + apply auto + apply (metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2)) + done + } + moreover + have "(\x\s. u * ux x + v * uy x) = 1" unfolding setsum_addf and setsum_right_distrib[symmetric] and ux(2) uy(2) using uv(3) by auto - moreover have "(\x\s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" - unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] by auto - ultimately show "\uc. (\x\s. 0 \ uc x) \ setsum uc s = 1 \ (\x\s. uc x *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" - apply(rule_tac x="\x. u * ux x + v * uy x" in exI) by auto + moreover + have "(\x\s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" + unfolding scaleR_left_distrib and setsum_addf and scaleR_scaleR[symmetric] and scaleR_right.setsum [symmetric] + by auto + ultimately + show "\uc. (\x\s. 0 \ uc x) \ setsum uc s = 1 \ + (\x\s. uc x *\<^sub>R x) = u *\<^sub>R (\x\s. ux x *\<^sub>R x) + v *\<^sub>R (\x\s. uy x *\<^sub>R x)" + apply (rule_tac x="\x. u * ux x + v * uy x" in exI) + apply auto + done next - fix t assume t:"s \ t" "convex t" - fix u assume u:"\x\s. 0 \ u x" "setsum u s = (1::real)" - thus "(\x\s. u x *\<^sub>R x) \ t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]] + fix t + assume t: "s \ t" "convex t" + fix u + assume u: "\x\s. 0 \ u x" "setsum u s = (1::real)" + then show "(\x\s. u x *\<^sub>R x) \ t" + using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]] using assms and t(1) by auto qed + subsubsection {* Another formulation from Lars Schewe *} lemma setsum_constant_scaleR: fixes y :: "'a::real_vector" shows "(\x\A. y) = of_nat (card A) *\<^sub>R y" -apply (cases "finite A") -apply (induct set: finite) -apply (simp_all add: algebra_simps) -done + apply (cases "finite A") + apply (induct set: finite) + apply (simp_all add: algebra_simps) + done lemma convex_hull_explicit: fixes p :: "'a::real_vector set" shows "convex hull p = {y. \s u. finite s \ s \ p \ - (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs") -proof- + (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs") +proof - { fix x assume "x\?lhs" - then obtain k u y where obt:"\i\{1::nat..k}. 0 \ u i \ y i \ p" "setsum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x" + then obtain k u y where + obt: "\i\{1::nat..k}. 0 \ u i \ y i \ p" "setsum u {1..k} = 1" "(\i = 1..k. u i *\<^sub>R y i) = x" unfolding convex_hull_indexed by auto - have fin:"finite {1..k}" by auto - have fin':"\v. finite {i \ {1..k}. y i = v}" by auto - { fix j assume "j\{1..k}" - hence "y j \ p" "0 \ setsum u {i. Suc 0 \ i \ i \ k \ y i = y j}" - using obt(1)[THEN bspec[where x=j]] and obt(2) apply simp - apply(rule setsum_nonneg) using obt(1) by auto } + have fin: "finite {1..k}" by auto + have fin': "\v. finite {i \ {1..k}. y i = v}" by auto + { fix j + assume "j\{1..k}" + then have "y j \ p" "0 \ setsum u {i. Suc 0 \ i \ i \ k \ y i = y j}" + using obt(1)[THEN bspec[where x=j]] and obt(2) + apply simp + apply (rule setsum_nonneg) + using obt(1) + apply auto + done + } moreover have "(\v\y ` {1..k}. setsum u {i \ {1..k}. y i = v}) = 1" unfolding setsum_image_gen[OF fin, symmetric] using obt(2) by auto moreover have "(\v\y ` {1..k}. setsum u {i \ {1..k}. y i = v} *\<^sub>R v) = x" using setsum_image_gen[OF fin, of "\i. u i *\<^sub>R y i" y, symmetric] unfolding scaleR_left.setsum using obt(3) by auto - ultimately have "\s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = x" - apply(rule_tac x="y ` {1..k}" in exI) - apply(rule_tac x="\v. setsum u {i\{1..k}. y i = v}" in exI) by auto - hence "x\?rhs" by auto } + ultimately + have "\s u. finite s \ s \ p \ (\x\s. 0 \ u x) \ setsum u s = 1 \ (\v\s. u v *\<^sub>R v) = x" + apply (rule_tac x="y ` {1..k}" in exI) + apply (rule_tac x="\v. setsum u {i\{1..k}. y i = v}" in exI) + apply auto + done + then have "x\?rhs" by auto + } moreover { fix y assume "y\?rhs" - then obtain s u where obt:"finite s" "s \ p" "\x\s. 0 \ u x" "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = y" by auto - - obtain f where f:"inj_on f {1..card s}" "f ` {1..card s} = s" using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto - - { fix i::nat assume "i\{1..card s}" - hence "f i \ s" apply(subst f(2)[symmetric]) by auto - hence "0 \ u (f i)" "f i \ p" using obt(2,3) by auto } + then obtain s u where + obt: "finite s" "s \ p" "\x\s. 0 \ u x" "setsum u s = 1" "(\v\s. u v *\<^sub>R v) = y" by auto + + obtain f where f: "inj_on f {1..card s}" "f ` {1..card s} = s" + using ex_bij_betw_nat_finite_1[OF obt(1)] unfolding bij_betw_def by auto + + { fix i :: nat + assume "i\{1..card s}" + then have "f i \ s" + apply (subst f(2)[symmetric]) + apply auto + done + then have "0 \ u (f i)" "f i \ p" using obt(2,3) by auto + } moreover have *:"finite {1..card s}" by auto - { fix y assume "y\s" - then obtain i where "i\{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto - hence "{x. Suc 0 \ x \ x \ card s \ f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto - hence "card {x. Suc 0 \ x \ x \ card s \ f x = y} = 1" by auto - hence "(\x\{x \ {1..card s}. f x = y}. u (f x)) = u y" - "(\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" - by (auto simp add: setsum_constant_scaleR) } - - hence "(\x = 1..card s. u (f x)) = 1" "(\i = 1..card s. u (f i) *\<^sub>R f i) = y" + { fix y + assume "y\s" + then obtain i where "i\{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] + by auto + then have "{x. Suc 0 \ x \ x \ card s \ f x = y} = {i}" + apply auto + using f(1)[unfolded inj_on_def] + apply(erule_tac x=x in ballE) + apply auto + done + then have "card {x. Suc 0 \ x \ x \ card s \ f x = y} = 1" by auto + then have "(\x\{x \ {1..card s}. f x = y}. u (f x)) = u y" + "(\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" + by (auto simp add: setsum_constant_scaleR) + } + then have "(\x = 1..card s. u (f x)) = 1" "(\i = 1..card s. u (f i) *\<^sub>R f i) = y" unfolding setsum_image_gen[OF *(1), of "\x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\x. u (f x)" f] unfolding f using setsum_cong2[of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\v. u v *\<^sub>R v"] - using setsum_cong2 [of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto - - ultimately have "\k u x. (\i\{1..k}. 0 \ u i \ x i \ p) \ setsum u {1..k} = 1 \ (\i::nat = 1..k. u i *\<^sub>R x i) = y" - apply(rule_tac x="card s" in exI) apply(rule_tac x="u \ f" in exI) apply(rule_tac x=f in exI) by fastforce - hence "y \ ?lhs" unfolding convex_hull_indexed by auto } + using setsum_cong2 [of s "\y. (\x\{x \ {1..card s}. f x = y}. u (f x))" u] + unfolding obt(4,5) by auto + ultimately + have "\k u x. (\i\{1..k}. 0 \ u i \ x i \ p) \ setsum u {1..k} = 1 \ + (\i::nat = 1..k. u i *\<^sub>R x i) = y" + apply (rule_tac x="card s" in exI) + apply (rule_tac x="u \ f" in exI) + apply (rule_tac x=f in exI) + apply fastforce + done + then have "y \ ?lhs" unfolding convex_hull_indexed by auto + } ultimately show ?thesis unfolding set_eq_iff by blast qed + subsubsection {* A stepping theorem for that expansion *} lemma convex_hull_finite_step: - fixes s :: "'a::real_vector set" assumes "finite s" + fixes s :: "'a::real_vector set" + assumes "finite s" shows "(\u. (\x\insert a s. 0 \ u x) \ setsum u (insert a s) = w \ setsum (\x. u x *\<^sub>R x) (insert a s) = y) \ (\v\0. \u. (\x\s. 0 \ u x) \ setsum u s = w - v \ setsum (\x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs") -proof(rule, case_tac[!] "a\s") - assume "a\s" hence *:"insert a s = s" by auto - assume ?lhs thus ?rhs unfolding * apply(rule_tac x=0 in exI) by auto +proof (rule, case_tac[!] "a\s") + assume "a\s" + then have *:" insert a s = s" by auto + assume ?lhs + then show ?rhs + unfolding * + apply (rule_tac x=0 in exI) + apply auto + done next - assume ?lhs then obtain u where u:"\x\insert a s. 0 \ u x" "setsum u (insert a s) = w" "(\x\insert a s. u x *\<^sub>R x) = y" by auto - assume "a\s" thus ?rhs apply(rule_tac x="u a" in exI) using u(1)[THEN bspec[where x=a]] apply simp - apply(rule_tac x=u in exI) using u[unfolded setsum_clauses(2)[OF assms]] and `a\s` by auto + assume ?lhs + then obtain u where u: "\x\insert a s. 0 \ u x" "setsum u (insert a s) = w" "(\x\insert a s. u x *\<^sub>R x) = y" + by auto + assume "a \ s" + then show ?rhs + apply (rule_tac x="u a" in exI) + using u(1)[THEN bspec[where x=a]] + apply simp + apply (rule_tac x=u in exI) + using u[unfolded setsum_clauses(2)[OF assms]] and `a\s` + apply auto + done next - assume "a\s" hence *:"insert a s = s" by auto - have fin:"finite (insert a s)" using assms by auto - assume ?rhs then obtain v u where uv:"v\0" "\x\s. 0 \ u x" "setsum u s = w - v" "(\x\s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto - show ?lhs apply(rule_tac x="\x. (if a = x then v else 0) + u x" in exI) unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin] - unfolding setsum_clauses(2)[OF assms] using uv and uv(2)[THEN bspec[where x=a]] and `a\s` by auto + assume "a \ s" + then have *: "insert a s = s" by auto + have fin: "finite (insert a s)" using assms by auto + assume ?rhs + then obtain v u where uv: "v\0" "\x\s. 0 \ u x" "setsum u s = w - v" "(\x\s. u x *\<^sub>R x) = y - v *\<^sub>R a" + by auto + show ?lhs + apply (rule_tac x = "\x. (if a = x then v else 0) + u x" in exI) + unfolding scaleR_left_distrib and setsum_addf and setsum_delta''[OF fin] and setsum_delta'[OF fin] + unfolding setsum_clauses(2)[OF assms] + using uv and uv(2)[THEN bspec[where x=a]] and `a\s` + apply auto + done next - assume ?rhs then obtain v u where uv:"v\0" "\x\s. 0 \ u x" "setsum u s = w - v" "(\x\s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto - moreover assume "a\s" moreover have "(\x\s. if a = x then v else u x) = setsum u s" "(\x\s. (if a = x then v else u x) *\<^sub>R x) = (\x\s. u x *\<^sub>R x)" - apply(rule_tac setsum_cong2) defer apply(rule_tac setsum_cong2) using `a\s` by auto - ultimately show ?lhs apply(rule_tac x="\x. if a = x then v else u x" in exI) unfolding setsum_clauses(2)[OF assms] by auto -qed + assume ?rhs + then obtain v u where uv: "v\0" "\x\s. 0 \ u x" "setsum u s = w - v" "(\x\s. u x *\<^sub>R x) = y - v *\<^sub>R a" + by auto + moreover + assume "a \ s" + moreover + have "(\x\s. if a = x then v else u x) = setsum u s" "(\x\s. (if a = x then v else u x) *\<^sub>R x) = (\x\s. u x *\<^sub>R x)" + apply (rule_tac setsum_cong2) + defer + apply (rule_tac setsum_cong2) + using `a \ s` + apply auto + done + ultimately show ?lhs + apply (rule_tac x="\x. if a = x then v else u x" in exI) + unfolding setsum_clauses(2)[OF assms] + apply auto + done +qed + subsubsection {* Hence some special cases *} diff -r fec14e8fefb8 -r b6659475b5af src/Pure/General/socket_io.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/socket_io.ML Thu Jan 10 23:02:58 2013 +0100 @@ -0,0 +1,87 @@ +(* Title: Pure/General/socket_io.ML + Author: Timothy Bourke, NICTA + Author: Makarius + +Stream IO over TCP sockets. Following example 10.2 in "The Standard +ML Basis Library" by Emden R. Gansner and John H. Reppy. + +Note: BinIO requires Poly/ML 5.5.x to work reliably. +*) + +signature SOCKET_IO = +sig + val make_streams: Socket.active INetSock.stream_sock -> BinIO.instream * BinIO.outstream + val open_streams: string -> BinIO.instream * BinIO.outstream +end; + +structure Socket_IO: SOCKET_IO = +struct + +fun make_streams socket = + let + val (host, port) = INetSock.fromAddr (Socket.Ctl.getSockName socket); + val name = NetHostDB.toString host ^ ":" ^ string_of_int port; + + val rd = + BinPrimIO.RD { + name = name, + chunkSize = Socket.Ctl.getRCVBUF socket, + readVec = SOME (fn n => Socket.recvVec (socket, n)), + readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)), + readVecNB = NONE, + readArrNB = NONE, + block = NONE, + canInput = NONE, + avail = fn () => NONE, + getPos = NONE, + setPos = NONE, + endPos = NONE, + verifyPos = NONE, + close = fn () => Socket.close socket, + ioDesc = NONE + }; + + val wr = + BinPrimIO.WR { + name = name, + chunkSize = Socket.Ctl.getSNDBUF socket, + writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)), + writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)), + writeVecNB = NONE, + writeArrNB = NONE, + block = NONE, + canOutput = NONE, + getPos = NONE, + setPos = NONE, + endPos = NONE, + verifyPos = NONE, + close = fn () => Socket.close socket, + ioDesc = NONE + }; + + val in_stream = + BinIO.mkInstream + (BinIO.StreamIO.mkInstream (rd, Word8Vector.fromList [])); + + val out_stream = + BinIO.mkOutstream + (BinIO.StreamIO.mkOutstream (wr, IO.BLOCK_BUF)); + + in (in_stream, out_stream) end; + + +fun open_streams socket_name = + let + fun err () = error ("Bad socket name: " ^ quote socket_name); + val (host, port) = + (case space_explode ":" socket_name of + [h, p] => + (case NetHostDB.getByName h of SOME host => host | NONE => err (), + case Int.fromString p of SOME port => port | NONE => err ()) + | _ => err ()); + val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket (); + val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port)); + in make_streams socket end; + +end; + diff -r fec14e8fefb8 -r b6659475b5af src/Pure/ML-Systems/proper_int.ML --- a/src/Pure/ML-Systems/proper_int.ML Thu Jan 10 18:19:13 2013 +0100 +++ b/src/Pure/ML-Systems/proper_int.ML Thu Jan 10 23:02:58 2013 +0100 @@ -257,13 +257,6 @@ (* Sockets *) -structure Socket = -struct - open Socket; - fun recvVec (a, b) = Socket.recvVec (a, dest_int b); - fun sendVec a = mk_int (Socket.sendVec a); -end; - structure INetSock = struct open INetSock; diff -r fec14e8fefb8 -r b6659475b5af src/Pure/ROOT --- a/src/Pure/ROOT Thu Jan 10 18:19:13 2013 +0100 +++ b/src/Pure/ROOT Thu Jan 10 23:02:58 2013 +0100 @@ -87,6 +87,7 @@ "General/seq.ML" "General/sha1.ML" "General/sha1_polyml.ML" + "General/socket_io.ML" "General/source.ML" "General/stack.ML" "General/symbol.ML" diff -r fec14e8fefb8 -r b6659475b5af src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Jan 10 18:19:13 2013 +0100 +++ b/src/Pure/ROOT.ML Thu Jan 10 23:02:58 2013 +0100 @@ -57,6 +57,7 @@ use "General/file.ML"; use "General/long_name.ML"; use "General/binding.ML"; +use "General/socket_io.ML"; use "General/sha1.ML"; if ML_System.is_polyml then use "General/sha1_polyml.ML" else (); diff -r fec14e8fefb8 -r b6659475b5af src/Pure/System/options.scala --- a/src/Pure/System/options.scala Thu Jan 10 18:19:13 2013 +0100 +++ b/src/Pure/System/options.scala Thu Jan 10 23:02:58 2013 +0100 @@ -63,8 +63,9 @@ private val SECTION = "section" private val OPTION = "option" private val OPTIONS = Path.explode("etc/options") - private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences") - private val PREFS_BACKUP = Path.explode("$ISABELLE_HOME_USER/etc/preferences~") + private val PREFS_DIR = Path.explode("$ISABELLE_HOME_USER/etc") + private val PREFS = PREFS_DIR + Path.basic("preferences") + private val PREFS_BACKUP = PREFS_DIR + Path.basic("preferences~") lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + @@ -347,6 +348,7 @@ changed.sortBy(_._1) .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString + Options.PREFS_DIR.file.mkdirs() Options.PREFS.file renameTo Options.PREFS_BACKUP.file File.write(Options.PREFS, "(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs) diff -r fec14e8fefb8 -r b6659475b5af src/Pure/System/system_channel.ML --- a/src/Pure/System/system_channel.ML Thu Jan 10 18:19:13 2013 +0100 +++ b/src/Pure/System/system_channel.ML Thu Jan 10 23:02:58 2013 +0100 @@ -47,65 +47,31 @@ end; -(* sockets *) (* FIXME proper buffering via BinIO (after Poly/ML 5.4.1) *) +(* sockets *) -local - -fun readN socket n = +fun read_line in_stream = let - fun read i buf = - let - val s = Byte.bytesToString (Socket.recvVec (socket, n - i)); - val m = size s; - val i' = i + m; - val buf' = Buffer.add s buf; - in if m > 0 andalso n > i' then read i' buf' else Buffer.content buf' end; - in read 0 Buffer.empty end; - -fun read_line socket = - let - fun result cs = implode (rev ("\n" :: cs)); + fun result cs = String.implode (rev (#"\n" :: cs)); fun read cs = - (case readN socket 1 of - "" => if null cs then NONE else SOME (result cs) - | "\n" => SOME (result cs) - | c => read (c :: cs)); + (case BinIO.input1 in_stream of + NONE => if null cs then NONE else SOME (result cs) + | SOME b => + (case Byte.byteToChar b of + #"\n" => SOME (result cs) + | c => read (c :: cs))); in read [] end; -fun write socket = - let - fun send buf = - if Word8VectorSlice.isEmpty buf then () - else - let - val n = Int.min (Word8VectorSlice.length buf, 4096); - val m = Socket.sendVec (socket, Word8VectorSlice.subslice (buf, 0, SOME n)); - val buf' = Word8VectorSlice.subslice (buf, m, NONE); - in send buf' end; - in fn s => send (Word8VectorSlice.full (Byte.stringToBytes s)) end; - -in - fun socket_rendezvous name = let - fun err () = error ("Bad socket name: " ^ quote name); - val (host, port) = - (case space_explode ":" name of - [h, p] => - (case NetHostDB.getByName h of SOME host => host | NONE => err (), - case Int.fromString p of SOME port => port | NONE => err ()) - | _ => err ()); - val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket (); - val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port)); + val (in_stream, out_stream) = Socket_IO.open_streams name; + val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); in System_Channel - {input_line = fn () => read_line socket, - inputN = fn n => readN socket n, - output = fn s => write socket s, - flush = fn () => ()} + {input_line = fn () => read_line in_stream, + inputN = fn n => Byte.bytesToString (BinIO.inputN (in_stream, n)), + output = fn s => BinIO.output (out_stream, Byte.stringToBytes s), + flush = fn () => BinIO.flushOut out_stream} end; end; -end; - diff -r fec14e8fefb8 -r b6659475b5af src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Thu Jan 10 18:19:13 2013 +0100 +++ b/src/Pure/Tools/main.scala Thu Jan 10 23:02:58 2013 +0100 @@ -17,7 +17,7 @@ try { Platform.init_laf() Isabelle_System.init() - Isabelle_System.isabelle_tool("jedit", args: _*) + Isabelle_System.isabelle_tool("jedit", ("-s" :: args.toList): _*) } catch { case exn: Throwable => (Exn.message(exn), 2) } diff -r fec14e8fefb8 -r b6659475b5af src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Thu Jan 10 18:19:13 2013 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Jan 10 23:02:58 2013 +0100 @@ -306,12 +306,11 @@ ## main -# perspective +if [ "$BUILD_ONLY" = false ]; then + mkdir -p "$JEDIT_SETTINGS/DockableWindowManager" -mkdir -p "$JEDIT_SETTINGS/DockableWindowManager" - -if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then - cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" < "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" < EOF cat > "$JEDIT_SETTINGS/perspective.xml" < EOF -fi - + fi -# main - -if [ "$BUILD_ONLY" = false ]; then if [ "$NO_BUILD" = false ]; then "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" RC="$?" diff -r fec14e8fefb8 -r b6659475b5af src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Thu Jan 10 18:19:13 2013 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Thu Jan 10 23:02:58 2013 +0100 @@ -7,6 +7,7 @@ buffer.noTabs=true buffer.sidekick.keystroke-parse=false buffer.tabSize=2 +console.dock-position=floating console.encoding=UTF-8 console.font=IsabelleText console.fontsize=14 @@ -182,7 +183,7 @@ isabelle-output.width=412 isabelle-readme.dock-position=bottom isabelle-symbols.dock-position=bottom -isabelle-theories.dock-position=bottom +isabelle-theories.dock-position=right isabelle.cancel-execution.label=Cancel execution isabelle.cancel-execution.shortcut=C+e BACK_SPACE isabelle.check-buffer.label=Commence full checking diff -r fec14e8fefb8 -r b6659475b5af src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Jan 10 18:19:13 2013 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Thu Jan 10 23:02:58 2013 +0100 @@ -189,9 +189,9 @@ react { case phase: Session.Phase => phase match { - case Session.Failed => + case Session.Inactive | Session.Failed => Swing_Thread.later { - Library.error_dialog(jEdit.getActiveView, "Prover process failure", + Library.error_dialog(jEdit.getActiveView, "Prover process terminated", "Isabelle Syslog", Library.scrollable_text(PIDE.session.current_syslog())) }