added "no_assms" option to Refute, and include structured proof assumptions by default;
will do the same for Quickcheck unless there are objections
--- a/src/HOL/Refute.thy Mon Dec 14 11:01:04 2009 +0100
+++ b/src/HOL/Refute.thy Mon Dec 14 12:14:12 2009 +0100
@@ -61,7 +61,8 @@
(* ------------------------------------------------------------------------- *)
(* PARAMETERS *)
(* *)
-(* The following global parameters are currently supported (and required): *)
+(* The following global parameters are currently supported (and required, *)
+(* except for "expect"): *)
(* *)
(* Name Type Description *)
(* *)
@@ -75,6 +76,10 @@
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *)
(* This value is ignored under some ML compilers. *)
(* "satsolver" string Name of the SAT solver to be used. *)
+(* "no_assms" bool If "true", assumptions in structured proofs are *)
+(* not considered. *)
+(* "expect" string Expected result ("genuine", "potential", "none", or *)
+(* "unknown"). *)
(* *)
(* See 'HOL/SAT.thy' for default values. *)
(* *)
--- a/src/HOL/SAT.thy Mon Dec 14 11:01:04 2009 +0100
+++ b/src/HOL/SAT.thy Mon Dec 14 12:14:12 2009 +0100
@@ -23,7 +23,8 @@
maxsize=8,
maxvars=10000,
maxtime=60,
- satsolver="auto"]
+ satsolver="auto",
+ no_assms="false"]
ML {* structure sat = SATFunc(cnf) *}
--- a/src/HOL/Tools/refute.ML Mon Dec 14 11:01:04 2009 +0100
+++ b/src/HOL/Tools/refute.ML Mon Dec 14 12:14:12 2009 +0100
@@ -45,13 +45,16 @@
val get_default_params : theory -> (string * string) list
val actual_params : theory -> (string * string) list -> params
- val find_model : theory -> params -> term -> bool -> unit
+ val find_model : theory -> params -> term list -> term -> bool -> unit
(* tries to find a model for a formula: *)
- val satisfy_term : theory -> (string * string) list -> term -> unit
+ val satisfy_term :
+ theory -> (string * string) list -> term list -> term -> unit
(* tries to find a model that refutes a formula: *)
- val refute_term : theory -> (string * string) list -> term -> unit
- val refute_goal : theory -> (string * string) list -> thm -> int -> unit
+ val refute_term :
+ theory -> (string * string) list -> term list -> term -> unit
+ val refute_goal :
+ Proof.context -> (string * string) list -> thm -> int -> unit
val setup : theory -> theory
@@ -153,8 +156,10 @@
(* formula. *)
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *)
(* "satsolver" string SAT solver to be used. *)
+(* "no_assms" bool If "true", assumptions in structured proofs are *)
+(* not considered. *)
(* "expect" string Expected result ("genuine", "potential", "none", or *)
-(* "unknown") *)
+(* "unknown"). *)
(* ------------------------------------------------------------------------- *)
type params =
@@ -165,6 +170,7 @@
maxvars : int,
maxtime : int,
satsolver: string,
+ no_assms : bool,
expect : string
};
@@ -360,6 +366,15 @@
fun actual_params thy override =
let
+ (* (string * string) list * string -> bool *)
+ fun read_bool (parms, name) =
+ case AList.lookup (op =) parms name of
+ SOME "true" => true
+ | SOME "false" => false
+ | SOME s => error ("parameter " ^ quote name ^
+ " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")
+ | NONE => error ("parameter " ^ quote name ^
+ " must be assigned a value")
(* (string * string) list * string -> int *)
fun read_int (parms, name) =
case AList.lookup (op =) parms name of
@@ -385,6 +400,7 @@
val maxtime = read_int (allparams, "maxtime")
(* string *)
val satsolver = read_string (allparams, "satsolver")
+ val no_assms = read_bool (allparams, "no_assms")
val expect = the_default "" (AList.lookup (op =) allparams "expect")
(* all remaining parameters of the form "string=int" are collected in *)
(* 'sizes' *)
@@ -395,10 +411,10 @@
(fn (name, value) => Option.map (pair name) (Int.fromString value))
(filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
andalso name<>"maxvars" andalso name<>"maxtime"
- andalso name<>"satsolver") allparams)
+ andalso name<>"satsolver" andalso name<>"no_assms") allparams)
in
{sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,
- maxtime=maxtime, satsolver=satsolver, expect=expect}
+ maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect}
end;
@@ -1118,6 +1134,7 @@
(* the model to the user by calling 'print_model' *)
(* thy : the current theory *)
(* {...} : parameters that control the translation/model generation *)
+(* assm_ts : assumptions to be considered unless "no_assms" is specified *)
(* t : term to be translated into a propositional formula *)
(* negate : if true, find a model that makes 't' false (rather than true) *)
(* ------------------------------------------------------------------------- *)
@@ -1125,7 +1142,7 @@
(* theory -> params -> Term.term -> bool -> unit *)
fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver,
- expect} t negate =
+ no_assms, expect} assm_ts t negate =
let
(* string -> unit *)
fun check_expect outcome_code =
@@ -1135,6 +1152,9 @@
fun wrapper () =
let
val timer = Timer.startRealTimer ()
+ val t = if no_assms then t
+ else if negate then Logic.list_implies (assm_ts, t)
+ else Logic.mk_conjunction_list (t :: assm_ts)
val u = unfold_defs thy t
val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
val axioms = collect_axioms thy u
@@ -1270,10 +1290,10 @@
(* parameters *)
(* ------------------------------------------------------------------------- *)
- (* theory -> (string * string) list -> Term.term -> unit *)
+ (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
- fun satisfy_term thy params t =
- find_model thy (actual_params thy params) t false;
+ fun satisfy_term thy params assm_ts t =
+ find_model thy (actual_params thy params) assm_ts t false;
(* ------------------------------------------------------------------------- *)
(* refute_term: calls 'find_model' to find a model that refutes 't' *)
@@ -1281,9 +1301,9 @@
(* parameters *)
(* ------------------------------------------------------------------------- *)
- (* theory -> (string * string) list -> Term.term -> unit *)
+ (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
- fun refute_term thy params t =
+ fun refute_term thy params assm_ts t =
let
(* disallow schematic type variables, since we cannot properly negate *)
(* terms containing them (their logical meaning is that there EXISTS a *)
@@ -1332,15 +1352,29 @@
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 thy (actual_params thy params) subst_t true
+ find_model thy (actual_params thy params) assm_ts subst_t true
+ handle REFUTE (s, s') => error ("REFUTE " ^ s ^ " " ^ s') (* ### *)
end;
(* ------------------------------------------------------------------------- *)
(* refute_goal *)
(* ------------------------------------------------------------------------- *)
- fun refute_goal thy params st i =
- refute_term thy params (Logic.get_goal (Thm.prop_of st) i);
+ fun refute_goal ctxt params th i =
+ let
+ val t = th |> prop_of
+ in
+ if Logic.count_prems t = 0 then
+ priority "No subgoal!"
+ else
+ let
+ val assms = map term_of (Assumption.all_assms_of ctxt)
+ val (t, frees) = Logic.goal_params t i
+ in
+ refute_term (ProofContext.theory_of ctxt) params assms
+ (subst_bounds (frees, t))
+ end
+ end
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/refute_isar.ML Mon Dec 14 11:01:04 2009 +0100
+++ b/src/HOL/Tools/refute_isar.ML Mon Dec 14 12:14:12 2009 +0100
@@ -12,8 +12,9 @@
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
-val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
-
+val scan_parm =
+ OuterParse.name
+ -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true")
val scan_parms = Scan.optional
(OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
@@ -27,9 +28,9 @@
(fn (parms, i) =>
Toplevel.keep (fn state =>
let
- val thy = Toplevel.theory_of state;
+ val ctxt = Toplevel.context_of state;
val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
- in Refute.refute_goal thy parms st i end)));
+ in Refute.refute_goal ctxt parms st i end)));
(* 'refute_params' command *)
--- a/src/HOL/ex/Refute_Examples.thy Mon Dec 14 11:01:04 2009 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Mon Dec 14 12:14:12 2009 +0100
@@ -1516,6 +1516,17 @@
refute
oops
+text {* Structured proofs *}
+
+lemma "x = y"
+proof cases
+ assume "x = y"
+ show ?thesis
+ refute
+ refute [no_assms]
+ refute [no_assms = false]
+oops
+
refute_params [satsolver="auto"]
end