src/HOL/SMT.thy
author blanchet
Tue Mar 11 15:34:38 2014 +0100 (2014-03-11)
changeset 56046 683148f3ae48
parent 55049 327eafb594ba
child 56078 624faeda77b5
permissions -rw-r--r--
full path
boehmes@36898
     1
(*  Title:      HOL/SMT.thy
boehmes@36898
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36898
     3
*)
boehmes@36898
     4
boehmes@36898
     5
header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
boehmes@36898
     6
boehmes@36898
     7
theory SMT
boehmes@41426
     8
imports Record
wenzelm@46950
     9
keywords "smt_status" :: diag
boehmes@36898
    10
begin
boehmes@36898
    11
wenzelm@48892
    12
ML_file "Tools/SMT/smt_utils.ML"
wenzelm@48892
    13
ML_file "Tools/SMT/smt_failure.ML"
wenzelm@48892
    14
ML_file "Tools/SMT/smt_config.ML"
boehmes@36898
    15
boehmes@36898
    16
huffman@36902
    17
subsection {* Triggers for quantifier instantiation *}
boehmes@36898
    18
boehmes@36898
    19
text {*
boehmes@41125
    20
Some SMT solvers support patterns as a quantifier instantiation
boehmes@41125
    21
heuristics.  Patterns may either be positive terms (tagged by "pat")
boehmes@41125
    22
triggering quantifier instantiations -- when the solver finds a
boehmes@41125
    23
term matching a positive pattern, it instantiates the corresponding
boehmes@41125
    24
quantifier accordingly -- or negative terms (tagged by "nopat")
boehmes@41125
    25
inhibiting quantifier instantiations.  A list of patterns
boehmes@41125
    26
of the same kind is called a multipattern, and all patterns in a
boehmes@41125
    27
multipattern are considered conjunctively for quantifier instantiation.
boehmes@41125
    28
A list of multipatterns is called a trigger, and their multipatterns
boehmes@41125
    29
act disjunctively during quantifier instantiation.  Each multipattern
boehmes@41125
    30
should mention at least all quantified variables of the preceding
boehmes@41125
    31
quantifier block.
boehmes@36898
    32
*}
boehmes@36898
    33
boehmes@36898
    34
datatype pattern = Pattern
boehmes@36898
    35
boehmes@37124
    36
definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
boehmes@37124
    37
definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
boehmes@36898
    38
boehmes@37124
    39
definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
boehmes@36898
    40
where "trigger _ P = P"
boehmes@36898
    41
boehmes@36898
    42
boehmes@36898
    43
boehmes@40664
    44
subsection {* Quantifier weights *}
boehmes@40664
    45
boehmes@40664
    46
text {*
boehmes@40664
    47
Weight annotations to quantifiers influence the priority of quantifier
boehmes@40664
    48
instantiations.  They should be handled with care for solvers, which support
boehmes@40664
    49
them, because incorrect choices of weights might render a problem unsolvable.
boehmes@40664
    50
*}
boehmes@40664
    51
boehmes@40664
    52
definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
boehmes@40664
    53
boehmes@40664
    54
text {*
boehmes@40664
    55
Weights must be non-negative.  The value @{text 0} is equivalent to providing
boehmes@40664
    56
no weight at all.
boehmes@40664
    57
boehmes@40664
    58
Weights should only be used at quantifiers and only inside triggers (if the
boehmes@40664
    59
quantifier has triggers).  Valid usages of weights are as follows:
boehmes@40664
    60
boehmes@40664
    61
\begin{itemize}
boehmes@40664
    62
\item
boehmes@40664
    63
@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
boehmes@40664
    64
\item
boehmes@40664
    65
@{term "\<forall>x. weight 3 (P x)"}
boehmes@40664
    66
\end{itemize}
boehmes@40664
    67
*}
boehmes@40664
    68
boehmes@40664
    69
boehmes@40664
    70
huffman@36902
    71
subsection {* Higher-order encoding *}
boehmes@36898
    72
boehmes@36898
    73
text {*
boehmes@36898
    74
Application is made explicit for constants occurring with varying
boehmes@36898
    75
numbers of arguments.  This is achieved by the introduction of the
boehmes@36898
    76
following constant.
boehmes@36898
    77
*}
boehmes@36898
    78
boehmes@41127
    79
definition fun_app where "fun_app f = f"
boehmes@36898
    80
boehmes@36898
    81
