- {desc|strip|escape|addbreaks|nonempty}
-
-+
-+{files}
-+
-
-
+<
+<
{author|obfuscate} [{date|rfc822date}] rev {rev}
+---
+>
{date|age}
+> {author|obfuscate} [{date|rfc822date}] rev {rev} {inbranch%inbranchtag}{branches%branchtag}{tags%tagtag}
+12a8,10
+>
+> {files}
+>
+diff -r gitweb/changeset.tmpl isabelle/changeset.tmpl
+32c32
+<
| {date|date} ({date|age} ago) |
+---
+>
| {date|date} ({date|age}) |
+diff -r gitweb/fileannotate.tmpl isabelle/fileannotate.tmpl
+39c39
+<
{date|date} ({date|age} ago) |
+---
+>
{date|date} ({date|age}) |
+diff -r gitweb/filerevision.tmpl isabelle/filerevision.tmpl
+39c39
+<
{date|date} ({date|age} ago) |
+---
+>
{date|date} ({date|age}) |
+diff -r gitweb/graph.tmpl isabelle/graph.tmpl
+66c66
+< revlink += '
_DATE ago, by _USER';
+---
+> revlink += '
_DATE, by _USER';
+diff -r gitweb/map isabelle/map
+81c81
+< title="{node|short}: {desc|escape|firstline}">{author|user}@{rev}
+---
+> title="{node|short}: {desc|escape}">{author|user}@{rev}
+153c153
+<
{date|age} ago |
+---
+>
{date|age} |
+164c164
+<
{date|age} ago |
+---
+>
{date|age} |
+207c207
+<
{date|age} ago |
+---
+>
{date|age} |
+208a209
+>
{date|shortdate} |
+211c212
+<
{desc|strip|firstline|escape|nonempty}
+---
+>
{desc|strip|escape|nonempty}
+222c223,225
+<
{date|age} ago |
+---
+>
{date|age} |
+>
{author|person} |
+>
{date|shortdate} |
+225c228
+<
{desc|strip|firstline|escape|nonempty}
+---
+>
{desc|strip|escape|nonempty}
+241c244
+<
{lastchange|age} ago |
+---
+>
{lastchange|age} |
diff -r adb22dbb5242 -r 6354e21e61fa Admin/Mercurial/misc.diff
--- a/Admin/Mercurial/misc.diff Fri Nov 05 15:15:28 2010 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-diff -r hgweb/webcommands.py hgweb/webcommands.py
-653c653
-< desc = templatefilters.firstline(ctx.description())
----
-> desc = ctx.description()
-diff -r templates/atom/changelogentry.tmpl templates/atom/changelogentry.tmpl
-2c2
-<
#desc|strip|firstline|strip|escape#
----
->
#desc|strip|escape#
-diff -r templates/rss/changelogentry.tmpl templates/rss/changelogentry.tmpl
-2c2
-<
#desc|strip|firstline|strip|escape#
----
->
#desc|strip|escape#
-diff -r templates/rss/filelogentry.tmpl templates/rss/filelogentry.tmpl
-2c2
-<
#desc|strip|firstline|strip|escape#
----
->
#desc|strip|escape#
diff -r adb22dbb5242 -r 6354e21e61fa CONTRIBUTORS
--- a/CONTRIBUTORS Fri Nov 05 15:15:28 2010 -0700
+++ b/CONTRIBUTORS Sat Nov 06 10:01:00 2010 -0700
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* October 2010: Bogdan Grechuk, University of Edinburgh
+ Extended convex analysis in Multivariate Analysis.
+
* October 2010: Dmitriy Traytel, TUM
Coercive subtyping via subtype constraints.
diff -r adb22dbb5242 -r 6354e21e61fa NEWS
--- a/NEWS Fri Nov 05 15:15:28 2010 -0700
+++ b/NEWS Sat Nov 06 10:01:00 2010 -0700
@@ -6,6 +6,13 @@
*** General ***
+* System settings: ISABELLE_HOME_USER now includes ISABELLE_IDENTIFIER
+(and thus refers to something like $HOME/.isabelle/IsabelleXXXX),
+while the default heap location within that directory lacks that extra
+suffix. This isolates multiple Isabelle installations from each
+other, avoiding problems with old settings in new versions.
+INCOMPATIBILITY, need to copy/upgrade old user settings manually.
+
* Significantly improved Isabelle/Isar implementation manual.
* Explicit treatment of UTF8 sequences as Isabelle symbols, such that
@@ -82,6 +89,8 @@
*** HOL ***
+* Theory Multiset provides stable quicksort implementation of sort_key.
+
* Quickcheck now has a configurable time limit which is set to 30 seconds
by default. This can be changed by adding [timeout = n] to the quickcheck
command. The time limit for auto quickcheck is still set independently,
@@ -325,6 +334,14 @@
- Renamed options:
sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
+ sledgehammer [timeout = 77 s] ~> sledgehammer [timeout = 77]
+ (and "ms" and "min" are no longer supported)
+ INCOMPATIBILITY.
+
+* Nitpick:
+ - Renamed options:
+ nitpick [timeout = 77 s] ~> nitpick [timeout = 77]
+ nitpick [tac_timeout = 777 ms] ~> nitpick [tac_timeout = 0.777]
INCOMPATIBILITY.
* Changed SMT configuration options:
@@ -337,6 +354,9 @@
yices_options
smt_datatypes
+* Removed [split_format ... and ... and ...] version of
+[split_format]. Potential INCOMPATIBILITY.
+
*** FOL ***
* All constant names are now qualified. INCOMPATIBILITY.
@@ -349,6 +369,10 @@
*** ML ***
+* Discontinued obsolete function sys_error and exception SYS_ERROR.
+See implementation manual for further details on exceptions in
+Isabelle/ML.
+
* Antiquotation @{assert} inlines a function bool -> unit that raises
Fail if the argument is false. Due to inlining the source position of
failed assertions is included in the error output.
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/Thy/Adaptation.thy Sat Nov 06 10:01:00 2010 -0700
@@ -2,7 +2,8 @@
imports Setup
begin
-setup %invisible {* Code_Target.extend_target ("\
", ("SML", K I)) *}
+setup %invisible {* Code_Target.extend_target ("\", ("SML", K I))
+ #> Code_Target.extend_target ("\", ("Haskell", K I)) *}
section {* Adaptation to target languages \label{sec:adaptation} *}
@@ -235,7 +236,7 @@
@{command_def "code_reserved"} command:
*}
-code_reserved %quote "\" bool true false andalso
+code_reserved %quote "\" bool true false andalso
text {*
\noindent Next, we try to map HOL pairs to SML pairs, using the
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Codegen/Thy/Evaluation.thy
--- a/doc-src/Codegen/Thy/Evaluation.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/Thy/Evaluation.thy Sat Nov 06 10:01:00 2010 -0700
@@ -18,7 +18,7 @@
subsection {* Evaluation techniques *}
text {*
- The existing infrastructure provides a rich palett of evaluation
+ The existing infrastructure provides a rich palette of evaluation
techniques, each comprising different aspects:
\begin{description}
@@ -135,7 +135,7 @@
"t'"}.
\item Evaluation of @{term t} terminates which en exception
- indicating a pattern match failure or a not-implemented
+ indicating a pattern match failure or a non-implemented
function. As sketched in \secref{sec:partiality}, this can be
interpreted as partiality.
@@ -148,8 +148,8 @@
Exceptions of the third kind are propagated to the user.
By default return values of plain evaluation are optional, yielding
- @{text "SOME t'"} in the first case, @{text "NONE"} and in the
- second propagating the exception in the third case. A strict
+ @{text "SOME t'"} in the first case, @{text "NONE"} in the
+ second, and propagating the exception in the third case. A strict
variant of plain evaluation either yields @{text "t'"} or propagates
any exception, a liberal variant caputures any exception in a result
of type @{text "Exn.result"}.
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Codegen/Thy/Further.thy
--- a/doc-src/Codegen/Thy/Further.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/Thy/Further.thy Sat Nov 06 10:01:00 2010 -0700
@@ -124,7 +124,8 @@
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
\cite{bulwahn-et-al:2008:imperative}; the framework described there
- is available in session @{text Imperative_HOL}.
+ is available in session @{text Imperative_HOL}, together with a short
+ primer document.
*}
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Codegen/Thy/Refinement.thy
--- a/doc-src/Codegen/Thy/Refinement.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/Thy/Refinement.thy Sat Nov 06 10:01:00 2010 -0700
@@ -17,7 +17,7 @@
text {*
Program refinement works by choosing appropriate code equations
- explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+ explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
numbers:
*}
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex Sat Nov 06 10:01:00 2010 -0700
@@ -26,7 +26,8 @@
%
\isataginvisible
\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\isanewline
+\ \ {\isacharhash}{\isachargreater}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSMLdummy}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}Haskell{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
\endisataginvisible
{\isafoldinvisible}%
%
@@ -420,7 +421,7 @@
%
\isatagquote
\isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
+\ {\isachardoublequoteopen}{\isasymSMLdummy}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
\endisatagquote
{\isafoldquote}%
%
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex Sat Nov 06 10:01:00 2010 -0700
@@ -38,7 +38,7 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The existing infrastructure provides a rich palett of evaluation
+The existing infrastructure provides a rich palette of evaluation
techniques, each comprising different aspects:
\begin{description}
@@ -188,7 +188,7 @@
\item Evaluation of \isa{t} terminates with a result \isa{t{\isacharprime}}.
\item Evaluation of \isa{t} terminates which en exception
- indicating a pattern match failure or a not-implemented
+ indicating a pattern match failure or a non-implemented
function. As sketched in \secref{sec:partiality}, this can be
interpreted as partiality.
@@ -200,8 +200,8 @@
Exceptions of the third kind are propagated to the user.
By default return values of plain evaluation are optional, yielding
- \isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} and in the
- second propagating the exception in the third case. A strict
+ \isa{SOME\ t{\isacharprime}} in the first case, \isa{NONE} in the
+ second, and propagating the exception in the third case. A strict
variant of plain evaluation either yields \isa{t{\isacharprime}} or propagates
any exception, a liberal variant caputures any exception in a result
of type \isa{Exn{\isachardot}result}.
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Codegen/Thy/document/Further.tex
--- a/doc-src/Codegen/Thy/document/Further.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/Thy/document/Further.tex Sat Nov 06 10:01:00 2010 -0700
@@ -240,7 +240,8 @@
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
\cite{bulwahn-et-al:2008:imperative}; the framework described there
- is available in session \isa{Imperative{\isacharunderscore}HOL}.%
+ is available in session \isa{Imperative{\isacharunderscore}HOL}, together with a short
+ primer document.%
\end{isamarkuptext}%
\isamarkuptrue%
%
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Codegen/Thy/document/Refinement.tex
--- a/doc-src/Codegen/Thy/document/Refinement.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/Thy/document/Refinement.tex Sat Nov 06 10:01:00 2010 -0700
@@ -37,7 +37,7 @@
%
\begin{isamarkuptext}%
Program refinement works by choosing appropriate code equations
- explicitly (cf.~\label{sec:equations}); as example, we use Fibonacci
+ explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci
numbers:%
\end{isamarkuptext}%
\isamarkuptrue%
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Codegen/style.sty
--- a/doc-src/Codegen/style.sty Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/style.sty Sat Nov 06 10:01:00 2010 -0700
@@ -45,6 +45,7 @@
%% a trick
\newcommand{\isasymSML}{SML}
+\newcommand{\isasymSMLdummy}{SML}
%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sat Nov 06 10:01:00 2010 -0700
@@ -72,22 +72,18 @@
\end{matharray}
\begin{rail}
- 'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
+ 'split_format' '(' 'complete' ')'
;
\end{rail}
\begin{description}
- \item @{attribute (HOL) split_format}~@{text "p\<^sub>1 \ p\<^sub>m \ \
- \ q\<^sub>1 \ q\<^sub>n"} puts expressions of low-level tuple types into
- canonical form as specified by the arguments given; the @{text i}-th
- collection of arguments refers to occurrences in premise @{text i}
- of the rule. The ``@{text "(complete)"}'' option causes \emph{all}
+ \item @{attribute (HOL) split_format}\ @{text "(complete)"} causes
arguments in function applications to be represented canonically
according to their tuple type structure.
- Note that these operations tend to invent funny names for new local
- parameters to be introduced.
+ Note that this operation tends to invent funny names for new local
+ parameters introduced.
\end{description}
*}
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sat Nov 06 10:01:00 2010 -0700
@@ -93,21 +93,18 @@
\end{matharray}
\begin{rail}
- 'split_format' ((( name * ) + 'and') | ('(' 'complete' ')'))
+ 'split_format' '(' 'complete' ')'
;
\end{rail}
\begin{description}
- \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub m\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ q\isactrlsub {\isadigit{1}}\ {\isasymdots}\ q\isactrlsub n{\isachardoublequote}} puts expressions of low-level tuple types into
- canonical form as specified by the arguments given; the \isa{i}-th
- collection of arguments refers to occurrences in premise \isa{i}
- of the rule. The ``\isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}}'' option causes \emph{all}
+ \item \hyperlink{attribute.HOL.split-format}{\mbox{\isa{split{\isacharunderscore}format}}}\ \isa{{\isachardoublequote}{\isacharparenleft}complete{\isacharparenright}{\isachardoublequote}} causes
arguments in function applications to be represented canonically
according to their tuple type structure.
- Note that these operations tend to invent funny names for new local
- parameters to be introduced.
+ Note that this operation tends to invent funny names for new local
+ parameters introduced.
\end{description}%
\end{isamarkuptext}%
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Nitpick/nitpick.tex Sat Nov 06 10:01:00 2010 -0700
@@ -261,7 +261,7 @@
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
\hbox{}\qquad\qquad $x = a_3$ \\[2\smallskipamount]
-Total time: 768 ms.
+Total time: 0.76 s.
\postw
Nitpick found a counterexample in which $'a$ has cardinality 3. (For
@@ -797,7 +797,7 @@
Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount]
-Total time: 1439 ms.
+Total time: 1.43 s.
\postw
No genuine counterexample is possible because Nitpick cannot rule out the
@@ -850,7 +850,7 @@
& 2 := \{0, 2, 4, 6, 8, 1^\Q, 3^\Q, 5^\Q, 7^\Q, 9^\Q\}, \\[-2pt]
& 1 := \{0, 2, 4, 1^\Q, 3^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\}, \\[-2pt]
& 0 := \{0, 2, 1^\Q, 3^\Q, 4^\Q, 5^\Q, 6^\Q, 7^\Q, 8^\Q, 9^\Q\})\end{aligned}$ \\[2\smallskipamount]
-Total time: 2420 ms.
+Total time: 2.42 s.
\postw
Nitpick's output is very instructive. First, it tells us that the predicate is
@@ -1012,7 +1012,7 @@
\hbox{}\qquad\qquad $\textit{b} = a_2$ \\
\hbox{}\qquad\qquad $\textit{xs} = \textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega$ \\
\hbox{}\qquad\qquad $\textit{ys} = \textit{LCons}~a_2~(\textsl{THE}~\omega.\; \omega = \textit{LCons}~a_1~\omega)$ \\[2\smallskipamount]
-Total time: 1027 ms.
+Total time: 1.02 s.
\postw
The lazy list $\textit{xs}$ is simply $[a_1, a_1, a_1, \ldots]$, whereas
@@ -1160,7 +1160,7 @@
4 := \textit{Var}~0,\>
5 := \textit{Var}~0)\end{aligned}$ \\
\hbox{}\qquad\qquad $t = \textit{Lam}~(\textit{Lam}~(\textit{Var}~1))$ \\[2\smallskipamount]
-Total time: $3560$ ms.
+Total time: 3.56 s.
\postw
Using \textit{eval}, we find out that $\textit{subst}~\sigma~t =
@@ -1255,7 +1255,7 @@
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $\textit{xs} = [a_1, a_2]$ \\
\hbox{}\qquad\qquad $\textit{ys} = [b_1, b_1]$ \\[2\smallskipamount]
-Total time: 1636 ms.
+Total time: 1.63 s.
\postw
In theory, it should be sufficient to test a single scope:
@@ -1849,7 +1849,7 @@
using \textbf{nitpick\_\allowbreak params}. For example:
\prew
-\textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60$\,s$]
+\textbf{nitpick\_params} [\textit{verbose}, \,\textit{timeout} = 60]
\postw
The options are categorized as follows:\ mode of operation
@@ -1887,10 +1887,10 @@
\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
\item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\}.
-
\item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
-\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
-(milliseconds), or the keyword \textit{none} ($\infty$ years).
+\item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
+(e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
+($\infty$ seconds).
\item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
\item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
\item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
@@ -1966,7 +1966,7 @@
{\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
(\S\ref{scope-of-search}).}
-\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{10}$}
+\opdefault{card}{int\_seq}{\upshape 1--10}
Specifies the default sequence of cardinalities to use. This can be overridden
on a per-type basis using the \textit{card}~\qty{type} option described above.
@@ -2014,7 +2014,7 @@
{\small See also \textit{bits} (\S\ref{scope-of-search}) and
\textit{show\_datatypes} (\S\ref{output-format}).}
-\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12},\mathbf{14},\mathbf{16}$}
+\opdefault{bits}{int\_seq}{\upshape 1,2,3,4,6,8,10,12,14,16}
Specifies the number of bits to use to represent natural numbers and integers in
binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
@@ -2064,12 +2064,12 @@
{\small See also \textit{wf} (\S\ref{scope-of-search}) and
\textit{star\_linear\_preds} (\S\ref{optimizations}).}
-\opdefault{iter}{int\_seq}{$\mathbf{0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}$}
+\opdefault{iter}{int\_seq}{\upshape 0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}
Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
predicates. This can be overridden on a per-predicate basis using the
\textit{iter} \qty{const} option above.
-\opdefault{bisim\_depth}{int\_seq}{$\mathbf{9}$}
+\opdefault{bisim\_depth}{int\_seq}{\upshape 9}
Specifies the sequence of iteration counts to use when unrolling the
bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
of $-1$ means that no predicate is generated, in which case Nitpick performs an
@@ -2214,7 +2214,7 @@
\opnodefault{show\_all}{bool}
Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
-\opdefault{max\_potential}{int}{$\mathbf{1}$}
+\opdefault{max\_potential}{int}{\upshape 1}
Specifies the maximum number of potential counterexamples to display. Setting
this option to 0 speeds up the search for a genuine counterexample. This option
is implicitly set to 0 for automatic runs. If you set this option to a value
@@ -2226,7 +2226,7 @@
{\small See also \textit{check\_potential} (\S\ref{authentication}) and
\textit{sat\_solver} (\S\ref{optimizations}).}
-\opdefault{max\_genuine}{int}{$\mathbf{1}$}
+\opdefault{max\_genuine}{int}{\upshape 1}
Specifies the maximum number of genuine counterexamples to display. If you set
this option to a value greater than 1, you will need an incremental SAT solver,
such as \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that
@@ -2267,7 +2267,7 @@
arguments that are not accounted for are left alone, as if the specification had
been $1,\ldots,1,n_1,\ldots,n_k$.
-\opdefault{format}{int\_seq}{$\mathbf{1}$}
+\opdefault{format}{int\_seq}{\upshape 1}
Specifies the default format to use. Irrespective of the default format, the
extra arguments to a Skolem constant corresponding to the outer bound variables
are kept separated from the remaining arguments, the \textbf{for} arguments of
@@ -2484,19 +2484,19 @@
Unless you are tracking down a bug in Nitpick or distrust the peephole
optimizer, you should leave this option enabled.
-\opdefault{datatype\_sym\_break}{int}{5}
+\opdefault{datatype\_sym\_break}{int}{\upshape 5}
Specifies an upper bound on the number of datatypes for which Nitpick generates
symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
considerably, especially for unsatisfiable problems, but too much of it can slow
it down.
-\opdefault{kodkod\_sym\_break}{int}{15}
+\opdefault{kodkod\_sym\_break}{int}{\upshape 15}
Specifies an upper bound on the number of relations for which Kodkod generates
symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
considerably, especially for unsatisfiable problems, but too much of it can slow
it down.
-\opdefault{max\_threads}{int}{0}
+\opdefault{max\_threads}{int}{\upshape 0}
Specifies the maximum number of threads to use in Kodkod. If this option is set
to 0, Kodkod will compute an appropriate value based on the number of processor
cores available. The option is implicitly set to 1 for automatic runs.
@@ -2510,8 +2510,8 @@
\label{timeouts}
\begin{enum}
-\opdefault{timeout}{time}{$\mathbf{30}$ s}
-Specifies the maximum amount of time that the \textbf{nitpick} command should
+\opdefault{timeout}{float\_or\_none}{\upshape 30}
+Specifies the maximum number of seconds that the \textbf{nitpick} command should
spend looking for a counterexample. Nitpick tries to honor this constraint as
well as it can but offers no guarantees. For automatic runs,
\textit{timeout} is ignored; instead, Auto Quickcheck and Auto Nitpick share
@@ -2521,8 +2521,8 @@
\nopagebreak
{\small See also \textit{max\_threads} (\S\ref{optimizations}).}
-\opdefault{tac\_timeout}{time}{$\mathbf{500}$\,ms}
-Specifies the maximum amount of time that the \textit{auto} tactic should use
+\opdefault{tac\_timeout}{float\_or\_none}{\upshape 0.5}
+Specifies the maximum number of seconds that the \textit{auto} tactic should use
when checking a counterexample, and similarly that \textit{lexicographic\_order}
and \textit{size\_change} should use when checking whether a (co)in\-duc\-tive
predicate is well-founded. Nitpick tries to honor this constraint as well as it
@@ -2863,7 +2863,7 @@
which can become invalid if you change the definition of an inductive predicate
that is registered in the cache. To clear the cache,
run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
-501$\,\textit{ms}$).
+$0.51$).
\item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
\textbf{guess} command in a structured proof.
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sat Nov 06 10:01:00 2010 -0700
@@ -377,10 +377,12 @@
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or
\textit{smart}.
\item[$\bullet$] \qtybf{int\/}: An integer.
+\item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers
+(e.g., 0.6 0.95).
\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
-\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes),
-$s$ (seconds), or \textit{ms}
-(milliseconds), or the keyword \textit{none} ($\infty$ years).
+\item[$\bullet$] \qtybf{float\_or\_none\/}: An integer (e.g., 60) or
+floating-point number (e.g., 0.5) expressing a number of seconds, or the keyword
+\textit{none} ($\infty$ seconds).
\end{enum}
Default values are indicated in square brackets. Boolean options have a negated
@@ -457,8 +459,8 @@
\opnodefault{atp}{string}
Legacy alias for \textit{provers}.
-\opdefault{timeout}{time}{$\mathbf{30}$ s}
-Specifies the maximum amount of time that the automatic provers should spend
+\opdefault{timeout}{float\_or\_none}{\upshape 30}
+Specifies the maximum number of seconds that the automatic provers should spend
searching for a proof. For historical reasons, the default value of this option
can be overridden using the option ``Sledgehammer: Time Limit'' from the
``Isabelle'' menu in Proof General.
@@ -503,15 +505,15 @@
\label{relevance-filter}
\begin{enum}
-\opdefault{relevance\_thresholds}{int\_pair}{45~85}
+\opdefault{relevance\_thresholds}{float\_pair}{\upshape 0.45~0.85}
Specifies the thresholds above which facts are considered relevant by the
relevance filter. The first threshold is used for the first iteration of the
relevance filter and the second threshold is used for the last iteration (if it
is reached). The effective threshold is quadratically interpolated for the other
-iterations. Each threshold ranges from 0 to 100, where 0 means that all theorems
-are relevant and 100 only theorems that refer to previously seen constants.
+iterations. Each threshold ranges from 0 to 1, where 0 means that all theorems
+are relevant and 1 only theorems that refer to previously seen constants.
-\opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}}
+\opsmart{max\_relevant}{int\_or\_smart}
Specifies the maximum number of facts that may be returned by the relevance
filter. If the option is set to \textit{smart}, it is set to a value that was
empirically found to be appropriate for the prover. A typical value would be
@@ -540,7 +542,7 @@
fails; however, they are usually faster and sometimes more robust than
\textit{metis} proofs.
-\opdefault{isar\_shrink\_factor}{int}{1}
+\opdefault{isar\_shrink\_factor}{int}{\upshape 1}
Specifies the granularity of the Isar proof. A value of $n$ indicates that each
Isar proof step should correspond to a group of up to $n$ consecutive proof
steps in the ATP proof.
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/System/Thy/Basics.thy Sat Nov 06 10:01:00 2010 -0700
@@ -95,7 +95,8 @@
\item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
exists) is run in the same way as the site default settings. Note
that the variable @{setting ISABELLE_HOME_USER} has already been set
- before --- usually to @{verbatim "~/.isabelle"}.
+ before --- usually to something like @{verbatim
+ "$HOME/.isabelle/IsabelleXXXX"}.
Thus individual users may override the site-wide defaults. See also
file @{"file" "$ISABELLE_HOME/etc/user-settings.sample"} in the
@@ -156,11 +157,12 @@
\item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
counterpart of @{setting ISABELLE_HOME}. The default value is
- @{verbatim "~/.isabelle"}, under rare circumstances this may be
- changed in the global setting file. Typically, the @{setting
- ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
- some extend. In particular, site-wide defaults may be overridden by
- a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
+ relative to @{verbatim "$HOME/.isabelle"}, under rare circumstances
+ this may be changed in the global setting file. Typically, the
+ @{setting ISABELLE_HOME_USER} directory mimics @{setting
+ ISABELLE_HOME} to some extend. In particular, site-wide defaults may
+ be overridden by a private @{verbatim
+ "$ISABELLE_HOME_USER/etc/settings"}.
\item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
set to a symbolic identifier for the underlying hardware and
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/System/Thy/Presentation.thy Sat Nov 06 10:01:00 2010 -0700
@@ -88,10 +88,11 @@
\end{ttbox}
and then change into the @{"file" "~~/src/FOL"} directory and run
- @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle} @{tool
- make}~@{verbatim all}. The presentation output will appear in
- @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
- @{verbatim "~/.isabelle/browser_info/FOL"}. Note that option
+ @{verbatim isabelle} @{tool make}, or even @{verbatim isabelle}
+ @{tool make}~@{verbatim all}. The presentation output will appear
+ in @{verbatim "ISABELLE_BROWSER_INFO/FOL"}, which usually refers to
+ something like @{verbatim
+ "~/.isabelle/IsabelleXXXX/browser_info/FOL"}. Note that option
@{verbatim "-v true"} will make the internal runs of @{tool usedir}
more explicit about such details.
@@ -768,7 +769,7 @@
This enables users to inspect {\LaTeX} runs in further detail, e.g.\
like this:
\begin{ttbox}
- cd ~/.isabelle/browser_info/HOL/Test/document
+ cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
isabelle latex -o pdf
\end{ttbox}
*}
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/System/Thy/document/Basics.tex
--- a/doc-src/System/Thy/document/Basics.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/System/Thy/document/Basics.tex Sat Nov 06 10:01:00 2010 -0700
@@ -114,7 +114,7 @@
\item The file \verb|$ISABELLE_HOME_USER/etc/settings| (if it
exists) is run in the same way as the site default settings. Note
that the variable \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} has already been set
- before --- usually to \verb|~/.isabelle|.
+ before --- usually to something like \verb|$HOME/.isabelle/IsabelleXXXX|.
Thus individual users may override the site-wide defaults. See also
file \hyperlink{file.$ISABELLE-HOME/etc/user-settings.sample}{\mbox{\isa{\isatt{{\isachardollar}ISABELLE{\isacharunderscore}HOME{\isacharslash}etc{\isacharslash}user{\isacharminus}settings{\isachardot}sample}}}} in the
@@ -175,10 +175,10 @@
\item[\indexdef{}{setting}{ISABELLE\_HOME\_USER}\hypertarget{setting.ISABELLE-HOME-USER}{\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}}}] is the user-specific
counterpart of \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. The default value is
- \verb|~/.isabelle|, under rare circumstances this may be
- changed in the global setting file. Typically, the \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to
- some extend. In particular, site-wide defaults may be overridden by
- a private \verb|$ISABELLE_HOME_USER/etc/settings|.
+ relative to \verb|$HOME/.isabelle|, under rare circumstances
+ this may be changed in the global setting file. Typically, the
+ \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME{\isacharunderscore}USER}}}} directory mimics \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}} to some extend. In particular, site-wide defaults may
+ be overridden by a private \verb|$ISABELLE_HOME_USER/etc/settings|.
\item[\indexdef{}{setting}{ISABELLE\_PLATFORM}\hypertarget{setting.ISABELLE-PLATFORM}{\hyperlink{setting.ISABELLE-PLATFORM}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PLATFORM}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}}] is automatically
set to a symbolic identifier for the underlying hardware and
diff -r adb22dbb5242 -r 6354e21e61fa doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/System/Thy/document/Presentation.tex Sat Nov 06 10:01:00 2010 -0700
@@ -104,9 +104,10 @@
\end{ttbox}
and then change into the \hyperlink{file.~~/src/FOL}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL}}}} directory and run
- \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|. The presentation output will appear in
- \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
- \verb|~/.isabelle/browser_info/FOL|. Note that option
+ \verb|isabelle| \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}, or even \verb|isabelle|
+ \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}~\verb|all|. The presentation output will appear
+ in \verb|ISABELLE_BROWSER_INFO/FOL|, which usually refers to
+ something like \verb|~/.isabelle/IsabelleXXXX/browser_info/FOL|. Note that option
\verb|-v true| will make the internal runs of \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
more explicit about such details.
@@ -776,7 +777,7 @@
This enables users to inspect {\LaTeX} runs in further detail, e.g.\
like this:
\begin{ttbox}
- cd ~/.isabelle/browser_info/HOL/Test/document
+ cd ~/.isabelle/IsabelleXXXX/browser_info/HOL/Test/document
isabelle latex -o pdf
\end{ttbox}%
\end{isamarkuptext}%
diff -r adb22dbb5242 -r 6354e21e61fa etc/isar-keywords.el
--- a/etc/isar-keywords.el Fri Nov 05 15:15:28 2010 -0700
+++ b/etc/isar-keywords.el Sat Nov 06 10:01:00 2010 -0700
@@ -129,7 +129,6 @@
"locale"
"method_setup"
"moreover"
- "new_domain"
"next"
"nitpick"
"nitpick_params"
@@ -311,6 +310,7 @@
"shows"
"structure"
"unchecked"
+ "unsafe"
"uses"
"where"))
@@ -478,7 +478,6 @@
"local_setup"
"locale"
"method_setup"
- "new_domain"
"nitpick_params"
"no_notation"
"no_syntax"
diff -r adb22dbb5242 -r 6354e21e61fa etc/settings
--- a/etc/settings Fri Nov 05 15:15:28 2010 -0700
+++ b/etc/settings Sat Nov 06 10:01:00 2010 -0700
@@ -103,7 +103,7 @@
###
# The place for user configuration, heap files, etc.
-ISABELLE_HOME_USER=~/.isabelle
+ISABELLE_HOME_USER="$HOME/.isabelle/$ISABELLE_IDENTIFIER"
# Where to look for isabelle tools (multiple dirs separated by ':').
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
@@ -112,10 +112,10 @@
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"
+ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER"
+ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
# Site settings check -- just to make it a little bit harder to copy this file verbatim!
diff -r adb22dbb5242 -r 6354e21e61fa lib/scripts/feeder
--- a/lib/scripts/feeder Fri Nov 05 15:15:28 2010 -0700
+++ b/lib/scripts/feeder Sat Nov 06 10:01:00 2010 -0700
@@ -16,7 +16,7 @@
echo "Usage: $PRG [OPTIONS]"
echo
echo " Options are:"
- echo " -h TEXT head text"
+ echo " -h TEXT head text (encoded as utf8)"
echo " -p emit my pid"
echo " -q do not pipe stdin"
echo " -t TEXT tail text"
diff -r adb22dbb5242 -r 6354e21e61fa lib/scripts/feeder.pl
--- a/lib/scripts/feeder.pl Fri Nov 05 15:15:28 2010 -0700
+++ b/lib/scripts/feeder.pl Sat Nov 06 10:01:00 2010 -0700
@@ -24,7 +24,11 @@
$emitpid && (print $$, "\n");
-$head && (print "$head", "\n");
+if ($head) {
+ utf8::encode($head);
+ $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
+ print $head, "\n";
+}
if (!$quit) {
while () {
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Bali/Eval.thy Sat Nov 06 10:01:00 2010 -0700
@@ -745,7 +745,7 @@
*)
ML {*
-bind_thm ("eval_induct_", rearrange_prems
+bind_thm ("eval_induct", rearrange_prems
[0,1,2,8,4,30,31,27,15,16,
17,18,19,20,21,3,5,25,26,23,6,
7,11,9,13,14,12,22,10,28,
@@ -753,11 +753,6 @@
*}
-lemmas eval_induct = eval_induct_ [split_format and and and and and and and and
- and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and
- and and
- s2 (* Fin *) and and s2 (* NewC *)]
-
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
inductive_cases halloc_elim_cases:
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Boogie/Examples/Boogie_Dijkstra.certs
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.certs Sat Nov 06 10:01:00 2010 -0700
@@ -1,4 +1,4 @@
-a959f1dced399224414912ad7379705a61749faa 6889 0
+6752602a8162146a4b4b0b817f42d730f1852d5d 6889 0
#2 := false
decl f11 :: (-> S5 S2 S1)
decl ?v1!7 :: (-> S2 S2)
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Boogie/Examples/Boogie_Max.certs
--- a/src/HOL/Boogie/Examples/Boogie_Max.certs Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Boogie/Examples/Boogie_Max.certs Sat Nov 06 10:01:00 2010 -0700
@@ -1,4 +1,4 @@
-16ee32e23503be38842c16c90807e66120a960ee 2224 0
+dea36391893064c022de7bc923e15ef446cb4303 2224 0
#2 := false
#8 := 0::int
decl f5 :: (-> int int)
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Boogie/Examples/VCC_Max.certs
--- a/src/HOL/Boogie/Examples/VCC_Max.certs Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Boogie/Examples/VCC_Max.certs Sat Nov 06 10:01:00 2010 -0700
@@ -1,4 +1,4 @@
-5815fb85125ba62bb3b4a150604c8978e5a08a22 7862 0
+9e8f6c5e5fd53eee967069dced75f48858a605e7 7862 0
#2 := false
decl f111 :: (-> S4 S5 int)
decl f67 :: (-> S5 int S3 S5)
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sat Nov 06 10:01:00 2010 -0700
@@ -138,7 +138,7 @@
else if member (op =) [Lt, Le, Eq] c then Thm.dest_arg
else if member (op =) [Gt, Ge] c then Thm.dest_arg1
else if c = NEq then (Thm.dest_arg o Thm.dest_arg)
- else sys_error "decomp_mpinf: Impossible case!!") fm
+ else raise Fail "decomp_mpinf: Impossible case!!") fm
val [mi_th, pi_th, nmi_th, npi_th, ld_th] =
if c = Nox then map (instantiate' [] [SOME fm])
[minf_P, pinf_P, nmi_P, npi_P, ld_P]
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Groups.thy
--- a/src/HOL/Groups.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Groups.thy Sat Nov 06 10:01:00 2010 -0700
@@ -284,6 +284,7 @@
finally show ?thesis .
qed
+
lemmas equals_zero_I = minus_unique (* legacy name *)
lemma minus_zero [simp]: "- 0 = 0"
@@ -305,6 +306,20 @@
finally show ?thesis .
qed
+subclass cancel_semigroup_add
+proof
+ fix a b c :: 'a
+ assume "a + b = a + c"
+ then have "- a + a + b = - a + a + c"
+ unfolding add_assoc by simp
+ then show "b = c" by simp
+next
+ fix a b c :: 'a
+ assume "b + a = c + a"
+ then have "b + a + - a = c + a + - a" by simp
+ then show "b = c" unfolding add_assoc by simp
+qed
+
lemma minus_add_cancel: "- a + (a + b) = b"
by (simp add: add_assoc [symmetric])
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Imperative_HOL/Array.thy Sat Nov 06 10:01:00 2010 -0700
@@ -134,9 +134,13 @@
by (auto simp add: update_def set_set_swap list_update_swap)
lemma get_alloc:
- "get (snd (alloc ls' h)) (fst (alloc ls h)) = ls'"
+ "get (snd (alloc xs h)) (fst (alloc ys h)) = xs"
by (simp add: Let_def split_def alloc_def)
+lemma length_alloc:
+ "length (snd (alloc (xs :: 'a::heap list) h)) (fst (alloc (ys :: 'a list) h)) = List.length xs"
+ by (simp add: Array.length_def get_alloc)
+
lemma set:
"set (fst (alloc ls h))
new_ls (snd (alloc ls h))
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Imperative_HOL/Overview.thy Sat Nov 06 10:01:00 2010 -0700
@@ -31,7 +31,7 @@
realisation has changed since, due to both extensions and
refinements. Therefore this overview wants to present the framework
\qt{as it is} by now. It focusses on the user-view, less on matters
- of constructions. For details study of the theory sources is
+ of construction. For details study of the theory sources is
encouraged.
*}
@@ -41,7 +41,8 @@
text {*
Heaps (@{type heap}) can be populated by values of class @{class
heap}; HOL's default types are already instantiated to class @{class
- heap}.
+ heap}. Class @{class heap} is a subclass of @{class countable}; see
+ theory @{text Countable} for ways to instantiate types as @{class countable}.
The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
following specification:
@@ -100,7 +101,7 @@
provides a simple relational calculus. Primitive rules are @{text
crelI} and @{text crelE}, rules appropriate for reasoning about
- imperative operation are available in the @{text crel_intros} and
+ imperative operations are available in the @{text crel_intros} and
@{text crel_elims} fact collections.
Often non-failure of imperative computations does not depend
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/IsaMakefile Sat Nov 06 10:01:00 2010 -0700
@@ -172,6 +172,7 @@
Sum_Type.thy \
Tools/abel_cancel.ML \
Tools/arith_data.ML \
+ Tools/async_manager.ML \
Tools/cnf_funcs.ML \
Tools/Datatype/datatype_abs_proofs.ML \
Tools/Datatype/datatype_aux.ML \
@@ -277,7 +278,6 @@
$(SRC)/Provers/Arith/cancel_numerals.ML \
$(SRC)/Provers/Arith/combine_numerals.ML \
$(SRC)/Provers/Arith/extract_common_term.ML \
- Tools/async_manager.ML \
Tools/ATP/atp_problem.ML \
Tools/ATP/atp_proof.ML \
Tools/ATP/atp_systems.ML \
@@ -431,7 +431,7 @@
Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \
Library/Preorder.thy Library/Product_Vector.thy \
Library/Product_ord.thy Library/Product_plus.thy \
- Library/Quickcheck_Types.thy Library/Quicksort.thy \
+ Library/Quickcheck_Types.thy \
Library/Quotient_List.thy Library/Quotient_Option.thy \
Library/Quotient_Product.thy Library/Quotient_Sum.thy \
Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
@@ -1023,13 +1023,14 @@
ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy \
ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \
- ex/Quickcheck_Lattice_Examples.thy ex/ROOT.ML ex/Recdefs.thy \
- ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
- ex/SAT_Examples.thy ex/SVC_Oracle.thy ex/Serbian.thy ex/Sqrt.thy \
- ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \
- ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \
- ex/While_Combinator_Example.thy ex/document/root.bib \
- ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
+ ex/Quickcheck_Lattice_Examples.thy ex/Quicksort.thy ex/ROOT.ML \
+ ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
+ ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
+ ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \
+ ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
+ ex/Unification.thy ex/While_Combinator_Example.thy \
+ ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
+ ex/svc_test.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Library/Eval_Witness.thy Sat Nov 06 10:01:00 2010 -0700
@@ -63,7 +63,7 @@
fun dest_exs 0 t = t
| dest_exs n (Const (@{const_name Ex}, _) $ Abs (v,T,b)) =
Abs (v, check_type T, dest_exs (n - 1) b)
- | dest_exs _ _ = sys_error "dest_exs";
+ | dest_exs _ _ = raise Fail "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
if Code_Runtime.dynamic_value_strict (Eval_Method.get, Eval_Method.put, "Eval_Method.put") thy NONE (K I) t ws
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Library/Library.thy Sat Nov 06 10:01:00 2010 -0700
@@ -45,7 +45,6 @@
Polynomial
Preorder
Product_Vector
- Quicksort
Quotient_List
Quotient_Option
Quotient_Product
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Library/Multiset.thy Sat Nov 06 10:01:00 2010 -0700
@@ -901,30 +901,27 @@
next
fix l
assume "l \ set ?rhs"
- have *: "\x P. P (f x) \ f l = f x \ P (f l) \ f l = f x" by auto
- have **: "\x. f l = f x \ f x = f l" by auto
+ let ?pivot = "f (xs ! (length xs div 2))"
+ have *: "\x. f l = f x \ f x = f l" by auto
have "[x \ sort_key f xs . f x = f l] = [x \ xs. f x = f l]"
unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same)
- with ** have [simp]: "[x \ sort_key f xs . f l = f x] = [x \ xs. f l = f x]" by simp
- let ?pivot = "f (xs ! (length xs div 2))"
+ with * have **: "[x \ sort_key f xs . f l = f x] = [x \ xs. f l = f x]" by simp
+ have "\x P. P (f x) ?pivot \ f l = f x \ P (f l) ?pivot \ f l = f x" by auto
+ then have "\P. [x \ sort_key f xs . P (f x) ?pivot \ f l = f x] =
+ [x \ sort_key f xs. P (f l) ?pivot \ f l = f x]" by simp
+ note *** = this [of "op <"] this [of "op >"] this [of "op ="]
show "[x \ ?rhs. f l = f x] = [x \ ?lhs. f l = f x]"
proof (cases "f l" ?pivot rule: linorder_cases)
case less then moreover have "f l \ ?pivot" and "\ f l > ?pivot" by auto
ultimately show ?thesis
- apply (auto simp add: filter_sort [symmetric])
- apply (subst *) apply simp
- apply (subst *) apply simp
- done
+ by (simp add: filter_sort [symmetric] ** ***)
next
case equal then show ?thesis
- by (auto simp add: ** less_le)
+ by (simp add: * less_le)
next
case greater then moreover have "f l \ ?pivot" and "\ f l < ?pivot" by auto
ultimately show ?thesis
- apply (auto simp add: filter_sort [symmetric])
- apply (subst *) apply simp
- apply (subst *) apply simp
- done
+ by (simp add: filter_sort [symmetric] ** ***)
qed
qed
@@ -934,8 +931,48 @@
@ sort [x\xs. x > xs ! (length xs div 2)]" (is "sort ?lhs = ?rhs")
using sort_key_by_quicksort [of "\x. x", symmetric] by simp
+text {* A stable parametrized quicksort *}
+
+definition part :: "('b \ 'a) \ 'a \ 'b list \ 'b list \ 'b list \ 'b list" where
+ "part f pivot xs = ([x \ xs. f x < pivot], [x \ xs. f x = pivot], [x \ xs. pivot < f x])"
+
+lemma part_code [code]:
+ "part f pivot [] = ([], [], [])"
+ "part f pivot (x # xs) = (let (lts, eqs, gts) = part f pivot xs; x' = f x in
+ if x' < pivot then (x # lts, eqs, gts)
+ else if x' > pivot then (lts, eqs, x # gts)
+ else (lts, x # eqs, gts))"
+ by (auto simp add: part_def Let_def split_def)
+
+lemma sort_key_by_quicksort_code [code]:
+ "sort_key f xs = (case xs of [] \ []
+ | [x] \ xs
+ | [x, y] \ (if f x \ f y then xs else [y, x])
+ | _ \ (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
+ in sort_key f lts @ eqs @ sort_key f gts))"
+proof (cases xs)
+ case Nil then show ?thesis by simp
+next
+ case (Cons _ ys) note hyps = Cons show ?thesis proof (cases ys)
+ case Nil with hyps show ?thesis by simp
+ next
+ case (Cons _ zs) note hyps = hyps Cons show ?thesis proof (cases zs)
+ case Nil with hyps show ?thesis by auto
+ next
+ case Cons
+ from sort_key_by_quicksort [of f xs]
+ have "sort_key f xs = (let (lts, eqs, gts) = part f (f (xs ! (length xs div 2))) xs
+ in sort_key f lts @ eqs @ sort_key f gts)"
+ by (simp only: split_def Let_def part_def fst_conv snd_conv)
+ with hyps Cons show ?thesis by (simp only: list.cases)
+ qed
+ qed
+qed
+
end
+hide_const (open) part
+
lemma multiset_of_remdups_le: "multiset_of (remdups xs) \ multiset_of xs"
by (induct xs) (auto intro: order_trans)
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy Fri Nov 05 15:15:28 2010 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(* Author: Tobias Nipkow
- Copyright 1994 TU Muenchen
-*)
-
-header {* Quicksort *}
-
-theory Quicksort
-imports Main Multiset
-begin
-
-context linorder
-begin
-
-fun quicksort :: "'a list \ 'a list" where
- "quicksort [] = []"
-| "quicksort (x#xs) = quicksort [y\xs. \ x\y] @ [x] @ quicksort [y\xs. x\y]"
-
-lemma [code]:
- "quicksort [] = []"
- "quicksort (x#xs) = quicksort [y\xs. yxs. x\y]"
- by (simp_all add: not_le)
-
-lemma quicksort_permutes [simp]:
- "multiset_of (quicksort xs) = multiset_of xs"
- by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
-
-lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
- by (simp add: set_count_greater_0)
-
-lemma sorted_quicksort: "sorted (quicksort xs)"
- by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
-
-theorem quicksort_sort [code_unfold]:
- "sort = quicksort"
- by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
-
-end
-
-end
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Library/State_Monad.thy Sat Nov 06 10:01:00 2010 -0700
@@ -2,7 +2,7 @@
Author: Florian Haftmann, TU Muenchen
*)
-header {* Combinator syntax for generic, open state monads (single threaded monads) *}
+header {* Combinator syntax for generic, open state monads (single-threaded monads) *}
theory State_Monad
imports Main Monad_Syntax
@@ -11,19 +11,18 @@
subsection {* Motivation *}
text {*
- The logic HOL has no notion of constructor classes, so
- it is not possible to model monads the Haskell way
- in full genericity in Isabelle/HOL.
+ The logic HOL has no notion of constructor classes, so it is not
+ possible to model monads the Haskell way in full genericity in
+ Isabelle/HOL.
- However, this theory provides substantial support for
- a very common class of monads: \emph{state monads}
- (or \emph{single-threaded monads}, since a state
- is transformed single-threaded).
+ However, this theory provides substantial support for a very common
+ class of monads: \emph{state monads} (or \emph{single-threaded
+ monads}, since a state is transformed single-threadedly).
To enter from the Haskell world,
- \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm}
- makes a good motivating start. Here we just sketch briefly
- how those monads enter the game of Isabelle/HOL.
+ \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} makes
+ a good motivating start. Here we just sketch briefly how those
+ monads enter the game of Isabelle/HOL.
*}
subsection {* State transformations and combinators *}
@@ -32,64 +31,66 @@
We classify functions operating on states into two categories:
\begin{description}
- \item[transformations]
- with type signature @{text "\ \ \'"},
+
+ \item[transformations] with type signature @{text "\ \ \'"},
transforming a state.
- \item[``yielding'' transformations]
- with type signature @{text "\ \ \ \ \'"},
- ``yielding'' a side result while transforming a state.
- \item[queries]
- with type signature @{text "\ \ \"},
- computing a result dependent on a state.
+
+ \item[``yielding'' transformations] with type signature @{text "\
+ \ \ \ \'"}, ``yielding'' a side result while transforming a
+ state.
+
+ \item[queries] with type signature @{text "\ \ \"}, computing a
+ result dependent on a state.
+
\end{description}
- By convention we write @{text "\"} for types representing states
- and @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"}
- for types representing side results. Type changes due
- to transformations are not excluded in our scenario.
+ By convention we write @{text "\"} for types representing states and
+ @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} for types
+ representing side results. Type changes due to transformations are
+ not excluded in our scenario.
- We aim to assert that values of any state type @{text "\"}
- are used in a single-threaded way: after application
- of a transformation on a value of type @{text "\"}, the
- former value should not be used again. To achieve this,
- we use a set of monad combinators:
+ We aim to assert that values of any state type @{text "\"} are used
+ in a single-threaded way: after application of a transformation on a
+ value of type @{text "\"}, the former value should not be used
+ again. To achieve this, we use a set of monad combinators:
*}
notation fcomp (infixl "\>" 60)
notation scomp (infixl "\\" 60)
-abbreviation (input)
- "return \ Pair"
-
text {*
- Given two transformations @{term f} and @{term g}, they
- may be directly composed using the @{term "op \>"} combinator,
- forming a forward composition: @{prop "(f \> g) s = f (g s)"}.
+ Given two transformations @{term f} and @{term g}, they may be
+ directly composed using the @{term "op \>"} combinator, forming a
+ forward composition: @{prop "(f \> g) s = f (g s)"}.
After any yielding transformation, we bind the side result
- immediately using a lambda abstraction. This
- is the purpose of the @{term "op \\"} combinator:
- @{prop "(f \\ (\x. g)) s = (let (x, s') = f s in g s')"}.
+ immediately using a lambda abstraction. This is the purpose of the
+ @{term "op \\"} combinator: @{prop "(f \\ (\x. g)) s = (let (x, s')
+ = f s in g s')"}.
For queries, the existing @{term "Let"} is appropriate.
- Naturally, a computation may yield a side result by pairing
- it to the state from the left; we introduce the
- suggestive abbreviation @{term return} for this purpose.
+ Naturally, a computation may yield a side result by pairing it to
+ the state from the left; we introduce the suggestive abbreviation
+ @{term return} for this purpose.
- The most crucial distinction to Haskell is that we do
- not need to introduce distinguished type constructors
- for different kinds of state. This has two consequences:
+ The most crucial distinction to Haskell is that we do not need to
+ introduce distinguished type constructors for different kinds of
+ state. This has two consequences:
+
\begin{itemize}
- \item The monad model does not state anything about
- the kind of state; the model for the state is
- completely orthogonal and may be
- specified completely independently.
- \item There is no distinguished type constructor
- encapsulating away the state transformation, i.e.~transformations
- may be applied directly without using any lifting
- or providing and dropping units (``open monad'').
+
+ \item The monad model does not state anything about the kind of
+ state; the model for the state is completely orthogonal and may
+ be specified completely independently.
+
+ \item There is no distinguished type constructor encapsulating
+ away the state transformation, i.e.~transformations may be
+ applied directly without using any lifting or providing and
+ dropping units (``open monad'').
+
\item The type of states may change due to a transformation.
+
\end{itemize}
*}
@@ -97,8 +98,8 @@
subsection {* Monad laws *}
text {*
- The common monadic laws hold and may also be used
- as normalization rules for monadic expressions:
+ The common monadic laws hold and may also be used as normalization
+ rules for monadic expressions:
*}
lemmas monad_simp = Pair_scomp scomp_Pair id_fcomp fcomp_id
@@ -145,7 +146,7 @@
"_sdo_block (_sdo_final e)" => "e"
text {*
- For an example, see HOL/Extraction/Higman.thy.
+ For an example, see @{text "HOL/Proofs/Extraction/Higman.thy"}.
*}
end
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/List.thy
--- a/src/HOL/List.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/List.thy Sat Nov 06 10:01:00 2010 -0700
@@ -1298,6 +1298,15 @@
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
by (induct xs) auto
+lemma concat_eq_concat_iff: "\(x, y) \ set (zip xs ys). length x = length y ==> length xs = length ys ==> (concat xs = concat ys) = (xs = ys)"
+proof (induct xs arbitrary: ys)
+ case (Cons x xs ys)
+ thus ?case by (cases ys) auto
+qed (auto)
+
+lemma concat_injective: "concat xs = concat ys ==> length xs = length ys ==> \(x, y) \ set (zip xs ys). length x = length y ==> xs = ys"
+by (simp add: concat_eq_concat_iff)
+
subsubsection {* @{text nth} *}
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Matrix/Compute_Oracle/compute.ML
--- a/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Sat Nov 06 10:01:00 2010 -0700
@@ -115,7 +115,7 @@
fun type_of (Free (_, ty)) = ty
| type_of (Const (_, ty)) = ty
| type_of (Var (_, ty)) = ty
- | type_of _ = sys_error "infer_types: type_of error"
+ | type_of _ = raise Fail "infer_types: type_of error"
in
fun infer_types naming encoding =
let
@@ -132,7 +132,7 @@
val (adom, arange) =
case aty of
Type ("fun", [dom, range]) => (dom, range)
- | _ => sys_error "infer_types: function type expected"
+ | _ => raise Fail "infer_types: function type expected"
val (b, bty) = infer_types level bounds (SOME adom) b
in
(a $ b, arange)
@@ -143,7 +143,8 @@
in
(Abs (naming level, dom, m), ty)
end
- | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction"
+ | infer_types _ _ NONE (AbstractMachine.Abs m) =
+ raise Fail "infer_types: cannot infer type of abstraction"
fun infer ty term =
let
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Nov 06 10:01:00 2010 -0700
@@ -349,17 +349,17 @@
#> Config.put Sledgehammer.measure_run_time true)
val params as {full_types, relevance_thresholds, max_relevant, ...} =
Sledgehammer_Isar.default_params ctxt
- [("timeout", Int.toString timeout ^ " s")]
+ [("timeout", Int.toString timeout)]
val default_max_relevant =
Sledgehammer.default_max_relevant_for_prover thy prover_name
- val irrelevant_consts =
- Sledgehammer.irrelevant_consts_for_prover prover_name
+ val is_built_in_const =
+ Sledgehammer.is_built_in_const_for_prover ctxt prover_name
val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name
val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val facts =
Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
- (the_default default_max_relevant max_relevant) irrelevant_consts
+ (the_default default_max_relevant max_relevant) is_built_in_const
relevance_fudge relevance_override chained_ths hyp_ts concl_t
val problem =
{state = st', goal = goal, subgoal = i,
@@ -369,10 +369,11 @@
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({outcome, message, used_facts, run_time_in_msecs = SOME time_prover, ...}
+ val ({outcome, message, used_facts, run_time_in_msecs, ...}
: Sledgehammer.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time
(prover params (K ""))) problem
+ val time_prover = run_time_in_msecs |> the_default ~1
in
case outcome of
NONE => (message, SH_OK (time_isa, time_prover, used_facts))
@@ -446,7 +447,7 @@
|> Option.map (fst o read_int o explode)
|> the_default 5
val params = Sledgehammer_Isar.default_params ctxt
- [("provers", prover_name), ("timeout", Int.toString timeout ^ " s")]
+ [("provers", prover_name), ("timeout", Int.toString timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts params 1
(Sledgehammer_Util.subgoal_count st)
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sat Nov 06 10:01:00 2010 -0700
@@ -111,8 +111,8 @@
|> the_default default_prover
val default_max_relevant =
Sledgehammer.default_max_relevant_for_prover thy prover
- val irrelevant_consts =
- Sledgehammer.irrelevant_consts_for_prover prover
+ val is_built_in_const =
+ Sledgehammer.is_built_in_const_for_prover ctxt default_prover
val relevance_fudge =
extract_relevance_fudge args
(Sledgehammer.relevance_fudge_for_prover prover)
@@ -124,9 +124,8 @@
val facts =
Sledgehammer_Filter.relevant_facts ctxt full_types
relevance_thresholds
- (the_default default_max_relevant max_relevant)
- irrelevant_consts relevance_fudge relevance_override facts hyp_ts
- concl_t
+ (the_default default_max_relevant max_relevant) is_built_in_const
+ relevance_fudge relevance_override facts hyp_ts concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
List.concat proofs |> sort_distinct string_ord
diff -r adb22dbb5242 -r 6354e21e61fa src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Nov 05 15:15:28 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Sat Nov 06 10:01:00 2010 -0700
@@ -13,9 +13,307 @@
(* To be moved elsewhere *)
(* ------------------------------------------------------------------------- *)
+lemma linear_scaleR: "linear (%(x :: 'n::euclidean_space). scaleR c x)"
+ by (metis linear_conv_bounded_linear scaleR.bounded_linear_right)
+
+lemma injective_scaleR:
+assumes "(c :: real) ~= 0"
+shows "inj (%(x :: 'n::euclidean_space). scaleR c x)"
+by (metis assms datatype_injI injI real_vector.scale_cancel_left)
+
+lemma linear_add_cmul:
+fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
+assumes "linear f"
+shows "f(a *\<^sub>R x + b *\<^sub>R y) = a *\<^sub>R f x + b *\<^sub>R f y"
+using linear_add[of f] linear_cmul[of f] assms by (simp)
+
+lemma mem_convex_2:
+ assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v=1"
+ shows "(u *\<^sub>R x + v *\<^sub>R y) : S"
+ using assms convex_def[of S] by auto
+
+lemma mem_convex_alt:
+ assumes "convex S" "x : S" "y : S" "u>=0" "v>=0" "u+v>0"
+ shows "((u/(u+v)) *\<^sub>R x + (v/(u+v)) *\<^sub>R y) : S"
+apply (subst mem_convex_2)
+using assms apply (auto simp add: algebra_simps zero_le_divide_iff)
+using add_divide_distrib[of u v "u+v"] by auto
+
+lemma card_ge1: assumes "d ~= {}" "finite d" shows "card d >= 1"
+by (metis Suc_eq_plus1 assms(1) assms(2) card_eq_0_iff fact_ge_one_nat fact_num_eq_if_nat one_le_mult_iff plus_nat.add_0)
+
+lemma inj_on_image_mem_iff: "inj_on f B ==> (A <= B) ==> (f a : f`A) ==> (a : B) ==> (a : A)"
+by (blast dest: inj_onD)
+
+lemma independent_injective_on_span_image:
+ assumes iS: "independent (S::(_::euclidean_space) set)"
+ and lf: "linear f" and fi: "inj_on f (span S)"
+ shows "independent (f ` S)"
+proof-
+ {fix a assume a: "a : S" "f a : span (f ` S - {f a})"
+ have eq: "f ` S - {f a} = f ` (S - {a})" using fi a span_inc
+ by (auto simp add: inj_on_def)
+ from a have "f a : f ` span (S -{a})"
+ unfolding eq span_linear_image[OF lf, of "S - {a}"] by blast
+ moreover have "span (S -{a}) <= span S" using span_mono[of "S-{a}" S] by auto
+ ultimately have "a : span (S -{a})" using fi a span_inc by (auto simp add: inj_on_def)
+ with a(1) iS have False by (simp add: dependent_def) }
+ then show ?thesis unfolding dependent_def by blast
+qed
+
+lemma dim_image_eq:
+fixes f :: "'n::euclidean_space => 'm::euclidean_space"
+assumes lf: "linear f" and fi: "inj_on f (span S)"
+shows "dim (f ` S) = dim (S:: ('n::euclidean_space) set)"
+proof-
+obtain B where B_def: "B<=S & independent B & S <= span B & card B = dim S"
+ using basis_exists[of S] by auto
+hence "span S = span B" using span_mono[of B S] span_mono[of S "span B"] span_span[of B] by auto
+hence "independent (f ` B)" using independent_injective_on_span_image[of B f] B_def assms by auto
+moreover have "card (f ` B) = card B" using assms card_image[of f B] subset_inj_on[of f "span S" B]
+ B_def span_inc by auto
+moreover have "(f ` B) <= (f ` S)" using B_def by auto
+ultimately have "dim (f ` S) >= dim S"
+ using independent_card_le_dim[of "f ` B" "f ` S"] B_def by auto
+from this show ?thesis using dim_image_le[of f S] assms by auto
+qed
+
+lemma linear_injective_on_subspace_0:
+fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
+assumes lf: "linear f" and "subspace S"
+ shows "inj_on f S <-> (!x : S. f x = 0 --> x = 0)"
+proof-
+ have "inj_on f S <-> (!x : S. !y : S. f x = f y --> x = y)" by (simp add: inj_on_def)
+ also have "... <-> (!x : S. !y : S. f x - f y = 0 --> x - y = 0)" by simp
+ also have "... <-> (!x : S. !y : S. f (x - y) = 0 --> x - y = 0)"
+ by (simp add: linear_sub[OF lf])
+ also have "... <-> (! x : S. f x = 0 --> x = 0)"
+ using `subspace S` subspace_def[of S] subspace_sub[of S] by auto
+ finally show ?thesis .
+qed
+
+lemma subspace_Inter: "(!s : f. subspace s) ==> subspace (Inter f)"
+ unfolding subspace_def by auto
+
+lemma span_eq[simp]: "(span s = s) <-> subspace s"
+proof-
+ { fix f assume "f <= subspace"
+ hence "subspace (Inter f)" using subspace_Inter[of f] unfolding subset_eq mem_def by auto }
+ thus ?thesis using hull_eq[unfolded mem_def, of subspace s] span_def by auto
+qed
+
+lemma basis_inj_on: "d \ {.. inj_on (basis :: nat => 'n::euclidean_space) d"
+ by(auto simp add: inj_on_def euclidean_eq[where 'a='n])
+
+lemma finite_substdbasis: "finite {basis i ::'n::euclidean_space |i. i : (d:: nat set)}" (is "finite ?S")
+proof-
+ have eq: "?S = basis ` d" by blast
+ show ?thesis unfolding eq apply(rule finite_subset[OF _ range_basis_finite]) by auto
+qed
+
+lemma card_substdbasis: assumes "d \ {..{..R basis i) d = (x::'a::euclidean_space)
+ <-> (!i f i = x$$i) & (i ~: d --> x $$ i = 0))"
+proof- have *:"\x a b P. x * (if P then a else b) = (if P then x*a else x*b)" by auto
+ have **:"finite d" apply(rule finite_subset[OF assms]) by fastsimp
+ have ***:"\i. (setsum (%i. f i *\<^sub>R ((basis i)::'a)) d) $$ i = (\x\d. if x = i then f x else 0)"
+ unfolding euclidean_component.setsum euclidean_scaleR basis_component *
+ apply(rule setsum_cong2) using assms by auto
+ show ?thesis unfolding euclidean_eq[where 'a='a] *** setsum_delta[OF **] using assms by auto
+qed
+
+lemma independent_substdbasis: assumes "d\{..R x"
+ hence "y : cball 0 e" using cball_def dist_norm[of 0 y] assms by auto
+ moreover have "x = (norm x/e) *\<^sub>R y" using y_def assms by simp
+ moreover hence "x = (norm x/e) *\<^sub>R y" by auto
+ ultimately have "x : span (cball 0 e)"
+ using span_mul[of y "cball 0 e" "norm x/e"] span_inc[of "cball 0 e"] by auto
+} hence "span (cball 0 e) = (UNIV :: ('n::euclidean_space) set)" by auto
+from this show ?thesis using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp add: dim_UNIV)
+qed
+
+lemma indep_card_eq_dim_span:
+fixes B :: "('n::euclidean_space) set"
+assumes "independent B"
+shows "finite B & card B = dim (span B)"
+ using assms basis_card_eq_dim[of B "span B"] span_inc by auto
+
+lemma setsum_not_0: "setsum f A ~= 0 ==> EX a:A. f a ~= 0"
+ apply(rule ccontr) by auto
+
+lemma translate_inj_on:
+fixes A :: "('n::euclidean_space) set"
+shows "inj_on (%x. a+x) A" unfolding inj_on_def by auto
+
+lemma translation_assoc:
+ fixes a b :: "'a::ab_group_add"
+ shows "(\x. b+x) ` ((\x. a+x) ` S) = (\x. (a+b)+x) ` S" by auto
+
+lemma translation_invert:
+ fixes a :: "'a::ab_group_add"
+ assumes "(\x. a+x) ` A = (\x. a+x) ` B"
+ shows "A=B"
+proof-
+ have "(%x. -a+x) ` ((%x. a+x) ` A) = (%x. -a+x) ` ((%x. a+x) ` B)" using assms by auto
+ from this show ?thesis using translation_assoc[of "-a" a A] translation_assoc[of "-a" a B] by auto
+qed
+
+lemma translation_galois:
+ fixes a :: "'a::ab_group_add"
+ shows "T=((\x. a+x) ` S) <-> S=((\x. (-a)+x) ` T)"
+ using translation_assoc[of "-a" a S] apply auto
+ using translation_assoc[of a "-a" T] by auto
+
+lemma translation_inverse_subset:
+ assumes "((%x. -a+x) ` V) <= (S :: 'n::ab_group_add set)"
+ shows "V <= ((%x. a+x) ` S)"
+proof-
+{ fix x assume "x:V" hence "x-a : S" using assms by auto
+ hence "x : {a + v |v. v : S}" apply auto apply (rule exI[of _ "x-a"]) apply simp done
+ hence "x : ((%x. a+x) ` S)" by auto }
+ from this show ?thesis by auto
+qed
+
lemma basis_0[simp]:"(basis i::'a::euclidean_space) = 0 \ i\DIM('a)"
using norm_basis[of i, where 'a='a] unfolding norm_eq_zero[where 'a='a,THEN sym] by auto
+lemma basis_to_basis_subspace_isomorphism:
+ assumes s: "subspace (S:: ('n::euclidean_space) set)"
+ and t: "subspace (T :: ('m::euclidean_space) set)"
+ and d: "dim S = dim T"
+ and B: "B <= S" "independent B" "S <= span B" "card B = dim S"
+ and C: "C <= T" "independent C" "T <= span C" "card C = dim T"
+ shows "EX f. linear f & f ` B = C & f ` S = T & inj_on f S"
+proof-
+(* Proof is a modified copy of the proof of similar lemma subspace_isomorphism
+*)
+ from B independent_bound have fB: "finite B" by blast
+ from C independent_bound have fC: "finite C" by blast
+ from B(4) C(4) card_le_inj[of B C] d obtain f where
+ f: "f ` B \ C" "inj_on f B" using `finite B` `finite C` by auto
+ from linear_independent_extend[OF B(2)] obtain g where
+ g: "linear g" "\x\ B. g x = f x" by blast
+ from inj_on_iff_eq_card[OF fB, of f] f(2)
+ have "card (f ` B) = card B" by simp
+ with B(4) C(4) have ceq: "card (f ` B) = card C" using d
+ by simp
+ have "g ` B = f ` B" using g(2)
+ by (auto simp add: image_iff)
+ also have "\ = C" using card_subset_eq[OF fC f(1) ceq] .
+ finally have gBC: "g ` B = C" .
+ have gi: "inj_on g B" using f(2) g(2)
+ by (auto simp add: inj_on_def)
+ note g0 = linear_indep_image_lemma[OF g(1) fB, unfolded gBC, OF C(2) gi]
+ {fix x y assume x: "x \ S" and y: "y \ S" and gxy:"g x = g y"
+ from B(3) x y have x': "x \ span B" and y': "y \ span B" by blast+
+ from gxy have th0: "g (x - y) = 0" by (simp add: linear_sub[OF g(1)])
+ have th1: "x - y \ span B" using x' y' by (metis span_sub)
+ have "x=y" using g0[OF th1 th0] by simp }
+ then have giS: "inj_on g S"
+ unfolding inj_on_def by blast
+ from span_subspace[OF B(1,3) s]
+ have "g ` S = span (g ` B)" by (simp add: span_linear_image[OF g(1)])
+ also have "\ = span C" unfolding gBC ..
+ also have "\ = T" using span_subspace[OF C(1,3) t] .
+ finally have gS: "g ` S = T" .
+ from g(1) gS giS gBC show ?thesis by blast
+qed
+
+lemma closure_linear_image:
+fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
+assumes "linear f"
+shows "f ` (closure S) <= closure (f ` S)"
+using image_closure_subset[of S f "closure (f ` S)"] assms linear_conv_bounded_linear[of f]
+linear_continuous_on[of f "closure S"] closed_closure[of "f ` S"] closure_subset[of "f ` S"] by auto
+
+lemma closure_injective_linear_image:
+fixes f :: "('n::euclidean_space) => ('n::euclidean_space)"
+assumes "linear f" "inj f"
+shows "f ` (closure S) = closure (f ` S)"
+proof-
+obtain f' where f'_def: "linear f' & f o f' = id & f' o f = id"
+ using assms linear_injective_isomorphism[of f] isomorphism_expand by auto
+hence "f' ` closure (f ` S) <= closure (S)"
+ using closure_linear_image[of f' "f ` S"] image_compose[of f' f] by auto
+hence "f ` f' ` closure (f ` S) <= f ` closure (S)" by auto
+hence "closure (f ` S) <= f ` closure (S)" using image_compose[of f f' "closure (f ` S)"] f'_def by auto
+from this show ?thesis using closure_linear_image[of f S] assms by auto
+qed
+
+lemma closure_direct_sum:
+fixes S :: "('n::euclidean_space) set"
+fixes T :: "('m::euclidean_space) set"
+shows "closure (S <*> T) = closure S <*> closure T"
+proof-
+{ fix x assume "x : closure S <*> closure T"
+ from this obtain xs xt where xst_def: "xs : closure S & xt : closure T & (xs,xt) = x" by auto
+ { fix ee assume ee_def: "(ee :: real) > 0"
+ def e == "ee/2" hence e_def: "(e :: real)>0 & 2*e=ee" using ee_def by auto
+ from this obtain e where e_def: "(e :: real)>0 & 2*e=ee" by auto
+ obtain ys where ys_def: "ys : S & (dist ys xs < e)"
+ using e_def xst_def closure_approachable[of xs S] by auto
+ obtain yt where yt_def: "yt : T & (dist yt xt < e)"
+ using e_def xst_def closure_approachable[of xt T] by auto
+ from ys_def yt_def have "dist (ys,yt) (xs,xt) < sqrt (2*e^2)"
+ unfolding dist_norm apply (auto simp add: norm_Pair)
+ using mult_strict_mono'[of "norm (ys - xs)" e "norm (ys - xs)" e] e_def
+ mult_strict_mono'[of "norm (yt - xt)" e "norm (yt - xt)" e] by (simp add: power2_eq_square)
+ hence "((ys,yt) : S <*> T) & (dist (ys,yt) x < 2*e)"
+ using e_def sqrt_add_le_add_sqrt[of "e^2" "e^2"] xst_def ys_def yt_def by auto
+ hence "EX y: S <*> T. dist y x < ee" using e_def by auto
+ } hence "x : closure (S <*> T)" using closure_approachable[of x "S <*> T"] by auto
+}
+hence "closure (S <*> T) >= closure S <*> closure T" by auto
+moreover have "closed (closure S <*> closure T)" using closed_Times by auto
+ultimately show ?thesis using closure_minimal[of "S <*> T" "closure S <*> closure T"]
+ closure_subset[of S] closure_subset[of T] by auto
+qed
+
+lemma closure_scaleR:
+fixes S :: "('n::euclidean_space) set"
+shows "(op *\<^sub>R c) ` (closure S) = closure ((op *\<^sub>R c) ` S)"
+proof-
+{ assume "c ~= 0" hence ?thesis using closure_injective_linear_image[of "(op *\<^sub>R c)" S]
+ linear_scaleR injective_scaleR by auto
+}
+moreover
+{ assume zero: "c=0 & S ~= {}"
+ hence "closure S ~= {}" using closure_subset by auto
+ hence "op *\<^sub>R c ` (closure S) = {0}" using zero by auto
+ moreover have "op *\<^sub>R 0 ` S = {0}" using zero by auto
+ ultimately have ?thesis using zero by auto
+}
+moreover
+{ assume "S={}" hence ?thesis by auto }
+ultimately show ?thesis by blast
+qed
+
+lemma fst_linear: "linear fst" unfolding linear_def by (simp add: algebra_simps)
+
+lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps)
+
+lemma fst_snd_linear: "linear (%z. fst z + snd z)" unfolding linear_def by (simp add: algebra_simps)
+
lemma scaleR_2:
fixes x :: "'a::real_vector"
shows "scaleR 2 x = x + x"
@@ -272,6 +570,30 @@
apply(rule_tac x=u in exI) by(auto intro!: exI)
qed
+lemma mem_affine:
+ assumes "affine S" "x : S" "y : S" "u+v=1"
+ shows "(u *\<^sub>R x + v *\<^sub>R y) : S"
+ using assms affine_def[of S] by auto
+
+lemma mem_affine_3:
+ assumes "affine S" "x : S" "y : S" "z : S" "u+v+w=1"
+ shows "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : S"
+proof-
+have "(u *\<^sub>R x + v *\<^sub>R y + w *\<^sub>R z) : affine hull {x, y, z}"
+ using affine_hull_3[of x y z] assms by auto
+moreover have " affine hull {x, y, z} <= affine hull S"
+ using hull_mono[of "{x, y, z}" "S"] assms by auto
+moreover have "affine hull S = S"
+ using assms affine_hull_eq[of S] by auto
+ultimately show ?thesis by auto
+qed
+
+lemma mem_affine_3_minus:
+ assumes "affine S" "x : S" "y : S" "z : S"
+ shows "x + v *\<^sub>R (y-z) : S"
+using mem_affine_3[of S x y z 1 v "-v"] assms by (simp add: algebra_simps)
+
+
subsection {* Some relations between affine hull and subspaces. *}
lemma affine_hull_insert_subset_span:
@@ -318,6 +640,163 @@
shows "affine hull s = {a + v | v. v \ span {x - a | x. x \ s - {a}}}"
using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
+subsection{* Parallel Affine Sets *}
+
+definition affine_parallel :: "'a::real_vector set => 'a::real_vector set => bool"
+where "affine_parallel S T = (? a. T = ((%x. a + x) ` S))"
+
+lemma affine_parallel_expl_aux:
+ fixes S T :: "'a::real_vector set"
+ assumes "!x. (x : S <-> (a+x) : T)"
+ shows "T = ((%x. a + x) ` S)"
+proof-
+{ fix x assume "x : T" hence "(-a)+x : S" using assms by auto
+ hence " x : ((%x. a + x) ` S)" using imageI[of "-a+x" S "(%x. a+x)"] by auto}
+moreover have "T >= ((%x. a + x) ` S)" using assms by auto
+ultimately show ?thesis by auto
+qed
+
+lemma affine_parallel_expl:
+ "affine_parallel S T = (? a. !x. (x : S <-> (a+x) : T))"
+ unfolding affine_parallel_def using affine_parallel_expl_aux[of S _ T] by auto
+
+lemma affine_parallel_reflex: "affine_parallel S S" unfolding affine_parallel_def apply (rule exI[of _ "0"]) by auto
+
+lemma affine_parallel_commut:
+assumes "affine_parallel A B" shows "affine_parallel B A"
+proof-
+from assms obtain a where "B=((%x. a + x) ` A)" unfolding affine_parallel_def by auto
+from this show ?thesis using translation_galois[of B a A] unfolding affine_parallel_def by auto
+qed
+
+lemma affine_parallel_assoc:
+assumes "affine_parallel A B" "affine_parallel B C"
+shows "affine_parallel A C"
+proof-
+from assms obtain ab where "B=((%x. ab + x) ` A)" unfolding affine_parallel_def by auto
+moreover
+from assms obtain bc where "C=((%x. bc + x) ` B)" unfolding affine_parallel_def by auto
+ultimately show ?thesis using translation_assoc[of bc ab A] unfolding affine_parallel_def by auto
+qed
+
+lemma affine_translation_aux:
+ fixes a :: "'a::real_vector"
+ assumes "affine ((%x. a + x) ` S)" shows "affine S"
+proof-
+{ fix x y u v
+ assume xy: "x : S" "y : S" "(u :: real)+v=1"
+ hence "(a+x):((%x. a + x) ` S)" "(a+y):((%x. a + x) ` S)" by auto
+ hence h1: "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) : ((%x. a + x) ` S)" using xy assms unfolding affine_def by auto
+ have "u *\<^sub>R (a+x) + v *\<^sub>R (a+y) = (u+v) *\<^sub>R a + (u *\<^sub>R x + v *\<^sub>R y)" by (simp add:algebra_simps)
+ also have "...= a + (u *\<^sub>R x + v *\<^sub>R y)" using `u+v=1` by auto
+ ultimately have "a + (u *\<^sub>R x + v *\<^sub>R y) : ((%x. a + x) ` S)" using h1 by auto
+ hence "u *\<^sub>R x + v *\<^sub>R y : S" by auto
+} from this show ?thesis unfolding affine_def by auto
+qed
+
+lemma affine_translation:
+ fixes a :: "'a::real_vector"
+ shows "affine S <-> affine ((%x. a + x) ` S)"
+proof-
+have "affine S ==> affine ((%x. a + x) ` S)" using affine_translation_aux[of "-a" "((%x. a + x) ` S)"] using translation_assoc[of "-a" a S] by auto
+from this show ?thesis using affine_translation_aux by auto
+qed
+
+lemma parallel_is_affine:
+fixes S T :: "'a::real_vector set"
+assumes "affine S" "affine_parallel S T"
+shows "affine T"
+proof-
+ from assms obtain a where "T=((%x. a + x) ` S)" unfolding affine_parallel_def by auto
+ from this show ?thesis using affine_translation assms by auto
+qed
+
+lemma subspace_imp_affine:
+ fixes s :: "(_::euclidean_space) set" shows "subspace s \ affine s"
+ unfolding subspace_def affine_def by auto
+
+subsection{* Subspace Parallel to an Affine Set *}
+
+lemma subspace_affine:
+ fixes S :: "('n::euclidean_space) set"
+ shows "subspace S <-> (affine S & 0 : S)"
+proof-
+have h0: "subspace S ==> (affine S & 0 : S)" using subspace_imp_affine[of S] subspace_0 by auto
+{ assume assm: "affine S & 0 : S"
+ { fix c :: real
+ fix x assume x_def: "x : S"
+ have "c *\<^sub>R x = (1-c) *\<^sub>R 0 + c *\<^sub>R x" by auto
+ moreover have "(1-c) *\<^sub>R 0 + c *\<^sub>R x : S" using affine_alt[of S] assm x_def by auto
+ ultimately have "c *\<^sub>R x : S" by auto
+ } hence h1: "!c. !x : S. c *\<^sub>R x : S" by auto
+ { fix x y assume xy_def: "x : S" "y : S"
+ def u == "(1 :: real)/2"
+ have "(1/2) *\<^sub>R (x+y) = (1/2) *\<^sub>R (x+y)" by auto
+ moreover have "(1/2) *\<^sub>R (x+y)=(1/2) *\<^sub>R x + (1-(1/2)) *\<^sub>R y" by (simp add: algebra_simps)
+ moreover have "(1-u) *\<^sub>R x + u *\<^sub>R y : S" using affine_alt[of S] assm xy_def by auto
+ ultimately have "(1/2) *\<^sub>R (x+y) : S" using u_def by auto
+ moreover have "(x+y) = 2 *\<^sub>R ((1/2) *\<^sub>R (x+y))" by auto
+ ultimately have "(x+y) : S" using h1[rule_format, of "(1/2) *\<^sub>R (x+y)" "2"] by auto
+ } hence "!x : S. !y : S. (x+y) : S" by auto
+ hence "subspace S" using h1 assm unfolding subspace_def by auto
+} from this show ?thesis using h0 by metis
+qed
+
+lemma affine_diffs_subspace:
+ fixes S :: "('n::euclidean_space) set"
+ assumes "affine S" "a : S"
+ shows "subspace ((%x. (-a)+x) ` S)"
+proof-
+have "affine ((%x. (-a)+x) ` S)" using affine_translation assms by auto
+moreover have "0 : ((%x. (-a)+x) ` S)" using assms exI[of "(%x. x:S & -a+x=0)" a] by auto
+ultimately show ?thesis using subspace_affine by auto
+qed
+
+lemma parallel_subspace_explicit:
+fixes a :: "'n::euclidean_space"
+assumes "affine S" "a : S"
+assumes "L == {y. ? x : S. (-a)+x=y}"
+shows "subspace L & affine_parallel S L"
+proof-
+have par: "affine_parallel S L" unfolding affine_parallel_def using assms by auto
+hence "affine L" using assms parallel_is_affine by auto
+moreover have "0 : L" using assms apply auto using exI[of "(%x. x:S & -a+x=0)" a] by auto
+ultimately show ?thesis using subspace_affine par by auto
+qed
+
+lemma parallel_subspace_aux:
+fixes A B :: "('n::euclidean_space) set"
+assumes "subspace A" "subspace B" "affine_parallel A B"
+shows "A>=B"
+proof-
+from assms obtain a where a_def: "!x. (x : A <-> (a+x) : B)" using affine_parallel_expl[of A B] by auto
+hence "-a : A" using assms subspace_0[of B] by auto
+hence "a : A" using assms subspace_neg[of A "-a"] by auto
+from this show ?thesis using assms a_def unfolding subspace_def by auto
+qed
+
+lemma parallel_subspace:
+fixes A B :: "('n::euclidean_space) set"
+assumes "subspace A" "subspace B" "affine_parallel A B"
+shows "A=B"
+proof-
+have "A>=B" using assms parallel_subspace_aux by auto
+moreover have "A<=B" using assms parallel_subspace_aux[of B A] affine_parallel_commut by auto
+ultimately show ?thesis by auto
+qed
+
+lemma affine_parallel_subspace:
+fixes S :: "('n::euclidean_space) set"
+assumes "affine S" "S ~= {}"
+shows "?!L. subspace L & affine_parallel S L"
+proof-
+have ex: "? L. subspace L & affine_parallel S L" using assms parallel_subspace_explicit by auto
+{ fix L1 L2 assume ass: "subspace L1 & affine_parallel S L1" "subspace L2 & affine_parallel S L2"
+ hence "affine_parallel L1 L2" using affine_parallel_commut[of S L1] affine_parallel_assoc[of L1 S L2] by auto
+ hence "L1=L2" using ass parallel_subspace by auto
+} from this show ?thesis using ex by auto
+qed
+
subsection {* Cones. *}
definition
@@ -343,6 +822,116 @@
apply(rule hull_eq[unfolded mem_def])
using cone_Inter unfolding subset_eq by (auto simp add: mem_def)
+lemma mem_cone:
+ assumes "cone S" "x : S" "c>=0"
+ shows "c *\<^sub>R x : S"
+ using assms cone_def[of S] by auto
+
+lemma cone_contains_0:
+fixes S :: "('m::euclidean_space) set"
+assumes "cone S"
+shows "(S ~= {}) <-> (0 : S)"
+proof-
+{ assume "S ~= {}" from this obtain a where "a:S" by auto
+ hence "0 : S" using assms mem_cone[of S a 0] by auto
+} from this show ?thesis by auto
+qed
+
+lemma cone_0:
+shows "cone {(0 :: 'm::euclidean_space)}"
+unfolding cone_def by auto
+
+lemma cone_Union[intro]: "(!s:f. cone s) --> (cone (Union f))"
+ unfolding cone_def by blast
+
+lemma cone_iff:
+fixes S :: "('m::euclidean_space) set"
+assumes "S ~= {}"
+shows "cone S <-> 0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
+proof-
+{ assume "cone S"
+ { fix c assume "(c :: real)>0"
+ { fix x assume "x : S" hence "x : (op *\<^sub>R c) ` S" unfolding image_def
+ using `cone S` `c>0` mem_cone[of S x "1/c"]
+ exI[of "(%t. t:S & x = c *\<^sub>R t)" "(1 / c) *\<^sub>R x"] by auto
+ }
+ moreover
+ { fix x assume "x : (op *\<^sub>R c) ` S"
+ (*from this obtain t where "t:S & x = c *\<^sub>R t" by auto*)
+ hence "x:S" using `cone S` `c>0` unfolding cone_def image_def `c>0` by auto
+ }
+ ultimately have "((op *\<^sub>R c) ` S) = S" by auto
+ } hence "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)" using `cone S` cone_contains_0[of S] assms by auto
+}
+moreover
+{ assume a: "0:S & (!c. c>0 --> ((op *\<^sub>R c) ` S) = S)"
+ { fix x assume "x:S"
+ fix c1 assume "(c1 :: real)>=0"
+ hence "(c1=0) | (c1>0)" by auto
+ hence "c1 *\<^sub>R x : S" using a `x:S` by auto
+ }
+ hence "cone S" unfolding cone_def by auto
+} ultimately show ?thesis by blast
+qed
+
+lemma cone_hull_empty:
+"cone hull {} = {}"
+by (metis cone_empty cone_hull_eq)
+
+lemma cone_hull_empty_iff:
+fixes S :: "('m::euclidean_space) set"
+shows "(S = {}) <-> (cone hull S = {})"
+by (metis bot_least cone_hull_empty hull_subset xtrans(5))
+
+lemma cone_hull_contains_0:
+fixes S :: "('m::euclidean_space) set"
+shows "(S ~= {}) <-> (0 : cone hull S)"
+using cone_cone_hull[of S] cone_contains_0[of "cone hull S"] cone_hull_empty_iff[of S] by auto
+
+lemma mem_cone_hull:
+ assumes "x : S" "c>=0"
+ shows "c *\<^sub>R x : cone hull S"
+by (metis assms cone_cone_hull hull_inc mem_cone mem_def)
+
+lemma cone_hull_expl:
+fixes S :: "('m::euclidean_space) set"
+shows "cone hull S = {c *\<^sub>R x | c x. c>=0 & x : S}" (is "?lhs = ?rhs")
+proof-
+{ fix x assume "x : ?rhs"
+ from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
+ fix c assume c_def: "(c :: real)>=0"
+ hence "c *\<^sub>R x = (c*cx) *\<^sub>R xx" using x_def by (simp add: algebra_simps)
+ moreover have "(c*cx) >= 0" using c_def x_def using mult_nonneg_nonneg by auto
+ ultimately have "c *\<^sub>R x : ?rhs" using x_def by auto
+} hence "cone ?rhs" unfolding cone_def by auto
+ hence "?rhs : cone" unfolding mem_def by auto
+{ fix x assume "x : S" hence "1 *\<^sub>R x : ?rhs" apply auto apply(rule_tac x="1" in exI) by auto
+ hence "x : ?rhs" by auto
+} hence "S <= ?rhs" by auto
+hence "?lhs <= ?rhs" using `?rhs : cone` hull_minimal[of S "?rhs" "cone"] by auto
+moreover
+{ fix x assume "x : ?rhs"
+ from this obtain cx xx where x_def: "x= cx *\<^sub>R xx & (cx :: real)>=0 & xx : S" by auto
+ hence "xx : cone hull S" using hull_subset[of S] by auto
+ hence "x : ?lhs" using x_def cone_cone_hull[of S] cone_def[of "cone hull S"] by auto
+} ultimately show ?thesis by auto
+qed
+
+lemma cone_closure:
+fixes S :: "('m::euclidean_space) set"
+assumes "cone S"
+shows "cone (closure S)"
+proof-
+{ assume "S = {}" hence ?thesis by auto }
+moreover
+{ assume "S ~= {}" hence "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto
+ hence "0:(closure S) & (!c. c>0 --> op *\<^sub>R c ` (closure S) = (closure S))"
+ using closure_subset by (auto simp add: closure_scaleR)
+ hence ?thesis using cone_iff[of "closure S"] by auto
+}
+ultimately show ?thesis by blast
+qed
+
subsection {* Affine dependence and consequential theorems (from Lars Schewe). *}
definition
@@ -514,6 +1103,28 @@
shows "finite s \ bounded(convex hull s)"
using bounded_convex_hull finite_imp_bounded by auto
+subsection {* Convex hull is "preserved" by a linear function. *}
+
+lemma convex_hull_linear_image:
+ assumes "bounded_linear f"
+ shows "f ` (convex hull s) = convex hull (f ` s)"
+ apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
+ apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
+ apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
+proof-
+ interpret f: bounded_linear f by fact
+ show "convex {x. f x \ convex hull f ` s}"
+ unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
+ interpret f: bounded_linear f by fact
+ show "convex {x. x \ f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s]
+ unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
+qed auto
+
+lemma in_convex_hull_linear_image:
+ assumes "bounded_linear f" "x \ convex hull s"
+ shows "(f x) \ convex hull (f ` s)"
+using convex_hull_linear_image[OF assms(1)] assms(2) by auto
+
subsection {* Stepping theorems for convex hulls of finite sets. *}
lemma convex_hull_empty[simp]: "convex hull {} = {}"
@@ -775,10 +1386,6 @@
text {* TODO: Generalize linear algebra concepts defined in @{text
Euclidean_Space.thy} so that we can generalize these lemmas. *}
-lemma subspace_imp_affine:
- fixes s :: "(_::euclidean_space) set" shows "subspace s \ affine s"
- unfolding subspace_def affine_def by auto
-
lemma affine_imp_convex: "affine s \ convex s"
unfolding affine_def convex_def by auto
@@ -952,6 +1559,979 @@
thus "x \ convex hull p" using hull_mono[OF `s\p`] by auto
qed
+
+subsection {* Some Properties of Affine Dependent Sets *}
+
+lemma affine_independent_empty: "~(affine_dependent {})"
+ by (simp add: affine_dependent_def)
+
+lemma affine_independent_sing:
+fixes a :: "'n::euclidean_space"
+shows "~(affine_dependent {a})"
+ by (simp add: affine_dependent_def)
+
+lemma affine_hull_translation:
+"affine hull ((%x. a + x) ` S) = (%x. a + x) ` (affine hull S)"
+proof-
+have "affine ((%x. a + x) ` (affine hull S))" using affine_translation affine_affine_hull by auto
+moreover have "(%x. a + x) ` S <= (%x. a + x) ` (affine hull S)" using hull_subset[of S] by auto
+ultimately have h1: "affine hull ((%x. a + x) ` S) <= (%x. a + x) ` (affine hull S)" by (metis hull_minimal mem_def)
+have "affine((%x. -a + x) ` (affine hull ((%x. a + x) ` S)))" using affine_translation affine_affine_hull by auto
+moreover have "(%x. -a + x) ` (%x. a + x) ` S <= (%x. -a + x) ` (affine hull ((%x. a + x) ` S))" using hull_subset[of "(%x. a + x) ` S"] by auto
+moreover have "S=(%x. -a + x) ` (%x. a + x) ` S" using translation_assoc[of "-a" a] by auto
+ultimately have "(%x. -a + x) ` (affine hull ((%x. a + x) ` S)) >= (affine hull S)" by (metis hull_minimal mem_def)
+hence "affine hull ((%x. a + x) ` S) >= (%x. a + x) ` (affine hull S)" by auto
+from this show ?thesis using h1 by auto
+qed
+
+lemma affine_dependent_translation:
+ assumes "affine_dependent S"
+ shows "affine_dependent ((%x. a + x) ` S)"
+proof-
+obtain x where x_def: "x : S & x : affine hull (S - {x})" using assms affine_dependent_def by auto
+have "op + a ` (S - {x}) = op + a ` S - {a + x}" by auto
+hence "a+x : affine hull ((%x. a + x) ` S - {a+x})" using affine_hull_translation[of a "S-{x}"] x_def by auto
+moreover have "a+x : (%x. a + x) ` S" using x_def by auto
+ultimately show ?thesis unfolding affine_dependent_def by auto
+qed
+
+lemma affine_dependent_translation_eq:
+ "affine_dependent S <-> affine_dependent ((%x. a + x) ` S)"
+proof-
+{ assume "affine_dependent ((%x. a + x) ` S)"
+ hence "affine_dependent S" using affine_dependent_translation[of "((%x. a + x) ` S)" "-a"] translation_assoc[of "-a" a] by auto
+} from this show ?thesis using affine_dependent_translation by auto
+qed
+
+lemma affine_hull_0_dependent:
+ fixes S :: "('n::euclidean_space) set"
+ assumes "0 : affine hull S"
+ shows "dependent S"
+proof-
+obtain s u where s_u_def: "finite s & s ~= {} & s <= S & setsum u s = 1 & (SUM v:s. u v *\<^sub>R v) = 0" using assms affine_hull_explicit[of S] by auto
+hence "EX v:s. u v ~= 0" using setsum_not_0[of "u" "s"] by auto
+hence "finite s & s <= S & (EX v:s. u v ~= 0 & (SUM v:s. u v *\<^sub>R v) = 0)" using s_u_def by auto
+from this show ?thesis unfolding dependent_explicit[of S] by auto
+qed
+
+lemma affine_dependent_imp_dependent2:
+ fixes S :: "('n::euclidean_space) set"
+ assumes "affine_dependent (insert 0 S)"
+ shows "dependent S"
+proof-
+obtain x where x_def: "x:insert 0 S & x : affine hull (insert 0 S - {x})" using affine_dependent_def[of "(insert 0 S)"] assms by blast
+hence "x : span (insert 0 S - {x})" using affine_hull_subset_span by auto
+moreover have "span (insert 0 S - {x}) = span (S - {x})" using insert_Diff_if[of "0" S "{x}"] span_insert_0[of "S-{x}"] by auto
+ultimately have "x : span (S - {x})" by auto
+hence "(x~=0) ==> dependent S" using x_def dependent_def by auto
+moreover
+{ assume "x=0" hence "0 : affine hull S" using x_def hull_mono[of "S - {0}" S] by auto
+ hence "dependent S" using affine_hull_0_dependent by auto
+} ultimately show ?thesis by auto
+qed
+
+lemma affine_dependent_iff_dependent:
+ fixes S :: "('n::euclidean_space) set"
+ assumes "a ~: S"
+ shows "affine_dependent (insert a S) <-> dependent ((%x. -a + x) ` S)"
+proof-
+have "(op + (- a) ` S)={x - a| x . x : S}" by auto
+from this show ?thesis using affine_dependent_translation_eq[of "(insert a S)" "-a"]
+ affine_dependent_imp_dependent2 assms
+ dependent_imp_affine_dependent[of a S] by auto
+qed
+
+lemma affine_dependent_iff_dependent2:
+ fixes S :: "('n::euclidean_space) set"
+ assumes "a : S"
+ shows "affine_dependent S <-> dependent ((%x. -a + x) ` (S-{a}))"
+proof-
+have "insert a (S - {a})=S" using assms by auto
+from this show ?thesis using assms affine_dependent_iff_dependent[of a "S-{a}"] by auto
+qed
+
+lemma affine_hull_insert_span_gen:
+ fixes a :: "_::euclidean_space"
+ shows "affine hull (insert a s) = (%x. a+x) ` span ((%x. -a+x) ` s)"
+proof-
+have h1: "{x - a |x. x : s}=((%x. -a+x) ` s)" by auto
+{ assume "a ~: s" hence ?thesis using affine_hull_insert_span[of a s] h1 by auto}
+moreover
+{ assume a1: "a : s"
+ have "EX x. x:s & -a+x=0" apply (rule exI[of _ a]) using a1 by auto
+ hence "insert 0 ((%x. -a+x) ` (s - {a}))=(%x. -a+x) ` s" by auto
+ hence "span ((%x. -a+x) ` (s - {a}))=span ((%x. -a+x) ` s)"
+ using span_insert_0[of "op + (- a) ` (s - {a})"] by auto
+ moreover have "{x - a |x. x : (s - {a})}=((%x. -a+x) ` (s - {a}))" by auto
+ moreover have "insert a (s - {a})=(insert a s)" using assms by auto
+ ultimately have ?thesis using assms affine_hull_insert_span[of "a" "s-{a}"] by auto
+}
+ultimately show ?thesis by auto
+qed
+
+lemma affine_hull_span2:
+ fixes a :: "_::euclidean_space"
+ assumes "a : s"
+ shows "affine hull s = (%x. a+x) ` span ((%x. -a+x) ` (s-{a}))"
+ using affine_hull_insert_span_gen[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
+
+lemma affine_hull_span_gen:
+ fixes a :: "_::euclidean_space"
+ assumes "a : affine hull s"
+ shows "affine hull s = (%x. a+x) ` span ((%x. -a+x) ` s)"
+proof-
+have "affine hull (insert a s) = affine hull s" using hull_redundant[of a affine s] assms by auto
+from this show ?thesis using affine_hull_insert_span_gen[of a "s"] by auto
+qed
+
+lemma affine_hull_span_0:
+ assumes "(0 :: _::euclidean_space) : affine hull S"
+ shows "affine hull S = span S"
+using affine_hull_span_gen[of "0" S] assms by auto
+
+
+lemma extend_to_affine_basis:
+fixes S V :: "('n::euclidean_space) set"
+assumes "~(affine_dependent S)" "S <= V" "S~={}"
+shows "? T. ~(affine_dependent T) & S<=T & T<=V & affine hull T = affine hull V"
+proof-
+obtain a where a_def: "a : S" using assms by auto
+hence h0: "independent ((%x. -a + x) ` (S-{a}))" using affine_dependent_iff_dependent2 assms by auto
+from this obtain B
+ where B_def: "(%x. -a+x) ` (S - {a}) <= B & B <= (%x. -a+x) ` V & independent B & (%x. -a+x) ` V <= span B"
+ using maximal_independent_subset_extend[of "(%x. -a+x) ` (S-{a})" "(%x. -a + x) ` V"] assms by blast
+def T == "(%x. a+x) ` (insert 0 B)" hence "T=insert a ((%x. a+x) ` B)" by auto
+hence "affine hull T = (%x. a+x) ` span B" using affine_hull_insert_span_gen[of a "((%x. a+x) ` B)"] translation_assoc[of "-a" a B] by auto
+hence "V <= affine hull T" using B_def assms translation_inverse_subset[of a V "span B"] by auto
+moreover have "T<=V" using T_def B_def a_def assms by auto
+ultimately have "affine hull T = affine hull V"
+ by (metis Int_absorb1 Int_absorb2 Int_commute Int_lower2 assms hull_hull hull_mono)
+moreover have "S<=T" using T_def B_def translation_inverse_subset[of a "S-{a}" B] by auto
+moreover have "~(affine_dependent T)" using T_def affine_dependent_translation_eq[of "insert 0 B"] affine_dependent_imp_dependent2 B_def by auto
+ultimately show ?thesis using `T<=V` by auto
+qed
+
+lemma affine_basis_exists:
+fixes V :: "('n::euclidean_space) set"
+shows "? B. B <= V & ~(affine_dependent B) & affine hull V = affine hull B"
+proof-
+{ assume empt: "V={}" have "? B. B <= V & ~(affine_dependent B) & (affine hull V=affine hull B)" using empt affine_independent_empty by auto
+}
+moreover
+{ assume nonempt: "V~={}" obtain x where "x:V" using nonempt by auto
+ hence "? B. B <= V & ~(affine_dependent B) & (affine hull V=affine hull B)"
+ using affine_dependent_def[of "{x}"] extend_to_affine_basis[of "{x}:: ('n::euclidean_space) set" V] by auto
+}
+ultimately show ?thesis by auto
+qed
+
+subsection {* Affine Dimension of a Set *}
+
+definition "aff_dim V = (SOME d :: int. ? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = d+1))"
+
+lemma aff_dim_basis_exists:
+ fixes V :: "('n::euclidean_space) set"
+ shows "? B. (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)"
+proof-
+obtain B where B_def: "~(affine_dependent B) & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto
+from this show ?thesis unfolding aff_dim_def some_eq_ex[of "%d. ? (B :: ('n::euclidean_space) set). (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = d+1)"] apply auto apply (rule exI[of _ "int (card B)-(1 :: int)"]) apply (rule exI[of _ "B"]) by auto
+qed
+
+lemma affine_hull_nonempty: "(S ~= {}) <-> affine hull S ~= {}"
+proof-
+fix S have "(S = {}) ==> affine hull S = {}"using affine_hull_empty by auto
+moreover have "affine hull S = {} ==> S = {}" unfolding hull_def by auto
+ultimately show "(S ~= {}) <-> affine hull S ~= {}" by blast
+qed
+
+lemma aff_dim_parallel_subspace_aux:
+fixes B :: "('n::euclidean_space) set"
+assumes "~(affine_dependent B)" "a:B"
+shows "finite B & ((card B) - 1 = dim (span ((%x. -a+x) ` (B-{a}))))"
+proof-
+have "independent ((%x. -a + x) ` (B-{a}))" using affine_dependent_iff_dependent2 assms by auto
+hence fin: "dim (span ((%x. -a+x) ` (B-{a}))) = card ((%x. -a + x) ` (B-{a}))" "finite ((%x. -a + x) ` (B - {a}))" using indep_card_eq_dim_span[of "(%x. -a+x) ` (B-{a})"] by auto
+{ assume emp: "(%x. -a + x) ` (B - {a}) = {}"
+ have "B=insert a ((%x. a + x) ` (%x. -a + x) ` (B - {a}))" using translation_assoc[of "a" "-a" "(B - {a})"] assms by auto
+ hence "B={a}" using emp by auto
+ hence ?thesis using assms fin by auto
+}
+moreover
+{ assume "(%x. -a + x) ` (B - {a}) ~= {}"
+ hence "card ((%x. -a + x) ` (B - {a}))>0" using fin by auto
+ moreover have h1: "card ((%x. -a + x) ` (B-{a})) = card (B-{a})"
+ apply (rule card_image) using translate_inj_on by auto
+ ultimately have "card (B-{a})>0" by auto
+ hence "finite(B-{a})" using card_gt_0_iff[of "(B - {a})"] by auto
+ moreover hence "(card (B-{a})= (card B) - 1)" using card_Diff_singleton assms by auto
+ ultimately have ?thesis using fin h1 by auto
+} ultimately show ?thesis by auto
+qed
+
+lemma aff_dim_parallel_subspace:
+fixes V L :: "('n::euclidean_space) set"
+assumes "V ~= {}"
+assumes "subspace L" "affine_parallel (affine hull V) L"
+shows "aff_dim V=int(dim L)"
+proof-
+obtain B where B_def: "affine hull B = affine hull V & ~ affine_dependent B & int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto
+hence "B~={}" using assms B_def affine_hull_nonempty[of V] affine_hull_nonempty[of B] by auto
+from this obtain a where a_def: "a : B" by auto
+def Lb == "span ((%x. -a+x) ` (B-{a}))"
+ moreover have "affine_parallel (affine hull B) Lb"
+ using Lb_def B_def assms affine_hull_span2[of a B] a_def affine_parallel_commut[of "Lb" "(affine hull B)"] unfolding affine_parallel_def by auto
+ moreover have "subspace Lb" using Lb_def subspace_span by auto
+ moreover have "affine hull B ~= {}" using assms B_def affine_hull_nonempty[of V] by auto
+ ultimately have "L=Lb" using assms affine_parallel_subspace[of "affine hull B"] affine_affine_hull[of B] B_def by auto
+ hence "dim L=dim Lb" by auto
+ moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def B_def by auto
+(* hence "card B=dim Lb+1" using `B~={}` card_gt_0_iff[of B] by auto *)
+ ultimately show ?thesis using B_def `B~={}` card_gt_0_iff[of B] by auto
+qed
+
+lemma aff_independent_finite:
+fixes B :: "('n::euclidean_space) set"
+assumes "~(affine_dependent B)"
+shows "finite B"
+proof-
+{ assume "B~={}" from this obtain a where "a:B" by auto
+ hence ?thesis using aff_dim_parallel_subspace_aux assms by auto
+} from this show ?thesis by auto
+qed
+
+lemma independent_finite:
+fixes B :: "('n::euclidean_space) set"
+assumes "independent B"
+shows "finite B"
+using affine_dependent_imp_dependent[of B] aff_independent_finite[of B] assms by auto
+
+lemma subspace_dim_equal:
+assumes "subspace (S :: ('n::euclidean_space) set)" "subspace T" "S <= T" "dim S >= dim T"
+shows "S=T"
+proof-
+obtain B where B_def: "B <= S & independent B & S <= span B & (card B = dim S)" using basis_exists[of S] by auto
+hence "span B <= S" using span_mono[of B S] span_eq[of S] assms by metis
+hence "span B = S" using B_def by auto
+have "dim S = dim T" using assms dim_subset[of S T] by auto
+hence "T <= span B" using card_eq_dim[of B T] B_def independent_finite assms by auto
+from this show ?thesis using assms `span B=S` by auto
+qed
+
+lemma span_substd_basis: assumes "d\{.. x$$i = 0)}"
+ (is "span ?A = ?B")
+proof-
+have "?A <= ?B" by auto
+moreover have s: "subspace ?B" using subspace_substandard[of "%i. i ~: d"] .
+ultimately have "span ?A <= ?B" using span_mono[of "?A" "?B"] span_eq[of "?B"] by blast
+moreover have "card d <= dim (span ?A)" using independent_card_le_dim[of "?A" "span ?A"]
+ independent_substdbasis[OF assms] card_substdbasis[OF assms] span_inc[of "?A"] by auto
+moreover hence "dim ?B <= dim (span ?A)" using dim_substandard[OF assms] by auto
+ultimately show ?thesis using s subspace_dim_equal[of "span ?A" "?B"]
+ subspace_span[of "?A"] by auto
+qed
+
+lemma basis_to_substdbasis_subspace_isomorphism:
+fixes B :: "('a::euclidean_space) set"
+assumes "independent B"
+shows "EX f d. card d = card B & linear f & f ` B = {basis i::'a |i. i : (d :: nat set)} &
+ f ` span B = {x. ALL i x $$ i = (0::real)} & inj_on f (span B) \ d\{.. "{..{.. aff_dim S = -1"
+proof-
+obtain B where "affine hull B = affine hull S & ~ affine_dependent B & int (card B) = aff_dim S + 1" using aff_dim_basis_exists by auto
+moreover hence "S={} <-> B={}" using affine_hull_nonempty[of B] affine_hull_nonempty[of S] by auto
+ultimately show ?thesis using aff_independent_finite[of B] card_gt_0_iff[of B] by auto
+qed
+
+lemma aff_dim_affine_hull:
+fixes S :: "('n::euclidean_space) set"
+shows "aff_dim (affine hull S)=aff_dim S"
+unfolding aff_dim_def using hull_hull[of _ S] by auto
+
+lemma aff_dim_affine_hull2:
+fixes S T :: "('n::euclidean_space) set"
+assumes "affine hull S=affine hull T"
+shows "aff_dim S=aff_dim T" unfolding aff_dim_def using assms by auto
+
+lemma aff_dim_unique:
+fixes B V :: "('n::euclidean_space) set"
+assumes "(affine hull B=affine hull V) & ~(affine_dependent B)"
+shows "of_nat(card B) = aff_dim V+1"
+proof-
+{ assume "B={}" hence "V={}" using affine_hull_nonempty[of V] affine_hull_nonempty[of B] assms by auto
+ hence "aff_dim V = (-1::int)" using aff_dim_empty by auto
+ hence ?thesis using `B={}` by auto
+}
+moreover
+{ assume "B~={}" from this obtain a where a_def: "a:B" by auto
+ def Lb == "span ((%x. -a+x) ` (B-{a}))"
+ have "affine_parallel (affine hull B) Lb"
+ using Lb_def affine_hull_span2[of a B] a_def affine_parallel_commut[of "Lb" "(affine hull B)"]
+ unfolding affine_parallel_def by auto
+ moreover have "subspace Lb" using Lb_def subspace_span by auto
+ ultimately have "aff_dim B=int(dim Lb)" using aff_dim_parallel_subspace[of B Lb] `B~={}` by auto
+ moreover have "(card B) - 1 = dim Lb" "finite B" using Lb_def aff_dim_parallel_subspace_aux a_def assms by auto
+ ultimately have "(of_nat(card B) = aff_dim B+1)" using `B~={}` card_gt_0_iff[of B] by auto
+ hence ?thesis using aff_dim_affine_hull2 assms by auto
+} ultimately show ?thesis by blast
+qed
+
+lemma aff_dim_affine_independent:
+fixes B :: "('n::euclidean_space) set"
+assumes "~(affine_dependent B)"
+shows "of_nat(card B) = aff_dim B+1"
+ using aff_dim_unique[of B B] assms by auto
+
+lemma aff_dim_sing:
+fixes a :: "'n::euclidean_space"
+shows "aff_dim {a}=0"
+ using aff_dim_affine_independent[of "{a}"] affine_independent_sing by auto
+
+lemma aff_dim_inner_basis_exists:
+ fixes V :: "('n::euclidean_space) set"
+ shows "? B. B<=V & (affine hull B=affine hull V) & ~(affine_dependent B) & (of_nat(card B) = aff_dim V+1)"
+proof-
+obtain B where B_def: "~(affine_dependent B) & B<=V & (affine hull B=affine hull V)" using affine_basis_exists[of V] by auto
+moreover hence "of_nat(card B) = aff_dim V+1" using aff_dim_unique by auto
+ultimately show ?thesis by auto
+qed
+
+lemma aff_dim_le_card:
+fixes V :: "('n::euclidean_space) set"
+assumes "finite V"
+shows "aff_dim V <= of_nat(card V) - 1"
+ proof-
+ obtain B where B_def: "B<=V & (of_nat(card B) = aff_dim V+1)" using aff_dim_inner_basis_exists[of V] by auto
+ moreover hence "card B <= card V" using assms card_mono by auto
+ ultimately show ?thesis by auto
+qed
+
+lemma aff_dim_parallel_eq:
+fixes S T :: "('n::euclidean_space) set"
+assumes "affine_parallel (affine hull S) (affine hull T)"
+shows "aff_dim S=aff_dim T"
+proof-
+{ assume "T~={}" "S~={}"
+ from this obtain L where L_def: "subspace L & affine_parallel (affine hull T) L"
+ using affine_parallel_subspace[of "affine hull T"] affine_affine_hull[of T] affine_hull_nonempty by auto
+ hence "aff_dim T = int(dim L)" using aff_dim_parallel_subspace `T~={}` by auto
+ moreover have "subspace L & affine_parallel (affine hull S) L"
+ using L_def affine_parallel_assoc[of "affine hull S" "affine hull T" L] assms by auto
+ moreover hence "aff_dim S = int(dim L)" using aff_dim_parallel_subspace `S~={}` by auto
+ ultimately have ?thesis by auto
+}
+moreover
+{ assume "S={}" hence "S={} & T={}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto
+ hence ?thesis using aff_dim_empty by auto
+}
+moreover
+{ assume "T={}" hence "S={} & T={}" using assms affine_hull_nonempty unfolding affine_parallel_def by auto
+ hence ?thesis using aff_dim_empty by auto
+}
+ultimately show ?thesis by blast
+qed
+
+lemma aff_dim_translation_eq:
+fixes a :: "'n::euclidean_space"
+shows "aff_dim ((%x. a + x) ` S)=aff_dim S"
+proof-
+have "affine_parallel (affine hull S) (affine hull ((%x. a + x) ` S))" unfolding affine_parallel_def apply (rule exI[of _ "a"]) using affine_hull_translation[of a S] by auto
+from this show ?thesis using aff_dim_parallel_eq[of S "(%x. a + x) ` S"] by auto
+qed
+
+lemma aff_dim_affine:
+fixes S L :: "('n::euclidean_space) set"
+assumes "S ~= {}" "affine S"
+assumes "subspace L" "affine_parallel S L"
+shows "aff_dim S=int(dim L)"
+proof-
+have 1: "(affine hull S) = S" using assms affine_hull_eq[of S] by auto
+hence "affine_parallel (affine hull S) L" using assms by (simp add:1)
+from this show ?thesis using assms aff_dim_parallel_subspace[of S L] by blast
+qed
+
+lemma dim_affine_hull:
+fixes S :: "('n::euclidean_space) set"
+shows "dim (affine hull S)=dim S"
+proof-
+have "dim (affine hull S)>=dim S" using dim_subset by auto
+moreover have "dim(span S) >= dim (affine hull S)" using dim_subset affine_hull_subset_span by auto
+moreover have "dim(span S)=dim S" using dim_span by auto
+ultimately show ?thesis by auto
+qed
+
+lemma aff_dim_subspace:
+fixes S :: "('n::euclidean_space) set"
+assumes "S ~= {}" "subspace S"
+shows "aff_dim S=int(dim S)" using aff_dim_affine[of S S] assms subspace_imp_affine[of S] affine_parallel_reflex[of S] by auto
+
+lemma aff_dim_zero:
+fixes S :: "('n::euclidean_space) set"
+assumes "0 : affine hull S"
+shows "aff_dim S=int(dim S)"
+proof-
+have "subspace(affine hull S)" using subspace_affine[of "affine hull S"] affine_affine_hull assms by auto
+hence "aff_dim (affine hull S) =int(dim (affine hull S))" using assms aff_dim_subspace[of "affine hull S"] by auto
+from this show ?thesis using aff_dim_affine_hull[of S] dim_affine_hull[of S] by auto
+qed
+
+lemma aff_dim_univ: "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))"
+ using aff_dim_subspace[of "(UNIV :: ('n::euclidean_space) set)"]
+ dim_UNIV[where 'a="'n::euclidean_space"] by auto
+
+lemma aff_dim_geq:
+ fixes V :: "('n::euclidean_space) set"
+ shows "aff_dim V >= -1"
+proof-
+obtain B where B_def: "affine hull B = affine hull V & ~ affine_dependent B & int (card B) = aff_dim V + 1" using aff_dim_basis_exists by auto
+from this show ?thesis by auto
+qed
+
+lemma independent_card_le_aff_dim:
+ assumes "(B::('n::euclidean_space) set) <= V"
+ assumes "~(affine_dependent B)"
+ shows "int(card B) <= aff_dim V+1"
+proof-
+{ assume "B~={}"
+ from this obtain T where T_def: "~(affine_dependent T) & B<=T & T<=V & affine hull T = affine hull V"
+ using assms extend_to_affine_basis[of B V] by auto
+ hence "of_nat(card T) = aff_dim V+1" using aff_dim_unique by auto
+ hence ?thesis using T_def card_mono[of T B] aff_independent_finite[of T] by auto
+}
+moreover
+{ assume "B={}"
+ moreover have "-1<= aff_dim V" using aff_dim_geq by auto
+ ultimately have ?thesis by auto
+} ultimately show ?thesis by blast
+qed
+
+lemma aff_dim_subset:
+ fixes S T :: "('n::euclidean_space) set"
+ assumes "S <= T"
+ shows "aff_dim S <= aff_dim T"
+proof-
+obtain B where B_def: "~(affine_dependent B) & B<=S & (affine hull B=affine hull S) & of_nat(card B) = aff_dim S+1" using aff_dim_inner_basis_exists[of S] by auto
+moreover hence "int (card B) <= aff_dim T + 1" using assms independent_card_le_aff_dim[of B T] by auto
+ultimately show ?thesis by auto
+qed
+
+lemma aff_dim_subset_univ:
+fixes S :: "('n::euclidean_space) set"
+shows "aff_dim S <= int(DIM('n))"
+proof -
+ have "aff_dim (UNIV :: ('n::euclidean_space) set) = int(DIM('n))" using aff_dim_univ by auto
+ from this show "aff_dim (S:: ('n::euclidean_space) set) <= int(DIM('n))" using assms aff_dim_subset[of S "(UNIV :: ('n::euclidean_space) set)"] subset_UNIV by auto
+qed
+
+lemma affine_dim_equal:
+assumes "affine (S :: ('n::euclidean_space) set)" "affine T" "S ~= {}" "S <= T" "aff_dim S = aff_dim T"
+shows "S=T"
+proof-
+obtain a where "a : S" using assms by auto
+hence "a : T" using assms by auto
+def LS == "{y. ? x : S. (-a)+x=y}"
+hence ls: "subspace LS & affine_parallel S LS" using assms parallel_subspace_explicit[of S a LS] `a : S` by auto
+hence h1: "int(dim LS) = aff_dim S" using assms aff_dim_affine[of S LS] by auto
+have "T ~= {}" using assms by auto
+def LT == "{y. ? x : T. (-a)+x=y}"
+hence lt: "subspace LT & affine_parallel T LT" using assms parallel_subspace_explicit[of T a LT] `a : T` by auto
+hence "int(dim LT) = aff_dim T" using assms aff_dim_affine[of T LT] `T ~= {}` by auto
+hence "dim LS = dim LT" using h1 assms by auto
+moreover have "LS <= LT" using LS_def LT_def assms by auto
+ultimately have "LS=LT" using subspace_dim_equal[of LS LT] ls lt by auto
+moreover have "S = {x. ? y : LS. a+y=x}" using LS_def by auto
+moreover have "T = {x. ? y : LT. a+y=x}" using LT_def by auto
+ultimately show ?thesis by auto
+qed
+
+lemma affine_hull_univ:
+fixes S :: "('n::euclidean_space) set"
+assumes "aff_dim S = int(DIM('n))"
+shows "affine hull S = (UNIV :: ('n::euclidean_space) set)"
+proof-
+have "S ~= {}" using assms aff_dim_empty[of S] by auto
+have h0: "S <= affine hull S" using hull_subset[of S _] by auto
+have h1: "aff_dim (UNIV :: ('n::euclidean_space) set) = aff_dim S" using aff_dim_univ assms by auto
+hence h2: "aff_dim (affine hull S) <= aff_dim (UNIV :: ('n::euclidean_space) set)" using aff_dim_subset_univ[of "affine hull S"] assms h0 by auto
+have h3: "aff_dim S <= aff_dim (affine hull S)" using h0 aff_dim_subset[of S "affine hull S"] assms by auto
+hence h4: "aff_dim (affine hull S) = aff_dim (UNIV :: ('n::euclidean_space) set)" using h0 h1 h2 by auto
+from this show ?thesis using affine_dim_equal[of "affine hull S" "(UNIV :: ('n::euclidean_space) set)"] affine_affine_hull[of S] affine_UNIV assms h4 h0 `S ~= {}` by auto
+qed
+
+lemma aff_dim_convex_hull:
+fixes S :: "('n::euclidean_space) set"
+shows "aff_dim (convex hull S)=aff_dim S"
+ using aff_dim_affine_hull[of S] convex_hull_subset_affine_hull[of S]
+ hull_subset[of S "convex"] aff_dim_subset[of S "convex hull S"]
+ aff_dim_subset[of "convex hull S" "affine hull S"] by auto
+
+lemma aff_dim_cball:
+fixes a :: "'n::euclidean_space"
+assumes "00 & cball x e <= S" using open_contains_cball[of S] assms by auto
+from this have "aff_dim (cball x e) <= aff_dim S" using aff_dim_subset by auto
+from this show ?thesis using aff_dim_cball[of e x] aff_dim_subset_univ[of S] e_def by auto
+qed
+
+lemma low_dim_interior:
+fixes S :: "('n::euclidean_space) set"
+assumes "~(aff_dim S = int (DIM('n)))"
+shows "interior S = {}"
+proof-
+have "aff_dim(interior S) <= aff_dim S"
+ using interior_subset aff_dim_subset[of "interior S" S] by auto
+from this show ?thesis using aff_dim_open[of "interior S"] aff_dim_subset_univ[of S] assms by auto
+qed
+
+subsection{* Relative Interior of a Set *}
+
+definition "rel_interior S = {x. ? T. openin (subtopology euclidean (affine hull S)) T & x : T & T <= S}"
+
+lemma rel_interior: "rel_interior S = {x : S. ? T. open T & x : T & (T Int (affine hull S)) <= S}"
+ unfolding rel_interior_def[of S] openin_open[of "affine hull S"] apply auto
+proof-
+fix x T assume a: "x:S" "open T" "x : T" "(T Int (affine hull S)) <= S"
+hence h1: "x : T Int affine hull S" using hull_inc by auto
+show "EX Tb. (EX Ta. open Ta & Tb = affine hull S Int Ta) & x : Tb & Tb <= S"
+apply (rule_tac x="T Int (affine hull S)" in exI)
+using a h1 by auto
+qed
+
+lemma mem_rel_interior:
+ "x : rel_interior S <-> (? T. open T & x : (T Int S) & (T Int (affine hull S)) <= S)"
+ by (auto simp add: rel_interior)
+
+lemma mem_rel_interior_ball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((ball x e) Int (affine hull S)) <= S)"
+ apply (simp add: rel_interior, safe)
+ apply (force simp add: open_contains_ball)
+ apply (rule_tac x="ball x e" in exI)
+ apply (simp add: open_ball centre_in_ball)
+ done
+
+lemma rel_interior_ball:
+ "rel_interior S = {x : S. ? e. e>0 & ((ball x e) Int (affine hull S)) <= S}"
+ using mem_rel_interior_ball [of _ S] by auto
+
+lemma mem_rel_interior_cball: "x : rel_interior S <-> x : S & (? e. 0 < e & ((cball x e) Int (affine hull S)) <= S)"
+ apply (simp add: rel_interior, safe)
+ apply (force simp add: open_contains_cball)
+ apply (rule_tac x="ball x e" in exI)
+ apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball])
+ apply auto
+ done
+
+lemma rel_interior_cball: "rel_interior S = {x : S. ? e. e>0 & ((cball x e) Int (affine hull S)) <= S}" using mem_rel_interior_cball [of _ S] by auto
+
+lemma rel_interior_empty: "rel_interior {} = {}"
+ by (auto simp add: rel_interior_def)
+
+lemma affine_hull_sing: "affine hull {a :: 'n::euclidean_space} = {a}"
+by (metis affine_hull_eq affine_sing)
+
+lemma rel_interior_sing: "rel_interior {a :: 'n::euclidean_space} = {a}"
+ unfolding rel_interior_ball affine_hull_sing apply auto
+ apply(rule_tac x="1 :: real" in exI) apply simp
+ done
+
+lemma subset_rel_interior:
+fixes S T :: "('n::euclidean_space) set"
+assumes "S<=T" "affine hull S=affine hull T"
+shows "rel_interior S <= rel_interior T"
+ using assms by (auto simp add: rel_interior_def)
+
+lemma rel_interior_subset: "rel_interior S <= S"
+ by (auto simp add: rel_interior_def)
+
+lemma rel_interior_subset_closure: "rel_interior S <= closure S"
+ using rel_interior_subset by (auto simp add: closure_def)
+
+lemma interior_subset_rel_interior: "interior S <= rel_interior S"
+ by (auto simp add: rel_interior interior_def)
+
+lemma interior_rel_interior:
+fixes S :: "('n::euclidean_space) set"
+assumes "aff_dim S = int(DIM('n))"
+shows "rel_interior S = interior S"
+proof -
+have "affine hull S = UNIV" using assms affine_hull_univ[of S] by auto
+from this show ?thesis unfolding rel_interior interior_def by auto
+qed
+
+lemma rel_interior_open:
+fixes S :: "('n::euclidean_space) set"
+assumes "open S"
+shows "rel_interior S = S"
+by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset)
+
+lemma interior_rel_interior_gen:
+fixes S :: "('n::euclidean_space) set"
+shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})"
+by (metis interior_rel_interior low_dim_interior)
+
+lemma rel_interior_univ:
+fixes S :: "('n::euclidean_space) set"
+shows "rel_interior (affine hull S) = affine hull S"
+proof-
+have h1: "rel_interior (affine hull S) <= affine hull S" using rel_interior_subset by auto
+{ fix x assume x_def: "x : affine hull S"
+ obtain e :: real where "e=1" by auto
+ hence "e>0 & ball x e Int affine hull (affine hull S) <= affine hull S" using hull_hull[of _ S] by auto
+ hence "x : rel_interior (affine hull S)" using x_def rel_interior_ball[of "affine hull S"] by auto
+} from this show ?thesis using h1 by auto
+qed
+
+lemma rel_interior_univ2: "rel_interior (UNIV :: ('n::euclidean_space) set) = UNIV"
+by (metis open_UNIV rel_interior_open)
+
+lemma rel_interior_convex_shrink:
+ fixes S :: "('a::euclidean_space) set"
+ assumes "convex S" "c : rel_interior S" "x : S" "0 < e" "e <= 1"
+ shows "x - e *\<^sub>R (x - c) : rel_interior S"
+proof-
+(* Proof is a modified copy of the proof of similar lemma mem_interior_convex_shrink
+*)
+obtain d where "d>0" and d:"ball c d Int affine hull S <= S"
+ using assms(2) unfolding mem_rel_interior_ball by auto
+{ fix y assume as:"dist (x - e *\<^sub>R (x - c)) y < e * d & y : affine hull S"
+ have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
+ have "x : affine hull S" using assms hull_subset[of S] by auto
+ moreover have "1 / e + - ((1 - e) / e) = 1"
+ using `e>0` mult_left.diff[of "1" "(1-e)" "1/e"] by auto
+ ultimately have **: "(1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x : affine hull S"
+ using as affine_affine_hull[of S] mem_affine[of "affine hull S" y x "(1 / e)" "-((1 - e) / e)"] by (simp add: algebra_simps)
+ have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
+ unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule arg_cong[where f=norm]) using `e>0`
+ by(auto simp add:euclidean_eq[where 'a='a] field_simps)
+ also have "... = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:arg_cong[where f=norm] simp add: algebra_simps)
+ also have "... < d" using as[unfolded dist_norm] and `e>0`
+ by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
+ finally have "y : S" apply(subst *)
+apply(rule assms(1)[unfolded convex_alt,rule_format])
+ apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) ** by auto
+} hence "ball (x - e *\<^sub>R (x - c)) (e*d) Int affine hull S <= S" by auto
+moreover have "0 < e*d" using `0R (x - c) : S"
+ using mem_convex[of S x c e] apply (simp add: algebra_simps) using assms by auto
+ultimately show ?thesis
+ using mem_rel_interior_ball[of "x - e *\<^sub>R (x - c)" S] `e>0` by auto
+qed
+
+lemma interior_real_semiline:
+fixes a :: real
+shows "interior {a..} = {a<..}"
+proof-
+{ fix y assume "a0 & cball y e \ {a..}"
+ using mem_interior_cball[of y "{a..}"] by auto
+ moreover hence "y-e : cball y e" by (auto simp add: cball_def dist_norm)
+ ultimately have "a<=y-e" by auto
+ hence "a {}" using assms unfolding set_eq_iff by (auto intro!: exI[of _ "(a + b) / 2"])
+ then show ?thesis
+ using interior_rel_interior_gen[of "{a..b}", symmetric]
+ by (simp split: split_if_asm add: interior_closed_interval)
+qed
+
+lemma rel_interior_real_semiline:
+ fixes a :: real shows "rel_interior {a..} = {a<..}"
+proof-
+ have *: "{a<..} \ {}" unfolding set_eq_iff by (auto intro!: exI[of _ "a + 1"])
+ then show ?thesis using interior_real_semiline
+ interior_rel_interior_gen[of "{a..}"]
+ by (auto split: split_if_asm)
+qed
+
+subsection "Relative open"
+
+definition "rel_open S <-> (rel_interior S) = S"
+
+lemma rel_open: "rel_open S <-> openin (subtopology euclidean (affine hull S)) S"
+ unfolding rel_open_def rel_interior_def apply auto
+ using openin_subopen[of "subtopology euclidean (affine hull S)" S] by auto
+
+lemma opein_rel_interior:
+ "openin (subtopology euclidean (affine hull S)) (rel_interior S)"
+ apply (simp add: rel_interior_def)
+ apply (subst openin_subopen) by blast
+
+lemma affine_rel_open:
+ fixes S :: "('n::euclidean_space) set"
+ assumes "affine S" shows "rel_open S"
+ unfolding rel_open_def using assms rel_interior_univ[of S] affine_hull_eq[of S] by metis
+
+lemma affine_closed:
+ fixes S :: "('n::euclidean_space) set"
+ assumes "affine S" shows "closed S"
+proof-
+{ assume "S ~= {}"
+ from this obtain L where L_def: "subspace L & affine_parallel S L"
+ using assms affine_parallel_subspace[of S] by auto
+ from this obtain "a" where a_def: "S=(op + a ` L)"
+ using affine_parallel_def[of L S] affine_parallel_commut by auto
+ have "closed L" using L_def closed_subspace by auto
+ hence "closed S" using closed_translation a_def by auto
+} from this show ?thesis by auto
+qed
+
+lemma closure_affine_hull:
+ fixes S :: "('n::euclidean_space) set"
+ shows "closure S <= affine hull S"
+proof-
+have "closure S <= closure (affine hull S)" using subset_closure by auto
+moreover have "closure (affine hull S) = affine hull S"
+ using affine_affine_hull affine_closed[of "affine hull S"] closure_eq by auto
+ultimately show ?thesis by auto
+qed
+
+lemma closure_same_affine_hull:
+ fixes S :: "('n::euclidean_space) set"
+ shows "affine hull (closure S) = affine hull S"
+proof-
+have "affine hull (closure S) <= affine hull S"
+ using hull_mono[of "closure S" "affine hull S" "affine"] closure_affine_hull[of S] hull_hull[of "affine" S] by auto
+moreover have "affine hull (closure S) >= affine hull S"
+ using hull_mono[of "S" "closure S" "affine"] closure_subset by auto
+ultimately show ?thesis by auto
+qed
+
+lemma closure_aff_dim:
+ fixes S :: "('n::euclidean_space) set"
+ shows "aff_dim (closure S) = aff_dim S"
+proof-
+have "aff_dim S <= aff_dim (closure S)" using aff_dim_subset closure_subset by auto
+moreover have "aff_dim (closure S) <= aff_dim (affine hull S)"
+ using aff_dim_subset closure_affine_hull by auto
+moreover have "aff_dim (affine hull S) = aff_dim S" using aff_dim_affine_hull by auto
+ultimately show ?thesis by auto
+qed
+
+lemma rel_interior_closure_convex_shrink:
+ fixes S :: "(_::euclidean_space) set"
+ assumes "convex S" "c : rel_interior S" "x : closure S" "0 < e" "e <= 1"
+ shows "x - e *\<^sub>R (x - c) : rel_interior S"
+proof-
+(* Proof is a modified copy of the proof of similar lemma mem_interior_closure_convex_shrink
+*)
+obtain d where "d>0" and d:"ball c d Int affine hull S <= S"
+ using assms(2) unfolding mem_rel_interior_ball by auto
+have "EX y : S. norm (y - x) * (1 - e) < e * d" proof(cases "x : S")
+ case True thus ?thesis using `e>0` `d>0` by(rule_tac bexI[where x=x], auto intro!: mult_pos_pos) next
+ case False hence x:"x islimpt S" using assms(3)[unfolded closure_def] by auto
+ show ?thesis proof(cases "e=1")
+ case True obtain y where "y : S" "y ~= x" "dist y x < 1"
+ using x[unfolded islimpt_approachable,THEN spec[where x=1]] by auto
+ thus ?thesis apply(rule_tac x=y in bexI) unfolding True using `d>0` by auto next
+ case False hence "0 < e * d / (1 - e)" and *:"1 - e > 0"
+ using `e<=1` `e>0` `d>0` by(auto intro!:mult_pos_pos divide_pos_pos)
+ then obtain y where "y : S" "y ~= x" "dist y x < e * d / (1 - e)"
+ using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
+ thus ?thesis apply(rule_tac x=y in bexI) unfolding dist_norm using pos_less_divide_eq[OF *] by auto qed qed
+ then obtain y where "y : S" and y:"norm (y - x) * (1 - e) < e * d" by auto
+ def z == "c + ((1 - e) / e) *\<^sub>R (x - y)"
+ have *:"x - e *\<^sub>R (x - c) = y - e *\<^sub>R (y - z)" unfolding z_def using `e>0` by (auto simp add: scaleR_right_diff_distrib scaleR_right_distrib scaleR_left_diff_distrib)
+ have zball: "z\ball c d"
+ using mem_ball z_def dist_norm[of c] using y and assms(4,5) by (auto simp add:field_simps norm_minus_commute)
+ have "x : affine hull S" using closure_affine_hull assms by auto
+ moreover have "y : affine hull S" using `y : S` hull_subset[of S] by auto
+ moreover have "c : affine hull S" using assms rel_interior_subset hull_subset[of S] by auto
+ ultimately have "z : affine hull S"
+ using z_def affine_affine_hull[of S]
+ mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"]
+ assms by (auto simp add: field_simps)
+ hence "z : S" using d zball by auto
+ obtain d1 where "d1>0" and d1:"ball z d1 <= ball c d"
+ using zball open_ball[of c d] openE[of "ball c d" z] by auto
+ hence "(ball z d1) Int (affine hull S) <= (ball c d) Int (affine hull S)" by auto
+ hence "(ball z d1) Int (affine hull S) <= S" using d by auto
+ hence "z : rel_interior S" using mem_rel_interior_ball using `d1>0` `z : S` by auto
+ hence "y - e *\<^sub>R (y - z) : rel_interior S" using rel_interior_convex_shrink[of S z y e] assms`y : S` by auto
+ thus ?thesis using * by auto
+qed
+
+subsection{* Relative interior preserves under linear transformations *}
+
+lemma rel_interior_translation_aux:
+fixes a :: "'n::euclidean_space"
+shows "((%x. a + x) ` rel_interior S) <= rel_interior ((%x. a + x) ` S)"
+proof-
+{ fix x assume x_def: "x : rel_interior S"
+ from this obtain T where T_def: "open T & x : (T Int S) & (T Int (affine hull S)) <= S" using mem_rel_interior[of x S] by auto
+ from this have "open ((%x. a + x) ` T)" and
+ "(a + x) : (((%x. a + x) ` T) Int ((%x. a + x) ` S))" and
+ "(((%x. a + x) ` T) Int (affine hull ((%x. a + x) ` S))) <= ((%x. a + x) ` S)"
+ using affine_hull_translation[of a S] open_translation[of T a] x_def by auto
+ from this have "(a+x) : rel_interior ((%x. a + x) ` S)"
+ using mem_rel_interior[of "a+x" "((%x. a + x) ` S)"] by auto
+} from this show ?thesis by auto
+qed
+
+lemma rel_interior_translation:
+fixes a :: "'n::euclidean_space"
+shows "rel_interior ((%x. a + x) ` S) = ((%x. a + x) ` rel_interior S)"
+proof-
+have "(%x. (-a) + x) ` rel_interior ((%x. a + x) ` S) <= rel_interior S"
+ using rel_interior_translation_aux[of "-a" "(%x. a + x) ` S"]
+ translation_assoc[of "-a" "a"] by auto
+hence "((%x. a + x) ` rel_interior S) >= rel_interior ((%x. a + x) ` S)"
+ using translation_inverse_subset[of a "rel_interior (op + a ` S)" "rel_interior S"]
+ by auto
+from this show ?thesis using rel_interior_translation_aux[of a S] by auto
+qed
+
+
+lemma affine_hull_linear_image:
+assumes "bounded_linear f"
+shows "f ` (affine hull s) = affine hull f ` s"
+(* Proof is a modified copy of the proof of similar lemma convex_hull_linear_image
+*)
+ apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
+ apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
+ apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
+proof-
+ interpret f: bounded_linear f by fact
+ show "affine {x. f x : affine hull f ` s}"
+ unfolding affine_def by(auto simp add: f.scaleR f.add affine_affine_hull[unfolded affine_def, rule_format]) next
+ interpret f: bounded_linear f by fact
+ show "affine {x. x : f ` (affine hull s)}" using affine_affine_hull[unfolded affine_def, of s]
+ unfolding affine_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
+qed auto
+
+
+lemma rel_interior_injective_on_span_linear_image:
+fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
+fixes S :: "('m::euclidean_space) set"
+assumes "bounded_linear f" and "inj_on f (span S)"
+shows "rel_interior (f ` S) = f ` (rel_interior S)"
+proof-
+{ fix z assume z_def: "z : rel_interior (f ` S)"
+ have "z : f ` S" using z_def rel_interior_subset[of "f ` S"] by auto
+ from this obtain x where x_def: "x : S & (f x = z)" by auto
+ obtain e2 where e2_def: "e2>0 & cball z e2 Int affine hull (f ` S) <= (f ` S)"
+ using z_def rel_interior_cball[of "f ` S"] by auto
+ obtain K where K_def: "K>0 & (! x. norm (f x) <= norm x * K)"
+ using assms RealVector.bounded_linear.pos_bounded[of f] by auto
+ def e1 == "1/K" hence e1_def: "e1>0 & (! x. e1 * norm (f x) <= norm x)"
+ using K_def pos_le_divide_eq[of e1] by auto
+ def e == "e1 * e2" hence "e>0" using e1_def e2_def real_mult_order by auto
+ { fix y assume y_def: "y : cball x e Int affine hull S"
+ from this have h1: "f y : affine hull (f ` S)"
+ using affine_hull_linear_image[of f S] assms by auto
+ from y_def have "norm (x-y)<=e1 * e2"
+ using cball_def[of x e] dist_norm[of x y] e_def by auto
+ moreover have "(f x)-(f y)=f (x-y)"
+ using assms linear_sub[of f x y] linear_conv_bounded_linear[of f] by auto
+ moreover have "e1 * norm (f (x-y)) <= norm (x-y)" using e1_def by auto
+ ultimately have "e1 * norm ((f x)-(f y)) <= e1 * e2" by auto
+ hence "(f y) : (cball z e2)"
+ using cball_def[of "f x" e2] dist_norm[of "f x" "f y"] e1_def x_def by auto
+ hence "f y : (f ` S)" using y_def e2_def h1 by auto
+ hence "y : S" using assms y_def hull_subset[of S] affine_hull_subset_span
+ inj_on_image_mem_iff[of f "span S" S y] by auto
+ }
+ hence "z : f ` (rel_interior S)" using mem_rel_interior_cball[of x S] `e>0` x_def by auto
+}
+moreover
+{ fix x assume x_def: "x : rel_interior S"
+ from this obtain e2 where e2_def: "e2>0 & cball x e2 Int affine hull S <= S"
+ using rel_interior_cball[of S] by auto
+ have "x : S" using x_def rel_interior_subset by auto
+ hence *: "f x : f ` S" by auto
+ have "! x:span S. f x = 0 --> x = 0"
+ using assms subspace_span linear_conv_bounded_linear[of f]
+ linear_injective_on_subspace_0[of f "span S"] by auto
+ from this obtain e1 where e1_def: "e1>0 & (! x : span S. e1 * norm x <= norm (f x))"
+ using assms injective_imp_isometric[of "span S" f]
+ subspace_span[of S] closed_subspace[of "span S"] by auto
+ def e == "e1 * e2" hence "e>0" using e1_def e2_def real_mult_order by auto
+ { fix y assume y_def: "y : cball (f x) e Int affine hull (f ` S)"
+ from this have "y : f ` (affine hull S)" using affine_hull_linear_image[of f S] assms by auto
+ from this obtain xy where xy_def: "xy : affine hull S & (f xy = y)" by auto
+ from this y_def have "norm ((f x)-(f xy))<=e1 * e2"
+ using cball_def[of "f x" e] dist_norm[of "f x" y] e_def by auto
+ moreover have "(f x)-(f xy)=f (x-xy)"
+ using assms linear_sub[of f x xy] linear_conv_bounded_linear[of f] by auto
+ moreover have "x-xy : span S"
+ using subspace_sub[of "span S" x xy] subspace_span `x : S` xy_def
+ affine_hull_subset_span[of S] span_inc by auto
+ moreover hence "e1 * norm (x-xy) <= norm (f (x-xy))" using e1_def by auto
+ ultimately have "e1 * norm (x-xy) <= e1 * e2" by auto
+ hence "xy : (cball x e2)" using cball_def[of x e2] dist_norm[of x xy] e1_def by auto
+ hence "y : (f ` S)" using xy_def e2_def by auto
+ }
+ hence "(f x) : rel_interior (f ` S)"
+ using mem_rel_interior_cball[of "(f x)" "(f ` S)"] * `e>0` by auto
+}
+ultimately show ?thesis by auto
+qed
+
+lemma rel_interior_injective_linear_image:
+fixes f :: "('m::euclidean_space) => ('n::euclidean_space)"
+assumes "bounded_linear f" and "inj f"
+shows "rel_interior (f ` S) = f ` (rel_interior S)"
+using assms rel_interior_injective_on_span_linear_image[of f S]
+ subset_inj_on[of f "UNIV" "span S"] by auto
+
+subsection{* Some Properties of subset of standard basis *}
+
+lemma affine_hull_substd_basis: assumes "d\{.. x$$i = 0)}"
+ (is "affine hull (insert 0 ?A) = ?B")
+proof- have *:"\A. op + (0\'a) ` A = A" "\A. op + (- (0\'a)) ` A = A" by auto
+ show ?thesis unfolding affine_hull_insert_span_gen span_substd_basis[OF assms,THEN sym] * ..
+qed
+
+lemma affine_hull_convex_hull: "affine hull (convex hull S) = affine hull S"
+by (metis Int_absorb1 Int_absorb2 convex_hull_subset_affine_hull hull_hull hull_mono hull_subset)
+
subsection {* Openness and compactness are preserved by convex hull operation. *}
lemma open_convex_hull[intro]:
@@ -1525,6 +3105,61 @@
"convex hull ((\x. a + c *\<^sub>R x) ` s) = (\x. a + c *\<^sub>R x) ` (convex hull s)"
by(simp only: image_image[THEN sym] convex_hull_scaling convex_hull_translation)
+subsection {* Convexity of cone hulls *}
+
+lemma convex_cone_hull:
+fixes S :: "('m::euclidean_space) set"
+assumes "convex S"
+shows "convex (cone hull S)"
+proof-
+{ fix x y assume xy_def: "x : cone hull S & y : cone hull S"
+ hence "S ~= {}" using cone_hull_empty_iff[of S] by auto
+ fix u v assume uv_def: "u>=0 & v>=0 & (u :: real)+v=1"
+ hence *: "u *\<^sub>R x : cone hull S & v *\<^sub>R y : cone hull S"
+ using cone_cone_hull[of S] xy_def cone_def[of "cone hull S"] by auto
+ from * obtain cx xx where x_def: "u *\<^sub>R x = cx *\<^sub>R xx & (cx :: real)>=0 & xx : S"
+ using cone_hull_expl[of S] by auto
+ from * obtain cy yy where y_def: "v *\<^sub>R y = cy *\<^sub>R yy & (cy :: real)>=0 & yy : S"
+ using cone_hull_expl[of S] by auto
+ { assume "cx+cy<=0" hence "u *\<^sub>R x=0 & v *\<^sub>R y=0" using x_def y_def by auto
+ hence "u *\<^sub>R x+ v *\<^sub>R y = 0" by auto
+ hence "u *\<^sub>R x+ v *\<^sub>R y : cone hull S" using cone_hull_contains_0[of S] `S ~= {}` by auto
+ }
+ moreover
+ { assume "cx+cy>0"
+ hence "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy : S"
+ using assms mem_convex_alt[of S xx yy cx cy] x_def y_def by auto
+ hence "cx *\<^sub>R xx + cy *\<^sub>R yy : cone hull S"
+ using mem_cone_hull[of "(cx/(cx+cy)) *\<^sub>R xx + (cy/(cx+cy)) *\<^sub>R yy" S "cx+cy"]
+ `cx+cy>0` by (auto simp add: scaleR_right_distrib)
+ hence "u *\<^sub>R x+ v *\<^sub>R y : cone hull S" using x_def y_def by auto
+ }
+ moreover have "(cx+cy<=0) | (cx+cy>0)" by auto
+ ultimately have "u *\<^sub>R x+ v *\<^sub>R y : cone hull S" by blast
+} from this show ?thesis unfolding convex_def by auto
+qed
+
+lemma cone_convex_hull:
+fixes S :: "('m::euclidean_space) set"
+assumes "cone S"
+shows "cone (convex hull S)"
+proof-
+{ assume "S = {}" hence ?thesis by auto }
+moreover
+{ assume "S ~= {}" hence *: "0:S & (!c. c>0 --> op *\<^sub>R c ` S = S)" using cone_iff[of S] assms by auto
+ { fix c assume "(c :: real)>0"
+ hence "op *\<^sub>R c ` (convex hull S) = convex hull (op *\<^sub>R c ` S)"
+ using convex_hull_scaling[of _ S] by auto
+ also have "...=convex hull S" using * `c>0` by auto
+ finally have "op *\<^sub>R c ` (convex hull S) = convex hull S" by auto
+ }
+ hence "0 : convex hull S & (!c. c>0 --> (op *\<^sub>R c ` (convex hull S)) = (convex hull S))"
+ using * hull_subset[of S convex] by auto
+ hence ?thesis using `S ~= {}` cone_iff[of "convex hull S"] by auto
+}
+ultimately show ?thesis by blast
+qed
+
subsection {* Convex set as intersection of halfspaces. *}
lemma convex_halfspace_intersection:
@@ -1653,28 +3288,6 @@
shows "\ f \{}"
apply(rule helly_induct) using assms by auto
-subsection {* Convex hull is "preserved" by a linear function. *}
-
-lemma convex_hull_linear_image:
- assumes "bounded_linear f"
- shows "f ` (convex hull s) = convex hull (f ` s)"
- apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
- apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
- apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
-proof-
- interpret f: bounded_linear f by fact
- show "convex {x. f x \ convex hull f ` s}"
- unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
- interpret f: bounded_linear f by fact
- show "convex {x. x \ f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s]
- unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
-qed auto
-
-lemma in_convex_hull_linear_image:
- assumes "bounded_linear f" "x \ convex hull s"
- shows "(f x) \ convex hull (f ` s)"
-using convex_hull_linear_image[OF assms(1)] assms(2) by auto
-
subsection {* Homeomorphism of all convex compact sets with nonempty interior. *}
lemma compact_frontier_line_lemma:
@@ -2459,43 +4072,49 @@
apply(rule_tac x=u in exI) defer apply(rule_tac x="\x. if x = 0 then 1 - setsum u s else u x" in exI) using assms(2)
unfolding if_smult and setsum_delta_notmem[OF assms(2)] by auto
+lemma substd_simplex: assumes "d\{.. x$$i = 0)}"
+ (is "convex hull (insert 0 ?p) = ?s")
+(* Proof is a modified copy of the proof of similar lemma std_simplex in Convex_Euclidean_Space.thy *)
+proof- let ?D = d (*"{.. ?D} = basis ` ?D" by auto
+ note sumbas = this setsum_reindex[OF basis_inj_on[of d], unfolded o_def, OF assms]
+ show ?thesis unfolding simplex[OF finite_substdbasis `0 ~: ?p`]
+ apply(rule set_eqI) unfolding mem_Collect_eq apply rule
+ apply(erule exE, (erule conjE)+) apply(erule_tac[2] conjE)+ proof-
+ fix x::"'a::euclidean_space" and u assume as: "\x\{basis i |i. i \?D}. 0 \ u x"
+ "setsum u {basis i |i. i \ ?D} \ 1" "(\x\{basis i |i. i \?D}. u x *\<^sub>R x) = x"
+ have *:"\i u (basis i) = x$$i" and "(!i x $$ i = 0)" using as(3)
+ unfolding sumbas unfolding substdbasis_expansion_unique[OF assms] by auto
+ hence **:"setsum u {basis i |i. i \ ?D} = setsum (op $$ x) ?D" unfolding sumbas
+ apply-apply(rule setsum_cong2) using assms by auto
+ have " (\i x$$i) \ setsum (op $$ x) ?D \ 1"
+ apply - proof(rule,rule,rule)
+ fix i assume i:"i 0 \ x$$i" unfolding *[rule_format,OF i,THEN sym]
+ apply(rule_tac as(1)[rule_format]) by auto
+ moreover have "i ~: d ==> 0 \ x$$i"
+ using `(!i x $$ i = 0)`[rule_format, OF i] by auto
+ ultimately show "0 \ x$$i" by auto
+ qed(insert as(2)[unfolded **], auto)
+ from this show " (\i x$$i) \ setsum (op $$ x) ?D \ 1 & (!i x $$ i = 0)"
+ using `(!i x $$ i = 0)` by auto
+ next fix x::"'a::euclidean_space" assume as:"\i x $$ i" "setsum (op $$ x) ?D \ 1"
+ "(!i x $$ i = 0)"
+ show "\u. (\x\{basis i |i. i \ ?D}. 0 \ u x) \
+ setsum u {basis i |i. i \ ?D} \ 1 \ (\x\{basis i |i. i \ ?D}. u x *\<^sub>R x) = x"
+ apply(rule_tac x="\y. inner y x" in exI) apply(rule,rule) unfolding mem_Collect_eq apply(erule exE)
+ using as(1) apply(erule_tac x=i in allE) unfolding sumbas apply safe unfolding not_less basis_zero
+ unfolding substdbasis_expansion_unique[OF assms] euclidean_component_def[THEN sym]
+ using as(2,3) by(auto simp add:dot_basis not_less basis_zero)
+ qed qed
+
lemma std_simplex:
"convex hull (insert 0 { basis i | i. ii x$$i) \ setsum (\i. x$$i) {..