# HG changeset patch
# User blanchet
# Date 1258993663 -3600
# Node ID 8f335b40b550698681db1df37de9934f64e54eaf
# Parent  232daf7eafaf237da87cb6017f50b0c79245893a# Parent  fb95d9152fa9d66379d7ca371b23505f81bdb64b
merge

diff -r 232daf7eafaf -r 8f335b40b550 Admin/isatest/minimal-test
--- 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"
 
 
diff -r 232daf7eafaf -r 8f335b40b550 CONTRIBUTORS
--- 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.
diff -r 232daf7eafaf -r 8f335b40b550 NEWS
--- 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 ***
 
diff -r 232daf7eafaf -r 8f335b40b550 doc-src/Functions/Thy/Functions.thy
--- 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:
+subsection {* The @{text size_change} method *}
+
+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}
+
+  Loading the theory @{text Multiset} makes the @{text size_change}
+  method a bit stronger: it can then use multiset orders internally.
 *}
-(*
-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
-
-termination apply lexicographic_order
-
-text {* If we try @{text "lexicographic_order"} method, we get the
-  following error *}
-termination by (lexicographic_order simp:l2)
-
-lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith
-
-function 
-
-*)
 
 section {* Mutual Recursion *}
 
diff -r 232daf7eafaf -r 8f335b40b550 doc-src/Functions/Thy/document/Functions.tex
--- 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%
 %
diff -r 232daf7eafaf -r 8f335b40b550 doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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}
 *}
 
diff -r 232daf7eafaf -r 8f335b40b550 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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%
diff -r 232daf7eafaf -r 8f335b40b550 doc-src/manual.bib
--- 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}},
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/decompose.ML
--- 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
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/fun.ML
--- 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
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/function_core.ML
--- 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
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/function_lib.ML
--- 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
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/induction_schema.ML
--- 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 
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/lexicographic_order.ML
--- 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))
 
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/mutual.ML
--- 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))
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/pattern_split.ML
--- 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
 
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/scnp_reconstruct.ML
--- 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)
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/scnp_solve.ML
--- 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
diff -r 232daf7eafaf -r 8f335b40b550 src/HOL/Tools/Function/termination.ML
--- 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