src/HOL/Tools/refute.ML

     next_idx  : int,
     bounds    : interpretation list,
     wellformed: prop_formula
   };
 
+val default_parameters =
+ [("itself", "1"),
+  ("minsize", "1"),
+  ("maxsize", "8"),
+  ("maxvars", "10000"),
+  ("maxtime", "60"),
+  ("satsolver", "auto"),
+  ("no_assms", "false")]
+ |> Symtab.make
 
 structure Data = Theory_Data
 (
   type T =
     {interpreters: (string * (Proof.context -> model -> arguments -> term ->
       (interpretation * model * arguments) option)) list,
      printers: (string * (Proof.context -> model -> typ -> interpretation ->
       (int -> bool) -> term option)) list,
      parameters: string Symtab.table};
-  val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
+  val empty =
+    {interpreters = [], printers = [], parameters = default_parameters};
   val extend = I;
   fun merge
     ({interpreters = in1, printers = pr1, parameters = pa1},
      {interpreters = in2, printers = pr2, parameters = pa2}) : T =
     {interpreters = AList.merge (op =) (K true) (in1, in2),

 (* ------------------------------------------------------------------------- *)
 (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)
 (*                    denotes membership to an axiomatic type class          *)
 (* ------------------------------------------------------------------------- *)
 
-fun is_const_of_class thy (s, T) =
+fun is_const_of_class thy (s, _) =
   let
     val class_const_names = map Logic.const_of_class (Sign.all_classes thy)
   in
     (* I'm not quite sure if checking the name 's' is sufficient, *)
     (* or if we should also check the type 'T'.                   *)

 (* ------------------------------------------------------------------------- *)
 (* is_IDT_recursor: returns 'true' iff 'Const (s, T)' is the recursion       *)
 (*                  operator of an inductive datatype in 'thy'               *)
 (* ------------------------------------------------------------------------- *)
 
-fun is_IDT_recursor thy (s, T) =
+fun is_IDT_recursor thy (s, _) =
   let
     val rec_names = Symtab.fold (append o #rec_names o snd)
       (Datatype.get_all thy) []
   in
     (* I'm not quite sure if checking the name 's' is sufficient, *)

             orelse is_IDT_recursor thy (s, T) then
             t  (* do not unfold IDT constructors/recursors *)
           (* unfold the constant if there is a defining equation *)
           else
             case get_def thy (s, T) of
-              SOME (axname, rhs) =>
+              SOME ((*axname*) _, rhs) =>
               (* Note: if the term to be unfolded (i.e. 'Const (s, T)')  *)
               (* occurs on the right-hand side of the equation, i.e. in  *)
               (* 'rhs', we must not use this equation to unfold, because *)
               (* that would loop.  Here would be the right place to      *)
               (* check this.  However, getting this really right seems   *)

       | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
       (* axiomatic type classes *)
       | Type ("itself", [T1]) => collect_type_axioms T1 axs
       | Type (s, Ts) =>
         (case Datatype.get_info thy s of
-          SOME info =>  (* inductive datatype *)
+          SOME _ =>  (* inductive datatype *)
             (* only collect relevant type axioms for the argument types *)
             fold collect_type_axioms Ts axs
         | NONE =>
           (case get_typedef thy T of
             SOME (axname, ax) =>

           else
             Option.map (fn xs' => max :: xs') (make_first max (len-1) (sum-max))
     (* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
     (* all list elements x (unless 'max'<0)                                *)
     (* int -> int -> int -> int list -> int list option *)
-    fun next max len sum [] =
+    fun next _ _ _ [] =
           NONE
       | next max len sum [x] =
           (* we've reached the last list element, so there's no shift possible *)
           make_first max (len+1) (sum+x+1)  (* increment 'sum' by 1 *)
       | next max len sum (x1::x2::xs) =

           (a, T) :: strip_all_vars t
       | strip_all_vars (Const (@{const_name Trueprop}, _) $ t) =
           strip_all_vars t
       | strip_all_vars (Const (@{const_name All}, _) $ Abs (a, T, t)) =
           (a, T) :: strip_all_vars t
-      | strip_all_vars t = [] : (string * typ) list
+      | strip_all_vars _ = [] : (string * typ) list
     val strip_t = strip_all_body ex_closure
     val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)
     val subst_t = Term.subst_bounds (map Free frees, strip_t)
   in
     find_model ctxt (actual_params ctxt params) assm_ts subst_t true

       | prop_formula_list_dot_product_interpretation_list (fm::fms,tr::trees) =
           interpretation_disjunction (prop_formula_times_interpretation (fm,tr),
             prop_formula_list_dot_product_interpretation_list (fms,trees))
       | prop_formula_list_dot_product_interpretation_list (_,_) =
           raise REFUTE ("interpretation_apply", "empty list (in dot product)")
-    (* concatenates 'x' with every list in 'xss', returning a new list of *)
-    (* lists                                                              *)
-    (* 'a -> 'a list list -> 'a list list *)
-    fun cons_list x xss = map (cons x) xss
     (* returns a list of lists, each one consisting of one element from each *)
     (* element of 'xss'                                                      *)
     (* 'a list list -> 'a list list *)
     fun pick_all [xs] = map single xs
       | pick_all (xs::xss) =

 (* simply typed lambda calculus: Isabelle's basic term syntax, with type *)
 (* variables, function types, and propT                                  *)
 
 fun stlc_interpreter ctxt model args t =
   let
-    val thy = Proof_Context.theory_of ctxt
     val (typs, terms) = model
     val {maxvars, def_eq, next_idx, bounds, wellformed} = args
     (* Term.typ -> (interpretation * model * arguments) option *)
     fun interpret_groundterm T =
       let

         (case t of
           Const (_, T) => interpret_groundterm T
         | Free (_, T) => interpret_groundterm T
         | Var (_, T) => interpret_groundterm T
         | Bound i => SOME (nth (#bounds args) i, model, args)
-        | Abs (x, T, body) =>
+        | Abs (_, T, body) =>
             let
               (* create all constants of type 'T' *)
               val constants = make_constants ctxt model T
               (* interpret the 'body' separately for each constant *)
               val (bodies, (model', args')) = fold_map

       in
         (* we use either 'make_def_equality' or 'make_equality' *)
         SOME ((if #def_eq args then make_def_equality else make_equality)
           (i1, i2), m2, a2)
       end
-  | Const (@{const_name "=="}, _) $ t1 =>
+  | Const (@{const_name "=="}, _) $ _ =>
       SOME (interpret ctxt model args (eta_expand t 1))
   | Const (@{const_name "=="}, _) =>
       SOME (interpret ctxt model args (eta_expand t 2))
   | Const (@{const_name "==>"}, _) $ t1 $ t2 =>
       (* 3-valued logic *)

         val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
         val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-  | Const (@{const_name "==>"}, _) $ t1 =>
+  | Const (@{const_name "==>"}, _) $ _ =>
       SOME (interpret ctxt model args (eta_expand t 1))
   | Const (@{const_name "==>"}, _) =>
       SOME (interpret ctxt model args (eta_expand t 2))
   | _ => NONE;
 

         val (i1, m1, a1) = interpret ctxt model args t1
         val (i2, m2, a2) = interpret ctxt m1 a1 t2
       in
         SOME (make_equality (i1, i2), m2, a2)
       end
-  | Const (@{const_name HOL.eq}, _) $ t1 =>
+  | Const (@{const_name HOL.eq}, _) $ _ =>
       SOME (interpret ctxt model args (eta_expand t 1))
   | Const (@{const_name HOL.eq}, _) =>
       SOME (interpret ctxt model args (eta_expand t 2))
   | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
       (* 3-valued logic *)

         val fmTrue = Prop_Logic.SAnd (toTrue i1, toTrue i2)
         val fmFalse = Prop_Logic.SOr (toFalse i1, toFalse i2)
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-  | Const (@{const_name HOL.conj}, _) $ t1 =>
+  | Const (@{const_name HOL.conj}, _) $ _ =>
       SOME (interpret ctxt model args (eta_expand t 1))
   | Const (@{const_name HOL.conj}, _) =>
       SOME (interpret ctxt model args (eta_expand t 2))
       (* this would make "undef" propagate, even for formulae like *)
       (* "False & undef":                                          *)

         val fmTrue = Prop_Logic.SOr (toTrue i1, toTrue i2)
         val fmFalse = Prop_Logic.SAnd (toFalse i1, toFalse i2)
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-  | Const (@{const_name HOL.disj}, _) $ t1 =>
+  | Const (@{const_name HOL.disj}, _) $ _ =>
       SOME (interpret ctxt model args (eta_expand t 1))
   | Const (@{const_name HOL.disj}, _) =>
       SOME (interpret ctxt model args (eta_expand t 2))
       (* this would make "undef" propagate, even for formulae like *)
       (* "True | undef":                                           *)

         val fmTrue = Prop_Logic.SOr (toFalse i1, toTrue i2)
         val fmFalse = Prop_Logic.SAnd (toTrue i1, toFalse i2)
       in
         SOME (Leaf [fmTrue, fmFalse], m2, a2)
       end
-  | Const (@{const_name HOL.implies}, _) $ t1 =>
+  | Const (@{const_name HOL.implies}, _) $ _ =>
       SOME (interpret ctxt model args (eta_expand t 1))
   | Const (@{const_name HOL.implies}, _) =>
       SOME (interpret ctxt model args (eta_expand t 2))
       (* this would make "undef" propagate, even for formulae like *)
       (* "False --> undef":                                        *)

                     in
                       case constrs2 of
                         [] =>
                           (* 'Const (s, T)' is not a constructor of this datatype *)
                           NONE
-                      | (_, ctypes)::cs =>
+                      | (_, ctypes)::_ =>
                           let
                             (* int option -- only /recursive/ IDTs have an associated *)
                             (*               depth                                    *)
                             val depth = AList.lookup (op =) typs (Type (s', Ts'))
                             (* this should never happen: at depth 0, this IDT fragment *)

                                     (*               the same in terms, for those elements *)
                                     val _ =
                                       let
                                         fun search (x::xs) (y::ys) =
                                               if x = y then search xs ys else search (x::xs) ys
-                                          | search (x::xs) [] =
+                                          | search (_::_) [] =
                                               raise REFUTE ("IDT_constructor_interpreter",
                                                 "element order not preserved")
                                           | search [] _ = ()
                                       in search terms' terms end
                                     (* int * interpretation list *)

                                     (* recursive argument is "rec_i params elem" *)
                                     compute_array_entry i (find_index (fn x => x = True) xs)
                                 | rec_intr (Datatype.DtRec _) (Node _) =
                                     raise REFUTE ("IDT_recursion_interpreter",
                                       "interpretation for IDT is a node")
-                                | rec_intr (Datatype.DtType ("fun", [dt1, dt2])) (Node xs) =
+                                | rec_intr (Datatype.DtType ("fun", [_, dt2])) (Node xs) =
                                     (* recursive argument is something like     *)
                                     (* "\<lambda>x::dt1. rec_? params (elem x)" *)
                                     Node (map (rec_intr dt2) xs)
                                 | rec_intr (Datatype.DtType ("fun", [_, _])) (Leaf _) =
                                     raise REFUTE ("IDT_recursion_interpreter",

       NONE
   end;
 
 fun set_interpreter ctxt model args t =
   let
-    val (typs, terms) = model
+    val (_, terms) = model
   in
     case AList.lookup (op =) terms t of
       SOME intr =>
         (* return an existing interpretation *)
         SOME (intr, model, args)

         | Const (@{const_name Collect}, _) =>
             SOME (interpret ctxt model args (eta_expand t 1))
         (* 'op :' == application *)
         | Const (@{const_name Set.member}, _) $ t1 $ t2 =>
             SOME (interpret ctxt model args (t2 $ t1))
-        | Const (@{const_name Set.member}, _) $ t1 =>
+        | Const (@{const_name Set.member}, _) $ _ =>
             SOME (interpret ctxt model args (eta_expand t 1))
         | Const (@{const_name Set.member}, _) =>
             SOME (interpret ctxt model args (eta_expand t 2))
         | _ => NONE)
   end;

 (* below is more efficient                                                *)
 
 fun Finite_Set_finite_interpreter ctxt model args t =
   case t of
     Const (@{const_name Finite_Set.finite},
-      Type ("fun", [Type ("fun", [T, @{typ bool}]),
+      Type ("fun", [Type ("fun", [_, @{typ bool}]),
                     @{typ bool}])) $ _ =>
         (* we only consider finite models anyway, hence EVERY set is *)
         (* "finite"                                                  *)
         SOME (TT, model, args)
   | Const (@{const_name Finite_Set.finite},