src/HOL/Refute.thy
changeset 16870 a1155e140597
parent 16417 9bc16273c2d4
child 17721 b943c01e1c6d
equal deleted inserted replaced
16869:bc98da5727be 16870:a1155e140597
     1 (*  Title:      HOL/Refute.thy
     1 (*  Title:      HOL/Refute.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tjark Weber
     3     Author:     Tjark Weber
     4     Copyright   2003-2004
     4     Copyright   2003-2005
     5 
     5 
     6 Basic setup and documentation for the 'refute' (and 'refute_params') command.
     6 Basic setup and documentation for the 'refute' (and 'refute_params') command.
     7 *)
     7 *)
     8 
     8 
     9 header {* Refute *}
     9 header {* Refute *}
    10 
    10 
    11 theory Refute
    11 theory Refute
    12 imports Map
    12 imports Map
    13 uses "Tools/prop_logic.ML"
    13 uses "Tools/prop_logic.ML"
    14       "Tools/sat_solver.ML"
    14      "Tools/sat_solver.ML"
    15       "Tools/refute.ML"
    15      "Tools/refute.ML"
    16       "Tools/refute_isar.ML"
    16      "Tools/refute_isar.ML"
    17 begin
    17 begin
    18 
    18 
    19 setup Refute.setup
    19 setup Refute.setup
    20 
    20 
    21 text {*
    21 text {*
    47 (* ------------------------------------------------------------------------- *)
    47 (* ------------------------------------------------------------------------- *)
    48 (* CURRENT LIMITATIONS                                                       *)
    48 (* CURRENT LIMITATIONS                                                       *)
    49 (*                                                                           *)
    49 (*                                                                           *)
    50 (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
    50 (* 'refute' currently accepts formulas of higher-order predicate logic (with *)
    51 (* equality), including free/bound/schematic variables, lambda abstractions, *)
    51 (* equality), including free/bound/schematic variables, lambda abstractions, *)
    52 (* sets and set membership, "arbitrary", "The", and "Eps".  Defining         *)
    52 (* sets and set membership, "arbitrary", "The", "Eps", records and           *)
    53 (* equations for constants are added automatically.  Inductive datatypes are *)
    53 (* inductively defined sets.  Defining equations for constants are added     *)
    54 (* supported, but may lead to spurious countermodels.                        *)
    54 (* automatically, as are sort axioms.  Other, user-asserted axioms however   *)
       
    55 (* are ignored.  Inductive datatypes and recursive functions are supported,  *)
       
    56 (* but may lead to spurious countermodels.                                   *)
    55 (*                                                                           *)
    57 (*                                                                           *)
    56 (* The (space) complexity of the algorithm is non-elementary.                *)
    58 (* The (space) complexity of the algorithm is non-elementary.                *)
    57 (*                                                                           *)
    59 (*                                                                           *)
    58 (* NOT (YET) SUPPORTED ARE                                                   *)
    60 (* Schematic type variables are not supported.                               *)
    59 (*                                                                           *)
       
    60 (* - schematic type variables                                                *)
       
    61 (* - axioms, sorts                                                           *)
       
    62 (* - inductively defined sets                                                *)
       
    63 (* - recursive functions on IDTs (case, recursion operators, size)           *)
       
    64 (* - ...                                                                     *)
       
    65 (* ------------------------------------------------------------------------- *)
    61 (* ------------------------------------------------------------------------- *)
    66 
    62 
    67 (* ------------------------------------------------------------------------- *)
    63 (* ------------------------------------------------------------------------- *)
    68 (* PARAMETERS                                                                *)
    64 (* PARAMETERS                                                                *)
    69 (*                                                                           *)
    65 (*                                                                           *)