1.1 --- a/Admin/isatest/minimal-test Mon Nov 23 17:26:32 2009 +0100
1.2 +++ b/Admin/isatest/minimal-test Mon Nov 23 17:27:43 2009 +0100
1.3 @@ -14,7 +14,7 @@
1.4 LOGDIR="$HOME/log"
1.5 LOG="$LOGDIR/test-${DATE}-${HOST}.log"
1.6
1.7 -TEST_NAME="minimal-test@${HOST}"
1.8 +TEST_NAME="minimal-test"
1.9 PUBLISH_TEST="/home/isabelle-repository/repos/testtool/publish_test.py"
1.10
1.11
2.1 --- a/CONTRIBUTORS Mon Nov 23 17:26:32 2009 +0100
2.2 +++ b/CONTRIBUTORS Mon Nov 23 17:27:43 2009 +0100
2.3 @@ -7,8 +7,11 @@
2.4 Contributions to Isabelle2009-1
2.5 -------------------------------
2.6
2.7 +* November 2009, Brian Huffman, PSU
2.8 + New definitional domain package for HOLCF.
2.9 +
2.10 * November 2009: Robert Himmelmann, TUM
2.11 - Derivation and Brouwer's fixpoint theorem in Multivariate Analysis
2.12 + Derivation and Brouwer's fixpoint theorem in Multivariate Analysis.
2.13
2.14 * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM
2.15 A tabled implementation of the reflexive transitive closure.
3.1 --- a/NEWS Mon Nov 23 17:26:32 2009 +0100
3.2 +++ b/NEWS Mon Nov 23 17:27:43 2009 +0100
3.3 @@ -55,6 +55,16 @@
3.4 relational model finder. See src/HOL/Tools/Nitpick and
3.5 src/HOL/Nitpick_Examples.
3.6
3.7 +* New commands 'code_pred' and 'values' to invoke the predicate
3.8 +compiler and to enumerate values of inductive predicates.
3.9 +
3.10 +* A tabled implementation of the reflexive transitive closure.
3.11 +
3.12 +* New implementation of quickcheck uses generic code generator;
3.13 +default generators are provided for all suitable HOL types, records
3.14 +and datatypes. Old quickcheck can be re-activated importing theory
3.15 +Library/SML_Quickcheck.
3.16 +
3.17 * New testing tool Mirabelle for automated proof tools. Applies
3.18 several tools and tactics like sledgehammer, metis, or quickcheck, to
3.19 every proof step in a theory. To be used in batch mode via the
3.20 @@ -71,25 +81,9 @@
3.21 to call an external tool every time the proof is checked. See
3.22 src/HOL/Library/Sum_Of_Squares.
3.23
3.24 -* New commands 'code_pred' and 'values' to invoke the predicate
3.25 -compiler and to enumerate values of inductive predicates.
3.26 -
3.27 -* A tabled implementation of the reflexive transitive closure.
3.28 -
3.29 -* New theory SupInf of the supremum and infimum operators for sets of
3.30 -reals.
3.31 -
3.32 -* New theory Probability, which contains a development of measure
3.33 -theory, eventually leading to Lebesgue integration and probability.
3.34 -
3.35 * New method "linarith" invokes existing linear arithmetic decision
3.36 procedure only.
3.37
3.38 -* New implementation of quickcheck uses generic code generator;
3.39 -default generators are provided for all suitable HOL types, records
3.40 -and datatypes. Old quickcheck can be re-activated importing theory
3.41 -Library/SML_Quickcheck.
3.42 -
3.43 * New command 'atp_minimal' reduces result produced by Sledgehammer.
3.44
3.45 * New Sledgehammer option "Full Types" in Proof General settings menu.
3.46 @@ -110,8 +104,14 @@
3.47 * ML antiquotation @{code_datatype} inserts definition of a datatype
3.48 generated by the code generator; e.g. see src/HOL/Predicate.thy.
3.49
3.50 -* Most rules produced by inductive and datatype package have mandatory
3.51 -prefixes. INCOMPATIBILITY.
3.52 +* New theory SupInf of the supremum and infimum operators for sets of
3.53 +reals.
3.54 +
3.55 +* New theory Probability, which contains a development of measure
3.56 +theory, eventually leading to Lebesgue integration and probability.
3.57 +
3.58 +* Extended Multivariate Analysis to include derivation and Brouwer's
3.59 +fixpoint theorem.
3.60
3.61 * Reorganization of number theory, INCOMPATIBILITY:
3.62 - new number theory development for nat and int, in
3.63 @@ -125,7 +125,7 @@
3.64 - moved theory Pocklington from src/HOL/Library to
3.65 src/HOL/Old_Number_Theory
3.66
3.67 -* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
3.68 +* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm
3.69 of finite and infinite sets. It is shown that they form a complete
3.70 lattice.
3.71
3.72 @@ -137,24 +137,6 @@
3.73 zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
3.74 INCOMPATIBILITY.
3.75
3.76 -* Extended Multivariate Analysis to include derivation and Brouwer's
3.77 -fixpoint theorem.
3.78 -
3.79 -* Removed predicate "M hassize n" (<--> card M = n & finite M).
3.80 -INCOMPATIBILITY.
3.81 -
3.82 -* Renamed vector_less_eq_def to vector_le_def, the more usual name.
3.83 -INCOMPATIBILITY.
3.84 -
3.85 -* Added theorem List.map_map as [simp]. Removed List.map_compose.
3.86 -INCOMPATIBILITY.
3.87 -
3.88 -* Code generator attributes follow the usual underscore convention:
3.89 - code_unfold replaces code unfold
3.90 - code_post replaces code post
3.91 - etc.
3.92 - INCOMPATIBILITY.
3.93 -
3.94 * Refinements to lattice classes and sets:
3.95 - less default intro/elim rules in locale variant, more default
3.96 intro/elim rules in class variant: more uniformity
3.97 @@ -165,27 +147,24 @@
3.98 - renamed ACI to inf_sup_aci
3.99 - new class "boolean_algebra"
3.100 - class "complete_lattice" moved to separate theory
3.101 - "complete_lattice"; corresponding constants (and abbreviations)
3.102 + "Complete_Lattice"; corresponding constants (and abbreviations)
3.103 renamed and with authentic syntax:
3.104 - Set.Inf ~> Complete_Lattice.Inf
3.105 - Set.Sup ~> Complete_Lattice.Sup
3.106 - Set.INFI ~> Complete_Lattice.INFI
3.107 - Set.SUPR ~> Complete_Lattice.SUPR
3.108 - Set.Inter ~> Complete_Lattice.Inter
3.109 - Set.Union ~> Complete_Lattice.Union
3.110 - Set.INTER ~> Complete_Lattice.INTER
3.111 - Set.UNION ~> Complete_Lattice.UNION
3.112 - - more convenient names for set intersection and union:
3.113 - Set.Int ~> Set.inter
3.114 - Set.Un ~> Set.union
3.115 + Set.Inf ~> Complete_Lattice.Inf
3.116 + Set.Sup ~> Complete_Lattice.Sup
3.117 + Set.INFI ~> Complete_Lattice.INFI
3.118 + Set.SUPR ~> Complete_Lattice.SUPR
3.119 + Set.Inter ~> Complete_Lattice.Inter
3.120 + Set.Union ~> Complete_Lattice.Union
3.121 + Set.INTER ~> Complete_Lattice.INTER
3.122 + Set.UNION ~> Complete_Lattice.UNION
3.123 - authentic syntax for
3.124 Set.Pow
3.125 Set.image
3.126 - mere abbreviations:
3.127 Set.empty (for bot)
3.128 Set.UNIV (for top)
3.129 - Set.inter (for inf)
3.130 - Set.union (for sup)
3.131 + Set.inter (for inf, formerly Set.Int)
3.132 + Set.union (for sup, formerly Set.Un)
3.133 Complete_Lattice.Inter (for Inf)
3.134 Complete_Lattice.Union (for Sup)
3.135 Complete_Lattice.INTER (for INFI)
3.136 @@ -219,31 +198,47 @@
3.137 abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
3.138 INCOMPATIBILITY.
3.139
3.140 -* Renamed theorems:
3.141 -Suc_eq_add_numeral_1 -> Suc_eq_plus1
3.142 -Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
3.143 -Suc_plus1 -> Suc_eq_plus1
3.144 +--
3.145 +
3.146 +* Most rules produced by inductive and datatype package have mandatory
3.147 +prefixes. INCOMPATIBILITY.
3.148
3.149 * Changed "DERIV_intros" to a dynamic fact, which can be augmented by
3.150 the attribute of the same name. Each of the theorems in the list
3.151 DERIV_intros assumes composition with an additional function and
3.152 matches a variable to the derivative, which has to be solved by the
3.153 Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative
3.154 -of most elementary terms.
3.155 -
3.156 -* Former Maclauren.DERIV_tac and Maclauren.deriv_tac are superseded
3.157 -are replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
3.158 +of most elementary terms. Former Maclauren.DERIV_tac and Maclauren.deriv_tac
3.159 +should be replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
3.160 +
3.161 +* Code generator attributes follow the usual underscore convention:
3.162 + code_unfold replaces code unfold
3.163 + code_post replaces code post
3.164 + etc.
3.165 + INCOMPATIBILITY.
3.166
3.167 * Renamed methods:
3.168 sizechange -> size_change
3.169 induct_scheme -> induction_schema
3.170 -
3.171 -* Lemma name change: replaced "anti_sym" by "antisym" everywhere.
3.172 -INCOMPATIBILITY.
3.173 + INCOMPATIBILITY.
3.174
3.175 * Discontinued abbreviation "arbitrary" of constant "undefined".
3.176 INCOMPATIBILITY, use "undefined" directly.
3.177
3.178 +* Renamed theorems:
3.179 + Suc_eq_add_numeral_1 -> Suc_eq_plus1
3.180 + Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
3.181 + Suc_plus1 -> Suc_eq_plus1
3.182 + *anti_sym -> *antisym*
3.183 + vector_less_eq_def -> vector_le_def
3.184 + INCOMPATIBILITY.
3.185 +
3.186 +* Added theorem List.map_map as [simp]. Removed List.map_compose.
3.187 +INCOMPATIBILITY.
3.188 +
3.189 +* Removed predicate "M hassize n" (<--> card M = n & finite M).
3.190 +INCOMPATIBILITY.
3.191 +
3.192
3.193 *** HOLCF ***
3.194
4.1 --- a/doc-src/Functions/Thy/Functions.thy Mon Nov 23 17:26:32 2009 +0100
4.2 +++ b/doc-src/Functions/Thy/Functions.thy Mon Nov 23 17:27:43 2009 +0100
4.3 @@ -309,8 +309,6 @@
4.4 *** At command "fun".\newline
4.5 \end{isabelle}
4.6 *}
4.7 -
4.8 -
4.9 text {*
4.10 The key to this error message is the matrix at the bottom. The rows
4.11 of that matrix correspond to the different recursive calls (In our
4.12 @@ -326,27 +324,30 @@
4.13
4.14 For the failed proof attempts, the unfinished subgoals are also
4.15 printed. Looking at these will often point to a missing lemma.
4.16 +*}
4.17
4.18 -% As a more real example, here is quicksort:
4.19 +subsection {* The @{text size_change} method *}
4.20 +
4.21 +text {*
4.22 + Some termination goals that are beyond the powers of
4.23 + @{text lexicographic_order} can be solved automatically by the
4.24 + more powerful @{text size_change} method, which uses a variant of
4.25 + the size-change principle, together with some other
4.26 + techniques. While the details are discussed
4.27 + elsewhere\cite{krauss_phd},
4.28 + here are a few typical situations where
4.29 + @{text lexicographic_order} has difficulties and @{text size_change}
4.30 + may be worth a try:
4.31 + \begin{itemize}
4.32 + \item Arguments are permuted in a recursive call.
4.33 + \item Several mutually recursive functions with multiple arguments.
4.34 + \item Unusual control flow (e.g., when some recursive calls cannot
4.35 + occur in sequence).
4.36 + \end{itemize}
4.37 +
4.38 + Loading the theory @{text Multiset} makes the @{text size_change}
4.39 + method a bit stronger: it can then use multiset orders internally.
4.40 *}
4.41 -(*
4.42 -function qs :: "nat list \<Rightarrow> nat list"
4.43 -where
4.44 - "qs [] = []"
4.45 -| "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"
4.46 -by pat_completeness auto
4.47 -
4.48 -termination apply lexicographic_order
4.49 -
4.50 -text {* If we try @{text "lexicographic_order"} method, we get the
4.51 - following error *}
4.52 -termination by (lexicographic_order simp:l2)
4.53 -
4.54 -lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith
4.55 -
4.56 -function
4.57 -
4.58 -*)
4.59
4.60 section {* Mutual Recursion *}
4.61
5.1 --- a/doc-src/Functions/Thy/document/Functions.tex Mon Nov 23 17:26:32 2009 +0100
5.2 +++ b/doc-src/Functions/Thy/document/Functions.tex Mon Nov 23 17:27:43 2009 +0100
5.3 @@ -453,9 +453,33 @@
5.4 \isa{{\isacharless}}, \isa{{\isacharless}{\isacharequal}} and \isa{{\isacharquery}}.
5.5
5.6 For the failed proof attempts, the unfinished subgoals are also
5.7 - printed. Looking at these will often point to a missing lemma.
5.8 + printed. Looking at these will often point to a missing lemma.%
5.9 +\end{isamarkuptext}%
5.10 +\isamarkuptrue%
5.11 +%
5.12 +\isamarkupsubsection{The \isa{size{\isacharunderscore}change} method%
5.13 +}
5.14 +\isamarkuptrue%
5.15 +%
5.16 +\begin{isamarkuptext}%
5.17 +Some termination goals that are beyond the powers of
5.18 + \isa{lexicographic{\isacharunderscore}order} can be solved automatically by the
5.19 + more powerful \isa{size{\isacharunderscore}change} method, which uses a variant of
5.20 + the size-change principle, together with some other
5.21 + techniques. While the details are discussed
5.22 + elsewhere\cite{krauss_phd},
5.23 + here are a few typical situations where
5.24 + \isa{lexicographic{\isacharunderscore}order} has difficulties and \isa{size{\isacharunderscore}change}
5.25 + may be worth a try:
5.26 + \begin{itemize}
5.27 + \item Arguments are permuted in a recursive call.
5.28 + \item Several mutually recursive functions with multiple arguments.
5.29 + \item Unusual control flow (e.g., when some recursive calls cannot
5.30 + occur in sequence).
5.31 + \end{itemize}
5.32
5.33 -% As a more real example, here is quicksort:%
5.34 + Loading the theory \isa{Multiset} makes the \isa{size{\isacharunderscore}change}
5.35 + method a bit stronger: it can then use multiset orders internally.%
5.36 \end{isamarkuptext}%
5.37 \isamarkuptrue%
5.38 %
6.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Nov 23 17:26:32 2009 +0100
6.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Nov 23 17:27:43 2009 +0100
6.3 @@ -452,20 +452,16 @@
6.4
6.5 \end{description}
6.6
6.7 - %FIXME check
6.8 -
6.9 Recursive definitions introduced by the @{command (HOL) "function"}
6.10 command accommodate
6.11 reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text
6.12 "c.induct"} (where @{text c} is the name of the function definition)
6.13 refers to a specific induction rule, with parameters named according
6.14 - to the user-specified equations.
6.15 - For the @{command (HOL) "primrec"} the induction principle coincides
6.16 + to the user-specified equations. Cases are numbered (starting from 1).
6.17 +
6.18 + For @{command (HOL) "primrec"}, the induction principle coincides
6.19 with structural recursion on the datatype the recursion is carried
6.20 out.
6.21 - Case names of @{command (HOL)
6.22 - "primrec"} are that of the datatypes involved, while those of
6.23 - @{command (HOL) "function"} are numbered (starting from 1).
6.24
6.25 The equations provided by these packages may be referred later as
6.26 theorem list @{text "f.simps"}, where @{text f} is the (collective)
6.27 @@ -510,6 +506,7 @@
6.28 @{method_def (HOL) pat_completeness} & : & @{text method} \\
6.29 @{method_def (HOL) relation} & : & @{text method} \\
6.30 @{method_def (HOL) lexicographic_order} & : & @{text method} \\
6.31 + @{method_def (HOL) size_change} & : & @{text method} \\
6.32 \end{matharray}
6.33
6.34 \begin{rail}
6.35 @@ -517,6 +514,9 @@
6.36 ;
6.37 'lexicographic\_order' ( clasimpmod * )
6.38 ;
6.39 + 'size\_change' ( orders ( clasimpmod * ) )
6.40 + ;
6.41 + orders: ( 'max' | 'min' | 'ms' ) *
6.42 \end{rail}
6.43
6.44 \begin{description}
6.45 @@ -544,6 +544,18 @@
6.46 In case of failure, extensive information is printed, which can help
6.47 to analyse the situation (cf.\ \cite{isabelle-function}).
6.48
6.49 + \item @{method (HOL) "size_change"} also works on termination goals,
6.50 + using a variation of the size-change principle, together with a
6.51 + graph decomposition technique (see \cite{krauss_phd} for details).
6.52 + Three kinds of orders are used internally: @{text max}, @{text min},
6.53 + and @{text ms} (multiset), which is only available when the theory
6.54 + @{text Multiset} is loaded. When no order kinds are given, they are
6.55 + tried in order. The search for a termination proof uses SAT solving
6.56 + internally.
6.57 +
6.58 + For local descent proofs, the same context modifiers as for @{method
6.59 + auto} are accepted, see \secref{sec:clasimp}.
6.60 +
6.61 \end{description}
6.62 *}
6.63
7.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 23 17:26:32 2009 +0100
7.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 23 17:27:43 2009 +0100
7.3 @@ -457,18 +457,15 @@
7.4
7.5 \end{description}
7.6
7.7 - %FIXME check
7.8 -
7.9 Recursive definitions introduced by the \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}}
7.10 command accommodate
7.11 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)
7.12 refers to a specific induction rule, with parameters named according
7.13 - to the user-specified equations.
7.14 - For the \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} the induction principle coincides
7.15 + to the user-specified equations. Cases are numbered (starting from 1).
7.16 +
7.17 + For \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}}, the induction principle coincides
7.18 with structural recursion on the datatype the recursion is carried
7.19 out.
7.20 - Case names of \hyperlink{command.HOL.primrec}{\mbox{\isa{\isacommand{primrec}}}} are that of the datatypes involved, while those of
7.21 - \hyperlink{command.HOL.function}{\mbox{\isa{\isacommand{function}}}} are numbered (starting from 1).
7.22
7.23 The equations provided by these packages may be referred later as
7.24 theorem list \isa{{\isachardoublequote}f{\isachardot}simps{\isachardoublequote}}, where \isa{f} is the (collective)
7.25 @@ -515,6 +512,7 @@
7.26 \indexdef{HOL}{method}{pat\_completeness}\hypertarget{method.HOL.pat-completeness}{\hyperlink{method.HOL.pat-completeness}{\mbox{\isa{pat{\isacharunderscore}completeness}}}} & : & \isa{method} \\
7.27 \indexdef{HOL}{method}{relation}\hypertarget{method.HOL.relation}{\hyperlink{method.HOL.relation}{\mbox{\isa{relation}}}} & : & \isa{method} \\
7.28 \indexdef{HOL}{method}{lexicographic\_order}\hypertarget{method.HOL.lexicographic-order}{\hyperlink{method.HOL.lexicographic-order}{\mbox{\isa{lexicographic{\isacharunderscore}order}}}} & : & \isa{method} \\
7.29 + \indexdef{HOL}{method}{size\_change}\hypertarget{method.HOL.size-change}{\hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}}} & : & \isa{method} \\
7.30 \end{matharray}
7.31
7.32 \begin{rail}
7.33 @@ -522,6 +520,9 @@
7.34 ;
7.35 'lexicographic\_order' ( clasimpmod * )
7.36 ;
7.37 + 'size\_change' ( orders ( clasimpmod * ) )
7.38 + ;
7.39 + orders: ( 'max' | 'min' | 'ms' ) *
7.40 \end{rail}
7.41
7.42 \begin{description}
7.43 @@ -549,6 +550,17 @@
7.44 In case of failure, extensive information is printed, which can help
7.45 to analyse the situation (cf.\ \cite{isabelle-function}).
7.46
7.47 + \item \hyperlink{method.HOL.size-change}{\mbox{\isa{size{\isacharunderscore}change}}} also works on termination goals,
7.48 + using a variation of the size-change principle, together with a
7.49 + graph decomposition technique (see \cite{krauss_phd} for details).
7.50 + Three kinds of orders are used internally: \isa{max}, \isa{min},
7.51 + and \isa{ms} (multiset), which is only available when the theory
7.52 + \isa{Multiset} is loaded. When no order kinds are given, they are
7.53 + tried in order. The search for a termination proof uses SAT solving
7.54 + internally.
7.55 +
7.56 + For local descent proofs, the same context modifiers as for \hyperlink{method.auto}{\mbox{\isa{auto}}} are accepted, see \secref{sec:clasimp}.
7.57 +
7.58 \end{description}%
7.59 \end{isamarkuptext}%
7.60 \isamarkuptrue%
8.1 --- a/doc-src/manual.bib Mon Nov 23 17:26:32 2009 +0100
8.2 +++ b/doc-src/manual.bib Mon Nov 23 17:27:43 2009 +0100
8.3 @@ -660,6 +660,14 @@
8.4 crossref = {ijcar2006},
8.5 pages = {589--603}}
8.6
8.7 +@PhdThesis{krauss_phd,
8.8 + author = {Alexander Krauss},
8.9 + title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
8.10 + school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
8.11 + year = {2009},
8.12 + address = {Germany}
8.13 +}
8.14 +
8.15 @manual{isabelle-function,
8.16 author = {Alexander Krauss},
8.17 title = {Defining Recursive Functions in {Isabelle/HOL}},
9.1 --- a/src/HOL/Tools/Function/decompose.ML Mon Nov 23 17:26:32 2009 +0100
9.2 +++ b/src/HOL/Tools/Function/decompose.ML Mon Nov 23 17:27:43 2009 +0100
9.3 @@ -74,7 +74,7 @@
9.4 | _ => no_tac)
9.5 | _ => no_tac)
9.6
9.7 -fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
9.8 +fun decompose_tac' cont err_cont D = Termination.CALLS (fn (cs, i) =>
9.9 let
9.10 val G = mk_dgraph D cs
9.11 val sccs = TermGraph.strong_conn G
9.12 @@ -94,12 +94,7 @@
9.13
9.14 fun decompose_tac ctxt chain_tac cont err_cont =
9.15 derive_chains ctxt chain_tac
9.16 - (decompose_tac' ctxt cont err_cont)
9.17 -
9.18 -fun auto_decompose_tac ctxt =
9.19 - Termination.TERMINATION ctxt
9.20 - (decompose_tac ctxt (auto_tac (clasimpset_of ctxt))
9.21 - (K (K all_tac)) (K (K no_tac)))
9.22 + (decompose_tac' cont err_cont)
9.23
9.24
9.25 end
10.1 --- a/src/HOL/Tools/Function/fun.ML Mon Nov 23 17:26:32 2009 +0100
10.2 +++ b/src/HOL/Tools/Function/fun.ML Mon Nov 23 17:27:43 2009 +0100
10.3 @@ -44,7 +44,7 @@
10.4 ())
10.5 end
10.6
10.7 - val (fname, qs, gs, args, rhs) = split_def ctxt geq
10.8 + val (_, qs, gs, args, _) = split_def ctxt geq
10.9
10.10 val _ = if not (null gs) then err "Conditional equations" else ()
10.11 val _ = map check_constr_pattern args
11.1 --- a/src/HOL/Tools/Function/function_core.ML Mon Nov 23 17:26:32 2009 +0100
11.2 +++ b/src/HOL/Tools/Function/function_core.ML Mon Nov 23 17:27:43 2009 +0100
11.3 @@ -97,8 +97,6 @@
11.4
11.5
11.6 (* Theory dependencies. *)
11.7 -val Pair_inject = @{thm Product_Type.Pair_inject};
11.8 -
11.9 val acc_induct_rule = @{thm accp_induct_rule};
11.10
11.11 val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence};
11.12 @@ -199,7 +197,7 @@
11.13
11.14 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
11.15 let
11.16 - val Globals {h, fvar, x, ...} = globals
11.17 + val Globals {h, ...} = globals
11.18
11.19 val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
11.20 val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
11.21 @@ -298,7 +296,7 @@
11.22 (* Generates the replacement lemma in fully quantified form. *)
11.23 fun mk_replacement_lemma thy h ih_elim clause =
11.24 let
11.25 - val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
11.26 + val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
11.27 local open Conv in
11.28 val ih_conv = arg1_conv o arg_conv o arg_conv
11.29 end
11.30 @@ -321,7 +319,7 @@
11.31 end
11.32
11.33
11.34 -fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj =
11.35 +fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj =
11.36 let
11.37 val Globals {h, y, x, fvar, ...} = globals
11.38 val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei
11.39 @@ -355,10 +353,10 @@
11.40
11.41
11.42
11.43 -fun mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
11.44 +fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
11.45 let
11.46 val Globals {x, y, ranT, fvar, ...} = globals
11.47 - val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
11.48 + val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei
11.49 val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs
11.50
11.51 val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
11.52 @@ -372,7 +370,7 @@
11.53 val P = cterm_of thy (mk_eq (y, rhsC))
11.54 val G_lhs_y = assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y)))
11.55
11.56 - val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas
11.57 + val unique_clauses = map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
11.58
11.59 val uniqueness = G_cases
11.60 |> forall_elim (cterm_of thy lhs)
11.61 @@ -430,7 +428,7 @@
11.62
11.63 val _ = trace_msg (K "Proving cases for unique existence...")
11.64 val (ex1s, values) =
11.65 - split_list (map (mk_uniqueness_case ctxt thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
11.66 + split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
11.67
11.68 val _ = trace_msg (K "Proving: Graph is a function")
11.69 val graph_is_function = complete
11.70 @@ -523,7 +521,7 @@
11.71 ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
11.72 end
11.73
11.74 -fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
11.75 +fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
11.76 let
11.77 val RT = domT --> domT --> boolT
11.78 val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
11.79 @@ -700,8 +698,6 @@
11.80 |> implies_intr D_dcl
11.81 |> implies_intr D_subset
11.82
11.83 - val subset_induct_all = fold_rev (forall_intr o cterm_of thy) [P, a, D] subset_induct_rule
11.84 -
11.85 val simple_induct_rule =
11.86 subset_induct_rule
11.87 |> forall_intr (cterm_of thy D)
11.88 @@ -724,7 +720,7 @@
11.89 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
11.90 let
11.91 val thy = ProofContext.theory_of ctxt
11.92 - val ClauseInfo {cdata = ClauseContext {qs, gs, lhs, rhs, cqs, ...},
11.93 + val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
11.94 qglr = (oqs, _, _, _), ...} = clause
11.95 val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
11.96 |> fold_rev (curry Logic.mk_implies) gs
11.97 @@ -748,8 +744,8 @@
11.98
11.99 fun mk_nest_term_case thy globals R' ihyp clause =
11.100 let
11.101 - val Globals {x, z, ...} = globals
11.102 - val ClauseInfo {cdata = ClauseContext {qs,cqs,ags,lhs,rhs,case_hyp,...},tree,
11.103 + val Globals {z, ...} = globals
11.104 + val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...},tree,
11.105 qglr=(oqs, _, _, _), ...} = clause
11.106
11.107 val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp
11.108 @@ -868,7 +864,7 @@
11.109
11.110 fun mk_trsimp clause psimp =
11.111 let
11.112 - val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, qs, gs, lhs, rhs, ...}, ...} = clause
11.113 + val ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {ctxt, cqs, gs, lhs, rhs, ...}, ...} = clause
11.114 val thy = ProofContext.theory_of ctxt
11.115 val rhs_f = Pattern.rewrite_term thy [(fvar, f)] [] rhs
11.116
11.117 @@ -925,7 +921,7 @@
11.118 val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
11.119
11.120 val ((R, RIntro_thmss, R_elim), lthy) =
11.121 - PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
11.122 + PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
11.123
11.124 val (_, lthy) =
11.125 Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
12.1 --- a/src/HOL/Tools/Function/function_lib.ML Mon Nov 23 17:26:32 2009 +0100
12.2 +++ b/src/HOL/Tools/Function/function_lib.ML Mon Nov 23 17:27:43 2009 +0100
12.3 @@ -14,9 +14,6 @@
12.4 fun fold_option f NONE y = y
12.5 | fold_option f (SOME x) y = f x y;
12.6
12.7 -fun fold_map_option f NONE y = (NONE, y)
12.8 - | fold_map_option f (SOME x) y = apfst SOME (f x y);
12.9 -
12.10 (* Ex: "The variable" ^ plural " is" "s are" vs *)
12.11 fun plural sg pl [x] = sg
12.12 | plural sg pl _ = pl
12.13 @@ -53,7 +50,7 @@
12.14
12.15
12.16 (* FIXME: similar to Variable.focus *)
12.17 -fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
12.18 +fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (n,T,b)) =
12.19 let
12.20 val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
12.21 val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
13.1 --- a/src/HOL/Tools/Function/induction_schema.ML Mon Nov 23 17:26:32 2009 +0100
13.2 +++ b/src/HOL/Tools/Function/induction_schema.ML Mon Nov 23 17:27:43 2009 +0100
13.3 @@ -75,7 +75,7 @@
13.4 let
13.5 fun mk_branch concl =
13.6 let
13.7 - val (ctxt', ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
13.8 + val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl
13.9 val (P, xs) = strip_comb Pxs
13.10 in
13.11 SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs }
13.12 @@ -103,7 +103,7 @@
13.13
13.14 fun mk_rcinfo pr =
13.15 let
13.16 - val (ctxt'', Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
13.17 + val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr
13.18 val (P', rcs) = strip_comb Phyp
13.19 in
13.20 (bidx P', Gvs, Gas, rcs)
13.21 @@ -151,7 +151,7 @@
13.22 |> mk_forall_rename ("P", Pbool)
13.23 end
13.24
13.25 -fun mk_wf ctxt R (IndScheme {T, ...}) =
13.26 +fun mk_wf R (IndScheme {T, ...}) =
13.27 HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
13.28
13.29 fun mk_ineqs R (IndScheme {T, cases, branches}) =
13.30 @@ -198,8 +198,6 @@
13.31 end
13.32
13.33
13.34 -fun mk_hol_imp a b = HOLogic.imp $ a $ b
13.35 -
13.36 fun mk_ind_goal thy branches =
13.37 let
13.38 fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
13.39 @@ -256,7 +254,7 @@
13.40 val (relevant_cases, ineqss') = filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) (scases_idx ~~ ineqss)
13.41 |> split_list
13.42
13.43 - fun prove_case (cidx, SchemeCase {qs, oqnames, gs, lhs, rs, ...}) ineq_press =
13.44 + fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press =
13.45 let
13.46 val case_hyps = map (assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
13.47
13.48 @@ -364,7 +362,7 @@
13.49 val ineqss = mk_ineqs R scheme
13.50 |> map (map (pairself (assume o cert)))
13.51 val complete = map_range (mk_completeness ctxt scheme #> cert #> assume) (length branches)
13.52 - val wf_thm = mk_wf ctxt R scheme |> cert |> assume
13.53 + val wf_thm = mk_wf R scheme |> cert |> assume
13.54
13.55 val (descent, pres) = split_list (flat ineqss)
13.56 val newgoals = complete @ pres @ wf_thm :: descent
14.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML Mon Nov 23 17:26:32 2009 +0100
14.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon Nov 23 17:27:43 2009 +0100
14.3 @@ -75,10 +75,6 @@
14.4 fold_rev Logic.all vars (Logic.list_implies (prems, concl))
14.5 end
14.6
14.7 -fun prove thy solve_tac t =
14.8 - cterm_of thy t |> Goal.init
14.9 - |> SINGLE solve_tac |> the
14.10 -
14.11 fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
14.12 let
14.13 val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
14.14 @@ -137,8 +133,6 @@
14.15
14.16 (** Error reporting **)
14.17
14.18 -fun pr_table table = writeln (cat_lines (map (fn r => implode (map pr_cell r)) table))
14.19 -
14.20 fun pr_goals ctxt st =
14.21 Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
14.22 |> Pretty.chunks
14.23 @@ -190,7 +184,7 @@
14.24 fun lex_order_tac quiet ctxt solve_tac (st: thm) =
14.25 let
14.26 val thy = ProofContext.theory_of ctxt
14.27 - val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
14.28 + val ((_ $ (_ $ rel)) :: tl) = prems_of st
14.29
14.30 val (domT, _) = HOLogic.dest_prodT (HOLogic.dest_setT (fastype_of rel))
14.31
15.1 --- a/src/HOL/Tools/Function/mutual.ML Mon Nov 23 17:26:32 2009 +0100
15.2 +++ b/src/HOL/Tools/Function/mutual.ML Mon Nov 23 17:27:43 2009 +0100
15.3 @@ -28,8 +28,6 @@
15.4
15.5 type qgar = string * (string * typ) list * term list * term list * term
15.6
15.7 -fun name_of_fqgar ((f, _, _, _, _): qgar) = f
15.8 -
15.9 datatype mutual_part =
15.10 MutualPart of
15.11 {
15.12 @@ -82,7 +80,6 @@
15.13 fun analyze_eqs ctxt defname fs eqs =
15.14 let
15.15 val num = length fs
15.16 - val fnames = map fst fs
15.17 val fqgars = map (split_def ctxt) eqs
15.18 val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
15.19 |> AList.lookup (op =) #> the
15.20 @@ -108,7 +105,7 @@
15.21 val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
15.22 val fsum_var = (fsum_var_name, fsum_type)
15.23
15.24 - fun define (fvar as (n, T)) caTs resultT i =
15.25 + fun define (fvar as (n, _)) caTs resultT i =
15.26 let
15.27 val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
15.28 val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
15.29 @@ -170,8 +167,8 @@
15.30 val thy = ProofContext.theory_of ctxt
15.31
15.32 val oqnames = map fst pre_qs
15.33 - val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
15.34 - |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
15.35 + val (qs, _) = Variable.variant_fixes oqnames ctxt
15.36 + |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
15.37
15.38 fun inst t = subst_bounds (rev qs, t)
15.39 val gs = map inst pre_gs
15.40 @@ -192,7 +189,7 @@
15.41
15.42 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq =
15.43 let
15.44 - val (MutualPart {f=SOME f, f_defthm=SOME f_def, ...}) = get_part fname parts
15.45 + val (MutualPart {f=SOME f, ...}) = get_part fname parts
15.46
15.47 val psimp = import sum_psimp_eq
15.48 val (simp, restore_cond) = case cprems_of psimp of
15.49 @@ -223,7 +220,7 @@
15.50 end
15.51
15.52
15.53 -fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, RST, parts, ...}) =
15.54 +fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, parts, ...}) =
15.55 let
15.56 val cert = cterm_of (ProofContext.theory_of lthy)
15.57 val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} =>
15.58 @@ -266,8 +263,8 @@
15.59 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
15.60 let
15.61 val result = inner_cont proof
15.62 - val FunctionResult {fs=[f], G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
15.63 - termination,domintros} = result
15.64 + val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
15.65 + termination, domintros, ...} = result
15.66
15.67 val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
15.68 (mk_applied_form lthy cargTs (symmetric f_def), f))
16.1 --- a/src/HOL/Tools/Function/pattern_split.ML Mon Nov 23 17:26:32 2009 +0100
16.2 +++ b/src/HOL/Tools/Function/pattern_split.ML Mon Nov 23 17:27:43 2009 +0100
16.3 @@ -50,9 +50,6 @@
16.4 fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
16.5 fun join_product (xs, ys) = map_product (curry join) xs ys
16.6
16.7 -fun join_list [] = []
16.8 - | join_list xs = foldr1 (join_product) xs
16.9 -
16.10
16.11 exception DISJ
16.12
17.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Nov 23 17:26:32 2009 +0100
17.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Nov 23 17:27:43 2009 +0100
17.3 @@ -73,7 +73,7 @@
17.4
17.5 val multiset_setup = Multiset_Setup.put o SOME
17.6
17.7 -fun undef x = error "undef"
17.8 +fun undef _ = error "undef"
17.9 fun get_multiset_setup thy = Multiset_Setup.get thy
17.10 |> the_default (Multiset
17.11 { msetT = undef, mk_mset=undef,
17.12 @@ -153,14 +153,13 @@
17.13
17.14 (* Reconstruction *)
17.15
17.16 -fun reconstruct_tac ctxt D cs (gp as GP (_, gs)) certificate =
17.17 +fun reconstruct_tac ctxt D cs (GP (_, gs)) certificate =
17.18 let
17.19 val thy = ProofContext.theory_of ctxt
17.20 val Multiset
17.21 { msetT, mk_mset,
17.22 - mset_regroup_conv, mset_member_tac,
17.23 - mset_nonempty_tac, mset_pwleq_tac, set_of_simps,
17.24 - smsI', wmsI2'', wmsI1, reduction_pair=ms_rp }
17.25 + mset_regroup_conv, mset_pwleq_tac, set_of_simps,
17.26 + smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...}
17.27 = get_multiset_setup thy
17.28
17.29 fun measure_fn p = nth (Termination.get_measures D p)
17.30 @@ -179,7 +178,7 @@
17.31
17.32 fun prove_lev strict g =
17.33 let
17.34 - val G (p, q, el) = nth gs g
17.35 + val G (p, q, _) = nth gs g
17.36
17.37 fun less_proof strict (j, b) (i, a) =
17.38 let
17.39 @@ -307,11 +306,10 @@
17.40 | print_cell (SOME (False _)) = "-"
17.41 | print_cell (NONE) = "?"
17.42
17.43 -fun print_error ctxt D = CALLS (fn (cs, i) =>
17.44 +fun print_error ctxt D = CALLS (fn (cs, _) =>
17.45 let
17.46 val np = get_num_points D
17.47 val ms = map_range (get_measures D) np
17.48 - val tys = map_range (get_types D) np
17.49 fun index xs = (1 upto length xs) ~~ xs
17.50 fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
17.51 val ims = index (map index ms)
18.1 --- a/src/HOL/Tools/Function/scnp_solve.ML Mon Nov 23 17:26:32 2009 +0100
18.2 +++ b/src/HOL/Tools/Function/scnp_solve.ML Mon Nov 23 17:27:43 2009 +0100
18.3 @@ -76,7 +76,7 @@
18.4 Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
18.5
18.6 (* "Virtual constructors" for various propositional variables *)
18.7 -fun var_constrs (gp as GP (arities, gl)) =
18.8 +fun var_constrs (gp as GP (arities, _)) =
18.9 let
18.10 val n = Int.max (num_graphs gp, num_prog_pts gp)
18.11 val k = fold Integer.max arities 1
19.1 --- a/src/HOL/Tools/Function/termination.ML Mon Nov 23 17:26:32 2009 +0100
19.2 +++ b/src/HOL/Tools/Function/termination.ML Mon Nov 23 17:27:43 2009 +0100
19.3 @@ -148,7 +148,7 @@
19.4 val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
19.5 fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
19.6 let
19.7 - val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
19.8 + val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _)
19.9 = Term.strip_qnt_body "Ex" c
19.10 in cons r o cons l end
19.11 in
19.12 @@ -181,7 +181,6 @@
19.13
19.14 fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
19.15 let
19.16 - val n = get_num_points D
19.17 val (sk, _, _, _, _) = D
19.18 val vs = Term.strip_qnt_vars "Ex" c
19.19
19.20 @@ -196,7 +195,7 @@
19.21 | dest_call D t = error "dest_call"
19.22
19.23
19.24 -fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D =
19.25 +fun derive_desc_aux thy tac c (vs, _, l', _, r', Gam) m1 m2 D =
19.26 case get_descent D c m1 m2 of
19.27 SOME _ => D
19.28 | NONE => let
19.29 @@ -225,7 +224,7 @@
19.30
19.31 (* all descents in one go *)
19.32 fun derive_descents thy tac c D =
19.33 - let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c
19.34 + let val cdesc as (_, p, _, q, _, _) = dest_call D c
19.35 in fold_product (derive_desc_aux thy tac c cdesc)
19.36 (get_measures D p) (get_measures D q) D
19.37 end
19.38 @@ -280,7 +279,7 @@
19.39 let
19.40 val thy = ProofContext.theory_of ctxt
19.41 val cert = cterm_of (theory_of_thm st)
19.42 - val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
19.43 + val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
19.44
19.45 fun mk_compr ineq =
19.46 let