documentation updated
authorwebertj
Wed May 26 18:06:38 2004 +0200 (2004-05-26)
changeset 148081bf198c9828f
parent 14807 e8ccb13d7774
child 14809 eaa5d6987ba2
documentation updated
src/HOL/Refute.thy
     1.1 --- a/src/HOL/Refute.thy	Wed May 26 18:03:52 2004 +0200
     1.2 +++ b/src/HOL/Refute.thy	Wed May 26 18:06:38 2004 +0200
     1.3 @@ -32,7 +32,8 @@
     1.4  (*                                                                           *)
     1.5  (* I strongly recommend that you install a stand-alone SAT solver if you     *)
     1.6  (* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
     1.7 -(* have installed ZChaff, simply set 'ZCHAFF_HOME' in 'etc/settings'.        *)
     1.8 +(* have installed ZChaff Version 2003.12.04, simply set 'ZCHAFF_HOME' in     *)
     1.9 +(* 'etc/settings'.                                                           *)
    1.10  (* ------------------------------------------------------------------------- *)
    1.11  
    1.12  (* ------------------------------------------------------------------------- *)
    1.13 @@ -47,20 +48,18 @@
    1.14  (*                                                                           *)
    1.15  (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
    1.16  (* equality), including free/bound/schematic variables, lambda abstractions, *)
    1.17 -(* sets and set membership, "arbitrary", "The", and "Eps".  Constants for    *)
    1.18 -(* which a defining equation exists are unfolded automatically.  Non-        *)
    1.19 -(* recursive inductive datatypes are supported.                              *)
    1.20 +(* sets and set membership, "arbitrary", "The", and "Eps".  Defining         *)
    1.21 +(* equations for constants are added automatically.  Inductive datatypes are *)
    1.22 +(* supported, but may lead to spurious countermodels.                        *)
    1.23  (*                                                                           *)
    1.24 -(* The (space) complexity of the algorithm is exponential in both the length *)
    1.25 -(* of the formula and the size of the model.                                 *)
    1.26 +(* The (space) complexity of the algorithm is non-elementary.                *)
    1.27  (*                                                                           *)
    1.28  (* NOT (YET) SUPPORTED ARE                                                   *)
    1.29  (*                                                                           *)
    1.30  (* - schematic type variables                                                *)
    1.31  (* - axioms, sorts                                                           *)
    1.32 -(* - type constructors other than bool, =>, set, non-recursive IDTs          *)
    1.33  (* - inductively defined sets                                                *)
    1.34 -(* - recursive functions                                                     *)
    1.35 +(* - recursive functions on IDTs (case, recursion operators, size)           *)
    1.36  (* - ...                                                                     *)
    1.37  (* ------------------------------------------------------------------------- *)
    1.38  
    1.39 @@ -78,9 +77,16 @@
    1.40  (* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
    1.41  (*                       when transforming the term into a propositional     *)
    1.42  (*                       formula.                                            *)
    1.43 +(* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
    1.44 +(*                       This value is ignored under some ML compilers.      *)
    1.45  (* "satsolver"   string  Name of the SAT solver to be used.                  *)
    1.46  (*                                                                           *)
    1.47  (* See 'HOL/Main.thy' for default values.                                    *)
    1.48 +(*                                                                           *)
    1.49 +(* The size of particular types can be specified in the form type=size       *)
    1.50 +(* (where 'type' is a string, and 'size' is an int).  Examples:              *)
    1.51 +(* "'a"=1                                                                    *)
    1.52 +(* "List.list"=2                                                             *)
    1.53  (* ------------------------------------------------------------------------- *)
    1.54  
    1.55  (* ------------------------------------------------------------------------- *)
    1.56 @@ -89,7 +95,7 @@
    1.57  (* HOL/Tools/prop_logic.ML    Propositional logic                            *)
    1.58  (* HOL/Tools/sat_solver.ML    SAT solvers                                    *)
    1.59  (* HOL/Tools/refute.ML        Translation HOL -> propositional logic and     *)
    1.60 -(*                            boolean assignment -> HOL model                *)
    1.61 +(*                            Boolean assignment -> HOL model                *)
    1.62  (* HOL/Tools/refute_isar.ML   Adds 'refute'/'refute_params' to Isabelle's    *)
    1.63  (*                            syntax                                         *)
    1.64  (* HOL/Refute.thy             This file: loads the ML files, basic setup,    *)