--- a/src/HOL/Tools/Function/decompose.ML Mon Nov 23 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/decompose.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_solve.ML Mon Nov 23 15:05:59 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 13:45:16 2009 +0100
+++ b/src/HOL/Tools/Function/termination.ML Mon Nov 23 15:05:59 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