--- a/Admin/MacOS/App1/build Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/MacOS/App1/build Fri Jan 11 13:24:16 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
--- a/Admin/MacOS/App1/script Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/MacOS/App1/script Fri Jan 11 13:24:16 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
--- a/Admin/Release/CHECKLIST Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Release/CHECKLIST Fri Jan 11 13:24:16 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
--- a/Admin/Release/makebundle Thu Jan 10 21:22:11 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 '<?xml version="1.0" encoding="utf-8" ?>'
- echo '<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">'
- echo '<html xmlns="http://www.w3.org/1999/xhtml">'
- echo '<head>'
- echo '<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>'
- echo "<title>${NAME}</title>"
- echo '</head>'
- echo '<body>'
- echo '<pre>'
- perl -w -p -e "s/&/&/g; s/</</g; s/>/>/g; s/'/'/g; s/\"/"/g;" "$FILE"
- echo '</pre>'
- echo '</body>'
- } > "${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"
--- a/Admin/Windows/Cygwin/Cygwin-Setup.bat Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Windows/Cygwin/Cygwin-Setup.bat Fri Jan 11 13:24:16 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"
--- a/Admin/Windows/Cygwin/Cygwin-Terminal.bat Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Windows/Cygwin/Cygwin-Terminal.bat Fri Jan 11 13:24:16 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
--- a/Admin/Windows/Cygwin/init.bat Thu Jan 10 21:22:11 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"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/isabelle/init.bat Fri Jan 11 13:24:16 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
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/isabelle/postinstall Fri Jan 11 13:24:16 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Windows/Cygwin/isabelle/rebaseall Fri Jan 11 13:24:16 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"
--- a/Admin/Windows/Cygwin/sfx.txt Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Windows/Cygwin/sfx.txt Fri Jan 11 13:24:16 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@!
Binary file Admin/Windows/launch4j/Isabelle.exe has changed
--- a/Admin/Windows/launch4j/isabelle.xml Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/Windows/launch4j/isabelle.xml Fri Jan 11 13:24:16 2013 +0100
@@ -20,11 +20,11 @@
<cp>%EXEDIR%\lib\classes\ext\scala-swing.jar</cp>
</classPath>
<jre>
- <path>%EXEDIR%\contrib\jdk-6u31_x86-cygwin\jdk1.6.0_31</path>
+ <path>%EXEDIR%\contrib\jdk-7u9\x86-cygwin\jdk1.7.0_09</path>
<minVersion></minVersion>
<maxVersion></maxVersion>
<jdkPreference>jdkOnly</jdkPreference>
- <opt>-Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\contrib\\cygwin-1.7.9"</opt>
+ <opt>-Disabelle.home="%EXEDIR%" -Dcygwin.root="%EXEDIR%\\cygwin"</opt>
</jre>
<splash>
<file>isabelle.bmp</file>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/bundled Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,3 @@
+#additional components to be bundled for release
+ProofGeneral-4.1
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/bundled-windows Fri Jan 11 13:24:16 2013 +0100
@@ -0,0 +1,3 @@
+#additional components to be bundled for release
+cygwin-20130110
+
--- a/Admin/components/components.sha1 Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/components/components.sha1 Fri Jan 11 13:24:16 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
--- a/Admin/lib/Tools/makedist Thu Jan 10 21:22:11 2013 +0100
+++ b/Admin/lib/Tools/makedist Fri Jan 11 13:24:16 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/makedist_bundles Fri Jan 11 13:24:16 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 '<?xml version="1.0" encoding="utf-8" ?>'
+ echo '<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">'
+ echo '<html xmlns="http://www.w3.org/1999/xhtml">'
+ echo '<head>'
+ echo '<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>'
+ echo "<title>${NAME}</title>"
+ echo '</head>'
+ echo '<body>'
+ echo '<pre>'
+ perl -w -p -e "s/&/&/g; s/</</g; s/>/>/g; s/'/'/g; s/\"/"/g;" "$FILE"
+ echo '</pre>'
+ echo '</body>'
+ } > "${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
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/makedist_cygwin Fri Jan 11 13:24:16 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 >/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"
--- a/Isabelle Thu Jan 10 21:22:11 2013 +0100
+++ b/Isabelle Fri Jan 11 13:24:16 2013 +0100
@@ -4,5 +4,5 @@
#
# Default Isabelle application wrapper.
-exec "$(dirname "$0")"/bin/isabelle jedit "$@"
+exec "$(dirname "$0")"/bin/isabelle jedit -s "$@"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Jan 11 13:24:16 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 (\<lambda>y. if (x = y) then P x else Q y) s = setsum Q s"
and "setsum (\<lambda>y. if (y = x) then P y else Q y) s = setsum Q s"
and "setsum (\<lambda>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) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> 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 \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
@@ -1163,90 +1165,109 @@
shows "\<exists>x \<ge> a. x <= b \<and> f x \<notin> e1 \<and> f x \<notin> e2" (is "\<exists> x. ?P x")
proof -
let ?S = "{c. \<forall>x \<ge> a. x <= c \<longrightarrow> f x \<in> e1}"
- have Se: " \<exists>x. x \<in> ?S" apply (rule exI[where x=a]) by (auto simp add: fa)
+ have Se: " \<exists>x. x \<in> ?S"
+ apply (rule exI[where x=a])
+ apply (auto simp add: fa)
+ done
have Sub: "\<exists>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 \<le> l" "l \<le> 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: "\<forall>z \<ge> a. z < l \<longrightarrow> f z \<in> 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: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
- have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
- have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
- then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
- {assume le2: "f l \<in> e2"
- from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
- hence lap: "l - a > 0" using alb by arith
- from e2[rule_format, OF le2] obtain e where
- e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
- from dst[OF alb e(1)] obtain d where
- d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
- let ?d' = "min (d/2) ((l - a)/2)"
- have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
- by (simp add: min_max.less_infI2)
- then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
- then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
- from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
- from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
- moreover
- have "f (l - d') \<in> 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: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
+ have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
+ have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
+ then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
+ { assume le2: "f l \<in> e2"
+ from le2 fa fb e12 alb have la: "l \<noteq> 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" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
+ from dst[OF alb e(1)] obtain d where
+ d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
+ let ?d' = "min (d/2) ((l - a)/2)"
+ have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
+ by (simp add: min_max.less_infI2)
+ then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
+ then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
+ from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
+ from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
moreover
- {assume le1: "f l \<in> e1"
+ have "f (l - d') \<in> 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 \<in> e1"
from le1 fa fb e12 alb have lb: "l \<noteq> b" by metis
- hence blp: "b - l > 0" using alb by arith
- from e1[rule_format, OF le1] obtain e where
- e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
- from dst[OF alb e(1)] obtain d where
- d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
- have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
- then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
- then obtain d' where d': "d' > 0" "d' < d" by metis
- from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
- hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
- with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> 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" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
+ from dst[OF alb e(1)] obtain d where
+ d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
+ have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
+ then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
+ then obtain d' where d': "d' > 0" "d' < d" by metis
+ from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
+ then have "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
+ with ale1 have "\<forall>y. a \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> 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 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
+proof -
+ { fix e1 e2
+ assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
assume "e1 \<inter> s \<noteq> {}" "e2 \<inter> s \<noteq> {}"
then obtain x1 x2 where x1:"x1\<in>e1" "x1\<in>s" and x2:"x2\<in>e2" "x2\<in>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 \<le> x" "x \<le> 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 "\<bar>y - x\<bar> < 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 "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> 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 "\<exists>d>0. \<forall>y. \<bar>y - x\<bar> < d \<longrightarrow> 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 "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1 \<and> (1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2"
- apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
- using * apply(simp add: dist_norm)
+ apply (rule connected_real_lemma)
+ apply (simp add: `x1\<in>e1` `x2\<in>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\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e2" by auto
- hence False using as(4)
+ using as(3) apply auto
+ done
+ then obtain x where "x\<ge>0" "x\<le>1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> e1" "(1 - x) *\<^sub>R x1 + x *\<^sub>R x2 \<notin> 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 \<le> 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) \<le> (1-u) * f x + u * f y" using `x\<in>s` `y\<in>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 \<in> ball x e" unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0<u`] unfolding dist_norm[symmetric]
+ 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 \<in> ball x e"
+ unfolding mem_ball dist_norm unfolding * and norm_scaleR and abs_of_pos[OF `0<u`]
+ unfolding dist_norm[symmetric]
using u unfolding pos_less_divide_eq[OF xy] by auto
- hence "f x \<le> 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 \<le> 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 \<le> u" "0 \<le> v" "u + v = 1"
- have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> 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 \<le> u" "0 \<le> v" "u + v = 1"
+ have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> 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 \<le> e" "dist x z \<le> e"
- fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
- have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> 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) \<le> 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 \<le> e" "dist x z \<le> e"
+ fix u v :: real
+ assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+ have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> 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) \<le> 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 \<longleftrightarrow> 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:"\<forall>x\<in>s. norm x \<le> 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: "\<forall>x\<in>s. norm x \<le> 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 \<Longrightarrow> 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 \<in> 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 \<in> f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s]
+ show "convex {x. x \<in> 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 \<in> convex hull s"
shows "(f x) \<in> 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 \<noteq> {}"
- shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
- b \<in> (convex hull s) \<and> (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 \<or> x \<in> s"
- thus "x\<in>?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. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and> b \<in> (convex hull s) \<and> (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 \<or> x \<in> s"
+ then show "x \<in> ?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\<in>?hull"
- then obtain u v b where obt:"u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b" by auto
- have "a\<in>convex hull insert a s" "b\<in>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\<in> 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 \<in> ?hull"
+ then obtain u v b where obt: "u\<ge>0" "v\<ge>0" "u + v = 1" "b \<in> convex hull s" "x = u *\<^sub>R a + v *\<^sub>R b"
+ by auto
+ have "a \<in> convex hull insert a s" "b\<in>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 \<in> 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) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
- from as(4) obtain u1 v1 b1 where obt1:"u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
- from as(5) obtain u2 v2 b2 where obt2:"u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
- have *:"\<And>(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 "\<exists>b \<in> 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 *:"\<And>(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) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
+ from as(4) obtain u1 v1 b1
+ where obt1: "u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
+ from as(5) obtain u2 v2 b2
+ where obt2: "u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
+ have *: "\<And>(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 **: "\<exists>b \<in> 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 *: "\<And>(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\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>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 "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)" using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
- also have "\<dots> = u * v1 + v * v2" by simp finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
- case False have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> 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 "\<dots> = u * (v1 + u1 - u1) + v * (v2 + u2 - u2)"
+ using as(3) obt1(3) obt2(3) by (auto simp add: field_simps)
+ also have "\<dots> = u * v1 + v * v2"
+ by simp
+ finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
+ have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> 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 \<le> 1" unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
- have u2:"u2 \<le> 1" unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
- have "u1 * u + u2 * v \<le> (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 "\<dots> \<le> 1" unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
- finally
- show "u *\<^sub>R x + v *\<^sub>R y \<in> ?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 \<le> 1"
+ unfolding obt1(3)[symmetric] and not_le using obt1(2) by auto
+ have u2: "u2 \<le> 1"
+ unfolding obt2(3)[symmetric] and not_le using obt2(2) by auto
+ have "u1 * u + u2 * v \<le> (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 "\<dots> \<le> 1"
+ unfolding distrib_left[symmetric] and as(3) using u1 u2 by auto
+ finally show "u *\<^sub>R x + v *\<^sub>R y \<in> ?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. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
- (setsum u {1..k} = 1) \<and>
- (setsum (\<lambda>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\<in>s"
- thus "x \<in> ?hull" unfolding mem_Collect_eq apply(rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI) by auto
+ shows "convex hull s =
+ {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
+ (setsum u {1..k} = 1) \<and>
+ (setsum (\<lambda>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\<in>s"
+ then show "x \<in> ?hull"
+ unfolding mem_Collect_eq
+ apply (rule_tac x=1 in exI, rule_tac x="\<lambda>x. 1" in exI)
+ apply auto
+ done
next
- fix t assume as:"s \<subseteq> t" "convex t"
- show "?hull \<subseteq> t" apply(rule) unfolding mem_Collect_eq apply(erule exE | erule conjE)+ proof-
- fix x k u y assume assm:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
- show "x\<in>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 \<subseteq> t" "convex t"
+ show "?hull \<subseteq> t"
+ apply rule
+ unfolding mem_Collect_eq
+ apply (erule exE | erule conjE)+
+ proof -
+ fix x k u y
+ assume assm:
+ "\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> s"
+ "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
+ show "x\<in>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\<le>u" "0\<le>v" "u+v=(1::real)" and xy:"x\<in>?hull" "y\<in>?hull"
- from xy obtain k1 u1 x1 where x:"\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto
- from xy obtain k2 u2 x2 where y:"\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto
- have *:"\<And>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\<le>u" "0\<le>v" "u + v = (1::real)" and xy: "x\<in>?hull" "y\<in>?hull"
+ from xy obtain k1 u1 x1 where
+ x: "\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x"
+ by auto
+ from xy obtain k2 u2 x2 where
+ y: "\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y"
+ by auto
+ have *: "\<And>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} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>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 (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto
- show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull" apply(rule)
- apply(rule_tac x="k1 + k2" in exI, rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
- apply(rule_tac x="\<lambda>i. if i \<in> {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 \<in> {1..k1+k2}"
- show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and> (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
- proof(cases "i\<in>{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 \<equiv> "i - k1"
- case False with i have "j \<in> {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 (\<lambda>i. i + k1) {1..k2}"
+ unfolding inj_on_def by auto
+ show "u *\<^sub>R x + v *\<^sub>R y \<in> ?hull"
+ apply rule
+ apply (rule_tac x="k1 + k2" in exI)
+ apply (rule_tac x="\<lambda>i. if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)" in exI)
+ apply (rule_tac x="\<lambda>i. if i \<in> {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 \<in> {1..k1+k2}"
+ show "0 \<le> (if i \<in> {1..k1} then u * u1 i else v * u2 (i - k1)) \<and>
+ (if i \<in> {1..k1} then x1 i else x2 (i - k1)) \<in> s"
+ proof (cases "i\<in>{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 \<equiv> "i - k1"
+ from i False have "j \<in> {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. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
- setsum u s = 1 \<and> setsum (\<lambda>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\<in>s" thus " \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
- apply(rule_tac x="\<lambda>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 \<and> setsum (\<lambda>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 \<in> s"
+ then show "\<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>x\<in>s. u x *\<^sub>R x) = x"
+ apply (rule_tac x="\<lambda>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 \<le> u" "0 \<le> v" "u + v = 1"
- fix ux assume ux:"\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
- fix uy assume uy:"\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"
- { fix x assume "x\<in>s"
- hence "0 \<le> 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 "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
+ fix u v :: real
+ assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
+ fix ux assume ux: "\<forall>x\<in>s. 0 \<le> ux x" "setsum ux s = (1::real)"
+ fix uy assume uy: "\<forall>x\<in>s. 0 \<le> uy x" "setsum uy s = (1::real)"
+ { fix x
+ assume "x\<in>s"
+ then have "0 \<le> 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 "(\<Sum>x\<in>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 "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>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 "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and> (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
- apply(rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI) by auto
+ moreover
+ have "(\<Sum>x\<in>s. (u * ux x + v * uy x) *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>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 "\<exists>uc. (\<forall>x\<in>s. 0 \<le> uc x) \<and> setsum uc s = 1 \<and>
+ (\<Sum>x\<in>s. uc x *\<^sub>R x) = u *\<^sub>R (\<Sum>x\<in>s. ux x *\<^sub>R x) + v *\<^sub>R (\<Sum>x\<in>s. uy x *\<^sub>R x)"
+ apply (rule_tac x="\<lambda>x. u * ux x + v * uy x" in exI)
+ apply auto
+ done
next
- fix t assume t:"s \<subseteq> t" "convex t"
- fix u assume u:"\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"
- thus "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> t" using t(2)[unfolded convex_explicit, THEN spec[where x=s], THEN spec[where x=u]]
+ fix t
+ assume t: "s \<subseteq> t" "convex t"
+ fix u
+ assume u: "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = (1::real)"
+ then show "(\<Sum>x\<in>s. u x *\<^sub>R x) \<in> 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 "(\<Sum>x\<in>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. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
- (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
-proof-
+ (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
+proof -
{ fix x assume "x\<in>?lhs"
- then obtain k u y where obt:"\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> p" "setsum u {1..k} = 1" "(\<Sum>i = 1..k. u i *\<^sub>R y i) = x"
+ then obtain k u y where
+ obt: "\<forall>i\<in>{1::nat..k}. 0 \<le> u i \<and> y i \<in> p" "setsum u {1..k} = 1" "(\<Sum>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':"\<And>v. finite {i \<in> {1..k}. y i = v}" by auto
- { fix j assume "j\<in>{1..k}"
- hence "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> 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': "\<And>v. finite {i \<in> {1..k}. y i = v}" by auto
+ { fix j
+ assume "j\<in>{1..k}"
+ then have "y j \<in> p" "0 \<le> setsum u {i. Suc 0 \<le> i \<and> i \<le> k \<and> 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 "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v}) = 1"
unfolding setsum_image_gen[OF fin, symmetric] using obt(2) by auto
moreover have "(\<Sum>v\<in>y ` {1..k}. setsum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x"
using setsum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
unfolding scaleR_left.setsum using obt(3) by auto
- ultimately have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
- apply(rule_tac x="y ` {1..k}" in exI)
- apply(rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI) by auto
- hence "x\<in>?rhs" by auto }
+ ultimately
+ have "\<exists>s u. finite s \<and> s \<subseteq> p \<and> (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
+ apply (rule_tac x="y ` {1..k}" in exI)
+ apply (rule_tac x="\<lambda>v. setsum u {i\<in>{1..k}. y i = v}" in exI)
+ apply auto
+ done
+ then have "x\<in>?rhs" by auto
+ }
moreover
{ fix y assume "y\<in>?rhs"
- then obtain s u where obt:"finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>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\<in>{1..card s}"
- hence "f i \<in> s" apply(subst f(2)[symmetric]) by auto
- hence "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto }
+ then obtain s u where
+ obt: "finite s" "s \<subseteq> p" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = 1" "(\<Sum>v\<in>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\<in>{1..card s}"
+ then have "f i \<in> s"
+ apply (subst f(2)[symmetric])
+ apply auto
+ done
+ then have "0 \<le> u (f i)" "f i \<in> p" using obt(2,3) by auto
+ }
moreover have *:"finite {1..card s}" by auto
- { fix y assume "y\<in>s"
- then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto
- hence "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> 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 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
- hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
- "(\<Sum>x\<in>{x \<in> {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 "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
+ { fix y
+ assume "y\<in>s"
+ then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"]
+ by auto
+ then have "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> 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 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
+ then have "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
+ "(\<Sum>x\<in>{x \<in> {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 "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
unfolding f using setsum_cong2[of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
- using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u] unfolding obt(4,5) by auto
-
- ultimately have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and> (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
- apply(rule_tac x="card s" in exI) apply(rule_tac x="u \<circ> f" in exI) apply(rule_tac x=f in exI) by fastforce
- hence "y \<in> ?lhs" unfolding convex_hull_indexed by auto }
+ using setsum_cong2 [of s "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x))" u]
+ unfolding obt(4,5) by auto
+ ultimately
+ have "\<exists>k u x. (\<forall>i\<in>{1..k}. 0 \<le> u i \<and> x i \<in> p) \<and> setsum u {1..k} = 1 \<and>
+ (\<Sum>i::nat = 1..k. u i *\<^sub>R x i) = y"
+ apply (rule_tac x="card s" in exI)
+ apply (rule_tac x="u \<circ> f" in exI)
+ apply (rule_tac x=f in exI)
+ apply fastforce
+ done
+ then have "y \<in> ?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 "(\<exists>u. (\<forall>x\<in>insert a s. 0 \<le> u x) \<and> setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y)
\<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs")
-proof(rule, case_tac[!] "a\<in>s")
- assume "a\<in>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\<in>s")
+ assume "a\<in>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:"\<forall>x\<in>insert a s. 0 \<le> u x" "setsum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y" by auto
- assume "a\<notin>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\<notin>s` by auto
+ assume ?lhs
+ then obtain u where u: "\<forall>x\<in>insert a s. 0 \<le> u x" "setsum u (insert a s) = w" "(\<Sum>x\<in>insert a s. u x *\<^sub>R x) = y"
+ by auto
+ assume "a \<notin> 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\<notin>s`
+ apply auto
+ done
next
- assume "a\<in>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\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
- show ?lhs apply(rule_tac x="\<lambda>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\<in>s` by auto
+ assume "a \<in> 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\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
+ by auto
+ show ?lhs
+ apply (rule_tac x = "\<lambda>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\<in>s`
+ apply auto
+ done
next
- assume ?rhs then obtain v u where uv:"v\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a" by auto
- moreover assume "a\<notin>s" moreover have "(\<Sum>x\<in>s. if a = x then v else u x) = setsum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"
- apply(rule_tac setsum_cong2) defer apply(rule_tac setsum_cong2) using `a\<notin>s` by auto
- ultimately show ?lhs apply(rule_tac x="\<lambda>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\<ge>0" "\<forall>x\<in>s. 0 \<le> u x" "setsum u s = w - v" "(\<Sum>x\<in>s. u x *\<^sub>R x) = y - v *\<^sub>R a"
+ by auto
+ moreover
+ assume "a \<notin> s"
+ moreover
+ have "(\<Sum>x\<in>s. if a = x then v else u x) = setsum u s" "(\<Sum>x\<in>s. (if a = x then v else u x) *\<^sub>R x) = (\<Sum>x\<in>s. u x *\<^sub>R x)"
+ apply (rule_tac setsum_cong2)
+ defer
+ apply (rule_tac setsum_cong2)
+ using `a \<notin> s`
+ apply auto
+ done
+ ultimately show ?lhs
+ apply (rule_tac x="\<lambda>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 *}
--- a/src/HOL/Num.thy Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Num.thy Fri Jan 11 13:24:16 2013 +0100
@@ -245,6 +245,12 @@
numeral_Bit0: "numeral (Bit0 n) = numeral n + numeral n" |
numeral_Bit1: "numeral (Bit1 n) = numeral n + numeral n + 1"
+lemma numeral_code [code]:
+ "numeral One = 1"
+ "numeral (Bit0 n) = (let m = numeral n in m + m)"
+ "numeral (Bit1 n) = (let m = numeral n in m + m + 1)"
+ by (simp_all add: Let_def)
+
lemma one_plus_numeral_commute: "1 + numeral x = numeral x + 1"
apply (induct x)
apply simp
@@ -1103,3 +1109,4 @@
Num Arith
end
+
--- a/src/HOL/TPTP/MaSh_Export.thy Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Fri Jan 11 13:24:16 2013 +0100
@@ -29,6 +29,7 @@
val thys = [@{theory List}]
val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
val prover = hd provers
+val max_suggestions = 1024
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/"
*}
@@ -71,8 +72,16 @@
ML {*
if do_it then
- generate_mepo_suggestions @{context} params thys 1024
- (prefix ^ "mash_mepo_suggestions")
+ generate_mepo_suggestions @{context} params thys max_suggestions
+ (prefix ^ "mepo_suggestions")
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ generate_mesh_suggestions max_suggestions (prefix ^ "mash_suggestions")
+ (prefix ^ "mepo_suggestions") (prefix ^ "mesh_suggestions")
else
()
*}
--- a/src/HOL/TPTP/mash_eval.ML Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jan 11 13:24:16 2013 +0100
@@ -42,8 +42,7 @@
default_params ctxt []
val prover = hd provers
val slack_max_facts = generous_max_facts (the max_facts)
- val sugg_path = sugg_file_name |> Path.explode
- val lines = sugg_path |> File.read_lines
+ val lines = Path.explode sugg_file_name |> File.read_lines
val css = clasimpset_rule_table_of ctxt
val facts = all_facts ctxt true false Symtab.empty [] [] css
val name_tabs = build_name_tables nickname_of_thm facts
@@ -88,8 +87,11 @@
val (mash_facts, mash_unks) =
find_mash_suggestions slack_max_facts suggs facts [] []
|>> weight_mash_facts
- val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
- val mesh_facts = mesh_facts slack_max_facts mess
+ val mess =
+ [(mepo_weight, (mepo_facts, [])),
+ (mash_weight, (mash_facts, mash_unks))]
+ val mesh_facts =
+ mesh_facts (Thm.eq_thm o pairself snd) slack_max_facts mess
val isar_facts =
find_suggested_facts (map (rpair 1.0) isar_deps) facts
(* adapted from "mirabelle_sledgehammer.ML" *)
--- a/src/HOL/TPTP/mash_export.ML Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML Fri Jan 11 13:24:16 2013 +0100
@@ -24,6 +24,7 @@
Proof.context -> params -> int * int option -> theory list -> string -> unit
val generate_mepo_suggestions :
Proof.context -> params -> theory list -> int -> string -> unit
+ val generate_mesh_suggestions : int -> string -> string -> string -> unit
end;
structure MaSh_Export : MASH_EXPORT =
@@ -164,16 +165,17 @@
generate_isar_or_prover_commands ctxt prover (SOME params)
fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...}) thys
- max_facts file_name =
+ max_suggs file_name =
let
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val path = file_name |> Path.explode
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
val name_tabs = build_name_tables nickname_of_thm facts
- fun do_fact ((_, th), old_facts) =
+ fun do_fact (j, ((_, th), old_facts)) =
let
val name = nickname_of_thm th
+ val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val isar_deps = isar_dependencies_of name_tabs th
@@ -185,13 +187,38 @@
val suggs =
old_facts
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
- max_facts NONE hyp_ts concl_t
+ max_suggs NONE hyp_ts concl_t
|> map (nickname_of_thm o snd)
in escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" end
end
fun accum x (yss as ys :: _) = (x :: ys) :: yss
val old_factss = tl (fold accum new_facts [old_facts])
- val lines = Par_List.map do_fact (new_facts ~~ rev old_factss)
+ val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ rev old_factss))
in File.write_list path lines end
+fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name
+ mesh_file_name =
+ let
+ val mesh_path = Path.explode mesh_file_name
+ val _ = File.write mesh_path ""
+ fun do_fact (mash_line, mepo_line) =
+ let
+ val (mash_name, mash_suggs) =
+ extract_suggestions mash_line
+ ||> (map fst #> weight_mash_facts)
+ val (mepo_name, mepo_suggs) =
+ extract_suggestions mepo_line
+ ||> (map fst #> weight_mash_facts)
+ val _ =
+ if mash_name = mepo_name then () else error "Input files out of sync."
+ val mess =
+ [(mepo_weight, (mepo_suggs, [])),
+ (mash_weight, (mash_suggs, []))]
+ val mesh_suggs = mesh_facts (op =) max_suggs mess
+ val mesh_line = mash_name ^ ": " ^ space_implode " " mesh_suggs ^ "\n"
+ in File.append mesh_path mesh_line end
+ val mash_lines = Path.explode mash_file_name |> File.read_lines
+ val mepo_lines = Path.explode mepo_file_name |> File.read_lines
+ in List.app do_fact (mash_lines ~~ mepo_lines) end
+
end;
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Jan 11 13:24:16 2013 +0100
@@ -449,9 +449,11 @@
end
end;
-fun size_matters_for _ Ts = not (forall
- (fn Type (tyco, []) => is_some (try (unprefix "Enum.finite") tyco) | _ => false) Ts)
- (*FIXME eliminate dynamic name reference*)
+val size_types = [@{type_name Enum.finite_1}, @{type_name Enum.finite_2},
+ @{type_name Enum.finite_3}, @{type_name Enum.finite_4}, @{type_name Enum.finite_5}];
+
+fun size_matters_for _ Ts =
+ not (forall (fn Type (tyco, []) => member (op =) size_types tyco | _ => false) Ts);
val test_goals =
Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr));
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jan 11 13:24:16 2013 +0100
@@ -344,12 +344,12 @@
let
fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
fun add_plain canon alias =
- Symtab.update (Thm.get_name_hint canon,
+ Symtab.update (Thm.get_name_hint alias,
name_of (if_thm_before canon alias))
fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
fun add_inclass (name, target) =
fold (fn s => Symtab.update (s, target)) (un_class_ify name)
- val prop_tab = fold_rev cons_thm facts Termtab.empty
+ val prop_tab = fold cons_thm facts Termtab.empty
val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
in (plain_name_tab, inclass_name_tab) end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 10 21:22:11 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 11 13:24:16 2013 +0100
@@ -49,8 +49,8 @@
val find_suggested_facts :
(string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
val mesh_facts :
- int -> (real * ((('a * thm) * real) list * ('a * thm) list)) list
- -> ('a * thm) list
+ ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
+ -> 'a list
val theory_ord : theory * theory -> order
val thm_ord : thm * thm -> order
val goal_of_thm : theory -> thm -> thm
@@ -81,6 +81,8 @@
val is_mash_enabled : unit -> bool
val mash_can_suggest_facts : Proof.context -> bool
val generous_max_facts : int -> int
+ val mepo_weight : real
+ val mash_weight : real
val relevant_facts :
Proof.context -> params -> string -> int -> fact_override -> term list
-> term -> fact list -> fact list
@@ -444,13 +446,13 @@
map (apsnd (curry Real.* (1.0 / avg))) xs
end
-fun mesh_facts max_facts [(_, (sels, unks))] =
+fun mesh_facts _ max_facts [(_, (sels, unks))] =
map fst (take max_facts sels) @ take (max_facts - length sels) unks
- | mesh_facts max_facts mess =
+ | mesh_facts eq max_facts mess =
let
val mess =
mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
- val fact_eq = Thm.eq_thm o pairself snd
+ val fact_eq = eq
fun score_in fact (global_weight, ((sel_len, sels), unks)) =
let
fun score_at j =
@@ -769,7 +771,7 @@
val unknown =
raw_unknown
|> fold (subtract (Thm.eq_thm_prop o pairself snd)) [chained, proximity]
- in (mesh_facts max_facts mess, unknown) end
+ in (mesh_facts (Thm.eq_thm o pairself snd) max_facts mess, unknown) end
fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
concl_t facts =
@@ -1054,6 +1056,9 @@
later for various reasons. *)
fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts div 2)
+val mepo_weight = 0.5
+val mash_weight = 0.5
+
(* The threshold should be large enough so that MaSh doesn't kick in for Auto
Sledgehammer and Try. *)
val min_secs_for_learning = 15
@@ -1106,10 +1111,12 @@
hyp_ts concl_t facts
|>> weight_mash_facts
val mess =
- [] |> (if fact_filter <> mashN then cons (0.5, (mepo (), [])) else I)
- |> (if fact_filter <> mepoN then cons (0.5, (mash ())) else I)
+ [] |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), []))
+ else I)
+ |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
+ else I)
in
- mesh_facts max_facts mess
+ mesh_facts (Thm.eq_thm o pairself snd) max_facts mess
|> not (null add_ths) ? prepend_facts add_ths
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/socket_io.ML Fri Jan 11 13:24:16 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;
+
--- a/src/Pure/ML-Systems/proper_int.ML Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML Fri Jan 11 13:24:16 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;
--- a/src/Pure/ROOT Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/ROOT Fri Jan 11 13:24:16 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"
--- a/src/Pure/ROOT.ML Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/ROOT.ML Fri Jan 11 13:24:16 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 ();
--- a/src/Pure/System/options.scala Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/System/options.scala Fri Jan 11 13:24:16 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)
--- a/src/Pure/System/system_channel.ML Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/System/system_channel.ML Fri Jan 11 13:24:16 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;
-
--- a/src/Pure/Tools/main.scala Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Pure/Tools/main.scala Fri Jan 11 13:24:16 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) }
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Jan 11 13:24:16 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" <<EOF
+ if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
+ cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
EOF
cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
@@ -323,12 +322,8 @@
</VIEW>
</PERSPECTIVE>
EOF
-fi
-
+ fi
-# main
-
-if [ "$BUILD_ONLY" = false ]; then
if [ "$NO_BUILD" = false ]; then
"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}"
RC="$?"
--- a/src/Tools/jEdit/src/jEdit.props Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Fri Jan 11 13:24:16 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
--- a/src/Tools/jEdit/src/plugin.scala Thu Jan 10 21:22:11 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Jan 11 13:24:16 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()))
}