src/HOL/Refute.thy
changeset 14457 6d5d6e78d851
parent 14350 41b32020d0b3
child 14463 ed09706ecc5d
     1.1 --- a/src/HOL/Refute.thy	Wed Mar 10 22:33:48 2004 +0100
     1.2 +++ b/src/HOL/Refute.thy	Wed Mar 10 22:35:37 2004 +0100
     1.3 @@ -14,16 +14,10 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 -(* INSTALLATION                                                              *)
     1.8 +(* NOTE                                                                      *)
     1.9  (*                                                                           *)
    1.10 -(* 1. Install a stand-alone SAT solver.  The default parameters in           *)
    1.11 -(*    'HOL/Main.thy' assume that ZChaff 2003.12.04 (available for Solaris/   *)
    1.12 -(*    Linux/Cygwin/Windows at http://ee.princeton.edu/~chaff/zchaff.php) is  *)
    1.13 -(*    installed as '$HOME/bin/zchaff'.  If you want to use a different SAT   *)
    1.14 -(*    solver (or install ZChaff to a different location), you will need to   *)
    1.15 -(*    modify at least the values for 'command' and (probably) 'success'.     *)
    1.16 -(*                                                                           *)
    1.17 -(* 2. That's it. You can now use the 'refute' command in your own theories.  *)
    1.18 +(* I strongly recommend that you install a stand-alone SAT solver if you     *)
    1.19 +(* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.         *)
    1.20  (* ------------------------------------------------------------------------- *)
    1.21  
    1.22  (* ------------------------------------------------------------------------- *)
    1.23 @@ -38,17 +32,15 @@
    1.24  (*                                                                           *)
    1.25  (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
    1.26  (* equality), including free/bound/schematic variables, lambda abstractions, *)
    1.27 -(* sets and set membership.                                                  *)
    1.28 +(* sets and set membership, "arbitrary", "The", and "Eps".  Constants for    *)
    1.29 +(* which a defining equation exists are unfolded automatically.              *)
    1.30  (*                                                                           *)
    1.31  (* NOT (YET) SUPPORTED ARE                                                   *)
    1.32  (*                                                                           *)
    1.33  (* - schematic type variables                                                *)
    1.34 -(* - type constructors other than =>, set, unit, and inductive datatypes     *)
    1.35 -(* - constants, including constructors of inductive datatypes and recursive  *)
    1.36 -(*   functions on inductive datatypes                                        *)
    1.37 -(*                                                                           *)
    1.38 -(* Unfolding of constants currently needs to be done manually, e.g. using    *)
    1.39 -(* 'apply (unfold xxx_def)'.                                                 *)
    1.40 +(* - type constructors other than bool, =>, set                              *)
    1.41 +(* - other constants, including constructors of inductive datatypes,         *)
    1.42 +(*   inductively defined sets and recursive functions                        *)
    1.43  (*                                                                           *)
    1.44  (* For formulas that contain (variables of) an inductive datatype, a         *)
    1.45  (* spurious countermodel may be returned.  Currently no warning is issued in *)
    1.46 @@ -69,45 +61,37 @@
    1.47  (* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
    1.48  (*                       when transforming the term into a propositional     *)
    1.49  (*                       formula.                                            *)
    1.50 -(* "satfile"     string  Name of the file used to store the propositional    *)
    1.51 -(*                       formula, i.e. the input to the SAT solver.          *)
    1.52 -(* "satformat"   string  Format of the SAT solver's input file.  Must be     *)
    1.53 -(*                       either "cnf", "defcnf", or "sat".  Since "sat" is   *)
    1.54 -(*                       not supported by most SAT solvers, and "cnf" can    *)
    1.55 -(*                       cause exponential blowup of the formula, "defcnf"   *)
    1.56 -(*                       is recommended.                                     *)
    1.57 -(* "resultfile"  string  Name of the file containing the SAT solver's        *)
    1.58 -(*                       output.                                             *)
    1.59 -(* "success"     string  Part of the line in the SAT solver's output that    *)
    1.60 -(*                       precedes a list of integers representing the        *)
    1.61 -(*                       satisfying assignment.                              *)
    1.62 -(* "command"     string  System command used to execute the SAT solver.      *)
    1.63 -(*                       Note that you if you change 'satfile' or            *)
    1.64 -(*                       'resultfile', you will also need to change          *)
    1.65 -(*                       'command'.                                          *)
    1.66 +(* "satsolver"   string  Name of the SAT solver to be used.                  *)
    1.67 +(*                                                                           *)
    1.68 +(* See 'HOL/Main.thy' for default values.                                    *)
    1.69  (* ------------------------------------------------------------------------- *)
    1.70  
    1.71  (* ------------------------------------------------------------------------- *)
    1.72  (* FILES                                                                     *)
    1.73  (*                                                                           *)
    1.74 -(* HOL/Tools/refute.ML        Implementation of the algorithm.               *)
    1.75 +(* HOL/Tools/prop_logic.ML    Propositional logic                            *)
    1.76 +(* HOL/Tools/sat_solver.ML    SAT solvers                                    *)
    1.77 +(* HOL/Tools/refute.ML        Translation HOL -> propositional logic and     *)
    1.78 +(*                            boolean assignment -> HOL model                *)
    1.79  (* HOL/Tools/refute_isar.ML   Adds 'refute'/'refute_params' to Isabelle's    *)
    1.80 -(*                            syntax.                                        *)
    1.81 -(* HOL/Refute.thy             This file. Loads the ML files, basic setup,    *)
    1.82 -(*                            documentation.                                 *)
    1.83 -(* HOL/Main.thy               Sets default parameters.                       *)
    1.84 -(* HOL/ex/RefuteExamples.thy  Examples.                                      *)
    1.85 +(*                            syntax                                         *)
    1.86 +(* HOL/Refute.thy             This file: loads the ML files, basic setup,    *)
    1.87 +(*                            documentation                                  *)
    1.88 +(* HOL/Main.thy               Sets default parameters                        *)
    1.89 +(* HOL/ex/RefuteExamples.thy  Examples                                       *)
    1.90  (* ------------------------------------------------------------------------- *)
    1.91  
    1.92  header {* Refute *}
    1.93  
    1.94  theory Refute = Map
    1.95  
    1.96 -files "Tools/refute.ML"
    1.97 +files "Tools/prop_logic.ML"
    1.98 +      "Tools/sat_solver.ML"
    1.99 +      "Tools/refute.ML"
   1.100        "Tools/refute_isar.ML":
   1.101  
   1.102 -(* Setting up the 'refute' and 'refute\_params' commands *)
   1.103 -
   1.104 +use "Tools/prop_logic.ML"
   1.105 +use "Tools/sat_solver.ML"
   1.106  use "Tools/refute.ML"
   1.107  use "Tools/refute_isar.ML"
   1.108