src/HOL/Tools/refute.ML
changeset 34120 f9920a3ddf50
parent 34017 ef2776c89799
child 34974 18b41bba42b5
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Dec 14 11:01:04 2009 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Dec 14 12:14:12 2009 +0100
     1.3 @@ -45,13 +45,16 @@
     1.4    val get_default_params : theory -> (string * string) list
     1.5    val actual_params      : theory -> (string * string) list -> params
     1.6  
     1.7 -  val find_model : theory -> params -> term -> bool -> unit
     1.8 +  val find_model : theory -> params -> term list -> term -> bool -> unit
     1.9  
    1.10    (* tries to find a model for a formula: *)
    1.11 -  val satisfy_term   : theory -> (string * string) list -> term -> unit
    1.12 +  val satisfy_term :
    1.13 +    theory -> (string * string) list -> term list -> term -> unit
    1.14    (* tries to find a model that refutes a formula: *)
    1.15 -  val refute_term : theory -> (string * string) list -> term -> unit
    1.16 -  val refute_goal : theory -> (string * string) list -> thm -> int -> unit
    1.17 +  val refute_term :
    1.18 +    theory -> (string * string) list -> term list -> term -> unit
    1.19 +  val refute_goal :
    1.20 +    Proof.context -> (string * string) list -> thm -> int -> unit
    1.21  
    1.22    val setup : theory -> theory
    1.23  
    1.24 @@ -153,8 +156,10 @@
    1.25  (*                       formula.                                            *)
    1.26  (* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
    1.27  (* "satsolver"   string  SAT solver to be used.                              *)
    1.28 +(* "no_assms"    bool    If "true", assumptions in structured proofs are     *)
    1.29 +(*                       not considered.                                     *)
    1.30  (* "expect"      string  Expected result ("genuine", "potential", "none", or *)
    1.31 -(*                       "unknown")                                          *)
    1.32 +(*                       "unknown").                                         *)
    1.33  (* ------------------------------------------------------------------------- *)
    1.34  
    1.35    type params =
    1.36 @@ -165,6 +170,7 @@
    1.37        maxvars  : int,
    1.38        maxtime  : int,
    1.39        satsolver: string,
    1.40 +      no_assms : bool,
    1.41        expect   : string
    1.42      };
    1.43  
    1.44 @@ -360,6 +366,15 @@
    1.45  
    1.46    fun actual_params thy override =
    1.47    let
    1.48 +    (* (string * string) list * string -> bool *)
    1.49 +    fun read_bool (parms, name) =
    1.50 +      case AList.lookup (op =) parms name of
    1.51 +        SOME "true" => true
    1.52 +      | SOME "false" => false
    1.53 +      | SOME s => error ("parameter " ^ quote name ^
    1.54 +        " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")
    1.55 +      | NONE   => error ("parameter " ^ quote name ^
    1.56 +          " must be assigned a value")
    1.57      (* (string * string) list * string -> int *)
    1.58      fun read_int (parms, name) =
    1.59        case AList.lookup (op =) parms name of
    1.60 @@ -385,6 +400,7 @@
    1.61      val maxtime   = read_int (allparams, "maxtime")
    1.62      (* string *)
    1.63      val satsolver = read_string (allparams, "satsolver")
    1.64 +    val no_assms = read_bool (allparams, "no_assms")
    1.65      val expect = the_default "" (AList.lookup (op =) allparams "expect")
    1.66      (* all remaining parameters of the form "string=int" are collected in *)
    1.67      (* 'sizes'                                                            *)
    1.68 @@ -395,10 +411,10 @@
    1.69        (fn (name, value) => Option.map (pair name) (Int.fromString value))
    1.70        (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
    1.71          andalso name<>"maxvars" andalso name<>"maxtime"
    1.72 -        andalso name<>"satsolver") allparams)
    1.73 +        andalso name<>"satsolver" andalso name<>"no_assms") allparams)
    1.74    in
    1.75      {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,
    1.76 -      maxtime=maxtime, satsolver=satsolver, expect=expect}
    1.77 +      maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect}
    1.78    end;
    1.79  
    1.80  
    1.81 @@ -1118,6 +1134,7 @@
    1.82  (*             the model to the user by calling 'print_model'                *)
    1.83  (* thy       : the current theory                                            *)
    1.84  (* {...}     : parameters that control the translation/model generation      *)
    1.85 +(* assm_ts   : assumptions to be considered unless "no_assms" is specified   *)
    1.86  (* t         : term to be translated into a propositional formula            *)
    1.87  (* negate    : if true, find a model that makes 't' false (rather than true) *)
    1.88  (* ------------------------------------------------------------------------- *)
    1.89 @@ -1125,7 +1142,7 @@
    1.90    (* theory -> params -> Term.term -> bool -> unit *)
    1.91  
    1.92    fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver,
    1.93 -    expect} t negate =
    1.94 +    no_assms, expect} assm_ts t negate =
    1.95    let
    1.96      (* string -> unit *)
    1.97      fun check_expect outcome_code =
    1.98 @@ -1135,6 +1152,9 @@
    1.99      fun wrapper () =
   1.100      let
   1.101        val timer  = Timer.startRealTimer ()
   1.102 +      val t = if no_assms then t
   1.103 +              else if negate then Logic.list_implies (assm_ts, t)
   1.104 +              else Logic.mk_conjunction_list (t :: assm_ts)
   1.105        val u      = unfold_defs thy t
   1.106        val _      = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
   1.107        val axioms = collect_axioms thy u
   1.108 @@ -1270,10 +1290,10 @@
   1.109  (*               parameters                                                  *)
   1.110  (* ------------------------------------------------------------------------- *)
   1.111  
   1.112 -  (* theory -> (string * string) list -> Term.term -> unit *)
   1.113 +  (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
   1.114  
   1.115 -  fun satisfy_term thy params t =
   1.116 -    find_model thy (actual_params thy params) t false;
   1.117 +  fun satisfy_term thy params assm_ts t =
   1.118 +    find_model thy (actual_params thy params) assm_ts t false;
   1.119  
   1.120  (* ------------------------------------------------------------------------- *)
   1.121  (* refute_term: calls 'find_model' to find a model that refutes 't'          *)
   1.122 @@ -1281,9 +1301,9 @@
   1.123  (*              parameters                                                   *)
   1.124  (* ------------------------------------------------------------------------- *)
   1.125  
   1.126 -  (* theory -> (string * string) list -> Term.term -> unit *)
   1.127 +  (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
   1.128  
   1.129 -  fun refute_term thy params t =
   1.130 +  fun refute_term thy params assm_ts t =
   1.131    let
   1.132      (* disallow schematic type variables, since we cannot properly negate  *)
   1.133      (* terms containing them (their logical meaning is that there EXISTS a *)
   1.134 @@ -1332,15 +1352,29 @@
   1.135      val frees   = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)
   1.136      val subst_t = Term.subst_bounds (map Free frees, strip_t)
   1.137    in
   1.138 -    find_model thy (actual_params thy params) subst_t true
   1.139 +    find_model thy (actual_params thy params) assm_ts subst_t true
   1.140 +    handle REFUTE (s, s') => error ("REFUTE " ^ s ^ " " ^ s') (* ### *)
   1.141    end;
   1.142  
   1.143  (* ------------------------------------------------------------------------- *)
   1.144  (* refute_goal                                                               *)
   1.145  (* ------------------------------------------------------------------------- *)
   1.146  
   1.147 -  fun refute_goal thy params st i =
   1.148 -    refute_term thy params (Logic.get_goal (Thm.prop_of st) i);
   1.149 +  fun refute_goal ctxt params th i =
   1.150 +  let
   1.151 +    val t = th |> prop_of
   1.152 +  in
   1.153 +    if Logic.count_prems t = 0 then
   1.154 +      priority "No subgoal!"
   1.155 +    else
   1.156 +      let
   1.157 +        val assms = map term_of (Assumption.all_assms_of ctxt)
   1.158 +        val (t, frees) = Logic.goal_params t i
   1.159 +      in
   1.160 +        refute_term (ProofContext.theory_of ctxt) params assms
   1.161 +        (subst_bounds (frees, t))
   1.162 +      end
   1.163 +  end
   1.164  
   1.165  
   1.166  (* ------------------------------------------------------------------------- *)