--- a/Admin/isatest/minimal-test Mon Nov 23 16:15:18 2009 +0100
+++ b/Admin/isatest/minimal-test Mon Nov 23 16:15:39 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/doc-src/Functions/Thy/Functions.thy Mon Nov 23 16:15:18 2009 +0100
+++ b/doc-src/Functions/Thy/Functions.thy Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/doc-src/Functions/Thy/document/Functions.tex Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/doc-src/manual.bib Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/decompose.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_solve.ML Mon Nov 23 16:15:39 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 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Function/termination.ML Mon Nov 23 16:15:39 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
--- a/src/HOL/Tools/Nitpick/HISTORY Mon Nov 23 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Mon Nov 23 16:15:39 2009 +0100
@@ -10,9 +10,11 @@
* Optimized Kodkod encoding of datatypes whose constructors don't appear in
the formula to falsify
* Added support for codatatype view of datatypes
- * Fixed soundness bugs related to sets and sets of sets
+ * Fixed soundness bugs related to sets, sets of sets, and (co)inductive
+ predicates
* Fixed monotonicity check
- * Fixed error when processing definitions that resulted in an exception
+ * Fixed error when processing definitions
+ * Fixed error in "star_linear_preds" optimization
* Fixed error in Kodkod encoding of "The" and "Eps"
* Fixed error in display of uncurried constants
* Speeded up scope enumeration
@@ -70,7 +72,7 @@
* Improved precision of "trancl" and "rtrancl"
* Optimized Kodkod encoding of "tranclp" and "rtranclp"
* Made detection of inconsistent scope specifications more robust
- * Fixed a few Kodkod generation bugs that resulted in exceptions
+ * Fixed a few Kodkod generation bugs
Version 1.1.1 (24 Jun 2009)
@@ -79,8 +81,7 @@
* Improved precision of some set constructs
* Fiddled with the automatic monotonicity check
* Fixed performance issues related to scope enumeration
- * Fixed a few Kodkod generation bugs that resulted in exceptions or stack
- overflows
+ * Fixed a few Kodkod generation bugs
Version 1.1.0 (16 Jun 2009)
@@ -117,7 +118,7 @@
* Fixed soundness issue in handling of non-definitional axioms
* Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
"nat", "int", and "*"
- * Fixed a few Kodkod generation bugs that resulted in exceptions
+ * Fixed a few Kodkod generation bugs
* Optimized "div", "mod", and "dvd" on "nat" and "int"
Version 1.0.2 (12 Mar 2009)
@@ -152,7 +153,7 @@
infinite loop for "Nominal.perm"
* Added support for multiple instantiations of non-well-founded inductive
predicates, which previously raised an exception
- * Fixed a Kodkod generation bug that resulted in an exception
+ * Fixed a Kodkod generation bug
* Altered order of scope enumeration and automatic SAT solver selection
* Optimized "Eps", "nat_case", and "list_case"
* Improved output formatting
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Nov 23 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Nov 23 16:15:39 2009 +0100
@@ -1740,9 +1740,12 @@
| do_lfp_def _ = false
in do_lfp_def o strip_abs_body end
-(* typ -> typ -> term -> term *)
-fun ap_split tuple_T =
- HOLogic.mk_psplits (HOLogic.flat_tupleT_paths tuple_T) tuple_T
+(* int -> int list list *)
+fun n_ptuple_paths 0 = []
+ | n_ptuple_paths 1 = []
+ | n_ptuple_paths n = [] :: map (cons 2) (n_ptuple_paths (n - 1))
+(* int -> typ -> typ -> term -> term *)
+val ap_n_split = HOLogic.mk_psplits o n_ptuple_paths
(* term -> term * term *)
val linear_pred_base_and_step_rhss =
@@ -1776,16 +1779,17 @@
|> List.foldl s_disj @{const False}
in
(list_abs (tl xs, incr_bv (~1, j, base_body))
- |> ap_split tuple_T bool_T,
+ |> ap_n_split (length arg_Ts) tuple_T bool_T,
Abs ("y", tuple_T, list_abs (tl xs, step_body)
- |> ap_split tuple_T bool_T))
+ |> ap_n_split (length arg_Ts) tuple_T bool_T))
end
| aux t =
raise TERM ("Nitpick_HOL.linear_pred_base_and_step_rhss.aux", [t])
in aux end
(* extended_context -> styp -> term -> term *)
-fun closed_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T)) def =
+fun starred_linear_pred_const (ext_ctxt as {simp_table, ...}) (x as (s, T))
+ def =
let
val j = maxidx_of_term def + 1
val (outer, fp_app) = strip_abs def
@@ -1832,7 +1836,7 @@
unrolled_const (* already done *)
else if not gfp andalso is_linear_inductive_pred_def def
andalso star_linear_preds then
- closed_linear_pred_const ext_ctxt x def
+ starred_linear_pred_const ext_ctxt x def
else
let
val j = maxidx_of_term def + 1
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Nov 23 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Nov 23 16:15:39 2009 +0100
@@ -956,7 +956,8 @@
(case u of
Cst (False, _, _) => Kodkod.False
| Cst (True, _, _) => Kodkod.True
- | Op1 (Not, _, _, u1) => kk_not (to_f u1)
+ | Op1 (Not, _, _, u1) =>
+ kk_not (to_f_with_polarity (flip_polarity polar) u1)
| Op1 (Finite, _, _, u1) =>
let val opt1 = is_opt_rep (rep_of u1) in
case polar of
@@ -968,10 +969,14 @@
| Neg => Kodkod.True
end
| Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1
- | Op2 (All, _, _, u1, u2) => kk_all (untuple to_decl u1) (to_f u2)
- | Op2 (Exist, _, _, u1, u2) => kk_exist (untuple to_decl u1) (to_f u2)
- | Op2 (Or, _, _, u1, u2) => kk_or (to_f u1) (to_f u2)
- | Op2 (And, _, _, u1, u2) => kk_and (to_f u1) (to_f u2)
+ | Op2 (All, _, _, u1, u2) =>
+ kk_all (untuple to_decl u1) (to_f_with_polarity polar u2)
+ | Op2 (Exist, _, _, u1, u2) =>
+ kk_exist (untuple to_decl u1) (to_f_with_polarity polar u2)
+ | Op2 (Or, _, _, u1, u2) =>
+ kk_or (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
+ | Op2 (And, _, _, u1, u2) =>
+ kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
| Op2 (Less, T, Formula polar, u1, u2) =>
formula_from_opt_atom polar bool_j0
(to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
@@ -1105,9 +1110,10 @@
to_f_with_polarity polar
(Op2 (Apply, T, Opt (Atom (2, offset_of_type ofs T)), u1, u2)))
| Op3 (Let, _, _, u1, u2, u3) =>
- kk_formula_let [to_expr_assign u1 u2] (to_f u3)
+ kk_formula_let [to_expr_assign u1 u2] (to_f_with_polarity polar u3)
| Op3 (If, _, _, u1, u2, u3) =>
- kk_formula_if (to_f u1) (to_f u2) (to_f u3)
+ kk_formula_if (to_f u1) (to_f_with_polarity polar u2)
+ (to_f_with_polarity polar u3)
| FormulaReg (j, _, _) => Kodkod.FormulaReg j
| _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
| Atom (2, j0) => formula_from_atom j0 (to_r u)
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Nov 23 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Nov 23 16:15:39 2009 +0100
@@ -554,7 +554,8 @@
end
fun do_equals T (gamma, cset) =
let val C = ctype_for (domain_type T) in
- (CFun (C, S Neg, CFun (C, S Neg, ctype_for (nth_range_type 2 T))),
+ (CFun (C, S Neg, CFun (C, V (Unsynchronized.inc max_fresh),
+ ctype_for (nth_range_type 2 T))),
(gamma, cset |> add_ctype_is_right_unique C))
end
fun do_robust_set_operation T (gamma, cset) =
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Nov 23 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Nov 23 16:15:39 2009 +0100
@@ -712,15 +712,16 @@
else if is_rep_fun thy x then
Func oo best_non_opt_symmetric_reps_for_fun_type
else if all_precise orelse is_skolem_name v
- orelse s mem [@{const_name undefined_fast_The},
- @{const_name undefined_fast_Eps},
- @{const_name bisim}] then
+ orelse original_name s
+ mem [@{const_name undefined_fast_The},
+ @{const_name undefined_fast_Eps},
+ @{const_name bisim},
+ @{const_name bisim_iterator_max}] then
best_non_opt_set_rep_for_type
else if original_name s
mem [@{const_name set}, @{const_name distinct},
@{const_name ord_class.less},
- @{const_name ord_class.less_eq},
- @{const_name bisim_iterator_max}] then
+ @{const_name ord_class.less_eq}] then
best_set_rep_for_type
else
best_opt_set_rep_for_type) scope T
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Nov 23 16:15:18 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Nov 23 16:15:39 2009 +0100
@@ -100,8 +100,7 @@
forall (is_precise_type dtypes) Ts
| is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts
| is_precise_type dtypes T =
- T <> nat_T andalso T <> int_T
- andalso #precise (the (datatype_spec dtypes T))
+ not (is_integer_type T) andalso #precise (the (datatype_spec dtypes T))
handle Option.Option => true
fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) =
is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2