--- a/src/HOL/SMT/Tools/cvc3_solver.ML Fri Nov 13 15:11:41 2009 +0100
+++ b/src/HOL/SMT/Tools/cvc3_solver.ML Fri Nov 13 15:47:37 2009 +0100
@@ -23,11 +23,11 @@
fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])
-fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) =
+fun core_oracle ({output, ...} : SMT_Solver.proof_data) =
let
val empty_line = (fn "" => true | _ => false)
val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
- val (l, ls) = split_first (dropwhile empty_line output)
+ val (l, _) = split_first (dropwhile empty_line output)
in
if is_unsat l then @{cprop False}
else if is_sat l then raise_cex true
--- a/src/HOL/SMT/Tools/smt_normalize.ML Fri Nov 13 15:11:41 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_normalize.ML Fri Nov 13 15:47:37 2009 +0100
@@ -285,14 +285,14 @@
fun add_sym t = if AList.defined (op =) defs t then insert (op =) t else I
fun add_syms thms = fold (Term.fold_aterms add_sym o Thm.prop_of) thms []
- fun unfold_conv ctxt ct =
+ fun unfold_conv ct =
(case AList.lookup (op =) defs (Term.head_of (Thm.term_of ct)) of
SOME (_, eq) => Conv.rewr_conv eq
| NONE => Conv.all_conv) ct
in
fun add_abs_min_max_rules ctxt thms =
if Config.get ctxt unfold_defs
- then map (Conv.fconv_rule (More_Conv.bottom_conv unfold_conv ctxt)) thms
+ then map (Conv.fconv_rule (More_Conv.bottom_conv (K unfold_conv) ctxt)) thms
else map fst (map_filter (AList.lookup (op =) defs) (add_syms thms)) @ thms
end
@@ -319,13 +319,12 @@
let
val cvs' = used_vars cvs ct
val ct' = fold_rev Thm.cabs cvs' ct
- val mk_repl = fold (fn ct => fn cu => Thm.capply cu ct) cvs'
in
(case Termtab.lookup defs (Thm.term_of ct') of
SOME (_, eq) => (make_def cvs' eq, cx)
| NONE =>
let
- val {t, T, ...} = Thm.rep_cterm ct'
+ val {T, ...} = Thm.rep_cterm ct'
val (n, nctxt') = fresh_name "" nctxt
val eq = Thm.assume (mk_meta_eq (cert ctxt (Free (n, T))) ct')
in (make_def cvs' eq, (nctxt', add_def ct' eq defs)) end)
@@ -410,8 +409,8 @@
(case Term.strip_comb (Thm.term_of ct) of
(Const (n, _), ts) => app_conv tb (const n) (length ts) ctxt
| (Free (n, _), ts) => app_conv tb (free n) (length ts) ctxt
- | (Abs _, ts) => nary_conv (abs_conv sub_conv tb ctxt) (sub_conv tb ctxt)
- | (_, ts) => nary_conv Conv.all_conv (sub_conv tb ctxt)) ct
+ | (Abs _, _) => nary_conv (abs_conv sub_conv tb ctxt) (sub_conv tb ctxt)
+ | (_, _) => nary_conv Conv.all_conv (sub_conv tb ctxt)) ct
and app_conv tb n i ctxt =
(case Symtab.lookup tb n of
NONE => nary_conv Conv.all_conv (sub_conv tb ctxt)
--- a/src/HOL/SMT/Tools/smt_solver.ML Fri Nov 13 15:11:41 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML Fri Nov 13 15:47:37 2009 +0100
@@ -144,7 +144,7 @@
true)
end
-fun run_locally f ctxt env_var args ps =
+fun run_locally f env_var args ps =
if getenv env_var = ""
then f ("Undefined Isabelle environment variable: " ^ quote env_var)
else
@@ -173,7 +173,7 @@
let val ps = [File.shell_path problem_path, ">", File.shell_path proof_path]
in
if use_certificate ctxt ps then ()
- else run_locally (run_remote remote_name args ps) ctxt env_var args ps
+ else run_locally (run_remote remote_name args ps) env_var args ps
end
in
--- a/src/HOL/SMT/Tools/smt_translate.ML Fri Nov 13 15:11:41 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_translate.ML Fri Nov 13 15:47:37 2009 +0100
@@ -142,7 +142,7 @@
SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
| _ => NONE)
in
-fun bv_rotate mk_name T ts =
+fun bv_rotate mk_name _ ts =
dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
fun bv_extend mk_name T ts =
@@ -196,7 +196,7 @@
fun group_quant qname vs (t as Const (q, _) $ Abs (n, T, u)) =
if q = qname then group_quant qname ((n, T) :: vs) u else (vs, t)
- | group_quant qname vs t = (vs, t)
+ | group_quant _ vs t = (vs, t)
fun dest_trigger (@{term trigger} $ tl $ t) = (HOLogic.dest_list tl, t)
| dest_trigger t = ([], t)
@@ -208,11 +208,11 @@
fun trans Ts t =
(case Term.strip_comb t of
- (t1 as Const (qn, qT), [t2 as Abs (n, T, t3)]) =>
+ (Const (qn, _), [Abs (n, T, t1)]) =>
(case quantifier qn of
SOME q =>
let
- val (vs, u) = group_quant qn [(n, T)] t3
+ val (vs, u) = group_quant qn [(n, T)] t1
val Us = map snd vs @ Ts
val (ps, b) = dest_trigger u
in SQuant (q, rev vs, map (pat (trans Us) []) ps, trans Us b) end
@@ -277,7 +277,7 @@
fun sep loc t =
(case t of
- SVar i => pair t
+ SVar _ => pair t
| SApp (c as SConst (@{const_name If}, _), u :: us) =>
mark sep false u ##>> fold_map (sep loc) us #>> app c o (op ::)
| SApp (c, us) =>
@@ -429,7 +429,7 @@
let val (n, ns') = fresh_typ ns
in (n, (vars, ns', add_typ (T, n) sgn)) end)
- fun rep_var bs (n, T) (vars, ns, sgn) =
+ fun rep_var bs (_, T) (vars, ns, sgn) =
let val (n', vars') = fresh_name vars
in (vars', ns, sgn) |> rep_typ bs T |>> pair n' end
@@ -458,9 +458,9 @@
fun sign loc t =
(case t of
SVar i => pair (SVar i)
- | SApp (c as SConst (@{const_name term}, _), [u]) =>
+ | SApp (SConst (@{const_name term}, _), [u]) =>
sign true u #>> app term_marker o single
- | SApp (c as SConst (@{const_name formula}, _), [u]) =>
+ | SApp (SConst (@{const_name formula}, _), [u]) =>
sign false u #>> app formula_marker o single
| SApp (SConst (c as (_, T)), ts) =>
(case builtin_lookup (builtin_fun loc) thy c ts of
--- a/src/HOL/SMT/Tools/yices_solver.ML Fri Nov 13 15:11:41 2009 +0100
+++ b/src/HOL/SMT/Tools/yices_solver.ML Fri Nov 13 15:47:37 2009 +0100
@@ -19,11 +19,11 @@
fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])
-fun core_oracle ({context, output, recon, ...} : SMT_Solver.proof_data) =
+fun core_oracle ({output, ...} : SMT_Solver.proof_data) =
let
val empty_line = (fn "" => true | _ => false)
val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
- val (l, ls) = split_first (dropwhile empty_line output)
+ val (l, _) = split_first (dropwhile empty_line output)
in
if String.isPrefix "unsat" l then @{cprop False}
else if String.isPrefix "sat" l then raise_cex true
--- a/src/HOL/SMT/Tools/z3_model.ML Fri Nov 13 15:11:41 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_model.ML Fri Nov 13 15:47:37 2009 +0100
@@ -130,7 +130,8 @@
in
(case (can HOLogic.dest_number t, cs) of
(true, [c]) => trans 0 T c #>> (fn (_, u) => [mk_eq u ([], t)])
- | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t))
+ | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t)
+ | _ => raise TERM ("translate: no cases", [t]))
end
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML Fri Nov 13 15:11:41 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML Fri Nov 13 15:47:37 2009 +0100
@@ -222,7 +222,6 @@
and dest_disj3 = precompose (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
and dest_disj4 = precompose (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
- val is_neg = (fn @{term Not} $ _ => true | _ => false)
fun dest_disj_rules t =
(case dest_disj_term' is_neg t of
SOME (true, true) => SOME (dest_disj2, dest_disj4)
@@ -458,7 +457,7 @@
let val cv = mk_var ctxt idx (#T (Thm.rep_cterm ct))
in (cv, (ctxt, mk_var, idx + 1, gen, Ctermtab.update (ct, cv) tab)) end)
-fun prove_abstraction tac ct (ctxt, _, _, gen, tab) =
+fun prove_abstraction tac ct (_, _, _, gen, tab) =
let
val insts = map swap (Ctermtab.dest tab)
val thm = Goal.prove_internal [] ct (fn _ => tac 1)
@@ -1096,11 +1095,14 @@
val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
+ fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
+ | dest_binop t = raise TERM ("dest_binop", [t])
- fun prove_antisym_le ss ((le as Const(_, T)) $ r $ s) =
+ fun prove_antisym_le ss t =
let
+ val (le, r, s) = dest_binop t
+ val less = Const (@{const_name less}, Term.fastype_of le)
val prems = Simplifier.prems_of_ss ss
- val less = Const (@{const_name less}, T)
in
(case find_first (eq_prop (le $ s $ r)) prems of
NONE =>
@@ -1110,16 +1112,17 @@
end
handle THM _ => NONE
- fun prove_antisym_less ss (_ $ ((less as Const(_,T)) $ r $ s)) =
+ fun prove_antisym_less ss t =
let
+ val (less, r, s) = dest_binop (HOLogic.dest_not t)
+ val le = Const (@{const_name less_eq}, Term.fastype_of less)
val prems = prems_of_ss ss
- val le = Const (@{const_name less_eq}, T)
in
(case find_first (eq_prop (le $ r $ s)) prems of
NONE =>
find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
|> Option.map (fn thm => thm RS antisym_less2)
- | SOME thm => SOME (thm RS antisym_le2))
+ | SOME thm => SOME (thm RS antisym_le2))
end
handle THM _ => NONE
in
@@ -1249,7 +1252,7 @@
Tactic.rtac iffI_rule THEN_ALL_NEW arith_tac ctxt
ORELSE' arith_tac ctxt
- val simp_tac = CHANGED o Simplifier.simp_tac z3_simpset
+ fun simp_tac thms = CHANGED o Simplifier.simp_tac (z3_simpset addsimps thms)
ORELSE' Classical.best_tac HOL_cs
in
fun rewrite ctxt thms ct =
@@ -1261,7 +1264,7 @@
("distinct", distinct),
("arith", by_tac' (arith_eq_tac ctxt)),
("classical", by_tac' (Classical.best_tac HOL_cs)),
- ("simp", by_tac' simp_tac),
+ ("simp", by_tac' (simp_tac thms)),
("full arith", by_tac' (Arith_Data.arith_tac ctxt))] (T.mk_prop ct))
end
end
--- a/src/HOL/SMT/Tools/z3_proof_terms.ML Fri Nov 13 15:11:41 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_terms.ML Fri Nov 13 15:47:37 2009 +0100
@@ -132,7 +132,7 @@
in mk_preterm (ct, [(i, ct)]) end
local
-fun mk_quant q thy (n, T) e =
+fun mk_quant q thy (_, T) e =
let
val (ct, vs) = dest_preterm e
val cv =