--- a/Admin/isatest/minimal-test Mon Nov 23 17:26:32 2009 +0100
+++ b/Admin/isatest/minimal-test Mon Nov 23 17:27:43 2009 +0100
@@ -14,7 +14,7 @@
LOGDIR="$HOME/log"
LOG="$LOGDIR/test-${DATE}-${HOST}.log"
-TEST_NAME="minimal-test@${HOST}"
+TEST_NAME="minimal-test"
PUBLISH_TEST="/home/isabelle-repository/repos/testtool/publish_test.py"
--- a/CONTRIBUTORS Mon Nov 23 17:26:32 2009 +0100
+++ b/CONTRIBUTORS Mon Nov 23 17:27:43 2009 +0100
@@ -7,8 +7,11 @@
Contributions to Isabelle2009-1
-------------------------------
+* November 2009, Brian Huffman, PSU
+ New definitional domain package for HOLCF.
+
* November 2009: Robert Himmelmann, TUM
- Derivation and Brouwer's fixpoint theorem in Multivariate Analysis
+ Derivation and Brouwer's fixpoint theorem in Multivariate Analysis.
* November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
A tabled implementation of the reflexive transitive closure.
--- a/NEWS Mon Nov 23 17:26:32 2009 +0100
+++ b/NEWS Mon Nov 23 17:27:43 2009 +0100
@@ -55,6 +55,16 @@
relational model finder. See src/HOL/Tools/Nitpick and
src/HOL/Nitpick_Examples.
+* New commands 'code_pred' and 'values' to invoke the predicate
+compiler and to enumerate values of inductive predicates.
+
+* A tabled implementation of the reflexive transitive closure.
+
+* New implementation of quickcheck uses generic code generator;
+default generators are provided for all suitable HOL types, records
+and datatypes. Old quickcheck can be re-activated importing theory
+Library/SML_Quickcheck.
+
* New testing tool Mirabelle for automated proof tools. Applies
several tools and tactics like sledgehammer, metis, or quickcheck, to
every proof step in a theory. To be used in batch mode via the
@@ -71,25 +81,9 @@
to call an external tool every time the proof is checked. See
src/HOL/Library/Sum_Of_Squares.
-* New commands 'code_pred' and 'values' to invoke the predicate
-compiler and to enumerate values of inductive predicates.
-
-* A tabled implementation of the reflexive transitive closure.
-
-* New theory SupInf of the supremum and infimum operators for sets of
-reals.
-
-* New theory Probability, which contains a development of measure
-theory, eventually leading to Lebesgue integration and probability.
-
* New method "linarith" invokes existing linear arithmetic decision
procedure only.
-* New implementation of quickcheck uses generic code generator;
-default generators are provided for all suitable HOL types, records
-and datatypes. Old quickcheck can be re-activated importing theory
-Library/SML_Quickcheck.
-
* New command 'atp_minimal' reduces result produced by Sledgehammer.
* New Sledgehammer option "Full Types" in Proof General settings menu.
@@ -110,8 +104,14 @@
* ML antiquotation @{code_datatype} inserts definition of a datatype
generated by the code generator; e.g. see src/HOL/Predicate.thy.
-* Most rules produced by inductive and datatype package have mandatory
-prefixes. INCOMPATIBILITY.
+* New theory SupInf of the supremum and infimum operators for sets of
+reals.
+
+* New theory Probability, which contains a development of measure
+theory, eventually leading to Lebesgue integration and probability.
+
+* Extended Multivariate Analysis to include derivation and Brouwer's
+fixpoint theorem.
* Reorganization of number theory, INCOMPATIBILITY:
- new number theory development for nat and int, in
@@ -125,7 +125,7 @@
- moved theory Pocklington from src/HOL/Library to
src/HOL/Old_Number_Theory
-* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
+* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm
of finite and infinite sets. It is shown that they form a complete
lattice.
@@ -137,24 +137,6 @@
zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
INCOMPATIBILITY.
-* Extended Multivariate Analysis to include derivation and Brouwer's
-fixpoint theorem.
-
-* Removed predicate "M hassize n" (<--> card M = n & finite M).
-INCOMPATIBILITY.
-
-* Renamed vector_less_eq_def to vector_le_def, the more usual name.
-INCOMPATIBILITY.
-
-* Added theorem List.map_map as [simp]. Removed List.map_compose.
-INCOMPATIBILITY.
-
-* Code generator attributes follow the usual underscore convention:
- code_unfold replaces code unfold
- code_post replaces code post
- etc.
- INCOMPATIBILITY.
-
* Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
@@ -165,27 +147,24 @@
- renamed ACI to inf_sup_aci
- new class "boolean_algebra"
- class "complete_lattice" moved to separate theory
- "complete_lattice"; corresponding constants (and abbreviations)
+ "Complete_Lattice"; corresponding constants (and abbreviations)
renamed and with authentic syntax:
- Set.Inf ~> Complete_Lattice.Inf
- Set.Sup ~> Complete_Lattice.Sup
- Set.INFI ~> Complete_Lattice.INFI
- Set.SUPR ~> Complete_Lattice.SUPR
- Set.Inter ~> Complete_Lattice.Inter
- Set.Union ~> Complete_Lattice.Union
- Set.INTER ~> Complete_Lattice.INTER
- Set.UNION ~> Complete_Lattice.UNION
- - more convenient names for set intersection and union:
- Set.Int ~> Set.inter
- Set.Un ~> Set.union
+ Set.Inf ~> Complete_Lattice.Inf
+ Set.Sup ~> Complete_Lattice.Sup
+ Set.INFI ~> Complete_Lattice.INFI
+ Set.SUPR ~> Complete_Lattice.SUPR
+ Set.Inter ~> Complete_Lattice.Inter
+ Set.Union ~> Complete_Lattice.Union
+ Set.INTER ~> Complete_Lattice.INTER
+ Set.UNION ~> Complete_Lattice.UNION
- authentic syntax for
Set.Pow
Set.image
- mere abbreviations:
Set.empty (for bot)
Set.UNIV (for top)
- Set.inter (for inf)
- Set.union (for sup)
+ Set.inter (for inf, formerly Set.Int)
+ Set.union (for sup, formerly Set.Un)
Complete_Lattice.Inter (for Inf)
Complete_Lattice.Union (for Sup)
Complete_Lattice.INTER (for INFI)
@@ -219,31 +198,47 @@
abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
INCOMPATIBILITY.
-* Renamed theorems:
-Suc_eq_add_numeral_1 -> Suc_eq_plus1
-Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
-Suc_plus1 -> Suc_eq_plus1
+--
+
+* Most rules produced by inductive and datatype package have mandatory
+prefixes. INCOMPATIBILITY.
* Changed "DERIV_intros" to a dynamic fact, which can be augmented by
the attribute of the same name. Each of the theorems in the list
DERIV_intros assumes composition with an additional function and
matches a variable to the derivative, which has to be solved by the
Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative
-of most elementary terms.
-
-* Former Maclauren.DERIV_tac and Maclauren.deriv_tac are superseded
-are replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
+of most elementary terms. Former Maclauren.DERIV_tac and Maclauren.deriv_tac
+should be replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
+
+* Code generator attributes follow the usual underscore convention:
+ code_unfold replaces code unfold
+ code_post replaces code post
+ etc.
+ INCOMPATIBILITY.
* Renamed methods:
sizechange -> size_change
induct_scheme -> induction_schema
-
-* Lemma name change: replaced "anti_sym" by "antisym" everywhere.
-INCOMPATIBILITY.
+ INCOMPATIBILITY.
* Discontinued abbreviation "arbitrary" of constant "undefined".
INCOMPATIBILITY, use "undefined" directly.
+* Renamed theorems:
+ Suc_eq_add_numeral_1 -> Suc_eq_plus1
+ Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
+ Suc_plus1 -> Suc_eq_plus1
+ *anti_sym -> *antisym*
+ vector_less_eq_def -> vector_le_def
+ INCOMPATIBILITY.
+
+* Added theorem List.map_map as [simp]. Removed List.map_compose.
+INCOMPATIBILITY.
+
+* Removed predicate "M hassize n" (<--> card M = n & finite M).
+INCOMPATIBILITY.
+
*** HOLCF ***
--- a/doc-src/Functions/Thy/Functions.thy Mon Nov 23 17:26:32 2009 +0100
+++ b/doc-src/Functions/Thy/Functions.thy Mon Nov 23 17:27:43 2009 +0100
@@ -309,8 +309,6 @@
*** At command "fun".\newline
\end{isabelle}
*}
-
-
text {*
The key to this error message is the matrix at the bottom. The rows
of that matrix correspond to the different recursive calls (In our
@@ -326,27 +324,30 @@
For the failed proof attempts, the unfinished subgoals are also
printed. Looking at these will often point to a missing lemma.
+*}
-% As a more real example, here is quicksort:
-*}
-(*
-function qs :: "nat list \<Rightarrow> nat list"
-where
- "qs [] = []"
-| "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"
-by pat_completeness auto
+subsection {* The @{text size_change} method *}
-termination apply lexicographic_order
-
-text {* If we try @{text "lexicographic_order"} method, we get the
- following error *}
-termination by (lexicographic_order simp:l2)
+text {*
+ Some termination goals that are beyond the powers of
+ @{text lexicographic_order} can be solved automatically by the
+ more powerful @{text size_change} method, which uses a variant of
+ the size-change principle, together with some other
+ techniques. While the details are discussed
+ elsewhere\cite{krauss_phd},
+ here are a few typical situations where
+ @{text lexicographic_order} has difficulties and @{text size_change}
+ may be worth a try:
+ \begin{itemize}
+ \item Arguments are permuted in a recursive call.
+ \item Several mutually recursive functions with multiple arguments.
+ \item Unusual control flow (e.g., when some recursive calls cannot
+ occur in sequence).
+ \end{itemize}
-lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith
-
-function
-
-*)
+ Loading the theory @{text Multiset} makes the @{text size_change}
+ method a bit stronger: it can then use multiset orders internally.
+*}
section {* Mutual Recursion *}
--- a/doc-src/Functions/Thy/document/Functions.tex Mon Nov 23 17:26:32 2009 +0100
+++ b/doc-src/Functions/Thy/document/Functions.tex Mon Nov 23 17:27:43 2009 +0100
@@ -453,9 +453,33 @@
\isa{{\isacharless}}, \isa{{\isacharless}{\isacharequal}} and \isa{{\isacharquery}}.
For the failed proof attempts, the unfinished subgoals are also
- printed. Looking at these will often point to a missing lemma.
+ printed. Looking at these will often point to a missing lemma.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{The \isa{size{\isacharunderscore}change} method%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Some termination goals that are beyond the powers of
+ \isa{lexicographic{\isacharunderscore}order} can be solved automatically by the
+ more powerful \isa{size{\isacharunderscore}change} method, which uses a variant of
+ the size-change principle, together with some other
+ techniques. While the details are discussed
+ elsewhere\cite{krauss_phd},
+ here are a few typical situations where
+ \isa{lexicographic{\isacharunderscore}order} has difficulties and \isa{size{\isacharunderscore}change}
+ may be worth a try:
+ \begin{itemize}
+ \item Arguments are permuted in a recursive call.
+ \item Several mutually recursive functions with multiple arguments.
+ \item Unusual control flow (e.g., when some recursive calls cannot
+ occur in sequence).
+ \end{itemize}
-% As a more real example, here is quicksort:%
+ Loading the theory \isa{Multiset} makes the \isa{size{\isacharunderscore}change}
+ method a bit stronger: it can then use multiset orders internally.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Nov 23 17:26:32 2009 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Nov 23 17:27:43 2009 +0100
@@ -452,20 +452,16 @@
\end{description}
- %FIXME check
-
Recursive definitions introduced by the @{command (HOL) "function"}
command accommodate
reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
"c.induct"} (where @{text c} is the name of the function definition)
refers to a specific induction rule, with parameters named according
- to the user-specified equations.
- For the @{command (HOL) "primrec"} the induction principle coincides
+ to the user-specified equations. Cases are numbered (starting from 1).
+
+ For @{command (HOL) "primrec"}, the induction principle coincides
with structural recursion on the datatype the recursion is carried
out.
- Case names of @{command (HOL)
- "primrec"} are that of the datatypes involved, while those of
- @{command (HOL) "function"} are numbered (starting from 1).
The equations provided by these packages may be referred later as
theorem list @{text "f.simps"}, where @{text f} is the (collective)
@@ -510,6 +506,7 @@
@{method_def (HOL) pat_completeness} & : & @{text method} \\
@{method_def (HOL) relation} & : & @{text method} \\
@{method_def (HOL) lexicographic_order} & : & @{text method} \\
+ @{method_def (HOL) size_change} & : & @{text method} \\
\end{matharray}
\begin{rail}
@@ -517,6 +514,9 @@
;
'lexicographic\_order' ( clasimpmod * )
;
+ 'size\_change' ( orders ( clasimpmod * ) )
+ ;
+ orders: ( 'max' | 'min' | 'ms' ) *
\end{rail}
\begin{description}
@@ -544,6 +544,18 @@
In case of failure, extensive information is printed, which can help
to analyse the situation (cf.\ \cite{isabelle-function}).
+ \item @{method (HOL) "size_change"} also works on termination goals,
+ using a variation of the size-change principle, together with a
+ graph decomposition technique (see \cite{krauss_phd} for details).
+ Three kinds of orders are used internally: @{text max}, @{text min},
+ and @{text ms} (multiset), which is only available when the theory
+ @{text Multiset} is loaded. When no order kinds are given, they are
+ tried in order. The search for a termination proof uses SAT solving
+ internally.
+
+ For local descent proofs, the same context modifiers as for @{method
+ auto} are accepted, see \secref{sec:clasimp}.
+
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 23 17:26:32 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 23 17:27:43 2009 +0100
@@ -457,18 +457,15 @@
\end{description}
- %FIXME check
-
Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
command accommodate
reasoning by induction (cf.\ \secref{sec:cases-induct}): rule \isa{{\isachardoublequote}c{\isachardot}induct{\isachardoublequote}} (where \isa{c} is the name of the function definition)
refers to a specific induction rule, with parameters named according
- to the user-specified equations.
- For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides
+ to the user-specified equations. Cases are numbered (starting from 1).
+
+ For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
with structural recursion on the datatype the recursion is carried
out.
- Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
- \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).
The equations provided by these packages may be referred later as
theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)
@@ -515,6 +512,7 @@
\indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isa{method} \\
\indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
\indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isa{method} \\
+ \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}}} & : & \isa{method} \\
\end{matharray}
\begin{rail}
@@ -522,6 +520,9 @@
;
'lexicographic\_order' ( clasimpmod * )
;
+ 'size\_change' ( orders ( clasimpmod * ) )
+ ;
+ orders: ( 'max' | 'min' | 'ms' ) *
\end{rail}
\begin{description}
@@ -549,6 +550,17 @@
In case of failure, extensive information is printed, which can help
to analyse the situation (cf.\ \cite{isabelle-function}).
+ \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}} also works on termination goals,
+ using a variation of the size-change principle, together with a
+ graph decomposition technique (see \cite{krauss_phd} for details).
+ Three kinds of orders are used internally: \isa{max}, \isa{min},
+ and \isa{ms} (multiset), which is only available when the theory
+ \isa{Multiset} is loaded. When no order kinds are given, they are
+ tried in order. The search for a termination proof uses SAT solving
+ internally.
+
+ For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/manual.bib Mon Nov 23 17:26:32 2009 +0100
+++ b/doc-src/manual.bib Mon Nov 23 17:27:43 2009 +0100
@@ -660,6 +660,14 @@
crossref = {ijcar2006},
pages = {589--603}}
+@PhdThesis{krauss_phd,
+ author = {Alexander Krauss},
+ title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
+ school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
+ year = {2009},
+ address = {Germany}
+}
+
@manual{isabelle-function,
author = {Alexander Krauss},
title = {Defining Recursive Functions in {Isabelle/HOL}},
--- a/src/HOL/Tools/Function/decompose.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/decompose.ML Mon Nov 23 17:27:43 2009 +0100
@@ -74,7 +74,7 @@
| _ => no_tac)
| _ => no_tac)
-fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+fun decompose_tac' cont err_cont D = Termination.CALLS (fn (cs, i) =>
let
val G = mk_dgraph D cs
val sccs = TermGraph.strong_conn G
@@ -94,12 +94,7 @@
fun decompose_tac ctxt chain_tac cont err_cont =
derive_chains ctxt chain_tac
- (decompose_tac' ctxt cont err_cont)
-
-fun auto_decompose_tac ctxt =
- Termination.TERMINATION ctxt
- (decompose_tac ctxt (auto_tac (clasimpset_of ctxt))
- (K (K all_tac)) (K (K no_tac)))
+ (decompose_tac' cont err_cont)
end
--- a/src/HOL/Tools/Function/fun.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML Mon Nov 23 17:27:43 2009 +0100
@@ -44,7 +44,7 @@
())
end
- val (fname, qs, gs, args, rhs) = split_def ctxt geq
+ val (_, qs, gs, args, _) = split_def ctxt geq
val _ = if not (null gs) then err "Conditional equations" else ()
val _ = map check_constr_pattern args
--- a/src/HOL/Tools/Function/function_core.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Mon Nov 23 17:27:43 2009 +0100
@@ -97,8 +97,6 @@
(* Theory dependencies. *)
-val Pair_inject = @{thm Product_Type.Pair_inject};
-
val acc_induct_rule = @{thm accp_induct_rule};
val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
@@ -199,7 +197,7 @@
fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
let
- val Globals {h, fvar, x, ...} = globals
+ val Globals {h, ...} = globals
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
@@ -298,7 +296,7 @@
(* Generates the replacement lemma in fully quantified form. *)
fun mk_replacement_lemma thy h ih_elim clause =
let
- val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
+ val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
local open Conv in
val ih_conv = arg1_conv o arg_conv o arg_conv
end
@@ -321,7 +319,7 @@
end
-fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
+fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj =
let
val Globals {h, y, x, fvar, ...} = globals
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
@@ -355,10 +353,10 @@
-fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
+fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
let
val Globals {x, y, ranT, fvar, ...} = globals
- val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
+ val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
@@ -372,7 +370,7 @@
val P = cterm_of thy (mk_eq (y, rhsC))
val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
- val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
+ val unique_clauses = map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
val uniqueness = G_cases
|> forall_elim (cterm_of thy lhs)
@@ -430,7 +428,7 @@
val _ = trace_msg (K "Proving cases for unique existence...")
val (ex1s, values) =
- split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
+ split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
val _ = trace_msg (K "Proving: Graph is a function")
val graph_is_function = complete
@@ -523,7 +521,7 @@
((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
end
-fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
+fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
let
val RT = domT --> domT --> boolT
val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
@@ -700,8 +698,6 @@
|> implies_intr D_dcl
|> implies_intr D_subset
- val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
-
val simple_induct_rule =
subset_induct_rule
|> forall_intr (cterm_of thy D)
@@ -724,7 +720,7 @@
fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
let
val thy = ProofContext.theory_of ctxt
- val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
+ val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
qglr = (oqs, _, _, _), ...} = clause
val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
|> fold_rev (curry Logic.mk_implies) gs
@@ -748,8 +744,8 @@
fun mk_nest_term_case thy globals R' ihyp clause =
let
- val Globals {x, z, ...} = globals
- val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
+ val Globals {z, ...} = globals
+ val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...},tree,
qglr=(oqs, _, _, _), ...} = clause
val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
@@ -868,7 +864,7 @@
fun mk_trsimp clause psimp =
let
- val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
+ val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
val thy = ProofContext.theory_of ctxt
val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
@@ -925,7 +921,7 @@
val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
val ((R, RIntro_thmss, R_elim), lthy) =
- PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
+ PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
val (_, lthy) =
Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
--- a/src/HOL/Tools/Function/function_lib.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Mon Nov 23 17:27:43 2009 +0100
@@ -14,9 +14,6 @@
fun fold_option f NONE y = y
| fold_option f (SOME x) y = f x y;
-fun fold_map_option f NONE y = (NONE, y)
- | fold_map_option f (SOME x) y = apfst SOME (f x y);
-
(* Ex: "The variable" ^ plural " is" "s are" vs *)
fun plural sg pl [x] = sg
| plural sg pl _ = pl
@@ -53,7 +50,7 @@
(* FIXME: similar to Variable.focus *)
-fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
+fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (n,T,b)) =
let
val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
--- a/src/HOL/Tools/Function/induction_schema.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Mon Nov 23 17:27:43 2009 +0100
@@ -75,7 +75,7 @@
let
fun mk_branch concl =
let
- val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
+ val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
val (P, xs) = strip_comb Pxs
in
SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
@@ -103,7 +103,7 @@
fun mk_rcinfo pr =
let
- val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
+ val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
val (P', rcs) = strip_comb Phyp
in
(bidx P', Gvs, Gas, rcs)
@@ -151,7 +151,7 @@
|> mk_forall_rename ("P", Pbool)
end
-fun mk_wf ctxt R (IndScheme {T, ...}) =
+fun mk_wf R (IndScheme {T, ...}) =
HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
fun mk_ineqs R (IndScheme {T, cases, branches}) =
@@ -198,8 +198,6 @@
end
-fun mk_hol_imp a b = HOLogic.imp $ a $ b
-
fun mk_ind_goal thy branches =
let
fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
@@ -256,7 +254,7 @@
val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
|> split_list
- fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
+ fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
let
val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
@@ -364,7 +362,7 @@
val ineqss = mk_ineqs R scheme
|> map (map (pairself (assume o cert)))
val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
- val wf_thm = mk_wf ctxt R scheme |> cert |> assume
+ val wf_thm = mk_wf R scheme |> cert |> assume
val (descent, pres) = split_list (flat ineqss)
val newgoals = complete @ pres @ wf_thm :: descent
--- a/src/HOL/Tools/Function/lexicographic_order.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon Nov 23 17:27:43 2009 +0100
@@ -75,10 +75,6 @@
fold_rev Logic.all vars (Logic.list_implies (prems, concl))
end
-fun prove thy solve_tac t =
- cterm_of thy t |> Goal.init
- |> SINGLE solve_tac |> the
-
fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
let
val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
@@ -137,8 +133,6 @@
(** Error reporting **)
-fun pr_table table = writeln (cat_lines (map (fn r => implode (map pr_cell r)) table))
-
fun pr_goals ctxt st =
Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
|> Pretty.chunks
@@ -190,7 +184,7 @@
fun lex_order_tac quiet ctxt solve_tac (st: thm) =
let
val thy = ProofContext.theory_of ctxt
- val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
+ val ((_ $ (_ $ rel)) :: tl) = prems_of st
val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
--- a/src/HOL/Tools/Function/mutual.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Mon Nov 23 17:27:43 2009 +0100
@@ -28,8 +28,6 @@
type qgar = string * (string * typ) list * term list * term list * term
-fun name_of_fqgar ((f, _, _, _, _): qgar) = f
-
datatype mutual_part =
MutualPart of
{
@@ -82,7 +80,6 @@
fun analyze_eqs ctxt defname fs eqs =
let
val num = length fs
- val fnames = map fst fs
val fqgars = map (split_def ctxt) eqs
val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
|> AList.lookup (op =) #> the
@@ -108,7 +105,7 @@
val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
val fsum_var = (fsum_var_name, fsum_type)
- fun define (fvar as (n, T)) caTs resultT i =
+ fun define (fvar as (n, _)) caTs resultT i =
let
val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
@@ -170,8 +167,8 @@
val thy = ProofContext.theory_of ctxt
val oqnames = map fst pre_qs
- val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
- |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
+ val (qs, _) = Variable.variant_fixes oqnames ctxt
+ |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
fun inst t = subst_bounds (rev qs, t)
val gs = map inst pre_gs
@@ -192,7 +189,7 @@
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq =
let
- val (MutualPart {f=SOME f, f_defthm=SOME f_def, ...}) = get_part fname parts
+ val (MutualPart {f=SOME f, ...}) = get_part fname parts
val psimp = import sum_psimp_eq
val (simp, restore_cond) = case cprems_of psimp of
@@ -223,7 +220,7 @@
end
-fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, RST, parts, ...}) =
+fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) =
let
val cert = cterm_of (ProofContext.theory_of lthy)
val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} =>
@@ -266,8 +263,8 @@
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
let
val result = inner_cont proof
- val FunctionResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
- termination,domintros} = result
+ val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
+ termination, domintros, ...} = result
val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
(mk_applied_form lthy cargTs (symmetric f_def), f))
--- a/src/HOL/Tools/Function/pattern_split.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML Mon Nov 23 17:27:43 2009 +0100
@@ -50,9 +50,6 @@
fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
fun join_product (xs, ys) = map_product (curry join) xs ys
-fun join_list [] = []
- | join_list xs = foldr1 (join_product) xs
-
exception DISJ
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Nov 23 17:27:43 2009 +0100
@@ -73,7 +73,7 @@
val multiset_setup = Multiset_Setup.put o SOME
-fun undef x = error "undef"
+fun undef _ = error "undef"
fun get_multiset_setup thy = Multiset_Setup.get thy
|> the_default (Multiset
{ msetT = undef, mk_mset=undef,
@@ -153,14 +153,13 @@
(* Reconstruction *)
-fun reconstruct_tac ctxt D cs (gp as GP (_, gs)) certificate =
+fun reconstruct_tac ctxt D cs (GP (_, gs)) certificate =
let
val thy = ProofContext.theory_of ctxt
val Multiset
{ msetT, mk_mset,
- mset_regroup_conv, mset_member_tac,
- mset_nonempty_tac, mset_pwleq_tac, set_of_simps,
- smsI', wmsI2'', wmsI1, reduction_pair=ms_rp }
+ mset_regroup_conv, mset_pwleq_tac, set_of_simps,
+ smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...}
= get_multiset_setup thy
fun measure_fn p = nth (Termination.get_measures D p)
@@ -179,7 +178,7 @@
fun prove_lev strict g =
let
- val G (p, q, el) = nth gs g
+ val G (p, q, _) = nth gs g
fun less_proof strict (j, b) (i, a) =
let
@@ -307,11 +306,10 @@
| print_cell (SOME (False _)) = "-"
| print_cell (NONE) = "?"
-fun print_error ctxt D = CALLS (fn (cs, i) =>
+fun print_error ctxt D = CALLS (fn (cs, _) =>
let
val np = get_num_points D
val ms = map_range (get_measures D) np
- val tys = map_range (get_types D) np
fun index xs = (1 upto length xs) ~~ xs
fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
val ims = index (map index ms)
--- a/src/HOL/Tools/Function/scnp_solve.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_solve.ML Mon Nov 23 17:27:43 2009 +0100
@@ -76,7 +76,7 @@
Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
(* "Virtual constructors" for various propositional variables *)
-fun var_constrs (gp as GP (arities, gl)) =
+fun var_constrs (gp as GP (arities, _)) =
let
val n = Int.max (num_graphs gp, num_prog_pts gp)
val k = fold Integer.max arities 1
--- a/src/HOL/Tools/Function/termination.ML Mon Nov 23 17:26:32 2009 +0100
+++ b/src/HOL/Tools/Function/termination.ML Mon Nov 23 17:27:43 2009 +0100
@@ -148,7 +148,7 @@
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+ val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _)
= Term.strip_qnt_body "Ex" c
in cons r o cons l end
in
@@ -181,7 +181,6 @@
fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val n = get_num_points D
val (sk, _, _, _, _) = D
val vs = Term.strip_qnt_vars "Ex" c
@@ -196,7 +195,7 @@
| dest_call D t = error "dest_call"
-fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D =
+fun derive_desc_aux thy tac c (vs, _, l', _, r', Gam) m1 m2 D =
case get_descent D c m1 m2 of
SOME _ => D
| NONE => let
@@ -225,7 +224,7 @@
(* all descents in one go *)
fun derive_descents thy tac c D =
- let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c
+ let val cdesc as (_, p, _, q, _, _) = dest_call D c
in fold_product (derive_desc_aux thy tac c cdesc)
(get_measures D p) (get_measures D q) D
end
@@ -280,7 +279,7 @@
let
val thy = ProofContext.theory_of ctxt
val cert = cterm_of (theory_of_thm st)
- val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
+ val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
fun mk_compr ineq =
let