text {*
boehmes@36898
    82
Some solvers support a theory of arrays which can be used to encode
boehmes@36898
    83
higher-order functions.  The following set of lemmas specifies the
boehmes@36898
    84
properties of such (extensional) arrays.
boehmes@36898
    85
*}
boehmes@36898
    86
boehmes@36898
    87
lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
boehmes@37157
    88
  fun_upd_upd fun_app_def
boehmes@36898
    89
boehmes@36898
    90
boehmes@36898
    91
huffman@36902
    92
subsection {* First-order logic *}
boehmes@36898
    93
boehmes@36898
    94
text {*
boehmes@41059
    95
Some SMT solvers only accept problems in first-order logic, i.e.,
boehmes@41059
    96
where formulas and terms are syntactically separated. When
boehmes@41059
    97
translating higher-order into first-order problems, all
boehmes@41059
    98
uninterpreted constants (those not built-in in the target solver)
boehmes@36898
    99
are treated as function symbols in the first-order sense.  Their
boehmes@41059
   100
occurrences as head symbols in atoms (i.e., as predicate symbols) are
boehmes@41281
   101
turned into terms by logically equating such atoms with @{term True}.
boehmes@41281
   102
For technical reasons, @{term True} and @{term False} occurring inside
boehmes@41281
   103
terms are replaced by the following constants.
boehmes@36898
   104
*}
boehmes@36898
   105
boehmes@41281
   106
definition term_true where "term_true = True"
boehmes@41281
   107
definition term_false where "term_false = False"
boehmes@41281
   108
boehmes@36898
   109
boehmes@36898
   110
boehmes@37151
   111
subsection {* Integer division and modulo for Z3 *}
boehmes@37151
   112
boehmes@37151
   113
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
boehmes@37151
   114
  "z3div k l = (if 0 \<le> l then k div l else -(k div (-l)))"
boehmes@37151
   115
boehmes@37151
   116
definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
boehmes@37151
   117
  "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
boehmes@37151
   118
boehmes@37151
   119
boehmes@37151
   120
huffman@36902
   121
subsection {* Setup *}
boehmes@36898
   122
wenzelm@48892
   123
ML_file "Tools/SMT/smt_builtin.ML"
wenzelm@48892
   124
ML_file "Tools/SMT/smt_datatypes.ML"
wenzelm@48892
   125
ML_file "Tools/SMT/smt_normalize.ML"
wenzelm@48892
   126
ML_file "Tools/SMT/smt_translate.ML"
wenzelm@48892
   127
ML_file "Tools/SMT/smt_solver.ML"
wenzelm@48892
   128
ML_file "Tools/SMT/smtlib_interface.ML"
wenzelm@48892
   129
ML_file "Tools/SMT/z3_interface.ML"
wenzelm@48892
   130
ML_file "Tools/SMT/z3_proof_parser.ML"
wenzelm@48892
   131
ML_file "Tools/SMT/z3_proof_tools.ML"
wenzelm@48892
   132
ML_file "Tools/SMT/z3_proof_literals.ML"
wenzelm@48892
   133
ML_file "Tools/SMT/z3_proof_methods.ML"
wenzelm@48892
   134
ML_file "Tools/SMT/z3_proof_reconstruction.ML"
wenzelm@48892
   135
ML_file "Tools/SMT/z3_model.ML"
wenzelm@48892
   136
ML_file "Tools/SMT/smt_setup_solvers.ML"
boehmes@36898
   137
boehmes@36898
   138
setup {*
boehmes@40424
   139
  SMT_Config.setup #>
boehmes@41059
   140
  SMT_Normalize.setup #>
boehmes@41059
   141
  SMTLIB_Interface.setup #>
boehmes@41059
   142
  Z3_Interface.setup #>
boehmes@36898
   143
  Z3_Proof_Reconstruction.setup #>
boehmes@40162
   144
  SMT_Setup_Solvers.setup
boehmes@36898
   145
*}
boehmes@36898
   146
wenzelm@47701
   147
method_setup smt = {*
wenzelm@47701
   148
  Scan.optional Attrib.thms [] >>
wenzelm@47701
   149
    (fn thms => fn ctxt =>
wenzelm@47701
   150
      METHOD (fn facts => HEADGOAL (SMT_Solver.smt_tac ctxt (thms @ facts))))
wenzelm@47701
   151
*} "apply an SMT solver to the current goal"
boehmes@36898
   152
boehmes@36898
   153
huffman@36902
   154
subsection {* Configuration *}
boehmes@36898
   155
