src/HOL/Tools/refute.ML
changeset 46096 a00685a18e55
parent 45896 100fb1f33e3e
child 46098 ce939621a1fe
     1.1 --- a/src/HOL/Tools/refute.ML	Tue Jan 03 18:33:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -204,6 +204,15 @@
     1.4      wellformed: prop_formula
     1.5    };
     1.6  
     1.7 +val default_parameters =
     1.8 + [("itself", "1"),
     1.9 +  ("minsize", "1"),
    1.10 +  ("maxsize", "8"),
    1.11 +  ("maxvars", "10000"),
    1.12 +  ("maxtime", "60"),
    1.13 +  ("satsolver", "auto"),
    1.14 +  ("no_assms", "false")]
    1.15 + |> Symtab.make
    1.16  
    1.17  structure Data = Theory_Data
    1.18  (
    1.19 @@ -213,7 +222,8 @@
    1.20       printers: (string * (Proof.context -> model -> typ -> interpretation ->
    1.21        (int -> bool) -> term option)) list,
    1.22       parameters: string Symtab.table};
    1.23 -  val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
    1.24 +  val empty =
    1.25 +    {interpreters = [], printers = [], parameters = default_parameters};
    1.26    val extend = I;
    1.27    fun merge
    1.28      ({interpreters = in1, printers = pr1, parameters = pa1},
    1.29 @@ -417,7 +427,7 @@
    1.30  (*                    denotes membership to an axiomatic type class          *)
    1.31  (* ------------------------------------------------------------------------- *)
    1.32  
    1.33 -fun is_const_of_class thy (s, T) =
    1.34 +fun is_const_of_class thy (s, _) =
    1.35    let
    1.36      val class_const_names = map Logic.const_of_class (Sign.all_classes thy)
    1.37    in
    1.38 @@ -446,7 +456,7 @@
    1.39  (*                  operator of an inductive datatype in 'thy'               *)
    1.40  (* ------------------------------------------------------------------------- *)
    1.41  
    1.42 -fun is_IDT_recursor thy (s, T) =
    1.43 +fun is_IDT_recursor thy (s, _) =
    1.44    let
    1.45      val rec_names = Symtab.fold (append o #rec_names o snd)
    1.46        (Datatype.get_all thy) []
    1.47 @@ -625,7 +635,7 @@
    1.48            (* unfold the constant if there is a defining equation *)
    1.49            else
    1.50              case get_def thy (s, T) of
    1.51 -              SOME (axname, rhs) =>
    1.52 +              SOME ((*axname*) _, rhs) =>
    1.53                (* Note: if the term to be unfolded (i.e. 'Const (s, T)')  *)
    1.54                (* occurs on the right-hand side of the equation, i.e. in  *)
    1.55                (* 'rhs', we must not use this equation to unfold, because *)
    1.56 @@ -721,7 +731,7 @@
    1.57        | Type ("itself", [T1]) => collect_type_axioms T1 axs
    1.58        | Type (s, Ts) =>
    1.59          (case Datatype.get_info thy s of
    1.60 -          SOME info =>  (* inductive datatype *)
    1.61 +          SOME _ =>  (* inductive datatype *)
    1.62              (* only collect relevant type axioms for the argument types *)
    1.63              fold collect_type_axioms Ts axs
    1.64          | NONE =>
    1.65 @@ -972,7 +982,7 @@
    1.66      (* enumerates all int lists with a fixed length, where 0<=x<='max' for *)
    1.67      (* all list elements x (unless 'max'<0)                                *)
    1.68      (* int -> int -> int -> int list -> int list option *)
    1.69 -    fun next max len sum [] =
    1.70 +    fun next _ _ _ [] =
    1.71            NONE
    1.72        | next max len sum [x] =
    1.73            (* we've reached the last list element, so there's no shift possible *)
    1.74 @@ -1243,7 +1253,7 @@
    1.75            strip_all_vars t
    1.76        | strip_all_vars (Const (@{const_name All}, _) $ Abs (a, T, t)) =
    1.77            (a, T) :: strip_all_vars t
    1.78 -      | strip_all_vars t = [] : (string * typ) list
    1.79 +      | strip_all_vars _ = [] : (string * typ) list
    1.80      val strip_t = strip_all_body ex_closure
    1.81      val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)
    1.82      val subst_t = Term.subst_bounds (map Free frees, strip_t)
    1.83 @@ -1470,10 +1480,6 @@
    1.84              prop_formula_list_dot_product_interpretation_list (fms,trees))
    1.85        | prop_formula_list_dot_product_interpretation_list (_,_) =
    1.86            raise REFUTE ("interpretation_apply", "empty list (in dot product)")
    1.87 -    (* concatenates 'x' with every list in 'xss', returning a new list of *)
    1.88 -    (* lists                                                              *)
    1.89 -    (* 'a -> 'a list list -> 'a list list *)
    1.90 -    fun cons_list x xss = map (cons x) xss
    1.91      (* returns a list of lists, each one consisting of one element from each *)
    1.92      (* element of 'xss'                                                      *)
    1.93      (* 'a list list -> 'a list list *)
    1.94 @@ -1535,7 +1541,6 @@
    1.95  
    1.96  fun stlc_interpreter ctxt model args t =
    1.97    let
    1.98 -    val thy = Proof_Context.theory_of ctxt
    1.99      val (typs, terms) = model
   1.100      val {maxvars, def_eq, next_idx, bounds, wellformed} = args
   1.101      (* Term.typ -> (interpretation * model * arguments) option *)
   1.102 @@ -1616,7 +1621,7 @@
   1.103          | Free (_, T) => interpret_groundterm T
   1.104          | Var (_, T) => interpret_groundterm T
   1.105          | Bound i => SOME (nth (#bounds args) i, model, args)
   1.106 -        | Abs (x, T, body) =>
   1.107 +        | Abs (_, T, body) =>
   1.108              let
   1.109                (* create all constants of type 'T' *)
   1.110                val constants = make_constants ctxt model T
   1.111 @@ -1679,7 +1684,7 @@
   1.112          SOME ((if #def_eq args then make_def_equality else make_equality)
   1.113            (i1, i2), m2, a2)
   1.114        end
   1.115 -  | Const (@{const_name "=="}, _) $ t1 =>
   1.116 +  | Const (@{const_name "=="}, _) $ _ =>
   1.117        SOME (interpret ctxt model args (eta_expand t 1))
   1.118    | Const (@{const_name "=="}, _) =>
   1.119        SOME (interpret ctxt model args (eta_expand t 2))
   1.120 @@ -1693,7 +1698,7 @@
   1.121        in
   1.122          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.123        end
   1.124 -  | Const (@{const_name "==>"}, _) $ t1 =>
   1.125 +  | Const (@{const_name "==>"}, _) $ _ =>
   1.126        SOME (interpret ctxt model args (eta_expand t 1))
   1.127    | Const (@{const_name "==>"}, _) =>
   1.128        SOME (interpret ctxt model args (eta_expand t 2))
   1.129 @@ -1759,7 +1764,7 @@
   1.130        in
   1.131          SOME (make_equality (i1, i2), m2, a2)
   1.132        end
   1.133 -  | Const (@{const_name HOL.eq}, _) $ t1 =>
   1.134 +  | Const (@{const_name HOL.eq}, _) $ _ =>
   1.135        SOME (interpret ctxt model args (eta_expand t 1))
   1.136    | Const (@{const_name HOL.eq}, _) =>
   1.137        SOME (interpret ctxt model args (eta_expand t 2))
   1.138 @@ -1773,7 +1778,7 @@
   1.139        in
   1.140          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.141        end
   1.142 -  | Const (@{const_name HOL.conj}, _) $ t1 =>
   1.143 +  | Const (@{const_name HOL.conj}, _) $ _ =>
   1.144        SOME (interpret ctxt model args (eta_expand t 1))
   1.145    | Const (@{const_name HOL.conj}, _) =>
   1.146        SOME (interpret ctxt model args (eta_expand t 2))
   1.147 @@ -1790,7 +1795,7 @@
   1.148        in
   1.149          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.150        end
   1.151 -  | Const (@{const_name HOL.disj}, _) $ t1 =>
   1.152 +  | Const (@{const_name HOL.disj}, _) $ _ =>
   1.153        SOME (interpret ctxt model args (eta_expand t 1))
   1.154    | Const (@{const_name HOL.disj}, _) =>
   1.155        SOME (interpret ctxt model args (eta_expand t 2))
   1.156 @@ -1807,7 +1812,7 @@
   1.157        in
   1.158          SOME (Leaf [fmTrue, fmFalse], m2, a2)
   1.159        end
   1.160 -  | Const (@{const_name HOL.implies}, _) $ t1 =>
   1.161 +  | Const (@{const_name HOL.implies}, _) $ _ =>
   1.162        SOME (interpret ctxt model args (eta_expand t 1))
   1.163    | Const (@{const_name HOL.implies}, _) =>
   1.164        SOME (interpret ctxt model args (eta_expand t 2))
   1.165 @@ -2053,7 +2058,7 @@
   1.166                          [] =>
   1.167                            (* 'Const (s, T)' is not a constructor of this datatype *)
   1.168                            NONE
   1.169 -                      | (_, ctypes)::cs =>
   1.170 +                      | (_, ctypes)::_ =>
   1.171                            let
   1.172                              (* int option -- only /recursive/ IDTs have an associated *)
   1.173                              (*               depth                                    *)
   1.174 @@ -2144,7 +2149,7 @@
   1.175                                        let
   1.176                                          fun search (x::xs) (y::ys) =
   1.177                                                if x = y then search xs ys else search (x::xs) ys
   1.178 -                                          | search (x::xs) [] =
   1.179 +                                          | search (_::_) [] =
   1.180                                                raise REFUTE ("IDT_constructor_interpreter",
   1.181                                                  "element order not preserved")
   1.182                                            | search [] _ = ()
   1.183 @@ -2471,7 +2476,7 @@
   1.184                                  | rec_intr (Datatype.DtRec _) (Node _) =
   1.185                                      raise REFUTE ("IDT_recursion_interpreter",
   1.186                                        "interpretation for IDT is a node")
   1.187 -                                | rec_intr (Datatype.DtType ("fun", [dt1, dt2])) (Node xs) =
   1.188 +                                | rec_intr (Datatype.DtType ("fun", [_, dt2])) (Node xs) =
   1.189                                      (* recursive argument is something like     *)
   1.190                                      (* "\<lambda>x::dt1. rec_? params (elem x)" *)
   1.191                                      Node (map (rec_intr dt2) xs)
   1.192 @@ -2518,7 +2523,7 @@
   1.193  
   1.194  fun set_interpreter ctxt model args t =
   1.195    let
   1.196 -    val (typs, terms) = model
   1.197 +    val (_, terms) = model
   1.198    in
   1.199      case AList.lookup (op =) terms t of
   1.200        SOME intr =>
   1.201 @@ -2534,7 +2539,7 @@
   1.202          (* 'op :' == application *)
   1.203          | Const (@{const_name Set.member}, _) $ t1 $ t2 =>
   1.204              SOME (interpret ctxt model args (t2 $ t1))
   1.205 -        | Const (@{const_name Set.member}, _) $ t1 =>
   1.206 +        | Const (@{const_name Set.member}, _) $ _ =>
   1.207              SOME (interpret ctxt model args (eta_expand t 1))
   1.208          | Const (@{const_name Set.member}, _) =>
   1.209              SOME (interpret ctxt model args (eta_expand t 2))
   1.210 @@ -2592,7 +2597,7 @@
   1.211  fun Finite_Set_finite_interpreter ctxt model args t =
   1.212    case t of
   1.213      Const (@{const_name Finite_Set.finite},
   1.214 -      Type ("fun", [Type ("fun", [T, @{typ bool}]),
   1.215 +      Type ("fun", [Type ("fun", [_, @{typ bool}]),
   1.216                      @{typ bool}])) $ _ =>
   1.217          (* we only consider finite models anyway, hence EVERY set is *)
   1.218          (* "finite"                                                  *)