--- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 22:31:56 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 22:33:16 2013 +0200
@@ -1,5 +1,8 @@
(* Title: Doc/Datatypes/Datatypes.thy
Author: Jasmin Blanchette, TU Muenchen
+ Author: Lorenz Panny, TU Muenchen
+ Author: Andrei Popescu, TU Muenchen
+ Author: Dmitriy Traytel, TU Muenchen
Tutorial for (co)datatype definitions with the new package.
*)
@@ -22,7 +25,7 @@
to use the new package.
Perhaps the main advantage of the new package is that it supports recursion
-through a large class of non-datatypes, comprising finite sets:
+through a large class of non-datatypes, such as finite sets:
*}
datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s 'a "'a tree\<^sub>f\<^sub>s fset"
@@ -48,7 +51,11 @@
finite and infinite values:
*}
- codatatype 'a llist (*<*)(map: lmap) (*>*)= LNil | LCons 'a "'a llist"
+(*<*)
+ locale dummy_llist
+ begin
+(*>*)
+ codatatype 'a llist = LNil | LCons 'a "'a llist"
text {*
\noindent
@@ -56,10 +63,6 @@
following four Rose tree examples:
*}
-(*<*)
- locale dummy_tree
- begin
-(*>*)
datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
datatype_new 'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
codatatype 'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
@@ -122,21 +125,21 @@
to register arbitrary type constructors as BNFs.
\item Section
-\ref{sec:generating-destructors-and-theorems-for-free-constructors},
-``Generating Destructors and Theorems for Free Constructors,'' explains how to
+\ref{sec:deriving-destructors-and-theorems-for-free-constructors},
+``Deriving Destructors and Theorems for Free Constructors,'' explains how to
use the command @{command wrap_free_constructors} to derive destructor constants
and theorems for freely generated types, as performed internally by @{command
datatype_new} and @{command codatatype}.
-\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
-describes the package's programmatic interface.
+%\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
+%describes the package's programmatic interface.
-\item Section \ref{sec:interoperability}, ``Interoperability,''
-is concerned with the packages' interaction with other Isabelle packages and
-tools, such as the code generator and the counterexample generators.
+%\item Section \ref{sec:interoperability}, ``Interoperability,''
+%is concerned with the packages' interaction with other Isabelle packages and
+%tools, such as the code generator and the counterexample generators.
-\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
-Limitations,'' concludes with known open issues at the time of writing.
+%\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
+%Limitations,'' concludes with known open issues at the time of writing.
\end{itemize}
@@ -174,17 +177,19 @@
\label{sec:defining-datatypes} *}
text {*
-This section describes how to specify datatypes using the @{command
-datatype_new} command. The command is first illustrated through concrete
-examples featuring different flavors of recursion. More examples can be found in
-the directory \verb|~~/src/HOL/BNF/Examples|.
+Datatypes can be specified using the @{command datatype_new} command. The
+command is first illustrated through concrete examples featuring different
+flavors of recursion. More examples can be found in the directory
+\verb|~~/src/HOL/BNF/Examples|.
*}
-subsection {* Examples
- \label{ssec:datatype-examples} *}
+subsection {* Introductory Examples
+ \label{ssec:datatype-introductory-examples} *}
-subsubsection {* Nonrecursive Types *}
+
+subsubsection {* Nonrecursive Types
+ \label{sssec:datatype-nonrecursive-types} *}
text {*
Datatypes are introduced by specifying the desired names and argument types for
@@ -228,17 +233,14 @@
datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
-subsubsection {* Simple Recursion *}
+subsubsection {* Simple Recursion
+ \label{sssec:datatype-simple-recursion} *}
text {*
Natural numbers are the simplest example of a recursive type:
*}
datatype_new nat = Zero | Suc nat
-(*<*)
- (* FIXME: remove once "datatype_new" is integrated with "fun" *)
- datatype_new_compat nat
-(*>*)
text {*
\noindent
@@ -261,7 +263,8 @@
*}
-subsubsection {* Mutual Recursion *}
+subsubsection {* Mutual Recursion
+ \label{sssec:datatype-mutual-recursion} *}
text {*
\emph{Mutually recursive} types are introduced simultaneously and may refer to
@@ -269,8 +272,8 @@
natural numbers:
*}
- datatype_new enat = EZero | ESuc onat
- and onat = OSuc enat
+ datatype_new even_nat = Even_Zero | Even_Suc odd_nat
+ and odd_nat = Odd_Suc even_nat
text {*
\noindent
@@ -286,7 +289,8 @@
Const 'a | Var 'b | Expr "('a, 'b) exp"
-subsubsection {* Nested Recursion *}
+subsubsection {* Nested Recursion
+ \label{sssec:datatype-nested-recursion} *}
text {*
\emph{Nested recursion} occurs when recursive occurrences of a type appear under
@@ -319,6 +323,13 @@
text {*
\noindent
+This is legal:
+*}
+
+ datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
+
+text {*
+\noindent
In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
@{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
@@ -333,48 +344,17 @@
*}
-subsubsection {* Auxiliary Constants and Syntaxes *}
+subsubsection {* Custom Names and Syntaxes
+ \label{sssec:datatype-custom-names-and-syntaxes} *}
text {*
The @{command datatype_new} command introduces various constants in addition to
-the constructors. Given a type @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
-with $m > 0$ live type variables and $n$ constructors
-@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
-following auxiliary constants are introduced (among others):
-
-\begin{itemize}
-\setlength{\itemsep}{0pt}
-
-\item \relax{Case combinator}: @{text t_case} (rendered using the familiar
-@{text case}--@{text of} syntax)
-
-\item \relax{Iterator}: @{text t_fold}
-
-\item \relax{Recursor}: @{text t_rec}
-
-\item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
-@{text "t.is_C\<^sub>n"}
-
-\item \relax{Selectors}:
-@{text t.un_C\<^sub>11}$, \ldots, @{text t.un_C\<^sub>1k\<^sub>1}, \\
-\phantom{\relax{Selectors:}} \quad\vdots \\
-\phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
-
-\item \relax{Set functions} (or \relax{natural transformations}):
-@{text t_set1}, \ldots, @{text t_setm}
-
-\item \relax{Map function} (or \relax{functorial action}): @{text t_map}
-
-\item \relax{Relator}: @{text t_rel}
-
-\end{itemize}
-
-\noindent
-The case combinator, discriminators, and selectors are collectively called
-\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
-name and is normally hidden. The set functions, map function, relator,
-discriminators, and selectors can be given custom names, as in the example
-below:
+the constructors. With each datatype are associated set functions, a map
+function, a relator, discriminators, and selectors, all of which can be given
+custom names. In the example below, the traditional names
+@{text set}, @{text map}, @{text list_all2}, @{text null}, @{text hd}, and
+@{text tl} override the default names @{text list_set}, @{text list_map}, @{text
+list_rel}, @{text is_Nil}, @{text un_Cons1}, and @{text un_Cons2}:
*}
(*<*)
@@ -413,7 +393,7 @@
to ensure that the tail of the empty list is itself (instead of being left
unspecified).
-Because @{const Nil} is a nullary constructor, it is also possible to use
+Because @{const Nil} is nullary, it is also possible to use
@{term "\<lambda>xs. xs = Nil"} as a discriminator. This is specified by
entering ``@{text "="}'' instead of the identifier @{const null}. Although this
may look appealing, the mixture of constructors and selectors in the
@@ -449,8 +429,12 @@
"[x]" == "x # []"
-subsection {* Syntax
- \label{ssec:datatype-syntax} *}
+subsection {* Command Syntax
+ \label{ssec:datatype-command-syntax} *}
+
+
+subsubsection {* \keyw{datatype\_new}
+ \label{sssec:datatype-new} *}
text {*
Datatype definitions have the following general syntax:
@@ -459,7 +443,7 @@
@@{command_def datatype_new} target? @{syntax dt_options}? \\
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
;
- @{syntax_def dt_options}: '(' ((@'no_discs_sels' | @'rep_compat') + ',') ')'
+ @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
"}
The syntactic quantity \synt{target} can be used to specify a local
@@ -472,11 +456,11 @@
\setlength{\itemsep}{0pt}
\item
-The \keyw{no\_discs\_sels} option indicates that no discriminators or selectors
+The @{text "no_discs_sels"} option indicates that no discriminators or selectors
should be generated.
\item
-The \keyw{rep\_compat} option indicates that the names generated by the
+The @{text "rep_compat"} option indicates that the names generated by the
package should contain optional (and normally not displayed) ``@{text "new."}''
components to prevent clashes with a later call to \keyw{rep\_datatype}. See
Section~\ref{ssec:datatype-compatibility-issues} for details.
@@ -530,7 +514,7 @@
constructors as long as they share the same type.
@{rail "
- @{syntax_def dt_sel_defaults}: '(' @'defaults' (name ':' term +) ')'
+ @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
"}
\noindent
@@ -543,12 +527,102 @@
(i.e., it may depends on @{text C}'s arguments).
*}
+
+subsubsection {* \keyw{datatype\_new\_compat}
+ \label{sssec:datatype-new-compat} *}
+
+text {*
+The old datatype package provides some functionality that is not yet replicated
+in the new package:
+
+\begin{itemize}
+\item It is integrated with \keyw{fun} and \keyw{function}
+\cite{isabelle-function}, Nitpick \cite{isabelle-nitpick}, Quickcheck,
+and other packages.
+
+\item It is extended by various add-ons, notably to produce instances of the
+@{const size} function.
+\end{itemize}
+
+\noindent
+New-style datatypes can in most case be registered as old-style datatypes using
+the command
+
+@{rail "
+ @@{command_def datatype_new_compat} names
+"}
+
+\noindent
+where the \textit{names} argument is simply a space-separated list of type names
+that are mutually recursive. For example:
+*}
+
+ datatype_new_compat even_nat odd_nat
+
+text {* \blankline *}
+
+ thm even_nat_odd_nat.size
+
+text {* \blankline *}
+
+ ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
+
+text {*
+For nested recursive datatypes, all types through which recursion takes place
+must be new-style datatypes. In principle, it should be possible to support
+old-style datatypes as well, but the command does not support this yet.
+*}
+
+
+subsection {* Generated Constants
+ \label{ssec:datatype-generated-constants} *}
+
+text {*
+Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
+with $m > 0$ live type variables and $n$ constructors
+@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
+following auxiliary constants are introduced:
+
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\item \relax{Case combinator}: @{text t_case} (rendered using the familiar
+@{text case}--@{text of} syntax)
+
+\item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots,
+@{text "t.is_C\<^sub>n"}
+
+\item \relax{Selectors}:
+@{text t.un_C\<^sub>11}$, \ldots, @{text t.un_C\<^sub>1k\<^sub>1}, \\
+\phantom{\relax{Selectors:}} \quad\vdots \\
+\phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}.
+
+\item \relax{Set functions} (or \relax{natural transformations}):
+@{text t_set1}, \ldots, @{text t_setm}
+
+\item \relax{Map function} (or \relax{functorial action}): @{text t_map}
+
+\item \relax{Relator}: @{text t_rel}
+
+\item \relax{Iterator}: @{text t_fold}
+
+\item \relax{Recursor}: @{text t_rec}
+
+\end{itemize}
+
+\noindent
+The case combinator, discriminators, and selectors are collectively called
+\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
+name and is normally hidden.
+*}
+
+
subsection {* Generated Theorems
\label{ssec:datatype-generated-theorems} *}
text {*
The characteristic theorems generated by @{command datatype_new} are grouped in
-two broad categories:
+three broad categories:
\begin{itemize}
\item The \emph{free constructor theorems} are properties about the constructors
@@ -580,7 +654,8 @@
to the top of the theory file.
*}
-subsubsection {* Free Constructor Theorems *}
+subsubsection {* Free Constructor Theorems
+ \label{sssec:free-constructor-theorems} *}
(*<*)
consts is_Cons :: 'a
@@ -593,42 +668,55 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\rmfamily:] ~ \\
@{thm list.inject[no_vars]}
-\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\rmfamily:] ~ \\
@{thm list.distinct(1)[no_vars]} \\
@{thm list.distinct(2)[no_vars]}
-\item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
@{thm list.exhaust[no_vars]}
-\item[@{text "t."}\hthm{nchotomy}\upshape:] ~ \\
+\item[@{text "t."}\hthm{nchotomy}\rmfamily:] ~ \\
@{thm list.nchotomy[no_vars]}
\end{description}
\end{indentblock}
\noindent
+In addition, these nameless theorems are registered as safe elimination rules:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{list.distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rmfamily:] ~ \\
+@{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
+@{thm list.distinct(2)[THEN notE, elim!, no_vars]}
+
+\end{description}
+\end{indentblock}
+
+\noindent
The next subgroup is concerned with the case combinator:
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{case} @{text "[simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{case} @{text "[simp]"}\rmfamily:] ~ \\
@{thm list.case(1)[no_vars]} \\
@{thm list.case(2)[no_vars]}
-\item[@{text "t."}\hthm{case\_cong}\upshape:] ~ \\
+\item[@{text "t."}\hthm{case\_cong}\rmfamily:] ~ \\
@{thm list.case_cong[no_vars]}
-\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\rmfamily:] ~ \\
@{thm list.weak_case_cong[no_vars]}
-\item[@{text "t."}\hthm{split}\upshape:] ~ \\
+\item[@{text "t."}\hthm{split}\rmfamily:] ~ \\
@{thm list.split[no_vars]}
-\item[@{text "t."}\hthm{split\_asm}\upshape:] ~ \\
+\item[@{text "t."}\hthm{split\_asm}\rmfamily:] ~ \\
@{thm list.split_asm[no_vars]}
\item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
@@ -642,32 +730,32 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{discs} @{text "[simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{discs} @{text "[simp]"}\rmfamily:] ~ \\
@{thm list.discs(1)[no_vars]} \\
@{thm list.discs(2)[no_vars]}
-\item[@{text "t."}\hthm{sels} @{text "[simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{sels} @{text "[simp]"}\rmfamily:] ~ \\
@{thm list.sels(1)[no_vars]} \\
@{thm list.sels(2)[no_vars]}
-\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rmfamily:] ~ \\
@{thm list.collapse(1)[no_vars]} \\
@{thm list.collapse(2)[no_vars]}
-\item[@{text "t."}\hthm{disc\_exclude}\upshape:] ~ \\
+\item[@{text "t."}\hthm{disc\_exclude}\rmfamily:] ~ \\
These properties are missing for @{typ "'a list"} because there is only one
proper discriminator. Had the datatype been introduced with a second
discriminator called @{const is_Cons}, they would have read thusly: \\[\jot]
@{prop "null list \<Longrightarrow> \<not> is_Cons list"} \\
@{prop "is_Cons list \<Longrightarrow> \<not> null list"}
-\item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
@{thm list.disc_exhaust[no_vars]}
-\item[@{text "t."}\hthm{expand}\upshape:] ~ \\
+\item[@{text "t."}\hthm{expand}\rmfamily:] ~ \\
@{thm list.expand[no_vars]}
-\item[@{text "t."}\hthm{case\_conv}\upshape:] ~ \\
+\item[@{text "t."}\hthm{case\_conv}\rmfamily:] ~ \\
@{thm list.case_conv[no_vars]}
\end{description}
@@ -675,27 +763,28 @@
*}
-subsubsection {* Functorial Theorems *}
+subsubsection {* Functorial Theorems
+ \label{sssec:functorial-theorems} *}
text {*
-The BNF-related theorem are listed below:
+The BNF-related theorem are as follows:
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{sets} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{sets} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.sets(1)[no_vars]} \\
@{thm list.sets(2)[no_vars]}
-\item[@{text "t."}\hthm{map} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{map} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.map(1)[no_vars]} \\
@{thm list.map(2)[no_vars]}
-\item[@{text "t."}\hthm{rel\_inject} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{rel\_inject} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.rel_inject(1)[no_vars]} \\
@{thm list.rel_inject(2)[no_vars]}
-\item[@{text "t."}\hthm{rel\_distinct} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{rel\_distinct} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.rel_distinct(1)[no_vars]} \\
@{thm list.rel_distinct(2)[no_vars]}
@@ -704,26 +793,27 @@
*}
-subsubsection {* Inductive Theorems *}
+subsubsection {* Inductive Theorems
+ \label{sssec:inductive-theorems} *}
text {*
-The inductive theorems are listed below:
+The inductive theorems are as follows:
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
@{thm list.induct[no_vars]}
-\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\upshape:] ~ \\
+\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
prove $m$ properties simultaneously.
-\item[@{text "t."}\hthm{fold} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{fold} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.fold(1)[no_vars]} \\
@{thm list.fold(2)[no_vars]}
-\item[@{text "t."}\hthm{rec} @{text "[code]"}\upshape:] ~ \\
+\item[@{text "t."}\hthm{rec} @{text "[code]"}\rmfamily:] ~ \\
@{thm list.rec(1)[no_vars]} \\
@{thm list.rec(2)[no_vars]}
@@ -744,47 +834,45 @@
*}
+(*
subsection {* Compatibility Issues
\label{ssec:datatype-compatibility-issues} *}
text {*
- * main incompabilities between two packages
- * differences in theorem names (e.g. singular vs. plural for some props?)
- * differences in "simps"?
- * different recursor/induction in nested case
- * discussed in Section~\ref{sec:defining-recursive-functions}
- * different ML interfaces / extension mechanisms
+% * main incompabilities between two packages
+% * differences in theorem names (e.g. singular vs. plural for some props?)
+% * differences in "simps"?
+% * different recursor/induction in nested case
+% * discussed in Section~\ref{sec:defining-recursive-functions}
+% * different ML interfaces / extension mechanisms
+%
+% * register new datatype as old datatype
+% * motivation:
+% * do recursion through new datatype in old datatype
+% (e.g. useful when porting to the new package one type at a time)
+% * use old primrec
+% * use fun
+% * use extensions like size (needed for fun), the AFP order, Quickcheck,
+% Nitpick
+% * provide exactly the same theorems with the same names (compatibility)
+% * option 1
+% * @{text "rep_compat"}
+% * \keyw{rep\_datatype}
+% * has some limitations
+% * mutually recursive datatypes? (fails with rep_datatype?)
+% * nested datatypes? (fails with datatype_new?)
+% * option 2
+% * @{command datatype_new_compat}
+% * not fully implemented yet?
- * register new datatype as old datatype
- * motivation:
- * do recursion through new datatype in old datatype
- (e.g. useful when porting to the new package one type at a time)
- * use old primrec
- * use fun
- * use extensions like size (needed for fun), the AFP order, Quickcheck,
- Nitpick
- * provide exactly the same theorems with the same names (compatibility)
- * option 1
- * \keyw{rep\_compat}
- * \keyw{rep\_datatype}
- * has some limitations
- * mutually recursive datatypes? (fails with rep_datatype?)
- * nested datatypes? (fails with datatype_new?)
- * option 2
- * @{command datatype_new_compat}
- * not fully implemented yet?
-
-@{rail "
- @@{command_def datatype_new_compat} types
-"}
-
- * register old datatype as new datatype
- * no clean way yet
- * if the goal is to do recursion through old datatypes, can register it as
- a BNF (Section XXX)
- * can also derive destructors etc. using @{command wrap_free_constructors}
- (Section XXX)
+% * register old datatype as new datatype
+% * no clean way yet
+% * if the goal is to do recursion through old datatypes, can register it as
+% a BNF (Section XXX)
+% * can also derive destructors etc. using @{command wrap_free_constructors}
+% (Section XXX)
*}
+*)
section {* Defining Recursive Functions
@@ -793,65 +881,72 @@
text {*
This describes how to specify recursive functions over datatypes specified using
@{command datatype_new}. The focus in on the @{command primrec_new} command,
-which supports primitive recursion. A few examples feature the \keyw{fun} and
-\keyw{function} commands, described in a separate tutorial
-\cite{isabelle-function}.
+which supports primitive recursion. More examples can be found in
+\verb|~~/src/HOL/BNF/Examples|.
+
+%%% TODO: partial_function
+*}
+
-%%% TODO: partial_function?
-*}
+subsection {* Introductory Examples
+ \label{ssec:primrec-introductory-examples} *}
+
+
+subsubsection {* Nonrecursive Types
+ \label{sssec:primrec-nonrecursive-types} *}
text {*
-More examples in \verb|~~/src/HOL/BNF/Examples|.
-*}
-
-subsection {* Examples
- \label{ssec:primrec-examples} *}
-
-subsubsection {* Nonrecursive Types *}
-
-text {*
- * simple (depth 1) pattern matching on the left-hand side
+Primitive recursion removes one layer of constructors on the left-hand side in
+each equation. For example:
*}
primrec_new bool_of_trool :: "trool \<Rightarrow> bool" where
- "bool_of_trool Faalse = False" |
- "bool_of_trool Truue = True"
+ "bool_of_trool Faalse \<longleftrightarrow> False" |
+ "bool_of_trool Truue \<longleftrightarrow> True"
-text {*
- * OK to specify the cases in a different order
- * OK to leave out some case (but get a warning -- maybe we need a "quiet"
- or "silent" flag?)
- * case is then unspecified
-
-More examples:
-*}
+text {* \blankline *}
primrec_new the_list :: "'a option \<Rightarrow> 'a list" where
"the_list None = []" |
"the_list (Some a) = [a]"
+text {* \blankline *}
+
primrec_new the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
"the_default d None = d" |
"the_default _ (Some a) = a"
+text {* \blankline *}
+
primrec_new mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
"mirrror (Triple a b c) = Triple c b a"
+text {*
+\noindent
+The equations can be specified in any order, and it is acceptable to leave out
+some cases, which are then unspecified. Pattern matching on the left-hand side
+is restricted to a single datatype, which must correspond to the same argument
+in all equations.
+*}
-subsubsection {* Simple Recursion *}
+
+subsubsection {* Simple Recursion
+ \label{sssec:primrec-simple-recursion} *}
text {*
-again, simple pattern matching on left-hand side, but possibility
-to call a function recursively on an argument to a constructor:
+For simple recursive types, recursive calls on a constructor argument are
+allowed on the right-hand side:
*}
+(*<*)
+ context dummy_tlist
+ begin
+(*>*)
primrec_new replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
"replicate Zero _ = []" |
"replicate (Suc n) a = a # replicate n a"
-text {*
-we don't like the confusing name @{const nth}:
-*}
+text {* \blankline *}
primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
"at (a # as) j =
@@ -859,10 +954,8 @@
Zero \<Rightarrow> a
| Suc j' \<Rightarrow> at as j')"
-(*<*)
- context dummy_tlist
- begin
-(*>*)
+text {* \blankline *}
+
primrec_new tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
"tfold _ (TNil b) = b" |
"tfold f (TCons a as) = f a (tfold f as)"
@@ -871,39 +964,37 @@
(*>*)
text {*
-Show one example where fun is needed.
+\noindent
+The next example is not primitive recursive, but it can be defined easily using
+@{command fun}. The @{command datatype_new_compat} command is needed to register
+new-style datatypes for use with @{command fun} and @{command function}
+(Section~\ref{sssec:datatype-new-compat}):
*}
-subsubsection {* Mutual Recursion *}
+ datatype_new_compat nat
+
+text {* \blankline *}
+
+ fun at_least_two :: "nat \<Rightarrow> bool" where
+ "at_least_two (Suc (Suc _)) \<longleftrightarrow> True" |
+ "at_least_two _ \<longleftrightarrow> False"
+
+
+subsubsection {* Mutual Recursion
+ \label{sssec:primrec-mutual-recursion} *}
text {*
-E.g., converting even/odd naturals to plain old naturals:
+The syntax for mutually recursive functions over mutually recursive datatypes
+is straightforward:
*}
primrec_new
- nat_of_enat :: "enat \<Rightarrow> nat" and
- nat_of_onat :: "onat => nat"
+ nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
+ nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
where
- "nat_of_enat EZero = Zero" |
- "nat_of_enat (ESuc n) = Suc (nat_of_onat n)" |
- "nat_of_onat (OSuc n) = Suc (nat_of_enat n)"
-
-text {*
-Mutual recursion is be possible within a single type, but currently only using fun:
-*}
-
- fun
- even :: "nat \<Rightarrow> bool" and
- odd :: "nat \<Rightarrow> bool"
- where
- "even Zero = True" |
- "even (Suc n) = odd n" |
- "odd Zero = False" |
- "odd (Suc n) = even n"
-
-text {*
-More elaborate example that works with primrec_new:
-*}
+ "nat_of_even_nat Even_Zero = Zero" |
+ "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
+ "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
primrec_new
eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
@@ -918,26 +1009,54 @@
"eval\<^sub>f _ \<xi> (Var b) = \<xi> b" |
"eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e"
+text {*
+\noindent
+Mutual recursion is be possible within a single type, using @{command fun}:
+*}
-subsubsection {* Nested Recursion *}
+ fun
+ even :: "nat \<Rightarrow> bool" and
+ odd :: "nat \<Rightarrow> bool"
+ where
+ "even Zero = True" |
+ "even (Suc n) = odd n" |
+ "odd Zero = False" |
+ "odd (Suc n) = even n"
+
+
+subsubsection {* Nested Recursion
+ \label{sssec:primrec-nested-recursion} *}
+
+text {*
+In a departure from the old datatype package, nested recursion is normally
+handled via the map functions of the nesting type constructors. For example,
+recursive calls are lifted to lists using @{const map}:
+*}
(*<*)
datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
- datatype_new 'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
+
+ context dummy_tlist
+ begin
(*>*)
primrec_new at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
"at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
(case js of
[] \<Rightarrow> a
| j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
+(*<*)
+ end
+(*>*)
text {*
-Explain @{const lmap}.
+The next example features recursion through the @{text option} type. Although
+@{text option} is not a new-style datatype, it is registered as a BNF with the
+map function @{const option_map}:
*}
(*<*)
locale sum_btree_nested
- begin
+ begin
(*>*)
primrec_new sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
"sum_btree (BNode a lt rt) =
@@ -948,15 +1067,31 @@
(*>*)
text {*
-Show example with function composition (ftree).
+\noindent
+The same principle applies for arbitrary type constructors through which
+recursion is possible. Notably, the map function for the function type
+(@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
*}
-subsubsection {* Nested-as-Mutual Recursion *}
+ primrec_new ftree_map :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
+ "ftree_map f (FTLeaf x) = FTLeaf (f x)" |
+ "ftree_map f (FTNode g) = FTNode (ftree_map f \<circ> g)"
text {*
- * can pretend a nested type is mutually recursive (if purely inductive)
- * avoids the higher-order map
- * e.g.
+\noindent
+(No such function is defined by the package because @{typ 'a} is dead in
+@{typ "'a ftree"}, but we can easily do it ourselves.)
+*}
+
+
+subsubsection {* Nested-as-Mutual Recursion
+ \label{sssec:datatype-nested-as-mutual-recursion} *}
+
+text {*
+For compatibility with the old package, but also because it is sometimes
+convenient in its own right, it is possible to treat nested recursive datatypes
+as mutually recursive ones if the recursion takes place though new-style
+datatypes. For example:
*}
primrec_new
@@ -972,6 +1107,8 @@
Zero \<Rightarrow> at_tree\<^sub>f\<^sub>f t
| Suc j' \<Rightarrow> at_trees\<^sub>f\<^sub>f ts j')"
+text {* \blankline *}
+
primrec_new
sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
sum_btree_option :: "'a btree option \<Rightarrow> 'a"
@@ -982,34 +1119,42 @@
"sum_btree_option (Some t) = sum_btree t"
text {*
- * this can always be avoided;
- * e.g. in our previous example, we first mapped the recursive
- calls, then we used a generic at function to retrieve the result
- * there's no hard-and-fast rule of when to use one or the other,
- just like there's no rule when to use fold and when to use
- primrec_new
-
- * higher-order approach, considering nesting as nesting, is more
- compositional -- e.g. we saw how we could reuse an existing polymorphic
- at or the_default, whereas @{text at_trees\<^sub>f\<^sub>f} is much more specific
+% * can pretend a nested type is mutually recursive (if purely inductive)
+% * avoids the higher-order map
+% * e.g.
- * but:
- * is perhaps less intuitive, because it requires higher-order thinking
- * may seem inefficient, and indeed with the code generator the
- mutually recursive version might be nicer
- * is somewhat indirect -- must apply a map first, then compute a result
- (cannot mix)
- * the auxiliary functions like @{text at_trees\<^sub>f\<^sub>f} are sometimes useful in own right
-
- * impact on automation unclear
-
-%%% TODO: change text antiquotation to const once the real primrec is used
+% * this can always be avoided;
+% * e.g. in our previous example, we first mapped the recursive
+% calls, then we used a generic at function to retrieve the result
+%
+% * there's no hard-and-fast rule of when to use one or the other,
+% just like there's no rule when to use fold and when to use
+% primrec_new
+%
+% * higher-order approach, considering nesting as nesting, is more
+% compositional -- e.g. we saw how we could reuse an existing polymorphic
+% at or the_default, whereas @{const at_trees\<^sub>f\<^sub>f} is much more specific
+%
+% * but:
+% * is perhaps less intuitive, because it requires higher-order thinking
+% * may seem inefficient, and indeed with the code generator the
+% mutually recursive version might be nicer
+% * is somewhat indirect -- must apply a map first, then compute a result
+% (cannot mix)
+% * the auxiliary functions like @{const at_trees\<^sub>f\<^sub>f} are sometimes useful in own right
+%
+% * impact on automation unclear
+%
*}
-subsection {* Syntax
- \label{ssec:primrec-syntax} *}
+subsection {* Command Syntax
+ \label{ssec:primrec-command-syntax} *}
+
+
+subsubsection {* \keyw{primrec\_new}
+ \label{sssec:primrec-new} *}
text {*
Primitive recursive functions have the following general syntax:
@@ -1023,28 +1168,31 @@
*}
+(*
subsection {* Generated Theorems
\label{ssec:primrec-generated-theorems} *}
text {*
- * synthesized nonrecursive definition
- * user specification is rederived from it, exactly as entered
+% * synthesized nonrecursive definition
+% * user specification is rederived from it, exactly as entered
+%
+% * induct
+% * mutualized
+% * without some needless induction hypotheses if not used
+% * fold, rec
+% * mutualized
+*}
+*)
- * induct
- * mutualized
- * without some needless induction hypotheses if not used
- * fold, rec
- * mutualized
-*}
subsection {* Recursive Default Values for Selectors
- \label{ssec:recursive-default-values-for-selectors} *}
+ \label{ssec:primrec-recursive-default-values-for-selectors} *}
text {*
A datatype selector @{text un_D} can have a default value for each constructor
on which it is not otherwise specified. Occasionally, it is useful to have the
default value be defined recursively. This produces a chicken-and-egg situation
-that appears unsolvable, because the datatype is not introduced yet at the
+that may seem unsolvable, because the datatype is not introduced yet at the
moment when the selectors are introduced. Of course, we can always define the
selectors manually afterward, but we then have to state and prove all the
characteristic theorems ourselves instead of letting the package do it.
@@ -1072,100 +1220,263 @@
for @{text "un_D\<^sub>0"}.
\end{enumerate}
+\noindent
The following example illustrates this procedure:
*}
consts termi\<^sub>0 :: 'a
+text {* \blankline *}
+
datatype_new ('a, 'b) tlist =
TNil (termi: 'b) (defaults ttl: TNil)
| TCons (thd: 'a) (ttl : "('a, 'b) tlist") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs")
+text {* \blankline *}
+
overloading
termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
begin
primrec_new termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
- "termi\<^sub>0 (TNil y) = y" |
- "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
+ "termi\<^sub>0 (TNil y) = y" |
+ "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
end
+text {* \blankline *}
+
lemma terminal_TCons[simp]: "termi (TCons x xs) = termi xs"
by (cases xs) auto
+(*
subsection {* Compatibility Issues
- \label{ssec:datatype-compatibility-issues} *}
+ \label{ssec:primrec-compatibility-issues} *}
text {*
- * different induction in nested case
- * solution: define nested-as-mutual functions with primrec,
- and look at .induct
-
- * different induction and recursor in nested case
- * only matters to low-level users; they can define a dummy function to force
- generation of mutualized recursor
+% * different induction in nested case
+% * solution: define nested-as-mutual functions with primrec,
+% and look at .induct
+%
+% * different induction and recursor in nested case
+% * only matters to low-level users; they can define a dummy function to force
+% generation of mutualized recursor
*}
+*)
section {* Defining Codatatypes
\label{sec:defining-codatatypes} *}
text {*
-This section describes how to specify codatatypes using the @{command codatatype}
-command.
+Codatatypes can be specified using the @{command codatatype} command. The
+command is first illustrated through concrete examples featuring different
+flavors of corecursion. More examples can be found in the directory
+\verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs} also
+includes some useful codatatypes, notably for lazy lists \cite{lochbihler-2010}.
+*}
+
+
+subsection {* Introductory Examples
+ \label{ssec:codatatype-introductory-examples} *}
+
+
+subsubsection {* Simple Corecursion
+ \label{sssec:codatatype-simple-corecursion} *}
+
+text {*
+Noncorecursive codatatypes coincide with the corresponding datatypes, so
+they have no practical uses. \emph{Corecursive codatatypes} have the same syntax
+as recursive datatypes, except for the command name. For example, here is the
+definition of lazy lists:
+*}
+
+ codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
+ lnull: LNil (defaults ltl: LNil)
+ | LCons (lhd: 'a) (ltl: "'a llist")
+
+text {*
+\noindent
+Lazy lists can be infinite, such as @{text "LCons 0 (LCons 0 (\<dots>))"} and
+@{text "LCons 0 (LCons 1 (LCons 2 (\<dots>)))"}. Another interesting type that can
+be defined as a codatatype is that of the extended natural numbers:
+*}
+
+ codatatype enat = EZero | ESuc nat
- * libraries include some useful codatatypes, notably lazy lists;
- see the ``Coinductive'' AFP entry \cite{xxx} for an elaborate library
+text {*
+\noindent
+This type has exactly one infinite element, @{text "ESuc (ESuc (ESuc (\<dots>)))"},
+that represents $\infty$. In addition, it has finite values of the form
+@{text "ESuc (\<dots> (ESuc EZero)\<dots>)"}.
+*}
+
+
+subsubsection {* Mutual Corecursion
+ \label{sssec:codatatype-mutual-corecursion} *}
+
+text {*
+\noindent
+The example below introduces a pair of \emph{mutually corecursive} types:
+*}
+
+ codatatype even_enat = Even_EZero | Even_ESuc odd_enat
+ and odd_enat = Odd_ESuc even_enat
+
+
+subsubsection {* Nested Corecursion
+ \label{sssec:codatatype-nested-corecursion} *}
+
+text {*
+\noindent
+The next two examples feature \emph{nested corecursion}:
+*}
+
+ codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
+ codatatype 'a tree\<^sub>i\<^sub>s = Node\<^sub>i\<^sub>s 'a "'a tree\<^sub>i\<^sub>s fset"
+
+
+subsection {* Command Syntax
+ \label{ssec:codatatype-command-syntax} *}
+
+
+subsubsection {* \keyw{codatatype}
+ \label{sssec:codatatype} *}
+
+text {*
+Definitions of codatatypes have almost exactly the same syntax as for datatypes
+(Section~\ref{ssec:datatype-command-syntax}), with two exceptions: The command
+is called @{command codatatype}. The @{text "no_discs_sels"} option is not
+available, because destructors are a crucial notion for codatatypes.
*}
-subsection {* Examples
- \label{ssec:codatatype-examples} *}
+subsection {* Generated Constants
+ \label{ssec:codatatype-generated-constants} *}
text {*
-More examples in \verb|~~/src/HOL/BNF/Examples|.
+Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
+with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
+\ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
+datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
+iterator and the recursor are replaced by dual concepts:
+
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\item \relax{Coiterator}: @{text t_unfold}
+
+\item \relax{Corecursor}: @{text t_corec}
+
+\end{itemize}
+*}
+
+
+subsection {* Generated Theorems
+ \label{ssec:codatatype-generated-theorems} *}
+
+text {*
+The characteristic theorems generated by @{command codatatype} are grouped in
+three broad categories:
+
+\begin{itemize}
+\item The \emph{free constructor theorems} are properties about the constructors
+and destructors that can be derived for any freely generated type.
+
+\item The \emph{functorial theorems} are properties of datatypes related to
+their BNF nature.
+
+\item The \emph{coinductive theorems} are properties of datatypes related to
+their coinductive nature.
+\end{itemize}
+
+\noindent
+The first two categories are exactly as for datatypes and are described in
+Sections \ref{ssec:free-constructor-theorems}~and~\ref{ssec:functorial-theorems}.
*}
-subsection {* Syntax
- \label{ssec:codatatype-syntax} *}
+subsubsection {* Coinductive Theorems
+ \label{sssec:coinductive-theorems} *}
text {*
-Definitions of codatatypes have almost exactly the same syntax as for datatypes
-(Section~\ref{ssec:datatype-syntax}), with two exceptions: The command is called
-@{command codatatype}; the \keyw{no\_discs\_sels} option is not available,
-because destructors are a central notion for codatatypes.
+The coinductive theorems are as follows:
+
+% [(coinductN, map single coinduct_thms,
+% fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
+% (corecN, corec_thmss, K coiter_attrs),
+% (disc_corecN, disc_corec_thmss, K disc_coiter_attrs),
+% (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs),
+% (disc_unfoldN, disc_unfold_thmss, K disc_coiter_attrs),
+% (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_coiter_iff_attrs),
+% (sel_corecN, sel_corec_thmss, K sel_coiter_attrs),
+% (sel_unfoldN, sel_unfold_thmss, K sel_coiter_attrs),
+% (simpsN, simp_thmss, K []),
+% (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
+% (unfoldN, unfold_thmss, K coiter_attrs)]
+% |> massage_multi_notes;
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{coinduct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
+@{thm llist.coinduct[no_vars]}
+
+\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
+Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
+prove $m$ properties simultaneously.
+
+\item[@{text "t."}\hthm{unfold} @{text "[code]"}\rmfamily:] ~ \\
+@{thm llist.unfold(1)[no_vars]} \\
+@{thm llist.unfold(2)[no_vars]}
+
+\item[@{text "t."}\hthm{corec} @{text "[code]"}\rmfamily:] ~ \\
+@{thm llist.corec(1)[no_vars]} \\
+@{thm llist.corec(2)[no_vars]}
+
+\end{description}
+\end{indentblock}
+
+\noindent
+For convenience, @{command codatatype} also provides the following collection:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
+@{text t.rel_distinct} @{text t.sets}
+
+\end{description}
+\end{indentblock}
*}
-subsection {* Generated Theorems
- \label{ssec:codatatype-generated-theorems} *}
-
section {* Defining Corecursive Functions
\label{sec:defining-corecursive-functions} *}
text {*
-This section describes how to specify corecursive functions using the
-@{command primcorec} command.
+Corecursive functions can be specified using the @{command primcorec} command.
%%% TODO: partial_function? E.g. for defining tail recursive function on lazy
%%% lists (cf. terminal0 in TLList.thy)
*}
-subsection {* Examples
- \label{ssec:primcorec-examples} *}
+(*
+subsection {* Introductory Examples
+ \label{ssec:primcorec-introductory-examples} *}
text {*
More examples in \verb|~~/src/HOL/BNF/Examples|.
-
-Also, for default values, the same trick as for datatypes is possible for
-codatatypes (Section~\ref{ssec:recursive-default-values-for-selectors}).
*}
+*)
-subsection {* Syntax
- \label{ssec:primcorec-syntax} *}
+subsection {* Command Syntax
+ \label{ssec:primcorec-command-syntax} *}
+
+
+subsubsection {* \keyw{primcorec}
+ \label{sssec:primcorec} *}
text {*
Primitive corecursive definitions have the following general syntax:
@@ -1179,38 +1490,54 @@
*}
+(*
subsection {* Generated Theorems
\label{ssec:primcorec-generated-theorems} *}
+*)
+
+
+(*
+subsection {* Recursive Default Values for Selectors
+ \label{ssec:primcorec-recursive-default-values-for-selectors} *}
+
+text {*
+partial_function to the rescue
+*}
+*)
section {* Registering Bounded Natural Functors
\label{sec:registering-bounded-natural-functors} *}
text {*
-This section explains how to set up the (co)datatype package to allow nested
-recursion through custom well-behaved type constructors. The key concept is that
-of a bounded natural functor (BNF).
+The (co)datatype package can be set up to allow nested recursion through custom
+well-behaved type constructors. The key concept is that of a bounded natural
+functor (BNF).
- * @{command bnf}
- * @{command print_bnfs}
*}
-subsection {* Example
- \label{ssec:bnf-examples} *}
+(*
+subsection {* Introductory Example
+ \label{ssec:bnf-introductory-example} *}
text {*
More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
\verb|~~/src/HOL/BNF/More_BNFs.thy|.
-Mention distinction between live and dead type arguments;
- * and existence of map, set for those
-mention =>.
+%Mention distinction between live and dead type arguments;
+% * and existence of map, set for those
+%mention =>.
*}
+*)
-subsection {* Syntax
- \label{ssec:bnf-syntax} *}
+subsection {* Command Syntax
+ \label{ssec:bnf-command-syntax} *}
+
+
+subsubsection {* \keyw{bnf}
+ \label{sssec:bnf} *}
text {*
@{rail "
@@ -1219,35 +1546,49 @@
;
X_list: '[' (X + ',') ']'
"}
-
-options: no_discs_sels rep_compat
*}
-section {* Generating Destructors and Theorems for Free Constructors
- \label{sec:generating-destructors-and-theorems-for-free-constructors} *}
+
+subsubsection {* \keyw{print\_bnfs}
+ \label{sssec:print-bnfs} *}
text {*
-This section explains how to derive convenience theorems for free constructors,
-as performed internally by @{command datatype_new} and @{command codatatype}.
-
- * need for this is rare but may arise if you want e.g. to add destructors to
- a type not introduced by ...
-
- * also useful for compatibility with old package, e.g. add destructors to
- old \keyw{datatype}
-
- * @{command wrap_free_constructors}
- * \keyw{no\_discs\_sels}, \keyw{rep\_compat}
- * hack to have both co and nonco view via locale (cf. ext nats)
+@{command print_bnfs}
*}
-subsection {* Example
- \label{ssec:ctors-examples} *}
+section {* Deriving Destructors and Theorems for Free Constructors
+ \label{sec:deriving-destructors-and-theorems-for-free-constructors} *}
+
+text {*
+The derivation of convenience theorems for types equipped with free constructors,
+as performed internally by @{command datatype_new} and @{command codatatype},
+is available as a stand-alone command called @{command wrap_free_constructors}.
+
+% * need for this is rare but may arise if you want e.g. to add destructors to
+% a type not introduced by ...
+%
+% * also useful for compatibility with old package, e.g. add destructors to
+% old \keyw{datatype}
+%
+% * @{command wrap_free_constructors}
+% * @{text "no_discs_sels"}, @{text "rep_compat"}
+% * hack to have both co and nonco view via locale (cf. ext nats)
+*}
-subsection {* Syntax
- \label{ssec:ctors-syntax} *}
+(*
+subsection {* Introductory Example
+ \label{ssec:ctors-introductory-example} *}
+*)
+
+
+subsection {* Command Syntax
+ \label{ssec:ctors-command-syntax} *}
+
+
+subsubsection {* \keyw{wrap\_free\_constructors}
+ \label{sssec:wrap-free-constructors} *}
text {*
Free constructor wrapping has the following general syntax:
@@ -1261,29 +1602,31 @@
@{syntax_def name_term}: (name ':' term)
"}
-options: no_discs_sels rep_compat
+% options: no_discs_sels rep_compat
-X_list is as for BNF
+% X_list is as for BNF
Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
*}
+(*
section {* Standard ML Interface
\label{sec:standard-ml-interface} *}
text {*
-This section describes the package's programmatic interface.
+The package's programmatic interface.
*}
+*)
+(*
section {* Interoperability
\label{sec:interoperability} *}
text {*
-This section is concerned with the packages' interaction with other Isabelle
-packages and tools, such as the code generator and the counterexample
-generators.
+The package's interaction with other Isabelle packages and tools, such as the
+code generator and the counterexample generators.
*}
@@ -1305,37 +1648,36 @@
subsection {* Nominal Isabelle
\label{ssec:nominal-isabelle} *}
+*)
+(*
section {* Known Bugs and Limitations
\label{sec:known-bugs-and-limitations} *}
text {*
-This section lists known open issues of the package.
+Known open issues of the package.
*}
text {*
-* primcorec is unfinished
-
-* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
-
-* issues with HOL-Proofs?
-
-* partial documentation
-
-* too much output by commands like "datatype_new" and "codatatype"
-
-* no direct way to define recursive functions for default values -- but show trick
- based on overloading
-
-* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
- (for @{command datatype_new_compat} and prim(co)rec)
-
-* no way to register same type as both data- and codatatype?
-
-* no recursion through unused arguments (unlike with the old package)
-
-* in a locale, cannot use locally fixed types (because of limitation in typedef)?
+%* primcorec is unfinished
+%
+%* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
+%
+%* issues with HOL-Proofs?
+%
+%* partial documentation
+%
+%* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
+% (for @{command datatype_new_compat} and prim(co)rec)
+%
+% * a fortiori, no way to register same type as both data- and codatatype
+%
+%* no recursion through unused arguments (unlike with the old package)
+%
+%* in a locale, cannot use locally fixed types (because of limitation in typedef)?
+%
+% *names of variables suboptimal
*}
@@ -1343,13 +1685,15 @@
\label{sec:acknowledgments} *}
text {*
-Tobias Nipkow and Makarius Wenzel made this work possible. Andreas Lochbihler
-provided lots of comments on earlier versions of the package, especially for the
-coinductive part. Brian Huffman suggested major simplifications to the internal
-constructions, much of which has yet to be implemented. Florian Haftmann and
-Christian Urban provided general advice advice on Isabelle and package writing.
-Stefan Milius and Lutz Schr\"oder suggested an elegant proof to eliminate one of
-the BNF assumptions.
+Tobias Nipkow and Makarius Wenzel have encouraged us to implement the new
+(co)datatype package. Andreas Lochbihler provided lots of comments on earlier
+versions of the package, especially for the coinductive part. Brian Huffman
+suggested major simplifications to the internal constructions, much of which has
+yet to be implemented. Florian Haftmann and Christian Urban provided general
+advice advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder
+suggested an elegant proof to eliminate one of the BNF assumptions.
*}
+*)
+
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Sep 13 22:31:56 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Sep 13 22:33:16 2013 +0200
@@ -20,6 +20,9 @@
lemma linear_scaleR: "linear (\<lambda>x. scaleR c x)"
by (simp add: linear_iff scaleR_add_right)
+lemma linear_scaleR_left: "linear (\<lambda>r. scaleR r x)"
+ by (simp add: linear_iff scaleR_add_left)
+
lemma injective_scaleR: "c \<noteq> 0 \<Longrightarrow> inj (\<lambda>x::'a::real_vector. scaleR c x)"
by (simp add: inj_on_def)
@@ -1405,7 +1408,7 @@
assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
using uv yz
- using convex_distance[of "ball x e" x, unfolded convex_on_def,
+ using convex_on_dist [of "ball x e" x, unfolded convex_on_def,
THEN bspec[where x=y], THEN bspec[where x=z]]
by auto
then show "dist x (u *\<^sub>R y + v *\<^sub>R z) < e"
@@ -1423,7 +1426,7 @@
assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z"
using uv yz
- using convex_distance[of "cball x e" x, unfolded convex_on_def,
+ using convex_on_dist [of "cball x e" x, unfolded convex_on_def,
THEN bspec[where x=y], THEN bspec[where x=z]]
by auto
then have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e"
@@ -1478,33 +1481,60 @@
subsubsection {* Convex hull is "preserved" by a linear function *}
lemma convex_hull_linear_image:
- assumes "bounded_linear f"
+ assumes f: "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 \<in> convex hull f ` s}"
- unfolding convex_def
- by (auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format])
- show "convex {x. x \<in> f ` (convex hull s)}"
- using convex_convex_hull[unfolded convex_def, of s]
- unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
-qed auto
+proof
+ show "convex hull (f ` s) \<subseteq> f ` (convex hull s)"
+ by (intro hull_minimal image_mono hull_subset convex_linear_image assms convex_convex_hull)
+ show "f ` (convex hull s) \<subseteq> convex hull (f ` s)"
+ proof (unfold image_subset_iff_subset_vimage, rule hull_minimal)
+ show "s \<subseteq> f -` (convex hull (f ` s))"
+ by (fast intro: hull_inc)
+ show "convex (f -` (convex hull (f ` s)))"
+ by (intro convex_linear_vimage [OF f] convex_convex_hull)
+ qed
+qed
lemma in_convex_hull_linear_image:
- assumes "bounded_linear f"
+ assumes "linear f"
and "x \<in> convex hull s"
shows "f x \<in> convex hull (f ` s)"
using convex_hull_linear_image[OF assms(1)] assms(2) by auto
+lemma convex_hull_Times:
+ "convex hull (s \<times> t) = (convex hull s) \<times> (convex hull t)"
+proof
+ show "convex hull (s \<times> t) \<subseteq> (convex hull s) \<times> (convex hull t)"
+ by (intro hull_minimal Sigma_mono hull_subset convex_Times convex_convex_hull)
+ have "\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)"
+ proof (intro hull_induct)
+ fix x y assume "x \<in> s" and "y \<in> t"
+ then show "(x, y) \<in> convex hull (s \<times> t)"
+ by (simp add: hull_inc)
+ next
+ fix x let ?S = "((\<lambda>y. (0, y)) -` (\<lambda>p. (- x, 0) + p) ` (convex hull s \<times> t))"
+ have "convex ?S"
+ by (intro convex_linear_vimage convex_translation convex_convex_hull,
+ simp add: linear_iff)
+ also have "?S = {y. (x, y) \<in> convex hull (s \<times> t)}"
+ by (auto simp add: uminus_add_conv_diff image_def Bex_def)
+ finally show "convex {y. (x, y) \<in> convex hull (s \<times> t)}" .
+ next
+ show "convex {x. \<forall>y\<in>convex hull t. (x, y) \<in> convex hull (s \<times> t)}"
+ proof (unfold Collect_ball_eq, rule convex_INT [rule_format])
+ fix y let ?S = "((\<lambda>x. (x, 0)) -` (\<lambda>p. (0, - y) + p) ` (convex hull s \<times> t))"
+ have "convex ?S"
+ by (intro convex_linear_vimage convex_translation convex_convex_hull,
+ simp add: linear_iff)
+ also have "?S = {x. (x, y) \<in> convex hull (s \<times> t)}"
+ by (auto simp add: uminus_add_conv_diff image_def Bex_def)
+ finally show "convex {x. (x, y) \<in> convex hull (s \<times> t)}" .
+ qed
+ qed
+ then show "(convex hull s) \<times> (convex hull t) \<subseteq> convex hull (s \<times> t)"
+ unfolding subset_eq split_paired_Ball_Sigma .
+qed
+
subsubsection {* Stepping theorems for convex hulls of finite sets *}
@@ -5693,36 +5723,34 @@
apply auto
done
-(* FIXME: rewrite these lemmas without using vec1
-subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
+subsection {* On @{text "real"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
lemma is_interval_1:
- "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"
- unfolding is_interval_def forall_1 by auto
-
-lemma is_interval_connected_1: "is_interval s \<longleftrightarrow> connected (s::(real^1) set)"
+ "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
+ unfolding is_interval_def by auto
+
+lemma is_interval_connected_1: "is_interval s \<longleftrightarrow> connected (s::real set)"
apply(rule, rule is_interval_connected, assumption) unfolding is_interval_1
apply(rule,rule,rule,rule,erule conjE,rule ccontr) proof-
- fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "dest_vec1 a \<le> dest_vec1 x" "dest_vec1 x \<le> dest_vec1 b" "x\<notin>s"
- hence *:"dest_vec1 a < dest_vec1 x" "dest_vec1 x < dest_vec1 b" apply(rule_tac [!] ccontr) unfolding not_less by auto
- let ?halfl = "{z. inner (basis 1) z < dest_vec1 x} " and ?halfr = "{z. inner (basis 1) z > dest_vec1 x} "
- { fix y assume "y \<in> s" have "y \<in> ?halfr \<union> ?halfl" apply(rule ccontr)
- using as(6) `y\<in>s` by (auto simp add: inner_vector_def) }
- moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def)
+ fix a b x assume as:"connected s" "a \<in> s" "b \<in> s" "a \<le> x" "x \<le> b" "x\<notin>s"
+ hence *:"a < x" "x < b" unfolding not_le [symmetric] by auto
+ let ?halfl = "{..<x} " and ?halfr = "{x<..} "
+ { fix y assume "y \<in> s" with `x \<notin> s` have "x \<noteq> y" by auto
+ then have "y \<in> ?halfr \<union> ?halfl" by auto }
+ moreover have "a\<in>?halfl" "b\<in>?halfr" using * by auto
hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" using as(2-3) by auto
ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]])
apply(rule_tac x="?halfl" in exI, rule_tac x="?halfr" in exI)
- apply(rule, rule open_halfspace_lt, rule, rule open_halfspace_gt)
- by(auto simp add: field_simps) qed
+ apply(rule, rule open_lessThan, rule, rule open_greaterThan)
+ by auto qed
lemma is_interval_convex_1:
- "is_interval s \<longleftrightarrow> convex (s::(real^1) set)"
+ "is_interval s \<longleftrightarrow> convex (s::real set)"
by(metis is_interval_convex convex_connected is_interval_connected_1)
lemma convex_connected_1:
- "connected s \<longleftrightarrow> convex (s::(real^1) set)"
+ "connected s \<longleftrightarrow> convex (s::real set)"
by(metis is_interval_convex convex_connected is_interval_connected_1)
-*)
subsection {* Another intermediate value theorem formulation *}
@@ -5800,7 +5828,93 @@
qed
lemma inner_setsum_Basis[simp]: "i \<in> Basis \<Longrightarrow> (\<Sum>Basis) \<bullet> i = 1"
- by (simp add: One_def inner_setsum_left setsum_cases inner_Basis)
+ by (simp add: inner_setsum_left setsum_cases inner_Basis)
+
+lemma convex_set_plus:
+ assumes "convex s" and "convex t" shows "convex (s + t)"
+proof -
+ have "convex {x + y |x y. x \<in> s \<and> y \<in> t}"
+ using assms by (rule convex_sums)
+ moreover have "{x + y |x y. x \<in> s \<and> y \<in> t} = s + t"
+ unfolding set_plus_def by auto
+ finally show "convex (s + t)" .
+qed
+
+lemma finite_set_setsum:
+ assumes "finite A" and "\<forall>i\<in>A. finite (B i)" shows "finite (\<Sum>i\<in>A. B i)"
+ using assms by (induct set: finite, simp, simp add: finite_set_plus)
+
+lemma set_setsum_eq:
+ "finite A \<Longrightarrow> (\<Sum>i\<in>A. B i) = {\<Sum>i\<in>A. f i |f. \<forall>i\<in>A. f i \<in> B i}"
+ apply (induct set: finite)
+ apply simp
+ apply simp
+ apply (safe elim!: set_plus_elim)
+ apply (rule_tac x="fun_upd f x a" in exI)
+ apply simp
+ apply (rule_tac f="\<lambda>x. a + x" in arg_cong)
+ apply (rule setsum_cong [OF refl])
+ apply clarsimp
+ apply (fast intro: set_plus_intro)
+ done
+
+lemma box_eq_set_setsum_Basis:
+ shows "{x. \<forall>i\<in>Basis. x\<bullet>i \<in> B i} = (\<Sum>i\<in>Basis. image (\<lambda>x. x *\<^sub>R i) (B i))"
+ apply (subst set_setsum_eq [OF finite_Basis])
+ apply safe
+ apply (fast intro: euclidean_representation [symmetric])
+ apply (subst inner_setsum_left)
+ apply (subgoal_tac "(\<Sum>x\<in>Basis. f x \<bullet> i) = f i \<bullet> i")
+ apply (drule (1) bspec)
+ apply clarsimp
+ apply (frule setsum_diff1' [OF finite_Basis])
+ apply (erule trans)
+ apply simp
+ apply (rule setsum_0')
+ apply clarsimp
+ apply (frule_tac x=i in bspec, assumption)
+ apply (drule_tac x=x in bspec, assumption)
+ apply clarsimp
+ apply (cut_tac u=x and v=i in inner_Basis, assumption+)
+ apply (rule ccontr)
+ apply simp
+ done
+
+lemma convex_hull_set_plus:
+ "convex hull (s + t) = convex hull s + convex hull t"
+ unfolding set_plus_image
+ apply (subst convex_hull_linear_image [symmetric])
+ apply (simp add: linear_iff scaleR_right_distrib)
+ apply (simp add: convex_hull_Times)
+ done
+
+lemma convex_hull_set_setsum:
+ "convex hull (\<Sum>i\<in>A. B i) = (\<Sum>i\<in>A. convex hull (B i))"
+proof (cases "finite A")
+ assume "finite A" then show ?thesis
+ by (induct set: finite, simp, simp add: convex_hull_set_plus)
+qed simp
+
+lemma bounded_linear_imp_linear: "bounded_linear f \<Longrightarrow> linear f" (* TODO: move elsewhere *)
+proof -
+ assume "bounded_linear f"
+ then interpret f: bounded_linear f .
+ show "linear f"
+ by (simp add: f.add f.scaleR linear_iff)
+qed
+
+lemma convex_hull_eq_real_interval:
+ fixes x y :: real assumes "x \<le> y"
+ shows "convex hull {x, y} = {x..y}"
+proof (rule hull_unique)
+ show "{x, y} \<subseteq> {x..y}" using `x \<le> y` by auto
+ show "convex {x..y}" by (rule convex_interval)
+next
+ fix s assume "{x, y} \<subseteq> s" and "convex s"
+ then show "{x..y} \<subseteq> s"
+ unfolding is_interval_convex_1 [symmetric] is_interval_def Basis_real_def
+ by - (clarify, simp (no_asm_use), fast)
+qed
lemma unit_interval_convex_hull:
defines "One \<equiv> \<Sum>Basis"
@@ -5809,145 +5923,21 @@
proof -
have One[simp]: "\<And>i. i \<in> Basis \<Longrightarrow> One \<bullet> i = 1"
by (simp add: One_def inner_setsum_left setsum_cases inner_Basis)
- have 01: "{0,One} \<subseteq> convex hull ?points"
- apply rule
- apply (rule_tac hull_subset[unfolded subset_eq, rule_format])
- apply auto
- done
- {
- fix n x
- assume "x \<in> {0::'a::ordered_euclidean_space .. One}"
- "n \<le> DIM('a)" "card {i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0} \<le> n"
- then have "x \<in> convex hull ?points"
- proof (induct n arbitrary: x)
- case 0
- then have "x = 0"
- apply (subst euclidean_eq_iff)
- apply rule
- apply auto
- done
- then show "x\<in>convex hull ?points" using 01 by auto
- next
- case (Suc n)
- show "x\<in>convex hull ?points"
- proof (cases "{i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0} = {}")
- case True
- then have "x = 0"
- apply (subst euclidean_eq_iff)
- apply auto
- done
- then show "x\<in>convex hull ?points"
- using 01 by auto
- next
- case False
- def xi \<equiv> "Min ((\<lambda>i. x\<bullet>i) ` {i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0})"
- have "xi \<in> (\<lambda>i. x\<bullet>i) ` {i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0}"
- unfolding xi_def
- apply (rule Min_in)
- using False
- apply auto
- done
- then obtain i where i': "x\<bullet>i = xi" "x\<bullet>i \<noteq> 0" "i\<in>Basis"
- by auto
- have i: "\<And>j. j\<in>Basis \<Longrightarrow> x\<bullet>j > 0 \<Longrightarrow> x\<bullet>i \<le> x\<bullet>j"
- unfolding i'(1) xi_def
- apply (rule_tac Min_le)
- unfolding image_iff
- defer
- apply (rule_tac x=j in bexI)
- using i'
- apply auto
- done
- have i01: "x\<bullet>i \<le> 1" "x\<bullet>i > 0"
- using Suc(2)[unfolded mem_interval,rule_format,of i]
- using i'(2-) `x\<bullet>i \<noteq> 0`
- by auto
- show ?thesis
- proof (cases "x\<bullet>i = 1")
- case True
- have "\<forall>j\<in>{i. i\<in>Basis \<and> x\<bullet>i \<noteq> 0}. x\<bullet>j = 1"
- apply rule
- apply (rule ccontr)
- unfolding mem_Collect_eq
- proof (erule conjE)
- fix j
- assume as: "x \<bullet> j \<noteq> 0" "x \<bullet> j \<noteq> 1" "j \<in> Basis"
- then have j: "x\<bullet>j \<in> {0<..<1}" using Suc(2)
- by (auto simp add: eucl_le[where 'a='a] elim!:allE[where x=j])
- then have "x\<bullet>j \<in> op \<bullet> x ` {i. i\<in>Basis \<and> x \<bullet> i \<noteq> 0}"
- using as(3) by auto
- then have "x\<bullet>j \<ge> x\<bullet>i"
- unfolding i'(1) xi_def
- apply (rule_tac Min_le)
- apply auto
- done
- then show False
- using True Suc(2) j
- by (auto simp add: elim!:ballE[where x=j])
- qed
- then show "x \<in> convex hull ?points"
- apply (rule_tac hull_subset[unfolded subset_eq, rule_format])
- apply auto
- done
- next
- let ?y = "\<Sum>j\<in>Basis. (if x\<bullet>j = 0 then 0 else (x\<bullet>j - x\<bullet>i) / (1 - x\<bullet>i)) *\<^sub>R j"
- case False
- then have *: "x = (x\<bullet>i) *\<^sub>R (\<Sum>j\<in>Basis. (if x\<bullet>j = 0 then 0 else 1) *\<^sub>R j) + (1 - x\<bullet>i) *\<^sub>R ?y"
- by (subst euclidean_eq_iff) (simp add: inner_simps)
- {
- fix j :: 'a
- assume j: "j \<in> Basis"
- have "x\<bullet>j \<noteq> 0 \<Longrightarrow> 0 \<le> (x \<bullet> j - x \<bullet> i) / (1 - x \<bullet> i)" "(x \<bullet> j - x \<bullet> i) / (1 - x \<bullet> i) \<le> 1"
- apply (rule_tac divide_nonneg_pos)
- using i(1)[of j]
- using False i01
- using Suc(2)[unfolded mem_interval, rule_format, of j]
- using j
- by (auto simp add: field_simps)
- with j have "0 \<le> ?y \<bullet> j \<and> ?y \<bullet> j \<le> 1"
- by (auto simp: inner_simps)
- }
- moreover have "i\<in>{j. j\<in>Basis \<and> x\<bullet>j \<noteq> 0} - {j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0}"
- using i01 using i'(3) by auto
- then have "{j. j\<in>Basis \<and> x\<bullet>j \<noteq> 0} \<noteq> {j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0}"
- using i'(3) by blast
- then have **: "{j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0} \<subset> {j. j\<in>Basis \<and> x\<bullet>j \<noteq> 0}"
- by auto
- have "card {j. j\<in>Basis \<and> ?y \<bullet> j \<noteq> 0} \<le> n"
- using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
- ultimately show ?thesis
- apply (subst *)
- apply (rule convex_convex_hull[unfolded convex_def, rule_format])
- apply (rule_tac hull_subset[unfolded subset_eq, rule_format])
- defer
- apply (rule Suc(1))
- unfolding mem_interval
- using i01 Suc(3)
- by auto
- qed
- qed
- qed
- } note * = this
- show ?thesis
- apply rule
- defer
- apply (rule hull_minimal)
- unfolding subset_eq
- prefer 3
- apply rule
- apply (rule_tac n2="DIM('a)" in *)
- prefer 3
- apply (rule card_mono)
- using 01 and convex_interval(1)
- prefer 5
- apply -
- apply rule
- unfolding mem_interval
- apply rule
- unfolding mem_Collect_eq
- apply (erule_tac x=i in ballE)
- apply auto
- done
+ have "?int = {x. \<forall>i\<in>Basis. x \<bullet> i \<in> {0..1}}"
+ by (auto simp add: eucl_le [where 'a='a])
+ also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` {0..1})"
+ by (simp only: box_eq_set_setsum_Basis)
+ also have "\<dots> = (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` (convex hull {0, 1}))"
+ by (simp only: convex_hull_eq_real_interval zero_le_one)
+ also have "\<dots> = (\<Sum>i\<in>Basis. convex hull ((\<lambda>x. x *\<^sub>R i) ` {0, 1}))"
+ by (simp only: convex_hull_linear_image linear_scaleR_left)
+ also have "\<dots> = convex hull (\<Sum>i\<in>Basis. (\<lambda>x. x *\<^sub>R i) ` {0, 1})"
+ by (simp only: convex_hull_set_setsum)
+ also have "\<dots> = convex hull {x. \<forall>i\<in>Basis. x\<bullet>i \<in> {0, 1}}"
+ by (simp only: box_eq_set_setsum_Basis)
+ also have "convex hull {x. \<forall>i\<in>Basis. x\<bullet>i \<in> {0, 1}} = convex hull ?points"
+ by simp
+ finally show ?thesis .
qed
text {* And this is a finite set of vertices. *}
@@ -6201,8 +6191,7 @@
by auto
lemma convex_on_continuous:
- assumes "open (s::('a::ordered_euclidean_space) set)" "convex_on s f"
- (* FIXME: generalize to euclidean_space *)
+ assumes "open (s::('a::euclidean_space) set)" "convex_on s f"
shows "continuous_on s f"
unfolding continuous_on_eq_continuous_at[OF assms(1)]
proof
@@ -6218,34 +6207,54 @@
apply auto
done
let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
- obtain c where c: "finite c" "{x - ?d..x + ?d} = convex hull c"
- using cube_convex_hull[OF `d>0`, of x] by auto
- have "x \<in> {x - ?d..x + ?d}"
- using `d > 0` unfolding mem_interval by (auto simp: inner_setsum_left_Basis inner_simps)
- then have "c \<noteq> {}" using c by auto
+ obtain c
+ where c: "finite c"
+ and c1: "convex hull c \<subseteq> cball x e"
+ and c2: "cball x d \<subseteq> convex hull c"
+ proof
+ def c \<equiv> "\<Sum>i\<in>Basis. (\<lambda>a. a *\<^sub>R i) ` {x\<bullet>i - d, x\<bullet>i + d}"
+ show "finite c"
+ unfolding c_def by (simp add: finite_set_setsum)
+ have 1: "convex hull c = {a. \<forall>i\<in>Basis. a \<bullet> i \<in> {x \<bullet> i - d..x \<bullet> i + d}}"
+ unfolding box_eq_set_setsum_Basis
+ unfolding c_def convex_hull_set_setsum
+ apply (subst convex_hull_linear_image [symmetric])
+ apply (simp add: linear_iff scaleR_add_left)
+ apply (rule setsum_cong [OF refl])
+ apply (rule image_cong [OF _ refl])
+ apply (rule convex_hull_eq_real_interval)
+ apply (cut_tac `0 < d`, simp)
+ done
+ then have 2: "convex hull c = {a. \<forall>i\<in>Basis. a \<bullet> i \<in> cball (x \<bullet> i) d}"
+ by (simp add: dist_norm abs_le_iff algebra_simps)
+ show "cball x d \<subseteq> convex hull c"
+ unfolding 2
+ apply clarsimp
+ apply (simp only: dist_norm)
+ apply (subst inner_diff_left [symmetric])
+ apply simp
+ apply (erule (1) order_trans [OF Basis_le_norm])
+ done
+ have e': "e = (\<Sum>(i::'a)\<in>Basis. d)"
+ by (simp add: d_def real_of_nat_def DIM_positive)
+ show "convex hull c \<subseteq> cball x e"
+ unfolding 2
+ apply clarsimp
+ apply (subst euclidean_dist_l2)
+ apply (rule order_trans [OF setL2_le_setsum])
+ apply (rule zero_le_dist)
+ unfolding e'
+ apply (rule setsum_mono)
+ apply simp
+ done
+ qed
def k \<equiv> "Max (f ` c)"
- have "convex_on {x - ?d..x + ?d} f"
+ have "convex_on (convex hull c) f"
apply(rule convex_on_subset[OF assms(2)])
apply(rule subset_trans[OF _ e(1)])
- unfolding subset_eq mem_cball
- proof
- fix z
- assume z: "z \<in> {x - ?d..x + ?d}"
- have e: "e = setsum (\<lambda>i::'a. d) Basis"
- unfolding setsum_constant d_def
- using dimge1
- unfolding real_eq_of_nat
- by auto
- show "dist x z \<le> e"
- unfolding dist_norm e
- apply (rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
- using z[unfolded mem_interval]
- apply (erule_tac x=b in ballE)
- apply (auto simp: inner_simps)
- done
- qed
- then have k: "\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k"
- unfolding c(2)
+ apply(rule c1)
+ done
+ then have k: "\<forall>y\<in>convex hull c. f y \<le> k"
apply (rule_tac convex_on_convex_hull_bound)
apply assumption
unfolding k_def
@@ -6261,33 +6270,20 @@
apply (auto simp: real_of_nat_ge_one_iff Suc_le_eq DIM_positive)
done
then have dsube: "cball x d \<subseteq> cball x e"
- unfolding subset_eq Ball_def mem_cball by auto
+ by (rule subset_cball)
have conv: "convex_on (cball x d) f"
apply (rule convex_on_subset)
apply (rule convex_on_subset[OF assms(2)])
apply (rule e(1))
- using dsube
- apply auto
+ apply (rule dsube)
done
then have "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)"
- apply (rule_tac convex_bounds_lemma)
- apply assumption
- proof
- fix y
- assume y: "y \<in> cball x d"
- {
- fix i :: 'a
- assume "i \<in> Basis"
- then have "x \<bullet> i - d \<le> y \<bullet> i" "y \<bullet> i \<le> x \<bullet> i + d"
- using order_trans[OF Basis_le_norm y[unfolded mem_cball dist_norm], of i]
- by (auto simp: inner_diff_left)
- }
- then show "f y \<le> k"
- apply (rule_tac k[rule_format])
- unfolding mem_cball mem_interval dist_norm
- apply (auto simp: inner_simps)
- done
- qed
+ apply (rule convex_bounds_lemma)
+ apply (rule ballI)
+ apply (rule k [rule_format])
+ apply (erule rev_subsetD)
+ apply (rule c2)
+ done
then have "continuous_on (ball x d) f"
apply (rule_tac convex_on_bounded_continuous)
apply (rule open_ball, rule convex_on_subset[OF conv])
@@ -7147,7 +7143,7 @@
using fd linear_0 by auto
then have "(convex hull (insert 0 d)) = f ` (convex hull (insert 0 B))"
using convex_hull_linear_image[of f "(insert 0 d)"]
- convex_hull_linear_image[of f "(insert 0 B)"] `bounded_linear f`
+ convex_hull_linear_image[of f "(insert 0 B)"] `linear f`
by auto
moreover have "rel_interior (f ` (convex hull insert 0 B)) =
f ` rel_interior (convex hull insert 0 B)"
@@ -8019,8 +8015,8 @@
by auto
then have "rel_interior (f ` S) = rel_interior (f ` rel_interior S)"
using assms convex_rel_interior
- linear_conv_bounded_linear[of f] convex_linear_image[of S]
- convex_linear_image[of "rel_interior S"]
+ linear_conv_bounded_linear[of f] convex_linear_image[of _ S]
+ convex_linear_image[of _ "rel_interior S"]
closure_eq_rel_interior_eq[of "f ` S" "f ` rel_interior S"]
by auto
then have "rel_interior (f ` S) \<subseteq> f ` rel_interior S"
@@ -8045,30 +8041,12 @@
}
then have "z \<in> rel_interior (f ` S)"
using convex_rel_interior_iff[of "f ` S" z] `convex S`
- `linear f` `S ~= {}` convex_linear_image[of S f] linear_conv_bounded_linear[of f]
+ `linear f` `S ~= {}` convex_linear_image[of f S] linear_conv_bounded_linear[of f]
by auto
}
ultimately show ?thesis by auto
qed
-
-lemma convex_linear_preimage:
- assumes c: "convex S"
- and l: "bounded_linear f"
- shows "convex (f -` S)"
-proof (auto simp add: convex_def)
- interpret f: bounded_linear f by fact
- fix x y
- assume xy: "f x \<in> S" "f y \<in> S"
- fix u v :: real
- assume uv: "0 \<le> u" "0 \<le> v" "u + v = 1"
- show "f (u *\<^sub>R x + v *\<^sub>R y) \<in> S"
- unfolding image_iff
- using bexI[of _ "u *\<^sub>R x + v *\<^sub>R y"] f.add f.scaleR c[unfolded convex_def] xy uv
- by auto
-qed
-
-
lemma rel_interior_convex_linear_preimage:
fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
assumes "linear f"
@@ -8083,7 +8061,7 @@
then have "S \<inter> (range f) \<noteq> {}"
by auto
have conv: "convex (f -` S)"
- using convex_linear_preimage assms linear_conv_bounded_linear by auto
+ using convex_linear_vimage assms by auto
then have "convex (S \<inter> range f)"
by (metis assms(1) assms(2) convex_Int subspace_UNIV subspace_imp_convex subspace_linear_image)
{
@@ -8134,112 +8112,6 @@
ultimately show ?thesis by auto
qed
-
-lemma convex_direct_sum:
- fixes S :: "'n::euclidean_space set"
- and T :: "'m::euclidean_space set"
- assumes "convex S"
- and "convex T"
- shows "convex (S \<times> T)"
-proof -
- {
- fix x
- assume "x \<in> S \<times> T"
- then obtain xs xt where xst: "xs \<in> S" "xt \<in> T" "(xs, xt) = x"
- by auto
- fix y assume "y \<in> S \<times> T"
- then obtain ys yt where yst: "ys \<in> S" "yt \<in> T" "(ys, yt) = y"
- by auto
- fix u v :: real assume uv: "u \<ge> 0 \<and> v \<ge> 0 \<and> u + v = 1"
- have "u *\<^sub>R x + v *\<^sub>R y = (u *\<^sub>R xs + v *\<^sub>R ys, u *\<^sub>R xt + v *\<^sub>R yt)"
- using xst yst by auto
- moreover have "u *\<^sub>R xs + v *\<^sub>R ys \<in> S"
- using uv xst yst convex_def[of S] assms by auto
- moreover have "u *\<^sub>R xt + v *\<^sub>R yt \<in> T"
- using uv xst yst convex_def[of T] assms by auto
- ultimately have "u *\<^sub>R x + v *\<^sub>R y \<in> S \<times> T" by auto
- }
- then show ?thesis
- unfolding convex_def by auto
-qed
-
-lemma convex_hull_direct_sum:
- fixes S :: "'n::euclidean_space set"
- and T :: "'m::euclidean_space set"
- shows "convex hull (S \<times> T) = (convex hull S) \<times> (convex hull T)"
-proof -
- {
- fix x
- assume "x \<in> (convex hull S) \<times> (convex hull T)"
- then obtain xs xt where xst: "xs \<in> convex hull S" "xt \<in> convex hull T" "(xs, xt) = x"
- by auto
- from xst obtain sI su where s: "finite sI" "sI \<subseteq> S" "\<forall>x\<in>sI. 0 \<le> su x"
- "setsum su sI = 1" "(\<Sum>v\<in>sI. su v *\<^sub>R v) = xs"
- using convex_hull_explicit[of S] by auto
- from xst obtain tI tu where t: "finite tI" "tI \<le> T" "\<forall>x\<in>tI. 0 \<le> tu x"
- "setsum tu tI = 1" "(\<Sum>v\<in>tI. tu v *\<^sub>R v) = xt"
- using convex_hull_explicit[of T] by auto
- def I \<equiv> "sI \<times> tI"
- def u \<equiv> "\<lambda>i. su (fst i) * tu (snd i)"
- have "fst (\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) =
- (\<Sum>vs\<in>sI. \<Sum>vt\<in>tI. (su vs * tu vt) *\<^sub>R vs)"
- using fst_setsum[of "(\<lambda>v. (su (fst v) * tu (snd v)) *\<^sub>R v)" "sI \<times> tI"]
- by (simp add: split_def scaleR_prod_def setsum_cartesian_product)
- also have "\<dots> = (\<Sum>vt\<in>tI. tu vt *\<^sub>R (\<Sum>vs\<in>sI. su vs *\<^sub>R vs))"
- using setsum_commute[of "(\<lambda>vt vs. (su vs * tu vt) *\<^sub>R vs)" sI tI]
- by (simp add: mult_commute scaleR_right.setsum)
- also have "\<dots> = (\<Sum>vt\<in>tI. tu vt *\<^sub>R xs)"
- using s by auto
- also have "\<dots> = (\<Sum>vt\<in>tI. tu vt) *\<^sub>R xs"
- by (simp add: scaleR_left.setsum)
- also have "\<dots> = xs"
- using t by auto
- finally have h1: "fst (\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v)=xs"
- by auto
- have "snd (\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) =
- (\<Sum>vs\<in>sI. \<Sum>vt\<in>tI. (su vs * tu vt) *\<^sub>R vt)"
- using snd_setsum[of "(\<lambda>v. (su (fst v) * tu (snd v)) *\<^sub>R v)" "sI \<times> tI"]
- by (simp add: split_def scaleR_prod_def setsum_cartesian_product)
- also have "\<dots> = (\<Sum>vs\<in>sI. su vs *\<^sub>R (\<Sum>vt\<in>tI. tu vt *\<^sub>R vt))"
- by (simp add: mult_commute scaleR_right.setsum)
- also have "\<dots> = (\<Sum>vs\<in>sI. su vs *\<^sub>R xt)"
- using t by auto
- also have "\<dots> = (\<Sum>vs\<in>sI. su vs) *\<^sub>R xt"
- by (simp add: scaleR_left.setsum)
- also have "\<dots> = xt"
- using s by auto
- finally have h2: "snd (\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) = xt"
- by auto
- from h1 h2 have "(\<Sum>v\<in>sI \<times> tI. (su (fst v) * tu (snd v)) *\<^sub>R v) = x"
- using xst by auto
-
- moreover have "finite I" "I \<subseteq> S \<times> T"
- using s t I_def by auto
- moreover have "\<forall>i\<in>I. 0 \<le> u i"
- using s t I_def u_def by (simp add: mult_nonneg_nonneg)
- moreover have "setsum u I = 1"
- using u_def I_def setsum_cartesian_product[of "\<lambda>x y. su x * tu y"]
- s t setsum_product[of su sI tu tI]
- by (auto simp add: split_def)
- ultimately have "x \<in> convex hull (S \<times> T)"
- apply (subst convex_hull_explicit[of "S \<times> T"])
- apply rule
- apply (rule_tac x="I" in exI)
- apply (rule_tac x="u" in exI)
- using I_def u_def
- apply auto
- done
- }
- then have "convex hull (S \<times> T) \<supseteq> (convex hull S) \<times> (convex hull T)"
- by auto
- moreover have "convex ((convex hull S) \<times> (convex hull T))"
- by (simp add: convex_direct_sum convex_convex_hull)
- ultimately show ?thesis
- using hull_minimal[of "S \<times> T" "(convex hull S) \<times> (convex hull T)" "convex"]
- hull_subset[of S convex] hull_subset[of T convex]
- by auto
-qed
-
lemma rel_interior_direct_sum:
fixes S :: "'n::euclidean_space set"
and T :: "'m::euclidean_space set"
@@ -8289,7 +8161,7 @@
by auto
also have "\<dots> = rel_interior (S \<times> (UNIV :: 'm set)) \<inter> rel_interior ((UNIV :: 'n set) \<times> T)"
apply (subst convex_rel_interior_inter_two[of "S \<times> (UNIV :: 'm set)" "(UNIV :: 'n set) <*> T"])
- using * ri assms convex_direct_sum
+ using * ri assms convex_Times
apply auto
done
finally have ?thesis using * by auto
@@ -8366,7 +8238,7 @@
using rel_interior_convex_linear_preimage[of f S]
by auto
then show ?thesis
- using convex_linear_preimage assms linear_conv_bounded_linear
+ using convex_linear_vimage assms
by auto
qed
@@ -8495,7 +8367,7 @@
{ assume "S={}" hence ?thesis by (simp add: rel_interior_empty cone_hull_empty) }
moreover
{ assume "S ~= {}" from this obtain s where "s : S" by auto
-have conv: "convex ({(1 :: real)} <*> S)" using convex_direct_sum[of "{(1 :: real)}" S]
+have conv: "convex ({(1 :: real)} <*> S)" using convex_Times[of "{(1 :: real)}" S]
assms convex_singleton[of "1 :: real"] by auto
def f == "(%y. {z. (y,z) : cone hull ({(1 :: real)} <*> S)})"
hence *: "(c, x) : rel_interior (cone hull ({(1 :: real)} <*> S)) =
@@ -8687,7 +8559,7 @@
have "(convex hull S) + (convex hull T) =
(%(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
by (simp add: set_plus_image)
-also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
+also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_Times by auto
also have "...= convex hull (S + T)" using fst_snd_linear linear_conv_bounded_linear
convex_hull_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
finally show ?thesis by auto
@@ -8701,7 +8573,7 @@
have "(rel_interior S) + (rel_interior T) = (%(x,y). x + y) ` (rel_interior S <*> rel_interior T)"
by (simp add: set_plus_image)
also have "... = (%(x,y). x + y) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
-also have "...= rel_interior (S + T)" using fst_snd_linear convex_direct_sum assms
+also have "...= rel_interior (S + T)" using fst_snd_linear convex_Times assms
rel_interior_convex_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
finally show ?thesis by auto
qed
@@ -8732,7 +8604,7 @@
fixes S T :: "('n::euclidean_space) set"
assumes "convex S" "rel_open S" "convex T" "rel_open T"
shows "convex (S <*> T) & rel_open (S <*> T)"
-by (metis assms convex_direct_sum rel_interior_direct_sum rel_open_def)
+by (metis assms convex_Times rel_interior_direct_sum rel_open_def)
lemma convex_rel_open_sum:
fixes S T :: "('n::euclidean_space) set"
@@ -8808,7 +8680,7 @@
def K == "(%i. cone hull ({(1 :: real)} <*> (S i)))"
have "!i:I. K i ~= {}" unfolding K_def using assms by (simp add: cone_hull_empty_iff[symmetric])
{ fix i assume "i:I"
- hence "convex (K i)" unfolding K_def apply (subst convex_cone_hull) apply (subst convex_direct_sum)
+ hence "convex (K i)" unfolding K_def apply (subst convex_cone_hull) apply (subst convex_Times)
using assms by auto
}
hence convK: "!i:I. convex (K i)" by auto
@@ -8817,14 +8689,14 @@
}
hence "K0 >= Union (K ` I)" by auto
moreover have "convex K0" unfolding K0_def
- apply (subst convex_cone_hull) apply (subst convex_direct_sum)
+ apply (subst convex_cone_hull) apply (subst convex_Times)
unfolding C0_def using convex_convex_hull by auto
ultimately have geq: "K0 >= convex hull (Union (K ` I))" using hull_minimal[of _ "K0" "convex"] by blast
have "!i:I. K i >= {(1 :: real)} <*> (S i)" using K_def by (simp add: hull_subset)
hence "Union (K ` I) >= {(1 :: real)} <*> Union (S ` I)" by auto
hence "convex hull Union (K ` I) >= convex hull ({(1 :: real)} <*> Union (S ` I))" by (simp add: hull_mono)
hence "convex hull Union (K ` I) >= {(1 :: real)} <*> C0" unfolding C0_def
- using convex_hull_direct_sum[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
+ using convex_hull_Times[of "{(1 :: real)}" "Union (S ` I)"] convex_hull_singleton by auto
moreover have "cone (convex hull(Union (K ` I)))" apply (subst cone_convex_hull)
using cone_Union[of "K ` I"] apply auto unfolding K_def using cone_cone_hull by auto
ultimately have "convex hull (Union (K ` I)) >= K0"
@@ -8835,7 +8707,7 @@
using assms apply blast
using `I ~= {}` apply blast
unfolding K_def apply rule
- apply (subst convex_cone_hull) apply (subst convex_direct_sum)
+ apply (subst convex_cone_hull) apply (subst convex_Times)
using assms cone_cone_hull `!i:I. K i ~= {}` K_def by auto
finally have "K0 = setsum K I" by auto
hence *: "rel_interior K0 = setsum (%i. (rel_interior (K i))) I"