boehmes@36898
   156
text {*
boehmes@36899
   157
The current configuration can be printed by the command
boehmes@36899
   158
@{text smt_status}, which shows the values of most options.
boehmes@36898
   159
*}
boehmes@36898
   160
boehmes@36898
   161
boehmes@36898
   162
boehmes@36898
   163
subsection {* General configuration options *}
boehmes@36898
   164
boehmes@36898
   165
text {*
boehmes@36898
   166
The option @{text smt_solver} can be used to change the target SMT
boehmes@41432
   167
solver.  The possible values can be obtained from the @{text smt_status}
boehmes@41432
   168
command.
boehmes@41459
   169
boehmes@41459
   170
Due to licensing restrictions, Yices and Z3 are not installed/enabled
boehmes@41459
   171
by default.  Z3 is free for non-commercial applications and can be enabled
wenzelm@55007
   172
by setting Isabelle system option @{text z3_non_commercial} to @{text yes}.
boehmes@36898
   173
*}
boehmes@36898
   174
boehmes@41601
   175
declare [[ smt_solver = z3 ]]
boehmes@36898
   176
boehmes@36898
   177
text {*
boehmes@36898
   178
Since SMT solvers are potentially non-terminating, there is a timeout
boehmes@36898
   179
(given in seconds) to restrict their runtime.  A value greater than
boehmes@36898
   180
120 (seconds) is in most cases not advisable.
boehmes@36898
   181
*}
boehmes@36898
   182
boehmes@36898
   183
declare [[ smt_timeout = 20 ]]
boehmes@36898
   184
boehmes@40162
   185
text {*
boehmes@41121
   186
SMT solvers apply randomized heuristics.  In case a problem is not
boehmes@41121
   187
solvable by an SMT solver, changing the following option might help.
boehmes@41121
   188
*}
boehmes@41121
   189
boehmes@41121
   190
declare [[ smt_random_seed = 1 ]]
boehmes@41121
   191
boehmes@41121
   192
text {*
boehmes@40162
   193
In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
boehmes@40162
   194
solvers are fully trusted without additional checks.  The following
boehmes@40162
   195
option can cause the SMT solver to run in proof-producing mode, giving
boehmes@40162
   196
a checkable certificate.  This is currently only implemented for Z3.
boehmes@40162
   197
*}
boehmes@40162
   198
boehmes@40162
   199
declare [[ smt_oracle = false ]]
boehmes@40162
   200
boehmes@40162
   201
text {*
boehmes@40162
   202
Each SMT solver provides several commandline options to tweak its
boehmes@40162
   203
behaviour.  They can be passed to the solver by setting the following
boehmes@40162
   204
options.
boehmes@40162
   205
*}
boehmes@40162
   206
boehmes@55049
   207
declare [[ cvc3_options = "" ]]
boehmes@41432
   208
declare [[ yices_options = "" ]]
boehmes@55049
   209
declare [[ z3_options = "" ]]
boehmes@40162
   210
boehmes@40162
   211
text {*
boehmes@40162
   212
Enable the following option to use built-in support for datatypes and
boehmes@40162
   213
records.  Currently, this is only implemented for Z3 running in oracle
boehmes@40162
   214
mode.
boehmes@40162
   215
*}
boehmes@40162
   216
boehmes@40162
   217
declare [[ smt_datatypes = false ]]
boehmes@40162
   218
boehmes@41125
   219
text {*
boehmes@41125
   220
The SMT method provides an inference mechanism to detect simple triggers
boehmes@41125
   221
in quantified formulas, which might increase the number of problems
boehmes@41125
   222
solvable by SMT solvers (note: triggers guide quantifier instantiations
boehmes@41125
   223
in the SMT solver).  To turn it on, set the following option.
boehmes@41125
   224
*}
boehmes@41125
   225
boehmes@41125
   226
declare [[ smt_infer_triggers = false ]]
boehmes@41125
   227
boehmes@41125
   228
text {*
boehmes@41125
   229
The SMT method monomorphizes the given facts, that is, it tries to
boehmes@41125
   230
instantiate all schematic type variables with fixed types occurring
boehmes@41125
   231
in the problem.  This is a (possibly nonterminating) fixed-point
boehmes@41125
   232
construction whose cycles are limited by the following option.
boehmes@41125
   233
*}
boehmes@41125
   234
boehmes@43230
   235
declare [[ monomorph_max_rounds = 5 ]]
boehmes@41125
   236
boehmes@41762
   237
