src/HOL/Refute.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46960 f19e5837ad69
child 48891 c0eafbd55de3
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     1
(*  Title:      HOL/Refute.thy
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     2
    Author:     Tjark Weber
22058
49faa8c7a5d9 updated to mention the automatic unfolding of constants
webertj
parents: 21332
diff changeset
     3
    Copyright   2003-2007
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     4
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     5
Basic setup and documentation for the 'refute' (and 'refute_params') command.
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     6
*)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
     7
14589
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
     8
header {* Refute *}
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
     9
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14808
diff changeset
    10
theory Refute
40178
00152d17855b reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents: 40121
diff changeset
    11
imports Hilbert_Choice List Sledgehammer
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 40178
diff changeset
    12
keywords "refute" :: diag and "refute_params" :: thy_decl
39048
4006f5c3f421 just one refute.ML;
wenzelm
parents: 34120
diff changeset
    13
uses "Tools/refute.ML"
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14808
diff changeset
    14
begin
14589
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
    15
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
    16
setup Refute.setup
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
    17
46960
f19e5837ad69 refute_params are given in *this* theory;
wenzelm
parents: 46950
diff changeset
    18
refute_params
f19e5837ad69 refute_params are given in *this* theory;
wenzelm
parents: 46950
diff changeset
    19
 [itself = 1,
f19e5837ad69 refute_params are given in *this* theory;
wenzelm
parents: 46950
diff changeset
    20
  minsize = 1,
f19e5837ad69 refute_params are given in *this* theory;
wenzelm
parents: 46950
diff changeset
    21
  maxsize = 8,
f19e5837ad69 refute_params are given in *this* theory;
wenzelm
parents: 46950
diff changeset
    22
  maxvars = 10000,
f19e5837ad69 refute_params are given in *this* theory;
wenzelm
parents: 46950
diff changeset
    23
  maxtime = 60,
f19e5837ad69 refute_params are given in *this* theory;
wenzelm
parents: 46950
diff changeset
    24
  satsolver = auto,
f19e5837ad69 refute_params are given in *this* theory;
wenzelm
parents: 46950
diff changeset
    25
  no_assms = false]
f19e5837ad69 refute_params are given in *this* theory;
wenzelm
parents: 46950
diff changeset
    26
14589
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
    27
