src/HOL/SMT.thy
author haftmann
Mon, 12 Jul 2010 08:58:13 +0200
changeset 37765 26bdfb7b680b
parent 37157 86872cbae9e9
child 37818 dd65033fed78
permissions -rw-r--r--
dropped superfluous [code del]s
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/SMT.thy
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
theory SMT
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
imports List
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     9
uses
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
  "~~/src/Tools/cache_io.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
  ("Tools/SMT/smt_monomorph.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
  ("Tools/SMT/smt_normalize.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
  ("Tools/SMT/smt_translate.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
  ("Tools/SMT/smt_solver.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
  ("Tools/SMT/smtlib_interface.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
  ("Tools/SMT/z3_proof_parser.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
  ("Tools/SMT/z3_proof_tools.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
  ("Tools/SMT/z3_proof_literals.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
  ("Tools/SMT/z3_proof_reconstruction.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
  ("Tools/SMT/z3_model.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
  ("Tools/SMT/z3_interface.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
  ("Tools/SMT/z3_solver.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
  ("Tools/SMT/cvc3_solver.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
  ("Tools/SMT/yices_solver.ML")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
begin
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
36902
c6bae4456741 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents: 36899
diff changeset
    29
subsection {* Triggers for quantifier instantiation *}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
Some SMT solvers support triggers for quantifier instantiation.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
Each trigger consists of one ore more patterns.  A pattern may either
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    34
be a list of positive subterms (each being tagged by "pat"), or a
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    35
list of negative subterms (each being tagged by "nopat").
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    36
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    37
When an SMT solver finds a term matching a positive pattern (a
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    38
pattern with positive subterms only), it instantiates the
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    39
corresponding quantifier accordingly.  Negative patterns inhibit
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    40
quantifier instantiations.  Each pattern should mention all preceding
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    41
bound variables.
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
datatype pattern = Pattern
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    46
definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    47
definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    49
definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
where "trigger _ P = P"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
36902
c6bae4456741 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents: 36899
diff changeset
    54
subsection {* Higher-order encoding *}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
Application is made explicit for constants occurring with varying
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
numbers of arguments.  This is achieved by the introduction of the
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
following constant.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
37153
8feed34275ce renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents: 37151
diff changeset
    62
definition fun_app where "fun_app f x = f x"
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
Some solvers support a theory of arrays which can be used to encode
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
higher-order functions.  The following set of lemmas specifies the
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
properties of such (extensional) arrays.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
37157
86872cbae9e9 added function update examples and set examples
boehmes
parents: 37153
diff changeset
    71
  fun_upd_upd fun_app_def
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
36902
c6bae4456741 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents: 36899
diff changeset
    75
subsection {* First-order logic *}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
Some SMT solvers require a strict separation between formulas and
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
terms.  When translating higher-order into first-order problems,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
all uninterpreted constants (those not builtin in the target solver)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
are treated as function symbols in the first-order sense.  Their
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
occurrences as head symbols in atoms (i.e., as predicate symbols) is
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
turned into terms by equating such atoms with @{term True} using the
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
following term-level equation symbol.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
    87
definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
37151
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
    91
subsection {* Integer division and modulo for Z3 *}
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
    92
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
    93
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
    94
  "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
    95
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
    96
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
    97
  "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
    98
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
    99
lemma div_by_z3div: "k div l = (
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   100
     if k = 0 \<or> l = 0 then 0
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   101
     else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3div k l
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   102
     else z3div (-k) (-l))"
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   103
  by (auto simp add: z3div_def)
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   104
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   105
lemma mod_by_z3mod: "k mod l = (
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   106
     if l = 0 then k
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   107
     else if k = 0 then 0
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   108
     else if (0 < k \<and> 0 < l) \<or> (k < 0 \<and> 0 < l) then z3mod k l
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   109
     else - z3mod (-k) (-l))"
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   110
  by (auto simp add: z3mod_def)
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   111
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   112
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 37124
diff changeset
   113
36902
c6bae4456741 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents: 36899
diff changeset
   114
subsection {* Setup *}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
use "Tools/SMT/smt_monomorph.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
use "Tools/SMT/smt_normalize.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
use "Tools/SMT/smt_translate.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
use "Tools/SMT/smt_solver.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
use "Tools/SMT/smtlib_interface.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
use "Tools/SMT/z3_interface.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
use "Tools/SMT/z3_proof_parser.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
use "Tools/SMT/z3_proof_tools.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
use "Tools/SMT/z3_proof_literals.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
use "Tools/SMT/z3_proof_reconstruction.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
use "Tools/SMT/z3_model.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
use "Tools/SMT/z3_solver.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
use "Tools/SMT/cvc3_solver.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
use "Tools/SMT/yices_solver.ML"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
setup {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
  SMT_Solver.setup #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
  Z3_Proof_Reconstruction.setup #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
  Z3_Solver.setup #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
  CVC3_Solver.setup #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
  Yices_Solver.setup
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
36902
c6bae4456741 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents: 36899
diff changeset
   141
subsection {* Configuration *}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
text {*
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   144
The current configuration can be printed by the command
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   145
@{text smt_status}, which shows the values of most options.
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
subsection {* General configuration options *}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
The option @{text smt_solver} can be used to change the target SMT
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
solver.  The possible values are @{text cvc3}, @{text yices}, and
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
@{text z3}.  It is advisable to locally install the selected solver,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
although this is not necessary for @{text cvc3} and @{text z3}, which
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
can also be used over an Internet-based service.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
When using local SMT solvers, the path to their binaries should be
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
declared by setting the following environment variables:
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
@{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
declare [[ smt_solver = z3 ]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
Since SMT solvers are potentially non-terminating, there is a timeout
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
(given in seconds) to restrict their runtime.  A value greater than
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
120 (seconds) is in most cases not advisable.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
declare [[ smt_timeout = 20 ]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
subsection {* Certificates *}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
By setting the option @{text smt_certificates} to the name of a file,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
all following applications of an SMT solver a cached in that file.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
Any further application of the same SMT solver (using the very same
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
configuration) re-uses the cached certificate instead of invoking the
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
solver.  An empty string disables caching certificates.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
The filename should be given as an explicit path.  It is good
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
practice to use the name of the current theory (with ending
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
@{text ".certs"} instead of @{text ".thy"}) as the certificates file.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
declare [[ smt_certificates = "" ]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
The option @{text smt_fixed} controls whether only stored
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
certificates are should be used or invocation of an SMT solver is
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
allowed.  When set to @{text true}, no SMT solver will ever be
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
invoked and only the existing certificates found in the configured
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
cache are used;  when set to @{text false} and there is no cached
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
certificate for some proposition, then the configured SMT solver is
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
invoked.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
declare [[ smt_fixed = false ]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
subsection {* Tracing *}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
For tracing the generated problem file given to the SMT solver as
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
well as the returned result of the solver, the option
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   211
@{text smt_trace} should be set to @{text true}.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
declare [[ smt_trace = false ]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   218
subsection {* Z3-specific options *}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   221
Z3 is the only SMT solver whose proofs are checked (or reconstructed)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   222
in Isabelle (all other solvers are implemented as oracles).  Enabling
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
or disabling proof reconstruction for Z3 is controlled by the option
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
@{text z3_proofs}. 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   227
declare [[ z3_proofs = true ]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
From the set of assumptions given to Z3, those assumptions used in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
the proof are traced when the option @{text z3_trace_assms} is set to
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
@{term true}.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
declare [[ z3_trace_assms = false ]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
Z3 provides several commandline options to tweak its behaviour.  They
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
can be configured by writing them literally as value for the option
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
@{text z3_options}.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
declare [[ z3_options = "" ]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
36902
c6bae4456741 use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
huffman
parents: 36899
diff changeset
   247
subsection {* Schematic rules for Z3 proof reconstruction *}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
text {*
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
Several prof rules of Z3 are not very well documented.  There are two
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
lemma groups which can turn failing Z3 proof reconstruction attempts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
into succeeding ones: the facts in @{text z3_rule} are tried prior to
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
any implemented reconstruction procedure for all uncertain Z3 proof
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
rules;  the facts in @{text z3_simp} are only fed to invocations of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
the simplifier when reconstructing theory-specific proof steps.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
*}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
lemmas [z3_rule] =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
  refl eq_commute conj_commute disj_commute simp_thms nnf_simps
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
  ring_distribs field_simps times_divide_eq_right times_divide_eq_left
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
  if_True if_False not_not
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
lemma [z3_rule]:
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
  "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
  "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
  "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
  by auto
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
lemma [z3_rule]:
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
  "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
  by auto
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
lemma [z3_rule]:
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
  "((\<not>P) = P) = False"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
  "(P = (\<not>P)) = False"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
  "(P \<noteq> Q) = (Q = (\<not>P))"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
  "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
  "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
  by auto
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
lemma [z3_rule]:
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
  "(if P then P else \<not>P) = True"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
  "(if \<not>P then \<not>P else P) = True"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
  "(if P then True else False) = P"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
  "(if P then False else True) = (\<not>P)"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
  "(if \<not>P then x else y) = (if P then y else x)"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
  by auto
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
lemma [z3_rule]:
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
  "P = Q \<or> P \<or> Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   291
  "P = Q \<or> \<not>P \<or> \<not>Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
  "(\<not>P) = Q \<or> \<not>P \<or> Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
  "(\<not>P) = Q \<or> P \<or> \<not>Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
  "P = (\<not>Q) \<or> \<not>P \<or> Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
  "P = (\<not>Q) \<or> P \<or> \<not>Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   296
  "P \<noteq> Q \<or> P \<or> \<not>Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
  "P \<noteq> Q \<or> \<not>P \<or> Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
  "P \<noteq> (\<not>Q) \<or> P \<or> Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
  "(\<not>P) \<noteq> Q \<or> P \<or> Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
  "P \<or> Q \<or> P \<noteq> (\<not>Q)"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
  "P \<or> Q \<or> (\<not>P) \<noteq> Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
  "P \<or> \<not>Q \<or> P \<noteq> Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
  "\<not>P \<or> Q \<or> P \<noteq> Q"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
  by auto
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
lemma [z3_rule]:
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
  "0 + (x::int) = x"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
  "x + 0 = x"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
  "0 * x = 0"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
  "1 * x = x"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
  "x + y = y + x"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
  by auto
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
   314
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
   315
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
   316
hide_type (open) pattern
37153
8feed34275ce renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents: 37151
diff changeset
   317
hide_const Pattern term_eq
8feed34275ce renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents: 37151
diff changeset
   318
hide_const (open) trigger pat nopat fun_app z3div z3mod
37124
fe22fc54b876 hide constants and types introduced by SMT,
boehmes
parents: 36902
diff changeset
   319
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
end