text {*
boehmes@41762
   238
In addition, the number of generated monomorphic instances is limited
boehmes@41762
   239
by the following option.
boehmes@41762
   240
*}
boehmes@41762
   241
boehmes@43230
   242
declare [[ monomorph_max_new_instances = 500 ]]
boehmes@41762
   243
boehmes@36898
   244
boehmes@36898
   245
boehmes@36898
   246
subsection {* Certificates *}
boehmes@36898
   247
boehmes@36898
   248
text {*
boehmes@36898
   249
By setting the option @{text smt_certificates} to the name of a file,
boehmes@36898
   250
all following applications of an SMT solver a cached in that file.
boehmes@36898
   251
Any further application of the same SMT solver (using the very same
boehmes@36898
   252
configuration) re-uses the cached certificate instead of invoking the
boehmes@36898
   253
solver.  An empty string disables caching certificates.
boehmes@36898
   254
boehmes@36898
   255
The filename should be given as an explicit path.  It is good
boehmes@36898
   256
practice to use the name of the current theory (with ending
boehmes@36898
   257
@{text ".certs"} instead of @{text ".thy"}) as the certificates file.
wenzelm@50317
   258
Certificate files should be used at most once in a certain theory context,
wenzelm@50317
   259
to avoid race conditions with other concurrent accesses.
boehmes@36898
   260
*}
boehmes@36898
   261
boehmes@36898
   262
declare [[ smt_certificates = "" ]]
boehmes@36898
   263
boehmes@36898
   264
text {*
blanchet@47152
   265
The option @{text smt_read_only_certificates} controls whether only
blanchet@47152
   266
stored certificates are should be used or invocation of an SMT solver
blanchet@47152
   267
is allowed.  When set to @{text true}, no SMT solver will ever be
boehmes@36898
   268
invoked and only the existing certificates found in the configured
boehmes@36898
   269
cache are used;  when set to @{text false} and there is no cached
boehmes@36898
   270
certificate for some proposition, then the configured SMT solver is
boehmes@36898
   271
invoked.
boehmes@36898
   272
*}
boehmes@36898
   273
blanchet@47152
   274
declare [[ smt_read_only_certificates = false ]]
boehmes@36898
   275
boehmes@36898
   276
boehmes@36898
   277
boehmes@36898
   278
subsection {* Tracing *}
boehmes@36898
   279
boehmes@36898
   280
text {*
boehmes@40424
   281
The SMT method, when applied, traces important information.  To
boehmes@40424
   282
make it entirely silent, set the following option to @{text false}.
boehmes@40424
   283
*}
boehmes@40424
   284
boehmes@40424
   285
declare [[ smt_verbose = true ]]
boehmes@40424
   286
boehmes@40424
   287
text {*
boehmes@36898
   288
For tracing the generated problem file given to the SMT solver as
boehmes@36898
   289
well as the returned result of the solver, the option
boehmes@36898
   290
@{text smt_trace} should be set to @{text true}.
boehmes@36898
   291
*}
boehmes@36898
   292
boehmes@36898
   293
declare [[ smt_trace = false ]]
boehmes@36898
   294
boehmes@36898
   295
text {*
boehmes@40162
   296
From the set of assumptions given to the SMT solver, those assumptions
boehmes@40162
   297
used in the proof are traced when the following option is set to
boehmes@40162
   298
@{term true}.  This only works for Z3 when it runs in non-oracle mode
boehmes@40162
   299
(see options @{text smt_solver} and @{text smt_oracle} above).
boehmes@36898
   300
*}
boehmes@36898
   301
boehmes@40162
   302
declare [[ smt_trace_used_facts = false ]]
boehmes@39298
   303
boehmes@36898
   304
boehmes@36898
   305
huffman@36902
   306
subsection {* Schematic rules for Z3 proof reconstruction *}
boehmes@36898
   307
boehmes@36898
   308
text {*
boehmes@36898
   309
Several prof rules of Z3 are not very well documented.  There are two
boehmes@36898
   310
lemma groups which can turn failing Z3 proof reconstruction attempts
boehmes@36898
   311
into succeeding ones: the facts in @{text z3_rule} are tried prior to
boehmes@36898
   312
any implemented reconstruction procedure for all uncertain Z3 proof
boehmes@36898
   313
rules;  the facts in @{text z3_simp} are only fed to invocations of
boehmes@36898
   314
the simplifier when reconstructing theory-specific proof steps.
boehmes@36898
   315
*}
boehmes@36898
   316