text {*
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
    28
\small
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
    29
\begin{verbatim}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    30
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    31
(* REFUTE                                                                    *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    32
(*                                                                           *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    33
(* We use a SAT solver to search for a (finite) model that refutes a given   *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    34
(* HOL formula.                                                              *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    35
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    36
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    37
(* ------------------------------------------------------------------------- *)
14457
6d5d6e78d851 *** empty log message ***
webertj
parents: 14350
diff changeset
    38
(* NOTE                                                                      *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    39
(*                                                                           *)
14457
6d5d6e78d851 *** empty log message ***
webertj
parents: 14350
diff changeset
    40
(* I strongly recommend that you install a stand-alone SAT solver if you     *)
14463
ed09706ecc5d Documentation updated
webertj
parents: 14457
diff changeset
    41
(* want to use 'refute'.  For details see 'HOL/Tools/sat_solver.ML'.  If you *)
15293
7797a04cc188 removed explicit mentioning of zChaffs version number
webertj
parents: 15140
diff changeset
    42
(* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME'  *)
7797a04cc188 removed explicit mentioning of zChaffs version number
webertj
parents: 15140
diff changeset
    43
(* in 'etc/settings'.                                                        *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    44
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    45
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    46
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    47
(* USAGE                                                                     *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    48
(*                                                                           *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    49
(* See the file 'HOL/ex/Refute_Examples.thy' for examples.  The supported    *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    50
(* parameters are explained below.                                           *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    51
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    52
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    53
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    54
(* CURRENT LIMITATIONS                                                       *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    55
(*                                                                           *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    56
(* 'refute' currently accepts formulas of higher-order predicate logic (with *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    57
(* equality), including free/bound/schematic variables, lambda abstractions, *)
16870
a1155e140597 Documentation updated
webertj
parents: 16417
diff changeset
    58
(* sets and set membership, "arbitrary", "The", "Eps", records and           *)
22058
49faa8c7a5d9 updated to mention the automatic unfolding of constants
webertj
parents: 21332
diff changeset
    59
(* inductively defined sets.  Constants are unfolded automatically, and sort *)
49faa8c7a5d9 updated to mention the automatic unfolding of constants
webertj
parents: 21332
diff changeset
    60
(* axioms are added as well.  Other, user-asserted axioms however are        *)
49faa8c7a5d9 updated to mention the automatic unfolding of constants
webertj
parents: 21332
diff changeset
    61
(* ignored.  Inductive datatypes and recursive functions are supported, but  *)
49faa8c7a5d9 updated to mention the automatic unfolding of constants
webertj
parents: 21332
diff changeset
    62
(* may lead to spurious countermodels.                                       *)
14463
ed09706ecc5d Documentation updated
webertj
parents: 14457
diff changeset
    63
(*                                                                           *)
14808
1bf198c9828f documentation updated
webertj
parents: 14771
diff changeset
    64
(* The (space) complexity of the algorithm is non-elementary.                *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    65
(*                                                                           *)
16870
a1155e140597 Documentation updated
webertj
parents: 16417
diff changeset
    66
(* Schematic type variables are not supported.                               *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    67
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    68
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    69
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    70
(* PARAMETERS                                                                *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    71
(*                                                                           *)
34120
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 34018
diff changeset
    72
(* The following global parameters are currently supported (and required,    *)
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 34018
diff changeset
    73
(* except for "expect"):                                                     *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    74
(*                                                                           *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    75
(* Name          Type    Description                                         *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    76
(*                                                                           *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    77
(* "minsize"     int     Only search for models with size at least           *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    78
(*                       'minsize'.                                          *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    79
(* "maxsize"     int     If >0, only search for models with size at most     *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    80
(*                       'maxsize'.                                          *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    81
(* "maxvars"     int     If >0, use at most 'maxvars' boolean variables      *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    82
(*                       when transforming the term into a propositional     *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    83
(*                       formula.                                            *)
14808
1bf198c9828f documentation updated
webertj
parents: 14771
diff changeset
    84
(* "maxtime"     int     If >0, terminate after at most 'maxtime' seconds.   *)
1bf198c9828f documentation updated
webertj
parents: 14771
diff changeset
    85
(*                       This value is ignored under some ML compilers.      *)
14457
6d5d6e78d851 *** empty log message ***
webertj
parents: 14350
diff changeset
    86
(* "satsolver"   string  Name of the SAT solver to be used.                  *)
34120
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 34018
diff changeset
    87
(* "no_assms"    bool    If "true", assumptions in structured proofs are     *)
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 34018
diff changeset
    88
(*                       not considered.                                     *)
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 34018
diff changeset
    89
(* "expect"      string  Expected result ("genuine", "potential", "none", or *)
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents: 34018
diff changeset
    90
(*                       "unknown").                                         *)
14457
6d5d6e78d851 *** empty log message ***
webertj
parents: 14350
diff changeset
    91
(*                                                                           *)
14808
1bf198c9828f documentation updated
webertj
parents: 14771
diff changeset
    92
(* The size of particular types can be specified in the form type=size       *)
1bf198c9828f documentation updated
webertj
parents: 14771
diff changeset
    93
(* (where 'type' is a string, and 'size' is an int).  Examples:              *)
1bf198c9828f documentation updated
webertj
parents: 14771
diff changeset
    94
(* "'a"=1                                                                    *)
1bf198c9828f documentation updated
webertj
parents: 14771
diff changeset
    95
(* "List.list"=2                                                             *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    96
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    97
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    98
(* ------------------------------------------------------------------------- *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
    99
(* FILES                                                                     *)
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   100
(*                                                                           *)
39048
4006f5c3f421 just one refute.ML;
wenzelm
parents: 34120
diff changeset
   101
(* HOL/Tools/prop_logic.ML     Propositional logic                           *)
4006f5c3f421 just one refute.ML;
wenzelm
parents: 34120
diff changeset
   102
(* HOL/Tools/sat_solver.ML     SAT solvers                                   *)
4006f5c3f421 just one refute.ML;
wenzelm
parents: 34120
diff changeset
   103
(* HOL/Tools/refute.ML         Translation HOL -> propositional logic and    *)
4006f5c3f421 just one refute.ML;
wenzelm
parents: 34120
diff changeset
   104
(*                             Boolean assignment -> HOL model               *)
4006f5c3f421 just one refute.ML;
wenzelm
parents: 34120
diff changeset
   105
(* HOL/Refute.thy              This file: loads the ML files, basic setup,   *)
4006f5c3f421 just one refute.ML;
wenzelm
parents: 34120
diff changeset
   106
(*                             documentation                                 *)
4006f5c3f421 just one refute.ML;
wenzelm
parents: 34120
diff changeset
   107
(* HOL/SAT.thy                 Sets default parameters                       *)
4006f5c3f421 just one refute.ML;
wenzelm
parents: 34120
diff changeset
   108
(* HOL/ex/Refute_Examples.thy  Examples                                      *)
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   109
(* ------------------------------------------------------------------------- *)
14589
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
   110
\end{verbatim}
feae7b5fd425 tuned document;
wenzelm
parents: 14463
diff changeset
   111
*}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   112
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents:
diff changeset
   113
end