# HG changeset patch
# User boehmes
# Date 1258123657 -3600
# Node ID d62805a237ef84dba01d8baba554bf23105d9ed8
# Parent  a84fd63858325afd411622cc2fdd121018aee731
removed unused code and unused arguments,
tuned

diff -r a84fd6385832 -r d62805a237ef src/HOL/SMT/Tools/cvc3_solver.ML
--- 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
diff -r a84fd6385832 -r d62805a237ef src/HOL/SMT/Tools/smt_normalize.ML
--- 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)
diff -r a84fd6385832 -r d62805a237ef src/HOL/SMT/Tools/smt_solver.ML
--- 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
diff -r a84fd6385832 -r d62805a237ef src/HOL/SMT/Tools/smt_translate.ML
--- 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
diff -r a84fd6385832 -r d62805a237ef src/HOL/SMT/Tools/yices_solver.ML
--- 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
diff -r a84fd6385832 -r d62805a237ef src/HOL/SMT/Tools/z3_model.ML
--- 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
 
 
diff -r a84fd6385832 -r d62805a237ef src/HOL/SMT/Tools/z3_proof_rules.ML
--- 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
diff -r a84fd6385832 -r d62805a237ef src/HOL/SMT/Tools/z3_proof_terms.ML
--- 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 =