boehmes@36898
   317
lemmas [z3_rule] =
boehmes@36898
   318
  refl eq_commute conj_commute disj_commute simp_thms nnf_simps
boehmes@36898
   319
  ring_distribs field_simps times_divide_eq_right times_divide_eq_left
boehmes@36898
   320
  if_True if_False not_not
boehmes@36898
   321
boehmes@36898
   322
lemma [z3_rule]:
boehmes@44488
   323
  "(P \<and> Q) = (\<not>(\<not>P \<or> \<not>Q))"
boehmes@44488
   324
  "(P \<and> Q) = (\<not>(\<not>Q \<or> \<not>P))"
boehmes@44488
   325
  "(\<not>P \<and> Q) = (\<not>(P \<or> \<not>Q))"
boehmes@44488
   326
  "(\<not>P \<and> Q) = (\<not>(\<not>Q \<or> P))"
boehmes@44488
   327
  "(P \<and> \<not>Q) = (\<not>(\<not>P \<or> Q))"
boehmes@44488
   328
  "(P \<and> \<not>Q) = (\<not>(Q \<or> \<not>P))"
boehmes@44488
   329
  "(\<not>P \<and> \<not>Q) = (\<not>(P \<or> Q))"
boehmes@44488
   330
  "(\<not>P \<and> \<not>Q) = (\<not>(Q \<or> P))"
boehmes@44488
   331
  by auto
boehmes@44488
   332
boehmes@44488
   333
lemma [z3_rule]:
boehmes@36898
   334
  "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
boehmes@36898
   335
  "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
boehmes@36898
   336
  "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
boehmes@44488
   337
  "(True \<longrightarrow> P) = P"
boehmes@44488
   338
  "(P \<longrightarrow> True) = True"
boehmes@44488
   339
  "(False \<longrightarrow> P) = True"
boehmes@44488
   340
  "(P \<longrightarrow> P) = True"
boehmes@36898
   341
  by auto
boehmes@36898
   342
boehmes@36898
   343
lemma [z3_rule]:
boehmes@36898
   344
  "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
boehmes@36898
   345
  by auto
boehmes@36898
   346
boehmes@36898
   347
lemma [z3_rule]:
boehmes@44488
   348
  "(\<not>True) = False"
boehmes@44488
   349
  "(\<not>False) = True"
boehmes@44488
   350
  "(x = x) = True"
boehmes@44488
   351
  "(P = True) = P"
boehmes@44488
   352
  "(True = P) = P"
boehmes@44488
   353
  "(P = False) = (\<not>P)"
boehmes@44488
   354
  "(False = P) = (\<not>P)"
boehmes@36898
   355
  "((\<not>P) = P) = False"
boehmes@36898
   356
  "(P = (\<not>P)) = False"
boehmes@44488
   357
  "((\<not>P) = (\<not>Q)) = (P = Q)"
boehmes@44488
   358
  "\<not>(P = (\<not>Q)) = (P = Q)"
boehmes@44488
   359
  "\<not>((\<not>P) = Q) = (P = Q)"
boehmes@36898
   360
  "(P \<noteq> Q) = (Q = (\<not>P))"
boehmes@36898
   361
  "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
boehmes@36898
   362
  "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
boehmes@36898
   363
  by auto
boehmes@36898
   364
boehmes@36898
   365
lemma [z3_rule]:
boehmes@36898
   366
  "(if P then P else \<not>P) = True"
boehmes@36898
   367
  "(if \<not>P then \<not>P else P) = True"
boehmes@36898
   368
  "(if P then True else False) = P"
boehmes@36898
   369
  "(if P then False else True) = (\<not>P)"
boehmes@44488
   370
  "(if P then Q else True) = ((\<not>P) \<or> Q)"
boehmes@44488
   371
  "(if P then Q else True) = (Q \<or> (\<not>P))"
boehmes@44488
   372
  "(if P then Q else \<not>Q) = (P = Q)"
boehmes@44488
   373
  "(if P then Q else \<not>Q) = (Q = P)"
boehmes@44488
   374
  "(if P then \<not>Q else Q) = (P = (\<not>Q))"
boehmes@44488
   375
  "(if P then \<not>Q else Q) = ((\<not>Q) = P)"
boehmes@36898
   376
  "(if \<not>P then x else y) = (if P then y else x)"
boehmes@44488
   377
  "(if P then (if Q then x else y) else x) = (if P \<and> (\<not>Q) then y else x)"
