--- a/Admin/polyml/build Sun Aug 22 22:28:24 2010 +0200
+++ b/Admin/polyml/build Mon Aug 23 11:18:38 2010 +0200
@@ -52,11 +52,13 @@
;;
x86-darwin)
OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3'
- CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3')
+ CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3'
+ LDFLAGS='-segprot POLY rwx rwx')
;;
x86_64-darwin)
OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3'
- CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64')
+ CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64'
+ LDFLAGS='-segprot POLY rwx rwx')
;;
x86-cygwin)
OPTIONS=()
--- a/NEWS Sun Aug 22 22:28:24 2010 +0200
+++ b/NEWS Mon Aug 23 11:18:38 2010 +0200
@@ -35,6 +35,10 @@
*** HOL ***
+* Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
+canonical names for instance definitions for functions; various improvements.
+INCOMPATIBILITY.
+
* Records: logical foundation type for records do not carry a '_type' suffix
any longer. INCOMPATIBILITY.
--- a/doc-src/Sledgehammer/sledgehammer.tex Sun Aug 22 22:28:24 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Aug 23 11:18:38 2010 +0200
@@ -343,6 +343,7 @@
\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
\item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or \textit{smart}.
\item[$\bullet$] \qtybf{int\/}: An integer.
+\item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}.
\item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), $s$ (seconds), or \textit{ms}
(milliseconds), or the keyword \textit{none} ($\infty$ years).
\end{enum}
@@ -384,24 +385,31 @@
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
that contains the \texttt{vampire} executable.
-\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E executes
+\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\_vampire}:} The remote version of
-Vampire executes on Geoff Sutcliffe's Miami servers. Version 9 is used.
+Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
+\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E 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\_snark}:} SNARK is a prover
+developed by Stickel et al.\ \cite{snark}. The remote version of
+SNARK runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer will run E, SPASS, and Vampire in parallel. For E and
-SPASS, it will use any locally installed version if available, falling back
-on the remote versions if necessary. For historical reasons, the default value
-of this option can be overridden using the option ``Sledgehammer: ATPs'' from
-the ``Isabelle'' menu in Proof General.
+By default, Sledgehammer will run E, SPASS, Vampire, and SInE-E in parallel.
+For at most two of E, SPASS, and Vampire, it will use any locally installed
+version if available. For historical reasons, the default value of this option
+can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
+menu in Proof General.
It is a good idea to run several ATPs in parallel, although it could slow down
-your machine. Tobias Nipkow observed that running E, SPASS, and Vampire together
-for 5 seconds yields the same success rate as running the most effective of
-these (Vampire) for 120 seconds \cite{boehme-nipkow-2010}.
+your machine. Running E, SPASS, and Vampire together for 5 seconds yields about
+the same success rate as running the most effective of these (Vampire) for 120
+seconds \cite{boehme-nipkow-2010}.
\opnodefault{atp}{string}
Alias for \textit{atps}.
@@ -433,7 +441,12 @@
the ATPs significantly. For historical reasons, the default value of this option
can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
menu in Proof General.
+\end{enum}
+\subsection{Relevance Filter}
+\label{relevance-filter}
+
+\begin{enum}
\opdefault{relevance\_threshold}{int}{50}
Specifies the threshold above which facts are considered relevant by the
relevance filter. The option ranges from 0 to 100, where 0 means that all
@@ -444,6 +457,12 @@
filter. This quotient is used by the relevance filter to scale down the
relevance of facts at each iteration of the filter.
+\opdefault{max\_relevant\_per\_iter}{int\_or\_smart}{\textit{smart}}
+Specifies the maximum number of facts that may be added during one iteration of
+the relevance filter. If the option is set to \textit{smart}, it is set to a
+value that was empirically found to be appropriate for the ATP. A typical value
+would be 50.
+
\opsmartx{theory\_relevant}{theory\_irrelevant}
Specifies whether the theory from which a fact comes should be taken into
consideration by the relevance filter. If the option is set to \textit{smart},
@@ -495,10 +514,6 @@
proof. For historical reasons, the default value of this option can be
overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
menu in Proof General.
-
-\opdefault{minimize\_timeout}{time}{$\mathbf{5}$\,s}
-Specifies the maximum amount of time that the ATPs should spend looking for a
-proof for \textbf{sledgehammer}~\textit{minimize}.
\end{enum}
\let\em=\sl
--- a/doc-src/manual.bib Sun Aug 22 22:28:24 2010 +0200
+++ b/doc-src/manual.bib Mon Aug 23 11:18:38 2010 +0200
@@ -591,6 +591,11 @@
number = 5,
month = May}
+@misc{sine,
+ author = "Kry\v{s}tof Hoder",
+ title = "SInE (Sumo Inference Engine)",
+ note = "\url{http://www.cs.man.ac.uk/~hoderk/sine/}"}
+
@book{Hudak-Haskell,author={Paul Hudak},
title={The Haskell School of Expression},publisher=CUP,year=2000}
@@ -714,6 +719,15 @@
title = {The Objective Caml system -- Documentation and user's manual},
note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}}
+@incollection{lochbihler-2010,
+ title = "Coinduction",
+ author = "Andreas Lochbihler",
+ booktitle = "The Archive of Formal Proofs",
+ editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
+ publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
+ month = "Feb.",
+ year = 2010}
+
@InProceedings{lowe-fdr,
author = {Gavin Lowe},
title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
@@ -1335,6 +1349,12 @@
crossref = {tphols96},
pages = {381-397}}
+@inproceedings{snark,
+ author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood},
+ title = {Deductive composition of astronomical software from subroutine libraries},
+ pages = "341--355",
+ crossref = {cade12}}
+
@book{suppes72,
author = {Patrick Suppes},
title = {Axiomatic Set Theory},
@@ -1819,12 +1839,3 @@
key = "Wikipedia",
title = "Wikipedia: {AA} Tree",
note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
-
-@incollection{lochbihler-2010,
- title = "Coinduction",
- author = "Andreas Lochbihler",
- booktitle = "The Archive of Formal Proofs",
- editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
- publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
- month = "Feb.",
- year = 2010}
--- a/src/HOL/Fun.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Fun.thy Mon Aug 23 11:18:38 2010 +0200
@@ -162,6 +162,13 @@
lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
by (force simp add: inj_on_def)
+lemma inj_comp:
+ "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
+ by (simp add: inj_on_def)
+
+lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
+ by (simp add: inj_on_def expand_fun_eq)
+
lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
by (simp add: inj_on_eq_iff)
--- a/src/HOL/IsaMakefile Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Aug 23 11:18:38 2010 +0200
@@ -408,6 +408,7 @@
Library/Executable_Set.thy Library/Float.thy \
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \
Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy \
+ Library/Function_Algebras.thy \
Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \
Library/Indicator_Function.thy Library/Infinite_Set.thy \
Library/Inner_Product.thy Library/Kleene_Algebra.thy \
@@ -428,8 +429,8 @@
Library/Quotient_Product.thy Library/Quotient_Sum.thy \
Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
Library/RBT.thy Library/RBT_Impl.thy Library/README.html \
- Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy \
- Library/SML_Quickcheck.thy Library/SetsAndFunctions.thy \
+ Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
+ Library/Reflection.thy Library/SML_Quickcheck.thy \
Library/Sublist_Order.thy Library/Sum_Of_Squares.thy \
Library/Sum_Of_Squares/sos_wrapper.ML \
Library/Sum_Of_Squares/sum_of_squares.ML \
--- a/src/HOL/Library/BigO.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Library/BigO.thy Mon Aug 23 11:18:38 2010 +0200
@@ -5,7 +5,7 @@
header {* Big O notation *}
theory BigO
-imports Complex_Main SetsAndFunctions
+imports Complex_Main Function_Algebras Set_Algebras
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Function_Algebras.thy Mon Aug 23 11:18:38 2010 +0200
@@ -0,0 +1,207 @@
+(* Title: HOL/Library/Function_Algebras.thy
+ Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
+*)
+
+header {* Pointwise instantiation of functions to algebra type classes *}
+
+theory Function_Algebras
+imports Main
+begin
+
+text {* Pointwise operations *}
+
+instantiation "fun" :: (type, plus) plus
+begin
+
+definition
+ "f + g = (\<lambda>x. f x + g x)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, zero) zero
+begin
+
+definition
+ "0 = (\<lambda>x. 0)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, times) times
+begin
+
+definition
+ "f * g = (\<lambda>x. f x * g x)"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, one) one
+begin
+
+definition
+ "1 = (\<lambda>x. 1)"
+
+instance ..
+
+end
+
+
+text {* Additive structures *}
+
+instance "fun" :: (type, semigroup_add) semigroup_add proof
+qed (simp add: plus_fun_def add.assoc)
+
+instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add proof
+qed (simp_all add: plus_fun_def expand_fun_eq)
+
+instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add proof
+qed (simp add: plus_fun_def add.commute)
+
+instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add proof
+qed simp
+
+instance "fun" :: (type, monoid_add) monoid_add proof
+qed (simp_all add: plus_fun_def zero_fun_def)
+
+instance "fun" :: (type, comm_monoid_add) comm_monoid_add proof
+qed simp
+
+instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
+
+instance "fun" :: (type, group_add) group_add proof
+qed (simp_all add: plus_fun_def zero_fun_def fun_Compl_def fun_diff_def diff_minus)
+
+instance "fun" :: (type, ab_group_add) ab_group_add proof
+qed (simp_all add: diff_minus)
+
+
+text {* Multiplicative structures *}
+
+instance "fun" :: (type, semigroup_mult) semigroup_mult proof
+qed (simp add: times_fun_def mult.assoc)
+
+instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult proof
+qed (simp add: times_fun_def mult.commute)
+
+instance "fun" :: (type, ab_semigroup_idem_mult) ab_semigroup_idem_mult proof
+qed (simp add: times_fun_def)
+
+instance "fun" :: (type, monoid_mult) monoid_mult proof
+qed (simp_all add: times_fun_def one_fun_def)
+
+instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult proof
+qed simp
+
+
+text {* Misc *}
+
+instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
+
+instance "fun" :: (type, mult_zero) mult_zero proof
+qed (simp_all add: zero_fun_def times_fun_def)
+
+instance "fun" :: (type, mult_mono) mult_mono proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
+
+instance "fun" :: (type, mult_mono1) mult_mono1 proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
+
+instance "fun" :: (type, zero_neq_one) zero_neq_one proof
+qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
+
+
+text {* Ring structures *}
+
+instance "fun" :: (type, semiring) semiring proof
+qed (simp_all add: plus_fun_def times_fun_def algebra_simps)
+
+instance "fun" :: (type, comm_semiring) comm_semiring proof
+qed (simp add: plus_fun_def times_fun_def algebra_simps)
+
+instance "fun" :: (type, semiring_0) semiring_0 ..
+
+instance "fun" :: (type, comm_semiring_0) comm_semiring_0 ..
+
+instance "fun" :: (type, semiring_0_cancel) semiring_0_cancel ..
+
+instance "fun" :: (type, comm_semiring_0_cancel) comm_semiring_0_cancel ..
+
+instance "fun" :: (type, semiring_1) semiring_1 ..
+
+lemma of_nat_fun:
+ shows "of_nat n = (\<lambda>x::'a. of_nat n)"
+proof -
+ have comp: "comp = (\<lambda>f g x. f (g x))"
+ by (rule ext)+ simp
+ have plus_fun: "plus = (\<lambda>f g x. f x + g x)"
+ by (rule ext, rule ext) (fact plus_fun_def)
+ have "of_nat n = (comp (plus (1::'b)) ^^ n) (\<lambda>x::'a. 0)"
+ by (simp add: of_nat_def plus_fun zero_fun_def one_fun_def comp)
+ also have "... = comp ((plus 1) ^^ n) (\<lambda>x::'a. 0)"
+ by (simp only: comp_funpow)
+ finally show ?thesis by (simp add: of_nat_def comp)
+qed
+
+instance "fun" :: (type, comm_semiring_1) comm_semiring_1 ..
+
+instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
+
+instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel ..
+
+instance "fun" :: (type, semiring_char_0) semiring_char_0 proof
+ from inj_of_nat have "inj (\<lambda>n (x::'a). of_nat n :: 'b)"
+ by (rule inj_fun)
+ then have "inj (\<lambda>n. of_nat n :: 'a \<Rightarrow> 'b)"
+ by (simp add: of_nat_fun)
+ then show "inj (of_nat :: nat \<Rightarrow> 'a \<Rightarrow> 'b)" .
+qed
+
+instance "fun" :: (type, ring) ring ..
+
+instance "fun" :: (type, comm_ring) comm_ring ..
+
+instance "fun" :: (type, ring_1) ring_1 ..
+
+instance "fun" :: (type, comm_ring_1) comm_ring_1 ..
+
+instance "fun" :: (type, ring_char_0) ring_char_0 ..
+
+
+text {* Ordereded structures *}
+
+instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add proof
+qed (auto simp add: plus_fun_def le_fun_def intro: add_left_mono)
+
+instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
+
+instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le proof
+qed (simp add: plus_fun_def le_fun_def)
+
+instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
+
+instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
+
+instance "fun" :: (type, ordered_semiring) ordered_semiring ..
+
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
+
+instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
+
+instance "fun" :: (type, ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
+
+instance "fun" :: (type, ordered_ring) ordered_ring ..
+
+instance "fun" :: (type, ordered_comm_ring) ordered_comm_ring ..
+
+
+lemmas func_plus = plus_fun_def
+lemmas func_zero = zero_fun_def
+lemmas func_times = times_fun_def
+lemmas func_one = one_fun_def
+
+end
--- a/src/HOL/Library/Library.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Library/Library.thy Mon Aug 23 11:18:38 2010 +0200
@@ -22,6 +22,7 @@
FrechetDeriv
Fset
FuncSet
+ Function_Algebras
Fundamental_Theorem_Algebra
Indicator_Function
Infinite_Set
@@ -54,6 +55,7 @@
Ramsey
Reflection
RBT
+ Set_Algebras
SML_Quickcheck
State_Monad
Sum_Of_Squares
--- a/src/HOL/Library/Nat_Infinity.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Mon Aug 23 11:18:38 2010 +0200
@@ -227,8 +227,10 @@
apply (simp add: plus_1_iSuc iSuc_Fin)
done
-instance inat :: semiring_char_0
- by default (simp add: of_nat_eq_Fin)
+instance inat :: semiring_char_0 proof
+ have "inj Fin" by (rule injI) simp
+ then show "inj (\<lambda>n. of_nat n :: inat)" by (simp add: of_nat_eq_Fin)
+qed
subsection {* Ordering *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Set_Algebras.thy Mon Aug 23 11:18:38 2010 +0200
@@ -0,0 +1,357 @@
+(* Title: HOL/Library/Set_Algebras.thy
+ Author: Jeremy Avigad and Kevin Donnelly; Florian Haftmann, TUM
+*)
+
+header {* Algebraic operations on sets *}
+
+theory Set_Algebras
+imports Main
+begin
+
+text {*
+ This library lifts operations like addition and muliplication to
+ sets. It was designed to support asymptotic calculations. See the
+ comments at the top of theory @{text BigO}.
+*}
+
+definition set_plus :: "'a::plus set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<oplus>" 65) where
+ "A \<oplus> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a + b}"
+
+definition set_times :: "'a::times set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<otimes>" 70) where
+ "A \<otimes> B = {c. \<exists>a\<in>A. \<exists>b\<in>B. c = a * b}"
+
+definition elt_set_plus :: "'a::plus \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "+o" 70) where
+ "a +o B = {c. \<exists>b\<in>B. c = a + b}"
+
+definition elt_set_times :: "'a::times \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "*o" 80) where
+ "a *o B = {c. \<exists>b\<in>B. c = a * b}"
+
+abbreviation (input) elt_set_eq :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infix "=o" 50) where
+ "x =o A \<equiv> x \<in> A"
+
+interpretation set_add!: semigroup "set_plus :: 'a::semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_plus_def add.assoc)
+
+interpretation set_add!: abel_semigroup "set_plus :: 'a::ab_semigroup_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_plus_def add.commute)
+
+interpretation set_add!: monoid "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
+qed (simp_all add: set_plus_def)
+
+interpretation set_add!: comm_monoid "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" proof
+qed (simp add: set_plus_def)
+
+definition listsum_set :: "('a::monoid_add set) list \<Rightarrow> 'a set" where
+ "listsum_set = monoid_add.listsum set_plus {0}"
+
+interpretation set_add!: monoid_add "set_plus :: 'a::monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
+ "monoid_add.listsum set_plus {0::'a} = listsum_set"
+proof -
+ show "class.monoid_add set_plus {0::'a}" proof
+ qed (simp_all add: set_add.assoc)
+ then interpret set_add!: monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
+ show "monoid_add.listsum set_plus {0::'a} = listsum_set"
+ by (simp only: listsum_set_def)
+qed
+
+definition setsum_set :: "('b \<Rightarrow> ('a::comm_monoid_add) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
+ "setsum_set f A = (if finite A then fold_image set_plus f {0} A else {0})"
+
+interpretation set_add!:
+ comm_monoid_big "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" setsum_set
+proof
+qed (fact setsum_set_def)
+
+interpretation set_add!: comm_monoid_add "set_plus :: 'a::comm_monoid_add set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" where
+ "monoid_add.listsum set_plus {0::'a} = listsum_set"
+ and "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
+proof -
+ show "class.comm_monoid_add (set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {0}" proof
+ qed (simp_all add: set_add.commute)
+ then interpret set_add!: comm_monoid_add "set_plus :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{0}" .
+ show "monoid_add.listsum set_plus {0::'a} = listsum_set"
+ by (simp only: listsum_set_def)
+ show "comm_monoid_add.setsum set_plus {0::'a} = setsum_set"
+ by (simp add: set_add.setsum_def setsum_set_def expand_fun_eq)
+qed
+
+interpretation set_mult!: semigroup "set_times :: 'a::semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_times_def mult.assoc)
+
+interpretation set_mult!: abel_semigroup "set_times :: 'a::ab_semigroup_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" proof
+qed (force simp add: set_times_def mult.commute)
+
+interpretation set_mult!: monoid "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
+qed (simp_all add: set_times_def)
+
+interpretation set_mult!: comm_monoid "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" proof
+qed (simp add: set_times_def)
+
+definition power_set :: "nat \<Rightarrow> ('a::monoid_mult set) \<Rightarrow> 'a set" where
+ "power_set n A = power.power {1} set_times A n"
+
+interpretation set_mult!: monoid_mult "{1}" "set_times :: 'a::monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
+ "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+proof -
+ show "class.monoid_mult {1} (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set)" proof
+ qed (simp_all add: set_mult.assoc)
+ show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+ by (simp add: power_set_def)
+qed
+
+definition setprod_set :: "('b \<Rightarrow> ('a::comm_monoid_mult) set) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
+ "setprod_set f A = (if finite A then fold_image set_times f {1} A else {1})"
+
+interpretation set_mult!:
+ comm_monoid_big "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" setprod_set
+proof
+qed (fact setprod_set_def)
+
+interpretation set_mult!: comm_monoid_mult "set_times :: 'a::comm_monoid_mult set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" where
+ "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+ and "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
+proof -
+ show "class.comm_monoid_mult (set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set) {1}" proof
+ qed (simp_all add: set_mult.commute)
+ then interpret set_mult!: comm_monoid_mult "set_times :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" "{1}" .
+ show "power.power {1} set_times = (\<lambda>A n. power_set n A)"
+ by (simp add: power_set_def)
+ show "comm_monoid_mult.setprod set_times {1::'a} = setprod_set"
+ by (simp add: set_mult.setprod_def setprod_set_def expand_fun_eq)
+qed
+
+lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
+ by (auto simp add: set_plus_def)
+
+lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
+ by (auto simp add: elt_set_plus_def)
+
+lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
+ (b +o D) = (a + b) +o (C \<oplus> D)"
+ apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
+ apply (rule_tac x = "ba + bb" in exI)
+ apply (auto simp add: add_ac)
+ apply (rule_tac x = "aa + a" in exI)
+ apply (auto simp add: add_ac)
+ done
+
+lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
+ (a + b) +o C"
+ by (auto simp add: elt_set_plus_def add_assoc)
+
+lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
+ a +o (B \<oplus> C)"
+ apply (auto simp add: elt_set_plus_def set_plus_def)
+ apply (blast intro: add_ac)
+ apply (rule_tac x = "a + aa" in exI)
+ apply (rule conjI)
+ apply (rule_tac x = "aa" in bexI)
+ apply auto
+ apply (rule_tac x = "ba" in bexI)
+ apply (auto simp add: add_ac)
+ done
+
+theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
+ a +o (C \<oplus> D)"
+ apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
+ apply (rule_tac x = "aa + ba" in exI)
+ apply (auto simp add: add_ac)
+ done
+
+theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
+ set_plus_rearrange3 set_plus_rearrange4
+
+lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
+ by (auto simp add: elt_set_plus_def)
+
+lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
+ C \<oplus> E <= D \<oplus> F"
+ by (auto simp add: set_plus_def)
+
+lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
+ by (auto simp add: elt_set_plus_def set_plus_def)
+
+lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
+ a +o D <= D \<oplus> C"
+ by (auto simp add: elt_set_plus_def set_plus_def add_ac)
+
+lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
+ apply (subgoal_tac "a +o B <= a +o D")
+ apply (erule order_trans)
+ apply (erule set_plus_mono3)
+ apply (erule set_plus_mono)
+ done
+
+lemma set_plus_mono_b: "C <= D ==> x : a +o C
+ ==> x : a +o D"
+ apply (frule set_plus_mono)
+ apply auto
+ done
+
+lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
+ x : D \<oplus> F"
+ apply (frule set_plus_mono2)
+ prefer 2
+ apply force
+ apply assumption
+ done
+
+lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
+ apply (frule set_plus_mono3)
+ apply auto
+ done
+
+lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
+ x : a +o D ==> x : D \<oplus> C"
+ apply (frule set_plus_mono4)
+ apply auto
+ done
+
+lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
+ by (auto simp add: elt_set_plus_def)
+
+lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
+ apply (auto intro!: subsetI simp add: set_plus_def)
+ apply (rule_tac x = 0 in bexI)
+ apply (rule_tac x = x in bexI)
+ apply (auto simp add: add_ac)
+ done
+
+lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
+ by (auto simp add: elt_set_plus_def add_ac diff_minus)
+
+lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
+ apply (auto simp add: elt_set_plus_def add_ac diff_minus)
+ apply (subgoal_tac "a = (a + - b) + b")
+ apply (rule bexI, assumption, assumption)
+ apply (auto simp add: add_ac)
+ done
+
+lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
+ by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
+ assumption)
+
+lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
+ by (auto simp add: set_times_def)
+
+lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
+ by (auto simp add: elt_set_times_def)
+
+lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
+ (b *o D) = (a * b) *o (C \<otimes> D)"
+ apply (auto simp add: elt_set_times_def set_times_def)
+ apply (rule_tac x = "ba * bb" in exI)
+ apply (auto simp add: mult_ac)
+ apply (rule_tac x = "aa * a" in exI)
+ apply (auto simp add: mult_ac)
+ done
+
+lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
+ (a * b) *o C"
+ by (auto simp add: elt_set_times_def mult_assoc)
+
+lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
+ a *o (B \<otimes> C)"
+ apply (auto simp add: elt_set_times_def set_times_def)
+ apply (blast intro: mult_ac)
+ apply (rule_tac x = "a * aa" in exI)
+ apply (rule conjI)
+ apply (rule_tac x = "aa" in bexI)
+ apply auto
+ apply (rule_tac x = "ba" in bexI)
+ apply (auto simp add: mult_ac)
+ done
+
+theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
+ a *o (C \<otimes> D)"
+ apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
+ mult_ac)
+ apply (rule_tac x = "aa * ba" in exI)
+ apply (auto simp add: mult_ac)
+ done
+
+theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
+ set_times_rearrange3 set_times_rearrange4
+
+lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
+ by (auto simp add: elt_set_times_def)
+
+lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
+ C \<otimes> E <= D \<otimes> F"
+ by (auto simp add: set_times_def)
+
+lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
+ by (auto simp add: elt_set_times_def set_times_def)
+
+lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
+ a *o D <= D \<otimes> C"
+ by (auto simp add: elt_set_times_def set_times_def mult_ac)
+
+lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
+ apply (subgoal_tac "a *o B <= a *o D")
+ apply (erule order_trans)
+ apply (erule set_times_mono3)
+ apply (erule set_times_mono)
+ done
+
+lemma set_times_mono_b: "C <= D ==> x : a *o C
+ ==> x : a *o D"
+ apply (frule set_times_mono)
+ apply auto
+ done
+
+lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
+ x : D \<otimes> F"
+ apply (frule set_times_mono2)
+ prefer 2
+ apply force
+ apply assumption
+ done
+
+lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
+ apply (frule set_times_mono3)
+ apply auto
+ done
+
+lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
+ x : a *o D ==> x : D \<otimes> C"
+ apply (frule set_times_mono4)
+ apply auto
+ done
+
+lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
+ by (auto simp add: elt_set_times_def)
+
+lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
+ (a * b) +o (a *o C)"
+ by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
+
+lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
+ (a *o B) \<oplus> (a *o C)"
+ apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
+ apply blast
+ apply (rule_tac x = "b + bb" in exI)
+ apply (auto simp add: ring_distribs)
+ done
+
+lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
+ a *o D \<oplus> C \<otimes> D"
+ apply (auto intro!: subsetI simp add:
+ elt_set_plus_def elt_set_times_def set_times_def
+ set_plus_def ring_distribs)
+ apply auto
+ done
+
+theorems set_times_plus_distribs =
+ set_times_plus_distrib
+ set_times_plus_distrib2
+
+lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
+ - a : C"
+ by (auto simp add: elt_set_times_def)
+
+lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
+ - a : (- 1) *o C"
+ by (auto simp add: elt_set_times_def)
+
+end
--- a/src/HOL/Library/SetsAndFunctions.thy Sun Aug 22 22:28:24 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,373 +0,0 @@
-(* Title: HOL/Library/SetsAndFunctions.thy
- Author: Jeremy Avigad and Kevin Donnelly
-*)
-
-header {* Operations on sets and functions *}
-
-theory SetsAndFunctions
-imports Main
-begin
-
-text {*
-This library lifts operations like addition and muliplication to sets and
-functions of appropriate types. It was designed to support asymptotic
-calculations. See the comments at the top of theory @{text BigO}.
-*}
-
-subsection {* Basic definitions *}
-
-definition
- set_plus :: "('a::plus) set => 'a set => 'a set" (infixl "\<oplus>" 65) where
- "A \<oplus> B == {c. EX a:A. EX b:B. c = a + b}"
-
-instantiation "fun" :: (type, plus) plus
-begin
-
-definition
- func_plus: "f + g == (%x. f x + g x)"
-
-instance ..
-
-end
-
-definition
- set_times :: "('a::times) set => 'a set => 'a set" (infixl "\<otimes>" 70) where
- "A \<otimes> B == {c. EX a:A. EX b:B. c = a * b}"
-
-instantiation "fun" :: (type, times) times
-begin
-
-definition
- func_times: "f * g == (%x. f x * g x)"
-
-instance ..
-
-end
-
-
-instantiation "fun" :: (type, zero) zero
-begin
-
-definition
- func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
-
-instance ..
-
-end
-
-instantiation "fun" :: (type, one) one
-begin
-
-definition
- func_one: "1::(('a::type) => ('b::one)) == %x. 1"
-
-instance ..
-
-end
-
-definition
- elt_set_plus :: "'a::plus => 'a set => 'a set" (infixl "+o" 70) where
- "a +o B = {c. EX b:B. c = a + b}"
-
-definition
- elt_set_times :: "'a::times => 'a set => 'a set" (infixl "*o" 80) where
- "a *o B = {c. EX b:B. c = a * b}"
-
-abbreviation (input)
- elt_set_eq :: "'a => 'a set => bool" (infix "=o" 50) where
- "x =o A == x : A"
-
-instance "fun" :: (type,semigroup_add)semigroup_add
- by default (auto simp add: func_plus add_assoc)
-
-instance "fun" :: (type,comm_monoid_add)comm_monoid_add
- by default (auto simp add: func_zero func_plus add_ac)
-
-instance "fun" :: (type,ab_group_add)ab_group_add
- apply default
- apply (simp add: fun_Compl_def func_plus func_zero)
- apply (simp add: fun_Compl_def func_plus fun_diff_def diff_minus)
- done
-
-instance "fun" :: (type,semigroup_mult)semigroup_mult
- apply default
- apply (auto simp add: func_times mult_assoc)
- done
-
-instance "fun" :: (type,comm_monoid_mult)comm_monoid_mult
- apply default
- apply (auto simp add: func_one func_times mult_ac)
- done
-
-instance "fun" :: (type,comm_ring_1)comm_ring_1
- apply default
- apply (auto simp add: func_plus func_times fun_Compl_def fun_diff_def
- func_one func_zero algebra_simps)
- apply (drule fun_cong)
- apply simp
- done
-
-interpretation set_semigroup_add: semigroup_add "op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"
- apply default
- apply (unfold set_plus_def)
- apply (force simp add: add_assoc)
- done
-
-interpretation set_semigroup_mult: semigroup_mult "op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"
- apply default
- apply (unfold set_times_def)
- apply (force simp add: mult_assoc)
- done
-
-interpretation set_comm_monoid_add: comm_monoid_add "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set" "{0}"
- apply default
- apply (unfold set_plus_def)
- apply (force simp add: add_ac)
- apply force
- done
-
-interpretation set_comm_monoid_mult: comm_monoid_mult "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set" "{1}"
- apply default
- apply (unfold set_times_def)
- apply (force simp add: mult_ac)
- apply force
- done
-
-
-subsection {* Basic properties *}
-
-lemma set_plus_intro [intro]: "a : C ==> b : D ==> a + b : C \<oplus> D"
- by (auto simp add: set_plus_def)
-
-lemma set_plus_intro2 [intro]: "b : C ==> a + b : a +o C"
- by (auto simp add: elt_set_plus_def)
-
-lemma set_plus_rearrange: "((a::'a::comm_monoid_add) +o C) \<oplus>
- (b +o D) = (a + b) +o (C \<oplus> D)"
- apply (auto simp add: elt_set_plus_def set_plus_def add_ac)
- apply (rule_tac x = "ba + bb" in exI)
- apply (auto simp add: add_ac)
- apply (rule_tac x = "aa + a" in exI)
- apply (auto simp add: add_ac)
- done
-
-lemma set_plus_rearrange2: "(a::'a::semigroup_add) +o (b +o C) =
- (a + b) +o C"
- by (auto simp add: elt_set_plus_def add_assoc)
-
-lemma set_plus_rearrange3: "((a::'a::semigroup_add) +o B) \<oplus> C =
- a +o (B \<oplus> C)"
- apply (auto simp add: elt_set_plus_def set_plus_def)
- apply (blast intro: add_ac)
- apply (rule_tac x = "a + aa" in exI)
- apply (rule conjI)
- apply (rule_tac x = "aa" in bexI)
- apply auto
- apply (rule_tac x = "ba" in bexI)
- apply (auto simp add: add_ac)
- done
-
-theorem set_plus_rearrange4: "C \<oplus> ((a::'a::comm_monoid_add) +o D) =
- a +o (C \<oplus> D)"
- apply (auto intro!: subsetI simp add: elt_set_plus_def set_plus_def add_ac)
- apply (rule_tac x = "aa + ba" in exI)
- apply (auto simp add: add_ac)
- done
-
-theorems set_plus_rearranges = set_plus_rearrange set_plus_rearrange2
- set_plus_rearrange3 set_plus_rearrange4
-
-lemma set_plus_mono [intro!]: "C <= D ==> a +o C <= a +o D"
- by (auto simp add: elt_set_plus_def)
-
-lemma set_plus_mono2 [intro]: "(C::('a::plus) set) <= D ==> E <= F ==>
- C \<oplus> E <= D \<oplus> F"
- by (auto simp add: set_plus_def)
-
-lemma set_plus_mono3 [intro]: "a : C ==> a +o D <= C \<oplus> D"
- by (auto simp add: elt_set_plus_def set_plus_def)
-
-lemma set_plus_mono4 [intro]: "(a::'a::comm_monoid_add) : C ==>
- a +o D <= D \<oplus> C"
- by (auto simp add: elt_set_plus_def set_plus_def add_ac)
-
-lemma set_plus_mono5: "a:C ==> B <= D ==> a +o B <= C \<oplus> D"
- apply (subgoal_tac "a +o B <= a +o D")
- apply (erule order_trans)
- apply (erule set_plus_mono3)
- apply (erule set_plus_mono)
- done
-
-lemma set_plus_mono_b: "C <= D ==> x : a +o C
- ==> x : a +o D"
- apply (frule set_plus_mono)
- apply auto
- done
-
-lemma set_plus_mono2_b: "C <= D ==> E <= F ==> x : C \<oplus> E ==>
- x : D \<oplus> F"
- apply (frule set_plus_mono2)
- prefer 2
- apply force
- apply assumption
- done
-
-lemma set_plus_mono3_b: "a : C ==> x : a +o D ==> x : C \<oplus> D"
- apply (frule set_plus_mono3)
- apply auto
- done
-
-lemma set_plus_mono4_b: "(a::'a::comm_monoid_add) : C ==>
- x : a +o D ==> x : D \<oplus> C"
- apply (frule set_plus_mono4)
- apply auto
- done
-
-lemma set_zero_plus [simp]: "(0::'a::comm_monoid_add) +o C = C"
- by (auto simp add: elt_set_plus_def)
-
-lemma set_zero_plus2: "(0::'a::comm_monoid_add) : A ==> B <= A \<oplus> B"
- apply (auto intro!: subsetI simp add: set_plus_def)
- apply (rule_tac x = 0 in bexI)
- apply (rule_tac x = x in bexI)
- apply (auto simp add: add_ac)
- done
-
-lemma set_plus_imp_minus: "(a::'a::ab_group_add) : b +o C ==> (a - b) : C"
- by (auto simp add: elt_set_plus_def add_ac diff_minus)
-
-lemma set_minus_imp_plus: "(a::'a::ab_group_add) - b : C ==> a : b +o C"
- apply (auto simp add: elt_set_plus_def add_ac diff_minus)
- apply (subgoal_tac "a = (a + - b) + b")
- apply (rule bexI, assumption, assumption)
- apply (auto simp add: add_ac)
- done
-
-lemma set_minus_plus: "((a::'a::ab_group_add) - b : C) = (a : b +o C)"
- by (rule iffI, rule set_minus_imp_plus, assumption, rule set_plus_imp_minus,
- assumption)
-
-lemma set_times_intro [intro]: "a : C ==> b : D ==> a * b : C \<otimes> D"
- by (auto simp add: set_times_def)
-
-lemma set_times_intro2 [intro!]: "b : C ==> a * b : a *o C"
- by (auto simp add: elt_set_times_def)
-
-lemma set_times_rearrange: "((a::'a::comm_monoid_mult) *o C) \<otimes>
- (b *o D) = (a * b) *o (C \<otimes> D)"
- apply (auto simp add: elt_set_times_def set_times_def)
- apply (rule_tac x = "ba * bb" in exI)
- apply (auto simp add: mult_ac)
- apply (rule_tac x = "aa * a" in exI)
- apply (auto simp add: mult_ac)
- done
-
-lemma set_times_rearrange2: "(a::'a::semigroup_mult) *o (b *o C) =
- (a * b) *o C"
- by (auto simp add: elt_set_times_def mult_assoc)
-
-lemma set_times_rearrange3: "((a::'a::semigroup_mult) *o B) \<otimes> C =
- a *o (B \<otimes> C)"
- apply (auto simp add: elt_set_times_def set_times_def)
- apply (blast intro: mult_ac)
- apply (rule_tac x = "a * aa" in exI)
- apply (rule conjI)
- apply (rule_tac x = "aa" in bexI)
- apply auto
- apply (rule_tac x = "ba" in bexI)
- apply (auto simp add: mult_ac)
- done
-
-theorem set_times_rearrange4: "C \<otimes> ((a::'a::comm_monoid_mult) *o D) =
- a *o (C \<otimes> D)"
- apply (auto intro!: subsetI simp add: elt_set_times_def set_times_def
- mult_ac)
- apply (rule_tac x = "aa * ba" in exI)
- apply (auto simp add: mult_ac)
- done
-
-theorems set_times_rearranges = set_times_rearrange set_times_rearrange2
- set_times_rearrange3 set_times_rearrange4
-
-lemma set_times_mono [intro]: "C <= D ==> a *o C <= a *o D"
- by (auto simp add: elt_set_times_def)
-
-lemma set_times_mono2 [intro]: "(C::('a::times) set) <= D ==> E <= F ==>
- C \<otimes> E <= D \<otimes> F"
- by (auto simp add: set_times_def)
-
-lemma set_times_mono3 [intro]: "a : C ==> a *o D <= C \<otimes> D"
- by (auto simp add: elt_set_times_def set_times_def)
-
-lemma set_times_mono4 [intro]: "(a::'a::comm_monoid_mult) : C ==>
- a *o D <= D \<otimes> C"
- by (auto simp add: elt_set_times_def set_times_def mult_ac)
-
-lemma set_times_mono5: "a:C ==> B <= D ==> a *o B <= C \<otimes> D"
- apply (subgoal_tac "a *o B <= a *o D")
- apply (erule order_trans)
- apply (erule set_times_mono3)
- apply (erule set_times_mono)
- done
-
-lemma set_times_mono_b: "C <= D ==> x : a *o C
- ==> x : a *o D"
- apply (frule set_times_mono)
- apply auto
- done
-
-lemma set_times_mono2_b: "C <= D ==> E <= F ==> x : C \<otimes> E ==>
- x : D \<otimes> F"
- apply (frule set_times_mono2)
- prefer 2
- apply force
- apply assumption
- done
-
-lemma set_times_mono3_b: "a : C ==> x : a *o D ==> x : C \<otimes> D"
- apply (frule set_times_mono3)
- apply auto
- done
-
-lemma set_times_mono4_b: "(a::'a::comm_monoid_mult) : C ==>
- x : a *o D ==> x : D \<otimes> C"
- apply (frule set_times_mono4)
- apply auto
- done
-
-lemma set_one_times [simp]: "(1::'a::comm_monoid_mult) *o C = C"
- by (auto simp add: elt_set_times_def)
-
-lemma set_times_plus_distrib: "(a::'a::semiring) *o (b +o C)=
- (a * b) +o (a *o C)"
- by (auto simp add: elt_set_plus_def elt_set_times_def ring_distribs)
-
-lemma set_times_plus_distrib2: "(a::'a::semiring) *o (B \<oplus> C) =
- (a *o B) \<oplus> (a *o C)"
- apply (auto simp add: set_plus_def elt_set_times_def ring_distribs)
- apply blast
- apply (rule_tac x = "b + bb" in exI)
- apply (auto simp add: ring_distribs)
- done
-
-lemma set_times_plus_distrib3: "((a::'a::semiring) +o C) \<otimes> D <=
- a *o D \<oplus> C \<otimes> D"
- apply (auto intro!: subsetI simp add:
- elt_set_plus_def elt_set_times_def set_times_def
- set_plus_def ring_distribs)
- apply auto
- done
-
-theorems set_times_plus_distribs =
- set_times_plus_distrib
- set_times_plus_distrib2
-
-lemma set_neg_intro: "(a::'a::ring_1) : (- 1) *o C ==>
- - a : C"
- by (auto simp add: elt_set_times_def)
-
-lemma set_neg_intro2: "(a::'a::ring_1) : C ==>
- - a : (- 1) *o C"
- by (auto simp add: elt_set_times_def)
-
-end
--- a/src/HOL/Metis_Examples/BigO.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy Mon Aug 23 11:18:38 2010 +0200
@@ -7,7 +7,7 @@
header {* Big O notation *}
theory BigO
-imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main SetsAndFunctions
+imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main Function_Algebras Set_Algebras
begin
subsection {* Definitions *}
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Aug 23 11:18:38 2010 +0200
@@ -389,7 +389,7 @@
|> Option.map (fst o read_int o explode)
|> the_default 5
val params = Sledgehammer_Isar.default_params thy
- [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")]
+ [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")]
val minimize =
Sledgehammer_Fact_Minimize.minimize_theorems params 1 (subgoal_count st)
val _ = log separator
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Aug 23 11:18:38 2010 +0200
@@ -346,15 +346,15 @@
lemma one_index[simp]:
"(1 :: 'a::one ^'n)$i = 1" by vector
-instance cart :: (semiring_char_0,finite) semiring_char_0
-proof (intro_classes)
- fix m n ::nat
- show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"
- by (simp add: Cart_eq of_nat_index)
+instance cart :: (semiring_char_0, finite) semiring_char_0
+proof
+ fix m n :: nat
+ show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)"
+ by (auto intro!: injI simp add: Cart_eq of_nat_index)
qed
-instance cart :: (comm_ring_1,finite) comm_ring_1 by intro_classes
-instance cart :: (ring_char_0,finite) ring_char_0 by intro_classes
+instance cart :: (comm_ring_1,finite) comm_ring_1 ..
+instance cart :: (ring_char_0,finite) ring_char_0 ..
instance cart :: (real_vector,finite) real_vector ..
--- a/src/HOL/NSA/StarDef.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Aug 23 11:18:38 2010 +0200
@@ -1000,8 +1000,11 @@
lemma star_of_of_int [simp]: "star_of (of_int z) = of_int z"
by transfer (rule refl)
-instance star :: (semiring_char_0) semiring_char_0
-by intro_classes (simp only: star_of_nat_def star_of_eq of_nat_eq_iff)
+instance star :: (semiring_char_0) semiring_char_0 proof
+ have "inj (star_of :: 'a \<Rightarrow> 'a star)" by (rule injI) simp
+ then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)" using inj_of_nat by (rule inj_comp)
+ then show "inj (of_nat :: nat \<Rightarrow> 'a star)" by (simp add: comp_def)
+qed
instance star :: (ring_char_0) ring_char_0 ..
--- a/src/HOL/Nat.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Nat.thy Mon Aug 23 11:18:38 2010 +0200
@@ -1227,21 +1227,27 @@
finally show ?thesis .
qed
+lemma comp_funpow:
+ fixes f :: "'a \<Rightarrow> 'a"
+ shows "comp f ^^ n = comp (f ^^ n)"
+ by (induct n) simp_all
-subsection {* Embedding of the Naturals into any
- @{text semiring_1}: @{term of_nat} *}
+
+subsection {* Embedding of the Naturals into any @{text semiring_1}: @{term of_nat} *}
context semiring_1
begin
-primrec
- of_nat :: "nat \<Rightarrow> 'a"
-where
- of_nat_0: "of_nat 0 = 0"
- | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
+definition of_nat :: "nat \<Rightarrow> 'a" where
+ "of_nat n = (plus 1 ^^ n) 0"
+
+lemma of_nat_simps [simp]:
+ shows of_nat_0: "of_nat 0 = 0"
+ and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
+ by (simp_all add: of_nat_def)
lemma of_nat_1 [simp]: "of_nat 1 = 1"
- unfolding One_nat_def by simp
+ by (simp add: of_nat_def)
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
by (induct m) (simp_all add: add_ac)
@@ -1274,19 +1280,19 @@
Includes non-ordered rings like the complex numbers.*}
class semiring_char_0 = semiring_1 +
- assumes of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
+ assumes inj_of_nat: "inj of_nat"
begin
+lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \<longleftrightarrow> m = n"
+ by (auto intro: inj_of_nat injD)
+
text{*Special cases where either operand is zero*}
lemma of_nat_0_eq_iff [simp, no_atp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
- by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
+ by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])
lemma of_nat_eq_0_iff [simp, no_atp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
- by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
-
-lemma inj_of_nat: "inj of_nat"
- by (simp add: inj_on_def)
+ by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
end
@@ -1315,8 +1321,8 @@
text{*Every @{text linordered_semidom} has characteristic zero.*}
-subclass semiring_char_0
- proof qed (simp add: eq_iff order_eq_iff)
+subclass semiring_char_0 proof
+qed (auto intro!: injI simp add: eq_iff)
text{*Special cases where either operand is zero*}
--- a/src/HOL/RealVector.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/RealVector.thy Mon Aug 23 11:18:38 2010 +0200
@@ -270,6 +270,10 @@
lemma of_real_eq_iff [simp]: "(of_real x = of_real y) = (x = y)"
by (simp add: of_real_def)
+lemma inj_of_real:
+ "inj of_real"
+ by (auto intro: injI)
+
lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
@@ -291,13 +295,11 @@
by (simp add: number_of_eq)
text{*Every real algebra has characteristic zero*}
+
instance real_algebra_1 < ring_char_0
proof
- fix m n :: nat
- have "(of_real (of_nat m) = (of_real (of_nat n)::'a)) = (m = n)"
- by (simp only: of_real_eq_iff of_nat_eq_iff)
- thus "(of_nat m = (of_nat n::'a)) = (m = n)"
- by (simp only: of_real_of_nat_eq)
+ from inj_of_real inj_of_nat have "inj (of_real \<circ> of_nat)" by (rule inj_comp)
+ then show "inj (of_nat :: nat \<Rightarrow> 'a)" by (simp add: comp_def)
qed
instance real_field < field_char_0 ..
--- a/src/HOL/Sledgehammer.thy Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Aug 23 11:18:38 2010 +0200
@@ -31,28 +31,31 @@
[no_atp]: "skolem_id = (\<lambda>x. x)"
definition COMBI :: "'a \<Rightarrow> 'a" where
-[no_atp]: "COMBI P \<equiv> P"
+[no_atp]: "COMBI P = P"
definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
-[no_atp]: "COMBK P Q \<equiv> P"
+[no_atp]: "COMBK P Q = P"
definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
-"COMBB P Q R \<equiv> P (Q R)"
+"COMBB P Q R = P (Q R)"
definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBC P Q R \<equiv> P R Q"
+[no_atp]: "COMBC P Q R = P R Q"
definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
-[no_atp]: "COMBS P Q R \<equiv> P R (Q R)"
+[no_atp]: "COMBS P Q R = P R (Q R)"
definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
-"fequal X Y \<equiv> (X = Y)"
+"fequal X Y \<longleftrightarrow> (X = Y)"
+
+lemma fequal_imp_equal [no_atp]: "\<not> fequal X Y \<or> X = Y"
+by (simp add: fequal_def)
-lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y"
- by (simp add: fequal_def)
+lemma equal_imp_fequal [no_atp]: "\<not> X = Y \<or> fequal X Y"
+by (simp add: fequal_def)
-lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
- by (simp add: fequal_def)
+lemma equal_imp_equal [no_atp]: "X = Y ==> X = Y"
+by auto
text{*Theorems for translation to combinators*}
--- a/src/HOL/Tools/ATP/async_manager.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/ATP/async_manager.ML Mon Aug 23 11:18:38 2010 +0200
@@ -72,8 +72,8 @@
val message' =
desc ^ "\n" ^ message ^
(if verbose then
- "Total time: " ^ Int.toString (Time.toMilliseconds
- (Time.- (now, birth_time))) ^ " ms.\n"
+ "\nTotal time: " ^ Int.toString (Time.toMilliseconds
+ (Time.- (now, birth_time))) ^ " ms."
else
"")
val messages' = (tool, message') :: messages;
--- a/src/HOL/Tools/ATP/atp_problem.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Aug 23 11:18:38 2010 +0200
@@ -15,14 +15,14 @@
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
- datatype kind = Axiom | Conjecture
+ datatype kind = Axiom | Hypothesis | Conjecture
datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list
val timestamp : unit -> string
val is_tptp_variable : string -> bool
val strings_for_tptp_problem :
- (string * string problem_line list) list -> string list
+ bool -> (string * string problem_line list) list -> string list
val nice_tptp_problem :
bool -> ('a * (string * string) problem_line list) list
-> ('a * string problem_line list) list
@@ -42,12 +42,16 @@
AConn of connective * ('a, 'b) formula list |
AAtom of 'b
-datatype kind = Axiom | Conjecture
+datatype kind = Axiom | Hypothesis | Conjecture
datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
+fun string_for_kind Axiom = "axiom"
+ | string_for_kind Hypothesis = "hypothesis"
+ | string_for_kind Conjecture = "conjecture"
+
fun string_for_term (ATerm (s, [])) = s
| string_for_term (ATerm ("equal", ts)) =
space_implode " = " (map string_for_term ts)
@@ -74,17 +78,26 @@
(map string_for_formula phis) ^ ")"
| string_for_formula (AAtom tm) = string_for_term tm
-fun string_for_problem_line (Fof (ident, kind, phi)) =
- "fof(" ^ ident ^ ", " ^
- (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^
- " (" ^ string_for_formula phi ^ ")).\n"
-fun strings_for_tptp_problem problem =
+fun string_for_problem_line use_conjecture_for_hypotheses
+ (Fof (ident, kind, phi)) =
+ let
+ val (kind, phi) =
+ if kind = Hypothesis andalso use_conjecture_for_hypotheses then
+ (Conjecture, AConn (ANot, [phi]))
+ else
+ (kind, phi)
+ in
+ "fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
+ string_for_formula phi ^ ")).\n"
+ end
+fun strings_for_tptp_problem use_conjecture_for_hypotheses problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
maps (fn (_, []) => []
| (heading, lines) =>
"\n% " ^ heading ^ " (" ^ Int.toString (length lines) ^ ")\n" ::
- map string_for_problem_line lines) problem
+ map (string_for_problem_line use_conjecture_for_hypotheses) lines)
+ problem
fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 23 11:18:38 2010 +0200
@@ -18,9 +18,10 @@
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- max_new_relevant_facts_per_iter: int,
- prefers_theory_relevant: bool,
- explicit_forall: bool}
+ default_max_relevant_per_iter: int,
+ default_theory_relevant: bool,
+ explicit_forall: bool,
+ use_conjecture_for_hypotheses: bool}
val string_for_failure : failure -> string
val known_failure_in_output :
@@ -49,9 +50,10 @@
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- max_new_relevant_facts_per_iter: int,
- prefers_theory_relevant: bool,
- explicit_forall: bool}
+ default_max_relevant_per_iter: int,
+ default_theory_relevant: bool,
+ explicit_forall: bool,
+ use_conjecture_for_hypotheses: bool}
val missing_message_tail =
" appears to be missing. You will need to install it if you want to run \
@@ -144,9 +146,10 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- max_new_relevant_facts_per_iter = 50 (* FIXME *),
- prefers_theory_relevant = false,
- explicit_forall = false}
+ default_max_relevant_per_iter = 50 (* FIXME *),
+ default_theory_relevant = false,
+ explicit_forall = false,
+ use_conjecture_for_hypotheses = true}
val e = ("e", e_config)
@@ -171,9 +174,10 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
- max_new_relevant_facts_per_iter = 35 (* FIXME *),
- prefers_theory_relevant = true,
- explicit_forall = true}
+ default_max_relevant_per_iter = 35 (* FIXME *),
+ default_theory_relevant = true,
+ explicit_forall = true,
+ use_conjecture_for_hypotheses = true}
val spass = ("spass", spass_config)
@@ -185,7 +189,7 @@
required_execs = [],
arguments = fn _ => fn timeout =>
"--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
- " --input_file",
+ " --thanks Andrei --input_file",
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -196,11 +200,11 @@
(IncompleteUnprovable, "CANNOT PROVE"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
- (OutOfResources, "Refutation not found"),
(VampireTooOld, "not a valid option")],
- max_new_relevant_facts_per_iter = 45 (* FIXME *),
- prefers_theory_relevant = false,
- explicit_forall = false}
+ default_max_relevant_per_iter = 45 (* FIXME *),
+ default_theory_relevant = false,
+ explicit_forall = false,
+ use_conjecture_for_hypotheses = true}
val vampire = ("vampire", vampire_config)
@@ -220,52 +224,79 @@
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
-fun get_system prefix = Synchronized.change_result systems (fn systems =>
- (if null systems then get_systems () else systems)
- |> `(find_first (String.isPrefix prefix)));
+fun get_system prefix =
+ Synchronized.change_result systems
+ (fn systems => (if null systems then get_systems () else systems)
+ |> `(find_first (String.isPrefix prefix)))
fun the_system prefix =
(case get_system prefix of
NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
| SOME sys => sys);
-fun remote_config atp_prefix
- ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
- prefers_theory_relevant, ...} : prover_config) : prover_config =
+fun remote_config system_prefix proof_delims known_failures
+ default_max_relevant_per_iter default_theory_relevant
+ use_conjecture_for_hypotheses =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn timeout =>
" -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
- the_system atp_prefix,
+ the_system system_prefix,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
known_failures =
known_failures @ known_perl_failures @
[(TimedOut, "says Timeout")],
- max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
- prefers_theory_relevant = prefers_theory_relevant,
- explicit_forall = true}
+ default_max_relevant_per_iter = default_max_relevant_per_iter,
+ default_theory_relevant = default_theory_relevant,
+ explicit_forall = true,
+ use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
+
+fun remotify_config system_prefix
+ ({proof_delims, known_failures, default_max_relevant_per_iter,
+ default_theory_relevant, use_conjecture_for_hypotheses, ...}
+ : prover_config) : prover_config =
+ remote_config system_prefix proof_delims known_failures
+ default_max_relevant_per_iter default_theory_relevant
+ use_conjecture_for_hypotheses
-val remote_name = prefix "remote_"
-fun remote_prover (name, config) atp_prefix =
- (remote_name name, remote_config atp_prefix config)
+val remotify_name = prefix "remote_"
+fun remote_prover name system_prefix proof_delims known_failures
+ default_max_relevant_per_iter default_theory_relevant
+ use_conjecture_for_hypotheses =
+ (remotify_name name,
+ remote_config system_prefix proof_delims known_failures
+ default_max_relevant_per_iter default_theory_relevant
+ use_conjecture_for_hypotheses)
+fun remotify_prover (name, config) system_prefix =
+ (remotify_name name, remotify_config system_prefix config)
-val remote_e = remote_prover e "EP---"
-val remote_vampire = remote_prover vampire "Vampire---9"
-
+val remote_e = remotify_prover e "EP---"
+val remote_vampire = remotify_prover vampire "Vampire---9"
+val remote_sine_e =
+ remote_prover "sine_e" "SInE---" []
+ [(Unprovable, "says Unknown")] 150 (* FIXME *) false true
+val remote_snark =
+ remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] []
+ 50 (* FIXME *) false true
(* Setup *)
fun is_installed ({exec, required_execs, ...} : prover_config) =
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
fun maybe_remote (name, config) =
- name |> not (is_installed config) ? remote_name
+ name |> not (is_installed config) ? remotify_name
fun default_atps_param_value () =
space_implode " " ([maybe_remote e] @
(if is_installed (snd spass) then [fst spass] else []) @
- [remote_name (fst vampire)])
+ [if forall (is_installed o snd) [e, spass] then
+ remotify_name (fst vampire)
+ else
+ maybe_remote vampire,
+ fst remote_sine_e])
-val provers = [e, spass, vampire, remote_e, remote_vampire]
+val provers = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
+ remote_snark]
val setup = fold add_prover provers
end;
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Aug 23 11:18:38 2010 +0200
@@ -92,7 +92,7 @@
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
let
val rty = fastype_of rconst
- val qty = derive_qtyp qtys rty ctxt
+ val qty = derive_qtyp ctxt qtys rty
val lhs = Free (qconst_name, qty)
in
quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Aug 23 11:18:38 2010 +0200
@@ -18,7 +18,7 @@
val lift_procedure_tac: Proof.context -> thm -> int -> tactic
val lift_tac: Proof.context -> thm list -> int -> tactic
- val lifted: typ list -> Proof.context -> thm -> thm
+ val lifted: Proof.context -> typ list -> thm list -> thm -> thm
val lifted_attrib: attribute
end;
@@ -627,7 +627,7 @@
THEN' SUBGOAL (fn (goal, i) =>
let
val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
- val rtrm = derive_rtrm qtys goal ctxt
+ val rtrm = derive_rtrm ctxt qtys goal
val rule = procedure_inst ctxt rtrm goal
in
rtac rule i
@@ -647,7 +647,7 @@
end
-(** lifting as tactic **)
+(** lifting as a tactic **)
(* the tactic leaves three subgoals to be proved *)
fun lift_procedure_tac ctxt rthm =
@@ -661,39 +661,48 @@
(rtac rule THEN' rtac rthm') i
end)
+
+fun lift_single_tac ctxt rthm =
+ lift_procedure_tac ctxt rthm
+ THEN' RANGE
+ [ regularize_tac ctxt,
+ all_injection_tac ctxt,
+ clean_tac ctxt ]
+
fun lift_tac ctxt rthms =
+ Goal.conjunction_tac
+ THEN' RANGE (map (lift_single_tac ctxt) rthms)
+
+
+(* automated lifting with pre-simplification of the theorems;
+ for internal usage *)
+fun lifted ctxt qtys simps rthm =
let
- fun mk_tac rthm =
- lift_procedure_tac ctxt rthm
- THEN' RANGE
- [ regularize_tac ctxt,
- all_injection_tac ctxt,
- clean_tac ctxt ]
+ val ss = (mk_minimal_ss ctxt) addsimps simps
+
+ (* When the theorem is atomized, eta redexes are contracted,
+ so we do it both in the original theorem *)
+ val rthm' =
+ rthm
+ |> asm_full_simplify ss
+ |> Drule.eta_contraction_rule
+ val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
+ val goal = derive_qtrm ctxt qtys (prop_of rthm'')
in
- Goal.conjunction_tac THEN' RANGE (map mk_tac rthms)
+ Goal.prove ctxt' [] [] goal
+ (K ((asm_full_simp_tac ss THEN' lift_single_tac ctxt' rthm') 1))
+ |> singleton (ProofContext.export ctxt' ctxt)
end
-(** lifting as attribute **)
-
-fun lifted qtys ctxt thm =
-let
- (* When the theorem is atomized, eta redexes are contracted,
- so we do it both in the original theorem *)
- val thm' = Drule.eta_contraction_rule thm
- val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
- val goal = derive_qtrm qtys (prop_of thm'') ctxt'
-in
- Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
- |> singleton (ProofContext.export ctxt' ctxt)
-end;
+(* lifting as an attribute *)
val lifted_attrib = Thm.rule_attribute (fn context =>
let
val ctxt = Context.proof_of context
val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
in
- lifted qtys ctxt
+ lifted ctxt qtys []
end)
end; (* structure *)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Aug 23 11:18:38 2010 +0200
@@ -26,10 +26,10 @@
val inj_repabs_trm: Proof.context -> term * term -> term
val inj_repabs_trm_chk: Proof.context -> term * term -> term
- val derive_qtyp: typ list -> typ -> Proof.context -> typ
- val derive_qtrm: typ list -> term -> Proof.context -> term
- val derive_rtyp: typ list -> typ -> Proof.context -> typ
- val derive_rtrm: typ list -> term -> Proof.context -> term
+ val derive_qtyp: Proof.context -> typ list -> typ -> typ
+ val derive_qtrm: Proof.context -> typ list -> term -> term
+ val derive_rtyp: Proof.context -> typ list -> typ -> typ
+ val derive_rtrm: Proof.context -> typ list -> term -> term
end;
structure Quotient_Term: QUOTIENT_TERM =
@@ -498,7 +498,7 @@
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
- | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
Const (@{const_name All}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -509,7 +509,7 @@
else mk_ball $ (mk_resp $ resrel) $ subtrm
end
- | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
Const (@{const_name Ex}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -520,7 +520,7 @@
else mk_bex $ (mk_resp $ resrel) $ subtrm
end
- | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
+ | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -638,18 +638,18 @@
as the type of subterms needs to be calculated *)
fun inj_repabs_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
- (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
- Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
+ (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
+ Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
- | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
- Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
+ | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
+ Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
- | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
+ | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) =>
let
val rty = fastype_of rtrm
val qty = fastype_of qtrm
in
- mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
+ mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
end
| (Abs (x, T, t), Abs (x', T', t')) =>
@@ -767,19 +767,19 @@
(* derives a qtyp and qtrm out of a rtyp and rtrm,
respectively
*)
-fun derive_qtyp qtys rty ctxt =
+fun derive_qtyp ctxt qtys rty =
subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
-fun derive_qtrm qtys rtrm ctxt =
+fun derive_qtrm ctxt qtys rtrm =
subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
(* derives a rtyp and rtrm out of a qtyp and qtrm,
respectively
*)
-fun derive_rtyp qtys qty ctxt =
+fun derive_rtyp ctxt qtys qty =
subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
-fun derive_rtrm qtys qtrm ctxt =
+fun derive_rtrm ctxt qtys qtrm =
subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 23 11:18:38 2010 +0200
@@ -7,6 +7,8 @@
signature CLAUSIFIER =
sig
+ val transform_elim_theorem : thm -> thm
+ val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
val cnf_axiom: theory -> thm -> thm list
@@ -83,7 +85,7 @@
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_term" in "ATP_Systems".) *)
+ (Cf. "extensionalize_term" in "Sledgehammer_Translate".) *)
fun extensionalize_theorem th =
case prop_of th of
_ $ (Const (@{const_name "op ="}, Type (_, [Type (@{type_name fun}, _), _]))
@@ -223,12 +225,13 @@
(* Converts an Isabelle theorem (intro, elim or simp format, even higher-order)
into NNF. *)
fun to_nnf th ctxt0 =
- let val th1 = th |> transform_elim_theorem |> zero_var_indexes
- val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
- val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
- |> extensionalize_theorem
- |> Meson.make_nnf ctxt
- in (th3, ctxt) end;
+ let
+ val th1 = th |> transform_elim_theorem |> zero_var_indexes
+ val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
+ val th3 = th2 |> Conv.fconv_rule Object_Logic.atomize
+ |> extensionalize_theorem
+ |> Meson.make_nnf ctxt
+ in (th3, ctxt) end
(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
fun cnf_axiom thy th =
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 23 11:18:38 2010 +0200
@@ -66,8 +66,10 @@
(* HOL to FOL (Isabelle to Metis) *)
(* ------------------------------------------------------------------------- *)
-fun fn_isa_to_met "equal" = "="
- | fn_isa_to_met x = x;
+fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
+ | fn_isa_to_met_sublevel x = x
+fun fn_isa_to_met_toplevel "equal" = "="
+ | fn_isa_to_met_toplevel x = x
fun metis_lit b c args = (b, (c, args));
@@ -89,7 +91,7 @@
| _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm")
fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
- Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
+ Metis.Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
| hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
| hol_term_to_fol_HO (CombApp (tm1, tm2)) =
Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
@@ -99,7 +101,7 @@
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
| hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
- wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
+ wrap_type (Metis.Term.Fn(fn_isa_to_met_sublevel a, []), ty)
| hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
combtyp_of tm)
@@ -108,7 +110,7 @@
let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
val lits = map hol_term_to_fol_FO tms
- in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end
+ in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
| hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
(case strip_combterm_comb tm of
(CombConst(("equal", _), _, _), tms) =>
@@ -224,13 +226,16 @@
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
+fun smart_invert_const "fequal" = @{const_name "op ="}
+ | smart_invert_const s = invert_const s
+
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
(case strip_prefix_and_undo_ascii tvar_prefix v of
SOME w => make_tvar w
| NONE => make_tvar v)
| hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
(case strip_prefix_and_undo_ascii type_const_prefix x of
- SOME tc => Term.Type (invert_const tc,
+ SOME tc => Term.Type (smart_invert_const tc,
map (hol_type_from_metis_term ctxt) tys)
| NONE =>
case strip_prefix_and_undo_ascii tfree_prefix x of
@@ -265,7 +270,7 @@
| applic_to_tt (a,ts) =
case strip_prefix_and_undo_ascii const_prefix a of
SOME b =>
- let val c = invert_const b
+ let val c = smart_invert_const b
val ntypes = num_type_args thy c
val nterms = length ts - ntypes
val tts = map tm_to_tt ts
@@ -283,7 +288,7 @@
| NONE => (*Not a constant. Is it a type constructor?*)
case strip_prefix_and_undo_ascii type_const_prefix a of
SOME b =>
- Type (Term.Type (invert_const b, types_of (map tm_to_tt ts)))
+ Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
| NONE => (*Maybe a TFree. Should then check that ts=[].*)
case strip_prefix_and_undo_ascii tfree_prefix a of
SOME b => Type (mk_tfree ctxt b)
@@ -311,7 +316,7 @@
Const (@{const_name "op ="}, HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
(case strip_prefix_and_undo_ascii const_prefix x of
- SOME c => Const (invert_const c, dummyT)
+ SOME c => Const (smart_invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix_and_undo_ascii fixed_var_prefix x of
SOME v => Free (v, hol_type_from_metis_term ctxt ty)
@@ -325,7 +330,7 @@
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
(case strip_prefix_and_undo_ascii const_prefix x of
- SOME c => Const (invert_const c, dummyT)
+ SOME c => Const (smart_invert_const c, dummyT)
| NONE => (*Not a constant. Is it a fixed variable??*)
case strip_prefix_and_undo_ascii fixed_var_prefix x of
SOME v => Free (v, dummyT)
@@ -598,9 +603,6 @@
(* Translation of HO Clauses *)
(* ------------------------------------------------------------------------- *)
-fun cnf_helper_theorem thy raw th =
- if raw then th else the_single (Clausifier.cnf_axiom thy th)
-
fun type_ext thy tms =
let val subs = tfree_classes_of_terms tms
val supers = tvar_classes_of_terms tms
@@ -650,15 +652,16 @@
| string_of_mode FT = "FT"
val helpers =
- [("c_COMBI", (false, @{thms COMBI_def})),
- ("c_COMBK", (false, @{thms COMBK_def})),
- ("c_COMBB", (false, @{thms COMBB_def})),
- ("c_COMBC", (false, @{thms COMBC_def})),
- ("c_COMBS", (false, @{thms COMBS_def})),
- ("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})),
- ("c_True", (true, @{thms True_or_False})),
- ("c_False", (true, @{thms True_or_False})),
- ("c_If", (true, @{thms if_True if_False True_or_False}))]
+ [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
+ ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
+ ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
+ ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
+ ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
+ ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
+ @{thms fequal_imp_equal equal_imp_fequal})),
+ ("c_True", (true, map (`I) @{thms True_or_False})),
+ ("c_False", (true, map (`I) @{thms True_or_False})),
+ ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
fun is_quasi_fol_clause thy =
Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
@@ -673,18 +676,20 @@
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture ith {axioms, tfrees, skolems} : logic_map =
+ fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
+ : logic_map =
let
val (mth, tfree_lits, skolems) =
- hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems ith
+ hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems
+ metis_ith
in
- {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
+ {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
end;
val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
- |> fold (add_thm true) cls
+ |> fold (add_thm true o `I) cls
|> add_tfrees
- |> fold (add_thm false) ths
+ |> fold (add_thm false o `I) ths
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
fun is_used c =
exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -695,11 +700,12 @@
let
val helper_ths =
helpers |> filter (is_used o fst)
- |> maps (fn (_, (raw, thms)) =>
- if mode = FT orelse not raw then
- map (cnf_helper_theorem @{theory} raw) thms
+ |> maps (fn (c, (needs_full_types, thms)) =>
+ if not (is_used c) orelse
+ needs_full_types andalso mode <> FT then
+ []
else
- [])
+ thms)
in lmap |> fold (add_thm false) helper_ths end
in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
@@ -772,9 +778,19 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+(* Extensionalize "th", because that makes sense and that's what Sledgehammer
+ does, but also keep an unextensionalized version of "th" for backward
+ compatibility. *)
+fun also_extensionalize_theorem th =
+ let val th' = Clausifier.extensionalize_theorem th in
+ if Thm.eq_thm (th, th') then [th]
+ else th :: Meson.make_clauses_unsorted [th']
+ end
+
val neg_clausify =
single
#> Meson.make_clauses_unsorted
+ #> maps also_extensionalize_theorem
#> map Clausifier.introduce_combinators_in_theorem
#> Meson.finish_cnf
@@ -802,9 +818,24 @@
val metisF_tac = generic_metis_tac FO
val metisFT_tac = generic_metis_tac FT
+(* Whenever "X" has schematic type variables, we treat "using X by metis" as
+ "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
+ We don't do it for nonschematic facts "X" because this breaks a few proofs
+ (in the rare and subtle case where a proof relied on extensionality not being
+ applied) and brings no benefits. *)
+val has_tvar =
+ exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
fun method name mode =
Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
- SIMPLE_METHOD' (CHANGED_PROP o generic_metis_tac mode ctxt ths)))
+ METHOD (fn facts =>
+ let
+ val (schem_facts, nonschem_facts) =
+ List.partition has_tvar facts
+ in
+ HEADGOAL (Method.insert_tac nonschem_facts THEN'
+ CHANGED_PROP
+ o generic_metis_tac mode ctxt (schem_facts @ ths))
+ end)))
val setup =
type_lits_setup
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 23 11:18:38 2010 +0200
@@ -20,12 +20,12 @@
explicit_apply: bool,
relevance_threshold: real,
relevance_convergence: real,
+ max_relevant_per_iter: int option,
theory_relevant: bool option,
defs_relevant: bool,
isar_proof: bool,
isar_shrink_factor: int,
- timeout: Time.time,
- minimize_timeout: Time.time}
+ timeout: Time.time}
type problem =
{subgoal: int,
goal: Proof.context * (thm list * thm),
@@ -89,12 +89,12 @@
explicit_apply: bool,
relevance_threshold: real,
relevance_convergence: real,
+ max_relevant_per_iter: int option,
theory_relevant: bool option,
defs_relevant: bool,
isar_proof: bool,
isar_shrink_factor: int,
- timeout: Time.time,
- minimize_timeout: Time.time}
+ timeout: Time.time}
type problem =
{subgoal: int,
@@ -208,10 +208,11 @@
fun prover_fun atp_name
{exec, required_execs, arguments, proof_delims, known_failures,
- max_new_relevant_facts_per_iter, prefers_theory_relevant,
- explicit_forall}
+ default_max_relevant_per_iter, default_theory_relevant,
+ explicit_forall, use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
- relevance_threshold, relevance_convergence, theory_relevant,
+ relevance_threshold, relevance_convergence,
+ max_relevant_per_iter, theory_relevant,
defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
minimize_command
({subgoal, goal, relevance_override, axioms} : problem) =
@@ -231,8 +232,10 @@
(print_d (fn () => "Selecting relevant facts for " ^ quote atp_name ^
".");
relevant_facts full_types relevance_threshold relevance_convergence
- defs_relevant max_new_relevant_facts_per_iter
- (the_default prefers_theory_relevant theory_relevant)
+ defs_relevant
+ (the_default default_max_relevant_per_iter
+ max_relevant_per_iter)
+ (the_default default_theory_relevant theory_relevant)
relevance_override goal hyp_ts concl_t
|> tap ((fn n => print_v (fn () =>
"Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
@@ -306,7 +309,9 @@
val (problem, pool, conjecture_offset, axiom_names) =
prepare_problem ctxt readable_names explicit_forall full_types
explicit_apply hyp_ts concl_t the_axioms
- val _ = File.write_list probfile (strings_for_tptp_problem problem)
+ val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
+ problem
+ val _ = File.write_list probfile ss
val conjecture_shape =
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
|> map single
@@ -331,21 +336,19 @@
()
else
File.write (Path.explode (Path.implode probfile ^ "_proof")) output
-
val ((pool, conjecture_shape, axiom_names),
(output, msecs, proof, outcome)) =
with_path cleanup export run_on (prob_pathname subgoal)
val (conjecture_shape, axiom_names) =
repair_conjecture_shape_and_theorem_names output conjecture_shape
axiom_names
-
val (message, used_thm_names) =
case outcome of
NONE =>
proof_text isar_proof
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
(full_types, minimize_command, proof, axiom_names, th, subgoal)
- | SOME failure => (string_for_failure failure ^ "\n", [])
+ | SOME failure => (string_for_failure failure, [])
in
{outcome = outcome, message = message, pool = pool,
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 23 11:18:38 2010 +0200
@@ -43,21 +43,13 @@
val name = Facts.string_of_ref xref
|> forall (member Thm.eq_thm chained_ths) ths
? prefix chained_prefix
- in (name, ths) end
+ in (name, ths |> map Clausifier.transform_elim_theorem) end
(***************************************************************)
(* Relevance Filtering *)
(***************************************************************)
-fun strip_Trueprop_and_all (@{const Trueprop} $ t) =
- strip_Trueprop_and_all t
- | strip_Trueprop_and_all (Const (@{const_name all}, _) $ Abs (_, _, t)) =
- strip_Trueprop_and_all t
- | strip_Trueprop_and_all (Const (@{const_name All}, _) $ Abs (_, _, t)) =
- strip_Trueprop_and_all t
- | strip_Trueprop_and_all t = t
-
(*** constants with types ***)
(*An abstraction of Isabelle types*)
@@ -82,9 +74,9 @@
(*Pairs a constant with the list of its type instantiations (using const_typ)*)
fun const_with_typ thy (c,typ) =
- let val tvars = Sign.const_typargs thy (c,typ)
- in (c, map const_typ_of tvars) end
- handle TYPE _ => (c,[]); (*Variable (locale constant): monomorphic*)
+ let val tvars = Sign.const_typargs thy (c,typ) in
+ (c, map const_typ_of tvars) end
+ handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*)
(*Add a const/type pair to the table, but a [] entry means a standard connective,
which we ignore.*)
@@ -95,52 +87,64 @@
val fresh_prefix = "Sledgehammer.Fresh."
val flip = Option.map not
(* These are typically simplified away by "Meson.presimplify". *)
-val boring_consts = [@{const_name If}, @{const_name Let}]
+val boring_consts =
+ [@{const_name If}, @{const_name Let} (* TODO: , @{const_name Set.member}, @{const_name Collect} *)]
fun get_consts_typs thy pos ts =
let
- (* Free variables are included, as well as constants, to handle locales.
- "skolem_id" is included to increase the complexity of theorems containing
- Skolem functions. In non-CNF form, "Ex" is included but each occurrence
- is considered fresh, to simulate the effect of Skolemization. *)
+ (* We include free variables, as well as constants, to handle locales. For
+ each quantifiers that must necessarily be skolemized by the ATP, we
+ introduce a fresh constant to simulate the effect of Skolemization. *)
fun do_term t =
case t of
Const x => add_const_type_to_table (const_with_typ thy x)
- | Free x => add_const_type_to_table (const_with_typ thy x)
- | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
+ | Free (s, _) => add_const_type_to_table (s, [])
| t1 $ t2 => do_term t1 #> do_term t2
| Abs (_, _, t) =>
(* Abstractions lead to combinators, so we add a penalty for them. *)
add_const_type_to_table (gensym fresh_prefix, [])
#> do_term t
| _ => I
- fun do_quantifier sweet_pos pos body_t =
+ fun do_quantifier will_surely_be_skolemized body_t =
do_formula pos body_t
- #> (if pos = SOME sweet_pos then I
- else add_const_type_to_table (gensym fresh_prefix, []))
- and do_equality T t1 t2 =
- fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
- else do_term) [t1, t2]
+ #> (if will_surely_be_skolemized then
+ add_const_type_to_table (gensym fresh_prefix, [])
+ else
+ I)
+ and do_term_or_formula T =
+ if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
+ else do_term
and do_formula pos t =
case t of
Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
- do_quantifier false pos body_t
+ do_quantifier (pos = SOME false) body_t
| @{const "==>"} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
| Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
- do_equality T t1 t2
+ fold (do_term_or_formula T) [t1, t2]
| @{const Trueprop} $ t1 => do_formula pos t1
| @{const Not} $ t1 => do_formula (flip pos) t1
| Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
- do_quantifier false pos body_t
+ do_quantifier (pos = SOME false) body_t
| Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
- do_quantifier true pos body_t
+ do_quantifier (pos = SOME true) body_t
| @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
| @{const "op -->"} $ t1 $ t2 =>
do_formula (flip pos) t1 #> do_formula pos t2
| Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
- do_equality T t1 t2
+ fold (do_term_or_formula T) [t1, t2]
+ | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
+ $ t1 $ t2 $ t3 =>
+ do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3]
+ | Const (@{const_name Ex1}, _) $ Abs (_, _, body_t) =>
+ do_quantifier (is_some pos) body_t
+ | Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, body_t) =>
+ do_quantifier (pos = SOME false)
+ (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, body_t))
+ | Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, body_t) =>
+ do_quantifier (pos = SOME true)
+ (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, body_t))
| (t0 as Const (_, @{typ bool})) $ t1 =>
do_term t0 #> do_formula pos t1 (* theory constant *)
| _ => do_term t
@@ -186,7 +190,7 @@
fun count_axiom_consts theory_relevant thy (_, th) =
let
fun do_const (a, T) =
- let val (c, cts) = const_with_typ thy (a,T) in
+ let val (c, cts) = const_with_typ thy (a, T) in
(* Two-dimensional table update. Constant maps to types maps to
count. *)
CTtab.map_default (cts, 0) (Integer.add 1)
@@ -194,7 +198,6 @@
end
fun do_term (Const x) = do_const x
| do_term (Free x) = do_const x
- | do_term (Const (x as (@{const_name skolem_id}, _)) $ _) = do_const x
| do_term (t $ u) = do_term t #> do_term u
| do_term (Abs (_, _, t)) = do_term t
| do_term _ = I
@@ -233,7 +236,7 @@
fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
fun consts_typs_of_term thy t =
- Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) []
+ Symtab.fold add_expand_pairs (get_consts_typs thy (SOME true) [t]) []
fun pair_consts_typs_axiom theory_relevant thy axiom =
(axiom, axiom |> snd |> theory_const_prop_of theory_relevant
@@ -270,82 +273,36 @@
(* Limit the number of new facts, to prevent runaway acceptance. *)
fun take_best max_new (newpairs : (annotated_thm * real) list) =
- let val nnew = length newpairs
- in
- if nnew <= max_new then (map #1 newpairs, [])
+ let val nnew = length newpairs in
+ if nnew <= max_new then
+ (map #1 newpairs, [])
else
- let val cls = sort compare_pairs newpairs
- val accepted = List.take (cls, max_new)
+ let
+ val newpairs = sort compare_pairs newpairs
+ val accepted = List.take (newpairs, max_new)
in
trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
- ", exceeds the limit of " ^ Int.toString (max_new)));
+ ", exceeds the limit of " ^ Int.toString max_new));
trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
trace_msg (fn () => "Actually passed: " ^
space_implode ", " (map (fst o fst o fst) accepted));
-
- (map #1 accepted, map #1 (List.drop (cls, max_new)))
+ (map #1 accepted, map #1 (List.drop (newpairs, max_new)))
end
end;
-fun relevant_facts ctxt relevance_convergence defs_relevant max_new
- ({add, del, ...} : relevance_override) const_tab =
- let
- val thy = ProofContext.theory_of ctxt
- val add_thms = maps (ProofContext.get_fact ctxt) add
- val del_thms = maps (ProofContext.get_fact ctxt) del
- fun iter threshold rel_const_tab =
- let
- fun relevant ([], _) [] = [] (* Nothing added this iteration *)
- | relevant (newpairs, rejects) [] =
- let
- val (newrels, more_rejects) = take_best max_new newpairs
- val new_consts = maps #2 newrels
- val rel_const_tab =
- rel_const_tab |> fold add_const_type_to_table new_consts
- val threshold =
- threshold + (1.0 - threshold) / relevance_convergence
- in
- trace_msg (fn () => "relevant this iteration: " ^
- Int.toString (length newrels));
- map #1 newrels @ iter threshold rel_const_tab
- (more_rejects @ rejects)
- end
- | relevant (newrels, rejects)
- ((ax as (clsthm as (name, th), consts_typs)) :: axs) =
- let
- val weight =
- if member Thm.eq_thm add_thms th then 1.0
- else if member Thm.eq_thm del_thms th then 0.0
- else formula_weight const_tab rel_const_tab consts_typs
- in
- if weight >= threshold orelse
- (defs_relevant andalso defines thy th rel_const_tab) then
- (trace_msg (fn () =>
- name ^ " passes: " ^ Real.toString weight
- (* ^ " consts: " ^ commas (map fst consts_typs) *));
- relevant ((ax, weight) :: newrels, rejects) axs)
- else
- relevant (newrels, ax :: rejects) axs
- end
- in
- trace_msg (fn () => "relevant_facts, current threshold: " ^
- Real.toString threshold);
- relevant ([], [])
- end
- in iter end
-
fun relevance_filter ctxt relevance_threshold relevance_convergence
- defs_relevant max_new theory_relevant relevance_override
- thy axioms goal_ts =
+ defs_relevant max_new theory_relevant
+ ({add, del, ...} : relevance_override) axioms goal_ts =
if relevance_threshold > 1.0 then
[]
else if relevance_threshold < 0.0 then
axioms
else
let
+ val thy = ProofContext.theory_of ctxt
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
- val goal_const_tab = get_consts_typs thy (SOME true) goal_ts
+ val goal_const_tab = get_consts_typs thy (SOME false) goal_ts
val relevance_threshold = 0.8 * relevance_threshold (* FIXME *)
val _ =
trace_msg (fn () => "Initial constants: " ^
@@ -353,12 +310,56 @@
|> Symtab.dest
|> filter (curry (op <>) [] o snd)
|> map fst))
- val relevant =
- relevant_facts ctxt relevance_convergence defs_relevant max_new
- relevance_override const_tab relevance_threshold
- goal_const_tab
- (map (pair_consts_typs_axiom theory_relevant thy)
- axioms)
+ val add_thms = maps (ProofContext.get_fact ctxt) add
+ val del_thms = maps (ProofContext.get_fact ctxt) del
+ fun iter threshold rel_const_tab =
+ let
+ fun relevant ([], rejects) [] =
+ (* Nothing was added this iteration: Add "add:" facts. *)
+ if null add_thms then
+ []
+ else
+ map_filter (fn (p as (name, th), _) =>
+ if member Thm.eq_thm add_thms th then SOME p
+ else NONE) rejects
+ | relevant (newpairs, rejects) [] =
+ let
+ val (newrels, more_rejects) = take_best max_new newpairs
+ val new_consts = maps #2 newrels
+ val rel_const_tab =
+ rel_const_tab |> fold add_const_type_to_table new_consts
+ val threshold =
+ threshold + (1.0 - threshold) / relevance_convergence
+ in
+ trace_msg (fn () => "relevant this iteration: " ^
+ Int.toString (length newrels));
+ map #1 newrels @ iter threshold rel_const_tab
+ (more_rejects @ rejects)
+ end
+ | relevant (newrels, rejects)
+ ((ax as ((name, th), consts_typs)) :: axs) =
+ let
+ val weight =
+ if member Thm.eq_thm del_thms th then 0.0
+ else formula_weight const_tab rel_const_tab consts_typs
+ in
+ if weight >= threshold orelse
+ (defs_relevant andalso defines thy th rel_const_tab) then
+ (trace_msg (fn () =>
+ name ^ " passes: " ^ Real.toString weight
+ (* ^ " consts: " ^ commas (map fst consts_typs) *));
+ relevant ((ax, weight) :: newrels, rejects) axs)
+ else
+ relevant (newrels, ax :: rejects) axs
+ end
+ in
+ trace_msg (fn () => "relevant_facts, current threshold: " ^
+ Real.toString threshold);
+ relevant ([], [])
+ end
+ val relevant = iter relevance_threshold goal_const_tab
+ (map (pair_consts_typs_axiom theory_relevant thy)
+ axioms)
in
trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
relevant
@@ -432,13 +433,73 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-fun is_theorem_bad_for_atps thm =
+(**** Predicates to detect unwanted facts (prolific or likely to cause
+ unsoundness) ****)
+
+(* Too general means, positive equality literal with a variable X as one
+ operand, when X does not occur properly in the other operand. This rules out
+ clearly inconsistent facts such as X = a | X = b, though it by no means
+ guarantees soundness. *)
+
+(* Unwanted equalities are those between a (bound or schematic) variable that
+ does not properly occur in the second operand. *)
+val is_exhaustive_finite =
+ let
+ fun is_bad_equal (Var z) t =
+ not (exists_subterm (fn Var z' => z = z' | _ => false) t)
+ | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
+ | is_bad_equal _ _ = false
+ fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
+ fun do_formula pos t =
+ case (pos, t) of
+ (_, @{const Trueprop} $ t1) => do_formula pos t1
+ | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
+ do_formula pos t'
+ | (_, @{const "==>"} $ t1 $ t2) =>
+ do_formula (not pos) t1 andalso
+ (t2 = @{prop False} orelse do_formula pos t2)
+ | (_, @{const "op -->"} $ t1 $ t2) =>
+ do_formula (not pos) t1 andalso
+ (t2 = @{const False} orelse do_formula pos t2)
+ | (_, @{const Not} $ t1) => do_formula (not pos) t1
+ | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
+ | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
+ | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
+ | _ => false
+ in do_formula true end
+
+fun has_bound_or_var_of_type tycons =
+ exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s
+ | Abs (_, Type (s, _), _) => member (op =) tycons s
+ | _ => false)
+
+(* Facts are forbidden to contain variables of these types. The typical reason
+ is that they lead to unsoundness. Note that "unit" satisfies numerous
+ equations like "?x = ()". The resulting clauses will have no type constraint,
+ yielding false proofs. Even "bool" leads to many unsound proofs, though only
+ for higher-order problems. *)
+val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}];
+
+(* Facts containing variables of type "unit" or "bool" or of the form
+ "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
+ are omitted. *)
+fun is_dangerous_term full_types t =
+ not full_types andalso
+ (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t)
+
+fun is_theorem_bad_for_atps full_types thm =
let val t = prop_of thm in
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
- exists_sledgehammer_const t orelse is_strange_thm thm
+ is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
+ is_strange_thm thm
end
-fun all_name_thms_pairs ctxt chained_ths =
+fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
val local_facts = ProofContext.facts_of ctxt;
@@ -447,21 +508,24 @@
fun valid_facts facts =
(facts, []) |-> Facts.fold_static (fn (name, ths0) =>
- if Facts.is_concealed facts name orelse
- (respect_no_atp andalso is_package_def name) orelse
- member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
- String.isSuffix "_def_raw" (* FIXME: crude hack *) name then
+ if (Facts.is_concealed facts name orelse
+ (respect_no_atp andalso is_package_def name) orelse
+ member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
+ String.isSuffix "_def_raw" (* FIXME: crude hack *) name) andalso
+ forall (not o member Thm.eq_thm add_thms) ths0 then
I
else
let
fun check_thms a =
(case try (ProofContext.get_thms ctxt) a of
NONE => false
- | SOME ths1 => Thm.eq_thms (ths0, ths1));
-
+ | SOME ths1 => Thm.eq_thms (ths0, ths1))
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
- val ths = filter_out is_theorem_bad_for_atps ths0
+ val ths =
+ ths0 |> map Clausifier.transform_elim_theorem
+ |> filter ((not o is_theorem_bad_for_atps full_types) orf
+ member Thm.eq_thm add_thms)
in
case find_first check_thms [name1, name2, name] of
NONE => I
@@ -503,69 +567,21 @@
(* ATP invocation methods setup *)
(***************************************************************)
-(**** Predicates to detect unwanted facts (prolific or likely to cause
- unsoundness) ****)
-
-(* Too general means, positive equality literal with a variable X as one
- operand, when X does not occur properly in the other operand. This rules out
- clearly inconsistent facts such as X = a | X = b, though it by no means
- guarantees soundness. *)
-
-(* Unwanted equalities are those between a (bound or schematic) variable that
- does not properly occur in the second operand. *)
-fun too_general_eqterms (Var z) t =
- not (exists_subterm (fn Var z' => z = z' | _ => false) t)
- | too_general_eqterms (Bound j) t = not (loose_bvar1 (t, j))
- | too_general_eqterms _ _ = false
-
-fun too_general_equality (Const (@{const_name "op ="}, _) $ t1 $ t2) =
- too_general_eqterms t1 t2 orelse too_general_eqterms t2 t1
- | too_general_equality _ = false
-
-fun has_typed_var tycons = exists_subterm
- (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
-
-(* Facts are forbidden to contain variables of these types. The typical reason
- is that they lead to unsoundness. Note that "unit" satisfies numerous
- equations like "?x = ()". The resulting clauses will have no type constraint,
- yielding false proofs. Even "bool" leads to many unsound proofs, though only
- for higher-order problems. *)
-val dangerous_types = [@{type_name unit}, @{type_name bool}];
-
-(* Facts containing variables of type "unit" or "bool" or of the form
- "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
- are omitted. *)
-fun is_dangerous_term _ @{prop True} = true
- | is_dangerous_term full_types t =
- not full_types andalso
- (has_typed_var dangerous_types t orelse
- forall too_general_equality (HOLogic.disjuncts (strip_Trueprop_and_all t)))
-
fun relevant_facts full_types relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant
(relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) hyp_ts concl_t =
let
- val thy = ProofContext.theory_of ctxt
val add_thms = maps (ProofContext.get_fact ctxt) add
- val has_override = not (null add) orelse not (null del)
-(* FIXME:
- val is_FO = forall Meson.is_fol_term thy (concl_t :: hyp_ts)
-*)
val axioms =
checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
- (map (name_thms_pair_from_ref ctxt chained_ths) add @
- (if only then [] else all_name_thms_pairs ctxt chained_ths))
- |> not has_override ? make_unique
- |> filter (fn (_, th) =>
- member Thm.eq_thm add_thms th orelse
- ((* FIXME: keep? (not is_FO orelse is_quasi_fol_theorem thy th) andalso*)
- not (is_dangerous_term full_types (prop_of th))))
+ (if only then map (name_thms_pair_from_ref ctxt chained_ths) add
+ else all_name_thms_pairs ctxt full_types add_thms chained_ths)
+ |> make_unique
in
relevance_filter ctxt relevance_threshold relevance_convergence
defs_relevant max_new theory_relevant relevance_override
- thy axioms (concl_t :: hyp_ts)
- |> has_override ? make_unique
+ axioms (concl_t :: hyp_ts)
|> sort_wrt fst
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Mon Aug 23 11:18:38 2010 +0200
@@ -18,6 +18,7 @@
structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
struct
+open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
@@ -42,9 +43,9 @@
end
fun test_theorems ({debug, verbose, overlord, atps, full_types,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor,
- ...} : params)
+ relevance_threshold, relevance_convergence,
+ defs_relevant, isar_proof, isar_shrink_factor, ...}
+ : params)
(prover : prover) explicit_apply timeout subgoal state
name_thms_pairs =
let
@@ -55,9 +56,9 @@
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
- theory_relevant = theory_relevant, defs_relevant = defs_relevant,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout, minimize_timeout = timeout}
+ max_relevant_per_iter = NONE, theory_relevant = NONE,
+ defs_relevant = defs_relevant, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, timeout = timeout}
val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
@@ -93,32 +94,29 @@
(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
preprocessing time is included in the estimate below but isn't part of the
timeout. *)
-val fudge_msecs = 250
+val fudge_msecs = 1000
fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
| minimize_theorems
- (params as {debug, verbose, overlord, atps as atp :: _, full_types,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor,
- minimize_timeout, ...})
+ (params as {debug, atps = atp :: _, full_types, isar_proof,
+ isar_shrink_factor, timeout, ...})
i n state name_thms_pairs =
let
val thy = Proof.theory_of state
val prover = get_prover_fun thy atp
- val msecs = Time.toMilliseconds minimize_timeout
- val _ =
- priority ("Sledgehammer minimize: ATP " ^ quote atp ^
- " with a time limit of " ^ string_of_int msecs ^ " ms.")
+ val msecs = Time.toMilliseconds timeout
+ val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".")
val {context = ctxt, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val explicit_apply =
not (forall (Meson.is_fol_term thy)
- (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs))
+ (concl_t :: hyp_ts @
+ maps (map prop_of o snd) name_thms_pairs))
fun do_test timeout =
test_theorems params prover explicit_apply timeout i state
val timer = Timer.startRealTimer ()
in
- (case do_test minimize_timeout name_thms_pairs of
+ (case do_test timeout name_thms_pairs of
result as {outcome = NONE, pool, used_thm_names,
conjecture_shape, ...} =>
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 23 11:18:38 2010 +0200
@@ -69,11 +69,11 @@
("explicit_apply", "false"),
("relevance_threshold", "50"),
("relevance_convergence", "320"),
+ ("max_relevant_per_iter", "smart"),
("theory_relevant", "smart"),
("defs_relevant", "false"),
("isar_proof", "false"),
- ("isar_shrink_factor", "1"),
- ("minimize_timeout", "5 s")]
+ ("isar_shrink_factor", "1")]
val alias_params =
[("atp", "atps")]
@@ -89,7 +89,7 @@
val params_for_minimize =
["debug", "verbose", "overlord", "full_types", "isar_proof",
- "isar_shrink_factor", "minimize_timeout"]
+ "isar_shrink_factor", "timeout"]
val property_dependent_params = ["atps", "full_types", "timeout"]
@@ -158,6 +158,10 @@
SOME n => n
| NONE => error ("Parameter " ^ quote name ^
" must be assigned an integer value.")
+ fun lookup_int_option name =
+ case lookup name of
+ SOME "smart" => NONE
+ | _ => SOME (lookup_int name)
val debug = lookup_bool "debug"
val verbose = debug orelse lookup_bool "verbose"
val overlord = lookup_bool "overlord"
@@ -168,20 +172,21 @@
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val relevance_convergence =
0.01 * Real.fromInt (lookup_int "relevance_convergence")
+ val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
val theory_relevant = lookup_bool_option "theory_relevant"
val defs_relevant = lookup_bool "defs_relevant"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val timeout = lookup_time "timeout"
- val minimize_timeout = lookup_time "minimize_timeout"
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
+ max_relevant_per_iter = max_relevant_per_iter,
theory_relevant = theory_relevant, defs_relevant = defs_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout, minimize_timeout = minimize_timeout}
+ timeout = timeout}
end
fun get_params thy = extract_params (default_raw_params thy)
@@ -200,9 +205,6 @@
val kill_atpsN = "kill_atps"
val refresh_tptpN = "refresh_tptp"
-fun minimizize_raw_param_name "timeout" = "minimize_timeout"
- | minimizize_raw_param_name name = name
-
val is_raw_param_relevant_for_minimize =
member (op =) params_for_minimize o fst o unalias_raw_param
fun string_for_raw_param (key, values) =
@@ -226,9 +228,8 @@
(minimize_command override_params i) state
end
else if subcommand = minimizeN then
- run_minimize (get_params thy (map (apfst minimizize_raw_param_name)
- override_params))
- (the_default 1 opt_i) (#add relevance_override) state
+ run_minimize (get_params thy override_params) (the_default 1 opt_i)
+ (#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
else if subcommand = available_atpsN then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Aug 23 11:18:38 2010 +0200
@@ -10,7 +10,6 @@
sig
type minimize_command = string list -> string
- val metis_line: bool -> int -> int -> string list -> string
val metis_proof_text:
bool * minimize_command * string * string vector * thm * int
-> string * string list
@@ -547,6 +546,17 @@
(** EXTRACTING LEMMAS **)
+(* Like "split_line", but ignores "\n" that follow a comma (as in SNARK's
+ output). *)
+val split_proof_lines =
+ let
+ fun aux [] [] = []
+ | aux line [] = [implode (rev line)]
+ | aux line ("," :: "\n" :: rest) = aux ("," :: line) rest
+ | aux line ("\n" :: rest) = aux line [] @ aux [] rest
+ | aux line (s :: rest) = aux (s :: line) rest
+ in aux [] o explode end
+
(* A list consisting of the first number in each line is returned. For TSTP,
interesting lines have the form "fof(108, axiom, ...)", where the number
(108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
@@ -564,16 +574,19 @@
val tokens_of =
String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
val thm_name_list = Vector.foldr (op ::) [] axiom_names
- fun do_line ("fof" :: num :: "axiom" :: (rest as _ :: _)) =
- (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
- SOME name =>
- if member (op =) rest "file" then SOME name else axiom_name num
- | NONE => axiom_name num)
+ fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) =
+ if tag = "cnf" orelse tag = "fof" then
+ (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
+ SOME name =>
+ if member (op =) rest "file" then SOME name else axiom_name num
+ | NONE => axiom_name num)
+ else
+ NONE
| do_line (num :: "0" :: "Inp" :: _) = axiom_name num
| do_line (num :: rest) =
(case List.last rest of "input" => axiom_name num | _ => NONE)
| do_line _ = NONE
- in atp_proof |> split_lines |> map_filter (do_line o tokens_of) end
+ in atp_proof |> split_proof_lines |> map_filter (do_line o tokens_of) end
val indent_size = 2
val no_label = ("", ~1)
@@ -598,14 +611,14 @@
metis_using ls ^ metis_apply i n ^ metis_call full_types ss
fun metis_line full_types i n ss =
"Try this command: " ^
- Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ ".\n"
+ Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
fun minimize_line _ [] = ""
| minimize_line minimize_command facts =
case minimize_command facts of
"" => ""
| command =>
- "To minimize the number of lemmas, try this: " ^
- Markup.markup Markup.sendback command ^ ".\n"
+ "\nTo minimize the number of lemmas, try this: " ^
+ Markup.markup Markup.sendback command ^ "."
val unprefix_chained = perhaps (try (unprefix chained_prefix))
@@ -984,7 +997,7 @@
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
do_indent 0 ^ "proof -\n" ^
do_steps "" "" 1 proof ^
- do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
+ do_indent 0 ^ (if n <> 1 then "next" else "qed")
in do_proof end
fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
@@ -1006,14 +1019,14 @@
|> kill_useless_labels_in_proof
|> relabel_proof
|> string_for_proof ctxt full_types i n of
- "" => "No structured proof available.\n"
- | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
+ "" => "\nNo structured proof available."
+ | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
if debug then
isar_proof_for ()
else
try isar_proof_for ()
- |> the_default "Warning: The Isar proof construction failed.\n"
+ |> the_default "\nWarning: The Isar proof construction failed."
in (one_line_proof ^ isar_proof, lemma_names) end
fun proof_text isar_proof isar_params other_params =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 23 11:18:38 2010 +0200
@@ -79,21 +79,7 @@
|>> AAtom ||> union (op =) ts)
in do_formula [] end
-(* Converts an elim-rule into an equivalent theorem that does not have the
- predicate variable. Leaves other theorems unchanged. We simply instantiate
- the conclusion variable to False. (Cf. "transform_elim_term" in
- "ATP_Systems".) *)
-fun transform_elim_term t =
- case Logic.strip_imp_concl t of
- @{const Trueprop} $ Var (z, @{typ bool}) =>
- subst_Vars [(z, @{const False})] t
- | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
- | _ => t
-
-fun presimplify_term thy =
- Skip_Proof.make_thm thy
- #> Meson.presimplify
- #> prop_of
+val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
fun conceal_bounds Ts t =
@@ -103,6 +89,25 @@
subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
(0 upto length Ts - 1 ~~ Ts))
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+ (Cf. "extensionalize_theorem" in "Clausifier".) *)
+fun extensionalize_term t =
+ let
+ fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
+ | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
+ Type (_, [_, res_T])]))
+ $ t2 $ Abs (var_s, var_T, t')) =
+ if s = @{const_name "op ="} orelse s = @{const_name "=="} then
+ let val var_t = Var ((var_s, j), var_T) in
+ Const (s, T' --> T' --> res_T)
+ $ betapply (t2, var_t) $ subst_bound (var_t, t')
+ |> aux (j + 1)
+ end
+ else
+ t
+ | aux _ t = t
+ in aux (maxidx_of_term t + 1) t end
+
fun introduce_combinators_in_term ctxt kind t =
let val thy = ProofContext.theory_of ctxt in
if Meson.is_fol_term thy t then
@@ -135,9 +140,8 @@
in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
handle THM _ =>
(* A type variable of sort "{}" will make abstraction fail. *)
- case kind of
- Axiom => HOLogic.true_const
- | Conjecture => HOLogic.false_const
+ if kind = Conjecture then HOLogic.false_const
+ else HOLogic.true_const
end
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
@@ -151,18 +155,33 @@
| aux t = t
in t |> exists_subterm is_Var t ? aux end
+(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
+ it leaves metaequalities over "prop"s alone. *)
+val atomize_term =
+ let
+ fun aux (@{const Trueprop} $ t1) = t1
+ | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
+ HOLogic.all_const T $ Abs (s, T, aux t')
+ | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
+ | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
+ HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
+ | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
+ HOLogic.eq_const T $ t1 $ t2
+ | aux _ = raise Fail "aux"
+ in perhaps (try aux) end
+
(* making axiom and conjecture formulas *)
-fun make_formula ctxt presimp (name, kind, t) =
+fun make_formula ctxt presimp name kind t =
let
val thy = ProofContext.theory_of ctxt
- val t = t |> transform_elim_term
- |> Object_Logic.atomize_term thy
+ val t = t |> Envir.beta_eta_contract
+ |> atomize_term
val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
|> extensionalize_term
|> presimp ? presimplify_term thy
|> perhaps (try (HOLogic.dest_Trueprop))
|> introduce_combinators_in_term ctxt kind
- |> kind = Conjecture ? freeze_term
+ |> kind <> Axiom ? freeze_term
val (combformula, ctypes_sorts) = combformula_for_prop thy t []
in
FOLFormula {name = name, combformula = combformula, kind = kind,
@@ -170,10 +189,16 @@
end
fun make_axiom ctxt presimp (name, th) =
- (name, make_formula ctxt presimp (name, Axiom, prop_of th))
-fun make_conjectures ctxt ts =
- map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
- (0 upto length ts - 1) ts
+ case make_formula ctxt presimp name Axiom (prop_of th) of
+ FOLFormula {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} =>
+ NONE
+ | formula => SOME (name, formula)
+fun make_conjecture ctxt ts =
+ let val last = length ts - 1 in
+ map2 (fn j => make_formula ctxt true (Int.toString j)
+ (if j = last then Conjecture else Hypothesis))
+ (0 upto last) ts
+ end
(** Helper facts **)
@@ -194,7 +219,7 @@
val optional_typed_helpers =
[(["c_True", "c_False"], @{thms True_or_False}),
(["c_If"], @{thms if_True if_False True_or_False})]
-val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal}
+val mandatory_helpers = @{thms fequal_def}
val init_counters =
Symtab.make (maps (maps (map (rpair 0) o fst))
@@ -211,11 +236,9 @@
if exists is_needed ss then map (`Thm.get_name_hint) ths
else [])) @
(if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
- |> map (snd o make_axiom ctxt false)
+ |> map_filter (Option.map snd o make_axiom ctxt false)
end
-fun meta_not t = @{const "==>"} $ t $ @{prop False}
-
fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
let
val thy = ProofContext.theory_of ctxt
@@ -236,9 +259,9 @@
val supers = tvar_classes_of_terms axiom_ts
val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
(* TFrees in the conjecture; TVars in the axioms *)
- val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
+ val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
val (axiom_names, axioms) =
- ListPair.unzip (map (make_axiom ctxt true) axioms)
+ ListPair.unzip (map_filter (make_axiom ctxt true) axioms)
val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
@@ -336,7 +359,7 @@
map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
fun problem_line_for_free_type lit =
- Fof (tfrees_name, Conjecture, mk_anot (formula_for_fo_literal lit))
+ Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit)
fun problem_lines_for_free_types conjectures =
let
val litss = map free_type_literals_for_conjecture conjectures
@@ -420,8 +443,8 @@
type instantiations). If false, the constant always receives all of its
arguments and is used as a predicate. *)
fun is_predicate NONE s =
- s = "equal" orelse String.isPrefix type_const_prefix s orelse
- String.isPrefix class_prefix s
+ s = "equal" orelse s = "$false" orelse s = "$true" orelse
+ String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
| is_predicate (SOME the_const_tab) s =
case Symtab.lookup the_const_tab s of
SOME {min_arity, max_arity, sub_level} =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Aug 23 11:18:38 2010 +0200
@@ -15,7 +15,6 @@
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
- val extensionalize_term : term -> term
val monomorphic_term : Type.tyenv -> term -> term
val specialize_type : theory -> (string * typ) -> term -> term
val subgoal_count : Proof.state -> int
@@ -101,25 +100,6 @@
Keyword.is_keyword s) ? quote
end
-(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Clausifier".) *)
-fun extensionalize_term t =
- let
- fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
- | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
- Type (_, [_, res_T])]))
- $ t2 $ Abs (var_s, var_T, t')) =
- if s = @{const_name "op ="} orelse s = @{const_name "=="} then
- let val var_t = Var ((var_s, j), var_T) in
- Const (s, T' --> T' --> res_T)
- $ betapply (t2, var_t) $ subst_bound (var_t, t')
- |> aux (j + 1)
- end
- else
- t
- | aux _ t = t
- in aux (maxidx_of_term t + 1) t end
-
fun monomorphic_term subst t =
map_types (map_type_tvar (fn v =>
case Type.lookup subst v of
--- a/src/HOL/Tools/meson.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/HOL/Tools/meson.ML Mon Aug 23 11:18:38 2010 +0200
@@ -411,7 +411,7 @@
(fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
(*A higher-order instance of a first-order constant? Example is the definition of
- one, 1, at a function type in theory SetsAndFunctions.*)
+ one, 1, at a function type in theory Function_Algebras.*)
fun higher_inst_const thy (c,T) =
case binder_types T of
[] => false (*not a function type, OK*)
@@ -520,7 +520,7 @@
forward_res ctxt (make_nnf1 ctxt)
(tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
handle THM ("tryres", _, _) => th
- else th;
+ else th
(*The simplification removes defined quantifiers and occurrences of True and False.
nnf_ss also includes the one-point simprocs,
@@ -539,8 +539,7 @@
#> simplify nnf_ss
fun make_nnf ctxt th = case prems_of th of
- [] => th |> presimplify
- |> make_nnf1 ctxt
+ [] => th |> presimplify |> make_nnf1 ctxt
| _ => raise THM ("make_nnf: premises in argument", 0, [th]);
(*Pull existential quantifiers to front. This accomplishes Skolemization for
--- a/src/Pure/Isar/class.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/Pure/Isar/class.ML Mon Aug 23 11:18:38 2010 +0200
@@ -17,9 +17,8 @@
val print_classes: theory -> unit
val init: class -> theory -> Proof.context
val begin: class list -> sort -> Proof.context -> Proof.context
- val const: class -> (binding * mixfix) * (term list * term) -> theory -> theory
- val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
- val refresh_syntax: class -> Proof.context -> Proof.context
+ val const: class -> (binding * mixfix) * (term list * term) -> local_theory -> local_theory
+ val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
val class_prefix: string -> string
val register: class -> class list -> ((string * typ) * (string * typ)) list
@@ -286,12 +285,6 @@
|> Overloading.set_primary_constraints
end;
-fun refresh_syntax class ctxt =
- let
- val thy = ProofContext.theory_of ctxt;
- val base_sort = base_sort thy class;
- in synchronize_class_syntax [class] base_sort ctxt end;
-
fun redeclare_operations thy sort =
fold (redeclare_const thy o fst) (these_operations thy sort);
@@ -312,7 +305,15 @@
val class_prefix = Logic.const_of_class o Long_Name.base_name;
-fun const class ((c, mx), (type_params, dict)) thy =
+fun target_extension f class lthy =
+ lthy
+ |> Local_Theory.raw_theory f
+ |> Local_Theory.target (synchronize_class_syntax [class]
+ (base_sort (ProofContext.theory_of lthy) class));
+
+local
+
+fun target_const class ((c, mx), (type_params, dict)) thy =
let
val morph = morphism thy class;
val b = Morphism.binding morph c;
@@ -334,7 +335,7 @@
|> Sign.add_const_constraint (c', SOME ty')
end;
-fun abbrev class prmode ((c, mx), rhs) thy =
+fun target_abbrev class prmode ((c, mx), rhs) thy =
let
val morph = morphism thy class;
val unchecks = these_unchecks thy [class];
@@ -352,6 +353,13 @@
|> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
end;
+in
+
+fun const class arg = target_extension (target_const class arg) class;
+fun abbrev class prmode arg = target_extension (target_abbrev class prmode arg) class;
+
+end;
+
(* simple subclasses *)
--- a/src/Pure/Isar/named_target.ML Sun Aug 22 22:28:24 2010 +0200
+++ b/src/Pure/Isar/named_target.ML Mon Aug 23 11:18:38 2010 +0200
@@ -88,10 +88,6 @@
fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
-fun class_target (Target {target, ...}) f =
- Local_Theory.raw_theory f #>
- Local_Theory.target (Class.refresh_syntax target);
-
(* define *)
@@ -104,7 +100,7 @@
(((b, U), mx), (b_def, rhs)) (type_params, term_params) =
Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
#-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
- #> class_target ta (Class.const target ((b, mx), (type_params, lhs)))
+ #> Class.const target ((b, mx), (type_params, lhs))
#> pair (lhs, def))
fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
@@ -143,7 +139,7 @@
if is_locale
then lthy
|> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
- |> is_class ? class_target ta (Class.abbrev target prmode ((b, mx), t'))
+ |> is_class ? Class.abbrev target prmode ((b, mx), t')
else lthy
|> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);