added "no_assms" option to Refute, and include structured proof assumptions by default;
authorblanchet
Mon Dec 14 12:14:12 2009 +0100 (2009-12-14)
changeset 34120f9920a3ddf50
parent 34086 ff8b2ac0134c
child 34121 5e831d805118
added "no_assms" option to Refute, and include structured proof assumptions by default;
will do the same for Quickcheck unless there are objections
src/HOL/Refute.thy
src/HOL/SAT.thy
src/HOL/Tools/refute.ML
src/HOL/Tools/refute_isar.ML
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/Refute.thy	Mon Dec 14 11:01:04 2009 +0100
     1.2 +++ b/src/HOL/Refute.thy	Mon Dec 14 12:14:12 2009 +0100
     1.3 @@ -61,7 +61,8 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  (* PARAMETERS                                                                *)
     1.6  (*                                                                           *)
     1.7 -(* The following global parameters are currently supported (and required):   *)
     1.8 +(* The following global parameters are currently supported (and required,    *)
     1.9 +(* except for "expect"):                                                     *)
    1.10  (*                                                                           *)
    1.11  (* Name          Type    Description                                         *)
    1.12  (*                                                                           *)
    1.13 @@ -75,6 +76,10 @@
    1.14  (* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
    1.15  (*                       This value is ignored under some ML compilers.      *)
    1.16  (* "satsolver"   string  Name of the SAT solver to be used.                  *)
    1.17 +(* "no_assms"    bool    If "true", assumptions in structured proofs are     *)
    1.18 +(*                       not considered.                                     *)
    1.19 +(* "expect"      string  Expected result ("genuine", "potential", "none", or *)
    1.20 +(*                       "unknown").                                         *)
    1.21  (*                                                                           *)
    1.22  (* See 'HOL/SAT.thy' for default values.                                     *)
    1.23  (*                                                                           *)
     2.1 --- a/src/HOL/SAT.thy	Mon Dec 14 11:01:04 2009 +0100
     2.2 +++ b/src/HOL/SAT.thy	Mon Dec 14 12:14:12 2009 +0100
     2.3 @@ -23,7 +23,8 @@
     2.4    maxsize=8,
     2.5    maxvars=10000,
     2.6    maxtime=60,
     2.7 -  satsolver="auto"]
     2.8 +  satsolver="auto",
     2.9 +  no_assms="false"]
    2.10  
    2.11  ML {* structure sat = SATFunc(cnf) *}
    2.12  
     3.1 --- a/src/HOL/Tools/refute.ML	Mon Dec 14 11:01:04 2009 +0100
     3.2 +++ b/src/HOL/Tools/refute.ML	Mon Dec 14 12:14:12 2009 +0100
     3.3 @@ -45,13 +45,16 @@
     3.4    val get_default_params : theory -> (string * string) list
     3.5    val actual_params      : theory -> (string * string) list -> params
     3.6  
     3.7 -  val find_model : theory -> params -> term -> bool -> unit
     3.8 +  val find_model : theory -> params -> term list -> term -> bool -> unit
     3.9  
    3.10    (* tries to find a model for a formula: *)
    3.11 -  val satisfy_term   : theory -> (string * string) list -> term -> unit
    3.12 +  val satisfy_term :
    3.13 +    theory -> (string * string) list -> term list -> term -> unit
    3.14    (* tries to find a model that refutes a formula: *)
    3.15 -  val refute_term : theory -> (string * string) list -> term -> unit
    3.16 -  val refute_goal : theory -> (string * string) list -> thm -> int -> unit
    3.17 +  val refute_term :
    3.18 +    theory -> (string * string) list -> term list -> term -> unit
    3.19 +  val refute_goal :
    3.20 +    Proof.context -> (string * string) list -> thm -> int -> unit
    3.21  
    3.22    val setup : theory -> theory
    3.23  
    3.24 @@ -153,8 +156,10 @@
    3.25  (*                       formula.                                            *)
    3.26  (* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
    3.27  (* "satsolver"   string  SAT solver to be used.                              *)
    3.28 +(* "no_assms"    bool    If "true", assumptions in structured proofs are     *)
    3.29 +(*                       not considered.                                     *)
    3.30  (* "expect"      string  Expected result ("genuine", "potential", "none", or *)
    3.31 -(*                       "unknown")                                          *)
    3.32 +(*                       "unknown").                                         *)
    3.33  (* ------------------------------------------------------------------------- *)
    3.34  
    3.35    type params =
    3.36 @@ -165,6 +170,7 @@
    3.37        maxvars  : int,
    3.38        maxtime  : int,
    3.39        satsolver: string,
    3.40 +      no_assms : bool,
    3.41        expect   : string
    3.42      };
    3.43  
    3.44 @@ -360,6 +366,15 @@
    3.45  
    3.46    fun actual_params thy override =
    3.47    let
    3.48 +    (* (string * string) list * string -> bool *)
    3.49 +    fun read_bool (parms, name) =
    3.50 +      case AList.lookup (op =) parms name of
    3.51 +        SOME "true" => true
    3.52 +      | SOME "false" => false
    3.53 +      | SOME s => error ("parameter " ^ quote name ^
    3.54 +        " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")
    3.55 +      | NONE   => error ("parameter " ^ quote name ^
    3.56 +          " must be assigned a value")
    3.57      (* (string * string) list * string -> int *)
    3.58      fun read_int (parms, name) =
    3.59        case AList.lookup (op =) parms name of
    3.60 @@ -385,6 +400,7 @@
    3.61      val maxtime   = read_int (allparams, "maxtime")
    3.62      (* string *)
    3.63      val satsolver = read_string (allparams, "satsolver")
    3.64 +    val no_assms = read_bool (allparams, "no_assms")
    3.65      val expect = the_default "" (AList.lookup (op =) allparams "expect")
    3.66      (* all remaining parameters of the form "string=int" are collected in *)
    3.67      (* 'sizes'                                                            *)
    3.68 @@ -395,10 +411,10 @@
    3.69        (fn (name, value) => Option.map (pair name) (Int.fromString value))
    3.70        (filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
    3.71          andalso name<>"maxvars" andalso name<>"maxtime"
    3.72 -        andalso name<>"satsolver") allparams)
    3.73 +        andalso name<>"satsolver" andalso name<>"no_assms") allparams)
    3.74    in
    3.75      {sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,
    3.76 -      maxtime=maxtime, satsolver=satsolver, expect=expect}
    3.77 +      maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect}
    3.78    end;
    3.79  
    3.80  
    3.81 @@ -1118,6 +1134,7 @@
    3.82  (*             the model to the user by calling 'print_model'                *)
    3.83  (* thy       : the current theory                                            *)
    3.84  (* {...}     : parameters that control the translation/model generation      *)
    3.85 +(* assm_ts   : assumptions to be considered unless "no_assms" is specified   *)
    3.86  (* t         : term to be translated into a propositional formula            *)
    3.87  (* negate    : if true, find a model that makes 't' false (rather than true) *)
    3.88  (* ------------------------------------------------------------------------- *)
    3.89 @@ -1125,7 +1142,7 @@
    3.90    (* theory -> params -> Term.term -> bool -> unit *)
    3.91  
    3.92    fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver,
    3.93 -    expect} t negate =
    3.94 +    no_assms, expect} assm_ts t negate =
    3.95    let
    3.96      (* string -> unit *)
    3.97      fun check_expect outcome_code =
    3.98 @@ -1135,6 +1152,9 @@
    3.99      fun wrapper () =
   3.100      let
   3.101        val timer  = Timer.startRealTimer ()
   3.102 +      val t = if no_assms then t
   3.103 +              else if negate then Logic.list_implies (assm_ts, t)
   3.104 +              else Logic.mk_conjunction_list (t :: assm_ts)
   3.105        val u      = unfold_defs thy t
   3.106        val _      = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
   3.107        val axioms = collect_axioms thy u
   3.108 @@ -1270,10 +1290,10 @@
   3.109  (*               parameters                                                  *)
   3.110  (* ------------------------------------------------------------------------- *)
   3.111  
   3.112 -  (* theory -> (string * string) list -> Term.term -> unit *)
   3.113 +  (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
   3.114  
   3.115 -  fun satisfy_term thy params t =
   3.116 -    find_model thy (actual_params thy params) t false;
   3.117 +  fun satisfy_term thy params assm_ts t =
   3.118 +    find_model thy (actual_params thy params) assm_ts t false;
   3.119  
   3.120  (* ------------------------------------------------------------------------- *)
   3.121  (* refute_term: calls 'find_model' to find a model that refutes 't'          *)
   3.122 @@ -1281,9 +1301,9 @@
   3.123  (*              parameters                                                   *)
   3.124  (* ------------------------------------------------------------------------- *)
   3.125  
   3.126 -  (* theory -> (string * string) list -> Term.term -> unit *)
   3.127 +  (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
   3.128  
   3.129 -  fun refute_term thy params t =
   3.130 +  fun refute_term thy params assm_ts t =
   3.131    let
   3.132      (* disallow schematic type variables, since we cannot properly negate  *)
   3.133      (* terms containing them (their logical meaning is that there EXISTS a *)
   3.134 @@ -1332,15 +1352,29 @@
   3.135      val frees   = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)
   3.136      val subst_t = Term.subst_bounds (map Free frees, strip_t)
   3.137    in
   3.138 -    find_model thy (actual_params thy params) subst_t true
   3.139 +    find_model thy (actual_params thy params) assm_ts subst_t true
   3.140 +    handle REFUTE (s, s') => error ("REFUTE " ^ s ^ " " ^ s') (* ### *)
   3.141    end;
   3.142  
   3.143  (* ------------------------------------------------------------------------- *)
   3.144  (* refute_goal                                                               *)
   3.145  (* ------------------------------------------------------------------------- *)
   3.146  
   3.147 -  fun refute_goal thy params st i =
   3.148 -    refute_term thy params (Logic.get_goal (Thm.prop_of st) i);
   3.149 +  fun refute_goal ctxt params th i =
   3.150 +  let
   3.151 +    val t = th |> prop_of
   3.152 +  in
   3.153 +    if Logic.count_prems t = 0 then
   3.154 +      priority "No subgoal!"
   3.155 +    else
   3.156 +      let
   3.157 +        val assms = map term_of (Assumption.all_assms_of ctxt)
   3.158 +        val (t, frees) = Logic.goal_params t i
   3.159 +      in
   3.160 +        refute_term (ProofContext.theory_of ctxt) params assms
   3.161 +        (subst_bounds (frees, t))
   3.162 +      end
   3.163 +  end
   3.164  
   3.165  
   3.166  (* ------------------------------------------------------------------------- *)
     4.1 --- a/src/HOL/Tools/refute_isar.ML	Mon Dec 14 11:01:04 2009 +0100
     4.2 +++ b/src/HOL/Tools/refute_isar.ML	Mon Dec 14 12:14:12 2009 +0100
     4.3 @@ -12,8 +12,9 @@
     4.4  
     4.5  (*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
     4.6  
     4.7 -val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
     4.8 -
     4.9 +val scan_parm =
    4.10 +  OuterParse.name
    4.11 +  -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true")
    4.12  val scan_parms = Scan.optional
    4.13    (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
    4.14  
    4.15 @@ -27,9 +28,9 @@
    4.16        (fn (parms, i) =>
    4.17          Toplevel.keep (fn state =>
    4.18            let
    4.19 -            val thy = Toplevel.theory_of state;
    4.20 +            val ctxt = Toplevel.context_of state;
    4.21              val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
    4.22 -          in Refute.refute_goal thy parms st i end)));
    4.23 +          in Refute.refute_goal ctxt parms st i end)));
    4.24  
    4.25  
    4.26  (* 'refute_params' command *)
     5.1 --- a/src/HOL/ex/Refute_Examples.thy	Mon Dec 14 11:01:04 2009 +0100
     5.2 +++ b/src/HOL/ex/Refute_Examples.thy	Mon Dec 14 12:14:12 2009 +0100
     5.3 @@ -1516,6 +1516,17 @@
     5.4    refute
     5.5  oops
     5.6  
     5.7 +text {* Structured proofs *}
     5.8 +
     5.9 +lemma "x = y"
    5.10 +proof cases
    5.11 +  assume "x = y"
    5.12 +  show ?thesis
    5.13 +  refute
    5.14 +  refute [no_assms]
    5.15 +  refute [no_assms = false]
    5.16 +oops
    5.17 +
    5.18  refute_params [satsolver="auto"]
    5.19  
    5.20  end