boehmes@44488
   378
  "(if P then (if Q then x else y) else x) = (if (\<not>Q) \<and> P then y else x)"
boehmes@44488
   379
  "(if P then (if Q then x else y) else y) = (if P \<and> Q then x else y)"
boehmes@44488
   380
  "(if P then (if Q then x else y) else y) = (if Q \<and> P then x else y)"
boehmes@44488
   381
  "(if P then x else if P then y else z) = (if P then x else z)"
boehmes@44488
   382
  "(if P then x else if Q then x else y) = (if P \<or> Q then x else y)"
boehmes@44488
   383
  "(if P then x else if Q then x else y) = (if Q \<or> P then x else y)"
boehmes@44488
   384
  "(if P then x = y else x = z) = (x = (if P then y else z))"
boehmes@44488
   385
  "(if P then x = y else y = z) = (y = (if P then x else z))"
boehmes@44488
   386
  "(if P then x = y else z = y) = (y = (if P then x else z))"
boehmes@36898
   387
  by auto
boehmes@36898
   388
boehmes@36898
   389
lemma [z3_rule]:
boehmes@44488
   390
  "0 + (x::int) = x"
boehmes@44488
   391
  "x + 0 = x"
boehmes@44488
   392
  "x + x = 2 * x"
boehmes@44488
   393
  "0 * x = 0"
boehmes@44488
   394
  "1 * x = x"
boehmes@44488
   395
  "x + y = y + x"
boehmes@44488
   396
  by auto
boehmes@44488
   397
boehmes@44488
   398
lemma [z3_rule]:  (* for def-axiom *)
boehmes@36898
   399
  "P = Q \<or> P \<or> Q"
boehmes@36898
   400
  "P = Q \<or> \<not>P \<or> \<not>Q"
boehmes@36898
   401
  "(\<not>P) = Q \<or> \<not>P \<or> Q"
boehmes@36898
   402
  "(\<not>P) = Q \<or> P \<or> \<not>Q"
boehmes@36898
   403
  "P = (\<not>Q) \<or> \<not>P \<or> Q"
boehmes@36898
   404
  "P = (\<not>Q) \<or> P \<or> \<not>Q"
boehmes@36898
   405
  "P \<noteq> Q \<or> P \<or> \<not>Q"
boehmes@36898
   406
  "P \<noteq> Q \<or> \<not>P \<or> Q"
boehmes@36898
   407
  "P \<noteq> (\<not>Q) \<or> P \<or> Q"
boehmes@36898
   408
  "(\<not>P) \<noteq> Q \<or> P \<or> Q"
boehmes@36898
   409
  "P \<or> Q \<or> P \<noteq> (\<not>Q)"
boehmes@36898
   410
  "P \<or> Q \<or> (\<not>P) \<noteq> Q"
boehmes@36898
   411
  "P \<or> \<not>Q \<or> P \<noteq> Q"
boehmes@36898
   412
  "\<not>P \<or> Q \<or> P \<noteq> Q"
boehmes@44488
   413
  "P \<or> y = (if P then x else y)"
boehmes@44488
   414
  "P \<or> (if P then x else y) = y"
boehmes@44488
   415
  "\<not>P \<or> x = (if P then x else y)"
boehmes@44488
   416
  "\<not>P \<or>  (if P then x else y) = x"
boehmes@44488
   417
  "P \<or> R \<or> \<not>(if P then Q else R)"
boehmes@44488
   418
  "\<not>P \<or> Q \<or> \<not>(if P then Q else R)"
boehmes@44488
   419
  "\<not>(if P then Q else R) \<or> \<not>P \<or> Q"
boehmes@44488
   420
  "\<not>(if P then Q else R) \<or> P \<or> R"
boehmes@44488
   421
  "(if P then Q else R) \<or> \<not>P \<or> \<not>Q"
boehmes@44488
   422
  "(if P then Q else R) \<or> P \<or> \<not>R"
boehmes@44488
   423
  "(if P then \<not>Q else R) \<or> \<not>P \<or> Q"
boehmes@44488
   424
  "(if P then Q else \<not>R) \<or> P \<or> R"
boehmes@36898
   425
  by auto
boehmes@36898
   426
boehmes@37124
   427
boehmes@37124
   428
hide_type (open) pattern
boehmes@41281
   429
hide_const Pattern fun_app term_true term_false z3div z3mod
boehmes@41280
   430
hide_const (open) trigger pat nopat weight
boehmes@37124
   431
boehmes@36898
   432
end