Adding 'refute' to HOL.
(* Title: HOL/Refute.thy
ID: $Id$
Author: Tjark Weber
Copyright 2003-2004
Basic setup and documentation for the 'refute' (and 'refute_params') command.
*)
(* ------------------------------------------------------------------------- *)
(* REFUTE *)
(* *)
(* We use a SAT solver to search for a (finite) model that refutes a given *)
(* HOL formula. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* INSTALLATION *)
(* *)
(* 1. Install a stand-alone SAT solver. The default parameters in *)
(* 'HOL/Main.thy' assume that ZChaff 2003.12.04 (available for Solaris/ *)
(* Linux/Cygwin/Windows at http://ee.princeton.edu/~chaff/zchaff.php) is *)
(* installed as '$HOME/bin/zchaff'. If you want to use a different SAT *)
(* solver (or install ZChaff to a different location), you will need to *)
(* modify at least the values for 'command' and (probably) 'success'. *)
(* *)
(* 2. That's it. You can now use the 'refute' command in your own theories. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* USAGE *)
(* *)
(* See the file 'HOL/ex/Refute_Examples.thy' for examples. The supported *)
(* parameters are explained below. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* CURRENT LIMITATIONS *)
(* *)
(* 'refute' currently accepts formulas of higher-order predicate logic (with *)
(* equality), including free/bound/schematic variables, lambda abstractions, *)
(* sets and set membership. *)
(* *)
(* NOT (YET) SUPPORTED ARE *)
(* *)
(* - schematic type variables *)
(* - type constructors other than =>, set, unit, and inductive datatypes *)
(* - constants, including constructors of inductive datatypes and recursive *)
(* functions on inductive datatypes *)
(* *)
(* Unfolding of constants currently needs to be done manually, e.g. using *)
(* 'apply (unfold xxx_def)'. *)
(* *)
(* For formulas that contain (variables of) an inductive datatype, a *)
(* spurious countermodel may be returned. Currently no warning is issued in *)
(* this case. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* PARAMETERS *)
(* *)
(* The following global parameters are currently supported (and required): *)
(* *)
(* Name Type Description *)
(* *)
(* "minsize" int Only search for models with size at least *)
(* 'minsize'. *)
(* "maxsize" int If >0, only search for models with size at most *)
(* 'maxsize'. *)
(* "maxvars" int If >0, use at most 'maxvars' boolean variables *)
(* when transforming the term into a propositional *)
(* formula. *)
(* "satfile" string Name of the file used to store the propositional *)
(* formula, i.e. the input to the SAT solver. *)
(* "satformat" string Format of the SAT solver's input file. Must be *)
(* either "cnf", "defcnf", or "sat". Since "sat" is *)
(* not supported by most SAT solvers, and "cnf" can *)
(* cause exponential blowup of the formula, "defcnf" *)
(* is recommended. *)
(* "resultfile" string Name of the file containing the SAT solver's *)
(* output. *)
(* "success" string Part of the line in the SAT solver's output that *)
(* precedes a list of integers representing the *)
(* satisfying assignment. *)
(* "command" string System command used to execute the SAT solver. *)
(* Note that you if you change 'satfile' or *)
(* 'resultfile', you will also need to change *)
(* 'command'. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* FILES *)
(* *)
(* HOL/Tools/refute.ML Implementation of the algorithm. *)
(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *)
(* syntax. *)
(* HOL/Refute.thy This file. Loads the ML files, basic setup, *)
(* documentation. *)
(* HOL/Main.thy Sets default parameters. *)
(* HOL/ex/RefuteExamples.thy Examples. *)
(* ------------------------------------------------------------------------- *)
header {* Refute *}
theory Refute = Map
files "Tools/refute.ML"
"Tools/refute_isar.ML":
(* Setting up the 'refute' and 'refute\_params' commands *)
use "Tools/refute.ML"
use "Tools/refute_isar.ML"
setup Refute.setup
end