--- a/NEWS Wed Aug 10 00:29:31 2011 -0700
+++ b/NEWS Wed Aug 10 00:31:51 2011 -0700
@@ -67,17 +67,27 @@
generalized theorems INF_cong and SUP_cong. New type classes for complete
boolean algebras and complete linear orders. Lemmas Inf_less_iff,
less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
-Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
+Changed proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
+Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
+INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
+INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, UNION_eq_Union_image,
+Union_def, UN_singleton, UN_eq have been discarded.
More consistent and less misunderstandable names:
INFI_def ~> INF_def
SUPR_def ~> SUP_def
- le_SUPI ~> le_SUP_I
- le_SUPI2 ~> le_SUP_I2
- le_INFI ~> le_INF_I
+ INF_leI ~> INF_lower
+ INF_leI2 ~> INF_lower2
+ le_INFI ~> INF_greatest
+ le_SUPI ~> SUP_upper
+ le_SUPI2 ~> SUP_upper2
+ SUP_leI ~> SUP_least
INFI_bool_eq ~> INF_bool_eq
SUPR_bool_eq ~> SUP_bool_eq
INFI_apply ~> INF_apply
SUPR_apply ~> SUP_apply
+ INTER_def ~> INTER_eq
+ UNION_def ~> UNION_eq
+
INCOMPATIBILITY.
* Theorem collections ball_simps and bex_simps do not contain theorems referring
--- a/doc-src/IsarRef/Thy/Generic.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/doc-src/IsarRef/Thy/Generic.thy Wed Aug 10 00:31:51 2011 -0700
@@ -201,7 +201,7 @@
@{rail "
@@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
;
- @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
+ @@{method split} @{syntax thmrefs}
"}
These methods provide low-level facilities for equational reasoning
@@ -245,12 +245,13 @@
t"} where @{text x} is a free or bound variable.
\item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
- splitting using the given rules. By default, splitting is performed
- in the conclusion of a goal; the @{text "(asm)"} option indicates to
- operate on assumptions instead.
+ splitting using the given rules. Splitting is performed in the
+ conclusion or some assumption of the subgoal, depending of the
+ structure of the rule.
Note that the @{method simp} method already involves repeated
- application of split rules as declared in the current context.
+ application of split rules as declared in the current context, using
+ @{attribute split}, for example.
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/Generic.tex Wed Aug 10 00:29:31 2011 -0700
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Wed Aug 10 00:31:51 2011 -0700
@@ -336,14 +336,8 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
\rail@end
-\rail@begin{2}{}
+\rail@begin{1}{}
\rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@term{\isa{asm}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
\end{railoutput}
@@ -388,12 +382,13 @@
assumption; this only works for equations of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} where \isa{x} is a free or bound variable.
\item \hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} performs single-step case
- splitting using the given rules. By default, splitting is performed
- in the conclusion of a goal; the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option indicates to
- operate on assumptions instead.
+ splitting using the given rules. Splitting is performed in the
+ conclusion or some assumption of the subgoal, depending of the
+ structure of the rule.
Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
- application of split rules as declared in the current context.
+ application of split rules as declared in the current context, using
+ \hyperlink{attribute.split}{\mbox{\isa{split}}}, for example.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 10 00:29:31 2011 -0700
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 10 00:31:51 2011 -0700
@@ -85,15 +85,14 @@
Sledgehammer is a tool that applies automatic theorem provers (ATPs)
and satisfiability-modulo-theories (SMT) solvers on the current goal. The
-supported ATPs are E \cite{schulz-2002}, LEO-II \cite{leo2}, Satallax
-\cite{satallax}, SInE-E \cite{sine}, SNARK \cite{snark}, SPASS
-\cite{weidenbach-et-al-2009}, ToFoF-E \cite{tofof}, Vampire
-\cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are
-run either locally or remotely via the System\-On\-TPTP web service
-\cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is
-used by default, and you can tell Sledgehammer to try CVC3 \cite{cvc3} and Yices
-\cite{yices} as well; these are run either locally or on a server at the TU
-M\"unchen.
+supported ATPs are E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF
+\cite{tofof}, LEO-II \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark},
+SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and
+Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via
+the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs,
+the SMT solvers Z3 \cite{z3} is used by default, and you can tell Sledgehammer
+to try CVC3 \cite{cvc3} and Yices \cite{yices} as well; these are run either
+locally or on a server at the TU M\"unchen.
The problem passed to the automatic provers consists of your current goal
together with a heuristic selection of hundreds of facts (theorems) from the
@@ -141,10 +140,10 @@
\subsection{Installing ATPs}
-Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
-LEO-II, Satallax, SInE-E, SNARK, ToFoF-E, and Waldmeister are available remotely
-via System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
-should at least install E and SPASS locally.
+Currently, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
+addition, E, E-SInE, E-ToFoF, LEO-II, Satallax, SNARK, Waldmeister, and Vampire
+are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. If you want
+better performance, you should at least install E and SPASS locally.
There are three main ways to install ATPs on your machine:
@@ -266,7 +265,7 @@
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{remote\_sine\_e}'' on goal \\
+Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
%
@@ -275,7 +274,7 @@
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
\postw
-Sledgehammer ran E, SInE-E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
Depending on which provers are installed and how many processor cores are
available, some of the provers might be missing or present with a
\textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
@@ -525,7 +524,7 @@
it took to find it or replay it).
In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
-proofs or sometimes provide incomplete proofs. The minimizer is then invoked to
+proofs or sometimes produce incomplete proofs. The minimizer is then invoked to
find out which facts are actually needed from the (large) set of facts that was
initinally given to the prover. Finally, if a prover returns a proof with lots
of facts, the minimizer is invoked automatically since Metis would be unlikely
@@ -723,6 +722,23 @@
executable, or install the prebuilt E package from Isabelle's download page. See
\S\ref{installation} for details.
+\item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
+higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
+with support for the TPTP higher-order syntax (THF).
+
+\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
+the external provers, Metis itself can be used for proof search.
+
+\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
+Metis, corresponding to \textit{metis} (\textit{full\_types}).
+
+\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
+corresponding to \textit{metis} (\textit{no\_types}).
+
+\item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic
+higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
+support for the TPTP higher-order syntax (THF).
+
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
@@ -730,17 +746,17 @@
package from Isabelle's download page. Sledgehammer requires version 3.5 or
above. See \S\ref{installation} for details.
-\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
-SRI \cite{yices}. To use Yices, set the environment variable
-\texttt{YICES\_SOLVER} to the complete path of the executable, including the
-file name. Sledgehammer has been tested with version 1.0.
-
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is a first-order resolution
prover developed by Andrei Voronkov and his colleagues
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
executable. Sledgehammer has been tested with versions 11, 0.6, and 1.0.
+\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
+SRI \cite{yices}. To use Yices, set the environment variable
+\texttt{YICES\_SOLVER} to the complete path of the executable, including the
+file name. Sledgehammer has been tested with version 1.0.
+
\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
Microsoft Research \cite{z3}. To use Z3, set the environment variable
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
@@ -750,15 +766,6 @@
\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
ATP, exploiting Z3's undocumented support for the TPTP format. It is included
for experimental purposes. It requires version 2.18 or above.
-
-\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
-the external provers, Metis itself can be used for proof search.
-
-\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
-Metis, corresponding to \textit{metis} (\textit{full\_types}).
-
-\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
-corresponding to \textit{metis} (\textit{no\_types}).
\end{enum}
In addition, the following remote provers are supported:
@@ -771,32 +778,26 @@
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-\item[$\bullet$] \textbf{\textit{remote\_leo2}:} LEO-II is an automatic
-higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
-with support for the TPTP higher-order syntax (THF). The remote version of
-LEO-II runs on Geoff Sutcliffe's Miami servers. In the current setup, the
-problems given to LEO-II are only mildly higher-order.
-
-\item[$\bullet$] \textbf{\textit{remote\_satallax}:} Satallax is an automatic
-higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
-support for the TPTP higher-order syntax (THF). The remote version of Satallax
-runs on Geoff Sutcliffe's Miami servers. In the current setup, the problems
-given to Satallax are only mildly higher-order.
-
-\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
+\item[$\bullet$] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
SInE runs on Geoff Sutcliffe's Miami servers.
+\item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
+developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
+servers. This ATP supports the TPTP many-typed first-order format (TFF). The
+remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
+
+\item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
+runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+
+\item[$\bullet$] \textbf{\textit{remote\_satallax}:} The remote version of
+Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
TPTP many-typed first-order format (TFF). The remote version of SNARK runs on
Geoff Sutcliffe's Miami servers.
-\item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
-developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
-servers. This ATP supports the TPTP many-typed first-order format (TFF). The
-remote version of ToFoF-E runs on Geoff Sutcliffe's Miami servers.
-
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
@@ -814,12 +815,12 @@
as an ATP'' runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
-the SMT module's \textit{smt\_solver} configuration option is set to) in
-parallel---either locally or remotely, depending on the number of processor
-cores available. For historical reasons, the default value of this option can be
-overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
-in Proof General.
+By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever
+the SMT module's \textit{smt\_solver} configuration option is set to), and (if
+appropriate) Waldmeister in parallel---either locally or remotely, depending on
+the number of processor cores available. For historical reasons, the default
+value of this option can be overridden using the option ``Sledgehammer:
+Provers'' from the ``Isabelle'' menu in Proof General.
It is a good idea to run several provers in parallel, although it could slow
down your machine. Running E, SPASS, and Vampire for 5~seconds yields a similar
--- a/doc-src/manual.bib Wed Aug 10 00:29:31 2011 -0700
+++ b/doc-src/manual.bib Wed Aug 10 00:31:51 2011 -0700
@@ -140,7 +140,7 @@
%B
-@inproceedings{satallax,
+@inproceedings{backes-brown-2010,
title = "Analytic Tableaux for Higher-Order Logic with Choice",
author = "Julian Backes and Chad E. Brown",
booktitle={Automated Reasoning: IJCAR 2010},
@@ -335,6 +335,17 @@
publisher = {Academic Press},
year = 1988}
+@inproceedings{satallax,
+ author = "Chad E. Brown",
+ title = "Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems",
+ booktitle = {Automated Deduction --- CADE-23},
+ publisher = Springer,
+ series = LNCS,
+ volume = 6803,
+ pages = "147--161",
+ editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
+ year = 2011}
+
@Article{debruijn72,
author = {N. G. de Bruijn},
title = {Lambda Calculus Notation with Nameless Dummies,
@@ -686,9 +697,10 @@
booktitle = {Automated Deduction --- CADE-23},
publisher = Springer,
series = LNCS,
+ volume = 6803,
+ pages = "299--314",
editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
- year = 2011,
- note = "To appear."}
+ year = 2011}
@book{Hudak-Haskell,author={Paul Hudak},
title={The Haskell School of Expression},publisher=CUP,year=2000}
--- a/src/HOL/ATP.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/ATP.thy Wed Aug 10 00:31:51 2011 -0700
@@ -7,7 +7,8 @@
theory ATP
imports Meson
-uses "Tools/monomorph.ML"
+uses "Tools/lambda_lifting.ML"
+ "Tools/monomorph.ML"
"Tools/ATP/atp_util.ML"
"Tools/ATP/atp_problem.ML"
"Tools/ATP/atp_proof.ML"
--- a/src/HOL/Algebra/Ideal.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Algebra/Ideal.thy Wed Aug 10 00:31:51 2011 -0700
@@ -227,26 +227,14 @@
and notempty: "S \<noteq> {}"
shows "ideal (Inter S) R"
apply (unfold_locales)
-apply (simp_all add: Inter_def INTER_def)
- apply (rule, simp) defer 1
+apply (simp_all add: Inter_eq)
+ apply rule unfolding mem_Collect_eq defer 1
apply rule defer 1
apply rule defer 1
apply (fold a_inv_def, rule) defer 1
apply rule defer 1
apply rule defer 1
proof -
- fix x
- assume "\<forall>I\<in>S. x \<in> I"
- hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
-
- from notempty have "\<exists>I0. I0 \<in> S" by blast
- from this obtain I0 where I0S: "I0 \<in> S" by auto
-
- interpret ideal I0 R by (rule Sideals[OF I0S])
-
- from xI[OF I0S] have "x \<in> I0" .
- from this and a_subset show "x \<in> carrier R" by fast
-next
fix x y
assume "\<forall>I\<in>S. x \<in> I"
hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
@@ -298,6 +286,20 @@
from xI[OF JS] and ycarr
show "x \<otimes> y \<in> J" by (rule I_r_closed)
+next
+ fix x
+ assume "\<forall>I\<in>S. x \<in> I"
+ hence xI: "\<And>I. I \<in> S \<Longrightarrow> x \<in> I" by simp
+
+ from notempty have "\<exists>I0. I0 \<in> S" by blast
+ from this obtain I0 where I0S: "I0 \<in> S" by auto
+
+ interpret ideal I0 R by (rule Sideals[OF I0S])
+
+ from xI[OF I0S] have "x \<in> I0" .
+ from this and a_subset show "x \<in> carrier R" by fast
+next
+
qed
--- a/src/HOL/Complete_Lattice.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Complete_Lattice.thy Wed Aug 10 00:31:51 2011 -0700
@@ -1,6 +1,6 @@
-(* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
+ (* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *)
-header {* Complete lattices, with special focus on sets *}
+header {* Complete lattices *}
theory Complete_Lattice
imports Set
@@ -102,40 +102,40 @@
by (simp only: dual.INF_def SUP_def)
qed
-lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
+lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
by (auto simp add: INF_def intro: Inf_lower)
-lemma le_SUP_I: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+lemma INF_greatest: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
+ by (auto simp add: INF_def intro: Inf_greatest)
+
+lemma SUP_upper: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
by (auto simp add: SUP_def intro: Sup_upper)
-lemma le_INF_I: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
- by (auto simp add: INF_def intro: Inf_greatest)
-
-lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
+lemma SUP_least: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
by (auto simp add: SUP_def intro: Sup_least)
lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
using Inf_lower [of u A] by auto
-lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
- using INF_leI [of i A f] by auto
+lemma INF_lower2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
+ using INF_lower [of i A f] by auto
lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
using Sup_upper [of u A] by auto
-lemma le_SUP_I2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
- using le_SUP_I [of i A f] by auto
+lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
+ using SUP_upper [of i A f] by auto
-lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
+lemma le_Inf_iff (*[simp]*): "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
by (auto intro: Inf_greatest dest: Inf_lower)
-lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
+lemma le_INF_iff (*[simp]*): "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
by (auto simp add: INF_def le_Inf_iff)
-lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
+lemma Sup_le_iff (*[simp]*): "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
by (auto intro: Sup_least dest: Sup_upper)
-lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
+lemma SUP_le_iff (*[simp]*): "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
by (auto simp add: SUP_def Sup_le_iff)
lemma Inf_empty [simp]:
@@ -160,22 +160,22 @@
"\<Squnion>UNIV = \<top>"
by (auto intro!: antisym Sup_upper)
-lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
+lemma Inf_insert (*[simp]*): "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
by (simp add: INF_def Inf_insert)
-lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
+lemma Sup_insert (*[simp]*): "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
by (simp add: SUP_def Sup_insert)
-lemma INF_image: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
+lemma INF_image (*[simp]*): "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
by (simp add: INF_def image_image)
-lemma SUP_image: "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
+lemma SUP_image (*[simp]*): "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
by (simp add: SUP_def image_image)
lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
@@ -184,22 +184,6 @@
lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<sqsubseteq> b}"
by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
-lemma Inf_singleton [simp]:
- "\<Sqinter>{a} = a"
- by (auto intro: antisym Inf_lower Inf_greatest)
-
-lemma Sup_singleton [simp]:
- "\<Squnion>{a} = a"
- by (auto intro: antisym Sup_upper Sup_least)
-
-lemma Inf_binary:
- "\<Sqinter>{a, b} = a \<sqinter> b"
- by (simp add: Inf_insert)
-
-lemma Sup_binary:
- "\<Squnion>{a, b} = a \<squnion> b"
- by (simp add: Sup_insert)
-
lemma Inf_superset_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
by (auto intro: Inf_greatest Inf_lower)
@@ -282,23 +266,23 @@
lemma INF_union:
"(\<Sqinter>i \<in> A \<union> B. M i) = (\<Sqinter>i \<in> A. M i) \<sqinter> (\<Sqinter>i\<in>B. M i)"
- by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 le_INF_I INF_leI)
+ by (auto intro!: antisym INF_mono intro: le_infI1 le_infI2 INF_greatest INF_lower)
lemma Sup_union_distrib: "\<Squnion>(A \<union> B) = \<Squnion>A \<squnion> \<Squnion>B"
by (rule antisym) (auto intro: Sup_least Sup_upper le_supI1 le_supI2)
lemma SUP_union:
"(\<Squnion>i \<in> A \<union> B. M i) = (\<Squnion>i \<in> A. M i) \<squnion> (\<Squnion>i\<in>B. M i)"
- by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_leI le_SUP_I)
+ by (auto intro!: antisym SUP_mono intro: le_supI1 le_supI2 SUP_least SUP_upper)
lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)"
- by (rule antisym) (rule le_INF_I, auto intro: le_infI1 le_infI2 INF_leI INF_mono)
+ by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)"
- by (rule antisym) (auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono,
- rule SUP_leI, auto intro: le_supI1 le_supI2 le_SUP_I SUP_mono)
+ by (rule antisym) (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono,
+ rule SUP_least, auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
-lemma Inf_top_conv [no_atp]:
+lemma Inf_top_conv (*[simp]*) [no_atp]:
"\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
"\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
proof -
@@ -306,7 +290,7 @@
proof
assume "\<forall>x\<in>A. x = \<top>"
then have "A = {} \<or> A = {\<top>}" by auto
- then show "\<Sqinter>A = \<top>" by auto
+ then show "\<Sqinter>A = \<top>" by (auto simp add: Inf_insert)
next
assume "\<Sqinter>A = \<top>"
show "\<forall>x\<in>A. x = \<top>"
@@ -320,12 +304,12 @@
then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
qed
-lemma INF_top_conv:
+lemma INF_top_conv (*[simp]*):
"(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
"\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
by (auto simp add: INF_def Inf_top_conv)
-lemma Sup_bot_conv [no_atp]:
+lemma Sup_bot_conv (*[simp]*) [no_atp]:
"\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
"\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
proof -
@@ -334,28 +318,28 @@
from dual.Inf_top_conv show ?P and ?Q by simp_all
qed
-lemma SUP_bot_conv:
+lemma SUP_bot_conv (*[simp]*):
"(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
"\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
by (auto simp add: SUP_def Sup_bot_conv)
lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
- by (auto intro: antisym INF_leI le_INF_I)
+ by (auto intro: antisym INF_lower INF_greatest)
lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
- by (auto intro: antisym SUP_leI le_SUP_I)
+ by (auto intro: antisym SUP_upper SUP_least)
-lemma INF_top: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
+lemma INF_top (*[simp]*): "(\<Sqinter>x\<in>A. \<top>) = \<top>"
by (cases "A = {}") (simp_all add: INF_empty)
-lemma SUP_bot: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
+lemma SUP_bot (*[simp]*): "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
by (cases "A = {}") (simp_all add: SUP_empty)
lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
- by (iprover intro: INF_leI le_INF_I order_trans antisym)
+ by (iprover intro: INF_lower INF_greatest order_trans antisym)
lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
- by (iprover intro: SUP_leI le_SUP_I order_trans antisym)
+ by (iprover intro: SUP_upper SUP_least order_trans antisym)
lemma INF_absorb:
assumes "k \<in> I"
@@ -381,20 +365,12 @@
"(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
by (simp add: SUP_empty)
-lemma INF_eq:
- "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
- by (simp add: INF_def image_def)
-
-lemma SUP_eq:
- "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
- by (simp add: SUP_def image_def)
-
lemma less_INF_D:
assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
proof -
note `y < (\<Sqinter>i\<in>A. f i)`
also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using `i \<in> A`
- by (rule INF_leI)
+ by (rule INF_lower)
finally show "y < f i" .
qed
@@ -402,19 +378,11 @@
assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
proof -
have "f i \<le> (\<Squnion>i\<in>A. f i)" using `i \<in> A`
- by (rule le_SUP_I)
+ by (rule SUP_upper)
also note `(\<Squnion>i\<in>A. f i) < y`
finally show "f i < y" .
qed
-lemma INF_UNIV_range:
- "(\<Sqinter>x. f x) = \<Sqinter>range f"
- by (fact INF_def)
-
-lemma SUP_UNIV_range:
- "(\<Squnion>x. f x) = \<Squnion>range f"
- by (fact SUP_def)
-
lemma INF_UNIV_bool_expand:
"(\<Sqinter>b. A b) = A True \<sqinter> A False"
by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
@@ -450,7 +418,7 @@
and prove @{text inf_Sup} and @{text sup_Inf} from that? *}
fix a b c
from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
- then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary)
+ then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_insert)
qed
lemma Inf_sup:
@@ -525,23 +493,23 @@
"class.complete_linorder Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
-lemma Inf_less_iff:
+lemma Inf_less_iff (*[simp]*):
"\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
unfolding not_le [symmetric] le_Inf_iff by auto
-lemma INF_less_iff:
+lemma INF_less_iff (*[simp]*):
"(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
unfolding INF_def Inf_less_iff by auto
-lemma less_Sup_iff:
+lemma less_Sup_iff (*[simp]*):
"a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
unfolding not_le [symmetric] Sup_le_iff by auto
-lemma less_SUP_iff:
+lemma less_SUP_iff (*[simp]*):
"a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
unfolding SUP_def less_Sup_iff by auto
-lemma Sup_eq_top_iff:
+lemma Sup_eq_top_iff (*[simp]*):
"\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
proof
assume *: "\<Squnion>A = \<top>"
@@ -563,11 +531,11 @@
qed
qed
-lemma SUP_eq_top_iff:
+lemma SUP_eq_top_iff (*[simp]*):
"(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
unfolding SUP_def Sup_eq_top_iff by auto
-lemma Inf_eq_bot_iff:
+lemma Inf_eq_bot_iff (*[simp]*):
"\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
proof -
interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
@@ -575,7 +543,7 @@
from dual.Sup_eq_top_iff show ?thesis .
qed
-lemma INF_eq_bot_iff:
+lemma INF_eq_bot_iff (*[simp]*):
"(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
unfolding INF_def Inf_eq_bot_iff by auto
@@ -637,7 +605,7 @@
by (simp add: Sup_fun_def)
instance proof
-qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_leI le_SUP_I le_INF_I SUP_leI)
+qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_lower INF_greatest SUP_upper SUP_least)
end
@@ -703,9 +671,6 @@
lemma Inter_greatest: "(\<And>X. X \<in> A \<Longrightarrow> C \<subseteq> X) \<Longrightarrow> C \<subseteq> Inter A"
by (fact Inf_greatest)
-lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
- by (fact Inf_binary [symmetric])
-
lemma Inter_empty: "\<Inter>{} = UNIV"
by (fact Inf_empty) (* already simp *)
@@ -762,34 +727,26 @@
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
*} -- {* to avoid eta-contraction of body *}
-lemma INTER_eq_Inter_image:
- "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
- by (fact INF_def)
-
-lemma Inter_def:
- "\<Inter>S = (\<Inter>x\<in>S. x)"
- by (simp add: INTER_eq_Inter_image image_def)
-
-lemma INTER_def:
+lemma INTER_eq:
"(\<Inter>x\<in>A. B x) = {y. \<forall>x\<in>A. y \<in> B x}"
- by (auto simp add: INTER_eq_Inter_image Inter_eq)
+ by (auto simp add: INF_def)
lemma Inter_image_eq [simp]:
"\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
by (rule sym) (fact INF_def)
lemma INT_iff [simp]: "b \<in> (\<Inter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. b \<in> B x)"
- by (unfold INTER_def) blast
+ by (auto simp add: INF_def image_def)
lemma INT_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> b \<in> B x) \<Longrightarrow> b \<in> (\<Inter>x\<in>A. B x)"
- by (unfold INTER_def) blast
+ by (auto simp add: INF_def image_def)
lemma INT_D [elim, Pure.elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> B a"
by auto
lemma INT_E [elim]: "b \<in> (\<Inter>x\<in>A. B x) \<Longrightarrow> (b \<in> B a \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
-- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
- by (unfold INTER_def) blast
+ by (auto simp add: INF_def image_def)
lemma INT_cong [cong]:
"A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Inter>x\<in>A. C x) = (\<Inter>x\<in>B. D x)"
@@ -802,13 +759,13 @@
by blast
lemma INT_lower: "a \<in> A \<Longrightarrow> (\<Inter>x\<in>A. B x) \<subseteq> B a"
- by (fact INF_leI)
+ by (fact INF_lower)
lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
- by (fact le_INF_I)
+ by (fact INF_greatest)
lemma INT_empty: "(\<Inter>x\<in>{}. B x) = UNIV"
- by (fact INF_empty) (* already simp *)
+ by (fact INF_empty)
lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
by (fact INF_absorb)
@@ -829,10 +786,6 @@
lemma INT_constant [simp]: "(\<Inter>y\<in>A. c) = (if A = {} then UNIV else c)"
by (fact INF_constant)
-lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
- -- {* Look: it has an \emph{existential} quantifier *}
- by (fact INF_eq)
-
lemma INTER_UNIV_conv [simp]:
"(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
"((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
@@ -891,9 +844,6 @@
lemma Union_least: "(\<And>X. X \<in> A \<Longrightarrow> X \<subseteq> C) \<Longrightarrow> \<Union>A \<subseteq> C"
by (fact Sup_least)
-lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
- by blast
-
lemma Union_empty [simp]: "\<Union>{} = {}"
by (fact Sup_empty)
@@ -966,24 +916,16 @@
[Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax UNION} @{syntax_const "_UNION"}]
*} -- {* to avoid eta-contraction of body *}
-lemma UNION_eq_Union_image:
- "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
- by (fact SUP_def)
-
-lemma Union_def:
- "\<Union>S = (\<Union>x\<in>S. x)"
- by (simp add: UNION_eq_Union_image image_def)
-
-lemma UNION_def [no_atp]:
+lemma UNION_eq [no_atp]:
"(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"
- by (auto simp add: UNION_eq_Union_image Union_eq)
+ by (auto simp add: SUP_def)
lemma Union_image_eq [simp]:
"\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
- by (rule sym) (fact UNION_eq_Union_image)
+ by (auto simp add: UNION_eq)
lemma UN_iff [simp]: "(b \<in> (\<Union>x\<in>A. B x)) = (\<exists>x\<in>A. b \<in> B x)"
- by (unfold UNION_def) blast
+ by (auto simp add: SUP_def image_def)
lemma UN_I [intro]: "a \<in> A \<Longrightarrow> b \<in> B a \<Longrightarrow> b \<in> (\<Union>x\<in>A. B x)"
-- {* The order of the premises presupposes that @{term A} is rigid;
@@ -991,7 +933,7 @@
by auto
lemma UN_E [elim!]: "b \<in> (\<Union>x\<in>A. B x) \<Longrightarrow> (\<And>x. x\<in>A \<Longrightarrow> b \<in> B x \<Longrightarrow> R) \<Longrightarrow> R"
- by (unfold UNION_def) blast
+ by (auto simp add: SUP_def image_def)
lemma UN_cong [cong]:
"A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Union>x\<in>A. C x) = (\<Union>x\<in>B. D x)"
@@ -1005,10 +947,10 @@
by blast
lemma UN_upper: "a \<in> A \<Longrightarrow> B a \<subseteq> (\<Union>x\<in>A. B x)"
- by (fact le_SUP_I)
+ by (fact SUP_upper)
lemma UN_least: "(\<And>x. x \<in> A \<Longrightarrow> B x \<subseteq> C) \<Longrightarrow> (\<Union>x\<in>A. B x) \<subseteq> C"
- by (fact SUP_leI)
+ by (fact SUP_least)
lemma Collect_bex_eq [no_atp]: "{x. \<exists>y\<in>A. P x y} = (\<Union>y\<in>A. {x. P x y})"
by blast
@@ -1017,21 +959,18 @@
by blast
lemma UN_empty [no_atp]: "(\<Union>x\<in>{}. B x) = {}"
- by (fact SUP_empty) (* already simp *)
+ by (fact SUP_empty)
lemma UN_empty2 [simp]: "(\<Union>x\<in>A. {}) = {}"
by (fact SUP_bot)
-lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
- by blast
-
lemma UN_absorb: "k \<in> I \<Longrightarrow> A k \<union> (\<Union>i\<in>I. A i) = (\<Union>i\<in>I. A i)"
by (fact SUP_absorb)
lemma UN_insert [simp]: "(\<Union>x\<in>insert a A. B x) = B a \<union> UNION A B"
by (fact SUP_insert)
-lemma UN_Un[simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
+lemma UN_Un [simp]: "(\<Union>i \<in> A \<union> B. M i) = (\<Union>i\<in>A. M i) \<union> (\<Union>i\<in>B. M i)"
by (fact SUP_union)
lemma UN_UN_flatten: "(\<Union>x \<in> (\<Union>y\<in>A. B y). C x) = (\<Union>y\<in>A. \<Union>x\<in>B y. C x)"
@@ -1043,9 +982,6 @@
lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
by (fact SUP_constant)
-lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
- by (fact SUP_eq)
-
lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
by blast
@@ -1212,19 +1148,91 @@
text {* Legacy names *}
+lemma (in complete_lattice) Inf_singleton [simp]:
+ "\<Sqinter>{a} = a"
+ by (simp add: Inf_insert)
+
+lemma (in complete_lattice) Sup_singleton [simp]:
+ "\<Squnion>{a} = a"
+ by (simp add: Sup_insert)
+
+lemma (in complete_lattice) Inf_binary:
+ "\<Sqinter>{a, b} = a \<sqinter> b"
+ by (simp add: Inf_insert)
+
+lemma (in complete_lattice) Sup_binary:
+ "\<Squnion>{a, b} = a \<squnion> b"
+ by (simp add: Sup_insert)
+
lemmas (in complete_lattice) INFI_def = INF_def
lemmas (in complete_lattice) SUPR_def = SUP_def
-lemmas (in complete_lattice) le_SUPI = le_SUP_I
-lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
-lemmas (in complete_lattice) le_INFI = le_INF_I
+lemmas (in complete_lattice) INF_leI = INF_lower
+lemmas (in complete_lattice) INF_leI2 = INF_lower2
+lemmas (in complete_lattice) le_INFI = INF_greatest
+lemmas (in complete_lattice) le_SUPI = SUP_upper
+lemmas (in complete_lattice) le_SUPI2 = SUP_upper2
+lemmas (in complete_lattice) SUP_leI = SUP_least
lemmas (in complete_lattice) less_INFD = less_INF_D
+lemmas INFI_apply = INF_apply
+lemmas SUPR_apply = SUP_apply
+
+text {* Grep and put to news from here *}
+
+lemma (in complete_lattice) INF_eq:
+ "(\<Sqinter>x\<in>A. B x) = \<Sqinter>({Y. \<exists>x\<in>A. Y = B x})"
+ by (simp add: INF_def image_def)
+
+lemma (in complete_lattice) SUP_eq:
+ "(\<Squnion>x\<in>A. B x) = \<Squnion>({Y. \<exists>x\<in>A. Y = B x})"
+ by (simp add: SUP_def image_def)
+
lemma (in complete_lattice) INF_subset:
"B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
by (rule INF_superset_mono) auto
-lemmas INFI_apply = INF_apply
-lemmas SUPR_apply = SUP_apply
+lemma (in complete_lattice) INF_UNIV_range:
+ "(\<Sqinter>x. f x) = \<Sqinter>range f"
+ by (fact INF_def)
+
+lemma (in complete_lattice) SUP_UNIV_range:
+ "(\<Squnion>x. f x) = \<Squnion>range f"
+ by (fact SUP_def)
+
+lemma Int_eq_Inter: "A \<inter> B = \<Inter>{A, B}"
+ by (simp add: Inf_insert)
+
+lemma INTER_eq_Inter_image:
+ "(\<Inter>x\<in>A. B x) = \<Inter>(B`A)"
+ by (fact INF_def)
+
+lemma Inter_def:
+ "\<Inter>S = (\<Inter>x\<in>S. x)"
+ by (simp add: INTER_eq_Inter_image image_def)
+
+lemmas INTER_def = INTER_eq
+lemmas UNION_def = UNION_eq
+
+lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
+ by (fact INF_eq)
+
+lemma Un_eq_Union: "A \<union> B = \<Union>{A, B}"
+ by blast
+
+lemma UNION_eq_Union_image:
+ "(\<Union>x\<in>A. B x) = \<Union>(B ` A)"
+ by (fact SUP_def)
+
+lemma Union_def:
+ "\<Union>S = (\<Union>x\<in>S. x)"
+ by (simp add: UNION_eq_Union_image image_def)
+
+lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
+ by blast
+
+lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
+ by (fact SUP_eq)
+
text {* Finally *}
--- a/src/HOL/Import/HOLLight/hollight.imp Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Import/HOLLight/hollight.imp Wed Aug 10 00:31:51 2011 -0700
@@ -590,8 +590,6 @@
"UNIONS_INSERT" > "Complete_Lattice.Union_insert"
"UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
"UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
- "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
- "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
"UNIONS_0" > "Complete_Lattice.Union_empty"
"UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
"TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
@@ -1597,8 +1595,6 @@
"INTERS_INSERT" > "Complete_Lattice.Inter_insert"
"INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
"INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
- "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
- "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
"INTERS_0" > "Complete_Lattice.Inter_empty"
"INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
"INSERT_UNION_EQ" > "Set.Un_insert_left"
--- a/src/HOL/IsaMakefile Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/IsaMakefile Wed Aug 10 00:31:51 2011 -0700
@@ -244,7 +244,9 @@
Tools/inductive_codegen.ML \
Tools/inductive_realizer.ML \
Tools/inductive_set.ML \
+ Tools/lambda_lifting.ML \
Tools/lin_arith.ML \
+ Tools/monomorph.ML \
Tools/nat_arith.ML \
Tools/primrec.ML \
Tools/prop_logic.ML \
@@ -309,10 +311,8 @@
Tools/code_evaluation.ML \
Tools/groebner.ML \
Tools/int_arith.ML \
- Tools/lambda_lifting.ML \
Tools/list_code.ML \
Tools/list_to_set_comprehension.ML \
- Tools/monomorph.ML \
Tools/nat_numeral_simprocs.ML \
Tools/Nitpick/kodkod.ML \
Tools/Nitpick/kodkod_sat.ML \
--- a/src/HOL/Lattices.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Lattices.thy Wed Aug 10 00:31:51 2011 -0700
@@ -177,10 +177,10 @@
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
by (fact inf.left_commute)
-lemma inf_idem: "x \<sqinter> x = x"
+lemma inf_idem (*[simp]*): "x \<sqinter> x = x"
by (fact inf.idem)
-lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
+lemma inf_left_idem (*[simp]*): "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
by (fact inf.left_idem)
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
@@ -216,10 +216,10 @@
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
by (fact sup.left_commute)
-lemma sup_idem: "x \<squnion> x = x"
+lemma sup_idem (*[simp]*): "x \<squnion> x = x"
by (fact sup.idem)
-lemma sup_left_idem: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
+lemma sup_left_idem (*[simp]*): "x \<squnion> (x \<squnion> y) = x \<squnion> y"
by (fact sup.left_idem)
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
@@ -240,10 +240,10 @@
by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
(unfold_locales, auto)
-lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
+lemma inf_sup_absorb (*[simp]*): "x \<sqinter> (x \<squnion> y) = x"
by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
-lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
+lemma sup_inf_absorb (*[simp]*): "x \<squnion> (x \<sqinter> y) = x"
by (blast intro: antisym sup_ge1 sup_least inf_le1)
lemmas inf_sup_aci = inf_aci sup_aci
@@ -436,11 +436,11 @@
by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
(unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
-lemma compl_inf_bot:
+lemma compl_inf_bot (*[simp]*):
"- x \<sqinter> x = \<bottom>"
by (simp add: inf_commute inf_compl_bot)
-lemma compl_sup_top:
+lemma compl_sup_top (*[simp]*):
"- x \<squnion> x = \<top>"
by (simp add: sup_commute sup_compl_top)
@@ -522,7 +522,7 @@
then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
qed
-lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
+lemma compl_le_compl_iff (*[simp]*):
"- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
by (auto dest: compl_mono)
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 10 00:31:51 2011 -0700
@@ -9,11 +9,11 @@
val prover_timeoutK = "prover_timeout"
val keepK = "keep"
val type_encK = "type_enc"
+val soundK = "sound"
val slicingK = "slicing"
val lambda_translationK = "lambda_translation"
val e_weight_methodK = "e_weight_method"
-val spass_force_sosK = "spass_force_sos"
-val vampire_force_sosK = "vampire_force_sos"
+val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
val minimizeK = "minimize"
val minimize_timeoutK = "minimize_timeout"
@@ -213,6 +213,8 @@
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
+val str0 = string_of_int o the_default 0
+
local
val str = string_of_int
@@ -242,13 +244,9 @@
str3 (avg_time time_prover_fail (calls - success)))
)
-
fun str_of_pos (pos, triv) =
- let val str0 = string_of_int o the_default 0
- in
- str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^
- (if triv then "[T]" else "")
- end
+ str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^
+ (if triv then "[T]" else "")
fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
re_nontriv_success, re_proofs, re_time, re_timeout,
@@ -354,35 +352,36 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_enc max_relevant slicing lambda_translation
- e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout dir
- st =
+fun run_sh prover_name prover type_enc sound max_relevant slicing
+ lambda_translation e_weight_method force_sos hard_timeout timeout dir
+ pos st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
- fun change_dir (SOME dir) =
+ fun set_file_name (SOME dir) =
Config.put Sledgehammer_Provers.dest_dir dir
+ #> Config.put Sledgehammer_Provers.problem_prefix
+ ("prob_" ^ str0 (Position.line_of pos))
#> Config.put SMT_Config.debug_files
(dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
^ serial_string ())
- | change_dir NONE = I
+ | set_file_name NONE = I
val st' =
st |> Proof.map_context
- (change_dir dir
+ (set_file_name dir
#> (Option.map (Config.put
Sledgehammer_Provers.atp_lambda_translation)
lambda_translation |> the_default I)
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
- #> (Option.map (Config.put ATP_Systems.spass_force_sos)
- spass_force_sos |> the_default I)
- #> (Option.map (Config.put ATP_Systems.vampire_force_sos)
- vampire_force_sos |> the_default I)
+ #> (Option.map (Config.put ATP_Systems.force_sos)
+ force_sos |> the_default I)
#> Config.put Sledgehammer_Provers.measure_run_time true)
val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
("type_enc", type_enc),
+ ("sound", sound),
("max_relevant", max_relevant),
("slicing", slicing),
("timeout", string_of_int timeout)]
@@ -451,20 +450,20 @@
in
-fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
+fun run_sledgehammer trivial args reconstructor named_thms id
+ ({pre=st, log, pos, ...}: Mirabelle.run_args) =
let
val triv_str = if trivial then "[T] " else ""
val _ = change_data id inc_sh_calls
val _ = if trivial then () else change_data id inc_sh_nontriv_calls
val (prover_name, prover) = get_prover (Proof.context_of st) args
val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
+ val sound = AList.lookup (op =) args soundK |> the_default "false"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
val lambda_translation = AList.lookup (op =) args lambda_translationK
val e_weight_method = AList.lookup (op =) args e_weight_methodK
- val spass_force_sos = AList.lookup (op =) args spass_force_sosK
- |> Option.map (curry (op <>) "false")
- val vampire_force_sos = AList.lookup (op =) args vampire_force_sosK
+ val force_sos = AList.lookup (op =) args force_sosK
|> Option.map (curry (op <>) "false")
val dir = AList.lookup (op =) args keepK
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
@@ -472,9 +471,9 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_enc max_relevant slicing lambda_translation
- e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout
- dir st
+ run_sh prover_name prover type_enc sound max_relevant slicing
+ lambda_translation e_weight_method force_sos hard_timeout timeout dir
+ pos st
in
case result of
SH_OK (time_isa, time_prover, names) =>
@@ -511,6 +510,7 @@
val n0 = length (these (!named_thms))
val (prover_name, _) = get_prover ctxt args
val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
+ val sound = AList.lookup (op =) args soundK |> the_default "false"
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
@@ -519,6 +519,7 @@
[("provers", prover_name),
("verbose", "true"),
("type_enc", type_enc),
+ ("sound", sound),
("timeout", string_of_int timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts prover_name params
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Wed Aug 10 00:31:51 2011 -0700
@@ -8,7 +8,7 @@
imports
"~~/src/HOL/Algebra/Ring"
"~~/src/HOL/Algebra/FiniteProduct"
-begin;
+begin
(* finiteness stuff *)
@@ -34,7 +34,7 @@
definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where
"units_of G == (| carrier = Units G,
Group.monoid.mult = Group.monoid.mult G,
- one = one G |)";
+ one = one G |)"
(*
@@ -264,7 +264,7 @@
(ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |]
==> finprod G f (Union C) = finprod G (finprod G f) C"
apply (frule finprod_UN_disjoint [of C id f])
- apply (unfold Union_def id_def, auto)
+ apply (auto simp add: SUP_def)
done
lemma (in comm_monoid) finprod_one [rule_format]:
--- a/src/HOL/Probability/Caratheodory.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Probability/Caratheodory.thy Wed Aug 10 00:31:51 2011 -0700
@@ -6,7 +6,7 @@
header {*Caratheodory Extension Theorem*}
theory Caratheodory
- imports Sigma_Algebra Extended_Real_Limits
+imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
begin
lemma sums_def2:
@@ -433,8 +433,7 @@
hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
by (simp add: lambda_system_eq UNION_in)
have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
- by (blast intro: increasingD [OF inc] UNION_eq_Union_image
- UNION_in U_in)
+ by (blast intro: increasingD [OF inc] UNION_in U_in)
thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a - (\<Union>i. A i)) \<le> f a"
by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
next
--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Aug 10 00:31:51 2011 -0700
@@ -315,10 +315,10 @@
by (auto simp add: binary_def)
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
- by (simp add: UNION_eq_Union_image range_binary_eq)
+ by (simp add: SUP_def range_binary_eq)
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
- by (simp add: INTER_eq_Inter_image range_binary_eq)
+ by (simp add: INF_def range_binary_eq)
lemma sigma_algebra_iff2:
"sigma_algebra M \<longleftrightarrow>
@@ -1109,7 +1109,7 @@
done
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
- by (simp add: UNION_eq_Union_image range_binaryset_eq)
+ by (simp add: SUP_def range_binaryset_eq)
section {* Closed CDI *}
--- a/src/HOL/SMT.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/SMT.thy Wed Aug 10 00:31:51 2011 -0700
@@ -7,7 +7,6 @@
theory SMT
imports Record
uses
- "Tools/lambda_lifting.ML"
"Tools/SMT/smt_utils.ML"
"Tools/SMT/smt_failure.ML"
"Tools/SMT/smt_config.ML"
--- a/src/HOL/TPTP/atp_export.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/TPTP/atp_export.ML Wed Aug 10 00:31:51 2011 -0700
@@ -160,8 +160,7 @@
facts
|> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
|> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
- (rpair [] o map (introduce_combinators ctxt))
- false true [] @{prop False}
+ combinatorsN false true [] @{prop False}
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 10 00:31:51 2011 -0700
@@ -25,6 +25,7 @@
best_slices :
Proof.context -> (real * (bool * (int * string * string))) list}
+ val force_sos : bool Config.T
val e_smartN : string
val e_autoN : string
val e_fun_weightN : string
@@ -36,16 +37,14 @@
val e_default_sym_offs_weight : real Config.T
val e_sym_offs_weight_base : real Config.T
val e_sym_offs_weight_span : real Config.T
- val spass_force_sos : bool Config.T
- val vampire_force_sos : bool Config.T
val eN : string
val spassN : string
val vampireN : string
val leo2N : string
val satallaxN : string
- val sine_eN : string
+ val e_sineN : string
val snarkN : string
- val tofof_eN : string
+ val e_tofofN : string
val waldmeisterN : string
val z3_atpN : string
val remote_prefix : string
@@ -103,14 +102,14 @@
(* named ATPs *)
val eN = "e"
+val leo2N = "leo2"
+val satallaxN = "satallax"
val spassN = "spass"
val vampireN = "vampire"
val z3_atpN = "z3_atp"
-val leo2N = "leo2"
-val satallaxN = "satallax"
-val sine_eN = "sine_e"
+val e_sineN = "e_sine"
val snarkN = "snark"
-val tofof_eN = "tofof_e"
+val e_tofofN = "e_tofof"
val waldmeisterN = "waldmeister"
val remote_prefix = "remote_"
@@ -128,6 +127,8 @@
val sosN = "sos"
val no_sosN = "no_sos"
+val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
+
(* E *)
@@ -228,10 +229,49 @@
val e = (eN, e_config)
-(* SPASS *)
+(* LEO-II *)
+
+val leo2_config : atp_config =
+ {exec = ("LEO2_HOME", "leo"),
+ required_execs = [],
+ arguments =
+ fn _ => fn _ => fn sos => fn timeout => fn _ =>
+ "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
+ |> sos = sosN ? prefix "--sos ",
+ proof_delims = tstp_proof_delims,
+ known_failures = [],
+ conj_sym_kind = Axiom,
+ prem_kind = Hypothesis,
+ formats = [THF, FOF],
+ best_slices = fn ctxt =>
+ (* FUDGE *)
+ [(0.667, (false, (150, "simple_higher", sosN))),
+ (0.333, (true, (50, "simple_higher", no_sosN)))]
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
+ else I)}
-val spass_force_sos =
- Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
+val leo2 = (leo2N, leo2_config)
+
+
+(* Satallax *)
+
+val satallax_config : atp_config =
+ {exec = ("SATALLAX_HOME", "satallax"),
+ required_execs = [],
+ arguments =
+ fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ "-t " ^ string_of_int (to_secs 1 timeout),
+ proof_delims = tstp_proof_delims,
+ known_failures = [(ProofMissing, "SZS status Theorem")],
+ conj_sym_kind = Axiom,
+ prem_kind = Hypothesis,
+ formats = [THF],
+ best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
+
+val satallax = (satallaxN, satallax_config)
+
+
+(* SPASS *)
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
@@ -260,7 +300,7 @@
[(0.333, (false, (150, "mangled_tags", sosN))),
(0.333, (false, (300, "poly_tags?", sosN))),
(0.334, (true, (50, "mangled_tags?", no_sosN)))]
- |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
val spass = (spassN, spass_config)
@@ -268,9 +308,6 @@
(* Vampire *)
-val vampire_force_sos =
- Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
-
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
@@ -301,7 +338,7 @@
[(0.333, (false, (150, "poly_guards", sosN))),
(0.334, (true, (50, "mangled_guards?", no_sosN))),
(0.333, (false, (500, "mangled_tags?", sosN)))]
- |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
val vampire = (vampireN, vampire_config)
@@ -411,26 +448,26 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
(K (750, "mangled_tags?") (* FUDGE *))
+val remote_leo2 =
+ remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
+ (K (100, "simple_higher") (* FUDGE *))
+val remote_satallax =
+ remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
+ (K (100, "simple_higher") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
(K (200, "mangled_guards?") (* FUDGE *))
val remote_z3_atp =
remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
-val remote_leo2 =
- remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
- (K (100, "simple_higher") (* FUDGE *))
-val remote_satallax =
- remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
- (K (64, "simple_higher") (* FUDGE *))
-val remote_sine_e =
- remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
+val remote_e_sine =
+ remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
[TFF, FOF] (K (100, "simple") (* FUDGE *))
-val remote_tofof_e =
- remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
+val remote_e_tofof =
+ remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
@@ -461,9 +498,9 @@
Synchronized.change systems (fn _ => get_systems ())
val atps =
- [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
- remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e,
- remote_waldmeister]
+ [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
+ remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
+ remote_e_tofof, remote_waldmeister]
val setup = fold add_atp atps
end;
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Aug 10 00:31:51 2011 -0700
@@ -31,6 +31,13 @@
Guards of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
+ val no_lambdasN : string
+ val concealedN : string
+ val liftingN : string
+ val combinatorsN : string
+ val hybridN : string
+ val lambdasN : string
+ val smartN : string
val bound_var_prefix : string
val schematic_var_prefix : string
val fixed_var_prefix : string
@@ -88,11 +95,10 @@
val unmangled_const_name : string -> string
val helper_table : ((string * bool) * thm list) list
val factsN : string
- val introduce_combinators : Proof.context -> term -> term
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
- -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
- -> term -> ((string * locality) * term) list
+ -> bool -> string -> bool -> bool -> term list -> term
+ -> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
* (string * locality) list vector * int list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
@@ -106,6 +112,14 @@
type name = string * string
+val no_lambdasN = "no_lambdas"
+val concealedN = "concealed"
+val liftingN = "lifting"
+val combinatorsN = "combinators"
+val hybridN = "hybrid"
+val lambdasN = "lambdas"
+val smartN = "smart"
+
val generate_info = false (* experimental *)
fun isabelle_info s =
@@ -606,6 +620,29 @@
| _ => type_enc)
| format => (format, type_enc))
+fun lift_lambdas ctxt type_enc =
+ map (close_form o Envir.eta_contract) #> rpair ctxt
+ #-> Lambda_Lifting.lift_lambdas
+ (if polymorphism_of_type_enc type_enc = Polymorphic then
+ SOME polymorphic_free_prefix
+ else
+ NONE)
+ Lambda_Lifting.is_quantifier
+ #> fst
+
+fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
+ intentionalize_def t
+ | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+ let
+ fun lam T t = Abs (Name.uu, T, t)
+ val (head, args) = strip_comb t ||> rev
+ val head_T = fastype_of head
+ val n = length args
+ val arg_Ts = head_T |> binder_types |> take n |> rev
+ val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
+ in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
+ | intentionalize_def t = t
+
type translated_formula =
{name : string,
locality : locality,
@@ -834,8 +871,13 @@
| (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
| (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
| (false, s) =>
- if is_tptp_equal s then IConst (`I tptp_equal, T, [])
- else IConst (proxy_base |>> prefix const_prefix, T, T_args)
+ if is_tptp_equal s andalso length args = 2 then
+ IConst (`I tptp_equal, T, [])
+ else
+ (* Use a proxy even for partially applied THF equality, because
+ the LEO-II and Satallax parsers complain about not being
+ able to infer the type of "=". *)
+ IConst (proxy_base |>> prefix const_prefix, T, T_args)
| _ => IConst (name, T, [])
else
IConst (proxy_base |>> prefix const_prefix, T, T_args)
@@ -1918,9 +1960,36 @@
val explicit_apply = NONE (* for experiments *)
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
- exporter trans_lambdas readable_names preproc hyp_ts concl_t facts =
+ exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
let
val (format, type_enc) = choose_format [format] type_enc
+ val lambda_trans =
+ if lambda_trans = smartN then
+ if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
+ else if lambda_trans = lambdasN andalso
+ not (is_type_enc_higher_order type_enc) then
+ error ("Lambda translation method incompatible with first-order \
+ \encoding.")
+ else
+ lambda_trans
+ val trans_lambdas =
+ if lambda_trans = no_lambdasN then
+ rpair []
+ else if lambda_trans = concealedN then
+ lift_lambdas ctxt type_enc ##> K []
+ else if lambda_trans = liftingN then
+ lift_lambdas ctxt type_enc
+ else if lambda_trans = combinatorsN then
+ map (introduce_combinators ctxt) #> rpair []
+ else if lambda_trans = hybridN then
+ lift_lambdas ctxt type_enc
+ ##> maps (fn t => [t, introduce_combinators ctxt
+ (intentionalize_def t)])
+ else if lambda_trans = lambdasN then
+ map (Envir.eta_contract) #> rpair []
+ else
+ error ("Unknown lambda translation method: " ^
+ quote lambda_trans ^ ".")
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts
--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Aug 10 00:31:51 2011 -0700
@@ -197,7 +197,7 @@
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
- (rpair []) false false [] @{prop False} props
+ no_lambdasN false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 10 00:31:51 2011 -0700
@@ -199,7 +199,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put SPASS first. *)
fun default_provers_param_value ctxt =
- [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, sine_eN, waldmeisterN]
+ [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
max_default_remote_threads)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Aug 10 00:31:51 2011 -0700
@@ -60,12 +60,6 @@
type prover =
params -> (string -> minimize_command) -> prover_problem -> prover_result
- val concealedN : string
- val liftingN : string
- val combinatorsN : string
- val hybridN : string
- val lambdasN : string
- val smartN : string
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
@@ -335,13 +329,6 @@
(* configuration attributes *)
-val concealedN = "concealed"
-val liftingN = "lifting"
-val combinatorsN = "combinators"
-val hybridN = "hybrid"
-val lambdasN = "lambdas"
-val smartN = "smart"
-
(* Empty string means create files in Isabelle's temporary files directory. *)
val dest_dir =
Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
@@ -527,56 +514,6 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
-fun lift_lambdas ctxt type_enc =
- map (close_form o Envir.eta_contract) #> rpair ctxt
- #-> Lambda_Lifting.lift_lambdas
- (if polymorphism_of_type_enc type_enc = Polymorphic then
- SOME polymorphic_free_prefix
- else
- NONE)
- Lambda_Lifting.is_quantifier
- #> fst
-
-fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
- intentionalize_def t
- | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
- let
- fun lam T t = Abs (Name.uu, T, t)
- val (head, args) = strip_comb t ||> rev
- val head_T = fastype_of head
- val n = length args
- val arg_Ts = head_T |> binder_types |> take n |> rev
- val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
- in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
- | intentionalize_def t = t
-
-fun translate_atp_lambdas ctxt type_enc =
- Config.get ctxt atp_lambda_translation
- |> (fn trans =>
- if trans = smartN then
- if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
- else if trans = lambdasN andalso
- not (is_type_enc_higher_order type_enc) then
- error ("Lambda translation method incompatible with first-order \
- \encoding.")
- else
- trans)
- |> (fn trans =>
- if trans = concealedN then
- lift_lambdas ctxt type_enc ##> K []
- else if trans = liftingN then
- lift_lambdas ctxt type_enc
- else if trans = combinatorsN then
- map (introduce_combinators ctxt) #> rpair []
- else if trans = hybridN then
- lift_lambdas ctxt type_enc
- ##> maps (fn t => [t, introduce_combinators ctxt
- (intentionalize_def t)])
- else if trans = lambdasN then
- map (Envir.eta_contract) #> rpair []
- else
- error ("Unknown lambda translation method: " ^ quote trans ^ "."))
-
val metis_minimize_max_time = seconds 2.0
fun choose_minimize_command minimize_command name preplay =
@@ -708,7 +645,8 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_enc sound false (translate_atp_lambdas ctxt type_enc)
+ type_enc sound false
+ (Config.get ctxt atp_lambda_translation)
(Config.get ctxt atp_readable_names) true hyp_ts concl_t
facts
fun weights () = atp_problem_weights atp_problem
--- a/src/HOL/UNITY/ELT.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/UNITY/ELT.thy Wed Aug 10 00:31:51 2011 -0700
@@ -186,9 +186,7 @@
lemma leadsETo_Un:
"[| F : A leadsTo[CC] C; F : B leadsTo[CC] C |]
==> F : (A Un B) leadsTo[CC] C"
-apply (subst Un_eq_Union)
-apply (blast intro: leadsETo_Union)
-done
+ using leadsETo_Union [of "{A, B}" F CC C] by auto
lemma single_leadsETo_I:
"(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
@@ -407,9 +405,7 @@
lemma LeadsETo_Un:
"[| F : A LeadsTo[CC] C; F : B LeadsTo[CC] C |]
==> F : (A Un B) LeadsTo[CC] C"
-apply (subst Un_eq_Union)
-apply (blast intro: LeadsETo_Union)
-done
+ using LeadsETo_Union [of "{A, B}" F CC C] by auto
(*Lets us look at the starting state*)
lemma single_LeadsETo_I:
--- a/src/HOL/UNITY/ProgressSets.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/UNITY/ProgressSets.thy Wed Aug 10 00:31:51 2011 -0700
@@ -42,25 +42,21 @@
lemma UN_in_lattice:
"[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Union>i\<in>I. r i) \<in> L"
-apply (simp add: UN_eq)
+apply (unfold SUP_def)
apply (blast intro: Union_in_lattice)
done
lemma INT_in_lattice:
"[|lattice L; !!i. i\<in>I ==> r i \<in> L|] ==> (\<Inter>i\<in>I. r i) \<in> L"
-apply (simp add: INT_eq)
+apply (unfold INF_def)
apply (blast intro: Inter_in_lattice)
done
lemma Un_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<union>y \<in> L"
-apply (simp only: Un_eq_Union)
-apply (blast intro: Union_in_lattice)
-done
+ using Union_in_lattice [of "{x, y}" L] by simp
lemma Int_in_lattice: "[|x\<in>L; y\<in>L; lattice L|] ==> x\<inter>y \<in> L"
-apply (simp only: Int_eq_Inter)
-apply (blast intro: Inter_in_lattice)
-done
+ using Inter_in_lattice [of "{x, y}" L] by simp
lemma lattice_stable: "lattice {X. F \<in> stable X}"
by (simp add: lattice_def stable_def constrains_def, blast)
--- a/src/HOL/UNITY/SubstAx.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/UNITY/SubstAx.thy Wed Aug 10 00:31:51 2011 -0700
@@ -85,16 +85,14 @@
lemma LeadsTo_UN:
"(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
-apply (simp only: Union_image_eq [symmetric])
+apply (unfold SUP_def)
apply (blast intro: LeadsTo_Union)
done
text{*Binary union introduction rule*}
lemma LeadsTo_Un:
"[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
-apply (subst Un_eq_Union)
-apply (blast intro: LeadsTo_Union)
-done
+ using LeadsTo_UN [of "{A, B}" F id C] by auto
text{*Lets us look at the starting state*}
lemma single_LeadsTo_I:
--- a/src/HOL/UNITY/Transformers.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/UNITY/Transformers.thy Wed Aug 10 00:31:51 2011 -0700
@@ -467,7 +467,7 @@
"single_valued act
==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq>
wens_set (mk_program (init, {act}, allowed)) B"
-apply (simp add: wens_single_eq_Union UN_eq)
+apply (simp add: SUP_def image_def wens_single_eq_Union)
apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
done
--- a/src/HOL/UNITY/WFair.thy Wed Aug 10 00:29:31 2011 -0700
+++ b/src/HOL/UNITY/WFair.thy Wed Aug 10 00:31:51 2011 -0700
@@ -211,9 +211,7 @@
text{*Binary union introduction rule*}
lemma leadsTo_Un:
"[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
-apply (subst Un_eq_Union)
-apply (blast intro: leadsTo_Union)
-done
+ using leadsTo_Union [of "{A, B}" F C] by auto
lemma single_leadsTo_I:
"(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B"
--- a/src/Pure/Syntax/parser.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/Pure/Syntax/parser.ML Wed Aug 10 00:31:51 2011 -0700
@@ -747,7 +747,7 @@
in get_prods (connected_with chains nts nts) [] end;
-fun PROCESSS ctxt warned prods chains Estate i c states =
+fun PROCESSS ctxt prods chains Estate i c states =
let
fun all_prods_for nt = prods_for prods chains true c [nt];
@@ -773,14 +773,6 @@
val tk_prods = all_prods_for nt;
val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods);
in (Inttab.update (nt, (min_prec, [])) used, States') end);
-
- val _ =
- if not (! warned) andalso
- length new_states + length States > Config.get ctxt branching_level then
- (Context_Position.if_visible ctxt warning
- "Currently parsed expression could be extremely ambiguous";
- warned := true)
- else ();
in
processS used' (new_states @ States) (S :: Si, Sii)
end
@@ -803,7 +795,7 @@
in processS Inttab.empty states ([], []) end;
-fun produce ctxt warned prods tags chains stateset i indata prev_token =
+fun produce ctxt prods tags chains stateset i indata prev_token =
(case Array.sub (stateset, i) of
[] =>
let
@@ -821,10 +813,10 @@
[] => s
| c :: cs =>
let
- val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
+ val (si, sii) = PROCESSS ctxt prods chains stateset i c s;
val _ = Array.update (stateset, i, si);
val _ = Array.update (stateset, i + 1, sii);
- in produce ctxt warned prods tags chains stateset (i + 1) cs c end));
+ in produce ctxt prods tags chains stateset (i + 1) cs c end));
fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
@@ -841,7 +833,7 @@
val _ = Array.update (Estate, 0, S0);
in
get_trees
- (produce ctxt (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
+ (produce ctxt prods tags chains Estate 0 indata Lexicon.eof)
end;
--- a/src/Pure/proofterm.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/Pure/proofterm.ML Wed Aug 10 00:31:51 2011 -0700
@@ -567,13 +567,16 @@
(**** Freezing and thawing of variables in proof terms ****)
+local
+
fun frzT names =
- map_type_tvar (fn (ixn, xs) => TFree ((the o AList.lookup (op =) names) ixn, xs));
+ map_type_tvar (fn (ixn, S) => TFree (the (AList.lookup (op =) names ixn), S));
fun thawT names =
- map_type_tfree (fn (s, xs) => case AList.lookup (op =) names s of
- NONE => TFree (s, xs)
- | SOME ixn => TVar (ixn, xs));
+ map_type_tfree (fn (a, S) =>
+ (case AList.lookup (op =) names a of
+ NONE => TFree (a, S)
+ | SOME ixn => TVar (ixn, S)));
fun freeze names names' (t $ u) =
freeze names names' t $ freeze names names' u
@@ -582,7 +585,7 @@
| freeze names names' (Const (s, T)) = Const (s, frzT names' T)
| freeze names names' (Free (s, T)) = Free (s, frzT names' T)
| freeze names names' (Var (ixn, T)) =
- Free ((the o AList.lookup (op =) names) ixn, frzT names' T)
+ Free (the (AList.lookup (op =) names ixn), frzT names' T)
| freeze names names' t = t;
fun thaw names names' (t $ u) =
@@ -591,14 +594,16 @@
Abs (s, thawT names' T, thaw names names' t)
| thaw names names' (Const (s, T)) = Const (s, thawT names' T)
| thaw names names' (Free (s, T)) =
- let val T' = thawT names' T
- in case AList.lookup (op =) names s of
+ let val T' = thawT names' T in
+ (case AList.lookup (op =) names s of
NONE => Free (s, T')
- | SOME ixn => Var (ixn, T')
+ | SOME ixn => Var (ixn, T'))
end
| thaw names names' (Var (ixn, T)) = Var (ixn, thawT names' T)
| thaw names names' t = t;
+in
+
fun freeze_thaw_prf prf =
let
val (fs, Tfs, vs, Tvs) = fold_proof_terms
@@ -618,6 +623,8 @@
map_proof_terms (thaw rnames rnames') (thawT rnames'))
end;
+end;
+
(***** implication introduction *****)
@@ -881,23 +888,25 @@
let
val f = Envir.beta_norm f;
val g = Envir.beta_norm g;
- val prf = if check_comb prf1 then
+ val prf =
+ if check_comb prf1 then
combination_axm % NONE % NONE
- else (case prf1 of
+ else
+ (case prf1 of
PAxm ("Pure.reflexive", _, _) % _ =>
combination_axm %> remove_types f % NONE
| _ => combination_axm %> remove_types f %> remove_types g)
in
(case T of
- Type ("fun", _) => prf %
- (case head_of f of
- Abs _ => SOME (remove_types t)
- | Var _ => SOME (remove_types t)
- | _ => NONE) %
- (case head_of g of
- Abs _ => SOME (remove_types u)
- | Var _ => SOME (remove_types u)
- | _ => NONE) %% prf1 %% prf2
+ Type ("fun", _) => prf %
+ (case head_of f of
+ Abs _ => SOME (remove_types t)
+ | Var _ => SOME (remove_types t)
+ | _ => NONE) %
+ (case head_of g of
+ Abs _ => SOME (remove_types u)
+ | Var _ => SOME (remove_types u)
+ | _ => NONE) %% prf1 %% prf2
| _ => prf % NONE % NONE %% prf1 %% prf2)
end;
--- a/src/Pure/thm.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/Pure/thm.ML Wed Aug 10 00:31:51 2011 -0700
@@ -1515,44 +1515,61 @@
prop = prop'}));
-(* strip_apply f (A, B) strips off all assumptions/parameters from A
+(* strip_apply f B A strips off all assumptions/parameters from A
introduced by lifting over B, and applies f to remaining part of A*)
fun strip_apply f =
- let fun strip(Const("==>",_)$ A1 $ B1,
- Const("==>",_)$ _ $ B2) = Logic.mk_implies (A1, strip(B1,B2))
- | strip((c as Const("all",_)) $ Abs(a,T,t1),
- Const("all",_) $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))
- | strip(A,_) = f A
+ let fun strip (Const ("==>", _) $ _ $ B1)
+ (Const ("==>", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
+ | strip ((c as Const ("all", _)) $ Abs (_, _, t1))
+ ( Const ("all", _) $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
+ | strip _ A = f A
in strip end;
+fun strip_lifted (Const ("==>", _) $ _ $ B1)
+ (Const ("==>", _) $ _ $ B2) = strip_lifted B1 B2
+ | strip_lifted (Const ("all", _) $ Abs (_, _, t1))
+ (Const ("all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
+ | strip_lifted _ A = A;
+
(*Use the alist to rename all bound variables and some unknowns in a term
dpairs = current disagreement pairs; tpairs = permanent ones (flexflex);
Preserves unknowns in tpairs and on lhs of dpairs. *)
-fun rename_bvs([],_,_,_) = I
- | rename_bvs(al,dpairs,tpairs,B) =
+fun rename_bvs [] _ _ _ _ = K I
+ | rename_bvs al dpairs tpairs B As =
let
val add_var = fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I);
val vids = []
|> fold (add_var o fst) dpairs
|> fold (add_var o fst) tpairs
|> fold (add_var o snd) tpairs;
+ val vids' = fold (add_var o strip_lifted B) As [];
(*unknowns appearing elsewhere be preserved!*)
- fun rename(t as Var((x,i),T)) =
- (case AList.lookup (op =) al x of
- SOME y =>
- if member (op =) vids x orelse member (op =) vids y then t
- else Var((y,i),T)
- | NONE=> t)
- | rename(Abs(x,T,t)) =
+ val al' = distinct ((op =) o pairself fst)
+ (filter_out (fn (x, y) =>
+ not (member (op =) vids' x) orelse
+ member (op =) vids x orelse member (op =) vids y) al);
+ val unchanged = filter_out (AList.defined (op =) al') vids';
+ fun del_clashing clash xs _ [] qs =
+ if clash then del_clashing false xs xs qs [] else qs
+ | del_clashing clash xs ys ((p as (x, y)) :: ps) qs =
+ if member (op =) ys y
+ then del_clashing true (x :: xs) (x :: ys) ps qs
+ else del_clashing clash xs (y :: ys) ps (p :: qs);
+ val al'' = del_clashing false unchanged unchanged al' [];
+ fun rename (t as Var ((x, i), T)) =
+ (case AList.lookup (op =) al'' x of
+ SOME y => Var ((y, i), T)
+ | NONE => t)
+ | rename (Abs (x, T, t)) =
Abs (the_default x (AList.lookup (op =) al x), T, rename t)
- | rename(f$t) = rename f $ rename t
- | rename(t) = t;
- fun strip_ren Ai = strip_apply rename (Ai,B)
+ | rename (f $ t) = rename f $ rename t
+ | rename t = t;
+ fun strip_ren f Ai = f rename B Ai
in strip_ren end;
(*Function to rename bounds/unknowns in the argument, lifted over B*)
-fun rename_bvars(dpairs, tpairs, B) =
- rename_bvs(List.foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
+fun rename_bvars dpairs =
+ rename_bvs (List.foldr Term.match_bvars [] dpairs) dpairs;
(*** RESOLUTION ***)
@@ -1640,9 +1657,11 @@
fun newAs(As0, n, dpairs, tpairs) =
let val (As1, rder') =
if not lifted then (As0, rder)
- else (map (rename_bvars(dpairs,tpairs,B)) As0,
- deriv_rule1 (Proofterm.map_proof_terms
- (rename_bvars (dpairs, tpairs, Bound 0)) I) rder);
+ else
+ let val rename = rename_bvars dpairs tpairs B As0
+ in (map (rename strip_apply) As0,
+ deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder)
+ end;
in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
handle TERM _ =>
raise THM("bicompose: 1st premise", 0, [orule])
--- a/src/Tools/eqsubst.ML Wed Aug 10 00:29:31 2011 -0700
+++ b/src/Tools/eqsubst.ML Wed Aug 10 00:31:51 2011 -0700
@@ -108,10 +108,6 @@
val searchf_bt_unify_valid :
searchinfo -> term -> match Seq.seq Seq.seq
- (* syntax tools *)
- val ith_syntax : int list parser
- val options_syntax : bool parser
-
(* Isar level hooks *)
val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
@@ -546,23 +542,15 @@
fun eqsubst_asm_meth ctxt occL inthms =
SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
-(* syntax for options, given "(asm)" will give back true, without
- gives back false *)
-val options_syntax =
- (Args.parens (Args.$$$ "asm") >> (K true)) ||
- (Scan.succeed false);
-
-val ith_syntax =
- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
-
(* combination method that takes a flag (true indicates that subst
should be done to an assumption, false = apply to the conclusion of
the goal) as well as the theorems to use *)
val setup =
Method.setup @{binding subst}
- (Scan.lift (options_syntax -- ith_syntax) -- Attrib.thms >>
- (fn ((asmflag, occL), inthms) => fn ctxt =>
- (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
+ (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
+ Attrib.thms >>
+ (fn ((asm, occL), inthms) => fn ctxt =>
+ (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
"single-step substitution";
end;