--- a/Admin/lib/Tools/build_doc Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: build Isabelle documentation
-
-isabelle_admin_build jars || exit $?
-
-
-case "$ISABELLE_JAVA_PLATFORM" in
- x86-*)
- ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
- ;;
- x86_64-*)
- ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
- ;;
-esac
-
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-isabelle java "${JAVA_ARGS[@]}" isabelle.Build_Doc "$@"
--- a/NEWS Sun Apr 03 10:25:17 2016 +0200
+++ b/NEWS Sun Apr 03 23:57:32 2016 +0200
@@ -259,6 +259,12 @@
*** System ***
+* Many Isabelle tools that require a Java runtime system refer to the
+settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,
+depending on the underlying platform. The settings for "isabelle build"
+ISABELLE_BUILD_JAVA_OPTIONS32 / ISABELLE_BUILD_JAVA_OPTIONS64 have been
+discontinued. Potential INCOMPATIBILITY.
+
* The Isabelle system environment always ensures that the main
executables are found within the shell search $PATH: "isabelle" and
"isabelle_scala_script".
--- a/bin/isabelle Sun Apr 03 10:25:17 2016 +0200
+++ b/bin/isabelle Sun Apr 03 23:57:32 2016 +0200
@@ -18,46 +18,40 @@
source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-## diagnostics
+## external tool (shell script)
+
+if [ "$#" -ge 1 -a "$1" != "-?" ]
+then
+ TOOL_NAME="$1"
-function usage()
-{
- echo
- echo "Usage: $PRG NAME [ARGS ...]"
- echo
- echo " Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help."
- echo
- echo "Available tools:"
- perl -w "$ISABELLE_HOME/lib/scripts/tools.pl"
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
+ splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
+ for DIR in "${TOOLS[@]}"
+ do
+ TOOL="$DIR/$TOOL_NAME"
+ case "$TOOL" in
+ *~ | *.orig) ;;
+ *)
+ if [ -f "$TOOL" -a -x "$TOOL" ]; then
+ shift
+ exec "$TOOL" "$@"
+ fi
+ ;;
+ esac
+ done
+fi
-## args
-
-[ "$#" -lt 1 -o "$1" = "-?" ] && usage
+## internal tool or usage (Scala)
-TOOLNAME="$1"
-shift
-
-
-## main
+isabelle_admin_build jars || exit $?
-splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
+case "$ISABELLE_JAVA_PLATFORM" in
+ x86-*)
+ eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS32)"
+ ;;
+ x86_64-*)
+ eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS64)"
+ ;;
+esac
-for DIR in "${TOOLS[@]}"
-do
- TOOL="$DIR/$TOOLNAME"
- case "$TOOL" in
- *~ | *.orig) ;;
- *) [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" ;;
- esac
-done
-
-fail "Unknown Isabelle tool: $TOOLNAME"
+exec isabelle java "${JAVA_ARGS[@]}" isabelle.Isabelle_Tool "$@"
--- a/etc/settings Sun Apr 03 10:25:17 2016 +0200
+++ b/etc/settings Sun Apr 03 23:57:32 2016 +0200
@@ -16,6 +16,9 @@
ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0"
+ISABELLE_TOOL_JAVA_OPTIONS32="-Djava.awt.headless=true -Xms128m -Xmx1024m -Xss1m"
+ISABELLE_TOOL_JAVA_OPTIONS64="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"
+
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
#paranoia settings -- avoid intrusion of alien options
@@ -39,9 +42,6 @@
ISABELLE_BUILD_OPTIONS=""
-ISABELLE_BUILD_JAVA_OPTIONS32="-Djava.awt.headless=true -Xms128m -Xmx1024m -Xss1m"
-ISABELLE_BUILD_JAVA_OPTIONS64="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"
-
###
### Document preparation (cf. isabelle latex/document)
--- a/lib/Tools/build Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: build and manage Isabelle sessions
-
-isabelle_admin_build jars || exit $?
-
-case "$ISABELLE_JAVA_PLATFORM" in
- x86-*)
- ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
- ;;
- x86_64-*)
- ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
- ;;
-esac
-
-eval "declare -a JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-exec isabelle java "${JAVA_ARGS[@]}" isabelle.Build "$@"
--- a/lib/Tools/check_sources Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: some sanity checks for Isabelle sources
-
-isabelle_admin_build jars || exit $?
-
-isabelle java isabelle.Check_Sources "$@"
--- a/lib/Tools/console Sun Apr 03 10:25:17 2016 +0200
+++ b/lib/Tools/console Sun Apr 03 23:57:32 2016 +0200
@@ -8,14 +8,14 @@
case "$ISABELLE_JAVA_PLATFORM" in
x86-*)
- ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
+ ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS32"
;;
x86_64-*)
- ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
+ ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS64"
;;
esac
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
--- a/lib/Tools/doc Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# DESCRIPTION: view Isabelle documentation
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Doc "$@"
--- a/lib/Tools/getenv Sun Apr 03 10:25:17 2016 +0200
+++ b/lib/Tools/getenv Sun Apr 03 23:57:32 2016 +0200
@@ -57,6 +57,7 @@
# args
+[ -z "$ALL" -a -z "$DUMP" -a "$#" -eq 0 ] && usage
[ -n "$ALL" -a "$#" -ne 0 ] && usage
--- a/lib/Tools/options Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: print Isabelle system options
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Options "$@"
--- a/lib/Tools/process Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: raw ML process (batch mode)
-
-isabelle_admin_build jars || exit $?
-
-case "$ISABELLE_JAVA_PLATFORM" in
- x86-*)
- ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS32"
- ;;
- x86_64-*)
- ISABELLE_BUILD_JAVA_OPTIONS="$ISABELLE_BUILD_JAVA_OPTIONS64"
- ;;
-esac
-
-declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
-
-mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
-
-exec isabelle java isabelle.ML_Process "$@"
--- a/lib/Tools/update_cartouches Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: update theory syntax to use cartouches
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Cartouches "$@"
--- a/lib/Tools/update_header Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: replace obsolete theory header command
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Header "$@"
--- a/lib/Tools/update_then Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: expand old Isar command conflations 'hence' and 'thus'
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Then "$@"
--- a/lib/Tools/update_theorems Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: update toplevel theorem keywords
-
-isabelle_admin_build jars || exit $?
-
-exec isabelle java isabelle.Update_Theorems "$@"
--- a/lib/scripts/tools.pl Sun Apr 03 10:25:17 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-#
-# Author: Makarius
-#
-# tools.pl - list Isabelle tools with description
-#
-
-use strict;
-use warnings;
-
-my @tools = ();
-
-for my $dir (split(":", $ENV{"ISABELLE_TOOLS"})) {
- if (-d $dir) {
- if (opendir DIR, $dir) {
- for my $name (readdir DIR) {
- my $file = "$dir/$name";
- if (-f $file and -x $file and !($file =~ /~$/ or $file =~ /\.orig$/)) {
- if (open FILE, $file) {
- my $description;
- while (<FILE>) {
- if (!defined($description) and m/DESCRIPTION: *(.*)$/) {
- $description = $1;
- }
- }
- close FILE;
- if (defined($description)) {
- push(@tools, " $name - $description\n");
- }
- }
- }
- }
- closedir DIR;
- }
- }
-}
-
-for (sort @tools) { print };
--- a/src/Doc/System/Environment.thy Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Doc/System/Environment.thy Sun Apr 03 23:57:32 2016 +0200
@@ -267,7 +267,7 @@
@{verbatim [display]
\<open>Usage: isabelle TOOL [ARGS ...]
- Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
+ Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
Available tools:
...\<close>}
--- a/src/Doc/System/Sessions.thy Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Doc/System/Sessions.thy Sun Apr 03 23:57:32 2016 +0200
@@ -270,7 +270,6 @@
Build and manage Isabelle sessions, depending on implicit settings:
ISABELLE_BUILD_OPTIONS="..."
- ISABELLE_BUILD_JAVA_OPTIONS="..."
ML_PLATFORM="..."
ML_HOME="..."
--- a/src/Doc/antiquote_setup.ML Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Doc/antiquote_setup.ML Sun Apr 03 23:57:32 2016 +0200
@@ -157,17 +157,6 @@
(Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
handle ERROR _ => false;
-fun check_tool ctxt (name, pos) =
- let
- fun tool dir =
- let val path = Path.append dir (Path.basic name)
- in if File.exists path then SOME path else NONE end;
- in
- (case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of
- NONE => false
- | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true))
- end;
-
val arg = enclose "{" "}" o clean_string;
fun entity check markup binding index =
@@ -220,7 +209,7 @@
entity_antiqs check_system_option "isasystem" @{binding system_option} #>
entity_antiqs no_check "" @{binding inference} #>
entity_antiqs no_check "isasystem" @{binding executable} #>
- entity_antiqs check_tool "isatool" @{binding tool} #>
+ entity_antiqs no_check "isatool" @{binding tool} #>
entity_antiqs ML_Context.check_antiquotation "" @{binding ML_antiquotation} #>
entity_antiqs (K JEdit.check_action) "isasystem" @{binding action});
--- a/src/HOL/Library/Complete_Partial_Order2.thy Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Sun Apr 03 23:57:32 2016 +0200
@@ -2,7 +2,7 @@
Author: Andreas Lochbihler, ETH Zurich
*)
-section {* Formalisation of chain-complete partial orders, continuity and admissibility *}
+section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
theory Complete_Partial_Order2 imports
Main
@@ -83,10 +83,10 @@
fix x'
assume "x' \<in> (\<lambda>f. f x) ` Y"
then obtain f where "f \<in> Y" "x' = f x" by blast
- note `x' = f x` also
- from `f \<in> Y` `x \<sqsubseteq> y` have "f x \<le> f y" by(blast dest: mono monotoneD)
+ note \<open>x' = f x\<close> also
+ from \<open>f \<in> Y\<close> \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y" by(blast dest: mono monotoneD)
also have "\<dots> \<le> \<Squnion>((\<lambda>f. f y) ` Y)" using chain''
- by(rule ccpo_Sup_upper)(simp add: `f \<in> Y`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Y\<close>)
finally show "x' \<le> \<Squnion>((\<lambda>f. f y) ` Y)" .
qed
qed
@@ -108,9 +108,9 @@
fix x'
assume "x' \<in> f x ` Y"
then obtain y' where "y' \<in> Y" "x' = f x y'" by blast note this(2)
- also from mono1[OF `y' \<in> Y`] le have "\<dots> \<le> f y y'" by(rule monotoneD)
+ also from mono1[OF \<open>y' \<in> Y\<close>] le have "\<dots> \<le> f y y'" by(rule monotoneD)
also have "\<dots> \<le> ?rhs" using chain'[OF y]
- by (auto intro!: ccpo_Sup_upper simp add: `y' \<in> Y`)
+ by (auto intro!: ccpo_Sup_upper simp add: \<open>y' \<in> Y\<close>)
finally show "x' \<le> ?rhs" .
qed(rule x)
@@ -128,17 +128,17 @@
fix x'
assume "x' \<in> (\<lambda>x. \<Squnion>(f x ` Y)) ` Y"
then obtain y' where "y' \<in> Y" "x' = \<Squnion>(f y' ` Y)" by blast note this(2)
- also have "\<dots> \<le> ?rhs" using chain2[OF `y' \<in> Y`]
+ also have "\<dots> \<le> ?rhs" using chain2[OF \<open>y' \<in> Y\<close>]
proof(rule ccpo_Sup_least)
fix x
assume "x \<in> f y' ` Y"
then obtain y where "y \<in> Y" and x: "x = f y' y" by blast
def y'' \<equiv> "if y \<sqsubseteq> y' then y' else y"
- from chain `y \<in> Y` `y' \<in> Y` have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
- hence "f y' y \<le> f y'' y''" using `y \<in> Y` `y' \<in> Y`
+ from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y \<sqsubseteq> y' \<or> y' \<sqsubseteq> y" by(rule chainD)
+ hence "f y' y \<le> f y'' y''" using \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close>
by(auto simp add: y''_def intro: mono2 monotoneD[OF mono1])
- also from `y \<in> Y` `y' \<in> Y` have "y'' \<in> Y" by(simp add: y''_def)
- from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: `y'' \<in> Y`)
+ also from \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "y'' \<in> Y" by(simp add: y''_def)
+ from chain3 have "f y'' y'' \<le> ?rhs" by(rule ccpo_Sup_upper)(simp add: \<open>y'' \<in> Y\<close>)
finally show "x \<le> ?rhs" by(simp add: x)
qed
finally show "x' \<le> ?rhs" .
@@ -149,9 +149,9 @@
fix y
assume "y \<in> (\<lambda>x. f x x) ` Y"
then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
- also from chain2[OF `x \<in> Y`] have "\<dots> \<le> \<Squnion>(f x ` Y)"
- by(rule ccpo_Sup_upper)(simp add: `x \<in> Y`)
- also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: `x \<in> Y`)
+ also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
+ by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
+ also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>)
finally show "y \<le> ?lhs" .
qed
qed
@@ -171,8 +171,8 @@
fix x
assume "x \<in> f ` Y"
then obtain y where "y \<in> Y" and "x = f y" by blast note this(2)
- also have "y \<sqsubseteq> \<Or>Y" using ccpo chain `y \<in> Y` by(rule ccpo.ccpo_Sup_upper)
- hence "f y \<le> f (\<Or>Y)" using `y \<in> Y` by(rule mono)
+ also have "y \<sqsubseteq> \<Or>Y" using ccpo chain \<open>y \<in> Y\<close> by(rule ccpo.ccpo_Sup_upper)
+ hence "f y \<le> f (\<Or>Y)" using \<open>y \<in> Y\<close> by(rule mono)
finally show "x \<le> \<dots>" .
qed
@@ -196,14 +196,14 @@
fix f g
assume "f \<in> Z" "g \<in> Z"
and "fun_ord op \<le> f g"
- from chain1[OF `f \<in> Z`] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
+ from chain1[OF \<open>f \<in> Z\<close>] show "\<Squnion>(f ` Y) \<le> \<Squnion>(g ` Y)"
proof(rule ccpo_Sup_least)
fix x
assume "x \<in> f ` Y"
then obtain y where "y \<in> Y" "x = f y" by blast note this(2)
- also have "\<dots> \<le> g y" using `fun_ord op \<le> f g` by(simp add: fun_ord_def)
- also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF `g \<in> Z`]
- by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
+ also have "\<dots> \<le> g y" using \<open>fun_ord op \<le> f g\<close> by(simp add: fun_ord_def)
+ also have "\<dots> \<le> \<Squnion>(g ` Y)" using chain1[OF \<open>g \<in> Z\<close>]
+ by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
finally show "x \<le> \<Squnion>(g ` Y)" .
qed
qed
@@ -219,9 +219,9 @@
fix x'
assume "x' \<in> (\<lambda>f. f x) ` Z"
then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
- also have "f x \<le> f y" using `f \<in> Z` `x \<sqsubseteq> y` by(rule monotoneD[OF mono])
+ also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono])
also have "f y \<le> ?rhs" using chain3
- by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
finally show "x' \<le> ?rhs" .
qed
qed
@@ -231,14 +231,14 @@
fix x
assume "x \<in> (\<lambda>x. \<Squnion>(x ` Y)) ` Z"
then obtain f where "f \<in> Z" "x = \<Squnion>(f ` Y)" by blast note this(2)
- also have "\<dots> \<le> ?rhs" using chain1[OF `f \<in> Z`]
+ also have "\<dots> \<le> ?rhs" using chain1[OF \<open>f \<in> Z\<close>]
proof(rule ccpo_Sup_least)
fix x'
assume "x' \<in> f ` Y"
then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
- by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
- also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
+ also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
finally show "x' \<le> ?rhs" .
qed
finally show "x \<le> ?rhs" .
@@ -254,10 +254,10 @@
fix x'
assume "x' \<in> (\<lambda>f. f y) ` Z"
then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
- also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF `f \<in> Z`]
- by(rule ccpo_Sup_upper)(simp add: `y \<in> Y`)
+ also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>]
+ by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
also have "\<dots> \<le> ?lhs" using chain2
- by(rule ccpo_Sup_upper)(simp add: `f \<in> Z`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
finally show "x' \<le> ?lhs" .
qed
finally show "x \<le> ?lhs" .
@@ -314,9 +314,9 @@
assume "x' \<in> (\<lambda>f. f x) ` ?iter"
then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
also have "f x \<le> f y"
- by(rule monotoneD[OF iterates_mono[OF `f \<in> ?iter` mono2]])(blast intro: `x \<sqsubseteq> y`)+
+ by(rule monotoneD[OF iterates_mono[OF \<open>f \<in> ?iter\<close> mono2]])(blast intro: \<open>x \<sqsubseteq> y\<close>)+
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
- by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
finally show "x' \<le> \<dots>" .
qed
qed
@@ -333,7 +333,7 @@
shows "monotone orda ordc (\<lambda>x. f x (t x))"
by(blast intro: monotoneI transpD[OF trans] monotoneD[OF t] monotoneD[OF 2] monotoneD[OF 1])
-subsection {* Continuity *}
+subsection \<open>Continuity\<close>
definition cont :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
where
@@ -345,10 +345,10 @@
"mcont luba orda lubb ordb f \<longleftrightarrow>
monotone orda ordb f \<and> cont luba orda lubb ordb f"
-subsubsection {* Theorem collection @{text cont_intro} *}
+subsubsection \<open>Theorem collection \<open>cont_intro\<close>\<close>
named_theorems cont_intro "continuity and admissibility intro rules"
-ML {*
+ML \<open>
(* apply cont_intro rules as intro and try to solve
the remaining of the emerging subgoals with simp *)
fun cont_intro_tac ctxt =
@@ -374,13 +374,13 @@
end
handle THM _ => NONE
| TYPE _ => NONE
-*}
+\<close>
simproc_setup "cont_intro"
( "ccpo.admissible lub ord P"
| "mcont lub ord lub' ord' f"
| "monotone ord ord' f"
- ) = {* K cont_intro_simproc *}
+ ) = \<open>K cont_intro_simproc\<close>
lemmas [cont_intro] =
call_mono
@@ -604,10 +604,10 @@
fix x'
assume "x' \<in> (\<lambda>f. f x) ` ?iter"
then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
- also from _ `x \<sqsubseteq> y` have "f x \<le> f y"
- by(rule mcont_monoD[OF iterates_mcont[OF `f \<in> ?iter` mcont]])
+ also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
+ by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
- by(rule ccpo_Sup_upper)(simp add: `f \<in> ?iter`)
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
finally show "x' \<le> \<dots>" .
qed
next
@@ -783,7 +783,7 @@
end
-subsection {* Admissibility *}
+subsection \<open>Admissibility\<close>
lemma admissible_subst:
assumes adm: "ccpo.admissible luba orda (\<lambda>x. P x)"
@@ -860,10 +860,10 @@
fix x
assume "x \<in> f ` A"
then obtain y where "y \<in> A" "x = f y" by blast note this(2)
- also have "f y \<le> g y" using le `y \<in> A` by simp
+ also have "f y \<le> g y" using le \<open>y \<in> A\<close> by simp
also have "Complete_Partial_Order.chain op \<le> (g ` A)"
using chain by(rule chain_imageI)(rule mcont_monoD[OF g])
- hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: `y \<in> A`)
+ hence "g y \<le> \<Squnion>(g ` A)" by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> A\<close>)
finally show "x \<le> \<dots>" .
qed
also have "\<dots> = g (luba A)" by(simp add: mcont_contD[OF g] chain False)
@@ -992,7 +992,7 @@
end
-subsection {* @{term "op ="} as order *}
+subsection \<open>@{term "op ="} as order\<close>
definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
@@ -1038,7 +1038,7 @@
\<Longrightarrow> mcont the_Sup op = lub ord f"
by(simp add: mcont_def cont_eqI monotone_eqI)
-subsection {* ccpo for products *}
+subsection \<open>ccpo for products\<close>
definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
@@ -1197,7 +1197,7 @@
with cont have "f (prod_lub luba lubb ?Y) = lubc (f ` ?Y)" by(rule contD)
moreover have "f ` ?Y = (\<lambda>y. f (x, y)) ` Y" by auto
ultimately show "f (x, lubb Y) = lubc ((\<lambda>y. f (x, y)) ` Y)" using luba
- by(simp add: prod_lub_def `Y \<noteq> {}` lub_singleton_def)
+ by(simp add: prod_lub_def \<open>Y \<noteq> {}\<close> lub_singleton_def)
qed
lemma cont_prodD2:
@@ -1253,9 +1253,9 @@
have "f (prod_lub luba lubb Y) = f (luba (fst ` Y), lubb (snd ` Y))"
by(simp add: prod_lub_def)
also from cont2 have "f (luba (fst ` Y), lubb (snd ` Y)) = \<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y)"
- by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] `Y \<noteq> {}`)
+ by(rule contD)(simp_all add: chain_rel_prodD1[OF chain] \<open>Y \<noteq> {}\<close>)
also from cont1 have "\<And>x. f (x, lubb (snd ` Y)) = \<Squnion>((\<lambda>y. f (x, y)) ` snd ` Y)"
- by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] `Y \<noteq> {}`)
+ by(rule contD)(simp_all add: chain_rel_prodD2[OF chain] \<open>Y \<noteq> {}\<close>)
hence "\<Squnion>((\<lambda>x. f (x, lubb (snd ` Y))) ` fst ` Y) = \<Squnion>((\<lambda>x. \<dots> x) ` fst ` Y)" by simp
also have "\<dots> = \<Squnion>((\<lambda>x. f (fst x, snd x)) ` Y)"
unfolding image_image split_def using chain
@@ -1330,7 +1330,7 @@
shows "monotone orda ordb (\<lambda>f. case_prod (pair f) x)"
by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
-subsection {* Complete lattices as ccpo *}
+subsection \<open>Complete lattices as ccpo\<close>
context complete_lattice begin
@@ -1374,8 +1374,8 @@
fix y
assume "y \<in> op \<squnion> x ` Y"
then obtain z where "y = x \<squnion> z" and "z \<in> Y" by blast
- from `z \<in> Y` have "z \<le> \<Squnion>Y" by(rule Sup_upper)
- with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding `y = x \<squnion> z` by(rule sup_mono) simp
+ from \<open>z \<in> Y\<close> have "z \<le> \<Squnion>Y" by(rule Sup_upper)
+ with _ show "y \<le> x \<squnion> \<Squnion>Y" unfolding \<open>y = x \<squnion> z\<close> by(rule sup_mono) simp
next
fix y
assume upper: "\<And>z. z \<in> op \<squnion> x ` Y \<Longrightarrow> z \<le> y"
@@ -1385,8 +1385,8 @@
assume "z \<in> insert x Y"
from assms obtain z' where "z' \<in> Y" by blast
let ?z = "if z \<in> Y then x \<squnion> z else x \<squnion> z'"
- have "z \<le> x \<squnion> ?z" using `z' \<in> Y` `z \<in> insert x Y` by auto
- also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: `z' \<in> Y`)
+ have "z \<le> x \<squnion> ?z" using \<open>z' \<in> Y\<close> \<open>z \<in> insert x Y\<close> by auto
+ also have "\<dots> \<le> y" by(rule upper)(auto split: if_split_asm intro: \<open>z' \<in> Y\<close>)
finally show "z \<le> y" .
qed
qed
@@ -1426,14 +1426,14 @@
interpretation lfp: partial_function_definitions "op \<le> :: _ :: complete_lattice \<Rightarrow> _" Sup
by(rule complete_lattice_partial_function_definitions)
-declaration {* Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
- @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE *}
+declaration \<open>Partial_Function.init "lfp" @{term lfp.fixp_fun} @{term lfp.mono_body}
+ @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>
interpretation gfp: partial_function_definitions "op \<ge> :: _ :: complete_lattice \<Rightarrow> _" Inf
by(rule complete_lattice_partial_function_definitions_dual)
-declaration {* Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
- @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE *}
+declaration \<open>Partial_Function.init "gfp" @{term gfp.fixp_fun} @{term gfp.mono_body}
+ @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>
lemma insert_mono [partial_function_mono]:
"monotone (fun_ord op \<subseteq>) op \<subseteq> A \<Longrightarrow> monotone (fun_ord op \<subseteq>) op \<subseteq> (\<lambda>y. insert x (A y))"
@@ -1505,23 +1505,23 @@
fix u
assume "u \<in> (\<lambda>x. g x z) ` Y"
then obtain y' where "u = g y' z" "y' \<in> Y" by auto
- from chain `y \<in> Y` `y' \<in> Y` have "ord y y' \<or> ord y' y" by(rule chainD)
+ from chain \<open>y \<in> Y\<close> \<open>y' \<in> Y\<close> have "ord y y' \<or> ord y' y" by(rule chainD)
thus "u \<le> ?rhs"
proof
- note `u = g y' z` also
+ note \<open>u = g y' z\<close> also
assume "ord y y'"
with f have "f y \<subseteq> f y'" by(rule mcont_monoD)
- with `z \<in> f y`
+ with \<open>z \<in> f y\<close>
have "g y' z \<le> \<Squnion>(g y' ` f y')" by(auto intro: Sup_upper)
- also have "\<dots> \<le> ?rhs" using `y' \<in> Y` by(auto intro: Sup_upper)
+ also have "\<dots> \<le> ?rhs" using \<open>y' \<in> Y\<close> by(auto intro: Sup_upper)
finally show ?thesis .
next
- note `u = g y' z` also
+ note \<open>u = g y' z\<close> also
assume "ord y' y"
with g have "g y' z \<le> g y z" by(rule mcont_monoD)
- also have "\<dots> \<le> \<Squnion>(g y ` f y)" using `z \<in> f y`
+ also have "\<dots> \<le> \<Squnion>(g y ` f y)" using \<open>z \<in> f y\<close>
by(auto intro: Sup_upper)
- also have "\<dots> \<le> ?rhs" using `y \<in> Y` by(auto intro: Sup_upper)
+ also have "\<dots> \<le> ?rhs" using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
finally show ?thesis .
qed
qed
@@ -1537,11 +1537,11 @@
fix u
assume "u \<in> g y ` f y"
then obtain z where "u = g y z" "z \<in> f y" by auto
- note `u = g y z`
+ note \<open>u = g y z\<close>
also have "g y z \<le> \<Squnion>((\<lambda>x. g x z) ` Y)"
- using `y \<in> Y` by(auto intro: Sup_upper)
+ using \<open>y \<in> Y\<close> by(auto intro: Sup_upper)
also have "\<dots> = g (lub Y) z" by(simp add: mcont_contD[OF g chain Y])
- also have "\<dots> \<le> ?lhs" using `z \<in> f y` `y \<in> Y`
+ also have "\<dots> \<le> ?lhs" using \<open>z \<in> f y\<close> \<open>y \<in> Y\<close>
by(auto intro: Sup_upper simp add: mcont_contD[OF f chain Y])
finally show "u \<le> ?lhs" .
qed
@@ -1567,7 +1567,7 @@
shows admissible_Bex: "ccpo.admissible Union op \<subseteq> (\<lambda>A. \<exists>x\<in>A. P x)"
by(rule ccpo.admissibleI)(auto)
-subsection {* Parallel fixpoint induction *}
+subsection \<open>Parallel fixpoint induction\<close>
context
fixes luba :: "'a set \<Rightarrow> 'a"
--- a/src/HOL/Library/Multiset.thy Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Sun Apr 03 23:57:32 2016 +0200
@@ -443,7 +443,7 @@
interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
- -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
+ \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
lemma mset_less_eqI:
"(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"
@@ -464,7 +464,7 @@
by standard (simp, fact mset_le_exists_conv)
declare subset_mset.zero_order[simp del]
- -- \<open>this removes some simp rules not in the usual order for multisets\<close>
+ \<comment> \<open>this removes some simp rules not in the usual order for multisets\<close>
lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
by (fact subset_mset.add_le_cancel_right)
@@ -587,7 +587,7 @@
show "class.semilattice_inf op #\<inter> op \<subseteq># op \<subset>#"
by standard (auto simp add: multiset_inter_def subseteq_mset_def)
qed
- -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
+ \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
lemma multiset_inter_count [simp]:
fixes A B :: "'a multiset"
@@ -712,7 +712,7 @@
subsubsection \<open>Bounded union\<close>
definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)
- where "sup_subset_mset A B = A + (B - A)" -- \<open>FIXME irregular fact name\<close>
+ where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>
interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#"
proof -
@@ -721,9 +721,9 @@
show "class.semilattice_sup op #\<union> op \<subseteq># op \<subset>#"
by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
qed
- -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
-
-lemma sup_subset_mset_count [simp]: -- \<open>FIXME irregular fact name\<close>
+ \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
+
+lemma sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close>
"count (A #\<union> B) x = max (count A x) (count B x)"
by (simp add: sup_subset_mset_def)
@@ -1554,8 +1554,8 @@
"\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" ("\<Union>#_" [900] 900)
- where "\<Union># MM \<equiv> msetsum MM" -- \<open>FIXME ambiguous notation --
- could likewise refer to @{text "\<Squnion>#"}\<close>
+ where "\<Union># MM \<equiv> msetsum MM" \<comment> \<open>FIXME ambiguous notation --
+ could likewise refer to \<open>\<Squnion>#\<close>\<close>
lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
by (induct MM) auto
@@ -2115,7 +2115,7 @@
unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
by standard (auto simp add: le_multiset_def irrefl dest: trans)
-qed -- \<open>FIXME avoid junk stemming from type class interpretation\<close>
+qed \<comment> \<open>FIXME avoid junk stemming from type class interpretation\<close>
lemma mult_less_irrefl [elim!]:
fixes M :: "'a::order multiset"
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sun Apr 03 23:57:32 2016 +0200
@@ -606,10 +606,10 @@
shows "valid_path (f o g)"
proof -
obtain s where "finite s" and g_diff: "g C1_differentiable_on {0..1} - s"
- using `valid_path g` unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
+ using \<open>valid_path g\<close> unfolding valid_path_def piecewise_C1_differentiable_on_def by auto
have "f \<circ> g differentiable at t" when "t\<in>{0..1} - s" for t
proof (rule differentiable_chain_at)
- show "g differentiable at t" using `valid_path g`
+ show "g differentiable at t" using \<open>valid_path g\<close>
by (meson C1_differentiable_on_eq \<open>g C1_differentiable_on {0..1} - s\<close> that)
next
have "g t\<in>path_image g" using that DiffD1 image_eqI path_image_def by metis
@@ -627,7 +627,7 @@
next
have "continuous_on {0..1} (\<lambda>x. deriv f (g x))"
using continuous_on_compose[OF _ con[unfolded path_image_def],unfolded comp_def]
- `valid_path g` piecewise_C1_differentiable_on_def valid_path_def
+ \<open>valid_path g\<close> piecewise_C1_differentiable_on_def valid_path_def
by blast
then show "continuous_on ({0..1} - s) (\<lambda>x. deriv f (g x))"
using continuous_on_subset by blast
@@ -650,14 +650,14 @@
have "isCont f x" when "x\<in>path_image g" for x
proof -
obtain f' where "(f has_field_derivative f') (at x)"
- using der[rule_format] `x\<in>path_image g` by auto
+ using der[rule_format] \<open>x\<in>path_image g\<close> by auto
thus ?thesis using DERIV_isCont by auto
qed
then have "continuous_on (path_image g) f" using continuous_at_imp_continuous_on by auto
- then show ?thesis using path_continuous_image `valid_path g` valid_path_imp_path by auto
+ then show ?thesis using path_continuous_image \<open>valid_path g\<close> valid_path_imp_path by auto
qed
ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
- using `finite s` by auto
+ using \<open>finite s\<close> by auto
qed
@@ -5730,13 +5730,13 @@
lemma valid_path_compose_holomorphic:
assumes "valid_path g" and holo:"f holomorphic_on s" and "open s" "path_image g \<subseteq> s"
shows "valid_path (f o g)"
-proof (rule valid_path_compose[OF `valid_path g`])
+proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
fix x assume "x \<in> path_image g"
then show "\<exists>f'. (f has_field_derivative f') (at x)"
- using holo holomorphic_on_open[OF `open s`] `path_image g \<subseteq> s` by auto
+ using holo holomorphic_on_open[OF \<open>open s\<close>] \<open>path_image g \<subseteq> s\<close> by auto
next
have "deriv f holomorphic_on s"
- using holomorphic_deriv holo `open s` by auto
+ using holomorphic_deriv holo \<open>open s\<close> by auto
then show "continuous_on (path_image g) (deriv f)"
using assms(4) holomorphic_on_imp_continuous_on holomorphic_on_subset by auto
qed
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Sun Apr 03 23:57:32 2016 +0200
@@ -964,7 +964,7 @@
proof -
have f0: "(f \<longlongrightarrow> 0) at_infinity"
proof -
- have DIM_complex[intro]: "2 \<le> DIM(complex)" --\<open>should not be necessary!\<close>
+ have DIM_complex[intro]: "2 \<le> DIM(complex)" \<comment>\<open>should not be necessary!\<close>
by simp
have "continuous_on (inverse ` (ball 0 r - {0})) f"
using continuous_on_subset holf holomorphic_on_imp_continuous_on by blast
@@ -2149,61 +2149,61 @@
proof -
assume "n>m"
have "(h \<longlongrightarrow> 0) (at z within ball z r)"
- proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (n - m) * g w"])
- have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> h w = (w-z)^(n-m) * g w" using `n>m` asm
+ proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) ^ (n - m) * g w"])
+ have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> h w = (w-z)^(n-m) * g w" using \<open>n>m\<close> asm
by (auto simp add:field_simps power_diff)
then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
\<Longrightarrow> (x' - z) ^ (n - m) * g x' = h x'" for x' by auto
next
def F\<equiv>"at z within ball z r"
and f'\<equiv>"\<lambda>x. (x - z) ^ (n-m)"
- have "f' z=0" using `n>m` unfolding f'_def by auto
+ have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def
by (intro continuous_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
moreover have "(g \<longlongrightarrow> g z) F"
- using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] `r>0`
+ using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] \<open>r>0\<close>
unfolding F_def by auto
ultimately show " ((\<lambda>w. f' w * g w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
qed
moreover have "(h \<longlongrightarrow> h z) (at z within ball z r)"
using holomorphic_on_imp_continuous_on[OF h_holo]
- by (auto simp add:continuous_on_def `r>0`)
- moreover have "at z within ball z r \<noteq> bot" using `r>0`
+ by (auto simp add:continuous_on_def \<open>r>0\<close>)
+ moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close>
by (auto simp add:trivial_limit_within islimpt_ball)
ultimately have "h z=0" by (auto intro: tendsto_unique)
- thus False using asm `r>0` by auto
+ thus False using asm \<open>r>0\<close> by auto
qed
moreover have "m>n \<Longrightarrow> False"
proof -
assume "m>n"
have "(g \<longlongrightarrow> 0) (at z within ball z r)"
- proof (rule Lim_transform_within[OF _ `r>0`, where f="\<lambda>w. (w - z) ^ (m - n) * h w"])
- have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> g w = (w-z)^(m-n) * h w" using `m>n` asm
+ proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) ^ (m - n) * h w"])
+ have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> g w = (w-z)^(m-n) * h w" using \<open>m>n\<close> asm
by (auto simp add:field_simps power_diff)
then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk>
\<Longrightarrow> (x' - z) ^ (m - n) * h x' = g x'" for x' by auto
next
def F\<equiv>"at z within ball z r"
and f'\<equiv>"\<lambda>x. (x - z) ^ (m-n)"
- have "f' z=0" using `m>n` unfolding f'_def by auto
+ have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto
moreover have "continuous F f'" unfolding f'_def F_def
by (intro continuous_intros)
ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def
by (simp add: continuous_within)
moreover have "(h \<longlongrightarrow> h z) F"
- using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] `r>0`
+ using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] \<open>r>0\<close>
unfolding F_def by auto
ultimately show " ((\<lambda>w. f' w * h w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce
qed
moreover have "(g \<longlongrightarrow> g z) (at z within ball z r)"
using holomorphic_on_imp_continuous_on[OF g_holo]
- by (auto simp add:continuous_on_def `r>0`)
- moreover have "at z within ball z r \<noteq> bot" using `r>0`
+ by (auto simp add:continuous_on_def \<open>r>0\<close>)
+ moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close>
by (auto simp add:trivial_limit_within islimpt_ball)
ultimately have "g z=0" by (auto intro: tendsto_unique)
- thus False using asm `r>0` by auto
+ thus False using asm \<open>r>0\<close> by auto
qed
ultimately show "n=m" by fastforce
qed
@@ -2220,18 +2220,18 @@
g:"g holomorphic_on ball z r"
"\<And>w. w \<in> ball z r \<Longrightarrow> f w = (w - z) ^ n * g w"
"\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0"
- using holomorphic_factor_zero_nonconstant[OF holo `open s` `connected s` `z\<in>s` `f z=0`]
+ using holomorphic_factor_zero_nonconstant[OF holo \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>]
by (metis assms(3) assms(5) assms(6))
def r'\<equiv>"r/2"
have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff)
hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'"
"(\<forall>w\<in>cball z r'. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)"
- using g `ball z r \<subseteq> s` by auto
- moreover have "r'>0" unfolding r'_def using `0<r` by auto
+ using g \<open>ball z r \<subseteq> s\<close> by auto
+ moreover have "r'>0" unfolding r'_def using \<open>0<r\<close> by auto
ultimately show "\<exists>n g r. 0 < n \<and> 0 < r \<and> g holomorphic_on cball z r
\<and> (\<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)"
apply (intro exI[of _ n] exI[of _ g] exI[of _ r'])
- by (simp add:`0 < n`)
+ by (simp add:\<open>0 < n\<close>)
next
fix m n
def fac\<equiv>"\<lambda>n g r. \<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0"
@@ -2242,7 +2242,7 @@
obtain h r2 where "0 < m" "0 < r2" and h_holo: "h holomorphic_on cball z r2"
and "fac m h r2" using m_asm by auto
def r\<equiv>"min r1 r2"
- have "r>0" using `r1>0` `r2>0` unfolding r_def by auto
+ have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto
moreover have "\<forall>w\<in>ball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0 \<and> f w = (w - z)^m * h w \<and> h w\<noteq>0"
using \<open>fac m h r2\<close> \<open>fac n g r1\<close> unfolding fac_def r_def
by fastforce
@@ -2257,11 +2257,11 @@
proof
fix p assume "p\<in>s"
then obtain e1 where "0 < e1" and e1_b:"ball p e1 \<subseteq> s"
- using open_contains_ball_eq[OF `open s`] by auto
+ using open_contains_ball_eq[OF \<open>open s\<close>] by auto
obtain e2 where "0<e2" and "\<forall>x\<in>pts. x \<noteq> p \<longrightarrow> e2 \<le> dist p x"
- using finite_set_avoid[OF `finite pts`,of p] by auto
+ using finite_set_avoid[OF \<open>finite pts\<close>,of p] by auto
hence "\<forall>w\<in>ball p (min e1 e2). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)" using e1_b by auto
- thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` `e1>0`
+ thus "\<exists>e>0. \<forall>w\<in>ball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using \<open>e2>0\<close> \<open>e1>0\<close>
apply (rule_tac x="min e1 e2" in exI)
by auto
qed
@@ -2275,33 +2275,33 @@
then obtain e1 where "e1>0" and e1: "\<forall>w\<in>ball p e1. w\<in>s \<and> (w\<noteq>p \<longrightarrow> w\<notin>pts)"
using finite_ball_avoid[OF assms] by auto
def e2\<equiv>"e1/2"
- have "e2>0" and "e2<e1" unfolding e2_def using `e1>0` by auto
+ have "e2>0" and "e2<e1" unfolding e2_def using \<open>e1>0\<close> by auto
then have "cball p e2 \<subseteq> ball p e1" by (subst cball_subset_ball_iff,auto)
- then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using `e2>0` e1 by auto
+ then show "\<exists>e>0. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)" using \<open>e2>0\<close> e1 by auto
qed
lemma get_integrable_path:
assumes "open s" "connected (s-pts)" "finite pts" "f holomorphic_on (s-pts) " "a\<in>s-pts" "b\<in>s-pts"
obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b"
"path_image g \<subseteq> s-pts" "f contour_integrable_on g" using assms
-proof (induct arbitrary:s thesis a rule:finite_induct[OF `finite pts`]) print_cases
+proof (induct arbitrary:s thesis a rule:finite_induct[OF \<open>finite pts\<close>]) print_cases
case 1
obtain g where "valid_path g" "path_image g \<subseteq> s" "pathstart g = a" "pathfinish g = b"
- using connected_open_polynomial_connected[OF `open s`,of a b ] `connected (s - {})`
+ using connected_open_polynomial_connected[OF \<open>open s\<close>,of a b ] \<open>connected (s - {})\<close>
valid_path_polynomial_function "1.prems"(6) "1.prems"(7) by auto
moreover have "f contour_integrable_on g"
- using contour_integrable_holomorphic_simple[OF _ `open s` `valid_path g` `path_image g \<subseteq> s`,of f]
- `f holomorphic_on s - {}`
+ using contour_integrable_holomorphic_simple[OF _ \<open>open s\<close> \<open>valid_path g\<close> \<open>path_image g \<subseteq> s\<close>,of f]
+ \<open>f holomorphic_on s - {}\<close>
by auto
ultimately show ?case using "1"(1)[of g] by auto
next
case idt:(2 p pts)
obtain e where "e>0" and e:"\<forall>w\<in>ball a e. w \<in> s \<and> (w \<noteq> a \<longrightarrow> w \<notin> insert p pts)"
- using finite_ball_avoid[OF `open s` `finite (insert p pts)`,rule_format,of a]
- `a \<in> s - insert p pts`
+ using finite_ball_avoid[OF \<open>open s\<close> \<open>finite (insert p pts)\<close>,rule_format,of a]
+ \<open>a \<in> s - insert p pts\<close>
by auto
def a'\<equiv>"a+e/2"
- have "a'\<in>s-{p} -pts" using e[rule_format,of "a+e/2"] `e>0`
+ have "a'\<in>s-{p} -pts" using e[rule_format,of "a+e/2"] \<open>e>0\<close>
by (auto simp add:dist_complex_def a'_def)
then obtain g' where g'[simp]:"valid_path g'" "pathstart g' = a'" "pathfinish g' = b"
"path_image g' \<subseteq> s - {p} - pts" "f contour_integrable_on g'"
@@ -2312,7 +2312,7 @@
moreover have "pathstart g = a" and "pathfinish g = b" unfolding g_def by auto
moreover have "path_image g \<subseteq> s - insert p pts" unfolding g_def
proof (rule subset_path_image_join)
- have "closed_segment a a' \<subseteq> ball a e" using `e>0`
+ have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close>
by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
then show "path_image (linepath a a') \<subseteq> s - insert p pts" using e idt(9)
by auto
@@ -2321,7 +2321,7 @@
qed
moreover have "f contour_integrable_on g"
proof -
- have "closed_segment a a' \<subseteq> ball a e" using `e>0`
+ have "closed_segment a a' \<subseteq> ball a e" using \<open>e>0\<close>
by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute)
then have "continuous_on (closed_segment a a') f"
using e idt.prems(6) holomorphic_on_imp_continuous_on[OF idt.prems(5)]
@@ -2331,7 +2331,7 @@
using contour_integrable_continuous_linepath by auto
then show ?thesis unfolding g_def
apply (rule contour_integrable_joinI)
- by (auto simp add: `e>0`)
+ by (auto simp add: \<open>e>0\<close>)
qed
ultimately show ?case using idt.prems(1)[of g] by auto
qed
@@ -2343,32 +2343,32 @@
"\<forall>p\<in>s. h p>0 \<and> (\<forall>w\<in>cball p (h p). w\<in>s \<and> (w\<noteq>p \<longrightarrow> w \<notin> pts))"
shows "contour_integral g f = (\<Sum>p\<in>pts. winding_number g p * contour_integral (circlepath p (h p)) f)"
using assms
-proof (induct arbitrary:s g rule:finite_induct[OF `finite pts`])
+proof (induct arbitrary:s g rule:finite_induct[OF \<open>finite pts\<close>])
case 1
then show ?case by (simp add: Cauchy_theorem_global contour_integral_unique)
next
case (2 p pts)
- note fin[simp] = `finite (insert p pts)`
- and connected = `connected (s - insert p pts)`
- and valid[simp] = `valid_path g`
- and g_loop[simp] = `pathfinish g = pathstart g`
- and holo[simp]= `f holomorphic_on s - insert p pts`
- and path_img = `path_image g \<subseteq> s - insert p pts`
- and winding = `\<forall>z. z \<notin> s \<longrightarrow> winding_number g z = 0`
- and h = `\<forall>pa\<in>s. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s \<and> (w \<noteq> pa \<longrightarrow> w \<notin> insert p pts))`
+ note fin[simp] = \<open>finite (insert p pts)\<close>
+ and connected = \<open>connected (s - insert p pts)\<close>
+ and valid[simp] = \<open>valid_path g\<close>
+ and g_loop[simp] = \<open>pathfinish g = pathstart g\<close>
+ and holo[simp]= \<open>f holomorphic_on s - insert p pts\<close>
+ and path_img = \<open>path_image g \<subseteq> s - insert p pts\<close>
+ and winding = \<open>\<forall>z. z \<notin> s \<longrightarrow> winding_number g z = 0\<close>
+ and h = \<open>\<forall>pa\<in>s. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s \<and> (w \<noteq> pa \<longrightarrow> w \<notin> insert p pts))\<close>
have "h p>0" and "p\<in>s"
and h_p: "\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> insert p pts)"
- using h `insert p pts \<subseteq> s` by auto
+ using h \<open>insert p pts \<subseteq> s\<close> by auto
obtain pg where pg[simp]: "valid_path pg" "pathstart pg = pathstart g" "pathfinish pg=p+h p"
"path_image pg \<subseteq> s-insert p pts" "f contour_integrable_on pg"
proof -
have "p + h p\<in>cball p (h p)" using h[rule_format,of p]
by (simp add: \<open>p \<in> s\<close> dist_norm)
- then have "p + h p \<in> s - insert p pts" using h[rule_format,of p] `insert p pts \<subseteq> s`
+ then have "p + h p \<in> s - insert p pts" using h[rule_format,of p] \<open>insert p pts \<subseteq> s\<close>
by fastforce
moreover have "pathstart g \<in> s - insert p pts " using path_img by auto
ultimately show ?thesis
- using get_integrable_path[OF `open s` connected fin holo,of "pathstart g" "p+h p"] that
+ using get_integrable_path[OF \<open>open s\<close> connected fin holo,of "pathstart g" "p+h p"] that
by blast
qed
obtain n::int where "n=winding_number g p"
@@ -2394,7 +2394,7 @@
and "pathstart (n_circ 0) = p + h p"
and "pathfinish (n_circ 0) = p + h p"
and "p \<notin> path_image (n_circ 0)"
- unfolding n_circ_def p_circ_pt_def using `h p > 0`
+ unfolding n_circ_def p_circ_pt_def using \<open>h p > 0\<close>
by (auto simp add: dist_norm)
show "winding_number (n_circ 0) p'=0 \<and> p'\<notin>path_image (n_circ 0)" when "p'\<notin>s- pts" for p'
unfolding n_circ_def p_circ_pt_def
@@ -2409,7 +2409,7 @@
case (Suc k)
have n_Suc:"n_circ (Suc k) = p_circ +++ n_circ k" unfolding n_circ_def by auto
have pcirc:"p \<notin> path_image p_circ" "valid_path p_circ" "pathfinish p_circ = pathstart (n_circ k)"
- using Suc(3) unfolding p_circ_def using `h p > 0` by (auto simp add: p_circ_def)
+ using Suc(3) unfolding p_circ_def using \<open>h p > 0\<close> by (auto simp add: p_circ_def)
have pcirc_image:"path_image p_circ \<subseteq> s - insert p pts"
proof -
have "path_image p_circ \<subseteq> cball p (h p)" using \<open>0 < h p\<close> p_circ_def by auto
@@ -2426,15 +2426,15 @@
proof -
have "path_image p_circ = sphere p (h p)"
unfolding p_circ_def using \<open>0 < h p\<close> by auto
- then show ?thesis unfolding n_Suc using Suc.hyps(5) `h p>0`
+ then show ?thesis unfolding n_Suc using Suc.hyps(5) \<open>h p>0\<close>
by (auto simp add: path_image_join[OF pcirc(3)] dist_norm)
qed
- then show "p \<notin> path_image (n_circ (Suc k))" using `h p>0` by auto
+ then show "p \<notin> path_image (n_circ (Suc k))" using \<open>h p>0\<close> by auto
show "winding_number (n_circ (Suc k)) p = of_nat (Suc k)"
proof -
have "winding_number p_circ p = 1"
- by (simp add: `h p > 0` p_circ_def winding_number_circlepath_centre)
- moreover have "p \<notin> path_image (n_circ k)" using Suc(5) `h p>0` by auto
+ by (simp add: \<open>h p > 0\<close> p_circ_def winding_number_circlepath_centre)
+ moreover have "p \<notin> path_image (n_circ k)" using Suc(5) \<open>h p>0\<close> by auto
then have "winding_number (p_circ +++ n_circ k) p
= winding_number p_circ p + winding_number (n_circ k) p"
using valid_path_imp_path Suc.hyps(1) Suc.hyps(2) pcirc
@@ -2485,14 +2485,14 @@
using n_circ unfolding cp_def by auto
next
have "sphere p (h p) \<subseteq> s - insert p pts"
- using h[rule_format,of p] `insert p pts \<subseteq> s` by force
+ using h[rule_format,of p] \<open>insert p pts \<subseteq> s\<close> by force
moreover have "p + complex_of_real (h p) \<in> s - insert p pts"
using pg(3) pg(4) by (metis pathfinish_in_path_image subsetCE)
ultimately show "path_image cp \<subseteq> s - insert p pts" unfolding cp_def
using n_circ(5) by auto
next
show "winding_number cp p = - n"
- unfolding cp_def using winding_number_reversepath n_circ `h p>0` by auto
+ unfolding cp_def using winding_number_reversepath n_circ \<open>h p>0\<close> by auto
next
show "winding_number cp p'=0 \<and> p' \<notin> path_image cp" when "p'\<notin>s - pts" for p'
unfolding cp_def
@@ -2509,11 +2509,11 @@
qed
def g'\<equiv>"g +++ pg +++ cp +++ (reversepath pg)"
have "contour_integral g' f = (\<Sum>p\<in>pts. winding_number g' p * contour_integral (circlepath p (h p)) f)"
- proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ `finite pts` ])
+ proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ \<open>finite pts\<close> ])
show "connected (s - {p} - pts)" using connected by (metis Diff_insert2)
- show "open (s - {p})" using `open s` by auto
- show " pts \<subseteq> s - {p}" using `insert p pts \<subseteq> s` ` p \<notin> pts` by blast
- show "f holomorphic_on s - {p} - pts" using holo `p \<notin> pts` by (metis Diff_insert2)
+ show "open (s - {p})" using \<open>open s\<close> by auto
+ show " pts \<subseteq> s - {p}" using \<open>insert p pts \<subseteq> s\<close> \<open> p \<notin> pts\<close> by blast
+ show "f holomorphic_on s - {p} - pts" using holo \<open>p \<notin> pts\<close> by (metis Diff_insert2)
show "valid_path g'"
unfolding g'_def cp_def using n_circ valid pg g_loop
by (auto intro!:valid_path_join )
@@ -2536,7 +2536,7 @@
have "winding_number (g +++ pg +++ cp +++ reversepath pg) z = winding_number g z
+ winding_number (pg +++ cp +++ (reversepath pg)) z"
proof (rule winding_number_join)
- show "path g" using `valid_path g` by simp
+ show "path g" using \<open>valid_path g\<close> by simp
show "z \<notin> path_image g" using z path_img by auto
show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp by auto
next
@@ -2568,7 +2568,7 @@
finally have "winding_number g' z = winding_number g z + winding_number cp z"
unfolding g'_def .
moreover have "winding_number g z + winding_number cp z = 0"
- using winding z `n=winding_number g p` by auto
+ using winding z \<open>n=winding_number g p\<close> by auto
ultimately show "winding_number g' z = 0" unfolding g'_def by auto
qed
show "\<forall>pa\<in>s - {p}. 0 < h pa \<and> (\<forall>w\<in>cball pa (h pa). w \<in> s - {p} \<and> (w \<noteq> pa \<longrightarrow> w \<notin> pts))"
@@ -2581,7 +2581,7 @@
+ contour_integral (pg +++ cp +++ reversepath pg) f"
unfolding g'_def
apply (subst Cauchy_Integral_Thm.contour_integral_join)
- by (auto simp add:open_Diff[OF `open s`,OF finite_imp_closed[OF fin]]
+ by (auto simp add:open_Diff[OF \<open>open s\<close>,OF finite_imp_closed[OF fin]]
intro!: contour_integrable_holomorphic_simple[OF holo _ _ path_img]
contour_integrable_reversepath)
also have "... = contour_integral g f + contour_integral pg f
@@ -2596,7 +2596,7 @@
using contour_integral_reversepath
by (auto simp add:contour_integrable_reversepath)
also have "... = contour_integral g f - winding_number g p * contour_integral p_circ f"
- using `n=winding_number g p` by auto
+ using \<open>n=winding_number g p\<close> by auto
finally show ?thesis .
qed
moreover have "winding_number g' p' = winding_number g p'" when "p'\<in>pts" for p'
@@ -2631,7 +2631,7 @@
ultimately show ?case unfolding p_circ_def
apply (subst (asm) setsum.cong[OF refl,
of pts _ "\<lambda>p. winding_number g p * contour_integral (circlepath p (h p)) f"])
- by (auto simp add:setsum.insert[OF `finite pts` `p\<notin>pts`] algebra_simps)
+ by (auto simp add:setsum.insert[OF \<open>finite pts\<close> \<open>p\<notin>pts\<close>] algebra_simps)
qed
@@ -2652,7 +2652,7 @@
have "pts=pts1 \<union> pts2" "pts1 \<inter> pts2 = {}" "pts2 \<inter> s={}" "pts1\<subseteq>s"
unfolding pts1_def pts2_def by auto
have "contour_integral g f = (\<Sum>p\<in>pts1. circ p)" unfolding circ_def
- proof (rule Cauchy_theorem_aux[OF `open s` _ _ `pts1\<subseteq>s` _ `valid_path g` loop _ homo])
+ proof (rule Cauchy_theorem_aux[OF \<open>open s\<close> _ _ \<open>pts1\<subseteq>s\<close> _ \<open>valid_path g\<close> loop _ homo])
show "connected (s - pts1)" by (metis Diff_Int2 Int_absorb assms(2) pts1_def)
show "finite pts1" using \<open>pts = pts1 \<union> pts2\<close> assms(3) by auto
show "f holomorphic_on s - pts1" by (metis Diff_Int2 Int_absorb holo pts1_def)
@@ -2663,14 +2663,14 @@
moreover have "setsum circ pts2=0"
proof -
have "winding_number g p=0" when "p\<in>pts2" for p
- using `pts2 \<inter> s={}` that homo[rule_format,of p] by auto
+ using \<open>pts2 \<inter> s={}\<close> that homo[rule_format,of p] by auto
thus ?thesis unfolding circ_def
apply (intro setsum.neutral)
by auto
qed
moreover have "?R=setsum circ pts1 + setsum circ pts2"
unfolding circ_def
- using setsum.union_disjoint[OF _ _ `pts1 \<inter> pts2 = {}`] `finite pts` `pts=pts1 \<union> pts2`
+ using setsum.union_disjoint[OF _ _ \<open>pts1 \<inter> pts2 = {}\<close>] \<open>finite pts\<close> \<open>pts=pts1 \<union> pts2\<close>
by blast
ultimately show ?thesis
apply (fold circ_def)
@@ -2717,8 +2717,8 @@
have "(\<exists>!n. n>0 \<and> (\<exists> h r. P h r n))"
proof -
have "\<exists>!n. \<exists>h r. n>0 \<and> P h r n"
- using holomorphic_factor_zero_Ex1[OF `open s` `connected s` `z\<in>s` holo `f z=0`
- `\<exists>w\<in>s. f w\<noteq>0`] unfolding P_def
+ using holomorphic_factor_zero_Ex1[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo \<open>f z=0\<close>
+ \<open>\<exists>w\<in>s. f w\<noteq>0\<close>] unfolding P_def
apply (subst mult.commute)
by auto
thus ?thesis by auto
@@ -2738,10 +2738,10 @@
obtain r2 where "r2>0" "cball z r2 \<subseteq> s"
using assms(3) assms(5) open_contains_cball_eq by blast
def r3\<equiv>"min r1 r2"
- have "P h r3 n" using `P h r1 n` `r2>0` unfolding P_def r3_def
+ have "P h r3 n" using \<open>P h r1 n\<close> \<open>r2>0\<close> unfolding P_def r3_def
by auto
- moreover have "cball z r3 \<subseteq> s" using `cball z r2 \<subseteq> s` unfolding r3_def by auto
- ultimately show ?thesis using `n>0` unfolding P_def by auto
+ moreover have "cball z r3 \<subseteq> s" using \<open>cball z r2 \<subseteq> s\<close> unfolding r3_def by auto
+ ultimately show ?thesis using \<open>n>0\<close> unfolding P_def by auto
qed
lemma porder_exist:
@@ -2756,8 +2756,8 @@
def zo\<equiv>"zorder (inverse \<circ> f) z" and zp\<equiv>"zer_poly (inverse \<circ> f) z"
obtain r where "0 < zo" "0 < r" "cball z r \<subseteq> s" and zp_holo: "zp holomorphic_on cball z r" and
zp_fac: "\<forall>w\<in>cball z r. (inverse \<circ> f) w = zp w * (w - z) ^ zo \<and> zp w \<noteq> 0"
- using zorder_exist[OF `open s` `connected s` `z\<in>s` holo,folded zo_def zp_def]
- `f z=0` `\<exists>w\<in>s. f w\<noteq>0`
+ using zorder_exist[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo,folded zo_def zp_def]
+ \<open>f z=0\<close> \<open>\<exists>w\<in>s. f w\<noteq>0\<close>
by auto
have n:"n=zo" and h:"h=inverse o zp"
unfolding n_def zo_def porder_def h_def zp_def pol_poly_def by simp_all
@@ -2767,8 +2767,8 @@
using zp_fac unfolding h n comp_def
by (metis divide_inverse_commute field_class.field_inverse_zero inverse_inverse_eq
inverse_mult_distrib mult.commute)
- moreover have "0 < n" unfolding n using `zo>0` by simp
- ultimately show ?thesis using `0 < r` `cball z r \<subseteq> s` by auto
+ moreover have "0 < n" unfolding n using \<open>zo>0\<close> by simp
+ ultimately show ?thesis using \<open>0 < r\<close> \<open>cball z r \<subseteq> s\<close> by auto
qed
lemma base_residue:
@@ -2785,7 +2785,7 @@
r_b:"cball z r \<subseteq> s" and
h_holo:"h holomorphic_on cball z r"
and h:"(\<forall>w\<in>cball z r. f w = h w / (w - z) ^ n \<and> h w \<noteq> 0)"
- using porder_exist[OF `open s` `connected s` `z\<in>s` holo `f z=0` non_c]
+ using porder_exist[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo \<open>f z=0\<close> non_c]
unfolding n_def h_def by auto
def c\<equiv>"complex_of_real (2 * pi) * \<i>"
have "residue f z = (deriv ^^ (n - 1)) h z / fact (n-1)"
@@ -2795,15 +2795,15 @@
then have "((\<lambda>u. h u / (u - z) ^ n) has_contour_integral c * residue f z)
(circlepath z r)"
using Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n -1"
- ,unfolded Suc_diff_1[OF `n>0`],folded c_def] h_holo r_b
- by (auto simp add:`r>0` holomorphic_on_imp_continuous_on holomorphic_on_subset)
+ ,unfolded Suc_diff_1[OF \<open>n>0\<close>],folded c_def] h_holo r_b
+ by (auto simp add:\<open>r>0\<close> holomorphic_on_imp_continuous_on holomorphic_on_subset)
then have "(f has_contour_integral c * residue f z) (circlepath z r)"
proof (elim has_contour_integral_eq)
fix x assume "x \<in> path_image (circlepath z r)"
hence "x\<in>cball z r" using \<open>0 < r\<close> by auto
then show "h x / (x - z) ^ n = f x" using h by auto
qed
- then show ?thesis using `r>0` `cball z r \<subseteq> s` unfolding c_def by auto
+ then show ?thesis using \<open>r>0\<close> \<open>cball z r \<subseteq> s\<close> unfolding c_def by auto
qed
theorem residue_theorem:
@@ -2822,26 +2822,26 @@
def contour\<equiv>"\<lambda>p e. (f has_contour_integral c * residue f p) (circlepath p e)"
def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)"
have "poles \<subseteq> pts" and "finite pts"
- using poles `finite {p. f p=0}` unfolding pts_def is_pole_def by auto
+ using poles \<open>finite {p. f p=0}\<close> unfolding pts_def is_pole_def by auto
have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> contour p e)"
when "p\<in>s" for p
proof -
obtain e1 where e:"e1>0" and e:"avoid p e1"
- using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto
+ using finite_cball_avoid[OF \<open>open s\<close> \<open>finite pts\<close>] \<open>p\<in>s\<close> unfolding avoid_def by auto
have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> contour p e2"
when "p\<in>poles" unfolding c_def contour_def
- proof (rule base_residue[of "ball p e1" p f,simplified,OF `e1>0`])
+ proof (rule base_residue[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>])
show "inverse \<circ> f holomorphic_on ball p e1"
proof -
def f'\<equiv>"inverse o f"
have "f holomorphic_on ball p e1 - {p}"
- using holo e `poles \<subseteq> pts` unfolding avoid_def
+ using holo e \<open>poles \<subseteq> pts\<close> unfolding avoid_def
apply (elim holomorphic_on_subset)
by auto
then have f'_holo:"f' holomorphic_on ball p e1 - {p}" unfolding f'_def comp_def
apply (elim holomorphic_on_inverse)
using e pts_def ball_subset_cball unfolding avoid_def by blast
- moreover have "isCont f' p" using `p\<in>poles` poles unfolding f'_def is_pole_def by auto
+ moreover have "isCont f' p" using \<open>p\<in>poles\<close> poles unfolding f'_def is_pole_def by auto
ultimately show "f' holomorphic_on ball p e1"
apply (elim no_isolated_singularity[rotated])
apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified])
@@ -2849,10 +2849,10 @@
holomorphic_on_imp_differentiable_at by fastforce
qed
next
- show "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto
+ show "f p = 0" using \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
next
def p'\<equiv>"p+e1/2"
- have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+ have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
apply (rule_tac x=p' in bexI)
by (auto simp add:pts_def)
@@ -2861,7 +2861,7 @@
def e3\<equiv>"if p\<in>poles then e2 else e1"
have "avoid p e3"
using e2 e that avoid_def e3_def by auto
- moreover have "e3>0" using `e1>0` e2 unfolding e3_def by auto
+ moreover have "e3>0" using \<open>e1>0\<close> e2 unfolding e3_def by auto
moreover have " p\<in>poles \<longrightarrow> contour p e3" using e2 unfolding e3_def by auto
ultimately show ?thesis by auto
qed
@@ -2870,12 +2870,12 @@
def cont\<equiv>"\<lambda>p. contour_integral (circlepath p (h p)) f"
have "contour_integral \<gamma> f = (\<Sum>p\<in>poles. winding_number \<gamma> p * cont p)"
unfolding cont_def
- proof (rule Cauchy_theorem_singularities[OF `open s` `connected (s-poles)` _ holo `valid_path \<gamma>`
- loop `path_image \<gamma> \<subseteq> s-poles` homo])
- show "finite poles" using `poles \<subseteq> pts` and `finite pts` by (simp add: finite_subset)
+ proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> \<open>connected (s-poles)\<close> _ holo \<open>valid_path \<gamma>\<close>
+ loop \<open>path_image \<gamma> \<subseteq> s-poles\<close> homo])
+ show "finite poles" using \<open>poles \<subseteq> pts\<close> and \<open>finite pts\<close> by (simp add: finite_subset)
next
show "\<forall>p\<in>s. 0 < h p \<and> (\<forall>w\<in>cball p (h p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> poles))"
- using `poles \<subseteq> pts` h unfolding avoid_def by blast
+ using \<open>poles \<subseteq> pts\<close> h unfolding avoid_def by blast
qed
also have "... = (\<Sum>p\<in>poles. c * (winding_number \<gamma> p * residue f p))"
proof (rule setsum.cong[of poles poles,simplified])
@@ -2886,7 +2886,7 @@
then have "cont p=c*residue f p"
unfolding cont_def
apply (intro contour_integral_unique)
- using h[unfolded contour_def] `p \<in> poles` by blast
+ using h[unfolded contour_def] \<open>p \<in> poles\<close> by blast
then show ?thesis by auto
next
assume "p\<notin>s"
@@ -2925,12 +2925,12 @@
def cont_zero\<equiv>"\<lambda>ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)"
def avoid\<equiv>"\<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts)"
have "poles \<subseteq> pts" and "zeros \<subseteq> pts" and "finite zeros" and "pts=zeros \<union> poles"
- using poles `finite pts` unfolding pts_def zeros_def is_pole_def by auto
+ using poles \<open>finite pts\<close> unfolding pts_def zeros_def is_pole_def by auto
have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> cont_pole ff p e) \<and> (p\<in>zeros \<longrightarrow> cont_zero ff p e)"
when "p\<in>s" for p
proof -
obtain e1 where e:"e1>0" and e:"avoid p e1"
- using finite_cball_avoid[OF `open s` `finite pts`] `p\<in>s` unfolding avoid_def by auto
+ using finite_cball_avoid[OF \<open>open s\<close> \<open>finite pts\<close>] \<open>p\<in>s\<close> unfolding avoid_def by auto
have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2"
when "p\<in>poles"
proof -
@@ -2941,7 +2941,7 @@
have "inverse \<circ> f holomorphic_on ball p e1"
proof -
have "f holomorphic_on ball p e1 - {p}"
- using f_holo e `poles \<subseteq> pts` unfolding avoid_def
+ using f_holo e \<open>poles \<subseteq> pts\<close> unfolding avoid_def
apply (elim holomorphic_on_subset)
by auto
then have inv_holo:"(inverse o f) holomorphic_on ball p e1 - {p}"
@@ -2949,7 +2949,7 @@
apply (elim holomorphic_on_inverse)
using e pts_def ball_subset_cball unfolding avoid_def by blast
moreover have "isCont (inverse o f) p"
- using `p\<in>poles` poles unfolding is_pole_def by auto
+ using \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
ultimately show "(inverse o f) holomorphic_on ball p e1"
apply (elim no_isolated_singularity[rotated])
apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified])
@@ -2957,11 +2957,11 @@
holomorphic_on_imp_differentiable_at unfolding comp_def
by fastforce
qed
- moreover have "f p = 0" using `p\<in>poles` poles unfolding is_pole_def by auto
+ moreover have "f p = 0" using \<open>p\<in>poles\<close> poles unfolding is_pole_def by auto
moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0"
proof -
def p'\<equiv>"p+e1/2"
- have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+ have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
apply (rule_tac x=p' in bexI)
by (auto simp add:pts_def)
@@ -2971,50 +2971,50 @@
"cball p r \<subseteq> ball p e1" and
pp_holo:"pp holomorphic_on cball p r" and
pp_po:"(\<forall>w\<in>cball p r. f w = pp w / (w - p) ^ po \<and> pp w \<noteq> 0)"
- using porder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding po_def pp_def
+ using porder_exist[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>] unfolding po_def pp_def
by auto
def e2\<equiv>"r/2"
- have "e2>0" using `r>0` unfolding e2_def by auto
+ have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto
def anal\<equiv>"\<lambda>w. deriv pp w * h w / pp w" and prin\<equiv>"\<lambda>w. - of_nat po * h w / (w - p)"
have "((\<lambda>w. prin w + anal w) has_contour_integral - c * po * h p) (circlepath p e2)"
proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified])
have "ball p r \<subseteq> s"
using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast
then have "cball p e2 \<subseteq> s"
- using `r>0` unfolding e2_def by auto
+ using \<open>r>0\<close> unfolding e2_def by auto
then have "(\<lambda>w. - of_nat po * h w) holomorphic_on cball p e2"
using h_holo
by (auto intro!: holomorphic_intros)
then show "(prin has_contour_integral - c * of_nat po * h p ) (circlepath p e2)"
using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. - of_nat po * h w"]
- `e2>0`
+ \<open>e2>0\<close>
unfolding prin_def
by (auto simp add: mult.assoc)
have "anal holomorphic_on ball p r" unfolding anal_def
- using pp_holo h_holo pp_po `ball p r \<subseteq> s`
+ using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close>
by (auto intro!: holomorphic_intros)
then show "(anal has_contour_integral 0) (circlepath p e2)"
- using e2_def `r>0`
+ using e2_def \<open>r>0\<close>
by (auto elim!: Cauchy_theorem_disc_simple)
qed
then have "cont_pole ff' p e2" unfolding cont_pole_def po_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
- then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+ then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
def wp\<equiv>"w-p"
have "wp\<noteq>0" and "pp w \<noteq>0"
- unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto
+ unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto
moreover have der_f':"deriv f' w = - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po"
proof (rule DERIV_imp_deriv)
def der \<equiv> "- po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po"
- have po:"po = Suc (po - Suc 0) " using `po>0` by auto
+ have po:"po = Suc (po - Suc 0) " using \<open>po>0\<close> by auto
have "(pp has_field_derivative (deriv pp w)) (at w)"
- using DERIV_deriv_iff_field_differentiable `w\<in>ball p r`
+ using DERIV_deriv_iff_field_differentiable \<open>w\<in>ball p r\<close>
holomorphic_on_imp_differentiable_at[of _ "ball p r"]
holomorphic_on_subset [OF pp_holo ball_subset_cball]
by (metis open_ball)
then show "(f' has_field_derivative der) (at w)"
- using `w\<noteq>p` `po>0` unfolding der_def f'_def
+ using \<open>w\<noteq>p\<close> \<open>po>0\<close> unfolding der_def f'_def
apply (auto intro!: derivative_eq_intros simp add:field_simps)
apply (subst (4) po)
apply (subst power_Suc)
@@ -3030,7 +3030,7 @@
then have "cont_pole ff p e2" unfolding cont_pole_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
- then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+ then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
have "deriv f' w = deriv f w"
proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"])
show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo
@@ -3038,14 +3038,14 @@
next
have "ball p e1 - {p} \<subseteq> s - poles"
using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto
- then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1`
+ then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close>
using ball_subset_cball by blast
then show "f holomorphic_on ball p r - {p}" using f_holo
by auto
next
show "open (ball p r - {p})" by auto
next
- show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto
+ show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto
next
fix x assume "x \<in> ball p r - {p}"
then show "f' x = f x"
@@ -3058,7 +3058,7 @@
qed
moreover have "cball p e2 \<subseteq> ball p e1"
using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto
- ultimately show ?thesis using `e2>0` by auto
+ ultimately show ?thesis using \<open>e2>0\<close> by auto
qed
then obtain e2 where e2:"p\<in>poles \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2"
by auto
@@ -3075,12 +3075,12 @@
using \<open>poles \<subseteq> pts\<close> avoid_def ball_subset_cball e that zeros_def by fastforce
thus ?thesis using f_holo by auto
qed
- moreover have "f p = 0" using `p\<in>zeros`
+ moreover have "f p = 0" using \<open>p\<in>zeros\<close>
using DiffD1 mem_Collect_eq pts_def zeros_def by blast
moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0"
proof -
def p'\<equiv>"p+e1/2"
- have "p'\<in>ball p e1" and "p'\<noteq>p" using `e1>0` unfolding p'_def by (auto simp add:dist_norm)
+ have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e unfolding avoid_def
apply (rule_tac x=p' in bexI)
by (auto simp add:pts_def)
@@ -3090,50 +3090,50 @@
"cball p r \<subseteq> ball p e1" and
pp_holo:"zp holomorphic_on cball p r" and
pp_po:"(\<forall>w\<in>cball p r. f w = zp w * (w - p) ^ zo \<and> zp w \<noteq> 0)"
- using zorder_exist[of "ball p e1" p f,simplified,OF `e1>0`] unfolding zo_def zp_def
+ using zorder_exist[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>] unfolding zo_def zp_def
by auto
def e2\<equiv>"r/2"
- have "e2>0" using `r>0` unfolding e2_def by auto
+ have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto
def anal\<equiv>"\<lambda>w. deriv zp w * h w / zp w" and prin\<equiv>"\<lambda>w. of_nat zo * h w / (w - p)"
have "((\<lambda>w. prin w + anal w) has_contour_integral c * zo * h p) (circlepath p e2)"
proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified])
have "ball p r \<subseteq> s"
using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e by blast
then have "cball p e2 \<subseteq> s"
- using `r>0` unfolding e2_def by auto
+ using \<open>r>0\<close> unfolding e2_def by auto
then have "(\<lambda>w. of_nat zo * h w) holomorphic_on cball p e2"
using h_holo
by (auto intro!: holomorphic_intros)
then show "(prin has_contour_integral c * of_nat zo * h p ) (circlepath p e2)"
using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. of_nat zo * h w"]
- `e2>0`
+ \<open>e2>0\<close>
unfolding prin_def
by (auto simp add: mult.assoc)
have "anal holomorphic_on ball p r" unfolding anal_def
- using pp_holo h_holo pp_po `ball p r \<subseteq> s`
+ using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close>
by (auto intro!: holomorphic_intros)
then show "(anal has_contour_integral 0) (circlepath p e2)"
- using e2_def `r>0`
+ using e2_def \<open>r>0\<close>
by (auto elim!: Cauchy_theorem_disc_simple)
qed
then have "cont_zero ff' p e2" unfolding cont_zero_def zo_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
- then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+ then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
def wp\<equiv>"w-p"
have "wp\<noteq>0" and "zp w \<noteq>0"
- unfolding wp_def using `w\<noteq>p` `w\<in>ball p r` pp_po by auto
+ unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto
moreover have der_f':"deriv f' w = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo"
proof (rule DERIV_imp_deriv)
def der\<equiv>"zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo"
- have po:"zo = Suc (zo - Suc 0) " using `zo>0` by auto
+ have po:"zo = Suc (zo - Suc 0) " using \<open>zo>0\<close> by auto
have "(zp has_field_derivative (deriv zp w)) (at w)"
- using DERIV_deriv_iff_field_differentiable `w\<in>ball p r`
+ using DERIV_deriv_iff_field_differentiable \<open>w\<in>ball p r\<close>
holomorphic_on_imp_differentiable_at[of _ "ball p r"]
holomorphic_on_subset [OF pp_holo ball_subset_cball]
by (metis open_ball)
then show "(f' has_field_derivative der) (at w)"
- using `w\<noteq>p` `zo>0` unfolding der_def f'_def
+ using \<open>w\<noteq>p\<close> \<open>zo>0\<close> unfolding der_def f'_def
by (auto intro!: derivative_eq_intros simp add:field_simps)
qed
ultimately show "prin w + anal w = ff' w"
@@ -3147,7 +3147,7 @@
then have "cont_zero ff p e2" unfolding cont_zero_def
proof (elim has_contour_integral_eq)
fix w assume "w \<in> path_image (circlepath p e2)"
- then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using `r>0` by auto
+ then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto
have "deriv f' w = deriv f w"
proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"])
show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo
@@ -3155,14 +3155,14 @@
next
have "ball p e1 - {p} \<subseteq> s - poles"
using avoid_def ball_subset_cball e \<open>poles \<subseteq> pts\<close> by auto
- then have "ball p r - {p} \<subseteq> s - poles" using `cball p r \<subseteq> ball p e1`
+ then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close>
using ball_subset_cball by blast
then show "f holomorphic_on ball p r - {p}" using f_holo
by auto
next
show "open (ball p r - {p})" by auto
next
- show "w \<in> ball p r - {p}" using `w\<in>ball p r` `w\<noteq>p` by auto
+ show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto
next
fix x assume "x \<in> ball p r - {p}"
then show "f' x = f x"
@@ -3175,13 +3175,13 @@
qed
moreover have "cball p e2 \<subseteq> ball p e1"
using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto
- ultimately show ?thesis using `e2>0` by auto
+ ultimately show ?thesis using \<open>e2>0\<close> by auto
qed
then obtain e3 where e3:"p\<in>zeros \<longrightarrow> e3>0 \<and> cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3"
by auto
def e4\<equiv>"if p\<in>poles then e2 else if p\<in>zeros then e3 else e1"
- have "e4>0" using e2 e3 `e1>0` unfolding e4_def by auto
- moreover have "avoid p e4" using e2 e3 `e1>0` e unfolding e4_def avoid_def by auto
+ have "e4>0" using e2 e3 \<open>e1>0\<close> unfolding e4_def by auto
+ moreover have "avoid p e4" using e2 e3 \<open>e1>0\<close> e unfolding e4_def avoid_def by auto
moreover have "p\<in>poles \<longrightarrow> cont_pole ff p e4" and "p\<in>zeros \<longrightarrow> cont_zero ff p e4"
by (auto simp add: e2 e3 e4_def pts_def zeros_def)
ultimately show ?thesis by auto
@@ -3193,17 +3193,17 @@
def w\<equiv>"\<lambda>p. winding_number g p"
have "contour_integral g ff = (\<Sum>p\<in>pts. w p * cont p)"
unfolding cont_def w_def
- proof (rule Cauchy_theorem_singularities[OF `open s` connected finite _ `valid_path g` loop
+ proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> connected finite _ \<open>valid_path g\<close> loop
path_img homo])
- have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] `open s` by auto
- then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo `poles \<subseteq> pts` h_holo
+ have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] \<open>open s\<close> by auto
+ then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo \<open>poles \<subseteq> pts\<close> h_holo
by (auto intro!: holomorphic_intros simp add:pts_def)
next
show "\<forall>p\<in>s. 0 < get_e p \<and> (\<forall>w\<in>cball p (get_e p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pts))"
using get_e using avoid_def by blast
qed
also have "... = (\<Sum>p\<in>zeros. w p * cont p) + (\<Sum>p\<in>poles. w p * cont p)"
- using `finite pts` unfolding `pts=zeros \<union> poles`
+ using \<open>finite pts\<close> unfolding \<open>pts=zeros \<union> poles\<close>
apply (subst setsum.union_disjoint)
by (auto simp add:zeros_def)
also have "... = c * ((\<Sum>p\<in>zeros. w p * h p * zorder f p) - (\<Sum>p\<in>poles. w p * h p * porder f p))"
@@ -3216,7 +3216,7 @@
assume "p \<in> s"
have "cont p = c * h p * (zorder f p)" unfolding cont_def
apply (rule contour_integral_unique)
- using get_e `p\<in>s` `p\<in>zeros` unfolding cont_zero_def
+ using get_e \<open>p\<in>s\<close> \<open>p\<in>zeros\<close> unfolding cont_zero_def
by (metis mult.assoc mult.commute)
thus ?thesis by auto
next
@@ -3236,7 +3236,7 @@
assume "p \<in> s"
have "cont p = - c * h p * (porder f p)" unfolding cont_def
apply (rule contour_integral_unique)
- using get_e `p\<in>s` `p\<in>poles` unfolding cont_pole_def
+ using get_e \<open>p\<in>s\<close> \<open>p\<in>poles\<close> unfolding cont_pole_def
by (metis mult.assoc mult.commute)
thus ?thesis by auto
next
@@ -3259,7 +3259,7 @@
proof (rule differentiable_at_imp_differentiable_on)
fix x assume "x\<in>s"
obtain f' where "(f has_field_derivative f') (at x) "
- using holomorphic_on_imp_differentiable_at[OF f_holo `open s` `x\<in>s`]
+ using holomorphic_on_imp_differentiable_at[OF f_holo \<open>open s\<close> \<open>x\<in>s\<close>]
unfolding field_differentiable_def by auto
then have " (f has_derivative op * f') (at x)"
using has_field_derivative_imp_has_derivative[of f f' "at x"] by auto
@@ -3290,8 +3290,8 @@
proof -
have False when "z\<in>path_image \<gamma>" and "f z + g z=0" for z
proof -
- have "cmod (f z) > cmod (g z)" using `z\<in>path_image \<gamma>` path_less by auto
- moreover have "f z = - g z" using `f z + g z =0` by (simp add: eq_neg_iff_add_eq_0)
+ have "cmod (f z) > cmod (g z)" using \<open>z\<in>path_image \<gamma>\<close> path_less by auto
+ moreover have "f z = - g z" using \<open>f z + g z =0\<close> by (simp add: eq_neg_iff_add_eq_0)
then have "cmod (f z) = cmod (g z)" by auto
ultimately show False by auto
qed
@@ -3301,8 +3301,8 @@
proof -
have False when "z\<in>path_image \<gamma>" and "f z =0" for z
proof -
- have "cmod (g z) < cmod (f z) " using `z\<in>path_image \<gamma>` path_less by auto
- then have "cmod (g z) < 0" using `f z=0` by auto
+ have "cmod (g z) < cmod (f z) " using \<open>z\<in>path_image \<gamma>\<close> path_less by auto
+ then have "cmod (g z) < 0" using \<open>f z=0\<close> by auto
then show False by auto
qed
then show ?thesis unfolding zeros_f_def using path_img by auto
@@ -3312,7 +3312,7 @@
def h\<equiv>"\<lambda>p. g p / f p + 1"
obtain spikes
where "finite spikes" and spikes: "\<forall>x\<in>{0..1} - spikes. \<gamma> differentiable at x"
- using `valid_path \<gamma>`
+ using \<open>valid_path \<gamma>\<close>
by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq)
have h_contour:"((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
proof -
@@ -3334,12 +3334,12 @@
by auto
qed
have valid_h:"valid_path (h \<circ> \<gamma>)"
- proof (rule valid_path_compose_holomorphic[OF `valid_path \<gamma>` _ _ path_f])
+ proof (rule valid_path_compose_holomorphic[OF \<open>valid_path \<gamma>\<close> _ _ path_f])
show "h holomorphic_on s - zeros_f"
unfolding h_def using f_holo g_holo
by (auto intro!: holomorphic_intros simp add:zeros_f_def)
next
- show "open (s - zeros_f)" using `finite zeros_f` `open s` finite_imp_closed
+ show "open (s - zeros_f)" using \<open>finite zeros_f\<close> \<open>open s\<close> finite_imp_closed
by auto
qed
have "((\<lambda>z. 1/z) has_contour_integral 0) (h \<circ> \<gamma>)"
@@ -3362,7 +3362,7 @@
moreover have "vector_derivative (h \<circ> \<gamma>) (at x) = vector_derivative \<gamma> (at x) * deriv h (\<gamma> x)"
when "x\<in>{0..1} - spikes" for x
proof (rule vector_derivative_chain_at_general)
- show "\<gamma> differentiable at x" using that `valid_path \<gamma>` spikes by auto
+ show "\<gamma> differentiable at x" using that \<open>valid_path \<gamma>\<close> spikes by auto
next
def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"
def t\<equiv>"\<gamma> x"
@@ -3374,13 +3374,13 @@
unfolding h_def der_def using g_holo f_holo
apply (auto intro!: derivative_eq_intros)
by (auto simp add: DERIV_deriv_iff_field_differentiable
- holomorphic_on_imp_differentiable_at[OF _ `open s`])
+ holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>])
then show "\<exists>g'. (h has_field_derivative g') (at (\<gamma> x))" unfolding t_def by auto
qed
then have " (op / 1 has_contour_integral 0) (h \<circ> \<gamma>)
= ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>"
unfolding has_contour_integral
- apply (intro has_integral_spike_eq[OF negligible_finite, OF `finite spikes`])
+ apply (intro has_integral_spike_eq[OF negligible_finite, OF \<open>finite spikes\<close>])
by auto
ultimately show ?thesis by auto
qed
@@ -3390,8 +3390,8 @@
+ contour_integral \<gamma> (\<lambda>p. deriv h p / h p)"
proof -
have "(\<lambda>p. deriv f p / f p) contour_integrable_on \<gamma>"
- proof (rule contour_integrable_holomorphic_simple[OF _ _ `valid_path \<gamma>` path_f])
- show "open (s - zeros_f)" using finite_imp_closed[OF `finite zeros_f`] `open s`
+ proof (rule contour_integrable_holomorphic_simple[OF _ _ \<open>valid_path \<gamma>\<close> path_f])
+ show "open (s - zeros_f)" using finite_imp_closed[OF \<open>finite zeros_f\<close>] \<open>open s\<close>
by auto
then show "(\<lambda>p. deriv f p / f p) holomorphic_on s - zeros_f"
using f_holo
@@ -3420,23 +3420,23 @@
ultimately show False by auto
qed
have der_fg:"deriv fg p = deriv f p + deriv g p" unfolding fg_def
- using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _ `open s`] path_img that
+ using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>] path_img that
by (auto intro!: deriv_add)
have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)"
proof -
def der\<equiv>"\<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)"
have "p\<in>s" using path_img that by auto
then have "(h has_field_derivative der p) (at p)"
- unfolding h_def der_def using g_holo f_holo `f p\<noteq>0`
+ unfolding h_def der_def using g_holo f_holo \<open>f p\<noteq>0\<close>
apply (auto intro!: derivative_eq_intros)
by (auto simp add: DERIV_deriv_iff_field_differentiable
- holomorphic_on_imp_differentiable_at[OF _ `open s`])
+ holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>])
then show ?thesis unfolding der_def using DERIV_imp_deriv by auto
qed
show ?thesis
apply (simp only:der_fg der_h)
- apply (auto simp add:field_simps `h p\<noteq>0` `f p\<noteq>0` `fg p\<noteq>0`)
- by (auto simp add:field_simps h_def `f p\<noteq>0` fg_def)
+ apply (auto simp add:field_simps \<open>h p\<noteq>0\<close> \<open>f p\<noteq>0\<close> \<open>fg p\<noteq>0\<close>)
+ by (auto simp add:field_simps h_def \<open>f p\<noteq>0\<close> fg_def)
qed
then have "contour_integral \<gamma> (\<lambda>p. deriv fg p / fg p)
= contour_integral \<gamma> (\<lambda>p. deriv f p / f p + deriv h p / h p)"
@@ -3445,19 +3445,19 @@
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)"
unfolding c_def zeros_fg_def w_def
- proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
+ proof (rule argument_principle[OF \<open>open s\<close> _ _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
show "connected (s - {p. fg p = 0})" using connected_fg unfolding zeros_fg_def .
show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto
show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def .
- show " finite {p. fg p = 0}" using `finite zeros_fg` unfolding zeros_fg_def .
+ show " finite {p. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def .
qed
moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)"
unfolding c_def zeros_f_def w_def
- proof (rule argument_principle[OF `open s` _ _ _ `valid_path \<gamma>` loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
+ proof (rule argument_principle[OF \<open>open s\<close> _ _ _ \<open>valid_path \<gamma>\<close> loop _ homo, of _ "{}" "\<lambda>_. 1",simplified])
show "connected (s - {p. f p = 0})" using connected_f unfolding zeros_f_def .
show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto
show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def .
- show "finite {p. f p = 0}" using `finite zeros_f` unfolding zeros_f_def .
+ show "finite {p. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def .
qed
ultimately have "c * (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))"
by auto
--- a/src/HOL/Multivariate_Analysis/Integration.thy Sun Apr 03 10:25:17 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Sun Apr 03 23:57:32 2016 +0200
@@ -2409,7 +2409,7 @@
using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
text\<open>The case analysis eliminates the condition @{term "f integrable_on s"} at the cost
- of the type class constraint @{text"division_ring"}\<close>
+ of the type class constraint \<open>division_ring\<close>\<close>
corollary integral_mult_left [simp]:
fixes c:: "'a::{real_normed_algebra,division_ring}"
shows "integral s (\<lambda>x. f x * c) = integral s f * c"
--- a/src/Pure/General/file.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/General/file.scala Sun Apr 03 23:57:32 2016 +0200
@@ -141,7 +141,15 @@
if (path.is_file) path else error("No such file: " + path)
- /* find files */
+ /* directory content */
+
+ def read_dir(dir: Path): List[String] =
+ {
+ if (!dir.is_dir) error("Bad directory: " + dir.toString)
+ val files = dir.file.listFiles
+ if (files == null) Nil
+ else files.toList.map(_.getName)
+ }
def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] =
{
--- a/src/Pure/ML/ml_env.ML Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/ML/ml_env.ML Sun Apr 03 23:57:32 2016 +0200
@@ -57,12 +57,12 @@
val empty =
make_data (true,
(Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
- (Symtab.make ML_Name_Space.initial_val,
- Symtab.make ML_Name_Space.initial_type,
- Symtab.make ML_Name_Space.initial_fixity,
- Symtab.make ML_Name_Space.initial_structure,
- Symtab.make ML_Name_Space.initial_signature,
- Symtab.make ML_Name_Space.initial_functor),
+ (Symtab.make ML_Name_Space.sml_val,
+ Symtab.make ML_Name_Space.sml_type,
+ Symtab.make ML_Name_Space.sml_fixity,
+ Symtab.make ML_Name_Space.sml_structure,
+ Symtab.make ML_Name_Space.sml_signature,
+ Symtab.make ML_Name_Space.sml_functor),
Inttab.empty);
fun extend (data : T) = make_data (false, #tables data, #sml_tables data, #breakpoints data);
fun merge (data : T * T) =
--- a/src/Pure/ML/ml_name_space.ML Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML Sun Apr 03 23:57:32 2016 +0200
@@ -40,30 +40,35 @@
type valueVal = Values.value;
fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
- val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
val forget_val = PolyML.Compiler.forgetValue;
type typeVal = TypeConstrs.typeConstr;
fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
- val initial_type = #allType global ();
val forget_type = PolyML.Compiler.forgetType;
type fixityVal = Infixes.fixity;
fun displayFix (_: string, x) = Infixes.print x;
- val initial_fixity = #allFix global ();
type structureVal = Structures.structureVal;
fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
- val initial_structure =
- List.filter (fn (a, _) => not (List.exists (fn b => a = b) critical_structures))
- (#allStruct global ());
val forget_structure = PolyML.Compiler.forgetStructure;
type signatureVal = Signatures.signatureVal;
fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
- val initial_signature = #allSig global ();
type functorVal = Functors.functorVal;
fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
- val initial_functor = #allFunct global ();
+
+
+ (* Standard ML name space *)
+
+ val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
+ val sml_type = #allType global ();
+ val sml_fixity = #allFix global ();
+ val sml_structure =
+ List.filter (fn (a, _) => a <> "PolyML" andalso a <> "ML_System" andalso
+ not (List.exists (fn b => a = b) critical_structures)) (#allStruct global ());
+ val sml_signature =
+ List.filter (fn (a, _) => a <> "ML_SYSTEM" andalso a <> "ML_NAME_SPACE") (#allSig global ());
+ val sml_functor = #allFunct global ();
end;
--- a/src/Pure/System/isabelle_system.ML Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/System/isabelle_system.ML Sun Apr 03 23:57:32 2016 +0200
@@ -6,7 +6,6 @@
signature ISABELLE_SYSTEM =
sig
- val isabelle_tool: string -> string -> int
val mkdirs: Path.T -> unit
val mkdir: Path.T -> unit
val copy_dir: Path.T -> Path.T -> unit
@@ -37,29 +36,12 @@
in rc end;
-(* system commands *)
-
-fun isabelle_tool name args =
- (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
- let
- val path = Path.append (Path.explode dir) (Path.basic name);
- val platform_path = File.platform_path path;
- in
- if can OS.FileSys.modTime platform_path andalso
- not (OS.FileSys.isDir platform_path) andalso
- OS.FileSys.access (platform_path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
- then SOME path
- else NONE
- end handle OS.SysErr _ => NONE) of
- SOME path => bash (File.bash_path path ^ " " ^ args)
- | NONE => (warning ("Unknown Isabelle tool: " ^ name); 2));
+(* directory operations *)
fun system_command cmd =
- if bash cmd <> 0 then error ("System command failed: " ^ cmd)
- else ();
+ if bash cmd <> 0 then error ("System command failed: " ^ cmd) else ();
-
-(* directory operations *)
+fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
fun mkdirs path =
if File.is_dir path then ()
@@ -112,8 +94,6 @@
(* tmp dirs *)
-fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path);
-
fun with_tmp_dir name f =
let
val path = create_tmp_path name "";
@@ -121,4 +101,3 @@
in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end;
end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_tool.scala Sun Apr 03 23:57:32 2016 +0200
@@ -0,0 +1,109 @@
+/* Title: Pure/System/isabelle_tool.scala
+ Author: Makarius
+
+Isabelle system tools: external executables or internal Scala functions.
+*/
+
+package isabelle
+
+
+object Isabelle_Tool
+{
+ /* external tools */
+
+ private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS"))
+
+ private def is_external(dir: Path, name: String): Boolean =
+ {
+ val file = (dir + Path.basic(name)).file
+ try {
+ file.isFile && file.canRead && file.canExecute &&
+ !name.endsWith("~") && !name.endsWith(".orig")
+ }
+ catch { case _: SecurityException => false }
+ }
+
+ private def list_external(): List[(String, String)] =
+ {
+ val Description = """.*\bDESCRIPTION: *(.*)""".r
+ for {
+ dir <- dirs() if dir.is_dir
+ name <- File.read_dir(dir) if is_external(dir, name)
+ } yield {
+ val source = File.read(dir + Path.basic(name))
+ val description =
+ split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
+ (name, description)
+ }
+ }
+
+ private def find_external(name: String): Option[List[String] => Unit] =
+ dirs.collectFirst({ case dir if is_external(dir, name) =>
+ (args: List[String]) =>
+ {
+ val tool = dir + Path.basic(name)
+ val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
+ sys.exit(result.print_stdout.rc)
+ }
+ })
+
+
+ /* internal tools */
+
+ private var internal_tools = Map.empty[String, (String, List[String] => Nothing)]
+
+ private def list_internal(): List[(String, String)] =
+ synchronized {
+ for ((name, (description, _)) <- internal_tools.toList) yield (name, description)
+ }
+
+ private def find_internal(name: String): Option[List[String] => Unit] =
+ synchronized { internal_tools.get(name).map(_._2) }
+
+ private def register(isabelle_tool: Isabelle_Tool): Unit =
+ synchronized {
+ internal_tools +=
+ (isabelle_tool.name ->
+ (isabelle_tool.description,
+ args => Command_Line.tool0 { isabelle_tool.body(args) }))
+ }
+
+ register(Build.isabelle_tool)
+ register(Build_Doc.isabelle_tool)
+ register(Check_Sources.isabelle_tool)
+ register(Doc.isabelle_tool)
+ register(ML_Process.isabelle_tool)
+ register(Options.isabelle_tool)
+ register(Update_Cartouches.isabelle_tool)
+ register(Update_Header.isabelle_tool)
+ register(Update_Then.isabelle_tool)
+ register(Update_Theorems.isabelle_tool)
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool0 {
+ args.toList match {
+ case Nil | List("-?") =>
+ val tool_descriptions =
+ (list_external() ::: list_internal()).sortBy(_._1).
+ map({ case (a, "") => a case (a, b) => a + " - " + b })
+ Getopts("""
+Usage: isabelle TOOL [ARGS ...]
+
+ Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
+
+Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage
+ case tool_name :: tool_args =>
+ find_external(tool_name) orElse find_internal(tool_name) match {
+ case Some(tool) => tool(tool_args)
+ case None => error("Unknown Isabelle tool: " + quote(tool_name))
+ }
+ }
+ }
+ }
+}
+
+sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
--- a/src/Pure/System/options.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/System/options.scala Sun Apr 03 23:57:32 2016 +0200
@@ -140,17 +140,16 @@
val encode: XML.Encode.T[Options] = (options => options.encode)
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
+ val isabelle_tool = Isabelle_Tool("option", "print Isabelle system options", args =>
{
- Command_Line.tool0 {
- var build_options = false
- var get_option = ""
- var list_options = false
- var export_file = ""
+ var build_options = false
+ var get_option = ""
+ var list_options = false
+ var export_file = ""
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
Options are:
@@ -162,34 +161,33 @@
Report Isabelle system options, augmented by MORE_OPTIONS given as
arguments NAME=VAL or NAME.
""",
- "b" -> (_ => build_options = true),
- "g:" -> (arg => get_option = arg),
- "l" -> (_ => list_options = true),
- "x:" -> (arg => export_file = arg))
+ "b" -> (_ => build_options = true),
+ "g:" -> (arg => get_option = arg),
+ "l" -> (_ => list_options = true),
+ "x:" -> (arg => export_file = arg))
- val more_options = getopts(args)
- if (get_option == "" && !list_options && export_file == "") getopts.usage()
+ val more_options = getopts(args)
+ if (get_option == "" && !list_options && export_file == "") getopts.usage()
- val options =
- {
- val options0 = Options.init()
- val options1 =
- if (build_options)
- (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
- else options0
- (options1 /: more_options)(_ + _)
- }
+ val options =
+ {
+ val options0 = Options.init()
+ val options1 =
+ if (build_options)
+ (options0 /: Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")))(_ + _)
+ else options0
+ (options1 /: more_options)(_ + _)
+ }
- if (get_option != "")
- Console.println(options.check_name(get_option).value)
+ if (get_option != "")
+ Console.println(options.check_name(get_option).value)
- if (export_file != "")
- File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
+ if (export_file != "")
+ File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
- if (get_option == "" && export_file == "")
- Console.println(options.print)
- }
- }
+ if (get_option == "" && export_file == "")
+ Console.println(options.print)
+ })
}
--- a/src/Pure/Thy/present.ML Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Thy/present.ML Sun Apr 03 23:57:32 2016 +0200
@@ -269,8 +269,8 @@
val doc_dir = Path.append doc_prefix (Path.basic doc_name);
val _ = Isabelle_System.mkdirs doc_dir;
val _ =
- Isabelle_System.isabelle_tool "latex"
- ("-o sty " ^ File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
+ Isabelle_System.bash ("isabelle latex -o sty " ^
+ File.bash_path (Path.append doc_dir (Path.basic "root.tex")));
val _ = List.app (fn file => Isabelle_System.copy_file_base file doc_dir) doc_files;
val _ = Isabelle_System.copy_file graph_file (Path.append doc_dir session_graph_path);
val _ = write_tex_index tex_index doc_dir;
@@ -360,8 +360,8 @@
val _ = Isabelle_System.mkdirs doc_path;
val root_path = Path.append doc_path (Path.basic "root.tex");
val _ = Isabelle_System.copy_file (Path.explode "~~/lib/texinputs/draft.tex") root_path;
- val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.bash_path root_path);
- val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.bash_path root_path);
+ val _ = Isabelle_System.bash ("isabelle latex -o sty " ^ File.bash_path root_path);
+ val _ = Isabelle_System.bash ("isabelle latex -o syms " ^ File.bash_path root_path);
fun known name =
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
@@ -382,8 +382,6 @@
val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"
val _ = Isabelle_System.mkdirs target_dir;
val _ = Isabelle_System.copy_file result target;
- in
- Isabelle_System.isabelle_tool "display" (File.bash_path target ^ " &")
- end);
+ in Isabelle_System.bash ("isabelle display " ^ File.bash_path target ^ " &") end);
end;
--- a/src/Pure/Tools/build.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/build.scala Sun Apr 03 23:57:32 2016 +0200
@@ -685,43 +685,40 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
+ val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
{
- Command_Line.tool {
- def show_settings(): String =
- cat_lines(List(
- "ISABELLE_BUILD_OPTIONS=" +
- quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
- "ISABELLE_BUILD_JAVA_OPTIONS=" +
- quote(Isabelle_System.getenv("ISABELLE_BUILD_JAVA_OPTIONS")),
- "",
- "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")),
- "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")),
- "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")),
- "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS"))))
+ def show_settings(): String =
+ cat_lines(List(
+ "ISABELLE_BUILD_OPTIONS=" +
+ quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
+ "",
+ "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")),
+ "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")),
+ "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")),
+ "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS"))))
- val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
+ val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
- var select_dirs: List[Path] = Nil
- var requirements = false
- var exclude_session_groups: List[String] = Nil
- var all_sessions = false
- var build_heap = false
- var clean_build = false
- var dirs: List[Path] = Nil
- var session_groups: List[String] = Nil
- var max_jobs = 1
- var check_keywords: Set[String] = Set.empty
- var list_files = false
- var no_build = false
- var options = (Options.init() /: build_options)(_ + _)
- var system_mode = false
- var verbose = false
- var exclude_sessions: List[String] = Nil
+ var select_dirs: List[Path] = Nil
+ var requirements = false
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var build_heap = false
+ var clean_build = false
+ var dirs: List[Path] = Nil
+ var session_groups: List[String] = Nil
+ var max_jobs = 1
+ var check_keywords: Set[String] = Set.empty
+ var list_files = false
+ var no_build = false
+ var options = (Options.init() /: build_options)(_ + _)
+ var system_mode = false
+ var verbose = false
+ var exclude_sessions: List[String] = Nil
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
@@ -745,58 +742,57 @@
Build and manage Isabelle sessions, depending on implicit settings:
""" + Library.prefix_lines(" ", show_settings()),
- "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
- "R" -> (_ => requirements = true),
- "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
- "a" -> (_ => all_sessions = true),
- "b" -> (_ => build_heap = true),
- "c" -> (_ => clean_build = true),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "g:" -> (arg => session_groups = session_groups ::: List(arg)),
- "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
- "k:" -> (arg => check_keywords = check_keywords + arg),
- "l" -> (_ => list_files = true),
- "n" -> (_ => no_build = true),
- "o:" -> (arg => options = options + arg),
- "s" -> (_ => system_mode = true),
- "v" -> (_ => verbose = true),
- "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "R" -> (_ => requirements = true),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "b" -> (_ => build_heap = true),
+ "c" -> (_ => clean_build = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+ "k:" -> (arg => check_keywords = check_keywords + arg),
+ "l" -> (_ => list_files = true),
+ "n" -> (_ => no_build = true),
+ "o:" -> (arg => options = options + arg),
+ "s" -> (_ => system_mode = true),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
- val sessions = getopts(args)
+ val sessions = getopts(args)
- val progress = new Console_Progress(verbose)
+ val progress = new Console_Progress(verbose)
- if (verbose) {
- progress.echo(
- Library.trim_line(
- Isabelle_System.bash(
- """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
- progress.echo(show_settings() + "\n")
- }
+ if (verbose) {
+ progress.echo(
+ Library.trim_line(
+ Isabelle_System.bash(
+ """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
+ progress.echo(show_settings() + "\n")
+ }
- val start_time = Time.now()
- val results =
- progress.interrupt_handler {
- build(options, progress, requirements, all_sessions, build_heap, clean_build,
- dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
- check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
- }
- val elapsed_time = Time.now() - start_time
+ val start_time = Time.now()
+ val results =
+ progress.interrupt_handler {
+ build(options, progress, requirements, all_sessions, build_heap, clean_build,
+ dirs, select_dirs, exclude_session_groups, session_groups, max_jobs, list_files,
+ check_keywords, no_build, system_mode, verbose, exclude_sessions, sessions)
+ }
+ val elapsed_time = Time.now() - start_time
- if (verbose) {
- progress.echo("\n" +
- Library.trim_line(
- Isabelle_System.bash("""echo -n "Finished at "; date""").out))
- }
+ if (verbose) {
+ progress.echo("\n" +
+ Library.trim_line(
+ Isabelle_System.bash("""echo -n "Finished at "; date""").out))
+ }
- val total_timing =
- (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
- copy(elapsed = elapsed_time)
- progress.echo(total_timing.message_resources)
+ val total_timing =
+ (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
+ copy(elapsed = elapsed_time)
+ progress.echo(total_timing.message_resources)
- results.rc
- }
- }
+ sys.exit(results.rc)
+ })
/* PIDE protocol */
--- a/src/Pure/Tools/build_doc.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/build_doc.scala Sun Apr 03 23:57:32 2016 +0200
@@ -67,17 +67,16 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
+ val isabelle_tool = Isabelle_Tool("build_doc", "build Isabelle documentation", args =>
{
- Command_Line.tool {
- var all_docs = false
- var max_jobs = 1
- var system_mode = false
+ var all_docs = false
+ var max_jobs = 1
+ var system_mode = false
- val getopts =
- Getopts("""
+ val getopts =
+ Getopts("""
Usage: isabelle build_doc [OPTIONS] [DOCS ...]"
Options are:
@@ -88,19 +87,20 @@
Build Isabelle documentation from documentation sessions with
suitable document_variants entry.
""",
- "a" -> (_ => all_docs = true),
- "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
- "s" -> (_ => system_mode = true))
+ "a" -> (_ => all_docs = true),
+ "j:" -> (arg => max_jobs = Properties.Value.Int.parse(arg)),
+ "s" -> (_ => system_mode = true))
+
+ val docs = getopts(args)
- val docs = getopts(args)
+ if (!all_docs && docs.isEmpty) getopts.usage()
- if (!all_docs && docs.isEmpty) getopts.usage()
-
- val options = Options.init()
- val progress = new Console_Progress()
+ val options = Options.init()
+ val progress = new Console_Progress()
+ val rc =
progress.interrupt_handler {
build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
}
- }
- }
+ sys.exit(rc)
+ })
}
--- a/src/Pure/Tools/check_sources.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/check_sources.scala Sun Apr 03 23:57:32 2016 +0200
@@ -52,11 +52,11 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
- {
- Command_Line.tool0 {
+ val isabelle_tool =
+ Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
+ {
val getopts = Getopts("""
Usage: isabelle check_sources [ROOT_DIRS...]
@@ -67,6 +67,5 @@
if (specs.isEmpty) getopts.usage()
for (root <- specs) check_hg(Path.explode(root))
- }
- }
+ })
}
--- a/src/Pure/Tools/doc.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/doc.scala Sun Apr 03 23:57:32 2016 +0200
@@ -91,28 +91,26 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
+ val isabelle_tool = Isabelle_Tool("doc", "view Isabelle documentation", args =>
{
- Command_Line.tool0 {
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle doc [DOC ...]
View Isabelle documentation.
""")
- val docs = getopts(args)
+ val docs = getopts(args)
- val entries = contents()
- if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
- else {
- docs.foreach(doc =>
- entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
- case Some(path) => view(path)
- case None => error("No Isabelle documentation entry: " + quote(doc))
- }
- )
- }
+ val entries = contents()
+ if (docs.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
+ else {
+ docs.foreach(doc =>
+ entries.collectFirst { case Doc(name, _, path) if doc == name => path } match {
+ case Some(path) => view(path)
+ case None => error("No Isabelle documentation entry: " + quote(doc))
+ }
+ )
}
- }
+ })
}
--- a/src/Pure/Tools/ml_process.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala Sun Apr 03 23:57:32 2016 +0200
@@ -102,18 +102,17 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
+ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args =>
{
- Command_Line.tool {
- var dirs: List[Path] = Nil
- var eval_args: List[String] = Nil
- var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
- var modes: List[String] = Nil
- var options = Options.init()
+ var dirs: List[Path] = Nil
+ var eval_args: List[String] = Nil
+ var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+ var modes: List[String] = Nil
+ var options = Options.init()
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle process [OPTIONS]
Options are:
@@ -127,20 +126,19 @@
Run the raw Isabelle ML process in batch mode.
""",
- "T:" -> (arg =>
- eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
- "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
- "l:" -> (arg => logic = arg),
- "m:" -> (arg => modes = arg :: modes),
- "o:" -> (arg => options = options + arg))
+ "T:" -> (arg =>
+ eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string0(arg))),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
+ "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
+ "l:" -> (arg => logic = arg),
+ "m:" -> (arg => modes = arg :: modes),
+ "o:" -> (arg => options = options + arg))
- val more_args = getopts(args)
- if (args.isEmpty || !more_args.isEmpty) getopts.usage()
+ val more_args = getopts(args)
+ if (args.isEmpty || !more_args.isEmpty) getopts.usage()
- ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
- result().print_stdout.rc
- }
- }
+ ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
+ result().print_stdout.rc
+ })
}
--- a/src/Pure/Tools/update_cartouches.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/update_cartouches.scala Sun Apr 03 23:57:32 2016 +0200
@@ -82,11 +82,11 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
- {
- Command_Line.tool0 {
+ val isabelle_tool =
+ Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args =>
+ {
var replace_comment = false
var replace_text = false
@@ -112,6 +112,5 @@
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
} update_cartouches(replace_comment, replace_text, Path.explode(File.standard_path(file)))
- }
- }
+ })
}
--- a/src/Pure/Tools/update_header.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/update_header.scala Sun Apr 03 23:57:32 2016 +0200
@@ -23,14 +23,14 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
private val headings =
Set("chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph")
- def main(args: Array[String])
- {
- Command_Line.tool0 {
+ val isabelle_tool =
+ Isabelle_Tool("update_header", "replace obsolete theory header command", args =>
+ {
var section = "section"
val getopts = Getopts("""
@@ -57,6 +57,5 @@
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
} update_header(section, Path.explode(File.standard_path(file)))
- }
- }
+ })
}
--- a/src/Pure/Tools/update_then.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/update_then.scala Sun Apr 03 23:57:32 2016 +0200
@@ -28,11 +28,11 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
- {
- Command_Line.tool0 {
+ val isabelle_tool =
+ Isabelle_Tool("update_then", "expand old Isar command conflations 'hence' and 'thus'", args =>
+ {
val getopts = Getopts("""
Usage: isabelle update_then [FILES|DIRS...]
@@ -51,6 +51,5 @@
spec <- specs
file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
} update_then(Path.explode(File.standard_path(file)))
- }
- }
+ })
}
--- a/src/Pure/Tools/update_theorems.scala Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/Tools/update_theorems.scala Sun Apr 03 23:57:32 2016 +0200
@@ -29,12 +29,11 @@
}
- /* command line entry point */
+ /* Isabelle tool wrapper */
- def main(args: Array[String])
+ val isabelle_tool = Isabelle_Tool("update_theorems", "update toplevel theorem keywords", args =>
{
- Command_Line.tool0 {
- val getopts = Getopts("""
+ val getopts = Getopts("""
Usage: isabelle update_theorems [FILES|DIRS...]
Recursively find .thy files and update toplevel theorem keywords:
@@ -47,13 +46,12 @@
Old versions of files are preserved by appending "~~".
""")
- val specs = getopts(args)
- if (specs.isEmpty) getopts.usage()
+ val specs = getopts(args)
+ if (specs.isEmpty) getopts.usage()
- for {
- spec <- specs
- file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
- } update_theorems(Path.explode(File.standard_path(file)))
- }
- }
+ for {
+ spec <- specs
+ file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+ } update_theorems(Path.explode(File.standard_path(file)))
+ })
}
--- a/src/Pure/build-jars Sun Apr 03 10:25:17 2016 +0200
+++ b/src/Pure/build-jars Sun Apr 03 23:57:32 2016 +0200
@@ -81,6 +81,7 @@
System/isabelle_charset.scala
System/isabelle_process.scala
System/isabelle_system.scala
+ System/isabelle_tool.scala
System/options.scala
System/platform.scala
System/posix_interrupt.scala